*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set*From*: Jeremy Avigad <avigad at cmu.edu>*Date*: Tue, 27 Oct 2009 21:32:57 +0100*In-reply-to*: <4AE6046B.2060007@in.tum.de>*References*: <4AE5D661.2080708@uni-muenster.de> <4AE6046B.2060007@in.tum.de>

Friends,

(1) (Re)do everything in locales, as Larry suggests.

Best wishes, Jeremy On Oct 26, 2009, at 9:19 PM, Alexander Krauss wrote:

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 necessarytheoremsfor explicit carrier sets?The developer version contains a transfer tool (written by AmineChaieb) which may be helpful in situations like yours. Currently itis used for lifting theorems between int and nat etc. But there isnot really much experience in using it, and it is not part of anofficial release, so expect the unexpected! (and maybe redoing theproofs is less painful in the end). Probably Amine or someone elsecan point you to an example of how it can be used...Alex

**Follow-Ups**:**Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set***From:*Lawrence Paulson

**References**:**[isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set***From:*Peter Lammich

**Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set***From:*Alexander Krauss

- Previous by Date: [isabelle] Simplifier problem (Congruence rules?)
- Next by Date: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set[SEC=UNCLASSIFIED]
- Previous by Thread: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
- Next by Thread: Re: [isabelle] Lattices with explicit carrier set vs. lattices with implicit carrier set
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list