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



Dear Joachim, 

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

I am glad you found it useful.  This was precisely the intended target: 
the "working" mathematics, needing only basic cardinality results.  

>> In case you update your AFP entry to use List.lists instead of your own
>> List definition,

Yes, I will soon.

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










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