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



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. I have, 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 boilerplate than the above tactics-expression, and much more complicated to read and write if one does not know the ML-interface by heart> *} "..."

Is there a way without manually translating the above Tactics-expression to ML code?

Basically, it seems that methods can be combined in these sorts of ways, but it is hidden in the source code, which is essentially undocumented.
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

The other way, it seems I never finished figuring it out (I looked at this sort of stuff some years ago, and pretty much gave up on it, so I decided to stick to using tactics directly - which are all described in the Reference Manual).

The problem may be that a Method.text seems to be applied directly, not by turning it into a method, see

> 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)

(Incidentally all the above code is Isabelle2007, some of it also changed to make some functions visible).

If you can use a compound tactic, it would be much easier.
Method.erule is based on Tactic.eresolve_tac, plus some other stuff, including doing something with facts. If you can do without the other stuff, just use tactics and the tactic combinators - so then it would look like

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

Jeremy




Regards and thanks,
 Peter









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