1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 Adds positivity law to separation algebra, as well as defining 9 the septraction and sep-coimplication operators, providing lemmas 10 for each. 11*) 12 13theory Extended_Separation_Algebra 14imports 15 Lib.Lib 16 "Sep_Tactics" 17begin 18 19no_notation pred_and (infixr "and" 35) 20no_notation pred_or (infixr "or" 30) 21no_notation pred_not ("not _" [40] 40) 22no_notation pred_imp (infixr "imp" 25) 23 24lemma sep_conj_exists_left[simp]: "((\<lambda>s. \<exists>x. (P x) s) \<and>* R) \<equiv> (EXS x. (P x \<and>* R)) " 25 apply (rule eq_reflection) 26 by (clarsimp simp: sep_conj_def, fastforce) 27 28instantiation "bool" :: stronger_sep_algebra 29begin 30 definition "zero_bool \<equiv> True" 31 definition "plus_bool \<equiv> \<lambda>(x :: bool) (y :: bool). x \<and> y" 32 definition "sep_disj_bool \<equiv> \<lambda>(x :: bool) (y :: bool). x \<or> y" 33instance 34 by (intro_classes; fastforce simp: zero_bool_def plus_bool_def sep_disj_bool_def) 35end 36 37instantiation "prod" :: (stronger_sep_algebra, stronger_sep_algebra) stronger_sep_algebra 38begin 39definition "zero_prod \<equiv> (0,0)" 40definition "plus_prod p p' \<equiv> (fst p + fst p', snd p + snd p')" 41definition "sep_disj_prod p p' \<equiv> fst p ## fst p' \<and> snd p ## snd p'" 42instance 43 apply (intro_classes; simp add: zero_prod_def plus_prod_def sep_disj_prod_def) 44 apply (simp add: sep_add_assoc | fastforce simp: sep_disj_commute sep_add_commute)+ 45 done 46end 47 48 49instantiation "fun" :: (type, pre_sep_algebra) pre_sep_algebra 50begin 51definition "zero_fun = (\<lambda>x. 0)" 52definition "plus_fun f f' \<equiv> (\<lambda>x. (f x) + (f' x) )" 53definition "sep_disj_fun \<equiv> (\<lambda>f f'. \<forall>x. f x ## f' x ) :: ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool " 54instance 55 apply (intro_classes) 56 apply (clarsimp simp: comp_def sep_disj_fun_def ) 57 apply (clarsimp simp: zero_fun_def sep_disj_fun_def plus_fun_def ) 58 apply (clarsimp simp: zero_fun_def comp_def sep_disj_fun_def plus_fun_def ) 59 apply (simp add: sep_disj_commute) 60 apply (clarsimp simp: zero_fun_def sep_disj_commuteI sep_disj_fun_def plus_fun_def) 61 apply (clarsimp simp: zero_fun_def sep_disj_commuteI sep_disj_fun_def plus_fun_def sep_add_commute) 62 apply (clarsimp simp: zero_fun_def sep_disj_commuteI sep_disj_fun_def plus_fun_def sep_add_commute sep_add_assoc) 63 done 64end 65 66instantiation "fun" :: (type, sep_algebra) sep_algebra 67begin 68 69instance 70 apply (intro_classes) 71 apply (clarsimp simp: zero_fun_def sep_disj_fun_def plus_fun_def ) 72 using sep_disj_addD apply blast 73 apply (clarsimp simp: zero_fun_def comp_def sep_disj_fun_def plus_fun_def ) 74 by (simp add: sep_disj_addI1) 75end 76 77instantiation option :: (type) sep_algebra begin 78definition "sep_disj_option (h :: 'a option) (h' :: 'a option) = 79 (case h of (Some x) \<Rightarrow> h' = None | _ \<Rightarrow> h = None)" 80definition "plus_option (h :: 'a option) (h' :: 'a option) = 81 (case h of (Some x) \<Rightarrow> h | _ \<Rightarrow> h')" 82definition "zero_option = None" 83instance 84 apply (intro_classes) 85 by (clarsimp simp: sep_disj_option_def zero_option_def plus_option_def split: option.splits)+ 86end 87 88instantiation option :: (type) cancellative_sep_algebra begin 89instance 90 apply (intro_classes) 91 apply (simp add: option.case_eq_if plus_option_def sep_disj_option_def) 92 apply (clarsimp simp: zero_option_def option.case_eq_if plus_option_def sep_disj_option_def split: if_split_asm option.splits) 93 apply (clarsimp simp: zero_option_def option.case_eq_if plus_option_def sep_disj_option_def split: if_split_asm option.splits) 94 done 95end 96 97 98instantiation "fun" :: (type, cancellative_sep_algebra) cancellative_sep_algebra begin 99instance 100 apply (intro_classes) 101 apply (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def) 102 apply (safe; fastforce) 103 apply (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def) 104 apply (rule ext) 105 apply (meson sep_disj_positive) 106 apply (rule ext) 107 apply (clarsimp simp: plus_fun_def sep_disj_fun_def zero_fun_def) 108 by (meson sep_add_cancel) 109end 110 111 112lemma sep_substate_antisym: 113 "x \<preceq> y \<Longrightarrow> y \<preceq> x \<Longrightarrow> x = (y :: 'a ::cancellative_sep_algebra)" 114 apply (clarsimp simp: sep_substate_def) 115 apply (rename_tac h' h) 116 apply (subgoal_tac "h' = 0") 117 apply (clarsimp) 118 apply (drule_tac trans[where s=x and t="x+0"]) 119 apply (clarsimp) 120 apply (subgoal_tac "(x + h' + h = x + 0) \<longrightarrow> ((0 + x) = (h' + h) + x)") 121 apply (drule mp, clarsimp) 122 apply (metis sep_add_cancelD sep_add_disj_eq sep_disj_commuteI sep_disj_positive_zero sep_disj_zero) 123 by (metis sep_add_assoc sep_add_commute sep_add_zero sep_add_zero_sym sep_disj_commuteI) 124 125context sep_algebra begin 126 127definition 128 septraction :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infix "-*" 25) 129where 130 "septraction P Q = (not (P \<longrightarrow>* not Q))" 131 132 133lemma septraction_impl1: 134 "(P -* Q) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (P' -* Q) s " 135 apply (clarsimp simp: septraction_def pred_neg_def) 136 using sep_impl_def by auto 137 138lemma septraction_impl2: 139 "(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P -* Q') s " 140 apply (clarsimp simp: septraction_def pred_neg_def) 141 using sep_impl_def by auto 142 143definition 144 sep_coimpl :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infix "\<leadsto>*" 24) 145where 146 "sep_coimpl P Q \<equiv> \<lambda>s. \<not> (P \<and>* not Q) s" 147 148lemma sep_septraction_snake: 149 "(P -* Q) s \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> (P \<leadsto>* Q') s) \<Longrightarrow> Q' s" 150 apply (clarsimp simp: sep_coimpl_def septraction_def pred_neg_def sep_conj_def sep_impl_def) 151 using sep_add_commute sep_disj_commute by auto 152 153lemma sep_snake_septraction: 154 "Q s \<Longrightarrow> (\<And>s. (P -* Q) s \<Longrightarrow> Q' s) \<Longrightarrow> (P \<leadsto>* Q') s " 155 apply (clarsimp simp: sep_coimpl_def septraction_def pred_neg_def sep_conj_def sep_impl_def) 156 using sep_add_commute sep_disj_commute by fastforce 157 158lemma septraction_snake_trivial: 159 "(P -* (P \<leadsto>* R)) s \<Longrightarrow> R s" by (erule sep_septraction_snake) 160 161end 162 163 164lemma sep_impl_impl: 165 "(P \<longrightarrow>* Q) s\<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P \<longrightarrow>* Q') s" 166 by (metis sep_implD sep_implI) 167 168lemma disjointness_equiv: 169 "(\<forall>P (s :: 'a :: sep_algebra). strictly_exact P \<longrightarrow> \<not>P 0 \<longrightarrow> (P \<leadsto>* (P \<leadsto>* sep_false)) s) = 170 (\<forall>h :: 'a. h ## h \<longrightarrow> h = 0)" 171 apply (rule iffI) 172 apply (clarsimp) 173 apply (erule_tac x="(=) h" in allE) 174 apply (drule mp) 175 apply (clarsimp simp: strictly_exact_def) 176 apply (rule ccontr) 177 apply (drule mp) 178 apply (clarsimp) 179 apply (erule_tac x="h + h" in allE) 180 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) 181 apply (erule_tac x=h in allE, clarsimp) 182 apply (erule_tac x=0 in allE, clarsimp) 183 apply (clarsimp) 184 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def strictly_exact_def) 185 apply (erule_tac x=x in allE, erule_tac x=xa in allE, clarsimp simp: sep_empty_def) 186 apply (erule_tac x=x in allE, clarsimp) 187 using sep_disj_addD1 by blast 188 189 190definition 191 sep_min :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" where 192 "sep_min P \<equiv> P and (P \<leadsto>* \<box>)" 193 194definition 195 sep_subtract :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" where 196 "sep_subtract P Q \<equiv> P and (Q \<leadsto>* \<box>)" 197 198lemma sep_min_subtract_subtract: 199 "sep_min P = sep_subtract P P" 200 apply (clarsimp simp: sep_subtract_def sep_min_def) 201 done 202 203lemma sep_subtract_distrib_disj: 204 "sep_subtract (P or Q) R = ((sep_subtract P R) or (sep_subtract Q R))" 205 apply (rule ext, rule iffI) 206 apply (clarsimp simp: pred_disj_def pred_conj_def sep_subtract_def) 207 apply (clarsimp simp: pred_disj_def pred_conj_def sep_subtract_def) 208 apply (safe) 209 done 210 211lemma sep_snake_sep_impl: 212 "(P \<longrightarrow>* R) s \<Longrightarrow> (\<And> s. R s \<Longrightarrow> (P \<leadsto>* sep_false) s) \<Longrightarrow> (not P \<and>* (not (P -* R))) s" 213 apply (drule sep_impl_impl[where Q'="(P \<leadsto>* sep_false)"]) 214 apply (atomize) 215 apply (erule allE, drule mp, assumption) 216 apply (assumption) 217 apply (erule contrapos_pp) 218 apply (clarsimp simp: sep_impl_def sep_coimpl_def sep_conj_def pred_neg_def septraction_def) 219 apply (erule_tac x=0 in allE) 220 apply (erule_tac x=s in allE) 221 apply (clarsimp) 222 apply (rule_tac x=0 in exI) 223 apply (clarsimp) 224 by (metis (full_types) disjoint_zero_sym sep_add_commute sep_add_zero_sym sep_disj_commuteI) 225 226lemma sep_snake_mp: 227 "(P \<leadsto>* Q) s \<Longrightarrow> (P \<and>* sep_true) s \<Longrightarrow> (P \<and>* Q) s " 228 apply (clarsimp simp: sep_coimpl_def) 229 apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) 230 apply (fastforce) 231 done 232 233lemma sep_coimpl_contrapos: 234 "(P \<leadsto>* Q) = ((not Q) \<leadsto>* (not P))" 235 by (rule ext, rule iffI; simp add: sep_coimpl_def pred_neg_def sep_conj_commute) 236 237lemma sep_coimpl_def': 238 "(\<not> (P \<and>* Q) s) = ((P \<leadsto>* (not Q)) s)" 239 by (simp add: pred_neg_def sep_coimpl_def) 240 241lemma rewrite_sp: 242 "(\<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s)) \<longleftrightarrow> (\<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) )" 243 apply (rule iffI) 244 apply (clarsimp) 245 apply (erule_tac x="P -* R" in allE) 246 apply (erule_tac x=s in allE) 247 apply (drule mp) 248 apply (erule (1) sep_snake_septraction) 249 apply (assumption) 250 apply (clarsimp) 251 apply (erule_tac x="P \<leadsto>* R" in allE) 252 apply (erule_tac x=s in allE) 253 apply (clarsimp) 254 apply (sep_cancel) 255 apply (erule (1) sep_septraction_snake) 256 done 257 258lemma sep_coimpl_weaken: 259 "(P \<leadsto>* Q) s \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> (P' \<leadsto>* Q) s" 260 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) 261 apply (fastforce) 262 done 263 264lemma sep_curry': 265 "R s \<Longrightarrow> (P \<longrightarrow>* (P \<and>* R)) s" 266 by (simp add: sep_wand_trivial) 267 268lemma sep_coimpl_mp_gen: 269 "(P \<and>* Q) s \<Longrightarrow> (P' \<leadsto>* Q') s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> ((P and P') \<and>* (Q and Q')) s" 270 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_conj_def pred_neg_def) 271 by (fastforce simp: sep_disj_commute sep_add_commute) 272 273lemma ex_pull: 274 "\<exists>h s. P h s \<and> Q h \<Longrightarrow> \<exists>h. Q h \<and> (\<exists>s. P h s)" 275 apply (fastforce) 276 done 277 278lemma sep_mp_snake_mp: 279 "(P \<and>* (P \<longrightarrow>* (P \<leadsto>* Q))) s \<Longrightarrow> (P \<and>* Q) s" 280 apply (clarsimp simp: sep_conj_def) 281 apply (rename_tac x y) 282 apply (rule_tac x=x in exI) 283 apply (rule_tac x=y in exI) 284 apply (clarsimp) 285 apply (clarsimp simp: sep_impl_def) 286 apply (erule_tac x=x in allE) 287 apply (clarsimp simp: sep_disj_commute) 288 apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) 289 by (fastforce simp: sep_disj_commute sep_add_commute) 290 291lemma septract_cancel: 292 "(P -* Q) s \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<And>s. Q s \<Longrightarrow> Q' s) \<Longrightarrow> (P' -* Q') s" 293 apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def) 294 apply (fastforce) 295 done 296 297lemma sep_coimpl_mp_zero: 298 "(P \<leadsto>* Q) s \<Longrightarrow> P s \<Longrightarrow> Q (0)" 299 apply (clarsimp simp: sep_coimpl_def sep_conj_def) 300 apply (erule_tac x=s in allE) 301 apply (clarsimp, erule_tac x="0" in allE) 302 apply (clarsimp simp: pred_neg_def) 303 done 304 305lemma sep_neg_not: 306 "(P \<leadsto>* sep_false) s \<Longrightarrow> \<not>P s" 307 apply (cases "P s") 308 apply (drule(1) sep_coimpl_mp_zero) 309 apply (clarsimp) 310 apply (simp) 311 done 312 313lemma sep_antimp': 314 "P s \<Longrightarrow> (Q \<leadsto>* (Q -* P)) s \<and> P s" 315 apply (clarsimp) 316 apply (erule sep_snake_septraction, assumption) 317 done 318 319definition 320 sep_precise_conj :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" where 321 "sep_precise_conj P \<equiv> P and (ALLS R. (sep_true \<longrightarrow>* (P \<leadsto>* R)))" 322 323notation sep_precise_conj (infix "\<and>@" 50) 324 325definition 326 coprecise :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> bool" where 327 "coprecise P = (\<forall>s h h'. P h \<longrightarrow> P h' \<longrightarrow> s \<preceq> h \<longrightarrow> s \<preceq> h' \<longrightarrow> s \<noteq> 0 \<longrightarrow> h = h')" 328 329definition 330 cointuitionistic :: "(('a :: sep_algebra) \<Rightarrow> bool) \<Rightarrow> bool" where 331 "cointuitionistic P = (\<forall>h h'. P h \<and> h' \<preceq> h \<longrightarrow> P h')" 332 333lemma intuitionistic_def': 334 "intuitionistic P = (\<forall>s R. (P \<and>* R) s \<longrightarrow> P s)" 335 apply (rule iffI) 336 apply (clarsimp simp: intuitionistic_def) 337 apply (clarsimp simp: sep_conj_def) 338 using sep_substate_disj_add apply blast 339 apply (clarsimp simp: intuitionistic_def) 340 apply (erule_tac x=h' in allE) 341 apply (drule mp) 342 apply (rule_tac x=sep_true in exI) 343 apply (clarsimp simp:sep_conj_def sep_substate_def, fastforce) 344 apply (assumption) 345 done 346 347lemma cointuitionistic_def': 348 "cointuitionistic P = (\<forall>s R. P s \<longrightarrow> (R \<leadsto>* P) s)" 349 apply (rule iffI) 350 apply (clarsimp) 351 apply (clarsimp simp: sep_coimpl_def) 352 apply (clarsimp simp: sep_conj_def pred_neg_def cointuitionistic_def) 353 apply (rename_tac R x y) 354 apply (erule_tac x="x + y" in allE) 355 apply (erule_tac x=y in allE) 356 apply (clarsimp) 357 using sep_disj_commuteI sep_substate_disj_add' apply blast 358 apply (clarsimp simp: cointuitionistic_def) 359 apply (erule_tac x=h in allE) 360 apply (clarsimp) 361 apply (clarsimp simp: sep_substate_def) 362 apply (erule_tac x="\<lambda>s. s = z" in allE) 363 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) 364 apply (fastforce simp: sep_disj_commute sep_add_commute) 365 done 366 367lemma saturated_split: 368 "cointuitionistic P \<Longrightarrow> P s \<Longrightarrow> (Q \<and>* R) s \<Longrightarrow> ((P and Q) \<and>* (P and R)) s" 369 apply (clarsimp simp: cointuitionistic_def sep_conj_def pred_conj_def) 370 apply (rule_tac x=x in exI) 371 apply (rule_tac x=y in exI) 372 apply (clarsimp) 373 using sep_disj_commuteI sep_substate_disj_add sep_substate_disj_add' by blast 374 375lemma sep_wand_dne: 376 "((P \<longrightarrow>* sep_false) \<longrightarrow>* sep_false) s \<Longrightarrow> \<exists>s. P s" 377 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def) 378 apply (erule_tac x=0 in allE) 379 apply (clarsimp) 380 done 381 382lemma sep_snake_dne: 383 "(sep_true \<leadsto>* P) s \<Longrightarrow> ((P \<leadsto>* sep_false) \<leadsto>* sep_false) s" 384 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def) 385 apply (rename_tac x y) 386 apply (erule_tac x=y in allE) 387 apply (erule_tac x=x in allE) 388 apply (rule_tac x=x in exI) 389 apply (rule_tac x=0 in exI) 390 apply (clarsimp) 391 apply (fastforce simp: sep_disj_commute sep_add_commute) 392 done 393 394lemma strictly_exactI: 395 "(\<And>P s. ((P -* R) -* R) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)) \<Longrightarrow> strictly_exact R" 396 apply (atomize) 397 apply (clarsimp simp: strictly_exact_def) 398 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def strictly_exact_def) 399 apply (rename_tac h h') 400 apply (erule_tac x="\<lambda>s. s = h" in allE) 401 by (metis disjoint_zero_sym sep_add_commute sep_add_zero sep_disj_zero) 402 403lemma strictly_exact_septractD: 404 "strictly_exact R \<Longrightarrow> ((P -* R) -* R) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)" 405 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_conj_def sep_coimpl_def 406 strictly_exact_def) 407 by (metis sep_add_cancel sep_add_commute sep_disj_commuteI) 408 409lemma strictly_exact_def': 410 "(\<forall>P s. ((P -* R) -* R) s \<longrightarrow> P (s :: 'a :: cancellative_sep_algebra)) = strictly_exact R" 411 using strictly_exactI strictly_exact_septractD by auto 412 413lemma copreciseI: 414 "(\<forall>(s ) R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) \<Longrightarrow> coprecise P" 415 apply (clarsimp simp: coprecise_def) 416 apply (clarsimp simp: sep_substate_def) 417 apply (erule_tac x="0" in allE) 418 apply (rename_tac s h h') 419 apply (erule_tac x="\<lambda>s'. s' = s + h" in allE) 420 apply (drule mp) 421 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) 422 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) 423 done 424 425lemma sep_implI': 426 "strictly_exact P \<Longrightarrow> (P -* R) s \<Longrightarrow> (P \<longrightarrow>* R) s" 427 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def coprecise_def strictly_exact_def) 428 apply (fastforce) 429 done 430 431lemma 432 "\<forall>s P. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> \<exists>s. R s \<Longrightarrow> R s" 433 apply (clarsimp simp: coprecise_def) 434 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) 435 by (metis disjoint_zero_sym sep_add_zero_sym) 436 437lemma strictly_exactI': 438 "\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s \<Longrightarrow> strictly_exact P" 439 apply (clarsimp simp: strictly_exact_def) 440 apply (erule_tac x="0" in allE) 441 apply (rename_tac h h') 442 apply (erule_tac x="\<lambda>h. h = h'" in allE) 443 apply (drule mp) 444 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) 445 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) 446 done 447 448lemma strictly_exact_def'': 449 "(\<forall>s R. (P -* R) s \<longrightarrow> (P \<longrightarrow>* R) s) = strictly_exact P" 450 using sep_implI' strictly_exactI' by blast 451 452lemma conj_coimpl_precise: 453 "(\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s) \<Longrightarrow> precise P" 454 apply (clarsimp simp: precise_def) 455 apply (clarsimp simp: sep_substate_def) 456 apply (rename_tac h h' z z') 457 apply (erule_tac x="h + z" in allE) 458 apply (erule_tac x="\<lambda>s. s= z" in allE) 459 apply (drule mp) 460 apply (clarsimp simp: sep_conj_def) 461 apply (fastforce) 462 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) 463 using sep_add_cancel by fastforce 464 465lemma precise_conj_coimpl: 466 "precise P \<Longrightarrow> (\<forall>s R. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s)" 467 apply (clarsimp simp: precise_def) 468 apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def) 469 by (metis cancellative_sep_algebra_class.sep_add_cancelD sep_add_commute 470 sep_disj_commuteI sep_substate_disj_add) 471 472lemma septract_cancel_eq_precise: 473 "(\<forall>s. ((P -* (P \<and>* R)) s \<longrightarrow> R s)) = (\<forall>s. (P \<and>* R) s \<longrightarrow> (P \<leadsto>* R) s)" 474 apply (rule iffI) 475 apply (clarsimp) 476 apply (clarsimp simp: sep_conj_def sep_impl_def septraction_def pred_neg_def sep_coimpl_def) 477 apply (rule ccontr) 478 apply (rename_tac x y h h') 479 apply (erule_tac x=h' in allE) 480 apply (clarsimp) 481 apply (erule_tac x=h in allE) 482 apply (clarsimp simp: sep_disj_commute) 483 apply (erule_tac x=x in allE) 484 apply (clarsimp) 485 apply (erule_tac x=y in allE) 486 apply (clarsimp) 487 apply (fastforce simp: sep_disj_commute sep_add_commute) 488 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def) 489 by (metis pred_neg_def sep_coimpl_def sep_conjI sep_conj_commuteI) 490 491lemma sep_coimpl_cancel: 492 "(P \<leadsto>* Q) s \<Longrightarrow> ((P \<and>* Q) s \<Longrightarrow> (P \<leadsto>* Q') s) \<Longrightarrow> (P \<leadsto>* Q') s" 493 apply (clarsimp simp: sep_coimpl_def pred_neg_def) 494 apply (clarsimp simp: sep_conj_def) 495 by blast 496 497lemma sep_cases: 498 "R s \<Longrightarrow> (P \<and>* (P -* R)) s \<or> (P \<leadsto>* (sep_false)) s" 499 apply (safe) 500 apply (clarsimp simp: sep_coimpl_def) 501 apply (rule ccontr) 502 by (meson sep_antimp' sep_conj_sep_true_right sep_snake_mp) 503 504lemma contra: 505 "(\<forall>s. P s \<longrightarrow> Q s) \<Longrightarrow> (\<forall>s. \<not> Q s \<longrightarrow> \<not> P s )" 506 apply (safe) 507 by (fastforce) 508 509lemma 510 "(\<forall>R s. (P \<and>* R) (s) \<longrightarrow> (Q \<and>* R) (f s) ) = (\<forall>R s. (Q \<leadsto>* R) (f s) \<longrightarrow> (P \<leadsto>* R) ( s))" 511 apply (clarsimp simp: sep_coimpl_def) 512 apply (rule iffI) 513 apply (clarsimp) 514 apply (clarsimp) 515 by (meson sep_coimpl_def sep_coimpl_def') 516 517lemma 518 "R s \<Longrightarrow> strictly_exact R \<Longrightarrow> (P \<longrightarrow>* R) s' \<Longrightarrow> (P -* R) s' \<Longrightarrow> s' \<preceq> s \<Longrightarrow> (P \<and>* sep_true) s" 519 apply (clarsimp simp: sep_conj_def sep_coimpl_def pred_neg_def septraction_def sep_impl_def) 520 by (metis sep_add_commute sep_disj_commuteI strictly_exact_def) 521 522lemma sep_coimpl_comb: 523 " (R \<leadsto>* P) s \<Longrightarrow> (R \<leadsto>* Q) s \<Longrightarrow> (R \<leadsto>* (P and Q)) s" 524 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def pred_conj_def) 525 done 526 527lemma sep_coimpl_contra: 528 "(R \<leadsto>* (not Q)) s \<Longrightarrow> (R \<leadsto>* Q) s \<Longrightarrow> (R \<leadsto>* sep_false) s" 529 apply (drule sep_coimpl_comb, assumption) 530 apply (clarsimp simp: pred_neg_def pred_conj_def) 531 done 532 533lemma sep_comb': 534 "((not Q) \<leadsto>* P) s \<Longrightarrow> (Q \<leadsto>* R) s \<Longrightarrow> ((R or P) \<and>* sep_true) s" 535 apply (clarsimp simp: sep_coimpl_def sep_conj_def pred_neg_def) 536 by (metis (full_types) disjoint_zero_sym pred_disj_def sep_add_zero sep_add_zero_sym sep_disj_zero) 537 538lemma sep_coimpl_dne: 539 "((R \<leadsto>* sep_false) \<leadsto>* sep_false) s \<Longrightarrow> (R \<and>* sep_true) s" 540 by (metis sep_coimpl_def sep_conj_sep_true_right sep_neg_not) 541 542lemma sep_antimp_contrapos: 543 " (R) s \<Longrightarrow> ((P \<longrightarrow>* not R) \<leadsto>* (not P)) s " 544 by (metis pred_neg_def sep_coimpl_def' sep_mp_gen) 545 546lemma sep_snake_trivial: 547 "(sep_true \<leadsto>* Q) s \<Longrightarrow> Q s" 548 by (metis pred_neg_def sep_coimpl_def sep_conj_sep_true') 549 550lemma min_predD: 551 "(R \<leadsto>* \<box>) s \<Longrightarrow> (R \<and>* sep_true) s \<Longrightarrow> R s" 552 using Sep_Cancel_Set.sep_conj_empty' sep_coimpl_dne sep_snake_mp by blast 553 554lemma septract_sep_wand: 555 "(P -* R) s \<Longrightarrow> (P \<longrightarrow>* Q) s \<Longrightarrow> (P -* (Q and R)) s" 556 apply (clarsimp simp: sep_impl_def septraction_def pred_neg_def) 557 by (fastforce simp: pred_conj_def) 558 559lemma 560 "(P -* (P \<and>* R)) s \<Longrightarrow> (P \<longrightarrow>* Q) s \<Longrightarrow> (\<And>s. (Q and (P \<and>* R)) s \<Longrightarrow> (P \<leadsto>* R) s) \<Longrightarrow> R s" 561 using sep_septraction_snake septract_sep_wand by blast 562 563lemma sep_elsewhereD: 564 "(P -* sep_true) s \<Longrightarrow> (P \<longrightarrow>* (P \<leadsto>* R)) s \<Longrightarrow> R s" 565 apply (drule (1) septract_sep_wand, simp add: pred_conj_def) 566 using sep_septraction_snake by blast 567 568lemma sep_conj_coimplI: 569 "(Q \<leadsto>* R) s \<Longrightarrow> ((P \<and>* Q) \<leadsto>* (P -* R)) s " 570 by (metis sep_coimpl_def sep_coimpl_def' sep_conj_commuteI sep_mp_frame septraction_def) 571 572lemma sep_conj_septract_curry: 573 "((P \<and>* Q) -* R) s \<Longrightarrow> (P -* (Q -* R)) s" 574 by (smt sep_antimp' sep_conj_coimplI sep_septraction_snake) 575 576lemma sep_snake_boxI: 577 "Q s \<Longrightarrow> (\<box> \<leadsto>* Q) s" 578 by (simp add: pred_neg_def sep_coimpl_def) 579 580lemma sep_snake_boxD: 581 "(Q \<leadsto>* \<box>) s \<Longrightarrow> ((Q \<leadsto>* sep_false) or Q) s" 582 apply (simp only: pred_disj_def) 583 apply (safe) 584 using Sep_Cancel_Set.sep_conj_empty' sep_coimpl_cancel by blast 585 586lemma septract_wandD: 587 "(( R \<longrightarrow>* (not Q)) -* Q) s \<Longrightarrow> (not R) s" 588 apply (erule sep_septraction_snake) 589 by (simp add: sep_antimp_contrapos) 590 591lemma sep_impl_septractD: 592 "(P \<longrightarrow>* Q) s \<Longrightarrow> (R -* (not Q)) s \<Longrightarrow> ((R and not P) -* (not Q)) s" 593 apply (clarsimp simp: sep_impl_def pred_neg_def septraction_def) 594 apply (erule_tac x=h' in allE) 595 apply (clarsimp simp: pred_conj_def) 596 apply (fastforce) 597 done 598 599lemma sep_neg_impl: 600 "(not (R \<longrightarrow>* Q)) = (R -* (not Q)) " 601 apply (clarsimp simp: pred_neg_def septraction_def) 602 done 603 604lemma 605 "P s \<Longrightarrow> (R -* Q) s \<Longrightarrow> ((R and (P -* Q)) -* Q) s" 606 apply (clarsimp simp: septraction_def sep_impl_def pred_neg_def pred_conj_def) 607 by (fastforce simp: sep_add_commute sep_disj_commute) 608 609lemma sep_coimpl_notempty: 610 "(Q \<leadsto>* (not \<box>)) s \<Longrightarrow> (not Q) s" 611 apply (clarsimp simp: sep_coimpl_def pred_neg_def) 612 done 613 614method sep_subst uses add = (sep_frule (direct) add) 615 616lemma septract_empty_empty: 617 "(P -* \<box>) s \<Longrightarrow> \<box> (s :: 'a :: cancellative_sep_algebra)" 618 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_empty_def) 619 done 620 621lemma septract_trivial: 622 "P s \<Longrightarrow> (sep_true -* P) s" 623 apply (clarsimp simp: septraction_def pred_neg_def sep_impl_def sep_empty_def) 624 using sep_disj_zero by fastforce 625 626lemma sep_empty_and_conj: 627 "\<box> s \<Longrightarrow> (P \<and>* Q) s \<Longrightarrow> P (s :: 'a :: cancellative_sep_algebra)" 628 by (metis sep_conj_def sep_disj_positive_zero sep_empty_def) 629 630lemma sep_conj_coimpl_mp: 631 "(P \<and>* R) s \<Longrightarrow> (P \<leadsto>* Q) s \<Longrightarrow> (P \<and>* (Q and R)) s" 632 apply (drule (2) sep_coimpl_mp_gen, clarsimp simp: pred_conj_def conj_commute) 633 done 634 635lemma sep_conj_coimpl_contrapos_mp: 636 "(P \<and>* Q) s \<Longrightarrow> (R \<leadsto>* (not Q)) s \<Longrightarrow> (Q \<and>* (P and (not R))) s" 637 apply (subst (asm) sep_coimpl_contrapos) 638 apply (clarsimp simp: pred_neg_def) 639 apply (sep_drule (direct) sep_conj_coimpl_mp[where P=Q], assumption) 640 apply (clarsimp simp: pred_conj_def conj_commute) 641 done 642 643end