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
suggested earlier.

Viorel











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