*To*: Ognjen Maric <ognjen.maric at gmail.com>*Subject*: Re: [isabelle] Lifting package and state transformers*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 17 May 2016 20:41:16 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <a5d7c557-fb53-82af-2243-4cc8d9c131f6@gmail.com>*References*: <573AA3A5.7070101@inf.ethz.ch> <3E77413C-C0C7-48DF-BE91-B9F08FF06102@inf.ethz.ch> <573B02A4.3030007@inf.ethz.ch> <a5d7c557-fb53-82af-2243-4cc8d9c131f6@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.7.2

Dear Ognjen,

Thanks for the suggestion, Andreas On 17/05/16 20:34, Ognjen Maric wrote:

On 05/17/2016 01:38 PM, Andreas Lochbihler wrote:No theorem of the form "type_definition Rep Abs X" will work, because it would state that the new type is isomorphic to the set X. But ('s, 'm) stateT has much more elements than 'm (unless 's is a singleton type), so there cannot be such an isomorphic subset.I don't know if it helps your use case, but there should still be an isomorphism if 's is finite and 'm is infinite. At least in ZF, you can prove from the axiom of choice that every infinite set A is equipotent to the Cartesian product A x A - in fact, the two are equivalent by a theorem of Tarski. I don't know if the same holds in HOL. Ognjen

**References**:**[isabelle] Lifting package and state transformers***From:*Andreas Lochbihler

**Re: [isabelle] Lifting package and state transformers***From:*Dmitriy Traytel

**Re: [isabelle] Lifting package and state transformers***From:*Andreas Lochbihler

**Re: [isabelle] Lifting package and state transformers***From:*Ognjen Maric

- Previous by Date: Re: [isabelle] Lifting package and state transformers
- Next by Date: [isabelle] Isabelle/HOL 2005
- Previous by Thread: Re: [isabelle] Lifting package and state transformers
- Next by Thread: Re: [isabelle] Lifting package and state transformers
- Cl-isabelle-users May 2016 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