simplify card_UNIV type class,
authorAndreas Lochbihler
Fri Jun 01 14:34:46 2012 +0200 (2012-06-01)
changeset 48059f6ce99d3719b
parent 48058 11a732f7d79f
child 48060 1f4d00a7f59f
simplify card_UNIV type class,
tuned proofs
src/HOL/Library/Cardinality.thy
src/HOL/Library/FinFun.thy
src/HOL/ex/FinFunPred.thy
     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')"
     2.1 --- a/src/HOL/Library/FinFun.thy	Fri Jun 01 13:52:51 2012 +0200
     2.2 +++ b/src/HOL/Library/FinFun.thy	Fri Jun 01 14:34:46 2012 +0200
     2.3 @@ -435,8 +435,8 @@
     2.4  by transfer (simp add: finfun_default_aux_update_const)
     2.5  
     2.6  lemma finfun_default_const_code [code]:
     2.7 -  "finfun_default ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = (if card_UNIV (TYPE('a)) = 0 then c else undefined)"
     2.8 -by(simp add: finfun_default_const card_UNIV_eq_0_infinite_UNIV)
     2.9 +  "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)"
    2.10 +by(simp add: finfun_default_const)
    2.11  
    2.12  lemma finfun_default_update_code [code]:
    2.13    "finfun_default (finfun_update_code f a b) = finfun_default f"
    2.14 @@ -1285,9 +1285,8 @@
    2.15  
    2.16  lemma finfun_dom_const_code [code]:
    2.17    "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
    2.18 -   (if card_UNIV (TYPE('a)) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
    2.19 -unfolding card_UNIV_eq_0_infinite_UNIV
    2.20 -by(simp add: finfun_dom_const)
    2.21 +   (if CARD('a) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
    2.22 +by(simp add: finfun_dom_const card_UNIV card_eq_0_iff)
    2.23  
    2.24  lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
    2.25  using finite_finfun_default[of f]
    2.26 @@ -1349,9 +1348,8 @@
    2.27  
    2.28  lemma finfun_to_list_const_code [code]:
    2.29    "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
    2.30 -   (if card_UNIV (TYPE('a)) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
    2.31 -unfolding card_UNIV_eq_0_infinite_UNIV
    2.32 -by(auto simp add: finfun_to_list_const)
    2.33 +   (if CARD('a) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
    2.34 +by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
    2.35  
    2.36  lemma remove1_insort_insert_same:
    2.37    "x \<notin> set xs \<Longrightarrow> remove1 x (insort_insert x xs) = xs"
     3.1 --- a/src/HOL/ex/FinFunPred.thy	Fri Jun 01 13:52:51 2012 +0200
     3.2 +++ b/src/HOL/ex/FinFunPred.thy	Fri Jun 01 14:34:46 2012 +0200
     3.3 @@ -258,4 +258,11 @@
     3.4    by eval
     3.5  end
     3.6  
     3.7 +declare iso_finfun_Ball_Ball[code_unfold]
     3.8 +notepad begin
     3.9 +have "(\<forall>x. ((\<lambda>_ :: nat. False)(1 := True, 2 := True)) x \<longrightarrow> x < 3)"
    3.10 +  by eval
    3.11 +end
    3.12 +declare iso_finfun_Ball_Ball[code_unfold del]
    3.13 +
    3.14  end
    3.15 \ No newline at end of file