# Re: [isabelle] Sets

On Friday 10 March 2006 06:42, Kobayashi, Hidetsune wrote:
> Hi! Thaks for the answers.
>
> Let me explain the problem again.
>
> Given (I :: 'i set), (A i :: 'a set) .
> The direct product of the family {A i} is
> ('i => 'a) set.
>
> My question is:
> is it possible to find some set B isomorphic
> to the direct product and B having
> some 'a123 type (the only condition for
> the type of B is that the type is expressed
> in one string, say as a123, not as 'i => 'a)?
Maybe what you want is to define a new type that is isomorphic to the old set.
You can do this with Isabelle's typedef command. With your example, I'll
assume you have a function called direct_product that calculates the direct
product of A; then you can use:
typedef foo = "direct_product A"
Then the set "UNIV::foo set" will be isomorphic to the set "direct_product A".
However, you will also need to prove that "direct_product A" is nonempty for
this to work. You can read more about typedef in the Isabelle tutorial.
- Brian

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