--- 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 +