在 Isabelle 中调试 ML 证明

Question

我写了下面的ML代码：

lemma fstI: "x = (y, z) ⟹ y = fst x"
  by simp

ML ‹
val ctxt0 = @{context};
val ctxt = ctxt0;
val (_,ctxt) = Variable.add_fixes ["z1'","x1'","y1'","x1", "y1", "x2", "y2"] ctxt;
val (assms,ctxt) = Assumption.add_assumes 
                       [@{cprop "z1' = (x1',y1')"},@{cprop "z1' = ext_add (x1,y1) (x2,y2)"}] ctxt;
val th1 = @{thm fstI}  OF  [(nth assms 0)]
val th2 = Thm.instantiate' [SOME @{ctyp "'a"}] [SOME @{cterm "fst::'a×'a ⇒ 'a"}] (@{thm arg_cong} OF [(nth assms 1)])
val x1'_expr = Goal.prove ctxt [] []
                               @{prop "x1' = fst (ext_add (x1,y1) (x2,y2))"}
                          (fn _ => EqSubst.eqsubst_tac ctxt [1] [th1] 1
                                  THEN EqSubst.eqsubst_tac ctxt [1] [th2] 1
                                  THEN simp_tac ctxt 1)
›

对应以下Isar证明：

lemma taylored_assoc: 
  assumes "z1' = (x1',y1')"
          "z1' = ext_add (x1,y1) (x2,y2)" "z3' = add (x2,y2) (x3,y3)" 
  shows "x1' = fst (ext_add (x1,y1) (x2,y2))"   
  by(tactic ‹EqSubst.eqsubst_tac @{context} [1] [@{thm fstI[OF assms(1)]}] 1
                THEN EqSubst.eqsubst_tac @{context} [1] [@{thm arg_cong[OF assms(2), of fst]}] 1
                THEN simp_tac @{context} 1›)

它的 ML 版本出于某种原因无法使用？我该如何调试呢？有 print_tac 策略，但它只接受字符串，而我想在应用每个策略后打印实际的子目标。

Answer 1

我认为问题与类型推断有关：在反引号 @{cprop "z1' = (x1',y1')"} 中没有简单的方法来推断变量 x1' 和 [ 的所需类型 'a =13=] 自动进行，因为假设列表中的每个反引号在传递给 add_assumes 之前都独立于其他反引号进行了预处理。因此，推断出最一般的类型。您只需要明确提供每个变量的类型，例如@{cprop "z1' = (x1'::'a,y1'::'a)"} 并且该策略应该有效。但是，在我看来，更好的解决方案是直接在 ML 中使用显式类型分配定义 x1' 和 y1' 等变量，例如val x1t = Free("x1", T)，其中 T 是所需的类型 'a。

在 Isabelle 中调试 ML 证明

Debugging ML proofs in Isabelle

ml

isabelle