Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] intro and types


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 12:29 UTC