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