author haftmann Thu, 20 Sep 2007 16:37:28 +0200 changeset 24656 67f6bf194ca6 parent 24655 24b630fd008f child 24657 185502d54c3d
code lemmas for cardinality
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions
```--- 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 +```