1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8 * This is a purely theoretical theory containing proofs
9 * that the whileLoop rules in "WhileLoopRules" are complete.
10 *
11 * You probably don't care about this.
12 *)
13theory WhileLoopRulesCompleteness
14imports WhileLoopRules
15begin
16
17lemma whileLoop_rule_strong_complete:
18  "(\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. (r, s) \<in> fst Q \<rbrace>
19        \<and> (\<forall>r'' s''. (r'', s'') \<in> fst Q \<longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> \<lambda>r s. r = r'' \<and> s = s'' \<rbrace>)
20        \<and> (snd Q \<longrightarrow> snd (whileLoop C B r s))
21        \<and> (\<not> snd Q \<longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>_ _. True \<rbrace>!))
22    = (whileLoop C B r s = Q)"
23  apply (rule iffI)
24   apply (rule whileLoop_rule_strong, auto)[1]
25  apply (clarsimp simp: valid_def exs_valid_def validNF_alt_def)
26  apply force
27  done
28
29lemma valid_whileLoop_complete:
30  "(\<exists>I.
31       (\<forall>s. P r s \<longrightarrow> I r s )
32     \<and> (\<forall>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<rbrace> B r \<lbrace> I \<rbrace>)
33     \<and> (\<forall>r s. ( I r s \<and> \<not> C r s ) \<longrightarrow> Q r s))
34    = \<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"
35  apply (rule iffI)
36   apply clarsimp
37   apply (rule_tac I=I in valid_whileLoop, auto)[1]
38  apply (rule exI [where x="\<lambda>r s. \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>"])
39  apply (intro conjI)
40    apply (clarsimp simp: valid_def)
41   apply (subst (2) valid_def)
42   apply clarsimp
43   apply (subst (asm) (2) whileLoop_unroll)
44   apply (case_tac "C a b")
45    apply (clarsimp simp: valid_def bind_def' Bex_def condition_def split: if_split_asm)
46    apply force
47   apply (clarsimp simp: valid_def bind_def' Bex_def condition_def split: if_split_asm)
48   apply force
49  apply (subst whileLoop_unroll)
50  apply (clarsimp simp: valid_def bind_def' condition_def return_def)
51  done
52
53lemma validNF_whileLoop_complete:
54  "(\<exists>I R.
55       (\<forall>s. P r s \<longrightarrow> I r s )
56     \<and> (\<forall>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>!)
57     \<and> (wf R)
58     \<and> (\<forall>r s. ( I r s \<and> \<not> C r s ) \<longrightarrow> Q r s))
59    = \<lbrace> P r \<rbrace> whileLoop C B r \<lbrace> Q \<rbrace>!"
60  (is "(\<exists>I R. ?LHS I R) = ?RHS")
61proof (rule iffI)
62  assume lhs: "\<exists>I R. ?LHS I R"
63
64  obtain I R where "?LHS I R"
65    using lhs
66    by auto
67
68  thus ?RHS
69    by (rule_tac validNF_whileLoop [where I=I and R=R], auto)
70next
71  assume loop: "?RHS"
72
73  define I where "I \<equiv> \<lambda>r s. \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. Q r s \<rbrace>!"
74  define R where "R \<equiv> {(x, y). C (fst y) (snd y) \<and> x \<in> fst (B (fst y) (snd y)) \<and>
75                                whileLoop_terminates C B (fst y) (snd y)}"
76
77  have "wf R"
78    using R_def whileLoop_terminates_wf
79    by auto
80
81  have start: "\<And>s. P r s \<Longrightarrow> I r s"
82    by (metis (full_types) I_def loop validNF_weaken_pre)
83
84  have fin: "\<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s"
85    apply (unfold I_def)
86    apply (subst (asm) whileLoop_unroll)
87    apply (clarsimp simp: condition_def bind_def'
88                     validNF_alt_def return_def)
89    done
90
91  have step: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r
92                   \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> R\<rbrace>!"
93             (is "\<And>r s. \<lbrace> ?pre r s \<rbrace> B r \<lbrace> ?post r s \<rbrace>!")
94  proof -
95    have inv_step:
96        "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
97      apply (clarsimp simp: I_def)
98      apply (subst (asm) whileLoop_unroll)
99      apply (clarsimp simp: condition_def bind_def' validNF_alt_def)
100      apply force
101      done
102
103    have R_step:
104        "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> ((r', s'), (r, s)) \<in> R"
105      apply (clarsimp simp: I_def R_def)
106      apply (clarsimp simp: validNF_alt_def whileLoop_def)
107      done
108
109    show "\<And>r s. ?thesis r s"
110      apply rule
111       apply (clarsimp simp: valid_def inv_step R_step)
112      apply (clarsimp simp: no_fail_def I_def validNF_alt_def)
113      apply (drule (1) snd_whileLoop_first_step)
114      apply simp
115      done
116    qed
117
118  show "\<exists>I' R'. ?LHS I' R'"
119    using \<open>wf R\<close> start fin step
120    by blast
121qed
122
123
124lemma snd_whileLoop_complete:
125  shows "snd (whileLoop C B r s) =
126              (\<exists>I. I r s \<and> C r s \<and>
127                   (\<forall>r. \<lbrace> \<lambda>s. I r s \<and> C r s \<and> \<not> snd (B r s) \<rbrace>
128                            B r \<exists>\<lbrace> \<lambda>r s. C r s \<and> I r s \<rbrace>))"
129  (is "?LHS = ?RHS")
130proof (rule iffI)
131  assume "?LHS"
132  thus "?RHS"
133    apply (clarsimp simp: whileLoop_def)
134    apply (erule disjE)
135     apply (rule exI [where x="\<lambda>r s. (Some (r, s), None) \<in> whileLoop_results C B"])
136     apply (intro conjI)
137       apply simp
138      apply (metis Pair_inject whileLoop_results_cases_fail)
139     apply (clarsimp simp: exs_valid_def)
140     apply (erule whileLoop_results_cases_fail, fastforce)
141     apply clarsimp
142     apply (erule bexI [rotated])
143     apply clarsimp
144     apply (metis fst_conv snd_conv whileLoop_results_cases_fail)
145    apply (rule exI [where x="\<lambda>r s. \<not> whileLoop_terminates C B r s"])
146    apply clarsimp
147    apply (rule conjI)
148     apply (subst (asm)  whileLoop_terminates_simps)
149     apply clarsimp
150    apply (clarsimp simp: exs_valid_def)
151    apply (subst (asm) (2)  whileLoop_terminates_simps)
152    apply clarsimp
153    apply (erule bexI [rotated])
154    apply clarsimp
155    apply (subst (asm) (2)  whileLoop_terminates_simps)
156    apply clarsimp
157    done
158next
159  assume "?RHS"
160  thus "?LHS"
161    apply clarsimp
162    apply (erule (1) snd_whileLoop)
163    apply force
164    done
165qed
166
167lemma not_snd_whileLoop_complete:
168  shows "(\<not> snd (whileLoop C B r s)) = (\<exists>I R . I r s \<and> wf R \<and>
169           (\<forall>r s r' s'. (I r s \<and> C r s \<and> (r', s') \<in> fst (B r s)) \<longrightarrow> I r' s')
170           \<and> (\<forall>r s. I r s \<and> C r s \<longrightarrow> \<not> snd (B r s))
171           \<and> (\<forall>r s r' s'. I r s \<and> C r s \<and> (r', s') \<in> fst (B r s) \<longrightarrow> ((r', s'), (r, s)) \<in> R))"
172   (is "?LHS = ?RHS")
173proof (rule iffI)
174  assume "?RHS"
175  thus "?LHS"
176    apply (clarsimp)
177    apply (erule make_pos_goal, rule not_snd_whileLoop)
178      apply assumption
179     defer
180     apply assumption
181    apply (clarsimp simp: validNF_def no_fail_def valid_def)
182    done
183next
184  assume no_fail: "?LHS"
185  define I where "I \<equiv> \<lambda>r s. \<not> snd (whileLoop C B r s)"
186  define R where "R \<equiv> {((r', s'), (r, s)). C r s \<and> (r', s') \<in> fst (B r s) \<and>
187                                            whileLoop_terminates C B r s}"
188
189  have "I r s"
190    by (clarsimp simp: I_def no_fail)
191
192  moreover have "wf R"
193    apply (rule wf_subset [OF whileLoop_terminates_wf [where C=C and B=B]])
194    apply (clarsimp simp: R_def)
195    done
196
197  moreover have "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> I r' s'"
198    apply (clarsimp simp: I_def whileLoop_def)
199    apply (rule conjI)
200     apply (metis whileLoop_results_simps)
201    apply (erule whileLoop_terminates_cases)
202     apply clarsimp
203    apply fastforce
204    done
205
206  moreover have "\<And>r s. \<lbrakk> I r s; C r s \<rbrakk> \<Longrightarrow> \<not> snd (B r s)"
207    apply (clarsimp simp: I_def)
208    apply (subst (asm) whileLoop_unroll)
209    apply (clarsimp simp: condition_true bind_def)
210    done
211
212  moreover have "\<And>r s r' s'. \<lbrakk> I r s; C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> ((r', s'), (r, s)) \<in> R"
213    apply (clarsimp simp: R_def)
214    apply (metis I_def snd_conv whileLoop_def)
215    done
216
217  ultimately show ?RHS
218    by (metis (mono_tags))
219qed
220
221
222fun valid_path
223where
224    "valid_path C B [] = False"
225  | "valid_path C B [x] = (\<not> C (fst x) (snd x))"
226  | "valid_path C B (x#y#xs) = ((C (fst x) (snd x) \<and> y \<in> fst (B (fst x) (snd x)) \<and> valid_path C B (y#xs)))"
227
228definition "shortest_path_length C B x Q \<equiv>
229        (LEAST n. \<exists>l. valid_path C B l \<and> hd l = x \<and> Q (fst (last l)) (snd (last l)) \<and> length l = n)"
230
231lemma shortest_path_length_same [simp]:
232  "\<lbrakk> \<not> C (fst a) (snd a); Q (fst a) (snd a) \<rbrakk> \<Longrightarrow> shortest_path_length C B a Q = 1"
233  apply (clarsimp simp: shortest_path_length_def)
234  apply (rule Least_equality)
235   apply (rule exI [where x="[a]"])
236   apply clarsimp
237  apply (case_tac "y = 0")
238   apply clarsimp
239  apply clarsimp
240  done
241
242lemma valid_path_simp:
243  "valid_path C B l =
244        (((\<exists>r s. l = [(r, s)] \<and> \<not> C r s) \<or>
245              (\<exists>r s r' s' xs. l = (r, s)#(r', s')#xs \<and> C r s \<and> (r', s') \<in> fst (B r s) \<and> valid_path C B ((r', s')#xs))))"
246  apply (case_tac l)
247   apply clarsimp
248  apply (case_tac list)
249   apply clarsimp
250  apply clarsimp
251  done
252
253lemma path_exists:
254  assumes path: "\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>"
255  shows "\<exists>l. valid_path C B l \<and> hd l = (r, s) \<and> Q (fst (last l)) (snd (last l))"
256proof -
257  {
258    fix r' s'
259    assume x: "(r', s') \<in> fst (whileLoop C B r s)"
260    assume y: "Q r' s'"
261    have ?thesis
262      using x y
263      apply (induct rule: in_whileLoop_induct)
264       apply (rule_tac x="[(r,s)]" in exI)
265       apply clarsimp
266      apply clarsimp
267      apply (case_tac l)
268       apply clarsimp
269      apply (rule_tac x="(r, s)#l" in exI)
270      apply clarsimp
271      done
272  }
273
274  thus ?thesis
275    using path
276    by (clarsimp simp: exs_valid_def)
277qed
278
279lemma shortest_path_exists:
280  "\<lbrakk> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace> \<rbrakk> \<Longrightarrow>
281       \<exists>l. valid_path C B l
282              \<and> shortest_path_length C B (r, s) Q = length l
283              \<and> hd l = (r, s)
284              \<and> Q (fst (last l)) (snd (last l))"
285  apply (frule path_exists)
286  apply (clarsimp simp: simp: shortest_path_length_def)
287  apply (rule LeastI2_ex)
288   apply force
289  apply force
290  done
291
292lemma shortest_path_is_shortest:
293  "\<lbrakk> valid_path C B l; Q (fst (last l)) (snd (last l)) \<rbrakk> \<Longrightarrow> shortest_path_length C B (hd l) Q \<le> length l"
294  apply (clarsimp simp: simp: shortest_path_length_def)
295  apply (rule Least_le)
296  apply force
297  done
298
299lemma valid_path_implies_exs_valid_whileLoop:
300    "valid_path C B l \<Longrightarrow> \<lbrace> \<lambda>s. s = snd (hd l) \<rbrace> whileLoop C B (fst (hd l)) \<exists>\<lbrace> \<lambda>r s. (r, s) = last l  \<rbrace>"
301  apply (induct l)
302   apply clarsimp
303  apply clarsimp
304  apply rule
305   apply clarsimp
306   apply (subst whileLoop_unroll)
307   apply (clarsimp simp: condition_def bind_def' exs_valid_def return_def)
308  apply clarsimp
309  apply (subst whileLoop_unroll)
310  apply (clarsimp simp: condition_def bind_def' exs_valid_def return_def)
311  apply rule
312   apply (clarsimp split: prod.splits)
313   apply (case_tac l)
314    apply clarsimp
315   apply (clarsimp split del: if_split)
316   apply (erule bexI [rotated])
317   apply clarsimp
318  apply clarsimp
319  apply (case_tac l, auto)
320  done
321
322lemma shortest_path_gets_shorter:
323  "\<lbrakk> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>;
324       C r s \<rbrakk>
325     \<Longrightarrow> \<exists>(r', s') \<in> fst (B r s).
326                shortest_path_length C B (r', s') Q < shortest_path_length C B (r, s) Q
327                 \<and> \<lbrace> \<lambda>s. s = s' \<rbrace> whileLoop C B r' \<exists>\<lbrace> Q \<rbrace>"
328  apply (drule shortest_path_exists)
329  apply clarsimp
330  apply (case_tac l)
331   apply clarsimp
332  apply (case_tac list)
333   apply clarsimp
334  apply (rule_tac x="aa" in bexI)
335   apply clarify
336   apply (simp only: valid_path.simps, clarify)
337   apply (frule shortest_path_is_shortest [where Q=Q])
338    apply simp
339   apply clarsimp
340   apply (drule valid_path_implies_exs_valid_whileLoop)
341   apply (clarsimp simp: exs_valid_def)
342   apply (erule bexI [rotated])
343   apply (clarsimp split: if_split_asm)
344  apply clarsimp
345  done
346
347lemma exs_valid_whileLoop_complete:
348   "(\<exists>T R.
349         (\<forall>s. P s \<longrightarrow> T r s)
350         \<and> (\<forall>r s0. \<lbrace> \<lambda>s. T r s \<and> C r s \<and> s = s0 \<rbrace> B r
351                            \<exists>\<lbrace> \<lambda>r' s'. T r' s' \<and> ((r', s'), (r, s0)) \<in> R \<rbrace>)
352         \<and> wf R
353         \<and> (\<forall>r s. (T r s \<and> \<not> C r s) \<longrightarrow> Q r s))
354      = (\<lbrace> P \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>)"
355  (is "(\<exists>T R. ?LHS T R) = ?RHS")
356proof (rule iffI)
357  assume lhs: "\<exists>T R. ?LHS T R"
358  obtain T R where TR: "?LHS T R"
359    using lhs
360    by blast
361
362  show "?RHS"
363    by (rule exs_valid_whileLoop [where T=T and R=R], auto simp: TR)
364next
365  assume rhs: "?RHS"
366
367  define I where "I \<equiv> \<lambda>r s. \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> Q \<rbrace>"
368
369  define R where "R \<equiv> measure (\<lambda>(r, s). shortest_path_length C B (r, s) Q)"
370
371  have P_s: "\<And>s. P s \<Longrightarrow> I r s"
372    using rhs
373    by (clarsimp simp: I_def exs_valid_def)
374
375  have inv_holds: "\<And>r s. \<lbrakk> I r s; C r s \<rbrakk> \<Longrightarrow>
376              \<exists>(r', s') \<in> fst (B r s). I r' s' \<and> ((r', s'), r, s) \<in> R"
377    apply (clarsimp simp: I_def R_def)
378    apply (frule (1) shortest_path_gets_shorter)
379    apply clarsimp
380    apply (rule bexI [rotated], assumption)
381    apply clarsimp
382    done
383
384  have wf_R: "wf R"
385    by (clarsimp simp: R_def)
386
387  have last_step: "\<And>r s. \<lbrakk> I r s; \<not> C r s \<rbrakk> \<Longrightarrow> Q r s"
388    apply (clarsimp simp: I_def exs_valid_def)
389    apply (metis in_return whileLoop_cond_fail)
390    done
391
392  show "\<exists>I R. ?LHS I R"
393    apply (rule exI [where x=I])
394    apply (rule exI [where x=R])
395    using P_s inv_holds wf_R last_step
396    apply (clarsimp simp: exs_valid_def)
397    done
398qed
399
400end
401