In Isabelle, how to print the state (i.e. subgoals to prove) in other formats (like S-expression, Json format...)?

Question

In Isabelle, the command print_state can print the current goals needed to be proved. However, I want the goals to to be printed in other easy-to-tackle formats like S-expressions and abstract syntax tree.

The default printing mode doesn't include this kind of format, so I am wondering how to modify the ML file inside Isabelle. Or more specific, how does the current goals pass to be printed. I am pretty it is in AST format inside the ML files before being passed to be printed, but I was having a hard time finding how the variables are transferred. Does anyone know how to solve this?

What exactly you want is a bit unclear, but no safety-breaking modifications of the source files are necessary. You can directly inspect the ML representation of a goal with `ML_val "@{Isar.goal}"` at any point in a proof. — Josh, Jul 20 '20 at 12:54
it would be nice to extend this question to request for `json` format that is usually leads to a nice alternative format. — Charlie Parker, Jul 22 '20 at 21:09

score 4 · Accepted Answer · answered Jul 20 '20 at 17:57

Here is an example of using ML to print the current goal as S-Expr (building on the comment by Josh Chen).

ML ‹
fun print_sep sep xs = 
  case xs of
    [] => ""
  | [x] => x
  | x::ys => x ^ sep ^ print_sep sep ys

fun sort_to_sexpr (s: sort) = 
  print_sep " " s

fun typ_to_sexpr (t: typ) = 
  case t of
     Type (n, []) => "(type " ^ n ^ ")"
   | Type (n, ts) => "(type " ^ n ^ " " ^ print_sep " " (map typ_to_sexpr ts) ^ ")"
   | TFree (n, s) => "(tfree " ^ n ^ " " ^ sort_to_sexpr s ^ ")"
   | TVar  (n, s) => "(tfree " ^ @{make_string} n ^ " " ^ sort_to_sexpr s ^ ")"


fun to_sexpr (t: term) = 
  case t of
     f $ x => "(apply " ^ to_sexpr f ^ " " ^ to_sexpr x ^ ")"
   | Const (n, t) => "(const " ^ n ^ " " ^ typ_to_sexpr t  ^ ")"
   | Free (n, t) => "(free " ^ n ^ " " ^ typ_to_sexpr t  ^ ")"
   | Var (n, t) => "(var " ^  @{make_string} n ^ " " ^ typ_to_sexpr t  ^ ")"
   | Bound n => "(bound " ^ @{make_string} n ^ ")"
   | Abs (n, t, e) => "(bound " ^ n ^ " " ^ typ_to_sexpr t ^ " " ^ to_sexpr e ^   ")"

fun to_sexpr_untyped (t: term) = 
  case t of
     f $ x => "(apply " ^ to_sexpr_untyped f ^ " " ^ to_sexpr_untyped x ^ ")"
   | Const (n, _) => "(const " ^ n ^  ")"
   | Free (n, _) => "(free " ^ n ^ ")"
   | Var (n, _) => "(var " ^  @{make_string} n ^ ")"
   | Bound n => "(bound " ^ @{make_string} n ^ ")"
   | Abs (n, _, e) => "(bound " ^ n ^ " " ^ to_sexpr_untyped e ^   ")"

›

lemma "P ∧ Q ⟶ P"
  ML_val ‹to_sexpr (Thm.concl_of (#goal @{Isar.goal}))›
  ML_val ‹to_sexpr_untyped (Thm.concl_of (#goal @{Isar.goal}))›

This will print

(apply (const Pure.prop (type fun (type prop) (type prop))) (apply (const HOL.Trueprop (type fun (type HOL.bool) (type prop))) (apply (apply (const HOL.implies (type fun (type HOL.bool) (type fun (type HOL.bool) (type HOL.bool)))) (apply (apply (const HOL.conj (type fun (type HOL.bool) (type fun (type HOL.bool) (type HOL.bool)))) (free P (type HOL.bool))) (free Q (type HOL.bool)))) (free P (type HOL.bool)))))
(apply (const Pure.prop) (apply (const HOL.Trueprop) (apply (apply (const HOL.implies) (apply (apply (const HOL.conj) (free P)) (free Q))) (free P))))

also, how do you know this completely covers all constructor cases? — Charlie Parker, Jul 21 '20 at 22:06
I modified the code from Peter Zeller a bit and it worked fine for me currently, but I am still doing some tests. — Q.Yang, Jul 21 '20 at 22:50
I don't see a big problem in changing the code to Json, it would just be a bit more verbose. You can be sure that this covers all constructor cases since PolyML will give you a warning if you miss one in a `case` construct. — Peter Zeller, Jul 22 '20 at 13:30

In Isabelle, how to print the state (i.e. subgoals to prove) in other formats (like S-expression, Json format...)?

1 Answers1