# Re: [isabelle] cardinality

From: Tjark Weber <tjark.weber at gmx.de>
>It is of course just an instance of a more general lemma, which you could
>prove using induction:
>
>lemma "card {x. x<n} = n"
That seemed like an interesting exercise, so I went ahead and did it.
I often feel that my proofs are too wordy, and I suspect there are
good tactics out there that I should be using but I don't know about
them. Is there a list somewhere of all of the generally-useful
tactics, their arguments, and examples of their use?
I found some .dvi documents that came with Isabelle, but they are a
long exposition that I don't know how to search, rather than a list.
--
Tim Freeman http://www.fungible.com tim at fungible.com
Pass it on: The Integral Fast Reactor can provide safe, clean
energy. Politically motivated misrepresentation stopped the research.
Check it out at: http://en.wikipedia.org/wiki/Integral_Fast_Reactor
P. S. Here's my proof. Does anyone have one that's shorter?
theory Card = Main:
lemma finite_less_n: "finite {(x::nat). x < n}"
proof
let ?A = "(%x . x) ` {i::nat. i<n}"
from nat_seg_image_imp_finite have "?A = ?A ?ªä finite ?A" .
thus ?thesis by simp
thus "Finites ?©Í Finites" by blast
qed
lemma insert: "{x. x < Suc n} = insert n {x. x < n}" by force
lemma notin: "n ?©Ï {x::nat. x < n}" by blast
lemma cardsuc: "card (insert n {x::nat. x < n}) = Suc (card {x::nat . x < n})"
by (simp add: card_insert_disjoint add: notin add: finite_less_n)
lemma "card {(x::nat). x<n} = n"
apply (induct_tac n)
apply auto
apply (simp add: cardsuc add: insert)
done

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