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 rewriting under refinement. *) 8 9theory MonadicRewrite 10imports 11 NonDetMonadVCG 12 Corres_UL 13 EmptyFailLib 14 LemmaBucket 15begin 16 17definition 18 monadic_rewrite :: "bool \<Rightarrow> bool \<Rightarrow> ('a \<Rightarrow> bool) 19 \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> bool" 20where 21 "monadic_rewrite F E P f g \<equiv> \<forall>s. P s \<and> (F \<longrightarrow> \<not> snd (f s)) 22 \<longrightarrow> (E \<longrightarrow> f s = g s) 23 \<and> (\<not> E \<longrightarrow> fst (g s) \<subseteq> fst (f s) \<and> (snd (g s) \<longrightarrow> snd (f s)))" 24 25 26(* FIXME: also in Retype_C *) 27lemma snd_bind: 28 "snd ((a >>= b) s) = (snd (a s) \<or> (\<exists>(r, s') \<in> fst (a s). snd (b r s')))" 29 by (auto simp add: bind_def split_def) 30 31lemma monadic_rewrite_bind: 32 "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); 33 \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace> \<rbrakk> 34 \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= (\<lambda>x. h x)) (g >>= (\<lambda>x. j x))" 35 apply (cases E) 36 apply (clarsimp simp: monadic_rewrite_def snd_bind imp_conjL) 37 apply (drule spec, drule(1) mp, clarsimp) 38 apply (rule bind_apply_cong) 39 apply simp 40 apply (frule(2) use_valid) 41 apply fastforce 42 apply (clarsimp simp: monadic_rewrite_def snd_bind imp_conjL) 43 apply (simp add: bind_def split_def) 44 apply (rule conjI) 45 apply (rule UN_mono) 46 apply simp 47 apply clarsimp 48 apply (frule(2) use_valid) 49 apply fastforce 50 apply (rule conjI) 51 apply fastforce 52 apply clarsimp 53 apply (frule(2) use_valid) 54 apply fastforce 55 done 56 57lemma monadic_rewrite_refl: 58 "monadic_rewrite F E \<top> f f" 59 by (simp add: monadic_rewrite_def) 60 61lemma monadic_rewrite_bindE: 62 "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); 63 \<lbrace>R\<rbrace> g \<lbrace>Q\<rbrace>,- \<rbrakk> 64 \<Longrightarrow> monadic_rewrite F E (P and R) (f >>=E (\<lambda>x. h x)) (g >>=E (\<lambda>x. j x))" 65 apply (simp add: bindE_def) 66 apply (erule monadic_rewrite_bind) 67 defer 68 apply (simp add: validE_R_def validE_def) 69 apply (case_tac x, simp_all add: lift_def monadic_rewrite_refl) 70 done 71 72lemma monadic_rewrite_catch: 73 "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); 74 \<lbrace>R\<rbrace> g -,\<lbrace>Q\<rbrace> \<rbrakk> 75 \<Longrightarrow> monadic_rewrite F E (P and R) (f <catch> (\<lambda>x. h x)) (g <catch> (\<lambda>x. j x))" 76 apply (simp add: catch_def) 77 apply (erule monadic_rewrite_bind) 78 defer 79 apply (simp add: validE_E_def validE_def) 80 apply (case_tac x, simp_all add: lift_def monadic_rewrite_refl) 81 done 82 83lemma monadic_rewrite_symb_exec_pre: 84 assumes inv: "\<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>" 85 and ef: "empty_fail g" 86 and rv: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>y s. y \<in> S\<rbrace>" 87 and h': "\<And>y. y \<in> S \<longrightarrow> h y = h'" 88 shows "monadic_rewrite True True P (g >>= h) h'" 89proof - 90 have P: "\<And>s v. \<lbrakk> P s; v \<in> fst (g s) \<rbrakk> \<Longrightarrow> split h v = h' s" 91 apply clarsimp 92 apply (frule use_valid[OF _ inv], rule refl) 93 apply (frule(1) use_valid[OF _ rv]) 94 apply (simp add: h') 95 done 96 97 show ?thesis 98 apply (clarsimp simp: monadic_rewrite_def bind_def P image_constant_conv 99 cong: image_cong) 100 apply (drule empty_failD2[OF ef]) 101 apply (clarsimp simp: prod_eq_iff split: if_split_asm) 102 done 103qed 104 105lemma monadic_rewrite_trans: 106 "\<lbrakk> monadic_rewrite F E P f g; monadic_rewrite F E Q g h \<rbrakk> 107 \<Longrightarrow> monadic_rewrite F E (P and Q) f h" 108 by (auto simp add: monadic_rewrite_def) 109 110lemma singleton_eq_imp_helper: 111 "v \<in> {x} \<longrightarrow> h v = h x" by simp 112 113lemmas monadic_rewrite_symb_exec 114 = monadic_rewrite_symb_exec_pre [OF _ _ _ singleton_eq_imp_helper, 115 THEN monadic_rewrite_trans, 116 simplified] 117 118lemma eq_UNIV_imp_helper: 119 "v \<in> UNIV \<longrightarrow> x = x" by simp 120 121lemmas monadic_rewrite_symb_exec2 122 = monadic_rewrite_symb_exec_pre[OF _ _ _ eq_UNIV_imp_helper, where P=\<top>, 123 simplified, THEN monadic_rewrite_trans] 124 125lemma monadic_rewrite_imp: 126 "\<lbrakk> monadic_rewrite F E Q f g; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> monadic_rewrite F E P f g" 127 by (auto simp add: monadic_rewrite_def) 128 129lemmas monadic_rewrite_bind_tail 130 = monadic_rewrite_bind [OF monadic_rewrite_refl, simplified pred_and_true_var] 131lemmas monadic_rewrite_bind_head 132 = monadic_rewrite_bind [OF _ monadic_rewrite_refl hoare_vcg_prop, 133 simplified pred_and_true] 134 135lemma monadic_rewrite_bind2: 136 "\<lbrakk> monadic_rewrite F E P f g; \<And>x. monadic_rewrite F E (Q x) (h x) (j x); 137 \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> 138 \<Longrightarrow> monadic_rewrite F E (P and R) (f >>= (\<lambda>x. h x)) (g >>= (\<lambda>x. j x))" 139 apply (rule monadic_rewrite_imp) 140 apply (rule monadic_rewrite_trans) 141 apply (erule(1) monadic_rewrite_bind_tail) 142 apply (erule monadic_rewrite_bind_head) 143 apply simp 144 done 145 146lemma monadic_rewrite_if: 147 "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q a c; \<not> P \<Longrightarrow> monadic_rewrite F E R b d \<rbrakk> \<Longrightarrow> 148 monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) 149 (If P a b) (If P c d)" 150 by (cases P, simp_all) 151 152lemma monadic_rewrite_liftM: 153 "monadic_rewrite F E P f g \<Longrightarrow> monadic_rewrite F E P (liftM fn f) (liftM fn g)" 154 apply (simp add: liftM_def) 155 apply (erule monadic_rewrite_bind_head) 156 done 157 158lemmas monadic_rewrite_liftE 159 = monadic_rewrite_liftM[where fn=Inr, folded liftE_liftM] 160 161lemma monadic_rewrite_from_simple: 162 "P \<longrightarrow> f = g \<Longrightarrow> monadic_rewrite F E (\<lambda>_. P) f g" 163 by (simp add: monadic_rewrite_def) 164 165lemma monadic_rewrite_gen_asm: 166 "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q f g \<rbrakk> \<Longrightarrow> monadic_rewrite F E ((\<lambda>_. P) and Q) f g" 167 by (auto simp add: monadic_rewrite_def) 168 169lemma monadic_rewrite_assert: 170 "\<lbrakk> Q \<Longrightarrow> monadic_rewrite True E P (f ()) g \<rbrakk> 171 \<Longrightarrow> monadic_rewrite True E (\<lambda>s. Q \<longrightarrow> P s) (assert Q >>= f) g" 172 apply (simp add: assert_def split: if_split) 173 apply (simp add: monadic_rewrite_def fail_def) 174 done 175 176lemma monadic_rewrite_drop_modify: 177 "monadic_rewrite F E (\<lambda>s. f s = s) (modify f >>= v) (v ())" 178 by (simp add: monadic_rewrite_def bind_def simpler_modify_def) 179 180lemma monadic_rewrite_symb_exec_r: 181 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; no_fail P' m; 182 \<And>rv. monadic_rewrite F False (Q rv) x (y rv); 183 \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk> 184 \<Longrightarrow> monadic_rewrite F False (P and P') x (m >>= y)" 185 apply (clarsimp simp: monadic_rewrite_def bind_def) 186 apply (drule(1) no_failD) 187 apply (subgoal_tac "\<forall>v \<in> fst (m s). Q (fst v) (snd v) \<and> snd v = s") 188 apply fastforce 189 apply clarsimp 190 apply (frule(2) use_valid) 191 apply (frule use_valid, assumption, rule refl) 192 apply simp 193 done 194 195lemma monadic_rewrite_symb_exec_r': 196 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; no_fail P m; 197 \<And>rv. monadic_rewrite F False (Q rv) x (y rv); 198 \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk> 199 \<Longrightarrow> monadic_rewrite F False P x (m >>= y)" 200 apply (rule monadic_rewrite_imp) 201 apply (rule monadic_rewrite_symb_exec_r; assumption) 202 apply simp 203 done 204 205lemma monadic_rewrite_symb_exec_l'': 206 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; empty_fail m; 207 \<not> F \<longrightarrow> no_fail P' m; 208 \<And>rv. monadic_rewrite F False (Q rv) (x rv) y; 209 \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk> 210 \<Longrightarrow> monadic_rewrite F False (P and P') (m >>= x) y" 211 apply (clarsimp simp: monadic_rewrite_def bind_def) 212 apply (subgoal_tac "\<not> snd (m s)") 213 apply (subgoal_tac "\<forall>v \<in> fst (m s). Q (fst v) (snd v) \<and> snd v = s") 214 apply (frule(1) empty_failD2) 215 apply (clarsimp simp: split_def) 216 apply fastforce 217 apply clarsimp 218 apply (frule(2) use_valid) 219 apply (frule use_valid, assumption, rule refl) 220 apply simp 221 apply (cases F, simp_all add: no_failD) 222 done 223 224lemma monadic_rewrite_symb_exec_l': 225 "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>r. P\<rbrace>; empty_fail m; 226 \<not> F \<longrightarrow> no_fail P' m; 227 \<And>rv. monadic_rewrite F E (Q rv) (x rv) y; 228 \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk> 229 \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= x) y" 230 apply (cases E) 231 apply (clarsimp simp: monadic_rewrite_def bind_def prod_eq_iff) 232 apply (subgoal_tac "\<not> snd (m s)") 233 apply (simp add: empty_fail_def, drule_tac x=s in spec) 234 apply (subgoal_tac "\<forall>(rv, s') \<in> fst (m s). x rv s' = y s") 235 apply (rule conjI) 236 apply (rule equalityI) 237 apply (clarsimp simp: Ball_def) 238 apply (fastforce simp: Ball_def elim!: nonemptyE elim: rev_bexI) 239 apply (simp add: Bex_def Ball_def cong: conj_cong) 240 apply auto[1] 241 apply clarsimp 242 apply (drule(1) in_inv_by_hoareD) 243 apply (frule(2) use_valid) 244 apply (clarsimp simp: Ball_def prod_eq_iff) 245 apply (clarsimp simp: no_fail_def) 246 apply simp 247 apply (rule monadic_rewrite_symb_exec_l'', assumption+) 248 done 249 250(* FIXME this should replace monadic_rewrite_symb_exec_l' as it preserves names, 251 and this approach should be used everywhere else anyhow, however that breaks proofs 252 relying on arbitrarily generated names, so will be dealt with in future *) 253lemma monadic_rewrite_symb_exec_l'_preserve_names: 254 "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>r. P\<rbrace>; empty_fail m; 255 \<not> F \<longrightarrow> no_fail P' m; 256 \<And>rv. monadic_rewrite F E (Q rv) (x rv) y; 257 \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace> \<rbrakk> 258 \<Longrightarrow> monadic_rewrite F E (P and P') (m >>= (\<lambda>rv. x rv)) y" 259 by (rule monadic_rewrite_symb_exec_l') 260 261(* FIXME merge into below upon change-over desribed above *) 262lemmas monadic_rewrite_symb_exec_l'_TT 263 = monadic_rewrite_symb_exec_l'_preserve_names[where P'="\<top>" and F=True, simplified] 264 265lemmas monadic_rewrite_symb_exec_l 266 = monadic_rewrite_symb_exec_l''[where F=True and P'=\<top>, simplified] 267 monadic_rewrite_symb_exec_l''[where F=False, simplified simp_thms] 268 269lemma monadic_rewrite_alternative_rhs: 270 "\<lbrakk> monadic_rewrite F E P a b; monadic_rewrite F E Q a c \<rbrakk> 271 \<Longrightarrow> monadic_rewrite F E (P and Q) a (b \<sqinter> c)" 272 apply (clarsimp simp: monadic_rewrite_def alternative_def) 273 apply auto 274 done 275 276lemma monadic_rewrite_rdonly_bind: 277 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>rv. (=) s\<rbrace> \<rbrakk> \<Longrightarrow> 278 monadic_rewrite F False \<top> 279 (alternative (f >>= (\<lambda>x. g x)) h) 280 (f >>= (\<lambda>x. alternative (g x) h))" 281 apply (clarsimp simp: monadic_rewrite_def bind_def 282 alternative_def imp_conjL) 283 apply (subgoal_tac "\<forall>x \<in> fst (f s). snd x = s") 284 apply (simp add: image_image split_def cong: image_cong) 285 apply fastforce 286 apply clarsimp 287 apply (frule use_valid, (assumption | rule refl | simp)+) 288 done 289 290lemmas monadic_rewrite_rdonly_bind_l 291 = monadic_rewrite_trans [OF monadic_rewrite_rdonly_bind] 292 293lemma monadic_rewrite_if_rhs: 294 "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q a b; \<not> P \<Longrightarrow> monadic_rewrite F E R a c \<rbrakk> 295 \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) 296 a (If P b c)" 297 by (cases P, simp_all) 298 299lemma monadic_rewrite_transverse: 300 "\<lbrakk> monadic_rewrite False True Q c b; monadic_rewrite F E P a b \<rbrakk> 301 \<Longrightarrow> monadic_rewrite F E (P and Q) a c" 302 by (auto simp add: monadic_rewrite_def) 303 304lemma monadic_rewrite_alternative_l: 305 "monadic_rewrite F False \<top> (alternative f g) g" 306 by (clarsimp simp: monadic_rewrite_def alternative_def) 307 308lemma monadic_rewrite_introduce_alternative: 309 "\<lbrakk> f = f'; monadic_rewrite F E P (alternative f' f) g \<rbrakk> 310 \<Longrightarrow> monadic_rewrite F E P f g" 311 by (simp add: alternative_def) 312 313lemma monadic_rewrite_modify_noop: 314 "monadic_rewrite F E (\<lambda>s. f s = s) (modify f) (return ())" 315 by (clarsimp simp: monadic_rewrite_def simpler_modify_def return_def) 316 317lemma monadic_rewrite_split_fn: 318 "\<lbrakk> monadic_rewrite F E P (liftM fn a) c; 319 \<And>rv. monadic_rewrite F E (Q rv) (b rv) (d (fn rv)); 320 \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> 321 monadic_rewrite F E (P and R) (a >>= b) (c >>= d)" 322 apply (rule monadic_rewrite_imp) 323 apply (rule monadic_rewrite_trans[rotated]) 324 apply (erule monadic_rewrite_bind_head) 325 apply (simp add: liftM_def) 326 apply (erule(1) monadic_rewrite_bind_tail) 327 apply simp 328 done 329 330lemma monadic_rewrite_pick_alternative_1: 331 "monadic_rewrite F False \<top> (alternative f g) f" 332 by (auto simp add: monadic_rewrite_def alternative_def) 333 334lemma monadic_rewrite_pick_alternative_2: 335 "monadic_rewrite F False \<top> (alternative f g) g" 336 by (auto simp add: monadic_rewrite_def alternative_def) 337 338lemma monadic_rewrite_weaken: 339 "monadic_rewrite (F \<and> F') (E \<or> E') P f g 340 \<Longrightarrow> monadic_rewrite F' E' P f g" 341 apply (clarsimp simp add: monadic_rewrite_def) 342 apply auto 343 done 344 345lemma monadic_rewrite_is_refl: 346 "x = y \<Longrightarrow> monadic_rewrite F E \<top> x y" 347 by (simp add: monadic_rewrite_refl) 348 349lemma monadic_rewrite_refl3: 350 "[| !!s. P s ==> f s = g s |] ==> monadic_rewrite F E P f g" 351 by (simp add: monadic_rewrite_def) 352 353lemmas monadic_rewrite_refl2 = monadic_rewrite_refl3[where P=\<top>] 354 355lemma monadic_rewrite_cases: 356 "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q a b; \<not> P \<Longrightarrow> monadic_rewrite F E R a b \<rbrakk> 357 \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) a b" 358 by (cases P, simp_all) 359 360lemma monadic_rewrite_symb_exec_l_known: 361 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; empty_fail m; 362 monadic_rewrite True False Q (x rv) y; \<lbrace>P\<rbrace> m \<lbrace>\<lambda>rv' s. rv' = rv \<and> Q s\<rbrace> \<rbrakk> 363 \<Longrightarrow> monadic_rewrite True False P (m >>= x) y" 364 apply (erule(1) monadic_rewrite_symb_exec_l) 365 apply (rule_tac P="rva = rv" in monadic_rewrite_gen_asm) 366 apply simp 367 apply (erule hoare_strengthen_post) 368 apply simp 369 done 370 371lemma monadic_rewrite_gets_the_known_v: 372 "monadic_rewrite F E (\<lambda>s. f s = Some v) 373 (gets_the f) (return v)" 374 by (simp add: monadic_rewrite_def gets_the_def 375 exec_gets assert_opt_def) 376 377lemma monadic_rewrite_gets_the_walk: 378 "\<lbrakk> \<And>x. monadic_rewrite True False (P x) (g x) (gets_the pf >>= g' x); 379 \<And>Q. \<lbrace>\<lambda>s. Q (pf s)\<rbrace> f \<lbrace>\<lambda>rv s. Q (pf s)\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>P\<rbrace>; empty_fail f \<rbrakk> 380 \<Longrightarrow> monadic_rewrite True False R 381 (f >>= g) 382 (do v \<leftarrow> gets_the pf; x \<leftarrow> f; g' x v od)" 383 apply (rule monadic_rewrite_imp) 384 apply (rule monadic_rewrite_trans) 385 apply (erule(1) monadic_rewrite_bind_tail) 386 apply (simp add: gets_the_def bind_assoc) 387 apply (rule monadic_rewrite_symb_exec_r, wp+) 388 apply (rule monadic_rewrite_trans) 389 apply (rule monadic_rewrite_bind_tail) 390 apply (rule_tac rv=rv in monadic_rewrite_symb_exec_l_known, 391 (wp empty_fail_gets)+) 392 apply (rule monadic_rewrite_refl) 393 apply wp 394 apply assumption 395 apply (rule_tac P="rv = None" in monadic_rewrite_cases[where Q=\<top>]) 396 apply (simp add: assert_opt_def) 397 apply (clarsimp simp: monadic_rewrite_def fail_def snd_bind) 398 apply (rule ccontr, drule(1) empty_failD2) 399 apply clarsimp 400 apply (simp add: assert_opt_def case_option_If2) 401 apply (rule monadic_rewrite_refl) 402 apply wp 403 apply simp 404 done 405 406lemma monadic_rewrite_alternatives: 407 "\<lbrakk> monadic_rewrite E F P a c; monadic_rewrite E F Q b d \<rbrakk> 408 \<Longrightarrow> monadic_rewrite E F (P and Q) (a \<sqinter> b) (c \<sqinter> d)" 409 by (auto simp: monadic_rewrite_def alternative_def) 410 411lemma monadic_rewrite_weaken2: 412 "monadic_rewrite F E P f g 413 \<Longrightarrow> monadic_rewrite F' E' ((\<lambda>_. (F \<longrightarrow> F') \<and> (E' \<longrightarrow> E)) and P) f g" 414 apply (rule monadic_rewrite_gen_asm) 415 apply (rule monadic_rewrite_weaken[where F=F and E=E]) 416 apply auto 417 done 418 419lemma monadic_rewrite_case_sum: 420 "\<lbrakk> \<And>v. x = Inl v \<Longrightarrow> monadic_rewrite F E (P v) (a v) (c v); 421 \<And>v. x = Inr v \<Longrightarrow> monadic_rewrite F E (Q v) (b v) (d v) \<rbrakk> 422 \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (\<not> isRight x \<longrightarrow> P (theLeft x) s) \<and> (isRight x \<longrightarrow> Q (theRight x) s)) 423 (case_sum a b x) (case_sum c d x)" 424 by (cases x, simp_all add: isRight_def) 425 426lemma monadic_rewrite_add_gets: 427 "monadic_rewrite F E \<top> m (gets f >>= (\<lambda>_. m))" 428 by (simp add: monadic_rewrite_def exec_gets) 429 430lemma monadic_rewrite_add_assert: 431 "monadic_rewrite F E (\<lambda>s. P) m (assert P >>= (\<lambda>_. m))" 432 by (simp add: monadic_rewrite_def) 433 434lemma monadic_rewrite_gets_known: 435 "monadic_rewrite F E (\<lambda>s. f s = rv) (gets f >>= m) (m rv)" 436 by (simp add: monadic_rewrite_def exec_gets) 437 438lemma monadic_rewrite_name_pre: 439 "\<lbrakk> \<And>s. P s \<Longrightarrow> monadic_rewrite F E ((=) s) f g \<rbrakk> 440 \<Longrightarrow> monadic_rewrite F E P f g" 441 by (auto simp add: monadic_rewrite_def) 442 443lemma monadic_rewrite_named_bindE: 444 "\<lbrakk> monadic_rewrite F E ((=) s) f f'; 445 \<And>rv s'. (Inr rv, s') \<in> fst (f' s) 446 \<Longrightarrow> monadic_rewrite F E ((=) s') (g rv) (g' rv) \<rbrakk> 447 \<Longrightarrow> monadic_rewrite F E ((=) s) (f >>=E (\<lambda>rv. g rv)) (f' >>=E g')" 448 apply (rule monadic_rewrite_imp) 449 apply (erule_tac R="(=) s" and Q="\<lambda>rv s'. (Inr rv, s') \<in> fst (f' s)" in monadic_rewrite_bindE) 450 apply (rule monadic_rewrite_name_pre) 451 apply clarsimp 452 apply (clarsimp simp add: validE_R_def validE_def valid_def 453 split: sum.split) 454 apply simp 455 done 456 457lemmas monadic_rewrite_named_if 458 = monadic_rewrite_if[where Q="(=) s" and R="(=) s", simplified] for s 459 460lemma monadic_rewrite_if_lhs: 461 "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q b a; \<not> P \<Longrightarrow> monadic_rewrite F E R c a \<rbrakk> 462 \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) 463 (If P b c) a" 464 by (cases P, simp_all) 465 466lemma monadic_rewrite_to_eq: 467 "monadic_rewrite False True \<top> f g ==> f = g" 468 by (simp add: monadic_rewrite_def fun_eq_iff) 469 470lemma corres_underlyingI: 471 assumes rv: "\<And>s t rv' t'. \<lbrakk>(s, t) \<in> R; P s; P' t; (rv', t') \<in> fst (c t)\<rbrakk> \<Longrightarrow> \<exists>(rv, s') \<in> fst (a s). (s', t') \<in> R \<and> r rv rv'" 472 and nf: "\<And>s t. \<lbrakk>(s, t) \<in> R; P s; P' t; nf'\<rbrakk> \<Longrightarrow> \<not> snd (c t)" 473 shows "corres_underlying R nf nf' r P P' a c" 474 unfolding corres_underlying_def using rv nf by (auto simp: split_def) 475 476lemma corres_underlyingE: 477 assumes cul: "corres_underlying R nf nf' r P P' a c" 478 and xin: "(s, t) \<in> R" "P s" "P' t" "(rv', t') \<in> fst (c t)" 479 and rl: "\<And>s' rv. \<lbrakk>nf' \<longrightarrow> \<not> snd (c t); (rv, s') \<in> fst (a s); (s', t') \<in> R; r rv rv'\<rbrakk> \<Longrightarrow> Q" 480 and nf: "nf \<longrightarrow> \<not> snd (a s)" 481 shows "Q" 482 using cul xin nf 483 unfolding corres_underlying_def by (fastforce simp: split_def intro: rl) 484 485(* Above here is generic *) 486lemma monadic_rewrite_corres: 487 assumes cu: "corres_underlying R False nf' r P P' a' c" 488 and me: "monadic_rewrite False True Q a a'" 489 shows "corres_underlying R False nf' r (P and Q) P' a c" 490proof (rule corres_underlyingI) 491 fix s t rv' t' 492 assume st: "(s, t) \<in> R" and pq: "(P and Q) s" and pt: "P' t" and ct: "(rv', t') \<in> fst (c t)" 493 from pq have Ps: "P s" and Qs: "Q s" by simp_all 494 495 from cu st Ps pt ct obtain s' rv where 496 as': "(rv, s') \<in> fst (a' s)" and rest: "nf' \<longrightarrow> \<not> snd (c t)" "(s', t') \<in> R" "r rv rv'" 497 by (fastforce elim: corres_underlyingE) 498 499 from me st Qs as' have as: "(rv, s') \<in> fst (a s)" 500 by (clarsimp simp: monadic_rewrite_def) 501 502 with rest show "\<exists>(rv, s')\<in>fst (a s). (s', t') \<in> R \<and> r rv rv'" by auto 503next 504 fix s t 505 assume "(s, t) \<in> R" "(P and Q) s" "P' t" "nf'" 506 thus "\<not> snd (c t)" using cu 507 by (fastforce simp: corres_underlying_def split_def) 508qed 509 510lemma monadic_rewrite_refine_valid: 511 "monadic_rewrite F E P f g 512 \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> 513 \<Longrightarrow> F \<longrightarrow> no_fail P'' f 514 \<Longrightarrow> \<lbrace>P and P' and P''\<rbrace> g \<lbrace>Q\<rbrace>" 515 apply (clarsimp simp: monadic_rewrite_def valid_def no_fail_def imp_conjL) 516 apply (drule spec, drule(1) mp)+ 517 apply (clarsimp simp: Ball_def) 518 apply auto 519 done 520 521lemma monadic_rewrite_refine_validE_R: 522 "monadic_rewrite F E P f g 523 \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, - 524 \<Longrightarrow> F \<longrightarrow> no_fail P'' f 525 \<Longrightarrow> \<lbrace>P and P' and P''\<rbrace> g \<lbrace>Q\<rbrace>, -" 526 by (simp add: validE_R_def validE_def monadic_rewrite_refine_valid) 527 528lemma wpc_helper_monadic_rewrite: 529 "monadic_rewrite F E Q' m m' 530 \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (monadic_rewrite F E (\<lambda>s. s \<in> P') m m')" 531 apply (clarsimp simp: wpc_helper_def) 532 apply (erule monadic_rewrite_imp) 533 apply auto 534 done 535 536lemma monadic_rewrite_trans_dup: 537 "\<lbrakk> monadic_rewrite F E P f g; monadic_rewrite F E P g h \<rbrakk> 538 \<Longrightarrow> monadic_rewrite F E P f h" 539 by (auto simp add: monadic_rewrite_def) 540 541lemmas monadic_rewrite_bind_alt 542 = monadic_rewrite_trans[OF monadic_rewrite_bind_tail monadic_rewrite_bind_head, rotated -1] 543 544wpc_setup "\<lambda>m. monadic_rewrite F E Q' m m'" wpc_helper_monadic_rewrite 545wpc_setup "\<lambda>m. monadic_rewrite F E Q' (m >>= c) m'" wpc_helper_monadic_rewrite 546 547end 548