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.