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