simplify card_UNIV type class,
tuned proofs

--- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 13:52:51 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 14:34:46 2012 +0200
@@ -88,58 +88,25 @@
 
 subsection {* A type class for computing the cardinality of types *}
 
+definition is_list_UNIV :: "'a list \<Rightarrow> bool"
+where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
+
+lemmas [code_unfold] = is_list_UNIV_def[abs_def]
+
+lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
+by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
+   dest: subst[where P="finite", OF _ finite_set] card_eq_UNIV_imp_eq_UNIV)
+
+lemma card_UNIV_eq_0_is_list_UNIV_False:
+  "CARD('a) = 0 \<Longrightarrow> is_list_UNIV = (\<lambda>xs :: 'a list. False)"
+by(simp add: is_list_UNIV_def[abs_def])
+
 class card_UNIV = 
   fixes card_UNIV :: "'a itself \<Rightarrow> nat"
-  assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
-begin
-
-lemma card_UNIV_neq_0_finite_UNIV:
-  "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
-by(simp add: card_UNIV card_eq_0_iff)
-
-lemma card_UNIV_ge_0_finite_UNIV:
-  "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
-by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
-
-lemma card_UNIV_eq_0_infinite_UNIV:
-  "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
-by(simp add: card_UNIV card_eq_0_iff)
-
-definition is_list_UNIV :: "'a list \<Rightarrow> bool"
-where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
+  assumes card_UNIV: "card_UNIV x = CARD('a)"
 
-lemma is_list_UNIV_iff: fixes xs :: "'a list"
-  shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
-proof
-  assume "is_list_UNIV xs"
-  hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
-    unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
-  from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
-  have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
-  also note set_remdups
-  finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
-next
-  assume xs: "set xs = UNIV"
-  from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
-  hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
-  moreover have "size (remdups xs) = card (set (remdups xs))"
-    by(subst distinct_card) auto
-  ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
-qed
-
-lemma card_UNIV_eq_0_is_list_UNIV_False:
-  assumes cU0: "card_UNIV x = 0"
-  shows "is_list_UNIV = (\<lambda>xs. False)"
-proof(rule ext)
-  fix xs :: "'a list"
-  from cU0 have "\<not> finite (UNIV :: 'a set)"
-    by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
-  moreover have "finite (set xs)" by(rule finite_set)
-  ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
-  thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
-qed
-
-end
+lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
+by(simp add: card_UNIV)
 
 subsection {* Instantiations for @{text "card_UNIV"} *}
 
@@ -315,7 +282,7 @@
 lemma eq_set_code [code]:
   fixes xs ys :: "'a :: card_UNIV list"
   defines "rhs \<equiv> 
-  let n = card_UNIV TYPE('a)
+  let n = CARD('a)
   in if n = 0 then False else 
         let xs' = remdups xs; ys' = remdups ys 
         in length xs' + length ys' = n \<and> (\<forall>x \<in> set xs'. x \<notin> set ys') \<and> (\<forall>y \<in> set ys'. y \<notin> set xs')"

--- a/src/HOL/Library/FinFun.thy	Fri Jun 01 13:52:51 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Fri Jun 01 14:34:46 2012 +0200
@@ -435,8 +435,8 @@
 by transfer (simp add: finfun_default_aux_update_const)
 
 lemma finfun_default_const_code [code]:
-  "finfun_default ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
-by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
+  "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
+by(simp add: finfun_default_const)
 
 lemma finfun_default_update_code [code]:
   "finfun_default (finfun_update_code f a b) = finfun_default f"
@@ -1285,9 +1285,8 @@
 
 lemma finfun_dom_const_code [code]:
   "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
-   (if card_UNIV (TYPE('a)) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
-unfolding card_UNIV_eq_0_infinite_UNIV
-by(simp add: finfun_dom_const)
+   (if CARD('a) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
+by(simp add: finfun_dom_const card_UNIV card_eq_0_iff)
 
 lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
 using finite_finfun_default[of f]
@@ -1349,9 +1348,8 @@
 
 lemma finfun_to_list_const_code [code]:
   "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
-   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
-unfolding card_UNIV_eq_0_infinite_UNIV
-by(auto simp add: finfun_to_list_const)
+   (if CARD('a) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
+by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
 
 lemma remove1_insort_insert_same:
   "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"

--- a/src/HOL/ex/FinFunPred.thy	Fri Jun 01 13:52:51 2012 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Fri Jun 01 14:34:46 2012 +0200
@@ -258,4 +258,11 @@
   by eval
 end
 
+declare iso_finfun_Ball_Ball[code_unfold]
+notepad begin
+have "(\<forall>x. ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) x \<longrightarrow> x < 3)"
+  by eval
+end
+declare iso_finfun_Ball_Ball[code_unfold del]
+
 end
\ No newline at end of file