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



On Mon, 15 Sep 2008, Peter Lammich wrote:

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

Just to get the terminology right:

  * A tactic is a function that maps a goal state to a lazy sequence of 
    potential successor state, with ML type tactic = thm -> thm Seq.seq;
    tactics with explicit sub-goal addressing are also quite common, and 
    have type int -> tactic unsurprisingly.

  * A tactical is a combinator for tactics, e.g. THEN, ORELSE, REPEAT.

  * A proof method (in Isar) is a tactic that refers to an explicit proof 
    context and a list of immediate facts to be "used" in the goal 
    refinement.

    The ML type is essentially Proof.context -> thm list -> tactic.
    Methods handle goal addressing internally.  "Methodicals" are limited 
    to regular expression combinators: ",", "|", "+".    

What you descrive above is a way to define your own methods.  In 
Isabelle/Isar almost everything is "defined" in that sense anyway, and you 
can introduce methods on your own.  See the 'method_setup' command in the 
isar-ref manual or the existing theory sources.

When implementing a method, the implementation body works with ML tactics 
and tacticals, wrapped into method syntax.


	Makarius





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