[isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
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
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
Any ideas? Is the only way to redo the proofs of all necessary theorems
for explicit carrier sets?
Regards and thanks for any hints,
This archive was generated by a fusion of
Pipermail (Mailman edition) and