[isabelle] Tactic Emulation



Thanks Christian

This sounds like the kind of thing I want to do, but I've hit a snag in implementing your suggestion of writing the tactics in ML and then using this directly in Isar.

Say I have a lemma " |- A --> A --> A --> A", then using the Isar method of doing things, I use

apply ((rule impr)+)?

which returns

Subgoal:

A, A, A |- A

as expected.  However, if I use the direct tactic from Isabelle

apply (tactic {* REPEAT (rtac impr 1) *} )

I simply get back the original goal; the rule fails to be applied even once. This was confirmed when I tried

apply (tactic {* rtac impr 1 *} )

which fails. After scouring the manuals for both Isar (Appendix B: Converting between Isabelle and Isar) and Isabelle (Chapters 3 and 4), I cannot figure out why the two representations do not have the same behaviour. If it is important, the theorems are declared in a file called G3cp.thy, which is included in the file where I am actually performing the calculations, G3cpExamples.thy.

Thanks

Peter




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