Re: [isabelle] cardinality



On Wednesday 08 March 2006 16:09, kuecuek at rbg.informatik.tu-darmstadt.de wrote:
> for example if i try to prove this with card  :
> there are 3 natural numbers smaller than 3
>
> card {(x::nat). x<3} = (3::nat)
>
> is this right or how should i construct this lemma?

The lemma looks good to me, and once you've established that {(x::nat). x<3} is
equal to {0, 1, 2}, it can be proven automatically:

lemma "card {(x::nat). x<3} = 3"
  apply (subgoal_tac "{(x::nat). x<3} = {0, 1, 2}")
  apply auto
done

It is of course just an instance of a more general lemma, which you could prove
using induction:

lemma "card {x. x<n} = n"

> another question is where can i find useful lemmas about card? (in set?)

Rather in Finite_Set (http://isabelle.in.tum.de/dist/library/HOL/Finite_Set.html).
Note that the cardinality of infinite sets is defined as 0::nat.

Best,
Tjark





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