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

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

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

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

- Previous by Date: Re: [isabelle] Lifting package and state transformers
- Next by Date: Re: [isabelle] Lifting package and state transformers
- 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