Re: [isabelle] Lattices and syntactic classes



On 09/08/2011 11:00 PM, Makarius wrote:
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?

To me this looks rather like a workaround for some specific situations. If I understand correctly, it wouldn't work with a more complex class hierarchy, where parts of the instance may already be established etc. The issue certainly deserves more thourough examination at some point.

For now I have just added (5e51075cbd97) the syntactic classes for inf and sup, which were originally asked for by Viorel. This is a rather straightforward thing, and the more general typings that may arise seem to have little impact in practice.

Alex





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