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


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.