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



Hi Peter,

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...

Alex






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