theory WhileLoopRule imports week09B_demo_monad begin text \ While Loop rules follow \ 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 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 lemma whileLoop_results_induct_lemma2 [consumes 1]: "\ (a, b) \ whileLoop_results C B; a = Some (x :: 'a \ 'b); b = Some y; P x; \s t. \ P s; t \ fst (B (fst s) (snd s)); C (fst s) (snd s) \ \ P t \ \ P y" apply (induct arbitrary: x y rule: whileLoop_results.induct) apply simp apply simp apply fastforce done lemma whileLoop_results_induct_lemma3 [consumes 1]: assumes result: "(Some (r, s), Some (r', s')) \ whileLoop_results C B" and inv_start: "I r s" 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 split_def, simplified]) apply (rule result) apply simp apply simp apply fact apply (erule (1) inv_step) apply clarsimp done lemma whileLoop_cond_fail: "\ \ C x s \ \ (whileLoop C B x s) = (return x s)" apply (auto simp: return_def whileLoop_def intro: whileLoop_results.intros whileLoop_terminates.intros elim!: whileLoop_results.cases) done definition condition :: "('s \ bool) \ ('s, 'r) nondet_monad \ ('s, 'r) nondet_monad \ ('s, 'r) nondet_monad" where "condition P L R \ \s. if (P s) then (L s) else (R s)" notation (output) condition ("(condition (_)// (_)// (_))" [1000,1000,1000] 1000) lemma monad_state_eqI [intro]: "\ \r t. (r, t) \ fst (A s) \ (r, t) \ fst (B s'); \r t. (r, t) \ fst (B s') \ (r, t) \ fst (A s); snd (A s) = snd (B s') \ \ (A :: ('s, 'a) nondet_monad) s = B s'" apply (fastforce intro!: set_eqI prod_eqI) done lemma whileLoop_unroll: "(whileLoop C B r) = ((condition (C r) (B r >>= (whileLoop C B)) (return r)))" (is "?LHS r = ?RHS r") proof - have cond_fail: "\r s. \ C r s \ ?LHS r s = ?RHS r s" apply (subst whileLoop_cond_fail, simp) apply (clarsimp simp: condition_def bind_def return_def) done have cond_pass: "\r s. C r s \ whileLoop C B r s = (B r >>= (whileLoop C B)) s" apply (rule monad_state_eqI) apply (clarsimp simp: whileLoop_def bind_def split_def) apply (subst (asm) whileLoop_results_simps_valid) apply fastforce apply (clarsimp simp: whileLoop_def bind_def split_def) apply (subst whileLoop_results.simps) apply fastforce apply (clarsimp simp: whileLoop_def bind_def split_def) apply (subst whileLoop_results.simps) apply (subst whileLoop_terminates.simps) apply fastforce done show ?thesis apply (rule ext) apply (metis cond_fail cond_pass condition_def) done qed subsection "Inductive reasoning about whileLoop results" 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''" shows "I r s r' s'" proof cases assume "C r s" { obtain a where a_def: "a = Some (r, s)" by blast obtain b where b_def: "b = Some (r', s')" 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 hence "(Some (r, s), Some (r', s')) \ whileLoop_results C B \ I r s r' s'" by (clarsimp simp: a_def b_def) } thus ?thesis using in_whileLoop by (clarsimp simp: whileLoop_def) next assume "\ C r s" hence "r' = r \ s' = s" using in_whileLoop by (subst (asm) whileLoop_unroll, clarsimp simp: condition_def return_def) thus ?thesis by (metis init_I `\ C r s`) qed 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" shows "I r s" apply (insert init induct) apply atomize apply (unfold whileLoop_def) 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 clarsimp apply clarsimp apply (erule (1) step) apply (clarsimp simp: whileLoop_def) apply clarsimp apply (metis terminates) done subsection "Direct reasoning about whileLoop components" lemma fst_whileLoop_cond_false: assumes loop_result: "(r', s') \ fst (whileLoop C B r s)" shows "\ C r' s'" using loop_result by (rule in_whileLoop_induct, auto) lemma use_valid: "\(r, s') \ fst (f s); \P\ f \Q\; P s \ \ Q r s'" apply (simp add: valid_def) apply blast done 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 \" proof - { fix r' s' s assume inv: "I r s" assume step: "(r', s') \ fst (whileLoop C B r s)" have "I r' s'" using step inv apply (induct rule: in_whileLoop_induct) apply simp apply (drule use_valid, rule inv_step, auto) done } thus ?thesis apply (clarsimp simp: valid_def) apply (drule first_step) apply (rule final_step, simp) apply (metis fst_whileLoop_cond_false) done qed lemma whileLoop_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 C B r \ Q \" by (rule valid_whileLoop) end