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