Re: [isabelle] Lifting package and state transformers



Dear Ognjen,

Equipotence of A and A * A for infinite A also holds in HOL. But in general, my state space 's is infinite :-(.

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





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