*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Sun, 19 Sep 2010 20:20:55 -0700 (PDT)*Cc*: mail at joachim-breitner.de*In-reply-to*: <mailman.5.1284865202.21615.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.5.1284865202.21615.cl-isabelle-users@lists.cam.ac.uk>

Hi Joachim, >> BTW, are there already theories about uncountable sets? I?d need, as a >> lemma, the fact that the M* (the set of finite words) of a uncountably >> infinte set M has the same cardinality. Actually, quite a bit of the ZF theory of cardinals can be done in HOL. I have already set the basis of such a theory: it is in the Isabelle AFP, and is fairly well documented. http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml Your lemma is stated there in the theory Cardinal_order_relation, in subsection "Cardinals versus lists", as List_infinite_bij_betw (NB: it holds for any infinite set, including the countably infinite ones.) Best regards, Andrei ----- Original Message ---- From: "cl-isabelle-users-request at lists.cam.ac.uk" <cl-isabelle-users-request at lists.cam.ac.uk> To: cl-isabelle-users at lists.cam.ac.uk Sent: Sat, September 18, 2010 10:00:02 PM Subject: Cl-isabelle-users Digest, Vol 63, Issue 21 Send Cl-isabelle-users mailing list submissions to cl-isabelle-users at lists.cam.ac.uk To subscribe or unsubscribe via the World Wide Web, visit https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users or, via email, send a message with subject or body 'help' to cl-isabelle-users-request at lists.cam.ac.uk You can reach the person managing the list at cl-isabelle-users-owner at lists.cam.ac.uk When replying, please edit your Subject line so it is more specific than "Re: Contents of Cl-isabelle-users digest..." Today's Topics: 1. Re: Unicode (Was: Update on I3P) (Joachim Breitner) 2. FuncSet without extensional? (Joachim Breitner) 3. Re: FuncSet without extensional? (Lawrence Paulson) 4. Re: FuncSet without extensional? (Tobias Nipkow) 5. Re: FuncSet without extensional? (Joachim Breitner) ---------------------------------------------------------------------- Message: 1 Date: Sat, 18 Sep 2010 15:31:04 +0200 From: Joachim Breitner <mail at joachim-breitner.de> Subject: Re: [isabelle] Unicode (Was: Update on I3P) To: Holger Gast <gast at informatik.uni-tuebingen.de> Cc: isabelle-users at cl.cam.ac.uk Message-ID: <1284816664.14778.3.camel at kirk> Content-Type: text/plain; charset="utf-8" Hi, Am Freitag, den 10.09.2010, 18:20 +0200 schrieb Makarius: > On Fri, 10 Sep 2010, Joachim Breitner wrote: > > I should add that this sequence of four characters is the utf8 > > representation of ?? (\<Z>), re-encoded as utf8: > > $ echo -n ????|iconv -futf8 -tlatin1 > > ?? > > $ echo -n ?? | iconv -flatin1 -tutf8 > > ???? > > > > Maybe i3p has problems with unicode character code points that do not > > fit in one 16-bit number? > > This is a deeper problem of the way Unicode works on the JVM, see also > http://download.oracle.com/javase/6/docs/api/java/lang/Character.html > > Few Java applications get this specification of "surrogate code points" > right, because this situation occurs rarely. UTF-8 works generally better > because the multi-character sequences are the rule, not the exception. > > It is unlikely that this will get fundamentally better on the JVM, > although some people have already started joking that Oracle will soon > identify "" and null for type String ... > > The easyiest fix is to remove these non-16bit codes from the table of > Isabelle symbol interpretation. Yes, this is a work-around (although I had to edit the copy of the symbols file in i3p/modules/org-i3p-fontsupport.jar). A proper fix would be nice, though ? Unicode is just too shiny :-) Greetings, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 198 bytes Desc: This is a digitally signed message part Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20100918/f2ee9d77/attachment.bin ------------------------------ Message: 2 Date: Sat, 18 Sep 2010 20:18:30 +0200 From: Joachim Breitner <mail at joachim-breitner.de> Subject: [isabelle] FuncSet without extensional? To: isabelle-users at cl.cam.ac.uk Message-ID: <1284833910.14778.10.camel at kirk> Content-Type: text/plain; charset="utf-8" Hi, I was trying to prove the statement that there is a bijection between Hom(F(X),C2) and Pow(X). I started with "? f. bij_betw f (Pow X) (hom (?\<^bsub>X\<^esub>) C2)" and it went relatively well... until I noticed that hom is not suitable here. Group.hom is defined via FuncSet.Pi, which has the following definition: Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where "Pi A B = {f. ?x. x ? A --> f x ? B x}" (With an abbreviation A -> B). This means that for example ({} -> {}) is not a one-element-set, but is actually the set UNIV::('a -> 'b). Right below the definition of Pi, there is a predicate specifying that functions are undefined outside their definition: definition extensional :: "'a set => ('a => 'b) set" where "extensional A = {f. ?x. x~:A --> f x = undefined}" For my current goal, it would be great if this were part of the definition of Pi. Would this be generally useful? Or are there hard reasons not to require "extensional A" for function in "A -> B"? Thanks, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 198 bytes Desc: This is a digitally signed message part Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20100918/08d56850/attachment.bin ------------------------------ Message: 3 Date: Sat, 18 Sep 2010 20:37:35 +0100 From: Lawrence Paulson <lp15 at cam.ac.uk> Subject: Re: [isabelle] FuncSet without extensional? To: Joachim Breitner <mail at joachim-breitner.de> Cc: isabelle-users at cl.cam.ac.uk Message-ID: <EC81FCE0-85EB-4EC4-95B7-8BA90C1D8BB9 at cam.ac.uk> Content-Type: text/plain; charset=utf-8 Extensionality isn't always wanted, so the concepts are defined separately. Possibly you want a new definition of hom. Larry Paulson On 18 Sep 2010, at 19:18, Joachim Breitner wrote: > Hi, > > I was trying to prove the statement that there is a bijection between > Hom(F(X),C2) and Pow(X). I started with > "? f. bij_betw f (Pow X) (hom (?\<^bsub>X\<^esub>) C2)" > and it went relatively well... until I noticed that hom is not suitable > here. Group.hom is defined via FuncSet.Pi, which has the following > definition: > > Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where > "Pi A B = {f. ?x. x ? A --> f x ? B x}" > (With an abbreviation A -> B). > > This means that for example ({} -> {}) is not a one-element-set, but is > actually the set UNIV::('a -> 'b). > > Right below the definition of Pi, there is a predicate specifying that > functions are undefined outside their definition: > > definition > extensional :: "'a set => ('a => 'b) set" where > "extensional A = {f. ?x. x~:A --> f x = undefined}" > > For my current goal, it would be great if this were part of the > definition of Pi. Would this be generally useful? Or are there hard > reasons not to require "extensional A" for function in "A -> B"? > > Thanks, > Joachim > > > -- > Joachim Breitner > e-Mail: mail at joachim-breitner.de > Homepage: http://www.joachim-breitner.de > ICQ#: 74513189 > Jabber-ID: nomeata at joachim-breitner.de ------------------------------ Message: 4 Date: Sat, 18 Sep 2010 22:16:07 +0200 From: Tobias Nipkow <nipkow at in.tum.de> Subject: Re: [isabelle] FuncSet without extensional? To: Joachim Breitner <mail at joachim-breitner.de> Cc: isabelle-users at cl.cam.ac.uk Message-ID: <4C951E07.7050702 at in.tum.de> Content-Type: text/plain; charset=UTF-8 Since this is a library theory, you can expect a number of client theories to break if you make such a drastic change. For example lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" within FuncSet would no longer hold, although it is a standard law about function spaces. At the moment users have the choice: they can always adjoin "extensional" in their context if needed. Your suggestion deprives them of that choice. Tobias Joachim Breitner schrieb: > Hi, > > I was trying to prove the statement that there is a bijection between > Hom(F(X),C2) and Pow(X). I started with > "? f. bij_betw f (Pow X) (hom (?\<^bsub>X\<^esub>) C2)" > and it went relatively well... until I noticed that hom is not suitable > here. Group.hom is defined via FuncSet.Pi, which has the following > definition: > > Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where > "Pi A B = {f. ?x. x ? A --> f x ? B x}" > (With an abbreviation A -> B). > > This means that for example ({} -> {}) is not a one-element-set, but is > actually the set UNIV::('a -> 'b). > > Right below the definition of Pi, there is a predicate specifying that > functions are undefined outside their definition: > > definition > extensional :: "'a set => ('a => 'b) set" where > "extensional A = {f. ?x. x~:A --> f x = undefined}" > > For my current goal, it would be great if this were part of the > definition of Pi. Would this be generally useful? Or are there hard > reasons not to require "extensional A" for function in "A -> B"? > > Thanks, > Joachim > > ------------------------------ Message: 5 Date: Sun, 19 Sep 2010 00:13:44 +0200 From: Joachim Breitner <mail at joachim-breitner.de> Subject: Re: [isabelle] FuncSet without extensional? To: isabelle-users at cl.cam.ac.uk Message-ID: <1284848024.14778.16.camel at kirk> Content-Type: text/plain; charset="utf-8" Hi, points taken. I?ll try with a definition homr here, combining hom and extensional. But assuming one would give hom or iso more structure (e.g. a group structure), then demanding extensionality would be required, e.g. for the uniqueness of \<one>. BTW, are there already theories about uncountable sets? I?d need, as a lemma, the fact that the M* (the set of finite words) of a uncountably infinte set M has the same cardinality. Thanks, Joachim Am Samstag, den 18.09.2010, 22:16 +0200 schrieb Tobias Nipkow: > Since this is a library theory, you can expect a number of client > theories to break if you make such a drastic change. For example > > lemma Pi_anti_mono: "A' <= A ==> Pi A B <= Pi A' B" > > within FuncSet would no longer hold, although it is a standard law about > function spaces. > > At the moment users have the choice: they can always adjoin > "extensional" in their context if needed. Your suggestion deprives them > of that choice. > > Tobias > > Joachim Breitner schrieb: > > Hi, > > > > I was trying to prove the statement that there is a bijection between > > Hom(F(X),C2) and Pow(X). I started with > > "? f. bij_betw f (Pow X) (hom (?\<^bsub>X\<^esub>) C2)" > > and it went relatively well... until I noticed that hom is not suitable > > here. Group.hom is defined via FuncSet.Pi, which has the following > > definition: > > > > Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" where > > "Pi A B = {f. ?x. x ? A --> f x ? B x}" > > (With an abbreviation A -> B). > > > > This means that for example ({} -> {}) is not a one-element-set, but is > > actually the set UNIV::('a -> 'b). > > > > Right below the definition of Pi, there is a predicate specifying that > > functions are undefined outside their definition: > > > > definition > > extensional :: "'a set => ('a => 'b) set" where > > "extensional A = {f. ?x. x~:A --> f x = undefined}" > > > > For my current goal, it would be great if this were part of the > > definition of Pi. Would this be generally useful? Or are there hard > > reasons not to require "extensional A" for function in "A -> B"? > > > > Thanks, > > Joachim > > > > > > -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 198 bytes Desc: This is a digitally signed message part Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20100919/d78030f5/attachment.bin End of Cl-isabelle-users Digest, Vol 63, Issue 21 *************************************************

**Follow-Ups**:**Re: [isabelle] FuncSet without extensional? (Joachim Breitner)***From:*Joachim Breitner

**Re: [isabelle] FuncSet without extensional? (Joachim Breitner)***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)
- Next by Date: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Previous by Thread: Re: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)
- Next by Thread: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list