Email Gateway (Aug 18 2022 at 14:43): Email Gateway (Aug 18 2022 at 14:43):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there!
I am currently reading through some Isabelle/HOL formalizations that
I've been doing over the last few years. Doing that, I discovered the
following: It is sometimes convenient to have specialized rules for more
specific types. For example I use
lemma subsetI2: assumes "!!x y. (x,y) : S ==> (x,y) : T" shows "S <= T"
rather often at the beginning of some proof (usually about binary
relations). That is, a corresponding proof starts as follows:
proof (rule subsetI2)
What I would like to have instead is
proof
Now, declaring subsetI2 as 'intro' doesn't help. Still, the more general
rule subsetI is used. So my question is, how do I specify, when several
rules would be applicable, which one is used by the 'rule' method? The
same problem arises, when there are several introduction rules for some
constant. As far as I figured out, as long as the types are at the same
level (in contrast to the above subsetI2, where the original rule can be
applied on 'a set, but subsetI2 can only be applied on ('a * 'a)set),
the order in which rules are declared as 'intro' does matter. Is that
correct or was it just a coincidence in my case?
best regards
chris
Email Gateway (Aug 18 2022 at 14:43):From: Makarius <makarius@sketis.net>
In principle, later rule declarations take precedence over earlier ones --
at least that is the usual policy that tools should follow.
For the "rule" method the situation is more complex, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009-1/src/Provers/classical.ML#l931
Rules from the Pure context and the Classical reasoner are concatenated in
a certain order -- both have additional ways to specifiy extra priorities,
notably via "!" and "?" qualifiers.
Since the "!" versions of Pure are tried first, but do not influence the
automated tools, declaring subsetI2 as "Pure.intro!" should do the job.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC