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



On Thu, 18 Feb 2010, Peter Lammich wrote:

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

Not really. Isar was introduced to overcome adhoc "scripting" of proofs, and there is a carefully chosen terminology to emphasize this ("proof text" and "proof method", instead of the more primitive "proof script" and "tactic"). This was just one further step to less operational detail compared to old-style ML tactics of classic Isabelle/HOL, which was already much more stylized in 1998 than original HOL with its huge numbers of small tactics and tacticals.

Comparing formalizations from these different eras, my general impression is that people now achieve more with the more abstract means of Isar, and the results are checked faster and easier to maintain. Nonetheless, there is still a lack of serious interactive proof development support, say some kind of "prover IDE" that deserves this name.


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> *} "..."

Designing (and implementing) Isar proof methods needs some care, this is not for quick scripting.

First of all, in many situations, the intended goal refinement can be achieve more declaratively, e.g. by deriving suitable compound rules, or feeding certain rules to simp/fast/blast/auto etc. with intro/elim/iff declarations.

If you really need to define a goal refinement macro, you can actually
give a name to a tactic (not a complex method expression as in the example above). E.g. like this:

ML {* val my_tac = REPEAT o (rtac @{thm foo} THEN' (TRY o atac)) *}

and use it later via the "tactic" method, e.g. like this:

lemma True
  apply (tactic {* my_tac 1 *})


This still looks a bit scary, but the overhead for argument parsing is avoided.


If you explain your application more specifically, it is easier to say what is really needed.


	Makarius





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