1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Corres_Method 8imports Corres_UL SpecValid_R 9begin 10 11(*TODO move this *) 12 13method_setup repeat_new = 14 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => 15 let 16 fun tac i st' = 17 Goal.restrict i 1 st' 18 |> method_evaluate m ctxt facts 19 |> Seq.map (Goal.unrestrict i) 20 21 in SIMPLE_METHOD (SUBGOAL (fn (_,i) => REPEAT_ALL_NEW tac i) 1) facts end) 22\<close> 23 24chapter \<open>Corres Methods\<close> 25 26section \<open>Boilerplate\<close> 27 28context begin 29 30private definition "my_true \<equiv> True" 31 32private lemma my_true: "my_true" by (simp add: my_true_def) 33 34method no_schematic_concl = (fails \<open>rule my_true\<close>) 35 36end 37 38definition 39 "corres_underlyingK sr nf nf' F r Q Q' f g \<equiv> 40 F \<longrightarrow> corres_underlying sr nf nf' r Q Q' f g" 41 42lemma corresK_name_pre: 43 "\<lbrakk> \<And>s s'. \<lbrakk> P s; P' s'; F; (s, s') \<in> sr \<rbrakk> 44 \<Longrightarrow> corres_underlyingK sr nf nf' F r ((=) s) ((=) s') f g \<rbrakk> 45 \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f g" 46 apply (clarsimp simp add: corres_underlyingK_def) 47 apply (rule corres_name_pre) 48 apply blast 49 done 50 51lemma corresK_assume_pre: 52 "\<lbrakk> \<And>s s'. \<lbrakk> P s; P' s'; F; (s, s') \<in> sr \<rbrakk> 53 \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f g \<rbrakk> 54 \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f g" 55 apply (clarsimp simp add: corres_underlyingK_def) 56 apply (rule corres_assume_pre) 57 apply blast 58 done 59 60lemma corresK_drop_any_guard: 61 "corres_underlying sr nf nf' r Q Q' f g \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g" 62 by (simp add: corres_underlyingK_def) 63 64lemma corresK_assume_guard: 65 "(F \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g) \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g" 66 by (simp add: corres_underlyingK_def) 67 68lemma corresK_unlift: 69 "corres_underlyingK sr nf nf' F r Q Q' f g \<Longrightarrow> (F \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g)" 70 by (simp add: corres_underlyingK_def) 71 72lemma corresK_lift: 73 "corres_underlying sr nf nf' r Q Q' f g \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g" 74 by (simp add: corres_underlyingK_def) 75 76lemma corresK_lift_rule: 77 "corres_underlying sr nf nf' r Q Q' f g \<longrightarrow> corres_underlying sra nfa nfa' ra Qa Qa' fa ga 78 \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g \<longrightarrow> corres_underlyingK sra nfa nfa' F ra Qa Qa' fa ga" 79 by (simp add: corres_underlyingK_def) 80 81lemmas corresK_drop = corresK_drop_any_guard[where F=True] 82 83context begin 84 85lemma corresK_start: 86 assumes x: "corres_underlyingK sr nf nf' F r Q Q' f g" 87 assumes y: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> F \<and> Q s \<and> Q' s'" 88 shows "corres_underlying sr nf nf' r P P' f g" 89 using x by (auto simp: y corres_underlying_def corres_underlyingK_def) 90 91lemma corresK_weaken: 92 assumes x: "corres_underlyingK sr nf nf' F' r Q Q' f g" 93 assumes y: "\<And>s s'. \<lbrakk> P s; P' s'; F; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> F' \<and> Q s \<and> Q' s'" 94 shows "corres_underlyingK sr nf nf' F r P P' f g" 95 using x by (auto simp: y corres_underlying_def corres_underlyingK_def) 96 97private lemma corres_trivial: 98 "False \<Longrightarrow> corres_underlying sr nf nf' r P P' f f'" 99 by simp 100 101method check_corres = 102 (succeeds \<open>rule corres_trivial\<close>, fails \<open>rule TrueI\<close>) 103 104private lemma corresK_trivial: 105 "False \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f f'" 106 by simp 107 108(* Ensure we don't apply calculational rules if either function is schematic *) 109 110private definition "dummy_fun \<equiv> undefined" 111 112private lemma corresK_dummy_left: 113 "False \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' dummy_fun f'" 114 by simp 115 116private lemma corresK_dummy_right: 117 "False \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f dummy_fun" 118 by simp 119 120method check_corresK = 121 (succeeds \<open>rule corresK_trivial\<close>, fails \<open>rule corresK_dummy_left corresK_dummy_right\<close>) 122 123private definition "my_false s \<equiv> False" 124 125private 126 lemma corres_my_falseE: "my_false x \<Longrightarrow> P" by (simp add: my_false_def) 127 128method no_schematic_prems = (fails \<open>erule corres_my_falseE\<close>) 129 130private lemma hoare_pre: "\<lbrace>my_false\<rbrace> f \<lbrace>Q\<rbrace>" by (simp add: valid_def my_false_def) 131private lemma hoareE_pre: "\<lbrace>my_false\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>Q'\<rbrace>" by (simp add: validE_def valid_def my_false_def) 132private lemma hoare_E_E_pre: "\<lbrace>my_false\<rbrace> f -,\<lbrace>Q\<rbrace>" by (simp add: validE_E_def validE_def valid_def my_false_def) 133private lemma hoare_E_R_pre: "\<lbrace>my_false\<rbrace> f \<lbrace>Q\<rbrace>,-" by (simp add: validE_R_def validE_def valid_def my_false_def) 134 135private lemmas hoare_pres = hoare_pre hoare_pre hoare_E_E_pre hoare_E_R_pre 136 137method schematic_hoare_pre = (succeeds \<open>rule hoare_pres\<close>) 138 139private 140 lemma corres_my_false: "corres_underlying sr nf nf' r my_false P f f'" 141 "corres_underlying sr nf nf' r P' my_false f f'" 142 by (auto simp add: my_false_def[abs_def] corres_underlying_def) 143 144private 145 lemma corresK_my_false: "corres_underlyingK sr nf nf' F r my_false P f f'" 146 "corres_underlyingK sr nf nf' F r P' my_false f f'" 147 by (auto simp add: corres_my_false corres_underlyingK_def) 148 149 150method corres_raw_pre = 151 (check_corres, (fails \<open>rule corres_my_false\<close>, rule corresK_start)?) 152 153lemma corresK_weaken_states: 154 "corres_underlyingK sr nf nf' F r Q Q' f g \<Longrightarrow> 155 corres_underlyingK sr nf nf' (F \<and> (\<forall>s s'. P s \<longrightarrow> P' s' \<longrightarrow> (s, s') \<in> sr \<longrightarrow> Q s \<and> Q' s')) 156 r P P' f g" 157 apply (erule corresK_weaken) 158 apply simp 159 done 160 161private lemma 162 corresK_my_falseF: 163 "corres_underlyingK sr nf nf' (my_false undefined) r P P' f f'" 164 by (simp add: corres_underlyingK_def my_false_def) 165 166method corresK_pre = 167 (check_corresK, 168 (fails \<open>rule corresK_my_false\<close>, 169 ((succeeds \<open>rule corresK_my_falseF\<close>, rule corresK_weaken_states) | 170 rule corresK_weaken))) 171 172method corres_pre = (corres_raw_pre | corresK_pre)? 173 174lemma corresK_weakenK: 175 "corres_underlyingK sr nf nf' F' r P P' f f' \<Longrightarrow> (F \<Longrightarrow> F') \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' f f'" 176 by (simp add: corres_underlyingK_def) 177 178(* Special corres rules which should only be applied when the return value relation is 179 concrete, to avoid bare schematics. *) 180 181named_theorems corres_concrete_r and corres_concrete_rER 182 183private lemma corres_r_False: 184 "False \<Longrightarrow> corres_underlyingK sr nf nf' F (\<lambda>_. my_false) P P' f f'" 185 by simp 186 187private lemma corres_r_FalseE: 188 "False \<Longrightarrow> corres_underlyingK sr nf nf' F ((\<lambda>_. my_false) \<oplus> r) P P' f f'" 189 by simp 190 191private lemma corres_r_FalseE': 192 "False \<Longrightarrow> corres_underlyingK sr nf nf' F (r \<oplus> (\<lambda>_. my_false)) P P' f f'" 193 by simp 194 195method corres_concrete_r declares corres_concrete_r corres_concrete_rER = 196 (fails \<open>rule corres_r_False corres_r_FalseE corres_r_FalseE'\<close>, determ \<open>rule corres_concrete_r\<close>) 197 | (fails \<open>rule corres_r_FalseE\<close>, determ \<open>rule corres_concrete_rER\<close>) 198 199 200end 201 202 203section \<open>Corresc - Corres over case statements\<close> 204 205text 206 \<open>Based on wpc, corresc examines the split rule for top-level case statements on the left 207 and right hand sides, propagating backwards the stateless and left/right preconditions.\<close> 208 209ML \<open> 210 211fun get_split_rule ctxt target = 212let 213 val (hdTarget,args) = strip_comb (Envir.eta_contract target) 214 val (constNm, _) = dest_Const hdTarget 215 val constNm_fds = (String.fields (fn c => c = #".") constNm) 216 217 val _ = if String.isPrefix "case_" (List.last constNm_fds) then () 218 else raise TERM ("Not a case statement",[target]) 219 220 val typeNm = (String.concatWith "." o rev o tl o rev) constNm_fds; 221 val split = Proof_Context.get_thm ctxt (typeNm ^ ".split"); 222 val vars = Term.add_vars (Thm.prop_of split) [] 223 224 val datatype_name = List.nth (rev constNm_fds,1) 225 226 fun T_is_datatype (Type (nm,_)) = (Long_Name.base_name nm) = (Long_Name.base_name datatype_name) 227 | T_is_datatype _ = false 228 229 val datatype_var = 230 case (find_first (fn ((_,_),T') => (T_is_datatype T')) vars) of 231 SOME (ix,_) => ix 232 | NONE => error ("Couldn't find datatype in thm: " ^ datatype_name) 233 234 val split' = Drule.infer_instantiate ctxt 235 [(datatype_var, Thm.cterm_of ctxt (List.last args))] split 236 237in 238 SOME split' end 239 handle TERM _ => NONE; 240\<close> 241 242attribute_setup get_split_rule = \<open>Args.term >> 243 (fn t => Thm.rule_attribute [] (fn context => fn _ => 244 case (get_split_rule (Context.proof_of context) t) of 245 SOME thm => thm 246 | NONE => Drule.free_dummy_thm))\<close> 247 248method apply_split for f :: 'a and R :: "'a \<Rightarrow> bool"= 249 (match [[get_split_rule f]] in U: "(?x :: bool) = ?y" \<Rightarrow> 250 \<open>match U[THEN iffD2] in U': "\<And>H. ?A \<Longrightarrow> H (?z :: 'c)" \<Rightarrow> 251 \<open>match (R) in "R' :: 'c \<Rightarrow> bool" for R' \<Rightarrow> 252 \<open>rule U'[where H=R']\<close>\<close>\<close>) 253 254definition 255 wpc2_helper :: "(('a \<Rightarrow> bool) \<times> 'b set) 256 \<Rightarrow> (('a \<Rightarrow> bool) \<times> 'b set) \<Rightarrow> (('a \<Rightarrow> bool) \<times> 'b set) 257 \<Rightarrow> (('a \<Rightarrow> bool) \<times> 'b set) \<Rightarrow> bool \<Rightarrow> bool" where 258 "wpc2_helper \<equiv> \<lambda>(P, P') (Q, Q') (PP, PP') (QQ,QQ') R. 259 ((\<forall>s. P s \<longrightarrow> Q s) \<and> P' \<subseteq> Q') \<longrightarrow> ((\<forall>s. PP s \<longrightarrow> QQ s) \<and> PP' \<subseteq> QQ') \<longrightarrow> R" 260 261definition 262 "wpc2_protect B Q \<equiv> (Q :: bool)" 263 264lemma wpc2_helperI: 265 "wpc2_helper (P, P') (P, P') (PP, PP') (PP, PP') Q \<Longrightarrow> Q" 266 by (simp add: wpc2_helper_def) 267 268lemma wpc2_conj_process: 269 "\<lbrakk> wpc2_helper (P, P') (A, A') (PP, PP') (AA, AA') C; wpc2_helper (P, P') (B, B') (PP, PP') (BB, BB') D \<rbrakk> 270 \<Longrightarrow> wpc2_helper (P, P') (\<lambda>s. A s \<and> B s, A' \<inter> B') (PP, PP') (\<lambda>s. AA s \<and> BB s, AA' \<inter> BB') (C \<and> D)" 271 by (clarsimp simp add: wpc2_helper_def) 272 273lemma wpc2_all_process: 274 "\<lbrakk> \<And>x. wpc2_helper (P, P') (Q x, Q' x) (PP, PP') (QQ x, QQ' x) (R x) \<rbrakk> 275 \<Longrightarrow> wpc2_helper (P, P') (\<lambda>s. \<forall>x. Q x s, {s. \<forall>x. s \<in> Q' x}) (PP, PP') (\<lambda>s. \<forall>x. QQ x s, {s. \<forall>x. s \<in> QQ' x}) (\<forall>x. R x)" 276 by (clarsimp simp: wpc2_helper_def subset_iff) 277 278lemma wpc2_imp_process: 279 "\<lbrakk> wpc2_protect B Q \<Longrightarrow> wpc2_helper (P, P') (R, R') (PP, PP') (RR, RR') S \<rbrakk> 280 \<Longrightarrow> wpc2_helper (P, P') (\<lambda>s. Q \<longrightarrow> R s, {s. Q \<longrightarrow> s \<in> R'}) (PP, PP') (\<lambda>s. Q \<longrightarrow> RR s, {s. Q \<longrightarrow> s \<in> RR'}) (Q \<longrightarrow> S)" 281 by (clarsimp simp add: wpc2_helper_def subset_iff wpc2_protect_def) 282 283 284 285text \<open> 286 Generate quadratic blowup of the case statements on either side of refinement. 287 Attempt to discharge resulting contradictions. 288\<close> 289 290 291method corresc_body for B :: bool uses helper = 292 determ \<open>(rule wpc2_helperI, 293 repeat_new \<open>rule wpc2_conj_process wpc2_all_process wpc2_imp_process[where B=B]\<close> ; (rule helper))\<close> 294 295lemma wpc2_helper_corres_left: 296 "corres_underlyingK sr nf nf' QQ r Q A f f' \<Longrightarrow> 297 wpc2_helper (P, P') (Q, Q') (\<lambda>_. PP,PP') (\<lambda>_. QQ,QQ') (corres_underlyingK sr nf nf' PP r P A f f')" 298 by (clarsimp simp: wpc2_helper_def corres_underlyingK_def elim!: corres_guard_imp) 299 300method corresc_left_raw = 301 determ \<open>(match conclusion in "corres_underlyingK sr nf nf' F r P P' f f'" for sr nf nf' F r P P' f f' 302 \<Rightarrow> \<open>apply_split f "\<lambda>f. corres_underlyingK sr nf nf' F r P P' f f'"\<close>, 303 corresc_body False helper: wpc2_helper_corres_left)\<close> 304 305lemma wpc2_helper_corres_right: 306 "corres_underlyingK sr nf nf' QQ r A Q f f' \<Longrightarrow> 307 wpc2_helper (P, P') (Q, Q') (\<lambda>_. PP,PP') (\<lambda>_. QQ,QQ') (corres_underlyingK sr nf nf' PP r A P f f')" 308 by (clarsimp simp: wpc2_helper_def corres_underlyingK_def elim!: corres_guard_imp) 309 310method corresc_right_raw = 311 determ \<open>(match conclusion in "corres_underlyingK sr nf nf' F r P P' f f'" for sr nf nf' F r P P' f f' 312 \<Rightarrow> \<open>apply_split f' "\<lambda>f'. corres_underlyingK sr nf nf' F r P P' f f'"\<close>, 313 corresc_body True helper: wpc2_helper_corres_right)\<close> 314 315definition 316 "corres_protect r = (r :: bool)" 317 318lemma corres_protect_conj_elim[simp]: 319 "corres_protect (a \<and> b) = (corres_protect a \<and> corres_protect b)" 320 by (simp add: corres_protect_def) 321 322lemma wpc2_corres_protect: 323 "wpc2_protect B Q \<Longrightarrow> corres_protect Q" 324 by (simp add: wpc2_protect_def corres_protect_def) 325 326method corresc_left = (corresc_left_raw; (drule wpc2_corres_protect[where B=False])) 327method corresc_right = (corresc_right_raw; (drule wpc2_corres_protect[where B=True])) 328 329named_theorems corresc_simp 330 331declare wpc2_protect_def[corresc_simp] 332declare corres_protect_def[corresc_simp] 333 334lemma corresK_false_guard_instantiate: 335 "False \<Longrightarrow> corres_underlyingK sr nf nf' True r P P' f f'" 336 by (simp add: corres_underlyingK_def) 337 338lemma 339 wpc_contr_helper: 340 "wpc2_protect False (A = B) \<Longrightarrow> wpc2_protect True (A = C) \<Longrightarrow> B \<noteq> C \<Longrightarrow> P" 341 by (auto simp: wpc2_protect_def) 342 343method corresc declares corresc_simp = 344 (check_corresK, corresc_left_raw; corresc_right_raw; 345 ((solves \<open>rule corresK_false_guard_instantiate, 346 determ \<open>(erule (1) wpc_contr_helper)?\<close>, simp add: corresc_simp\<close>) 347 | (drule wpc2_corres_protect[where B=False], drule wpc2_corres_protect[where B=True])))[1] 348 349section \<open>Corres_rv\<close> 350 351text \<open>Corres_rv is used to propagate backwards the stateless precondition (F) from corres_underlyingK. 352 It's main purpose is to defer the decision of where each condition should go: either continue 353 through the stateless precondition, or be pushed into the left/right side as a hoare triple.\<close> 354 355 356(*Don't unfold the definition. Use corres_rv method or associated rules. *) 357definition corres_rv :: "bool \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> ('t \<Rightarrow> bool) 358 \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('t, 'b) nondet_monad \<Rightarrow> 359 ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 360 where 361 "corres_rv F r P P' f f' Q \<equiv> 362 F \<longrightarrow> (\<forall>s s'. P s \<longrightarrow> P' s' \<longrightarrow> 363 (\<forall>sa rv. (rv, sa) \<in> fst (f s) \<longrightarrow> (\<forall>sa' rv'. (rv', sa') \<in> fst (f' s') \<longrightarrow> r rv rv' \<longrightarrow> Q rv rv')))" 364 365(*Don't unfold the definition. Use corres_rv method or associated rules. *) 366definition "corres_rvE_R F r P P' f f' Q \<equiv> 367 corres_rv F (\<lambda>_ _. True) P P' f f' 368 (\<lambda>rvE rvE'. case (rvE,rvE') of (Inr rv, Inr rv') \<Rightarrow> r rv rv' \<longrightarrow> Q rv rv' | _ \<Rightarrow> True)" 369 370lemma corres_rvD: 371 "corres_rv F r P P' f f' Q \<Longrightarrow> 372 F \<Longrightarrow> P s \<Longrightarrow> P' s' \<Longrightarrow> (rv,sa) \<in> fst (f s) \<Longrightarrow> 373 (rv',sa') \<in> fst (f' s') \<Longrightarrow> r rv rv' \<Longrightarrow> Q rv rv'" 374 by (auto simp add: corres_rv_def) 375 376lemma corres_rvE_RD: 377 "corres_rvE_R F r P P' f f' Q \<Longrightarrow> 378 F \<Longrightarrow> P s \<Longrightarrow> P' s' \<Longrightarrow> (Inr rv,sa) \<in> fst (f s) \<Longrightarrow> 379 (Inr rv',sa') \<in> fst (f' s') \<Longrightarrow> r rv rv' \<Longrightarrow> Q rv rv'" 380 by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 381 382lemma corres_rv_prove: 383 "(\<And>s s' sa sa' rv rv'. F \<Longrightarrow> 384 (rv,sa) \<in> fst (f s) \<Longrightarrow> (rv',sa') \<in> fst (f' s') \<Longrightarrow> P s \<Longrightarrow> P' s' \<Longrightarrow> r rv rv' \<Longrightarrow> Q rv rv') \<Longrightarrow> 385 corres_rv F r P P' f f' Q" 386 by (auto simp add: corres_rv_def) 387 388lemma corres_rvE_R_prove: 389 "(\<And>s s' sa sa' rv rv'. F \<Longrightarrow> 390 (Inr rv,sa) \<in> fst (f s) \<Longrightarrow> (Inr rv',sa') \<in> fst (f' s') \<Longrightarrow> P s \<Longrightarrow> P' s' \<Longrightarrow> r rv rv' \<Longrightarrow> Q rv rv') \<Longrightarrow> 391 corres_rvE_R F r P P' f f' Q" 392 by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 393 394lemma corres_rv_wp_left: 395 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. r rv rv' \<longrightarrow> Q rv rv'\<rbrace> \<Longrightarrow> corres_rv True r P \<top> f f' Q" 396 by (fastforce simp add: corres_rv_def valid_def) 397 398lemma corres_rvE_R_wp_left: 399 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. r rv rv' \<longrightarrow> Q rv rv'\<rbrace>, - \<Longrightarrow> corres_rvE_R True r P \<top> f f' Q" 400 apply (simp add: corres_rvE_R_def validE_def validE_R_def) 401 apply (rule corres_rv_wp_left) 402 apply (erule hoare_strengthen_post) 403 apply (auto split: sum.splits) 404 done 405 406lemma corres_rv_wp_right: 407 "\<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>rv' s. \<forall>rv. r rv rv' \<longrightarrow> Q rv rv'\<rbrace> \<Longrightarrow> corres_rv True r \<top> P' f f' Q" 408 by (fastforce simp add: corres_rv_def valid_def) 409 410lemma corres_rvE_R_wp_right: 411 "\<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>rv' s. \<forall>rv. r rv rv' \<longrightarrow> Q rv rv'\<rbrace>, - \<Longrightarrow> corres_rvE_R True r \<top> P' f f' Q" 412 apply (simp add: corres_rvE_R_def validE_def validE_R_def) 413 apply (rule corres_rv_wp_right) 414 apply (erule hoare_strengthen_post) 415 apply (auto split: sum.splits) 416 done 417 418lemma corres_rv_weaken: 419 "(\<And>rv rv'. Q rv rv' \<Longrightarrow> Q' rv rv') \<Longrightarrow> corres_rv F r P P' f f' Q \<Longrightarrow> corres_rv F r P P' f f' Q'" 420 by (auto simp add: corres_rv_def) 421 422lemma corres_rvE_R_weaken: 423 "(\<And>rv rv'. Q rv rv' \<Longrightarrow> Q' rv rv') \<Longrightarrow> corres_rvE_R F r P P' f f' Q \<Longrightarrow> corres_rvE_R F r P P' f f' Q'" 424 by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 425 426lemma corres_rv_defer_no_args: 427 "corres_rv (\<forall>rv rv'. r rv rv' \<longrightarrow> F) r (\<lambda>_. True) (\<lambda>_. True) f f' (\<lambda>_ _. F)" 428 by (auto simp add: corres_rv_def) 429 430lemma corres_rvE_R_defer_no_args: 431 "corres_rvE_R (\<forall>rv rv'. r rv rv' \<longrightarrow> F) r (\<lambda>_. True) (\<lambda>_. True) f f' (\<lambda>_ _. F)" 432 by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 433 434(*UNSAFE*) 435lemma corres_rv_defer: 436 "corres_rv (\<forall>rv rv'. r rv rv' \<longrightarrow> Q rv rv') r (\<lambda>_. True) (\<lambda>_. True) f f' Q" 437 by (auto simp add: corres_rv_def) 438 439(*UNSAFE*) 440lemma corres_rvE_R_defer: 441 "corres_rvE_R (\<forall>rv rv'. r rv rv' \<longrightarrow> Q rv rv') r (\<lambda>_. True) (\<lambda>_. True) f f' Q" 442 by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 443 444lemmas corres_rv_proveT = 445 corres_rv_prove[where P=\<top> and P'=\<top> and F=True, simplified] 446 447lemmas corres_rvE_R_proveT = 448 corres_rvE_R_prove[where P=\<top> and P'=\<top> and F=True,simplified] 449 450lemma corres_rv_conj_lift: 451 "corres_rv F r P PP f g Q \<Longrightarrow> corres_rv F' r P' PP' f g Q' \<Longrightarrow> 452 corres_rv (F \<and> F') r (\<lambda>s. P s \<and> P' s) (\<lambda>s'. PP s' \<and> PP' s') f g (\<lambda>rv rv'. Q rv rv' \<and> Q' rv rv')" 453 by (clarsimp simp add: corres_rv_def) 454 455lemma corres_rvE_R_conj_lift: 456 "corres_rvE_R F r P PP f g Q \<Longrightarrow> corres_rvE_R F' r P' PP' f g Q' \<Longrightarrow> 457 corres_rvE_R (F \<and> F') r (\<lambda>s. P s \<and> P' s) (\<lambda>s'. PP s' \<and> PP' s') f g (\<lambda>rv rv'. Q rv rv' \<and> Q' rv rv')" 458 by (auto simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 459 460subsection \<open>Corres_rv method\<close> 461 462text \<open>This method propagate corres_rv obligations into each precondition according to the following 463heuristic: 464 For each conjunct in the obligation: 465 466 1) Try to solve trivially (to handle schematic conditions) 467 2) If it does not depend on function return values, propagate it as a stateless precondition 468 3) If either side is a corres_noop (used by symbolic execution), propagate as hoare triple 469 for other side. 470 4) If it can be phrased entirely with variables accessible to the left side, propagate it as 471 a left hoare triple. 472 5) As in 3) but on the right. 473 474 Fail if any of 1-5 are unsuccessful for any conjunct. 475 476In the case where corres_rv fails, the user will need to intervene, either 477by specifying where to defer the obligation or solving the goal in-place. 478\<close> 479 480definition "corres_noop = return undefined" 481 482context begin 483 484private lemma corres_rv_defer_left: 485 "corres_rv F r (\<lambda>_. \<forall>rv rv'. Q rv rv') P' f f' Q" 486 by (simp add: corres_rv_def) 487 488private lemma corres_rvE_R_defer_left: 489 "corres_rvE_R F r (\<lambda>_. \<forall>rv rv'. Q rv rv') P' f f' Q" 490 by (simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 491 492private lemma corres_rv_defer_right: 493 "corres_rv F r P (\<lambda>_. \<forall>rv rv'. Q rv rv') f f' Q" 494 by (simp add: corres_rv_def) 495 496private lemma corres_rvE_R_defer_right: 497 "corres_rvE_R F r P (\<lambda>_. \<forall>rv rv'. Q rv rv') f f' Q" 498 by (simp add: corres_rv_def corres_rvE_R_def split: sum.splits) 499 500lemmas corres_rv_proves = 501 corres_rv_proveT corres_rvE_R_proveT 502 503(* Try to handle cases where corres_rv obligations have been left schematic *) 504lemmas corres_rv_trivials = 505 corres_rv_proves[where Q="\<lambda>_ _. True", OF TrueI] 506 corres_rv_proves[where Q="\<lambda>rv rv'. F rv rv' \<longrightarrow> True" for F, # \<open>simp\<close>] 507 corres_rv_proves[where Q=r and r=r for r, # \<open>simp\<close>] 508 509lemmas corres_rv_defers = 510 corres_rv_defer_no_args corres_rvE_R_defer_no_args 511 512lemmas corres_rv_wp_lefts = 513 corres_rv_wp_left corres_rvE_R_wp_left 514 515lemmas corres_rv_wp_rights = 516 corres_rv_wp_right corres_rvE_R_wp_right 517 518lemmas corres_rv_noops = 519 corres_rv_wp_lefts[where f'=corres_noop] corres_rv_wp_rights[where f=corres_noop] 520 521lemmas corres_rv_lifts' = 522 corres_rv_conj_lift corres_rvE_R_conj_lift 523 524lemmas corres_rv_lifts = 525 corres_rv_lifts' 526 corres_rv_lifts'[where P="\<lambda>_. True" and P'="\<lambda>_. True" and f="corres_noop", simplified] 527 corres_rv_lifts'[where PP="\<lambda>_. True" and PP'="\<lambda>_. True" and g="corres_noop", simplified] 528 529lemmas corres_rv_prove_simple = 530 corres_rv_proveT[# \<open>thin_tac _, thin_tac _\<close>, simplified] 531 532method corres_rv = 533 (((repeat_new \<open>rule corres_rv_trivials corres_rv_lifts\<close>)?); 534 ((rule corres_rv_trivials corres_rv_defers corres_rv_noops | 535 (succeeds \<open>rule corres_rv_defer_left corres_rvE_R_defer_left\<close>, 536 rule corres_rv_wp_lefts) | 537 (succeeds \<open>rule corres_rv_defer_right corres_rvE_R_defer_right\<close>, 538 rule corres_rv_wp_rights)))) 539 540end 541 542 543section \<open>CorresK Split rules\<close> 544 545text \<open> 546 The corresK split allows preconditions to be propagated backward via the extra stateless precondition 547 (here given as @{term F}. The head function is propagated backward directly, while the tail 548 is propagated via corres_rv. Using the corres_rv method, this condition is then decomposed and 549 pushed into the stateless, left, and right preconditions as appropriate. 550 551 The return value relation is now almost never needed directly, and so it is wrapped in corres_protect 552 to prevent it from being used during simplification. 553 \<close> 554 555lemma corresK_split: 556 assumes x: "corres_underlyingK sr nf nf' F r' P P' a c" 557 assumes y: "\<And>rv rv'. corres_protect (r' rv rv') \<Longrightarrow> corres_underlyingK sr nf nf' (F' rv rv') r (R rv) (R' rv') (b rv) (d rv')" 558 assumes c: "corres_rv F'' r' PP PP' a c F'" 559 assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>" 560 shows "corres_underlyingK sr nf nf' (F \<and> F'') r (PP and P and Q) (PP' and P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" 561 apply (clarsimp simp: corres_underlying_def corres_underlyingK_def bind_def) 562 apply (rule conjI) 563 apply (frule (3) x[simplified corres_underlyingK_def, rule_format, THEN corres_underlyingD],simp) 564 apply clarsimp 565 apply (drule(1) bspec,clarsimp) 566 apply (drule (5) corres_rvD[OF c]) 567 apply (rule_tac x="(ac,bc)" in bexI,clarsimp) 568 apply (frule_tac s'=baa in y[simplified corres_underlyingK_def corres_protect_def, rule_format, THEN corres_underlyingD]) 569 apply assumption+ 570 apply (erule(1) use_valid[OF _ z(1)]) 571 apply (erule(1) use_valid[OF _ z(2)]) 572 apply fastforce 573 apply clarsimp 574 apply (drule(1) bspec,clarsimp) 575 apply simp 576 apply (frule (3) x[simplified corres_underlyingK_def, rule_format, THEN corres_underlyingD],simp) 577 apply clarsimp 578 apply (drule(1) bspec,clarsimp) 579 apply (drule (5) corres_rvD[OF c]) 580 apply (frule_tac s'=baa in y[simplified corres_underlyingK_def corres_protect_def, rule_format, THEN corres_underlyingD]) 581 apply simp+ 582 apply (erule(1) use_valid[OF _ z(1)]) 583 apply (erule(1) use_valid[OF _ z(2)]) 584 apply fastforce 585 apply clarsimp 586 done 587 588section \<open>Corres_inst\<close> 589 590text \<open>Handles rare in-place subgoals generated by corres rules which need to be solved immediately 591 in order to instantiate a schematic. 592 We peek into the generated return-value relation to see if we can solve the instantiation. 593\<close> 594 595definition "corres_inst_eq x y \<equiv> x = y" 596 597lemma corres_inst_eqI[wp]: "corres_inst_eq x x" by (simp add: corres_inst_eq_def) 598 599lemma corres_inst_test: "False \<Longrightarrow> corres_inst_eq x y" by simp 600 601method corres_inst = 602 (succeeds \<open>rule corres_inst_test\<close>, fails \<open>rule TrueI\<close>, 603 (rule corres_inst_eqI | 604 (clarsimp simp: corres_protect_def split del: if_split, rule corres_inst_eqI) 605 | (clarsimp simp: corres_protect_def split del: if_split, 606 fastforce intro!: corres_inst_eqI)))[1] 607 608section \<open>Corres Method\<close> 609 610text \<open>Handles structured decomposition of corres goals\<close> 611 612named_theorems 613 corres_splits and (* rules that, one applied, must 614 eventually yield a successful corres or corresK rule application*) 615 corres_simp_del and (* bad simp rules that break everything *) 616 corres and (* solving terminal corres subgoals *) 617 corresK (* calculational rules that are phrased as corresK rules *) 618 619context begin 620 621lemma corres_fold_dc: 622 "corres_underlyingK sr nf nf' F dc P P' f f' \<Longrightarrow> corres_underlyingK sr nf nf' F (\<lambda>_ _. True) P P' f f'" 623 by (simp add: dc_def[abs_def]) 624 625private method corres_fold_dc = 626 (match conclusion in 627 "corres_underlyingK _ _ _ _ (\<lambda>_ _. True) _ _ _ _" \<Rightarrow> \<open>rule corres_fold_dc\<close>) 628 629section \<open>Corres_apply method\<close> 630 631text \<open>This is a private method that performs an in-place rewrite of corres rules into 632 corresK rules. This is primarily for backwards-compatibility with the existing corres proofs. 633 Works by trying to apply a corres rule, then folding the resulting subgoal state into a single 634 conjunct and atomizing it, then propagating the result into the stateless precondition. 635\<close> 636 637private definition "guard_collect (F :: bool) \<equiv> F" 638private definition "maybe_guard F \<equiv> True" 639 640private lemma corresK_assume_guard_guarded: 641 "(guard_collect F \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g) \<Longrightarrow> 642 maybe_guard F \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g" 643 by (simp add: corres_underlyingK_def guard_collect_def) 644 645private lemma guard_collect: "guard_collect F \<Longrightarrow> F" 646 by (simp add: guard_collect_def) 647 648private lemma has_guard: "maybe_guard F" by (simp add: maybe_guard_def) 649private lemma no_guard: "maybe_guard True" by (simp add: maybe_guard_def) 650 651private method corres_apply = 652 (rule corresK_assume_guard_guarded, 653 (determ \<open>rule corres\<close>, safe_fold_subgoals)[1], 654 #break "corres_apply", 655 ((focus_concl \<open>(atomize (full))?\<close>, erule guard_collect, rule has_guard) | rule no_guard))[1] 656 657private method corres_alternate = corres_inst | corres_rv 658 659 660 661method corres_once declares corres_splits corres corresK corresc_simp = 662 (no_schematic_concl, 663 (corres_alternate | 664 (corres_fold_dc?, 665 (corres_pre, 666 #break "corres", 667 ( (check_corresK, determ \<open>rule corresK\<close>) 668 | corres_apply 669 | corres_concrete_r 670 | corresc 671 | (rule corres_splits, corres_once) 672 ))))) 673 674 675method corres declares corres_splits corres corresK corresc_simp = 676 (corres_once+)[1] 677 678text \<open>Unconditionally try applying split rules. Useful for determining why corres is not applying 679 in a given proof.\<close> 680 681method corres_unsafe_split declares corres_splits corres corresK corresc_simp = 682 ((rule corres_splits | corres_pre | corres_once)+)[1] 683 684end 685 686lemmas [corres_splits] = 687 corresK_split 688 689lemma corresK_when [corres_splits]: 690 "\<lbrakk>corres_protect G \<Longrightarrow> corres_protect G' \<Longrightarrow> corres_underlyingK sr nf nf' F dc P P' a c\<rbrakk> 691\<Longrightarrow> corres_underlyingK sr nf nf' ((G = G') \<and> F) dc ((\<lambda>x. G \<longrightarrow> P x)) (\<lambda>x. G' \<longrightarrow> P' x) (when G a) (when G' c)" 692 apply (simp add: corres_underlying_def corres_underlyingK_def corres_protect_def) 693 apply (cases "G = G'"; cases G; simp) 694 by (clarsimp simp: return_def) 695 696lemma corresK_return_trivial: 697 "corres_underlyingK sr nf nf' True dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ())" 698 by (simp add: corres_underlyingK_def) 699 700lemma corresK_return_eq: 701 "corres_underlyingK sr nf nf' True (=) (\<lambda>_. True) (\<lambda>_. True) (return x) (return x)" 702 by (simp add: corres_underlyingK_def) 703 704lemma corres_lift_to_K: 705 "corres_underlying sra nfa nf'a ra Pa P'a fa f'a \<longrightarrow> corres_underlying sr nf nf' r P P' f f' \<Longrightarrow> 706 corres_underlyingK sra nfa nf'a F ra Pa P'a fa f'a \<longrightarrow> corres_underlyingK sr nf nf' F r P P' f f'" 707 by (simp add: corres_underlyingK_def) 708 709lemmas [THEN iffD2, atomized, THEN corresK_lift_rule, rule_format, simplified o_def, corres_splits] = 710 corres_liftE_rel_sum 711 corres_liftM_simp 712 corres_liftM2_simp 713 714 715lemmas [corresK] = 716 corresK_return_trivial 717 corresK_return_eq 718 719lemma corresK_subst_left: "g = f \<Longrightarrow> 720 corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> 721 corres_underlyingK sr nf nf' F r P P' g f'" by simp 722 723lemma corresK_subst_right: "g' = f' \<Longrightarrow> 724 corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow> 725 corres_underlyingK sr nf nf' F r P P' f g'" by simp 726 727lemmas corresK_fun_app_left[corres_splits] = corresK_subst_left[OF fun_app_def[THEN meta_eq_to_obj_eq]] 728lemmas corresK_fun_app_right[corres_splits] = corresK_subst_right[OF fun_app_def[THEN meta_eq_to_obj_eq]] 729 730lemmas corresK_Let_left[corres_splits] = corresK_subst_left[OF Let_def[THEN meta_eq_to_obj_eq]] 731lemmas corresK_Let_right[corres_splits] = corresK_subst_right[OF Let_def[THEN meta_eq_to_obj_eq]] 732 733lemmas corresK_return_bind_left[corres_splits] = corresK_subst_left[OF return_bind] 734lemmas corresK_return_bind_right[corres_splits] = corresK_subst_right[OF return_bind] 735 736lemmas corresK_liftE_bindE_left[corres_splits] = corresK_subst_left[OF liftE_bindE] 737lemmas corresK_liftE_bindE_right[corres_splits] = corresK_subst_right[OF liftE_bindE] 738 739lemmas corresK_K_bind_left[corres_splits] = 740 corresK_subst_left[where g="K_bind f rv" and f="f" for f rv, # \<open>simp\<close>] 741 742lemmas corresK_K_bind_right[corres_splits] = 743 corresK_subst_right[where g'="K_bind f' rv" and f'="f'" for f' rv, # \<open>simp\<close>] 744 745 746section \<open>Corres Search - find symbolic execution path that allows a given rule to be applied\<close> 747 748lemma corresK_if [corres_splits]: 749 "\<lbrakk>(corres_protect G \<Longrightarrow> corres_protect G' \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' a c); 750 (corres_protect (\<not>G) \<Longrightarrow> corres_protect (\<not>G') \<Longrightarrow> corres_underlyingK sr nf nf' F' r Q Q' b d)\<rbrakk> 751\<Longrightarrow> corres_underlyingK sr nf nf' ((G = G') \<and> (G \<longrightarrow> F) \<and> (\<not>G \<longrightarrow> F')) r (if G then P else Q) (if G' then P' else Q') (if G then a else b) 752 (if G' then c else d)" 753 by (simp add: corres_underlying_def corres_underlyingK_def corres_protect_def) 754 755lemma corresK_if_rev: 756 "\<lbrakk>(corres_protect (\<not> G) \<Longrightarrow> corres_protect G' \<Longrightarrow> corres_underlyingK sr nf nf' F r P P' a c); 757 (corres_protect G \<Longrightarrow> corres_protect (\<not>G') \<Longrightarrow> corres_underlyingK sr nf nf' F' r Q Q' b d)\<rbrakk> 758\<Longrightarrow> corres_underlyingK sr nf nf' ((\<not> G = G') \<and> (\<not>G \<longrightarrow> F) \<and> (G \<longrightarrow> F')) r (if G then Q else P) (if G' then P' else Q') (if G then b else a) 759 (if G' then c else d)" 760 by (simp add: corres_underlying_def corres_underlyingK_def corres_protect_def) 761 762 763 764named_theorems corres_symb_exec_ls and corres_symb_exec_rs 765 766lemma corresK_symb_exec_l_search[corres_symb_exec_ls]: 767 fixes x :: "'b \<Rightarrow> 'a \<Rightarrow> ('d \<times> 'a) set \<times> bool" 768 notes [simp] = corres_noop_def 769 shows 770 "\<lbrakk>\<And>s. \<lbrace>PP s\<rbrace> m \<lbrace>\<lambda>_. (=) s\<rbrace>; \<And>rv. corres_underlyingK sr nf True (F rv) r (Q rv) P' (x rv) y; 771 corres_rv F' dc RR (\<lambda>_. True) m (corres_noop) (\<lambda>rv _. F rv); 772 empty_fail m; no_fail P m; \<lbrace>R\<rbrace> m \<lbrace>Q\<rbrace>\<rbrakk> 773\<Longrightarrow> corres_underlyingK sr nf True F' r (RR and P and R and (\<lambda>s. \<forall>s'. s = s' \<longrightarrow> PP s' s)) P' (m >>= x) y" 774 apply (clarsimp simp add: corres_underlyingK_def) 775 apply (rule corres_name_pre) 776 apply (clarsimp simp: corres_underlying_def corres_underlyingK_def 777 bind_def valid_def empty_fail_def no_fail_def) 778 apply (drule_tac x=a in meta_spec)+ 779 apply (drule_tac x=a in spec)+ 780 apply (drule mp, assumption)+ 781 apply (clarsimp simp: not_empty_eq) 782 apply (drule corres_rvD; (assumption | simp add: return_def)?) 783 apply (drule_tac x="(aa,ba)" in bspec,simp)+ 784 apply clarsimp 785 apply (drule_tac x=aa in meta_spec) 786 apply clarsimp 787 apply (drule_tac x="(ba,b)" in bspec,simp) 788 apply clarsimp 789 apply (drule mp, fastforce) 790 apply clarsimp 791 apply (drule_tac x="(a,bb)" in bspec,simp) 792 apply clarsimp 793 apply (rule_tac x="(aa,ba)" in bexI) 794 apply (clarsimp) 795 apply (rule_tac x="(ab,bc)" in bexI) 796 apply (clarsimp)+ 797 done 798 799 800lemmas corresK_symb_exec_liftME_l_search[corres_symb_exec_ls] = 801 corresK_symb_exec_l_search[where 'd="'x + 'y", folded liftE_bindE] 802 803lemma corresK_symb_exec_r_search[corres_symb_exec_rs]: 804 fixes y :: "'b \<Rightarrow> 'a \<Rightarrow> ('e \<times> 'a) set \<times> bool" 805 assumes X: "\<And>s. \<lbrace>PP' s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>" 806 assumes corres: "\<And>rv. corres_underlyingK sr nf nf' (F rv) r P (Q' rv) x (y rv)" 807 assumes Y: "corres_rv F' dc (\<lambda>_. True) RR (corres_noop) m (\<lambda>_ rv'. F rv')" 808 assumes nf: "nf' \<Longrightarrow> no_fail P' m" 809 assumes Z: "\<lbrace>R\<rbrace> m \<lbrace>Q'\<rbrace>" 810 notes [simp] = corres_noop_def 811 shows 812 "corres_underlyingK sr nf nf' F' r P (RR and P' and R and (\<lambda>s. \<forall>s'. s = s' \<longrightarrow> PP' s' s)) x (m >>= y)" 813 apply (insert corres) 814 apply (simp add: corres_underlyingK_def) 815 apply (rule impI) 816 apply (rule corres_name_pre) 817 apply (clarsimp simp: corres_underlying_def corres_underlyingK_def 818 bind_def valid_def empty_fail_def no_fail_def) 819 apply (intro impI conjI ballI) 820 apply clarsimp 821 apply (frule(1) use_valid[OF _ X]) 822 apply (drule corres_rvD[OF Y]; (assumption | simp add: return_def)?) 823 apply (frule(1) use_valid[OF _ Z]) 824 apply (drule_tac x=aa in meta_spec) 825 apply clarsimp 826 apply (drule_tac x="(a, ba)" in bspec,simp) 827 apply (clarsimp) 828 apply (drule(1) bspec) 829 apply clarsimp 830 apply clarsimp 831 apply (frule(1) use_valid[OF _ X]) 832 apply (drule corres_rvD[OF Y]; (assumption | simp add: return_def)?) 833 apply (frule(1) use_valid[OF _ Z]) 834 apply fastforce 835 apply (rule no_failD[OF nf],simp+) 836 done 837 838lemmas corresK_symb_exec_liftME_r_search[corres_symb_exec_rs] = 839 corresK_symb_exec_r_search[where 'e="'x + 'y", folded liftE_bindE] 840 841context begin 842 843private method corres_search_wp = solves \<open>((wp | wpc | simp)+)[1]\<close> 844 845text \<open> 846 Depth-first search via symbolic execution of both left and right hand 847 sides, handling case statements and 848 potentially mismatched if statements. The find_goal 849 method handles searching each branch of case or if statements, while 850 we rely on backtracking to guess the order of left/right executions. 851 852 According to the above rules, a symbolic execution step can be taken 853 when the function can be shown to not modify the state. Questions 854 of wellformedness (i.e. empty_fail or no_fail) are deferred to the user 855 after the search concludes. 856\<close> 857 858 859private method corres_search_frame methods m uses search = 860 (#break "corres_search", 861 ((corres?, corres_once corres: search corresK:search) 862 | (corresc, find_goal \<open>m\<close>)[1] 863 | (rule corresK_if, find_goal \<open>m\<close>)[1] 864 | (rule corresK_if_rev, find_goal \<open>m\<close>)[1] 865 | (rule corres_symb_exec_ls, corres_search_wp, m) 866 | (rule corres_symb_exec_rs, corres_search_wp, m))) 867 868text \<open> 869 Set up local context where we make sure we don't know how to 870 corres our given rule. The search is finished when we can only 871 make corres progress once we add our rule back in 872\<close> 873 874method corres_search uses search 875 declares corres corres_symb_exec_ls corres_symb_exec_rs = 876 (corres_pre, 877 use search[corres del] search[corresK del] search[corres_splits del] in 878 \<open>use in \<open>corres_search_frame \<open>corres_search search: search\<close> search: search\<close>\<close>)[1] 879 880end 881 882chapter \<open>Misc Helper Lemmas\<close> 883 884 885lemma corresK_assert[corresK]: 886 "corres_underlyingK sr nf nf' ((nf' \<longrightarrow> Q) \<and> P) dc \<top> \<top> (assert P) (assert Q)" 887 by (auto simp add: corres_underlyingK_def corres_underlying_def return_def assert_def fail_def) 888 889lemma corres_stateAssert_implied_frame: 890 assumes A: "\<forall>s s'. (s, s') \<in> sr \<longrightarrow> F' \<longrightarrow> P' s \<longrightarrow> Q' s' \<longrightarrow> A s'" 891 assumes C: "\<And>x. corres_underlyingK sr nf nf' F r P Q f (g x)" 892 shows 893 "corres_underlyingK sr nf nf' (F \<and> F') r (P and P') (Q and Q') f (stateAssert A [] >>= g)" 894 apply (clarsimp simp: bind_assoc stateAssert_def) 895 apply (corres_search search: C[THEN corresK_unlift]) 896 apply (wp corres_rv_defer | simp add: A)+ 897 done 898 899lemma corresK_return [corres_concrete_r]: 900 "corres_underlyingK sr nf nf' (r a b) r \<top> \<top> (return a) (return b)" 901 by (simp add: corres_underlyingK_def) 902 903lemma corres_throwError_str [corres_concrete_rER]: 904 "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)" 905 by (simp add: corres_underlyingK_def)+ 906 907section \<open>Error Monad\<close> 908 909 910 911lemma corresK_splitE [corres_splits]: 912 assumes x: "corres_underlyingK sr nf nf' F (f \<oplus> r') P P' a c" 913 assumes y: "\<And>rv rv'. corres_protect (r' rv rv') \<Longrightarrow> corres_underlyingK sr nf nf' (F' rv rv') (f \<oplus> r) (R rv) (R' rv') (b rv) (d rv')" 914 assumes c: "corres_rvE_R F'' r' PP PP' a c F'" 915 assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>, -" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>, -" 916 shows "corres_underlyingK sr nf nf' (F \<and> F'') (f \<oplus> r) (PP and P and Q) (PP' and P' and Q') (a >>=E (\<lambda>rv. b rv)) (c >>=E (\<lambda>rv'. d rv'))" 917 unfolding bindE_def 918 apply (rule corresK_weakenK) 919 apply (rule corresK_split[OF x, where F'="\<lambda>rv rv'. case (rv,rv') of (Inr rva, Inr rva') \<Rightarrow> F' rva rva' | _ \<Rightarrow> True"]) 920 apply (simp add: corres_protect_def) 921 prefer 2 922 apply simp 923 apply (rule corres_rv_prove[where F=F'']) 924 apply (case_tac rv; case_tac rv'; simp) 925 apply (rule corres_rvE_RD[OF c]; assumption) 926 apply (case_tac rv; case_tac rv'; simp) 927 apply (simp add: corres_underlyingK_def corres_protect_def) 928 apply (rule corresK_weaken) 929 apply (rule y) 930 apply (simp add: corres_protect_def) 931 apply (subst conj_assoc[symmetric]) 932 apply (rule conjI) 933 apply (rule conjI) 934 apply (subgoal_tac "(case (Inr b) of (Inr b) \<Rightarrow> R b s 935 | _ \<Rightarrow> True)"; assumption?) 936 apply (subgoal_tac "(case (Inr ba) of (Inr ba) \<Rightarrow> R' ba s' 937 | _ \<Rightarrow> True)"; assumption?) 938 apply clarsimp+ 939 apply (insert z) 940 by ((fastforce simp: valid_def validE_def validE_R_def split: sum.splits)+) 941 942lemma corresK_returnOk [corres_concrete_r]: 943 "corres_underlyingK sr nf nf' (r (Inr a) (Inr b)) r \<top> \<top> (returnOk a) (returnOk b)" 944 by (simp add: returnOk_def corres_underlyingK_def) 945 946lemma corres_assertE_str[corresK]: 947 "corres_underlyingK sr nf nf' ((nf' \<longrightarrow> Q) \<and> P) (f \<oplus> dc) \<top> \<top> (assertE P) (assertE Q)" 948 by (auto simp add: corres_underlying_def corres_underlyingK_def returnOk_def return_def assertE_def fail_def) 949 950lemmas corres_symb_exec_whenE_l_search[corres_symb_exec_ls] = 951 corresK_symb_exec_l_search[where 'd="'x + 'y", folded liftE_bindE] 952 953lemmas corres_returnOk_liftEs 954 [folded returnOk_liftE, THEN iffD2, atomized, THEN corresK_lift_rule, rule_format, corresK] = 955 corres_liftE_rel_sum[where m="return x" for x] 956 corres_liftE_rel_sum[where m'="return x" for x] 957 958 959(* Failure *) 960 961lemma corresK_fail[corresK]: 962 "corres_underlyingK sr nf True False r P P' f fail" 963 by (simp add: corres_underlyingK_def) 964 965lemma corresK_fail_no_fail'[corresK]: 966 "corres_underlyingK sr nf False True (\<lambda>_ _. False) (\<lambda>_. True) (\<lambda>_. True) f fail" 967 apply (simp add: corres_underlyingK_def) 968 by (fastforce intro!: corres_fail) 969 970section \<open>Correswp\<close> 971 972text 973 \<open>This method wraps up wp and wpc to ensure that they don't accidentally generate schematic 974 assumptions when handling hoare triples that emerge from corres proofs. 975 This is partially due to wp not being smart enough to avoid applying certain wp_comb rules 976 when the precondition is schematic, and arises when the schematic precondition doesn't have 977 access to some meta-variables in the postcondition. 978 979 To solve this, instead of meta-implication in the wp_comb rules we use corres_inst_eq, which 980 can only be solved by reflexivity. In most cases these comb rules are either never applied or 981 solved trivially. If users manually apply corres_rv rules to create postconditions with 982 inaccessible meta-variables (@{method corres_rv} will never do this), then these rules will 983 be used. Since @{method corres_inst} has access to the protected return-value relation, it has a chance 984 to unify the generated precondition with the original schematic one.\<close> 985 986named_theorems correswp_wp_comb and correswp_wp_comb_del 987 988lemma corres_inst_eq_imp: 989 "corres_inst_eq A B \<Longrightarrow> A \<longrightarrow> B" by (simp add: corres_inst_eq_def) 990 991lemmas corres_hoare_pre = hoare_pre[# \<open>-\<close> \<open>atomize (full), rule allI, rule corres_inst_eq_imp\<close>] 992 993method correswp uses wp = 994 (determ \<open> 995 (fails \<open>schematic_hoare_pre\<close>, (wp add: wp | wpc)) 996 | (schematic_hoare_pre, 997 (use correswp_wp_comb [wp_comb] 998 correswp_wp_comb_del[wp_comb del] 999 hoare_pre[wp_pre del] 1000 corres_hoare_pre[wp_pre] 1001 in 1002 \<open>use in \<open>wp add: wp | wpc\<close>\<close>))\<close>) 1003 1004lemmas [correswp_wp_comb_del] = 1005 hoare_vcg_precond_imp 1006 hoare_vcg_precond_impE 1007 hoare_vcg_precond_impE_R 1008 1009lemma corres_inst_conj_lift[correswp_wp_comb]: 1010 "\<lbrakk>\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. corres_inst_eq (R s) (P s)\<rbrakk> \<Longrightarrow> 1011 \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" 1012 by (rule hoare_vcg_conj_lift; simp add: valid_def corres_inst_eq_def) 1013 1014lemmas [correswp_wp_comb] = 1015 correswp_wp_comb_del[# \<open>-\<close> \<open>atomize (full), rule allI, rule corres_inst_eq_imp\<close>] 1016 valid_validE_R 1017 hoare_vcg_R_conj[OF valid_validE_R] 1018 hoare_vcg_E_elim[OF valid_validE_E] 1019 hoare_vcg_E_conj[OF valid_validE_E] 1020 validE_validE_R 1021 hoare_vcg_R_conj 1022 hoare_vcg_E_elim 1023 hoare_vcg_E_conj 1024 hoare_vcg_conj_lift 1025 1026declare hoare_post_comb_imp_conj[correswp_wp_comb_del] 1027 1028section \<open>Corressimp\<close> 1029text \<open>Combines corres, wp and clarsimp\<close> 1030 1031text 1032\<open>If clarsimp solves a terminal subgoal, its preconditions are left uninstantiated. We can 1033try to catch this by first attempting a trivial instantiation before invoking clarsimp, but 1034only keeping the result if clarsimp solves the goal,\<close> 1035 1036lemmas hoare_True_inst = 1037 hoare_pre[where P="\<lambda>_. True", of "\<lambda>_. True", # \<open>-\<close> \<open>simp\<close>] 1038 asm_rl[of "\<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>E\<rbrace>,\<lbrace>R\<rbrace>" for f E R] 1039 1040lemmas corres_rv_True_inst = 1041 asm_rl[of "corres_rv True r (\<lambda>_. True) (\<lambda>_. True) f f' Q" for r f f' Q] 1042 asm_rl[of "corres_rvE_R True r (\<lambda>_. True) (\<lambda>_. True) f f' Q" for r f f' Q] 1043 1044lemmas corresK_True_inst = 1045 asm_rl[of "corres_underlyingK sr nf nf' True dc (\<lambda>_. True) (\<lambda>_. True) f g" for sr nf nf' f g] 1046 asm_rl[of "corres_underlyingK sr nf nf' True r (\<lambda>_. True) (\<lambda>_. True) f g" for sr nf nf' r f g] 1047 asm_rl[of "corres_underlying sr nf nf' dc (\<lambda>_. True) (\<lambda>_. True) f g" for sr nf nf' f g] 1048 asm_rl[of "corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) f g" for sr nf nf' r f g] 1049 1050lemmas calculus_True_insts = hoare_True_inst corres_rv_True_inst corresK_True_inst 1051 1052method corressimp uses simp cong search wp 1053 declares corres corresK corres_splits corresc_simp = 1054 ((no_schematic_concl, 1055 (corres corresc_simp: simp 1056 | correswp wp: wp 1057 | (rule calculus_True_insts, solves \<open>clarsimp cong: cong simp: simp corres_protect_def\<close>) 1058 | clarsimp cong: cong simp: simp simp del: corres_simp_del split del: if_split 1059 | (match search in _ \<Rightarrow> \<open>corres_search search: search\<close>)))+)[1] 1060 1061declare corres_return[corres_simp_del] 1062 1063section \<open>Normalize corres rule into corresK rule\<close> 1064 1065lemma corresK_convert: 1066 "A \<longrightarrow> corres_underlying sr nf nf' r P Q f f' \<Longrightarrow> 1067 corres_underlyingK sr nf nf' A r P Q f f'" 1068 by (auto simp add: corres_underlyingK_def) 1069 1070method corresK_convert = (((drule uncurry)+)?, drule corresK_convert corresK_drop) 1071 1072section \<open>Lifting corres results into wp proofs\<close> 1073 1074definition 1075 "ex_abs_underlying sr P s' \<equiv> \<exists>s. (s,s') \<in> sr \<and> P s" 1076 1077lemma ex_absI[intro!]: 1078 "(s, s') \<in> sr \<Longrightarrow> P s \<Longrightarrow> ex_abs_underlying sr P s'" 1079 by (auto simp add: ex_abs_underlying_def) 1080 1081lemma use_corresK': 1082 "corres_underlyingK sr False nf' F r PP PP' f f' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> 1083 \<lbrace>K F and PP' and ex_abs_underlying sr (PP and P)\<rbrace> f' \<lbrace>\<lambda>rv' s'. \<exists>rv. r rv rv' \<and> ex_abs_underlying sr (Q rv) s'\<rbrace>" 1084 by (fastforce simp: corres_underlying_def corres_underlyingK_def valid_def ex_abs_underlying_def) 1085 1086lemma use_corresK [wp]: 1087 "corres_underlyingK sr False nf' F r PP PP' f f' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. r rv rv' \<longrightarrow> Q rv' s\<rbrace> \<Longrightarrow> 1088 \<lbrace>K F and PP' and ex_abs_underlying sr (PP and P)\<rbrace> f' \<lbrace>\<lambda>rv'. ex_abs_underlying sr (Q rv')\<rbrace>" 1089 apply (fastforce simp: corres_underlying_def corres_underlyingK_def valid_def ex_abs_underlying_def) 1090 done 1091 1092lemma hoare_add_post': 1093 "\<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>P''\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> Q rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and P''\<rbrace> f \<lbrace>Q\<rbrace>" 1094 by (fastforce simp add: valid_def) 1095 1096lemma use_corresK_frame: 1097 assumes corres: "corres_underlyingK sr False nf' F r PP P' f f'" 1098 assumes frame: "(\<forall>s s' rv rv'. (s,s') \<in> sr \<longrightarrow> r rv rv' \<longrightarrow> Q rv s \<longrightarrow> Q' rv' s' \<longrightarrow> QQ' rv' s')" 1099 assumes valid: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1100 assumes valid': "\<lbrace>PP'\<rbrace> f' \<lbrace>Q'\<rbrace>" 1101 shows "\<lbrace>K F and P' and PP' and ex_abs_underlying sr (PP and P)\<rbrace> f' \<lbrace>QQ'\<rbrace>" 1102 apply (rule hoare_pre) 1103 apply (rule hoare_add_post'[OF valid']) 1104 apply (rule hoare_strengthen_post) 1105 apply (rule use_corresK'[OF corres valid]) 1106 apply (insert frame)[1] 1107 apply (clarsimp simp: ex_abs_underlying_def) 1108 apply clarsimp 1109 done 1110 1111lemma use_corresK_frame_E_R: 1112 assumes corres: "corres_underlyingK sr False nf' F (lf \<oplus> r) PP P' f f'" 1113 assumes frame: "(\<forall>s s' rv rv'. (s,s') \<in> sr \<longrightarrow> r rv rv' \<longrightarrow> Q rv s \<longrightarrow> Q' rv' s' \<longrightarrow> QQ' rv' s')" 1114 assumes valid: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -" 1115 assumes valid': "\<lbrace>PP'\<rbrace> f' \<lbrace>Q'\<rbrace>, -" 1116 shows "\<lbrace>K F and P' and PP' and ex_abs_underlying sr (PP and P)\<rbrace> f' \<lbrace>QQ'\<rbrace>, -" 1117 apply (simp only: validE_R_def validE_def) 1118 apply (rule use_corresK_frame[OF corres _ valid[simplified validE_R_def validE_def] valid'[simplified validE_R_def validE_def]]) 1119 by (auto simp: frame split: sum.splits) 1120 1121lemma K_True: "K True = (\<lambda>_. True)" by simp 1122lemma True_And: "((\<lambda>_. True) and P) = P" by simp 1123 1124method use_corres uses frame = 1125 (corresK_convert?, drule use_corresK_frame use_corresK_frame_E_R, rule frame, 1126 (solves \<open>wp\<close> | defer_tac), (solves \<open>wp\<close> | defer_tac), (simp only: True_And K_True)?) 1127 1128experiment 1129 fixes sr nf' r P P' f f' F G Q Q' QQ' PP PP' g g' 1130 assumes f_corres[corres]: "G \<Longrightarrow> F \<Longrightarrow> corres_underlying sr False True r P P' f f'" and 1131 g_corres[corres]: "corres_underlying sr False True dc \<top> \<top> g g'" and 1132 wpl [wp]: "\<lbrace>PP\<rbrace> f \<lbrace>Q\<rbrace>" and wpr [wp]: "\<lbrace>PP'\<rbrace> f' \<lbrace>Q'\<rbrace>" 1133 and [wp]: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>" "\<lbrace>PP\<rbrace> g \<lbrace>\<lambda>_. PP\<rbrace>" "\<lbrace>P'\<rbrace> g' \<lbrace>\<lambda>_. P'\<rbrace>" "\<lbrace>PP'\<rbrace> g' \<lbrace>\<lambda>_. PP'\<rbrace>" and 1134 frameA: "\<forall>s s' rv rv'. (s,s') \<in> sr \<longrightarrow> r rv rv' \<longrightarrow> Q rv s \<longrightarrow> Q' rv' s' \<longrightarrow> QQ' rv' s'" 1135 begin 1136 1137 lemmas f_Q' = f_corres[atomized, @\<open>use_corres frame: frameA\<close>] 1138 1139 lemma "G \<Longrightarrow> F \<Longrightarrow> corres_underlying sr False True dc (P and PP) (P' and PP') 1140 (g >>= (K (f >>= K (assert True)))) (g' >>= (K (f' >>= (\<lambda>rv'. (stateAssert (QQ' rv') [])))))" 1141 apply (simp only: stateAssert_def K_def) 1142 apply corres 1143 apply (corres_search search: corresK_assert) 1144 apply corres_rv 1145 apply (correswp | simp)+ 1146 apply corres_rv 1147 apply (correswp wp: f_Q' | simp)+ 1148 apply corressimp+ 1149 by auto 1150 1151end 1152 1153section \<open>Corres Argument lifting\<close> 1154 1155text \<open>Used for rewriting corres rules with syntactically equivalent arguments\<close> 1156 1157lemma lift_args_corres: 1158 "corres_underlying sr nf nf' r (P x) (P' x) (f x) (f' x) \<Longrightarrow> x = x' \<Longrightarrow> 1159 corres_underlying sr nf nf' r (P x) (P' x') (f x) (f' x')" by simp 1160 1161method lift_corres_args = 1162 (match premises in 1163 H[thin]:"corres_underlying _ _ _ _ (P x) (P' x) (f x) (f' x)" (cut 5) for P P' f f' x \<Rightarrow> 1164 \<open>match (f) in "\<lambda>_. g" for g \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> 1165 \<open>match (f') in "\<lambda>_. g'" for g' \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> 1166 \<open>cut_tac lift_args_corres[where f=f and f'=f' and P=P and P'=P', OF H]\<close>\<close>\<close>)+ 1167 1168(* Use calculational rules. Don't unfold the definition! *) 1169lemmas corres_rv_def_I_know_what_I'm_doing = corres_rv_def 1170lemmas corres_rvE_R_def_I_know_what_I'm_doing = corres_rvE_R_def 1171 1172hide_fact corres_rv_def 1173hide_fact corres_rvE_R_def 1174 1175end 1176