theory Hoare_ann_SIMP imports Hoare_SIMP begin datatype 'data annotated_command = AnnAssignCom "var_name" "'data exp" (infix ":=" 110) | AnnSeqCom "'data annotated_command" "'data annotated_command" (infixl ";;" 109) | AnnCondCom "'data bool_exp" "'data annotated_command" "'data annotated_command" ("If _/ Then _/ Else _/ Fi" [70,70,70]70) | AnnWhileCom "'data bool_exp" "'data bool_exp" "'data annotated_command" ("While _/ Inv _/ Do _/ Od" [70,70]70) inductive ann_valid :: "'data bool_exp \ 'data annotated_command \ 'data bool_exp \ bool" ("\_\_\_\" [60,60,60]60) where AnnAssignmentAxiom: "\(P[x\e])\ (x:=e) \P\" | AnnSequenceRule: "\\P\ C \Q\; \Q\ C' \R\\ \ \P\(C;;C')\R\" | AnnRuleOfConsequence: "\|\ (P [\] P') ; \P'\C\Q'\; |\ (Q' [\] Q) \\ \P\C\Q\" | AnnIfThenElseRule: "\\(P [\] B)\C\Q\; \(P[\]([\]B))\C'\Q\\ \ \P\(If B Then C Else C' Fi)\Q\" | AnnWhileRule: "\\(P [\] B)\C\P\\ \ \P\(While B Inv P Do C Od)\(P [\] ([\]B))\" lemma AnnPreconditionStrengthening: "\|\ (P [\] P') ; \P'\C\Q\\\ \P\C\Q\" apply (rule_tac Q' = "Q" in AnnRuleOfConsequence) by auto lemma AnnPostconditionWeakening: "\|\ (Q' [\] Q) ; \P\C\Q'\\\ \P\C\Q\" apply (rule_tac P' = "P" in AnnRuleOfConsequence) by auto fun strip_annotations :: "'data annotated_command \ 'data command" where "strip_annotations (v := e) = (v ::= e)" | "strip_annotations (AnnSeqCom C C') = SeqCom(strip_annotations C) (strip_annotations C')" | "strip_annotations (If B Then C Else C' Fi) = (IF B THEN (strip_annotations C) ELSE (strip_annotations C') FI)" | "strip_annotations (While B Inv I' Do C Od) = (WHILE B DO (strip_annotations C) OD)" thm ann_valid.induct lemma ann_valid_valid: "\\P\C\Q\\ \ {{P}}(strip_annotations C){{Q}}" apply (erule ann_valid.induct) apply auto apply (rule AssignmentAxiom) apply (erule SequenceRule) apply assumption apply (erule RuleOfConsequence) apply assumption apply assumption apply (erule IfThenElseRule) apply assumption apply (erule WhileRule) done lemma valid_ann_valid: "\{{P}}C{{Q}}\ \ \C'.(\P\C'\Q\ \ (strip_annotations C' = C))" apply (erule hvalid.induct) apply auto apply (rule_tac x = "x := e" in exI) apply (clarsimp simp add: AnnAssignmentAxiom) apply (rule_tac x = "C'a;;C'b" in exI) apply (clarsimp simp add: AnnSequenceRule) apply (rule_tac x = "C'" in exI) apply simp apply (erule AnnRuleOfConsequence) apply assumption apply assumption apply (rule_tac x = "If B Then C'a Else C'b Fi" in exI) apply (clarsimp simp add: AnnIfThenElseRule) apply (rule_tac x = "While B Inv P Do C' Od" in exI) apply (clarsimp simp add: AnnWhileRule) done fun wp :: "'data annotated_command \ 'data bool_exp \ 'data bool_exp" where wp_Asg: "wp (x := e) Q = (Q [x\e])" | wp_Seq: "wp (C;;C') Q = wp C (wp C' Q)" | wp_If: "wp (If B Then C Else C' Fi) Q = ((B [\] (wp C Q)) [\] (([\] B) [\] (wp C' Q)))" | wp_While: "wp (While B Inv I' Do C Od) Q = I'" lemma wp_monotonic [rule_format]: "\ P Q.( |\ (P [\] Q)) \ ( |\ ((wp C P) [\] (wp C Q)))" apply (induct C) apply clarsimp apply (drule_tac P = "(P [\] Q)" and x = "list" and e = "fun" in bvalid_substitute) apply clarsimp apply clarsimp apply (clarsimp simp add: bvalid_def substitute_def imp_b_def or_b_def and_b_def not_b_def) apply (clarsimp simp add: bvalid_def substitute_def imp_b_def or_b_def and_b_def not_b_def) done lemma wp_monotonic_plain[rule_format]: "(\ s. P s \ Q s) \ (\ s. wp C P s \ wp C Q s)" apply (cut_tac P=P and Q=Q and C=C in wp_monotonic) apply (simp_all add: bvalid_def imp_b_def) done lemma weakestAssignCase: "\P\ (x := e) \Q\ \ |\ (P [\] (Q[x\e]))" apply (subgoal_tac "\ C. (\P\C \Q\) \ (C = (x := e)) \ |\ (P [\] (Q[x\e]))") apply (erule_tac x = "x := e" in allE, clarsimp) apply (thin_tac "\P\(x := e)\Q\") apply (rule allI, rule impI) apply (erule ann_valid.induct) apply simp_all apply (clarsimp simp add: bvalid_def substitute_def imp_b_def) done lemma weakestSeqCase: "\\P Q. \P\C'\Q\ \ |\ (P [\] (wp C' Q)); \P Q. \P\C''\Q\ \ |\ (P [\] (wp C'' Q)); \P\(C';;C'')\Q\ \ \ |\ (P [\] (wp C' (wp C'' Q)))" apply (subgoal_tac "\ C. (\P\C \Q\) \ ((C = C';;C'') \ |\ (P [\] (wp C' (wp C'' Q))))") apply (erule_tac x = "C';;C''" in allE, clarsimp) apply (thin_tac "\P\(C' ;; C'')\Q\") apply (rule allI, rule impI) apply (erule ann_valid.induct) apply simp_all apply (clarsimp simp add: bvalid_def substitute_def imp_b_def) apply (thin_tac "C' = C' ;; C'' \ (\s. P s \ wp C' (wp C'' Q) s)") apply (thin_tac "C'' = C' ;; C'' \ (\s. Q s \ wp C' (wp C'' R) s)") apply (erule_tac x = "P" in allE) apply (erule_tac x = "Q" in allE) apply (erule_tac x = "Q" in allE) apply (erule_tac x = "R" in allE) thm wp_monotonic_plain apply (rule_tac P=Q in wp_monotonic_plain) apply clarsimp apply clarsimp apply (clarsimp simp add: bvalid_def substitute_def imp_b_def) apply (rule_tac P="wp C'' Q'" in wp_monotonic_plain) apply (rule_tac P=Q' in wp_monotonic_plain) apply clarsimp apply assumption apply (subgoal_tac "P' s", clarsimp, clarsimp) done lemma WeakestIfCase: "\\P Q. \P\C'\Q\ \ |\ (P [\] (wp C' Q)); \P Q. \P\C''\Q\ \ |\ (P [\] (wp C'' Q)); \P\If B Then C' Else C'' Fi\Q\ \ \ |\ (P [\] ((B [\] (wp C' Q)) [\] (([\] B) [\] (wp C'' Q))))" apply (subgoal_tac "\ C. (\P\C \Q\) \ ((C = (If B Then C' Else C'' Fi)) \ |\ (P [\] ((B [\] (wp C' Q)) [\] (([\] B) [\] (wp C'' Q)))))") apply clarsimp apply (thin_tac "\P\If B Then C' Else C'' Fi\Q\") apply (rule allI, rule impI) apply (erule ann_valid.induct) apply simp_all apply (clarsimp simp add: imp_b_def and_b_def or_b_def not_b_def bvalid_def) apply (erule_tac x = "s" in allE, erule_tac x = "s" in allE) apply simp apply (case_tac "B s", simp_all) apply (rule_tac P="Q'" in wp_monotonic_plain) apply clarsimp apply assumption apply (erule notE) apply (rule_tac P="Q'" in wp_monotonic_plain) apply clarsimp apply assumption apply (clarsimp simp add: imp_b_def and_b_def or_b_def not_b_def bvalid_def) apply (case_tac "B s", simp_all) done lemma WeakestWhileCase: "\(*\P Q. \P\C'\Q\ \ |\ (P [\] (wp C' Q));*) \P\While B Inv I Do C' Od\Q\ \ \ |\ (P [\] I)" apply (subgoal_tac "\ C. (\P\C \Q\) \ ((C = (While B Inv I Do C' Od)) \ |\ (P [\] I))") apply clarsimp apply (thin_tac "\P\While B Inv I Do C' Od\Q\") apply (rule allI, rule impI) apply (erule ann_valid.induct) apply simp_all apply (clarsimp simp add: imp_b_def bvalid_def) done lemma wp_always_weaker: "\P Q. \P\C\Q\ \ |\ (P [\] (wp C Q))" apply (induct C) apply auto apply (erule weakestAssignCase) apply (erule weakestSeqCase) apply assumption apply assumption apply (erule WeakestIfCase) apply assumption+ apply (erule WeakestWhileCase) done fun vcg :: "'data annotated_command \ 'data bool_exp \ 'data bool_exp" where vcg_Asg: "vcg (v := e) Q = true_b" | vcg_Seq: "vcg (C;;C') Q = (vcg C (wp C' Q)) [\] (vcg C' Q)" | vcg_If: "vcg (If B Then C Else C' Fi) Q = (vcg C Q) [\] (vcg C' Q)" | vcg_While: "vcg (While B Inv I Do C Od) Q = (((I [\] B) [\] (wp C I)) [\] (vcg C I) [\] (((I [\] ([\] B)) [\] Q)))" lemma vcg_imp_wp_good_enough[rule_format]: "\ Q. |\ (vcg C Q) \ \wp C Q\C\Q\" apply (induct C) apply auto apply (rule AnnAssignmentAxiom) apply (rule_tac Q = "wp C2 Q" in AnnSequenceRule) apply (erule allE, erule mp, erule bvalid_and_bE, clarsimp) apply (erule allE, erule mp, erule bvalid_and_bE, clarsimp) apply (rule AnnIfThenElseRule) apply (rule_tac P' = "wp C1 Q" in AnnPreconditionStrengthening) apply (clarsimp simp add: bvalid_def imp_b_def and_b_def or_b_def not_b_def) apply (erule allE, erule mp, erule bvalid_and_bE, clarsimp) apply (rule_tac P' = "wp C2 Q" in AnnPreconditionStrengthening) apply (clarsimp simp add: bvalid_def imp_b_def and_b_def or_b_def not_b_def) apply (erule allE, erule mp, erule bvalid_and_bE, clarsimp) apply (rule_tac Q' = "fun2 [\] ([\] fun1)" in AnnPostconditionWeakening) apply (erule bvalid_and_bE)+ apply assumption apply (rule AnnWhileRule) apply (rule_tac P' = "wp C fun2" in AnnPreconditionStrengthening) apply (erule bvalid_and_bE)+ apply assumption apply (erule bvalid_and_bE)+ apply auto done corollary vcg_and_P: "|\ ((P [\] wp C Q) [\] (vcg C Q)) \ \P\C\Q\" apply (erule bvalid_and_bE) apply (erule_tac P' = "wp C Q" in AnnPreconditionStrengthening) apply (erule vcg_imp_wp_good_enough) done lemma vcg_monotonic[rule_format]: "\ P Q. |\ (P [\] Q) \ |\ (vcg C P [\] vcg C Q)" apply (induct C) apply auto apply (clarsimp simp add: bvalid_def imp_b_def and_b_def) apply (erule_tac P = "vcg C1 (wp C2 P) s" in rev_mp) apply (erule_tac x="(wp C2 P)" in allE, erule_tac x="(wp C2 Q)" in allE, erule impE) apply (clarsimp, rule_tac P = "P" in wp_monotonic_plain) apply clarsimp apply assumption apply clarsimp apply (clarsimp simp add: bvalid_def imp_b_def and_b_def) apply (clarsimp simp add: bvalid_def imp_b_def and_b_def not_b_def) done lemma vcg_monotonic_plain: "\(\ s. P s \ Q s); vcg C P s\ \ vcg C Q s" apply (cut_tac P="P" and Q="Q" and C="C" in vcg_monotonic) apply (clarsimp simp add: bvalid_def imp_b_def) apply (clarsimp simp add: bvalid_def imp_b_def) done lemma triple_implies_vcg : "\P\C\Q\ \ |\ ((P [\] wp C Q) [\] (vcg C Q))" apply (erule ann_valid.induct) apply simp_all apply (erule bvalid_and_bE) apply (erule bvalid_and_bE) apply (rule bvalid_and_bI) apply (clarsimp simp add: imp_b_def and_b_def bvalid_def) apply (rule_tac P="Q" in wp_monotonic_plain) apply clarsimp apply clarsimp apply (rule bvalid_and_bI) apply (clarsimp simp add: imp_b_def and_b_def bvalid_def) thm vcg_monotonic_plain wp_monotonic_plain apply (erule_tac P="Q" in vcg_monotonic_plain) apply clarsimp apply assumption apply (erule bvalid_and_bE) apply (rule bvalid_and_bI) apply (clarsimp simp add: imp_b_def bvalid_def) thm wp_monotonic_plain apply (rule_tac P="Q'" in wp_monotonic_plain) apply clarsimp apply clarsimp apply (clarsimp simp add: imp_b_def bvalid_def) apply (erule_tac P="Q'" in vcg_monotonic_plain) apply clarsimp apply (erule bvalid_and_bE)+ apply (rule bvalid_and_bI) apply (clarsimp simp add: bvalid_def imp_b_def and_b_def or_b_def not_b_def) apply (erule_tac x = "s" in allE)+ apply (case_tac "B s", simp_all) done end