1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11(* Automation framework for general C refinement *) 12 13theory Ctac 14imports 15 AutoCorres_C 16 "CLib.XPres" 17begin 18 19(* This file includes theorems associated with ctac and friends *) 20 21context kernel 22begin 23 24(* tactic setup *) 25 26lemma match_ccorres: 27 "ccorres_underlying sr G r xf' arrel axf P P' hs a c 28 \<Longrightarrow> ccorres_underlying sr G r xf' arrel axf P P' hs a c" . 29 30(* xfru needs to appear in the lemma ... *) 31lemma match_ccorres_record: 32 fixes xfru :: "('a \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b" and xf' :: "cstate \<Rightarrow> 'b" and xfr :: "'b \<Rightarrow> 'a" 33 shows "ccorres_underlying sr G r (xfr \<circ> xf') arrel axf P P' hs a (c xfru) 34 \<Longrightarrow> ccorres_underlying sr G r (xfr \<circ> xf') arrel axf P P' hs a (c xfru)" . 35 36lemma match_ccorres_Seq: 37 "ccorres_underlying sr G r xf arrel axf P P' hs a (c ;; d) 38 \<Longrightarrow> ccorres_underlying sr G r xf arrel axf P P' hs a (c ;; d)" . 39 40lemma match_ccorres_call_Seq: 41 "ccorres_underlying sr G r xf arrel axf P P' hs a (call i f g c ;; d) 42 \<Longrightarrow> ccorres_underlying sr G r xf arrel axf P P' hs a (call i f g c ;; d)" . 43 44(* Most specific to least specific. ctac uses <base> ^ "_novcg" so the suffic is important for the 45 * ctac_splits lemmas *) 46lemmas ctac_splits_non_call = ccorres_split_nothrowE [where F = UNIV] ccorres_split_nothrow [where F = UNIV] 47lemmas ctac_splits_non_call_novcg = ccorres_split_nothrow_novcgE ccorres_split_nothrow_novcg 48 49lemmas ctac_splits_call = ccorres_split_nothrow_callE [where F = UNIV] ccorres_split_nothrow_call [where F = UNIV] 50lemmas ctac_splits_call_novcg = ccorres_split_nothrow_call_novcgE ccorres_split_nothrow_call_novcg 51 52lemmas ctac_splits_record = 53 ccorres_split_nothrow_call_record [where F = UNIV] ccorres_split_nothrow_record [where F = UNIV] 54(* Probably useless as-is *) 55lemmas ctac_splits_record_novcg = 56 ccorres_split_nothrow_call_record_novcg ccorres_split_nothrow_record_novcg 57 58(* None of these generate vcg obligations, so we don't need a _novcg alternative *) 59lemmas ctac_nosplit_non_call = match_ccorres 60lemmas ctac_nosplit_call = ccorres_callE ccorres_call 61lemmas ctac_nosplit_record = ccorres_call_record match_ccorres_record 62 63(* Used with the _spec and _modifies rules. WARNING: the order and 64 position of these assumptions is relied on by the tactic csymbr. The 65 guard for cc is then simplified and gen_asm2 can be used. *) 66lemma ccorres_lift_rhs_call: 67 assumes cc: "\<And>rv'. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv' \<inter> {s. P' rv' (i s)}) hs a (d' rv')" 68 (* WARNING: the tactic csymbr relies on the outermost variable (v) being of the same type as the return type of xf' *) 69 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 70 and f_spec: "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> P \<sigma> s} Call f {t. P' (xf'' t) s}" 71 and f_modifies: "modifies_spec f" 72 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 73 and gg: "\<And>x f s. globals (xfu' f s) = globals s" 74 and gi: "\<And>s. globals (i s) = globals s" 75 (* This is annoying, as simp doesn't always solve it *) 76 and Pig: "\<And>x (s :: cstate) v'. P' x (i s) 77 \<Longrightarrow> P' x (i (xfu' (\<lambda>_. x) s))" 78 (* The concrete guard here is stronger than required --- we really need xf'' t not v *) 79 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G 80 ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. v) s \<in> {s. s \<in> G' v}} 81 \<inter> {s. P (i s) (i s)}) hs a 82 (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xf'' t))) ;; d)" 83 (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") 84proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric], 85 rule ccorres_guard_imp [OF ccorres_split_nothrow, OF ccorres_call ceqv, OF _ gg xfxfu gi cc]) 86 show "ccorres dc xf'' \<top> (Collect (\<lambda>s. P s s)) [] (return ()) (Call f)" 87 apply (rule ccorres_guard_imp2) 88 apply (rule ccorres_noop_spec [OF f_spec f_modifies]) 89 apply simp 90 done 91next 92 show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp 93next 94 show "\<Gamma>\<turnstile> ?G' ?c {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s) \<inter> {sa. P' (xf' s) (i sa)}}" 95 apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. s", OF _ _ f_modifies]) 96 apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ f_spec]) 97 defer 98 apply vcg 99 apply (clarsimp simp add: gi mex_def meq_def xfxfu) 100 apply (clarsimp simp add: gi mex_def meq_def xfxfu Pig) 101 done 102qed simp_all 103 104lemma ccorres_lift_rhs_Basic: 105 assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' v)" 106 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 107 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 108 and gg: "\<And>x f s. globals (xfu' f s) = globals s" 109 (* WARNING: the tactic csymbr relies on the outermost variable being of the same type as the return type of xf' *) 110 (* and Pig: "\<And>x (s :: cstate) v'. P' x (i s) \<Longrightarrow> P' x (i (xfu' (\<lambda>_. x) s))" *) 111 (* The concrete guard here is stronger than required --- we really need xf'' t not v *) 112 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. xfu' (\<lambda>_. v) s \<in> G'} hs a (Basic (xfu' (\<lambda>_. v)) ;; d)" 113 (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") 114proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric], 115 rule ccorres_guard_imp [OF ccorres_split_nothrow, OF _ ceqv]) 116 show "ccorres dc xf' \<top> UNIV hs (return ()) ?c" 117 apply (rule ccorres_noop) 118 apply (vcg spec=modifies) 119 done 120next 121 fix rv' 122 show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> {s. rv' = v}) hs a (d' rv')" 123 apply (rule ccorres_gen_asm2) 124 apply (erule ssubst) 125 apply (rule cc) 126 done 127next 128 show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp 129next 130 show "\<Gamma>\<turnstile> ?G' ?c {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' \<inter> {_. xf' s = v}}" 131 apply vcg 132 apply (clarsimp simp add: xfxfu) 133 done 134qed simp_all 135 136 137(* This needs to correspond in the first 4 assumptions to the above _call: *) 138lemma ccorres_lift_rhs_call_record: 139 fixes xf' :: "cstate \<Rightarrow> 'a" and xfu' :: "('a \<Rightarrow> 'a) \<Rightarrow> cstate \<Rightarrow> cstate" 140 and xf'' :: "cstate \<Rightarrow> 'b" and xfr :: "'a \<Rightarrow> 'b" and xfru :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a" 141 assumes cc: "\<And>rv' :: 'b. ccorres_underlying rf_sr \<Gamma> r xf arrel axf 142 G (G' rv' \<inter> {s. P' rv' (i s)}) hs a (d' (xfru (\<lambda>_. rv') oldv))" 143 (* WARNING: the tactic csymbr relies on the outermost variable being of the same type as the return type of xf' *) 144 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 145 and f_spec: "\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> P \<sigma> s} Call f {t. P' (xf'' t) s}" 146 and f_modifies: "modifies_spec f" 147 (* WARNING: the tactic csymbr relies on the outermost variable being of the same type as the return type of xfr *) 148 and xfrxfru: "\<And>v s. xfr (xfru (\<lambda>_. v) s) = v" 149 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 150 and gg: "\<And>x f s. globals (xfu' f s) = globals s" 151 and gi: "\<And>s. globals (i s) = globals s" 152 and Pig: "\<And>x (s :: cstate) v'. P' x (i s) \<Longrightarrow> 153 P' x (i (xfu' (\<lambda>_. xfru (\<lambda>_. x) oldv) s))" 154 (* The concrete guard here is stronger than required --- we really need xf'' t not v *) 155 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G 156 ({s. \<forall>v v'. P' v (i s) \<longrightarrow> xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> {s. s \<in> G' v}} 157 \<inter> {s. P (i s) (i s)}) hs a 158 (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>_ t. Basic (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv))) ;; d)" 159 (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") 160proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric], 161 rule ccorres_guard_imp [OF ccorres_split_nothrow_record [where xfru = "xfru"], OF ccorres_call ceqv, OF _ gg _ gi cc]) 162 show "ccorres dc xf'' \<top> (Collect (\<lambda>s. P s s)) [] (return ()) (Call f)" 163 apply (rule ccorres_guard_imp2) 164 apply (rule ccorres_noop_spec [OF f_spec f_modifies]) 165 apply simp 166 done 167next 168 fix a s t 169 show "(xfr \<circ> xf') (xfu' (\<lambda>_. xfru (\<lambda>_. xf'' t) oldv) (s\<lparr>globals := globals t\<rparr>)) = xf'' t" 170 by (simp add: xfxfu xfrxfru) 171next 172 show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp 173next 174 show "\<Gamma>\<turnstile> ?G' ?c {s. xf' s = xfru (\<lambda>_. (xfr \<circ> xf') s) oldv \<and> 175 (\<forall>uu. dc uu ((xfr \<circ> xf') s) \<longrightarrow> s \<in> G' ((xfr \<circ> xf') s) \<inter> {sa. P' ((xfr \<circ> xf') s) (i sa)})}" 176 apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. s", OF _ _ f_modifies]) 177 apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ f_spec]) 178 defer 179 apply vcg 180 apply (clarsimp simp add: gi mex_def meq_def xfxfu) 181 apply (clarsimp simp add: gi mex_def meq_def xfxfu xfrxfru Pig) 182 done 183qed simp_all 184 185lemma ccorres_lift_rhs_Basic_record: 186 fixes xf' :: "cstate \<Rightarrow> 'a" and xfu' :: "('a \<Rightarrow> 'a) \<Rightarrow> cstate \<Rightarrow> cstate" and xfru :: "('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'a" 187 assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' (xfru (\<lambda>_. v) oldv))" 188 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 189 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 190 and gg: "\<And>x f s. globals (xfu' f s) = globals s" 191 (* The concrete guard here is stronger than required --- we really need xf'' t not v *) 192 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv) s \<in> G'} hs a (Basic (xfu' (\<lambda>_. xfru (\<lambda>_. v) oldv)) ;; d)" 193 (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") 194proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric], 195 rule ccorres_guard_imp [OF ccorres_split_nothrow_record [where xfru = "xfru"], OF _ ceqv]) 196 show "ccorres dc ((\<lambda>_. v) \<circ> xf') \<top> UNIV hs (return ()) ?c" 197 apply (rule ccorres_noop) 198 apply (vcg spec=modifies) 199 done 200next 201 fix rv' 202 show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> {s. rv' = v}) hs a (d' (xfru (\<lambda>_. rv') oldv))" 203 apply (rule ccorres_gen_asm2) 204 apply (erule ssubst) 205 apply (rule cc) 206 done 207next 208 show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp 209next 210 show "\<Gamma>\<turnstile> ?G' ?c {s. xf' s = xfru (\<lambda>_. ((\<lambda>_. v) \<circ> xf') s) oldv \<and> 211 (\<forall>uu. dc uu (((\<lambda>_. v) \<circ> xf') s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>((\<lambda>_. v) \<circ> xf') s = v\<rbrace>)}" 212 apply (rule conseqPre) 213 apply vcg 214 apply (clarsimp simp add: xfxfu) 215 done 216qed simp_all 217 218 219thm ccorres_lift_rhs_call [where P = "\<lambda>_ s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t (xfa s)"] 220 221lemmas ccorres_lift_rhs_no_guard = ccorres_lift_rhs_call [where P = "\<lambda>_ _. True", simplified] 222lemmas ccorres_lift_rhss = ccorres_lift_rhs_no_guard ccorres_lift_rhs_call 223 224lemmas ccorres_lift_rhs_record_no_guard = ccorres_lift_rhs_call_record [where P = "\<lambda>_ _. True", simplified] 225lemmas ccorres_lift_rhss_record = ccorres_lift_rhs_record_no_guard ccorres_lift_rhs_call_record 226 227lemma ccorres_lift_rhs_Basic_stateful: 228 assumes cc: "\<And>v. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' v) hs a (d' v)" 229 and xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v" 230 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 231 and gg: "\<And>x f s. globals (xfu' f s) = globals s" 232 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. xfu' (\<lambda>_. g s) s \<in> G' (g s)} hs a (Basic (\<lambda>s. xfu' (\<lambda>_. g s) s) ;; d)" 233 (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") 234proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric], 235 rule ccorres_guard_imp [OF ccorres_split_nothrow, OF _ ceqv]) 236 show "ccorres dc xf' \<top> UNIV hs (return ()) ?c" 237 apply (rule ccorres_noop) 238 apply (vcg spec=modifies) 239 done 240next 241 fix rv' 242 show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv') hs a (d' rv')" 243 by (rule cc) 244next 245 show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp 246next 247 show "\<Gamma>\<turnstile> ?G' ?c {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s)}" 248 apply (rule conseqPre) 249 apply vcg 250 apply (clarsimp simp add: xfxfu) 251 done 252qed simp_all 253 254lemma ccorres_lift_rhs_Spec_stateful: 255 assumes cc: "\<And>v. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' v) hs a (d' v)" 256 and ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')" 257 assumes gg: "\<And>v s. globals (upd (\<lambda>_. v) s) = globals s" 258 assumes upd_acc: "\<And>s. upd (\<lambda>_. accessor s) s = s" 259 shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. \<forall>v. upd (\<lambda>_. v) s \<in> G' (xf' (upd (\<lambda>_. v) s))} hs a (Spec {(s,t). \<exists>v. t = upd (\<lambda>_. v) s};; d)" 260 (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") 261proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric], 262 rule ccorres_guard_imp [OF ccorres_split_nothrow, OF _ ceqv]) 263 show "ccorres dc xf' \<top> UNIV hs (return ()) ?c" 264 apply (rule ccorres_noop) 265 apply (vcg spec=modifies) 266 apply clarsimp 267 apply (drule arg_cong[where f=globals]) 268 apply (simp add: gg) 269 apply (rule_tac x=x in exI) 270 apply (rule_tac x="accessor x" in exI) 271 apply (rule upd_acc [symmetric]) 272 done 273next 274 fix rv' 275 show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' rv') hs a (d' rv')" 276 by (rule cc) 277next 278 show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp 279next 280 show "\<Gamma>\<turnstile> ?G' ?c {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' (xf' s)}" 281 apply (rule conseqPre) 282 apply vcg 283 apply clarsimp 284 apply (rule conjI) 285 apply clarsimp 286 apply (rule_tac x=x in exI) 287 apply (rule_tac x="accessor x" in exI) 288 apply (rule upd_acc [symmetric]) 289 done 290qed simp_all 291 292(* For something like 293 294int foo(int x) 295{ 296 int i; 297 ... 298} 299 300the parser spits out 301 302lvar_nondet_init i_' i_'_update;; 303... 304 305which we need to remove --- lvar_nondet_init is a nondeterministic SPEC 306statement that picks any value for i, but leaves the rest unchanged. 307*) 308 309lemma ccorres_lift_rhs_remove_lvar_init: 310 assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a d" 311 assumes gg: "\<And>x f s. globals (i_upd f s) = globals s" 312 assumes upd_acc: "\<And>s. i_upd (\<lambda>_. i_acc s) s = s" 313 assumes arb: "\<And>s v. s \<in> G' \<Longrightarrow> i_upd (\<lambda>_. v) s \<in> G'" 314 shows "ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a (lvar_nondet_init i_acc i_upd ;; d)" 315 apply (unfold lvar_nondet_init_def) 316 apply (rule ccorres_guard_imp) 317 apply (rule ccorres_lift_rhs_Spec_stateful [OF cc ceqv_refl gg]) 318 apply (rule upd_acc) 319 apply assumption 320 apply (simp add: arb) 321 done 322 323lemma ccorres_lift_rhs_remove_lvar_init_unknown_guard: 324 assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a d" 325 assumes gg: "\<And>x f s. globals (i_upd f s) = globals s" 326 assumes upd_acc: "\<And>s. i_upd (\<lambda>_. i_acc s) s = s" 327 shows "ccorres_underlying rf_sr \<Gamma> r xf ar arf G {s. \<forall>v. i_upd (\<lambda>_. v) s \<in> G'} hs a (lvar_nondet_init i_acc i_upd ;; d)" 328 unfolding lvar_nondet_init_def 329 by (rule ccorres_lift_rhs_Spec_stateful [OF cc ceqv_refl gg], rule upd_acc) 330 331lemma ccorres_special_Int_cong: 332 "(\<And>s. P s = P' s) \<Longrightarrow> ccorres r xf G (G' \<inter> {s. P s}) hs a c = ccorres r xf G (G' \<inter> {s. P' s}) hs a c" by simp 333 334lemma ccorres_special_trim_Int: 335 "ccorres r xf G G' hs a c \<Longrightarrow> ccorres r xf G (G' \<inter> P') hs a c" 336 apply (erule ccorres_guard_imp) 337 apply simp 338 apply simp 339 done 340 341lemma semantic_equiv_def2: 342 fixes s :: "'b" and s' :: "('b, 'c) xstate" 343 shows "semantic_equiv G s s' a a' \<equiv> ((G \<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s') = (G \<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'))" 344 unfolding semantic_equiv_def ceqv_def 345 by simp 346 347(* MOVE *) 348lemma semantic_equiv_While_cong: 349 assumes se: "\<And>s s'. semantic_equiv Gamma s s' b b'" 350 shows "semantic_equiv Gamma s s' (While G b) (While G b')" 351 using se 352 apply - 353 apply (rule semantic_equivI) 354 apply (rule exec_While_cong) 355 apply (simp add: semantic_equiv_def2) 356 done 357 358lemma semantic_equiv_Seq_cong: 359 assumes sea: "\<And>s'. semantic_equiv Gamma s s' a a'" 360 and seb: "\<And>s. semantic_equiv Gamma s s' b b'" 361 shows "semantic_equiv Gamma s s' (a ;; b) (a' ;; b')" 362 using sea seb 363 apply (simp add: semantic_equiv_def2) 364 apply (rule exec_Seq_cong) 365 apply assumption 366 apply assumption 367 done 368 369lemma semantic_equiv_Seq_Skip: 370 assumes se: "semantic_equiv Gamma s s' a a'" 371 shows "semantic_equiv Gamma s s' (a ;; SKIP) a'" 372 using se unfolding semantic_equiv_def2 373 by (simp add: exec_Seq_Skip_simps) 374 375lemma semantic_equiv_Guard_cong: 376 assumes se: "semantic_equiv Gamma s s' a a'" 377 shows "semantic_equiv Gamma s s' (Guard F G a) (Guard F G a')" 378 using se 379 by (simp add: semantic_equiv_def2 exec_Guard) 380 381lemma semantic_equiv_Guard_UNIV: 382 assumes se: "semantic_equiv Gamma s s' a a'" 383 shows "semantic_equiv Gamma s s' (Guard F UNIV a) a'" 384 using se 385 by (simp add: semantic_equiv_def2 exec_Guard_UNIV_simp) 386 387lemma semantic_equiv_Guard_True: 388 assumes se: "semantic_equiv Gamma s s' a a'" 389 shows "semantic_equiv Gamma s s' (Guard F \<lbrace>True\<rbrace> a) a'" 390 using se 391 by (simp add: semantic_equiv_def2 exec_Guard_UNIV_simp) 392 393lemma semantic_equiv_refl: 394 shows "semantic_equiv Gamma s s' a a" 395 by (rule semantic_equivI, simp) 396 397lemma semantic_equiv_trans: 398 assumes sea: "semantic_equiv Gamma s s' a b" 399 and seb: "semantic_equiv Gamma s s' b c" 400 shows "semantic_equiv Gamma s s' a c" 401 using sea seb 402 by (simp add: semantic_equiv_def2) 403 404(* Ugh, a bit tricky to get this outcome without this sort of specialisation :( *) 405lemma semantic_equiv_Guard_Skip_Seq: 406 shows "semantic_equiv Gamma s s' (a ;; Guard F \<lbrace>True\<rbrace> SKIP) a" 407 apply (rule semantic_equiv_trans) 408 apply (rule semantic_equiv_Seq_cong) 409 apply (rule semantic_equiv_refl) 410 apply (rule semantic_equiv_Guard_True) 411 apply (rule semantic_equiv_refl) 412 apply (rule semantic_equiv_Seq_Skip) 413 apply (rule semantic_equiv_refl) 414 done 415 416lemma semantic_equiv_Seq_assoc: 417 shows "semantic_equiv Gamma s s' (a ;; (b ;; c)) (a ;; b ;; c)" 418 apply (rule semantic_equivI) 419 apply (rule exec_assoc) 420 done 421 422lemma semantic_equiv_seq_assoc_eq: 423 "semantic_equiv Gamma s s' (a ;; (b ;; c)) d 424 = semantic_equiv Gamma s s' (a ;; b ;; c) d" 425 "semantic_equiv Gamma s s' d (a ;; (b ;; c)) 426 = semantic_equiv Gamma s s' d (a ;; b ;; c)" 427 by (metis semantic_equiv_trans semantic_equiv_Seq_assoc 428 semantic_equiv_Seq_assoc[THEN semantic_equiv_sym[THEN iffD1]])+ 429 430lemma semantic_equiv_Cond: 431 assumes sel: "semantic_equiv Gamma s s' l l'" 432 and ser: "semantic_equiv Gamma s s' r r'" 433 shows "semantic_equiv Gamma s s' (Cond P l r) (Cond P l' r')" 434 using sel ser 435 by (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros) 436 437lemma semantic_equiv_Cond_True: 438 "semantic_equiv G s s' (Cond UNIV c c') c" 439 by (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros) 440 441lemma semantic_equiv_Cond_False: 442 "semantic_equiv G s s' (Cond {} c c') c'" 443 by (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros) 444 445lemma semantic_equiv_Cond_cases: 446 "semantic_equiv G s s' a (Cond P c d) 447 = semantic_equiv G s s' a (if s \<in> P then c else d)" 448 "semantic_equiv G s s' (Cond P c d) e 449 = semantic_equiv G s s' (if s \<in> P then c else d) e" 450 by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros) 451 452lemma semantic_equiv_cond_seq2: 453 "semantic_equiv G s s' (e;; Cond Q (c;;d) (c';;d)) (e;; Cond Q c c';; d)" 454 apply (simp add: semantic_equiv_seq_assoc_eq[symmetric]) 455 apply (rule semantic_equiv_Seq_cong, rule semantic_equiv_refl) 456 by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros) 457 458lemmas ccorres_cond_seq2 = ccorres_semantic_equiv[OF semantic_equiv_cond_seq2] 459 460lemma semantic_equiv_cond_seq2_seq: 461 "semantic_equiv G s s' (ci;; Cond Q (c;;ce) (c';;ce);; d) (ci;; Cond Q c c';; ce;; d)" 462 apply (simp add: semantic_equiv_seq_assoc_eq[symmetric]) 463 apply (rule semantic_equiv_Seq_cong, rule semantic_equiv_refl) 464 apply (simp add: semantic_equiv_seq_assoc_eq) 465 by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros) 466 467lemmas ccorres_cond_seq2_seq = ccorres_semantic_equiv[OF semantic_equiv_cond_seq2_seq] 468 469(* FIXME: move 470 It appears that the semantic equiv. lemmas should go into their own file, then 471 CCorresLemmas on top of that, and then finally Ctac on top of CCorresLemmas *) 472lemma ccorres_rewrite_cond_sr: 473 assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> s' \<in> Q' \<longrightarrow> (s' \<in> C) = (s' \<in> C') " 474 and c1: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs m (Cond C' c d)" 475 shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs 476 m (Cond C c d)" 477 apply (rule ccorres_name_pre) 478 apply (rule_tac Q="(=) s" and Q'="P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}" in stronger_ccorres_guard_imp) 479 apply (rule ccorres_semantic_equiv[THEN iffD1, rotated]) 480 apply (rule ccorres_guard_imp, rule c1, simp_all) 481 apply (clarsimp simp add: semantic_equiv_Cond_cases abs semantic_equiv_refl) 482 done 483 484lemma ccorres_rewrite_cond_sr_Seq: 485 assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> s' \<in> Q' \<longrightarrow> (s' \<in> C) = (s' \<in> C') " 486 and c1: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs m (Cond C' c d ;; e)" 487 shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs 488 m (Cond C c d ;; e)" 489 apply (rule ccorres_name_pre) 490 apply (rule_tac Q="(=) s" and Q'="P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}" in stronger_ccorres_guard_imp) 491 apply (rule ccorres_semantic_equiv[THEN iffD1, rotated]) 492 apply (rule ccorres_guard_imp, rule c1, simp_all) 493 apply (rule semantic_equiv_Seq_cong) 494 apply (clarsimp simp add: semantic_equiv_Cond_cases abs semantic_equiv_refl)+ 495 done 496 497definition 498 "push_in_stmt G stmt c c' \<equiv> (\<forall>s s'. semantic_equiv G s s' (c ;; stmt) c')" 499 500lemma pis_base: 501 "push_in_stmt G stmt c (c ;; stmt)" 502 unfolding push_in_stmt_def by (clarsimp intro!: semantic_equivI) 503 504lemma pis_throw: 505 "push_in_stmt G stmt THROW THROW" 506 unfolding push_in_stmt_def 507 by (auto elim!: exec_Normal_elim_cases intro: semantic_equivI exec.intros) 508 509lemma pis_Seq_right: 510 "push_in_stmt G stmt d d' \<Longrightarrow> push_in_stmt G stmt (c ;; d) (c ;; d')" 511 unfolding push_in_stmt_def 512 apply (intro allI) 513 apply (rule semantic_equiv_trans [rotated]) 514 apply (rule semantic_equiv_Seq_cong [OF semantic_equiv_refl]) 515 apply (drule spec, drule spec, assumption) 516 apply (subst semantic_equiv_sym) 517 apply (rule semantic_equiv_Seq_assoc) 518 done 519 520lemma pis_creturn: 521 "push_in_stmt G stmt (return_C xfu xf) (return_C xfu xf)" 522 unfolding creturn_def 523 by (rule pis_Seq_right | rule pis_throw)+ 524 525lemma pis_Cond: 526 "\<lbrakk> push_in_stmt G stmt l l'; push_in_stmt G stmt r r' \<rbrakk> \<Longrightarrow> 527 push_in_stmt G stmt (Cond P l r) (Cond P l' r')" 528 unfolding push_in_stmt_def 529 apply (intro allI) 530 apply (drule_tac x = s in spec, drule_tac x = s' in spec)+ 531 apply (case_tac "s \<in> P") 532 apply (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros) 533 done 534 535(* We check this before simplifying everything, so we need to deal with switch *) 536lemma pis_switch_Cons: 537 "\<lbrakk> push_in_stmt G stmt c c'; 538 push_in_stmt G stmt (switch v (x # xs)) (switch v cs) \<rbrakk> 539 \<Longrightarrow> push_in_stmt G stmt (switch v ((g, c) # (x # xs))) (switch v ((g, c') # cs))" 540 by (simp add: pis_Cond) 541 542lemma pis_switch_Singleton: 543 "\<lbrakk> push_in_stmt G stmt c c' \<rbrakk> \<Longrightarrow> push_in_stmt G stmt (switch v [(UNIV, c)]) (switch v [(UNIV, c')])" 544 apply (clarsimp simp: push_in_stmt_def) 545 apply (rule semantic_equiv_trans [OF _ iffD2 [OF semantic_equiv_sym, OF semantic_equiv_Cond_True]]) 546 apply (rule semantic_equiv_trans [rotated]) 547 apply (drule spec, drule spec, assumption) 548 apply (rule semantic_equiv_Seq_cong [OF semantic_equiv_Cond_True semantic_equiv_refl]) 549 done 550 551lemma pis_Guard: 552 "push_in_stmt G stmt c c' \<Longrightarrow> push_in_stmt G stmt (Guard f G' c) (Guard f G' c')" 553 unfolding push_in_stmt_def 554 apply (intro allI) 555 apply (rule semantic_equiv_trans [OF Guard_Seq_semantic_equiv]) 556 apply (rule semantic_equiv_Guard_cong) 557 apply (drule spec, erule spec) 558 done 559 560lemmas push_in_stmt_rules = 561 \<comment> \<open>No ordering apart from pis_base which must be last.\<close> 562 pis_throw 563 pis_creturn 564 pis_Seq_right 565 pis_Cond 566 pis_switch_Singleton pis_switch_Cons 567 pis_Guard 568 \<comment> \<open>Last, just stick it where it is\<close> 569 pis_base 570 571lemma ccorres_special_trim_guard_DontReach_pis: 572 assumes at: "push_in_stmt Gamma (Guard DontReach {} c) b b'" 573 and c: "ccorres_underlying sr Gamma r xf ar axf G G' hs a b'" 574 shows "ccorres_underlying sr Gamma r xf ar axf G G' hs a (b ;; Guard DontReach {} c)" 575 using c at unfolding push_in_stmt_def 576 apply - 577 apply (erule ccorres_semantic_equivD2) 578 apply (drule spec, erule spec) 579 done 580 581end 582 583lemmas ccorres_boilerplace_simp_dels = 584 Collect_const \<comment> \<open>Avoid getting an implication due to if_split. Should probably just remove if_split\<close> 585 586lemma ccorres_introduce_UNIV_Int_when_needed: 587 "ccorres_underlying sr Gamm r xf ar axf P (UNIV \<inter> {x. Q x}) hs a c 588 \<Longrightarrow> ccorres_underlying sr Gamm r xf ar axf P {x. Q x} hs a c" 589 by simp 590 591lemma Normal_Abrupt_resultE [consumes 2, case_names normal abrupt]: 592 assumes ex: "\<Gamma> \<turnstile> \<langle>c, s\<rangle> \<Rightarrow> t" 593 and t: "t = Normal t' \<or> t = Abrupt t'" 594 and r1: "\<And>s'. \<lbrakk>\<Gamma> \<turnstile> \<langle>c, Normal s'\<rangle> \<Rightarrow> t; s = Normal s'\<rbrakk> \<Longrightarrow> R" 595 and r2: "\<And>s'. \<lbrakk>\<Gamma> \<turnstile> \<langle>c, Abrupt s'\<rangle> \<Rightarrow> t; s = Abrupt s'\<rbrakk> \<Longrightarrow> R" 596 shows R 597 using ex t 598 apply - 599 apply (erule disjE) 600 apply simp 601 apply (erule Normal_resultE) 602 apply (rule r1) 603 apply simp 604 apply simp 605 apply simp 606 apply (erule Abrupt_resultE) 607 apply (rule r1) 608 apply simp 609 apply simp 610 apply (rule r2) 611 apply simp 612 apply simp 613 done 614 615(* Used so we can pattern match in ceqv (and hopefully speed things up *) 616definition 617 "rewrite_xf xf t v f f' \<equiv> xf t = v \<longrightarrow> f t = f' t" 618 619lemma rewrite_xfI: 620 "(xf t = v \<Longrightarrow> f t = f' t) \<Longrightarrow> rewrite_xf xf t v f f'" 621 unfolding rewrite_xf_def by auto 622 623lemma rewrite_xfD: 624 "\<lbrakk> rewrite_xf xf t v f f'; xf t = v \<rbrakk> \<Longrightarrow> f t = f' t" 625 unfolding rewrite_xf_def by auto 626 627lemma Basic_ceqv: 628 assumes rl: "rewrite_xf xf t v f f'" 629 shows "ceqv \<Gamma> xf v t t' (Basic f) (Basic f')" 630 apply - 631 apply (rule ceqvI) 632 apply (drule rewrite_xfD [OF rl]) 633 apply rule 634 apply (erule exec_Normal_elim_cases) 635 apply simp 636 apply rule 637 apply (erule exec_Normal_elim_cases) 638 apply simp 639 apply (erule subst) 640 apply (rule exec.Basic) 641 done 642 643(* the tactic uses THEN_ALL_NEW, which goes backwards *) 644lemma Seq_ceqv: 645 assumes ra: "\<And>t'. ceqv \<Gamma> xf v t t' a a'" 646 and rb: "\<And>t. ceqv \<Gamma> xf v t t' b b'" 647 and xp: "xpres xf v \<Gamma> a" (* Check that a does preserve xf first *) 648 shows "ceqv \<Gamma> xf v t t' (a ;; b) (a' ;; b')" 649 using xp 650 apply - 651 apply (rule ceqvI) 652 apply rule 653 apply (erule exec_Normal_elim_cases) 654 apply rule 655 apply (erule (1) ceqvD1 [OF _ _ ra]) 656 apply (case_tac s') 657 apply simp 658 apply (erule ceqvD1) 659 prefer 2 660 apply (rule assms) 661 apply (rule xpresD [where xf = xf], assumption+) 662 apply (fastforce dest: Abrupt_end Fault_end Stuck_end)+ 663 (* clag *) 664 apply (erule exec_Normal_elim_cases) 665 apply rule 666 apply (erule (1) ceqvD2 [OF _ _ ra]) 667 apply (case_tac s') 668 apply simp 669 apply (erule ceqvD2) 670 prefer 2 671 apply (rule assms) 672 apply (rule xpresD [where xf = xf], assumption+) 673 apply (erule (1) ceqvD2 [OF _ _ ra]) 674 apply (fastforce dest: Abrupt_end Fault_end Stuck_end)+ 675 done 676 677lemma Seq_weak_ceqv: (* A weaker form where xpres doesn't hold for a *) 678 assumes ra: "\<And>t'. ceqv \<Gamma> xf v t t' a a'" 679 shows "ceqv \<Gamma> xf v t t' (a ;; b) (a' ;; b)" 680 apply - 681 apply (rule ceqvI) 682 apply rule 683 apply (erule exec_Normal_elim_cases) 684 apply rule 685 apply (erule (2) ceqvD1 [OF _ _ ra]) 686 (* clag *) 687 apply (erule exec_Normal_elim_cases) 688 apply rule 689 apply (erule (2) ceqvD2 [OF _ _ ra]) 690 done 691 692lemma xpres_ceqv: 693 assumes xp: "xpres xf v \<Gamma> a" 694 and ceq: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'" 695 shows "xpres xf v \<Gamma> a'" 696 apply (rule xpresI) 697 apply (drule (1) ceqvD2 [OF _ _ ceq]) 698 apply (erule (2) xpres_exec0 [OF xp]) 699 done 700 701lemma While_ceqv_na0: 702 assumes ra: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'" 703 and xp: "xpres xf v \<Gamma> a" 704 and ex: "\<Gamma>\<turnstile> \<langle>d,s\<rangle> \<Rightarrow> t'" 705 and beq0: "\<And>t. xf t = v \<longrightarrow> (t \<in> b) = (t \<in> b')" 706 and d: "d = While b a" 707 and s: "s \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}" 708 and d': "d' = While b' a'" 709 and t: "\<not> isFault t'" "t' \<noteq> Stuck" 710 shows "\<Gamma>\<turnstile> \<langle>d',s\<rangle> \<Rightarrow> t'" 711 using ex d s d' t 712proof (induct) 713 case (WhileTrue s' b'' c' t u) 714 hence bv: "b'' = b" and cv: "c' = a" and xfs: "xf s' = v" by auto 715 716 note xp = xpres_ceqv [OF xp ra] 717 718 note beq = beq0 [rule_format] 719 720 have "\<Gamma> \<turnstile> \<langle>While b' a', Normal s'\<rangle> \<Rightarrow> u" 721 proof (rule exec.WhileTrue) 722 show "s' \<in> b'" using beq xfs bv[symmetric] WhileTrue 723 by auto 724 725 show ae: "\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t" using WhileTrue ceqvD1[OF _ _ ra] 726 by auto 727 728 show "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" 729 proof (subst d' [symmetric], rule WhileTrue.hyps(5)) 730 obtain z where "u = Normal z \<or> u = Abrupt z" 731 using WhileTrue.prems by (cases u, auto) 732 then obtain z' where "t = Normal z' \<or> t = Abrupt z'" 733 using WhileTrue.prems WhileTrue.hyps(2) WhileTrue.hyps(4) 734 by (auto elim: Normal_resultE Abrupt_resultE) 735 736 thus "t \<in> Normal ` {s. xf s = v} \<union> Abrupt ` {s. xf s = v}" using xp ae xfs 737 by (auto dest: xpres_exec0) 738 qed fact+ 739 qed 740 thus ?case using WhileTrue.prems by simp 741next 742 note beq = beq0 [rule_format] 743 744 case WhileFalse 745 thus ?case 746 apply simp 747 apply rule 748 apply (erule disjE) 749 apply (erule imageE, simp) 750 apply (auto simp: beq) 751 done 752qed simp_all 753 754lemmas While_ceqv_na = While_ceqv_na0 [OF _ _ _ _ refl _ refl] 755 756lemma While_ceqv_fs0: 757 assumes ra: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'" 758 and xp: "xpres xf v \<Gamma> a" 759 and ex: "\<Gamma>\<turnstile> \<langle>d,x\<rangle> \<Rightarrow> t'" 760 and d: "d = While b a" 761 and d': "d' = While b' a'" 762 and beq0: "\<And>t. xf t = v \<longrightarrow> (t \<in> b) = (t \<in> b')" 763 and t: "isFault t' \<or> t' = Stuck" 764 and s: "x \<in> Normal ` {s. xf s = v}" 765 shows "\<Gamma>\<turnstile> \<langle>d',x\<rangle> \<Rightarrow> t'" 766 using ex d d' t s 767proof (induct) 768 case (WhileTrue s' b'' c' t u) 769 hence bv: "b'' = b" and cv: "c' = a" and xfs: "xf s' = v" by auto 770 771 note xp = xpres_ceqv [OF xp ra] 772 773 note beq = beq0 [rule_format] 774 775 have "\<Gamma> \<turnstile> \<langle>While b' a', Normal s'\<rangle> \<Rightarrow> u" 776 proof (rule exec.WhileTrue) 777 show sb: "s' \<in> b'" using WhileTrue beq by auto 778 779 show ae: "\<Gamma>\<turnstile> \<langle>a',Normal s'\<rangle> \<Rightarrow> t" 780 using xfs WhileTrue ceqvD1[OF _ _ ra] by auto 781 782 { 783 fix f 784 assume "u = Fault f" and "t = Fault f" 785 hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" by simp 786 } moreover 787 { 788 fix f z 789 assume uv: "u = Fault f" and tv: "t = Normal z" 790 791 have "\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u" 792 proof (rule WhileTrue.hyps(5)) 793 show "isFault u \<or> u = Stuck" using uv by simp 794 have "xf z = v" using xfs ae 795 apply - 796 apply (erule xpresD [OF _ xp]) 797 apply (simp add: tv) 798 done 799 800 thus "t \<in> Normal ` {s. xf s = v}" by (simp add: tv) 801 qed fact+ 802 hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" using d' by simp 803 } moreover 804 { 805 assume "u = Stuck" and "t = Stuck" 806 hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" by simp 807 } moreover 808 { 809 fix z 810 assume uv: "u = Stuck" and tv: "t = Normal z" 811 (* clag *) 812 have "\<Gamma>\<turnstile> \<langle>d',t\<rangle> \<Rightarrow> u" 813 proof (rule WhileTrue.hyps(5)) 814 show "isFault u \<or> u = Stuck" using uv by simp 815 have "xf z = v" using xfs ae 816 apply - 817 apply (erule xpresD [OF _ xp]) 818 apply (simp add: tv) 819 done 820 821 thus "t \<in> Normal ` {s. xf s = v}" by (simp add: tv) 822 qed fact+ 823 hence "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" using d' by simp 824 } 825 ultimately show "\<Gamma>\<turnstile> \<langle>While b' a',t\<rangle> \<Rightarrow> u" using WhileTrue.prems WhileTrue.hyps(4) 826 by (auto elim: Fault_resultE Stuck_resultE elim!: isFaultE) 827 qed 828 thus ?case by (simp add: d') 829qed simp_all 830 831lemmas While_ceqv_fs = While_ceqv_fs0 [OF _ _ _ refl refl] 832 833lemma While_ceqv: 834 assumes beq: "\<And>t. xf t = v \<longrightarrow> (t \<in> b) = (t \<in> b')" 835 and ra: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'" 836 and xp: "xpres xf v \<Gamma> a" (* So we fail as early as possible *) 837 shows "ceqv \<Gamma> xf v t t' (While b a) (While b' a')" (* b is a set, doesn't rewrite nicely *) 838 using xp 839 apply - 840 apply (rule ceqvI) 841 apply (cases t') 842 apply rule 843 apply (erule (1) While_ceqv_na [OF ra]) 844 apply (rule beq) 845 apply simp 846 apply simp 847 apply simp 848 apply (rule While_ceqv_na [OF ceqv_sym [OF ra]]) 849 apply (erule (1) xpres_ceqv [OF _ ra]) 850 apply (rule impI) 851 apply (erule beq [rule_format, symmetric]) 852 apply simp 853 apply simp 854 apply simp 855 (* clag *) 856 apply rule 857 apply (erule (1) While_ceqv_na [OF ra]) 858 apply (rule beq) 859 apply simp 860 apply simp 861 apply simp 862 apply simp 863 apply (rule While_ceqv_na [OF ceqv_sym [OF ra]]) 864 apply (erule (1) xpres_ceqv [OF _ ra]) 865 apply (rule impI) 866 apply (erule beq [rule_format, symmetric]) 867 apply simp 868 apply simp 869 apply simp 870 apply rule 871 apply (erule While_ceqv_fs [OF ra xp]) 872 apply (rule beq) 873 apply simp 874 apply simp 875 apply (rule While_ceqv_fs [OF ceqv_sym [OF ra]]) 876 apply (erule (1) xpres_ceqv [OF _ ra]) 877 apply (rule impI) 878 apply (erule beq [rule_format, symmetric]) 879 apply simp 880 apply simp 881(* clag *) 882 apply rule 883 apply (erule While_ceqv_fs [OF ra xp]) 884 apply (rule beq) 885 apply simp 886 apply simp 887 apply (rule While_ceqv_fs [OF ceqv_sym [OF ra]]) 888 apply (erule (1) xpres_ceqv [OF _ ra]) 889 apply (rule impI) 890 apply (rule beq [rule_format, symmetric]) 891 apply simp 892 apply simp 893 apply simp 894 done 895 896lemma call_ceqv': 897 assumes ieq: "\<And>t. rewrite_xf xf t v i i'" 898 and ceqv: "\<And>t t' s'. ceqv \<Gamma> xf v (r t s') t' (c t s') (c' t s')" (* For record field updates *) 899 and xf: "\<And>t t'. xf t = v \<Longrightarrow> xf (r t t') = v" 900 shows "ceqv \<Gamma> xf v t t' (call i f r c) (call i' f r c')" 901 apply (rule ceqvI) 902 apply (rule iffI) 903 apply (erule exec_call_Normal_elim) 904 apply (drule ceqvD1 [OF _ _ ceqv]) 905 apply (simp add: xf) 906 apply (erule exec_call) 907 apply (simp add: rewrite_xfD [OF ieq]) 908 apply assumption 909 apply (clarsimp simp: rewrite_xfD [OF ieq] elim!: exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined) 910 apply (clarsimp simp: rewrite_xfD [OF ieq] elim!: exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined) 911 apply (clarsimp simp: rewrite_xfD [OF ieq] elim!: exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined) 912 apply (clarsimp simp: rewrite_xfD [OF ieq] elim!: exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined) 913 (* clag *) 914 apply (erule exec_call_Normal_elim) 915 apply (drule ceqvD2 [OF _ _ ceqv]) 916 apply (simp add: xf) 917 apply (erule exec_call) 918 apply (simp add: rewrite_xfD [OF ieq]) 919 apply assumption 920 apply (clarsimp simp: rewrite_xfD [OF ieq, symmetric] 921 elim!: exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined)+ 922 done 923 924lemma call_ceqv: 925 assumes ieq: "\<And>t. rewrite_xf xf t v i i'" 926 and ceqv: "\<And>t t' s'. ceqv \<Gamma> xf v (r t s') t' (c t s') (c' t s')" (* For record field updates *) 927 and xf: "\<And>t t'. xf (r t t') = xf t" 928 shows "ceqv \<Gamma> xf v t t' (call i f r c) (call i' f r c')" 929 by (rule call_ceqv' [OF ieq ceqv], simp add: xf) 930 931lemmas Skip_ceqv = ceqv_refl [where c = Skip] 932 933lemma Catch_ceqv: 934 assumes ca: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'" 935 and cb: "\<And>t t'. ceqv \<Gamma> xf v t t' b b'" 936 and xp: "xpres xf v \<Gamma> a" 937 shows "ceqv \<Gamma> xf v t t' (Catch a b) (Catch a' b')" 938 apply (rule ceqvI) 939 apply rule 940 apply (erule exec_Normal_elim_cases) 941 apply (drule (1) ceqvD1 [OF _ _ ca]) 942 apply (rule exec.CatchMatch, assumption) 943 apply (erule ceqvD1 [OF _ _ cb]) 944 apply (erule (1) xpres_abruptD [OF _ xpres_ceqv [OF xp ca]]) 945 apply (rule exec.CatchMiss) 946 apply (erule (1) ceqvD1 [OF _ _ ca]) 947 apply assumption 948 (* clag *) 949 apply (erule exec_Normal_elim_cases) 950 apply (drule (1) ceqvD2 [OF _ _ ca]) 951 apply (rule exec.CatchMatch, assumption) 952 apply (erule ceqvD2 [OF _ _ cb]) 953 apply (erule xpres_abruptD [where xf = xf]) 954 apply (rule xp) 955 apply assumption 956 apply (rule exec.CatchMiss) 957 apply (erule (1) ceqvD2 [OF _ _ ca]) 958 apply assumption 959 done 960 961lemma Cond_ceqv: 962 assumes be: "\<And>t. xf t = v \<longrightarrow> (t \<in> x) = (t \<in> x')" 963 and ca: "ceqv \<Gamma> xf v t t' a a'" 964 and cb: "ceqv \<Gamma> xf v t t' b b'" 965 shows "ceqv \<Gamma> xf v t t' (Cond x a b) (Cond x' a' b')" 966 apply (rule ceqvI) 967 apply rule 968 apply (erule exec_Normal_elim_cases) 969 apply (frule (1) iffD1 [OF be [rule_format]]) 970 apply (erule exec.CondTrue) 971 apply (erule (1) ceqvD1 [OF _ _ ca]) 972 apply (subst (asm) be) 973 apply assumption 974 apply (erule exec.CondFalse) 975 apply (erule (1) ceqvD1 [OF _ _ cb]) 976 (* clag *) 977 apply (erule exec_Normal_elim_cases) 978 apply (frule (1) iffD2 [OF be [ rule_format]]) 979 apply (erule exec.CondTrue) 980 apply (erule (1) ceqvD2 [OF _ _ ca]) 981 apply (subst (asm) be [rule_format, symmetric]) 982 apply assumption 983 apply (erule exec.CondFalse) 984 apply (erule (1) ceqvD2 [OF _ _ cb]) 985 done 986 987lemmas Throw_ceqv = ceqv_refl [where c = Throw] 988 989lemma Collect_mem_eqv: 990 "rewrite_xf xf t v Q Q' \<Longrightarrow> xf t = v \<longrightarrow> (t \<in> Collect Q) = (t \<in> Collect Q')" 991 apply (rule impI) 992 apply (drule (1) rewrite_xfD) 993 apply simp 994 done 995 996(* We could just use ceqv_refl at the end, but I want to catch missed cases. 997 I also assume that While and Cond have {s. P s} as conditionals. 998 The WhileAnnot case is a consequence of While. 999 *) 1000 1001lemma UNIV_mem_eqv: 1002 "xf t = v \<longrightarrow> (t \<in> UNIV) = (t \<in> UNIV)" 1003 by simp 1004 1005lemma empty_mem_eqv: 1006 "xf t = v \<longrightarrow> (t \<in> {}) = (t \<in> {})" 1007 by simp 1008 1009lemma creturn_ceqv_xf: 1010 fixes \<Gamma> :: "(('a globals_scheme, 'b) myvars_scheme) c_body" 1011 assumes xfg: "\<And>s f. xf (global_exn_var_'_update f s) = xf s" 1012 and xfxfu: "\<And>v s. xf (xfu (\<lambda>_. v) s) = v" 1013 shows "ceqv \<Gamma> xf v t t' (return_C xfu xf) (return_C xfu (\<lambda>_. v))" 1014 unfolding creturn_def 1015 apply (rule Seq_ceqv)+ 1016 apply (rule Basic_ceqv) 1017 apply (rule rewrite_xfI) 1018 apply simp 1019 apply (rule Seq_ceqv) 1020 apply (rule Basic_ceqv) 1021 apply (simp add: rewrite_xf_def) 1022 apply (rule Throw_ceqv) 1023 apply (rule xpres_basic) 1024 apply simp 1025 apply (simp add: xfg) 1026 apply (rule xpres_basic) 1027 apply (simp add: xfxfu) 1028 done 1029 1030lemma creturn_ceqv_not_xf: 1031 fixes \<Gamma> :: "(('a globals_scheme, 'b) myvars_scheme) c_body" 1032 assumes rl: "\<And>t. rewrite_xf xf t v rv rv'" 1033 and xfu: "\<And>s f. xf (xfu' f s) = xf s" \<comment> \<open>i.e., xf is independent of xfu\<close> 1034 and xfg: "\<And>s f. xf (global_exn_var_'_update f s) = xf s" 1035 shows "ceqv \<Gamma> xf v t t' (return_C xfu' rv) (return_C xfu' rv')" 1036 unfolding creturn_def 1037 apply (rule Seq_ceqv)+ 1038 apply (rule Basic_ceqv) 1039 apply (rule rewrite_xfI) 1040 apply (simp add: rewrite_xfD [OF rl] xfu) 1041 apply (rule Seq_ceqv) 1042 apply (rule Basic_ceqv) 1043 apply (simp add: rewrite_xf_def) 1044 apply (rule Throw_ceqv) 1045 apply (rule xpres_basic) 1046 apply (simp add: xfg) 1047 apply (rule xpres_basic) 1048 apply (simp add: xfu) 1049 done 1050 1051lemma Guard_ceqv: 1052 assumes be: "\<And>t. xf t = v \<longrightarrow> (t \<in> x) = (t \<in> x')" 1053 and ca: "ceqv \<Gamma> xf v t t' a a'" 1054 shows "ceqv \<Gamma> xf v t t' (Guard f x a) (Guard f x' a')" 1055 apply (rule ceqvI) 1056 apply rule 1057 apply (erule exec_Normal_elim_cases) 1058 apply (frule (1) iffD1 [OF be [rule_format]]) 1059 apply (erule exec.Guard) 1060 apply (erule (1) ceqvD1 [OF _ _ ca]) 1061 apply (subst (asm) be) 1062 apply assumption 1063 apply simp 1064 apply (erule exec.GuardFault) 1065 apply (erule exec_Normal_elim_cases) 1066 apply (frule (1) iffD2 [OF be [rule_format]]) 1067 apply (erule exec.Guard) 1068 apply (erule (1) ceqvD2 [OF _ _ ca]) 1069 apply (subst (asm) be [rule_format, symmetric]) 1070 apply assumption 1071 apply simp 1072 apply (erule exec.GuardFault) 1073 done 1074 1075lemma Cond_UNIV_ceqv: (* Crops up occasionally *) 1076 assumes ca: "ceqv \<Gamma> xf v t t' a a'" 1077 shows "ceqv \<Gamma> xf v t t' (Cond UNIV a b) a'" 1078 using ca 1079 apply - 1080 apply (rule ceqvI) 1081 apply (auto elim!: exec_Normal_elim_cases dest: ceqvD1 ceqvD2 intro: exec.intros) 1082 done 1083 1084lemma Cond_empty_ceqv: (* Crops up occasionally *) 1085 assumes ca: "ceqv \<Gamma> xf v t t' b b'" 1086 shows "ceqv \<Gamma> xf v t t' (Cond {} a b) b'" 1087 using ca 1088 apply - 1089 apply (rule ceqvI) 1090 apply (auto elim!: exec_Normal_elim_cases dest: ceqvD1 ceqvD2 intro: exec.intros) 1091 done 1092 1093lemmas Guard_UNIV_ceqv = Guard_ceqv [where x = UNIV and x' = UNIV, simplified] 1094 1095lemmas ceqv_rules = ceqv_refl [where xf' = xfdc] \<comment> \<open>Any ceqv with xfdc should be ignored\<close> 1096 While_ceqv [OF Collect_mem_eqv] While_ceqv [OF UNIV_mem_eqv] 1097 Cond_ceqv [OF Collect_mem_eqv] Cond_UNIV_ceqv Cond_empty_ceqv 1098 Guard_ceqv [OF Collect_mem_eqv] Guard_UNIV_ceqv 1099 Seq_ceqv Seq_weak_ceqv 1100 Basic_ceqv call_ceqv Skip_ceqv 1101 Catch_ceqv Throw_ceqv 1102 creturn_ceqv_xf creturn_ceqv_not_xf \<comment> \<open>order is important with these two, the second is more general\<close> 1103 ceqv_refl [where c = return_void_C] ceqv_refl [where c = break_C] 1104 ceqv_refl [where c = catchbrk_C] 1105 1106definition 1107 ceqv_xpres :: "('p \<rightharpoonup> ('s, 'p, 'x) com) \<Rightarrow> ('s \<Rightarrow> 'a) \<Rightarrow> 'a 1108 \<Rightarrow> bool \<Rightarrow> ('s, 'p, 'x) com \<Rightarrow> bool \<Rightarrow> ('s, 'p, 'x) com \<Rightarrow> bool" 1109where 1110 "ceqv_xpres \<Gamma> xf v pres c pres' c' 1111 \<equiv> \<forall>s s' s''. (pres \<longrightarrow> xf s = v) 1112 \<longrightarrow> (\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s' = \<Gamma> \<turnstile> \<langle>c', Normal s\<rangle> \<Rightarrow> s') 1113 \<and> (\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> s' \<and> (s' = Normal s'' \<or> s' = Abrupt s'') \<and> pres' 1114 \<longrightarrow> xf s'' = v) 1115 \<and> (\<not> pres \<longrightarrow> \<not> pres' \<and> c = c')" 1116 1117definition 1118 ceqv_xpres_rewrite_set :: "('s \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 's set \<Rightarrow> 's set \<Rightarrow> bool" where 1119 "ceqv_xpres_rewrite_set xf v S S' 1120 \<equiv> \<forall>s. xf s = v \<longrightarrow> (s \<in> S) = (s \<in> S')" 1121 1122definition 1123 ceqv_xpres_rewrite_basic :: "('s \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('s \<Rightarrow> 't) \<Rightarrow> ('s \<Rightarrow> 't) \<Rightarrow> bool" where 1124 "ceqv_xpres_rewrite_basic xf v f f' 1125 \<equiv> \<forall>s. xf s = v \<longrightarrow> f s = f' s" 1126 1127definition 1128 ceqv_xpres_basic_preserves :: "('s \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('s \<Rightarrow> 's) \<Rightarrow> bool \<Rightarrow> bool" where 1129 "ceqv_xpres_basic_preserves xf v f b 1130 \<equiv> b \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f s) = v)" 1131 1132definition 1133 ceqv_xpres_eq_If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where 1134 "ceqv_xpres_eq_If b x y z \<equiv> z = (if b then x else y)" 1135 1136definition 1137 ceqv_xpres_call_restore_args :: "'a \<Rightarrow> ('s \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> 's) \<Rightarrow> bool" 1138where 1139 "ceqv_xpres_call_restore_args x f g = (f = g)" 1140 1141lemma ceqv_xpres_eq_both: 1142 "ceqv_xpres \<Gamma> xf v True c True c' 1143 = ((\<forall>t t'. ceqv \<Gamma> xf v t t' c c') \<and> xpres xf v \<Gamma> c')" 1144 apply (simp add: ceqv_xpres_def ceqv_def xpres_def) 1145 apply blast 1146 done 1147 1148lemma ceqv_xpres_eq_ceqv: 1149 "ceqv_xpres \<Gamma> xf v True c False c' 1150 = (\<forall> t t'. ceqv \<Gamma> xf v t t' c c')" 1151 by (simp add: ceqv_xpres_def ceqv_def) 1152 1153lemma ceqv_xpres_eq_imp: 1154 "ceqv_xpres \<Gamma> xf v True c pres c' 1155 = ((\<forall>t t'. ceqv \<Gamma> xf v t t' c c') \<and> (pres \<longrightarrow> xpres xf v \<Gamma> c'))" 1156 by (cases pres, simp_all add: ceqv_xpres_eq_ceqv ceqv_xpres_eq_both) 1157 1158lemma ceqv_xpres_False: 1159 "ceqv_xpres \<Gamma> xf v False c pres c' = (\<not> pres \<and> c = c')" 1160 by (auto simp add: ceqv_xpres_def) 1161 1162lemma ceqv_xpres_eq_If_False: 1163 "ceqv_xpres_eq_If P Q False R = (R = (P \<and> Q))" 1164 by (simp add: ceqv_xpres_eq_If_def) 1165 1166lemma ceqv_xpres_False_pres: 1167 "ceqv_xpres \<Gamma> xf v False c False c" 1168 by (simp add: ceqv_xpres_def) 1169 1170lemma ceqv_xpres_xfdc: 1171 "ceqv_xpres \<Gamma> xfdc v pres c pres c" 1172 by (simp add: ceqv_xpres_def xfdc_def) 1173 1174lemma ceqv_xpres_call_restore_argsI: 1175 "\<forall> s. f s = g s \<Longrightarrow> ceqv_xpres_call_restore_args i f g" 1176 by (simp add: ceqv_xpres_call_restore_args_def fun_eq_iff) 1177 1178lemma ceqv_xpres_whileAnno: 1179 "\<lbrakk> ceqv_xpres \<Gamma> xf v True c pres c'; ceqv_xpres_rewrite_set xf v S S'; 1180 ceqv_xpres_eq_If pres c' c c''; ceqv_xpres_eq_If pres S' S S'' \<rbrakk> 1181 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (whileAnno S I V c) pres (whileAnno S'' I V c'')" 1182 apply (cases pres) 1183 apply (clarsimp simp add: ceqv_xpres_eq_both ceqv_xpres_eq_If_def 1184 whileAnno_def) 1185 apply (intro conjI allI) 1186 apply (rule While_ceqv) 1187 apply (simp add: ceqv_xpres_rewrite_set_def) 1188 apply simp 1189 apply (erule xpres_ceqv) 1190 apply (rule ceqv_sym, simp) 1191 apply (erule xpres_while) 1192 apply (simp add: ceqv_xpres_def ceqv_xpres_eq_If_def) 1193 done 1194 1195lemmas ceqv_xpres_While = ceqv_xpres_whileAnno[unfolded whileAnno_def] 1196 1197lemma ceqv_xpres_Cond: 1198 "\<lbrakk> ceqv_xpres_rewrite_set xf v S S'; ceqv_xpres \<Gamma> xf v True c cpres c'; 1199 ceqv_xpres \<Gamma> xf v True d dpres d'; ceqv_xpres_eq_If dpres cpres False pres \<rbrakk> 1200 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (Cond S c d) pres (Cond S' c' d')" 1201 apply (clarsimp simp add: ceqv_xpres_eq_imp ceqv_xpres_eq_If_False) 1202 apply (intro allI conjI impI) 1203 apply (rule Cond_ceqv) 1204 apply (simp add: ceqv_xpres_rewrite_set_def) 1205 apply simp 1206 apply simp 1207 apply simp 1208 apply (erule(1) xpres_cond) 1209 done 1210 1211lemma ceqv_xpres_Guard: 1212 "\<lbrakk> ceqv_xpres_rewrite_set xf v S S'; ceqv_xpres \<Gamma> xf v True c pres c' \<rbrakk> 1213 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (Guard g S c) pres (Guard g S' c')" 1214 apply (clarsimp simp: ceqv_xpres_eq_imp xpres_guard) 1215 apply (rule Guard_ceqv) 1216 apply (simp add: ceqv_xpres_rewrite_set_def) 1217 apply simp 1218 done 1219 1220lemma ceqv_xpres_Seq: 1221 "\<lbrakk> ceqv_xpres \<Gamma> xf v True c cpres c'; ceqv_xpres \<Gamma> xf v cpres d pres d' \<rbrakk> 1222 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (c ;; d) pres (c' ;; d')" 1223 apply (cases cpres) 1224 apply (clarsimp simp add: ceqv_xpres_eq_imp xpres_seq) 1225 apply (rule Seq_ceqv, simp+) 1226 apply (erule xpres_ceqv) 1227 apply (rule ceqv_sym, simp) 1228 apply (clarsimp simp add: ceqv_xpres_eq_imp ceqv_xpres_False) 1229 apply (rule Seq_weak_ceqv, simp) 1230 done 1231 1232lemma ceqv_xpres_Basic: 1233 "\<lbrakk> ceqv_xpres_rewrite_basic xf v f f'; 1234 ceqv_xpres_basic_preserves xf v f' pres \<rbrakk> 1235 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (Basic f) pres (Basic f')" 1236 apply (simp add: ceqv_xpres_eq_imp) 1237 apply (intro allI impI conjI) 1238 apply (rule Basic_ceqv) 1239 apply (simp add: rewrite_xf_def ceqv_xpres_rewrite_basic_def) 1240 apply (rule xpres_basic) 1241 apply (simp add: ceqv_xpres_basic_preserves_def) 1242 done 1243 1244lemma ceqv_xpres_call: 1245 "\<lbrakk> ceqv_xpres_call_restore_args f i i'; 1246 ceqv_xpres_rewrite_basic xf v i' i''; 1247 \<And>s'. ceqv_xpres_basic_preserves xf v (\<lambda>s. r s s') pres'; 1248 \<And>s' s''. ceqv_xpres \<Gamma> xf v pres' (c s' s'') pres (c' s' s'') \<rbrakk> 1249 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (call i f r c) pres (call i'' f r c')" 1250 apply (simp add: ceqv_xpres_eq_imp ceqv_xpres_call_restore_args_def) 1251 apply (intro allI conjI impI) 1252 defer 1253 apply (cases pres') 1254 apply (rule xpres_call) 1255 apply (simp add: ceqv_xpres_basic_preserves_def) 1256 apply (simp add: ceqv_xpres_eq_imp) 1257 apply (simp add: ceqv_xpres_False) 1258 apply (cases pres') 1259 apply (clarsimp simp add: ceqv_xpres_eq_imp) 1260 apply (rule call_ceqv') 1261 apply (simp add: rewrite_xf_def ceqv_xpres_rewrite_basic_def) 1262 apply simp 1263 apply (simp add: ceqv_xpres_basic_preserves_def) 1264 apply (simp add: ceqv_xpres_False) 1265 apply (clarsimp simp add: ceqv_def ceqv_xpres_rewrite_basic_def) 1266 apply (auto elim!: exec_call_Normal_elim exec_call 1267 exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined) 1268 done 1269 1270lemma ceqv_xpres_Skip: 1271 "ceqv_xpres \<Gamma> xf v True Skip True Skip" 1272 by (simp add: ceqv_xpres_eq_imp Skip_ceqv xpres_skip) 1273 1274lemma ceqv_xpres_Catch: 1275 "\<lbrakk> ceqv_xpres \<Gamma> xf v True c pres c'; ceqv_xpres \<Gamma> xf v pres h pres' h' \<rbrakk> 1276 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (Catch c h) pres' (Catch c' h')" 1277 apply (cases pres) 1278 apply (clarsimp simp add: ceqv_xpres_eq_imp xpres_catch) 1279 apply (rule Catch_ceqv) 1280 apply simp 1281 apply simp 1282 apply (erule xpres_ceqv) 1283 apply (rule ceqv_sym, simp) 1284 apply (clarsimp simp add: ceqv_xpres_False ceqv_xpres_eq_imp) 1285 apply (clarsimp simp: ceqv_def) 1286 apply (auto elim!: exec_Normal_elim_cases 1287 intro: exec.intros) 1288 done 1289 1290lemma ceqv_xpres_Throw: 1291 "ceqv_xpres \<Gamma> xf v True Throw True Throw" 1292 by (simp add: ceqv_xpres_eq_imp Throw_ceqv xpres_throw) 1293 1294lemma exec_Basic_Seq: 1295 "\<Gamma> \<turnstile> \<langle>Basic f ;; c, Normal s\<rangle> \<Rightarrow> s' 1296 = \<Gamma> \<turnstile> \<langle>c, Normal (f s)\<rangle> \<Rightarrow> s'" 1297 by (auto elim: exec_elim_cases intro: exec.Basic exec.Seq) 1298 1299lemma exec_Basic_Seq_Basic: 1300 "\<Gamma>\<turnstile> \<langle>Basic f;; Basic g, x\<rangle> \<Rightarrow> y = \<Gamma>\<turnstile> \<langle>Basic (g \<circ> f), x\<rangle> \<Rightarrow> y" 1301 by (auto simp: o_def elim: exec_elim_cases intro: exec.Basic exec.Seq) 1302 1303lemma ceqv_xpres_return_C: 1304 "\<lbrakk> ceqv_xpres_rewrite_basic xf v qf qf'; 1305 \<And>f. ceqv_xpres_basic_preserves xf v (xfu f) pres'; 1306 \<And>f. ceqv_xpres_basic_preserves xf v 1307 (global_exn_var_'_update f) pres''; 1308 ceqv_xpres_eq_If pres' pres'' False pres \<rbrakk> 1309 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (return_C xfu qf) pres (return_C xfu qf')" 1310 apply (simp add: ceqv_xpres_def ceqv_xpres_rewrite_basic_def 1311 ceqv_xpres_basic_preserves_def creturn_def 1312 ceqv_xpres_eq_If_False) 1313 apply (auto elim!: exec_elim_cases simp: exec_Basic_Seq) 1314 done 1315 1316lemma ceqv_xpres_C_bits: 1317 "\<lbrakk> \<And>f. ceqv_xpres_basic_preserves xf v 1318 (global_exn_var_'_update f) pres \<rbrakk> 1319 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True return_void_C pres return_void_C" 1320 "\<lbrakk> \<And>f. ceqv_xpres_basic_preserves xf v 1321 (global_exn_var_'_update f) pres \<rbrakk> 1322 \<Longrightarrow> ceqv_xpres \<Gamma> xf v True break_C pres break_C" 1323 "ceqv_xpres \<Gamma> xf v True catchbrk_C True catchbrk_C" 1324 by (auto simp: ceqv_xpres_def 1325 return_void_C_def cbreak_def 1326 catchbrk_C_def 1327 ceqv_xpres_basic_preserves_def 1328 elim!: exec_elim_cases) 1329 1330definition 1331 "ceqv_xpres_lvar_nondet_init xf v_upd pres \<equiv> pres \<longrightarrow> (\<forall>s v. xf (v_upd (\<lambda>_. v) s) = xf s)" 1332 1333lemma ceqv_xpres_lvar_nondet_init: 1334 "ceqv_xpres_lvar_nondet_init xf v_upd pres \<Longrightarrow> 1335 ceqv_xpres \<Gamma> xf v True (lvar_nondet_init v_acc v_upd) pres (lvar_nondet_init v_acc v_upd)" 1336 apply (clarsimp simp: ceqv_xpres_def lvar_nondet_init_def) 1337 apply (erule exec.cases, simp_all) 1338 apply (clarsimp simp: ceqv_xpres_lvar_nondet_init_def) 1339 done 1340 1341lemmas ceqv_xpres_rules = 1342 ceqv_xpres_False_pres ceqv_xpres_xfdc ceqv_xpres_whileAnno 1343 ceqv_xpres_While ceqv_xpres_Cond ceqv_xpres_Guard ceqv_xpres_Seq 1344 ceqv_xpres_lvar_nondet_init ceqv_xpres_Basic ceqv_xpres_call 1345 ceqv_xpres_Skip ceqv_xpres_Catch ceqv_xpres_Throw ceqv_xpres_return_C 1346 ceqv_xpres_C_bits 1347 1348lemma ceqv_xpres_FalseI: 1349 "ceqv_xpres \<Gamma> xf v pres c False c" 1350 by (simp add: ceqv_xpres_def) 1351 1352lemma ceqv_xpres_ceqvI: 1353 "ceqv_xpres \<Gamma> xf v True c pres c' \<Longrightarrow> ceqv \<Gamma> xf v t t' c c'" 1354 by (simp add: ceqv_xpres_eq_imp) 1355 1356lemma ceqv_xpres_rewrite_basic_left_cong: 1357 "\<lbrakk> \<And>s. xf s = v \<Longrightarrow> f s = f'' s \<rbrakk> 1358 \<Longrightarrow> ceqv_xpres_rewrite_basic xf v f f' 1359 = ceqv_xpres_rewrite_basic xf v f'' f'" 1360 by (simp add: ceqv_xpres_rewrite_basic_def) 1361 1362lemma ceqv_xpres_rewrite_basic_refl: 1363 "ceqv_xpres_rewrite_basic xf v f f" 1364 by (simp add: ceqv_xpres_rewrite_basic_def) 1365 1366lemma ceqv_xpres_basic_preserves_TrueI: 1367 "\<lbrakk> \<And>s. xf s = v \<longrightarrow> xf (f s) = v \<rbrakk> \<Longrightarrow> ceqv_xpres_basic_preserves xf v f True" 1368 by (simp add: ceqv_xpres_basic_preserves_def) 1369 1370lemma ceqv_xpres_basic_preserves_FalseI: 1371 "ceqv_xpres_basic_preserves xf v f False" 1372 by (simp add: ceqv_xpres_basic_preserves_def) 1373 1374lemma ceqv_xpres_lvar_nondet_init_TrueI: 1375 "(\<And>s v. xf (v_upd (\<lambda>_. v) s) = xf s) \<Longrightarrow> ceqv_xpres_lvar_nondet_init xf v_upd True" 1376 by (simp add: ceqv_xpres_lvar_nondet_init_def) 1377 1378lemma ceqv_xpres_lvar_nondet_init_FalseI: 1379 "ceqv_xpres_lvar_nondet_init xf v_upd False" 1380 by (simp add: ceqv_xpres_lvar_nondet_init_def) 1381 1382lemma ceqv_xpres_rewrite_set_rules: 1383 "ceqv_xpres_rewrite_basic xf v P P' 1384 \<Longrightarrow> ceqv_xpres_rewrite_set xf v {s. P s} {s. P' s}" 1385 "ceqv_xpres_rewrite_set xf v UNIV UNIV" 1386 "ceqv_xpres_rewrite_set xf v {} {}" 1387 "\<lbrakk> ceqv_xpres_rewrite_set xf v S S''; ceqv_xpres_rewrite_set xf v S' S''' \<rbrakk> 1388 \<Longrightarrow> ceqv_xpres_rewrite_set xf v (if G then S else S') (if G then S'' else S''')" 1389 by (simp_all add: ceqv_xpres_rewrite_set_def ceqv_xpres_rewrite_basic_def 1390 split: if_split) 1391 1392lemma ceqv_xpres_eq_If_rules: 1393 "ceqv_xpres_eq_If False x y y" 1394 "ceqv_xpres_eq_If True x y x" 1395 by (simp add: ceqv_xpres_eq_If_def)+ 1396 1397definition 1398 "simpl_sequence f xs 1399 = foldr (Seq) (map f xs) Skip" 1400 1401lemma simpl_sequence_Cons: 1402 "simpl_sequence f (x # xs) = Seq (f x) (simpl_sequence f xs)" 1403 by (simp add: simpl_sequence_def) 1404 1405fun(sequential) 1406 simpl_final_basic_opts :: "('s, 'p, 'x) com \<Rightarrow> ('s \<Rightarrow> 's) option" 1407where 1408 "simpl_final_basic_opts (x ;; y) 1409 = (case (simpl_final_basic_opts y) of None \<Rightarrow> simpl_final_basic_opts x 1410 | Some v \<Rightarrow> Some v)" 1411 | "simpl_final_basic_opts (Basic f) = Some f" 1412 | "simpl_final_basic_opts (Guard E F c) = simpl_final_basic_opts c" 1413 | "simpl_final_basic_opts Skip = None" 1414 | "simpl_final_basic_opts Throw = None" 1415 | "simpl_final_basic_opts c = Some id" 1416 1417definition 1418 "simpl_final_basic c = (case simpl_final_basic_opts c 1419 of Some v \<Rightarrow> v | None \<Rightarrow> id)" 1420 1421lemmas simpl_final_basic_simps[simp] 1422 = simpl_final_basic_def[where c="Seq c c'" for c c'] 1423 simpl_final_basic_def[where c="Basic f" for f] 1424 simpl_final_basic_def[where c="Guard E F c" for E F c] 1425 1426lemma simpl_final_basic_opts_exec[OF _ refl refl]: 1427 "\<Gamma> \<turnstile> \<langle>c, xs\<rangle> \<Rightarrow> xs' \<Longrightarrow> xs = Normal t \<Longrightarrow> xs' = Normal t' 1428 \<Longrightarrow> (case simpl_final_basic_opts c of None \<Rightarrow> t' = t 1429 | Some f \<Rightarrow> \<exists>s. t' = f s)" 1430 apply (induct arbitrary: t t' rule: exec.induct, simp_all) 1431 apply metis 1432 apply atomize 1433 apply clarsimp 1434 apply (case_tac s') 1435 apply (auto split: option.split_asm)[1] 1436 apply (auto elim!: exec_elim_cases) 1437 done 1438 1439lemma simpl_final_basic_exec: 1440 "\<Gamma> \<turnstile> \<langle>c, Normal t\<rangle> \<Rightarrow> Normal t' 1441 \<Longrightarrow> \<exists>s. t' = simpl_final_basic c s" 1442 apply (frule simpl_final_basic_opts_exec) 1443 apply (simp add: simpl_final_basic_def split: option.split_asm) 1444 done 1445 1446lemma ceqv_xpres_to_simpl_sequence: 1447 fixes v :: "'a :: ring_1" 1448 assumes c: "\<And>v. ceqv_xpres \<Gamma> xf' v True c pres (c' v)" 1449 and v: "\<And>v s. xf' (simpl_final_basic (c' v) s) - v = offs" 1450 shows "\<not> CP (v + of_nat n * offs) 1451 \<Longrightarrow> ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False 1452 (simpl_sequence c' (takeWhile CP (map (\<lambda>x. v + of_nat x * offs) [0 ..< n])))" 1453 (is "_ \<Longrightarrow> ceqv_xpres _ _ _ _ (While ?S _) _ _") 1454proof (induct n arbitrary: v) 1455 case 0 1456 show ?case using c[where v=v] 0 1457 apply (simp add: simpl_sequence_def) 1458 apply (simp add: ceqv_xpres_eq_imp ceqv_def) 1459 apply (auto elim!: exec_Normal_elim_cases intro: exec.intros)[1] 1460 done 1461next 1462 case (Suc n) 1463 have foo: "\<And>t t'. (\<Gamma> \<turnstile> \<langle>c' v, Normal t\<rangle> \<Rightarrow> Normal t') \<longrightarrow> xf' t' = v + offs" 1464 using v 1465 by (clarsimp simp: field_simps dest!: simpl_final_basic_exec) 1466 1467 show ?case using c[where v=v] Suc.hyps[where v="v + offs"] Suc.prems 1468 apply (subst upt_conv_Cons, simp) 1469 apply (simp only: map_Suc_upt[symmetric] list.simps) 1470 apply (cases "CP v") 1471 apply (simp add: o_def field_simps simpl_sequence_Cons 1472 ceqv_xpres_eq_imp) 1473 apply (clarsimp, rule ceqv_trans[where c'="c ;; While ?S c"]) 1474 apply (simp add: ceqv_def) 1475 apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq exec.WhileTrue)[1] 1476 apply (rule ceqv_trans[where c'="c' v ;; While ?S c"]) 1477 apply (simp add: ceqv_def) 1478 apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq)[1] 1479 apply (simp add: ceqv_def) 1480 apply (intro impI exec_Seq_cong refl) 1481 apply (simp add: foo) 1482 apply (simp add: simpl_sequence_def field_simps) 1483 apply (simp add: ceqv_xpres_eq_imp ceqv_def) 1484 apply (auto intro: exec.WhileFalse exec.Skip elim!: exec_Normal_elim_cases)[1] 1485 done 1486qed 1487 1488lemma ceqv_xpres_While_simpl_sequence: 1489 fixes v :: "'a :: ring_1" 1490 assumes c: "\<And>v. ceqv_xpres \<Gamma> xf' v True c pres (c' v)" 1491 shows "ceqv_xpres \<Gamma> xf' v True (While {s. CP (xf' s)} c) False 1492 (if \<exists>n offs. (\<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs)) \<and> \<not> CP (v + of_nat n * offs) 1493 then simpl_sequence c' (map (\<lambda>x. v + of_nat x 1494 * (THE offs. \<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs))) 1495 [0 ..< (LEAST n. \<not> CP (v + of_nat n 1496 * (THE offs. \<forall>s v. (xf' (simpl_final_basic (c' v) s) - v = offs))))]) 1497 else While {s. CP (xf' s)} c)" 1498 apply (split if_split, simp add: ceqv_xpres_def[where c=c and c'=c for c]) 1499 apply (clarsimp simp: ceqv_xpres_eq_ceqv) 1500 apply (rule ceqv_trans) 1501 apply (rule_tac n="LEAST n. \<not> CP (v + of_nat n * offs)" 1502 in ceqv_xpres_to_simpl_sequence[simplified ceqv_xpres_eq_ceqv, rule_format]) 1503 apply (rule c) 1504 apply simp 1505 apply simp 1506 apply (rule LeastI_ex) 1507 apply blast 1508 apply (subst takeWhile_eq_all_conv[THEN iffD2]) 1509 apply (clarsimp dest!: not_less_Least) 1510 apply (simp add: ceqv_def) 1511 done 1512 1513lemma ccorres_underlying_name_seq_bound: 1514 "(\<not> CP n \<and> (\<forall>n' < n. CP n')) 1515 \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m 1516 (simpl_sequence c' (map f [0 ..< n])) 1517 \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf 1518 G G' hs m (if \<exists>n. \<not> CP n 1519 then simpl_sequence c' (map f [0 ..< (LEAST n. \<not> CP n)]) 1520 else c)" 1521 apply (subst if_P, blast) 1522 apply (subst Least_equality[where x=n], simp_all) 1523 apply (rule ccontr, simp add: linorder_not_le) 1524 done 1525 1526lemma sequenceE_simpl_sequence_nth_corres': 1527 "\<lbrakk> length xs = length ys; 1528 \<And>zs. length zs < length xs \<Longrightarrow> 1529 ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (prev_xs @ zs @ [rv]) rv')) xf' 1530 (inl_rrel arrel) axf 1531 (P and F (length prev_xs + length zs)) (Q \<inter> {s. r' (prev_xs @ zs) (xf' s)}) hs 1532 (xs ! length zs) (f (ys ! length zs)); 1533 \<And>s \<sigma>. s \<in> Q \<Longrightarrow> P \<sigma> \<Longrightarrow> 1534 (\<sigma>, s) \<in> sr \<Longrightarrow> \<forall>y \<in> set ys. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} (f y) Q,UNIV; 1535 \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F (length prev_xs + n)\<rbrace> xs ! n \<lbrace>\<lambda>_. P and F (length prev_xs + Suc n)\<rbrace>, - 1536 \<rbrakk> 1537 \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (prev_xs @ rv) rv')) xf' 1538 (inl_rrel arrel) axf 1539 (\<lambda>s. xs \<noteq> [] \<longrightarrow> P s \<and> F (length prev_xs) s) (Q \<inter> {s. r' prev_xs (xf' s)}) hs 1540 (sequenceE xs) 1541 (simpl_sequence f ys)" 1542proof (induct xs ys arbitrary: prev_xs rule: list_induct2) 1543 case Nil 1544 show ?case 1545 apply (simp add: sequenceE_def simpl_sequence_def) 1546 apply (rule ccorres_guard_imp2, rule ccorres_returnOk_skip) 1547 apply simp 1548 done 1549next 1550 case (Cons x xs y ys) 1551 show ?case 1552 apply (simp add: simpl_sequence_Cons sequenceE_Cons) 1553 apply (rule ccorres_guard_imp2) 1554 apply (rule ccorres_splitE) 1555 apply (simp add: inl_rrel_inl_rrel) 1556 apply (rule Cons.prems(1)[where zs=Nil, simplified]) 1557 apply (rule ceqv_refl) 1558 apply (simp add: liftME_def[symmetric] liftME_liftM) 1559 apply (rule ccorres_rel_imp2, rule Cons.hyps(2)[where prev_xs="prev_xs @ [rv]" for rv]) 1560 apply (rule ccorres_guard_imp2, rule ccorres_rel_imp2, 1561 rule Cons.prems(1)[where zs="z # zs" for z zs, simplified]) 1562 apply simp+ 1563 apply (blast dest: Cons.prems[simplified]) 1564 apply simp 1565 apply (cut_tac n="Suc n" in Cons.prems(3), simp, simp) 1566 apply (clarsimp elim!: inl_inrE) 1567 apply assumption 1568 apply (clarsimp elim!: inl_inrE) 1569 apply simp 1570 apply (rule hoare_vcg_const_imp_lift_R) 1571 apply (rule hoare_gen_asmE) 1572 apply (erule Cons.prems(3)[where n=0, simplified]) 1573 apply (rule_tac P="Q \<inter> {s. \<exists>\<sigma>. P \<sigma> \<and> (\<sigma>, s) \<in> sr}" 1574 in HoarePartial.conseq_exploit_pre) 1575 apply (clarsimp, rule conseqPost, rule Cons.prems(2)[simplified, THEN conjunct1], 1576 simp+) 1577 apply (clarsimp simp: ccHoarePost_def elim!: inl_inrE) 1578 apply simp 1579 apply auto 1580 done 1581qed 1582 1583lemmas sequenceE_simpl_sequence_nth_corres 1584 = sequenceE_simpl_sequence_nth_corres'[where prev_xs=Nil, simplified] 1585 1586lemma mapME_x_simpl_sequence_fun_related: 1587 "\<lbrakk> ys = map yf xs; 1588 \<And>n x. x \<in> set xs \<Longrightarrow> 1589 ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel arrel) axf 1590 (P and F n (n < length xs) x) Q hs 1591 (f x) (f' (yf x)); 1592 \<And>s \<sigma>. s \<in> Q \<Longrightarrow> P \<sigma> \<Longrightarrow> 1593 (\<sigma>, s) \<in> sr \<Longrightarrow> \<forall>x \<in> set xs. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} (f' (yf x)) Q,UNIV; 1594 \<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>P and F n True (xs ! n)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. P and F (Suc n) (Suc n < length xs) (xs ! Suc n)\<rbrace>, - 1595 \<rbrakk> 1596 \<Longrightarrow> ccorres_underlying sr \<Gamma> (inr_rrel dc) xfdc 1597 (inl_rrel arrel) axf 1598 (P and F 0 (xs \<noteq> []) (xs ! 0)) Q hs 1599 (mapME_x f xs) 1600 (simpl_sequence f' ys)" 1601 apply (simp add: mapME_x_sequenceE liftME_def[symmetric] 1602 liftME_liftM) 1603 apply (rule ccorres_rel_imp2, rule ccorres_guard_imp2, 1604 rule sequenceE_simpl_sequence_nth_corres[where r'=dc and xf'=xfdc 1605 and P=P and F="\<lambda>i. F i (i < length xs) (xs ! i)" and Q=Q and arrel=arrel and axf=axf]; 1606 clarsimp elim!: inl_inrE) 1607 apply (erule_tac x="length zs" in meta_allE 1608 | erule_tac x="xs ! length zs" in meta_allE)+ 1609 apply (simp add: dc_def) 1610 done 1611 1612lemmas mapME_x_simpl_sequence_same 1613 = mapME_x_simpl_sequence_fun_related[where yf=id, simplified] 1614 1615lemma call_ignore_cong: 1616 "call i f g r = call i f g r" by (rule refl) 1617 1618(* These could be done with ML patterns, but this fits in better with tactics *) 1619lemma match_valid: 1620 "NonDetMonad.valid P a P' \<Longrightarrow> NonDetMonad.valid P a P'" . 1621 1622lemma match_validE: 1623 "NonDetMonad.validE P a P' P'' \<Longrightarrow> NonDetMonad.validE P a P' P''" . 1624 1625lemma match_hoare: 1626 "HoarePartialDef.hoarep G T F P C P' A \<Longrightarrow> HoarePartialDef.hoarep G T F P C P' A" . 1627 1628lemma match_all_hoare: 1629 "\<forall>x. HoarePartialDef.hoarep G T F (P x) C (P' x) (A x) \<Longrightarrow> 1630 \<forall>x. HoarePartialDef.hoarep G T F (P x) C (P' x) (A x)" . 1631 1632lemmas ctac_skips = match_valid match_validE match_all_hoare match_hoare 1633 1634lemma match_xpres: 1635 "xpres xf v \<Gamma> c \<Longrightarrow> xpres xf v \<Gamma> c" . 1636 1637lemma match_ceqv: 1638 "ceqv \<Gamma> xf v t t' c c' \<Longrightarrow> ceqv \<Gamma> xf v t t' c c'" . 1639 1640ML_file "ctac-method.ML" 1641 1642setup CtacImpl.setup 1643 1644method_setup ctac = {* CtacImpl.corres_ctac_tactic *} 1645 "Split and rewrite corres rules. Arguments simp (add|del|only), pre (add|del|only), (ccorres) (add|del|only)" 1646 1647method_setup clift = {* CtacImpl.corres_abstract_args *} 1648 "Abstract a local variable into a HOL variable" 1649 1650method_setup cinitlift = {* CtacImpl.corres_abstract_init_args *} 1651 "Abstract a list of local variables into HOL variable without touching the remaining guards" 1652 1653method_setup csymbr = {* CtacImpl.corres_symb_rhs *} 1654 "Symbolically execute the call on the right hand side of corres (see ccorres_lift_rhss). Arguments simp (add|del|only)." 1655 1656method_setup ceqv = {* CtacImpl.corres_ceqv *} 1657 "Solve ceqv goals." 1658 1659(* The true here says to unfold the Haskell side *) 1660method_setup cinit = {* CtacImpl.corres_boilerplate true *} 1661 "Boilerplate tactic for the start of a Call ccorres proof. Arguments 'lift' then 'simp (add|del|only)', e.g. apply (cinit lift: var1_' var2_' simp add: return_bind)" 1662 1663method_setup cinit' = {* CtacImpl.corres_boilerplate false *} 1664 "As for cinit without unfolding the abstract side" 1665 1666(* Debugging *) 1667method_setup ctac_print_xf = {* CtacImpl.corres_print_xf *} 1668 "Print out what ctac thinks is the current xf" 1669 1670(* Set up wpc *) 1671lemma 1672 wpc_helper_ccorres_final: 1673 "ccorres_underlying sr G rv xf arrel axf Q Q' hs f f' 1674 \<Longrightarrow> wpc_helper (P, P') (Q, Q') 1675 (ccorres_underlying sr G rv xf arrel axf P P' hs f f')" 1676 apply (clarsimp simp: wpc_helper_def) 1677 apply (erule ccorres_guard_imp) 1678 apply auto 1679 done 1680 1681wpc_setup "\<lambda>m. ccorres_underlying sr G rv xf arrel axf P P' hs m conc" wpc_helper_ccorres_final 1682wpc_setup "\<lambda>m. ccorres_underlying sr G rv xf arrel axf P P' hs (m >>= a) conc" wpc_helper_ccorres_final 1683 1684context kernel 1685begin 1686 1687(* Set up ctac proof sets. These are tried in reverse order (further down is tried first) *) 1688 1689declare ccorres_Guard [corres_pre] 1690declare ccorres_Guard_Seq [corres_pre] 1691 1692lemma c_guard_field_abs: 1693 fixes p :: "'a :: mem_type ptr" 1694 assumes abs: "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> c_guard p" 1695 shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s 1696 \<and> (P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type)))) 1697 \<longrightarrow> c_guard (Ptr &(p\<rightarrow>f) :: 'b :: mem_type ptr)" 1698 using c_guard_field abs by blast 1699 1700lemma h_t_valid_field_abs: 1701 fixes p :: "'a :: mem_type ptr" 1702 assumes abs: "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> s' \<Turnstile>\<^sub>c p" 1703 shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s 1704 \<and> (P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type)))) 1705 \<longrightarrow> s' \<Turnstile>\<^sub>c (Ptr &(p\<rightarrow>f) :: 'b :: mem_type ptr)" 1706 using h_t_valid_field abs by blast 1707 1708lemmas ccorres_move_c_guard_Seq_field = ccorres_move_Guard_Seq [OF c_guard_field_abs] 1709lemmas ccorres_move_c_guard_field = ccorres_move_Guard [OF c_guard_field_abs] 1710 1711lemma abs_c_guard_from_abs_h_t_valid: 1712 "(\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> s' \<Turnstile>\<^sub>c p) 1713 \<Longrightarrow> (\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> c_guard p)" 1714 by (auto intro: h_t_valid_c_guard) 1715 1716lemmas ccorres_move_c_guards = 1717 ccorres_move_c_guard_Seq_field[OF abs_c_guard_from_abs_h_t_valid] 1718 ccorres_move_Guard_Seq[OF h_t_valid_field_abs] 1719 ccorres_move_Guard_Seq[OF abs_c_guard_from_abs_h_t_valid] 1720 ccorres_move_Guard_Seq 1721 ccorres_move_c_guard_field[OF abs_c_guard_from_abs_h_t_valid] 1722 ccorres_move_Guard[OF h_t_valid_field_abs] 1723 ccorres_move_Guard[OF abs_c_guard_from_abs_h_t_valid] 1724 ccorres_move_Guard 1725 1726lemma h_t_array_valid_array_assertion: 1727 "h_t_array_valid htd ptr n \<Longrightarrow> 0 < n 1728 \<Longrightarrow> array_assertion ptr n htd" 1729 apply (simp add: array_assertion_def) 1730 apply (fastforce intro: exI[where x=0]) 1731 done 1732 1733lemma array_assertion_abs_to_const: 1734 "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' 1735 \<longrightarrow> (Suc 0 = 0 \<or> array_assertion (ptr s s') (n s s') (htd s s')) 1736 \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' 1737 \<longrightarrow> array_assertion (ptr s s') (n s s') (htd s s')" 1738 by simp 1739 1740lemmas ccorres_move_array_assertions 1741 = ccorres_move_Guard_Seq ccorres_move_Guard 1742 ccorres_move_Guard_Seq[OF array_assertion_abs_to_const] 1743 ccorres_move_Guard[OF array_assertion_abs_to_const] 1744 1745lemma ptr_add_assertion_positive_helper: 1746 "n == m \<Longrightarrow> 0 \<le> sint m \<Longrightarrow> 0 \<le> sint n" 1747 by simp 1748 1749lemma cvariable_array_map_const_add_map_option: 1750 "cvariable_array_map_relation m (\<lambda>_. n) 1751 = cvariable_array_map_relation (map_option f o m) (\<lambda>_. n)" 1752 by (simp add: cvariable_array_map_relation_def fun_eq_iff) 1753 1754lemma ccorres_move_const_guard: 1755 "ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m c 1756 \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf 1757 (P and K G) P' hs m (Guard F {s. G} c)" 1758 "ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c ;; d) 1759 \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf 1760 (P and K G) P' hs m (Guard F {s. G} c ;; d)" 1761 apply (rule ccorres_guard_imp2, erule ccorres_Guard, simp) 1762 apply (rule ccorres_guard_imp2, erule ccorres_Guard_Seq, simp) 1763 done 1764 1765lemmas ccorres_move_const_guards 1766 = ccorres_move_const_guard 1767 ccorres_move_const_guard[unfolded Collect_const] 1768 1769lemma liftM_exs_valid: 1770 "\<lbrace>P\<rbrace> m \<exists>\<lbrace>\<lambda>rv. Q (f rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<exists>\<lbrace>Q\<rbrace>" 1771 unfolding liftM_def exs_valid_def 1772 apply (clarsimp) 1773 apply (drule spec, drule (1) mp) 1774 apply (clarsimp simp: bind_def return_def) 1775 apply (erule bexI [rotated]) 1776 apply simp 1777 done 1778 1779lemma ceqv_remove_eqv_skip: 1780 "\<lbrakk> \<And>s. ceqv \<Gamma> xf () s s' b Skip \<rbrakk> \<Longrightarrow> 1781 ceqv \<Gamma> xf () s s' (a ;; b) a" 1782 apply (rule ceqv_trans) 1783 apply (erule Seq_ceqv [OF ceqv_refl]) 1784 apply (simp add: xpres_def) 1785 apply (clarsimp simp add: ceqv_def) 1786 apply (rule iffI) 1787 apply (auto elim!: exec_elim_cases)[1] 1788 apply (erule exec.intros) 1789 apply (cases s', simp_all) 1790 apply (rule exec.intros) 1791 done 1792 1793lemma ceqv_remove_eqv_skip': 1794 "\<lbrakk> \<And>s. ceqv \<Gamma> xf v s s' b Skip; \<And>s'. ceqv \<Gamma> xf v s s' a a'; xpres xf v \<Gamma> a \<rbrakk> \<Longrightarrow> 1795 ceqv \<Gamma> xf v s s' (a ;; b) a'" 1796 apply (rule ceqv_trans) 1797 apply (erule Seq_ceqv [OF ceqv_refl]) 1798 apply (simp add: xpres_ceqv) 1799 apply (clarsimp simp add: ceqv_def) 1800 apply (rule iffI) 1801 apply (erule exec_elim_cases, simp_all) 1802 apply (auto elim!: exec_elim_cases)[1] 1803 apply (rule exec.intros, simp) 1804 apply (cases s', simp_all) 1805 apply (rule exec.intros) 1806 done 1807 1808lemma xpres_triv: 1809 "xpres xf () G c" 1810 by (simp add: xpres_def) 1811 1812 1813lemma ceqv_Guard_UNIV: 1814 "ceqv G xf v s s' (Guard Err UNIV c) c' 1815 = ceqv G xf v s s' c c'" 1816 by (simp add: ceqv_def exec_Guard) 1817 1818lemma ceqv_guard_into_seq: 1819 "ceqv \<Gamma> xf v s s' (Guard Err S (a ;; b)) (Guard Err S a ;; b)" 1820 by (auto simp: ceqv_def elim!: exec_elim_cases intro: exec.intros) 1821 1822lemma ceqv_Seq_Skip_cases: 1823 "\<lbrakk> \<And>s'. ceqv \<Gamma> xf v s s' a a'; \<And>s. ceqv \<Gamma> xf v s s' b c; xpres xf v \<Gamma> a; 1824 (c = Skip \<and> c' = a' \<or> c' = (a' ;; c)) \<rbrakk> \<Longrightarrow> 1825 ceqv \<Gamma> xf v s s' (a ;; b) c'" 1826 by (metis Seq_ceqv ceqv_remove_eqv_skip') 1827 1828lemma finish_ceqv_Seq_Skip_cases: 1829 "(Skip = Skip \<and> x = x \<or> x = y)" 1830 "(y = Skip \<and> (x ;; y) = z \<or> (x ;; y) = (x ;; y))" 1831 by simp_all 1832 1833lemma semantic_equiv_IF_True: 1834 "semantic_equiv G s s' (IF True THEN c ELSE c' FI) c" 1835 apply (simp add: semantic_equiv_seq_assoc_eq[symmetric]) 1836 by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros) 1837 1838lemmas ccorres_IF_True = ccorres_semantic_equiv[OF semantic_equiv_IF_True] 1839 1840ML {* 1841fun tac ctxt = 1842 resolve_tac ctxt [@{thm ccorres_abstract[where xf'="\<lambda>s. ()"]}] 1 1843 THEN (REPEAT_DETERM 1844 (resolve_tac ctxt @{thms While_ceqv[OF impI, OF refl] Cond_ceqv[OF impI, OF refl] 1845 ceqv_Seq_Skip_cases ceqv_Guard_UNIV[THEN iffD2] 1846 Guard_ceqv[OF impI, OF refl] ceqv_refl 1847 finish_ceqv_Seq_Skip_cases} 1 1848 ORELSE (resolve_tac ctxt [@{thm xpresI}] THEN' simp_tac (ctxt |> Splitter.del_split @{thm "if_split"})) 1 1849 )) 1850 THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms com.case}) 1 1851*} 1852 1853end 1854 1855method_setup ccorres_remove_UNIV_guard = {* Args.context >> (fn ctxt => (K (Method.SIMPLE_METHOD (tac ctxt)))) *} 1856 "removes UNIV guards" 1857 1858end 1859