在 Isabelle 中，如何以其他格式（如 S-expression、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))))