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?

Answer 1

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

1. (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)))))
2. (apply (const Pure.prop) (apply (const HOL.Trueprop) (apply (apply (const HOL.implies) (apply (apply (const HOL.conj) (free P)) (free Q))) (free P))))