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



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
*************************************************



      






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