Re: [isabelle] Giving a symbolic name to a tactical



Peter Lammich wrote:
Hi all,

In my proof, at several positions, there occurs a step like this:
     apply (
       (intro exI conjI),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps, (rule compress_u_a[THEN tranclp_into_rtranclp] | rule elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN tranclp_into_rtranclp] ))+,
       (rule rtranclp.intros),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps, (rule compress_u_a[THEN tranclp_into_rtranclp] | rule elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN tranclp_into_rtranclp] ))+,
       (simp add: Un_ac)
     )

And I fear this step will even get longer in the future, but it's always the same step. Is there a way to give this a symbolic name once, and then refer to the step via this symbolic name ?

If the only way of doing so should be by converting this to an ML-tactical [As indicated in Christian Urban's mail of 2007-09-03], then regard this mail as a feature request:
 A nice feature would be:

   define my_tactical = tactical_expression

   and then use:

   apply my_tactical
   instead of

   apply tactical_expression



Best regards
 Peter


Peter,

This is exactly the sort of thing that is readily available in Standard ML, without requesting any new feature. In fact, ML was originally conceived to develop proof tactics in the LCF theorem prover (from which, I gather, HOL and Isabelle originated). In fact, HOL was first recommended to me, many years ago, on the grounds that it used a "real language" as its user interface language.

The features designed into ML made it become also a general purpose functional programming language as well as a user interaction language for theorem provers. It remains a highly effective language for combining tactics in various ways.

Regards,

Jeremy


<http://en.wikipedia.org/wiki/LCF_theorem_prover>










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