Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set

Quoting Peter Lammich <peter.lammich at>:

there are two ways of defining lattices in Isabelle:
The first approach makes the carrier set of the lattice explicit, as
e.g. in HOL/Algebra/Lattice.thy, the
second one (in HOL/Lattices.thy and HOL/Lattices/*) uses implicit
carrier sets (the UNIV-set of a type) and type-classes.

In fact, there is a third, even more general way: don't use the HOL equality, but an arbitrary equivalence relation. HOL/Algebra/Lattice.thy explores this, based on work by Stephan Hohe.

Is there a systematic/automatic way to go from theorems with the
implicit carrier set to corresponding theorems for an explicit carrier set?

I believe that this is theoretically not possible in general. It might be, if you restrict the kind of statements to a subset of formulae -- for example, universal sentences only. I believe that Peter Homeier addressed such issues in his quotient type work for HOL.


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