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.