# HG changeset patch
# User haftmann
# Date 1190299048 -7200
# Node ID 67f6bf194ca65e9ceb0ab6cc4dae33f178fa683e
# Parent  24b630fd008f429fc49cc9d56c5ffb0f0d2d4935
code lemmas for cardinality

diff -r 24b630fd008f -r 67f6bf194ca6 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Sep 20 16:23:12 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Sep 20 16:37:28 2007 +0200
@@ -2371,8 +2371,6 @@
 where
   "Sup_fin = fold1 (op \<squnion>)"
 
-end context lattice begin
-
 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<sqsubseteq> \<Squnion>\<^bsub>fin\<^esub>A"
 apply(unfold Sup_fin_def Inf_fin_def)
 apply(subgoal_tac "EX a. a:A")
@@ -2683,7 +2681,14 @@
 
 lemma finite_code [code func]:
   "finite {} \<longleftrightarrow> True"
-  "finite (insert a A) \<longleftrightarrow> finite A" by auto
+  "finite (insert a A) \<longleftrightarrow> finite A"
+  by auto
+
+lemma card_code [code func]:
+  "card {} = 0"
+  "card (insert a A) =
+    (if finite A then Suc (card (A - {a})) else card (insert a A))"
+  by (auto simp add: card_insert)
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite (attach UNIV) = type +