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