1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Author: Rafal Kolanski, 2008 8 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 9 Rafal Kolanski <rafal.kolanski at nicta.com.au> 10*) 11 12chapter \<open>More properties of maps plus map disjuction.\<close> 13 14theory Map_Extra 15imports Main 16begin 17 18text \<open> 19 A note on naming: 20 Anything not involving heap disjuction can potentially be incorporated 21 directly into Map.thy, thus uses @{text "m"} for map variable names. 22 Anything involving heap disjunction is not really mergeable with Map, is 23 destined for use in separation logic, and hence uses @{text "h"} 24\<close> 25 26section \<open>Things that could go into Option Type\<close> 27 28text \<open>Misc option lemmas\<close> 29 30lemma None_not_eq: "(None \<noteq> x) = (\<exists>y. x = Some y)" by (cases x) auto 31 32lemma None_com: "(None = x) = (x = None)" by fast 33 34lemma Some_com: "(Some y = x) = (x = Some y)" by fast 35 36 37section \<open>Things that go into Map.thy\<close> 38 39text \<open>Map intersection: set of all keys for which the maps agree.\<close> 40 41definition 42 map_inter :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" (infixl "\<inter>\<^sub>m" 70) where 43 "m\<^sub>1 \<inter>\<^sub>m m\<^sub>2 \<equiv> {x \<in> dom m\<^sub>1. m\<^sub>1 x = m\<^sub>2 x}" 44 45text \<open>Map restriction via domain subtraction\<close> 46 47definition 48 sub_restrict_map :: "('a \<rightharpoonup> 'b) => 'a set => ('a \<rightharpoonup> 'b)" (infixl "`-" 110) 49 where 50 "m `- S \<equiv> (\<lambda>x. if x \<in> S then None else m x)" 51 52 53subsection \<open>Properties of maps not related to restriction\<close> 54 55lemma empty_forall_equiv: "(m = Map.empty) = (\<forall>x. m x = None)" 56 by (rule fun_eq_iff) 57 58lemma map_le_empty2 [simp]: 59 "(m \<subseteq>\<^sub>m Map.empty) = (m = Map.empty)" 60 by (auto simp: map_le_def) 61 62lemma dom_iff: 63 "(\<exists>y. m x = Some y) = (x \<in> dom m)" 64 by auto 65 66lemma non_dom_eval: 67 "x \<notin> dom m \<Longrightarrow> m x = None" 68 by auto 69 70lemma non_dom_eval_eq: 71 "x \<notin> dom m = (m x = None)" 72 by auto 73 74lemma map_add_same_left_eq: 75 "m\<^sub>1 = m\<^sub>1' \<Longrightarrow> (m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0 ++ m\<^sub>1')" 76 by simp 77 78lemma map_add_left_cancelI [intro!]: 79 "m\<^sub>1 = m\<^sub>1' \<Longrightarrow> m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0 ++ m\<^sub>1'" 80 by simp 81 82lemma dom_empty_is_empty: 83 "(dom m = {}) = (m = Map.empty)" 84proof (rule iffI) 85 assume a: "dom m = {}" 86 { assume "m \<noteq> Map.empty" 87 hence "dom m \<noteq> {}" 88 by - (subst (asm) empty_forall_equiv, simp add: dom_def) 89 hence False using a by blast 90 } 91 thus "m = Map.empty" by blast 92next 93 assume a: "m = Map.empty" 94 thus "dom m = {}" by simp 95qed 96 97lemma map_add_dom_eq: 98 "dom m = dom m' \<Longrightarrow> m ++ m' = m'" 99 by (rule ext) (auto simp: map_add_def split: option.splits) 100 101lemma map_add_right_dom_eq: 102 "\<lbrakk> m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0' ++ m\<^sub>1'; dom m\<^sub>1 = dom m\<^sub>1' \<rbrakk> \<Longrightarrow> m\<^sub>1 = m\<^sub>1'" 103 unfolding map_add_def 104 by (rule ext, rule ccontr, 105 drule_tac x=x in fun_cong, clarsimp split: option.splits, 106 drule sym, drule sym, force+) 107 108lemma map_le_same_dom_eq: 109 "\<lbrakk> m\<^sub>0 \<subseteq>\<^sub>m m\<^sub>1 ; dom m\<^sub>0 = dom m\<^sub>1 \<rbrakk> \<Longrightarrow> m\<^sub>0 = m\<^sub>1" 110 by (simp add: map_le_antisym map_le_def) 111 112 113subsection \<open>Properties of map restriction\<close> 114 115lemma restrict_map_cancel: 116 "(m |` S = m |` T) = (dom m \<inter> S = dom m \<inter> T)" 117 by (fastforce dest: fun_cong simp: restrict_map_def None_not_eq split: if_split_asm) 118 119lemma map_add_restricted_self [simp]: 120 "m ++ m |` S = m" 121 by (auto simp: restrict_map_def map_add_def split: option.splits) 122 123lemma map_add_restrict_dom_right [simp]: 124 "(m ++ m') |` dom m' = m'" 125 by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits) 126 127lemma restrict_map_UNIV [simp]: 128 "m |` UNIV = m" 129 by (simp add: restrict_map_def) 130 131lemma restrict_map_dom: 132 "S = dom m \<Longrightarrow> m |` S = m" 133 by (rule ext, auto simp: restrict_map_def None_not_eq) 134 135lemma restrict_map_subdom: 136 "dom m \<subseteq> S \<Longrightarrow> m |` S = m" 137 by (fastforce simp: restrict_map_def None_com) 138 139lemma map_add_restrict: 140 "(m\<^sub>0 ++ m\<^sub>1) |` S = ((m\<^sub>0 |` S) ++ (m\<^sub>1 |` S))" 141 by (force simp: map_add_def restrict_map_def) 142 143lemma map_le_restrict: 144 "m \<subseteq>\<^sub>m m' \<Longrightarrow> m = m' |` dom m" 145 by (force simp: map_le_def restrict_map_def None_com) 146 147lemma restrict_map_le: 148 "m |` S \<subseteq>\<^sub>m m" 149 by (auto simp: map_le_def) 150 151lemma restrict_map_remerge: 152 "\<lbrakk> S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m |` (S \<union> T)" 153 by (rule ext, clarsimp simp: restrict_map_def map_add_def 154 split: option.splits) 155 156lemma restrict_map_empty: 157 "dom m \<inter> S = {} \<Longrightarrow> m |` S = Map.empty" 158 by (fastforce simp: restrict_map_def) 159 160lemma map_add_restrict_comp_right [simp]: 161 "(m |` S ++ m |` (UNIV - S)) = m" 162 by (force simp: map_add_def restrict_map_def split: option.splits) 163 164lemma map_add_restrict_comp_right_dom [simp]: 165 "(m |` S ++ m |` (dom m - S)) = m" 166 by (rule ext, auto simp: map_add_def restrict_map_def split: option.splits) 167 168lemma map_add_restrict_comp_left [simp]: 169 "(m |` (UNIV - S) ++ m |` S) = m" 170 by (subst map_add_comm, auto) 171 172lemma restrict_self_UNIV: 173 "m |` (dom m - S) = m |` (UNIV - S)" 174 by (rule ext, auto simp: restrict_map_def) 175 176lemma map_add_restrict_nonmember_right: 177 "x \<notin> dom m' \<Longrightarrow> (m ++ m') |` {x} = m |` {x}" 178 by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits) 179 180lemma map_add_restrict_nonmember_left: 181 "x \<notin> dom m \<Longrightarrow> (m ++ m') |` {x} = m' |` {x}" 182 by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits) 183 184lemma map_add_restrict_right: 185 "x \<subseteq> dom m' \<Longrightarrow> (m ++ m') |` x = m' |` x" 186 by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits) 187 188lemma restrict_map_compose: 189 "\<lbrakk> S \<union> T = dom m ; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m" 190 by (fastforce simp: map_add_def restrict_map_def) 191 192lemma map_le_dom_subset_restrict: 193 "\<lbrakk> m' \<subseteq>\<^sub>m m; dom m' \<subseteq> S \<rbrakk> \<Longrightarrow> m' \<subseteq>\<^sub>m (m |` S)" 194 by (force simp: restrict_map_def map_le_def) 195 196lemma map_le_dom_restrict_sub_add: 197 "m' \<subseteq>\<^sub>m m \<Longrightarrow> m |` (dom m - dom m') ++ m' = m" 198 by (rule ext, auto simp: None_com map_add_def restrict_map_def map_le_def 199 split: option.splits; force simp: Some_com) 200 201lemma subset_map_restrict_sub_add: 202 "T \<subseteq> S \<Longrightarrow> m |` (S - T) ++ m |` T = m |` S" 203 by (rule ext) (auto simp: restrict_map_def map_add_def split: option.splits) 204 205lemma restrict_map_sub_union: 206 "m |` (dom m - (S \<union> T)) = (m |` (dom m - T)) |` (dom m - S)" 207 by (auto simp: restrict_map_def) 208 209lemma prod_restrict_map_add: 210 "\<lbrakk> S \<union> T = U; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` (X \<times> S) ++ m |` (X \<times> T) = m |` (X \<times> U)" 211 by (auto simp: map_add_def restrict_map_def split: option.splits) 212 213 214section \<open>Things that should not go into Map.thy (separation logic)\<close> 215 216subsection \<open>Definitions\<close> 217 218text \<open>Map disjuction\<close> 219 220definition 221 map_disj :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<bottom>" 51) where 222 "h\<^sub>0 \<bottom> h\<^sub>1 \<equiv> dom h\<^sub>0 \<inter> dom h\<^sub>1 = {}" 223 224declare None_not_eq [simp] 225 226 227subsection \<open>Properties of @{term "sub_restrict_map"}\<close> 228 229lemma restrict_map_sub_disj: "h |` S \<bottom> h `- S" 230 by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def 231 split: option.splits if_split_asm) 232 233lemma restrict_map_sub_add: "h |` S ++ h `- S = h" 234 by (fastforce simp: sub_restrict_map_def restrict_map_def map_add_def 235 split: option.splits if_split) 236 237 238subsection \<open>Properties of map disjunction\<close> 239 240lemma map_disj_empty_right [simp]: 241 "h \<bottom> Map.empty" 242 by (simp add: map_disj_def) 243 244lemma map_disj_empty_left [simp]: 245 "Map.empty \<bottom> h" 246 by (simp add: map_disj_def) 247 248lemma map_disj_com: 249 "h\<^sub>0 \<bottom> h\<^sub>1 = h\<^sub>1 \<bottom> h\<^sub>0" 250 by (simp add: map_disj_def, fast) 251 252lemma map_disjD: 253 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> dom h\<^sub>0 \<inter> dom h\<^sub>1 = {}" 254 by (simp add: map_disj_def) 255 256lemma map_disjI: 257 "dom h\<^sub>0 \<inter> dom h\<^sub>1 = {} \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1" 258 by (simp add: map_disj_def) 259 260 261subsection \<open>Map associativity-commutativity based on map disjuction\<close> 262 263lemma map_add_com: 264 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>1 ++ h\<^sub>0" 265 by (drule map_disjD, rule map_add_comm, force) 266 267lemma map_add_left_commute: 268 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 ++ (h\<^sub>1 ++ h\<^sub>2) = h\<^sub>1 ++ (h\<^sub>0 ++ h\<^sub>2)" 269 by (simp add: map_add_com map_disj_com) 270 271lemma map_add_disj: 272 "h\<^sub>0 \<bottom> (h\<^sub>1 ++ h\<^sub>2) = (h\<^sub>0 \<bottom> h\<^sub>1 \<and> h\<^sub>0 \<bottom> h\<^sub>2)" 273 by (simp add: map_disj_def, fast) 274 275lemma map_add_disj': 276 "(h\<^sub>1 ++ h\<^sub>2) \<bottom> h\<^sub>0 = (h\<^sub>1 \<bottom> h\<^sub>0 \<and> h\<^sub>2 \<bottom> h\<^sub>0)" 277 by (simp add: map_disj_def, fast) 278 279text \<open> 280 We redefine @{term "map_add"} associativity to bind to the right, which 281 seems to be the more common case. 282 Note that when a theory includes Map again, @{text "map_add_assoc"} will 283 return to the simpset and will cause infinite loops if its symmetric 284 counterpart is added (e.g. via @{text "map_add_ac"}) 285\<close> 286 287declare map_add_assoc [simp del] 288 289text \<open> 290 Since the associativity-commutativity of @{term "map_add"} relies on 291 map disjunction, we include some basic rules into the ac set. 292\<close> 293 294lemmas map_add_ac = 295 map_add_assoc[symmetric] map_add_com map_disj_com 296 map_add_left_commute map_add_disj map_add_disj' 297 298 299subsection \<open>Basic properties\<close> 300 301lemma map_disj_None_right: 302 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; x \<in> dom h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>1 x = None" 303 by (auto simp: map_disj_def dom_def) 304 305lemma map_disj_None_left: 306 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; x \<in> dom h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 x = None" 307 by (auto simp: map_disj_def dom_def) 308 309lemma map_disj_None_left': 310 "\<lbrakk> h\<^sub>0 x = Some y ; h\<^sub>1 \<bottom> h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>1 x = None " 311 by (auto simp: map_disj_def) 312 313lemma map_disj_None_right': 314 "\<lbrakk> h\<^sub>1 x = Some y ; h\<^sub>1 \<bottom> h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0 x = None " 315 by (auto simp: map_disj_def) 316 317lemma map_disj_common: 318 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; h\<^sub>0 p = Some v ; h\<^sub>1 p = Some v' \<rbrakk> \<Longrightarrow> False" 319 by (frule (1) map_disj_None_left', simp) 320 321lemma map_disj_eq_dom_left: 322 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; dom h\<^sub>0' = dom h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0' \<bottom> h\<^sub>1" 323 by (auto simp: map_disj_def) 324 325 326subsection \<open>Map disjunction and addition\<close> 327 328lemma map_add_eval_left: 329 "\<lbrakk> x \<in> dom h ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x" 330 by (auto dest!: map_disj_None_right simp: map_add_def cong: option.case_cong) 331 332lemma map_add_eval_right: 333 "\<lbrakk> x \<in> dom h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x" 334 by (rule map_add_dom_app_simps) 335 336lemma map_add_eval_left': 337 "\<lbrakk> x \<notin> dom h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x" 338 by (rule map_add_dom_app_simps) 339 340lemma map_add_eval_right': 341 "\<lbrakk> x \<notin> dom h \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x" 342 by (rule map_add_dom_app_simps) 343 344lemma map_add_left_dom_eq: 345 assumes eq: "h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'" 346 assumes etc: "h\<^sub>0 \<bottom> h\<^sub>1" "h\<^sub>0' \<bottom> h\<^sub>1'" "dom h\<^sub>0 = dom h\<^sub>0'" 347 shows "h\<^sub>0 = h\<^sub>0'" 348proof - 349 from eq have "h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'" using etc by (simp add: map_add_ac) 350 thus ?thesis using etc 351 by (fastforce elim!: map_add_right_dom_eq simp: map_add_ac) 352qed 353 354lemma map_add_left_eq: 355 assumes eq: "h\<^sub>0 ++ h = h\<^sub>1 ++ h" 356 assumes disj: "h\<^sub>0 \<bottom> h" "h\<^sub>1 \<bottom> h" 357 shows "h\<^sub>0 = h\<^sub>1" 358proof (rule ext) 359 fix x 360 from eq have eq': "(h\<^sub>0 ++ h) x = (h\<^sub>1 ++ h) x" by auto 361 { assume "x \<in> dom h" 362 hence "h\<^sub>0 x = h\<^sub>1 x" using disj by (simp add: map_disj_None_left) 363 } moreover { 364 assume "x \<notin> dom h" 365 hence "h\<^sub>0 x = h\<^sub>1 x" using disj eq' by (simp add: map_add_eval_left') 366 } 367 ultimately show "h\<^sub>0 x = h\<^sub>1 x" by cases 368qed 369 370lemma map_add_right_eq: 371 "\<lbrakk>h ++ h\<^sub>0 = h ++ h\<^sub>1; h\<^sub>0 \<bottom> h; h\<^sub>1 \<bottom> h\<rbrakk> \<Longrightarrow> h\<^sub>0 = h\<^sub>1" 372 by (rule_tac h=h in map_add_left_eq, auto simp: map_add_ac) 373 374lemma map_disj_add_eq_dom_right_eq: 375 assumes merge: "h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'" and d: "dom h\<^sub>0 = dom h\<^sub>0'" and 376 ab_disj: "h\<^sub>0 \<bottom> h\<^sub>1" and cd_disj: "h\<^sub>0' \<bottom> h\<^sub>1'" 377 shows "h\<^sub>1 = h\<^sub>1'" 378proof (rule ext) 379 fix x 380 from merge have merge_x: "(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0' ++ h\<^sub>1') x" by simp 381 with d ab_disj cd_disj show "h\<^sub>1 x = h\<^sub>1' x" 382 by - (case_tac "h\<^sub>1 x", case_tac "h\<^sub>1' x", simp, fastforce simp: map_disj_def, 383 case_tac "h\<^sub>1' x", clarsimp, simp add: Some_com, 384 force simp: map_disj_def, simp) 385qed 386 387lemma map_disj_add_eq_dom_left_eq: 388 assumes add: "h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'" and 389 dom: "dom h\<^sub>1 = dom h\<^sub>1'" and 390 disj: "h\<^sub>0 \<bottom> h\<^sub>1" "h\<^sub>0' \<bottom> h\<^sub>1'" 391 shows "h\<^sub>0 = h\<^sub>0'" 392proof - 393 have "h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'" using add disj by (simp add: map_add_ac) 394 thus ?thesis using dom disj 395 by - (rule map_disj_add_eq_dom_right_eq, auto simp: map_disj_com) 396qed 397 398lemma map_add_left_cancel: 399 assumes disj: "h\<^sub>0 \<bottom> h\<^sub>1" "h\<^sub>0 \<bottom> h\<^sub>1'" 400 shows "(h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1') = (h\<^sub>1 = h\<^sub>1')" 401proof (rule iffI, rule ext) 402 fix x 403 assume "(h\<^sub>0 ++ h\<^sub>1) = (h\<^sub>0 ++ h\<^sub>1')" 404 hence "(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0 ++ h\<^sub>1') x" by auto 405 hence "h\<^sub>1 x = h\<^sub>1' x" using disj 406 by (cases "x \<in> dom h\<^sub>0"; simp add: map_disj_None_right map_add_eval_right') 407 thus "h\<^sub>1 x = h\<^sub>1' x" by auto 408qed auto 409 410lemma map_add_lr_disj: 411 "\<lbrakk> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'; h\<^sub>1 \<bottom> h\<^sub>1' \<rbrakk> \<Longrightarrow> dom h\<^sub>1 \<subseteq> dom h\<^sub>0'" 412 by (clarsimp simp: map_disj_def map_add_def, drule_tac x=x in fun_cong) 413 (auto split: option.splits) 414 415 416subsection \<open>Map disjunction and map updates\<close> 417 418lemma map_disj_update_left [simp]: 419 "p \<in> dom h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1(p \<mapsto> v) = h\<^sub>0 \<bottom> h\<^sub>1" 420 by (clarsimp simp: map_disj_def, blast) 421 422lemma map_disj_update_right [simp]: 423 "p \<in> dom h\<^sub>1 \<Longrightarrow> h\<^sub>1(p \<mapsto> v) \<bottom> h\<^sub>0 = h\<^sub>1 \<bottom> h\<^sub>0" 424 by (simp add: map_disj_com) 425 426lemma map_add_update_left: 427 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; p \<in> dom h\<^sub>0 \<rbrakk> \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1)(p \<mapsto> v) = (h\<^sub>0(p \<mapsto> v) ++ h\<^sub>1)" 428 by (drule (1) map_disj_None_right) 429 (auto simp: map_add_def cong: option.case_cong) 430 431lemma map_add_update_right: 432 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; p \<in> dom h\<^sub>1 \<rbrakk> \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1)(p \<mapsto> v) = (h\<^sub>0 ++ h\<^sub>1 (p \<mapsto> v))" 433 by (drule (1) map_disj_None_left) 434 (auto simp: map_add_def cong: option.case_cong) 435 436lemma map_add3_update: 437 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; h\<^sub>1 \<bottom> h\<^sub>2 ; h\<^sub>0 \<bottom> h\<^sub>2 ; p \<in> dom h\<^sub>0 \<rbrakk> 438 \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1 ++ h\<^sub>2)(p \<mapsto> v) = h\<^sub>0(p \<mapsto> v) ++ h\<^sub>1 ++ h\<^sub>2" 439 by (auto simp: map_add_update_left[symmetric] map_add_ac) 440 441 442subsection \<open>Map disjunction and @{term "map_le"}\<close> 443 444lemma map_le_override [simp]: 445 "\<lbrakk> h \<bottom> h' \<rbrakk> \<Longrightarrow> h \<subseteq>\<^sub>m h ++ h'" 446 by (auto simp: map_le_def map_add_def map_disj_def split: option.splits) 447 448lemma map_leI_left: 449 "\<lbrakk> h = h\<^sub>0 ++ h\<^sub>1 ; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h" by auto 450 451lemma map_leI_right: 452 "\<lbrakk> h = h\<^sub>0 ++ h\<^sub>1 ; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>1 \<subseteq>\<^sub>m h" by auto 453 454lemma map_disj_map_le: 455 "\<lbrakk> h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0' \<bottom> h\<^sub>1" 456 by (force simp: map_disj_def map_le_def) 457 458lemma map_le_on_disj_left: 459 "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^sub>0 \<bottom> h\<^sub>1 ; h' = h\<^sub>0 ++ h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h" 460 unfolding map_le_def 461 by (rule ballI, erule_tac x=a in ballE, auto simp: map_add_eval_left)+ 462 463lemma map_le_on_disj_right: 464 "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^sub>0 \<bottom> h\<^sub>1 ; h' = h\<^sub>1 ++ h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h" 465 by (auto simp: map_le_on_disj_left map_add_ac) 466 467lemma map_le_add_cancel: 468 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0' ++ h\<^sub>1 \<subseteq>\<^sub>m h\<^sub>0 ++ h\<^sub>1" 469 by (auto simp: map_le_def map_add_def map_disj_def split: option.splits) 470 471lemma map_le_override_bothD: 472 assumes subm: "h\<^sub>0' ++ h\<^sub>1 \<subseteq>\<^sub>m h\<^sub>0 ++ h\<^sub>1" 473 assumes disj': "h\<^sub>0' \<bottom> h\<^sub>1" 474 assumes disj: "h\<^sub>0 \<bottom> h\<^sub>1" 475 shows "h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0" 476unfolding map_le_def 477proof (rule ballI) 478 fix a 479 assume a: "a \<in> dom h\<^sub>0'" 480 hence sumeq: "(h\<^sub>0' ++ h\<^sub>1) a = (h\<^sub>0 ++ h\<^sub>1) a" 481 using subm unfolding map_le_def by auto 482 from a have "a \<notin> dom h\<^sub>1" using disj' by (auto dest!: map_disj_None_right) 483 thus "h\<^sub>0' a = h\<^sub>0 a" using a sumeq disj disj' 484 by (simp add: map_add_eval_left map_add_eval_left') 485qed 486 487lemma map_le_conv: 488 "(h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0 \<and> h\<^sub>0' \<noteq> h\<^sub>0) = (\<exists>h\<^sub>1. h\<^sub>0 = h\<^sub>0' ++ h\<^sub>1 \<and> h\<^sub>0' \<bottom> h\<^sub>1 \<and> h\<^sub>0' \<noteq> h\<^sub>0)" 489 unfolding map_le_def map_disj_def map_add_def 490 by (rule iffI, 491 clarsimp intro!: exI[where x="\<lambda>x. if x \<notin> dom h\<^sub>0' then h\<^sub>0 x else None"]) 492 (fastforce intro: split: option.splits if_split_asm)+ 493 494lemma map_le_conv2: 495 "h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0 = (\<exists>h\<^sub>1. h\<^sub>0 = h\<^sub>0' ++ h\<^sub>1 \<and> h\<^sub>0' \<bottom> h\<^sub>1)" 496 by (case_tac "h\<^sub>0'=h\<^sub>0", insert map_le_conv, auto intro: exI[where x=Map.empty]) 497 498 499subsection \<open>Map disjunction and restriction\<close> 500 501lemma map_disj_comp [simp]: 502 "h\<^sub>0 \<bottom> h\<^sub>1 |` (UNIV - dom h\<^sub>0)" 503 by (force simp: map_disj_def) 504 505lemma restrict_map_disj: 506 "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h |` T" 507 by (auto simp: map_disj_def restrict_map_def dom_def) 508 509lemma map_disj_restrict_dom [simp]: 510 "h\<^sub>0 \<bottom> h\<^sub>1 |` (dom h\<^sub>1 - dom h\<^sub>0)" 511 by (force simp: map_disj_def) 512 513lemma restrict_map_disj_dom_empty: 514 "h \<bottom> h' \<Longrightarrow> h |` dom h' = Map.empty" 515 by (fastforce simp: map_disj_def restrict_map_def) 516 517lemma restrict_map_univ_disj_eq: 518 "h \<bottom> h' \<Longrightarrow> h |` (UNIV - dom h') = h" 519 by (rule ext, auto simp: map_disj_def restrict_map_def) 520 521lemma restrict_map_disj_dom: 522 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h |` dom h\<^sub>0 \<bottom> h |` dom h\<^sub>1" 523 by (auto simp: map_disj_def restrict_map_def dom_def) 524 525lemma map_add_restrict_dom_left: 526 "h \<bottom> h' \<Longrightarrow> (h ++ h') |` dom h = h" 527 by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def 528 split: option.splits) 529 530lemma map_add_restrict_dom_left': 531 "h \<bottom> h' \<Longrightarrow> S = dom h \<Longrightarrow> (h ++ h') |` S = h" 532 by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def 533 split: option.splits) 534 535lemma restrict_map_disj_left: 536 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 |` S \<bottom> h\<^sub>1" 537 by (auto simp: map_disj_def) 538 539lemma restrict_map_disj_right: 540 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1 |` S" 541 by (auto simp: map_disj_def) 542 543lemmas restrict_map_disj_both = restrict_map_disj_right restrict_map_disj_left 544 545lemma map_dom_disj_restrict_right: 546 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>0') |` dom h\<^sub>1 = h\<^sub>0' |` dom h\<^sub>1" 547 by (simp add: map_add_restrict restrict_map_empty map_disj_def) 548 549lemma restrict_map_on_disj: 550 "h\<^sub>0' \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 |` dom h\<^sub>0' \<bottom> h\<^sub>1" 551 unfolding map_disj_def by auto 552 553lemma restrict_map_on_disj': 554 "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1 |` S" 555 by (rule restrict_map_disj_right) 556 557lemma map_le_sub_dom: 558 "\<lbrakk> h\<^sub>0 ++ h\<^sub>1 \<subseteq>\<^sub>m h ; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h |` (dom h - dom h\<^sub>1)" 559 by (rule map_le_override_bothD, subst map_le_dom_restrict_sub_add) 560 (auto elim: map_add_le_mapE simp: map_add_ac) 561 562lemma map_submap_break: 563 "\<lbrakk> h \<subseteq>\<^sub>m h' \<rbrakk> \<Longrightarrow> h' = (h' |` (UNIV - dom h)) ++ h" 564 by (fastforce split: option.splits 565 simp: map_le_restrict restrict_map_def map_le_def map_add_def 566 dom_def) 567 568lemma map_add_disj_restrict_both: 569 "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1; S \<inter> S' = {}; T \<inter> T' = {} \<rbrakk> 570 \<Longrightarrow> (h\<^sub>0 |` S) ++ (h\<^sub>1 |` T) \<bottom> (h\<^sub>0 |` S') ++ (h\<^sub>1 |` T')" 571 by (auto simp: map_add_ac intro!: restrict_map_disj_both restrict_map_disj) 572 573end 574