Re: [isabelle] Lattices and syntactic classes
On Wed, 7 Sep 2011, Florian Haftmann wrote:
But note that to simplify your instantiation proofs you can
prove a specific introduction rule for P ==> OFCLASS('a, left_inf) where
P is the body of your left_inf class.
A further aspect: Pure.intro declaration have precedence over the intro
classes method, as shown in the folling silly example:
lemma nonsense [Pure.intro]:
"False \<Longrightarrow> OFCLASS('a, default_class)"
instance bool :: default
By declaring your customary class introduction rules Pure.intro, they
are preferred in instance proofs.
Does that solve the issues that were raised on this thread earlier? I
have followed the matter only with one eye, without really understanding
the full situation.
The "default" proof step is a little bit entangled, it tries to be smart
in including certain aspects of "intro_classes" to make such proof
patterns look somehow obvious. The classical reasoner overrides "default"
later once more, to add its classical viewpoint to the "rule" part.
If there is a need for it, such things can certainly be reformed, but it
would require a brief inspection of the status quo and the parts of the
history leading to it.
If plain Pure.intro (which already works with the "rule" method, BTW) is
sufficient, it is even easier.
This archive was generated by a fusion of
Pipermail (Mailman edition) and