Re: [isabelle] Lattices and syntactic classes
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.
Thank you for this change. I did use a work around which worked well. So
the alternatives suggested did not seem better to me.
The work around that I used is the following:
class inf =
fixes inf :: "'a => 'a => 'a" (infixl "\<sqinter>" 70)
class sup =
fixes sup :: "'a => 'a => 'a" (infixl "\<squnion>" 65)
class lattice_infix = order + inf + sup +
assumes lattice: "class.lattice (op \<le>) (op <) inf sup"
sublocale lattice_infix < lattice "op \<le>" "op <" inf sup
by (rule lattice)
After this I used lattice_infix instead of lattice. It seems that
this way works better and it is more general that the ways
This archive was generated by a fusion of
Pipermail (Mailman edition) and