From 708cee52f62ca0671e177e363e22e281eac3a572 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 30 Jan 2023 09:49:14 +1100 Subject: [PATCH] lib/monads: style cleanup in WhileLoopRules - adjusted thy imports for new theories - apply consistent style - fix indentation - minor proof contraction Signed-off-by: Gerwin Klein --- lib/Monads/WhileLoopRules.thy | 289 +++++++++++++++------------------- 1 file changed, 127 insertions(+), 162 deletions(-) diff --git a/lib/Monads/WhileLoopRules.thy b/lib/Monads/WhileLoopRules.thy index 87668f689..c107e8982 100644 --- a/lib/Monads/WhileLoopRules.thy +++ b/lib/Monads/WhileLoopRules.thy @@ -7,27 +7,29 @@ theory WhileLoopRules imports Empty_Fail - No_Fail + NonDetMonad_Total + NonDetMonad_Sat begin section "Well-ordered measures" -(* A version of "measure" that takes any wellorder, instead of - * being fixed to "nat". *) -definition measure' :: "('a \ 'b::wellorder) => ('a \ 'a) set" -where "measure' = (\f. {(a, b). f a < f b})" +(* A version of "measure" that takes any wellorder, instead of being fixed to "nat". *) +definition measure' :: "('a \ 'b::wellorder) => ('a \ 'a) set" where + "measure' = (\f. {(a, b). f a < f b})" lemma in_measure'[simp, code_unfold]: - "((x,y) : measure' f) = (f x < f y)" + "((x,y) \ measure' f) = (f x < f y)" by (simp add:measure'_def) -lemma wf_measure' [iff]: "wf (measure' f)" +lemma wf_measure'[iff]: + "wf (measure' f)" apply (clarsimp simp: measure'_def) apply (insert wf_inv_image [OF wellorder_class.wf, where f=f]) apply (clarsimp simp: inv_image_def) done -lemma wf_wellorder_measure: "wf {(a, b). (M a :: 'a :: wellorder) < M b}" +lemma wf_wellorder_measure: + "wf {(a, b). (M a :: 'a :: wellorder) < M b}" apply (subgoal_tac "wf (inv_image ({(a, b). a < b}) M)") apply (clarsimp simp: inv_image_def) apply (rule wf_inv_image) @@ -43,27 +45,30 @@ text \ @{const whileLoop} terms with information that can be used by automated tools. \ -definition - "whileLoop_inv (C :: 'a \ 'b \ bool) B x (I :: 'a \ 'b \ bool) (R :: (('a \ 'b) \ ('a \ 'b)) set) \ whileLoop C B x" +definition whileLoop_inv :: + "('a \ 'b \ bool) \ ('a \ ('b, 'a) nondet_monad) \ 'a \ ('a \ 'b \ bool) \ + (('a \ 'b) \ 'a \ 'b) set \ ('b, 'a) nondet_monad" where + "whileLoop_inv C B x I R \ whileLoop C B x" -definition - "whileLoopE_inv (C :: 'a \ 'b \ bool) B x (I :: 'a \ 'b \ bool) (R :: (('a \ 'b) \ ('a \ 'b)) set) \ whileLoopE C B x" +definition whileLoopE_inv :: + "('a \ 'b \ bool) \ ('a \ ('b, 'c + 'a) nondet_monad) \ 'a \ ('a \ 'b \ bool) \ + (('a \ 'b) \ 'a \ 'b) set \ ('b, 'c + 'a) nondet_monad" where + "whileLoopE_inv C B x I R \ whileLoopE C B x" -lemma whileLoop_add_inv: "whileLoop B C = (\x. whileLoop_inv B C x I (measure' M))" +lemma whileLoop_add_inv: + "whileLoop B C = (\x. whileLoop_inv B C x I (measure' M))" by (clarsimp simp: whileLoop_inv_def) -lemma whileLoopE_add_inv: "whileLoopE B C = (\x. whileLoopE_inv B C x I (measure' M))" +lemma whileLoopE_add_inv: + "whileLoopE B C = (\x. whileLoopE_inv B C x I (measure' M))" by (clarsimp simp: whileLoopE_inv_def) subsection "Simple base rules" lemma whileLoop_terminates_unfold: - "\ whileLoop_terminates C B r s; (r', s') \ fst (B r s); C r s \ - \ whileLoop_terminates C B r' s'" - apply (erule whileLoop_terminates.cases) - apply simp - apply force - done + "\ whileLoop_terminates C B r s; (r', s') \ fst (B r s); C r s \ \ + whileLoop_terminates C B r' s'" + by (force elim!: whileLoop_terminates.cases) lemma snd_whileLoop_first_step: "\ \ snd (whileLoop C B r s); C r s \ \ \ snd (B r s)" apply (subst (asm) whileLoop_unroll) @@ -79,21 +84,16 @@ lemma snd_whileLoopE_first_step: "\ \ snd (whileLoopE C B r s); C r done lemma snd_whileLoop_unfold: - "\ \ snd (whileLoop C B r s); C r s; (r', s') \ fst (B r s) \ \ \ snd (whileLoop C B r' s')" + "\ \ snd (whileLoop C B r s); C r s; (r', s') \ fst (B r s) \ \ \ snd (whileLoop C B r' s')" apply (clarsimp simp: whileLoop_def) - apply (auto simp: elim: whileLoop_results.cases whileLoop_terminates.cases - intro: whileLoop_results.intros whileLoop_terminates.intros) + apply (auto elim: whileLoop_results.cases whileLoop_terminates.cases + intro: whileLoop_results.intros whileLoop_terminates.intros) done lemma snd_whileLoopE_unfold: - "\ \ snd (whileLoopE C B r s); (Inr r', s') \ fst (B r s); C r s \ \ \ snd (whileLoopE C B r' s')" - apply (clarsimp simp: whileLoopE_def) - apply (drule snd_whileLoop_unfold) - apply clarsimp - apply (clarsimp simp: lift_def) - apply assumption - apply (clarsimp simp: lift_def) - done + "\ \ snd (whileLoopE C B r s); (Inr r', s') \ fst (B r s); C r s \ \ \ snd (whileLoopE C B r' s')" + unfolding whileLoopE_def + by (fastforce simp: lift_def dest: snd_whileLoop_unfold) lemma whileLoop_results_cong [cong]: assumes C: "\r s. C r s = C' r s" @@ -103,26 +103,17 @@ proof - { fix x y C B C' B' have "\ (x, y) \ whileLoop_results C B; - \(r :: 'r) (s :: 's). C r s = C' r s; - \r s. C' r s \ B r s = B' r s \ - \ (x, y) \ whileLoop_results C' B'" - apply (induct rule: whileLoop_results.induct) - apply clarsimp - apply clarsimp - apply (rule whileLoop_results.intros, auto)[1] - apply clarsimp - apply (rule whileLoop_results.intros, auto)[1] - done + \(r :: 'r) (s :: 's). C r s = C' r s; \r s. C' r s \ B r s = B' r s \ + \ (x, y) \ whileLoop_results C' B'" + by (induct rule: whileLoop_results.induct) (auto intro: whileLoop_results.intros) } thus ?thesis apply - - apply (rule set_eqI, rule iffI) - apply (clarsimp split: prod.splits) - apply (clarsimp simp: C B split: prod.splits) - apply (clarsimp split: prod.splits) - apply (clarsimp simp: C [symmetric] B [symmetric] split: prod.splits) - done + apply (rule set_eqI, rule iffI; clarsimp split: prod.splits) + apply (clarsimp simp: C B) + apply (clarsimp simp: C [symmetric] B [symmetric]) + done qed lemma whileLoop_terminates_cong [cong]: @@ -154,42 +145,30 @@ next done qed -lemma whileLoop_cong [cong]: +lemma whileLoop_cong[cong]: "\ \r s. C r s = C' r s; \r s. C r s \ B r s = B' r s \ \ whileLoop C B = whileLoop C' B'" - apply (rule ext, clarsimp simp: whileLoop_def) - done + by (clarsimp simp: whileLoop_def) -lemma whileLoopE_cong [cong]: - "\ \r s. C r s = C' r s ; \r s. C r s \ B r s = B' r s \ - \ whileLoopE C B = whileLoopE C' B'" - apply (clarsimp simp: whileLoopE_def) - apply (rule whileLoop_cong [THEN arg_cong]) - apply (clarsimp split: sum.splits) - apply (clarsimp split: sum.splits) - apply (clarsimp simp: lift_def throwError_def split: sum.splits) - done +lemma whileLoopE_cong[cong]: + "\ \r s. C r s = C' r s ; \r s. C r s \ B r s = B' r s \ \ whileLoopE C B = whileLoopE C' B'" + unfolding whileLoopE_def + by (rule whileLoop_cong[THEN arg_cong]; clarsimp simp: lift_def throwError_def split: sum.splits) lemma whileLoop_terminates_wf: - "wf {(x, y). C (fst y) (snd y) \ x \ fst (B (fst y) (snd y)) \ whileLoop_terminates C B (fst y) (snd y)}" - apply (rule wfI [where A="UNIV" and B="{(r, s). whileLoop_terminates C B r s}"]) - apply clarsimp - apply clarsimp - apply (erule whileLoop_terminates.induct) - apply blast - apply blast + "wf {(x, y). C (fst y) (snd y) \ x \ fst (B (fst y) (snd y)) \ whileLoop_terminates C B (fst y) (snd y)}" + apply (rule wfI[where A="UNIV" and B="{(r, s). whileLoop_terminates C B r s}"]; clarsimp) + apply (erule whileLoop_terminates.induct; blast) done subsection "Basic induction helper lemmas" lemma whileLoop_results_induct_lemma1: - "\ (a, b) \ whileLoop_results C B; b = Some (x, y) \ \ \ C x y" - apply (induct rule: whileLoop_results.induct, auto) - done + "\ (a, b) \ whileLoop_results C B; b = Some (x, y) \ \ \ C x y" + by (induct rule: whileLoop_results.induct) auto lemma whileLoop_results_induct_lemma1': - "\ (a, b) \ whileLoop_results C B; a \ b \ \ \x. a = Some x \ C (fst x) (snd x)" - apply (induct rule: whileLoop_results.induct, auto) - done + "\ (a, b) \ whileLoop_results C B; a \ b \ \ \x. a = Some x \ C (fst x) (snd x)" + by (induct rule: whileLoop_results.induct) auto lemma whileLoop_results_induct_lemma2 [consumes 1]: "\ (a, b) \ whileLoop_results C B; @@ -208,7 +187,7 @@ lemma whileLoop_results_induct_lemma3 [consumes 1]: and inv_step: "\r s r' s'. \ I r s; C r s; (r', s') \ fst (B r s) \ \ I r' s'" shows "I r' s'" apply (rule whileLoop_results_induct_lemma2 [where P="case_prod I" and y="(r', s')" and x="(r, s)", - simplified case_prod_unfold, simplified]) + simplified case_prod_unfold, simplified]) apply (rule result) apply simp apply simp @@ -219,14 +198,12 @@ lemma whileLoop_results_induct_lemma3 [consumes 1]: subsection "Inductive reasoning about whileLoop results" -lemma in_whileLoop_induct [consumes 1]: +lemma in_whileLoop_induct[consumes 1]: assumes in_whileLoop: "(r', s') \ fst (whileLoop C B r s)" and init_I: "\ r s. \ C r s \ I r s r s" - and step: - "\r s r' s' r'' s''. - \ C r s; (r', s') \ fst (B r s); - (r'', s'') \ fst (whileLoop C B r' s'); - I r' s' r'' s'' \ \ I r s r'' s''" + and step: "\r s r' s' r'' s''. \ C r s; (r', s') \ fst (B r s); + (r'', s'') \ fst (whileLoop C B r' s'); + I r' s' r'' s'' \ \ I r s r'' s''" shows "I r s r' s'" proof cases assume "C r s" @@ -238,13 +215,11 @@ proof cases by blast have "\ (a, b) \ whileLoop_results C B; \x. a = Some x; \x. b = Some x \ - \ I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b))" - apply (induct rule: whileLoop_results.induct) - apply (auto simp: init_I whileLoop_def intro: step) - done + \ I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b))" + by (induct rule: whileLoop_results.induct) + (auto simp: init_I whileLoop_def intro: step) - hence "(Some (r, s), Some (r', s')) \ whileLoop_results C B - \ I r s r' s'" + hence "(Some (r, s), Some (r', s')) \ whileLoop_results C B \ I r s r' s'" by (clarsimp simp: a_def b_def) } @@ -256,8 +231,7 @@ next hence "r' = r \ s' = s" using in_whileLoop - by (subst (asm) whileLoop_unroll, - clarsimp simp: condition_def return_def) + by (subst (asm) whileLoop_unroll, clarsimp simp: condition_def return_def) thus ?thesis by (metis init_I \\ C r s\) @@ -267,10 +241,8 @@ lemma snd_whileLoop_induct [consumes 1]: assumes induct: "snd (whileLoop C B r s)" and terminates: "\ whileLoop_terminates C B r s \ I r s" and init: "\ r s. \ snd (B r s); C r s \ \ I r s" - and step: "\r s r' s' r'' s''. - \ C r s; (r', s') \ fst (B r s); - snd (whileLoop C B r' s'); - I r' s' \ \ I r s" + and step: "\r s r' s' r'' s''. \ C r s; (r', s') \ fst (B r s); snd (whileLoop C B r' s'); + I r' s' \ \ I r s" shows "I r s" apply (insert init induct) apply atomize @@ -278,8 +250,7 @@ lemma snd_whileLoop_induct [consumes 1]: apply clarsimp apply (erule disjE) apply (erule rev_mp) - apply (induct "Some (r, s)" "None :: ('a \ 'b) option" - arbitrary: r s rule: whileLoop_results.induct) + apply (induct "Some (r, s)" "None :: ('a \ 'b) option" arbitrary: r s rule: whileLoop_results.induct) apply clarsimp apply clarsimp apply (erule (1) step) @@ -298,15 +269,11 @@ lemma whileLoop_terminatesE_induct [consumes 1]: apply (subgoal_tac "(\r s. case (Inr r) of Inl x \ True | Inr x \ I x s) r s") apply simp apply (induction rule: whileLoop_terminates.induct) - apply (case_tac r) - apply simp - apply clarsimp - apply (erule init) + apply (clarsimp split: sum.splits elim!: init) apply (clarsimp split: sum.splits) apply (rule step) apply simp - apply (clarsimp simp: lift_def split: sum.splits) - apply force + apply (force simp: lift_def split: sum.splits) done subsection "Direct reasoning about whileLoop components" @@ -320,9 +287,8 @@ lemma fst_whileLoop_cond_false: lemma snd_whileLoop: assumes init_I: "I r s" and cond_I: "C r s" - and non_term: "\r. \ \s. I r s \ C r s \ \ snd (B r s) \ - B r \\ \r' s'. C r' s' \ I r' s' \" - shows "snd (whileLoop C B r s)" + and non_term: "\r. \ \s. I r s \ C r s \ \ snd (B r s) \ B r \\ \r' s'. C r' s' \ I r' s' \" + shows "snd (whileLoop C B r s)" apply (clarsimp simp: whileLoop_def) apply (rotate_tac) apply (insert init_I cond_I) @@ -357,15 +323,15 @@ lemma not_snd_whileLoop: assumes init_I: "I r s" and inv_holds: "\r s. \\s'. I r s' \ C r s' \ s' = s \ B r \ \r' s'. I r' s' \ ((r', s'), (r, s)) \ R \!" and wf_R: "wf R" - shows "\ snd (whileLoop C B r s)" + shows "\ snd (whileLoop C B r s)" proof - { fix x y have "\ (x, y) \ whileLoop_results C B; x = Some (r, s); y = None \ \ False" apply (insert init_I) apply (induct arbitrary: r s rule: whileLoop_results.inducts) - apply simp apply simp + apply simp apply (insert snd_validNF [OF inv_holds])[1] apply blast apply (drule use_validNF [OF _ inv_holds]) @@ -375,20 +341,20 @@ proof - } also have "whileLoop_terminates C B r s" - apply (rule whileLoop_terminates_inv [where I=I, OF init_I _ wf_R]) - apply (insert inv_holds) - apply (clarsimp simp: validNF_def) - done + apply (rule whileLoop_terminates_inv [where I=I, OF init_I _ wf_R]) + apply (insert inv_holds) + apply (clarsimp simp: validNF_def) + done ultimately show ?thesis - by (clarsimp simp: whileLoop_def, blast) + by (clarsimp simp: whileLoop_def, blast) qed lemma valid_whileLoop: assumes first_step: "\s. P r s \ I r s" and inv_step: "\r. \ \s. I r s \ C r s \ B r \ I \" and final_step: "\r s. \ I r s; \ C r s \ \ Q r s" - shows "\ P r \ whileLoop C B r \ Q \" + shows "\ P r \ whileLoop C B r \ Q \" proof - { fix r' s' s @@ -396,7 +362,7 @@ proof - assume step: "(r', s') \ fst (whileLoop C B r s)" have "I r' s'" - using step inv + using step inv apply (induct rule: in_whileLoop_induct) apply simp apply (drule use_valid, rule inv_step, auto) @@ -419,7 +385,7 @@ lemma whileLoop_wp: lemma whileLoop_wp_inv [wp]: "\ \r. \\s. I r s \ C r s\ B r \I\; \r s. \I r s; \ C r s\ \ Q r s \ - \ \ I r \ whileLoop_inv C B r I M \ Q \" + \ \ I r \ whileLoop_inv C B r I M \ Q \" apply (clarsimp simp: whileLoop_inv_def) apply (rule valid_whileLoop [where P=I and I=I], auto) done @@ -427,11 +393,11 @@ lemma whileLoop_wp_inv [wp]: lemma validE_whileLoopE: "\\s. P r s \ I r s; \r. \ \s. I r s \ C r s \ B r \ I \,\ A \; - \r s. \ I r s; \ C r s \ \ Q r s - \ \ \ P r \ whileLoopE C B r \ Q \,\ A \" + \r s. \ I r s; \ C r s \ \ Q r s\ \ + \ P r \ whileLoopE C B r \ Q \,\ A \" apply (clarsimp simp: whileLoopE_def validE_def) apply (rule valid_whileLoop [where I="\r s. (case r of Inl x \ A x s | Inr x \ I x s)" - and Q="\r s. (case r of Inl x \ A x s | Inr x \ Q x s)"]) + and Q="\r s. (case r of Inl x \ A x s | Inr x \ Q x s)"]) apply atomize apply (clarsimp simp: valid_def lift_def split: sum.splits) apply (clarsimp simp: valid_def lift_def split: sum.splits) @@ -446,9 +412,7 @@ lemma whileLoopE_wp: lemma exs_valid_whileLoop: assumes init_T: "\s. P s \ T r s" - and iter_I: "\ r s0. - \ \s. T r s \ C r s \ s = s0 \ - B r \\\r' s'. T r' s' \ ((r', s'),(r, s0)) \ R\" + and iter_I: "\r s0. \\s. T r s \ C r s \ s = s0\ B r \\\r' s'. T r' s' \ ((r', s'),(r, s0)) \ R\" and wf_R: "wf R" and final_I: "\r s. \ T r s; \ C r s \ \ Q r s" shows "\ P \ whileLoop C B r \\ Q \" @@ -458,8 +422,7 @@ proof (clarsimp simp: exs_valid_def Bex_def) { fix x - have "T (fst x) (snd x) \ - \r' s'. (r', s') \ fst (whileLoop C B (fst x) (snd x)) \ T r' s'" + have "T (fst x) (snd x) \ \r' s'. (r', s') \ fst (whileLoop C B (fst x) (snd x)) \ T r' s'" using wf_R apply induction apply atomize @@ -475,8 +438,7 @@ proof (clarsimp simp: exs_valid_def Bex_def) } thus "\r' s'. (r', s') \ fst (whileLoop C B r s) \ Q r' s'" - by (metis \P s\ fst_conv init_T snd_conv - final_I fst_whileLoop_cond_false) + by (metis \P s\ fst_conv init_T snd_conv final_I fst_whileLoop_cond_false) qed lemma empty_fail_whileLoop: @@ -525,9 +487,9 @@ lemma whileLoop_results_bisim: and inv_step: "\r s r' s'. \ I r s; C r s; (r', s') \ fst (B r s) \ \ I r' s'" and cond_match: "\r s. I r s \ C r s = C' (rt r) (st s)" and fail_step: "\r s. \C r s; snd (B r s); I r s\ - \ (Some (rt r, st s), None) \ whileLoop_results C' B'" + \ (Some (rt r, st s), None) \ whileLoop_results C' B'" and refine: "\r s r' s'. \ I r s; C r s; (r', s') \ fst (B r s) \ - \ (rt r', st s') \ fst (B' (rt r) (st s))" + \ (rt r', st s') \ fst (B' (rt r) (st s))" shows "(Q, R) \ whileLoop_results C' B'" apply (subst vars1) apply (subst vars2) @@ -541,10 +503,10 @@ lemma whileLoop_results_bisim: apply (metis fail_step) apply (case_tac z) apply (clarsimp simp: option.splits) + apply (metis cond_match inv_step refine whileLoop_results.intros(3)) + apply (clarsimp simp: option.splits) apply (metis cond_match inv_step refine whileLoop_results.intros(3)) - apply (clarsimp simp: option.splits) - apply (metis cond_match inv_step refine whileLoop_results.intros(3)) - done + done lemma whileLoop_terminates_liftE: "whileLoop_terminatesE C (\r. liftE (B r)) r s = whileLoop_terminates C B r s" @@ -557,14 +519,18 @@ lemma whileLoop_terminates_liftE: apply (clarsimp simp: split_def) apply (rule whileLoop_terminates.intros(2)) apply clarsimp - apply (clarsimp simp: liftE_def in_bind return_def lift_def [abs_def] - bind_def lift_def throwError_def o_def split: sum.splits - cong: sum.case_cong) + apply (clarsimp simp: liftE_def in_bind return_def lift_def[abs_def] + bind_def lift_def throwError_def o_def + split: sum.splits + cong: sum.case_cong) apply (drule (1) bspec) apply clarsimp - apply (subgoal_tac "case (Inr r) of Inl _ \ True | Inr r \ - whileLoop_terminates (\r s. (\r s. case r of Inl _ \ False | Inr v \ C v s) (Inr r) s) - (\r. (lift (\r. liftE (B r)) (Inr r)) >>= (\x. return (projr x))) r s") + apply (subgoal_tac + "case Inr r of + Inl _ \ True + | Inr r \ whileLoop_terminates + (\r s. (\r s. case r of Inl _ \ False | Inr v \ C v s) (Inr r) s) + (\r. lift (\r. liftE (B r)) (Inr r) >>= (\x. return (projr x))) r s") apply (clarsimp simp: liftE_def lift_def) apply (erule whileLoop_terminates.induct) apply (clarsimp simp: liftE_def lift_def split: sum.splits) @@ -575,8 +541,8 @@ lemma whileLoop_terminates_liftE: apply force done -lemma snd_X_return [simp]: - "\A X s. snd ((A >>= (\a. return (X a))) s) = snd (A s)" +lemma snd_X_return[simp]: + "snd ((A >>= (\a. return (X a))) s) = snd (A s)" by (clarsimp simp: return_def bind_def split_def) lemma whileLoopE_liftE: @@ -590,22 +556,27 @@ lemma whileLoopE_liftE: apply (rule_tac x="b" in exI) apply (rule_tac x="projr a" in exI) apply (rule conjI) - apply (erule whileLoop_results_bisim [where rt=projr and st="\x. x" and I="\r s. case r of Inr x \ True | _ \ False"], - auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1] - apply (drule whileLoop_results_induct_lemma2 [where P="\(r, s). case r of Inr x \ True | _ \ False"] ) + apply (erule whileLoop_results_bisim[where rt=projr + and st="\x. x" + and I="\r s. case r of Inr x \ True | _ \ False"], + auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1] + apply (drule whileLoop_results_induct_lemma2[where P="\(r, s). case r of Inr x \ True | _ \ False"]) apply (rule refl) apply (rule refl) apply clarsimp apply (clarsimp simp: return_def bind_def lift_def split: sum.splits) apply (clarsimp simp: return_def bind_def lift_def split: sum.splits) apply (clarsimp simp: in_bind whileLoop_def liftE_def) - apply (erule whileLoop_results_bisim [where rt=Inr and st="\x. x" and I="\r s. True"], - auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def split: sum.splits)[1] + apply (erule whileLoop_results_bisim[where rt=Inr and st="\x. x" and I="\r s. True"], + auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def + split: sum.splits)[1] apply (rule iffI) apply (clarsimp simp: whileLoop_def liftE_def del: notI) apply (erule disjE) - apply (erule whileLoop_results_bisim [where rt=projr and st="\x. x" and I="\r s. case r of Inr x \ True | _ \ False"], - auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1] + apply (erule whileLoop_results_bisim[where rt=projr + and st="\x. x" + and I="\r s. case r of Inr x \ True | _ \ False"], + auto intro: whileLoop_results.intros simp: bind_def return_def lift_def split: sum.splits)[1] apply (subst (asm) whileLoop_terminates_liftE [symmetric]) apply (fastforce simp: whileLoop_def liftE_def whileLoop_terminatesE_def) apply (clarsimp simp: whileLoop_def liftE_def del: notI) @@ -616,7 +587,8 @@ lemma whileLoopE_liftE: apply (clarsimp split: option.splits) apply (clarsimp split: option.splits) apply (clarsimp split: option.splits) - apply (auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def split: sum.splits) + apply (auto intro: whileLoop_results.intros intro!: bexI simp: bind_def return_def lift_def + split: sum.splits) done lemma validNF_whileLoop: @@ -628,8 +600,7 @@ lemma validNF_whileLoop: apply rule apply (rule valid_whileLoop) apply fact - apply (insert inv, clarsimp simp: validNF_def - valid_def split: prod.splits, force)[1] + apply (insert inv, clarsimp simp: validNF_def valid_def split: prod.splits, force)[1] apply (metis post_cond) apply (unfold no_fail_def) apply (intro allI impI) @@ -655,7 +626,7 @@ lemma validNF_whileLoop_inv_measure [wp]: and post_cond: "\r s. \I r s; \ C r s\ \ Q r s" shows "\I r\ whileLoop_inv C B r I (measure' (\(r, s). M r s)) \Q\!" apply (clarsimp simp: whileLoop_inv_def) - apply (rule validNF_whileLoop [where R="measure' (\(r, s). M r s)" and I=I]) + apply (rule validNF_whileLoop[where R="measure' (\(r, s). M r s)" and I=I]) apply simp apply clarsimp apply (rule inv) @@ -688,30 +659,24 @@ lemma validNF_whileLoopE: and post_cond: "\r s. \I r s; \ C r s\ \ Q r s" shows "\ P r \ whileLoopE C B r \ Q \,\ E \!" apply (unfold validE_NF_alt_def whileLoopE_def) - apply (rule validNF_whileLoop [ - where I="\r s. case r of Inl x \ E x s | Inr x \ I x s" - and R="{((r', s'), (r, s)). \x x'. r' = Inl x' \ r = Inr x} - \ {((r', s'), (r, s)). \x x'. r' = Inr x' \ r = Inr x \ ((x', s'),(x, s)) \ R}"]) + apply (rule validNF_whileLoop [where + I="\r s. case r of Inl x \ E x s | Inr x \ I x s" and + R="{((r', s'), (r, s)). \x x'. r' = Inl x' \ r = Inr x} \ + {((r', s'), (r, s)). \x x'. r' = Inr x' \ r = Inr x \ ((x', s'),(x, s)) \ R}"]) apply (simp add: pre) apply (insert inv)[1] - apply (fastforce simp: lift_def validNF_def valid_def - validE_NF_def throwError_def no_fail_def return_def - validE_def split: sum.splits prod.splits) + apply (fastforce simp: lift_def validNF_def valid_def validE_NF_def throwError_def no_fail_def + return_def validE_def + split: sum.splits prod.splits) apply (rule wf_Un) apply (rule wf_custom_measure [where f="\(r, s). case r of Inl _ \ 0 | _ \ 1"]) apply clarsimp apply (insert wf_inv_image [OF wf, where f="\(r, s). (projr r, s)"]) apply (drule wf_Int1 [where r'="{((r', s'),(r, s)). (\x. r = Inr x) \ (\x. r' = Inr x)}"]) apply (erule wf_subset) - apply rule - apply (clarsimp simp: inv_image_def split: prod.splits sum.splits) - apply clarsimp - apply rule - apply rule - apply clarsimp - apply clarsimp - apply (clarsimp split: sum.splits) - apply (blast intro: post_cond) + apply (fastforce simp: inv_image_def split: prod.splits sum.splits) + apply fastforce + apply (fastforce split: sum.splits intro: post_cond) done lemma validNF_whileLoopE_inv [wp]: