在Isabelle中，如何以其他格式(如S-表达式、Json格式..)打印状态(即要证明的子目标)

Question

在Isabelle中，命令print_state可以打印需要证明的当前目标。然而，我希望目标能够以其他易于处理的格式打印出来，比如S表达式和抽象语法树。

默认的打印模式不包括这种格式，所以我想知道如何修改Isabelle中的ML文件。或者更具体地说，当前目标是如何通过打印的。我很高兴它在被传递到打印之前是ML文件中的AST格式，但我很难找到变量是如何传输的。有人知道怎么解决这个问题吗？

Answer 1

下面是一个使用ML将当前目标打印为S-Expr的示例(基于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}))›

这将打印

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))))