1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Authors: Gerwin Klein and Rafal Kolanski, 2012 8 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 9 Rafal Kolanski <rafal.kolanski at nicta.com.au> 10*) 11 12chapter "Abstract Separation Algebra" 13 14theory Separation_Algebra 15imports 16 Arbitrary_Comm_Monoid 17 "HOL-Library.Adhoc_Overloading" 18begin 19 20text \<open>This theory is the main abstract separation algebra development\<close> 21 22 23section \<open>Input syntax for lifting boolean predicates to separation predicates\<close> 24 25abbreviation (input) 26 pred_and :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "and" 35) where 27 "a and b \<equiv> \<lambda>s. a s \<and> b s" 28 29abbreviation (input) 30 pred_or :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "or" 30) where 31 "a or b \<equiv> \<lambda>s. a s \<or> b s" 32 33abbreviation (input) 34 pred_not :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" ("not _" [40] 40) where 35 "not a \<equiv> \<lambda>s. \<not>a s" 36 37abbreviation (input) 38 pred_imp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "imp" 25) where 39 "a imp b \<equiv> \<lambda>s. a s \<longrightarrow> b s" 40 41abbreviation (input) 42 pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where 43 "\<langle>f\<rangle> \<equiv> \<lambda>s. f" 44 45abbreviation (input) 46 pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where 47 "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s" 48 49abbreviation (input) 50 pred_all :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "ALLS " 10) where 51 "ALLS x. P x \<equiv> \<lambda>s. \<forall>x. P x s" 52 53 54section \<open>Associative/Commutative Monoid Basis of Separation Algebras\<close> 55 56class pre_sep_algebra = zero + plus + 57 fixes sep_disj :: "'a => 'a => bool" (infix "##" 60) 58 59 assumes sep_disj_zero [simp]: "x ## 0" 60 assumes sep_disj_commuteI: "x ## y \<Longrightarrow> y ## x" 61 62 assumes sep_add_zero [simp]: "x + 0 = x" 63 assumes sep_add_commute: "x ## y \<Longrightarrow> x + y = y + x" 64 65 assumes sep_add_assoc: 66 "\<lbrakk> x ## y; y ## z; x ## z \<rbrakk> \<Longrightarrow> (x + y) + z = x + (y + z)" 67begin 68 69lemma sep_disj_commute: "x ## y = y ## x" 70 by (blast intro: sep_disj_commuteI) 71 72lemma sep_add_left_commute: 73 assumes a: "a ## b" "b ## c" "a ## c" 74 shows "b + (a + c) = a + (b + c)" (is "?lhs = ?rhs") 75proof - 76 have "?lhs = b + a + c" using a 77 by (simp add: sep_add_assoc[symmetric] sep_disj_commute) 78 also have "... = a + b + c" using a 79 by (simp add: sep_add_commute sep_disj_commute) 80 also have "... = ?rhs" using a 81 by (simp add: sep_add_assoc sep_disj_commute) 82 finally show ?thesis . 83qed 84 85lemmas sep_add_ac = sep_add_assoc sep_add_commute sep_add_left_commute 86 sep_disj_commute (* nearly always necessary *) 87 88end 89 90 91section \<open>Separation Algebra as Defined by Calcagno et al.\<close> 92 93class sep_algebra = pre_sep_algebra + 94 assumes sep_disj_addD1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y" 95 assumes sep_disj_addI1: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + y ## z" 96begin 97 98subsection \<open>Basic Construct Definitions and Abbreviations\<close> 99 100(* Lower precedence than pred_conj, otherwise "P \<and>* Q and R" is ambiguous, 101 * (noting that Isabelle turns "(P \<and>* Q) and R" into "P \<and>* Q and R"). 102 *) 103definition 104 sep_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "**" 36) 105 where 106 "P ** Q \<equiv> \<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y" 107 108notation 109 sep_conj (infixr "\<and>*" 36) 110notation (latex output) 111 sep_conj (infixr "\<and>\<^sup>*" 36) 112 113definition 114 sep_empty :: "'a \<Rightarrow> bool" ("\<box>") where 115 "\<box> \<equiv> \<lambda>h. h = 0" 116 117definition 118 sep_impl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixr "\<longrightarrow>*" 25) 119 where 120 "P \<longrightarrow>* Q \<equiv> \<lambda>h. \<forall>h'. h ## h' \<and> P h' \<longrightarrow> Q (h + h')" 121 122definition 123 sep_substate :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 60) where 124 "x \<preceq> y \<equiv> \<exists>z. x ## z \<and> x + z = y" 125 126(* We want these to be abbreviations not definitions, because basic True and 127 False will occur by simplification in sep_conj terms *) 128abbreviation 129 "sep_true \<equiv> \<langle>True\<rangle>" 130 131abbreviation 132 "sep_false \<equiv> \<langle>False\<rangle>" 133 134 135subsection \<open>Disjunction/Addition Properties\<close> 136 137lemma disjoint_zero_sym [simp]: "0 ## x" 138 by (simp add: sep_disj_commute) 139 140lemma sep_add_zero_sym [simp]: "0 + x = x" 141 by (simp add: sep_add_commute) 142 143lemma sep_disj_addD2: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## z" 144 by (metis sep_add_commute sep_disj_addD1 sep_disj_commuteI) 145 146lemma sep_disj_addD: "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x ## y \<and> x ## z" 147 by (metis sep_disj_addD1 sep_disj_addD2) 148 149lemma sep_add_disjD: "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## z \<and> y ## z" 150 by (metis sep_disj_addD sep_disj_commuteI) 151 152lemma sep_disj_addI2: 153 "\<lbrakk> x ## y + z; y ## z \<rbrakk> \<Longrightarrow> x + z ## y" 154 using sep_add_commute sep_disj_addI1 sep_disj_commuteI by presburger 155 156lemma sep_add_disjI1: 157 "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> x + z ## y" 158 by (metis sep_add_commute sep_disj_addI1 sep_disj_commuteI sep_add_disjD) 159 160lemma sep_add_disjI2: 161 "\<lbrakk> x + y ## z; x ## y \<rbrakk> \<Longrightarrow> z + y ## x" 162 by (metis sep_add_commute sep_disj_addI1 sep_disj_commuteI sep_add_disjD) 163 164lemma sep_disj_addI3: 165 "x + y ## z \<Longrightarrow> x ## y \<Longrightarrow> x ## y + z" 166 by (metis sep_add_commute sep_disj_addI1 sep_disj_commuteI sep_add_disjD) 167 168lemma sep_disj_add: 169 "\<lbrakk> y ## z; x ## y \<rbrakk> \<Longrightarrow> x ## y + z = x + y ## z" 170 by (metis sep_disj_addI1 sep_disj_addI3) 171 172 173subsection \<open>Substate Properties\<close> 174 175lemma sep_substate_disj_add: 176 "x ## y \<Longrightarrow> x \<preceq> x + y" 177 unfolding sep_substate_def by blast 178 179lemma sep_substate_disj_add': 180 "x ## y \<Longrightarrow> x \<preceq> y + x" 181 by (simp add: sep_add_ac sep_substate_disj_add) 182 183 184subsection \<open>Separating Conjunction Properties\<close> 185 186lemma sep_conjD: 187 "(P \<and>* Q) h \<Longrightarrow> \<exists>x y. x ## y \<and> h = x + y \<and> P x \<and> Q y" 188 by (simp add: sep_conj_def) 189 190lemma sep_conjE: 191 "\<lbrakk> (P ** Q) h; \<And>x y. \<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> X \<rbrakk> \<Longrightarrow> X" 192 by (auto simp: sep_conj_def) 193 194lemma sep_conjI: 195 "\<lbrakk> P x; Q y; x ## y; h = x + y \<rbrakk> \<Longrightarrow> (P ** Q) h" 196 by (auto simp: sep_conj_def) 197 198lemma sep_conj_commuteI: 199 "(P ** Q) h \<Longrightarrow> (Q ** P) h" 200 by (auto intro!: sep_conjI elim!: sep_conjE simp: sep_add_ac) 201 202lemma sep_conj_commute: 203 "(P ** Q) = (Q ** P)" 204 by (rule ext) (auto intro: sep_conj_commuteI) 205 206lemma sep_conj_assoc: 207 "((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs") 208proof (rule ext, rule iffI) 209 fix h 210 assume a: "?lhs h" 211 then obtain x y z where "P x" and "Q y" and "R z" 212 and "x ## y" and "x ## z" and "y ## z" and "x + y ## z" 213 and "h = x + y + z" 214 by (auto dest!: sep_conjD dest: sep_add_disjD) 215 moreover 216 then have "x ## y + z" 217 by (simp add: sep_disj_add) 218 ultimately 219 show "?rhs h" 220 by (auto simp: sep_add_ac intro!: sep_conjI) 221next 222 fix h 223 assume a: "?rhs h" 224 then obtain x y z where "P x" and "Q y" and "R z" 225 and "x ## y" and "x ## z" and "y ## z" and "x ## y + z" 226 and "h = x + y + z" 227 by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD) 228 thus "?lhs h" 229 by (metis sep_conj_def sep_disj_addI1) 230qed 231 232lemma sep_conj_impl: 233 "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> P' h; \<And>h. Q h \<Longrightarrow> Q' h \<rbrakk> \<Longrightarrow> (P' ** Q') h" 234 by (erule sep_conjE, auto intro!: sep_conjI) 235 236lemma sep_conj_impl1: 237 assumes P: "\<And>h. P h \<Longrightarrow> I h" 238 shows "(P ** R) h \<Longrightarrow> (I ** R) h" 239 by (auto intro: sep_conj_impl P) 240 241lemma sep_globalise: 242 "\<lbrakk> (P ** R) h; (\<And>h. P h \<Longrightarrow> Q h) \<rbrakk> \<Longrightarrow> (Q ** R) h" 243 by (fast elim: sep_conj_impl) 244 245lemma sep_conj_trivial_strip1: 246 "Q = R \<Longrightarrow> (P ** Q) = (P ** R)" by simp 247 248lemma sep_conj_trivial_strip2: 249 "Q = R \<Longrightarrow> (Q ** P) = (R ** P)" by simp 250 251lemma disjoint_subheaps_exist: 252 "\<exists>x y. x ## y \<and> h = x + y" 253 by (rule_tac x=0 in exI, auto) 254 255lemma sep_conj_left_commute: (* for permutative rewriting *) 256 "(P ** (Q ** R)) = (Q ** (P ** R))" (is "?x = ?y") 257proof - 258 have "?x = ((Q ** R) ** P)" by (simp add: sep_conj_commute) 259 also have "\<dots> = (Q ** (R ** P))" by (subst sep_conj_assoc, simp) 260 finally show ?thesis by (simp add: sep_conj_commute) 261qed 262 263lemmas sep_conj_ac = sep_conj_commute sep_conj_assoc sep_conj_left_commute 264 265lemma sep_empty_zero [simp,intro!]: "\<box> 0" 266 by (simp add: sep_empty_def) 267 268 269subsection \<open>Properties of @{text sep_true} and @{text sep_false}\<close> 270 271lemma sep_conj_sep_true: 272 "P h \<Longrightarrow> (P ** sep_true) h" 273 by (simp add: sep_conjI[where y=0]) 274 275lemma sep_conj_sep_true': 276 "P h \<Longrightarrow> (sep_true ** P) h" 277 by (simp add: sep_conjI[where x=0]) 278 279lemma sep_conj_true [simp]: 280 "(sep_true ** sep_true) = sep_true" 281 unfolding sep_conj_def 282 by (auto intro: disjoint_subheaps_exist) 283 284lemma sep_conj_false_right [simp]: 285 "(P ** sep_false) = sep_false" 286 by (force elim: sep_conjE) 287 288lemma sep_conj_false_left [simp]: 289 "(sep_false ** P) = sep_false" 290 by (subst sep_conj_commute) (rule sep_conj_false_right) 291 292 293 294subsection \<open>Properties of @{const sep_empty}\<close> 295 296lemma sep_conj_empty [simp]: 297 "(P ** \<box>) = P" 298 by (simp add: sep_conj_def sep_empty_def) 299 300lemma sep_conj_empty'[simp]: 301 "(\<box> ** P) = P" 302 by (subst sep_conj_commute, rule sep_conj_empty) 303 304lemma sep_conj_sep_emptyI: 305 "P h \<Longrightarrow> (P ** \<box>) h" 306 by simp 307 308lemma sep_conj_sep_emptyE: 309 "\<lbrakk> P s; (P ** \<box>) s \<Longrightarrow> (Q ** R) s \<rbrakk> \<Longrightarrow> (Q ** R) s" 310 by simp 311 312 313subsection \<open>Properties of top (@{text sep_true})\<close> 314 315lemma sep_conj_true_P [simp]: 316 "(sep_true ** (sep_true ** P)) = (sep_true ** P)" 317 by (simp add: sep_conj_assoc[symmetric]) 318 319lemma sep_conj_disj: 320 "((P or Q) ** R) = ((P ** R) or (Q ** R))" 321 by (rule ext, auto simp: sep_conj_def) 322 323lemma sep_conj_sep_true_left: 324 "(P ** Q) h \<Longrightarrow> (sep_true ** Q) h" 325 by (erule sep_conj_impl, simp+) 326 327lemma sep_conj_sep_true_right: 328 "(P ** Q) h \<Longrightarrow> (P ** sep_true) h" 329 by (subst (asm) sep_conj_commute, drule sep_conj_sep_true_left, 330 simp add: sep_conj_ac) 331 332 333subsection \<open>Separating Conjunction with Quantifiers\<close> 334 335lemma sep_conj_conj: 336 "((P and Q) ** R) h \<Longrightarrow> ((P ** R) and (Q ** R)) h" 337 by (force intro: sep_conjI elim!: sep_conjE) 338 339lemma sep_conj_exists1: 340 "((EXS x. P x) ** Q) = (EXS x. (P x ** Q))" 341 by (force intro: sep_conjI elim: sep_conjE) 342 343lemma sep_conj_exists2: 344 "(P ** (EXS x. Q x)) = (EXS x. P ** Q x)" 345 by (force intro!: sep_conjI elim!: sep_conjE) 346 347lemmas sep_conj_exists = sep_conj_exists1 sep_conj_exists2 348 349lemma sep_conj_spec1: 350 "((ALLS x. P x) ** Q) h \<Longrightarrow> (P x ** Q) h" 351 by (force intro: sep_conjI elim: sep_conjE) 352 353lemma sep_conj_spec2: 354 "(P ** (ALLS x. Q x)) h \<Longrightarrow> (P ** Q x) h" 355 by (force intro: sep_conjI elim: sep_conjE) 356 357lemmas sep_conj_spec = sep_conj_spec1 sep_conj_spec2 358 359subsection \<open>Properties of Separating Implication\<close> 360 361lemma sep_implI: 362 assumes a: "\<And>h'. \<lbrakk> h ## h'; P h' \<rbrakk> \<Longrightarrow> Q (h + h')" 363 shows "(P \<longrightarrow>* Q) h" 364 unfolding sep_impl_def by (auto elim: a) 365 366lemma sep_implD: 367 "(x \<longrightarrow>* y) h \<Longrightarrow> \<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h')" 368 by (force simp: sep_impl_def) 369 370lemma sep_implE: 371 "(x \<longrightarrow>* y) h \<Longrightarrow> (\<forall>h'. h ## h' \<and> x h' \<longrightarrow> y (h + h') \<Longrightarrow> Q) \<Longrightarrow> Q" 372 by (auto dest: sep_implD) 373 374lemma sep_impl_sep_true [simp]: 375 "(P \<longrightarrow>* sep_true) = sep_true" 376 by (force intro!: sep_implI) 377 378lemma sep_impl_sep_false [simp]: 379 "(sep_false \<longrightarrow>* P) = sep_true" 380 by (force intro!: sep_implI) 381 382lemma sep_impl_sep_true_P: 383 "(sep_true \<longrightarrow>* P) h \<Longrightarrow> P h" 384 by (clarsimp dest!: sep_implD elim!: allE[where x=0]) 385 386lemma sep_impl_sep_true_false [simp]: 387 "(sep_true \<longrightarrow>* sep_false) = sep_false" 388 by (force dest: sep_impl_sep_true_P) 389 390lemma sep_conj_sep_impl: 391 "\<lbrakk> P h; \<And>h. (P ** Q) h \<Longrightarrow> R h \<rbrakk> \<Longrightarrow> (Q \<longrightarrow>* R) h" 392proof (rule sep_implI) 393 fix h' h 394 assume "P h" and "h ## h'" and "Q h'" 395 hence "(P ** Q) (h + h')" by (force intro: sep_conjI) 396 moreover assume "\<And>h. (P ** Q) h \<Longrightarrow> R h" 397 ultimately show "R (h + h')" by simp 398qed 399 400lemma sep_conj_sep_impl2: 401 "\<lbrakk> (P ** Q) h; \<And>h. P h \<Longrightarrow> (Q \<longrightarrow>* R) h \<rbrakk> \<Longrightarrow> R h" 402 by (force dest: sep_implD elim: sep_conjE) 403 404lemma sep_conj_sep_impl_sep_conj2: 405 "(P ** R) h \<Longrightarrow> (P ** (Q \<longrightarrow>* (Q ** R))) h" 406 by (erule (1) sep_conj_impl, erule sep_conj_sep_impl, simp add: sep_conj_ac) 407 408 409subsection \<open>Pure assertions\<close> 410 411definition 412 pure :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 413 "pure P \<equiv> \<forall>h h'. P h = P h'" 414 415lemma pure_sep_true: 416 "pure sep_true" 417 by (simp add: pure_def) 418 419lemma pure_sep_false: 420 "pure sep_false" 421 by (simp add: pure_def) 422 423lemma pure_split: 424 "pure P = (P = sep_true \<or> P = sep_false)" 425 by (force simp: pure_def) 426 427lemma pure_sep_conj: 428 "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<and>* Q)" 429 by (force simp: pure_split) 430 431lemma pure_sep_impl: 432 "\<lbrakk> pure P; pure Q \<rbrakk> \<Longrightarrow> pure (P \<longrightarrow>* Q)" 433 by (force simp: pure_split) 434 435lemma pure_conj_sep_conj: 436 "\<lbrakk> (P and Q) h; pure P \<or> pure Q \<rbrakk> \<Longrightarrow> (P \<and>* Q) h" 437 by (metis pure_def sep_add_zero sep_conjI sep_conj_commute sep_disj_zero) 438 439lemma pure_sep_conj_conj: 440 "\<lbrakk> (P \<and>* Q) h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P and Q) h" 441 by (force simp: pure_split) 442 443lemma pure_conj_sep_conj_assoc: 444 "pure P \<Longrightarrow> ((P and Q) \<and>* R) = (P and (Q \<and>* R))" 445 by (auto simp: pure_split) 446 447lemma pure_sep_impl_impl: 448 "\<lbrakk> (P \<longrightarrow>* Q) h; pure P \<rbrakk> \<Longrightarrow> P h \<longrightarrow> Q h" 449 by (force simp: pure_split dest: sep_impl_sep_true_P) 450 451lemma pure_impl_sep_impl: 452 "\<lbrakk> P h \<longrightarrow> Q h; pure P; pure Q \<rbrakk> \<Longrightarrow> (P \<longrightarrow>* Q) h" 453 by (force simp: pure_split) 454 455lemma pure_conj_right: "(Q \<and>* (\<langle>P'\<rangle> and Q')) = (\<langle>P'\<rangle> and (Q \<and>* Q'))" 456 by (rule ext, rule, rule, clarsimp elim!: sep_conjE) 457 (erule sep_conj_impl, auto) 458 459lemma pure_conj_right': "(Q \<and>* (P' and \<langle>Q'\<rangle>)) = (\<langle>Q'\<rangle> and (Q \<and>* P'))" 460 by (simp add: conj_comms pure_conj_right) 461 462lemma pure_conj_left: "((\<langle>P'\<rangle> and Q') \<and>* Q) = (\<langle>P'\<rangle> and (Q' \<and>* Q))" 463 by (simp add: pure_conj_right sep_conj_ac) 464 465lemma pure_conj_left': "((P' and \<langle>Q'\<rangle>) \<and>* Q) = (\<langle>Q'\<rangle> and (P' \<and>* Q))" 466 by (subst conj_comms, subst pure_conj_left, simp) 467 468lemmas pure_conj = pure_conj_right pure_conj_right' pure_conj_left 469 pure_conj_left' 470 471declare pure_conj[simp add] 472 473 474subsection \<open>Intuitionistic assertions\<close> 475 476definition intuitionistic :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 477 "intuitionistic P \<equiv> \<forall>h h'. P h \<and> h \<preceq> h' \<longrightarrow> P h'" 478 479lemma intuitionisticI: 480 "(\<And>h h'. \<lbrakk> P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h') \<Longrightarrow> intuitionistic P" 481 by (unfold intuitionistic_def, fast) 482 483lemma intuitionisticD: 484 "\<lbrakk> intuitionistic P; P h; h \<preceq> h' \<rbrakk> \<Longrightarrow> P h'" 485 by (unfold intuitionistic_def, fast) 486 487lemma pure_intuitionistic: 488 "pure P \<Longrightarrow> intuitionistic P" 489 by (clarsimp simp: intuitionistic_def pure_def, fast) 490 491lemma intuitionistic_conj: 492 "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P and Q)" 493 by (force intro: intuitionisticI dest: intuitionisticD) 494 495lemma intuitionistic_disj: 496 "\<lbrakk> intuitionistic P; intuitionistic Q \<rbrakk> \<Longrightarrow> intuitionistic (P or Q)" 497 by (force intro: intuitionisticI dest: intuitionisticD) 498 499lemma intuitionistic_forall: 500 "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (ALLS x. P x)" 501 by (force intro: intuitionisticI dest: intuitionisticD) 502 503lemma intuitionistic_exists: 504 "(\<And>x. intuitionistic (P x)) \<Longrightarrow> intuitionistic (EXS x. P x)" 505 by (force intro: intuitionisticI dest: intuitionisticD) 506 507lemma intuitionistic_sep_conj_sep_true: 508 "intuitionistic (sep_true \<and>* P)" 509proof (rule intuitionisticI) 510 fix h h' r 511 assume a: "(sep_true \<and>* P) h" 512 then obtain x y where P: "P y" and h: "h = x + y" and xyd: "x ## y" 513 by - (drule sep_conjD, clarsimp) 514 moreover assume a2: "h \<preceq> h'" 515 then obtain z where h': "h' = h + z" and hzd: "h ## z" 516 by (clarsimp simp: sep_substate_def) 517 518 moreover have "(P \<and>* sep_true) (y + (x + z))" 519 using P h hzd xyd 520 by (metis sep_add_disjI1 sep_disj_commute sep_conjI) 521 ultimately show "(sep_true \<and>* P) h'" using hzd 522 by (auto simp: sep_conj_commute sep_add_ac dest!: sep_disj_addD) 523qed 524 525lemma intuitionistic_sep_impl_sep_true: 526 "intuitionistic (sep_true \<longrightarrow>* P)" 527proof (rule intuitionisticI) 528 fix h h' 529 assume imp: "(sep_true \<longrightarrow>* P) h" and hh': "h \<preceq> h'" 530 531 from hh' obtain z where h': "h' = h + z" and hzd: "h ## z" 532 by (clarsimp simp: sep_substate_def) 533 show "(sep_true \<longrightarrow>* P) h'" using imp h' hzd 534 apply (clarsimp dest!: sep_implD) 535 apply (metis sep_add_assoc sep_add_disjD sep_disj_addI3 sep_implI) 536 done 537qed 538 539lemma intuitionistic_sep_conj: 540 assumes ip: "intuitionistic (P::('a \<Rightarrow> bool))" 541 shows "intuitionistic (P \<and>* Q)" 542proof (rule intuitionisticI) 543 fix h h' 544 assume sc: "(P \<and>* Q) h" and hh': "h \<preceq> h'" 545 546 from hh' obtain z where h': "h' = h + z" and hzd: "h ## z" 547 by (clarsimp simp: sep_substate_def) 548 549 from sc obtain x y where px: "P x" and qy: "Q y" 550 and h: "h = x + y" and xyd: "x ## y" 551 by (clarsimp simp: sep_conj_def) 552 553 have "x ## z" using hzd h xyd 554 by (metis sep_add_disjD) 555 556 with ip px have "P (x + z)" 557 by (fastforce elim: intuitionisticD sep_substate_disj_add) 558 559 thus "(P \<and>* Q) h'" using h' h hzd qy xyd 560 by (metis (full_types) sep_add_commute sep_add_disjD sep_add_disjI2 561 sep_add_left_commute sep_conjI) 562qed 563 564lemma intuitionistic_sep_impl: 565 assumes iq: "intuitionistic Q" 566 shows "intuitionistic (P \<longrightarrow>* Q)" 567proof (rule intuitionisticI) 568 fix h h' 569 assume imp: "(P \<longrightarrow>* Q) h" and hh': "h \<preceq> h'" 570 571 from hh' obtain z where h': "h' = h + z" and hzd: "h ## z" 572 by (clarsimp simp: sep_substate_def) 573 574 { 575 fix x 576 assume px: "P x" and hzx: "h + z ## x" 577 578 have "h + x \<preceq> h + x + z" using hzx hzd 579 by (metis sep_add_disjI1 sep_substate_def) 580 581 with imp hzd iq px hzx 582 have "Q (h + z + x)" 583 by (metis intuitionisticD sep_add_assoc sep_add_ac sep_add_disjD sep_implE) 584 } 585 586 with imp h' hzd iq show "(P \<longrightarrow>* Q) h'" 587 by (fastforce intro: sep_implI) 588qed 589 590lemma strongest_intuitionistic: 591 "\<not>(\<exists>Q. (\<forall>h. (Q h \<longrightarrow> (P \<and>* sep_true) h)) \<and> intuitionistic Q \<and> Q \<noteq> (P \<and>* sep_true) \<and> (\<forall>h. P h \<longrightarrow> Q h))" 592 by (fastforce intro!: ext sep_substate_disj_add dest!: sep_conjD intuitionisticD) 593 594lemma weakest_intuitionistic: 595 "\<not> (\<exists>Q. (\<forall>h. ((sep_true \<longrightarrow>* P) h \<longrightarrow> Q h)) \<and> intuitionistic Q \<and> 596 Q \<noteq> (sep_true \<longrightarrow>* P) \<and> (\<forall>h. Q h \<longrightarrow> P h))" 597 apply (clarsimp) 598 apply (rule ext) 599 apply (rule iffI) 600 apply (rule sep_implI) 601 apply (drule_tac h="x" and h'="x + h'" in intuitionisticD) 602 apply (clarsimp simp: sep_add_ac sep_substate_disj_add)+ 603 done 604 605lemma intuitionistic_sep_conj_sep_true_P: 606 "\<lbrakk> (P \<and>* sep_true) s; intuitionistic P \<rbrakk> \<Longrightarrow> P s" 607 by (force dest: intuitionisticD elim: sep_conjE sep_substate_disj_add) 608 609lemma intuitionistic_sep_conj_sep_true_simp: 610 "intuitionistic P \<Longrightarrow> (P \<and>* sep_true) = P" 611 by (fast intro!: sep_conj_sep_true 612 elim: intuitionistic_sep_conj_sep_true_P) 613 614lemma intuitionistic_sep_impl_sep_true_P: 615 "\<lbrakk> P h; intuitionistic P \<rbrakk> \<Longrightarrow> (sep_true \<longrightarrow>* P) h" 616 by (force intro!: sep_implI dest: intuitionisticD 617 intro: sep_substate_disj_add) 618 619lemma intuitionistic_sep_impl_sep_true_simp: 620 "intuitionistic P \<Longrightarrow> (sep_true \<longrightarrow>* P) = P" 621 by (fast elim: sep_impl_sep_true_P intuitionistic_sep_impl_sep_true_P) 622 623 624subsection \<open>Strictly exact assertions\<close> 625 626definition strictly_exact :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 627 "strictly_exact P \<equiv> \<forall>h h'. P h \<and> P h' \<longrightarrow> h = h'" 628 629lemma strictly_exactD: 630 "\<lbrakk> strictly_exact P; P h; P h' \<rbrakk> \<Longrightarrow> h = h'" 631 by (unfold strictly_exact_def, fast) 632 633lemma strictly_exactI: 634 "(\<And>h h'. \<lbrakk> P h; P h' \<rbrakk> \<Longrightarrow> h = h') \<Longrightarrow> strictly_exact P" 635 by (unfold strictly_exact_def, fast) 636 637lemma strictly_exact_sep_conj: 638 "\<lbrakk> strictly_exact P; strictly_exact Q \<rbrakk> \<Longrightarrow> strictly_exact (P \<and>* Q)" 639 apply (rule strictly_exactI) 640 apply (erule sep_conjE)+ 641 apply (drule_tac h="x" and h'="xa" in strictly_exactD, assumption+) 642 apply (drule_tac h="y" and h'="ya" in strictly_exactD, assumption+) 643 apply clarsimp 644 done 645 646lemma strictly_exact_conj_impl: 647 "\<lbrakk> (Q \<and>* sep_true) h; P h; strictly_exact Q \<rbrakk> \<Longrightarrow> (Q \<and>* (Q \<longrightarrow>* P)) h" 648 by (force intro: sep_conjI sep_implI dest: strictly_exactD elim!: sep_conjE 649 simp: sep_add_commute sep_add_assoc) 650 651end 652 653section \<open>Separation Algebra with Stronger, but More Intuitive Disjunction Axiom\<close> 654 655class stronger_sep_algebra = pre_sep_algebra + 656 assumes sep_add_disj_eq [simp]: "y ## z \<Longrightarrow> x ## y + z = (x ## y \<and> x ## z)" 657begin 658 659lemma sep_disj_add_eq [simp]: "x ## y \<Longrightarrow> x + y ## z = (x ## z \<and> y ## z)" 660 by (metis sep_add_disj_eq sep_disj_commute) 661 662subclass sep_algebra by standard auto 663 664end 665 666interpretation sep: ab_semigroup_mult "(**)" 667 by unfold_locales (simp add: sep_conj_ac)+ 668 669interpretation sep: comm_monoid "(**)" \<box> 670 by unfold_locales simp 671 672interpretation sep: comm_monoid_mult "(**)" \<box> 673 by unfold_locales simp 674 675section \<open>Folding separating conjunction over lists and sets of predicates\<close> 676 677definition 678 sep_list_conj :: "('a::sep_algebra \<Rightarrow> bool) list \<Rightarrow> ('a \<Rightarrow> bool)" where 679 "sep_list_conj Ps \<equiv> foldl ((**)) \<box> Ps" 680 681abbreviation 682 sep_map_list_conj :: "('b \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool) \<Rightarrow> 'b list \<Rightarrow> ('a \<Rightarrow> bool)" 683where 684 "sep_map_list_conj g S \<equiv> sep_list_conj (map g S)" 685 686abbreviation 687 sep_map_set_conj :: "('b \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool) \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> bool)" 688where 689 "sep_map_set_conj g S \<equiv> sep.prod g S" 690 691definition 692 sep_set_conj :: "('a::sep_algebra \<Rightarrow> bool) set \<Rightarrow> ('a \<Rightarrow> bool)" where 693 "sep_set_conj S \<equiv> sep.prod id S" 694 695(* Notation. *) 696consts 697 sep_conj_lifted :: "'b \<Rightarrow> ('a::sep_algebra \<Rightarrow> bool)" ("\<And>* _" [60] 90) 698notation (latex output) sep_conj_lifted ("\<And>\<^sup>* _" [60] 90) 699notation (latex output) sep_map_list_conj ("\<And>\<^sup>* _" [60] 90) 700 701adhoc_overloading sep_conj_lifted sep_list_conj 702adhoc_overloading sep_conj_lifted sep_set_conj 703 704 705(* FIXME. Add notation for sep_map_list_conj, and consider unifying with sep_map_set_conj. *) 706 707 708text\<open>Now: lots of fancy syntax. First, @{term "sep_map_set_conj (%x. g) A"} is written @{text"\<And>+x\<in>A. g"}.\<close> 709 710(* Clagged from Big_Operators. *) 711syntax 712 "_sep_map_set_conj" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SETSEPCONJ _:_. _)" [0, 51, 10] 10) 713syntax (xsymbols) 714 "_sep_map_set_conj" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<And>*_\<in>_. _)" [0, 51, 10] 10) 715syntax (HTML output) 716 "_sep_map_set_conj" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<And>*_\<in>_. _)" [0, 51, 10] 10) 717syntax (latex output) 718 "_sep_map_set_conj" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<And>\<^sup>*(00\<^bsub>_\<in>_\<^esub>) _)" [0, 51, 10] 10) 719 720translations \<comment> \<open>Beware of argument permutation!\<close> 721 "SETSEPCONJ x:A. g" == "CONST sep_map_set_conj (%x. g) A" 722 "\<And>* x\<in>A. g" == "CONST sep_map_set_conj (%x. g) A" 723 724text\<open>Instead of @{term"\<And>*x\<in>{x. P}. g"} we introduce the shorter @{text"\<And>+x|P. g"}.\<close> 725 726syntax 727 "_qsep_map_set_conj" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SETSEPCONJ _ |/ _./ _)" [0,0,10] 10) 728syntax (xsymbols) 729 "_qsep_map_set_conj" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<And>*_ | (_)./ _)" [0,0,10] 10) 730syntax (HTML output) 731 "_qsep_map_set_conj" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<And>*_ | (_)./ _)" [0,0,10] 10) 732syntax (latex output) 733 "_qsep_map_set_conj" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<And>\<^sup>*(00\<^bsub>_ | (_)\<^esub>) /_)" [0,0,10] 10) 734 735translations 736 "SETSEPCONJ x|P. g" => "CONST sep_map_set_conj (%x. g) {x. P}" 737 "\<And>*x|P. g" => "CONST sep_map_set_conj (%x. g) {x. P}" 738 739print_translation \<open> 740let 741 fun setsepconj_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = 742 if x <> y then raise Match 743 else 744 let 745 val x' = Syntax_Trans.mark_bound_body (x, Tx); 746 val t' = subst_bound (x', t); 747 val P' = subst_bound (x', P); 748 in 749 Syntax.const @{syntax_const "_qsep_map_set_conj"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t' 750 end 751 | setsepconj_tr' _ = raise Match; 752in [(@{const_syntax sep_map_set_conj}, K setsepconj_tr')] end 753\<close> 754 755 756interpretation sep: folding "(\<and>*)" \<box> 757 by unfold_locales (simp add: comp_def sep_conj_ac) 758 759lemma "\<And>* [\<box>,P] = P" 760 by (simp add: sep_list_conj_def) 761 762lemma "\<And>* {\<box>} = \<box>" 763 by (simp add: sep_set_conj_def) 764 765lemma "\<And>* {P,\<box>} = P" 766 by (cases "P = \<box>", auto simp: sep_set_conj_def) 767 768lemma "(\<And>* x\<in>{0,1::nat}. if x=0 then \<box> else P) = P" 769 by auto 770 771lemma map_sep_list_conj_cong: 772 "(\<And>x. x \<in> set xs \<Longrightarrow> f x = g x) \<Longrightarrow> \<And>* map f xs = \<And>* map g xs" 773 by (metis map_cong) 774 775lemma sep_list_conj_Nil [simp]: "\<And>* [] = \<box>" 776 by (simp add: sep_list_conj_def) 777 778(* apparently these two are rarely used and had to be removed from List.thy *) 779lemma (in semigroup) foldl_assoc: 780 "foldl f (f x y) zs = f x (foldl f y zs)" 781 by (induct zs arbitrary: y) (simp_all add:assoc) 782 783lemma (in monoid) foldl_absorb1: 784 "f x (foldl f z zs) = foldl f x zs" 785 by (induct zs) (simp_all add:foldl_assoc) 786 787 788context comm_monoid 789begin 790 791lemma foldl_map_filter: 792 "f (foldl f z (map P (filter t xs))) (foldl f z (map P (filter (not t) xs))) = foldl f z (map P xs)" 793proof (induct xs) 794 case Nil thus ?case by clarsimp 795next 796 case (Cons x xs) 797 hence IH: 798 "foldl f z (map P xs) = f (foldl f z (map P (filter t xs))) (foldl f z (map P [x\<leftarrow>xs . \<not> t x]))" 799 by (simp only: eq_commute) 800 801 have foldl_Cons': 802 "\<And>x xs. foldl f z (x # xs) = f x (foldl f z xs)" 803 by (simp, subst foldl_absorb1[symmetric], rule refl) 804 805 { assume "t x" 806 hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH ac_simps) 807 } moreover { 808 assume "\<not> t x" 809 hence ?case by (auto simp del: foldl_Cons simp add: foldl_Cons' IH ac_simps) 810 } 811 ultimately show ?case by blast 812qed 813 814lemma foldl_map_add: 815 "foldl f z (map (\<lambda>x. f (P x) (Q x)) xs) = f (foldl f z (map P xs)) (foldl f z (map Q xs))" 816 apply (induct xs) 817 apply clarsimp 818 apply simp 819 by (metis (full_types) commute foldl_absorb1 foldl_assoc) 820 821lemma foldl_map_remove1: 822 "x \<in> set xs \<Longrightarrow> foldl f z (map P xs) = f (P x) (foldl f z (map P (remove1 x xs)))" 823 apply (induction xs, simp) 824 apply clarsimp 825 by (metis foldl_absorb1 left_commute) 826 827end 828 829lemma sep_list_conj_Cons [simp]: "\<And>* (x#xs) = (x ** \<And>* xs)" 830 by (simp add: sep_list_conj_def sep.foldl_absorb1) 831 832lemma sep_list_conj_append [simp]: "\<And>* (xs @ ys) = (\<And>* xs ** \<And>* ys)" 833 by (simp add: sep_list_conj_def sep.foldl_absorb1) 834 835lemma sep_list_conj_map_append: 836 "\<And>* map f (xs @ ys) = (\<And>* map f xs \<and>* \<And>* map f ys)" 837 by (metis map_append sep_list_conj_append) 838 839lemma sep_list_con_map_filter: 840 "(\<And>* map P (filter t xs) \<and>* \<And>* map P (filter (not t) xs)) 841 = \<And>* map P xs" 842 apply (simp add: sep_list_conj_def) 843 apply (rule sep.foldl_map_filter) 844 done 845 846lemma union_filter: 847 "({x \<in> xs. P x} \<union> {x \<in> xs. \<not> P x}) = xs" 848 by fast 849 850lemma sep_map_set_conj_restrict: 851 "finite xs \<Longrightarrow> 852 sep_map_set_conj P xs = 853 (sep_map_set_conj P {x \<in> xs. t x} \<and>* 854 sep_map_set_conj P {x \<in> xs. \<not> t x})" 855 by (subst sep.prod.union_disjoint [symmetric], (fastforce simp: union_filter)+) 856 857 858lemma sep_list_conj_map_add: 859 "\<And>* map (\<lambda>x. f x \<and>* g x) xs = (\<And>* map f xs \<and>* \<And>* map g xs)" 860 apply (simp add: sep_list_conj_def) 861 apply (rule sep.foldl_map_add) 862 done 863 864 865lemma filter_empty: 866 "x \<notin> set xs \<Longrightarrow> filter ((=) x) xs = []" 867 by (induct xs, clarsimp+) 868 869lemma filter_singleton: 870 "\<lbrakk>x \<in> set xs; distinct xs\<rbrakk> \<Longrightarrow> [x'\<leftarrow>xs . x = x'] = [x]" 871 by (induct xs, auto simp: filter_empty) 872 873lemma remove1_filter: 874 "distinct xs \<Longrightarrow> remove1 x xs = filter (\<lambda>y. x \<noteq> y) xs" 875 apply (induct xs) 876 apply simp 877 apply clarsimp 878 apply (rule sym, rule filter_True) 879 apply clarsimp 880 done 881 882lemma sep_list_conj_map_remove1: 883 "x \<in> set xs \<Longrightarrow> \<And>* map P xs = (P x \<and>* \<And>* map P (remove1 x xs))" 884 apply (simp add: sep_list_conj_def) 885 apply (erule sep.foldl_map_remove1) 886 done 887 888lemma sep_map_take_Suc: 889 "i < length xs \<Longrightarrow> 890 \<And>* map P (take (Suc i) xs) = (\<And>* map P (take i xs) \<and>* P (xs ! i))" 891 by (subst take_Suc_conv_app_nth, simp+) 892 893lemma sep_conj_map_split: 894 "(\<And>* map f xs \<and>* f a \<and>* \<And>* map f ys) 895 = (\<And>* map f (xs @ a # ys))" 896 by (metis list.map(2) map_append sep_list_conj_Cons sep_list_conj_append) 897 898 899section "Separation predicates on sets" 900 901lemma sep_map_set_conj_cong: 902 "\<lbrakk>P = Q; xs = ys\<rbrakk> \<Longrightarrow> sep_map_set_conj P xs = sep_map_set_conj Q ys" 903 by simp 904 905lemma sep_set_conj_empty [simp]: 906 "sep_set_conj {} = \<box>" 907 by (simp add: sep_set_conj_def) 908 909 910(* FIXME: We should be able to pull this from the "comm_monoid_big" 911 * or "comm_monoid_add" locales, but I can't work out how... *) 912lemma sep_map_set_conj_reindex_cong: 913 "\<lbrakk>inj_on f A; B = f ` A; \<And>a. a \<in> A \<Longrightarrow> g a = h (f a)\<rbrakk> 914 \<Longrightarrow> sep_map_set_conj h B = sep_map_set_conj g A" 915 by (simp add: sep.prod.reindex) 916 917lemma sep_list_conj_sep_map_set_conj: 918 "distinct xs 919 \<Longrightarrow> \<And>* (map P xs) = (\<And>* x \<in> set xs. P x)" 920 by (induct xs, simp_all) 921 922lemma sep_list_conj_sep_set_conj: 923 "\<lbrakk>distinct xs; inj_on P (set xs)\<rbrakk> 924 \<Longrightarrow> \<And>* (map P xs) = \<And>* (P ` set xs)" 925 apply (subst sep_list_conj_sep_map_set_conj, assumption) 926 apply (clarsimp simp: sep_set_conj_def sep.prod.reindex) 927 done 928 929lemma sep_map_set_conj_sep_list_conj: 930 "finite A \<Longrightarrow> 931 \<exists>xs. set xs = A \<and> distinct xs \<and> sep_map_set_conj P A = \<And>* map P xs" 932 apply (frule finite_distinct_list) 933 apply (erule exE) 934 apply (rule_tac x=xs in exI) 935 apply clarsimp 936 apply (erule sep_list_conj_sep_map_set_conj [symmetric]) 937 done 938 939lemma sep_list_conj_eq: 940 "\<lbrakk>distinct xs; distinct ys; set xs = set ys\<rbrakk> \<Longrightarrow> 941 \<And>* (map P xs) = \<And>* (map P ys)" 942 apply (drule sep_list_conj_sep_map_set_conj [where P=P]) 943 apply (drule sep_list_conj_sep_map_set_conj [where P=P]) 944 apply simp 945 done 946 947lemma sep_list_conj_impl: 948 "\<lbrakk> list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) xs ys; (\<And>* xs) s \<rbrakk> \<Longrightarrow> (\<And>* ys) s" 949 apply (induct arbitrary: s rule: list_all2_induct) 950 apply simp 951 apply simp 952 apply (erule sep_conj_impl, simp_all) 953 done 954 955lemma sep_list_conj_exists: 956 "(\<exists>x. (\<And>* map (\<lambda>y s. P x y s) ys) s) \<Longrightarrow> ((\<And>* map (\<lambda>y s. \<exists>x. P x y s) ys) s)" 957 apply clarsimp 958 apply (erule sep_list_conj_impl[rotated]) 959 apply (rule list_all2I, simp_all) 960 by (fastforce simp: in_set_zip) 961 962lemma sep_list_conj_map_impl: 963 "\<lbrakk>\<And>s x. \<lbrakk>x \<in> set xs; P x s\<rbrakk> \<Longrightarrow> Q x s; (\<And>* map P xs) s\<rbrakk> 964 \<Longrightarrow> (\<And>* map Q xs) s" 965 apply (erule sep_list_conj_impl[rotated]) 966 apply (rule list_all2I, simp_all) 967 by (fastforce simp: in_set_zip) 968 969lemma sep_map_set_conj_impl: 970 "\<lbrakk>sep_map_set_conj P A s; \<And>s x. \<lbrakk>x \<in> A; P x s\<rbrakk> \<Longrightarrow> Q x s; finite A\<rbrakk> 971 \<Longrightarrow> sep_map_set_conj Q A s" 972 apply (frule sep_map_set_conj_sep_list_conj [where P=P]) 973 apply (drule sep_map_set_conj_sep_list_conj [where P=Q]) 974 by (metis sep_list_conj_map_impl sep_list_conj_sep_map_set_conj) 975 976lemma set_sub_sub: 977 "\<lbrakk>zs \<subseteq> ys\<rbrakk> \<Longrightarrow> (xs - zs) - (ys - zs) = (xs - ys)" 978 by blast 979 980lemma sep_map_set_conj_sub_sub_disjoint: 981 "\<lbrakk>finite xs; zs \<subseteq> ys; ys \<subseteq> xs\<rbrakk> 982 \<Longrightarrow> sep_map_set_conj P (xs - zs) = (sep_map_set_conj P (xs - ys) \<and>* sep_map_set_conj P (ys - zs))" 983 apply (cut_tac sep.prod.subset_diff [where A="xs-zs" and B="ys-zs" and g=P]) 984 apply (subst (asm) set_sub_sub, fast+) 985 done 986 987lemma foldl_use_filter_map: 988 "foldl (\<and>*) Q (map (\<lambda>x. if T x then P x else \<box>) xs) = 989 foldl (\<and>*) Q (map P (filter T xs))" 990 by (induct xs arbitrary: Q, simp_all) 991 992lemma sep_list_conj_filter_map: 993 "\<And>* (map (\<lambda>x. if T x then P x else \<box>) xs) = 994 \<And>* (map P (filter T xs))" 995 by (clarsimp simp: sep_list_conj_def foldl_use_filter_map) 996 997lemma sep_map_set_conj_restrict_predicate: 998 "finite A \<Longrightarrow> (\<And>* x\<in>A. if T x then P x else \<box>) = (\<And>* x\<in>(Set.filter T A). P x)" 999 by (simp add: Set.filter_def sep.prod.inter_filter) 1000 1001lemma distinct_filters: 1002 "\<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow> 1003 set [x\<leftarrow>xs . f x \<or> g x] = set [x\<leftarrow>xs . f x] \<union> set [x\<leftarrow>xs . g x]" 1004 by auto 1005 1006lemma sep_list_conj_distinct_filters: 1007 "\<lbrakk>distinct xs; \<And>x. (f x \<and> g x) = False\<rbrakk> \<Longrightarrow> 1008 \<And>* map P [x\<leftarrow>xs . f x \<or> g x] = (\<And>* map P [x\<leftarrow>xs . f x] \<and>* \<And>* map P [x\<leftarrow>xs . g x])" 1009 apply (subst sep_list_conj_sep_map_set_conj, simp)+ 1010 apply (subst distinct_filters, simp+) 1011 apply (subst sep.prod.union_disjoint, auto) 1012 done 1013 1014lemma sep_map_set_conj_set_disjoint: 1015 "\<lbrakk>finite {x. P x}; finite {x. Q x}; \<And>x. (P x \<and> Q x) = False\<rbrakk> 1016 \<Longrightarrow> sep_map_set_conj g {x. P x \<or> Q x} = 1017 (sep_map_set_conj g {x. P x} \<and>* sep_map_set_conj g {x. Q x})" 1018 apply (subst sep.prod.union_disjoint [symmetric], simp+) 1019 apply blast 1020 apply simp 1021 by (metis Collect_disj_eq) 1022 1023 1024text \<open> 1025 Separation algebra with positivity 1026\<close> 1027 1028class positive_sep_algebra = stronger_sep_algebra + 1029 assumes sep_disj_positive : "a ## a \<Longrightarrow> a + a = b \<Longrightarrow> a = b" 1030 1031 1032 1033section \<open>Separation Algebra with a Cancellative Monoid\<close> 1034 1035text \<open> 1036 Separation algebra with a cancellative monoid. The results of being a precise 1037 assertion (distributivity over separating conjunction) require this. 1038\<close> 1039class cancellative_sep_algebra = positive_sep_algebra + 1040 assumes sep_add_cancelD: "\<lbrakk> x + z = y + z ; x ## z ; y ## z \<rbrakk> \<Longrightarrow> x = y" 1041begin 1042 1043definition 1044 (* In any heap, there exists at most one subheap for which P holds *) 1045 precise :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where 1046 "precise P = (\<forall>h hp hp'. hp \<preceq> h \<and> P hp \<and> hp' \<preceq> h \<and> P hp' \<longrightarrow> hp = hp')" 1047 1048lemma "precise ((=) s)" 1049 by (metis (full_types) precise_def) 1050 1051lemma sep_add_cancel: 1052 "x ## z \<Longrightarrow> y ## z \<Longrightarrow> (x + z = y + z) = (x = y)" 1053 by (metis sep_add_cancelD) 1054 1055lemma precise_distribute: 1056 "precise P = (\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P)))" 1057proof (rule iffI) 1058 assume pp: "precise P" 1059 { 1060 fix Q R 1061 fix h hp hp' s 1062 1063 { assume a: "((Q and R) \<and>* P) s" 1064 hence "((Q \<and>* P) and (R \<and>* P)) s" 1065 by (fastforce dest!: sep_conjD elim: sep_conjI) 1066 } 1067 moreover 1068 { assume qs: "(Q \<and>* P) s" and qr: "(R \<and>* P) s" 1069 1070 from qs obtain x y where sxy: "s = x + y" and xy: "x ## y" 1071 and x: "Q x" and y: "P y" 1072 by (fastforce dest!: sep_conjD) 1073 from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'" 1074 and x': "R x'" and y': "P y'" 1075 by (fastforce dest!: sep_conjD) 1076 1077 from sxy have ys: "y \<preceq> x + y" using xy 1078 by (fastforce simp: sep_substate_disj_add' sep_disj_commute) 1079 from sxy' have ys': "y' \<preceq> x' + y'" using xy' 1080 by (fastforce simp: sep_substate_disj_add' sep_disj_commute) 1081 1082 from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys' 1083 by (fastforce simp: precise_def) 1084 1085 hence "x = x'" using sxy sxy' xy xy' 1086 by (fastforce dest!: sep_add_cancelD) 1087 1088 hence "((Q and R) \<and>* P) s" using sxy x x' yy y' xy' 1089 by (fastforce intro: sep_conjI) 1090 } 1091 ultimately 1092 have "((Q and R) \<and>* P) s = ((Q \<and>* P) and (R \<and>* P)) s" using pp by blast 1093 } 1094 thus "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" by blast 1095 1096next 1097 assume a: "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" 1098 thus "precise P" 1099 proof (clarsimp simp: precise_def) 1100 fix h hp hp' Q R 1101 assume hp: "hp \<preceq> h" and hp': "hp' \<preceq> h" and php: "P hp" and php': "P hp'" 1102 1103 obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp 1104 by (clarsimp simp: sep_substate_def) 1105 obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp' 1106 by (clarsimp simp: sep_substate_def) 1107 1108 have h_eq: "z' + hp' = z + hp" using hhp hhp' hpz hpz' 1109 by (fastforce simp: sep_add_ac) 1110 1111 from hhp hhp' a hpz hpz' h_eq 1112 have "\<forall>Q R. ((Q and R) \<and>* P) (z + hp) = ((Q \<and>* P) and (R \<and>* P)) (z' + hp')" 1113 by (fastforce simp: h_eq sep_add_ac sep_conj_commute) 1114 1115 hence "(((=) z and (=) z') \<and>* P) (z + hp) = 1116 (((=) z \<and>* P) and ((=) z' \<and>* P)) (z' + hp')" by blast 1117 1118 thus "hp = hp'" using php php' hpz hpz' h_eq 1119 by (fastforce dest!: iffD2 cong: conj_cong 1120 simp: sep_add_ac sep_add_cancel sep_conj_def) 1121 qed 1122qed 1123 1124lemma strictly_precise: "strictly_exact P \<Longrightarrow> precise P" 1125 by (metis precise_def strictly_exactD) 1126 1127lemma sep_disj_positive_zero[simp]: "x ## y \<Longrightarrow> x + y = 0 \<Longrightarrow> x = 0 \<and> y = 0" 1128 by (metis (full_types) disjoint_zero_sym sep_add_cancelD sep_add_disjD 1129 sep_add_zero_sym sep_disj_positive) 1130 1131end 1132 1133end