[isabelle] intro and types



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





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