*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Giving a name to a tactics-expression*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 19 Feb 2010 12:43:30 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4B7D7698.40207@uni-muenster.de>*References*: <4B7D7698.40207@uni-muenster.de>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Peter Lammich wrote:

Hi all. [Apologies if this question already was on this list some time ago]Is there a way to give a short name to a complex tactic-expression. Ihave, e.g., the following pattern that I frequently use.apply (((erule (1) lemma1)+)?,erule lemma2,simp)+ Lemma1 and lemma2 are two (fixed) lemmas proven in my theory. Instead, I would like to write something like: define_method my_method = (((erule (1) lemma1)+)?,erule lemma2,simp)+ and later: apply (my_method) However, the only way I know is something like:method_setup my_method = {* <Some scary ML-code, much more boilerplatethan the above tactics-expression, and much more complicated to readand write if one does not know the ML-interface by heart> *} "..."Is there a way without manually translating the aboveTactics-expression to ML code?

erule is Method.erule ; val it = fn : int -> Thm.thm list -> Method.method combining methods uses > Method.Then ; val it = fn : Method.text list -> Method.text > Method.Try ; val it = fn : Method.text -> Method.text > Method.Repeat1 ; val it = fn : Method.text -> Method.text You then have to work out how to get between a method and a Method.text One way would use > Method.Basic ; val it = fn : (ProofContext.context -> Method.method) -> Method.text

> Proof.apply ; val it = fn : Method.text -> Proof.state -> Proof.state Seq.seq (which uses Method.apply ; val it = fn : Method.method -> Thm.thm list -> RuleCases.tactic but unfortunately not by creating a single compound method en route)

If you can use a compound tactic, it would be much easier.

EVERY' [(TRY o REPEAT1 o eatac lemma1 1), etac lemma2, Simp_tac ] 1 ; Jeremy

Regards and thanks, Peter

**Follow-Ups**:**Re: [isabelle] Giving a name to a tactics-expression***From:*Makarius

**References**:**[isabelle] Giving a name to a tactics-expression***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Giving a name to a tactics-expression
- Next by Date: Re: [isabelle] Giving a name to a tactics-expression
- Previous by Thread: Re: [isabelle] Giving a name to a tactics-expression
- Next by Thread: Re: [isabelle] Giving a name to a tactics-expression
- Cl-isabelle-users February 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list