src/HOL/Library/Cardinality.thy
changeset 48059 f6ce99d3719b
parent 48058 11a732f7d79f
child 48060 1f4d00a7f59f
     1.1 --- a/src/HOL/Library/Cardinality.thy	Fri Jun 01 13:52:51 2012 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Fri Jun 01 14:34:46 2012 +0200
     1.3 @@ -88,58 +88,25 @@
     1.4  
     1.5  subsection {* A type class for computing the cardinality of types *}
     1.6  
     1.7 +definition is_list_UNIV :: "'a list \<Rightarrow> bool"
     1.8 +where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)"
     1.9 +
    1.10 +lemmas [code_unfold] = is_list_UNIV_def[abs_def]
    1.11 +
    1.12 +lemma is_list_UNIV_iff: "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    1.13 +by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] 
    1.14 +   dest: subst[where P="finite", OF _ finite_set] card_eq_UNIV_imp_eq_UNIV)
    1.15 +
    1.16 +lemma card_UNIV_eq_0_is_list_UNIV_False:
    1.17 +  "CARD('a) = 0 \<Longrightarrow> is_list_UNIV = (\<lambda>xs :: 'a list. False)"
    1.18 +by(simp add: is_list_UNIV_def[abs_def])
    1.19 +
    1.20  class card_UNIV = 
    1.21    fixes card_UNIV :: "'a itself \<Rightarrow> nat"
    1.22 -  assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
    1.23 -begin
    1.24 -
    1.25 -lemma card_UNIV_neq_0_finite_UNIV:
    1.26 -  "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
    1.27 -by(simp add: card_UNIV card_eq_0_iff)
    1.28 -
    1.29 -lemma card_UNIV_ge_0_finite_UNIV:
    1.30 -  "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
    1.31 -by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
    1.32 -
    1.33 -lemma card_UNIV_eq_0_infinite_UNIV:
    1.34 -  "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
    1.35 -by(simp add: card_UNIV card_eq_0_iff)
    1.36 -
    1.37 -definition is_list_UNIV :: "'a list \<Rightarrow> bool"
    1.38 -where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
    1.39 +  assumes card_UNIV: "card_UNIV x = CARD('a)"
    1.40  
    1.41 -lemma is_list_UNIV_iff: fixes xs :: "'a list"
    1.42 -  shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
    1.43 -proof
    1.44 -  assume "is_list_UNIV xs"
    1.45 -  hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
    1.46 -    unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
    1.47 -  from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
    1.48 -  have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
    1.49 -  also note set_remdups
    1.50 -  finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
    1.51 -next
    1.52 -  assume xs: "set xs = UNIV"
    1.53 -  from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
    1.54 -  hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
    1.55 -  moreover have "size (remdups xs) = card (set (remdups xs))"
    1.56 -    by(subst distinct_card) auto
    1.57 -  ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
    1.58 -qed
    1.59 -
    1.60 -lemma card_UNIV_eq_0_is_list_UNIV_False:
    1.61 -  assumes cU0: "card_UNIV x = 0"
    1.62 -  shows "is_list_UNIV = (\<lambda>xs. False)"
    1.63 -proof(rule ext)
    1.64 -  fix xs :: "'a list"
    1.65 -  from cU0 have "\<not> finite (UNIV :: 'a set)"
    1.66 -    by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
    1.67 -  moreover have "finite (set xs)" by(rule finite_set)
    1.68 -  ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
    1.69 -  thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
    1.70 -qed
    1.71 -
    1.72 -end
    1.73 +lemma card_UNIV_code [code_unfold]: "CARD('a :: card_UNIV) = card_UNIV TYPE('a)"
    1.74 +by(simp add: card_UNIV)
    1.75  
    1.76  subsection {* Instantiations for @{text "card_UNIV"} *}
    1.77  
    1.78 @@ -315,7 +282,7 @@
    1.79  lemma eq_set_code [code]:
    1.80    fixes xs ys :: "'a :: card_UNIV list"
    1.81    defines "rhs \<equiv> 
    1.82 -  let n = card_UNIV TYPE('a)
    1.83 +  let n = CARD('a)
    1.84    in if n = 0 then False else 
    1.85          let xs' = remdups xs; ys' = remdups ys 
    1.86          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')"