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

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.

- Brian

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