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



Hi all,

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.

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

My concrete problem is, that I have many theorems for the implicit
carrier-set, but the algorithms I want to verify require parametric
carrier sets, e.g.
I need the lattice of all subsets of control locations in the program,
that has some nice properties (e.g. finite-height) only, if there are
only finitely many
control locations.

However, because the set of control locations is a parameter of the
algorithm I want to verify, I cannot fix it in advance, and thus cannot
define a datatype of control locations, that
would be required to show that it's corresponding set-type is in the
lattice-typeclass.

Any ideas? Is the only way to redo the proofs of all necessary theorems
for explicit carrier sets?


Regards and thanks for any hints,
  Peter






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