Email Gateway (Aug 18 2022 at 10:18): Email Gateway (Aug 18 2022 at 10:18):From: Christian Urban <urbanc@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 thatapply (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
Last updated: May 03 2024 at 08:18 UTC