[isabelle] Renaming Tacticals

Hi Peter,

I am not an expert in this but here is some information.

Peter Chapman writes:
 > Hi
 > I have a series of methods to apply which looks something like this
 > apply (rule ((basic)+)?, ((conjL)+)?, ((disjR)+)?, ...)
 > Is there anyway that I can rename the above to something, say  
 > bigRule, so that
 > apply (rule bigRule)

Yes, this can be done, but must be done on the ML-level.

Judging from your apply-line, you want to apply rule basic as often as 
possible (possibly not at all), after this you want to do the same 
with rule conjL, and so on. To keep things in line with Isabelle-
terminology (and for understanding the documentation), let's call 
basic, conjL, disjR.... *theorems*. I guess they are axioms or lemmas 
in your proof-script and such things are in Isabelle called 
theorems, or short thm ;o)
 > executes the first line?  I had an attempt using ML as
 >   ML {* fun PETER (basic, impR, impL, conjL, disjR, false, conjR,  
 > disjL) = REPEAT (EVERY [basic, impR, impL, conjL, disjR, false,  
 > conjR, disjL]); *}

This already goes in the right direction. You have to write what
is called in Isabelle a tactical. EVERY and REPEAT are building
blocks for tacticals. This is described in chapter 4 of the Isabelle-
reference and also in 3.2 (look at the Isabelle webpage). First 
applying a theorem, like basic and disjL, is done with rtac. For 
example, for 

    lemma "A /\ B"
    apply(rule conjI)    

you can also do the following 

    lemma "A /\ B"
    apply(tactic {* rtac conjI 1 *})

to achieve pretty much the same on the ML-level (conjI is the theorem
that is applied, 1 refers to the first subgoal and "tactic {* *}" is a 
wrapper to call some ML-code from a proof-script). 

You want to apply "rtac conjI 1" as often as possible including
the possibility of not at all. For this you have to use REPEAT. For

    lemma "(A /\ B) /\ C"
    apply(tactic {* REPEAT (rtac conjI 1) *})

applies theorem conjI twice producing the goals A, B and C. Next you
want to do such things with a sequence of theorems. For this you
can use EVERY (this takes a list of tactics and applies them one
after the other. For example

    lemma "(A \/ B) /\ C"
    apply(tactic {* EVERY [REPEAT (rtac conjI 1), REPEAT (rtac disjI2 1)] *})

first takes apart the conjunction and then applies theorem disjI2,
i.e. produces goals B and C. With a bit of ML-hackery you can 
scale this up to your example and introduce some bigrule-shorthand. 

However, from what you are writing I guess you just want to try out
some rules on a goal and take it apart when a safe rule applies;
and repeat this process recursively with all the subgoals. This is not 
quite what your apply-line achieves (because of the imposed ordering). 
If this is what you want, I would write 

    REPEAT (FIRST [rtac conjI1 1,.....])

Hope this is helpful. The code above only works on the first subgoal. 
You might, however, like to apply your tactical to all subgoals that
have arisen in this process of taking goals apart. This can all be done 
with tacticals. However, be aware that writing tacticals can be a bit 
of a black art. ;o) Good luck


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