Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Hidetsune,
Let A be a set (A :: 'a set), then is there a
set (B :: 'b set) which is isomorphic to A?
Not in general. The type 'b might be too small to accommodate all the
elements of A. This doesn't hold because type variables are implicitly
universally quantified at the very beginning of a formula.
Clemens
Email Gateway (Aug 17 2022 at 14:14):From: Tjark Weber <tjark.weber@gmx.de>
Hidetsune,
this depends on A, 'a and 'b. It is not true in general. For example, take
'a to be int, A to be UNIV, and 'b to be bool.
Best,
Tjark
Email Gateway (Aug 17 2022 at 14:14):From: "Kobayashi, Hidetsune" <hd_coba@yahoo.co.jp>
Hi!
Let A be a set (A :: 'a set), then is there a
set (B :: 'b set) which is isomorphic to A? Here,
isomorphic means only having one-to-one
onto map from A to B.
If yes, is it possible to show the existence of
the isomorphism?
Thank you.
Kobayashi, Hidetsune
TSUKAME EIKOU! KAGAYAKE EGAO!
Yahoo! JAPAN JPC OFFICIAL PARTNER INTERNET PORTAL SITE
http://pr.mail.yahoo.co.jp/wintergames/
Email Gateway (Aug 17 2022 at 14:14):From: Brian Huffman <brianh@csee.ogi.edu>
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.
Email Gateway (Aug 17 2022 at 14:14):From: "Kobayashi, Hidetsune" <hd_coba@yahoo.co.jp>
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)?
TSUKAME EIKOU! KAGAYAKE EGAO!
Yahoo! JAPAN JPC OFFICIAL PARTNER INTERNET PORTAL SITE
http://pr.mail.yahoo.co.jp/wintergames/
Email Gateway (Aug 17 2022 at 14:14):From: "Kobayashi, Hidetsune" <hd_coba@yahoo.co.jp>
Elsa L Gunter's answer means:
"if we take I = B and A i = {0,1} then the
direct product has the cardinality strictly
larger than that of B and we have contradiction."
Is it?
This is the key point I am worrying. But, I
am still thinking that it is possible to express
such set B as type 'b in Isabelle/HOL. Because of
the set theory, we see there is a set isomorphic
to the direct product, we have only to put type
'b to the set B, I think.
It seems that Isabelle polymorphic type has no
restriction to instantiate. (My impression, I am
not sure, is that a type of a set with higher cardinality
shouldn't take a type of lower
cardinality in some cases.)
Therefore, if we carefully avoid such a wrong
instantiation, we can obtain correct formalization,
isn't it? Is it OK?
Best
Kobayashi, Hidetsune
--- Elsa L Gunter <egunter@cs.uiuc.edu> ：
TSUKAME EIKOU! KAGAYAKE EGAO!
Yahoo! JAPAN JPC OFFICIAL PARTNER INTERNET PORTAL SITE
http://pr.mail.yahoo.co.jp/wintergames/
Email Gateway (Aug 17 2022 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
I really don't see how to form a type that "big enough" to hold this
direct product unless it is some specific construction involving 'i
and 'a.
Larry
Last updated: May 03 2024 at 08:18 UTC