*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] calculational reasoning for transitive relations*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Wed, 22 Sep 2010 20:20:36 +0000 (UTC)*Cc*: Joachim Breitner <mail at joachim-breitner.de>*In-reply-to*: <1285142208.2562.5.camel@kirk>*References*: <mailman.5.1284865202.21615.cl-isabelle-users@lists.cam.ac.uk> <633215.28848.qm@web56107.mail.re3.yahoo.com> <1285142208.2562.5.camel@kirk>

Joachim Breitner wrote: >> Also, it would be nice if the transitivity rules for <o, <=o, =o were >> set up to work with Isar’s "also... also... finally". Good point. I actually though about this too, but did not investigate if it is possible. Now I see that a paper on the topic, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.2082 states that "Certainly, creative users of Isabelle/Isar may invent further ways of calculational reasoning at any time." It was not clear to me if this applies to the following situation: any combination of equalities and a relation proven to be transitive. 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: Wed, September 22, 2010 2:56:48 AM Subject: Re: FuncSet without extensional? (Joachim Breitner) Hi 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.) just FYI: I finished my results using your theory and committed my changes to the AFP mercurial repository. Thanks, it was exactly what I was expecting. In case you update your AFP entry to use List.lists instead of your own List definition, my theory will probably not compile any more. You can fix that by removing the lines: moreover (* Remove this if Ordinals_and_Cardinals uses List.lists as well *) have "|lists ((UNIV::bool set)\<times>X)| = |List ((UNIV::bool set)\<times>X)|" by (simp add: List_def lists_eq_set) from Free-Groups/Isomorphisms.thy Also, it would be nice if the transitivity rules for <o, <=o, =o were set up to work with Isar’s "also... also... finally". This would make my lemma "free_group_card_infinite" a bit more straight-forward to implement... but no big deal. Thanks for your theory! 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] calculational reasoning for transitive relations***From:*Brian Huffman

**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] FuncSet without extensional? (Joachim Breitner)
- Next by Date: Re: [isabelle] calculational reasoning for transitive relations
- Previous by Thread: Re: [isabelle] FuncSet without extensional? (Joachim Breitner)
- Next by Thread: Re: [isabelle] calculational reasoning for transitive relations
- 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