1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6theory TraceMonadVCG 7imports 8 TraceMonad 9 WPSimp 10 Strengthen 11begin 12 13lemma trace_steps_append: 14 "trace_steps (xs @ ys) s 15 = trace_steps xs s \<union> trace_steps ys (last_st_tr (rev xs) s)" 16 by (induct xs arbitrary: s, simp_all add: last_st_tr_def hd_append) 17 18lemma rely_cond_append: 19 "rely_cond R s (xs @ ys) = (rely_cond R s ys \<and> rely_cond R (last_st_tr ys s) xs)" 20 by (simp add: rely_cond_def trace_steps_append ball_Un conj_comms) 21 22lemma guar_cond_append: 23 "guar_cond G s (xs @ ys) = (guar_cond G s ys \<and> guar_cond G (last_st_tr ys s) xs)" 24 by (simp add: guar_cond_def trace_steps_append ball_Un conj_comms) 25 26lemma prefix_closed_bind: 27 "prefix_closed f \<Longrightarrow> (\<forall>x. prefix_closed (g x)) \<Longrightarrow> prefix_closed (f >>= g)" 28 apply (subst prefix_closed_def, clarsimp simp: bind_def) 29 apply (auto simp: Cons_eq_append_conv split: tmres.split_asm 30 dest!: prefix_closedD[rotated]; 31 fastforce elim: rev_bexI) 32 done 33 34lemmas prefix_closed_bind[rule_format, wp_split] 35 36lemma last_st_tr_append[simp]: 37 "last_st_tr (tr @ tr') s = last_st_tr tr (last_st_tr tr' s)" 38 by (simp add: last_st_tr_def hd_append) 39 40lemma last_st_tr_Nil[simp]: 41 "last_st_tr [] s = s" 42 by (simp add: last_st_tr_def) 43 44lemma last_st_tr_Cons[simp]: 45 "last_st_tr (x # xs) s = snd x" 46 by (simp add: last_st_tr_def) 47 48lemma bind_twp[wp_split]: 49 "\<lbrakk> \<And>r. \<lbrace>Q' r\<rbrace>,\<lbrace>R\<rbrace> g r \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace> \<rbrakk> 50 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= (\<lambda>r. g r) \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 51 apply (subst validI_def, rule conjI) 52 apply (blast intro: prefix_closed_bind validI_prefix_closed) 53 apply (clarsimp simp: bind_def rely_def) 54 apply (drule(2) validI_D) 55 apply (clarsimp simp: rely_cond_append split: tmres.split_asm) 56 apply (clarsimp split: tmres.split_asm) 57 apply (drule meta_spec, frule(2) validI_D) 58 apply (clarsimp simp: rely_cond_append split: if_split_asm) 59 apply (clarsimp simp: guar_cond_append) 60 done 61 62lemma trace_steps_rev_drop_nth: 63 "trace_steps (rev (drop n tr)) s 64 = (\<lambda>i. (fst (rev tr ! i), (if i = 0 then s else snd (rev tr ! (i - 1))), 65 snd (rev tr ! i))) ` {..< length tr - n}" 66 apply (simp add: trace_steps_nth) 67 apply (intro image_cong refl) 68 apply (simp add: rev_nth) 69 done 70 71lemma prefix_closed_drop: 72 "(tr, res) \<in> f s \<Longrightarrow> prefix_closed f \<Longrightarrow> \<exists>res'. (drop n tr, res') \<in> f s" 73proof (induct n arbitrary: res) 74 case 0 then show ?case by auto 75next 76 case (Suc n) 77 have drop_1: "\<And>tr res. (tr, res) \<in> f s \<Longrightarrow> \<exists>res'. (drop 1 tr, res') \<in> f s" 78 by (case_tac tr; fastforce dest: prefix_closedD[rotated] intro: Suc) 79 show ?case 80 using Suc.hyps[OF Suc.prems] 81 by (metis drop_1[simplified] drop_drop add_0 add_Suc) 82qed 83 84lemma validI_GD_drop: 85 "\<lbrakk> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; P s0 s; (tr, res) \<in> f s; 86 rely_cond R s0 (drop n tr) \<rbrakk> 87 \<Longrightarrow> guar_cond G s0 (drop n tr)" 88 apply (drule prefix_closed_drop[where n=n], erule validI_prefix_closed) 89 apply (auto dest: validI_GD) 90 done 91 92lemma parallel_prefix_closed[wp_split]: 93 "prefix_closed f \<Longrightarrow> prefix_closed g 94 \<Longrightarrow> prefix_closed (parallel f g)" 95 apply (subst prefix_closed_def, clarsimp simp: parallel_def) 96 apply (case_tac f_steps; clarsimp) 97 apply (drule(1) prefix_closedD)+ 98 apply fastforce 99 done 100 101lemma rely_cond_drop: 102 "rely_cond R s0 xs \<Longrightarrow> rely_cond R s0 (drop n xs)" 103 using rely_cond_append[where xs="take n xs" and ys="drop n xs"] 104 by simp 105 106lemma rely_cond_is_drop: 107 "rely_cond R s0 xs 108 \<Longrightarrow> (ys = drop (length xs - length ys) xs) 109 \<Longrightarrow> rely_cond R s0 ys" 110 by (metis rely_cond_drop) 111 112lemma bounded_rev_nat_induct: 113 "(\<And>n. N \<le> n \<Longrightarrow> P n) \<Longrightarrow> (\<And>n. n < N \<Longrightarrow> P (Suc n) \<Longrightarrow> P n) 114 \<Longrightarrow> P n" 115 by (induct diff\<equiv>"N - n" arbitrary: n; simp) 116 117lemma drop_n_induct: 118 "P [] \<Longrightarrow> (\<And>n. n < length xs \<Longrightarrow> P (drop (Suc n) xs) \<Longrightarrow> P (drop n xs)) 119 \<Longrightarrow> P (drop n xs)" 120 by (induct len\<equiv>"length (drop n xs)" arbitrary: n xs; simp) 121 122lemma guar_cond_Cons_eq: 123 "guar_cond R s0 (x # xs) 124 = (guar_cond R s0 xs \<and> (fst x \<noteq> Env \<longrightarrow> R (last_st_tr xs s0) (snd x)))" 125 by (cases "fst x"; simp add: guar_cond_def trace_steps_append conj_comms) 126 127lemma guar_cond_Cons: 128 "guar_cond R s0 xs 129 \<Longrightarrow> fst x \<noteq> Env \<longrightarrow> R (last_st_tr xs s0) (snd x) 130 \<Longrightarrow> guar_cond R s0 (x # xs)" 131 by (simp add: guar_cond_Cons_eq) 132 133lemma guar_cond_drop_Suc_eq: 134 "n < length xs 135 \<Longrightarrow> guar_cond R s0 (drop n xs) = (guar_cond R s0 (drop (Suc n) xs) 136 \<and> (fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" 137 apply (rule trans[OF _ guar_cond_Cons_eq]) 138 apply (simp add: Cons_nth_drop_Suc) 139 done 140 141lemma guar_cond_drop_Suc: 142 "guar_cond R s0 (drop (Suc n) xs) 143 \<Longrightarrow> fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n)) 144 \<Longrightarrow> guar_cond R s0 (drop n xs)" 145 by (case_tac "n < length xs"; simp add: guar_cond_drop_Suc_eq) 146 147lemma rely_cond_Cons_eq: 148 "rely_cond R s0 (x # xs) 149 = (rely_cond R s0 xs \<and> (fst x = Env \<longrightarrow> R (last_st_tr xs s0) (snd x)))" 150 by (simp add: rely_cond_def trace_steps_append conj_comms) 151 152lemma rely_cond_Cons: 153 "rely_cond R s0 xs 154 \<Longrightarrow> fst x = Env \<longrightarrow> R (last_st_tr xs s0) (snd x) 155 \<Longrightarrow> rely_cond R s0 (x # xs)" 156 by (simp add: rely_cond_Cons_eq) 157 158lemma rely_cond_drop_Suc_eq: 159 "n < length xs 160 \<Longrightarrow> rely_cond R s0 (drop n xs) = (rely_cond R s0 (drop (Suc n) xs) 161 \<and> (fst (xs ! n) = Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" 162 apply (rule trans[OF _ rely_cond_Cons_eq]) 163 apply (simp add: Cons_nth_drop_Suc) 164 done 165 166lemma rely_cond_drop_Suc: 167 "rely_cond R s0 (drop (Suc n) xs) 168 \<Longrightarrow> fst (xs ! n) = Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n)) 169 \<Longrightarrow> rely_cond R s0 (drop n xs)" 170 by (cases "n < length xs"; simp add: rely_cond_drop_Suc_eq) 171 172lemma last_st_tr_map_zip_hd: 173 "length flags = length tr 174 \<Longrightarrow> tr \<noteq> [] \<longrightarrow> snd (f (hd flags, hd tr)) = snd (hd tr) 175 \<Longrightarrow> last_st_tr (map f (zip flags tr)) = last_st_tr tr" 176 apply (cases tr; simp) 177 apply (cases flags; simp) 178 apply (simp add: fun_eq_iff) 179 done 180 181lemma last_st_tr_drop_map_zip_hd: 182 "length flags = length tr 183 \<Longrightarrow> n < length tr \<longrightarrow> snd (f (flags ! n, tr ! n)) = snd (tr ! n) 184 \<Longrightarrow> last_st_tr (drop n (map f (zip flags tr))) = last_st_tr (drop n tr)" 185 apply (simp add: drop_map drop_zip) 186 apply (rule last_st_tr_map_zip_hd; clarsimp) 187 apply (simp add: hd_drop_conv_nth) 188 done 189 190lemma last_st_tr_map_zip: 191 "length flags = length tr 192 \<Longrightarrow> \<forall>fl tmid s. snd (f (fl, (tmid, s))) = s 193 \<Longrightarrow> last_st_tr (map f (zip flags tr)) = last_st_tr tr" 194 apply (erule last_st_tr_map_zip_hd) 195 apply (clarsimp simp: neq_Nil_conv) 196 done 197 198lemma parallel_rely_induct: 199 assumes preds: "(tr, v) \<in> parallel f g s" "Pf s0 s" "Pg s0 s" 200 assumes validI: "\<lbrace>Pf\<rbrace>,\<lbrace>Rf\<rbrace> f' \<lbrace>Gf\<rbrace>,\<lbrace>Qf\<rbrace>" 201 "\<lbrace>Pg\<rbrace>,\<lbrace>Rg\<rbrace> g' \<lbrace>Gg\<rbrace>,\<lbrace>Qg\<rbrace>" 202 "f s \<subseteq> f' s" "g s \<subseteq> g' s" 203 and compat: "R \<le> Rf" "R \<le> Rg" "Gf \<le> G" "Gg \<le> G" 204 "Gf \<le> Rg" "Gg \<le> Rf" 205 and rely: "rely_cond R s0 (drop n tr)" 206 shows "\<exists>tr_f tr_g. (tr_f, v) \<in> f s \<and> (tr_g, v) \<in> g s 207 \<and> rely_cond Rf s0 (drop n tr_f) \<and> rely_cond Rg s0 (drop n tr_g) 208 \<and> map snd tr_f = map snd tr \<and> map snd tr_g = map snd tr 209 \<and> (\<forall>i \<le> length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0) 210 \<and> guar_cond G s0 (drop n tr)" 211 (is "\<exists>ys zs. _ \<and> _ \<and> ?concl ys zs") 212proof - 213 obtain ys zs where tr: "tr = map parallel_mrg (zip ys zs)" 214 and all2: "list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs" 215 and ys: "(ys, v) \<in> f s" and zs: "(zs, v) \<in> g s" 216 using preds 217 by (clarsimp simp: parallel_def2) 218 note len[simp] = list_all2_lengthD[OF all2] 219 220 have ys': "(ys, v) \<in> f' s" and zs': "(zs, v) \<in> g' s" 221 using ys zs validI by auto 222 223 note rely_f_step = validI_GD_drop[OF validI(1) preds(2) ys' rely_cond_drop_Suc] 224 note rely_g_step = validI_GD_drop[OF validI(2) preds(3) zs' rely_cond_drop_Suc] 225 226 note snd[simp] = list_all2_nthD[OF all2, THEN conjunct2] 227 228 have "?concl ys zs" 229 using rely tr all2 rely_f_step rely_g_step 230 apply (induct n rule: bounded_rev_nat_induct) 231 apply (subst drop_all, assumption) 232 apply clarsimp 233 apply (simp add: list_all2_conv_all_nth last_st_tr_def drop_map[symmetric] 234 hd_drop_conv_nth hd_append) 235 apply (fastforce simp: split_def intro!: nth_equalityI) 236 apply clarsimp 237 apply (erule_tac x=n in meta_allE)+ 238 apply (drule meta_mp, erule rely_cond_is_drop, simp) 239 apply (subst(asm) rely_cond_drop_Suc_eq[where xs="map f xs" for f xs], simp) 240 apply (clarsimp simp: last_st_tr_drop_map_zip_hd if_split[where P="\<lambda>x. x = Env"] 241 split_def) 242 apply (intro conjI; (rule guar_cond_drop_Suc rely_cond_drop_Suc, assumption)) 243 apply (auto simp: guar_cond_drop_Suc_eq last_st_tr_drop_map_zip_hd 244 intro: compat[THEN predicate2D]) 245 done 246 247 thus ?thesis 248 using ys zs 249 by auto 250qed 251 252lemmas parallel_rely_induct0 = parallel_rely_induct[where n=0, simplified] 253 254lemma rg_validI: 255 assumes validI: "\<lbrace>Pf\<rbrace>,\<lbrace>Rf\<rbrace> f \<lbrace>Gf\<rbrace>,\<lbrace>Qf\<rbrace>" 256 "\<lbrace>Pg\<rbrace>,\<lbrace>Rg\<rbrace> g \<lbrace>Gg\<rbrace>,\<lbrace>Qg\<rbrace>" 257 and compat: "R \<le> Rf" "R \<le> Rg" "Gf \<le> G" "Gg \<le> G" 258 "Gf \<le> Rg" "Gg \<le> Rf" 259 shows "\<lbrace>Pf And Pg\<rbrace>,\<lbrace>R\<rbrace> parallel f g \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Qf rv And Qg rv\<rbrace>" 260 apply (clarsimp simp: validI_def rely_def bipred_conj_def 261 parallel_prefix_closed validI[THEN validI_prefix_closed]) 262 apply (drule(3) parallel_rely_induct0[OF _ _ _ validI order_refl order_refl compat]) 263 apply clarsimp 264 apply (drule(2) validI[THEN validI_rvD])+ 265 apply (simp add: last_st_tr_def) 266 done 267 268lemma validI_weaken_pre[wp_pre]: 269 "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> 270 \<Longrightarrow> (\<And>s0 s. P s0 s \<Longrightarrow> P' s0 s) 271 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 272 by (simp add: validI_def, blast) 273 274lemma rely_weaken: 275 "(\<forall>s0 s. R s0 s \<longrightarrow> R' s0 s) 276 \<Longrightarrow> (tr, res) \<in> rely f R s s0 \<Longrightarrow> (tr, res) \<in> rely f R' s s0" 277 by (simp add: rely_def rely_cond_def, blast) 278 279lemma validI_weaken_rely[wp_pre]: 280 "\<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> 281 \<Longrightarrow> (\<forall>s0 s. R s0 s \<longrightarrow> R' s0 s) 282 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 283 apply (simp add: validI_def) 284 by (metis rely_weaken) 285 286lemma validI_strengthen_post: 287 "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace> 288 \<Longrightarrow> (\<forall>v s0 s. Q' v s0 s \<longrightarrow> Q v s0 s) 289 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 290 by (simp add: validI_def) 291 292lemma validI_strengthen_guar: 293 "\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G'\<rbrace>, \<lbrace>Q\<rbrace> 294 \<Longrightarrow> (\<forall>s0 s. G' s0 s \<longrightarrow> G s0 s) 295 \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>" 296 by (force simp: validI_def guar_cond_def) 297 298lemma rely_prim[simp]: 299 "rely (\<lambda>s. insert (v s) (f s)) R s0 = (\<lambda>s. {x. x = v s \<and> rely_cond R s0 (fst x)} \<union> (rely f R s0 s))" 300 "rely (\<lambda>s. {}) R s0 = (\<lambda>_. {})" 301 by (auto simp: rely_def prod_eq_iff) 302 303lemma prefix_closed_put_trace_elem[iff]: 304 "prefix_closed (put_trace_elem x)" 305 by (clarsimp simp: prefix_closed_def put_trace_elem_def) 306 307lemma prefix_closed_return[iff]: 308 "prefix_closed (return x)" 309 by (simp add: prefix_closed_def return_def) 310 311lemma prefix_closed_put_trace[iff]: 312 "prefix_closed (put_trace tr)" 313 by (induct tr; clarsimp simp: prefix_closed_bind) 314 315lemma put_trace_eq_drop: 316 "put_trace xs s 317 = ((\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {.. length xs})" 318 apply (induct xs) 319 apply (clarsimp simp: return_def) 320 apply (clarsimp simp: put_trace_elem_def bind_def) 321 apply (simp add: atMost_Suc_eq_insert_0 image_image) 322 apply (rule equalityI; clarsimp) 323 apply (split if_split_asm; clarsimp) 324 apply (auto intro: image_eqI[where x=0])[1] 325 apply (rule rev_bexI, simp) 326 apply clarsimp 327 done 328 329lemma put_trace_res: 330 "(tr, res) \<in> put_trace xs s 331 \<Longrightarrow> \<exists>n. tr = drop n xs \<and> n \<le> length xs 332 \<and> res = (case n of 0 \<Rightarrow> Result ((), s) | _ \<Rightarrow> Incomplete)" 333 apply (clarsimp simp: put_trace_eq_drop) 334 apply (case_tac n; auto intro: exI[where x=0]) 335 done 336 337lemma put_trace_twp[wp]: 338 "\<lbrace>\<lambda>s0 s. (\<forall>n. rely_cond R s0 (drop n xs) \<longrightarrow> guar_cond G s0 (drop n xs)) 339 \<and> (rely_cond R s0 xs \<longrightarrow> Q () (last_st_tr xs s0) s)\<rbrace>,\<lbrace>R\<rbrace> put_trace xs \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 340 apply (clarsimp simp: validI_def rely_def) 341 apply (drule put_trace_res) 342 apply (clarsimp; clarsimp split: nat.split_asm) 343 done 344 345lemmas put_trace_elem_twp = put_trace_twp[where xs="[x]" for x, simplified] 346 347lemma prefix_closed_select[iff]: 348 "prefix_closed (select S)" 349 by (simp add: prefix_closed_def select_def image_def) 350 351lemma select_wp[wp]: "\<lbrace>\<lambda>s. \<forall>x \<in> S. Q x s\<rbrace> select S \<lbrace>Q\<rbrace>" 352 by (simp add: select_def valid_def mres_def image_def) 353 354lemma rely_cond_rtranclp: 355 "rely_cond R s (map (Pair Env) xs) \<Longrightarrow> rtranclp R s (last_st_tr (map (Pair Env) xs) s)" 356 apply (induct xs arbitrary: s rule: rev_induct) 357 apply simp 358 apply (clarsimp simp add: rely_cond_def) 359 apply (erule converse_rtranclp_into_rtranclp) 360 apply simp 361 done 362 363lemma put_wp[wp]: 364 "\<lbrace>\<lambda>_. Q () s\<rbrace> put s \<lbrace>Q\<rbrace>" 365 by (simp add: put_def valid_def mres_def) 366 367lemma get_wp[wp]: 368 "\<lbrace>\<lambda>s. Q s s\<rbrace> get \<lbrace>Q\<rbrace>" 369 by (simp add: get_def valid_def mres_def) 370 371lemma bind_wp[wp_split]: 372 "\<lbrakk> \<And>r. \<lbrace>Q' r\<rbrace> g r \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>f \<lbrace>Q'\<rbrace> \<rbrakk> 373 \<Longrightarrow> \<lbrace>P\<rbrace> f >>= (\<lambda>r. g r) \<lbrace>Q\<rbrace>" 374 by (fastforce simp: valid_def bind_def2 mres_def intro: image_eqI[rotated]) 375 376lemma modify_wp[wp]: 377 "\<lbrace>\<lambda>s. Q () (f s)\<rbrace> modify f \<lbrace>Q\<rbrace>" 378 unfolding modify_def 379 by wp 380 381definition 382 no_trace :: "('s,'a) tmonad \<Rightarrow> bool" 383where 384 "no_trace f = (\<forall>tr res s. (tr, res) \<in> f s \<longrightarrow> tr = [] \<and> res \<noteq> Incomplete)" 385 386lemmas no_traceD = no_trace_def[THEN iffD1, rule_format] 387 388lemma no_trace_emp: 389 "no_trace f \<Longrightarrow> (tr, r) \<in> f s \<Longrightarrow> tr = []" 390 by (simp add: no_traceD) 391 392lemma no_trace_Incomplete_mem: 393 "no_trace f \<Longrightarrow> (tr, Incomplete) \<notin> f s" 394 by (auto dest: no_traceD) 395 396lemma no_trace_Incomplete_eq: 397 "no_trace f \<Longrightarrow> (tr, res) \<in> f s \<Longrightarrow> res \<noteq> Incomplete" 398 by (auto dest: no_traceD) 399 400lemma no_trace_prefix_closed: 401 "no_trace f \<Longrightarrow> prefix_closed f" 402 by (auto simp add: prefix_closed_def dest: no_trace_emp) 403 404(* Attempt to define triple_judgement to use valid_validI_wp as wp_comb rule. 405 It doesn't work. It seems that wp_comb rules cannot take more than 1 assumption *) 406lemma validI_is_triple: 407 "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> = 408 triple_judgement (\<lambda>(s0, s). prefix_closed f \<longrightarrow> P s0 s) f 409 (\<lambda>(s0,s) f. prefix_closed f \<and> (\<forall>tr res. (tr, res) \<in> rely f R s0 s 410 \<longrightarrow> guar_cond G s0 tr 411 \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')))" 412 apply (simp add: triple_judgement_def validI_def ) 413 apply (cases "prefix_closed f"; simp) 414 done 415 416lemma valid_is_triple: 417 "valid P f Q = 418 triple_judgement P f 419 (\<lambda>s f. (\<forall>(r,s') \<in> (mres (f s)). Q r s'))" 420 by (simp add: triple_judgement_def valid_def mres_def) 421 422lemma no_trace_is_triple: 423 "no_trace f = triple_judgement \<top> f (\<lambda>() f. id no_trace f)" 424 by (simp add: triple_judgement_def split: unit.split) 425 426lemmas [wp_trip] = valid_is_triple validI_is_triple no_trace_is_triple 427 428lemma valid_validI_wp[wp_comb]: 429 "no_trace f \<Longrightarrow> (\<And>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0 \<rbrace>) 430 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 431 by (fastforce simp: rely_def validI_def valid_def mres_def no_trace_prefix_closed dest: no_trace_emp 432 elim: image_eqI[rotated]) 433 434(* Since valid_validI_wp in wp_comb doesn't work, we add the rules directly in the wp set *) 435lemma no_trace_prim: 436 "no_trace get" 437 "no_trace (put s)" 438 "no_trace (modify f)" 439 "no_trace (return v)" 440 "no_trace fail" 441 by (simp_all add: no_trace_def get_def put_def modify_def bind_def 442 return_def select_def fail_def) 443 444lemma no_trace_select: 445 "no_trace (select S)" 446 by (clarsimp simp add: no_trace_def select_def) 447 448lemma no_trace_bind: 449 "no_trace f \<Longrightarrow> \<forall>rv. no_trace (g rv) 450 \<Longrightarrow> no_trace (do rv \<leftarrow> f; g rv od)" 451 apply (subst no_trace_def) 452 apply (clarsimp simp add: bind_def split: tmres.split_asm; 453 auto dest: no_traceD[rotated]) 454 done 455 456lemma no_trace_extra: 457 "no_trace (gets f)" 458 "no_trace (assert P)" 459 "no_trace (assert_opt Q)" 460 by (simp_all add: gets_def assert_def assert_opt_def no_trace_bind no_trace_prim 461 split: option.split) 462 463lemmas no_trace_all[wp, iff] = no_trace_prim no_trace_select no_trace_extra 464 465lemma env_steps_twp[wp]: 466 "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s0 s' \<longrightarrow> Q () s' s') \<and> Q () s0 s\<rbrace>,\<lbrace>R\<rbrace> env_steps \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 467 apply (simp add: interference_def env_steps_def) 468 apply wp 469 apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) 470 apply (drule rely_cond_rtranclp) 471 apply (clarsimp simp add: last_st_tr_def hd_append) 472 done 473 474lemma interference_twp[wp]: 475 "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s\<rbrace>,\<lbrace>R\<rbrace> interference \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 476 apply (simp add: interference_def commit_step_def del: put_trace.simps) 477 apply wp 478 apply clarsimp 479 apply (simp add: drop_Cons nat.split rely_cond_def guar_cond_def) 480 done 481 482(* what Await does if we haven't committed our step is a little 483 strange. this assumes we have, which means s0 = s. we should 484 revisit this if we find a use for Await when this isn't the 485 case *) 486lemma Await_sync_twp: 487 "\<lbrace>\<lambda>s0 s. s = s0 \<and> (\<forall>x. R\<^sup>*\<^sup>* s0 x \<and> c x \<longrightarrow> Q () x x)\<rbrace>,\<lbrace>R\<rbrace> Await c \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 488 apply (simp add: Await_def split_def) 489 apply wp 490 apply clarsimp 491 apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) 492 apply (drule rely_cond_rtranclp) 493 apply (simp add: o_def) 494 done 495 496(* Wrap up the standard usage pattern of wp/wpc/simp into its own command: *) 497method wpsimp uses wp simp split split_del cong = 498 ((determ \<open>wp add: wp|wpc|clarsimp simp: simp split: split split del: split_del cong: cong\<close>)+)[1] 499 500declare K_def [simp] 501 502section "Satisfiability" 503 504text \<open> 505 The dual to validity: an existential instead of a universal 506 quantifier for the post condition. In refinement, it is 507 often sufficient to know that there is one state that 508 satisfies a condition. 509\<close> 510definition 511 exs_valid :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) tmonad \<Rightarrow> 512 ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 513 ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") 514where 515 "exs_valid P f Q \<equiv> (\<forall>s. P s \<longrightarrow> (\<exists>(rv, s') \<in> mres (f s). Q rv s'))" 516 517 518text \<open>The above for the exception monad\<close> 519definition 520 ex_exs_validE :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'e + 'b) tmonad \<Rightarrow> 521 ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('e \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" 522 ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>, \<lbrace>_\<rbrace>") 523where 524 "ex_exs_validE P f Q E \<equiv> 525 exs_valid P f (\<lambda>rv. case rv of Inl e \<Rightarrow> E e | Inr v \<Rightarrow> Q v)" 526 527 528section "Lemmas" 529 530subsection \<open>Determinism\<close> 531 532lemma det_set_iff: 533 "det f \<Longrightarrow> (r \<in> mres (f s)) = (mres (f s) = {r})" 534 apply (simp add: det_def mres_def) 535 apply (fastforce elim: allE[where x=s]) 536 done 537 538lemma return_det [iff]: 539 "det (return x)" 540 by (simp add: det_def return_def) 541 542lemma put_det [iff]: 543 "det (put s)" 544 by (simp add: det_def put_def) 545 546lemma get_det [iff]: 547 "det get" 548 by (simp add: det_def get_def) 549 550lemma det_gets [iff]: 551 "det (gets f)" 552 by (auto simp add: gets_def det_def get_def return_def bind_def) 553 554lemma det_UN: 555 "det f \<Longrightarrow> (\<Union>x \<in> mres (f s). g x) = (g (THE x. x \<in> mres (f s)))" 556 unfolding det_def mres_def 557 apply simp 558 apply (drule spec [of _ s]) 559 apply (clarsimp simp: vimage_def) 560 done 561 562lemma bind_detI [simp, intro!]: 563 "\<lbrakk> det f; \<forall>x. det (g x) \<rbrakk> \<Longrightarrow> det (f >>= g)" 564 apply (simp add: bind_def det_def split_def) 565 apply clarsimp 566 apply (erule_tac x=s in allE) 567 apply clarsimp 568 done 569 570lemma det_modify[iff]: 571 "det (modify f)" 572 by (simp add: modify_def) 573 574lemma the_run_stateI: 575 "mres (M s) = {s'} \<Longrightarrow> the_run_state M s = s'" 576 by (simp add: the_run_state_def) 577 578lemma the_run_state_det: 579 "\<lbrakk> s' \<in> mres (M s); det M \<rbrakk> \<Longrightarrow> the_run_state M s = s'" 580 by (simp only: the_run_stateI det_set_iff[where f=M and s=s]) 581 582subsection "Lifting and Alternative Basic Definitions" 583 584lemma liftE_liftM: "liftE = liftM Inr" 585 apply (rule ext) 586 apply (simp add: liftE_def liftM_def) 587 done 588 589lemma liftME_liftM: "liftME f = liftM (case_sum Inl (Inr \<circ> f))" 590 apply (rule ext) 591 apply (simp add: liftME_def liftM_def bindE_def returnOk_def lift_def) 592 apply (rule_tac f="bind x" in arg_cong) 593 apply (rule ext) 594 apply (case_tac xa) 595 apply (simp_all add: lift_def throwError_def) 596 done 597 598lemma liftE_bindE: 599 "(liftE a) >>=E b = a >>= b" 600 apply (simp add: liftE_def bindE_def lift_def bind_assoc) 601 done 602 603lemma liftM_id[simp]: "liftM id = id" 604 apply (rule ext) 605 apply (simp add: liftM_def) 606 done 607 608lemma liftM_bind: 609 "(liftM t f >>= g) = (f >>= (\<lambda>x. g (t x)))" 610 by (simp add: liftM_def bind_assoc) 611 612lemma gets_bind_ign: "gets f >>= (\<lambda>x. m) = m" 613 apply (rule ext) 614 apply (simp add: bind_def simpler_gets_def) 615 done 616 617lemma get_bind_apply: "(get >>= f) x = f x x" 618 by (simp add: get_def bind_def) 619 620lemma exec_gets: 621 "(gets f >>= m) s = m (f s) s" 622 by (simp add: simpler_gets_def bind_def) 623 624lemma exec_get: 625 "(get >>= m) s = m s s" 626 by (simp add: get_def bind_def) 627 628lemma bind_eqI: 629 "\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" 630 apply (rule ext) 631 apply (simp add: bind_def) 632 done 633 634subsection "Simplification Rules for Lifted And/Or" 635 636lemma pred_andE[elim!]: "\<lbrakk> (A and B) x; \<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 637 by(simp add:pred_conj_def) 638 639lemma pred_andI[intro!]: "\<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> (A and B) x" 640 by(simp add:pred_conj_def) 641 642lemma pred_conj_app[simp]: "(P and Q) x = (P x \<and> Q x)" 643 by(simp add:pred_conj_def) 644 645lemma bipred_andE[elim!]: "\<lbrakk> (A And B) x y; \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 646 by(simp add:bipred_conj_def) 647 648lemma bipred_andI[intro!]: "\<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> (A And B) x y" 649 by (simp add:bipred_conj_def) 650 651lemma bipred_conj_app[simp]: "(P And Q) x = (P x and Q x)" 652 by(simp add:pred_conj_def bipred_conj_def) 653 654lemma pred_disjE[elim!]: "\<lbrakk> (P or Q) x; P x \<Longrightarrow> R; Q x \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 655 by (fastforce simp: pred_disj_def) 656 657lemma pred_disjI1[intro]: "P x \<Longrightarrow> (P or Q) x" 658 by (simp add: pred_disj_def) 659 660lemma pred_disjI2[intro]: "Q x \<Longrightarrow> (P or Q) x" 661 by (simp add: pred_disj_def) 662 663lemma pred_disj_app[simp]: "(P or Q) x = (P x \<or> Q x)" 664 by auto 665 666lemma bipred_disjI1[intro]: "P x y \<Longrightarrow> (P Or Q) x y" 667 by (simp add: bipred_disj_def) 668 669lemma bipred_disjI2[intro]: "Q x y \<Longrightarrow> (P Or Q) x y" 670 by (simp add: bipred_disj_def) 671 672lemma bipred_disj_app[simp]: "(P Or Q) x = (P x or Q x)" 673 by(simp add:pred_disj_def bipred_disj_def) 674 675lemma pred_notnotD[simp]: "(not not P) = P" 676 by(simp add:pred_neg_def) 677 678lemma pred_and_true[simp]: "(P and \<top>) = P" 679 by(simp add:pred_conj_def) 680 681lemma pred_and_true_var[simp]: "(\<top> and P) = P" 682 by(simp add:pred_conj_def) 683 684lemma pred_and_false[simp]: "(P and \<bottom>) = \<bottom>" 685 by(simp add:pred_conj_def) 686 687lemma pred_and_false_var[simp]: "(\<bottom> and P) = \<bottom>" 688 by(simp add:pred_conj_def) 689 690lemma bipred_disj_op_eq[simp]: 691 "reflp R \<Longrightarrow> (=) Or R = R" 692 apply (rule ext, rule ext) 693 apply (auto simp: reflp_def) 694 done 695 696lemma bipred_le_true[simp]: "R \<le> \<top>\<top>" 697 by clarsimp 698 699subsection "Hoare Logic Rules" 700 701lemma validE_def2: 702 "validE P f Q R \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> mres (f s). case r of Inr b \<Rightarrow> Q b s' 703 | Inl a \<Rightarrow> R a s')" 704 by (unfold valid_def validE_def) 705 706lemma seq': 707 "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; 708 \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; 709 \<forall>x s. B x s \<longrightarrow> P x \<and> C s \<rbrakk> \<Longrightarrow> 710 \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" 711 apply (erule bind_wp[rotated]) 712 apply (clarsimp simp: valid_def) 713 apply (fastforce elim: rev_bexI image_eqI[rotated]) 714 done 715 716lemma seq: 717 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>" 718 assumes g_valid: "\<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>" 719 assumes bind: "\<And>x s. B x s \<Longrightarrow> P x \<and> C s" 720 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" 721apply (insert f_valid g_valid bind) 722apply (blast intro: seq') 723done 724 725lemma seq_ext': 726 "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; 727 \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> 728 \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" 729 by (metis bind_wp) 730 731lemmas seq_ext = bind_wp[rotated] 732 733lemma seqE': 734 "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace> ; 735 \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 736 \<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 737 apply (simp add: bindE_def validE_def) 738 apply (erule seq_ext') 739 apply (auto simp: lift_def valid_def throwError_def return_def mres_def 740 split: sum.splits) 741 done 742 743lemma seqE: 744 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>" 745 assumes g_valid: "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 746 shows "\<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 747 apply(insert f_valid g_valid) 748 apply(blast intro: seqE') 749 done 750 751lemma hoare_TrueI: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. \<top>\<rbrace>" 752 by (simp add: valid_def) 753 754lemma hoareE_TrueI: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. \<top>\<rbrace>, \<lbrace>\<lambda>r. \<top>\<rbrace>" 755 by (simp add: validE_def valid_def) 756 757lemma hoare_True_E_R [simp]: 758 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>, -" 759 by (auto simp add: validE_R_def validE_def valid_def split: sum.splits) 760 761lemma hoare_post_conj [intro!]: 762 "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>" 763 by (fastforce simp: valid_def split_def bipred_conj_def) 764 765lemma hoare_pre_disj [intro!]: 766 "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>" 767 by (simp add:valid_def pred_disj_def) 768 769lemma hoare_conj: 770 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q And Q'\<rbrace>" 771 unfolding valid_def 772 by (auto) 773 774lemma hoare_post_taut: "\<lbrace> P \<rbrace> a \<lbrace> \<top>\<top> \<rbrace>" 775 by (simp add:valid_def) 776 777lemma wp_post_taut: "\<lbrace>\<lambda>r. True\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>" 778 by (rule hoare_post_taut) 779 780lemma wp_post_tautE: "\<lbrace>\<lambda>r. True\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>,\<lbrace>\<lambda>f s. True\<rbrace>" 781proof - 782 have P: "\<And>r. (case r of Inl a \<Rightarrow> True | _ \<Rightarrow> True) = True" 783 by (case_tac r, simp_all) 784 show ?thesis 785 by (simp add: validE_def P wp_post_taut) 786qed 787 788lemma hoare_pre_cont [simp]: "\<lbrace> \<bottom> \<rbrace> a \<lbrace> P \<rbrace>" 789 by (simp add:valid_def) 790 791 792subsection \<open>Strongest Postcondition Rules\<close> 793 794lemma get_sp: 795 "\<lbrace>P\<rbrace> get \<lbrace>\<lambda>a s. s = a \<and> P s\<rbrace>" 796 by(simp add:get_def valid_def mres_def) 797 798lemma put_sp: 799 "\<lbrace>\<top>\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>" 800 by(simp add:put_def valid_def mres_def) 801 802lemma return_sp: 803 "\<lbrace>P\<rbrace> return a \<lbrace>\<lambda>b s. b = a \<and> P s\<rbrace>" 804 by(simp add:return_def valid_def mres_def) 805 806lemma assert_sp: 807 "\<lbrace> P \<rbrace> assert Q \<lbrace> \<lambda>r s. P s \<and> Q \<rbrace>" 808 by (simp add: assert_def fail_def return_def valid_def mres_def) 809 810lemma hoare_gets_sp: 811 "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv s. rv = f s \<and> P s\<rbrace>" 812 by (simp add: valid_def simpler_gets_def mres_def) 813 814lemma hoare_return_drop_var [iff]: "\<lbrace> Q \<rbrace> return x \<lbrace> \<lambda>r. Q \<rbrace>" 815 by (simp add:valid_def return_def mres_def) 816 817lemma hoare_gets [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> gets f \<lbrace> Q \<rbrace>" 818 by (simp add:valid_def gets_def get_def bind_def return_def mres_def) 819 820lemma hoare_modifyE_var [intro!]: 821 "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> modify f \<lbrace> \<lambda>r s. Q s \<rbrace>" 822 by(simp add: valid_def modify_def put_def get_def bind_def mres_def) 823 824lemma hoare_if [intro!]: 825 "\<lbrakk> P \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>; \<not> P \<Longrightarrow> \<lbrace> Q \<rbrace> b \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> 826 \<lbrace> Q \<rbrace> if P then a else b \<lbrace> R \<rbrace>" 827 by (simp add:valid_def) 828 829lemma hoare_pre_subst: "\<lbrakk> A = B; \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>B\<rbrace> a \<lbrace>C\<rbrace>" 830 by(clarsimp simp:valid_def split_def) 831 832lemma hoare_post_subst: "\<lbrakk> B = C; \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace>" 833 by(clarsimp simp:valid_def split_def) 834 835lemma hoare_pre_tautI: "\<lbrakk> \<lbrace>A and P\<rbrace> a \<lbrace>B\<rbrace>; \<lbrace>A and not P\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace>" 836 by(fastforce simp:valid_def split_def pred_conj_def pred_neg_def) 837 838lemma hoare_pre_imp: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q s; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 839 by (fastforce simp add:valid_def) 840 841lemma hoare_post_imp: "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> R r s; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 842 by(fastforce simp:valid_def split_def) 843 844lemma hoare_post_impErr': "\<lbrakk> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; 845 \<forall>r s. Q r s \<longrightarrow> R r s; 846 \<forall>e s. E e s \<longrightarrow> F e s \<rbrakk> \<Longrightarrow> 847 \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>" 848 apply (simp add: validE_def) 849 apply (rule_tac Q="\<lambda>r s. case r of Inl a \<Rightarrow> E a s | Inr b \<Rightarrow> Q b s" in hoare_post_imp) 850 apply (case_tac r) 851 apply simp_all 852 done 853 854lemma hoare_post_impErr: "\<lbrakk> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; 855 \<And>r s. Q r s \<Longrightarrow> R r s; 856 \<And>e s. E e s \<Longrightarrow> F e s \<rbrakk> \<Longrightarrow> 857 \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>" 858 apply (blast intro: hoare_post_impErr') 859 done 860 861lemma hoare_validE_cases: 862 "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace>; \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_ _. True \<rbrace>, \<lbrace> R \<rbrace> \<rbrakk> 863 \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>, \<lbrace> R \<rbrace>" 864 by (simp add: validE_def valid_def split: sum.splits) blast 865 866lemma hoare_post_imp_dc: 867 "\<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. Q\<rbrace>; \<And>s. Q s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. R\<rbrace>,\<lbrace>\<lambda>r. R\<rbrace>" 868 by (simp add: validE_def valid_def split: sum.splits) blast 869 870lemma hoare_post_imp_dc2: 871 "\<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. Q\<rbrace>; \<And>s. Q s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. R\<rbrace>,\<lbrace>\<lambda>r s. True\<rbrace>" 872 by (simp add: validE_def valid_def split: sum.splits) blast 873 874lemma hoare_post_imp_dc2E: 875 "\<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. Q\<rbrace>; \<And>s. Q s \<Longrightarrow> R s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>r s. True\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace>" 876 by (simp add: validE_def valid_def split: sum.splits) fast 877 878lemma hoare_post_imp_dc2E_actual: 879 "\<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>r s. True\<rbrace>, \<lbrace>\<lambda>r. R\<rbrace>" 880 by (simp add: validE_def valid_def split: sum.splits) fast 881 882lemma hoare_post_imp_dc2_actual: 883 "\<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. R\<rbrace>, \<lbrace>\<lambda>r s. True\<rbrace>" 884 by (simp add: validE_def valid_def split: sum.splits) fast 885 886lemma hoare_post_impE: "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> R r s; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 887 by (fastforce simp:valid_def split_def) 888 889lemma hoare_conjD1: 890 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv and R rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv\<rbrace>" 891 unfolding valid_def by auto 892 893lemma hoare_conjD2: 894 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv and R rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. R rv\<rbrace>" 895 unfolding valid_def by auto 896 897lemma hoare_post_disjI1: 898 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv or R rv\<rbrace>" 899 unfolding valid_def by auto 900 901lemma hoare_post_disjI2: 902 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. R rv\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv or R rv\<rbrace>" 903 unfolding valid_def by auto 904 905lemma hoare_weaken_pre: 906 "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 907 apply (rule hoare_pre_imp) 908 prefer 2 909 apply assumption 910 apply blast 911 done 912 913lemma hoare_strengthen_post: 914 "\<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<And>r s. Q r s \<Longrightarrow> R r s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 915 apply (rule hoare_post_imp) 916 prefer 2 917 apply assumption 918 apply blast 919 done 920 921lemma use_valid: "\<lbrakk>(r, s') \<in> mres (f s); \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; P s \<rbrakk> \<Longrightarrow> Q r s'" 922 apply (simp add: valid_def) 923 apply blast 924 done 925 926lemma use_validE_norm: "\<lbrakk> (Inr r', s') \<in> mres (B s); \<lbrace> P \<rbrace> B \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; P s \<rbrakk> \<Longrightarrow> Q r' s'" 927 apply (clarsimp simp: validE_def valid_def) 928 apply force 929 done 930 931lemma use_validE_except: "\<lbrakk> (Inl r', s') \<in> mres (B s); \<lbrace> P \<rbrace> B \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; P s \<rbrakk> \<Longrightarrow> E r' s'" 932 apply (clarsimp simp: validE_def valid_def) 933 apply force 934 done 935 936lemma in_inv_by_hoareD: 937 "\<lbrakk> \<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; (x,s') \<in> mres (f s) \<rbrakk> \<Longrightarrow> s' = s" 938 apply (drule_tac x="(=) s" in meta_spec) 939 apply (auto simp add: valid_def mres_def) 940 done 941 942subsection "Satisfiability" 943 944lemma exs_hoare_post_imp: "\<lbrakk>\<And>r s. Q r s \<Longrightarrow> R r s; \<lbrace>P\<rbrace> a \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<exists>\<lbrace>R\<rbrace>" 945 apply (simp add: exs_valid_def) 946 apply safe 947 apply (erule_tac x=s in allE, simp) 948 apply blast 949 done 950 951lemma use_exs_valid: "\<lbrakk>\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; P s \<rbrakk> \<Longrightarrow> \<exists>(r, s') \<in> mres (f s). Q r s'" 952 by (simp add: exs_valid_def) 953 954definition "exs_postcondition P f \<equiv> (\<lambda>a b. \<exists>(rv, s)\<in> f a b. P rv s)" 955 956lemma exs_valid_is_triple: 957 "exs_valid P f Q = triple_judgement P f (exs_postcondition Q (\<lambda>s f. mres (f s)))" 958 by (simp add: triple_judgement_def exs_postcondition_def exs_valid_def) 959 960lemmas [wp_trip] = exs_valid_is_triple 961 962lemma exs_valid_weaken_pre [wp_comb]: 963 "\<lbrakk> \<lbrace> P' \<rbrace> f \<exists>\<lbrace> Q \<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<exists>\<lbrace> Q \<rbrace>" 964 apply atomize 965 apply (clarsimp simp: exs_valid_def) 966 done 967 968lemma exs_valid_chain: 969 "\<lbrakk> \<lbrace> P \<rbrace> f \<exists>\<lbrace> Q \<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>r s. Q r s \<Longrightarrow> S r s \<rbrakk> \<Longrightarrow> \<lbrace> R \<rbrace> f \<exists>\<lbrace> S \<rbrace>" 970 by (fastforce simp only: exs_valid_def Bex_def ) 971 972lemma exs_valid_assume_pre: 973 "\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace> P \<rbrace> f \<exists>\<lbrace> Q \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<exists>\<lbrace> Q \<rbrace>" 974 apply (fastforce simp: exs_valid_def) 975 done 976 977lemma exs_valid_bind [wp_split]: 978 "\<lbrakk> \<And>x. \<lbrace>B x\<rbrace> g x \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> A \<rbrace> f >>= (\<lambda>x. g x) \<exists>\<lbrace> C \<rbrace>" 979 apply atomize 980 apply (clarsimp simp: exs_valid_def bind_def2 mres_def) 981 apply (drule spec, drule(1) mp, clarsimp) 982 apply (drule spec2, drule(1) mp, clarsimp) 983 apply (simp add: image_def bex_Un) 984 apply (strengthen subst[where P="\<lambda>x. x \<in> f s" for s, mk_strg I _ E], simp) 985 apply (fastforce elim: rev_bexI) 986 done 987 988lemma exs_valid_return [wp]: 989 "\<lbrace> Q v \<rbrace> return v \<exists>\<lbrace> Q \<rbrace>" 990 by (clarsimp simp: exs_valid_def return_def mres_def) 991 992lemma exs_valid_select [wp]: 993 "\<lbrace> \<lambda>s. \<exists>r \<in> S. Q r s \<rbrace> select S \<exists>\<lbrace> Q \<rbrace>" 994 apply (clarsimp simp: exs_valid_def select_def mres_def) 995 apply (auto simp add: image_def) 996 done 997 998lemma exs_valid_get [wp]: 999 "\<lbrace> \<lambda>s. Q s s \<rbrace> get \<exists>\<lbrace> Q \<rbrace>" 1000 by (clarsimp simp: exs_valid_def get_def mres_def) 1001 1002lemma exs_valid_gets [wp]: 1003 "\<lbrace> \<lambda>s. Q (f s) s \<rbrace> gets f \<exists>\<lbrace> Q \<rbrace>" 1004 by (clarsimp simp: gets_def) wp 1005 1006lemma exs_valid_put [wp]: 1007 "\<lbrace> Q v \<rbrace> put v \<exists>\<lbrace> Q \<rbrace>" 1008 by (clarsimp simp: put_def exs_valid_def mres_def) 1009 1010lemma exs_valid_state_assert [wp]: 1011 "\<lbrace> \<lambda>s. Q () s \<and> G s \<rbrace> state_assert G \<exists>\<lbrace> Q \<rbrace>" 1012 by (clarsimp simp: state_assert_def exs_valid_def get_def 1013 assert_def bind_def2 return_def mres_def) 1014 1015lemmas exs_valid_guard = exs_valid_state_assert 1016 1017lemma exs_valid_fail [wp]: 1018 "\<lbrace> \<lambda>_. False \<rbrace> fail \<exists>\<lbrace> Q \<rbrace>" 1019 by (clarsimp simp: fail_def exs_valid_def) 1020 1021lemma exs_valid_condition [wp]: 1022 "\<lbrakk> \<lbrace> P \<rbrace> L \<exists>\<lbrace> Q \<rbrace>; \<lbrace> P' \<rbrace> R \<exists>\<lbrace> Q \<rbrace> \<rbrakk> \<Longrightarrow> 1023 \<lbrace> \<lambda>s. (C s \<and> P s) \<or> (\<not> C s \<and> P' s) \<rbrace> condition C L R \<exists>\<lbrace> Q \<rbrace>" 1024 by (clarsimp simp: condition_def exs_valid_def split: sum.splits) 1025 1026 1027subsection MISC 1028 1029lemma hoare_return_simp: 1030 "\<lbrace>P\<rbrace> return x \<lbrace>Q\<rbrace> = (\<forall>s. P s \<longrightarrow> Q x s)" 1031 by (simp add: valid_def return_def mres_def) 1032 1033lemma hoare_gen_asm: 1034 "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>" 1035 by (fastforce simp add: valid_def) 1036 1037lemma hoare_when_wp [wp]: 1038 "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> when P f \<lbrace>R\<rbrace>" 1039 by (clarsimp simp: when_def valid_def return_def mres_def) 1040 1041lemma hoare_conjI: 1042 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>" 1043 unfolding valid_def by blast 1044 1045lemma hoare_disjI1: 1046 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<or> R r s \<rbrace>" 1047 unfolding valid_def by blast 1048 1049lemma hoare_disjI2: 1050 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<or> R r s \<rbrace>" 1051 unfolding valid_def by blast 1052 1053lemma hoare_assume_pre: 1054 "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1055 by (auto simp: valid_def) 1056 1057lemma hoare_returnOk_sp: 1058 "\<lbrace>P\<rbrace> returnOk x \<lbrace>\<lambda>r s. r = x \<and> P s\<rbrace>, \<lbrace>Q\<rbrace>" 1059 by (simp add: valid_def validE_def returnOk_def return_def mres_def) 1060 1061lemma hoare_assume_preE: 1062 "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace>" 1063 by (auto simp: valid_def validE_def) 1064 1065lemma hoare_allI: 1066 "(\<And>x. \<lbrace>P\<rbrace>f\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r s. \<forall>x. Q x r s\<rbrace>" 1067 by (simp add: valid_def) blast 1068 1069lemma validE_allI: 1070 "(\<And>x. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q x r s\<rbrace>,\<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x. Q x r s\<rbrace>,\<lbrace>E\<rbrace>" 1071 by (fastforce simp: valid_def validE_def split: sum.splits) 1072 1073lemma hoare_exI: 1074 "\<lbrace>P\<rbrace> f \<lbrace>Q x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. \<exists>x. Q x r s\<rbrace>" 1075 by (simp add: valid_def) blast 1076 1077lemma hoare_impI: 1078 "(R \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r s. R \<longrightarrow> Q r s\<rbrace>" 1079 by (simp add: valid_def) blast 1080 1081lemma validE_impI: 1082 " \<lbrakk>\<And>E. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>E\<rbrace>; (P' \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>)\<rbrakk> \<Longrightarrow> 1083 \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. P' \<longrightarrow> Q r s\<rbrace>, \<lbrace>E\<rbrace>" 1084 by (fastforce simp: validE_def valid_def split: sum.splits) 1085 1086lemma hoare_case_option_wp: 1087 "\<lbrakk> \<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>; 1088 \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace> \<rbrakk> 1089 \<Longrightarrow> \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>" 1090 by (cases v) auto 1091 1092subsection "Reasoning directly about states" 1093 1094lemma in_throwError: 1095 "((v, s') \<in> mres (throwError e s)) = (v = Inl e \<and> s' = s)" 1096 by (simp add: throwError_def return_def mres_def) 1097 1098lemma in_returnOk: 1099 "((v', s') \<in> mres (returnOk v s)) = (v' = Inr v \<and> s' = s)" 1100 by (simp add: returnOk_def return_def mres_def) 1101 1102lemma in_bind: 1103 "((r,s') \<in> mres ((do x \<leftarrow> f; g x od) s)) = 1104 (\<exists>s'' x. (x, s'') \<in> mres (f s) \<and> (r, s') \<in> mres (g x s''))" 1105 apply (simp add: bind_def split_def mres_def) 1106 apply (auto split: tmres.splits; force elim: rev_bexI image_eqI[rotated]) 1107 done 1108 1109lemma in_bindE_R: 1110 "((Inr r,s') \<in> mres ((doE x \<leftarrow> f; g x odE) s)) = 1111 (\<exists>s'' x. (Inr x, s'') \<in> mres (f s) \<and> (Inr r, s') \<in> mres (g x s''))" 1112 apply (simp add: bindE_def in_bind) 1113 apply (simp add: lift_def split_def) 1114 apply (clarsimp simp: throwError_def return_def lift_def mres_def split: sum.splits) 1115 apply force 1116 done 1117 1118lemma in_bindE_L: 1119 "((Inl r, s') \<in> mres ((doE x \<leftarrow> f; g x odE) s)) \<Longrightarrow> 1120 (\<exists>s'' x. (Inr x, s'') \<in> mres (f s) \<and> (Inl r, s') \<in> mres (g x s'')) \<or> ((Inl r, s') \<in> mres (f s))" 1121 apply (simp add: bindE_def in_bind lift_def) 1122 apply safe 1123 apply (simp add: return_def throwError_def lift_def split_def mres_def split: sum.splits if_split_asm) 1124 apply force+ 1125 done 1126 1127lemma in_return: 1128 "(r, s') \<in> mres (return v s) = (r = v \<and> s' = s)" 1129 by (simp add: return_def mres_def) 1130 1131lemma in_liftE: 1132 "((v, s') \<in> mres (liftE f s)) = (\<exists>v'. v = Inr v' \<and> (v', s') \<in> mres (f s))" 1133 by (auto simp add: liftE_def in_bind in_return) 1134 1135lemma in_whenE: "((v, s') \<in> mres (whenE P f s)) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> 1136 (\<not>P \<longrightarrow> v = Inr () \<and> s' = s))" 1137 by (simp add: whenE_def in_returnOk) 1138 1139lemma inl_whenE: 1140 "((Inl x, s') \<in> mres (whenE P f s)) = (P \<and> (Inl x, s') \<in> mres (f s))" 1141 by (auto simp add: in_whenE) 1142 1143lemma in_fail: 1144 "r \<in> mres (fail s) = False" 1145 by (simp add: fail_def mres_def) 1146 1147lemma in_assert: 1148 "(r, s') \<in> mres (assert P s) = (P \<and> s' = s)" 1149 by (auto simp add: assert_def return_def fail_def mres_def) 1150 1151lemma in_assertE: 1152 "(r, s') \<in> mres (assertE P s) = (P \<and> r = Inr () \<and> s' = s)" 1153 by (auto simp add: assertE_def returnOk_def return_def fail_def mres_def) 1154 1155lemma in_assert_opt: 1156 "(r, s') \<in> mres (assert_opt v s) = (v = Some r \<and> s' = s)" 1157 by (auto simp: assert_opt_def in_fail in_return split: option.splits) 1158 1159lemma in_get: 1160 "(r, s') \<in> mres (get s) = (r = s \<and> s' = s)" 1161 by (simp add: get_def mres_def) 1162 1163lemma in_gets: 1164 "(r, s') \<in> mres (gets f s) = (r = f s \<and> s' = s)" 1165 by (simp add: simpler_gets_def mres_def) 1166 1167lemma in_put: 1168 "(r, s') \<in> mres (put x s) = (s' = x \<and> r = ())" 1169 by (simp add: put_def mres_def) 1170 1171lemma in_when: 1172 "(v, s') \<in> mres (when P f s) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not>P \<longrightarrow> v = () \<and> s' = s))" 1173 by (simp add: when_def in_return) 1174 1175lemma in_modify: 1176 "(v, s') \<in> mres (modify f s) = (s'=f s \<and> v = ())" 1177 by (auto simp add: modify_def bind_def get_def put_def mres_def) 1178 1179lemma gets_the_in_monad: 1180 "((v, s') \<in> mres (gets_the f s)) = (s' = s \<and> f s = Some v)" 1181 by (auto simp: gets_the_def in_bind in_gets in_assert_opt split: option.split) 1182 1183lemma in_alternative: 1184 "(r,s') \<in> mres ((f \<sqinter> g) s) = ((r,s') \<in> mres (f s) \<or> (r,s') \<in> mres (g s))" 1185 by (auto simp add: alternative_def mres_def) 1186 1187lemmas in_monad = inl_whenE in_whenE in_liftE in_bind in_bindE_L 1188 in_bindE_R in_returnOk in_throwError in_fail 1189 in_assertE in_assert in_return in_assert_opt 1190 in_get in_gets in_put in_when (* unlessE_whenE *) 1191 (* unless_when *) in_modify gets_the_in_monad 1192 in_alternative 1193 1194subsection "Non-Failure" 1195 1196lemma no_failD: 1197 "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> Failed \<notin> snd ` m s" 1198 by (simp add: no_fail_def) 1199 1200lemma non_fail_modify [wp,simp]: 1201 "no_fail \<top> (modify f)" 1202 by (simp add: no_fail_def modify_def get_def put_def bind_def) 1203 1204lemma non_fail_gets_simp[simp]: 1205 "no_fail P (gets f)" 1206 unfolding no_fail_def gets_def get_def return_def bind_def 1207 by simp 1208 1209lemma non_fail_gets: 1210 "no_fail \<top> (gets f)" 1211 by simp 1212 1213lemma snd_pair_image: 1214 "snd ` Pair x ` S = S" 1215 by (simp add: image_def) 1216 1217lemma non_fail_select [simp]: 1218 "no_fail \<top> (select S)" 1219 by (simp add: no_fail_def select_def image_def) 1220 1221lemma no_fail_pre: 1222 "\<lbrakk> no_fail P f; \<And>s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> no_fail Q f" 1223 by (simp add: no_fail_def) 1224 1225lemma no_fail_alt [wp]: 1226 "\<lbrakk> no_fail P f; no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f OR g)" 1227 by (auto simp add: no_fail_def alternative_def) 1228 1229lemma no_fail_return [simp, wp]: 1230 "no_fail \<top> (return x)" 1231 by (simp add: return_def no_fail_def) 1232 1233lemma no_fail_get [simp, wp]: 1234 "no_fail \<top> get" 1235 by (simp add: get_def no_fail_def) 1236 1237lemma no_fail_put [simp, wp]: 1238 "no_fail \<top> (put s)" 1239 by (simp add: put_def no_fail_def) 1240 1241lemma no_fail_when [wp]: 1242 "(P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else \<top>) (when P f)" 1243 by (simp add: when_def) 1244 1245lemma no_fail_unless [wp]: 1246 "(\<not>P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then \<top> else Q) (unless P f)" 1247 by (simp add: unless_def when_def) 1248 1249lemma no_fail_fail [simp, wp]: 1250 "no_fail \<bottom> fail" 1251 by (simp add: fail_def no_fail_def) 1252 1253lemmas [wp] = non_fail_gets 1254 1255lemma no_fail_assert [simp, wp]: 1256 "no_fail (\<lambda>_. P) (assert P)" 1257 by (simp add: assert_def) 1258 1259lemma no_fail_assert_opt [simp, wp]: 1260 "no_fail (\<lambda>_. P \<noteq> None) (assert_opt P)" 1261 by (simp add: assert_opt_def split: option.splits) 1262 1263lemma no_fail_case_option [wp]: 1264 assumes f: "no_fail P f" 1265 assumes g: "\<And>x. no_fail (Q x) (g x)" 1266 shows "no_fail (if x = None then P else Q (the x)) (case_option f g x)" 1267 by (clarsimp simp add: f g) 1268 1269lemma no_fail_if [wp]: 1270 "\<lbrakk> P \<Longrightarrow> no_fail Q f; \<not>P \<Longrightarrow> no_fail R g \<rbrakk> \<Longrightarrow> 1271 no_fail (if P then Q else R) (if P then f else g)" 1272 by simp 1273 1274lemma no_fail_apply [wp]: 1275 "no_fail P (f (g x)) \<Longrightarrow> no_fail P (f $ g x)" 1276 by simp 1277 1278lemma no_fail_undefined [simp, wp]: 1279 "no_fail \<bottom> undefined" 1280 by (simp add: no_fail_def) 1281 1282lemma no_fail_returnOK [simp, wp]: 1283 "no_fail \<top> (returnOk x)" 1284 by (simp add: returnOk_def) 1285 1286(* text {* Empty results implies non-failure *} 1287 1288lemma empty_fail_modify [simp]: 1289 "empty_fail (modify f)" 1290 by (simp add: empty_fail_def simpler_modify_def) 1291 1292lemma empty_fail_gets [simp]: 1293 "empty_fail (gets f)" 1294 by (simp add: empty_fail_def simpler_gets_def) 1295 1296lemma empty_failD: 1297 "\<lbrakk> empty_fail m; fst (m s) = {} \<rbrakk> \<Longrightarrow> snd (m s)" 1298 by (simp add: empty_fail_def) 1299 1300lemma empty_fail_select_f [simp]: 1301 assumes ef: "fst S = {} \<Longrightarrow> snd S" 1302 shows "empty_fail (select_f S)" 1303 by (fastforce simp add: empty_fail_def select_f_def intro: ef) 1304 1305lemma empty_fail_bind [simp]: 1306 "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)" 1307 apply (simp add: bind_def empty_fail_def split_def) 1308 apply clarsimp 1309 apply (case_tac "fst (a s) = {}") 1310 apply blast 1311 apply (clarsimp simp: ex_in_conv [symmetric]) 1312 done 1313 1314lemma empty_fail_return [simp]: 1315 "empty_fail (return x)" 1316 by (simp add: empty_fail_def return_def) 1317 1318lemma empty_fail_mapM [simp]: 1319 assumes m: "\<And>x. empty_fail (m x)" 1320 shows "empty_fail (mapM m xs)" 1321proof (induct xs) 1322 case Nil 1323 thus ?case by (simp add: mapM_def sequence_def) 1324next 1325 case Cons 1326 have P: "\<And>m x xs. mapM m (x # xs) = (do y \<leftarrow> m x; ys \<leftarrow> (mapM m xs); return (y # ys) od)" 1327 by (simp add: mapM_def sequence_def Let_def) 1328 from Cons 1329 show ?case by (simp add: P m) 1330qed 1331 1332lemma empty_fail [simp]: 1333 "empty_fail fail" 1334 by (simp add: fail_def empty_fail_def) 1335 1336lemma empty_fail_assert_opt [simp]: 1337 "empty_fail (assert_opt x)" 1338 by (simp add: assert_opt_def split: option.splits) 1339 1340lemma empty_fail_mk_ef: 1341 "empty_fail (mk_ef o m)" 1342 by (simp add: empty_fail_def mk_ef_def) 1343 *) 1344subsection "Failure" 1345 1346lemma fail_wp: "\<lbrace>\<lambda>x. True\<rbrace> fail \<lbrace>Q\<rbrace>" 1347 by (simp add: valid_def fail_def mres_def vimage_def) 1348 1349lemma failE_wp: "\<lbrace>\<lambda>x. True\<rbrace> fail \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1350 by (simp add: validE_def fail_wp) 1351 1352lemma fail_update [iff]: 1353 "fail (f s) = fail s" 1354 by (simp add: fail_def) 1355 1356 1357text \<open>We can prove postconditions using hoare triples\<close> 1358 1359lemma post_by_hoare: "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; P s; (r, s') \<in> mres (f s) \<rbrakk> \<Longrightarrow> Q r s'" 1360 apply (simp add: valid_def) 1361 apply blast 1362 done 1363 1364text \<open>Weakest Precondition Rules\<close> 1365 1366lemma hoare_vcg_prop: 1367 "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>" 1368 by (simp add: valid_def) 1369 1370lemma return_wp: 1371 "\<lbrace>P x\<rbrace> return x \<lbrace>P\<rbrace>" 1372 by(simp add:valid_def return_def mres_def) 1373 1374(* lemma get_wp: 1375 "\<lbrace>\<lambda>s. P s s\<rbrace> get \<lbrace>P\<rbrace>" 1376 by(auto simp add:valid_def split_def get_def mres_def) 1377 *) 1378lemma gets_wp: 1379 "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>" 1380 by(simp add:valid_def split_def gets_def return_def get_def bind_def mres_def) 1381 1382(* lemma modify_wp: 1383 "\<lbrace>\<lambda>s. P () (f s)\<rbrace> modify f \<lbrace>P\<rbrace>" 1384 by(simp add:valid_def split_def modify_def get_def put_def bind_def ) 1385 *) 1386(* lemma put_wp: 1387 "\<lbrace>\<lambda>s. P () x\<rbrace> put x \<lbrace>P\<rbrace>" 1388 by(simp add:valid_def put_def) 1389 *) 1390lemma returnOk_wp: 1391 "\<lbrace>P x\<rbrace> returnOk x \<lbrace>P\<rbrace>,\<lbrace>E\<rbrace>" 1392 by(simp add:validE_def2 returnOk_def return_def mres_def) 1393 1394lemma throwError_wp: 1395 "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>,\<lbrace>E\<rbrace>" 1396 by(simp add:validE_def2 throwError_def return_def mres_def) 1397 1398lemma returnOKE_R_wp : "\<lbrace>P x\<rbrace> returnOk x \<lbrace>P\<rbrace>, -" 1399 by (simp add: validE_R_def validE_def valid_def returnOk_def return_def mres_def) 1400 1401lemma catch_wp: 1402 "\<lbrakk> \<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 1403 \<lbrace>P\<rbrace> catch f handler \<lbrace>Q\<rbrace>" 1404 apply (unfold catch_def validE_def) 1405 apply (erule seq_ext) 1406 apply (simp add: return_wp split: sum.splits) 1407 done 1408 1409lemma handleE'_wp: 1410 "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace> \<rbrakk> \<Longrightarrow> 1411 \<lbrace>P\<rbrace> f <handle2> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1412 apply (unfold handleE'_def validE_def) 1413 apply (erule seq_ext) 1414 apply (clarsimp split: sum.splits) 1415 apply (simp add: valid_def return_def mres_def) 1416 done 1417 1418lemma handleE_wp: 1419 assumes x: "\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1420 assumes y: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>" 1421 shows "\<lbrace>P\<rbrace> f <handle> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1422 by (simp add: handleE_def handleE'_wp [OF x y]) 1423 1424lemma hoare_vcg_split_if: 1425 "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow> 1426 \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>" 1427 by simp 1428 1429lemma hoare_vcg_split_ifE: 1430 "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>; \<not>P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 1431 \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>" 1432 by simp 1433 1434lemma in_image_constant: 1435 "(x \<in> (\<lambda>_. v) ` S) = (x = v \<and> S \<noteq> {})" 1436 by (simp add: image_constant_conv) 1437 1438lemma hoare_liftM_subst: "\<lbrace>P\<rbrace> liftM f m \<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace>" 1439 apply (simp add: liftM_def bind_def2 return_def split_def mres_def) 1440 apply (simp add: valid_def Ball_def mres_def image_Un) 1441 apply (simp add: image_image in_image_constant) 1442 apply (rule_tac f=All in arg_cong) 1443 apply (rule ext) 1444 apply force 1445 done 1446 1447lemma liftE_validE[simp]: "\<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1448 apply (simp add: liftE_liftM validE_def hoare_liftM_subst o_def) 1449 done 1450 1451lemma liftE_wp: 1452 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1453 by simp 1454 1455lemma liftM_wp: "\<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<lbrace>Q\<rbrace>" 1456 by (simp add: hoare_liftM_subst) 1457 1458lemma hoare_liftME_subst: "\<lbrace>P\<rbrace> liftME f m \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> = \<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace>,\<lbrace>E\<rbrace>" 1459 apply (simp add: validE_def liftME_liftM hoare_liftM_subst o_def) 1460 apply (rule_tac f="valid P m" in arg_cong) 1461 apply (rule ext)+ 1462 apply (case_tac x, simp_all) 1463 done 1464 1465lemma liftME_wp: "\<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftME f m \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1466 by (simp add: hoare_liftME_subst) 1467 1468(* FIXME: Move *) 1469lemma o_const_simp[simp]: "(\<lambda>x. C) \<circ> f = (\<lambda>x. C)" 1470 by (simp add: o_def) 1471 1472lemma hoare_vcg_split_case_option: 1473 "\<lbrakk> \<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>; 1474 \<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow> 1475 \<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and> 1476 (\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace> 1477 case x of None \<Rightarrow> f x 1478 | Some y \<Rightarrow> g x y 1479 \<lbrace>R x\<rbrace>" 1480 apply(simp add:valid_def split_def) 1481 apply(case_tac x, simp_all) 1482done 1483 1484lemma hoare_vcg_split_case_optionE: 1485 assumes none_case: "\<And>x. x = None \<Longrightarrow> \<lbrace>P x\<rbrace> f x \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace>" 1486 assumes some_case: "\<And>x y. x = Some y \<Longrightarrow> \<lbrace>Q x y\<rbrace> g x y \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace>" 1487 shows "\<lbrace>\<lambda>s. (x = None \<longrightarrow> P x s) \<and> 1488 (\<forall>y. x = Some y \<longrightarrow> Q x y s)\<rbrace> 1489 case x of None \<Rightarrow> f x 1490 | Some y \<Rightarrow> g x y 1491 \<lbrace>R x\<rbrace>,\<lbrace>E x\<rbrace>" 1492 apply(case_tac x, simp_all) 1493 apply(rule none_case, simp) 1494 apply(rule some_case, simp) 1495done 1496 1497lemma hoare_vcg_split_case_sum: 1498 "\<lbrakk> \<And>x a. x = Inl a \<Longrightarrow> \<lbrace>P x a\<rbrace> f x a \<lbrace>R x\<rbrace>; 1499 \<And>x b. x = Inr b \<Longrightarrow> \<lbrace>Q x b\<rbrace> g x b \<lbrace>R x\<rbrace> \<rbrakk> \<Longrightarrow> 1500 \<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P x a s) \<and> 1501 (\<forall>b. x = Inr b \<longrightarrow> Q x b s) \<rbrace> 1502 case x of Inl a \<Rightarrow> f x a 1503 | Inr b \<Rightarrow> g x b 1504 \<lbrace>R x\<rbrace>" 1505 apply(simp add:valid_def split_def) 1506 apply(case_tac x, simp_all) 1507done 1508 1509lemma hoare_vcg_split_case_sumE: 1510 assumes left_case: "\<And>x a. x = Inl a \<Longrightarrow> \<lbrace>P x a\<rbrace> f x a \<lbrace>R x\<rbrace>" 1511 assumes right_case: "\<And>x b. x = Inr b \<Longrightarrow> \<lbrace>Q x b\<rbrace> g x b \<lbrace>R x\<rbrace>" 1512 shows "\<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P x a s) \<and> 1513 (\<forall>b. x = Inr b \<longrightarrow> Q x b s) \<rbrace> 1514 case x of Inl a \<Rightarrow> f x a 1515 | Inr b \<Rightarrow> g x b 1516 \<lbrace>R x\<rbrace>" 1517 apply(case_tac x, simp_all) 1518 apply(rule left_case, simp) 1519 apply(rule right_case, simp) 1520done 1521 1522lemma hoare_vcg_precond_imp: 1523 "\<lbrakk> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>" 1524 by (fastforce simp add:valid_def) 1525 1526lemma hoare_vcg_precond_impE: 1527 "\<lbrakk> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>" 1528 by (fastforce simp add:validE_def2) 1529 1530lemma hoare_seq_ext: 1531 assumes g_valid: "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>" 1532 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>" 1533 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" 1534 apply(insert f_valid g_valid) 1535 apply(blast intro: seq_ext') 1536done 1537 1538lemma hoare_vcg_seqE: 1539 assumes g_valid: "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 1540 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>" 1541 shows "\<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 1542 apply(insert f_valid g_valid) 1543 apply(blast intro: seqE') 1544done 1545 1546lemma hoare_seq_ext_nobind: 1547 "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>; 1548 \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace> \<rbrakk> \<Longrightarrow> 1549 \<lbrace>A\<rbrace> do f; g od \<lbrace>C\<rbrace>" 1550 apply (erule seq_ext) 1551 apply (clarsimp simp: valid_def) 1552 done 1553 1554lemma hoare_seq_ext_nobindE: 1555 "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>; 1556 \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 1557 \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 1558 apply (erule seqE) 1559 apply (clarsimp simp:validE_def) 1560 done 1561 1562lemma hoare_chain: 1563 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; 1564 \<And>s. R s \<Longrightarrow> P s; 1565 \<And>r s. Q r s \<Longrightarrow> S r s \<rbrakk> \<Longrightarrow> 1566 \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>" 1567 by(fastforce simp add:valid_def split_def) 1568 1569lemma validE_weaken: 1570 "\<lbrakk> \<lbrace>P'\<rbrace> A \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<And>r s. Q' r s \<Longrightarrow> Q r s; \<And>r s. E' r s \<Longrightarrow> E r s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> A \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1571 by (fastforce simp: validE_def2 split: sum.splits) 1572 1573lemmas hoare_chainE = validE_weaken 1574 1575lemma hoare_vcg_handle_elseE: 1576 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; 1577 \<And>e. \<lbrace>E e\<rbrace> g e \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>; 1578 \<And>x. \<lbrace>Q x\<rbrace> h x \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace> \<rbrakk> \<Longrightarrow> 1579 \<lbrace>P\<rbrace> f <handle> g <else> h \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>" 1580 apply (simp add: handle_elseE_def validE_def) 1581 apply (rule seq_ext) 1582 apply assumption 1583 apply (simp split: sum.split) 1584 done 1585 1586lemma in_mres: 1587 "(tr, Result (rv, s)) \<in> S \<Longrightarrow> (rv, s) \<in> mres S" 1588 by (fastforce simp: mres_def intro: image_eqI[rotated]) 1589 1590lemma alternative_valid: 1591 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1592 assumes y: "\<lbrace>P\<rbrace> f' \<lbrace>Q\<rbrace>" 1593 shows "\<lbrace>P\<rbrace> f OR f' \<lbrace>Q\<rbrace>" 1594 apply (simp add: valid_def alternative_def mres_def) 1595 using post_by_hoare[OF x _ in_mres] post_by_hoare[OF y _ in_mres] 1596 apply auto 1597 done 1598 1599lemma alternative_wp: 1600 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1601 assumes y: "\<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>" 1602 shows "\<lbrace>P and P'\<rbrace> f OR f' \<lbrace>Q\<rbrace>" 1603 apply (rule alternative_valid) 1604 apply (rule hoare_pre_imp [OF _ x], simp) 1605 apply (rule hoare_pre_imp [OF _ y], simp) 1606 done 1607 1608lemma alternativeE_wp: 1609 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" and y: "\<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1610 shows "\<lbrace>P and P'\<rbrace> f OR f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1611 apply (unfold validE_def) 1612 apply (wp add: x y alternative_wp | simp | fold validE_def)+ 1613 done 1614 1615lemma alternativeE_R_wp: 1616 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f OR f' \<lbrace>Q\<rbrace>,-" 1617 apply (simp add: validE_R_def) 1618 apply (rule alternativeE_wp) 1619 apply assumption+ 1620 done 1621 1622lemma alternative_R_wp: 1623 "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g -,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<sqinter> g -, \<lbrace>Q\<rbrace>" 1624 apply (simp add: validE_E_def) 1625 apply (rule alternativeE_wp) 1626 apply assumption+ 1627 done 1628 1629lemma state_select_wp [wp]: "\<lbrace> \<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t \<rbrace> state_select f \<lbrace> P \<rbrace>" 1630 apply (clarsimp simp: state_select_def assert_def) 1631 apply (rule hoare_weaken_pre) 1632 apply (wp select_wp hoare_vcg_split_if return_wp fail_wp) 1633 apply simp 1634 done 1635 1636lemma condition_wp [wp]: 1637 "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace> P \<rbrace>; \<lbrace> R \<rbrace> B \<lbrace> P \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s. if C s then Q s else R s \<rbrace> condition C A B \<lbrace> P \<rbrace>" 1638 apply (clarsimp simp: condition_def) 1639 apply (clarsimp simp: valid_def pred_conj_def pred_neg_def split_def) 1640 done 1641 1642lemma conditionE_wp [wp]: 1643 "\<lbrakk> \<lbrace> P \<rbrace> A \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>; \<lbrace> P' \<rbrace> B \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s. if C s then P s else P' s \<rbrace> condition C A B \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace>" 1644 apply (clarsimp simp: condition_def) 1645 apply (clarsimp simp: validE_def valid_def) 1646 done 1647 1648lemma state_assert_wp [wp]: "\<lbrace> \<lambda>s. f s \<longrightarrow> P () s \<rbrace> state_assert f \<lbrace> P \<rbrace>" 1649 apply (clarsimp simp: state_assert_def get_def 1650 assert_def bind_def valid_def return_def fail_def mres_def) 1651 done 1652 1653text \<open>The weakest precondition handler which works on conjunction\<close> 1654 1655lemma hoare_vcg_conj_lift: 1656 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1657 assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>" 1658 shows "\<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" 1659 apply (subst bipred_conj_def[symmetric], rule hoare_post_conj) 1660 apply (rule hoare_pre_imp [OF _ x], simp) 1661 apply (rule hoare_pre_imp [OF _ y], simp) 1662 done 1663 1664lemma hoare_vcg_conj_liftE1: 1665 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 1666 \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,\<lbrace>E\<rbrace>" 1667 unfolding valid_def validE_R_def validE_def 1668 apply (clarsimp simp: split_def split: sum.splits) 1669 apply (erule allE, erule (1) impE) 1670 apply (erule allE, erule (1) impE) 1671 apply (drule (1) bspec) 1672 apply (drule (1) bspec) 1673 apply clarsimp 1674 done 1675 1676lemma hoare_vcg_disj_lift: 1677 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1678 assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>" 1679 shows "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>" 1680 apply (simp add: valid_def) 1681 apply safe 1682 apply (erule(1) post_by_hoare [OF x]) 1683 apply (erule notE) 1684 apply (erule(1) post_by_hoare [OF y]) 1685 done 1686 1687lemma hoare_vcg_const_Ball_lift: 1688 "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace>" 1689 by (fastforce simp: valid_def) 1690 1691lemma hoare_vcg_const_Ball_lift_R: 1692 "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,- \<rbrakk> \<Longrightarrow> 1693 \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>,-" 1694 apply (simp add: validE_R_def validE_def) 1695 apply (rule hoare_strengthen_post) 1696 apply (erule hoare_vcg_const_Ball_lift) 1697 apply (simp split: sum.splits) 1698 done 1699 1700lemma hoare_vcg_all_lift: 1701 "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>" 1702 by (fastforce simp: valid_def) 1703 1704lemma hoare_vcg_all_lift_R: 1705 "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, -" 1706 by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified]) 1707 1708lemma hoare_vcg_const_imp_lift: 1709 "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> 1710 \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>" 1711 by (cases P, simp_all add: hoare_vcg_prop) 1712 1713lemma hoare_vcg_const_imp_lift_R: 1714 "(P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,-) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-" 1715 by (fastforce simp: validE_R_def validE_def valid_def split_def split: sum.splits) 1716 1717lemma hoare_weak_lift_imp: 1718 "\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> P' s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> Q rv s\<rbrace>" 1719 by (auto simp add: valid_def split_def) 1720 1721lemma hoare_vcg_ex_lift: 1722 "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>" 1723 by (clarsimp simp: valid_def, blast) 1724 1725lemma hoare_vcg_ex_lift_R1: 1726 "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>, -" 1727 by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits) 1728 1729(* for instantiations *) 1730lemma hoare_triv: "\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>" . 1731lemma hoare_trivE: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" . 1732lemma hoare_trivE_R: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" . 1733lemma hoare_trivR_R: "\<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" . 1734 1735lemma hoare_weaken_preE_E: 1736 "\<lbrakk> \<lbrace>P'\<rbrace> f -,\<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>" 1737 by (fastforce simp add: validE_E_def validE_def valid_def) 1738 1739lemma hoare_vcg_E_conj: 1740 "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> 1741 \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>rv s. E rv s \<and> E' rv s\<rbrace>" 1742 apply (unfold validE_def validE_E_def) 1743 apply (rule hoare_post_imp [OF _ hoare_vcg_conj_lift], simp_all) 1744 apply (case_tac r, simp_all) 1745 done 1746 1747lemma hoare_vcg_E_elim: 1748 "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,- \<rbrakk> 1749 \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1750 by (rule hoare_post_impErr [OF hoare_vcg_E_conj], 1751 (simp add: validE_R_def)+) 1752 1753lemma hoare_vcg_R_conj: 1754 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> 1755 \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,-" 1756 apply (unfold validE_R_def validE_def) 1757 apply (rule hoare_post_imp [OF _ hoare_vcg_conj_lift], simp_all) 1758 apply (case_tac r, simp_all) 1759 done 1760 1761lemma valid_validE: 1762 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace>" 1763 apply (simp add: validE_def) 1764 done 1765 1766lemma valid_validE2: 1767 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q'\<rbrace>; \<And>s. Q' s \<Longrightarrow> Q s; \<And>s. Q' s \<Longrightarrow> E s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>_. E\<rbrace>" 1768 unfolding valid_def validE_def 1769 by (clarsimp split: sum.splits) blast 1770 1771lemma validE_valid: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>" 1772 apply (unfold validE_def) 1773 apply (rule hoare_post_imp) 1774 defer 1775 apply assumption 1776 apply (case_tac r, simp_all) 1777 done 1778 1779lemma valid_validE_R: 1780 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>,-" 1781 by (simp add: validE_R_def hoare_post_impErr [OF valid_validE]) 1782 1783lemma valid_validE_E: 1784 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>\<lambda>rv. Q\<rbrace>" 1785 by (simp add: validE_E_def hoare_post_impErr [OF valid_validE]) 1786 1787lemma validE_validE_R: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<top>\<top>\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 1788 by (simp add: validE_R_def) 1789 1790lemma validE_R_validE: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" 1791 by (simp add: validE_R_def) 1792 1793lemma hoare_post_imp_R: "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; \<And>r s. Q' r s \<Longrightarrow> Q r s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 1794 apply (unfold validE_R_def) 1795 apply (rule hoare_post_impErr, simp+) 1796 done 1797 1798lemma hoare_post_comb_imp_conj: 1799 "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" 1800 apply (rule hoare_pre_imp) 1801 defer 1802 apply (rule hoare_vcg_conj_lift) 1803 apply assumption+ 1804 apply simp 1805 done 1806 1807lemma hoare_vcg_precond_impE_R: "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,-; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 1808 by (unfold validE_R_def, rule hoare_vcg_precond_impE, simp+) 1809 1810(* lemma valid_is_triple: 1811 "valid P f Q = triple_judgement P f (postcondition Q (\<lambda>s f. fst (f s)))" 1812 by (simp add: triple_judgement_def valid_def postcondition_def) 1813 *) 1814 1815lemma validE_is_triple: 1816 "validE P f Q E = triple_judgement P f 1817 (postconditions (\<lambda>s f. (\<forall>(r,s') \<in> {(rv, s'). (Inr rv, s') \<in> (mres (f s))}. Q r s')) 1818 (\<lambda>s f. (\<forall>(r,s') \<in> {(rv, s'). (Inl rv, s') \<in> (mres (f s))}. E r s')))" 1819 apply (simp add: validE_def triple_judgement_def valid_def postcondition_def 1820 postconditions_def split_def split: sum.split) 1821 apply (fastforce elim: image_eqI[rotated]) 1822 done 1823 1824lemma validE_R_is_triple: 1825 "validE_R P f Q = triple_judgement P f 1826 (\<lambda>s f. (\<forall>(r,s') \<in> {(rv, s'). (Inr rv, s') \<in> mres (f s)}. Q r s'))" 1827 by (simp add: validE_R_def validE_is_triple postconditions_def postcondition_def) 1828 1829lemma validE_E_is_triple: 1830 "validE_E P f E = triple_judgement P f 1831 (\<lambda>s f. (\<forall>(r,s') \<in> {(rv, s'). (Inl rv, s') \<in> mres (f s)}. E r s'))" 1832 by (simp add: validE_E_def validE_is_triple postconditions_def postcondition_def) 1833 1834lemmas hoare_wp_combs = 1835 hoare_post_comb_imp_conj hoare_vcg_precond_imp hoare_vcg_conj_lift 1836 1837lemmas hoare_wp_combsE = 1838 hoare_vcg_precond_impE 1839 hoare_vcg_precond_impE_R 1840 validE_validE_R 1841 hoare_vcg_R_conj 1842 hoare_vcg_E_elim 1843 hoare_vcg_E_conj 1844 1845lemmas hoare_wp_state_combsE = 1846 hoare_vcg_precond_impE[OF valid_validE] 1847 hoare_vcg_precond_impE_R[OF valid_validE_R] 1848 valid_validE_R 1849 hoare_vcg_R_conj[OF valid_validE_R] 1850 hoare_vcg_E_elim[OF valid_validE_E] 1851 hoare_vcg_E_conj[OF valid_validE_E] 1852 1853lemmas hoare_wp_splits [wp_split] = 1854 hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp 1855 validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]] 1856 validE_validE_R [OF handleE'_wp [OF validE_R_validE]] 1857 validE_validE_R [OF handleE_wp [OF validE_R_validE]] 1858 catch_wp hoare_vcg_split_if hoare_vcg_split_ifE 1859 validE_validE_R [OF hoare_vcg_split_ifE [OF validE_R_validE validE_R_validE]] 1860 liftM_wp liftME_wp 1861 validE_validE_R [OF liftME_wp [OF validE_R_validE]] 1862 validE_valid 1863 1864lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE hoare_wp_combs 1865 1866lemmas [wp] = hoare_vcg_prop 1867 wp_post_taut 1868 return_wp 1869 put_wp 1870 get_wp 1871 gets_wp 1872 modify_wp 1873 returnOk_wp 1874 throwError_wp 1875 fail_wp 1876 failE_wp 1877 liftE_wp 1878 1879lemmas [wp_trip] = valid_is_triple validE_is_triple validE_E_is_triple validE_R_is_triple 1880 1881 1882text \<open>Simplifications on conjunction\<close> 1883 1884lemma hoare_post_eq: "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1885 by simp 1886lemma hoare_post_eqE1: "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1887 by simp 1888lemma hoare_post_eqE2: "\<lbrakk> E = E'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1889 by simp 1890lemma hoare_post_eqE_R: "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" 1891 by simp 1892 1893lemma pred_conj_apply_elim: "(\<lambda>r. Q r and Q' r) = (\<lambda>r s. Q r s \<and> Q' r s)" 1894 by (simp add: pred_conj_def) 1895lemma pred_conj_conj_elim: "(\<lambda>r s. (Q r and Q' r) s \<and> Q'' r s) = (\<lambda>r s. Q r s \<and> Q' r s \<and> Q'' r s)" 1896 by simp 1897lemma conj_assoc_apply: "(\<lambda>r s. (Q r s \<and> Q' r s) \<and> Q'' r s) = (\<lambda>r s. Q r s \<and> Q' r s \<and> Q'' r s)" 1898 by simp 1899lemma all_elim: "(\<lambda>rv s. \<forall>x. P rv s) = P" 1900 by simp 1901lemma all_conj_elim: "(\<lambda>rv s. (\<forall>x. P rv s) \<and> Q rv s) = (\<lambda>rv s. P rv s \<and> Q rv s)" 1902 by simp 1903 1904lemmas vcg_rhs_simps = pred_conj_apply_elim pred_conj_conj_elim 1905 conj_assoc_apply all_elim all_conj_elim 1906 1907lemma if_apply_reduct: "\<lbrace>P\<rbrace> If P' (f x) (g x) \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> If P' f g x \<lbrace>Q\<rbrace>" 1908 by (cases P', simp_all) 1909lemma if_apply_reductE: "\<lbrace>P\<rbrace> If P' (f x) (g x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> If P' f g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1910 by (cases P', simp_all) 1911lemma if_apply_reductE_R: "\<lbrace>P\<rbrace> If P' (f x) (g x) \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> If P' f g x \<lbrace>Q\<rbrace>,-" 1912 by (cases P', simp_all) 1913 1914lemmas hoare_wp_simps [wp_split] = 1915 vcg_rhs_simps [THEN hoare_post_eq] vcg_rhs_simps [THEN hoare_post_eqE1] 1916 vcg_rhs_simps [THEN hoare_post_eqE2] vcg_rhs_simps [THEN hoare_post_eqE_R] 1917 if_apply_reduct if_apply_reductE if_apply_reductE_R TrueI 1918 1919schematic_goal if_apply_test: "\<lbrace>?Q\<rbrace> (if A then returnOk else K fail) x \<lbrace>P\<rbrace>,\<lbrace>E\<rbrace>" 1920 by wpsimp 1921 1922lemma hoare_elim_pred_conj: 1923 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>" 1924 by (unfold pred_conj_def) 1925 1926lemma hoare_elim_pred_conjE1: 1927 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>,\<lbrace>E\<rbrace>" 1928 by (unfold pred_conj_def) 1929 1930lemma hoare_elim_pred_conjE2: 1931 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>x s. E x s \<and> E' x s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>x. E x and E' x\<rbrace>" 1932 by (unfold pred_conj_def) 1933 1934lemma hoare_elim_pred_conjE_R: 1935 "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>,-" 1936 by (unfold pred_conj_def) 1937 1938lemmas hoare_wp_pred_conj_elims = 1939 hoare_elim_pred_conj hoare_elim_pred_conjE1 1940 hoare_elim_pred_conjE2 hoare_elim_pred_conjE_R 1941 1942lemmas hoare_weaken_preE = hoare_vcg_precond_impE 1943 1944lemmas hoare_pre [wp_pre] = 1945 hoare_weaken_pre 1946 hoare_weaken_preE 1947 hoare_vcg_precond_impE_R 1948 hoare_weaken_preE_E 1949 1950declare no_fail_pre [wp_pre] 1951 1952bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del] 1953 1954text \<open>Miscellaneous lemmas on hoare triples\<close> 1955 1956lemma hoare_vcg_mp: 1957 assumes a: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1958 assumes b: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<longrightarrow> Q' r s\<rbrace>" 1959 shows "\<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>" 1960 using assms 1961 by (auto simp: valid_def split_def) 1962 1963(* note about this precond stuff: rules get a chance to bind directly 1964 before any of their combined forms. As a result, these precondition 1965 implication rules are only used when needed. *) 1966 1967lemma hoare_add_post: 1968 assumes r: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>" 1969 assumes impP: "\<And>s. P s \<Longrightarrow> P' s" 1970 assumes impQ: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> Q rv s\<rbrace>" 1971 shows "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" 1972 apply (rule hoare_chain) 1973 apply (rule hoare_vcg_conj_lift) 1974 apply (rule r) 1975 apply (rule impQ) 1976 apply simp 1977 apply (erule impP) 1978 apply simp 1979 done 1980 1981lemma hoare_whenE_wp: 1982 "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>" 1983 unfolding whenE_def by clarsimp wp 1984 1985lemma hoare_gen_asmE: 1986 "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,-) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>, -" 1987 by (simp add: validE_R_def validE_def valid_def) blast 1988 1989lemma hoare_list_case: 1990 assumes P1: "\<lbrace>P1\<rbrace> f f1 \<lbrace>Q\<rbrace>" 1991 assumes P2: "\<And>y ys. xs = y#ys \<Longrightarrow> \<lbrace>P2 y ys\<rbrace> f (f2 y ys) \<lbrace>Q\<rbrace>" 1992 shows "\<lbrace>case xs of [] \<Rightarrow> P1 | y#ys \<Rightarrow> P2 y ys\<rbrace> 1993 f (case xs of [] \<Rightarrow> f1 | y#ys \<Rightarrow> f2 y ys) 1994 \<lbrace>Q\<rbrace>" 1995 apply (cases xs; simp) 1996 apply (rule P1) 1997 apply (rule P2) 1998 apply simp 1999 done 2000 2001lemma hoare_unless_wp: 2002 "(\<not>P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>if P then R () else Q\<rbrace> unless P f \<lbrace>R\<rbrace>" 2003 unfolding unless_def by wp auto 2004 2005lemma hoare_use_eq: 2006 assumes x: "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s)\<rbrace>" 2007 assumes y: "\<And>f. \<lbrace>\<lambda>s. P f s\<rbrace> m \<lbrace>\<lambda>rv s. Q f s\<rbrace>" 2008 shows "\<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>rv s. Q (f s :: 'c :: type) s \<rbrace>" 2009 apply (rule_tac Q="\<lambda>rv s. \<exists>f'. f' = f s \<and> Q f' s" in hoare_post_imp) 2010 apply simp 2011 apply (wpsimp wp: hoare_vcg_ex_lift x y) 2012 done 2013 2014lemma hoare_return_sp: 2015 "\<lbrace>P\<rbrace> return x \<lbrace>\<lambda>r. P and K (r = x)\<rbrace>" 2016 by (simp add: valid_def return_def mres_def) 2017 2018lemma hoare_fail_any [simp]: 2019 "\<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>" by wp 2020 2021lemma hoare_failE [simp]: "\<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by wp 2022 2023lemma hoare_FalseE [simp]: 2024 "\<lbrace>\<lambda>s. False\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2025 by (simp add: valid_def validE_def) 2026 2027lemma hoare_K_bind [wp]: 2028 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>" 2029 by simp 2030 2031text \<open>Setting up the precondition case splitter.\<close> 2032 2033lemma wpc_helper_valid: 2034 "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>" 2035 by (clarsimp simp: wpc_helper_def elim!: hoare_pre) 2036 2037lemma wpc_helper_validE: 2038 "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>" 2039 by (clarsimp simp: wpc_helper_def elim!: hoare_pre) 2040 2041lemma wpc_helper_validE_R: 2042 "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-" 2043 by (clarsimp simp: wpc_helper_def elim!: hoare_pre) 2044 2045lemma wpc_helper_validR_R: 2046 "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" 2047 by (clarsimp simp: wpc_helper_def elim!: hoare_pre) 2048 2049lemma wpc_helper_no_fail_final: 2050 "no_fail Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (no_fail P f)" 2051 by (clarsimp simp: wpc_helper_def elim!: no_fail_pre) 2052 2053lemma wpc_helper_validNF: 2054 "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace>! \<Longrightarrow> wpc_helper (P, P') (Q, Q') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>!" 2055 apply (clarsimp simp: wpc_helper_def) 2056 by (metis hoare_wp_combs(2) no_fail_pre validNF_def) 2057 2058lemma wpc_helper_validI: 2059 "(\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>) \<Longrightarrow> wpc_helper (P, P') (split Q, Q') (\<lbrace>curry P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>)" 2060 by (clarsimp simp: wpc_helper_def elim!: validI_weaken_pre) 2061 2062wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>" wpc_helper_valid 2063wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" wpc_helper_validE 2064wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,-" wpc_helper_validE_R 2065wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m -,\<lbrace>E\<rbrace>" wpc_helper_validR_R 2066wpc_setup "\<lambda>m. no_fail P m" wpc_helper_no_fail_final 2067wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!" wpc_helper_validNF 2068wpc_setup "\<lambda>m. \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>" wpc_helper_validI 2069 2070lemma in_liftM: 2071 "((r, s') \<in> mres (liftM t f s)) = (\<exists>r'. (r', s') \<in> mres (f s) \<and> r = t r')" 2072 by (simp add: liftM_def in_return in_bind) 2073 2074(* FIXME: eliminate *) 2075lemmas handy_liftM_lemma = in_liftM 2076 2077lemma hoare_fun_app_wp[wp]: 2078 "\<lbrace>P\<rbrace> f' x \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f' $ x \<lbrace>Q'\<rbrace>" 2079 "\<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2080 "\<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,-" 2081 "\<lbrace>P\<rbrace> f x -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f $ x -,\<lbrace>E\<rbrace>" 2082 by simp+ 2083 2084lemma hoare_validE_pred_conj: 2085 "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>f\<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q And R\<rbrace>,\<lbrace>E\<rbrace>" 2086 unfolding valid_def validE_def by (simp add: split_def split: sum.splits) 2087 2088lemma hoare_validE_conj: 2089 "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>f\<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,\<lbrace>E\<rbrace>" 2090 unfolding valid_def validE_def by (simp add: split_def split: sum.splits) 2091 2092lemma hoare_valid_validE: 2093 "\<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. Q\<rbrace>,\<lbrace>\<lambda>r. Q\<rbrace>" 2094 unfolding valid_def validE_def by (simp add: split_def split: sum.splits) 2095 2096lemma liftE_validE_E [wp]: 2097 "\<lbrace>\<top>\<rbrace> liftE f -, \<lbrace>Q\<rbrace>" 2098 by (clarsimp simp: validE_E_def valid_def) 2099 2100lemma validE_validE_E [wp_comb]: 2101 "\<lbrace>P\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>" 2102 by (simp add: validE_E_def) 2103 2104lemma validE_E_validE: 2105 "\<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<top>\<top>\<rbrace>, \<lbrace>E\<rbrace>" 2106 by (simp add: validE_E_def) 2107 2108(* 2109 * if_validE_E: 2110 * 2111 * \<lbrakk>?P1 \<Longrightarrow> \<lbrace>?Q1\<rbrace> ?f1 -, \<lbrace>?E\<rbrace>; \<not> ?P1 \<Longrightarrow> \<lbrace>?R1\<rbrace> ?g1 -, \<lbrace>?E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (?P1 \<longrightarrow> ?Q1 s) \<and> (\<not> ?P1 \<longrightarrow> ?R1 s)\<rbrace> if ?P1 then ?f1 else ?g1 -, \<lbrace>?E\<rbrace> 2112 *) 2113lemmas if_validE_E [wp_split] = 2114 validE_validE_E [OF hoare_vcg_split_ifE [OF validE_E_validE validE_E_validE]] 2115 2116lemma returnOk_E [wp]: 2117 "\<lbrace>\<top>\<rbrace> returnOk r -, \<lbrace>Q\<rbrace>" 2118 by (simp add: validE_E_def) wp 2119 2120lemma hoare_drop_imp: 2121 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>" 2122 by (auto simp: valid_def) 2123 2124lemma hoare_drop_impE: 2125 "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q s\<rbrace>, \<lbrace>E\<rbrace>" 2126 by (simp add: validE_weaken) 2127 2128lemma hoare_drop_impE_R: 2129 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>, -" 2130 by (auto simp: validE_R_def validE_def valid_def split_def split: sum.splits) 2131 2132lemma hoare_drop_impE_E: 2133 "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>\<lambda>r s. R r s \<longrightarrow> Q r s\<rbrace>" 2134 by (auto simp: validE_E_def validE_def valid_def split_def split: sum.splits) 2135 2136lemmas hoare_drop_imps = hoare_drop_imp hoare_drop_impE_R hoare_drop_impE_E 2137lemma mres_union: 2138 "mres (a \<union> b) = mres a \<union> mres b" 2139 by (simp add: mres_def image_Un) 2140 2141lemma mres_Failed_empty: 2142 "mres ((\<lambda>xs. (xs, Failed)) ` X ) = {}" 2143 "mres ((\<lambda>xs. (xs, Incomplete)) ` X ) = {}" 2144 by (auto simp add: mres_def image_def) 2145 2146lemma det_set_option_eq: 2147 "(\<Union>a\<in>m. set_option (snd a)) = {(r, s')} \<Longrightarrow> 2148 (ts, Some (rr, ss)) \<in> m \<Longrightarrow> rr = r \<and> ss = s'" 2149 by (metis UN_I option.set_intros prod.inject singleton_iff snd_conv) 2150 2151lemma det_set_option_eq': 2152 "(\<Union>a\<in>m. set_option (snd a)) = {(r, s')} \<Longrightarrow> 2153 Some (r, s') \<in> snd ` m" 2154 using image_iff by fastforce 2155 2156lemma bind_det_exec: 2157 "mres (a s) = {(r,s')} \<Longrightarrow> mres ((a >>= b) s) = mres (b r s')" 2158 by (simp add: in_bind set_eq_iff) 2159 2160lemma in_bind_det_exec: 2161 "mres (a s) = {(r,s')} \<Longrightarrow> (s'' \<in> mres ((a >>= b) s)) = (s'' \<in> mres (b r s'))" 2162 by (cases s'', simp add: in_bind) 2163 2164lemma exec_put: 2165 "(put s' >>= m) s = m () s'" 2166 by (auto simp add: bind_def put_def mres_def split_def) 2167 2168lemma bind_execI: 2169 "\<lbrakk> (r'',s'') \<in> mres (f s); \<exists>x \<in> mres (g r'' s''). P x \<rbrakk> \<Longrightarrow> 2170 \<exists>x \<in> mres ((f >>= g) s). P x" 2171 by (fastforce simp add: Bex_def in_bind) 2172 2173lemma True_E_E [wp]: "\<lbrace>\<top>\<rbrace> f -,\<lbrace>\<top>\<top>\<rbrace>" 2174 by (auto simp: validE_E_def validE_def valid_def split: sum.splits) 2175 2176(* 2177 * \<lbrakk>\<And>x. \<lbrace>?B1 x\<rbrace> ?g1 x -, \<lbrace>?E\<rbrace>; \<lbrace>?P\<rbrace> ?f1 \<lbrace>?B1\<rbrace>, \<lbrace>?E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f1 >>=E ?g1 -, \<lbrace>?E\<rbrace> 2178 *) 2179lemmas [wp_split] = 2180 validE_validE_E [OF hoare_vcg_seqE [OF validE_E_validE]] 2181 2182lemma case_option_wp: 2183 assumes x: "\<And>x. \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>" 2184 assumes y: "\<lbrace>P'\<rbrace> m' \<lbrace>Q\<rbrace>" 2185 shows "\<lbrace>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s)\<rbrace> 2186 case_option m' m x \<lbrace>Q\<rbrace>" 2187 apply (cases x; simp) 2188 apply (rule y) 2189 apply (rule x) 2190 done 2191 2192lemma case_option_wpE: 2193 assumes x: "\<And>x. \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2194 assumes y: "\<lbrace>P'\<rbrace> m' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2195 shows "\<lbrace>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s)\<rbrace> 2196 case_option m' m x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 2197 apply (cases x; simp) 2198 apply (rule y) 2199 apply (rule x) 2200 done 2201 2202lemma in_bindE: 2203 "(rv, s') \<in> mres ((f >>=E (\<lambda>rv'. g rv')) s) = 2204 ((\<exists>ex. rv = Inl ex \<and> (Inl ex, s') \<in> mres (f s)) \<or> 2205 (\<exists>rv' s''. (rv, s') \<in> mres (g rv' s'') \<and> (Inr rv', s'') \<in> mres (f s)))" 2206 apply (clarsimp simp: bindE_def in_bind lift_def in_throwError) 2207 apply (safe del: disjCI; strengthen subst[where P="\<lambda>x. x \<in> mres (f s)", mk_strg I _ E]; 2208 auto simp: in_throwError split: sum.splits) 2209 done 2210 2211(* 2212 * \<lbrace>?P\<rbrace> ?m1 -, \<lbrace>?E\<rbrace> \<Longrightarrow> \<lbrace>?P\<rbrace> liftME ?f1 ?m1 -, \<lbrace>?E\<rbrace> 2213 *) 2214lemmas [wp_split] = validE_validE_E [OF liftME_wp, simplified, OF validE_E_validE] 2215 2216lemma assert_A_True[simp]: "assert True = return ()" 2217 by (simp add: assert_def) 2218 2219lemma assert_wp [wp]: "\<lbrace>\<lambda>s. P \<longrightarrow> Q () s\<rbrace> assert P \<lbrace>Q\<rbrace>" 2220 by (cases P, (simp add: assert_def | wp)+) 2221 2222lemma list_cases_wp: 2223 assumes a: "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>" 2224 assumes b: "\<And>x xs. ts = x#xs \<Longrightarrow> \<lbrace>P_B x xs\<rbrace> b x xs \<lbrace>Q\<rbrace>" 2225 shows "\<lbrace>case_list P_A P_B ts\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>" 2226 by (cases ts, auto simp: a b) 2227 2228(* FIXME: make wp *) 2229lemma whenE_throwError_wp: 2230 "\<lbrace>\<lambda>s. \<not>Q \<longrightarrow> P s\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv. P\<rbrace>, -" 2231 unfolding whenE_def by wp blast 2232 2233lemma select_throwError_wp: 2234 "\<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select S >>= throwError -, \<lbrace>Q\<rbrace>" 2235 by (clarsimp simp add: bind_def throwError_def return_def select_def validE_E_def 2236 validE_def valid_def mres_def) 2237 2238 2239section "validNF Rules" 2240 2241subsection "Basic validNF theorems" 2242 2243lemma validNF [intro?]: 2244 "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!" 2245 by (clarsimp simp: validNF_def) 2246 2247lemma validNF_valid: "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>" 2248 by (clarsimp simp: validNF_def) 2249 2250lemma validNF_no_fail: "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f" 2251 by (clarsimp simp: validNF_def) 2252 2253lemma snd_validNF: 2254 "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Failed \<notin> snd ` (f s)" 2255 by (clarsimp simp: validNF_def no_fail_def) 2256 2257lemma use_validNF: 2258 "\<lbrakk> (r', s') \<in> mres (f s); \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Q r' s'" 2259 by (fastforce simp: validNF_def valid_def) 2260 2261subsection "validNF weakest pre-condition rules" 2262 2263lemma validNF_return [wp]: 2264 "\<lbrace> P x \<rbrace> return x \<lbrace> P \<rbrace>!" 2265 by (wp validNF)+ 2266 2267lemma validNF_get [wp]: 2268 "\<lbrace> \<lambda>s. P s s \<rbrace> get \<lbrace> P \<rbrace>!" 2269 by (wp validNF)+ 2270 2271lemma validNF_put [wp]: 2272 "\<lbrace> \<lambda>s. P () x \<rbrace> put x \<lbrace> P \<rbrace>!" 2273 by (wp validNF)+ 2274 2275lemma validNF_K_bind [wp]: 2276 "\<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> K_bind x f \<lbrace> Q \<rbrace>!" 2277 by simp 2278 2279lemma validNF_fail [wp]: 2280 "\<lbrace> \<lambda>s. False \<rbrace> fail \<lbrace> Q \<rbrace>!" 2281 by (clarsimp simp: validNF_def fail_def no_fail_def) 2282 2283lemma validNF_prop [wp_unsafe]: 2284 "\<lbrakk> no_fail (\<lambda>s. P) f \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s. P \<rbrace> f \<lbrace> \<lambda>rv s. P \<rbrace>!" 2285 by (wp validNF)+ 2286 2287lemma validNF_post_conj [intro!]: 2288 "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>!; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>!" 2289 by (clarsimp simp: validNF_def) 2290 2291lemma no_fail_or: 2292 "\<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a" 2293 by (clarsimp simp: no_fail_def) 2294 2295lemma validNF_pre_disj [intro!]: 2296 "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>!; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>!" 2297 by (rule validNF) (auto dest: validNF_valid validNF_no_fail intro: no_fail_or) 2298 2299(* 2300 * Set up combination rules for WP, which also requires 2301 * a "wp_trip" rule for validNF. 2302 *) 2303 2304definition "validNF_property Q s b \<equiv> Failed \<notin> snd ` (b s) \<and> (\<forall>(r', s') \<in> mres (b s). Q r' s')" 2305 2306lemma validNF_is_triple [wp_trip]: 2307 "validNF P f Q = triple_judgement P f (validNF_property Q)" 2308 apply (clarsimp simp: validNF_def triple_judgement_def validNF_property_def) 2309 apply (auto simp: no_fail_def valid_def) 2310 done 2311 2312lemma validNF_weaken_pre [wp_comb]: 2313 "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!" 2314 by (metis hoare_pre_imp no_fail_pre validNF_def) 2315 2316lemma validNF_post_comb_imp_conj: 2317 "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!" 2318 by (fastforce simp: validNF_def valid_def) 2319 2320lemma validNF_post_comb_conj_L: 2321 "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!" 2322 apply (clarsimp simp: validNF_def valid_def no_fail_def) 2323 apply force 2324 done 2325 2326lemma validNF_post_comb_conj_R: 2327 "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!" 2328 apply (clarsimp simp: validNF_def valid_def no_fail_def) 2329 apply force 2330 done 2331 2332lemma validNF_post_comb_conj: 2333 "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!" 2334 apply (clarsimp simp: validNF_def valid_def no_fail_def) 2335 apply force 2336 done 2337 2338lemma validNF_split_if [wp_split]: 2339 "\<lbrakk>P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>!; \<not> P \<Longrightarrow> \<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)\<rbrace> if P then f else g \<lbrace>S\<rbrace>!" 2340 by simp 2341 2342lemma validNF_vcg_conj_lift: 2343 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> 2344 \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>!" 2345 apply (subst bipred_conj_def[symmetric], rule validNF_post_conj) 2346 apply (erule validNF_weaken_pre, fastforce) 2347 apply (erule validNF_weaken_pre, fastforce) 2348 done 2349 2350lemma validNF_vcg_disj_lift: 2351 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>! \<rbrakk> \<Longrightarrow> 2352 \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>!" 2353 apply (clarsimp simp: validNF_def) 2354 apply safe 2355 apply (auto intro!: hoare_vcg_disj_lift)[1] 2356 apply (clarsimp simp: no_fail_def) 2357 done 2358 2359lemma validNF_vcg_all_lift [wp]: 2360 "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>!" 2361 apply atomize 2362 apply (rule validNF) 2363 apply (clarsimp simp: validNF_def) 2364 apply (rule hoare_vcg_all_lift) 2365 apply force 2366 apply (clarsimp simp: no_fail_def validNF_def) 2367 done 2368 2369lemma no_fail_bind[wp_split]: 2370 "\<lbrakk> no_fail P f; \<And>x. no_fail (R x) (g x); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> 2371 \<Longrightarrow> no_fail (P and Q) (do x \<leftarrow> f; g x od)" 2372 apply (simp add: no_fail_def bind_def2 image_Un image_image 2373 in_image_constant) 2374 apply (intro allI conjI impI) 2375 apply (fastforce simp: image_def) 2376 apply clarsimp 2377 apply (drule(1) post_by_hoare, erule in_mres) 2378 apply (fastforce simp: image_def) 2379 done 2380 2381lemma validNF_bind [wp_split]: 2382 "\<lbrakk> \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>! \<rbrakk> \<Longrightarrow> 2383 \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>!" 2384 apply (rule validNF) 2385 apply (metis validNF_valid hoare_seq_ext) 2386 apply (frule no_fail_bind[OF validNF_no_fail, where g=g]) 2387 apply (rule validNF_no_fail, assumption) 2388 apply (erule validNF_valid) 2389 apply (simp add: no_fail_def) 2390 done 2391 2392lemmas validNF_seq_ext = validNF_bind 2393 2394subsection "validNF compound rules" 2395lemma validNF_state_assert [wp]: 2396 "\<lbrace> \<lambda>s. P () s \<and> G s \<rbrace> state_assert G \<lbrace> P \<rbrace>!" 2397 apply (rule validNF) 2398 apply wpsimp 2399 apply (clarsimp simp: no_fail_def state_assert_def 2400 bind_def2 assert_def return_def get_def) 2401 done 2402 2403lemma validNF_modify [wp]: 2404 "\<lbrace> \<lambda>s. P () (f s) \<rbrace> modify f \<lbrace> P \<rbrace>!" 2405 apply (clarsimp simp: modify_def) 2406 apply wp 2407 done 2408 2409lemma validNF_gets [wp]: 2410 "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>!" 2411 apply (clarsimp simp: gets_def) 2412 apply wp 2413 done 2414 2415lemma validNF_condition [wp]: 2416 "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>!" 2417 apply rule 2418 apply (drule validNF_valid)+ 2419 apply (erule (1) condition_wp) 2420 apply (drule validNF_no_fail)+ 2421 apply (clarsimp simp: no_fail_def condition_def) 2422 done 2423 2424lemma validNF_alt_def: 2425 "validNF P m Q = (\<forall>s. P s \<longrightarrow> ((\<forall>(r', s') \<in> mres (m s). Q r' s') \<and> Failed \<notin> snd ` (m s)))" 2426 by (auto simp: validNF_def valid_def no_fail_def mres_def image_def) 2427 2428lemma validNF_assert [wp]: 2429 "\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!" 2430 apply (rule validNF) 2431 apply (clarsimp simp: valid_def in_return) 2432 apply (clarsimp simp: no_fail_def return_def) 2433 done 2434 2435lemma validNF_false_pre: 2436 "\<lbrace> \<lambda>_. False \<rbrace> P \<lbrace> Q \<rbrace>!" 2437 by (clarsimp simp: validNF_def no_fail_def) 2438 2439lemma validNF_chain: 2440 "\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r s. R' r s \<Longrightarrow> R r s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!" 2441 by (fastforce simp: validNF_def valid_def no_fail_def Ball_def) 2442 2443lemma validNF_case_prod [wp]: 2444 "\<lbrakk> \<And>x y. validNF (P x y) (B x y) Q \<rbrakk> \<Longrightarrow> validNF (case_prod P v) (case_prod (\<lambda>x y. B x y) v) Q" 2445 by (metis prod.exhaust split_conv) 2446 2447lemma validE_NF_case_prod [wp]: 2448 "\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> 2449 \<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!" 2450 apply (clarsimp simp: validE_NF_alt_def) 2451 apply (erule validNF_case_prod) 2452 done 2453 2454lemma no_fail_is_validNF_True: "no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)" 2455 by (clarsimp simp: no_fail_def validNF_def valid_def) 2456 2457subsection "validNF reasoning in the exception monad" 2458 2459lemma validE_NF [intro?]: 2460 "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!" 2461 apply (clarsimp simp: validE_NF_def) 2462 done 2463 2464lemma validE_NF_valid: 2465 "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>" 2466 apply (clarsimp simp: validE_NF_def) 2467 done 2468 2469lemma validE_NF_no_fail: 2470 "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f" 2471 apply (clarsimp simp: validE_NF_def) 2472 done 2473 2474lemma validE_NF_weaken_pre [wp_comb]: 2475 "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!" 2476 apply (clarsimp simp: validE_NF_alt_def) 2477 apply (erule validNF_weaken_pre) 2478 apply simp 2479 done 2480 2481lemma validE_NF_post_comb_conj_L: 2482 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace> E \<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace> E \<rbrace>!" 2483 apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def 2484 valid_def no_fail_def split: sum.splits) 2485 apply force 2486 done 2487 2488lemma validE_NF_post_comb_conj_R: 2489 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace> E \<rbrace>!" 2490 apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def 2491 valid_def no_fail_def split: sum.splits) 2492 apply force 2493 done 2494 2495lemma validE_NF_post_comb_conj: 2496 "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace> E \<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace> E \<rbrace>!" 2497 apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def 2498 valid_def no_fail_def split: sum.splits) 2499 apply force 2500 done 2501 2502lemma validE_NF_chain: 2503 "\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>,\<lbrace>E'\<rbrace>!; 2504 \<And>s. P s \<Longrightarrow> P' s; 2505 \<And>r' s'. R' r' s' \<Longrightarrow> R r' s'; 2506 \<And>r'' s''. E' r'' s'' \<Longrightarrow> E r'' s''\<rbrakk> \<Longrightarrow> 2507 \<lbrace>\<lambda>s. P s \<rbrace> a \<lbrace>\<lambda>r' s'. R r' s'\<rbrace>,\<lbrace>\<lambda>r'' s''. E r'' s''\<rbrace>!" 2508 by (fastforce simp: validE_NF_def validE_def2 no_fail_def Ball_def split: sum.splits) 2509 2510lemma validE_NF_bind_wp [wp]: 2511 "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!" 2512 apply (unfold validE_NF_alt_def bindE_def) 2513 apply (rule validNF_bind [rotated]) 2514 apply assumption 2515 apply (clarsimp simp: lift_def throwError_def split: sum.splits) 2516 apply wpsimp 2517 done 2518 2519lemma validNF_catch [wp]: 2520 "\<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>!" 2521 apply (unfold validE_NF_alt_def catch_def) 2522 apply (rule validNF_bind [rotated]) 2523 apply assumption 2524 apply (clarsimp simp: lift_def throwError_def split: sum.splits) 2525 apply wp 2526 done 2527 2528lemma validNF_throwError [wp]: 2529 "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!" 2530 by (unfold validE_NF_alt_def throwError_def o_def) wpsimp 2531 2532lemma validNF_returnOk [wp]: 2533 "\<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!" 2534 by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp 2535 2536lemma validNF_whenE [wp]: 2537 "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!" 2538 unfolding whenE_def by clarsimp wp 2539 2540lemma validNF_nobindE [wp]: 2541 "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!; 2542 \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> 2543 \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!" 2544 by clarsimp wp 2545 2546(* 2547 * Setup triple rules for validE_NF so that we can use the 2548 * "wp_comb" attribute. 2549 *) 2550 2551definition "validE_NF_property Q E s b \<equiv> Failed \<notin> snd ` (b s) 2552 \<and> (\<forall>(r', s') \<in> mres (b s). case r' of Inl x \<Rightarrow> E x s' | Inr x \<Rightarrow> Q x s')" 2553 2554lemma validE_NF_is_triple [wp_trip]: 2555 "validE_NF P f Q E = triple_judgement P f (validE_NF_property Q E)" 2556 apply (clarsimp simp: validE_NF_def validE_def2 no_fail_def triple_judgement_def 2557 validE_NF_property_def split: sum.splits) 2558 apply blast 2559 done 2560 2561lemmas [wp_comb] = validE_NF_weaken_pre 2562 2563lemma validNF_cong: 2564 "\<lbrakk> \<And>s. P s = P' s; \<And>s. P s \<Longrightarrow> m s = m' s; 2565 \<And>r' s' s. \<lbrakk> P s; (r', s') \<in> mres (m s) \<rbrakk> \<Longrightarrow> Q r' s' = Q' r' s' \<rbrakk> \<Longrightarrow> 2566 (\<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>!) = (\<lbrace> P' \<rbrace> m' \<lbrace> Q' \<rbrace>!)" 2567 by (fastforce simp: validNF_alt_def) 2568 2569lemma validE_NF_liftE [wp]: 2570 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" 2571 by (wpsimp simp: validE_NF_alt_def liftE_def) 2572 2573lemma validE_NF_handleE' [wp]: 2574 "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow> 2575 \<lbrace>P\<rbrace> f <handle2> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" 2576 apply (unfold validE_NF_alt_def handleE'_def) 2577 apply (rule validNF_bind [rotated]) 2578 apply assumption 2579 apply (clarsimp split: sum.splits) 2580 apply wpsimp 2581 done 2582 2583lemma validE_NF_handleE [wp]: 2584 "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow> 2585 \<lbrace>P\<rbrace> f <handle> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" 2586 apply (unfold handleE_def) 2587 apply (metis validE_NF_handleE') 2588 done 2589 2590lemma validE_NF_condition [wp]: 2591 "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!\<rbrakk> 2592 \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!" 2593 apply rule 2594 apply (drule validE_NF_valid)+ 2595 apply wp 2596 apply (drule validE_NF_no_fail)+ 2597 apply (clarsimp simp: no_fail_def condition_def) 2598 done 2599 2600lemma validI_name_pre: 2601 "prefix_closed f \<Longrightarrow> 2602 (\<And>s0 s. P s0 s \<Longrightarrow> \<lbrace>\<lambda>s0' s'. s0' = s0 \<and> s' = s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>) 2603 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 2604 unfolding validI_def 2605 by metis 2606 2607lemma validI_well_behaved': 2608 "prefix_closed f 2609 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G'\<rbrace>,\<lbrace>Q\<rbrace> 2610 \<Longrightarrow> R \<le> R' 2611 \<Longrightarrow> G' \<le> G 2612 \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" 2613 apply (subst validI_def, clarsimp) 2614 apply (clarsimp simp add: rely_def) 2615 apply (drule (2) validI_D) 2616 apply (fastforce simp: rely_cond_def guar_cond_def)+ 2617 done 2618 2619lemmas validI_well_behaved = validI_well_behaved'[unfolded le_fun_def, simplified] 2620 2621text \<open>Strengthen setup.\<close> 2622 2623context strengthen_implementation begin 2624 2625lemma strengthen_hoare [strg]: 2626 "(\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) 2627 \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>)" 2628 by (cases F, auto elim: hoare_strengthen_post) 2629 2630lemma strengthen_validE_R_cong[strg]: 2631 "(\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) 2632 \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -)" 2633 by (cases F, auto intro: hoare_post_imp_R) 2634 2635lemma strengthen_validE_cong[strg]: 2636 "(\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) 2637 \<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)) 2638 \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)" 2639 by (cases F, auto elim: hoare_post_impErr) 2640 2641lemma strengthen_validE_E_cong[strg]: 2642 "(\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)) 2643 \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>)" 2644 by (cases F, auto elim: hoare_post_impErr simp: validE_E_def) 2645 2646lemma strengthen_validI[strg]: 2647 "(\<And>r s0 s. st F (\<longrightarrow>) (Q r s0 s) (Q' r s0 s)) 2648 \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q'\<rbrace>)" 2649 by (cases F, auto elim: validI_strengthen_post) 2650 2651end 2652 2653end 2654