1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 * A theoretical framework for reasoning about non-interference 9 * of monadic programs. 10 *) 11 12theory EquivValid 13imports Corres_UL 14begin 15 16section\<open>State equivalence validity\<close> 17 18text\<open> 19 20A generalised information flow property. 21 22Often, we read in the entire state, but then only examine part of it. 23The following property may be used to split up binds whose first part 24does this. 25 26@{term "I"} is the state relation that holds invariantly. 27 28@{term "A"} (also) holds between initial states. 29 30@{term "B"} (also) holds between final states. 31 32@{term "P"} holds in the initial state for @{term "f"}. 33 34@{term "P'"} holds in the initial state for @{term "f'"}. 35 36\<close> 37 38definition 39 equiv_valid_2 :: "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s,'b) nondet_monad \<Rightarrow> ('s,'c) nondet_monad \<Rightarrow> bool" 40where 41 "equiv_valid_2 I A B R P P' f f' \<equiv> \<forall>s t. 42 P s \<and> P' t \<and> I s t \<and> A s t 43 \<longrightarrow> (\<forall>(rva, s') \<in> fst (f s). \<forall>(rvb, t') \<in> fst (f' t). 44 R rva rvb \<and> I s' t' \<and> B s' t')" 45 46lemma equiv_valid_2_bind_general: 47 assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D B C R (Q rv) (Q' rv') (g rv) (g' rv')" 48 assumes r1: "equiv_valid_2 D A B R' P P' f f'" 49 assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" 50 assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>" 51 shows "equiv_valid_2 D A C R (\<lambda> s. P s \<and> S s) (\<lambda> s. P' s \<and> S' s) (f >>= g) (f' >>= g')" 52 using assms 53 unfolding bind_def equiv_valid_2_def valid_def 54 apply fastforce 55 done 56 57(* almost all of the time, the second relation doesn't change *) 58lemma equiv_valid_2_bind: 59 assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')" 60 assumes r1: "equiv_valid_2 D A A R' P P' f f'" 61 assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" 62 assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>" 63 shows "equiv_valid_2 D A A R (\<lambda> s. P s \<and> S s) (\<lambda> s. P' s \<and> S' s) (f >>= g) (f' >>= g')" 64 using assms by (blast intro: equiv_valid_2_bind_general) 65 66lemma equiv_valid_2_guard_imp: 67 assumes reads_res: "equiv_valid_2 D A B R Q Q' f f'" 68 assumes guard_imp: "\<And> s. P s \<Longrightarrow> Q s" 69 assumes guard_imp': "\<And> s. P' s \<Longrightarrow> Q' s" 70 shows "equiv_valid_2 D A B R P P' f f'" 71 using assms 72 by (fastforce simp: equiv_valid_2_def) 73 74lemma equiv_valid_2_bind_pre: 75 assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')" 76 assumes r1: "equiv_valid_2 D A A R' P P' f f'" 77 assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" 78 assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>" 79 assumes guard_imp: "\<And> s. T s \<Longrightarrow> P s \<and> S s" 80 assumes guard_imp': "\<And> s. T' s \<Longrightarrow> P' s \<and> S' s" 81 shows "equiv_valid_2 D A A R T T' (f >>= g) (f' >>= g')" 82 using assms by (blast intro: equiv_valid_2_bind[THEN equiv_valid_2_guard_imp]) 83 84lemma return_ev2: 85 assumes rel: "\<And> s t. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R a b" 86 shows "equiv_valid_2 I A A R P P' (return a) (return b)" 87 by(auto simp: equiv_valid_2_def return_def rel) 88 89lemma equiv_valid_2_liftE: 90 "equiv_valid_2 D A B R P P' f f' \<Longrightarrow> 91 equiv_valid_2 D A B (E \<oplus> R) P P' (liftE f) (liftE f')" 92 apply(unfold liftE_def) 93 apply(rule equiv_valid_2_guard_imp) 94 apply(rule_tac Q="\<top>\<top>" and Q'="\<top>\<top>" and R'=R in equiv_valid_2_bind_general) 95 apply(fastforce intro: return_ev2) 96 apply assumption 97 apply(rule wp_post_taut)+ 98 by(simp_all) 99 100lemma equiv_valid_2_liftE_bindE_general: 101 assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D B C R (Q rv) (Q' rv') (g rv) (g' rv')" 102 assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" 103 assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>" 104 assumes r1: "equiv_valid_2 D A B R' P P' f f'" 105 shows "equiv_valid_2 D A C R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g')" 106 apply(unfold bindE_def) 107 apply(rule equiv_valid_2_guard_imp) 108 apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" and Q'="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q' v s)" in equiv_valid_2_bind_general) 109 prefer 2 110 apply(rule_tac E="dc" in equiv_valid_2_liftE) 111 apply(rule r1) 112 apply(clarsimp simp: lift_def split: sum.split) 113 apply(insert r2, fastforce simp: equiv_valid_2_def)[1] 114 apply(simp add: liftE_def, wp, fastforce intro!: hoare_strengthen_post[OF hoare]) 115 apply(simp add: liftE_def, wp, fastforce intro!: hoare_strengthen_post[OF hoare']) 116 by(auto) 117 118lemma equiv_valid_2_liftE_bindE: 119 assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')" 120 assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" 121 assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>" 122 assumes r1: "equiv_valid_2 D A A R' P P' f f'" 123 shows "equiv_valid_2 D A A R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g')" 124 using assms by(blast intro: equiv_valid_2_liftE_bindE_general) 125 126lemma equiv_valid_2_rvrel_imp: 127 "\<lbrakk>equiv_valid_2 I A A R P P' f f'; \<And> s t. R s t \<Longrightarrow> R' s t\<rbrakk> \<Longrightarrow> 128 equiv_valid_2 I A A R' P P' f f'" 129 apply(fastforce simp: equiv_valid_2_def) 130 done 131 132subsection\<open>Specialised fixed-state state equivalence validity\<close> 133 134text\<open> 135 136For resolve_address_bits and rec_del: talk about a fixed initial 137state. Note we only do this for one of the computations; the other 138state can be constrained by how it is related to this one by @{term 139"I"} and so forth. 140 141Also captures the typical case where the relation between the return 142values is equality and the required preconditions are identical. 143 144wp can cope with this. 145 146\<close> 147 148definition 149 spec_equiv_valid :: "'s \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s,'b) nondet_monad \<Rightarrow> bool" 150where 151 "spec_equiv_valid st I A B P f \<equiv> equiv_valid_2 I A B (=) (P and ((=) st)) P f f" 152 153abbreviation spec_equiv_valid_inv where 154 "spec_equiv_valid_inv st I A P f \<equiv> spec_equiv_valid st I A A P f" 155 156subsection\<open>Specialised state equivalence validity\<close> 157 158text\<open> 159 160Most of the time we deal with the streamlined version. 161 162wp can cope with this too. 163 164\<close> 165 166definition 167 equiv_valid :: "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('s,'b) nondet_monad \<Rightarrow> bool" 168where 169 "equiv_valid I A B P f \<equiv> \<forall>st. spec_equiv_valid st I A B P f" 170 171lemma equiv_valid_def2: 172 "equiv_valid I A B P f = equiv_valid_2 I A B (=) P P f f" 173 by (simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def) 174 175abbreviation equiv_valid_rv where 176 "equiv_valid_rv I A B R P f \<equiv> equiv_valid_2 I A B R P P f f" 177 178(* this is probably way more general than we need for all but a few special cases *) 179lemma bind_ev_general: 180 assumes reads_res_2: "\<And>rv. equiv_valid I B C (Q rv) (g rv)" 181 assumes reads_res_1: "equiv_valid I A B P' f" 182 assumes hoare: "\<lbrace> P'' \<rbrace> f \<lbrace> Q \<rbrace>" 183 shows "equiv_valid I A C (\<lambda>s. P' s \<and> P'' s) (f >>= g)" 184 unfolding equiv_valid_def2 185 apply (rule equiv_valid_2_bind_general[where R'="(=)"]) 186 apply (auto intro: reads_res_1[unfolded equiv_valid_def2] reads_res_2[unfolded equiv_valid_def2])[2] 187 apply (rule hoare) 188 apply (rule hoare) 189 done 190 191lemma bind_ev: 192 assumes reads_res_2: "\<And>rv. equiv_valid I A A (Q rv) (g rv)" 193 assumes reads_res_1: "equiv_valid I A A P' f" 194 assumes hoare: "\<lbrace> P'' \<rbrace> f \<lbrace> Q \<rbrace>" 195 shows "equiv_valid I A A (\<lambda>s. P' s \<and> P'' s) (f >>= g)" 196 using assms by (blast intro: bind_ev_general) 197 198lemma equiv_valid_guard_imp: 199 assumes reads_res: "equiv_valid I A B Q f" 200 assumes guard_imp: "\<And> s. P s \<Longrightarrow> Q s" 201 shows "equiv_valid I A B P f" 202 using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def) 203 204lemmas bind_ev_pre = bind_ev[THEN equiv_valid_guard_imp] 205 206lemma gen_asm_ev': 207 assumes "Q \<Longrightarrow> equiv_valid D A B P f" 208 shows "equiv_valid D A B (P and K Q) f" 209 using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def) 210 211declare K_def [simp del] 212 213lemmas gen_asm_ev = 214 gen_asm_ev'[where P="\<top>", simplified] 215 gen_asm_ev' 216 gen_asm_ev'[simplified K_def, where P="\<top>", simplified] 217 gen_asm_ev'[simplified K_def] 218 219declare K_def [simp] 220 221text \<open> 222 This is a further streamlined version that we expect to get the most from 223 automating, and for the most part, we shouldn't need to deal with the 224 extra generality of the properties above. 225\<close> 226abbreviation equiv_valid_inv where 227 "equiv_valid_inv I A P f \<equiv> equiv_valid I A A P f" 228 229abbreviation equiv_valid_rv_inv where 230 "equiv_valid_rv_inv I A R P f \<equiv> equiv_valid_rv I A A R P f" 231 232lemma get_evrv: 233 "equiv_valid_rv_inv I A (I And A) \<top> get" 234 by(auto simp: equiv_valid_2_def get_def) 235 236lemma equiv_valid_rv_bind_general: 237 assumes ev1: 238 "equiv_valid_rv I A B W P f" 239 assumes ev2: 240 "\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I B C R (Q rv) (Q rv') (g rv) (g rv')" 241 assumes hoare: 242 "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>" 243 shows "equiv_valid_rv I A C R P (f >>= g)" 244 apply(rule equiv_valid_2_guard_imp) 245 apply(rule equiv_valid_2_bind_general[OF ev2]) 246 apply(assumption) 247 apply(rule ev1) 248 apply(rule hoare) 249 apply(rule hoare) 250 apply(simp_all) 251 done 252 253lemma equiv_valid_rv_bind: 254 assumes ev1: 255 "equiv_valid_rv_inv I A W P f" 256 assumes ev2: 257 "\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (Q rv) (Q rv') (g rv) (g rv')" 258 assumes hoare: 259 "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>" 260 shows "equiv_valid_rv_inv I A R P (f >>= g)" 261 using assms by(blast intro: equiv_valid_rv_bind_general) 262 263lemma modify_ev2: 264 assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I (f s) (f' t) \<and> B (f s) (f' t)" 265 shows 266 "equiv_valid_2 I A B R P P' (modify f) (modify f')" 267 apply(clarsimp simp: equiv_valid_2_def in_monad) 268 using assms by auto 269 270lemma modify_ev: 271 "equiv_valid I A B 272 (\<lambda> s. \<forall> s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) 273 (modify f)" 274 apply(clarsimp simp:equiv_valid_def2) 275 apply(rule modify_ev2) 276 by auto 277 278lemma modify_ev': 279 "equiv_valid I A B 280 (\<lambda> s. \<forall> t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) 281 (modify f)" 282 apply(clarsimp simp:equiv_valid_def2) 283 apply(rule modify_ev2) 284 by auto 285 286lemma modify_ev'': 287 assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P t\<rbrakk> \<Longrightarrow> I (f s) (f t) \<and> B (f s) (f t)" 288 shows "equiv_valid I A B P (modify f)" 289 apply(clarsimp simp:equiv_valid_def2) 290 apply(rule modify_ev2) 291 using assms by auto 292 293 294lemma put_ev2: 295 assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x'" 296 shows 297 "equiv_valid_2 I A B R P P' (put x) (put x')" 298 apply(clarsimp simp: equiv_valid_2_def in_monad) 299 using assms by auto 300 301 302lemma get_bind_ev2: 303 assumes "\<And> rv rv'. \<lbrakk>I rv rv'; A rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 I A B R (P and ((=) rv)) (P' and ((=) rv')) (f rv) (f' rv')" 304 shows "equiv_valid_2 I A B R P P' (get >>= f) (get >>= f')" 305 apply(rule equiv_valid_2_guard_imp) 306 apply(rule_tac R'="I And A" in equiv_valid_2_bind_general) 307 apply(rule assms, simp+) 308 apply(rule get_evrv) 309 apply(wp get_sp)+ 310 by(auto) 311 312 313lemma return_ev_pre: 314 "equiv_valid_inv I A P (return x)" 315 apply (simp add: equiv_valid_def2 return_ev2) 316 done 317 318lemmas return_ev = return_ev_pre[where P=\<top>] 319 320lemma fail_ev2_l: 321 "equiv_valid_2 I A B R P P' fail f'" 322 by(simp add: equiv_valid_2_def fail_def) 323 324lemma fail_ev2_r: 325 "equiv_valid_2 I A B R P P' f fail" 326 by(simp add: equiv_valid_2_def fail_def) 327 328lemma fail_ev_pre: 329 "equiv_valid I A B P fail" 330 apply (simp add: equiv_valid_def2 fail_ev2_l) 331 done 332 333lemmas fail_ev = fail_ev_pre[where P=\<top>] 334 335lemma assert_ev2: 336 "R () () \<Longrightarrow> equiv_valid_2 I A A R P P' (assert a) (assert b)" 337 apply(simp add: assert_def fail_ev2_l fail_ev2_r) 338 apply(blast intro: return_ev2) 339 done 340 341lemma liftE_ev: 342 "equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (liftE f)" 343 unfolding liftE_def 344 apply (rule bind_ev_general[THEN equiv_valid_guard_imp, OF return_ev _ wp_post_taut]) 345 apply fastforce+ (* schematic instantiation *) 346 done 347 348lemma if_ev: 349 assumes "b \<Longrightarrow> equiv_valid I A B P f" 350 assumes "\<not> b \<Longrightarrow> equiv_valid I A B Q g" 351 shows "equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) (if b then f else g)" 352 apply (clarsimp split: if_split) 353 using assms by blast 354 355lemmas if_ev_pre = equiv_valid_guard_imp[OF if_ev] 356 357lemma assert_ev_pre: 358 "equiv_valid_inv I A P (assert b)" 359 apply(simp add: equiv_valid_def2 assert_ev2) 360 done 361 362lemmas assert_ev = assert_ev_pre[where P=\<top>] 363 364lemma assert_opt_ev: 365 "equiv_valid_inv I A \<top> (assert_opt v)" 366 apply (simp add: assert_opt_def return_ev fail_ev 367 split: option.split) 368 done 369 370lemma assert_opt_ev2: 371 assumes "\<And> a a'. \<lbrakk>v = Some a; v' = Some a'\<rbrakk> \<Longrightarrow> R a a'" 372 shows "equiv_valid_2 I A A R \<top> \<top> (assert_opt v) (assert_opt v')" 373 apply (simp add: assert_opt_def return_ev fail_ev2_l fail_ev2_r 374 split: option.split) 375 apply(intro allI impI) 376 apply(rule return_ev2) 377 apply(rule assms, assumption+) 378 done 379 380lemma select_f_ev: 381 "equiv_valid_inv I A (K (det f)) (select_f (f x))" 382 apply (rule gen_asm_ev) 383 apply (simp add: select_f_def equiv_valid_def2 equiv_valid_2_def det_set_iff) 384 done 385 386lemma gets_evrv: 387 "equiv_valid_rv_inv I A R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (f s) (f t))) (gets f)" 388 apply (auto simp: equiv_valid_2_def in_monad) 389 done 390 391lemma gets_evrv': 392 "equiv_valid_rv_inv I A R (\<lambda>s. (\<forall>t. I s t \<and> A s t \<longrightarrow> R (f s) (f t))) (gets f)" 393 apply (auto simp: equiv_valid_2_def in_monad) 394 done 395 396lemma gets_evrv'': 397 "\<forall>s t. I s t \<and> A s t \<and> P s \<and> P t \<longrightarrow> R (f s) (f t) \<Longrightarrow> equiv_valid_rv_inv I A R P (gets f)" 398 apply (auto simp: equiv_valid_2_def in_monad) 399 done 400 401lemma equiv_valid_rv_guard_imp: 402 "\<lbrakk>equiv_valid_rv I A B R P f; \<And> s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> 403 equiv_valid_rv I A B R Q f" 404 apply(simp add: equiv_valid_2_def) 405 apply fast 406 done 407 408lemma gets_ev: 409 shows "equiv_valid_inv I A (\<lambda> s. \<forall> s t. I s t \<and> A s t \<longrightarrow> f s = f t) (gets f)" 410 apply (simp add: equiv_valid_def2) 411 apply (auto intro: equiv_valid_rv_guard_imp[OF gets_evrv]) 412 done 413 414lemma gets_ev': 415 shows "equiv_valid_inv I A (\<lambda> s. \<forall> t. I s t \<and> A s t \<longrightarrow> f s = f t) (gets f)" 416 apply (simp add: equiv_valid_def2) 417 apply (auto intro: equiv_valid_rv_guard_imp[OF gets_evrv']) 418 done 419 420lemma gets_ev'': 421 "\<forall>s t. I s t \<and> A s t \<and> P s \<and> P t \<longrightarrow> f s = f t \<Longrightarrow> equiv_valid_inv I A P (gets f)" 422 apply (simp add: equiv_valid_def2) 423 apply (auto intro: equiv_valid_rv_guard_imp[OF gets_evrv'']) 424 done 425 426lemma gets_the_evrv: 427 "equiv_valid_rv_inv I A R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))) (gets_the f)" 428 unfolding gets_the_def 429 apply (rule equiv_valid_rv_bind) 430 apply(rule equiv_valid_rv_guard_imp[OF gets_evrv]) 431 apply simp 432 apply(rule assert_opt_ev2) 433 apply simp 434 apply wp 435 done 436 437lemma gets_the_ev: 438 "equiv_valid_inv I A (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t)) (gets_the f)" 439 unfolding equiv_valid_def2 440 apply(rule equiv_valid_rv_guard_imp[OF gets_the_evrv]) 441 by simp 442 443lemma throwError_ev_pre: 444 "equiv_valid_inv I A P (throwError e)" 445 by (auto simp: throwError_def return_ev_pre) 446 447lemmas throwError_ev = throwError_ev_pre[where P=\<top>] 448 449lemma returnOk_ev_pre: 450 "equiv_valid_inv I A P (returnOk v)" 451 by (auto simp: returnOk_def return_ev_pre) 452 453lemmas returnOk_ev = returnOk_ev_pre[where P=\<top>] 454 455(* this seems restrictive, to have the same beginning and ending state relation, 456 however, one suspects that bindE is used usually only in code that doesn't 457 modify the state, so is probably OK.. We'll see *) 458lemma bindE_ev: 459 assumes reads_res_2: "\<And> rv. equiv_valid_inv I A (Q rv) (g rv)" 460 assumes reads_res_1: "equiv_valid_inv I A P' f" 461 assumes hoare: "\<lbrace> P'' \<rbrace> f \<lbrace> Q \<rbrace>,-" 462 shows "equiv_valid_inv I A (\<lambda>s. P' s \<and> P'' s) (f >>=E g)" 463 unfolding bindE_def 464 apply (rule bind_ev) 465 prefer 3 466 apply(rule hoare[unfolded validE_R_def validE_def]) 467 apply(simp split: sum.split add: lift_def throwError_ev) 468 apply(blast intro!: reads_res_2) 469 apply(rule reads_res_1) 470 done 471 472lemmas bindE_ev_pre = bindE_ev[THEN equiv_valid_guard_imp] 473 474(* Of course, when we know that progress is always made, we can do better *) 475lemma liftE_bindE_ev_general: 476 assumes r2: "\<And> val. equiv_valid I B C (Q val) (g val)" 477 assumes r1: "equiv_valid I A B P f" 478 assumes hoare: "\<lbrace> R \<rbrace> f \<lbrace> Q \<rbrace>" 479 shows "equiv_valid I A C (\<lambda> s. P s \<and> R s) (liftE f >>=E g)" 480 apply(simp add: bindE_def) 481 apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" in bind_ev_general) 482 prefer 2 483 apply(rule liftE_ev) 484 apply(rule r1) 485 apply(insert r2, fastforce simp: lift_def split: sum.split simp: equiv_valid_def2 equiv_valid_2_def)[1] 486 apply(insert hoare, fastforce simp: valid_def liftE_def return_def bind_def) 487 done 488 489lemma liftE_bindE_ev: 490 assumes r2: "\<And> val. equiv_valid_inv I A (Q val) (g val)" 491 assumes r1: "equiv_valid_inv I A P f" 492 assumes hoare: "\<lbrace> R \<rbrace> f \<lbrace> Q \<rbrace>" 493 shows "equiv_valid_inv I A (\<lambda> s. P s \<and> R s) (liftE f >>=E g)" 494 using assms by (blast intro: liftE_bindE_ev_general) 495 496lemmas liftE_bindE_ev_pre = liftE_bindE_ev[THEN equiv_valid_guard_imp] 497 498lemma liftM_ev: 499 assumes reads_res: "equiv_valid I A B P g" 500 shows "equiv_valid I A B P (liftM f g)" 501 apply (simp add: liftM_def) 502 apply (rule bind_ev_general[THEN equiv_valid_guard_imp, OF return_ev reads_res wp_post_taut]) 503 apply simp 504 done 505 506lemma liftME_ev: 507 assumes reads_res: "equiv_valid_inv I A P g" 508 shows "equiv_valid_inv I A P (liftME f g)" 509 apply(simp add: liftME_def) 510 apply (rule bindE_ev_pre[OF returnOk_ev reads_res]) 511 apply (rule hoare_True_E_R) 512 apply fast 513 done 514 515lemma whenE_ev: 516 assumes a: "b \<Longrightarrow> equiv_valid_inv I A P m" 517 shows "equiv_valid_inv I A (\<lambda>s. b \<longrightarrow> P s) (whenE b m)" 518 unfolding whenE_def by (auto intro: a returnOk_ev_pre) 519 520lemma whenE_throwError_bindE_ev: 521 assumes "\<And> rv. \<not> b \<Longrightarrow> equiv_valid_inv I A P (g rv)" 522 shows "equiv_valid_inv I A P (whenE b (throwError e) >>=E g)" 523 apply (rule_tac Q="\<lambda> rv. P and (\<lambda> s. \<not> b)" in bindE_ev_pre) 524 apply (rule gen_asm_ev) 525 apply (blast intro: assms) 526 apply (rule whenE_ev) 527 apply (rule throwError_ev) 528 apply (wp whenE_throwError_wp) 529 apply simp 530 done 531 532(* FIXME: trivially generalised *) 533lemma K_bind_ev: 534 "equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (K_bind f x)" 535 by simp 536 537subsection\<open>wp setup\<close> 538 539lemmas splits_ev[wp_split] = 540 bind_ev_pre bindE_ev_pre 541 bind_ev bindE_ev 542 if_ev_pre 543 if_ev 544 545lemmas wp_ev[wp] = 546 return_ev_pre 547 return_ev 548 liftE_ev 549 fail_ev_pre 550 fail_ev 551 assert_opt_ev 552 assert_ev 553 gets_ev 554 gets_the_ev 555 returnOk_ev_pre 556 returnOk_ev 557 throwError_ev_pre 558 throwError_ev 559 liftM_ev 560 liftME_ev 561 whenE_ev 562 K_bind_ev 563 564subsection\<open>crunch setup\<close> 565 566lemmas pre_ev = 567 hoare_pre 568 equiv_valid_guard_imp 569 570subsection\<open>Tom instantiates wpc\<close> 571 572lemma wpc_helper_equiv_valid: 573 "equiv_valid D A B Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (equiv_valid D A B P f)" 574 using equiv_valid_guard_imp 575 apply (simp add: wpc_helper_def) 576 apply (blast) 577 done 578 579wpc_setup "\<lambda>m. equiv_valid D A B Q m" wpc_helper_equiv_valid 580 581subsection\<open>More hoare-like rules\<close> 582 583lemma mapM_ev_pre: 584 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 585 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>" 586 assumes inv_established: "\<And> s. P s \<Longrightarrow> I s" 587 shows "equiv_valid_inv D A P (mapM m lst)" 588 using assms 589 apply(atomize) 590 apply(rule_tac Q=I in equiv_valid_guard_imp) 591 apply(induct lst) 592 apply(simp add: mapM_Nil return_ev_pre) 593 apply(subst mapM_Cons) 594 apply(rule bind_ev_pre[where P''="I"]) 595 apply(rule bind_ev[OF return_ev]) 596 apply fastforce 597 apply (rule wp_post_taut) 598 apply fastforce+ 599 done 600 601lemma mapM_x_ev_pre: 602 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 603 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>" 604 assumes inv_established: "\<And> s. P s \<Longrightarrow> I s" 605 shows "equiv_valid_inv D A P (mapM_x m lst)" 606 apply(subst mapM_x_mapM) 607 apply(rule bind_ev_pre[OF return_ev mapM_ev_pre]) 608 apply (blast intro: reads_res invariant inv_established wp_post_taut)+ 609 done 610 611lemma mapM_ev: 612 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 613 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>" 614 shows "equiv_valid_inv D A I (mapM m lst)" 615 using assms by (auto intro: mapM_ev_pre) 616 617lemma mapM_x_ev: 618 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 619 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>" 620 shows "equiv_valid_inv D A I (mapM_x m lst)" 621 using assms by (auto intro: mapM_x_ev_pre) 622 623(* MOVE -- proof clagged from mapM_x_mapM *) 624lemma mapME_x_mapME: 625 "mapME_x f l = mapME f l >>=E (\<lambda> y. returnOk ())" 626 apply (simp add: mapME_x_def sequenceE_x_def mapME_def sequenceE_def) 627 apply (induct l, simp_all add: Let_def bindE_assoc) 628 done 629 630lemma mapME_ev_pre: 631 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 632 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>,-" 633 assumes inv_established: "\<And> s. P s \<Longrightarrow> I s" 634 shows "equiv_valid_inv D A P (mapME m lst)" 635 using assms 636 apply(atomize) 637 apply(rule_tac Q=I in equiv_valid_guard_imp) 638 apply(induct lst) 639 apply(simp add: mapME_Nil returnOk_ev_pre) 640 apply(subst mapME_Cons) 641 apply wp 642 apply fastforce 643 apply (rule hoare_True_E_R[where P="\<top>"]) 644 apply fastforce+ 645 done 646 647lemma mapME_ev: 648 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv I A P (m x)" 649 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> P \<rbrace> m x \<lbrace> \<lambda>_. P \<rbrace>, -" 650 shows "equiv_valid_inv I A P (mapME m lst)" 651 using assms by (auto intro: mapME_ev_pre) 652 653lemma mapME_x_ev_pre: 654 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 655 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>,-" 656 assumes inv_established: "\<And> s. P s \<Longrightarrow> I s" 657 shows "equiv_valid_inv D A P (mapME_x m lst)" 658 unfolding mapME_x_mapME 659 apply (wp assms mapME_ev_pre | simp)+ 660 done 661 662lemma mapME_x_ev: 663 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)" 664 assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>, -" 665 shows "equiv_valid_inv D A I (mapME_x m lst)" 666 using assms by (auto intro: mapME_x_ev_pre) 667 668lemma mapM_ev': 669 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)" 670 shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapM m lst)" 671 apply(rule mapM_ev) 672 apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) 673 done 674 675lemma mapM_x_ev': 676 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)" 677 shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapM_x m lst)" 678 apply(rule mapM_x_ev) 679 apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) 680 done 681 682lemma mapME_ev': 683 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)" 684 shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapME m lst)" 685 apply(rule mapME_ev) 686 apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) 687 done 688 689lemma mapME_x_ev': 690 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)" 691 shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapME_x m lst)" 692 apply(rule mapME_x_ev) 693 apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) 694 done 695 696subsection\<open>Rules for the specialised validity\<close> 697 698lemma use_spec_ev: 699 "(\<And>st. spec_equiv_valid st I A B P f) \<Longrightarrow> equiv_valid I A B P f" 700 by (simp add: equiv_valid_def) 701 702lemma drop_spec_ev: 703 "equiv_valid I A B P f \<Longrightarrow> spec_equiv_valid st I A B P f" 704 by (simp add: equiv_valid_def) 705 706lemma spec_equiv_valid_guard_imp: 707 assumes reads_res: "spec_equiv_valid_inv s' I A P' f" 708 assumes guard_imp: "\<And> s. P s \<Longrightarrow> P' s" 709 shows "spec_equiv_valid_inv s' I A P f" 710 using assms 711 by (fastforce simp: spec_equiv_valid_def equiv_valid_2_def) 712 713lemma bind_spec_ev: 714 assumes reads_res_2: "\<And> rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (Q rv) (g rv)" 715 assumes reads_res_1: "spec_equiv_valid_inv s' I A P' f" 716 assumes hoare: "\<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>" 717 shows "spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>= g)" 718 using reads_res_1 719 apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def valid_def bind_def split_def) 720 apply (erule_tac x=t in allE) 721 apply clarsimp 722 apply (erule_tac x="(a, b)" in ballE) 723 apply (erule_tac x="(ab, bb)" in ballE) 724 apply clarsimp 725 apply (cut_tac rv="ab" and s''="b" in reads_res_2) 726 apply assumption 727 apply (clarsimp simp: spec_equiv_valid_def equiv_valid_2_def) 728 apply(erule_tac x=bb in allE) 729 using hoare 730 apply (fastforce simp: valid_def)+ 731 done 732 733lemma bindE_spec_ev: 734 assumes reads_res_2: "\<And> rv s''. (Inr rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (Q rv) (g rv)" 735 assumes reads_res_1: "spec_equiv_valid_inv s' I A P' f" 736 assumes hoare: "\<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>,-" 737 shows "spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>=E g)" 738 unfolding bindE_def 739 apply (rule bind_spec_ev) 740 prefer 3 741 apply(rule hoare[simplified validE_R_def validE_def]) 742 apply(simp split: sum.split add: lift_def) 743 apply(rule conjI) 744 apply(fastforce simp: spec_equiv_valid_def throwError_def return_ev2) 745 apply(fastforce simp: reads_res_2) 746 apply(rule reads_res_1) 747 done 748 749lemma if_spec_ev: 750 "\<lbrakk> G \<Longrightarrow> spec_equiv_valid_inv s' I A P f; 751 \<not> G \<Longrightarrow> spec_equiv_valid_inv s' I A P' f' 752 \<rbrakk> \<Longrightarrow> spec_equiv_valid_inv s' I A (\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)) (if G then f else f')" 753 by (cases G, simp+) 754 755lemmas splits_spec_ev[wp_split] = 756 drop_spec_ev 757 spec_equiv_valid_guard_imp[OF bind_spec_ev] spec_equiv_valid_guard_imp[OF bindE_spec_ev] 758 bind_spec_ev bindE_spec_ev 759 spec_equiv_valid_guard_imp[OF if_spec_ev] if_spec_ev 760 761(* Miscellaneous rules. *) 762 763lemma assertE_ev[wp]: 764 "equiv_valid_inv I A \<top> (assertE b)" 765 unfolding assertE_def 766 apply wp 767 by simp 768 769lemma equiv_valid_2_bindE: 770 assumes g: "\<And>rv rv'. R' rv rv' \<Longrightarrow> 771 equiv_valid_2 D A A (E \<oplus> R) (Q rv) (Q' rv') (g rv) (g' rv')" 772 assumes h1: "\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>,-" 773 assumes h2: "\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>,-" 774 assumes f: "equiv_valid_2 D A A (E \<oplus> R') P P' f f'" 775 shows "equiv_valid_2 D A A (E \<oplus> R) (P and S) (P' and S') (f >>=E g) (f' >>=E g')" 776 apply(unfold bindE_def) 777 apply(rule equiv_valid_2_guard_imp) 778 apply(rule_tac R'="E \<oplus> R'" and Q="case_sum \<top>\<top> Q" and Q'="case_sum \<top>\<top> Q'" and S=S and S'=S' in equiv_valid_2_bind) 779 apply(clarsimp simp: lift_def split: sum.splits) 780 apply(intro impI conjI allI) 781 apply(simp add: throwError_def) 782 apply(rule return_ev2) 783 apply simp 784 apply(simp) 785 apply(simp) 786 apply(fastforce intro: g) 787 apply(rule f) 788 apply(insert h1, fastforce simp: valid_def validE_R_def validE_def split: sum.splits)[1] 789 apply(insert h2, fastforce simp: valid_def validE_R_def validE_def split: sum.splits)[1] 790 by auto 791 792lemma rel_sum_comb_equals: 793 "((=) \<oplus> (=)) = (=)" 794 apply(rule ext) 795 apply(rule ext) 796 apply(rename_tac a b) 797 apply(case_tac a, auto) 798 done 799 800definition spec_equiv_valid_2_inv where 801 "spec_equiv_valid_2_inv s I A R P P' f f' \<equiv> 802 equiv_valid_2 I A A R (P and ((=) s)) P' f f'" 803 804lemma spec_equiv_valid_def2: 805 "spec_equiv_valid s I A A P f = 806 spec_equiv_valid_2_inv s I A (=) P P f f" 807 apply(simp add: spec_equiv_valid_def spec_equiv_valid_2_inv_def) 808 done 809 810lemma drop_spec_ev2_inv: 811 "equiv_valid_2 I A A R P P' f f' \<Longrightarrow> 812 spec_equiv_valid_2_inv s I A R P P' f f'" 813 apply(simp add: spec_equiv_valid_2_inv_def) 814 apply(erule equiv_valid_2_guard_imp, auto) 815 done 816 817lemma spec_equiv_valid_2_inv_guard_imp: 818 "\<lbrakk>spec_equiv_valid_2_inv s I A R Q Q' f f'; \<And> s. P s \<Longrightarrow> Q s; \<And> s. P' s \<Longrightarrow> Q' s\<rbrakk> \<Longrightarrow> 819 spec_equiv_valid_2_inv s I A R P P' f f'" 820 by(auto simp: spec_equiv_valid_2_inv_def equiv_valid_2_def) 821 822lemma bind_spec_ev2: 823 assumes reads_res_2: "\<And> rv s' rv'. \<lbrakk>(rv, s') \<in> fst (f s); R' rv rv'\<rbrakk> \<Longrightarrow> spec_equiv_valid_2_inv s' I A R (Q rv) (Q' rv') (g rv) (g' rv')" 824 assumes reads_res_1: "spec_equiv_valid_2_inv s I A R' P P' f f'" 825 assumes hoare: "\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>" 826 assumes hoare': "\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>" 827 shows "spec_equiv_valid_2_inv s I A R (P and S) (P' and S') (f >>= g) (f' >>= g')" 828 using reads_res_1 829 apply (clarsimp simp: spec_equiv_valid_2_inv_def equiv_valid_2_def bind_def split_def) 830 apply (erule_tac x=t in allE) 831 apply clarsimp 832 apply (drule_tac x="(a, b)" in bspec, assumption) 833 apply (drule_tac x="(ab, bb)" in bspec, assumption) 834 apply clarsimp 835 apply (cut_tac rv="a" and s'="b" in reads_res_2) 836 apply assumption 837 apply assumption 838 apply (clarsimp simp: spec_equiv_valid_2_inv_def equiv_valid_2_def) 839 apply(drule_tac x=bb in spec) 840 apply clarsimp 841 using hoare hoare' 842 apply (fastforce simp: valid_def)+ 843 done 844 845lemma spec_equiv_valid_2_inv_bindE: 846 assumes g: "\<And>rv s' rv'. \<lbrakk>(Inr rv, s') \<in> fst (f s); R' rv rv'\<rbrakk> \<Longrightarrow> 847 spec_equiv_valid_2_inv s' I A (E \<oplus> R) (Q rv) (Q' rv') (g rv) (g' rv')" 848 assumes h1: "\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>,-" 849 assumes h2: "\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>,-" 850 assumes f: "spec_equiv_valid_2_inv s I A (E \<oplus> R') P P' f f'" 851 shows "spec_equiv_valid_2_inv s I A (E \<oplus> R) (P and S) (P' and S') (f >>=E g) (f' >>=E g')" 852 apply(unfold bindE_def) 853 apply(rule spec_equiv_valid_2_inv_guard_imp) 854 apply(rule_tac R'="E \<oplus> R'" and Q="case_sum \<top>\<top> Q" and Q'="case_sum \<top>\<top> Q'" and S=S and S'=S' in bind_spec_ev2) 855 apply(clarsimp simp: lift_def split: sum.splits) 856 apply(intro impI conjI allI) 857 apply(simp add: throwError_def) 858 apply(rule drop_spec_ev2_inv[OF return_ev2]) 859 apply simp 860 apply(simp) 861 apply(simp) 862 apply(fastforce intro: g) 863 apply(rule f) 864 apply(insert h1, fastforce simp: valid_def validE_R_def validE_def split: sum.splits)[1] 865 apply(insert h2, fastforce simp: valid_def validE_R_def validE_def split: sum.splits)[1] 866 by auto 867 868lemma trancl_subset_equivalence: 869 "\<lbrakk>(a, b) \<in> r'\<^sup>+; \<forall>x. (a, x)\<in>r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+" 870 apply(induct a b rule: trancl.induct) 871 apply(blast) 872 apply(simp) 873 apply(rule_tac b=b in trancl_into_trancl) 874 apply(simp) 875 apply(erule_tac x=c in allE) 876 apply(subgoal_tac "(a, c) \<in> r'\<^sup>+") 877 apply(auto) 878 done 879 880lemma equiv_valid_rv_gets_compD: 881 "equiv_valid_rv_inv I A R P (gets (f \<circ> g)) \<Longrightarrow> 882 equiv_valid_rv_inv I A (\<lambda> rv rv'. R (f rv) (f rv')) P (gets g)" 883 apply(clarsimp simp: equiv_valid_2_def gets_def bind_def return_def get_def) 884 done 885 886 887lemma liftE_ev2: 888 "equiv_valid_2 I A B R P P' f f' \<Longrightarrow> 889 equiv_valid_2 I A B (E \<oplus> R) P P' (liftE f) (liftE f')" 890 apply(clarsimp simp: liftE_def equiv_valid_2_def bind_def return_def) 891 apply fastforce 892 done 893 894lemma whenE_spec_ev2_inv: 895 assumes a: "b \<Longrightarrow> spec_equiv_valid_2_inv s I A R P P' m m'" 896 assumes r: "\<And> x. R x x" 897 shows "spec_equiv_valid_2_inv s I A R P P' (whenE b m) (whenE b m')" 898 unfolding whenE_def 899 apply (auto intro: a simp: returnOk_def intro!: drop_spec_ev2_inv[OF return_ev2] intro: r) 900 done 901 902lemma whenE_spec_ev: 903 assumes a: "b \<Longrightarrow> spec_equiv_valid_inv s I A P m" 904 shows "spec_equiv_valid_inv s I A P (whenE b m) " 905 unfolding whenE_def 906 apply (auto intro: a simp: returnOk_def intro!: drop_spec_ev[OF return_ev_pre]) 907 done 908 909 910lemma spec_equiv_valid_2_inv_by_spec_equiv_valid: 911 "\<lbrakk>spec_equiv_valid s I A A P f; P' = P; f' = f; 912 (\<And> a. R a a)\<rbrakk> \<Longrightarrow> 913 spec_equiv_valid_2_inv s I A R P P' f f'" 914 apply(clarsimp simp: spec_equiv_valid_def spec_equiv_valid_2_inv_def) 915 apply(fastforce simp: equiv_valid_2_def) 916 done 917 918lemma mapM_ev'': 919 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (P x) (m x)" 920 assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> \<lambda>s. \<forall>x\<in>set lst. P x s \<rbrace> m x \<lbrace> \<lambda>_ s. \<forall>x\<in>set lst. P x s \<rbrace>" 921 shows "equiv_valid_inv D A (\<lambda> s. \<forall>x\<in>set lst. P x s) (mapM m lst)" 922 apply(rule mapM_ev) 923 apply(rule equiv_valid_guard_imp[OF reads_res]; simp) 924 apply(wpsimp wp: inv) 925 done 926 927lemma mapM_x_ev'': 928 assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (P x) (m x)" 929 assumes inv: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> \<lambda>s. \<forall>x\<in>set lst. P x s \<rbrace> m x \<lbrace> \<lambda>_ s. \<forall>x\<in>set lst. P x s \<rbrace>" 930 shows "equiv_valid_inv D A (\<lambda> s. \<forall>x\<in>set lst. P x s) (mapM_x m lst)" 931 apply(rule mapM_x_ev) 932 apply(rule equiv_valid_guard_imp[OF reads_res]; simp) 933 apply(wpsimp wp: inv) 934 done 935 936lemma catch_ev[wp]: 937 assumes ok: 938 "equiv_valid I A A P f" 939 assumes err: 940 "\<And> e. equiv_valid I A A (E e) (handler e)" 941 assumes hoare: 942 "\<lbrace> P \<rbrace> f -, \<lbrace> E \<rbrace>" 943 shows 944 "equiv_valid I A A P (f <catch> handler)" 945 apply(simp add: catch_def) 946 apply (wp err ok | wpc | simp)+ 947 apply(insert hoare[simplified validE_E_def validE_def])[1] 948 apply(simp split: sum.splits) 949 by simp 950 951lemma equiv_valid_rv_trivial: 952 assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. P \<rbrace>" 953 shows "equiv_valid_rv_inv I A \<top>\<top> \<top> f" 954 by(auto simp: equiv_valid_2_def dest: state_unchanged[OF inv]) 955 956lemma equiv_valid_2_trivial: 957 assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. P \<rbrace>" 958 assumes inv': "\<And> P. \<lbrace> P \<rbrace> f' \<lbrace> \<lambda>_. P \<rbrace>" 959 shows "equiv_valid_2 I A A \<top>\<top> \<top> \<top> f f'" 960 by(auto simp: equiv_valid_2_def dest: state_unchanged[OF inv] state_unchanged[OF inv']) 961 962lemma gen_asm_ev2_r: 963 "\<lbrakk>P' \<Longrightarrow> equiv_valid_2 I A B R P Q f f'\<rbrakk> \<Longrightarrow> 964 equiv_valid_2 I A B R P (Q and (K P')) f f'" 965 apply(fastforce simp: equiv_valid_2_def) 966 done 967 968lemma gen_asm_ev2_l: 969 "\<lbrakk>P \<Longrightarrow> equiv_valid_2 I A B R Q P' f f'\<rbrakk> \<Longrightarrow> 970 equiv_valid_2 I A B R (Q and (K P)) P' f f'" 971 apply(fastforce simp: equiv_valid_2_def) 972 done 973 974lemma gen_asm_ev2_r': 975 "\<lbrakk>P' \<Longrightarrow> equiv_valid_2 I A B R P \<top> f f'\<rbrakk> \<Longrightarrow> 976 equiv_valid_2 I A B R P (\<lambda>s. P') f f'" 977 apply(fastforce simp: equiv_valid_2_def) 978 done 979 980lemma gen_asm_ev2_l': 981 "\<lbrakk>P \<Longrightarrow> equiv_valid_2 I A B R \<top> P' f f'\<rbrakk> \<Longrightarrow> 982 equiv_valid_2 I A B R (\<lambda>s. P) P' f f'" 983 apply(fastforce simp: equiv_valid_2_def) 984 done 985 986lemma equiv_valid_rv_liftE_bindE: 987 assumes ev1: 988 "equiv_valid_rv_inv I A W P f" 989 assumes ev2: 990 "\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (Q rv) (Q rv') (g rv) (g rv')" 991 assumes hoare: 992 "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>" 993 shows "equiv_valid_rv_inv I A R P ((liftE f) >>=E g)" 994 apply(unfold bindE_def) 995 apply(rule_tac Q="\<lambda> rv. K (\<forall> v. rv \<noteq> Inl v) and (\<lambda> s. \<forall> v. rv = Inr v \<longrightarrow> Q v s)" in equiv_valid_rv_bind) 996 apply(rule_tac E="dc" in equiv_valid_2_liftE) 997 apply(rule ev1) 998 apply(clarsimp simp: lift_def split: sum.split) 999 apply(insert ev2, fastforce simp: equiv_valid_2_def)[1] 1000 apply(insert hoare, clarsimp simp: valid_def liftE_def bind_def return_def split_def) 1001 done 1002 1003lemma if_evrv: 1004 assumes "b \<Longrightarrow> equiv_valid_rv_inv I A R P f" 1005 assumes "\<not> b \<Longrightarrow> equiv_valid_rv_inv I A R Q g" 1006 shows "equiv_valid_rv_inv I A R (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) (if b then f else g)" 1007 apply (clarsimp split: if_split) 1008 using assms by blast 1009 1010end 1011