*To*: Andrei Popescu <uuomul at yahoo.com>*Subject*: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 20 Sep 2010 22:59:07 +0200*Cc*: Joachim Breitner <mail at joachim-breitner.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <838761.37406.qm@web56105.mail.re3.yahoo.com>*References*: <mailman.5.1284865202.21615.cl-isabelle-users@lists.cam.ac.uk> <633215.28848.qm@web56107.mail.re3.yahoo.com> <1284972090.2657.4.camel@kirk.ehbuehl.net> <838761.37406.qm@web56105.mail.re3.yahoo.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

List.thy contains an inductively defined set "lists A" which is equivalent to your "List A". Strangely enough, the equality "lists A = {xs. set xs <= A}" is not present, but can be proved automatically. I will add that equality. Tobias Andrei Popescu schrieb: > Dear Joachim, > >>> You define >>> definition List :: "'a set => 'a list set" >>> where "List A ≡ {l. set l ≤ A}" > >>> This is a definition that I could use in the development of Free Groups. >>> Assuming I would not need the cardinality lemmas, what is the best >>> practice: Importing your theory nevertheless, copying the definition or >>> pushing to add this definition in a more standard, common place, i.e. >>> HOL or HOL/Library? > > IMO, if you only need that simple function, it is better to just redefine it > rather than > > importing the whole theory of cardinals. > I agree that its presence is desirable in the standard library though. > (Or maybe it even exists, but I was not able to find it.) > > Best regards, > Andrei > > > > > > ----- Original Message ---- > From: Joachim Breitner <mail at joachim-breitner.de> > To: Andrei Popescu <uuomul at yahoo.com> > Cc: cl-isabelle-users at lists.cam.ac.uk > Sent: Mon, September 20, 2010 3:41:30 AM > Subject: Re: [isabelle] FuncSet without extensional? (Joachim Breitner) > > Dear Andrei, > > Am Sonntag, den 19.09.2010, 20:20 -0700 schrieb Andrei Popescu: >>>> 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.) > > Thanks for the pointer. This is what I need... I need to get better at > finding existing theories :-) > > You define > definition List :: "'a set => 'a list set" > where "List A ≡ {l. set l ≤ A}" > > This is a definition that I could use in the development of Free Groups. > Assuming I would not need the cardinality lemmas, what is the best > practice: Importing your theory nevertheless, copying the definition or > pushing to add this definition in a more standard, common place, i.e. > HOL or HOL/Library? > > Greetings, > Joachim >

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

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

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

- Previous by Date: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Next by Date: Re: [isabelle] Building isabelle-devel on a 2GB of RAM
- Previous by Thread: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- 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