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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and