*To*: Peter Chapman <pc at cs.st-and.ac.uk>*Subject*: [isabelle] Renaming Tacticals*From*: Christian Urban <urbanc at in.tum.de>*Date*: Fri, 9 Mar 2007 14:36:48 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <3671E6B9-2FE4-4C77-9AC4-1FDC685F6399@cs.st-and.ac.uk>*References*: <3671E6B9-2FE4-4C77-9AC4-1FDC685F6399@cs.st-and.ac.uk>*Reply-to*: urbanc at in.tum.de

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 example 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 Christian

**Follow-Ups**:**[isabelle] Tactic Emulation***From:*Peter Chapman

**References**:**[isabelle] Renaming Tacticals***From:*Peter Chapman

- Previous by Date: [isabelle] Lectureship in automated verification at Oxford
- Next by Date: [isabelle] Automated Reasoning Workshop 2007 - Final CFP
- Previous by Thread: [isabelle] Renaming Tacticals
- Next by Thread: [isabelle] Tactic Emulation
- Cl-isabelle-users March 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list