1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* A theory of guarded monadic bisimulation. *) 8 9theory Bisim_UL 10imports 11 NonDetMonadVCG 12 Corres_UL 13 EmptyFailLib 14begin 15 16(* This still looks a bit wrong to me, although it is more or less what I want \<emdash> we want to be 17 able to move hoare triples across bisimulations, and this allows guards to be left behind, more or less 18definition 19 "bisim_underlying SR R P P' m m' \<equiv> 20 \<forall>s s'. SR s s' \<longrightarrow> (P s \<longrightarrow> (\<forall>(r, t) \<in> fst (m s). \<exists>(r', t') \<in> fst (m' s'). R r r' \<and> SR t t')) \<and> 21 (P' s' \<longrightarrow> (\<forall>(r', t') \<in> fst (m' s'). \<exists>(r, t) \<in> fst (m s). R r r' \<and> SR t t'))" 22*) 23 24definition 25 bisim_underlying :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> (('c \<times> 'a) set) \<times> bool) \<Rightarrow> ('b \<Rightarrow> (('d \<times> 'b) set) \<times> bool) \<Rightarrow> bool" 26where 27 "bisim_underlying SR R P P' m m' \<equiv> 28 \<forall>s s'. SR s s' \<and> P s \<and> P' s' \<longrightarrow> ((\<forall>(r, t) \<in> fst (m s). \<exists>(r', t') \<in> fst (m' s'). R r r' \<and> SR t t') \<and> 29 (\<forall>(r', t') \<in> fst (m' s'). \<exists>(r, t) \<in> fst (m s). R r r' \<and> SR t t'))" 30 31(* 32lemma bisim_is_corres_both_ways: 33 "bisim_underlying SR R P P' m m' = (corres_underlying SR False R P P' m m' \<and> corres_underlying (converse SR) False (swp R) P' P m' m)" 34 unfolding bisim_underlying_def corres_underlying_def 35 by (fastforce simp: swp_def Ball_def Bex_def) 36*) 37 38lemma bisim_valid: 39 assumes ac: "bisim_underlying (=) (=) P P' a a'" 40 and rl: "\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>" 41 shows "\<lbrace>P and P' and Q\<rbrace> a' \<lbrace>S\<rbrace>" 42 using ac rl 43 unfolding bisim_underlying_def valid_def 44 by (fastforce simp: split_def) 45 46lemma bisim_valid2: 47 assumes ac: "bisim_underlying (=) (=) P P' a a'" 48 and rl: "\<lbrace>Q\<rbrace> a' \<lbrace>S\<rbrace>" 49 shows "\<lbrace>P and P' and Q\<rbrace> a \<lbrace>S\<rbrace>" 50 using ac rl 51 unfolding bisim_underlying_def valid_def 52 by (fastforce simp: split_def) 53 54lemma bisim_underlyingI [consumes 0, case_names Left Right]: 55 assumes r1: "\<And>s s' r t. \<lbrakk>SR s s'; P s; P' s'; (r, t) \<in> fst (m s) \<rbrakk> \<Longrightarrow> \<exists>(r', t') \<in> fst (m' s'). R r r' \<and> SR t t'" 56 and r2: "\<And>s s' r' t'. \<lbrakk>SR s s'; P s; P' s'; (r', t') \<in> fst (m' s') \<rbrakk> \<Longrightarrow> \<exists>(r, t) \<in> fst (m s). R r r' \<and> SR t t'" 57 shows "bisim_underlying SR R P P' m m'" 58 unfolding bisim_underlying_def 59 by (fastforce dest: r1 r2 simp: split_def) 60 61lemma bisim_underlyingE1: 62 assumes bs: "bisim_underlying SR R P P' m m'" 63 and sr: "SR s s'" 64 and ps: "P s" "P' s'" 65 and ms: "(r, t) \<in> fst (m s)" 66 and rl: "\<And>r' t'. \<lbrakk> (r', t') \<in> fst (m' s'); R r r'; SR t t' \<rbrakk> \<Longrightarrow> X" 67 shows X 68 using bs sr ps ms unfolding bisim_underlying_def 69 by (fastforce intro: rl) 70 71lemma bisim_underlyingE2: 72 assumes bs: "bisim_underlying SR R P P' m m'" 73 and sr: "SR s s'" 74 and ps: "P s" "P' s'" 75 and ms: "(r', t') \<in> fst (m' s')" 76 and rl: "\<And>r t. \<lbrakk> (r, t) \<in> fst (m s); R r r'; SR t t' \<rbrakk> \<Longrightarrow> X" 77 shows X 78 using bs sr ps ms unfolding bisim_underlying_def 79 by (fastforce intro: rl) 80 81lemma bisim_split: 82 assumes ac: "bisim_underlying SR R' P P' a c" 83 and bd: "\<And>r r'. R' r r' \<Longrightarrow> bisim_underlying SR R (Q r) (Q' r') (b r) (d r')" 84 and v1: "\<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>" 85 and v2: "\<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>" 86 shows "bisim_underlying SR R (P and S) (P' and S') (a >>= b) (c >>= d)" 87 using ac 88 apply - 89 apply (rule bisim_underlyingI) 90 apply (clarsimp simp: in_monad split_def) 91 apply (erule (4) bisim_underlyingE1) 92 apply (frule (1) use_valid [OF _ v1]) 93 apply (frule (1) use_valid [OF _ v2]) 94 apply (erule (4) bisim_underlyingE1 [OF bd]) 95 apply (rename_tac r'' t'') 96 apply (rule_tac x = "(r'', t'')" in bexI) 97 apply clarsimp 98 apply (fastforce simp: in_monad) 99 apply (clarsimp simp: in_monad split_def) 100 apply (erule (4) bisim_underlyingE2) 101 apply (frule (1) use_valid [OF _ v1]) 102 apply (frule (1) use_valid [OF _ v2]) 103 apply (erule (4) bisim_underlyingE2 [OF bd]) 104 apply (rename_tac r'' t'') 105 apply (rule_tac x = "(r'', t'')" in bexI) 106 apply clarsimp 107 apply (fastforce simp: in_monad) 108 done 109 110abbreviation 111 "bisim \<equiv> bisim_underlying (=)" 112 113lemma bisim_refl: 114 assumes rrefl: "\<And>r. R r r" 115 shows "bisim R P P' m m" 116 apply (rule bisim_underlyingI) 117 apply (clarsimp simp: split_def) 118 apply (erule bexI [rotated]) 119 apply (simp add: rrefl) 120 apply (clarsimp simp: split_def) 121 apply (erule bexI [rotated]) 122 apply (simp add: rrefl) 123 done 124 125lemma bisim_guard_imp: 126 assumes bs: "bisim_underlying SR R Q Q' m m'" 127 and rls: "\<And>s. P s \<Longrightarrow> Q s" "\<And>s. P' s \<Longrightarrow> Q' s" 128 shows "bisim_underlying SR R P P' m m'" 129 using bs rls 130 by (fastforce intro!: bisim_underlyingI elim: bisim_underlyingE1 bisim_underlyingE2) 131 132lemma bisim_return': 133 assumes Rxx: "R x x'" 134 shows "bisim_underlying SR R P P' (return x) (return x')" 135 apply (rule bisim_underlyingI) 136 apply (clarsimp simp: in_monad split_def Bex_def Rxx) 137 apply (clarsimp simp: in_monad split_def Bex_def Rxx) 138 done 139 140lemmas bisim_return = bisim_return' [where P = \<top> and P' = \<top>] 141 142lemma bisim_split_handle: 143 assumes bm: "bisim (f' \<oplus> r) Pn Pn' m m'" 144 and bc: "\<And>x x'. f' x x' \<Longrightarrow> bisim (f \<oplus> r) (Pf x) (Pf' x') (c x) (c' x')" 145 and v1: "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>Pf\<rbrace>" 146 and v2: "\<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>Pf'\<rbrace>" 147 shows "bisim (f \<oplus> r) (Pn and P) (Pn' and P') (m <handle> c) (m' <handle> c')" 148 unfolding handleE_def handleE'_def 149 apply (rule bisim_split [where Q = "\<lambda>r s. case_sum (\<lambda>l. Pf l s) (\<lambda>_. True) r" and Q' = "\<lambda>r s. case_sum (\<lambda>l. Pf' l s) (\<lambda>_. True) r", OF bm, folded validE_def]) 150 apply (case_tac ra) 151 apply clarsimp 152 apply (erule bc) 153 apply clarsimp 154 apply (rule bisim_return') 155 apply simp 156 apply (rule v1) 157 apply (rule v2) 158 done 159 160(* Set up wpc *) 161lemma wpc_helper_bisim: 162 "bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (bisim_underlying SR r P (\<lambda>s. s \<in> P') f f')" 163 apply (clarsimp simp: wpc_helper_def) 164 apply (erule bisim_guard_imp) 165 apply simp 166 apply fastforce 167 done 168 169wpc_setup "\<lambda>m. bisim_underlying SR r P P' a m" wpc_helper_bisim 170wpc_setup "\<lambda>m. bisim_underlying SR r P P' a (m >>= c)" wpc_helper_bisim 171 172lemma bisim_split_refl: 173 assumes bs: "\<And>r. bisim R (Q r) (Q' r) (b r) (d r)" 174 and v1: "\<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>" 175 and v2: "\<lbrace>S'\<rbrace> a \<lbrace>Q'\<rbrace>" 176 shows "bisim R S S' (a >>= b) (a >>= d)" 177 apply (rule bisim_guard_imp) 178 apply (rule bisim_split [OF _ _ v1 v2]) 179 apply (rule bisim_refl [where P = \<top> and P' = \<top> and R = "(=)", OF refl]) 180 apply simp 181 apply (rule bs) 182 apply simp_all 183 done 184 185lemma bisim_throwError': 186 "f e e' \<Longrightarrow> bisim_underlying SR (f \<oplus> R') P P' (throwError e) (throwError e')" 187 apply (rule bisim_underlyingI) 188 apply (clarsimp simp: in_monad Bex_def)+ 189 done 190 191lemmas bisim_throwError = bisim_throwError' [where P = \<top> and P' = \<top>] 192 193lemma bisim_splitE: 194 assumes ac: "bisim_underlying SR (f \<oplus> R') P P' a c" 195 and bd: "\<And>r r'. R' r r' \<Longrightarrow> bisim_underlying SR (f \<oplus> R) (Q r) (Q' r') (b r) (d r')" 196 and v1: "\<lbrace>S\<rbrace> a \<lbrace>Q\<rbrace>, -" 197 and v2: "\<lbrace>S'\<rbrace> c \<lbrace>Q'\<rbrace>, -" 198 shows "bisim_underlying SR (f \<oplus> R) (P and S) (P' and S') (a >>=E b) (c >>=E d)" 199 apply (simp add: bindE_def lift_def[abs_def]) 200 apply (rule bisim_split [where Q = "\<lambda>r s. case_sum (\<lambda>_. True) (\<lambda>l. Q l s) r" and Q' = "\<lambda>r s. case_sum (\<lambda>_. True) (\<lambda>l. Q' l s) r", OF ac, folded validE_def, folded validE_R_def]) 201 apply (case_tac r') 202 apply clarsimp 203 apply (erule bisim_throwError') 204 apply clarsimp 205 apply (erule bd) 206 apply (rule v1) 207 apply (rule v2) 208 done 209 210lemma bisim_split_reflE: 211 assumes ab: "\<And>r. bisim (f \<oplus> R) (Q r) (Q' r) (a r) (b r)" 212 and v1: "\<lbrace>S\<rbrace> m \<lbrace>Q\<rbrace>, -" 213 and v2: "\<lbrace>S'\<rbrace> m \<lbrace>Q'\<rbrace>, -" 214 and refls: "\<And>e. f e e" "\<And>r. R r r" 215 shows "bisim (f \<oplus> R) S S' (m >>=E a) (m >>=E b)" 216 using refls 217 apply - 218 apply (rule bisim_guard_imp) 219 apply (rule bisim_splitE [where R' = "(=)", OF _ _ v1 v2]) 220 apply (rule bisim_refl) 221 apply (case_tac r, simp_all)[1] 222 apply simp 223 apply (rule ab) 224 apply simp+ 225 done 226 227lemma bisim_split_bind_case_sum: 228 "\<lbrakk>bisim_underlying sr (lr \<oplus> rr) P P' a d; 229 \<And>rv rv'. lr rv rv' \<Longrightarrow> bisim_underlying sr r (R rv) (R' rv') (b rv) (e rv'); 230 \<And>rv rv'. rr rv rv' \<Longrightarrow> bisim_underlying sr r (S rv) (S' rv') (c rv) (f rv'); \<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>, \<lbrace>R'\<rbrace>\<rbrakk> 231 \<Longrightarrow> bisim_underlying sr r (P and Q) (P' and Q') (a >>= case_sum b c) (d >>= case_sum e f)" 232 apply (erule bisim_split [where Q = "\<lambda>rv s. case_sum (\<lambda>l. R l s) (\<lambda>r. S r s) rv" and Q' = "\<lambda>rv s. case_sum (\<lambda>l. R' l s) (\<lambda>r. S' r s) rv", folded validE_def]) 233 apply (case_tac r') 234 apply clarsimp 235 apply clarsimp 236 apply assumption+ 237 done 238 239lemma bisim_liftE [simp]: 240 "bisim_underlying SR (f \<oplus> R) P P' (liftE a) (liftE b) = bisim_underlying SR R P P' a b" 241 by (fastforce simp: in_monad intro: bisim_underlyingI elim: bisim_underlyingE1 bisim_underlyingE2) 242 243lemma bisim_when: 244 assumes bs: "b \<Longrightarrow> bisim_underlying SR R P P' m m'" 245 and rr: "R () ()" 246 shows "bisim_underlying SR R (\<lambda>s. b \<longrightarrow> P s) (\<lambda>s. b \<longrightarrow> P' s) (when b m) (when b m')" 247 using assms 248 apply (cases b, simp_all add: when_def) 249 apply (erule bisim_return) 250 done 251 252 253(* not really used *) 254definition 255 "det_on P f \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>r. f s = ({r}, False))" 256 257lemma det_onE: 258 "\<lbrakk>det_on P f; P s; \<And>r s'. \<lbrakk> (r, s') \<in> fst (f s); \<not> snd (f s)\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 259 unfolding det_on_def by fastforce 260 261lemma bisim_noop_det_on: 262 assumes a: "\<And>s. \<lbrace>Pa and (=) s\<rbrace> a \<lbrace>\<lambda>_. (=) s\<rbrace>" 263 and b: "\<And>s. \<lbrace>Pb and (=) s\<rbrace> b \<lbrace>\<lambda>_. (=) s\<rbrace>" 264 and da: "det_on P a" 265 and db: "det_on P' b" 266 shows "bisim_underlying sr dc (Pa and P) (Pb and P') a b" 267 using da db 268 apply - 269 apply (rule bisim_underlyingI) 270 apply clarsimp 271 apply (erule (1) det_onE)+ 272 apply (frule use_valid [OF _ a], fastforce) 273 apply (frule use_valid [OF _ b], fastforce) 274 apply fastforce 275 276 apply clarsimp 277 apply (erule (1) det_onE)+ 278 apply (frule use_valid [OF _ a], fastforce) 279 apply (frule use_valid [OF _ b], fastforce) 280 apply fastforce 281 done 282 283lemma det_on_gets: 284 "det_on \<top> (gets f)" unfolding det_on_def 285 by (clarsimp simp: gets_def return_def bind_def get_def) 286 287lemma hoare_gen_asmE': 288 "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace>" 289 unfolding validE_def 290 by (erule hoare_gen_asm) 291 292lemma det_onE': 293 "\<lbrakk>det_on P f; P s; \<And>r s'. \<lbrakk> f s = ({(r, s')}, False)\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 294 unfolding det_on_def by fastforce 295 296(* ugh *) 297lemma det_on_guard_imp [wp_comb]: 298 assumes da: "det_on P' a" 299 and "\<And>s. P s \<Longrightarrow> P' s" 300 shows "det_on P a" 301 using assms unfolding det_on_def by auto 302 303lemma det_on_split [wp_split]: 304 assumes da: "det_on Pa a" 305 and db: "\<And>x. det_on (Pb x) (b x)" 306 and v: "\<lbrace>Pb'\<rbrace> a \<lbrace>Pb\<rbrace>" 307 shows "det_on (Pa and Pb') (a >>= b)" 308 unfolding det_on_def using da 309 apply - 310 apply clarsimp 311 apply (erule (1) det_onE) 312 apply (frule (1) use_valid [OF _ v]) 313 apply (erule det_onE' [OF da]) 314 apply (erule det_onE' [OF db]) 315 apply (clarsimp simp: bind_def split_def) 316 done 317 318lemma det_det_on: 319 "det m \<Longrightarrow> det_on \<top> m" 320 unfolding det_def det_on_def by auto 321 322lemma det_on_liftE [wp]: 323 "det_on P m \<Longrightarrow> det_on P (liftE m)" 324 unfolding liftE_def 325 apply (rule det_on_guard_imp) 326 apply (erule det_on_split [OF _ det_det_on]) 327 apply simp 328 apply wp 329 apply simp 330 done 331 332lemma det_on_lift [wp]: 333 "(\<And>y. det_on (P y) (m y)) \<Longrightarrow> det_on (case_sum (\<lambda>_. \<top>) P x) (lift m x)" 334 unfolding lift_def 335 by (auto simp: det_on_def throwError_def return_def split: sum.splits) 336 337lemma det_on_assert_opt [wp]: 338 "det_on (\<lambda>_. x \<noteq> None) (assert_opt x)" 339 unfolding det_on_def assert_opt_def by (fastforce split: option.splits simp: fail_def return_def) 340 341lemmas dets_to_det_on [wp] = det_det_on [OF det_gets] det_det_on [OF return_det] 342 343(* Set up wpc *) 344lemma wpc_helper_det_on: 345 "det_on Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (det_on P f)" 346 apply (clarsimp simp: wpc_helper_def det_on_def) 347 done 348 349wpc_setup "\<lambda>m. det_on P m" wpc_helper_det_on 350wpc_setup "\<lambda>m. det_on P (m >>= c)" wpc_helper_det_on 351 352lemma bisim_symb_exec_r_det_on: 353 assumes z: "\<And>rv. bisim_underlying sr r P (Q' rv) x (y rv)" 354 assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>Q'\<rbrace>" 355 assumes x: "\<And>s. \<lbrace>Pe and (=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>" 356 assumes nf: "det_on Pd m" 357 shows "bisim_underlying sr r P (P' and Pe and Pd) x (m >>= (\<lambda>rv. y rv))" 358 apply (rule bisim_guard_imp) 359 apply (subst gets_bind_ign [symmetric], rule bisim_split) 360 apply (rule bisim_noop_det_on [OF _ x det_on_gets]) 361 apply (rule hoare_pre, wp) 362 apply fastforce 363 apply (rule nf) 364 apply (rule z) 365 apply (wp y)+ 366 apply simp+ 367 done 368 369definition 370 not_empty :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b set \<times> bool) \<Rightarrow> bool" 371where 372 "not_empty P f \<equiv> \<forall>s. P s \<longrightarrow> (fst (f s) \<noteq> {})" 373 374lemma not_emptyE: 375 "\<lbrakk> not_empty P f; P s; \<And>r s'. \<lbrakk> (r, s') \<in> fst (f s)\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 376 unfolding not_empty_def by fastforce 377 378(* ugh *) 379lemma not_empty_guard_imp [wp_comb]: 380 assumes da: "not_empty P' a" 381 and "\<And>s. P s \<Longrightarrow> P' s" 382 shows "not_empty P a" 383 using assms unfolding not_empty_def by auto 384 385lemma not_empty_split [wp_split]: 386 assumes da: "not_empty Pa a" 387 and db: "\<And>x. not_empty (Pb x) (b x)" 388 and v: "\<lbrace>Pb'\<rbrace> a \<lbrace>Pb\<rbrace>" 389 shows "not_empty (Pa and Pb') (a >>= b)" 390 unfolding not_empty_def using da 391 apply - 392 apply clarsimp 393 apply (erule (1) not_emptyE) 394 apply (frule (1) use_valid [OF _ v]) 395 apply (erule not_emptyE [OF da]) 396 apply (erule not_emptyE [OF db]) 397 apply (fastforce simp: bind_def split_def) 398 done 399 400lemma not_empty_return [wp]: 401 "not_empty \<top> (return x)" 402 unfolding not_empty_def 403 by (simp add: return_def) 404 405lemma not_empty_liftE [wp]: 406 assumes ne: "not_empty P m" 407 shows "not_empty P (liftE m)" 408 unfolding liftE_def 409 apply (rule not_empty_guard_imp) 410 apply (wp ne) 411 apply simp 412 done 413 414lemma not_empty_lift [wp]: 415 "(\<And>y. not_empty (P y) (m y)) \<Longrightarrow> not_empty (case_sum (\<lambda>_. \<top>) P x) (lift m x)" 416 unfolding lift_def 417 by (auto simp: not_empty_def throwError_def return_def split: sum.splits) 418 419lemma not_empty_assert_opt [wp]: 420 "not_empty (\<lambda>_. x \<noteq> None) (assert_opt x)" 421 unfolding not_empty_def assert_opt_def by (fastforce split: option.splits simp: fail_def return_def) 422 423lemma not_empty_gets [wp]: 424 "not_empty \<top> (gets f)" unfolding not_empty_def 425 by (clarsimp simp: gets_def return_def bind_def get_def) 426 427(* Set up wpc *) 428lemma wpc_helper_not_empty: 429 "not_empty Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (not_empty P f)" 430 apply (clarsimp simp: wpc_helper_def not_empty_def) 431 done 432 433wpc_setup "\<lambda>m. not_empty P m" wpc_helper_not_empty 434wpc_setup "\<lambda>m. not_empty P (m >>= c)" wpc_helper_not_empty 435 436lemma bisim_noop: 437 assumes a: "\<And>s. \<lbrace>Pa and (=) s\<rbrace> a \<lbrace>\<lambda>_. (=) s\<rbrace>" 438 and b: "\<And>s. \<lbrace>Pb and (=) s\<rbrace> b \<lbrace>\<lambda>_. (=) s\<rbrace>" 439 and da: "not_empty P a" 440 and db: "not_empty P' b" 441 shows "bisim_underlying sr dc (Pa and P) (Pb and P') a b" 442 using da db 443 apply - 444 apply (rule bisim_underlyingI) 445 apply clarsimp 446 apply (erule (1) not_emptyE)+ 447 apply (frule use_valid [OF _ a], fastforce) 448 apply (frule use_valid [OF _ b], fastforce) 449 apply fastforce 450 451 apply clarsimp 452 apply (erule (1) not_emptyE)+ 453 apply (frule use_valid [OF _ a], fastforce) 454 apply (frule use_valid [OF _ b], fastforce) 455 apply fastforce 456 done 457 458lemma bisim_symb_exec_r: 459 assumes z: "\<And>rv. bisim_underlying sr r P (Q' rv) x (y rv)" 460 assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>Q'\<rbrace>" 461 assumes x: "\<And>s. \<lbrace>Pe and (=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>" 462 assumes ne: "not_empty Pd m" 463 shows "bisim_underlying sr r P (P' and Pe and Pd) x (m >>= (\<lambda>rv. y rv))" 464 apply (rule bisim_guard_imp) 465 apply (subst gets_bind_ign [symmetric], rule bisim_split) 466 apply (rule bisim_noop [OF _ x not_empty_gets]) 467 apply (rule hoare_pre, wp) 468 apply fastforce 469 apply (rule ne) 470 apply (rule z) 471 apply (wp y)+ 472 apply simp+ 473 done 474 475lemma bisim_not_empty: 476 assumes bs: "bisim r P P' m m'" 477 and ne: "not_empty R m" 478 shows "not_empty (P and P' and R) m'" 479 unfolding not_empty_def using bs ne 480 apply clarsimp 481 apply (erule (1) not_emptyE) 482 apply (erule_tac s=s and s'=s in bisim_underlyingE1 [where SR = "(=)"]) 483 apply simp+ 484 done 485 486lemma bisim_split_req: 487 assumes ac: "bisim (=) P P' a c" 488 and bd: "\<And>r. bisim R (Q r) (Q' r) (b r) (d r)" 489 and v1: "\<lbrace>S\<rbrace> a \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>" 490 shows "bisim R (P and S) P' (a >>= b) (c >>= d)" 491 using ac 492 apply - 493 apply (rule bisim_underlyingI) 494 apply (clarsimp simp: in_monad split_def) 495 apply (erule bisim_underlyingE1) 496 apply simp 497 apply assumption+ 498 apply (frule (1) use_valid [OF _ v1]) 499 apply clarsimp 500 apply (rule bisim_underlyingE1 [OF bd]) 501 apply simp 502 apply assumption+ 503 apply (rename_tac r'' t'') 504 apply (rule_tac x = "(r'', t'')" in bexI) 505 apply clarsimp 506 apply (fastforce simp: in_monad) 507 508 apply (clarsimp simp: in_monad split_def) 509 apply (erule bisim_underlyingE2) 510 apply simp 511 apply assumption+ 512 apply (frule (1) use_valid [OF _ v1]) 513 apply clarsimp 514 apply (rule bisim_underlyingE2 [OF bd]) 515 apply simp 516 apply assumption+ 517 apply (rename_tac r'' t'') 518 apply (rule_tac x = "(r'', t'')" in bexI) 519 apply clarsimp 520 apply (fastforce simp: in_monad) 521 done 522 523lemma bisim_splitE_req: 524 assumes ac: "bisim (f \<oplus> (=)) P P' a c" 525 and bd: "\<And>r. bisim (f \<oplus> R) (Q r) (Q' r) (b r) (d r)" 526 and v1: "\<lbrace>S\<rbrace> a \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>, -" 527 shows "bisim (f \<oplus> R) (P and S) P' (a >>=E b) (c >>=E d)" 528 using ac 529 apply - 530 apply (simp add: bindE_def lift_def[abs_def]) 531 apply (rule bisim_underlyingI) 532 apply (clarsimp simp: in_monad split_def) 533 apply (erule bisim_underlyingE1) 534 apply simp 535 apply assumption+ 536 apply (frule (1) use_valid [OF _ v1 [unfolded validE_R_def validE_def]]) 537 apply clarsimp 538 apply (case_tac x) 539 apply (clarsimp simp: in_monad) 540 apply (rule_tac x = "(Inl y', t')" in bexI) 541 apply fastforce 542 apply (fastforce simp: in_monad) 543 apply clarsimp 544 apply (rule bisim_underlyingE1 [OF bd]) 545 apply simp 546 apply assumption+ 547 apply (rename_tac r'' t'') 548 apply (rule_tac x = "(r'', t'')" in bexI) 549 apply clarsimp 550 apply (fastforce simp: in_monad) 551 552 apply (clarsimp simp: in_monad split_def) 553 apply (erule bisim_underlyingE2) 554 apply simp 555 apply assumption+ 556 apply (frule (1) use_valid [OF _ v1 [unfolded validE_R_def validE_def]]) 557 apply clarsimp 558 apply (case_tac r) 559 apply (clarsimp simp: in_monad) 560 apply (rule_tac x = "(Inl aa, s'')" in bexI) 561 apply fastforce 562 apply (fastforce simp: in_monad) 563 apply clarsimp 564 apply (rule bisim_underlyingE2 [OF bd]) 565 apply simp 566 apply assumption+ 567 apply (rename_tac r'' t'') 568 apply (rule_tac x = "(r'', t'')" in bexI) 569 apply clarsimp 570 apply (fastforce simp: in_monad) 571 done 572 573lemma bisim_symb_exec_r_bs: 574 assumes bs: "bisim (=) R R' (return ()) m" 575 and z: "\<And>rv. bisim r P P' x (y rv)" 576 shows "bisim r (P and R and P') R' x (m >>= (\<lambda>rv. y rv))" 577 apply (rule bisim_guard_imp) 578 apply (subst return_bind [symmetric, where f = "\<lambda>(_ :: unit).x"], rule bisim_split_req) 579 apply (rule bs) 580 apply (rule z) 581 apply wp 582 apply simp 583 apply simp+ 584 done 585 586end 587