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
apply default
oops

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.


	Makarius





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