Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
Quoting Peter Lammich <peter.lammich at uni-muenster.de>:
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