Re: [isabelle] Giving a name to a tactics-expression




Peter Lammich wrote:
Peter Lammich schrieb:
Is there a way to give a short name to a complex tactic-expression. I have, e.g., the following pattern that I frequently use.
 apply (((erule (1) lemma1)+)?,erule lemma2,simp)+

Trying to translate it to ML, I cannot find any ML-tactics equivalent for "erule (1)". There is only etac, but this seems to have no number of additional premises.

I was under the impression that erule (1) was just (erule,assumption) which then would translate to "etac some_rule THEN' atac" in ML.

In any case, check out Christian's example from the Isabelle Developer Workshop, where he shows an example translation from apply-style proof script to ML method: http://tphols.in.tum.de/IDW/CU-Ex1.thy

And also look at Makarius's slides/examples on proof methods. Available here:
http://tphols.in.tum.de/idw.html

I've found these practical examples have helped me much more than the reference manual. Once I understood what the point of the exercise was, the reference manual started to help instead of confuse.

Good luck!

Rafal Kolanski.






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