I wrote the following ML code:
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:
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? 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.
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. Therefore, the most general type is inferred. You merely need to provide the type of each variable explicitly, e.g. @{cprop "z1' = (x1'::'a,y1'::'a)"} and the tactic should work. 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, e.g. val x1t = Free("x1", T), where T is the desired type 'a.