[isabelle] method vs tactic behaviour



In Isabelle/HOL (using the repo version of Isabelle, as at a948ee5fb5f4) I was able to prove the following lemma, as an initial prototype while writing a tactic:

lemma H23_to_H24_e :
  "â R. H23 â (âH23; H24â â R) â R"
apply (unfold H23_def, unfold H24_def)
apply (erule TabDec, assumption)               (*1*)
done

I then started refining the prototype into tactic code by changing line (*1*) into

   apply (tactic {*HEADGOAL (eresolve_tac @{context} @{thms TabDec})*}, assumption)         (*2*)

and the lemma still went through. I refined it further by changing (*2*) into

  apply (tactic {*HEADGOAL (eresolve_tac @{context} @{thms TabDec} THEN' atac)*})           (*3*)

but then got "Failed to apply proof method". This was surprising, since it seemed to me that the tactic in line (*3*) specified the same thing as in line (*2*), but evidently this is not the case.

I then changed line (*3*) into the following three lines:

  apply (tactic {*HEADGOAL (eresolve_tac @{context} @{thms TabDec})*})
  back
  apply assumption       (*4*)

and the proof succeeded once again, but when I changed line (*4*) into

  apply (tactic {*HEADGOAL atac*})      (*5*)

the proof did not succeed.

Does anybody know why the result when using line (*4*) differs from that when using line (*5*), and if this also explains the difference observed when using lines (*1*), (*2*) and (*3*)?

Best wishes,
Nik








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.