Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit 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.
Any ideas? Is the only way to redo the proofs of all necessary theorems
for explicit carrier sets?
The developer version contains a transfer tool (written by Amine Chaieb)
which may be helpful in situations like yours. Currently it is used for
lifting theorems between int and nat etc. But there is not really much
experience in using it, and it is not part of an official release, so
expect the unexpected! (and maybe redoing the proofs is less painful in
the end). Probably Amine or someone else can point you to an example of
how it can be used...
This archive was generated by a fusion of
Pipermail (Mailman edition) and