src/HOL/Library/Cardinality.thy
 author Andreas Lochbihler Thu May 31 16:58:38 2012 +0200 (2012-05-31) changeset 48051 53a0df441e20 parent 47221 7205eb4a0a05 child 48052 b74766e4c11e permissions -rw-r--r--
unify Card_Univ and Cardinality
 haftmann@37653 ` 1` ```(* Title: HOL/Library/Cardinality.thy ``` Andreas@48051 ` 2` ``` Author: Brian Huffman, Andreas Lochbihler ``` kleing@24332 ` 3` ```*) ``` kleing@24332 ` 4` haftmann@37653 ` 5` ```header {* Cardinality of types *} ``` kleing@24332 ` 6` haftmann@37653 ` 7` ```theory Cardinality ``` huffman@47108 ` 8` ```imports "~~/src/HOL/Main" ``` kleing@24332 ` 9` ```begin ``` kleing@24332 ` 10` kleing@24332 ` 11` ```subsection {* Preliminary lemmas *} ``` kleing@24332 ` 12` ```(* These should be moved elsewhere *) ``` kleing@24332 ` 13` kleing@24332 ` 14` ```lemma (in type_definition) univ: ``` kleing@24332 ` 15` ``` "UNIV = Abs ` A" ``` kleing@24332 ` 16` ```proof ``` kleing@24332 ` 17` ``` show "Abs ` A \ UNIV" by (rule subset_UNIV) ``` kleing@24332 ` 18` ``` show "UNIV \ Abs ` A" ``` kleing@24332 ` 19` ``` proof ``` kleing@24332 ` 20` ``` fix x :: 'b ``` kleing@24332 ` 21` ``` have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric]) ``` kleing@24332 ` 22` ``` moreover have "Rep x \ A" by (rule Rep) ``` kleing@24332 ` 23` ``` ultimately show "x \ Abs ` A" by (rule image_eqI) ``` kleing@24332 ` 24` ``` qed ``` kleing@24332 ` 25` ```qed ``` kleing@24332 ` 26` kleing@24332 ` 27` ```lemma (in type_definition) card: "card (UNIV :: 'b set) = card A" ``` kleing@24332 ` 28` ``` by (simp add: univ card_image inj_on_def Abs_inject) ``` kleing@24332 ` 29` kleing@24332 ` 30` kleing@24332 ` 31` ```subsection {* Cardinalities of types *} ``` kleing@24332 ` 32` kleing@24332 ` 33` ```syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") ``` kleing@24332 ` 34` wenzelm@35431 ` 35` ```translations "CARD('t)" => "CONST card (CONST UNIV \ 't set)" ``` kleing@24332 ` 36` wenzelm@42247 ` 37` ```typed_print_translation (advanced) {* ``` wenzelm@42247 ` 38` ``` let ``` wenzelm@42247 ` 39` ``` fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T, _]))] = ``` wenzelm@42247 ` 40` ``` Syntax.const @{syntax_const "_type_card"} \$ Syntax_Phases.term_of_typ ctxt T; ``` wenzelm@42247 ` 41` ``` in [(@{const_syntax card}, card_univ_tr')] end ``` huffman@24407 ` 42` ```*} ``` huffman@24407 ` 43` huffman@30001 ` 44` ```lemma card_unit [simp]: "CARD(unit) = 1" ``` haftmann@26153 ` 45` ``` unfolding UNIV_unit by simp ``` kleing@24332 ` 46` huffman@30001 ` 47` ```lemma card_prod [simp]: "CARD('a \ 'b) = CARD('a::finite) * CARD('b::finite)" ``` haftmann@26153 ` 48` ``` unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) ``` kleing@24332 ` 49` huffman@30001 ` 50` ```lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" ``` haftmann@26153 ` 51` ``` unfolding UNIV_Plus_UNIV [symmetric] by (simp only: finite card_Plus) ``` kleing@24332 ` 52` huffman@30001 ` 53` ```lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)" ``` nipkow@31080 ` 54` ``` unfolding UNIV_option_conv ``` kleing@24332 ` 55` ``` apply (subgoal_tac "(None::'a option) \ range Some") ``` huffman@29997 ` 56` ``` apply (simp add: card_image) ``` kleing@24332 ` 57` ``` apply fast ``` kleing@24332 ` 58` ``` done ``` kleing@24332 ` 59` huffman@30001 ` 60` ```lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" ``` haftmann@26153 ` 61` ``` unfolding Pow_UNIV [symmetric] ``` huffman@47221 ` 62` ``` by (simp only: card_Pow finite) ``` kleing@24332 ` 63` huffman@30001 ` 64` ```lemma card_nat [simp]: "CARD(nat) = 0" ``` huffman@44142 ` 65` ``` by (simp add: card_eq_0_iff) ``` huffman@30001 ` 66` huffman@30001 ` 67` huffman@30001 ` 68` ```subsection {* Classes with at least 1 and 2 *} ``` huffman@30001 ` 69` huffman@30001 ` 70` ```text {* Class finite already captures "at least 1" *} ``` huffman@30001 ` 71` huffman@30001 ` 72` ```lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)" ``` huffman@29997 ` 73` ``` unfolding neq0_conv [symmetric] by simp ``` huffman@29997 ` 74` huffman@30001 ` 75` ```lemma one_le_card_finite [simp]: "Suc 0 \ CARD('a::finite)" ``` huffman@30001 ` 76` ``` by (simp add: less_Suc_eq_le [symmetric]) ``` huffman@30001 ` 77` huffman@30001 ` 78` ```text {* Class for cardinality "at least 2" *} ``` huffman@30001 ` 79` huffman@30001 ` 80` ```class card2 = finite + ``` huffman@30001 ` 81` ``` assumes two_le_card: "2 \ CARD('a)" ``` huffman@30001 ` 82` huffman@30001 ` 83` ```lemma one_less_card: "Suc 0 < CARD('a::card2)" ``` huffman@30001 ` 84` ``` using two_le_card [where 'a='a] by simp ``` huffman@30001 ` 85` huffman@30001 ` 86` ```lemma one_less_int_card: "1 < int CARD('a::card2)" ``` huffman@30001 ` 87` ``` using one_less_card [where 'a='a] by simp ``` huffman@30001 ` 88` Andreas@48051 ` 89` ```subsection {* A type class for computing the cardinality of types *} ``` Andreas@48051 ` 90` Andreas@48051 ` 91` ```class card_UNIV = ``` Andreas@48051 ` 92` ``` fixes card_UNIV :: "'a itself \ nat" ``` Andreas@48051 ` 93` ``` assumes card_UNIV: "card_UNIV x = card (UNIV :: 'a set)" ``` Andreas@48051 ` 94` ```begin ``` Andreas@48051 ` 95` Andreas@48051 ` 96` ```lemma card_UNIV_neq_0_finite_UNIV: ``` Andreas@48051 ` 97` ``` "card_UNIV x \ 0 \ finite (UNIV :: 'a set)" ``` Andreas@48051 ` 98` ```by(simp add: card_UNIV card_eq_0_iff) ``` Andreas@48051 ` 99` Andreas@48051 ` 100` ```lemma card_UNIV_ge_0_finite_UNIV: ``` Andreas@48051 ` 101` ``` "card_UNIV x > 0 \ finite (UNIV :: 'a set)" ``` Andreas@48051 ` 102` ```by(auto simp add: card_UNIV intro: card_ge_0_finite finite_UNIV_card_ge_0) ``` Andreas@48051 ` 103` Andreas@48051 ` 104` ```lemma card_UNIV_eq_0_infinite_UNIV: ``` Andreas@48051 ` 105` ``` "card_UNIV x = 0 \ \ finite (UNIV :: 'a set)" ``` Andreas@48051 ` 106` ```by(simp add: card_UNIV card_eq_0_iff) ``` Andreas@48051 ` 107` Andreas@48051 ` 108` ```definition is_list_UNIV :: "'a list \ bool" ``` Andreas@48051 ` 109` ```where "is_list_UNIV xs = (let c = card_UNIV (TYPE('a)) in if c = 0 then False else size (remdups xs) = c)" ``` Andreas@48051 ` 110` Andreas@48051 ` 111` ```lemma is_list_UNIV_iff: fixes xs :: "'a list" ``` Andreas@48051 ` 112` ``` shows "is_list_UNIV xs \ set xs = UNIV" ``` Andreas@48051 ` 113` ```proof ``` Andreas@48051 ` 114` ``` assume "is_list_UNIV xs" ``` Andreas@48051 ` 115` ``` hence c: "card_UNIV (TYPE('a)) > 0" and xs: "size (remdups xs) = card_UNIV (TYPE('a))" ``` Andreas@48051 ` 116` ``` unfolding is_list_UNIV_def by(simp_all add: Let_def split: split_if_asm) ``` Andreas@48051 ` 117` ``` from c have fin: "finite (UNIV :: 'a set)" by(auto simp add: card_UNIV_ge_0_finite_UNIV) ``` Andreas@48051 ` 118` ``` have "card (set (remdups xs)) = size (remdups xs)" by(subst distinct_card) auto ``` Andreas@48051 ` 119` ``` also note set_remdups ``` Andreas@48051 ` 120` ``` finally show "set xs = UNIV" using fin unfolding xs card_UNIV by-(rule card_eq_UNIV_imp_eq_UNIV) ``` Andreas@48051 ` 121` ```next ``` Andreas@48051 ` 122` ``` assume xs: "set xs = UNIV" ``` Andreas@48051 ` 123` ``` from finite_set[of xs] have fin: "finite (UNIV :: 'a set)" unfolding xs . ``` Andreas@48051 ` 124` ``` hence "card_UNIV (TYPE ('a)) \ 0" unfolding card_UNIV_neq_0_finite_UNIV . ``` Andreas@48051 ` 125` ``` moreover have "size (remdups xs) = card (set (remdups xs))" ``` Andreas@48051 ` 126` ``` by(subst distinct_card) auto ``` Andreas@48051 ` 127` ``` ultimately show "is_list_UNIV xs" using xs by(simp add: is_list_UNIV_def Let_def card_UNIV) ``` Andreas@48051 ` 128` ```qed ``` Andreas@48051 ` 129` Andreas@48051 ` 130` ```lemma card_UNIV_eq_0_is_list_UNIV_False: ``` Andreas@48051 ` 131` ``` assumes cU0: "card_UNIV x = 0" ``` Andreas@48051 ` 132` ``` shows "is_list_UNIV = (\xs. False)" ``` Andreas@48051 ` 133` ```proof(rule ext) ``` Andreas@48051 ` 134` ``` fix xs :: "'a list" ``` Andreas@48051 ` 135` ``` from cU0 have "\ finite (UNIV :: 'a set)" ``` Andreas@48051 ` 136` ``` by(auto simp only: card_UNIV_eq_0_infinite_UNIV) ``` Andreas@48051 ` 137` ``` moreover have "finite (set xs)" by(rule finite_set) ``` Andreas@48051 ` 138` ``` ultimately have "(UNIV :: 'a set) \ set xs" by(auto simp del: finite_set) ``` Andreas@48051 ` 139` ``` thus "is_list_UNIV xs = False" unfolding is_list_UNIV_iff by simp ``` Andreas@48051 ` 140` ```qed ``` Andreas@48051 ` 141` huffman@29997 ` 142` ```end ``` Andreas@48051 ` 143` Andreas@48051 ` 144` ```subsection {* Instantiations for @{text "card_UNIV"} *} ``` Andreas@48051 ` 145` Andreas@48051 ` 146` ```subsubsection {* @{typ "nat"} *} ``` Andreas@48051 ` 147` Andreas@48051 ` 148` ```instantiation nat :: card_UNIV begin ``` Andreas@48051 ` 149` Andreas@48051 ` 150` ```definition "card_UNIV_class.card_UNIV = (\a :: nat itself. 0)" ``` Andreas@48051 ` 151` Andreas@48051 ` 152` ```instance proof ``` Andreas@48051 ` 153` ``` fix x :: "nat itself" ``` Andreas@48051 ` 154` ``` show "card_UNIV x = card (UNIV :: nat set)" ``` Andreas@48051 ` 155` ``` unfolding card_UNIV_nat_def by simp ``` Andreas@48051 ` 156` ```qed ``` Andreas@48051 ` 157` Andreas@48051 ` 158` ```end ``` Andreas@48051 ` 159` Andreas@48051 ` 160` ```subsubsection {* @{typ "int"} *} ``` Andreas@48051 ` 161` Andreas@48051 ` 162` ```instantiation int :: card_UNIV begin ``` Andreas@48051 ` 163` Andreas@48051 ` 164` ```definition "card_UNIV_class.card_UNIV = (\a :: int itself. 0)" ``` Andreas@48051 ` 165` Andreas@48051 ` 166` ```instance proof ``` Andreas@48051 ` 167` ``` fix x :: "int itself" ``` Andreas@48051 ` 168` ``` show "card_UNIV x = card (UNIV :: int set)" ``` Andreas@48051 ` 169` ``` unfolding card_UNIV_int_def by(simp add: infinite_UNIV_int) ``` Andreas@48051 ` 170` ```qed ``` Andreas@48051 ` 171` Andreas@48051 ` 172` ```end ``` Andreas@48051 ` 173` Andreas@48051 ` 174` ```subsubsection {* @{typ "'a list"} *} ``` Andreas@48051 ` 175` Andreas@48051 ` 176` ```instantiation list :: (type) card_UNIV begin ``` Andreas@48051 ` 177` Andreas@48051 ` 178` ```definition "card_UNIV_class.card_UNIV = (\a :: 'a list itself. 0)" ``` Andreas@48051 ` 179` Andreas@48051 ` 180` ```instance proof ``` Andreas@48051 ` 181` ``` fix x :: "'a list itself" ``` Andreas@48051 ` 182` ``` show "card_UNIV x = card (UNIV :: 'a list set)" ``` Andreas@48051 ` 183` ``` unfolding card_UNIV_list_def by(simp add: infinite_UNIV_listI) ``` Andreas@48051 ` 184` ```qed ``` Andreas@48051 ` 185` Andreas@48051 ` 186` ```end ``` Andreas@48051 ` 187` Andreas@48051 ` 188` ```subsubsection {* @{typ "unit"} *} ``` Andreas@48051 ` 189` Andreas@48051 ` 190` ```lemma card_UNIV_unit: "card (UNIV :: unit set) = 1" ``` Andreas@48051 ` 191` ``` unfolding UNIV_unit by simp ``` Andreas@48051 ` 192` Andreas@48051 ` 193` ```instantiation unit :: card_UNIV begin ``` Andreas@48051 ` 194` Andreas@48051 ` 195` ```definition card_UNIV_unit_def: ``` Andreas@48051 ` 196` ``` "card_UNIV_class.card_UNIV = (\a :: unit itself. 1)" ``` Andreas@48051 ` 197` Andreas@48051 ` 198` ```instance proof ``` Andreas@48051 ` 199` ``` fix x :: "unit itself" ``` Andreas@48051 ` 200` ``` show "card_UNIV x = card (UNIV :: unit set)" ``` Andreas@48051 ` 201` ``` by(simp add: card_UNIV_unit_def card_UNIV_unit) ``` Andreas@48051 ` 202` ```qed ``` Andreas@48051 ` 203` Andreas@48051 ` 204` ```end ``` Andreas@48051 ` 205` Andreas@48051 ` 206` ```subsubsection {* @{typ "bool"} *} ``` Andreas@48051 ` 207` Andreas@48051 ` 208` ```lemma card_UNIV_bool: "card (UNIV :: bool set) = 2" ``` Andreas@48051 ` 209` ``` unfolding UNIV_bool by simp ``` Andreas@48051 ` 210` Andreas@48051 ` 211` ```instantiation bool :: card_UNIV begin ``` Andreas@48051 ` 212` Andreas@48051 ` 213` ```definition card_UNIV_bool_def: ``` Andreas@48051 ` 214` ``` "card_UNIV_class.card_UNIV = (\a :: bool itself. 2)" ``` Andreas@48051 ` 215` Andreas@48051 ` 216` ```instance proof ``` Andreas@48051 ` 217` ``` fix x :: "bool itself" ``` Andreas@48051 ` 218` ``` show "card_UNIV x = card (UNIV :: bool set)" ``` Andreas@48051 ` 219` ``` by(simp add: card_UNIV_bool_def card_UNIV_bool) ``` Andreas@48051 ` 220` ```qed ``` Andreas@48051 ` 221` Andreas@48051 ` 222` ```end ``` Andreas@48051 ` 223` Andreas@48051 ` 224` ```subsubsection {* @{typ "char"} *} ``` Andreas@48051 ` 225` Andreas@48051 ` 226` ```lemma card_UNIV_char: "card (UNIV :: char set) = 256" ``` Andreas@48051 ` 227` ```proof - ``` Andreas@48051 ` 228` ``` from enum_distinct ``` Andreas@48051 ` 229` ``` have "card (set (Enum.enum :: char list)) = length (Enum.enum :: char list)" ``` Andreas@48051 ` 230` ``` by (rule distinct_card) ``` Andreas@48051 ` 231` ``` also have "set Enum.enum = (UNIV :: char set)" by (auto intro: in_enum) ``` Andreas@48051 ` 232` ``` also note enum_chars ``` Andreas@48051 ` 233` ``` finally show ?thesis by (simp add: chars_def) ``` Andreas@48051 ` 234` ```qed ``` Andreas@48051 ` 235` Andreas@48051 ` 236` ```instantiation char :: card_UNIV begin ``` Andreas@48051 ` 237` Andreas@48051 ` 238` ```definition card_UNIV_char_def: ``` Andreas@48051 ` 239` ``` "card_UNIV_class.card_UNIV = (\a :: char itself. 256)" ``` Andreas@48051 ` 240` Andreas@48051 ` 241` ```instance proof ``` Andreas@48051 ` 242` ``` fix x :: "char itself" ``` Andreas@48051 ` 243` ``` show "card_UNIV x = card (UNIV :: char set)" ``` Andreas@48051 ` 244` ``` by(simp add: card_UNIV_char_def card_UNIV_char) ``` Andreas@48051 ` 245` ```qed ``` Andreas@48051 ` 246` Andreas@48051 ` 247` ```end ``` Andreas@48051 ` 248` Andreas@48051 ` 249` ```subsubsection {* @{typ "'a \ 'b"} *} ``` Andreas@48051 ` 250` Andreas@48051 ` 251` ```instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin ``` Andreas@48051 ` 252` Andreas@48051 ` 253` ```definition card_UNIV_product_def: ``` Andreas@48051 ` 254` ``` "card_UNIV_class.card_UNIV = (\a :: ('a \ 'b) itself. card_UNIV (TYPE('a)) * card_UNIV (TYPE('b)))" ``` Andreas@48051 ` 255` Andreas@48051 ` 256` ```instance proof ``` Andreas@48051 ` 257` ``` fix x :: "('a \ 'b) itself" ``` Andreas@48051 ` 258` ``` show "card_UNIV x = card (UNIV :: ('a \ 'b) set)" ``` Andreas@48051 ` 259` ``` by(simp add: card_UNIV_product_def card_UNIV UNIV_Times_UNIV[symmetric] card_cartesian_product del: UNIV_Times_UNIV) ``` Andreas@48051 ` 260` ```qed ``` Andreas@48051 ` 261` Andreas@48051 ` 262` ```end ``` Andreas@48051 ` 263` Andreas@48051 ` 264` ```subsubsection {* @{typ "'a + 'b"} *} ``` Andreas@48051 ` 265` Andreas@48051 ` 266` ```instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin ``` Andreas@48051 ` 267` Andreas@48051 ` 268` ```definition card_UNIV_sum_def: ``` Andreas@48051 ` 269` ``` "card_UNIV_class.card_UNIV = (\a :: ('a + 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b)) ``` Andreas@48051 ` 270` ``` in if ca \ 0 \ cb \ 0 then ca + cb else 0)" ``` Andreas@48051 ` 271` Andreas@48051 ` 272` ```instance proof ``` Andreas@48051 ` 273` ``` fix x :: "('a + 'b) itself" ``` Andreas@48051 ` 274` ``` show "card_UNIV x = card (UNIV :: ('a + 'b) set)" ``` Andreas@48051 ` 275` ``` 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) ``` Andreas@48051 ` 276` ```qed ``` Andreas@48051 ` 277` Andreas@48051 ` 278` ```end ``` Andreas@48051 ` 279` Andreas@48051 ` 280` ```subsubsection {* @{typ "'a \ 'b"} *} ``` Andreas@48051 ` 281` Andreas@48051 ` 282` ```instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin ``` Andreas@48051 ` 283` Andreas@48051 ` 284` ```definition card_UNIV_fun_def: ``` Andreas@48051 ` 285` ``` "card_UNIV_class.card_UNIV = (\a :: ('a \ 'b) itself. let ca = card_UNIV (TYPE('a)); cb = card_UNIV (TYPE('b)) ``` Andreas@48051 ` 286` ``` in if ca \ 0 \ cb \ 0 \ cb = 1 then cb ^ ca else 0)" ``` Andreas@48051 ` 287` Andreas@48051 ` 288` ```instance proof ``` Andreas@48051 ` 289` ``` fix x :: "('a \ 'b) itself" ``` Andreas@48051 ` 290` Andreas@48051 ` 291` ``` { assume "0 < card (UNIV :: 'a set)" ``` Andreas@48051 ` 292` ``` and "0 < card (UNIV :: 'b set)" ``` Andreas@48051 ` 293` ``` hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)" ``` Andreas@48051 ` 294` ``` by(simp_all only: card_ge_0_finite) ``` Andreas@48051 ` 295` ``` from finite_distinct_list[OF finb] obtain bs ``` Andreas@48051 ` 296` ``` where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast ``` Andreas@48051 ` 297` ``` from finite_distinct_list[OF fina] obtain as ``` Andreas@48051 ` 298` ``` where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast ``` Andreas@48051 ` 299` ``` have cb: "card (UNIV :: 'b set) = length bs" ``` Andreas@48051 ` 300` ``` unfolding bs[symmetric] distinct_card[OF distb] .. ``` Andreas@48051 ` 301` ``` have ca: "card (UNIV :: 'a set) = length as" ``` Andreas@48051 ` 302` ``` unfolding as[symmetric] distinct_card[OF dista] .. ``` Andreas@48051 ` 303` ``` let ?xs = "map (\ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)" ``` Andreas@48051 ` 304` ``` have "UNIV = set ?xs" ``` Andreas@48051 ` 305` ``` proof(rule UNIV_eq_I) ``` Andreas@48051 ` 306` ``` fix f :: "'a \ 'b" ``` Andreas@48051 ` 307` ``` from as have "f = the \ map_of (zip as (map f as))" ``` Andreas@48051 ` 308` ``` by(auto simp add: map_of_zip_map intro: ext) ``` Andreas@48051 ` 309` ``` thus "f \ set ?xs" using bs by(auto simp add: set_n_lists) ``` Andreas@48051 ` 310` ``` qed ``` Andreas@48051 ` 311` ``` moreover have "distinct ?xs" unfolding distinct_map ``` Andreas@48051 ` 312` ``` proof(intro conjI distinct_n_lists distb inj_onI) ``` Andreas@48051 ` 313` ``` fix xs ys :: "'b list" ``` Andreas@48051 ` 314` ``` assume xs: "xs \ set (Enum.n_lists (length as) bs)" ``` Andreas@48051 ` 315` ``` and ys: "ys \ set (Enum.n_lists (length as) bs)" ``` Andreas@48051 ` 316` ``` and eq: "the \ map_of (zip as xs) = the \ map_of (zip as ys)" ``` Andreas@48051 ` 317` ``` from xs ys have [simp]: "length xs = length as" "length ys = length as" ``` Andreas@48051 ` 318` ``` by(simp_all add: length_n_lists_elem) ``` Andreas@48051 ` 319` ``` have "map_of (zip as xs) = map_of (zip as ys)" ``` Andreas@48051 ` 320` ``` proof ``` Andreas@48051 ` 321` ``` fix x ``` Andreas@48051 ` 322` ``` from as bs have "\y. map_of (zip as xs) x = Some y" "\y. map_of (zip as ys) x = Some y" ``` Andreas@48051 ` 323` ``` by(simp_all add: map_of_zip_is_Some[symmetric]) ``` Andreas@48051 ` 324` ``` with eq show "map_of (zip as xs) x = map_of (zip as ys) x" ``` Andreas@48051 ` 325` ``` by(auto dest: fun_cong[where x=x]) ``` Andreas@48051 ` 326` ``` qed ``` Andreas@48051 ` 327` ``` with dista show "xs = ys" by(simp add: map_of_zip_inject) ``` Andreas@48051 ` 328` ``` qed ``` Andreas@48051 ` 329` ``` hence "card (set ?xs) = length ?xs" by(simp only: distinct_card) ``` Andreas@48051 ` 330` ``` moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists) ``` Andreas@48051 ` 331` ``` ultimately have "card (UNIV :: ('a \ 'b) set) = card (UNIV :: 'b set) ^ card (UNIV :: 'a set)" ``` Andreas@48051 ` 332` ``` using cb ca by simp } ``` Andreas@48051 ` 333` ``` moreover { ``` Andreas@48051 ` 334` ``` assume cb: "card (UNIV :: 'b set) = Suc 0" ``` Andreas@48051 ` 335` ``` then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq) ``` Andreas@48051 ` 336` ``` have eq: "UNIV = {\x :: 'a. b ::'b}" ``` Andreas@48051 ` 337` ``` proof(rule UNIV_eq_I) ``` Andreas@48051 ` 338` ``` fix x :: "'a \ 'b" ``` Andreas@48051 ` 339` ``` { fix y ``` Andreas@48051 ` 340` ``` have "x y \ UNIV" .. ``` Andreas@48051 ` 341` ``` hence "x y = b" unfolding b by simp } ``` Andreas@48051 ` 342` ``` thus "x \ {\x. b}" by(auto intro: ext) ``` Andreas@48051 ` 343` ``` qed ``` Andreas@48051 ` 344` ``` have "card (UNIV :: ('a \ 'b) set) = Suc 0" unfolding eq by simp } ``` Andreas@48051 ` 345` ``` ultimately show "card_UNIV x = card (UNIV :: ('a \ 'b) set)" ``` Andreas@48051 ` 346` ``` unfolding card_UNIV_fun_def card_UNIV Let_def ``` Andreas@48051 ` 347` ``` by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1) ``` Andreas@48051 ` 348` ```qed ``` Andreas@48051 ` 349` Andreas@48051 ` 350` ```end ``` Andreas@48051 ` 351` Andreas@48051 ` 352` ```subsubsection {* @{typ "'a option"} *} ``` Andreas@48051 ` 353` Andreas@48051 ` 354` ```instantiation option :: (card_UNIV) card_UNIV ``` Andreas@48051 ` 355` ```begin ``` Andreas@48051 ` 356` Andreas@48051 ` 357` ```definition card_UNIV_option_def: ``` Andreas@48051 ` 358` ``` "card_UNIV_class.card_UNIV = (\a :: 'a option itself. let c = card_UNIV (TYPE('a)) ``` Andreas@48051 ` 359` ``` in if c \ 0 then Suc c else 0)" ``` Andreas@48051 ` 360` Andreas@48051 ` 361` ```instance proof ``` Andreas@48051 ` 362` ``` fix x :: "'a option itself" ``` Andreas@48051 ` 363` ``` show "card_UNIV x = card (UNIV :: 'a option set)" ``` Andreas@48051 ` 364` ``` unfolding UNIV_option_conv ``` Andreas@48051 ` 365` ``` by(auto simp add: card_UNIV_option_def card_UNIV card_eq_0_iff Let_def intro: inj_Some dest: finite_imageD) ``` Andreas@48051 ` 366` ``` (subst card_insert_disjoint, auto simp add: card_eq_0_iff card_image inj_Some intro: finite_imageI card_ge_0_finite) ``` Andreas@48051 ` 367` ```qed ``` Andreas@48051 ` 368` Andreas@48051 ` 369` ```end ``` Andreas@48051 ` 370` Andreas@48051 ` 371` ```subsection {* Code setup for equality on sets *} ``` Andreas@48051 ` 372` Andreas@48051 ` 373` ```definition eq_set :: "'a :: card_UNIV set \ 'a :: card_UNIV set \ bool" ``` Andreas@48051 ` 374` ```where [simp, code del]: "eq_set = op =" ``` Andreas@48051 ` 375` Andreas@48051 ` 376` ```lemmas [code_unfold] = eq_set_def[symmetric] ``` Andreas@48051 ` 377` Andreas@48051 ` 378` ```lemma card_Compl: ``` Andreas@48051 ` 379` ``` "finite A \ card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)" ``` Andreas@48051 ` 380` ```by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) ``` Andreas@48051 ` 381` Andreas@48051 ` 382` ```lemma eq_set_code [code]: ``` Andreas@48051 ` 383` ``` fixes xs ys :: "'a :: card_UNIV list" ``` Andreas@48051 ` 384` ``` defines "rhs \ ``` Andreas@48051 ` 385` ``` let n = card_UNIV TYPE('a) ``` Andreas@48051 ` 386` ``` in if n = 0 then False else ``` Andreas@48051 ` 387` ``` let xs' = remdups xs; ys' = remdups ys ``` Andreas@48051 ` 388` ``` in length xs' + length ys' = n \ (\x \ set xs'. x \ set ys') \ (\y \ set ys'. y \ set xs')" ``` Andreas@48051 ` 389` ``` shows "eq_set (List.coset xs) (set ys) \ rhs" (is ?thesis1) ``` Andreas@48051 ` 390` ``` and "eq_set (set ys) (List.coset xs) \ rhs" (is ?thesis2) ``` Andreas@48051 ` 391` ``` and "eq_set (set xs) (set ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis3) ``` Andreas@48051 ` 392` ``` and "eq_set (List.coset xs) (List.coset ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" (is ?thesis4) ``` Andreas@48051 ` 393` ```proof - ``` Andreas@48051 ` 394` ``` show ?thesis1 (is "?lhs \ ?rhs") ``` Andreas@48051 ` 395` ``` proof ``` Andreas@48051 ` 396` ``` assume ?lhs thus ?rhs ``` Andreas@48051 ` 397` ``` by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) ``` Andreas@48051 ` 398` ``` next ``` Andreas@48051 ` 399` ``` assume ?rhs ``` Andreas@48051 ` 400` ``` moreover have "\ \y\set xs. y \ set ys; \x\set ys. x \ set xs \ \ set xs \ set ys = {}" by blast ``` Andreas@48051 ` 401` ``` ultimately show ?lhs ``` Andreas@48051 ` 402` ``` by(auto simp add: rhs_def Let_def List.card_set[symmetric] card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] dest: card_eq_UNIV_imp_eq_UNIV split: split_if_asm) ``` Andreas@48051 ` 403` ``` qed ``` Andreas@48051 ` 404` ``` thus ?thesis2 unfolding eq_set_def by blast ``` Andreas@48051 ` 405` ``` show ?thesis3 ?thesis4 unfolding eq_set_def List.coset_def by blast+ ``` Andreas@48051 ` 406` ```qed ``` Andreas@48051 ` 407` Andreas@48051 ` 408` ```(* test code setup *) ``` Andreas@48051 ` 409` ```value [code] "List.coset [True] = set [False] \ set [] = List.coset [True, False]" ``` Andreas@48051 ` 410` Andreas@48051 ` 411` ```end ```