Re: [isabelle] Lifting package and state transformers



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




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