1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Corres_UL 8imports 9 Crunch_Instances_NonDet 10 WPEx 11 WPFix 12 HaskellLemmaBucket 13begin 14 15text \<open>Definition of correspondence\<close> 16 17definition 18 corres_underlying :: "(('s \<times> 't) set) \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> 19 ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('t \<Rightarrow> bool) 20 \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('t, 'b) nondet_monad \<Rightarrow> bool" 21where 22 "corres_underlying srel nf nf' rrel G G' \<equiv> \<lambda>m m'. 23 \<forall>(s, s') \<in> srel. G s \<and> G' s' \<longrightarrow> 24 (nf \<longrightarrow> \<not> snd (m s)) \<longrightarrow> 25 (\<forall>(r', t') \<in> fst (m' s'). \<exists>(r, t) \<in> fst (m s). (t, t') \<in> srel \<and> rrel r r') \<and> 26 (nf' \<longrightarrow> \<not> snd (m' s'))" 27 28text \<open>Base case facts about correspondence\<close> 29 30lemma corres_underlyingD: 31 "\<lbrakk> corres_underlying R nf nf' rs P P' f f'; (s,s') \<in> R; P s; P' s'; nf \<longrightarrow> \<not> snd (f s) \<rbrakk> 32 \<Longrightarrow> (\<forall>(r',t')\<in>fst (f' s'). \<exists>(r,t)\<in>fst (f s). (t, t') \<in> R \<and> rs r r') \<and> (nf' \<longrightarrow> \<not> snd (f' s'))" 33 by (fastforce simp: corres_underlying_def) 34 35lemma corres_underlyingD2: 36 "\<lbrakk> corres_underlying R nf nf' rs P P' f f'; (s,s') \<in> R; P s; P' s'; (r',t')\<in>fst (f' s'); nf \<longrightarrow> \<not> snd (f s) \<rbrakk> 37 \<Longrightarrow> \<exists>(r,t)\<in>fst (f s). (t, t') \<in> R \<and> rs r r'" 38 by (fastforce dest: corres_underlyingD) 39 40lemma propagate_no_fail: 41 "\<lbrakk> corres_underlying S nf True R P P' f f'; 42 no_fail P f; \<forall>s'. P' s' \<longrightarrow> (\<exists>s. P s \<and> (s,s') \<in> S) \<rbrakk> 43 \<Longrightarrow> no_fail P' f'" 44 apply (clarsimp simp: corres_underlying_def no_fail_def) 45 apply (erule allE, erule (1) impE) 46 apply clarsimp 47 apply (drule (1) bspec, clarsimp) 48 done 49 50lemma corres_underlying_serial: 51 "\<lbrakk> corres_underlying S False True rrel G G' m m'; empty_fail m' \<rbrakk> \<Longrightarrow> 52 \<forall>s. (\<exists>s'. (s,s') \<in> S \<and> G s \<and> G' s') \<longrightarrow> fst (m s) \<noteq> {}" 53 apply (clarsimp simp: corres_underlying_def empty_fail_def) 54 apply (drule_tac x="(s, s')" in bspec, simp) 55 apply (drule_tac x=s' in spec) 56 apply auto 57 done 58 59(* FIXME: duplicated with HOL.iff_allI *) 60lemma All_eqI: 61 assumes ass: "\<And>x. A x = B x" 62 shows "(\<forall>x. A x) = (\<forall>x. B x)" 63 apply (subst ass) 64 apply (rule refl) 65 done 66 67lemma corres_singleton: 68 "corres_underlying sr nf nf' r P P' (\<lambda>s. ({(R s, S s)},x)) (\<lambda>s. ({(R' s, S' s)},False)) 69 = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<and> (nf \<longrightarrow> \<not> x) 70 \<longrightarrow> ((S s, S' s') \<in> sr \<and> r (R s) (R' s')))" 71 by (auto simp: corres_underlying_def) 72 73lemma corres_return[simp]: 74 "corres_underlying sr nf nf' r P P' (return a) (return b) = 75 ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r a b)" 76 by (simp add: return_def corres_singleton) 77 78lemma corres_get[simp]: 79 "corres_underlying sr nf nf' r P P' get get = 80 (\<forall> s s'. (s, s') \<in> sr \<and> P s \<and> P' s' \<longrightarrow> r s s')" 81 apply (simp add: get_def corres_singleton) 82 apply (rule All_eqI)+ 83 apply safe 84 done 85 86lemma corres_gets[simp]: 87 "corres_underlying sr nf nf' r P P' (gets a) (gets b) = 88 (\<forall> s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (a s) (b s'))" 89 by (simp add: simpler_gets_def corres_singleton) 90 91lemma corres_throwError[simp]: 92 "corres_underlying sr nf nf' r P P' (throwError a) (throwError b) = 93 ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r (Inl a) (Inl b))" 94 by (simp add: throwError_def) 95 96lemma corres_no_failI_base: 97 assumes f: "nf \<Longrightarrow> no_fail P f" 98 assumes f': "nf' \<Longrightarrow> no_fail P' f'" 99 assumes corres: "\<forall>(s, s') \<in> S. P s \<and> P' s' \<longrightarrow> 100 (\<forall>(r', t') \<in> fst (f' s'). \<exists>(r, t) \<in> fst (f s). (t, t') \<in> S \<and> R r r')" 101 shows "corres_underlying S nf nf' R P P' f f'" 102 using assms by (simp add: corres_underlying_def no_fail_def) 103 104(* This lemma gets the shorter name because many existing proofs want nf=False *) 105lemma corres_no_failI: 106 assumes f': "nf' \<Longrightarrow> no_fail P' f'" 107 assumes corres: "\<forall>(s, s') \<in> S. P s \<and> P' s' \<longrightarrow> 108 (\<forall>(r', t') \<in> fst (f' s'). \<exists>(r, t) \<in> fst (f s). (t, t') \<in> S \<and> R r r')" 109 shows "corres_underlying S False nf' R P P' f f'" 110 using assms by (simp add: corres_underlying_def no_fail_def) 111 112text \<open>Congruence rules for the correspondence functions.\<close> 113 114(* Rewrite everywhere, with full context. Use when there are no schematic variables. *) 115lemma corres_cong: 116 assumes "\<And>s. P s = P' s" 117 assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q s' = Q' s'" 118 assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s; Q' s' \<rbrakk> \<Longrightarrow> f s = f' s" 119 assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s; Q' s' \<rbrakk> \<Longrightarrow> g s' = g' s'" 120 assumes "\<And>x y s t s' t'. \<lbrakk> P' s; Q' t; (s', t') \<in> sr; 121 (x, s') \<in> fst (f' s); (y, t') \<in> fst (g' t) \<rbrakk> \<Longrightarrow> r x y = r' x y" 122 shows "corres_underlying sr nf nf' r P Q f g = corres_underlying sr nf nf' r' P' Q' f' g'" 123 by (force simp: corres_underlying_def assms split_def) 124 125(* Do not rewrite return relation or guards, but do rewrite monads under guard context. 126 This should be the default, because it protects potential schematics in return relation 127 and guards. *) 128lemmas corres_weak_cong = corres_cong[OF refl refl _ _ refl] 129 130(* Even more restrictive: only rewrite monads, no additional context. Occasionally useful *) 131lemma corres_weaker_cong: 132 assumes "f = f'" 133 assumes "g = g'" 134 shows "corres_underlying sr nf nf' r P Q f g = corres_underlying sr nf nf' r P Q f' g'" 135 by (simp add: assms cong: corres_cong) 136 137(* Rewrite only the return relation, with context. Occasionally useful: *) 138lemmas corres_rel_cong = corres_cong[OF refl refl refl refl] 139 140(* Rewrite only the guards, with the state relation as context. Use when guards are not schematic. *) 141lemmas corres_guard_cong = corres_cong[OF _ _ refl refl refl] 142 143bundle corres_default_cong = corres_weak_cong[cong] 144bundle corres_cong = corres_cong[cong] 145bundle corres_no_cong = corres_cong[cong del] 146 147(* How to use these: *) 148experiment 149begin 150 151lemma 152 assumes cross_rule: "\<And>s s'. \<lbrakk> (s,s') \<in> sr; Q s \<rbrakk> \<Longrightarrow> Q' s'" 153 shows "corres_underlying sr nf nf' r (K P and Q) (Q' and K P) (assert P) (do get; assert P od)" 154 including corres_no_cong (* current default *) 155 apply simp (* simplifies K, but nothing else *) 156 including corres_cong 157 apply simp (* turns asserts into returns, simplifies pred_and, removes P from rhs guard *) 158 apply (simp add: cross_rule) (* turns concrete guard into True *) 159 oops 160 161schematic_goal 162 "\<And>x y z. \<lbrakk> x = Suc z; y = 0 \<rbrakk> \<Longrightarrow> 163 corres_underlying sr nf nf' (?r x y) (\<lambda>s. P z) (?Q x y) (assert (P z)) g" 164 including corres_default_cong 165 apply simp (* Turns assert into return, but does not touch schematics *) 166 including corres_no_cong 167 apply simp (* substitutes into schematic params, messy *) 168 oops 169 170(* Mixing schematic guards with non-schematic guards only works if the non-schematic guard 171 is in the right form already. It explicitly does not get rewritten by the cong rule: *) 172schematic_goal 173 "\<And>x y z. \<lbrakk> x = Suc z; y = 0 \<rbrakk> \<Longrightarrow> 174 corres_underlying sr nf nf' (?r x y) (K P) (?Q x y) (assert P) (do assert P; g od)" 175 including corres_default_cong 176 apply simp (* Only rewrite K_bind, because (K P) does not get rewritten 177 before it can be applied to (assert P) *) 178 (* You can make specific variants on the fly. Replace all bits that should not be rewritten 179 with refl like this: *) 180 apply (simp cong: corres_cong[OF _ refl _ _ refl]) (* Does not touch concrete guard and 181 return relation, rewrites the rest *) 182 (* Note that the last refl (for return relation) is important -- without it the rule does 183 nothing, probably because it would instantiate something *) 184 oops 185 186(* Mixing schematics within one guard will ignore that guard for rewriting: *) 187schematic_goal 188 "corres_underlying sr nf nf' (?r x y) (\<lambda>s. P \<and> ?P') (?Q x y) (assert P) g" 189 including corres_default_cong 190 apply simp (* Does nothing visible, because ?P' might get instantiated if used as a rewrite rule *) 191 oops 192 193end 194 195text \<open>The guard weakening rule\<close> 196 197lemma stronger_corres_guard_imp: 198 assumes x: "corres_underlying sr nf nf' r Q Q' f g" 199 assumes y: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> Q s" 200 assumes z: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> Q' s'" 201 shows "corres_underlying sr nf nf' r P P' f g" 202 using x by (auto simp: y z corres_underlying_def) 203 204lemma corres_guard_imp: 205 assumes x: "corres_underlying sr nf nf' r Q Q' f g" 206 assumes y: "\<And>s. P s \<Longrightarrow> Q s" "\<And>s. P' s \<Longrightarrow> Q' s" 207 shows "corres_underlying sr nf nf' r P P' f g" 208 apply (rule stronger_corres_guard_imp) 209 apply (rule x) 210 apply (simp add: y)+ 211 done 212 213lemma corres_rel_imp: 214 assumes x: "corres_underlying sr nf nf' r' P P' f g" 215 assumes y: "\<And>x y. r' x y \<Longrightarrow> r x y" 216 shows "corres_underlying sr nf nf' r P P' f g" 217 apply (insert x) 218 apply (simp add: corres_underlying_def) 219 apply clarsimp 220 apply (drule (1) bspec, clarsimp) 221 apply (drule (1) bspec, clarsimp) 222 apply (blast intro: y) 223 done 224 225text \<open>Splitting rules for correspondence of composite monads\<close> 226 227lemma corres_underlying_split: 228 assumes ac: "corres_underlying s nf nf' r' G G' a c" 229 assumes valid: "\<lbrace>G\<rbrace> a \<lbrace>P\<rbrace>" "\<lbrace>G'\<rbrace> c \<lbrace>P'\<rbrace>" 230 assumes bd: "\<forall>rv rv'. r' rv rv' \<longrightarrow> 231 corres_underlying s nf nf' r (P rv) (P' rv') (b rv) (d rv')" 232 shows "corres_underlying s nf nf' r G G' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" 233 using ac bd valid 234 apply (clarsimp simp: corres_underlying_def bind_def) 235 apply (clarsimp simp: Bex_def Ball_def valid_def) 236 apply meson 237 done 238 239lemma corres_split': 240 assumes x: "corres_underlying sr nf nf' r' P P' a c" 241 assumes y: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (Q rv) (Q' rv') (b rv) (d rv')" 242 assumes "\<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>" "\<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>" 243 shows "corres_underlying sr nf nf' r P P' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" 244 by (fastforce intro!: corres_underlying_split assms) 245 246text \<open>Derivative splitting rules\<close> 247 248lemma corres_split: 249 assumes y: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')" 250 assumes x: "corres_underlying sr nf nf' r' P P' a c" 251 assumes "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>" 252 shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" 253 using assms 254 apply - 255 apply (rule corres_split') 256 apply (rule corres_guard_imp, rule x, simp_all) 257 apply (erule y) 258 apply (rule hoare_weaken_pre, assumption) 259 apply simp 260 apply (rule hoare_weaken_pre, assumption) 261 apply simp 262 done 263 264primrec 265 rel_sum_comb :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) 266 \<Rightarrow> ('a + 'c \<Rightarrow> 'b + 'd \<Rightarrow> bool)" (infixl "\<oplus>" 95) 267where 268 "(f \<oplus> g) (Inr x) y = (\<exists>y'. y = Inr y' \<and> (g x y'))" 269| "(f \<oplus> g) (Inl x) y = (\<exists>y'. y = Inl y' \<and> (f x y'))" 270 271lemma rel_sum_comb_r2[simp]: 272 "(f \<oplus> g) x (Inr y) = (\<exists>x'. x = Inr x' \<and> g x' y)" 273 apply (case_tac x, simp_all) 274 done 275 276lemma rel_sum_comb_l2[simp]: 277 "(f \<oplus> g) x (Inl y) = (\<exists>x'. x = Inl x' \<and> f x' y)" 278 apply (case_tac x, simp_all) 279 done 280 281lemma corres_splitEE: 282 assumes y: "\<And>rv rv'. r' rv rv' 283 \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (R rv) (R' rv') (b rv) (d rv')" 284 assumes "corres_underlying sr nf nf' (f \<oplus> r') P P' a c" 285 assumes x: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" 286 shows "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>rv. b rv)) (c >>=E (\<lambda>rv'. d rv'))" 287 using assms 288 apply (unfold bindE_def validE_def) 289 apply (rule corres_split) 290 defer 291 apply assumption+ 292 apply (case_tac rv) 293 apply (clarsimp simp: lift_def y)+ 294 done 295 296lemma corres_split_handle: 297 assumes y: "\<And>ft ft'. f' ft ft' 298 \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft')" 299 assumes "corres_underlying sr nf nf' (f' \<oplus> r) P P' a c" 300 assumes x: "\<lbrace>Q\<rbrace> a \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E'\<rbrace>" 301 shows "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a <handle> (\<lambda>ft. b ft)) (c <handle> (\<lambda>ft'. d ft'))" 302 using assms 303 apply (simp add: handleE_def handleE'_def validE_def) 304 apply (rule corres_split) 305 defer 306 apply assumption+ 307 apply (case_tac v, simp_all, safe, simp_all add: y) 308 done 309 310lemma corres_split_catch: 311 assumes y: "\<And>ft ft'. f ft ft' \<Longrightarrow> corres_underlying sr nf nf' r (E ft) (E' ft') (b ft) (d ft')" 312 assumes x: "corres_underlying sr nf nf' (f \<oplus> r) P P' a c" 313 assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E'\<rbrace>" 314 shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a <catch> (\<lambda>ft. b ft)) (c <catch> (\<lambda>ft'. d ft'))" 315 apply (simp add: catch_def) 316 apply (rule corres_split [OF _ x, where R="case_sum E \<top>\<top>" and R'="case_sum E' \<top>\<top>"]) 317 apply (case_tac x) 318 apply (clarsimp simp: y) 319 apply clarsimp 320 apply (insert z) 321 apply (simp add: validE_def valid_def split_def split: sum.splits)+ 322 done 323 324lemma corres_split_eqr: 325 assumes y: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' rv) (b rv) (d rv)" 326 assumes x: "corres_underlying sr nf nf' (=) P P' a c" "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>" 327 shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= d)" 328 apply (rule corres_split[OF _ x]) 329 apply (simp add: y) 330 done 331 332definition 333 "dc \<equiv> \<lambda>rv rv'. True" 334 335lemma dc_simp[simp]: "dc a b" 336 by (simp add: dc_def) 337 338lemma dc_o_simp1[simp]: "dc \<circ> f = dc" 339 by (simp add: dc_def o_def) 340 341lemma dc_o_simp2[simp]: "dc x \<circ> f = dc x" 342 by (simp add: dc_def o_def) 343 344lemma unit_dc_is_eq: 345 "(dc::unit\<Rightarrow>_\<Rightarrow>_) = (=)" 346 by (fastforce simp: dc_def) 347 348lemma corres_split_nor: 349 "\<lbrakk> corres_underlying sr nf nf' r R R' b d; corres_underlying sr nf nf' dc P P' a c; 350 \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>x. R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>x. R'\<rbrace> \<rbrakk> 351 \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b)) (c >>= (\<lambda>rv. d))" 352 apply (rule corres_split, assumption+) 353 done 354 355lemma corres_split_norE: 356 "\<lbrakk> corres_underlying sr nf nf' (f \<oplus> r) R R' b d; corres_underlying sr nf nf' (f \<oplus> dc) P P' a c; 357 \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>x. R\<rbrace>, \<lbrace>\<top>\<top>\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>x. R'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace> \<rbrakk> 358 \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>rv. b)) (c >>=E (\<lambda>rv. d))" 359 apply (rule corres_splitEE, assumption+) 360 done 361 362lemma corres_split_eqrE: 363 assumes y: "\<And>rv. corres_underlying sr nf nf' (f \<oplus> r) (R rv) (R' rv) (b rv) (d rv)" 364 assumes z: "corres_underlying sr nf nf' (f \<oplus> (=)) P P' a c" 365 assumes x: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" 366 shows "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>rv. b rv)) (c >>=E d)" 367 apply (rule corres_splitEE[OF _ z x]) 368 apply (simp add: y) 369 done 370 371lemma corres_split_mapr: 372 assumes x: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' (f rv)) (b rv) (d (f rv))" 373 assumes y: "corres_underlying sr nf nf' ((=) \<circ> f) P P' a c" 374 assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>" 375 shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= d)" 376 apply (rule corres_split[OF _ y z]) 377 apply simp 378 apply (drule sym) 379 apply (simp add: x) 380 done 381 382lemma corres_split_maprE: 383 assumes y: "\<And>rv. corres_underlying sr nf nf' (r' \<oplus> r) (R rv) (R' (f rv)) (b rv) (d (f rv))" 384 assumes z: "corres_underlying sr nf nf' (r' \<oplus> ((=) \<circ> f)) P P' a c" 385 assumes x: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" 386 shows "corres_underlying sr nf nf' (r' \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>rv. b rv)) (c >>=E d)" 387 apply (rule corres_splitEE[OF _ z x]) 388 apply simp 389 apply (drule sym) 390 apply (simp add: y) 391 done 392 393text \<open>Some rules for walking correspondence into basic constructs\<close> 394 395lemma corres_if: 396 "\<lbrakk> G = G'; corres_underlying sr nf nf' r P P' a c; corres_underlying sr nf nf' r Q Q' b d \<rbrakk> 397 \<Longrightarrow> corres_underlying sr nf nf' r 398 (if G then P else Q) (if G' then P' else Q') 399 (if G then a else b) (if G' then c else d)" 400 by simp 401 402lemma corres_whenE: 403 "\<lbrakk> G = G'; corres_underlying sr nf nf' (fr \<oplus> r) P P' f g; r () () \<rbrakk> 404 \<Longrightarrow> corres_underlying sr nf nf' (fr \<oplus> r) (\<lambda>s. G \<longrightarrow> P s) (\<lambda>s. G' \<longrightarrow> P' s) (whenE G f) (whenE G' g)" 405 by (simp add: whenE_def returnOk_def) 406 407lemmas corres_if2 = corres_if[unfolded if_apply_def2] 408lemmas corres_when = 409 corres_if2[where b="return ()" and d="return ()" 410 and Q="\<top>" and Q'="\<top>" and r=dc, simplified, 411 folded when_def] 412 413lemma corres_if_r: 414 "\<lbrakk> corres_underlying sr nf nf' r P P' a c; corres_underlying sr nf nf' r P Q' a d \<rbrakk> 415 \<Longrightarrow> corres_underlying sr nf nf' r (P) (if G' then P' else Q') 416 (a) (if G' then c else d)" 417 by (simp) 418 419lemma corres_if3: 420 "\<lbrakk> G = G'; 421 G \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; 422 \<not> G' \<Longrightarrow> corres_underlying sr nf nf' r Q Q' b d \<rbrakk> 423 \<Longrightarrow> corres_underlying sr nf nf' r (if G then P else Q) (if G' then P' else Q') 424 (if G then a else b) (if G' then c else d)" 425 by simp 426 427 428text \<open>Some equivalences about liftM and other useful simps\<close> 429 430lemma snd_liftM [simp]: 431 "snd (liftM t f s) = snd (f s)" 432 by (auto simp: liftM_def bind_def return_def) 433 434lemma corres_liftM_simp[simp]: 435 "(corres_underlying sr nf nf' r P P' (liftM t f) g) 436 = (corres_underlying sr nf nf' (r \<circ> t) P P' f g)" 437 apply (simp add: corres_underlying_def 438 handy_liftM_lemma Ball_def Bex_def) 439 apply (rule All_eqI)+ 440 apply blast 441 done 442 443lemma corres_liftM2_simp[simp]: 444 "corres_underlying sr nf nf' r P P' f (liftM t g) = 445 corres_underlying sr nf nf' (\<lambda>x. r x \<circ> t) P P' f g" 446 apply (simp add: corres_underlying_def 447 handy_liftM_lemma Ball_def) 448 apply (rule All_eqI)+ 449 apply blast 450 done 451 452lemma corres_liftE_rel_sum[simp]: 453 "corres_underlying sr nf nf' (f \<oplus> r) P P' (liftE m) (liftE m') = corres_underlying sr nf nf' r P P' m m'" 454 by (simp add: liftE_liftM o_def) 455 456text \<open>Support for proving correspondence to noop with hoare triples\<close> 457 458lemma corres_noop: 459 assumes P: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> r x rv\<rbrace>" 460 assumes nf': "\<And>s. \<lbrakk> P s; nf' \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f" 461 shows "corres_underlying sr nf nf' r P P' (return x) f" 462 apply (simp add: corres_underlying_def return_def) 463 apply clarsimp 464 apply (frule P) 465 apply (insert nf') 466 apply (clarsimp simp: valid_def no_fail_def) 467 done 468 469lemma corres_noopE: 470 assumes P: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> r x rv\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>" 471 assumes nf': "\<And>s. \<lbrakk> P s; nf' \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f" 472 shows "corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f" 473proof - 474 have Q: "\<And>P f Q E. \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case_sum (\<lambda>e. E e s) (\<lambda>r. Q r s) r\<rbrace>" 475 by (simp add: validE_def) 476 thus ?thesis 477 apply (simp add: returnOk_def) 478 apply (rule corres_noop) 479 apply (rule hoare_post_imp) 480 defer 481 apply (rule Q) 482 apply (rule P) 483 apply assumption 484 apply (erule(1) nf') 485 apply (case_tac ra, simp_all) 486 done 487qed 488 489(* this could be stronger in the no_fail part *) 490lemma corres_noop2: 491 assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 492 assumes y: "\<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>" 493 assumes z: "nf' \<Longrightarrow> no_fail P f" "nf' \<Longrightarrow> no_fail P' g" 494 shows "corres_underlying sr nf nf' dc P P' f g" 495 apply (clarsimp simp: corres_underlying_def) 496 apply (rule conjI) 497 apply clarsimp 498 apply (rule use_exs_valid) 499 apply (rule exs_hoare_post_imp) 500 prefer 2 501 apply (rule x) 502 apply assumption 503 apply simp_all 504 apply (subgoal_tac "ba = b") 505 apply simp 506 apply (rule sym) 507 apply (rule use_valid[OF _ y], assumption+) 508 apply simp 509 apply (insert z) 510 apply (clarsimp simp: no_fail_def) 511 done 512 513text \<open>Support for dividing correspondence along 514 logical boundaries\<close> 515 516lemma corres_disj_division: 517 "\<lbrakk> P \<or> Q; P \<Longrightarrow> corres_underlying sr nf nf' r R S x y; Q \<Longrightarrow> corres_underlying sr nf nf' r T U x y \<rbrakk> 518 \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)) (\<lambda>s. (P \<longrightarrow> S s) \<and> (Q \<longrightarrow> U s)) x y" 519 apply safe 520 apply (rule corres_guard_imp) 521 apply simp 522 apply simp 523 apply simp 524 apply (rule corres_guard_imp) 525 apply simp 526 apply simp 527 apply simp 528 done 529 530lemma corres_weaker_disj_division: 531 "\<lbrakk> P \<or> Q; P \<Longrightarrow> corres_underlying sr nf nf' r R S x y; Q \<Longrightarrow> corres_underlying sr nf nf' r T U x y \<rbrakk> 532 \<Longrightarrow> corres_underlying sr nf nf' r (R and T) (S and U) x y" 533 apply (rule corres_guard_imp) 534 apply (rule corres_disj_division) 535 apply simp+ 536 done 537 538lemma corres_symmetric_bool_cases: 539 "\<lbrakk> P = P'; \<lbrakk> P; P' \<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' r Q Q' f g; 540 \<lbrakk> \<not> P; \<not> P' \<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' r R R' f g \<rbrakk> 541 \<Longrightarrow> corres_underlying srel nf nf' r (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) 542 (\<lambda>s. (P' \<longrightarrow> Q' s) \<and> (\<not> P' \<longrightarrow> R' s)) 543 f g" 544 by (cases P, simp_all) 545 546text \<open>Support for symbolically executing into the guards 547 and manipulating them\<close> 548 549lemma corres_symb_exec_l: 550 assumes z: "\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (x rv) y" 551 assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 552 assumes y: "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>" 553 assumes nf: "nf' \<Longrightarrow> no_fail P m" 554 shows "corres_underlying sr nf nf' r P P' (m >>= (\<lambda>rv. x rv)) y" 555 apply (rule corres_guard_imp) 556 apply (subst gets_bind_ign[symmetric], rule corres_split) 557 apply (rule z) 558 apply (rule corres_noop2) 559 apply (erule x) 560 apply (rule gets_wp) 561 apply (erule nf) 562 apply (rule non_fail_gets) 563 apply (rule y) 564 apply (rule gets_wp) 565 apply simp+ 566 done 567 568lemma corres_symb_exec_r: 569 assumes z: "\<And>rv. corres_underlying sr nf nf' r P (Q' rv) x (y rv)" 570 assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>Q'\<rbrace>" 571 assumes x: "\<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>" 572 assumes nf: "nf' \<Longrightarrow> no_fail P' m" 573 shows "corres_underlying sr nf nf' r P P' x (m >>= (\<lambda>rv. y rv))" 574 apply (rule corres_guard_imp) 575 apply (subst gets_bind_ign[symmetric], rule corres_split) 576 apply (rule z) 577 apply (rule corres_noop2) 578 apply (simp add: simpler_gets_def exs_valid_def) 579 apply (erule x) 580 apply (rule non_fail_gets) 581 apply (erule nf) 582 apply (rule gets_wp) 583 apply (rule y) 584 apply simp+ 585 done 586 587lemma corres_symb_exec_r_conj: 588 assumes z: "\<And>rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)" 589 assumes y: "\<lbrace>Q'\<rbrace> m \<lbrace>R'\<rbrace>" 590 assumes x: "\<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr\<rbrace>" 591 assumes nf: "\<And>s. nf' \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') m" 592 shows "corres_underlying sr nf nf' r Q (P' and Q') x (m >>= (\<lambda>rv. y rv))" 593proof - 594 have P: "corres_underlying sr nf nf' dc \<top> P' (return undefined) m" 595 apply (rule corres_noop) 596 apply (simp add: x) 597 apply (erule nf) 598 done 599 show ?thesis 600 apply (rule corres_guard_imp) 601 apply (subst return_bind[symmetric], 602 rule corres_split [OF _ P]) 603 apply (rule z) 604 apply wp 605 apply (rule y) 606 apply simp+ 607 done 608qed 609 610lemma corres_bind_return_r: 611 "corres_underlying S nf nf' (\<lambda>x y. r x (h y)) P Q f g \<Longrightarrow> 612 corres_underlying S nf nf' r P Q f (do x \<leftarrow> g; return (h x) od)" 613 by (fastforce simp: corres_underlying_def bind_def return_def) 614 615lemma corres_underlying_symb_exec_l: 616 "\<lbrakk> corres_underlying sr nf nf' dc P P' f (return ()); \<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; 617 \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> 618 \<Longrightarrow> corres_underlying sr nf nf' r P P' (f >>= g) h" 619 apply (drule(1) corres_underlying_split) 620 apply (rule return_wp) 621 apply clarsimp 622 apply (erule meta_allE, assumption) 623 apply simp 624 done 625 626text \<open>Inserting assumptions to be proved later\<close> 627 628lemma corres_req: 629 assumes x: "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; P' s' \<rbrakk> \<Longrightarrow> F" 630 assumes y: "F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 631 shows "corres_underlying sr nf nf' r P P' f g" 632 apply (cases "F") 633 apply (rule y) 634 apply assumption 635 apply (simp add: corres_underlying_def) 636 apply clarsimp 637 apply (subgoal_tac "F") 638 apply simp 639 apply (rule x, assumption+) 640 done 641 642(* Insert assumption to be proved later, on the left-hand (abstract) side *) 643lemma corres_gen_asm: 644 assumes x: "F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 645 shows "corres_underlying sr nf nf' r (P and (\<lambda>s. F)) P' f g" 646 apply (rule corres_req[where F=F]) 647 apply simp 648 apply (rule corres_guard_imp [OF x]) 649 apply simp+ 650 done 651 652(* Insert assumption to be proved later, on the right-hand (concrete) side *) 653lemma corres_gen_asm2: 654 assumes x: "F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 655 shows "corres_underlying sr nf nf' r P (P' and (\<lambda>s. F)) f g" 656 apply (rule corres_req[where F=F]) 657 apply simp 658 apply (rule corres_guard_imp [OF x]) 659 apply simp+ 660 done 661 662lemma corres_trivial: 663 "corres_underlying sr nf nf' r \<top> \<top> f g \<Longrightarrow> corres_underlying sr nf nf' r \<top> \<top> f g" 664 by assumption 665 666lemma corres_assume_pre: 667 assumes R: "\<And>s s'. \<lbrakk> P s; Q s'; (s,s') \<in> sr \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P Q f g" 668 shows "corres_underlying sr nf nf' r P Q f g" 669 apply (clarsimp simp add: corres_underlying_def) 670 apply (frule (2) R) 671 apply (clarsimp simp add: corres_underlying_def) 672 apply blast 673 done 674 675lemma corres_guard_imp2: 676 "\<lbrakk>corres_underlying sr nf nf' r Q P' f g; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 677 by (blast intro: corres_guard_imp) 678(* FIXME: names\<dots> (cf. corres_guard2_imp below) *) 679lemmas corres_guard1_imp = corres_guard_imp2 680 681lemma corres_guard2_imp: 682 "\<lbrakk>corres_underlying sr nf nf' r P Q' f g; \<And>s. P' s \<Longrightarrow> Q' s\<rbrakk> 683 \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 684 by (drule (1) corres_guard_imp[where P'=P' and Q=P], assumption+) 685 686lemma corres_initial_splitE: 687"\<lbrakk> corres_underlying sr nf nf' (f \<oplus> r') P P' a c; 688 \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (Q rv) (Q' rv') (b rv) (d rv'); 689 \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>; 690 \<lbrace>P'\<rbrace> c \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>\<rbrakk> 691\<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) P P' (a >>=E b) (c >>=E d)" 692 apply (rule corres_guard_imp) 693 apply (erule (3) corres_splitEE) 694 apply simp 695 apply simp 696 done 697 698lemma corres_assert_assume: 699 "\<lbrakk> P' \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' \<rbrakk> \<Longrightarrow> 700 corres_underlying sr nf nf' r P Q f (assert P' >>= g)" 701 by (auto simp: bind_def assert_def fail_def return_def 702 corres_underlying_def) 703 704lemma corres_assert_gen_asm_cross: 705 "\<lbrakk> \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; Q' s'\<rbrakk> \<Longrightarrow> A; 706 A \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk> 707 \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (Q and Q') f (assert A >>= g)" 708 by (metis corres_assert_assume corres_assume_pre corres_guard_imp pred_andE) 709 710lemma corres_state_assert: 711 "corres_underlying sr nf nf' rr P Q f (g ()) \<Longrightarrow> 712 (\<And>s. Q s \<Longrightarrow> R s) \<Longrightarrow> 713 corres_underlying sr nf nf' rr P Q f (state_assert R >>= g)" 714 by (clarsimp simp: corres_underlying_def state_assert_def get_def assert_def 715 return_def bind_def) 716 717lemma corres_stateAssert_assume: 718 "\<lbrakk> corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> 719 corres_underlying sr nf nf' r P Q f (stateAssert P' [] >>= g)" 720 apply (clarsimp simp: bind_assoc stateAssert_def) 721 apply (rule corres_symb_exec_r [OF _ get_sp]) 722 apply (rule corres_assert_assume) 723 apply (rule corres_assume_pre) 724 apply (erule corres_guard_imp, clarsimp+) 725 apply (wp | rule no_fail_pre)+ 726 done 727 728lemma corres_stateAssert_implied: 729 "\<lbrakk> corres_underlying sr nf nf' r P Q f (g ()); 730 \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; P' s; Q s' \<rbrakk> \<Longrightarrow> Q' s' \<rbrakk> 731 \<Longrightarrow> corres_underlying sr nf nf' r (P and P') Q f (stateAssert Q' [] >>= g)" 732 apply (clarsimp simp: bind_assoc stateAssert_def) 733 apply (rule corres_symb_exec_r [OF _ get_sp]) 734 apply (rule corres_assume_pre) 735 apply (rule corres_assert_assume) 736 apply (erule corres_guard_imp, clarsimp+) 737 apply (wp | rule no_fail_pre)+ 738 done 739 740lemma corres_assert: 741 "corres_underlying sr nf nf' dc (%_. P) (%_. Q) (assert P) (assert Q)" 742 by (clarsimp simp add: corres_underlying_def return_def) 743 744lemma corres_split2: 745 assumes corr: "\<And>a a' b b'. \<lbrakk> r a a' b b'\<rbrakk> 746 \<Longrightarrow> corres_underlying sr nf nf' r1 (P1 a b) (P1' a' b') (H a b) (H' a' b')" 747 and corr': "corres_underlying sr nf nf' (\<lambda>(a, b).\<lambda>(a', b'). r a a' b b') P P' 748 (do a \<leftarrow> F; b \<leftarrow> G; return (a, b) od) 749 (do a' \<leftarrow> F'; b' \<leftarrow> G'; return (a', b') od)" 750 and h1: "\<lbrace>P\<rbrace> do fx \<leftarrow> F; gx \<leftarrow> G; return (fx, gx) od \<lbrace>\<lambda>rv. P1 (fst rv) (snd rv)\<rbrace>" 751 and h2: "\<lbrace>P'\<rbrace> do fx \<leftarrow> F'; gx \<leftarrow> G'; return (fx, gx) od \<lbrace>\<lambda>rv. P1' (fst rv) (snd rv)\<rbrace>" 752 shows "corres_underlying sr nf nf' r1 P P' 753 (do a \<leftarrow> F; b \<leftarrow> G; H a b od) 754 (do a' \<leftarrow> F'; b' \<leftarrow> G'; H' a' b' od)" 755proof - 756 have "corres_underlying sr nf nf' r1 P P' 757 (do a \<leftarrow> F; b \<leftarrow> G; rv \<leftarrow> return (a, b); H (fst rv) (snd rv) od) 758 (do a' \<leftarrow> F'; b' \<leftarrow> G'; rv' \<leftarrow> return (a', b'); H' (fst rv') (snd rv') od)" 759 by (rule corres_split' [OF corr' corr, simplified bind_assoc, OF _ h1 h2]) 760 (simp add: split_beta split_def) 761 762 thus ?thesis by simp 763qed 764 765 766lemma corres_split3: 767 assumes corr: "\<And>a a' b b' c c'. \<lbrakk> r a a' b b' c c'\<rbrakk> 768 \<Longrightarrow> corres_underlying sr nf nf' r1 (P1 a b c) (P1' a' b' c') (H a b c) (H' a' b' c')" 769 and corr': "corres_underlying sr nf nf' (\<lambda>(a, b, c).\<lambda>(a', b', c'). r a a' b b' c c') P P' 770 (do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; return (a, b, c) od) 771 (do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; return (a', b', c') od)" 772 and h1: "\<lbrace>P\<rbrace> 773 do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; return (a, b, c) od 774 \<lbrace>\<lambda>(a, b, c). P1 a b c\<rbrace>" 775 and h2: "\<lbrace>P'\<rbrace> 776 do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; return (a', b', c') od 777 \<lbrace>\<lambda>(a', b', c'). P1' a' b' c'\<rbrace>" 778 shows "corres_underlying sr nf nf' r1 P P' 779 (do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; H a b c od) 780 (do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; H' a' b' c' od)" 781proof - 782 have "corres_underlying sr nf nf' r1 P P' 783 (do a \<leftarrow> A; b \<leftarrow> B a; c \<leftarrow> C a b; rv \<leftarrow> return (a, b, c); 784 H (fst rv) (fst (snd rv)) (snd (snd rv)) od) 785 (do a' \<leftarrow> A'; b' \<leftarrow> B' a'; c' \<leftarrow> C' a' b'; rv \<leftarrow> return (a', b', c'); 786 H' (fst rv) (fst (snd rv)) (snd (snd rv)) od)" using h1 h2 787 by - (rule corres_split' [OF corr' corr, simplified bind_assoc ], 788 simp_all add: split_beta split_def) 789 790 thus ?thesis by simp 791qed 792 793(* A little broken --- see above *) 794lemma corres_split4: 795 assumes corr: "\<And>a a' b b' c c' d d'. \<lbrakk> r a a' b b' c c' d d'\<rbrakk> 796 \<Longrightarrow> corres_underlying sr nf nf' r1 (P1 a b c d) (P1' a' b' c' d') 797 (H a b c d) (H' a' b' c' d')" 798 and corr': "corres_underlying sr nf nf' (\<lambda>(a, b, c, d).\<lambda>(a', b', c', d'). r a a' b b' c c' d d') P P' 799 (do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; return (a, b, c, d) od) 800 (do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; return (a', b', c', d') od)" 801 and h1: "\<lbrace>P\<rbrace> 802 do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; return (a, b, c, d) od 803 \<lbrace>\<lambda>(a, b, c, d). P1 a b c d\<rbrace>" 804 and h2: "\<lbrace>P'\<rbrace> 805 do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; return (a', b', c', d') od 806 \<lbrace>\<lambda>(a', b', c', d'). P1' a' b' c' d'\<rbrace>" 807 shows "corres_underlying sr nf nf' r1 P P' 808 (do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; H a b c d od) 809 (do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; H' a' b' c' d' od)" 810proof - 811 have "corres_underlying sr nf nf' r1 P P' 812 (do a \<leftarrow> A; b \<leftarrow> B; c \<leftarrow> C; d \<leftarrow> D; rv \<leftarrow> return (a, b, c, d); 813 H (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv))) od) 814 (do a' \<leftarrow> A'; b' \<leftarrow> B'; c' \<leftarrow> C'; d' \<leftarrow> D'; rv \<leftarrow> return (a', b', c', d'); 815 H' (fst rv) (fst (snd rv)) (fst (snd (snd rv))) (snd (snd (snd rv))) od)" 816 using h1 h2 817 by - (rule corres_split' [OF corr' corr, simplified bind_assoc], 818 simp_all add: split_beta split_def) 819 820 thus ?thesis by simp 821qed 822 823(* for instantiations *) 824lemma corres_inst: "corres_underlying sr nf nf' r P P' f g \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" . 825 826lemma corres_assert_opt_assume: 827 assumes "\<And>x. P' = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g x)" 828 assumes "\<And>s. Q s \<Longrightarrow> P' \<noteq> None" 829 shows "corres_underlying sr nf nf' r P Q f (assert_opt P' >>= g)" using assms 830 by (auto simp: bind_def assert_opt_def assert_def fail_def return_def 831 corres_underlying_def split: option.splits) 832 833 834text \<open>Support for proving correspondance by decomposing the state relation\<close> 835 836lemma corres_underlying_decomposition: 837 assumes x: "corres_underlying {(s, s'). P s s'} nf nf' r Pr Pr' f g" 838 and y: "\<And>s'. \<lbrace>R s'\<rbrace> f \<lbrace>\<lambda>rv s. Q s s'\<rbrace>" 839 and z: "\<And>s. \<lbrace>P s and Q s and K (Pr s) and Pr'\<rbrace> g \<lbrace>\<lambda>rv s'. R s' s\<rbrace>" 840 shows "corres_underlying {(s, s'). P s s' \<and> Q s s'} nf nf' r Pr Pr' f g" 841 using x apply (clarsimp simp: corres_underlying_def) 842 apply (elim allE, drule(1) mp, clarsimp) 843 apply (drule(1) bspec) 844 apply clarsimp 845 apply (rule rev_bexI, assumption) 846 apply simp 847 apply (erule use_valid [OF _ y]) 848 apply (erule use_valid [OF _ z]) 849 apply simp 850 done 851 852 853 854lemma corres_stronger_no_failI: 855 assumes f': "nf' \<Longrightarrow> no_fail (\<lambda>s'. \<exists>s. P s \<and> (s,s') \<in> S \<and> P' s') f'" 856 assumes corres: "\<forall>(s, s') \<in> S. P s \<and> P' s' \<longrightarrow> 857 (\<forall>(r', t') \<in> fst (f' s'). \<exists>(r, t) \<in> fst (f s). (t, t') \<in> S \<and> R r r')" 858 shows "corres_underlying S nf nf' R P P' f f'" 859 using assms 860 apply (simp add: corres_underlying_def no_fail_def) 861 apply clarsimp 862 apply (rule conjI) 863 apply clarsimp 864 apply blast 865 apply clarsimp 866 apply blast 867 done 868 869lemma corres_fail: 870 assumes no_fail: "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P s; P' s'; nf' \<rbrakk> \<Longrightarrow> False" 871 shows "corres_underlying sr nf nf' R P P' f fail" 872 using no_fail 873 by (auto simp add: corres_underlying_def fail_def) 874 875lemma corres_returnOk: 876 "(\<And>s s'. \<lbrakk> (s,s') \<in> sr; P s; P' s' \<rbrakk> \<Longrightarrow> r x y) \<Longrightarrow> 877 corres_underlying sr nf nf' (r' \<oplus> r) P P' (returnOk x) (returnOk y)" 878 apply (rule corres_noopE) 879 apply wp 880 apply clarsimp 881 apply wp 882 done 883 884lemmas corres_returnOkTT = corres_trivial [OF corres_returnOk] 885 886lemma corres_False [simp]: 887 "corres_underlying sr nf nf' r P \<bottom> f f'" 888 by (simp add: corres_underlying_def) 889 890lemma corres_liftME[simp]: 891 "corres_underlying sr nf nf' (f \<oplus> r) P P' (liftME fn m) m' 892 = corres_underlying sr nf nf' (f \<oplus> (r \<circ> fn)) P P' m m'" 893 apply (simp add: liftME_liftM) 894 apply (rule corres_cong [OF refl refl refl refl]) 895 apply (case_tac x, simp_all) 896 done 897 898lemma corres_liftME2[simp]: 899 "corres_underlying sr nf nf' (f \<oplus> r) P P' m (liftME fn m') 900 = corres_underlying sr nf nf' (f \<oplus> (\<lambda>x. r x \<circ> fn)) P P' m m'" 901 apply (simp add: liftME_liftM) 902 apply (rule corres_cong [OF refl refl refl refl]) 903 apply (case_tac y, simp_all) 904 done 905 906lemma corres_assertE_assume: 907 "\<lbrakk>\<And>s. P s \<longrightarrow> P'; \<And>s'. Q s' \<longrightarrow> Q'\<rbrakk> \<Longrightarrow> 908 corres_underlying sr nf nf' (f \<oplus> (=)) P Q (assertE P') (assertE Q')" 909 apply (simp add: corres_underlying_def assertE_def returnOk_def 910 fail_def return_def) 911 by blast 912 913definition 914 rel_prod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool)" 915 (infix "\<otimes>" 97) 916where 917 "rel_prod \<equiv> \<lambda>f g (a,b) (c,d). f a c \<and> g b d" 918 919lemma rel_prod_apply [simp]: 920 "(f \<otimes> g) (a,b) (c,d) = (f a c \<and> g b d)" 921 by (simp add: rel_prod_def) 922 923lemma mapME_x_corres_inv: 924 assumes x: "\<And>x. corres_underlying sr nf nf' (f \<oplus> dc) (P x) (P' x) (m x) (m' x)" 925 assumes y: "\<And>x P. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>x. P\<rbrace>,-" "\<And>x P'. \<lbrace>P'\<rbrace> m' x \<lbrace>\<lambda>x. P'\<rbrace>,-" 926 assumes z: "xs = ys" 927 shows "corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set ys. P' y s) 928 (mapME_x m xs) (mapME_x m' ys)" 929 unfolding z 930proof (induct ys) 931 case Nil 932 show ?case 933 by (simp add: mapME_x_def sequenceE_x_def returnOk_def) 934next 935 case (Cons z zs) 936 from Cons have IH: 937 "corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s) 938 (mapME_x m zs) (mapME_x m' zs)" . 939 show ?case 940 apply (simp add: mapME_x_def sequenceE_x_def) 941 apply (fold mapME_x_def sequenceE_x_def dc_def) 942 apply (rule corres_guard_imp) 943 apply (rule corres_splitEE) 944 apply (rule IH) 945 apply (rule x) 946 apply (fold validE_R_def) 947 apply (rule y)+ 948 apply simp+ 949 done 950qed 951 952lemma select_corres_eq: 953 "corres_underlying sr nf nf' (=) \<top> \<top> (select UNIV) (select UNIV)" 954 by (simp add: corres_underlying_def select_def) 955 956lemma corres_cases: 957 "\<lbrakk> R \<Longrightarrow> corres_underlying sr nf nf' r P P' f g; \<not>R \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g \<rbrakk> 958 \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') f g" 959 by (simp add: corres_underlying_def) blast 960 961lemma corres_cases': 962 "\<lbrakk> R \<Longrightarrow> corres_underlying sr nf nf' r P P' f g; \<not>R \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g \<rbrakk> 963 \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not>R \<longrightarrow> Q s)) 964 (\<lambda>s. (R \<longrightarrow> P' s) \<and> (\<not>R \<longrightarrow> Q' s)) f g" 965 by (cases R; simp) 966 967lemma corres_alternate1: 968 "corres_underlying sr nf nf' r P P' a c \<Longrightarrow> corres_underlying sr nf nf' r P P' (a \<sqinter> b) c" 969 apply (simp add: corres_underlying_def alternative_def) 970 apply clarsimp 971 apply (drule (1) bspec, clarsimp)+ 972 apply (rule rev_bexI) 973 apply (rule UnI1) 974 apply assumption 975 apply simp 976 done 977 978lemma corres_alternate2: 979 "corres_underlying sr nf nf' r P P' b c \<Longrightarrow> corres_underlying sr nf nf' r P P' (a \<sqinter> b) c" 980 apply (simp add: corres_underlying_def alternative_def) 981 apply clarsimp 982 apply (drule (1) bspec, clarsimp)+ 983 apply (rule rev_bexI) 984 apply (rule UnI2) 985 apply assumption 986 apply simp 987 done 988 989lemma corres_False': 990 "corres_underlying sr nf nf' r \<bottom> P' f g" 991 by (simp add: corres_underlying_def) 992 993lemma corres_symb_exec_l_Ex: 994 assumes x: "\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h" 995 shows "corres_underlying sr nf nf' r (\<lambda>s. \<exists>rv. Q rv s \<and> (rv, s) \<in> fst (f s)) P' 996 (do rv \<leftarrow> f; g rv od) h" 997 apply (clarsimp simp add: corres_underlying_def) 998 apply (cut_tac rv=rv in x) 999 apply (clarsimp simp add: corres_underlying_def) 1000 apply (drule(1) bspec, clarsimp) 1001 apply (case_tac nf) 1002 apply (clarsimp simp: bind_def') 1003 apply blast 1004 apply clarsimp 1005 apply (drule(1) bspec, clarsimp) 1006 apply (clarsimp simp: bind_def | erule rev_bexI)+ 1007 done 1008 1009lemma corres_symb_exec_r_All: 1010 assumes nf: "\<And>rv. nf' \<Longrightarrow> no_fail (Q' rv) g" 1011 assumes x: "\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv)" 1012 shows "corres_underlying sr nf nf' r P (\<lambda>s. (\<forall>p \<in> fst (g s). snd p = s \<and> Q' (fst p) s) \<and> (\<exists>rv. Q' rv s)) 1013 f (do rv \<leftarrow> g; h rv od)" 1014 apply (clarsimp simp add: corres_underlying_def bind_def) 1015 apply (rule conjI) 1016 apply clarsimp 1017 apply (cut_tac rv=aa in x) 1018 apply (clarsimp simp add: corres_underlying_def bind_def) 1019 apply (drule(1) bspec, clarsimp)+ 1020 apply (insert nf) 1021 apply (clarsimp simp: no_fail_def) 1022 apply (erule (1) my_BallE) 1023 apply (cut_tac rv="aa" in x) 1024 apply (clarsimp simp add: corres_underlying_def bind_def) 1025 apply (drule(1) bspec, clarsimp)+ 1026 done 1027 1028lemma corres_split_bind_case_sum: 1029 assumes x: "corres_underlying sr nf nf' (lr \<oplus> rr) P P' a d" 1030 assumes y: "\<And>rv rv'. lr rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (e rv')" 1031 assumes z: "\<And>rv rv'. rr rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (S rv) (S' rv') (c rv) (f rv')" 1032 assumes w: "\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> d \<lbrace>S'\<rbrace>,\<lbrace>R'\<rbrace>" 1033 shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') 1034 (a >>= (\<lambda>rv. case_sum b c rv)) (d >>= (\<lambda>rv'. case_sum e f rv'))" 1035 apply (rule corres_split [OF _ x]) 1036 defer 1037 apply (insert w)[2] 1038 apply (simp add: validE_def)+ 1039 apply (case_tac rv) 1040 apply (clarsimp simp: y) 1041 apply (clarsimp simp: z) 1042 done 1043 1044lemma whenE_throwError_corres_initial: 1045 assumes P: "frel f f'" 1046 assumes Q: "P = P'" 1047 assumes R: "\<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' m m'" 1048 shows "corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' 1049 (whenE P (throwError f ) >>=E (\<lambda>_. m )) 1050 (whenE P' (throwError f') >>=E (\<lambda>_. m'))" 1051 unfolding whenE_def 1052 apply (cases P) 1053 apply (simp add: P Q) 1054 apply (simp add: Q) 1055 apply (rule R) 1056 apply (simp add: Q) 1057 done 1058 1059lemma whenE_throwError_corres: 1060 assumes P: "frel f f'" 1061 assumes Q: "P = P'" 1062 assumes R: "\<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' m m'" 1063 shows "corres_underlying sr nf nf' (frel \<oplus> rvr) (\<lambda>s. \<not> P \<longrightarrow> Q s) (\<lambda>s. \<not> P' \<longrightarrow> Q' s) 1064 (whenE P (throwError f ) >>=E (\<lambda>_. m )) 1065 (whenE P' (throwError f') >>=E (\<lambda>_. m'))" 1066 apply (rule whenE_throwError_corres_initial) 1067 apply (simp_all add: P Q R) 1068 done 1069 1070lemma corres_move_asm: 1071 "\<lbrakk> corres_underlying sr nf nf' r P Q f g; 1072 \<And>s s'. \<lbrakk>(s,s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> Q s'\<rbrakk> 1073 \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 1074 by (fastforce simp: corres_underlying_def) 1075 1076lemmas corres_cross_over_guard = corres_move_asm[rotated] 1077 1078lemma corres_either_alternate: 1079 "\<lbrakk> corres_underlying sr nf nf' r P Pa' a c; corres_underlying sr nf nf' r P Pb' b c \<rbrakk> 1080 \<Longrightarrow> corres_underlying sr nf nf' r P (Pa' or Pb') (a \<sqinter> b) c" 1081 apply (simp add: corres_underlying_def alternative_def) 1082 apply clarsimp 1083 apply (drule (1) bspec, clarsimp)+ 1084 apply (erule disjE, clarsimp) 1085 apply (drule(1) bspec, clarsimp) 1086 apply (rule rev_bexI) 1087 apply (erule UnI1) 1088 apply simp 1089 apply (clarsimp, drule(1) bspec, clarsimp) 1090 apply (rule rev_bexI) 1091 apply (erule UnI2) 1092 apply simp 1093 done 1094 1095lemma corres_either_alternate2: 1096 "\<lbrakk> corres_underlying sr nf nf' r P R a c; corres_underlying sr nf nf' r Q R b c \<rbrakk> 1097 \<Longrightarrow> corres_underlying sr nf nf' r (P or Q) R (a \<sqinter> b) c" 1098 apply (simp add: corres_underlying_def alternative_def) 1099 apply clarsimp 1100 apply (drule (1) bspec, clarsimp)+ 1101 apply (erule disjE) 1102 apply clarsimp 1103 apply (drule(1) bspec, clarsimp) 1104 apply (rule rev_bexI) 1105 apply (erule UnI1) 1106 apply simp 1107 apply clarsimp 1108 apply (drule(1) bspec, clarsimp) 1109 apply (rule rev_bexI) 1110 apply (erule UnI2) 1111 apply simp 1112 done 1113 1114lemma option_corres: 1115 assumes None: "\<lbrakk> x = None; x' = None \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' (A None) (C None)" 1116 assumes Some: "\<And>z z'. \<lbrakk> x = Some z; x' = Some z' \<rbrakk> \<Longrightarrow> 1117 corres_underlying sr nf nf' r (Q z) (Q' z') (A (Some z)) (C (Some z'))" 1118 assumes None_eq: "(x = None) = (x' = None)" 1119 shows "corres_underlying sr nf nf' r (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>z. x = Some z \<longrightarrow> Q z s)) 1120 (\<lambda>s. (x' = None \<longrightarrow> P' s) \<and> (\<forall>z. x' = Some z \<longrightarrow> Q' z s)) 1121 (A x) (C x')" 1122 apply (cases x; cases x'; simp add: assms) 1123 apply (simp add: None flip: None_eq) 1124 apply (simp flip: None_eq) 1125 done 1126 1127 1128lemma corres_bind_return: 1129 "corres_underlying sr nf nf' r P P' (f >>= return) g \<Longrightarrow> 1130 corres_underlying sr nf nf' r P P' f g" 1131 by (simp add: corres_underlying_def) 1132 1133lemma corres_bind_return2: 1134 "corres_underlying sr nf nf' r P P' f (g >>= return) \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 1135 by simp 1136 1137lemma corres_stateAssert_implied2: 1138 assumes c: "corres_underlying sr nf nf' r P Q f g" 1139 assumes sr: "\<And>s s'. \<lbrakk>(s, s') \<in> sr; R s; R' s'\<rbrakk> \<Longrightarrow> Q' s'" 1140 assumes f: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. R\<rbrace>" 1141 assumes g: "\<lbrace>Q\<rbrace> g \<lbrace>\<lambda>_. R'\<rbrace>" 1142 shows "corres_underlying sr nf nf' dc P Q f (g >>= (\<lambda>_. stateAssert Q' []))" 1143 apply (subst bind_return[symmetric]) 1144 apply (rule corres_guard_imp) 1145 apply (rule corres_split) 1146 prefer 2 1147 apply (rule c) 1148 apply (clarsimp simp: corres_underlying_def return_def 1149 stateAssert_def bind_def get_def assert_def 1150 fail_def) 1151 apply (drule (2) sr) 1152 apply simp 1153 apply (rule f) 1154 apply (rule g) 1155 apply simp 1156 apply simp 1157 done 1158 1159lemma corres_add_noop_lhs: 1160 "corres_underlying sr nf nf' r P P' (return () >>= (\<lambda>_. f)) g 1161 \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 1162 by simp 1163 1164lemma corres_add_noop_lhs2: 1165 "corres_underlying sr nf nf' r P P' (f >>= (\<lambda>_. return ())) g 1166 \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 1167 by simp 1168 1169lemmas corres_split_noop_rhs 1170 = corres_split_nor[THEN corres_add_noop_lhs, OF _ _ return_wp] 1171 1172lemmas corres_split_noop_rhs2 1173 = corres_split_nor[THEN corres_add_noop_lhs2] 1174 1175lemmas corres_split_dc = corres_split[where r'=dc, simplified] 1176 1177lemma isLeft_case_sum: 1178 "isLeft v \<Longrightarrow> (case v of Inl v' \<Rightarrow> f v' | Inr v' \<Rightarrow> g v') = f (theLeft v)" 1179 by (clarsimp simp: isLeft_def) 1180 1181lemma corres_symb_exec_catch_r: 1182 "\<lbrakk> \<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); 1183 \<lbrace>P'\<rbrace> g \<lbrace>\<bottom>\<bottom>\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g \<rbrakk> 1184 \<Longrightarrow> corres_underlying sr nf nf' r P P' f (g <catch> h)" 1185 apply (simp add: catch_def) 1186 apply (rule corres_symb_exec_r, simp_all) 1187 apply (rule_tac F="isLeft x" in corres_gen_asm2) 1188 apply (simp add: isLeft_case_sum) 1189 apply assumption 1190 apply (simp add: validE_def) 1191 apply (erule hoare_chain, simp_all)[1] 1192 apply (simp add: isLeft_def split: sum.split_asm) 1193 done 1194 1195lemma corres_return_eq_same: 1196 "a = b \<Longrightarrow> corres_underlying srel nf' nf (=) \<top> \<top> (return a) (return b)" 1197 apply (simp add: corres_underlying_def return_def) 1198 done 1199 1200lemmas corres_discard_r = 1201 corres_symb_exec_r [where P'=P' and Q'="\<lambda>_. P'" for P', simplified] 1202 1203lemmas corres_returnTT = corres_return[where P=\<top> and P'=\<top>, THEN iffD2] 1204 1205lemma corres_assert_gen_asm: 1206 "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk> 1207 \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q f (assert F >>= g)" 1208 by (simp add: corres_gen_asm) 1209 1210lemma corres_assert_gen_asm_l: 1211 "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q (f ()) g \<rbrakk> 1212 \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q (assert F >>= f) g" 1213 by (simp add: corres_gen_asm) 1214 1215lemma corres_assert_gen_asm2: 1216 "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk> 1217 \<Longrightarrow> corres_underlying sr nf nf' r P (Q and (\<lambda>_. F)) f (assert F >>= g)" 1218 by (simp add: corres_gen_asm2) 1219 1220lemma corres_assert_gen_asm_l2: 1221 "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q (f ()) g \<rbrakk> 1222 \<Longrightarrow> corres_underlying sr nf nf' r P (Q and (\<lambda>_. F)) (assert F >>= f) g" 1223 by (simp add: corres_gen_asm2) 1224 1225lemma corres_add_guard: 1226 "\<lbrakk>\<And>s s'. \<lbrakk>Q s; Q' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s \<and> P' s'; 1227 corres_underlying sr nf nf' r (Q and P) (Q' and P') f g\<rbrakk> \<Longrightarrow> 1228 corres_underlying sr nf nf' r Q Q' f g" 1229 by (auto simp: corres_underlying_def) 1230 1231(* safer non-rewrite version of corres_gets *) 1232lemma corres_gets_trivial: 1233 "\<lbrakk>\<And>s s'. (s,s') \<in> sr \<Longrightarrow> f s = f' s' \<rbrakk> 1234 \<Longrightarrow> corres_underlying sr nf nf' (=) \<top> \<top> (gets f) (gets f')" 1235 unfolding corres_underlying_def gets_def get_def return_def bind_def 1236 by clarsimp 1237 1238(* When we are ignoring failure on the concrete side, fail does refine fail *) 1239lemma corres_underlying_fail_fail: 1240 "corres_underlying rf_sr nf False r \<top> \<top> fail fail" 1241 by (simp add: corres_underlying_def fail_def) 1242 1243(* assert refinement when concrete failure is ignored *) 1244lemma corres_underlying_assert_assert: 1245 "Q' = Q \<Longrightarrow> corres_underlying rf_sr nf False dc \<top> \<top> (assert Q) (assert Q')" 1246 by (simp add: assert_def corres_underlying_fail_fail) 1247 1248(* stateAssert refinement when concrete failure is ignored *) 1249lemma corres_underlying_stateAssert_stateAssert: 1250 assumes "\<And>s s'. \<lbrakk> (s,s') \<in> rf_sr; P s; P' s' \<rbrakk> \<Longrightarrow> Q' s' = Q s" 1251 shows "corres_underlying rf_sr nf False dc P P' (stateAssert Q []) (stateAssert Q' [])" 1252 by (auto simp: stateAssert_def get_def NonDetMonad.bind_def corres_underlying_def 1253 assert_def return_def fail_def assms) 1254 1255(* We can ignore a stateAssert in the middle of a computation even if we don't ignore abstract 1256 failure if we have separately proved no_fail for the entire computation *) 1257lemma corres_stateAssert_no_fail: 1258 "\<lbrakk> no_fail P (do v \<leftarrow> g; _ \<leftarrow> stateAssert X []; h v od); 1259 corres_underlying S False nf' r P Q (do v \<leftarrow> g; h v od) f \<rbrakk> \<Longrightarrow> 1260 corres_underlying S False nf' r P Q (do v \<leftarrow> g; _ \<leftarrow> stateAssert X []; h v od) f" 1261 apply (simp add: corres_underlying_def stateAssert_def get_def assert_def return_def no_fail_def fail_def cong: if_cong) 1262 apply (clarsimp simp: split_def NonDetMonad.bind_def split: if_splits) 1263 apply (erule allE, erule (1) impE) 1264 apply (drule (1) bspec, clarsimp)+ 1265 done 1266 1267(* We can switch to the corres framework that is allowed to assume non-failure of the abstract 1268 side when we have already proved that the abstract side doesn't fail *) 1269lemma corres_no_fail_nf: 1270 "\<lbrakk> no_fail P f; corres_underlying S True nf' r P Q f g \<rbrakk> \<Longrightarrow> 1271 corres_underlying S False nf' r P Q f g" 1272 by (simp add: corres_underlying_def no_fail_def) 1273 1274text \<open>Some setup of specialised methods.\<close> 1275 1276lemma (in strengthen_implementation) wpfix_strengthen_corres_guard_imp: 1277 "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (Q s)) 1278 \<Longrightarrow> (\<And>s. st (\<not> F) (\<longrightarrow>) (P' s) (Q' s)) 1279 \<Longrightarrow> st F (\<longrightarrow>) 1280 (corres_underlying sr nf nf' r P P' f g) 1281 (corres_underlying sr nf nf' r Q Q' f g)" 1282 by (cases F; auto elim: corres_guard_imp) 1283 1284lemmas wpfix_strengthen_corres_guard_imp[wp_fix_strgs] 1285 = strengthen_implementation.wpfix_strengthen_corres_guard_imp 1286 1287lemma corres_name_pre: 1288 "\<lbrakk> \<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> 1289 \<Longrightarrow> corres_underlying sr nf nf' r ((=) s) ((=) s') f g \<rbrakk> 1290 \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" 1291 apply (simp add: corres_underlying_def split_def 1292 Ball_def) 1293 apply blast 1294 done 1295 1296lemma corres_return_trivial: 1297 "corres_underlying srel nf' nf dc \<top> \<top> (return a) (return b)" 1298 by (simp add: corres_underlying_def return_def) 1299 1300lemma mapME_x_corres_same_xs: 1301 assumes x: "\<And>x. x \<in> set xs 1302 \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (P x) (P' x) (m x) (m' x)" 1303 assumes y: "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y \<in> set xs. P y s\<rbrace> m x \<lbrace>\<lambda>_ s. \<forall>y \<in> set xs. P y s\<rbrace>,-" 1304 "\<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y \<in> set xs. P' y s\<rbrace> m' x \<lbrace>\<lambda>_ s. \<forall>y \<in> set xs. P' y s\<rbrace>,-" 1305 assumes z: "xs = ys" 1306 shows "corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set ys. P' y s) 1307 (mapME_x m xs) (mapME_x m' ys)" 1308 apply (subgoal_tac "set ys \<subseteq> set xs 1309 \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set xs. P' y s) 1310 (mapME_x m ys) (mapME_x m' ys)") 1311 apply (simp add: z) 1312proof (induct ys) 1313 case Nil 1314 show ?case 1315 by (simp add: mapME_x_def sequenceE_x_def returnOk_def) 1316next 1317 case (Cons z zs) 1318 from Cons have IH: 1319 "corres_underlying sr nf nf' (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set xs. P x s) (\<lambda>s. \<forall>y\<in>set xs. P' y s) 1320 (mapME_x m zs) (mapME_x m' zs)" 1321 by (simp add: dc_def) 1322 from Cons have in_set: 1323 "z \<in> set xs" "set zs \<subseteq> set xs" by auto 1324 thus ?case 1325 apply (simp add: mapME_x_def sequenceE_x_def) 1326 apply (fold mapME_x_def sequenceE_x_def dc_def) 1327 apply (rule corres_guard_imp) 1328 apply (rule corres_splitEE) 1329 apply (rule IH) 1330 apply (rule x, simp) 1331 apply (wp y | simp)+ 1332 done 1333qed 1334 1335end 1336