1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory WhileLoopRules
8imports "NonDetMonadVCG"
9begin
10
11section "Well-ordered measures"
12
13(* A version of "measure" that takes any wellorder, instead of
14 * being fixed to "nat". *)
15definition measure' :: "('a \<Rightarrow> 'b::wellorder) => ('a \<times> 'a) set"
16where "measure' = (\<lambda>f. {(a, b). f a < f b})"
17
18lemma in_measure'[simp, code_unfold]:
19    "((x,y) : measure' f) = (f x < f y)"
20  by (simp add:measure'_def)
21
22lemma wf_measure' [iff]: "wf (measure' f)"
23  apply (clarsimp simp: measure'_def)
24  apply (insert wf_inv_image [OF wellorder_class.wf, where f=f])
25  apply (clarsimp simp: inv_image_def)
26  done
27
28lemma wf_wellorder_measure: "wf {(a, b). (M a :: 'a :: wellorder) < M b}"
29  apply (subgoal_tac "wf (inv_image ({(a, b). a < b}) M)")
30   apply (clarsimp simp: inv_image_def)
31  apply (rule wf_inv_image)
32  apply (rule wellorder_class.wf)
33  done
34
35
36section "whileLoop lemmas"
37
38text \<open>
39  The following @{const whileLoop} definitions with additional
40  invariant/variant annotations allow the user to annotate
41  @{const whileLoop} terms with information that can be used
42  by automated tools.
43\<close>
44definition
45  "whileLoop_inv (C :: 'a \<Rightarrow> 'b \<Rightarrow> bool) B x (I :: 'a \<Rightarrow> 'b \<Rightarrow> bool) (R :: (('a \<times> 'b) \<times> ('a \<times> 'b)) set) \<equiv> whileLoop C B x"
46
47definition
48  "whileLoopE_inv (C :: 'a \<Rightarrow> 'b \<Rightarrow> bool) B x (I :: 'a \<Rightarrow> 'b \<Rightarrow> bool) (R :: (('a \<times> 'b) \<times> ('a \<times> 'b)) set) \<equiv> whileLoopE C B x"
49
50lemma whileLoop_add_inv: "whileLoop B C = (\<lambda>x. whileLoop_inv B C x I (measure' M))"
51  by (clarsimp simp: whileLoop_inv_def)
52
53lemma whileLoopE_add_inv: "whileLoopE B C = (\<lambda>x. whileLoopE_inv B C x I (measure' M))"
54  by (clarsimp simp: whileLoopE_inv_def)
55
56subsection "Simple base rules"
57
58lemma whileLoop_terminates_unfold:
59  "\<lbrakk> whileLoop_terminates C B r s; (r', s') \<in> fst (B r s); C r s \<rbrakk>
60        \<Longrightarrow> whileLoop_terminates C B r' s'"
61  apply (erule whileLoop_terminates.cases)
62   apply simp
63  apply force
64  done
65
66lemma snd_whileLoop_first_step: "\<lbrakk> \<not> snd (whileLoop C B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd (B r s)"
67  apply (subst (asm) whileLoop_unroll)
68  apply (clarsimp simp: bind_def condition_def)
69  done
70
71lemma snd_whileLoopE_first_step: "\<lbrakk> \<not> snd (whileLoopE C B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd (B r s)"
72  apply (subgoal_tac "\<lbrakk> \<not> snd (whileLoopE C B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd ((lift B (Inr r)) s)")
73   apply (clarsimp simp: lift_def)
74  apply (unfold whileLoopE_def)
75  apply (erule snd_whileLoop_first_step)
76  apply clarsimp
77  done
78
79lemma snd_whileLoop_unfold:
80      "\<lbrakk> \<not> snd (whileLoop C B r s); C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> \<not> snd (whileLoop C B r' s')"
81  apply (clarsimp simp: whileLoop_def)
82  apply (auto simp: elim: whileLoop_results.cases whileLoop_terminates.cases
83     intro: whileLoop_results.intros whileLoop_terminates.intros)
84  done
85
86lemma snd_whileLoopE_unfold:
87      "\<lbrakk> \<not> snd (whileLoopE C B r s); (Inr r', s') \<in> fst (B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd (whileLoopE C B r' s')"
88  apply (clarsimp simp: whileLoopE_def)
89  apply (drule snd_whileLoop_unfold)
90    apply clarsimp
91   apply (clarsimp simp: lift_def)
92   apply assumption
93  apply (clarsimp simp: lift_def)
94  done
95
96lemma whileLoop_results_cong [cong]:
97  assumes C:  "\<And>r s. C r s = C' r s"
98  and B:"\<And>(r :: 'r) (s :: 's). C' r s \<Longrightarrow> B r s = B' r s"
99  shows "whileLoop_results C B = whileLoop_results C' B'"
100proof -
101  {
102    fix x y C B C' B'
103    have  "\<lbrakk> (x, y) \<in> whileLoop_results C B;
104                 \<And>(r :: 'r) (s :: 's). C r s = C' r s;
105                 \<And>r s. C' r s \<Longrightarrow> B r s = B' r s \<rbrakk>
106               \<Longrightarrow> (x, y) \<in> whileLoop_results C' B'"
107      apply (induct rule: whileLoop_results.induct)
108         apply clarsimp
109        apply clarsimp
110       apply (rule whileLoop_results.intros, auto)[1]
111      apply clarsimp
112      apply (rule whileLoop_results.intros, auto)[1]
113      done
114  }
115
116  thus ?thesis
117    apply -
118    apply (rule set_eqI, rule iffI)
119     apply (clarsimp split: prod.splits)
120     apply (clarsimp simp: C B split: prod.splits)
121    apply (clarsimp split: prod.splits)
122    apply (clarsimp simp: C [symmetric] B [symmetric] split: prod.splits)
123  done
124qed
125
126lemma whileLoop_terminates_cong [cong]:
127  assumes r: "r = r'"
128  and s: "s = s'"
129  and C: "\<And>r s. C r s = C' r s"
130  and B: "\<And>r s. C' r s \<Longrightarrow> B r s = B' r s"
131  shows "whileLoop_terminates C B r s = whileLoop_terminates C' B' r' s'"
132proof (rule iffI)
133  assume T: "whileLoop_terminates C B r s"
134  show "whileLoop_terminates C' B' r' s'"
135    apply (insert T r s)
136    apply (induct arbitrary: r' s' rule: whileLoop_terminates.induct)
137     apply (clarsimp simp: C)
138     apply (erule whileLoop_terminates.intros)
139    apply (clarsimp simp: C B split: prod.splits)
140    apply (rule whileLoop_terminates.intros, assumption)
141    apply (clarsimp simp: C B split: prod.splits)
142    done
143next
144  assume T: "whileLoop_terminates C' B' r' s'"
145  show "whileLoop_terminates C B r s"
146    apply (insert T r s)
147    apply (induct arbitrary: r s rule: whileLoop_terminates.induct)
148     apply (rule whileLoop_terminates.intros)
149     apply (clarsimp simp: C)
150    apply (rule whileLoop_terminates.intros, fastforce simp: C)
151    apply (clarsimp simp: C B split: prod.splits)
152    done
153qed
154
155lemma whileLoop_cong [cong]:
156  "\<lbrakk> \<And>r s. C r s = C' r s; \<And>r s. C r s \<Longrightarrow> B r s = B' r s \<rbrakk> \<Longrightarrow> whileLoop C B = whileLoop C' B'"
157  apply (rule ext, clarsimp simp: whileLoop_def)
158  done
159
160lemma whileLoopE_cong [cong]:
161  "\<lbrakk> \<And>r s. C r s = C' r s ; \<And>r s. C r s \<Longrightarrow> B r s = B' r s \<rbrakk>
162                 \<Longrightarrow> whileLoopE C B = whileLoopE C' B'"
163  apply (clarsimp simp: whileLoopE_def)
164  apply (rule whileLoop_cong [THEN arg_cong])
165    apply (clarsimp split: sum.splits)
166   apply (clarsimp split: sum.splits)
167  apply (clarsimp simp: lift_def throwError_def split: sum.splits)
168  done
169
170lemma whileLoop_terminates_wf:
171    "wf {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and> whileLoop_terminates C B (fst y) (snd y)}"
172  apply (rule wfI [where A="UNIV" and B="{(r, s). whileLoop_terminates C B r s}"])
173   apply clarsimp
174  apply clarsimp
175  apply (erule whileLoop_terminates.induct)
176   apply blast
177  apply blast
178  done
179
180subsection "Basic induction helper lemmas"
181
182lemma whileLoop_results_induct_lemma1:
183    "\<lbrakk> (a, b) \<in> whileLoop_results C B; b = Some (x, y) \<rbrakk> \<Longrightarrow> \<not> C x y"
184    apply (induct rule: whileLoop_results.induct, auto)
185    done
186
187lemma whileLoop_results_induct_lemma1':
188    "\<lbrakk> (a, b) \<in> whileLoop_results C B; a \<noteq> b \<rbrakk> \<Longrightarrow> \<exists>x. a = Some x \<and> C (fst x) (snd x)"
189    apply (induct rule: whileLoop_results.induct, auto)
190    done
191
192lemma whileLoop_results_induct_lemma2 [consumes 1]:
193  "\<lbrakk> (a, b) \<in> whileLoop_results C B;
194     a = Some (x :: 'a \<times> 'b); b = Some y;
195     P x; \<And>s t. \<lbrakk> P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s) \<rbrakk> \<Longrightarrow> P t \<rbrakk> \<Longrightarrow> P y"
196  apply (induct arbitrary: x y rule: whileLoop_results.induct)
197    apply simp
198   apply simp
199  apply atomize
200  apply fastforce
201  done
202
203lemma whileLoop_results_induct_lemma3 [consumes 1]:
204  assumes result: "(Some (r, s), Some (r', s')) \<in> whileLoop_results C B"
205  and inv_start: "I r s"
206  and inv_step: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
207  shows "I r' s'"
208  apply (rule whileLoop_results_induct_lemma2 [where P="case_prod I" and y="(r', s')" and x="(r, s)",
209      simplified case_prod_unfold, simplified])
210      apply (rule result)
211     apply simp
212    apply simp
213   apply fact
214  apply (erule (1) inv_step)
215  apply clarsimp
216  done
217
218subsection "Inductive reasoning about whileLoop results"
219
220lemma in_whileLoop_induct [consumes 1]:
221  assumes in_whileLoop: "(r', s') \<in> fst (whileLoop C B r s)"
222  and init_I: "\<And> r s. \<not> C r s \<Longrightarrow> I r s r s"
223  and step:
224     "\<And>r s r' s' r'' s''.
225        \<lbrakk> C r s; (r', s') \<in> fst (B r s);
226          (r'', s'') \<in> fst (whileLoop C B r' s');
227           I r' s' r'' s'' \<rbrakk> \<Longrightarrow> I r s r'' s''"
228  shows "I r s r' s'"
229proof cases
230  assume "C r s"
231
232  {
233    obtain a where a_def: "a = Some (r, s)"
234      by blast
235    obtain b where b_def: "b = Some (r', s')"
236      by blast
237
238    have "\<lbrakk> (a, b) \<in> whileLoop_results C B; \<exists>x. a = Some x;  \<exists>x. b = Some x \<rbrakk>
239        \<Longrightarrow> I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b))"
240      apply (induct rule: whileLoop_results.induct)
241      apply (auto simp: init_I whileLoop_def intro: step)
242      done
243
244    hence "(Some (r, s), Some (r', s')) \<in> whileLoop_results C B
245                 \<Longrightarrow> I r s r' s'"
246      by (clarsimp simp: a_def b_def)
247   }
248
249   thus ?thesis
250     using in_whileLoop
251     by (clarsimp simp: whileLoop_def)
252next
253  assume "\<not> C r s"
254
255  hence "r' = r \<and> s' = s"
256    using in_whileLoop
257    by (subst (asm) whileLoop_unroll,
258             clarsimp simp: condition_def return_def)
259
260  thus ?thesis
261    by (metis init_I \<open>\<not> C r s\<close>)
262qed
263
264lemma snd_whileLoop_induct [consumes 1]:
265  assumes induct: "snd (whileLoop C B r s)"
266  and terminates: "\<not> whileLoop_terminates C B r s \<Longrightarrow> I r s"
267  and init: "\<And> r s. \<lbrakk> snd (B r s); C r s \<rbrakk> \<Longrightarrow> I r s"
268  and step: "\<And>r s r' s' r'' s''.
269        \<lbrakk> C r s; (r', s') \<in> fst (B r s);
270           snd (whileLoop C B r' s');
271           I r' s' \<rbrakk> \<Longrightarrow> I r s"
272  shows "I r s"
273  apply (insert init induct)
274  apply atomize
275  apply (unfold whileLoop_def)
276  apply clarsimp
277  apply (erule disjE)
278   apply (erule rev_mp)
279   apply (induct "Some (r, s)" "None :: ('a \<times> 'b) option"
280        arbitrary: r s rule: whileLoop_results.induct)
281    apply clarsimp
282   apply clarsimp
283   apply (erule (1) step)
284    apply (clarsimp simp: whileLoop_def)
285   apply clarsimp
286  apply (metis terminates)
287  done
288
289lemma whileLoop_terminatesE_induct [consumes 1]:
290  assumes induct: "whileLoop_terminatesE C B r s"
291  and init: "\<And>r s. \<not> C r s \<Longrightarrow> I r s"
292  and step: "\<And>r s r' s'. \<lbrakk> C r s; \<forall>(v', s') \<in> fst (B r s). case v' of Inl _ \<Rightarrow> True | Inr r' \<Rightarrow> I r' s' \<rbrakk> \<Longrightarrow> I r s"
293  shows "I r s"
294  apply (insert induct)
295  apply (clarsimp simp: whileLoop_terminatesE_def)
296  apply (subgoal_tac "(\<lambda>r s. case (Inr r) of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s) r s")
297   apply simp
298  apply (induction rule: whileLoop_terminates.induct)
299   apply (case_tac r)
300    apply simp
301   apply clarsimp
302   apply (erule init)
303  apply (clarsimp split: sum.splits)
304  apply (rule step)
305   apply simp
306  apply (clarsimp simp: lift_def split: sum.splits)
307  apply force
308  done
309
310subsection "Direct reasoning about whileLoop components"
311
312lemma fst_whileLoop_cond_false:
313  assumes loop_result: "(r', s') \<in> fst (whileLoop C B r s)"
314  shows "\<not> C r' s'"
315  using loop_result
316  by (rule in_whileLoop_induct, auto)
317
318lemma snd_whileLoop:
319  assumes init_I: "I r s"
320      and cond_I: "C r s"
321      and non_term:  "\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<rbrace>
322                                   B r \<exists>\<lbrace> \<lambda>r' s'. C r' s' \<and> I r' s' \<rbrace>"
323      shows "snd (whileLoop C B r s)"
324  apply (clarsimp simp: whileLoop_def)
325  apply (rotate_tac)
326  apply (insert init_I cond_I)
327  apply (induct rule: whileLoop_terminates.induct)
328   apply clarsimp
329  apply (cut_tac r=r in non_term)
330  apply (clarsimp simp: exs_valid_def)
331   apply (subst (asm) (2) whileLoop_results.simps)
332   apply clarsimp
333  apply (insert whileLoop_results.simps)
334  apply fast
335  done
336
337lemma whileLoop_terminates_inv:
338  assumes init_I: "I r s"
339  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>"
340  assumes wf_R: "wf R"
341  shows "whileLoop_terminates C B r s"
342  apply (insert init_I)
343  using wf_R
344  apply (induction "(r, s)" arbitrary: r s)
345  apply atomize
346  apply (subst whileLoop_terminates_simps)
347  apply clarsimp
348  apply (erule use_valid)
349  apply (rule hoare_strengthen_post, rule inv)
350   apply force
351  apply force
352  done
353
354lemma not_snd_whileLoop:
355  assumes init_I: "I r s"
356      and inv_holds: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>!"
357      and wf_R: "wf R"
358      shows "\<not> snd (whileLoop C B r s)"
359proof -
360  {
361    fix x y
362    have "\<lbrakk> (x, y) \<in> whileLoop_results C B; x = Some (r, s); y = None \<rbrakk> \<Longrightarrow> False"
363      apply (insert init_I)
364      apply (induct arbitrary: r s rule: whileLoop_results.inducts)
365         apply simp
366        apply simp
367       apply (insert snd_validNF [OF inv_holds])[1]
368       apply blast
369      apply (drule use_validNF [OF _ inv_holds])
370       apply simp
371      apply clarsimp
372      apply blast
373      done
374  }
375
376  also have "whileLoop_terminates C B r s"
377     apply (rule whileLoop_terminates_inv [where I=I, OF init_I _ wf_R])
378     apply (insert inv_holds)
379     apply (clarsimp simp: validNF_def)
380     done
381
382  ultimately show ?thesis
383     by (clarsimp simp: whileLoop_def, blast)
384qed
385
386lemma valid_whileLoop:
387  assumes first_step: "\<And>s. P r s \<Longrightarrow> I r s"
388      and inv_step: "\<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>"
389      and final_step: "\<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s"
390   shows "\<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
391proof -
392  {
393    fix r' s' s
394    assume inv: "I r s"
395    assume step: "(r', s') \<in> fst (whileLoop C B r s)"
396
397    have "I r' s'"
398     using step inv
399      apply (induct rule: in_whileLoop_induct)
400       apply simp
401      apply (drule use_valid, rule inv_step, auto)
402      done
403  }
404
405  thus ?thesis
406    apply (clarsimp simp: valid_def)
407    apply (drule first_step)
408    apply (rule final_step, simp)
409    apply (metis fst_whileLoop_cond_false)
410    done
411qed
412
413lemma whileLoop_wp:
414  "\<lbrakk> \<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>;
415     \<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s \<rbrakk> \<Longrightarrow>
416  \<lbrace> I r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
417  by (rule valid_whileLoop)
418
419lemma whileLoop_wp_inv [wp]:
420  "\<lbrakk> \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s \<rbrakk>
421      \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoop_inv C B r I M \<lbrace> Q \<rbrace>"
422  apply (clarsimp simp: whileLoop_inv_def)
423  apply (rule valid_whileLoop [where P=I and I=I], auto)
424  done
425
426lemma validE_whileLoopE:
427  "\<lbrakk>\<And>s. P r s \<Longrightarrow> I r s;
428    \<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>,\<lbrace> A \<rbrace>;
429    \<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s
430   \<rbrakk> \<Longrightarrow> \<lbrace> P r \<rbrace> whileLoopE C B r \<lbrace> Q \<rbrace>,\<lbrace> A \<rbrace>"
431  apply (clarsimp simp: whileLoopE_def validE_def)
432  apply (rule valid_whileLoop [where I="\<lambda>r s. (case r of Inl x \<Rightarrow> A x s | Inr x \<Rightarrow> I x s)"
433             and Q="\<lambda>r s. (case r of Inl x \<Rightarrow> A x s | Inr x \<Rightarrow> Q x s)"])
434    apply atomize
435    apply (clarsimp simp: valid_def lift_def split: sum.splits)
436   apply (clarsimp simp: valid_def lift_def split: sum.splits)
437  apply (clarsimp split: sum.splits)
438  done
439
440lemma whileLoopE_wp:
441  "\<lbrakk> \<And>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>, \<lbrace> A \<rbrace>;
442     \<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s \<rbrakk> \<Longrightarrow>
443  \<lbrace> I r \<rbrace> whileLoopE C B r \<lbrace> Q \<rbrace>, \<lbrace> A \<rbrace>"
444  by (rule validE_whileLoopE)
445
446lemma exs_valid_whileLoop:
447 assumes init_T: "\<And>s. P s \<Longrightarrow> T r s"
448    and iter_I: "\<And> r s0.
449         \<lbrace> \<lambda>s. T r s \<and> C r s \<and> s = s0 \<rbrace>
450                B r \<exists>\<lbrace>\<lambda>r' s'. T r' s' \<and> ((r', s'),(r, s0)) \<in> R\<rbrace>"
451    and wf_R: "wf R"
452    and final_I: "\<And>r s. \<lbrakk> T r s; \<not> C r s  \<rbrakk> \<Longrightarrow> Q r s"
453 shows "\<lbrace> P \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>"
454proof (clarsimp simp: exs_valid_def Bex_def)
455  fix s
456  assume "P s"
457
458  {
459    fix x
460    have "T (fst x) (snd x) \<Longrightarrow>
461             \<exists>r' s'. (r', s') \<in> fst (whileLoop C B (fst x) (snd x)) \<and> T r' s'"
462      using wf_R
463      apply induction
464      apply atomize
465      apply (case_tac "C (fst x) (snd x)")
466       apply (subst whileLoop_unroll)
467       apply (clarsimp simp: condition_def bind_def' split: prod.splits)
468       apply (cut_tac ?s0.0=b and r=a in iter_I)
469       apply (clarsimp simp: exs_valid_def)
470       apply blast
471      apply (subst whileLoop_unroll)
472      apply (clarsimp simp: condition_def bind_def' return_def)
473      done
474  }
475
476  thus "\<exists>r' s'. (r', s') \<in> fst (whileLoop C B r s) \<and> Q r' s'"
477    by (metis \<open>P s\<close> fst_conv init_T snd_conv
478                  final_I fst_whileLoop_cond_false)
479qed
480
481lemma empty_fail_whileLoop:
482  assumes body_empty_fail: "\<And>r. empty_fail (B r)"
483  shows "empty_fail (whileLoop C B r)"
484proof -
485  {
486    fix s A
487    assume empty: "fst (whileLoop C B r s) = {}"
488
489    have cond_true: "\<And>x s. fst (whileLoop C B x s) = {} \<Longrightarrow> C x s"
490      apply (subst (asm) whileLoop_unroll)
491      apply (clarsimp simp: condition_def return_def split: if_split_asm)
492      done
493
494    have  "snd (whileLoop C B r s)"
495      apply (rule snd_whileLoop [where I="\<lambda>x s. fst (whileLoop C B x s) = {}"])
496        apply fact
497       apply (rule cond_true, fact)
498      apply (clarsimp simp: exs_valid_def)
499      apply (case_tac "fst (B r s) = {}")
500       apply (metis empty_failD [OF body_empty_fail])
501      apply (subst (asm) whileLoop_unroll)
502      apply (fastforce simp: condition_def bind_def split_def cond_true)
503      done
504   }
505
506  thus ?thesis
507    by (clarsimp simp: empty_fail_def)
508qed
509
510lemma empty_fail_whileLoopE:
511  assumes body_empty_fail: "\<And>r. empty_fail (B r)"
512  shows "empty_fail (whileLoopE C B r)"
513  apply (clarsimp simp: whileLoopE_def)
514  apply (rule empty_fail_whileLoop)
515  apply (insert body_empty_fail)
516  apply (clarsimp simp: empty_fail_def lift_def throwError_def return_def split: sum.splits)
517  done
518
519lemma whileLoop_results_bisim:
520  assumes base: "(a, b) \<in> whileLoop_results C B"
521  and vars1: "Q = (case a of Some (r, s) \<Rightarrow> Some (rt r, st s) | _ \<Rightarrow> None)"
522  and vars2: "R = (case b of Some (r, s) \<Rightarrow> Some (rt r, st s) | _ \<Rightarrow> None)"
523  and inv_init: "case a of Some (r, s) \<Rightarrow> I r s | _ \<Rightarrow> True"
524  and inv_step: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
525  and cond_match: "\<And>r s. I r s \<Longrightarrow> C r s = C' (rt r) (st s)"
526  and fail_step: "\<And>r s. \<lbrakk>C r s; snd (B r s); I r s\<rbrakk>
527          \<Longrightarrow> (Some (rt r, st s), None) \<in> whileLoop_results C' B'"
528  and refine: "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in>  fst (B r s) \<rbrakk>
529                           \<Longrightarrow> (rt r', st s') \<in> fst (B' (rt r) (st s))"
530  shows "(Q, R) \<in> whileLoop_results C' B'"
531  apply (subst vars1)
532  apply (subst vars2)
533  apply (insert base inv_init)
534  apply (induct rule: whileLoop_results.induct)
535    apply clarsimp
536    apply (subst (asm) cond_match)
537     apply (clarsimp simp: option.splits)
538    apply (clarsimp simp: option.splits)
539   apply (clarsimp simp: option.splits)
540   apply (metis fail_step)
541  apply (case_tac z)
542   apply (clarsimp simp: option.splits)
543  apply (metis cond_match inv_step refine whileLoop_results.intros(3))
544   apply (clarsimp simp: option.splits)
545 apply (metis cond_match inv_step refine whileLoop_results.intros(3))
546 done
547
548lemma whileLoop_terminates_liftE:
549  "whileLoop_terminatesE C (\<lambda>r. liftE (B r)) r s = whileLoop_terminates C B r s"
550  apply (subst eq_sym_conv)
551  apply (clarsimp simp: whileLoop_terminatesE_def)
552  apply (rule iffI)
553   apply (erule whileLoop_terminates.induct)
554    apply (rule whileLoop_terminates.intros)
555    apply clarsimp
556   apply (clarsimp simp: split_def)
557   apply (rule whileLoop_terminates.intros(2))
558    apply clarsimp
559   apply (clarsimp simp: liftE_def in_bind return_def lift_def [abs_def]
560               bind_def lift_def throwError_def o_def split: sum.splits
561               cong: sum.case_cong)
562   apply (drule (1) bspec)
563   apply clarsimp
564  apply (subgoal_tac "case (Inr r) of Inl _ \<Rightarrow> True | Inr r \<Rightarrow>
565      whileLoop_terminates (\<lambda>r s. (\<lambda>r s. case r of Inl _ \<Rightarrow> False | Inr v \<Rightarrow> C v s) (Inr r) s)
566           (\<lambda>r. (lift (\<lambda>r. liftE (B r)) (Inr r)) >>= (\<lambda>x. return (theRight x))) r s")
567   apply (clarsimp simp: liftE_def lift_def)
568  apply (erule whileLoop_terminates.induct)
569   apply (clarsimp simp: liftE_def lift_def split: sum.splits)
570   apply (erule whileLoop_terminates.intros)
571  apply (clarsimp simp: liftE_def split: sum.splits)
572  apply (clarsimp simp: bind_def return_def split_def lift_def)
573  apply (erule whileLoop_terminates.intros)
574  apply force
575  done
576
577lemma snd_X_return [simp]:
578     "\<And>A X s. snd ((A >>= (\<lambda>a. return (X a))) s) = snd (A s)"
579  by (clarsimp simp: return_def bind_def split_def)
580
581lemma whileLoopE_liftE:
582  "whileLoopE C (\<lambda>r. liftE (B r)) r = liftE (whileLoop C B r)"
583  apply (rule ext)
584  apply (clarsimp simp: whileLoopE_def)
585  apply (rule prod_eqI)
586   apply (rule set_eqI, rule iffI)
587    apply clarsimp
588    apply (clarsimp simp: in_bind whileLoop_def liftE_def)
589    apply (rule_tac x="b" in exI)
590    apply (rule_tac x="theRight a" in exI)
591    apply (rule conjI)
592     apply (erule whileLoop_results_bisim [where rt=theRight and st="\<lambda>x. x" and I="\<lambda>r s. case r of Inr x \<Rightarrow> True | _ \<Rightarrow> False"],
593        auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1]
594    apply (drule whileLoop_results_induct_lemma2 [where P="\<lambda>(r, s). case r of Inr x \<Rightarrow> True | _ \<Rightarrow> False"] )
595        apply (rule refl)
596       apply (rule refl)
597      apply clarsimp
598     apply (clarsimp simp: return_def bind_def lift_def split: sum.splits)
599    apply (clarsimp simp: return_def bind_def lift_def split: sum.splits)
600   apply (clarsimp simp: in_bind whileLoop_def liftE_def)
601   apply (erule whileLoop_results_bisim [where rt=Inr and st="\<lambda>x. x" and I="\<lambda>r s. True"],
602     auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def split: sum.splits)[1]
603  apply (rule iffI)
604   apply (clarsimp simp: whileLoop_def liftE_def del: notI)
605   apply (erule disjE)
606    apply (erule whileLoop_results_bisim [where rt=theRight and st="\<lambda>x. x" and I="\<lambda>r s. case r of Inr x \<Rightarrow> True | _ \<Rightarrow> False"],
607      auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1]
608   apply (subst (asm) whileLoop_terminates_liftE [symmetric])
609   apply (fastforce simp: whileLoop_def liftE_def whileLoop_terminatesE_def)
610  apply (clarsimp simp: whileLoop_def liftE_def del: notI)
611  apply (subst (asm) whileLoop_terminates_liftE [symmetric])
612  apply (clarsimp simp: whileLoop_def liftE_def whileLoop_terminatesE_def)
613  apply (erule disjE)
614   apply (erule whileLoop_results_bisim [where rt=Inr and st="\<lambda>x. x" and I="\<lambda>r s. True"])
615         apply (clarsimp split: option.splits)
616        apply (clarsimp split: option.splits)
617       apply (clarsimp split: option.splits)
618      apply (auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def split: sum.splits)
619  done
620
621lemma validNF_whileLoop:
622  assumes pre: "\<And>s. P r s \<Longrightarrow> I r s"
623  and inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>!"
624  and wf: "wf R"
625  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
626  shows "\<lbrace>P r\<rbrace> whileLoop C B r \<lbrace>Q\<rbrace>!"
627  apply rule
628   apply (rule valid_whileLoop)
629     apply fact
630    apply (insert inv, clarsimp simp: validNF_def
631        valid_def split: prod.splits, force)[1]
632   apply (metis post_cond)
633  apply (unfold no_fail_def)
634  apply (intro allI impI)
635  apply (rule not_snd_whileLoop [where I=I and R=R])
636    apply (auto intro: assms)
637  done
638
639lemma validNF_whileLoop_inv [wp]:
640  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>!"
641  and wf: "wf R"
642  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
643  shows "\<lbrace>I r\<rbrace> whileLoop_inv C B r I R \<lbrace>Q\<rbrace>!"
644  apply (clarsimp simp: whileLoop_inv_def)
645  apply (rule validNF_whileLoop [where I=I and R=R])
646     apply simp
647    apply (rule inv)
648   apply (rule wf)
649  apply (metis post_cond)
650  done
651
652lemma validNF_whileLoop_inv_measure [wp]:
653  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> M r' s' < M r s \<rbrace>!"
654  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
655  shows "\<lbrace>I r\<rbrace> whileLoop_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>!"
656  apply (clarsimp simp: whileLoop_inv_def)
657    apply (rule validNF_whileLoop [where R="measure' (\<lambda>(r, s). M r s)" and I=I])
658     apply simp
659    apply clarsimp
660    apply (rule inv)
661   apply simp
662  apply (metis post_cond)
663  done
664
665lemma validNF_whileLoop_inv_measure_twosteps:
666  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<rbrace>!"
667  assumes measure: "\<And>r m. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> M r s = m \<rbrace> B r \<lbrace> \<lambda>r' s'. M r' s' < m \<rbrace>"
668  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
669  shows "\<lbrace>I r\<rbrace> whileLoop_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>!"
670  apply (rule validNF_whileLoop_inv_measure)
671   apply (rule validNF_weaken_pre)
672    apply (rule validNF_post_comb_conj_L)
673     apply (rule inv)
674    apply (rule measure)
675   apply fast
676  apply (metis post_cond)
677  done
678
679lemma wf_custom_measure:
680  "\<lbrakk> \<And>a b. (a, b) \<in> R \<Longrightarrow> f a < (f :: 'a \<Rightarrow> nat) b \<rbrakk> \<Longrightarrow>  wf R"
681  by (metis in_measure wf_def wf_measure)
682
683lemma validNF_whileLoopE:
684  assumes pre: "\<And>s. P r s \<Longrightarrow> I r s"
685  and inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>,\<lbrace> E \<rbrace>!"
686  and wf: "wf R"
687  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
688  shows "\<lbrace> P r \<rbrace> whileLoopE C B r \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!"
689  apply (unfold validE_NF_alt_def whileLoopE_def)
690   apply (rule validNF_whileLoop [
691     where I="\<lambda>r s. case r of Inl x \<Rightarrow> E x s | Inr x \<Rightarrow> I x s"
692     and R="{((r', s'), (r, s)). \<exists>x x'. r' = Inl x' \<and> r = Inr x}
693     \<union> {((r', s'), (r, s)). \<exists>x x'. r' = Inr x' \<and> r = Inr x \<and> ((x', s'),(x, s)) \<in> R}"])
694     apply (simp add: pre)
695    apply (insert inv)[1]
696    apply (fastforce simp: lift_def validNF_def valid_def
697           validE_NF_def throwError_def no_fail_def return_def
698           validE_def split: sum.splits prod.splits)
699   apply (rule wf_Un)
700     apply (rule wf_custom_measure [where f="\<lambda>(r, s). case r of Inl _ \<Rightarrow> 0 | _ \<Rightarrow> 1"])
701     apply clarsimp
702    apply (insert wf_inv_image [OF wf, where f="\<lambda>(r, s). (theRight r, s)"])
703    apply (drule wf_Int1 [where r'="{((r', s'),(r, s)). (\<exists>x. r = Inr x) \<and> (\<exists>x. r' = Inr x)}"])
704    apply (erule wf_subset)
705    apply rule
706    apply (clarsimp simp: inv_image_def split: prod.splits sum.splits)
707   apply clarsimp
708   apply rule
709    apply rule
710    apply clarsimp
711   apply clarsimp
712  apply (clarsimp split: sum.splits)
713  apply (blast intro: post_cond)
714  done
715
716lemma validNF_whileLoopE_inv [wp]:
717  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>,\<lbrace> E \<rbrace>!"
718  and wf_R: "wf R"
719  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
720  shows "\<lbrace>I r\<rbrace> whileLoopE_inv C B r I R \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
721  apply (clarsimp simp: whileLoopE_inv_def)
722  apply (metis validNF_whileLoopE [OF _ inv] post_cond wf_R)
723  done
724
725lemma validNF_whileLoopE_inv_measure [wp]:
726  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> M r' s' < M r s \<rbrace>, \<lbrace> E \<rbrace>!"
727  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
728  shows "\<lbrace>I r\<rbrace> whileLoopE_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!"
729  apply (rule validNF_whileLoopE_inv)
730    apply clarsimp
731    apply (rule inv)
732   apply clarsimp
733  apply (metis post_cond)
734  done
735
736lemma validNF_whileLoopE_inv_measure_twosteps:
737  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<rbrace>, \<lbrace> E \<rbrace>!"
738  assumes measure: "\<And>r m. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> M r s = m \<rbrace> B r \<lbrace> \<lambda>r' s'. M r' s' < m \<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace>"
739  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
740  shows "\<lbrace>I r\<rbrace> whileLoopE_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
741  apply (rule validNF_whileLoopE_inv_measure)
742   apply (rule validE_NF_weaken_pre)
743    apply (rule validE_NF_post_comb_conj_L)
744     apply (rule inv)
745    apply (rule measure)
746   apply fast
747  apply (metis post_cond)
748  done
749
750lemma whileLoopE_wp_inv [wp]:
751  "\<lbrakk> \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>,\<lbrace>E\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s \<rbrakk>
752      \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoopE_inv C B r I M \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>"
753  apply (clarsimp simp: whileLoopE_inv_def)
754  apply (rule validE_whileLoopE [where I=I], auto)
755  done
756
757subsection "Stronger whileLoop rules"
758
759lemma whileLoop_rule_strong:
760  assumes init_U: "\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. (r, s) \<in> fst Q \<rbrace>"
761  and path_exists: "\<And>r'' s''. \<lbrakk> (r'', s'') \<in> fst Q \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> \<lambda>r s. r = r'' \<and> s = s'' \<rbrace>"
762  and loop_fail: "snd Q \<Longrightarrow> snd (whileLoop C B r s)"
763  and loop_nofail: "\<not> snd Q \<Longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>_ _. True \<rbrace>!"
764  shows "whileLoop C B r s = Q"
765  using assms
766  apply atomize
767  apply (clarsimp simp: valid_def exs_valid_def validNF_def no_fail_def)
768  apply rule
769    apply blast
770   apply blast
771  apply blast
772  done
773
774lemma whileLoop_rule_strong_no_fail:
775  assumes init_U: "\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. (r, s) \<in> fst Q \<rbrace>!"
776  and path_exists: "\<And>r'' s''. \<lbrakk> (r'', s'') \<in> fst Q \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> \<lambda>r s. r = r'' \<and> s = s'' \<rbrace>"
777  and loop_no_fail: "\<not> snd Q"
778  shows "whileLoop C B r s = Q"
779  apply (rule whileLoop_rule_strong)
780     apply (metis init_U validNF_valid)
781    apply (metis path_exists)
782   apply (metis loop_no_fail)
783  apply (metis (lifting, no_types) init_U validNF_chain)
784  done
785
786subsection "Miscellaneous rules"
787
788(* Failure of one whileLoop implies the failure of another whileloop
789 * which will only ever fail more. *)
790lemma snd_whileLoop_subset:
791    assumes a_fails: "snd (whileLoop C A r s)"
792    and b_success_step:
793        "\<And>r s r' s'. \<lbrakk> C r s; (r', s') \<in> fst (A r s); \<not> snd (B r s) \<rbrakk>
794             \<Longrightarrow> (r', s') \<in> fst (B r s)"
795    and b_fail_step: "\<And>r s. \<lbrakk> C r s; snd (A r s) \<rbrakk> \<Longrightarrow> snd (B r s) "
796   shows "snd (whileLoop C B r s)"
797  apply (insert a_fails)
798  apply (induct rule: snd_whileLoop_induct)
799    apply (unfold whileLoop_def snd_conv)[1]
800    apply (rule disjCI, simp)
801    apply rotate_tac
802    apply (induct rule: whileLoop_terminates.induct)
803     apply (subst (asm) whileLoop_terminates.simps)
804     apply simp
805    apply (subst (asm) (3) whileLoop_terminates.simps, clarsimp)
806    apply (subst whileLoop_results.simps, clarsimp)
807    apply (rule classical)
808    apply (frule b_success_step, assumption, simp)
809    apply (drule (1) bspec)
810    apply clarsimp
811   apply (frule (1) b_fail_step)
812   apply (metis snd_whileLoop_first_step)
813  apply (metis b_success_step snd_whileLoop_first_step snd_whileLoop_unfold)
814  done
815
816end
817