Re: [isabelle] Cardinality in HOL (Was: FuncSet without extensional?)

Hi Brian,

Am Sonntag, den 19.09.2010, 09:12 -0700 schrieb Brian Huffman:
> On Sun, Sep 19, 2010 at 12:46 AM, Joachim Breitner
> <mail at> wrote:
> > Hi again,
> >
> > Am Sonntag, den 19.09.2010, 00:13 +0200 schrieb Joachim Breitner:
> >> 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.
> >
> ...
> > Maybe I can try the result above at least for countable infinite M in
> > HOL.
> Hi Joachim,
> If you want to work with countable sets in HOL, you should look at
> HOL/Library/Nat_Bijection.thy. This file defines various bijections
> to/from the natural numbers. For example:
> prod_encode :: nat * nat => nat
> prod_decode :: nat => nat * nat
> list_encode :: nat list => nat
> list_decode :: nat => nat list
> I think it should be easy to show now, that if f :: 'a => nat and g ::
> nat => 'a are a bijection between M :: 'a set and UNIV :: nat set,
> then (list_encode o map f) and (map g o list_decode) are a bijection
> between "lists M :: 'a list set" and UNIV.

thanks for the pointer. I wasn’t aware of HOL/Library, and I’ll make
sure to look there the next time as well. HOL/Library/Countable looks
interesting as well.

I’d like to know of a way to proof this for uncountable sets as well
before digging into this, though. Having the result only for nat is not
very exciting.


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.