src/HOL/Library/Cardinality.thy
 author wenzelm Tue Jan 16 09:30:00 2018 +0100 (19 months ago) changeset 67443 3abf6a722518 parent 67399 eab6ce8368fa child 68011 fb6469cdf094 permissions -rw-r--r--
 haftmann@37653 ` 1` ```(* Title: HOL/Library/Cardinality.thy ``` Andreas@48051 ` 2` ``` Author: Brian Huffman, Andreas Lochbihler ``` kleing@24332 ` 3` ```*) ``` kleing@24332 ` 4` wenzelm@60500 ` 5` ```section \Cardinality of types\ ``` kleing@24332 ` 6` haftmann@37653 ` 7` ```theory Cardinality ``` Andreas@48164 ` 8` ```imports Phantom_Type ``` kleing@24332 ` 9` ```begin ``` kleing@24332 ` 10` wenzelm@60500 ` 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` Andreas@48060 ` 30` ```lemma finite_range_Some: "finite (range (Some :: 'a \ 'a option)) = finite (UNIV :: 'a set)" ``` Andreas@48060 ` 31` ```by(auto dest: finite_imageD intro: inj_Some) ``` Andreas@48060 ` 32` Andreas@48176 ` 33` ```lemma infinite_literal: "\ finite (UNIV :: String.literal set)" ``` Andreas@48176 ` 34` ```proof - ``` Andreas@48176 ` 35` ``` have "inj STR" by(auto intro: injI) ``` Andreas@48176 ` 36` ``` thus ?thesis ``` Andreas@48176 ` 37` ``` by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD) ``` Andreas@48176 ` 38` ```qed ``` kleing@24332 ` 39` wenzelm@60500 ` 40` ```subsection \Cardinalities of types\ ``` kleing@24332 ` 41` kleing@24332 ` 42` ```syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))") ``` kleing@24332 ` 43` wenzelm@61076 ` 44` ```translations "CARD('t)" => "CONST card (CONST UNIV :: 't set)" ``` kleing@24332 ` 45` wenzelm@60500 ` 46` ```print_translation \ ``` wenzelm@42247 ` 47` ``` let ``` wenzelm@52147 ` 48` ``` fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] = ``` wenzelm@49689 ` 49` ``` Syntax.const @{syntax_const "_type_card"} \$ Syntax_Phases.term_of_typ ctxt T ``` wenzelm@42247 ` 50` ``` in [(@{const_syntax card}, card_univ_tr')] end ``` wenzelm@60500 ` 51` ```\ ``` huffman@24407 ` 52` Andreas@48058 ` 53` ```lemma card_prod [simp]: "CARD('a \ 'b) = CARD('a) * CARD('b)" ``` haftmann@26153 ` 54` ``` unfolding UNIV_Times_UNIV [symmetric] by (simp only: card_cartesian_product) ``` kleing@24332 ` 55` Andreas@48060 ` 56` ```lemma card_UNIV_sum: "CARD('a + 'b) = (if CARD('a) \ 0 \ CARD('b) \ 0 then CARD('a) + CARD('b) else 0)" ``` Andreas@48060 ` 57` ```unfolding UNIV_Plus_UNIV[symmetric] ``` Andreas@48060 ` 58` ```by(auto simp add: card_eq_0_iff card_Plus simp del: UNIV_Plus_UNIV) ``` Andreas@48060 ` 59` huffman@30001 ` 60` ```lemma card_sum [simp]: "CARD('a + 'b) = CARD('a::finite) + CARD('b::finite)" ``` Andreas@48060 ` 61` ```by(simp add: card_UNIV_sum) ``` Andreas@48060 ` 62` Andreas@48060 ` 63` ```lemma card_UNIV_option: "CARD('a option) = (if CARD('a) = 0 then 0 else CARD('a) + 1)" ``` Andreas@48060 ` 64` ```proof - ``` Andreas@48060 ` 65` ``` have "(None :: 'a option) \ range Some" by clarsimp ``` Andreas@48060 ` 66` ``` thus ?thesis ``` wenzelm@53191 ` 67` ``` by (simp add: UNIV_option_conv card_eq_0_iff finite_range_Some card_image) ``` Andreas@48060 ` 68` ```qed ``` kleing@24332 ` 69` huffman@30001 ` 70` ```lemma card_option [simp]: "CARD('a option) = Suc CARD('a::finite)" ``` Andreas@48060 ` 71` ```by(simp add: card_UNIV_option) ``` Andreas@48060 ` 72` Andreas@48060 ` 73` ```lemma card_UNIV_set: "CARD('a set) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))" ``` Andreas@48060 ` 74` ```by(simp add: Pow_UNIV[symmetric] card_eq_0_iff card_Pow del: Pow_UNIV) ``` kleing@24332 ` 75` huffman@30001 ` 76` ```lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)" ``` Andreas@48060 ` 77` ```by(simp add: card_UNIV_set) ``` kleing@24332 ` 78` huffman@30001 ` 79` ```lemma card_nat [simp]: "CARD(nat) = 0" ``` huffman@44142 ` 80` ``` by (simp add: card_eq_0_iff) ``` huffman@30001 ` 81` Andreas@48060 ` 82` ```lemma card_fun: "CARD('a \ 'b) = (if CARD('a) \ 0 \ CARD('b) \ 0 \ CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)" ``` Andreas@48060 ` 83` ```proof - ``` Andreas@48060 ` 84` ``` { assume "0 < CARD('a)" and "0 < CARD('b)" ``` Andreas@48060 ` 85` ``` hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)" ``` Andreas@48060 ` 86` ``` by(simp_all only: card_ge_0_finite) ``` Andreas@48060 ` 87` ``` from finite_distinct_list[OF finb] obtain bs ``` Andreas@48060 ` 88` ``` where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast ``` Andreas@48060 ` 89` ``` from finite_distinct_list[OF fina] obtain as ``` Andreas@48060 ` 90` ``` where as: "set as = (UNIV :: 'a set)" and dista: "distinct as" by blast ``` Andreas@48060 ` 91` ``` have cb: "CARD('b) = length bs" ``` Andreas@48060 ` 92` ``` unfolding bs[symmetric] distinct_card[OF distb] .. ``` Andreas@48060 ` 93` ``` have ca: "CARD('a) = length as" ``` Andreas@48060 ` 94` ``` unfolding as[symmetric] distinct_card[OF dista] .. ``` wenzelm@67091 ` 95` ``` let ?xs = "map (\ys. the \ map_of (zip as ys)) (List.n_lists (length as) bs)" ``` Andreas@48060 ` 96` ``` have "UNIV = set ?xs" ``` Andreas@48060 ` 97` ``` proof(rule UNIV_eq_I) ``` Andreas@48060 ` 98` ``` fix f :: "'a \ 'b" ``` Andreas@48060 ` 99` ``` from as have "f = the \ map_of (zip as (map f as))" ``` Andreas@48060 ` 100` ``` by(auto simp add: map_of_zip_map) ``` Andreas@48060 ` 101` ``` thus "f \ set ?xs" using bs by(auto simp add: set_n_lists) ``` Andreas@48060 ` 102` ``` qed ``` Andreas@48060 ` 103` ``` moreover have "distinct ?xs" unfolding distinct_map ``` Andreas@48060 ` 104` ``` proof(intro conjI distinct_n_lists distb inj_onI) ``` Andreas@48060 ` 105` ``` fix xs ys :: "'b list" ``` haftmann@49948 ` 106` ``` assume xs: "xs \ set (List.n_lists (length as) bs)" ``` haftmann@49948 ` 107` ``` and ys: "ys \ set (List.n_lists (length as) bs)" ``` Andreas@48060 ` 108` ``` and eq: "the \ map_of (zip as xs) = the \ map_of (zip as ys)" ``` Andreas@48060 ` 109` ``` from xs ys have [simp]: "length xs = length as" "length ys = length as" ``` Andreas@48060 ` 110` ``` by(simp_all add: length_n_lists_elem) ``` Andreas@48060 ` 111` ``` have "map_of (zip as xs) = map_of (zip as ys)" ``` Andreas@48060 ` 112` ``` proof ``` Andreas@48060 ` 113` ``` fix x ``` Andreas@48060 ` 114` ``` from as bs have "\y. map_of (zip as xs) x = Some y" "\y. map_of (zip as ys) x = Some y" ``` Andreas@48060 ` 115` ``` by(simp_all add: map_of_zip_is_Some[symmetric]) ``` Andreas@48060 ` 116` ``` with eq show "map_of (zip as xs) x = map_of (zip as ys) x" ``` Andreas@48060 ` 117` ``` by(auto dest: fun_cong[where x=x]) ``` Andreas@48060 ` 118` ``` qed ``` Andreas@48060 ` 119` ``` with dista show "xs = ys" by(simp add: map_of_zip_inject) ``` Andreas@48060 ` 120` ``` qed ``` Andreas@48060 ` 121` ``` hence "card (set ?xs) = length ?xs" by(simp only: distinct_card) ``` Andreas@48060 ` 122` ``` moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists) ``` Andreas@48060 ` 123` ``` ultimately have "CARD('a \ 'b) = CARD('b) ^ CARD('a)" using cb ca by simp } ``` Andreas@48060 ` 124` ``` moreover { ``` Andreas@48060 ` 125` ``` assume cb: "CARD('b) = 1" ``` Andreas@48060 ` 126` ``` then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq) ``` Andreas@48060 ` 127` ``` have eq: "UNIV = {\x :: 'a. b ::'b}" ``` Andreas@48060 ` 128` ``` proof(rule UNIV_eq_I) ``` Andreas@48060 ` 129` ``` fix x :: "'a \ 'b" ``` Andreas@48060 ` 130` ``` { fix y ``` Andreas@48060 ` 131` ``` have "x y \ UNIV" .. ``` Andreas@48060 ` 132` ``` hence "x y = b" unfolding b by simp } ``` Andreas@48060 ` 133` ``` thus "x \ {\x. b}" by(auto) ``` Andreas@48060 ` 134` ``` qed ``` Andreas@48060 ` 135` ``` have "CARD('a \ 'b) = 1" unfolding eq by simp } ``` Andreas@48060 ` 136` ``` ultimately show ?thesis ``` Andreas@48060 ` 137` ``` by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1) ``` Andreas@48060 ` 138` ```qed ``` Andreas@48060 ` 139` Andreas@48176 ` 140` ```corollary finite_UNIV_fun: ``` Andreas@48176 ` 141` ``` "finite (UNIV :: ('a \ 'b) set) \ ``` Andreas@48176 ` 142` ``` finite (UNIV :: 'a set) \ finite (UNIV :: 'b set) \ CARD('b) = 1" ``` Andreas@48176 ` 143` ``` (is "?lhs \ ?rhs") ``` Andreas@48176 ` 144` ```proof - ``` Andreas@48176 ` 145` ``` have "?lhs \ CARD('a \ 'b) > 0" by(simp add: card_gt_0_iff) ``` Andreas@48176 ` 146` ``` also have "\ \ CARD('a) > 0 \ CARD('b) > 0 \ CARD('b) = 1" ``` Andreas@48176 ` 147` ``` by(simp add: card_fun) ``` Andreas@48176 ` 148` ``` also have "\ = ?rhs" by(simp add: card_gt_0_iff) ``` Andreas@48176 ` 149` ``` finally show ?thesis . ``` Andreas@48176 ` 150` ```qed ``` Andreas@48176 ` 151` Andreas@48060 ` 152` ```lemma card_literal: "CARD(String.literal) = 0" ``` Andreas@48176 ` 153` ```by(simp add: card_eq_0_iff infinite_literal) ``` huffman@30001 ` 154` wenzelm@60500 ` 155` ```subsection \Classes with at least 1 and 2\ ``` huffman@30001 ` 156` wenzelm@60500 ` 157` ```text \Class finite already captures "at least 1"\ ``` huffman@30001 ` 158` huffman@30001 ` 159` ```lemma zero_less_card_finite [simp]: "0 < CARD('a::finite)" ``` huffman@29997 ` 160` ``` unfolding neq0_conv [symmetric] by simp ``` huffman@29997 ` 161` huffman@30001 ` 162` ```lemma one_le_card_finite [simp]: "Suc 0 \ CARD('a::finite)" ``` huffman@30001 ` 163` ``` by (simp add: less_Suc_eq_le [symmetric]) ``` huffman@30001 ` 164` wenzelm@60500 ` 165` ```text \Class for cardinality "at least 2"\ ``` huffman@30001 ` 166` huffman@30001 ` 167` ```class card2 = finite + ``` huffman@30001 ` 168` ``` assumes two_le_card: "2 \ CARD('a)" ``` huffman@30001 ` 169` huffman@30001 ` 170` ```lemma one_less_card: "Suc 0 < CARD('a::card2)" ``` huffman@30001 ` 171` ``` using two_le_card [where 'a='a] by simp ``` huffman@30001 ` 172` huffman@30001 ` 173` ```lemma one_less_int_card: "1 < int CARD('a::card2)" ``` huffman@30001 ` 174` ``` using one_less_card [where 'a='a] by simp ``` huffman@30001 ` 175` Andreas@48176 ` 176` wenzelm@60500 ` 177` ```subsection \A type class for deciding finiteness of types\ ``` Andreas@48176 ` 178` Andreas@48176 ` 179` ```type_synonym 'a finite_UNIV = "('a, bool) phantom" ``` Andreas@48176 ` 180` Andreas@48176 ` 181` ```class finite_UNIV = ``` Andreas@48176 ` 182` ``` fixes finite_UNIV :: "('a, bool) phantom" ``` Andreas@48176 ` 183` ``` assumes finite_UNIV: "finite_UNIV = Phantom('a) (finite (UNIV :: 'a set))" ``` Andreas@48176 ` 184` Andreas@48176 ` 185` ```lemma finite_UNIV_code [code_unfold]: ``` Andreas@48176 ` 186` ``` "finite (UNIV :: 'a :: finite_UNIV set) ``` Andreas@48176 ` 187` ``` \ of_phantom (finite_UNIV :: 'a finite_UNIV)" ``` Andreas@48176 ` 188` ```by(simp add: finite_UNIV) ``` Andreas@48176 ` 189` wenzelm@60500 ` 190` ```subsection \A type class for computing the cardinality of types\ ``` Andreas@48051 ` 191` Andreas@48059 ` 192` ```definition is_list_UNIV :: "'a list \ bool" ``` Andreas@51116 ` 193` ```where "is_list_UNIV xs = (let c = CARD('a) in if c = 0 then False else size (remdups xs) = c)" ``` Andreas@48059 ` 194` Andreas@48059 ` 195` ```lemma is_list_UNIV_iff: "is_list_UNIV xs \ set xs = UNIV" ``` Andreas@48059 ` 196` ```by(auto simp add: is_list_UNIV_def Let_def card_eq_0_iff List.card_set[symmetric] ``` Andreas@48059 ` 197` ``` dest: subst[where P="finite", OF _ finite_set] card_eq_UNIV_imp_eq_UNIV) ``` Andreas@48059 ` 198` Andreas@48164 ` 199` ```type_synonym 'a card_UNIV = "('a, nat) phantom" ``` Andreas@48164 ` 200` Andreas@48176 ` 201` ```class card_UNIV = finite_UNIV + ``` Andreas@48164 ` 202` ``` fixes card_UNIV :: "'a card_UNIV" ``` Andreas@48164 ` 203` ``` assumes card_UNIV: "card_UNIV = Phantom('a) CARD('a)" ``` Andreas@48051 ` 204` wenzelm@61585 ` 205` ```subsection \Instantiations for \card_UNIV\\ ``` Andreas@48051 ` 206` Andreas@48051 ` 207` ```instantiation nat :: card_UNIV begin ``` Andreas@48176 ` 208` ```definition "finite_UNIV = Phantom(nat) False" ``` Andreas@48164 ` 209` ```definition "card_UNIV = Phantom(nat) 0" ``` Andreas@48176 ` 210` ```instance by intro_classes (simp_all add: finite_UNIV_nat_def card_UNIV_nat_def) ``` Andreas@48051 ` 211` ```end ``` Andreas@48051 ` 212` Andreas@48051 ` 213` ```instantiation int :: card_UNIV begin ``` Andreas@48176 ` 214` ```definition "finite_UNIV = Phantom(int) False" ``` Andreas@48164 ` 215` ```definition "card_UNIV = Phantom(int) 0" ``` Andreas@48176 ` 216` ```instance by intro_classes (simp_all add: card_UNIV_int_def finite_UNIV_int_def infinite_UNIV_int) ``` Andreas@48051 ` 217` ```end ``` Andreas@48051 ` 218` haftmann@51143 ` 219` ```instantiation natural :: card_UNIV begin ``` haftmann@51143 ` 220` ```definition "finite_UNIV = Phantom(natural) False" ``` haftmann@51143 ` 221` ```definition "card_UNIV = Phantom(natural) 0" ``` wenzelm@60679 ` 222` ```instance ``` wenzelm@60679 ` 223` ``` by standard ``` wenzelm@60679 ` 224` ``` (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff ``` wenzelm@60679 ` 225` ``` type_definition.univ [OF type_definition_natural] natural_eq_iff ``` wenzelm@60679 ` 226` ``` dest!: finite_imageD intro: inj_onI) ``` haftmann@51143 ` 227` ```end ``` haftmann@51143 ` 228` haftmann@51143 ` 229` ```instantiation integer :: card_UNIV begin ``` haftmann@51143 ` 230` ```definition "finite_UNIV = Phantom(integer) False" ``` haftmann@51143 ` 231` ```definition "card_UNIV = Phantom(integer) 0" ``` wenzelm@60679 ` 232` ```instance ``` wenzelm@60679 ` 233` ``` by standard ``` wenzelm@60679 ` 234` ``` (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff ``` wenzelm@60679 ` 235` ``` type_definition.univ [OF type_definition_integer] infinite_UNIV_int ``` wenzelm@60679 ` 236` ``` dest!: finite_imageD intro: inj_onI) ``` Andreas@48165 ` 237` ```end ``` Andreas@48165 ` 238` Andreas@48051 ` 239` ```instantiation list :: (type) card_UNIV begin ``` Andreas@48176 ` 240` ```definition "finite_UNIV = Phantom('a list) False" ``` Andreas@48164 ` 241` ```definition "card_UNIV = Phantom('a list) 0" ``` Andreas@48176 ` 242` ```instance by intro_classes (simp_all add: card_UNIV_list_def finite_UNIV_list_def infinite_UNIV_listI) ``` Andreas@48051 ` 243` ```end ``` Andreas@48051 ` 244` Andreas@48051 ` 245` ```instantiation unit :: card_UNIV begin ``` Andreas@48176 ` 246` ```definition "finite_UNIV = Phantom(unit) True" ``` Andreas@48164 ` 247` ```definition "card_UNIV = Phantom(unit) 1" ``` Andreas@48176 ` 248` ```instance by intro_classes (simp_all add: card_UNIV_unit_def finite_UNIV_unit_def) ``` Andreas@48051 ` 249` ```end ``` Andreas@48051 ` 250` Andreas@48051 ` 251` ```instantiation bool :: card_UNIV begin ``` Andreas@48176 ` 252` ```definition "finite_UNIV = Phantom(bool) True" ``` Andreas@48164 ` 253` ```definition "card_UNIV = Phantom(bool) 2" ``` Andreas@48176 ` 254` ```instance by(intro_classes)(simp_all add: card_UNIV_bool_def finite_UNIV_bool_def) ``` Andreas@48051 ` 255` ```end ``` Andreas@48051 ` 256` Andreas@48051 ` 257` ```instantiation char :: card_UNIV begin ``` Andreas@48176 ` 258` ```definition "finite_UNIV = Phantom(char) True" ``` Andreas@48164 ` 259` ```definition "card_UNIV = Phantom(char) 256" ``` Andreas@48176 ` 260` ```instance by intro_classes (simp_all add: card_UNIV_char_def card_UNIV_char finite_UNIV_char_def) ``` Andreas@48176 ` 261` ```end ``` Andreas@48176 ` 262` Andreas@48176 ` 263` ```instantiation prod :: (finite_UNIV, finite_UNIV) finite_UNIV begin ``` Andreas@48176 ` 264` ```definition "finite_UNIV = Phantom('a \ 'b) ``` Andreas@48176 ` 265` ``` (of_phantom (finite_UNIV :: 'a finite_UNIV) \ of_phantom (finite_UNIV :: 'b finite_UNIV))" ``` Andreas@48176 ` 266` ```instance by intro_classes (simp add: finite_UNIV_prod_def finite_UNIV finite_prod) ``` Andreas@48051 ` 267` ```end ``` Andreas@48051 ` 268` Andreas@48051 ` 269` ```instantiation prod :: (card_UNIV, card_UNIV) card_UNIV begin ``` Andreas@48176 ` 270` ```definition "card_UNIV = Phantom('a \ 'b) ``` Andreas@48176 ` 271` ``` (of_phantom (card_UNIV :: 'a card_UNIV) * of_phantom (card_UNIV :: 'b card_UNIV))" ``` Andreas@48060 ` 272` ```instance by intro_classes (simp add: card_UNIV_prod_def card_UNIV) ``` Andreas@48051 ` 273` ```end ``` Andreas@48051 ` 274` Andreas@48176 ` 275` ```instantiation sum :: (finite_UNIV, finite_UNIV) finite_UNIV begin ``` Andreas@48176 ` 276` ```definition "finite_UNIV = Phantom('a + 'b) ``` Andreas@48176 ` 277` ``` (of_phantom (finite_UNIV :: 'a finite_UNIV) \ of_phantom (finite_UNIV :: 'b finite_UNIV))" ``` Andreas@48176 ` 278` ```instance ``` Andreas@48176 ` 279` ``` by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV) ``` Andreas@48176 ` 280` ```end ``` Andreas@48176 ` 281` Andreas@48051 ` 282` ```instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin ``` Andreas@48164 ` 283` ```definition "card_UNIV = Phantom('a + 'b) ``` Andreas@48164 ` 284` ``` (let ca = of_phantom (card_UNIV :: 'a card_UNIV); ``` Andreas@48164 ` 285` ``` cb = of_phantom (card_UNIV :: 'b card_UNIV) ``` Andreas@48164 ` 286` ``` in if ca \ 0 \ cb \ 0 then ca + cb else 0)" ``` Andreas@48060 ` 287` ```instance by intro_classes (auto simp add: card_UNIV_sum_def card_UNIV card_UNIV_sum) ``` Andreas@48051 ` 288` ```end ``` Andreas@48051 ` 289` Andreas@48176 ` 290` ```instantiation "fun" :: (finite_UNIV, card_UNIV) finite_UNIV begin ``` Andreas@48176 ` 291` ```definition "finite_UNIV = Phantom('a \ 'b) ``` Andreas@48176 ` 292` ``` (let cb = of_phantom (card_UNIV :: 'b card_UNIV) ``` Andreas@48176 ` 293` ``` in cb = 1 \ of_phantom (finite_UNIV :: 'a finite_UNIV) \ cb \ 0)" ``` Andreas@48176 ` 294` ```instance ``` Andreas@48176 ` 295` ``` by intro_classes (auto simp add: finite_UNIV_fun_def Let_def card_UNIV finite_UNIV finite_UNIV_fun card_gt_0_iff) ``` Andreas@48176 ` 296` ```end ``` Andreas@48176 ` 297` Andreas@48051 ` 298` ```instantiation "fun" :: (card_UNIV, card_UNIV) card_UNIV begin ``` Andreas@48164 ` 299` ```definition "card_UNIV = Phantom('a \ 'b) ``` Andreas@48164 ` 300` ``` (let ca = of_phantom (card_UNIV :: 'a card_UNIV); ``` Andreas@48164 ` 301` ``` cb = of_phantom (card_UNIV :: 'b card_UNIV) ``` Andreas@48164 ` 302` ``` in if ca \ 0 \ cb \ 0 \ cb = 1 then cb ^ ca else 0)" ``` Andreas@48060 ` 303` ```instance by intro_classes (simp add: card_UNIV_fun_def card_UNIV Let_def card_fun) ``` Andreas@48060 ` 304` ```end ``` Andreas@48051 ` 305` Andreas@48176 ` 306` ```instantiation option :: (finite_UNIV) finite_UNIV begin ``` Andreas@48176 ` 307` ```definition "finite_UNIV = Phantom('a option) (of_phantom (finite_UNIV :: 'a finite_UNIV))" ``` Andreas@48176 ` 308` ```instance by intro_classes (simp add: finite_UNIV_option_def finite_UNIV) ``` Andreas@48176 ` 309` ```end ``` Andreas@48176 ` 310` Andreas@48060 ` 311` ```instantiation option :: (card_UNIV) card_UNIV begin ``` Andreas@48164 ` 312` ```definition "card_UNIV = Phantom('a option) ``` Andreas@48164 ` 313` ``` (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c \ 0 then Suc c else 0)" ``` Andreas@48060 ` 314` ```instance by intro_classes (simp add: card_UNIV_option_def card_UNIV card_UNIV_option) ``` Andreas@48060 ` 315` ```end ``` Andreas@48051 ` 316` Andreas@48060 ` 317` ```instantiation String.literal :: card_UNIV begin ``` Andreas@48176 ` 318` ```definition "finite_UNIV = Phantom(String.literal) False" ``` Andreas@48164 ` 319` ```definition "card_UNIV = Phantom(String.literal) 0" ``` Andreas@48176 ` 320` ```instance ``` Andreas@48176 ` 321` ``` by intro_classes (simp_all add: card_UNIV_literal_def finite_UNIV_literal_def infinite_literal card_literal) ``` Andreas@48176 ` 322` ```end ``` Andreas@48176 ` 323` Andreas@48176 ` 324` ```instantiation set :: (finite_UNIV) finite_UNIV begin ``` Andreas@48176 ` 325` ```definition "finite_UNIV = Phantom('a set) (of_phantom (finite_UNIV :: 'a finite_UNIV))" ``` Andreas@48176 ` 326` ```instance by intro_classes (simp add: finite_UNIV_set_def finite_UNIV Finite_Set.finite_set) ``` Andreas@48060 ` 327` ```end ``` Andreas@48060 ` 328` Andreas@48060 ` 329` ```instantiation set :: (card_UNIV) card_UNIV begin ``` Andreas@48164 ` 330` ```definition "card_UNIV = Phantom('a set) ``` Andreas@48164 ` 331` ``` (let c = of_phantom (card_UNIV :: 'a card_UNIV) in if c = 0 then 0 else 2 ^ c)" ``` Andreas@48060 ` 332` ```instance by intro_classes (simp add: card_UNIV_set_def card_UNIV_set card_UNIV) ``` Andreas@48051 ` 333` ```end ``` Andreas@48051 ` 334` wenzelm@53015 ` 335` ```lemma UNIV_finite_1: "UNIV = set [finite_1.a\<^sub>1]" ``` Andreas@48060 ` 336` ```by(auto intro: finite_1.exhaust) ``` Andreas@48060 ` 337` wenzelm@53015 ` 338` ```lemma UNIV_finite_2: "UNIV = set [finite_2.a\<^sub>1, finite_2.a\<^sub>2]" ``` Andreas@48060 ` 339` ```by(auto intro: finite_2.exhaust) ``` Andreas@48051 ` 340` wenzelm@53015 ` 341` ```lemma UNIV_finite_3: "UNIV = set [finite_3.a\<^sub>1, finite_3.a\<^sub>2, finite_3.a\<^sub>3]" ``` Andreas@48060 ` 342` ```by(auto intro: finite_3.exhaust) ``` Andreas@48051 ` 343` wenzelm@53015 ` 344` ```lemma UNIV_finite_4: "UNIV = set [finite_4.a\<^sub>1, finite_4.a\<^sub>2, finite_4.a\<^sub>3, finite_4.a\<^sub>4]" ``` Andreas@48060 ` 345` ```by(auto intro: finite_4.exhaust) ``` Andreas@48060 ` 346` Andreas@48060 ` 347` ```lemma UNIV_finite_5: ``` wenzelm@53015 ` 348` ``` "UNIV = set [finite_5.a\<^sub>1, finite_5.a\<^sub>2, finite_5.a\<^sub>3, finite_5.a\<^sub>4, finite_5.a\<^sub>5]" ``` Andreas@48060 ` 349` ```by(auto intro: finite_5.exhaust) ``` Andreas@48051 ` 350` Andreas@48060 ` 351` ```instantiation Enum.finite_1 :: card_UNIV begin ``` Andreas@48176 ` 352` ```definition "finite_UNIV = Phantom(Enum.finite_1) True" ``` Andreas@48164 ` 353` ```definition "card_UNIV = Phantom(Enum.finite_1) 1" ``` Andreas@48176 ` 354` ```instance ``` Andreas@48176 ` 355` ``` by intro_classes (simp_all add: UNIV_finite_1 card_UNIV_finite_1_def finite_UNIV_finite_1_def) ``` Andreas@48060 ` 356` ```end ``` Andreas@48060 ` 357` Andreas@48060 ` 358` ```instantiation Enum.finite_2 :: card_UNIV begin ``` Andreas@48176 ` 359` ```definition "finite_UNIV = Phantom(Enum.finite_2) True" ``` Andreas@48164 ` 360` ```definition "card_UNIV = Phantom(Enum.finite_2) 2" ``` Andreas@48176 ` 361` ```instance ``` Andreas@48176 ` 362` ``` by intro_classes (simp_all add: UNIV_finite_2 card_UNIV_finite_2_def finite_UNIV_finite_2_def) ``` Andreas@48060 ` 363` ```end ``` Andreas@48051 ` 364` Andreas@48060 ` 365` ```instantiation Enum.finite_3 :: card_UNIV begin ``` Andreas@48176 ` 366` ```definition "finite_UNIV = Phantom(Enum.finite_3) True" ``` Andreas@48164 ` 367` ```definition "card_UNIV = Phantom(Enum.finite_3) 3" ``` Andreas@48176 ` 368` ```instance ``` Andreas@48176 ` 369` ``` by intro_classes (simp_all add: UNIV_finite_3 card_UNIV_finite_3_def finite_UNIV_finite_3_def) ``` Andreas@48060 ` 370` ```end ``` Andreas@48060 ` 371` Andreas@48060 ` 372` ```instantiation Enum.finite_4 :: card_UNIV begin ``` Andreas@48176 ` 373` ```definition "finite_UNIV = Phantom(Enum.finite_4) True" ``` Andreas@48164 ` 374` ```definition "card_UNIV = Phantom(Enum.finite_4) 4" ``` Andreas@48176 ` 375` ```instance ``` Andreas@48176 ` 376` ``` by intro_classes (simp_all add: UNIV_finite_4 card_UNIV_finite_4_def finite_UNIV_finite_4_def) ``` Andreas@48060 ` 377` ```end ``` Andreas@48060 ` 378` Andreas@48060 ` 379` ```instantiation Enum.finite_5 :: card_UNIV begin ``` Andreas@48176 ` 380` ```definition "finite_UNIV = Phantom(Enum.finite_5) True" ``` Andreas@48164 ` 381` ```definition "card_UNIV = Phantom(Enum.finite_5) 5" ``` Andreas@48176 ` 382` ```instance ``` Andreas@48176 ` 383` ``` by intro_classes (simp_all add: UNIV_finite_5 card_UNIV_finite_5_def finite_UNIV_finite_5_def) ``` Andreas@48051 ` 384` ```end ``` Andreas@48051 ` 385` wenzelm@60500 ` 386` ```subsection \Code setup for sets\ ``` Andreas@48051 ` 387` wenzelm@60500 ` 388` ```text \ ``` Andreas@51139 ` 389` ``` Implement @{term "CARD('a)"} via @{term card_UNIV} and provide ``` nipkow@67399 ` 390` ``` implementations for @{term "finite"}, @{term "card"}, @{term "(\)"}, ``` nipkow@67399 ` 391` ``` and @{term "(=)"}if the calling context already provides @{class finite_UNIV} ``` Andreas@51139 ` 392` ``` and @{class card_UNIV} instances. If we implemented the latter ``` Andreas@51139 ` 393` ``` always via @{term card_UNIV}, we would require instances of essentially all ``` Andreas@51139 ` 394` ``` element types, i.e., a lot of instantiation proofs and -- at run time -- ``` Andreas@51139 ` 395` ``` possibly slow dictionary constructions. ``` wenzelm@60500 ` 396` ```\ ``` Andreas@51116 ` 397` wenzelm@61115 ` 398` ```context ``` wenzelm@61115 ` 399` ```begin ``` wenzelm@61115 ` 400` wenzelm@61115 ` 401` ```qualified definition card_UNIV' :: "'a card_UNIV" ``` Andreas@51139 ` 402` ```where [code del]: "card_UNIV' = Phantom('a) CARD('a)" ``` Andreas@51139 ` 403` Andreas@51139 ` 404` ```lemma CARD_code [code_unfold]: ``` Andreas@51139 ` 405` ``` "CARD('a) = of_phantom (card_UNIV' :: 'a card_UNIV)" ``` Andreas@51139 ` 406` ```by(simp add: card_UNIV'_def) ``` Andreas@51139 ` 407` Andreas@51139 ` 408` ```lemma card_UNIV'_code [code]: ``` Andreas@51139 ` 409` ``` "card_UNIV' = card_UNIV" ``` Andreas@51139 ` 410` ```by(simp add: card_UNIV card_UNIV'_def) ``` Andreas@51139 ` 411` wenzelm@61115 ` 412` ```end ``` Andreas@51139 ` 413` Andreas@48051 ` 414` ```lemma card_Compl: ``` Andreas@48051 ` 415` ``` "finite A \ card (- A) = card (UNIV :: 'a set) - card (A :: 'a set)" ``` Andreas@48051 ` 416` ```by (metis Compl_eq_Diff_UNIV card_Diff_subset top_greatest) ``` Andreas@48051 ` 417` Andreas@51139 ` 418` ```context fixes xs :: "'a :: finite_UNIV list" ``` Andreas@51139 ` 419` ```begin ``` Andreas@48062 ` 420` wenzelm@61115 ` 421` ```qualified definition finite' :: "'a set \ bool" ``` Andreas@51139 ` 422` ```where [simp, code del, code_abbrev]: "finite' = finite" ``` Andreas@51139 ` 423` Andreas@51139 ` 424` ```lemma finite'_code [code]: ``` Andreas@51139 ` 425` ``` "finite' (set xs) \ True" ``` Andreas@51139 ` 426` ``` "finite' (List.coset xs) \ of_phantom (finite_UNIV :: 'a finite_UNIV)" ``` Andreas@48176 ` 427` ```by(simp_all add: card_gt_0_iff finite_UNIV) ``` Andreas@48062 ` 428` Andreas@51139 ` 429` ```end ``` Andreas@51139 ` 430` Andreas@51139 ` 431` ```context fixes xs :: "'a :: card_UNIV list" ``` Andreas@51139 ` 432` ```begin ``` Andreas@51139 ` 433` wenzelm@61115 ` 434` ```qualified definition card' :: "'a set \ nat" ``` Andreas@51139 ` 435` ```where [simp, code del, code_abbrev]: "card' = card" ``` Andreas@51139 ` 436` ``` ``` Andreas@51139 ` 437` ```lemma card'_code [code]: ``` Andreas@51139 ` 438` ``` "card' (set xs) = length (remdups xs)" ``` Andreas@51139 ` 439` ``` "card' (List.coset xs) = of_phantom (card_UNIV :: 'a card_UNIV) - length (remdups xs)" ``` Andreas@51139 ` 440` ```by(simp_all add: List.card_set card_Compl card_UNIV) ``` Andreas@51139 ` 441` Andreas@51139 ` 442` wenzelm@61115 ` 443` ```qualified definition subset' :: "'a set \ 'a set \ bool" ``` nipkow@67399 ` 444` ```where [simp, code del, code_abbrev]: "subset' = (\)" ``` Andreas@51139 ` 445` Andreas@51139 ` 446` ```lemma subset'_code [code]: ``` Andreas@51139 ` 447` ``` "subset' A (List.coset ys) \ (\y \ set ys. y \ A)" ``` Andreas@51139 ` 448` ``` "subset' (set ys) B \ (\y \ set ys. y \ B)" ``` Andreas@51139 ` 449` ``` "subset' (List.coset xs) (set ys) \ (let n = CARD('a) in n > 0 \ card(set (xs @ ys)) = n)" ``` Andreas@48062 ` 450` ```by(auto simp add: Let_def card_gt_0_iff dest: card_eq_UNIV_imp_eq_UNIV intro: arg_cong[where f=card]) ``` Andreas@48062 ` 451` ``` (metis finite_compl finite_set rev_finite_subset) ``` Andreas@48062 ` 452` wenzelm@61115 ` 453` ```qualified definition eq_set :: "'a set \ 'a set \ bool" ``` nipkow@67399 ` 454` ```where [simp, code del, code_abbrev]: "eq_set = (=)" ``` Andreas@51139 ` 455` Andreas@51139 ` 456` ```lemma eq_set_code [code]: ``` Andreas@51139 ` 457` ``` fixes ys ``` Andreas@48051 ` 458` ``` defines "rhs \ ``` Andreas@48059 ` 459` ``` let n = CARD('a) ``` Andreas@48051 ` 460` ``` in if n = 0 then False else ``` Andreas@48051 ` 461` ``` let xs' = remdups xs; ys' = remdups ys ``` Andreas@48051 ` 462` ``` in length xs' + length ys' = n \ (\x \ set xs'. x \ set ys') \ (\y \ set ys'. y \ set xs')" ``` wenzelm@60583 ` 463` ``` shows "eq_set (List.coset xs) (set ys) \ rhs" ``` wenzelm@60583 ` 464` ``` and "eq_set (set ys) (List.coset xs) \ rhs" ``` wenzelm@60583 ` 465` ``` and "eq_set (set xs) (set ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" ``` wenzelm@60583 ` 466` ``` and "eq_set (List.coset xs) (List.coset ys) \ (\x \ set xs. x \ set ys) \ (\y \ set ys. y \ set xs)" ``` wenzelm@61166 ` 467` ```proof goal_cases ``` wenzelm@60583 ` 468` ``` { ``` wenzelm@60583 ` 469` ``` case 1 ``` wenzelm@60583 ` 470` ``` show ?case (is "?lhs \ ?rhs") ``` wenzelm@60583 ` 471` ``` proof ``` wenzelm@60583 ` 472` ``` show ?rhs if ?lhs ``` wenzelm@60583 ` 473` ``` using that ``` wenzelm@60583 ` 474` ``` by (auto simp add: rhs_def Let_def List.card_set[symmetric] ``` wenzelm@60583 ` 475` ``` card_Un_Int[where A="set xs" and B="- set xs"] card_UNIV ``` wenzelm@60583 ` 476` ``` Compl_partition card_gt_0_iff dest: sym)(metis finite_compl finite_set) ``` wenzelm@60583 ` 477` ``` show ?lhs if ?rhs ``` wenzelm@60583 ` 478` ``` proof - ``` wenzelm@60583 ` 479` ``` have "\ \y\set xs. y \ set ys; \x\set ys. x \ set xs \ \ set xs \ set ys = {}" by blast ``` wenzelm@60583 ` 480` ``` with that show ?thesis ``` wenzelm@60583 ` 481` ``` by (auto simp add: rhs_def Let_def List.card_set[symmetric] ``` wenzelm@60583 ` 482` ``` card_UNIV card_gt_0_iff card_Un_Int[where A="set xs" and B="set ys"] ``` nipkow@62390 ` 483` ``` dest: card_eq_UNIV_imp_eq_UNIV split: if_split_asm) ``` wenzelm@60583 ` 484` ``` qed ``` wenzelm@60583 ` 485` ``` qed ``` wenzelm@60583 ` 486` ``` } ``` wenzelm@60583 ` 487` ``` moreover ``` wenzelm@60583 ` 488` ``` case 2 ``` wenzelm@60583 ` 489` ``` ultimately show ?case unfolding eq_set_def by blast ``` wenzelm@60583 ` 490` ```next ``` wenzelm@60583 ` 491` ``` case 3 ``` wenzelm@60583 ` 492` ``` show ?case unfolding eq_set_def List.coset_def by blast ``` wenzelm@60583 ` 493` ```next ``` wenzelm@60583 ` 494` ``` case 4 ``` wenzelm@60583 ` 495` ``` show ?case unfolding eq_set_def List.coset_def by blast ``` Andreas@48051 ` 496` ```qed ``` Andreas@48051 ` 497` Andreas@51139 ` 498` ```end ``` Andreas@51139 ` 499` wenzelm@60500 ` 500` ```text \ ``` Andreas@51139 ` 501` ``` Provide more informative exceptions than Match for non-rewritten cases. ``` Andreas@51139 ` 502` ``` If generated code raises one these exceptions, then a code equation calls ``` Andreas@51139 ` 503` ``` the mentioned operator for an element type that is not an instance of ``` Andreas@51139 ` 504` ``` @{class card_UNIV} and is therefore not implemented via @{term card_UNIV}. ``` Andreas@51139 ` 505` ``` Constrain the element type with sort @{class card_UNIV} to change this. ``` wenzelm@60500 ` 506` ```\ ``` Andreas@51139 ` 507` Andreas@51139 ` 508` ```lemma card_coset_error [code]: ``` Andreas@53745 ` 509` ``` "card (List.coset xs) = ``` Andreas@53745 ` 510` ``` Code.abort (STR ''card (List.coset _) requires type class instance card_UNIV'') ``` Andreas@53745 ` 511` ``` (\_. card (List.coset xs))" ``` Andreas@51139 ` 512` ```by(simp) ``` Andreas@51139 ` 513` Andreas@51139 ` 514` ```lemma coset_subseteq_set_code [code]: ``` Andreas@51139 ` 515` ``` "List.coset xs \ set ys \ ``` Andreas@53745 ` 516` ``` (if xs = [] \ ys = [] then False ``` Andreas@53745 ` 517` ``` else Code.abort ``` Andreas@53745 ` 518` ``` (STR ''subset_eq (List.coset _) (List.set _) requires type class instance card_UNIV'') ``` Andreas@53745 ` 519` ``` (\_. List.coset xs \ set ys))" ``` Andreas@51139 ` 520` ```by simp ``` Andreas@51139 ` 521` wenzelm@67443 ` 522` ```notepad begin \ \test code setup\ ``` Andreas@51139 ` 523` ```have "List.coset [True] = set [False] \ ``` Andreas@51139 ` 524` ``` List.coset [] \ List.set [True, False] \ ``` Andreas@51139 ` 525` ``` finite (List.coset [True])" ``` Andreas@48062 ` 526` ``` by eval ``` Andreas@48062 ` 527` ```end ``` Andreas@48062 ` 528` Andreas@48051 ` 529` ```end ```