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

Question

在伊莎贝尔中，命令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}))›

这将打印

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

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

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

isabelle