1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8 * Corres/Refinement for capDL 9 * 10 * Instantiates corres_underlying with capDL state translation and types. 11 *) 12 13theory Corres_D 14imports StateTranslationProofs_DR 15begin 16 17lemma truncate_state_unit[simp]: "truncate_state s = s" by simp 18 19declare dxo_noop[simp] 20 21lemma select_ext_select[simp]: "select_ext a S = (select S :: ('b, unit) s_monad)" 22 by (rule ext) 23 (auto simp: select_ext_def select_switch_unit_def assert_def get_def select_def 24 return_def bind_def fail_def image_def 25 split: if_split_asm) 26 27lemma OR_choice_OR[simp]: "(OR_choice c (f :: ('a,unit) s_monad) g) = (f \<sqinter> g)" 28 apply (rule ext, rename_tac s) 29 apply (clarsimp simp: OR_choice_def alternative_def get_def select_def return_def bind_def 30 select_f_def mk_ef_def wrap_ext_unit_def wrap_ext_bool_unit_def image_def 31 split: if_split_asm) 32 apply (case_tac "f s") 33 apply (case_tac "g s") 34 by (intro conjI set_eqI; clarsimp?; blast) 35 36lemma OR_choiceE_OR[simp]: "(OR_choiceE c (f :: ('a + 'b,unit) s_monad) g) = (f \<sqinter> g)" 37 apply (clarsimp simp: OR_choiceE_def bindE_def liftE_def) 38 apply (clarsimp simp: alternative_def get_def select_def return_def bind_def select_f_def 39 mk_ef_def wrap_ext_unit_def wrap_ext_bool_unit_def image_def 40 split: if_split_asm) 41 apply (rule ext, rename_tac s) 42 apply (case_tac "f s") 43 apply (case_tac "g s") 44 apply clarsimp 45 by (intro conjI set_eqI; clarsimp?; blast) 46 47(* state relation as set, in (simp split_def) normal form *) 48abbreviation 49dcorres :: 50 "('a::type \<Rightarrow> 'b::type \<Rightarrow> bool) 51 \<Rightarrow> (cdl_state \<Rightarrow> bool) 52 \<Rightarrow> (det_state \<Rightarrow> bool) 53 \<Rightarrow> 'a::type k_monad 54 \<Rightarrow> (det_state 55 \<Rightarrow> ('b::type \<times> det_state) set \<times> 56 bool) 57 \<Rightarrow> bool" 58where 59 "dcorres \<equiv> corres_underlying {ss'. transform (snd ss') = fst ss'} False False" 60 61(* Some obvious corres lemmas *) 62lemma corres_group_bind_rhs: 63 "corres_underlying sr nf nf' rvr P P' a (do y\<leftarrow>(do f; g od); h y od) 64 \<Longrightarrow> corres_underlying sr nf nf' rvr P P' a (do x \<leftarrow> f; y \<leftarrow> g; h y od)" 65 by (simp add: bind_assoc) 66 67lemma corres_expand_bind_rhs: 68 "dcorres rvr P P' a (do z \<leftarrow> f; y \<leftarrow> g z; h y od) 69 \<Longrightarrow> dcorres rvr P P' a (do y\<leftarrow> do z\<leftarrow>f; g z od; h y od)" 70 by (simp add: bind_assoc) 71 72lemma corres_bind_ignore_ret_rhs: 73 "corres_underlying sr nf nf' rvr P P' a (do f; g od) 74 \<Longrightarrow> corres_underlying sr nf nf' rvr P P' a (do y\<leftarrow> f;g od)" 75 by (simp add: bind_def) 76 77lemma corres_free_fail: 78 "dcorres c P P' f fail" 79 by (fastforce simp: corres_underlying_def bind_def fail_def) 80 81lemma corres_free_return: 82 "dcorres dc P P' (return a) (return b)" 83 by (clarsimp simp:return_def bind_def corres_underlying_def) 84 85lemma corres_free_set_object: 86 "\<lbrakk> \<forall> s s'. s = transform s' \<and> P s \<and> P' s' \<longrightarrow> 87 s = transform ((\<lambda>s. s \<lparr>kheap := kheap s (ptr \<mapsto> obj)\<rparr>) s')\<rbrakk> \<Longrightarrow> 88 dcorres dc P P' (return a) (set_object ptr obj )" 89 by (clarsimp simp: corres_underlying_def put_def return_def modify_def bind_def get_def 90 set_object_def get_object_def in_monad) 91 92 93(* Some dummy corres *) 94 95lemma corres_dummy_return_l: 96 "dcorres c P P' (do x\<leftarrow>f;return x od) g \<Longrightarrow> dcorres c P P' f g" 97 by (fastforce simp: corres_underlying_def bind_def return_def) 98 99lemma corres_dummy_return_pl: 100 "dcorres c P P' (do return b; f od) g \<Longrightarrow> dcorres c P P' f g" 101 by (fastforce simp: corres_underlying_def bind_def return_def) 102 103lemma corres_dummy_return_r: 104 "dcorres c P P' f (do x\<leftarrow>g;return x od) \<Longrightarrow> dcorres c P P' f g" 105 by (fastforce simp: corres_underlying_def bind_def return_def) 106 107lemma corres_dummy_return_pr: 108 "dcorres c P P' f (do return b; g od) \<Longrightarrow> dcorres c P P' f g" 109 by (fastforce simp: corres_underlying_def bind_def return_def) 110 111lemma corres_dummy_returnOk_r: 112 "dcorres c P P' f (g >>=E returnOk) \<Longrightarrow> dcorres c P P' f g" 113 by simp 114 115lemma corres_dummy_returnOk_pl: 116 "dcorres c P P' (returnOk b >>=E (\<lambda>_. f)) g \<Longrightarrow> dcorres c P P' f g" 117 by (fastforce simp: corres_underlying_def bindE_def returnOk_def) 118 119lemma corres_dummy_get_pr: 120 "dcorres c P P' f (do s\<leftarrow>get;g od)\<Longrightarrow> dcorres c P P' f g" 121 by (fastforce simp: corres_underlying_def bind_def get_def) 122 123lemma corres_dummy_get_pl: 124 "dcorres c P P' (do s\<leftarrow>get;g od) f \<Longrightarrow> dcorres c P P' g f" 125 by (fastforce simp: corres_underlying_def bind_def get_def) 126 127lemma dcorres_free_throw: 128 assumes "\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>" 129 shows "dcorres (dc \<oplus> r) P P' Monads_D.throw f" 130 using assms 131 apply (simp add:corres_underlying_def throwError_def return_def) 132 apply (clarsimp simp:validE_def valid_def) 133 apply (drule_tac x = b in meta_spec) 134 apply (fastforce split: sum.splits) 135 done 136 137lemma absorb_imp:"B \<and> A \<Longrightarrow> (a\<longrightarrow>A) \<and> B " 138 by simp 139 140 141(* This lemma is convienent if you want keep the prefix while split *) 142 143lemma corres_split_keep_pfx: 144 assumes x: "corres_underlying sr nf nf' r' P P' a c" 145 assumes y: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (P and (Q rv)) (P' and (Q' rv')) (b rv) (d rv')" 146 assumes "\<lbrace>P\<rbrace> a \<lbrace>\<lambda>x. P and (Q x)\<rbrace>" "\<lbrace>P'\<rbrace> c \<lbrace>\<lambda>x. P' and (Q' x)\<rbrace>" 147 shows "corres_underlying sr nf nf' r P P' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" 148 using assms by (rule corres_split') 149 150(* Following 2 lemmas allows you to get rid of the get function and move the prefix outside *) 151 152lemma dcorres_absorb_pfx: 153 assumes "dcorres r (P) (P') (f) (f')" 154 shows "\<And> s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f f' " 155 using assms 156by (fastforce simp:corres_underlying_def) 157 158lemma dcorres_expand_pfx: 159assumes "\<And> s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f f' " 160shows "dcorres r P P' f f'" 161using assms 162by (fastforce simp:corres_underlying_def) 163 164lemma dcorres_absorb_get_l: 165 assumes "!!s'. \<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g" 166 shows "dcorres rv P P' (do t\<leftarrow> get; f t od) g" 167 apply (rule corres_symb_exec_l [where Q="%x. P and ((=) x)"]) 168 apply (rule dcorres_expand_pfx) 169 apply clarsimp 170 apply (rule assms) 171 apply (clarsimp simp: valid_def exs_valid_def get_def)+ 172 done 173 174lemma dcorres_expand_get_l: 175 assumes "dcorres rv P P' (do t\<leftarrow>get; f t od) g" 176 shows "\<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow> 177 dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g" 178 using assms 179 by (simp add:get_def corres_underlying_def bind_def) 180 181lemma dcorres_absorb_get_r: 182 assumes "!!s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') f (g s')" 183 shows "dcorres rv P P' f (do t\<leftarrow> get; g t od)" 184 apply (rule corres_symb_exec_r [where Q'="%x. P' and ((=) x)"]) 185 apply (rule dcorres_expand_pfx) 186 apply clarsimp 187 apply (rule assms) 188 apply (clarsimp simp: valid_def exs_valid_def get_def)+ 189 done 190 191lemma dcorres_expand_get_r: 192 assumes "dcorres rv P P' f (do t\<leftarrow> get; g t od)" 193 shows "!!s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') f (g s')" 194 using assms 195 by (clarsimp simp:get_def corres_underlying_def bind_def) 196 197lemma dcorres_absorb_gets_the: 198 assumes A: "\<And>s' obj'. \<lbrakk>P' s'; g' s' = Some obj'; P (transform s')\<rbrakk> 199 \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') (f) (f' obj')" 200 shows "dcorres r P P' (f) (do a\<leftarrow> gets_the (g'); f' a od)" 201 apply (simp add: gets_the_def gets_def bind_assoc) 202 apply (rule dcorres_absorb_get_r) 203 apply (clarsimp simp :assert_opt_def split:option.splits) 204 apply (clarsimp simp:corres_free_fail) 205 apply (rule dcorres_expand_pfx) 206 apply (clarsimp simp:assms) 207done 208 209 210lemma dcorres_get: 211 assumes A: "\<And>s s'. \<lbrakk>s = transform s';P s; P' s'\<rbrakk> 212 \<Longrightarrow> dcorres r ((=) s) ((=) s') (f s) (f' s')" 213 shows "dcorres r P P' (do s\<leftarrow>get;f s od) (do s'\<leftarrow> get; f' s' od)" 214 apply (rule dcorres_expand_pfx) 215 apply (rule_tac r'="\<lambda>r r'. s=r \<and> s'=r'" and P="%x. (=) s" and P'="%x. (=) s'" in corres_underlying_split) 216 apply (clarsimp simp: corres_underlying_def get_def) 217 apply wp+ 218 apply (drule A) 219 apply clarsimp+ 220done 221 222lemma dcorres_gets_the: 223 assumes A: "\<And>s s' obj obj'. \<lbrakk>s = transform s';P s; P' s'; g' s' = Some obj' ;g s = Some obj\<rbrakk> 224 \<Longrightarrow> dcorres r ((=) s) ((=) s') (f obj) (f' obj')" 225 assumes B: "\<And>s s'. \<lbrakk>s = transform s'; P s; P' s' ; g' s' \<noteq> None\<rbrakk> \<Longrightarrow> g s \<noteq> None" 226 shows "dcorres r P P' (do a\<leftarrow>gets_the (g);f a od) (do a\<leftarrow> gets_the (g'); f' a od)" 227 apply (simp add:gets_the_def) 228 apply (simp add: gets_def) 229 apply (subst bind_assoc)+ 230 apply (rule corres_split_keep_pfx 231 [where r'="\<lambda>s s'. s = transform s'\<and> P s \<and> P' s'" and Q="\<lambda>x s. x = s" and Q'="\<lambda>x s. x = s "]) 232 apply (clarsimp simp: corres_underlying_def get_def) 233 apply (simp add: assert_opt_def) 234 apply (case_tac "g' xa = None") 235 apply (clarsimp split:option.splits simp:corres_free_fail) 236 apply (subgoal_tac "\<exists>obj. g x \<noteq> None") 237 apply (clarsimp split:option.splits) 238 apply (rule_tac Q="(=)(transform xa)" and Q'="(=) xa" in corres_guard_imp) 239 apply (simp add: A)+ 240 using B 241 apply (wp|clarsimp)+ 242done 243 244lemma wpc_helper_dcorres: 245 "dcorres r Q Q' f f' 246 \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (dcorres r P (\<lambda>s. s \<in> P') f f')" 247 apply (clarsimp simp: wpc_helper_def) 248 apply (erule corres_guard_imp) 249 apply simp 250 apply auto 251 done 252 253wpc_setup "\<lambda>m. dcorres r P P' a m" wpc_helper_dcorres 254wpc_setup "\<lambda>m. dcorres r P P' a (m >>= c)" wpc_helper_dcorres 255 256(* Shorthand to say that a TCB is at the given location in the given state. *) 257definition "cdl_tcb_at x \<equiv> \<lambda>s. \<exists>tcb . cdl_objects s x = Some (Tcb tcb)" 258 259(* 260 * We can strengthen the LHS precondition by using the RHS 261 * precondition if the state relation preserves it. 262 *) 263lemma dcorres_strengthen_lhs_guard: 264 "\<lbrakk> dcorres rr P P' g g'; \<And>s. P' s \<Longrightarrow> P (transform s) \<rbrakk> \<Longrightarrow> dcorres rr \<top> P' g g'" 265 by (rule stronger_corres_guard_imp [where Q=P and Q'=P']) auto 266 267(* A call to "mapM" is idempotent if its input monad is idempotent. *) 268lemma hoare_mapM_idempotent: "\<lbrakk> \<And> a R. \<lbrace> R \<rbrace> x a \<lbrace> \<lambda>_. R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> R \<rbrace> mapM x y \<lbrace> \<lambda>_. R \<rbrace>" 269 apply (induct_tac y) 270 apply (clarsimp simp: mapM_def sequence_def) 271 apply (clarsimp simp: mapM_def sequence_def) 272 apply atomize 273 apply (erule_tac x=a in allE) 274 apply (erule_tac x=R in allE) 275 apply (rule hoare_seq_ext) 276 apply wp 277 apply assumption 278 done 279 280(* A call to "mapM" corresponds to "return foo" if the mapM is idempotent. *) 281lemma dcorres_idempotent_mapM_rhs: 282 "\<lbrakk> \<And> a R. \<lbrace> R \<rbrace> x a \<lbrace> \<lambda>_. R \<rbrace> \<rbrakk> \<Longrightarrow> 283 dcorres dc P P' (return q) (mapM x y)" 284 apply (induct_tac y) 285 apply (clarsimp simp: mapM_def sequence_def) 286 apply (clarsimp simp: mapM_def sequence_def) 287 apply atomize 288 apply (erule_tac x=a in allE) 289 apply (rule corres_symb_exec_r [where Q'="\<lambda>_. P'"]) 290 apply (clarsimp simp: corres_underlying_def bind_def return_def split_def) 291 apply (erule_tac x=P' in allE, assumption) 292 apply (erule_tac x="(=) s" in allE, assumption) 293 apply simp 294 done 295 296(* rules used to get rid of the error branchs of decode proof *) 297lemma dcorres_throw: 298 "dcorres (dc \<oplus> anyrel) \<top> \<top> (Monads_D.throw) (throwError anyerror)" 299 by (clarsimp simp:corres_underlying_def throwError_def return_def) 300 301lemma dcorres_alternative_throw: 302 "dcorres (dc \<oplus> anyrel) \<top> \<top> (any \<sqinter> Monads_D.throw) (throwError anyerror)" 303 by (rule corres_alternate2[OF dcorres_throw]) 304 305lemma dcorres_returnOk: 306 "r a b \<Longrightarrow> 307 dcorres (dc \<oplus> r) \<top> \<top> (returnOk a) (returnOk b)" 308 by (clarsimp simp:corres_underlying_def return_def returnOk_def) 309 310lemma split_return_throw_thingy: 311 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> rvP rv\<rbrace>,\<lbrace>\<lambda>ft. (=) s\<rbrace>; 312 \<And>rv. rvP rv \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' (f \<sqinter> throwError e) (h rv); 313 nf' \<Longrightarrow> no_fail P' g \<rbrakk> 314 \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' 315 (f \<sqinter> throwError e) (g >>=E h)" 316 apply (simp add: bindE_def) 317 apply (rule corres_guard_imp) 318 apply (rule_tac Q'="\<lambda>rv. P' and (\<lambda>_. isRight rv \<longrightarrow> rvP (theRight rv))" 319 in corres_symb_exec_r[where P=P and P'=P'], simp_all) 320 apply (case_tac rv) 321 apply (simp add: lift_def) 322 apply (rule corres_alternate2, simp) 323 apply (rule corres_gen_asm2) 324 apply (simp add: lift_def isRight_def) 325 apply (clarsimp simp add: validE_def valid_def) 326 apply (erule meta_allE, drule(1) bspec) 327 apply (auto simp: isRight_def split: sum.split_asm)[1] 328 apply (simp add: validE_def) 329 apply (rule hoare_strengthen_post, assumption) 330 apply (simp split: sum.split_asm) 331 done 332 333lemma case_sum_triv_return: 334 "case_sum throwError returnOk = return" 335 apply (intro ext) 336 apply (simp add: throwError_def returnOk_def return_def 337 split: sum.split) 338 done 339 340lemma lift_returnOk_bind_triv: 341 "g >>= (lift returnOk) = g" 342 by (simp add: lift_def case_sum_triv_return cong: bind_cong) 343 344lemma corres_return_throw_thingy: 345 "\<lbrakk> \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>rv s'. s' = s \<and> Q rv\<rbrace>,\<lbrace>\<lambda>ft. (=) s\<rbrace>; 346 nf' \<Longrightarrow> no_fail P' g; \<forall>rv. Q rv \<longrightarrow> r v rv \<rbrakk> 347 \<Longrightarrow> corres_underlying sr nf nf' (dc \<oplus> r) P P' 348 (returnOk v \<sqinter> throwError e) (g)" 349 apply (subst lift_returnOk_bind_triv[where g=g, symmetric]) 350 apply (fold bindE_def, rule split_return_throw_thingy) 351 apply assumption 352 apply (rule corres_alternate1) 353 apply (clarsimp simp: returnOk_def) 354 apply simp 355 done 356 357lemma dcorres_throw_wp: 358assumes "\<forall>s. \<lbrace>(=) s\<rbrace>g\<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>" 359shows "dcorres (dc\<oplus>anyrel) \<top> P (Monads_D.throw) g" 360 using assms 361 apply (clarsimp simp:throwError_def corres_underlying_def return_def validE_def valid_def) 362 apply (drule spec) 363 apply (drule (1) bspec) 364 apply (clarsimp split:sum.split_asm) 365 done 366 367 368(* 369 * We can consider correspondence of a function starting with 370 * a conditional "throw" in two parts: when the error occurs 371 * and when the error does not occur. 372 *) 373lemma dcorres_whenE_throwError_abstract: 374 "\<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e); 375 \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'\<rbrakk> \<Longrightarrow> 376 dcorres rvrel (M and N) (M' and N') m (whenE cond (throwError e) >>=E (\<lambda>_. m'))" 377 apply (unfold whenE_def) 378 apply (case_tac cond) 379 apply (clarsimp) 380 apply (erule corres_guard_imp, simp+) 381 apply (erule corres_guard_imp, simp+) 382 done 383 384lemma dcorres_whenE_throwError_abstract': 385 "\<lbrakk>cond \<Longrightarrow> dcorres rvrel G G' m (throwError e); 386 \<not> cond \<Longrightarrow> dcorres rvrel G G' m m'\<rbrakk> \<Longrightarrow> 387 dcorres rvrel G G' m (whenE cond (throwError e) >>=E (\<lambda>_. m'))" 388 apply (rule corres_guard_imp) 389 apply (rule dcorres_whenE_throwError_abstract, assumption, assumption) 390 apply simp 391 apply simp 392 done 393 394lemma dcorres_symb_exec_r_catch: 395 "\<lbrakk> 396 \<And>rv. dcorres r P (Q1 rv) f (h rv); 397 \<And>rv'. dcorres r P (Q2 rv') f (i rv'<catch> h); 398 \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace> 399 \<rbrakk> 400 \<Longrightarrow> dcorres r P P' f (g >>=E i <catch> h)" 401 apply (subst catch_def) 402 apply (clarsimp simp:lift_def bindE_def bind_assoc) 403 apply (rule corres_symb_exec_r) 404 prefer 2 405 apply (clarsimp simp:lift_def validE_def bind_def) 406 apply (simp) 407 apply (case_tac x) 408 apply (simp add:throwError_def)+ 409 apply (simp add:catch_def)+ 410done 411 412lemma dcorres_symb_exec_r: 413 "\<lbrakk>\<And>rv. dcorres r P (Q' rv) h (g rv); \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>r. Q' r\<rbrace>; 414 \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> 415 \<Longrightarrow> dcorres r P P' h (f>>=g)" 416 apply (rule corres_dummy_return_pl) 417 apply (rule corres_guard_imp) 418 apply (rule corres_split[where R="\<lambda>rv. P" and R'="\<lambda>rv. Q' rv" and r' = dc]) 419 apply simp 420 defer 421 apply wp 422 apply simp+ 423 apply (clarsimp simp:valid_def corres_underlying_def return_def) 424 done 425 426lemma dcorres_symb_exec_r_strong: 427 "\<lbrakk>\<And>rv. dcorres r P (Q' rv) h (g rv); \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>r. Q' r\<rbrace>; 428 \<And>cs. \<lbrace>\<lambda>ps. P' ps \<and> transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> 429 \<Longrightarrow> dcorres r P P' h (f>>=g)" 430 apply (rule corres_dummy_return_pl) 431 apply (rule corres_guard_imp) 432 apply (rule corres_split[where R="\<lambda>rv. P" and P'=P' and R'="\<lambda>rv. Q' rv" and r' = dc]) 433 apply (unfold K_bind_def) 434 apply (assumption) 435 defer 436 apply wp 437 apply simp+ 438 apply (clarsimp simp:valid_def corres_underlying_def return_def) 439 done 440 441lemma dcorres_symb_exec_r_catch': 442 "\<lbrakk> 443 \<And>rv. dcorres r P (Q1 rv) f (h rv); 444 \<And>rv'. dcorres r P (Q2 rv') f (i rv'<catch> h); 445 \<lbrace>P'\<rbrace> g \<lbrace>Q2\<rbrace>, \<lbrace>Q1\<rbrace>; \<And>cs. \<lbrace>\<lambda>s. transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace> 446 \<rbrakk> 447 \<Longrightarrow> dcorres r P P' f (g >>=E i <catch> h)" 448 apply (subst catch_def) 449 apply (clarsimp simp:lift_def bindE_def bind_assoc) 450 apply (subst dcorres_symb_exec_r) 451 prefer 2 452 apply (clarsimp simp:lift_def validE_def bind_def) 453 apply (simp) 454 apply (case_tac rv) 455 apply (simp add:throwError_def)+ 456 apply (simp add:catch_def) 457 apply simp+ 458done 459 460lemma dcorres_to_wp: 461 "dcorres dc \<top> Q (return x) g \<Longrightarrow> \<lbrace>\<lambda>s. Q s \<and> transform s = cs\<rbrace>g\<lbrace>\<lambda>r s. transform s = cs\<rbrace>" 462 by (fastforce simp:corres_underlying_def valid_def return_def) 463 464lemma wp_to_dcorres: 465 "(\<And>cs. \<lbrace>\<lambda>s. Q s \<and> transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) Q (return x) g" 466 by (clarsimp simp:corres_underlying_def valid_def return_def) 467 468lemma dcorres_symb_exec_rE: 469 "\<lbrakk>\<And>rv. dcorres r P (Q' rv) h (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> 470 \<Longrightarrow> dcorres r P P' h (liftE f >>=E g)" 471 apply (simp add: liftE_def lift_def bindE_def) 472 apply (erule (1) dcorres_symb_exec_r) 473 apply assumption 474 done 475 476lemma throw_handle: 477 "(Monads_D.throw <handle2> (\<lambda>_. m)) = m" 478 by (simp add: handleE'_def throwError_def) 479 480lemma corres_handle2: 481 "corres_underlying R False nf' (dc \<oplus> r) P P' m m' \<Longrightarrow> 482 corres_underlying R False nf' (dc \<oplus> r) P P' (m <handle2> (\<lambda>x. Monads_D.throw)) m'" 483 apply (clarsimp simp: corres_underlying_def) 484 apply (rule conjI) 485 prefer 2 486 apply fastforce 487 apply clarsimp 488 apply (drule (1) bspec, clarsimp) 489 apply (drule (1) bspec, clarsimp) 490 apply (clarsimp simp: handleE'_def) 491 apply (simp add: bind_def) 492 apply (rule bexI) 493 prefer 2 494 apply assumption 495 apply (simp add: return_def throwError_def split: sum.splits) 496 apply fastforce 497 done 498 499lemma corres_handle2': 500 "corres_underlying R False nf' (dc \<oplus> r) P P' m m' \<Longrightarrow> 501 corres_underlying R False nf' (dc \<oplus> r) P P' m (m' <handle2> (throwError \<circ> e))" 502 apply (clarsimp simp: corres_underlying_def) 503 apply (rule conjI) 504 prefer 2 505 apply (clarsimp simp: handleE'_def bind_def) 506 apply (drule (1) bspec, clarsimp) 507 apply (drule (1) bspec, clarsimp) 508 apply (clarsimp simp: return_def throwError_def split: sum.splits) 509 apply clarsimp 510 apply (drule (1) bspec, clarsimp) 511 apply (clarsimp simp: handleE'_def bind_def) 512 apply (drule (1) bspec, clarsimp) 513 apply (fastforce simp: return_def throwError_def split: sum.splits) 514 done 515 516lemma corres_alternative_throw_splitE: 517 assumes a: "corres_underlying R False z (dc \<oplus> r') P P' (f \<sqinter> Monads_D.throw) f'" 518 assumes b: "\<And>x x'. r' x x' \<Longrightarrow> corres_underlying R False z (dc \<oplus> r) (Q x) (Q' x') (g x \<sqinter> Monads_D.throw) (g' x')" 519 assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>" 520 assumes f': "\<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>_. \<top>\<rbrace>" 521 assumes f'_eq: "\<And>s. \<lbrace>(=) s\<rbrace> f' \<lbrace>\<lambda>_. (=) s\<rbrace>" 522 assumes g'_eq: "\<And>s x. \<lbrace>\<lambda>s'. s' = s \<and> Q' x s'\<rbrace> g' x \<lbrace>\<lambda>_. \<top>\<rbrace>, \<lbrace>\<lambda>_. (=) s\<rbrace>" 523 shows "corres_underlying R False z (dc \<oplus> r) P P' ((f >>=E g) \<sqinter> Monads_D.throw) (f' >>=E g')" 524 apply (clarsimp simp: bindE_def corres_underlying_def) 525 apply (rule conjI) 526 prefer 2 527 apply (frule (2) corres_underlyingD [OF a]) 528 apply simp 529 apply (clarsimp simp: bind_def split_def lift_def) 530 apply (clarsimp simp: throwError_def return_def split: sum.splits) 531 apply (drule (1) bspec, clarsimp simp: alternative_def) 532 apply (drule b) 533 apply (thin_tac "(a,b) \<in> R") 534 apply (drule (1) corres_underlyingD) 535 apply (drule use_valid, rule f[unfolded validE_def]) 536 apply assumption 537 apply simp 538 apply (drule use_valid, rule f'[unfolded validE_def]) 539 apply assumption 540 apply simp 541 apply simp 542 apply simp 543 apply (clarsimp simp: in_bind) 544 apply (frule (3) corres_underlyingD2 [OF a]) 545 apply simp 546 apply (clarsimp simp: in_alternative in_throwError) 547 apply (erule disjE) 548 prefer 2 549 apply (clarsimp simp: lift_def in_throwError) 550 apply (clarsimp simp: alternative_def throwError_def return_def) 551 apply (simp add: lift_def split: sum.splits) 552 apply (clarsimp simp: in_throwError) 553 apply (rule_tac x="(Inl x',bb)" in bexI) 554 apply simp 555 apply (clarsimp simp: alternative_def bind_def) 556 apply (rule bexI) 557 prefer 2 558 apply assumption 559 apply (simp add: lift_def throwError_def return_def) 560 apply clarsimp 561 apply (drule b) 562 apply (drule_tac s'=s'' in corres_underlyingD2, assumption) 563 apply (drule use_valid, rule f[unfolded validE_def]) 564 apply assumption 565 apply simp 566 apply (drule use_valid, rule f'[unfolded validE_def]) 567 apply assumption 568 apply simp 569 apply assumption 570 apply simp 571 apply (clarsimp simp: in_alternative in_throwError) 572 apply (erule disjE) 573 apply (rule bexI, fastforce) 574 apply (clarsimp simp: alternative_def) 575 apply (simp add: bind_def) 576 apply (rule bexI) 577 prefer 2 578 apply assumption 579 apply (clarsimp simp: lift_def) 580 apply clarsimp 581 apply (frule use_valid, rule f'_eq, rule refl) 582 apply clarsimp 583 apply (drule use_valid, rule g'_eq[unfolded validE_def]) 584 apply (rule conjI, rule refl) 585 apply (drule use_valid, rule f'[unfolded validE_def], assumption) 586 apply simp 587 apply (simp add: alternative_def throwError_def return_def) 588 done 589 590lemma corres_throw_skip_r: 591 assumes c: "corres_underlying R False z (dc \<oplus> r) P P' (f \<sqinter> Monads_D.throw) g'" 592 assumes eq: "\<And>s. \<lbrace>(=) s\<rbrace> f' \<lbrace>\<lambda>_. (=) s\<rbrace>" 593 assumes nf: "z \<longrightarrow> no_fail P' f'" 594 shows "corres_underlying R nf z (dc \<oplus> r) P P' (f \<sqinter> Monads_D.throw) (f' >>=E (\<lambda>_. g'))" 595 using c 596 apply (clarsimp simp: corres_underlying_def alternative_def bindE_def) 597 apply (drule (1) bspec) 598 apply (rule conjI) 599 apply (clarsimp simp: in_bind) 600 apply (frule use_valid, rule eq, rule refl) 601 apply clarsimp 602 apply (clarsimp simp: lift_def in_throwError split: sum.splits) 603 apply (simp add: throwError_def return_def) 604 apply (drule (1) bspec, clarsimp) 605 apply clarsimp 606 apply (clarsimp simp: bind_def) 607 apply (erule disjE) 608 prefer 2 609 apply (insert nf)[1] 610 apply (clarsimp simp: no_fail_def) 611 apply (clarsimp simp: lift_def throwError_def return_def split: sum.splits) 612 apply (frule use_valid, rule eq, rule refl) 613 apply clarsimp 614 done 615 616lemma dcorres_rhs_noop_below: 617 "\<lbrakk> dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; 618 \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. Q \<rbrace>; \<lbrace> P' \<rbrace> g \<lbrace> \<lambda>_. Q' \<rbrace> \<rbrakk> 619 \<Longrightarrow> dcorres anyrel P P' (f :: unit k_monad) (g >>= (\<lambda>_. m))" 620 apply (rule corres_add_noop_lhs2) 621 apply (rule corres_underlying_split) 622 apply (assumption | clarsimp)+ 623 done 624 625lemma dcorres_rhs_noop_above: "\<lbrakk> dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; 626 \<lbrace> P \<rbrace> return () \<lbrace> \<lambda>_. Q \<rbrace>; \<lbrace> P' \<rbrace> m \<lbrace> \<lambda>_. Q' \<rbrace> \<rbrakk> 627 \<Longrightarrow> dcorres anyrel' P P' f (m >>= (\<lambda>_. g))" 628 apply (rule corres_add_noop_lhs) 629 apply (rule corres_underlying_split) 630 apply (assumption | clarsimp)+ 631 done 632 633lemmas dcorres_rhs_noop_below_True = dcorres_rhs_noop_below[OF _ _ hoare_TrueI hoare_TrueI] 634lemmas dcorres_rhs_noop_above_True = dcorres_rhs_noop_above[OF _ _ hoare_TrueI hoare_TrueI] 635 636declare hoare_TrueI[simp] 637 638lemma dcorres_dc_rhs_noop_below_gen: 639 "\<lbrakk> \<forall>rv'. dcorres dc (Q ()) (Q' rv') (return ()) (m rv'); 640 dcorres dc P P' f g; 641 \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; \<lbrace> P' \<rbrace> g \<lbrace> Q' \<rbrace> \<rbrakk> 642 \<Longrightarrow> dcorres dc P P' f (g >>= m)" 643 apply (rule corres_add_noop_lhs2) 644 apply (rule corres_underlying_split) 645 apply (assumption | clarsimp)+ 646 done 647 648lemma dcorres_dc_rhs_noop_below_2: "\<lbrakk> \<forall>rv'. dcorres dc (Q ()) (Q' rv') (return ()) m; 649 dcorres dc P P' f (g >>= h); 650 \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; 651 \<lbrace> P' \<rbrace> g \<lbrace> R'\<rbrace>; 652 (\<And>y. \<lbrace> R' y \<rbrace> h y \<lbrace> Q' \<rbrace>) 653 \<rbrakk> 654 \<Longrightarrow> dcorres dc P P' f (do x \<leftarrow> g; 655 _ \<leftarrow> h x; 656 m 657 od)" 658 apply (simp add: bind_assoc[symmetric]) 659 apply (rule dcorres_dc_rhs_noop_below_gen) 660 apply (wp | simp | assumption)+ 661 done 662 663lemmas dcorres_dc_rhs_noop_below_2_True = dcorres_dc_rhs_noop_below_2[OF _ _ hoare_TrueI hoare_TrueI hoare_TrueI] 664 665lemma dcorres_assert_opt_assume: 666 assumes "\<And>x. m = Some x \<Longrightarrow> dcorres R P P' a (c x)" 667 shows "dcorres R P P' a (assert_opt m >>= c)" 668 using assms 669 by (auto simp: bind_def assert_opt_def assert_def fail_def return_def 670 corres_underlying_def split: option.splits) 671 672end 673