Re: [isabelle] intro and types



On Sun, 14 Feb 2010, Christian Sternagel wrote:

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.

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





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