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