src/HOL/Library/Finite_Map.thy
 author wenzelm Wed Mar 07 19:02:22 2018 +0100 (16 months ago) changeset 67780 7655e6369c9f parent 67485 89f5d876a656 child 68249 949d93804740 permissions -rw-r--r--
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
 lars@63885 ` 1` ```(* Title: HOL/Library/Finite_Map.thy ``` lars@63885 ` 2` ``` Author: Lars Hupel, TU München ``` lars@63885 ` 3` ```*) ``` lars@63885 ` 4` lars@63885 ` 5` ```section \Type of finite maps defined as a subtype of maps\ ``` lars@63885 ` 6` lars@63885 ` 7` ```theory Finite_Map ``` lars@63885 ` 8` ``` imports FSet AList ``` wenzelm@67780 ` 9` ``` abbrevs "(=" = "\\<^sub>f" ``` lars@63885 ` 10` ```begin ``` lars@63885 ` 11` lars@63885 ` 12` ```subsection \Auxiliary constants and lemmas over @{type map}\ ``` lars@63885 ` 13` lars@63885 ` 14` ```context includes lifting_syntax begin ``` lars@63885 ` 15` lars@63885 ` 16` ```abbreviation rel_map :: "('b \ 'c \ bool) \ ('a \ 'b) \ ('a \ 'c) \ bool" where ``` nipkow@67399 ` 17` ```"rel_map f \ (=) ===> rel_option f" ``` lars@63885 ` 18` lars@63885 ` 19` ```lemma map_empty_transfer[transfer_rule]: "rel_map A Map.empty Map.empty" ``` lars@63885 ` 20` ```by transfer_prover ``` lars@63885 ` 21` lars@63885 ` 22` ```lemma ran_transfer[transfer_rule]: "(rel_map A ===> rel_set A) ran ran" ``` lars@63885 ` 23` ```proof ``` lars@63885 ` 24` ``` fix m n ``` lars@63885 ` 25` ``` assume "rel_map A m n" ``` lars@63885 ` 26` ``` show "rel_set A (ran m) (ran n)" ``` lars@63885 ` 27` ``` proof (rule rel_setI) ``` lars@63885 ` 28` ``` fix x ``` lars@63885 ` 29` ``` assume "x \ ran m" ``` lars@63885 ` 30` ``` then obtain a where "m a = Some x" ``` lars@63885 ` 31` ``` unfolding ran_def by auto ``` lars@63885 ` 32` lars@63885 ` 33` ``` have "rel_option A (m a) (n a)" ``` lars@63885 ` 34` ``` using \rel_map A m n\ ``` lars@63885 ` 35` ``` by (auto dest: rel_funD) ``` lars@63885 ` 36` ``` then obtain y where "n a = Some y" "A x y" ``` lars@63885 ` 37` ``` unfolding \m a = _\ ``` lars@63885 ` 38` ``` by cases auto ``` lars@64180 ` 39` ``` then show "\y \ ran n. A x y" ``` lars@63885 ` 40` ``` unfolding ran_def by blast ``` lars@63885 ` 41` ``` next ``` lars@63885 ` 42` ``` fix y ``` lars@63885 ` 43` ``` assume "y \ ran n" ``` lars@63885 ` 44` ``` then obtain a where "n a = Some y" ``` lars@63885 ` 45` ``` unfolding ran_def by auto ``` lars@63885 ` 46` lars@63885 ` 47` ``` have "rel_option A (m a) (n a)" ``` lars@63885 ` 48` ``` using \rel_map A m n\ ``` lars@63885 ` 49` ``` by (auto dest: rel_funD) ``` lars@63885 ` 50` ``` then obtain x where "m a = Some x" "A x y" ``` lars@63885 ` 51` ``` unfolding \n a = _\ ``` lars@63885 ` 52` ``` by cases auto ``` lars@64180 ` 53` ``` then show "\x \ ran m. A x y" ``` lars@63885 ` 54` ``` unfolding ran_def by blast ``` lars@63885 ` 55` ``` qed ``` lars@63885 ` 56` ```qed ``` lars@63885 ` 57` lars@63885 ` 58` ```lemma ran_alt_def: "ran m = (the \ m) ` dom m" ``` lars@63885 ` 59` ```unfolding ran_def dom_def by force ``` lars@63885 ` 60` nipkow@67399 ` 61` ```lemma dom_transfer[transfer_rule]: "(rel_map A ===> (=)) dom dom" ``` lars@63885 ` 62` ```proof ``` lars@63885 ` 63` ``` fix m n ``` lars@63885 ` 64` ``` assume "rel_map A m n" ``` lars@63885 ` 65` ``` have "m a \ None \ n a \ None" for a ``` lars@63885 ` 66` ``` proof - ``` lars@63885 ` 67` ``` from \rel_map A m n\ have "rel_option A (m a) (n a)" ``` lars@63885 ` 68` ``` unfolding rel_fun_def by auto ``` lars@64180 ` 69` ``` then show ?thesis ``` lars@63885 ` 70` ``` by cases auto ``` lars@63885 ` 71` ``` qed ``` lars@64180 ` 72` ``` then show "dom m = dom n" ``` lars@63885 ` 73` ``` by auto ``` lars@63885 ` 74` ```qed ``` lars@63885 ` 75` lars@63885 ` 76` ```definition map_upd :: "'a \ 'b \ ('a \ 'b) \ ('a \ 'b)" where ``` lars@63885 ` 77` ```"map_upd k v m = m(k \ v)" ``` lars@63885 ` 78` lars@63885 ` 79` ```lemma map_upd_transfer[transfer_rule]: ``` nipkow@67399 ` 80` ``` "((=) ===> A ===> rel_map A ===> rel_map A) map_upd map_upd" ``` lars@63885 ` 81` ```unfolding map_upd_def[abs_def] ``` lars@63885 ` 82` ```by transfer_prover ``` lars@63885 ` 83` lars@63885 ` 84` ```definition map_filter :: "('a \ bool) \ ('a \ 'b) \ ('a \ 'b)" where ``` lars@63885 ` 85` ```"map_filter P m = (\x. if P x then m x else None)" ``` lars@63885 ` 86` lars@63885 ` 87` ```lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \ m. P k]" ``` lars@63885 ` 88` ```proof ``` lars@63885 ` 89` ``` fix x ``` lars@63885 ` 90` ``` show "map_filter P (map_of m) x = map_of [(k, _) \ m. P k] x" ``` lars@63885 ` 91` ``` by (induct m) (auto simp: map_filter_def) ``` lars@63885 ` 92` ```qed ``` lars@63885 ` 93` lars@63885 ` 94` ```lemma map_filter_transfer[transfer_rule]: ``` nipkow@67399 ` 95` ``` "((=) ===> rel_map A ===> rel_map A) map_filter map_filter" ``` lars@63885 ` 96` ```unfolding map_filter_def[abs_def] ``` lars@63885 ` 97` ```by transfer_prover ``` lars@63885 ` 98` lars@63885 ` 99` ```lemma map_filter_finite[intro]: ``` lars@63885 ` 100` ``` assumes "finite (dom m)" ``` lars@63885 ` 101` ``` shows "finite (dom (map_filter P m))" ``` lars@63885 ` 102` ```proof - ``` lars@63885 ` 103` ``` have "dom (map_filter P m) = Set.filter P (dom m)" ``` lars@63885 ` 104` ``` unfolding map_filter_def Set.filter_def dom_def ``` lars@63885 ` 105` ``` by auto ``` lars@64180 ` 106` ``` then show ?thesis ``` lars@63885 ` 107` ``` using assms ``` lars@63885 ` 108` ``` by (simp add: Set.filter_def) ``` lars@63885 ` 109` ```qed ``` lars@63885 ` 110` lars@63885 ` 111` ```definition map_drop :: "'a \ ('a \ 'b) \ ('a \ 'b)" where ``` lars@63885 ` 112` ```"map_drop a = map_filter (\a'. a' \ a)" ``` lars@63885 ` 113` lars@63885 ` 114` ```lemma map_drop_transfer[transfer_rule]: ``` nipkow@67399 ` 115` ``` "((=) ===> rel_map A ===> rel_map A) map_drop map_drop" ``` lars@63885 ` 116` ```unfolding map_drop_def[abs_def] ``` lars@63885 ` 117` ```by transfer_prover ``` lars@63885 ` 118` lars@63885 ` 119` ```definition map_drop_set :: "'a set \ ('a \ 'b) \ ('a \ 'b)" where ``` lars@63885 ` 120` ```"map_drop_set A = map_filter (\a. a \ A)" ``` lars@63885 ` 121` lars@63885 ` 122` ```lemma map_drop_set_transfer[transfer_rule]: ``` nipkow@67399 ` 123` ``` "((=) ===> rel_map A ===> rel_map A) map_drop_set map_drop_set" ``` lars@63885 ` 124` ```unfolding map_drop_set_def[abs_def] ``` lars@63885 ` 125` ```by transfer_prover ``` lars@63885 ` 126` lars@63885 ` 127` ```definition map_restrict_set :: "'a set \ ('a \ 'b) \ ('a \ 'b)" where ``` lars@63885 ` 128` ```"map_restrict_set A = map_filter (\a. a \ A)" ``` lars@63885 ` 129` lars@63885 ` 130` ```lemma map_restrict_set_transfer[transfer_rule]: ``` nipkow@67399 ` 131` ``` "((=) ===> rel_map A ===> rel_map A) map_restrict_set map_restrict_set" ``` lars@63885 ` 132` ```unfolding map_restrict_set_def[abs_def] ``` lars@63885 ` 133` ```by transfer_prover ``` lars@63885 ` 134` lars@63885 ` 135` ```lemma map_add_transfer[transfer_rule]: ``` nipkow@67399 ` 136` ``` "(rel_map A ===> rel_map A ===> rel_map A) (++) (++)" ``` lars@63885 ` 137` ```unfolding map_add_def[abs_def] ``` lars@63885 ` 138` ```by transfer_prover ``` lars@63885 ` 139` lars@63885 ` 140` ```definition map_pred :: "('a \ 'b \ bool) \ ('a \ 'b) \ bool" where ``` lars@63885 ` 141` ```"map_pred P m \ (\x. case m x of None \ True | Some y \ P x y)" ``` lars@63885 ` 142` lars@63885 ` 143` ```lemma map_pred_transfer[transfer_rule]: ``` nipkow@67399 ` 144` ``` "(((=) ===> A ===> (=)) ===> rel_map A ===> (=)) map_pred map_pred" ``` lars@63885 ` 145` ```unfolding map_pred_def[abs_def] ``` lars@63885 ` 146` ```by transfer_prover ``` lars@63885 ` 147` lars@63885 ` 148` ```definition rel_map_on_set :: "'a set \ ('b \ 'c \ bool) \ ('a \ 'b) \ ('a \ 'c) \ bool" where ``` lars@63885 ` 149` ```"rel_map_on_set S P = eq_onp (\x. x \ S) ===> rel_option P" ``` lars@66267 ` 150` lars@63885 ` 151` ```lemma map_of_transfer[transfer_rule]: ``` lars@63885 ` 152` ``` includes lifting_syntax ``` nipkow@67399 ` 153` ``` shows "(list_all2 (rel_prod (=) A) ===> rel_map A) map_of map_of" ``` lars@63885 ` 154` ```unfolding map_of_def by transfer_prover ``` lars@66267 ` 155` lars@66282 ` 156` ```definition set_of_map :: "('a \ 'b) \ ('a \ 'b) set" where ``` lars@66282 ` 157` ```"set_of_map m = {(k, v)|k v. m k = Some v}" ``` lars@66282 ` 158` lars@66282 ` 159` ```lemma set_of_map_alt_def: "set_of_map m = (\k. (k, the (m k))) ` dom m" ``` lars@66282 ` 160` ```unfolding set_of_map_def dom_def ``` lars@66282 ` 161` ```by auto ``` lars@66282 ` 162` lars@66282 ` 163` ```lemma set_of_map_finite: "finite (dom m) \ finite (set_of_map m)" ``` lars@66282 ` 164` ```unfolding set_of_map_alt_def ``` lars@66282 ` 165` ```by auto ``` lars@66282 ` 166` lars@66282 ` 167` ```lemma set_of_map_inj: "inj set_of_map" ``` lars@66282 ` 168` ```proof ``` lars@66282 ` 169` ``` fix x y ``` lars@66282 ` 170` ``` assume "set_of_map x = set_of_map y" ``` lars@66282 ` 171` ``` hence "(x a = Some b) = (y a = Some b)" for a b ``` lars@66282 ` 172` ``` unfolding set_of_map_def by auto ``` lars@66282 ` 173` ``` hence "x k = y k" for k ``` lars@66282 ` 174` ``` by (metis not_None_eq) ``` lars@66282 ` 175` ``` thus "x = y" .. ``` lars@66282 ` 176` ```qed ``` lars@66282 ` 177` lars@63885 ` 178` ```end ``` lars@63885 ` 179` lars@63885 ` 180` lars@63885 ` 181` ```subsection \Abstract characterisation\ ``` lars@63885 ` 182` lars@63885 ` 183` ```typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a \ 'b) set" ``` lars@63885 ` 184` ``` morphisms fmlookup Abs_fmap ``` lars@63885 ` 185` ```proof ``` lars@63885 ` 186` ``` show "Map.empty \ {m. finite (dom m)}" ``` lars@63885 ` 187` ``` by auto ``` lars@63885 ` 188` ```qed ``` lars@63885 ` 189` lars@63885 ` 190` ```setup_lifting type_definition_fmap ``` lars@63885 ` 191` lars@63885 ` 192` ```lemma fmlookup_finite[intro, simp]: "finite (dom (fmlookup m))" ``` lars@63885 ` 193` ```using fmap.fmlookup by auto ``` lars@63885 ` 194` lars@63885 ` 195` ```lemma fmap_ext: ``` lars@63885 ` 196` ``` assumes "\x. fmlookup m x = fmlookup n x" ``` lars@63885 ` 197` ``` shows "m = n" ``` lars@63885 ` 198` ```using assms ``` lars@63885 ` 199` ```by transfer' auto ``` lars@63885 ` 200` lars@63885 ` 201` lars@63885 ` 202` ```subsection \Operations\ ``` lars@63885 ` 203` lars@63885 ` 204` ```context ``` lars@63885 ` 205` ``` includes fset.lifting ``` lars@63885 ` 206` ```begin ``` lars@63885 ` 207` lars@63885 ` 208` ```lift_definition fmran :: "('a, 'b) fmap \ 'b fset" ``` lars@63885 ` 209` ``` is ran ``` lars@63885 ` 210` ``` parametric ran_transfer ``` lars@63885 ` 211` ```unfolding ran_alt_def by auto ``` lars@63885 ` 212` lars@66268 ` 213` ```lemma fmlookup_ran_iff: "y |\| fmran m \ (\x. fmlookup m x = Some y)" ``` lars@66268 ` 214` ```by transfer' (auto simp: ran_def) ``` lars@66268 ` 215` lars@66268 ` 216` ```lemma fmranI: "fmlookup m x = Some y \ y |\| fmran m" by (auto simp: fmlookup_ran_iff) ``` lars@66268 ` 217` lars@66268 ` 218` ```lemma fmranE[elim]: ``` lars@66268 ` 219` ``` assumes "y |\| fmran m" ``` lars@66268 ` 220` ``` obtains x where "fmlookup m x = Some y" ``` lars@66268 ` 221` ```using assms by (auto simp: fmlookup_ran_iff) ``` lars@63885 ` 222` lars@63885 ` 223` ```lift_definition fmdom :: "('a, 'b) fmap \ 'a fset" ``` lars@63885 ` 224` ``` is dom ``` lars@63885 ` 225` ``` parametric dom_transfer ``` lars@63885 ` 226` ```. ``` lars@63885 ` 227` lars@66268 ` 228` ```lemma fmlookup_dom_iff: "x |\| fmdom m \ (\a. fmlookup m x = Some a)" ``` lars@66268 ` 229` ```by transfer' auto ``` lars@66268 ` 230` lars@66268 ` 231` ```lemma fmdom_notI: "fmlookup m x = None \ x |\| fmdom m" by (simp add: fmlookup_dom_iff) ``` lars@66268 ` 232` ```lemma fmdomI: "fmlookup m x = Some y \ x |\| fmdom m" by (simp add: fmlookup_dom_iff) ``` lars@66268 ` 233` ```lemma fmdom_notD[dest]: "x |\| fmdom m \ fmlookup m x = None" by (simp add: fmlookup_dom_iff) ``` lars@66268 ` 234` lars@66268 ` 235` ```lemma fmdomE[elim]: ``` lars@66268 ` 236` ``` assumes "x |\| fmdom m" ``` lars@66268 ` 237` ``` obtains y where "fmlookup m x = Some y" ``` lars@66268 ` 238` ```using assms by (auto simp: fmlookup_dom_iff) ``` lars@63885 ` 239` lars@63885 ` 240` ```lift_definition fmdom' :: "('a, 'b) fmap \ 'a set" ``` lars@63885 ` 241` ``` is dom ``` lars@63885 ` 242` ``` parametric dom_transfer ``` lars@63885 ` 243` ```. ``` lars@63885 ` 244` lars@66268 ` 245` ```lemma fmlookup_dom'_iff: "x \ fmdom' m \ (\a. fmlookup m x = Some a)" ``` lars@66268 ` 246` ```by transfer' auto ``` lars@66268 ` 247` lars@66268 ` 248` ```lemma fmdom'_notI: "fmlookup m x = None \ x \ fmdom' m" by (simp add: fmlookup_dom'_iff) ``` lars@66268 ` 249` ```lemma fmdom'I: "fmlookup m x = Some y \ x \ fmdom' m" by (simp add: fmlookup_dom'_iff) ``` lars@66268 ` 250` ```lemma fmdom'_notD[dest]: "x \ fmdom' m \ fmlookup m x = None" by (simp add: fmlookup_dom'_iff) ``` lars@63885 ` 251` lars@66268 ` 252` ```lemma fmdom'E[elim]: ``` lars@66268 ` 253` ``` assumes "x \ fmdom' m" ``` lars@66268 ` 254` ``` obtains x y where "fmlookup m x = Some y" ``` lars@66268 ` 255` ```using assms by (auto simp: fmlookup_dom'_iff) ``` lars@63885 ` 256` lars@66268 ` 257` ```lemma fmdom'_alt_def: "fmdom' m = fset (fmdom m)" ``` lars@66268 ` 258` ```by transfer' force ``` lars@63885 ` 259` lars@63885 ` 260` ```lift_definition fmempty :: "('a, 'b) fmap" ``` lars@63885 ` 261` ``` is Map.empty ``` lars@63885 ` 262` ``` parametric map_empty_transfer ``` lars@63885 ` 263` ```by simp ``` lars@63885 ` 264` lars@63885 ` 265` ```lemma fmempty_lookup[simp]: "fmlookup fmempty x = None" ``` lars@63885 ` 266` ```by transfer' simp ``` lars@63885 ` 267` lars@63885 ` 268` ```lemma fmdom_empty[simp]: "fmdom fmempty = {||}" by transfer' simp ``` lars@63885 ` 269` ```lemma fmdom'_empty[simp]: "fmdom' fmempty = {}" by transfer' simp ``` lars@66269 ` 270` ```lemma fmran_empty[simp]: "fmran fmempty = fempty" by transfer' (auto simp: ran_def map_filter_def) ``` lars@63885 ` 271` lars@63885 ` 272` ```lift_definition fmupd :: "'a \ 'b \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 273` ``` is map_upd ``` lars@63885 ` 274` ``` parametric map_upd_transfer ``` lars@63885 ` 275` ```unfolding map_upd_def[abs_def] ``` lars@63885 ` 276` ```by simp ``` lars@63885 ` 277` lars@63885 ` 278` ```lemma fmupd_lookup[simp]: "fmlookup (fmupd a b m) a' = (if a = a' then Some b else fmlookup m a')" ``` lars@63885 ` 279` ```by transfer' (auto simp: map_upd_def) ``` lars@63885 ` 280` lars@63885 ` 281` ```lemma fmdom_fmupd[simp]: "fmdom (fmupd a b m) = finsert a (fmdom m)" by transfer (simp add: map_upd_def) ``` lars@63885 ` 282` ```lemma fmdom'_fmupd[simp]: "fmdom' (fmupd a b m) = insert a (fmdom' m)" by transfer (simp add: map_upd_def) ``` lars@63885 ` 283` lars@63885 ` 284` ```lift_definition fmfilter :: "('a \ bool) \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 285` ``` is map_filter ``` lars@63885 ` 286` ``` parametric map_filter_transfer ``` lars@63885 ` 287` ```by auto ``` lars@63885 ` 288` lars@63885 ` 289` ```lemma fmdom_filter[simp]: "fmdom (fmfilter P m) = ffilter P (fmdom m)" ``` lars@63885 ` 290` ```by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) ``` lars@63885 ` 291` lars@63885 ` 292` ```lemma fmdom'_filter[simp]: "fmdom' (fmfilter P m) = Set.filter P (fmdom' m)" ``` lars@63885 ` 293` ```by transfer' (auto simp: map_filter_def Set.filter_def split: if_splits) ``` lars@63885 ` 294` lars@63885 ` 295` ```lemma fmlookup_filter[simp]: "fmlookup (fmfilter P m) x = (if P x then fmlookup m x else None)" ``` lars@63885 ` 296` ```by transfer' (auto simp: map_filter_def) ``` lars@63885 ` 297` lars@63885 ` 298` ```lemma fmfilter_empty[simp]: "fmfilter P fmempty = fmempty" ``` lars@63885 ` 299` ```by transfer' (auto simp: map_filter_def) ``` lars@63885 ` 300` lars@63900 ` 301` ```lemma fmfilter_true[simp]: ``` lars@66268 ` 302` ``` assumes "\x y. fmlookup m x = Some y \ P x" ``` lars@63900 ` 303` ``` shows "fmfilter P m = m" ``` lars@63900 ` 304` ```proof (rule fmap_ext) ``` lars@63900 ` 305` ``` fix x ``` lars@63900 ` 306` ``` have "fmlookup m x = None" if "\ P x" ``` lars@66268 ` 307` ``` using that assms by fastforce ``` lars@64180 ` 308` ``` then show "fmlookup (fmfilter P m) x = fmlookup m x" ``` lars@63900 ` 309` ``` by simp ``` lars@63900 ` 310` ```qed ``` lars@63885 ` 311` lars@66268 ` 312` ```lemma fmfilter_false[simp]: ``` lars@66268 ` 313` ``` assumes "\x y. fmlookup m x = Some y \ \ P x" ``` lars@66268 ` 314` ``` shows "fmfilter P m = fmempty" ``` lars@66268 ` 315` ```using assms by transfer' (fastforce simp: map_filter_def) ``` lars@63885 ` 316` lars@63885 ` 317` ```lemma fmfilter_comp[simp]: "fmfilter P (fmfilter Q m) = fmfilter (\x. P x \ Q x) m" ``` lars@63885 ` 318` ```by transfer' (auto simp: map_filter_def) ``` lars@63885 ` 319` lars@63885 ` 320` ```lemma fmfilter_comm: "fmfilter P (fmfilter Q m) = fmfilter Q (fmfilter P m)" ``` lars@63885 ` 321` ```unfolding fmfilter_comp by meson ``` lars@63885 ` 322` lars@63885 ` 323` ```lemma fmfilter_cong[cong]: ``` lars@66268 ` 324` ``` assumes "\x y. fmlookup m x = Some y \ P x = Q x" ``` lars@63885 ` 325` ``` shows "fmfilter P m = fmfilter Q m" ``` lars@63900 ` 326` ```proof (rule fmap_ext) ``` lars@63900 ` 327` ``` fix x ``` lars@63900 ` 328` ``` have "fmlookup m x = None" if "P x \ Q x" ``` lars@66268 ` 329` ``` using that assms by fastforce ``` lars@64180 ` 330` ``` then show "fmlookup (fmfilter P m) x = fmlookup (fmfilter Q m) x" ``` lars@63900 ` 331` ``` by auto ``` lars@63900 ` 332` ```qed ``` lars@63885 ` 333` lars@63885 ` 334` ```lemma fmfilter_cong'[fundef_cong]: ``` lars@67485 ` 335` ``` assumes "m = n" "\x. x \ fmdom' m \ P x = Q x" ``` lars@67485 ` 336` ``` shows "fmfilter P m = fmfilter Q n" ``` lars@67485 ` 337` ```using assms(2) unfolding assms(1) ``` lars@66268 ` 338` ```by (rule fmfilter_cong) (metis fmdom'I) ``` lars@63885 ` 339` lars@63900 ` 340` ```lemma fmfilter_upd[simp]: ``` lars@63900 ` 341` ``` "fmfilter P (fmupd x y m) = (if P x then fmupd x y (fmfilter P m) else fmfilter P m)" ``` lars@63885 ` 342` ```by transfer' (auto simp: map_upd_def map_filter_def) ``` lars@63885 ` 343` lars@63885 ` 344` ```lift_definition fmdrop :: "'a \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 345` ``` is map_drop ``` lars@63885 ` 346` ``` parametric map_drop_transfer ``` lars@63885 ` 347` ```unfolding map_drop_def by auto ``` lars@63885 ` 348` lars@63885 ` 349` ```lemma fmdrop_lookup[simp]: "fmlookup (fmdrop a m) a = None" ``` lars@63885 ` 350` ```by transfer' (auto simp: map_drop_def map_filter_def) ``` lars@63885 ` 351` lars@63885 ` 352` ```lift_definition fmdrop_set :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 353` ``` is map_drop_set ``` lars@63885 ` 354` ``` parametric map_drop_set_transfer ``` lars@63885 ` 355` ```unfolding map_drop_set_def by auto ``` lars@63885 ` 356` lars@63885 ` 357` ```lift_definition fmdrop_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 358` ``` is map_drop_set ``` lars@63885 ` 359` ``` parametric map_drop_set_transfer ``` lars@63885 ` 360` ```unfolding map_drop_set_def by auto ``` lars@63885 ` 361` lars@63885 ` 362` ```lift_definition fmrestrict_set :: "'a set \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 363` ``` is map_restrict_set ``` lars@63885 ` 364` ``` parametric map_restrict_set_transfer ``` lars@63885 ` 365` ```unfolding map_restrict_set_def by auto ``` lars@63885 ` 366` lars@63885 ` 367` ```lift_definition fmrestrict_fset :: "'a fset \ ('a, 'b) fmap \ ('a, 'b) fmap" ``` lars@63885 ` 368` ``` is map_restrict_set ``` lars@63885 ` 369` ``` parametric map_restrict_set_transfer ``` lars@63885 ` 370` ```unfolding map_restrict_set_def by auto ``` lars@63885 ` 371` lars@63885 ` 372` ```lemma fmfilter_alt_defs: ``` lars@63885 ` 373` ``` "fmdrop a = fmfilter (\a'. a' \ a)" ``` lars@63885 ` 374` ``` "fmdrop_set A = fmfilter (\a. a \ A)" ``` lars@63885 ` 375` ``` "fmdrop_fset B = fmfilter (\a. a |\| B)" ``` lars@63885 ` 376` ``` "fmrestrict_set A = fmfilter (\a. a \ A)" ``` lars@63885 ` 377` ``` "fmrestrict_fset B = fmfilter (\a. a |\| B)" ``` lars@63885 ` 378` ```by (transfer'; simp add: map_drop_def map_drop_set_def map_restrict_set_def)+ ``` lars@63885 ` 379` lars@63885 ` 380` ```lemma fmdom_drop[simp]: "fmdom (fmdrop a m) = fmdom m - {|a|}" unfolding fmfilter_alt_defs by auto ``` lars@63885 ` 381` ```lemma fmdom'_drop[simp]: "fmdom' (fmdrop a m) = fmdom' m - {a}" unfolding fmfilter_alt_defs by auto ``` lars@63885 ` 382` ```lemma fmdom'_drop_set[simp]: "fmdom' (fmdrop_set A m) = fmdom' m - A" unfolding fmfilter_alt_defs by auto ``` lars@63885 ` 383` ```lemma fmdom_drop_fset[simp]: "fmdom (fmdrop_fset A m) = fmdom m - A" unfolding fmfilter_alt_defs by auto ``` lars@63885 ` 384` ```lemma fmdom'_restrict_set: "fmdom' (fmrestrict_set A m) \ A" unfolding fmfilter_alt_defs by auto ``` lars@63885 ` 385` ```lemma fmdom_restrict_fset: "fmdom (fmrestrict_fset A m) |\| A" unfolding fmfilter_alt_defs by auto ``` lars@63885 ` 386` lars@63885 ` 387` ```lemma fmdom'_drop_fset[simp]: "fmdom' (fmdrop_fset A m) = fmdom' m - fset A" ``` lars@63885 ` 388` ```unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def split: if_splits) ``` lars@63885 ` 389` lars@63885 ` 390` ```lemma fmdom'_restrict_fset: "fmdom' (fmrestrict_fset A m) \ fset A" ``` lars@63885 ` 391` ```unfolding fmfilter_alt_defs by transfer' (auto simp: map_filter_def) ``` lars@63885 ` 392` lars@63885 ` 393` ```lemma fmlookup_drop[simp]: ``` lars@63885 ` 394` ``` "fmlookup (fmdrop a m) x = (if x \ a then fmlookup m x else None)" ``` lars@63885 ` 395` ```unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 396` lars@63885 ` 397` ```lemma fmlookup_drop_set[simp]: ``` lars@63885 ` 398` ``` "fmlookup (fmdrop_set A m) x = (if x \ A then fmlookup m x else None)" ``` lars@63885 ` 399` ```unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 400` lars@63885 ` 401` ```lemma fmlookup_drop_fset[simp]: ``` lars@63885 ` 402` ``` "fmlookup (fmdrop_fset A m) x = (if x |\| A then fmlookup m x else None)" ``` lars@63885 ` 403` ```unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 404` lars@63885 ` 405` ```lemma fmlookup_restrict_set[simp]: ``` lars@63885 ` 406` ``` "fmlookup (fmrestrict_set A m) x = (if x \ A then fmlookup m x else None)" ``` lars@63885 ` 407` ```unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 408` lars@63885 ` 409` ```lemma fmlookup_restrict_fset[simp]: ``` lars@63885 ` 410` ``` "fmlookup (fmrestrict_fset A m) x = (if x |\| A then fmlookup m x else None)" ``` lars@63885 ` 411` ```unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 412` lars@63900 ` 413` ```lemma fmrestrict_set_dom[simp]: "fmrestrict_set (fmdom' m) m = m" ``` lars@66268 ` 414` ``` by (rule fmap_ext) auto ``` lars@63900 ` 415` lars@63900 ` 416` ```lemma fmrestrict_fset_dom[simp]: "fmrestrict_fset (fmdom m) m = m" ``` lars@66268 ` 417` ``` by (rule fmap_ext) auto ``` lars@63900 ` 418` lars@63885 ` 419` ```lemma fmdrop_empty[simp]: "fmdrop a fmempty = fmempty" ``` lars@63885 ` 420` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 421` lars@63885 ` 422` ```lemma fmdrop_set_empty[simp]: "fmdrop_set A fmempty = fmempty" ``` lars@63885 ` 423` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 424` lars@63885 ` 425` ```lemma fmdrop_fset_empty[simp]: "fmdrop_fset A fmempty = fmempty" ``` lars@63885 ` 426` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 427` lars@63885 ` 428` ```lemma fmrestrict_set_empty[simp]: "fmrestrict_set A fmempty = fmempty" ``` lars@63885 ` 429` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 430` lars@63885 ` 431` ```lemma fmrestrict_fset_empty[simp]: "fmrestrict_fset A fmempty = fmempty" ``` lars@63885 ` 432` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 433` lars@66269 ` 434` ```lemma fmdrop_set_null[simp]: "fmdrop_set {} m = m" ``` lars@66269 ` 435` ``` by (rule fmap_ext) auto ``` lars@66269 ` 436` lars@66269 ` 437` ```lemma fmdrop_fset_null[simp]: "fmdrop_fset {||} m = m" ``` lars@66269 ` 438` ``` by (rule fmap_ext) auto ``` lars@66269 ` 439` lars@63885 ` 440` ```lemma fmdrop_set_single[simp]: "fmdrop_set {a} m = fmdrop a m" ``` lars@63885 ` 441` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 442` lars@63885 ` 443` ```lemma fmdrop_fset_single[simp]: "fmdrop_fset {|a|} m = fmdrop a m" ``` lars@63885 ` 444` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 445` lars@63885 ` 446` ```lemma fmrestrict_set_null[simp]: "fmrestrict_set {} m = fmempty" ``` lars@63885 ` 447` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 448` lars@63885 ` 449` ```lemma fmrestrict_fset_null[simp]: "fmrestrict_fset {||} m = fmempty" ``` lars@63885 ` 450` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 451` lars@63885 ` 452` ```lemma fmdrop_comm: "fmdrop a (fmdrop b m) = fmdrop b (fmdrop a m)" ``` lars@63885 ` 453` ```unfolding fmfilter_alt_defs by (rule fmfilter_comm) ``` lars@63885 ` 454` lars@66269 ` 455` ```lemma fmdrop_set_insert[simp]: "fmdrop_set (insert x S) m = fmdrop x (fmdrop_set S m)" ``` lars@66269 ` 456` ```by (rule fmap_ext) auto ``` lars@66269 ` 457` lars@66269 ` 458` ```lemma fmdrop_fset_insert[simp]: "fmdrop_fset (finsert x S) m = fmdrop x (fmdrop_fset S m)" ``` lars@66269 ` 459` ```by (rule fmap_ext) auto ``` lars@66269 ` 460` lars@63885 ` 461` ```lift_definition fmadd :: "('a, 'b) fmap \ ('a, 'b) fmap \ ('a, 'b) fmap" (infixl "++\<^sub>f" 100) ``` lars@63885 ` 462` ``` is map_add ``` lars@63885 ` 463` ``` parametric map_add_transfer ``` lars@63885 ` 464` ```by simp ``` lars@63885 ` 465` lars@63900 ` 466` ```lemma fmlookup_add[simp]: ``` lars@63900 ` 467` ``` "fmlookup (m ++\<^sub>f n) x = (if x |\| fmdom n then fmlookup n x else fmlookup m x)" ``` lars@63900 ` 468` ``` by transfer' (auto simp: map_add_def split: option.splits) ``` lars@63900 ` 469` lars@63885 ` 470` ```lemma fmdom_add[simp]: "fmdom (m ++\<^sub>f n) = fmdom m |\| fmdom n" by transfer' auto ``` lars@63885 ` 471` ```lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \ fmdom' n" by transfer' auto ``` lars@63885 ` 472` lars@63885 ` 473` ```lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n" ``` lars@63900 ` 474` ``` by (rule fmap_ext) auto ``` lars@63885 ` 475` lars@63885 ` 476` ```lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n" ``` lars@66268 ` 477` ``` by (rule fmap_ext) auto ``` lars@63885 ` 478` lars@63885 ` 479` ```lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n" ``` lars@63885 ` 480` ```by transfer' (auto simp: map_filter_def map_add_def) ``` lars@63885 ` 481` lars@63885 ` 482` ```lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n" ``` lars@63885 ` 483` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 484` lars@63885 ` 485` ```lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n" ``` lars@63885 ` 486` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 487` lars@63885 ` 488` ```lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n" ``` lars@63885 ` 489` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 490` lars@63885 ` 491` ```lemma fmrestrict_set_add_distrib[simp]: ``` lars@63885 ` 492` ``` "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n" ``` lars@63885 ` 493` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 494` lars@63885 ` 495` ```lemma fmrestrict_fset_add_distrib[simp]: ``` lars@63885 ` 496` ``` "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n" ``` lars@63885 ` 497` ``` unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 498` lars@63885 ` 499` ```lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m" ``` lars@63885 ` 500` ```by (transfer'; auto)+ ``` lars@63885 ` 501` lars@63885 ` 502` ```lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m" ``` lars@63885 ` 503` ```by transfer' (auto simp: map_add_def split: option.splits) ``` lars@63885 ` 504` lars@63885 ` 505` ```lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p" ``` lars@63885 ` 506` ```by transfer' simp ``` lars@63885 ` 507` lars@66269 ` 508` ```lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)" ``` lars@66269 ` 509` ```by (rule fmap_ext) simp ``` lars@66269 ` 510` lars@63885 ` 511` ```lift_definition fmpred :: "('a \ 'b \ bool) \ ('a, 'b) fmap \ bool" ``` lars@63885 ` 512` ``` is map_pred ``` lars@63885 ` 513` ``` parametric map_pred_transfer ``` lars@63885 ` 514` ```. ``` lars@63885 ` 515` lars@63885 ` 516` ```lemma fmpredI[intro]: ``` lars@63885 ` 517` ``` assumes "\x y. fmlookup m x = Some y \ P x y" ``` lars@63885 ` 518` ``` shows "fmpred P m" ``` lars@63885 ` 519` ```using assms ``` lars@63885 ` 520` ```by transfer' (auto simp: map_pred_def split: option.splits) ``` lars@63885 ` 521` lars@66267 ` 522` ```lemma fmpredD[dest]: "fmpred P m \ fmlookup m x = Some y \ P x y" ``` lars@63885 ` 523` ```by transfer' (auto simp: map_pred_def split: option.split_asm) ``` lars@63885 ` 524` lars@63885 ` 525` ```lemma fmpred_iff: "fmpred P m \ (\x y. fmlookup m x = Some y \ P x y)" ``` lars@63885 ` 526` ```by auto ``` lars@63885 ` 527` lars@63885 ` 528` ```lemma fmpred_alt_def: "fmpred P m \ fBall (fmdom m) (\x. P x (the (fmlookup m x)))" ``` lars@63885 ` 529` ```unfolding fmpred_iff ``` lars@63885 ` 530` ```apply auto ``` lars@63900 ` 531` ```apply (rename_tac x y) ``` lars@63885 ` 532` ```apply (erule_tac x = x in fBallE) ``` lars@63885 ` 533` ```apply simp ``` lars@63885 ` 534` ```by (simp add: fmlookup_dom_iff) ``` lars@63885 ` 535` lars@63885 ` 536` ```lemma fmpred_empty[intro!, simp]: "fmpred P fmempty" ``` lars@63885 ` 537` ```by auto ``` lars@63885 ` 538` lars@63885 ` 539` ```lemma fmpred_upd[intro]: "fmpred P m \ P x y \ fmpred P (fmupd x y m)" ``` lars@63885 ` 540` ```by transfer' (auto simp: map_pred_def map_upd_def) ``` lars@63885 ` 541` lars@63885 ` 542` ```lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \ P x y" ``` lars@63885 ` 543` ```by auto ``` lars@63885 ` 544` lars@63885 ` 545` ```lemma fmpred_add[intro]: "fmpred P m \ fmpred P n \ fmpred P (m ++\<^sub>f n)" ``` lars@63885 ` 546` ```by transfer' (auto simp: map_pred_def map_add_def split: option.splits) ``` lars@63885 ` 547` lars@63885 ` 548` ```lemma fmpred_filter[intro]: "fmpred P m \ fmpred P (fmfilter Q m)" ``` lars@63885 ` 549` ```by transfer' (auto simp: map_pred_def map_filter_def) ``` lars@63885 ` 550` lars@63885 ` 551` ```lemma fmpred_drop[intro]: "fmpred P m \ fmpred P (fmdrop a m)" ``` lars@63885 ` 552` ``` by (auto simp: fmfilter_alt_defs) ``` lars@63885 ` 553` lars@63885 ` 554` ```lemma fmpred_drop_set[intro]: "fmpred P m \ fmpred P (fmdrop_set A m)" ``` lars@63885 ` 555` ``` by (auto simp: fmfilter_alt_defs) ``` lars@63885 ` 556` lars@63885 ` 557` ```lemma fmpred_drop_fset[intro]: "fmpred P m \ fmpred P (fmdrop_fset A m)" ``` lars@63885 ` 558` ``` by (auto simp: fmfilter_alt_defs) ``` lars@63885 ` 559` lars@63885 ` 560` ```lemma fmpred_restrict_set[intro]: "fmpred P m \ fmpred P (fmrestrict_set A m)" ``` lars@63885 ` 561` ``` by (auto simp: fmfilter_alt_defs) ``` lars@63885 ` 562` lars@63885 ` 563` ```lemma fmpred_restrict_fset[intro]: "fmpred P m \ fmpred P (fmrestrict_fset A m)" ``` lars@63885 ` 564` ``` by (auto simp: fmfilter_alt_defs) ``` lars@63885 ` 565` lars@63885 ` 566` ```lemma fmpred_cases[consumes 1]: ``` lars@63885 ` 567` ``` assumes "fmpred P m" ``` lars@63885 ` 568` ``` obtains (none) "fmlookup m x = None" | (some) y where "fmlookup m x = Some y" "P x y" ``` lars@63885 ` 569` ```using assms by auto ``` lars@63885 ` 570` lars@63885 ` 571` ```lift_definition fmsubset :: "('a, 'b) fmap \ ('a, 'b) fmap \ bool" (infix "\\<^sub>f" 50) ``` lars@63885 ` 572` ``` is map_le ``` lars@63885 ` 573` ```. ``` lars@63885 ` 574` lars@63885 ` 575` ```lemma fmsubset_alt_def: "m \\<^sub>f n \ fmpred (\k v. fmlookup n k = Some v) m" ``` lars@63885 ` 576` ```by transfer' (auto simp: map_pred_def map_le_def dom_def split: option.splits) ``` lars@63885 ` 577` lars@63885 ` 578` ```lemma fmsubset_pred: "fmpred P m \ n \\<^sub>f m \ fmpred P n" ``` lars@63885 ` 579` ```unfolding fmsubset_alt_def fmpred_iff ``` lars@63885 ` 580` ```by auto ``` lars@63885 ` 581` lars@63885 ` 582` ```lemma fmsubset_filter_mono: "m \\<^sub>f n \ fmfilter P m \\<^sub>f fmfilter P n" ``` lars@63885 ` 583` ```unfolding fmsubset_alt_def fmpred_iff ``` lars@63885 ` 584` ```by auto ``` lars@63885 ` 585` lars@63885 ` 586` ```lemma fmsubset_drop_mono: "m \\<^sub>f n \ fmdrop a m \\<^sub>f fmdrop a n" ``` lars@63885 ` 587` ```unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) ``` lars@63885 ` 588` lars@63885 ` 589` ```lemma fmsubset_drop_set_mono: "m \\<^sub>f n \ fmdrop_set A m \\<^sub>f fmdrop_set A n" ``` lars@63885 ` 590` ```unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) ``` lars@63885 ` 591` lars@63885 ` 592` ```lemma fmsubset_drop_fset_mono: "m \\<^sub>f n \ fmdrop_fset A m \\<^sub>f fmdrop_fset A n" ``` lars@63885 ` 593` ```unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) ``` lars@63885 ` 594` lars@63885 ` 595` ```lemma fmsubset_restrict_set_mono: "m \\<^sub>f n \ fmrestrict_set A m \\<^sub>f fmrestrict_set A n" ``` lars@63885 ` 596` ```unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) ``` lars@63885 ` 597` lars@63885 ` 598` ```lemma fmsubset_restrict_fset_mono: "m \\<^sub>f n \ fmrestrict_fset A m \\<^sub>f fmrestrict_fset A n" ``` lars@63885 ` 599` ```unfolding fmfilter_alt_defs by (rule fmsubset_filter_mono) ``` lars@63885 ` 600` lars@66282 ` 601` ```lift_definition fset_of_fmap :: "('a, 'b) fmap \ ('a \ 'b) fset" is set_of_map ``` lars@66282 ` 602` ```by (rule set_of_map_finite) ``` lars@66282 ` 603` lars@66282 ` 604` ```lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap" ``` lars@66282 ` 605` ```apply rule ``` lars@66282 ` 606` ```apply transfer' ``` lars@66282 ` 607` ```using set_of_map_inj unfolding inj_def by auto ``` lars@66282 ` 608` lars@66398 ` 609` ```lemma fset_of_fmap_iff[simp]: "(a, b) |\| fset_of_fmap m \ fmlookup m a = Some b" ``` lars@66398 ` 610` ```by transfer' (auto simp: set_of_map_def) ``` lars@66398 ` 611` lars@66398 ` 612` ```lemma fset_of_fmap_iff'[simp]: "(a, b) \ fset (fset_of_fmap m) \ fmlookup m a = Some b" ``` lars@66398 ` 613` ```by transfer' (auto simp: set_of_map_def) ``` lars@66398 ` 614` lars@66398 ` 615` lars@63885 ` 616` ```lift_definition fmap_of_list :: "('a \ 'b) list \ ('a, 'b) fmap" ``` lars@63885 ` 617` ``` is map_of ``` lars@63885 ` 618` ``` parametric map_of_transfer ``` lars@63885 ` 619` ```by (rule finite_dom_map_of) ``` lars@63885 ` 620` lars@63885 ` 621` ```lemma fmap_of_list_simps[simp]: ``` lars@63885 ` 622` ``` "fmap_of_list [] = fmempty" ``` lars@63885 ` 623` ``` "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)" ``` lars@63885 ` 624` ```by (transfer, simp add: map_upd_def)+ ``` lars@63885 ` 625` lars@63885 ` 626` ```lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs" ``` lars@63885 ` 627` ```by transfer' simp ``` lars@63885 ` 628` lars@63885 ` 629` ```lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]" ``` lars@63885 ` 630` ```by transfer' (auto simp: map_upd_def) ``` lars@63885 ` 631` lars@63885 ` 632` ```lemma fmpred_of_list[intro]: ``` lars@63885 ` 633` ``` assumes "\k v. (k, v) \ set xs \ P k v" ``` lars@63885 ` 634` ``` shows "fmpred P (fmap_of_list xs)" ``` lars@63885 ` 635` ```using assms ``` lars@63885 ` 636` ```by (induction xs) (transfer'; auto simp: map_pred_def)+ ``` lars@63885 ` 637` lars@63885 ` 638` ```lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \ (k, v) \ set xs" ``` lars@63885 ` 639` ```by transfer' (auto dest: map_of_SomeD) ``` lars@63885 ` 640` lars@66269 ` 641` ```lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)" ``` lars@66269 ` 642` ```apply transfer' ``` lars@66269 ` 643` ```apply (subst dom_map_of_conv_image_fst) ``` lars@66269 ` 644` ```apply auto ``` lars@66269 ` 645` ```done ``` lars@66269 ` 646` lars@63885 ` 647` ```lift_definition fmrel_on_fset :: "'a fset \ ('b \ 'c \ bool) \ ('a, 'b) fmap \ ('a, 'c) fmap \ bool" ``` lars@63885 ` 648` ``` is rel_map_on_set ``` lars@63885 ` 649` ```. ``` lars@63885 ` 650` lars@63885 ` 651` ```lemma fmrel_on_fset_alt_def: "fmrel_on_fset S P m n \ fBall S (\x. rel_option P (fmlookup m x) (fmlookup n x))" ``` lars@63885 ` 652` ```by transfer' (auto simp: rel_map_on_set_def eq_onp_def rel_fun_def) ``` lars@63885 ` 653` lars@64181 ` 654` ```lemma fmrel_on_fsetI[intro]: ``` lars@63885 ` 655` ``` assumes "\x. x |\| S \ rel_option P (fmlookup m x) (fmlookup n x)" ``` lars@63885 ` 656` ``` shows "fmrel_on_fset S P m n" ``` lars@63885 ` 657` ```using assms ``` lars@63885 ` 658` ```unfolding fmrel_on_fset_alt_def by auto ``` lars@63885 ` 659` lars@63885 ` 660` ```lemma fmrel_on_fset_mono[mono]: "R \ Q \ fmrel_on_fset S R \ fmrel_on_fset S Q" ``` lars@63885 ` 661` ```unfolding fmrel_on_fset_alt_def[abs_def] ``` lars@63885 ` 662` ```apply (intro le_funI fBall_mono) ``` lars@63885 ` 663` ```using option.rel_mono by auto ``` lars@63885 ` 664` lars@63885 ` 665` ```lemma fmrel_on_fsetD: "x |\| S \ fmrel_on_fset S P m n \ rel_option P (fmlookup m x) (fmlookup n x)" ``` lars@63885 ` 666` ```unfolding fmrel_on_fset_alt_def ``` lars@63885 ` 667` ```by auto ``` lars@63885 ` 668` lars@63885 ` 669` ```lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \ T |\| S \ fmrel_on_fset T R m n" ``` lars@63885 ` 670` ```unfolding fmrel_on_fset_alt_def ``` lars@63885 ` 671` ```by auto ``` lars@63885 ` 672` lars@66274 ` 673` ```lemma fmrel_on_fset_unionI: ``` lars@66274 ` 674` ``` "fmrel_on_fset A R m n \ fmrel_on_fset B R m n \ fmrel_on_fset (A |\| B) R m n" ``` lars@66274 ` 675` ```unfolding fmrel_on_fset_alt_def ``` lars@66274 ` 676` ```by auto ``` lars@66274 ` 677` lars@66274 ` 678` ```lemma fmrel_on_fset_updateI: ``` lars@66274 ` 679` ``` assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2" ``` lars@66274 ` 680` ``` shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)" ``` lars@66274 ` 681` ```using assms ``` lars@66274 ` 682` ```unfolding fmrel_on_fset_alt_def ``` lars@66274 ` 683` ```by auto ``` lars@66274 ` 684` lars@63885 ` 685` ```end ``` lars@63885 ` 686` lars@63885 ` 687` lars@63885 ` 688` ```subsection \BNF setup\ ``` lars@63885 ` 689` lars@63885 ` 690` ```lift_bnf ('a, fmran': 'b) fmap [wits: Map.empty] ``` lars@63885 ` 691` ``` for map: fmmap ``` lars@63885 ` 692` ``` rel: fmrel ``` lars@63885 ` 693` ``` by auto ``` lars@63885 ` 694` lars@66269 ` 695` ```declare fmap.pred_mono[mono] ``` lars@66268 ` 696` lars@63885 ` 697` ```context includes lifting_syntax begin ``` lars@63885 ` 698` lars@63885 ` 699` ```lemma fmmap_transfer[transfer_rule]: ``` nipkow@67399 ` 700` ``` "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=)) (\f. (\) (map_option f)) fmmap" ``` lars@64180 ` 701` ``` unfolding fmmap_def ``` lars@64180 ` 702` ``` by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def) ``` lars@63885 ` 703` lars@63885 ` 704` ```lemma fmran'_transfer[transfer_rule]: ``` nipkow@67399 ` 705` ``` "(pcr_fmap (=) (=) ===> (=)) (\x. UNION (range x) set_option) fmran'" ``` lars@64180 ` 706` ``` unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce ``` lars@63885 ` 707` lars@63885 ` 708` ```lemma fmrel_transfer[transfer_rule]: ``` nipkow@67399 ` 709` ``` "((=) ===> pcr_fmap (=) (=) ===> pcr_fmap (=) (=) ===> (=)) rel_map fmrel" ``` lars@64180 ` 710` ``` unfolding fmrel_def fmap.pcr_cr_eq cr_fmap_def vimage2p_def by fastforce ``` lars@63885 ` 711` lars@63885 ` 712` ```end ``` lars@63885 ` 713` lars@63885 ` 714` lars@66268 ` 715` ```lemma fmran'_alt_def: "fmran' m = fset (fmran m)" ``` lars@63885 ` 716` ```including fset.lifting ``` lars@63885 ` 717` ```by transfer' (auto simp: ran_def fun_eq_iff) ``` lars@63885 ` 718` lars@66268 ` 719` ```lemma fmlookup_ran'_iff: "y \ fmran' m \ (\x. fmlookup m x = Some y)" ``` lars@66268 ` 720` ```by transfer' (auto simp: ran_def) ``` lars@66268 ` 721` lars@66268 ` 722` ```lemma fmran'I: "fmlookup m x = Some y \ y \ fmran' m" by (auto simp: fmlookup_ran'_iff) ``` lars@66268 ` 723` lars@66268 ` 724` ```lemma fmran'E[elim]: ``` lars@66268 ` 725` ``` assumes "y \ fmran' m" ``` lars@66268 ` 726` ``` obtains x where "fmlookup m x = Some y" ``` lars@66268 ` 727` ```using assms by (auto simp: fmlookup_ran'_iff) ``` lars@63885 ` 728` lars@63885 ` 729` ```lemma fmrel_iff: "fmrel R m n \ (\x. rel_option R (fmlookup m x) (fmlookup n x))" ``` lars@63885 ` 730` ```by transfer' (auto simp: rel_fun_def) ``` lars@63885 ` 731` lars@63885 ` 732` ```lemma fmrelI[intro]: ``` lars@63885 ` 733` ``` assumes "\x. rel_option R (fmlookup m x) (fmlookup n x)" ``` lars@63885 ` 734` ``` shows "fmrel R m n" ``` lars@63885 ` 735` ```using assms ``` lars@63885 ` 736` ```by transfer' auto ``` lars@63885 ` 737` lars@63885 ` 738` ```lemma fmrel_upd[intro]: "fmrel P m n \ P x y \ fmrel P (fmupd k x m) (fmupd k y n)" ``` lars@63885 ` 739` ```by transfer' (auto simp: map_upd_def rel_fun_def) ``` lars@63885 ` 740` lars@63885 ` 741` ```lemma fmrelD[dest]: "fmrel P m n \ rel_option P (fmlookup m x) (fmlookup n x)" ``` lars@63885 ` 742` ```by transfer' (auto simp: rel_fun_def) ``` lars@63885 ` 743` lars@63885 ` 744` ```lemma fmrel_addI[intro]: ``` lars@63885 ` 745` ``` assumes "fmrel P m n" "fmrel P a b" ``` lars@63885 ` 746` ``` shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)" ``` lars@63885 ` 747` ```using assms ``` lars@63885 ` 748` ```apply transfer' ``` lars@63885 ` 749` ```apply (auto simp: rel_fun_def map_add_def) ``` lars@63885 ` 750` ```by (metis option.case_eq_if option.collapse option.rel_sel) ``` lars@63885 ` 751` lars@63885 ` 752` ```lemma fmrel_cases[consumes 1]: ``` lars@63885 ` 753` ``` assumes "fmrel P m n" ``` lars@63885 ` 754` ``` obtains (none) "fmlookup m x = None" "fmlookup n x = None" ``` lars@63885 ` 755` ``` | (some) a b where "fmlookup m x = Some a" "fmlookup n x = Some b" "P a b" ``` lars@63885 ` 756` ```proof - ``` lars@63885 ` 757` ``` from assms have "rel_option P (fmlookup m x) (fmlookup n x)" ``` lars@63885 ` 758` ``` by auto ``` lars@64180 ` 759` ``` then show thesis ``` lars@63885 ` 760` ``` using none some ``` lars@63885 ` 761` ``` by (cases rule: option.rel_cases) auto ``` lars@63885 ` 762` ```qed ``` lars@63885 ` 763` lars@63885 ` 764` ```lemma fmrel_filter[intro]: "fmrel P m n \ fmrel P (fmfilter Q m) (fmfilter Q n)" ``` lars@63885 ` 765` ```unfolding fmrel_iff by auto ``` lars@63885 ` 766` lars@63885 ` 767` ```lemma fmrel_drop[intro]: "fmrel P m n \ fmrel P (fmdrop a m) (fmdrop a n)" ``` lars@63885 ` 768` ``` unfolding fmfilter_alt_defs by blast ``` lars@63885 ` 769` lars@63885 ` 770` ```lemma fmrel_drop_set[intro]: "fmrel P m n \ fmrel P (fmdrop_set A m) (fmdrop_set A n)" ``` lars@63885 ` 771` ``` unfolding fmfilter_alt_defs by blast ``` lars@63885 ` 772` lars@63885 ` 773` ```lemma fmrel_drop_fset[intro]: "fmrel P m n \ fmrel P (fmdrop_fset A m) (fmdrop_fset A n)" ``` lars@63885 ` 774` ``` unfolding fmfilter_alt_defs by blast ``` lars@63885 ` 775` lars@63885 ` 776` ```lemma fmrel_restrict_set[intro]: "fmrel P m n \ fmrel P (fmrestrict_set A m) (fmrestrict_set A n)" ``` lars@63885 ` 777` ``` unfolding fmfilter_alt_defs by blast ``` lars@63885 ` 778` lars@63885 ` 779` ```lemma fmrel_restrict_fset[intro]: "fmrel P m n \ fmrel P (fmrestrict_fset A m) (fmrestrict_fset A n)" ``` lars@63885 ` 780` ``` unfolding fmfilter_alt_defs by blast ``` lars@63885 ` 781` lars@66274 ` 782` ```lemma fmrel_on_fset_fmrel_restrict: ``` lars@66274 ` 783` ``` "fmrel_on_fset S P m n \ fmrel P (fmrestrict_fset S m) (fmrestrict_fset S n)" ``` lars@66274 ` 784` ```unfolding fmrel_on_fset_alt_def fmrel_iff ``` lars@66274 ` 785` ```by auto ``` lars@66274 ` 786` lars@66274 ` 787` ```lemma fmrel_on_fset_refl_strong: ``` lars@66274 ` 788` ``` assumes "\x y. x |\| S \ fmlookup m x = Some y \ P y y" ``` lars@66274 ` 789` ``` shows "fmrel_on_fset S P m m" ``` lars@66274 ` 790` ```unfolding fmrel_on_fset_fmrel_restrict fmrel_iff ``` lars@66274 ` 791` ```using assms ``` lars@66274 ` 792` ```by (simp add: option.rel_sel) ``` lars@66274 ` 793` lars@66274 ` 794` ```lemma fmrel_on_fset_addI: ``` lars@66274 ` 795` ``` assumes "fmrel_on_fset S P m n" "fmrel_on_fset S P a b" ``` lars@66274 ` 796` ``` shows "fmrel_on_fset S P (m ++\<^sub>f a) (n ++\<^sub>f b)" ``` lars@66274 ` 797` ```using assms ``` lars@66274 ` 798` ```unfolding fmrel_on_fset_fmrel_restrict ``` lars@66274 ` 799` ```by auto ``` lars@66274 ` 800` lars@66274 ` 801` ```lemma fmrel_fmdom_eq: ``` lars@66274 ` 802` ``` assumes "fmrel P x y" ``` lars@66274 ` 803` ``` shows "fmdom x = fmdom y" ``` lars@66274 ` 804` ```proof - ``` lars@66274 ` 805` ``` have "a |\| fmdom x \ a |\| fmdom y" for a ``` lars@66274 ` 806` ``` proof - ``` lars@66274 ` 807` ``` have "rel_option P (fmlookup x a) (fmlookup y a)" ``` lars@66274 ` 808` ``` using assms by (simp add: fmrel_iff) ``` lars@66274 ` 809` ``` thus ?thesis ``` lars@66274 ` 810` ``` by cases (auto intro: fmdomI) ``` lars@66274 ` 811` ``` qed ``` lars@66274 ` 812` ``` thus ?thesis ``` lars@66274 ` 813` ``` by auto ``` lars@66274 ` 814` ```qed ``` lars@66274 ` 815` lars@66274 ` 816` ```lemma fmrel_fmdom'_eq: "fmrel P x y \ fmdom' x = fmdom' y" ``` lars@66274 ` 817` ```unfolding fmdom'_alt_def ``` lars@66274 ` 818` ```by (metis fmrel_fmdom_eq) ``` lars@66274 ` 819` lars@66274 ` 820` ```lemma fmrel_rel_fmran: ``` lars@66274 ` 821` ``` assumes "fmrel P x y" ``` lars@66274 ` 822` ``` shows "rel_fset P (fmran x) (fmran y)" ``` lars@66274 ` 823` ```proof - ``` lars@66274 ` 824` ``` { ``` lars@66274 ` 825` ``` fix b ``` lars@66274 ` 826` ``` assume "b |\| fmran x" ``` lars@66274 ` 827` ``` then obtain a where "fmlookup x a = Some b" ``` lars@66274 ` 828` ``` by auto ``` lars@66274 ` 829` ``` moreover have "rel_option P (fmlookup x a) (fmlookup y a)" ``` lars@66274 ` 830` ``` using assms by auto ``` lars@66274 ` 831` ``` ultimately have "\b'. b' |\| fmran y \ P b b'" ``` lars@66274 ` 832` ``` by (metis option_rel_Some1 fmranI) ``` lars@66274 ` 833` ``` } ``` lars@66274 ` 834` ``` moreover ``` lars@66274 ` 835` ``` { ``` lars@66274 ` 836` ``` fix b ``` lars@66274 ` 837` ``` assume "b |\| fmran y" ``` lars@66274 ` 838` ``` then obtain a where "fmlookup y a = Some b" ``` lars@66274 ` 839` ``` by auto ``` lars@66274 ` 840` ``` moreover have "rel_option P (fmlookup x a) (fmlookup y a)" ``` lars@66274 ` 841` ``` using assms by auto ``` lars@66274 ` 842` ``` ultimately have "\b'. b' |\| fmran x \ P b' b" ``` lars@66274 ` 843` ``` by (metis option_rel_Some2 fmranI) ``` lars@66274 ` 844` ``` } ``` lars@66274 ` 845` ``` ultimately show ?thesis ``` lars@66274 ` 846` ``` unfolding rel_fset_alt_def ``` lars@66274 ` 847` ``` by auto ``` lars@66274 ` 848` ```qed ``` lars@66274 ` 849` lars@66274 ` 850` ```lemma fmrel_rel_fmran': "fmrel P x y \ rel_set P (fmran' x) (fmran' y)" ``` lars@66274 ` 851` ```unfolding fmran'_alt_def ``` lars@66274 ` 852` ```by (metis fmrel_rel_fmran rel_fset_fset) ``` lars@66274 ` 853` lars@63885 ` 854` ```lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\_. P)" ``` lars@63885 ` 855` ```unfolding fmap.pred_set fmran'_alt_def ``` lars@63885 ` 856` ```including fset.lifting ``` lars@63885 ` 857` ```apply transfer' ``` lars@63885 ` 858` ```apply (rule ext) ``` lars@63885 ` 859` ```apply (auto simp: map_pred_def ran_def split: option.splits dest: ) ``` lars@63885 ` 860` ```done ``` lars@63885 ` 861` lars@63885 ` 862` ```lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \ pred_fmap f m" ``` lars@63885 ` 863` ```unfolding fmap.pred_set fmap.set_map ``` lars@63885 ` 864` ```by simp ``` lars@63885 ` 865` lars@66274 ` 866` ```lemma pred_fmapD: "pred_fmap P m \ x |\| fmran m \ P x" ``` lars@66274 ` 867` ```by auto ``` lars@66274 ` 868` lars@63885 ` 869` ```lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)" ``` lars@64180 ` 870` ```by transfer' auto ``` lars@63885 ` 871` lars@63885 ` 872` ```lemma fmpred_map[simp]: "fmpred P (fmmap f m) \ fmpred (\k v. P k (f v)) m" ``` lars@63885 ` 873` ```unfolding fmpred_iff pred_fmap_def fmap.set_map ``` lars@63885 ` 874` ```by auto ``` lars@63885 ` 875` lars@63885 ` 876` ```lemma fmpred_id[simp]: "fmpred (\_. id) (fmmap f m) \ fmpred (\_. f) m" ``` lars@63885 ` 877` ```by simp ``` lars@63885 ` 878` lars@63885 ` 879` ```lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n" ``` lars@63885 ` 880` ```by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits) ``` lars@63885 ` 881` lars@63885 ` 882` ```lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty" ``` lars@63885 ` 883` ```by transfer auto ``` lars@63885 ` 884` lars@63885 ` 885` ```lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m" ``` lars@63885 ` 886` ```including fset.lifting ``` lars@63885 ` 887` ```by transfer' simp ``` lars@63885 ` 888` lars@63885 ` 889` ```lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m" ``` lars@63885 ` 890` ```by transfer' simp ``` lars@63885 ` 891` lars@66269 ` 892` ```lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m" ``` lars@66269 ` 893` ```including fset.lifting ``` lars@66269 ` 894` ```by transfer' (auto simp: ran_def) ``` lars@66269 ` 895` lars@66269 ` 896` ```lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m" ``` lars@66269 ` 897` ```by transfer' (auto simp: ran_def) ``` lars@66269 ` 898` lars@63885 ` 899` ```lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)" ``` lars@63885 ` 900` ```by transfer' (auto simp: map_filter_def) ``` lars@63885 ` 901` lars@63885 ` 902` ```lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 903` ```lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 904` ```lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 905` ```lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 906` ```lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp ``` lars@63885 ` 907` lars@63885 ` 908` ```lemma fmmap_subset[intro]: "m \\<^sub>f n \ fmmap f m \\<^sub>f fmmap f n" ``` lars@63885 ` 909` ```by transfer' (auto simp: map_le_def) ``` lars@63885 ` 910` lars@66398 ` 911` ```lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\(k, v). (k, f v)) |`| fset_of_fmap m" ``` lars@66398 ` 912` ```including fset.lifting ``` lars@66398 ` 913` ```by transfer' (auto simp: set_of_map_def) ``` lars@66398 ` 914` lars@66398 ` 915` lars@66398 ` 916` ```subsection \@{const size} setup\ ``` lars@66398 ` 917` lars@66398 ` 918` ```definition size_fmap :: "('a \ nat) \ ('b \ nat) \ ('a, 'b) fmap \ nat" where ``` lars@66398 ` 919` ```[simp]: "size_fmap f g m = size_fset (\(a, b). f a + g b) (fset_of_fmap m)" ``` lars@66398 ` 920` lars@66398 ` 921` ```instantiation fmap :: (type, type) size begin ``` lars@66398 ` 922` lars@66398 ` 923` ```definition size_fmap where ``` lars@66398 ` 924` ```size_fmap_overloaded_def: "size_fmap = Finite_Map.size_fmap (\_. 0) (\_. 0)" ``` lars@66398 ` 925` lars@66398 ` 926` ```instance .. ``` lars@66398 ` 927` lars@66398 ` 928` ```end ``` lars@66398 ` 929` lars@66398 ` 930` ```lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)" ``` lars@66398 ` 931` ```unfolding size_fmap_overloaded_def ``` lars@66398 ` 932` ```by simp ``` lars@66398 ` 933` lars@66398 ` 934` ```lemma fmap_size_o_map: "inj h \ size_fmap f g \ fmmap h = size_fmap f (g \ h)" ``` lars@66398 ` 935` ``` unfolding size_fmap_def ``` lars@66398 ` 936` ``` apply (auto simp: fun_eq_iff fmmap_fset_of_fmap) ``` lars@66398 ` 937` ``` apply (subst sum.reindex) ``` lars@66398 ` 938` ``` subgoal for m ``` lars@66398 ` 939` ``` using prod.inj_map[unfolded map_prod_def, of "\x. x" h] ``` lars@66398 ` 940` ``` unfolding inj_on_def ``` lars@66398 ` 941` ``` by auto ``` lars@66398 ` 942` ``` subgoal ``` lars@66398 ` 943` ``` by (rule sum.cong) (auto split: prod.splits) ``` lars@66398 ` 944` ``` done ``` lars@66398 ` 945` lars@66398 ` 946` ```setup \ ``` lars@66398 ` 947` ```BNF_LFP_Size.register_size_global @{type_name fmap} @{const_name size_fmap} ``` lars@66398 ` 948` ``` @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps} ``` lars@66398 ` 949` ``` @{thms fmap_size_o_map} ``` lars@66398 ` 950` ```\ ``` lars@66398 ` 951` lars@63885 ` 952` lars@66269 ` 953` ```subsection \Additional operations\ ``` lars@66269 ` 954` lars@66269 ` 955` ```lift_definition fmmap_keys :: "('a \ 'b \ 'c) \ ('a, 'b) fmap \ ('a, 'c) fmap" is ``` lars@66269 ` 956` ``` "\f m a. map_option (f a) (m a)" ``` lars@66269 ` 957` ```unfolding dom_def ``` lars@66269 ` 958` ```by simp ``` lars@66269 ` 959` lars@66269 ` 960` ```lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\a b. P a (f a b)) m" ``` lars@66269 ` 961` ```by transfer' (auto simp: map_pred_def split: option.splits) ``` lars@66269 ` 962` lars@66269 ` 963` ```lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m" ``` lars@66269 ` 964` ```including fset.lifting ``` lars@66269 ` 965` ```by transfer' auto ``` lars@66269 ` 966` lars@66269 ` 967` ```lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)" ``` lars@66269 ` 968` ```by transfer' simp ``` lars@66269 ` 969` lars@66269 ` 970` ```lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)" ``` lars@66269 ` 971` ```by transfer' (auto simp: map_filter_def) ``` lars@66269 ` 972` lars@66269 ` 973` ```lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)" ``` lars@66269 ` 974` ```unfolding fmfilter_alt_defs by simp ``` lars@66269 ` 975` lars@66269 ` 976` ```lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)" ``` lars@66269 ` 977` ```unfolding fmfilter_alt_defs by simp ``` lars@66269 ` 978` lars@66269 ` 979` ```lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)" ``` lars@66269 ` 980` ```unfolding fmfilter_alt_defs by simp ``` lars@66269 ` 981` lars@66269 ` 982` ```lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)" ``` lars@66269 ` 983` ```unfolding fmfilter_alt_defs by simp ``` lars@66269 ` 984` lars@66269 ` 985` ```lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)" ``` lars@66269 ` 986` ```unfolding fmfilter_alt_defs by simp ``` lars@66269 ` 987` lars@66269 ` 988` ```lemma fmmap_keys_subset[intro]: "m \\<^sub>f n \ fmmap_keys f m \\<^sub>f fmmap_keys f n" ``` lars@66269 ` 989` ```by transfer' (auto simp: map_le_def dom_def) ``` lars@66269 ` 990` lars@66269 ` 991` lars@66269 ` 992` ```subsection \Lifting/transfer setup\ ``` lars@66269 ` 993` lars@66269 ` 994` ```context includes lifting_syntax begin ``` lars@66269 ` 995` lars@66269 ` 996` ```lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty" ``` lars@66269 ` 997` ```by transfer auto ``` lars@66269 ` 998` lars@66269 ` 999` ```lemma fmadd_transfer[transfer_rule]: ``` lars@66269 ` 1000` ``` "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd" ``` lars@66269 ` 1001` ``` by (intro fmrel_addI rel_funI) ``` lars@66269 ` 1002` lars@66269 ` 1003` ```lemma fmupd_transfer[transfer_rule]: ``` nipkow@67399 ` 1004` ``` "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd" ``` lars@66269 ` 1005` ``` by auto ``` lars@66269 ` 1006` lars@66269 ` 1007` ```end ``` lars@66269 ` 1008` lars@66274 ` 1009` lars@66274 ` 1010` ```subsection \View as datatype\ ``` lars@66274 ` 1011` lars@66274 ` 1012` ```lemma fmap_distinct[simp]: ``` lars@66274 ` 1013` ``` "fmempty \ fmupd k v m" ``` lars@66274 ` 1014` ``` "fmupd k v m \ fmempty" ``` lars@66274 ` 1015` ```by (transfer'; auto simp: map_upd_def fun_eq_iff)+ ``` lars@66274 ` 1016` lars@66274 ` 1017` ```lifting_update fmap.lifting ``` lars@66274 ` 1018` lars@66274 ` 1019` ```lemma fmap_exhaust[case_names fmempty fmupd, cases type: fmap]: ``` lars@66274 ` 1020` ``` assumes fmempty: "m = fmempty \ P" ``` lars@66274 ` 1021` ``` assumes fmupd: "\x y m'. m = fmupd x y m' \ x |\| fmdom m' \ P" ``` lars@66274 ` 1022` ``` shows "P" ``` lars@66274 ` 1023` ```using assms including fmap.lifting fset.lifting ``` lars@66274 ` 1024` ```proof transfer ``` lars@66274 ` 1025` ``` fix m P ``` lars@66274 ` 1026` ``` assume "finite (dom m)" ``` lars@66274 ` 1027` ``` assume empty: P if "m = Map.empty" ``` lars@66274 ` 1028` ``` assume map_upd: P if "finite (dom m')" "m = map_upd x y m'" "x \ dom m'" for x y m' ``` lars@66274 ` 1029` lars@66274 ` 1030` ``` show P ``` lars@66274 ` 1031` ``` proof (cases "m = Map.empty") ``` lars@66274 ` 1032` ``` case True thus ?thesis using empty by simp ``` lars@66274 ` 1033` ``` next ``` lars@66274 ` 1034` ``` case False ``` lars@66274 ` 1035` ``` hence "dom m \ {}" by simp ``` lars@66274 ` 1036` ``` then obtain x where "x \ dom m" by blast ``` lars@66274 ` 1037` lars@66274 ` 1038` ``` let ?m' = "map_drop x m" ``` lars@66274 ` 1039` lars@66274 ` 1040` ``` show ?thesis ``` lars@66274 ` 1041` ``` proof (rule map_upd) ``` lars@66274 ` 1042` ``` show "finite (dom ?m')" ``` lars@66274 ` 1043` ``` using \finite (dom m)\ ``` lars@66274 ` 1044` ``` unfolding map_drop_def ``` lars@66274 ` 1045` ``` by auto ``` lars@66274 ` 1046` ``` next ``` lars@66274 ` 1047` ``` show "m = map_upd x (the (m x)) ?m'" ``` lars@66274 ` 1048` ``` using \x \ dom m\ unfolding map_drop_def map_filter_def map_upd_def ``` lars@66274 ` 1049` ``` by auto ``` lars@66274 ` 1050` ``` next ``` lars@66274 ` 1051` ``` show "x \ dom ?m'" ``` lars@66274 ` 1052` ``` unfolding map_drop_def map_filter_def ``` lars@66274 ` 1053` ``` by auto ``` lars@66274 ` 1054` ``` qed ``` lars@66274 ` 1055` ``` qed ``` lars@66274 ` 1056` ```qed ``` lars@66274 ` 1057` lars@66274 ` 1058` ```lemma fmap_induct[case_names fmempty fmupd, induct type: fmap]: ``` lars@66274 ` 1059` ``` assumes "P fmempty" ``` lars@66274 ` 1060` ``` assumes "(\x y m. P m \ fmlookup m x = None \ P (fmupd x y m))" ``` lars@66274 ` 1061` ``` shows "P m" ``` lars@66274 ` 1062` ```proof (induction "fmdom m" arbitrary: m rule: fset_induct_stronger) ``` lars@66274 ` 1063` ``` case empty ``` lars@66274 ` 1064` ``` hence "m = fmempty" ``` lars@66274 ` 1065` ``` by (metis fmrestrict_fset_dom fmrestrict_fset_null) ``` lars@66274 ` 1066` ``` with assms show ?case ``` lars@66274 ` 1067` ``` by simp ``` lars@66274 ` 1068` ```next ``` lars@66274 ` 1069` ``` case (insert x S) ``` lars@66274 ` 1070` ``` hence "S = fmdom (fmdrop x m)" ``` lars@66274 ` 1071` ``` by auto ``` lars@66274 ` 1072` ``` with insert have "P (fmdrop x m)" ``` lars@66274 ` 1073` ``` by auto ``` lars@66274 ` 1074` lars@66274 ` 1075` ``` have "x |\| fmdom m" ``` lars@66274 ` 1076` ``` using insert by auto ``` lars@66274 ` 1077` ``` then obtain y where "fmlookup m x = Some y" ``` lars@66274 ` 1078` ``` by auto ``` lars@66274 ` 1079` ``` hence "m = fmupd x y (fmdrop x m)" ``` lars@66274 ` 1080` ``` by (auto intro: fmap_ext) ``` lars@66274 ` 1081` lars@66274 ` 1082` ``` show ?case ``` lars@66274 ` 1083` ``` apply (subst \m = _\) ``` lars@66274 ` 1084` ``` apply (rule assms) ``` lars@66274 ` 1085` ``` apply fact ``` lars@66274 ` 1086` ``` apply simp ``` lars@66274 ` 1087` ``` done ``` lars@66274 ` 1088` ```qed ``` lars@66274 ` 1089` lars@66274 ` 1090` lars@63885 ` 1091` ```subsection \Code setup\ ``` lars@63885 ` 1092` lars@63885 ` 1093` ```instantiation fmap :: (type, equal) equal begin ``` lars@63885 ` 1094` lars@63885 ` 1095` ```definition "equal_fmap \ fmrel HOL.equal" ``` lars@63885 ` 1096` lars@63885 ` 1097` ```instance proof ``` lars@63885 ` 1098` ``` fix m n :: "('a, 'b) fmap" ``` nipkow@67399 ` 1099` ``` have "fmrel (=) m n \ (m = n)" ``` lars@63885 ` 1100` ``` by transfer' (simp add: option.rel_eq rel_fun_eq) ``` lars@64180 ` 1101` ``` then show "equal_class.equal m n \ (m = n)" ``` lars@63885 ` 1102` ``` unfolding equal_fmap_def ``` lars@63885 ` 1103` ``` by (simp add: equal_eq[abs_def]) ``` lars@63885 ` 1104` ```qed ``` lars@63885 ` 1105` lars@63885 ` 1106` ```end ``` lars@63885 ` 1107` lars@63885 ` 1108` ```lemma fBall_alt_def: "fBall S P \ (\x. x |\| S \ P x)" ``` lars@63885 ` 1109` ```by force ``` lars@63885 ` 1110` lars@63885 ` 1111` ```lemma fmrel_code: ``` lars@63885 ` 1112` ``` "fmrel R m n \ ``` lars@63885 ` 1113` ``` fBall (fmdom m) (\x. rel_option R (fmlookup m x) (fmlookup n x)) \ ``` lars@63885 ` 1114` ``` fBall (fmdom n) (\x. rel_option R (fmlookup m x) (fmlookup n x))" ``` lars@63885 ` 1115` ```unfolding fmrel_iff fmlookup_dom_iff fBall_alt_def ``` lars@63885 ` 1116` ```by (metis option.collapse option.rel_sel) ``` lars@63885 ` 1117` lars@66291 ` 1118` ```lemmas [code] = ``` lars@63885 ` 1119` ``` fmrel_code ``` lars@63885 ` 1120` ``` fmran'_alt_def ``` lars@63885 ` 1121` ``` fmdom'_alt_def ``` lars@63885 ` 1122` ``` fmfilter_alt_defs ``` lars@63885 ` 1123` ``` pred_fmap_fmpred ``` lars@63885 ` 1124` ``` fmsubset_alt_def ``` lars@63885 ` 1125` ``` fmupd_alt_def ``` lars@63885 ` 1126` ``` fmrel_on_fset_alt_def ``` lars@63885 ` 1127` ``` fmpred_alt_def ``` lars@63885 ` 1128` lars@63885 ` 1129` lars@63885 ` 1130` ```code_datatype fmap_of_list ``` lars@63885 ` 1131` ```quickcheck_generator fmap constructors: fmap_of_list ``` lars@63885 ` 1132` lars@63885 ` 1133` ```context includes fset.lifting begin ``` lars@63885 ` 1134` lars@66269 ` 1135` ```lemma fmlookup_of_list[code]: "fmlookup (fmap_of_list m) = map_of m" ``` lars@63885 ` 1136` ```by transfer simp ``` lars@63885 ` 1137` lars@66269 ` 1138` ```lemma fmempty_of_list[code]: "fmempty = fmap_of_list []" ``` lars@63885 ` 1139` ```by transfer simp ``` lars@63885 ` 1140` lars@66269 ` 1141` ```lemma fmran_of_list[code]: "fmran (fmap_of_list m) = snd |`| fset_of_list (AList.clearjunk m)" ``` lars@63885 ` 1142` ```by transfer (auto simp: ran_map_of) ``` lars@63885 ` 1143` lars@66269 ` 1144` ```lemma fmdom_of_list[code]: "fmdom (fmap_of_list m) = fst |`| fset_of_list m" ``` lars@63885 ` 1145` ```by transfer (auto simp: dom_map_of_conv_image_fst) ``` lars@63885 ` 1146` lars@66269 ` 1147` ```lemma fmfilter_of_list[code]: "fmfilter P (fmap_of_list m) = fmap_of_list (filter (\(k, _). P k) m)" ``` lars@63885 ` 1148` ```by transfer' auto ``` lars@63885 ` 1149` lars@66269 ` 1150` ```lemma fmadd_of_list[code]: "fmap_of_list m ++\<^sub>f fmap_of_list n = fmap_of_list (AList.merge m n)" ``` lars@63885 ` 1151` ```by transfer (simp add: merge_conv') ``` lars@63885 ` 1152` lars@66269 ` 1153` ```lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)" ``` lars@63885 ` 1154` ```apply transfer ``` lars@63885 ` 1155` ```apply (subst map_of_map[symmetric]) ``` lars@63885 ` 1156` ```apply (auto simp: apsnd_def map_prod_def) ``` lars@63885 ` 1157` ```done ``` lars@63885 ` 1158` lars@66269 ` 1159` ```lemma fmmap_keys_of_list[code]: "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\(a, b). (a, f a b)) m)" ``` lars@66269 ` 1160` ```apply transfer ``` lars@66269 ` 1161` ```subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff) ``` lars@66269 ` 1162` ```done ``` lars@66269 ` 1163` lars@63885 ` 1164` ```end ``` lars@63885 ` 1165` lars@66267 ` 1166` lars@66267 ` 1167` ```subsection \Instances\ ``` lars@66267 ` 1168` lars@66267 ` 1169` ```lemma exists_map_of: ``` lars@66267 ` 1170` ``` assumes "finite (dom m)" shows "\xs. map_of xs = m" ``` lars@66267 ` 1171` ``` using assms ``` lars@66267 ` 1172` ```proof (induction "dom m" arbitrary: m) ``` lars@66267 ` 1173` ``` case empty ``` lars@66267 ` 1174` ``` hence "m = Map.empty" ``` lars@66267 ` 1175` ``` by auto ``` lars@66267 ` 1176` ``` moreover have "map_of [] = Map.empty" ``` lars@66267 ` 1177` ``` by simp ``` lars@66267 ` 1178` ``` ultimately show ?case ``` lars@66267 ` 1179` ``` by blast ``` lars@66267 ` 1180` ```next ``` lars@66267 ` 1181` ``` case (insert x F) ``` lars@66267 ` 1182` ``` hence "F = dom (map_drop x m)" ``` lars@66267 ` 1183` ``` unfolding map_drop_def map_filter_def dom_def by auto ``` lars@66267 ` 1184` ``` with insert have "\xs'. map_of xs' = map_drop x m" ``` lars@66267 ` 1185` ``` by auto ``` lars@66267 ` 1186` ``` then obtain xs' where "map_of xs' = map_drop x m" ``` lars@66267 ` 1187` ``` .. ``` lars@66267 ` 1188` ``` moreover obtain y where "m x = Some y" ``` lars@66267 ` 1189` ``` using insert unfolding dom_def by blast ``` lars@66267 ` 1190` ``` ultimately have "map_of ((x, y) # xs') = m" ``` lars@66267 ` 1191` ``` using \insert x F = dom m\ ``` lars@66267 ` 1192` ``` unfolding map_drop_def map_filter_def ``` lars@66267 ` 1193` ``` by auto ``` lars@66267 ` 1194` ``` thus ?case ``` lars@66267 ` 1195` ``` .. ``` lars@66267 ` 1196` ```qed ``` lars@66267 ` 1197` lars@66267 ` 1198` ```lemma exists_fmap_of_list: "\xs. fmap_of_list xs = m" ``` lars@66267 ` 1199` ```by transfer (rule exists_map_of) ``` lars@66267 ` 1200` lars@66267 ` 1201` ```lemma fmap_of_list_surj[simp, intro]: "surj fmap_of_list" ``` lars@66267 ` 1202` ```proof - ``` lars@66267 ` 1203` ``` have "x \ range fmap_of_list" for x :: "('a, 'b) fmap" ``` lars@66267 ` 1204` ``` unfolding image_iff ``` lars@66267 ` 1205` ``` using exists_fmap_of_list by (metis UNIV_I) ``` lars@66267 ` 1206` ``` thus ?thesis by auto ``` lars@66267 ` 1207` ```qed ``` lars@66267 ` 1208` lars@66267 ` 1209` ```instance fmap :: (countable, countable) countable ``` lars@66267 ` 1210` ```proof ``` lars@66267 ` 1211` ``` obtain to_nat :: "('a \ 'b) list \ nat" where "inj to_nat" ``` lars@66267 ` 1212` ``` by (metis ex_inj) ``` lars@66267 ` 1213` ``` moreover have "inj (inv fmap_of_list)" ``` lars@66267 ` 1214` ``` using fmap_of_list_surj by (rule surj_imp_inj_inv) ``` lars@66267 ` 1215` ``` ultimately have "inj (to_nat \ inv fmap_of_list)" ``` lars@66267 ` 1216` ``` by (rule inj_comp) ``` lars@66267 ` 1217` ``` thus "\to_nat::('a, 'b) fmap \ nat. inj to_nat" ``` lars@66267 ` 1218` ``` by auto ``` lars@66267 ` 1219` ```qed ``` lars@66267 ` 1220` lars@66282 ` 1221` ```instance fmap :: (finite, finite) finite ``` lars@66282 ` 1222` ```proof ``` lars@66282 ` 1223` ``` show "finite (UNIV :: ('a, 'b) fmap set)" ``` lars@66282 ` 1224` ``` by (rule finite_imageD) auto ``` lars@66282 ` 1225` ```qed ``` lars@66282 ` 1226` lars@63885 ` 1227` ```lifting_update fmap.lifting ``` lars@63885 ` 1228` ```lifting_forget fmap.lifting ``` lars@63885 ` 1229` lars@67485 ` 1230` `end`