1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Card_Univ.thy Tue May 29 15:31:58 2012 +0200
1.3 @@ -0,0 +1,293 @@
1.4 +(* Author: Andreas Lochbihler, KIT *)
1.5 +
1.6 +header {* A type class for computing the cardinality of a type's universe *}
1.7 +
1.8 +theory Card_Univ imports Main begin
1.9 +
1.10 +subsection {* A type class for computing the cardinality of a type's universe *}
1.11 +
1.12 +class card_UNIV =
1.13 + fixes card_UNIV :: "'a itself \<Rightarrow> nat"
1.14 + assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)"
1.15 +begin
1.16 +
1.17 +lemma card_UNIV_neq_0_finite_UNIV:
1.18 + "card_UNIV x \<noteq> 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
1.19 +by(simp add: card_UNIV card_eq_0_iff)
1.20 +
1.21 +lemma card_UNIV_ge_0_finite_UNIV:
1.22 + "card_UNIV x > 0 \<longleftrightarrow> finite (UNIV :: 'a set)"
1.23 +by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0)
1.24 +
1.25 +lemma card_UNIV_eq_0_infinite_UNIV:
1.26 + "card_UNIV x = 0 \<longleftrightarrow> \<not> finite (UNIV :: 'a set)"
1.27 +by(simp add: card_UNIV card_eq_0_iff)
1.28 +
1.29 +definition is_list_UNIV :: "'a list \<Rightarrow> bool"
1.30 +where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)"
1.31 +
1.32 +lemma is_list_UNIV_iff:
1.33 + fixes xs :: "'a list"
1.34 + shows "is_list_UNIV xs \<longleftrightarrow> set xs = UNIV"
1.35 +proof
1.36 + assume "is_list_UNIV xs"
1.37 + hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))"
1.38 + unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm)
1.39 + from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV)
1.40 + have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto
1.41 + also note set_remdups
1.42 + finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV)
1.43 +next
1.44 + assume xs: "set xs = UNIV"
1.45 + from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs .
1.46 + hence "card_UNIV (TYPE ('a)) \<noteq> 0" unfolding card_UNIV_neq_0_finite_UNIV .
1.47 + moreover have "size (remdups xs) = card (set (remdups xs))"
1.48 + by(subst distinct_card) auto
1.49 + ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV)
1.50 +qed
1.51 +
1.52 +lemma card_UNIV_eq_0_is_list_UNIV_False:
1.53 + assumes cU0: "card_UNIV x = 0"
1.54 + shows "is_list_UNIV = (\<lambda>xs. False)"
1.55 +proof(rule ext)
1.56 + fix xs :: "'a list"
1.57 + from cU0 have "\<not> finite (UNIV :: 'a set)"
1.58 + by(auto simp only: card_UNIV_eq_0_infinite_UNIV)
1.59 + moreover have "finite (set xs)" by(rule finite_set)
1.60 + ultimately have "(UNIV :: 'a set) \<noteq> set xs" by(auto simp del: finite_set)
1.61 + thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp
1.62 +qed
1.63 +
1.64 +end
1.65 +
1.66 +subsection {* Instantiations for @{text "card_UNIV"} *}
1.67 +
1.68 +subsubsection {* @{typ "nat"} *}
1.69 +
1.70 +instantiation nat :: card_UNIV begin
1.71 +
1.72 +definition card_UNIV_nat_def:
1.73 + "card_UNIV_class.card_UNIV = (\<lambda>a :: nat itself. 0)"
1.74 +
1.75 +instance proof
1.76 + fix x :: "nat itself"
1.77 + show "card_UNIV x = card (UNIV :: nat set)"
1.78 + unfolding card_UNIV_nat_def by simp
1.79 +qed
1.80 +
1.81 +end
1.82 +
1.83 +subsubsection {* @{typ "int"} *}
1.84 +
1.85 +instantiation int :: card_UNIV begin
1.86 +
1.87 +definition card_UNIV_int_def:
1.88 + "card_UNIV_class.card_UNIV = (\<lambda>a :: int itself. 0)"
1.89 +
1.90 +instance proof
1.91 + fix x :: "int itself"
1.92 + show "card_UNIV x = card (UNIV :: int set)"
1.93 + unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int)
1.94 +qed
1.95 +
1.96 +end
1.97 +
1.98 +subsubsection {* @{typ "'a list"} *}
1.99 +
1.100 +instantiation list :: (type) card_UNIV begin
1.101 +
1.102 +definition card_UNIV_list_def:
1.103 + "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a list itself. 0)"
1.104 +
1.105 +instance proof
1.106 + fix x :: "'a list itself"
1.107 + show "card_UNIV x = card (UNIV :: 'a list set)"
1.108 + unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI)
1.109 +qed
1.110 +
1.111 +end
1.112 +
1.113 +subsubsection {* @{typ "unit"} *}
1.114 +
1.115 +lemma card_UNIV_unit: "card (UNIV :: unit set) = 1"
1.116 + unfolding UNIV_unit by simp
1.117 +
1.118 +instantiation unit :: card_UNIV begin
1.119 +
1.120 +definition card_UNIV_unit_def:
1.121 + "card_UNIV_class.card_UNIV = (\<lambda>a :: unit itself. 1)"
1.122 +
1.123 +instance proof
1.124 + fix x :: "unit itself"
1.125 + show "card_UNIV x = card (UNIV :: unit set)"
1.126 + by(simp add: card_UNIV_unit_def card_UNIV_unit)
1.127 +qed
1.128 +
1.129 +end
1.130 +
1.131 +subsubsection {* @{typ "bool"} *}
1.132 +
1.133 +lemma card_UNIV_bool: "card (UNIV :: bool set) = 2"
1.134 + unfolding UNIV_bool by simp
1.135 +
1.136 +instantiation bool :: card_UNIV begin
1.137 +
1.138 +definition card_UNIV_bool_def:
1.139 + "card_UNIV_class.card_UNIV = (\<lambda>a :: bool itself. 2)"
1.140 +
1.141 +instance proof
1.142 + fix x :: "bool itself"
1.143 + show "card_UNIV x = card (UNIV :: bool set)"
1.144 + by(simp add: card_UNIV_bool_def card_UNIV_bool)
1.145 +qed
1.146 +
1.147 +end
1.148 +
1.149 +subsubsection {* @{typ "char"} *}
1.150 +
1.151 +lemma card_UNIV_char: "card (UNIV :: char set) = 256"
1.152 +proof -
1.153 + from enum_distinct
1.154 + have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)"
1.155 + by (rule distinct_card)
1.156 + also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum)
1.157 + also note enum_chars
1.158 + finally show ?thesis by (simp add: chars_def)
1.159 +qed
1.160 +
1.161 +instantiation char :: card_UNIV begin
1.162 +
1.163 +definition card_UNIV_char_def:
1.164 + "card_UNIV_class.card_UNIV = (\<lambda>a :: char itself. 256)"
1.165 +
1.166 +instance proof
1.167 + fix x :: "char itself"
1.168 + show "card_UNIV x = card (UNIV :: char set)"
1.169 + by(simp add: card_UNIV_char_def card_UNIV_char)
1.170 +qed
1.171 +
1.172 +end
1.173 +
1.174 +subsubsection {* @{typ "'a \<times> 'b"} *}
1.175 +
1.176 +instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin
1.177 +
1.178 +definition card_UNIV_product_def:
1.179 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<times> 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))"
1.180 +
1.181 +instance proof
1.182 + fix x :: "('a \<times> 'b) itself"
1.183 + show "card_UNIV x = card (UNIV :: ('a \<times> 'b) set)"
1.184 + by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV)
1.185 +qed
1.186 +
1.187 +end
1.188 +
1.189 +subsubsection {* @{typ "'a + 'b"} *}
1.190 +
1.191 +instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
1.192 +
1.193 +definition card_UNIV_sum_def:
1.194 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
1.195 + in if ca \<noteq> 0 \<and> cb \<noteq> 0 then ca + cb else 0)"
1.196 +
1.197 +instance proof
1.198 + fix x :: "('a + 'b) itself"
1.199 + show "card_UNIV x = card (UNIV :: ('a + 'b) set)"
1.200 + by (auto simp add: card_UNIV_sum_def card_UNIV card_eq_0_iff UNIV_Plus_UNIV[symmetric] finite_Plus_iff Let_def card_Plus simp del: UNIV_Plus_UNIV dest!: card_ge_0_finite)
1.201 +qed
1.202 +
1.203 +end
1.204 +
1.205 +subsubsection {* @{typ "'a \<Rightarrow> 'b"} *}
1.206 +
1.207 +instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin
1.208 +
1.209 +definition card_UNIV_fun_def:
1.210 + "card_UNIV_class.card_UNIV = (\<lambda>a :: ('a \<Rightarrow> 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b))
1.211 + in if ca \<noteq> 0 \<and> cb \<noteq> 0 \<or> cb = 1 then cb ^ ca else 0)"
1.212 +
1.213 +instance proof
1.214 + fix x :: "('a \<Rightarrow> 'b) itself"
1.215 +
1.216 + { assume "0 < card (UNIV :: 'a set)"
1.217 + and "0 < card (UNIV :: 'b set)"
1.218 + hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
1.219 + by(simp_all only: card_ge_0_finite)
1.220 + from finite_distinct_list[OF finb] obtain bs
1.221 + where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
1.222 + from finite_distinct_list[OF fina] obtain as
1.223 + where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast
1.224 + have cb: "card (UNIV :: 'b set) = length bs"
1.225 + unfolding bs[symmetric] distinct_card[OF distb] ..
1.226 + have ca: "card (UNIV :: 'a set) = length as"
1.227 + unfolding as[symmetric] distinct_card[OF dista] ..
1.228 + let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
1.229 + have "UNIV = set ?xs"
1.230 + proof(rule UNIV_eq_I)
1.231 + fix f :: "'a \<Rightarrow> 'b"
1.232 + from as have "f = the \<circ> map_of (zip as (map f as))"
1.233 + by(auto simp add: map_of_zip_map intro: ext)
1.234 + thus "f \<in> set ?xs" using bs by(auto simp add: set_n_lists)
1.235 + qed
1.236 + moreover have "distinct ?xs" unfolding distinct_map
1.237 + proof(intro conjI distinct_n_lists distb inj_onI)
1.238 + fix xs ys :: "'b list"
1.239 + assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
1.240 + and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
1.241 + and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
1.242 + from xs ys have [simp]: "length xs = length as" "length ys = length as"
1.243 + by(simp_all add: length_n_lists_elem)
1.244 + have "map_of (zip as xs) = map_of (zip as ys)"
1.245 + proof
1.246 + fix x
1.247 + from as bs have "\<exists>y. map_of (zip as xs) x = Some y" "\<exists>y. map_of (zip as ys) x = Some y"
1.248 + by(simp_all add: map_of_zip_is_Some[symmetric])
1.249 + with eq show "map_of (zip as xs) x = map_of (zip as ys) x"
1.250 + by(auto dest: fun_cong[where x=x])
1.251 + qed
1.252 + with dista show "xs = ys" by(simp add: map_of_zip_inject)
1.253 + qed
1.254 + hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
1.255 + moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
1.256 + ultimately have "card (UNIV :: ('a \<Rightarrow> 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)"
1.257 + using cb ca by simp }
1.258 + moreover {
1.259 + assume cb: "card (UNIV :: 'b set) = Suc 0"
1.260 + then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
1.261 + have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
1.262 + proof(rule UNIV_eq_I)
1.263 + fix x :: "'a \<Rightarrow> 'b"
1.264 + { fix y
1.265 + have "x y \<in> UNIV" ..
1.266 + hence "x y = b" unfolding b by simp }
1.267 + thus "x \<in> {\<lambda>x. b}" by(auto intro: ext)
1.268 + qed
1.269 + have "card (UNIV :: ('a \<Rightarrow> 'b) set) = Suc 0" unfolding eq by simp }
1.270 + ultimately show "card_UNIV x = card (UNIV :: ('a \<Rightarrow> 'b) set)"
1.271 + unfolding card_UNIV_fun_def card_UNIV Let_def
1.272 + by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
1.273 +qed
1.274 +
1.275 +end
1.276 +
1.277 +subsubsection {* @{typ "'a option"} *}
1.278 +
1.279 +instantiation option :: (card_UNIV) card_UNIV
1.280 +begin
1.281 +
1.282 +definition card_UNIV_option_def:
1.283 + "card_UNIV_class.card_UNIV = (\<lambda>a :: 'a option itself. let c = card_UNIV (TYPE('a))
1.284 + in if c \<noteq> 0 then Suc c else 0)"
1.285 +
1.286 +instance proof
1.287 + fix x :: "'a option itself"
1.288 + show "card_UNIV x = card (UNIV :: 'a option set)"
1.289 + unfolding UNIV_option_conv
1.290 + by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD)
1.291 + (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite)
1.292 +qed
1.293 +
1.294 +end
1.295 +
1.296 +end
1.297 \ No newline at end of file