Re: [isabelle] 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.  
> 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 Breitner
  e-Mail: mail at
  ICQ#: 74513189
  Jabber-ID: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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