*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Mon, 20 Sep 2010 13:26:24 -0700 (PDT)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1284972090.2657.4.camel@kirk.ehbuehl.net>*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>

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 -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

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

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

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

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