isabelle - 在Isabelle中调试ML证明(Debugging ML proofs in Isabelle)

Question

I wrote the following ML code:

(我编写了以下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)
?

corresponding to the following Isar proof:

(对应于以下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?)

The ML version of it is not working for some reason?

(由于某些原因，它的ML版本无法正常工作吗？)

How could I debug this?

(我该如何调试呢？)

There is the print_tac tactic, but it only acccepts strings, while I would like to print the actual subgoal after each tactic is applied.

(有print_tac策略，但它只接受字符串，而我想在应用每种策略后打印实际的子目标。)

  ask by Rodrigo translate from so

Answer 1

I believe that the problem is related to the type inference: in the antiquotation @{cprop "z1' = (x1',y1')"} there is no simple way to infer the desired type 'a of the variables x1' and y1' automatically because each antiquotation in the list of assumptions is pre-processed independently of other antiquotations before being passed to add_assumes .

(我认为问题与类型推断有关：在反引号@{cprop "z1' = (x1',y1')"} ，没有简单的方法来推断变量x1'和y1'的所需类型'a之所以y1'自动进行，是因为假设列表中的每个反引号在传递给add_assumes之前都独立于其他反引号进行了add_assumes 。)

Therefore, the most general type is inferred.

(因此，可以推断出最通用的类??型。)

You merely need to provide the type of each variable explicitly, eg @{cprop "z1' = (x1'::'a,y1'::'a)"} and the tactic should work.

(您只需要显式地提供每个变量的类型，例如@{cprop "z1' = (x1'::'a,y1'::'a)"} ，该策略应该起作用。)

However, in my view, a better solution would be to define the variables such as x1' and y1' directly in ML with the explicit type assignment, eg val x1t = Free("x1", T) , where T is the desired type 'a .

(但是，我认为，更好的解决方案是直接在ML中使用显式类型分配定义变量，例如x1'和y1' ，例如val x1t = Free("x1", T) ，其中T是所需的类型'a 。)