(*<*) theory ex10 imports "Hoare_Sound_Complete" begin (*>*) text {* \ExerciseSheet{10}{18.~12.~2012} *} text {* \Exercise{Forward Assignment Rule} Think up and prove a forward assignment rule, i.e., a rule of the form @{text "\ {P} x::=a {\}"}, where @{text "\"} is some suitable postcondition. Hint: To prove this rule, use the completeness property, and prove the rule semantically. *} lemma fwd_Assign: "\ {P} x::=a { \s'. \s. P s \ s'=s[a/x]}" apply (rule hoare_relative_complete) unfolding hoare_valid_def apply auto done text {* Redo the proofs for @{text "MAX"} and @{text "MUL"} from the previous exercise sheet, this time using your forward assignment rule. *} (*<*) definition MAX :: com where "MAX \ IF (Less (V ''a'') (V ''b'')) THEN ''c''::=V ''b'' ELSE ''c''::=V ''a''" lemma [simp]: "(a::int) max a b = b" by (metis order_less_imp_le sup_absorb2 sup_int_def) lemma [simp]: "\(a::int) max a b = a" by (metis leI min_max.sup_absorb1) lemmas fwd_Assign' = weaken_post[OF fwd_Assign] thm fwd_Assign' lemma "\ {\s. True} MAX {\s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_def apply (rule If) apply (rule fwd_Assign') apply (auto) [] apply (rule fwd_Assign') apply (auto) [] done definition MUL :: com where "MUL \ ''z''::=N 0; ''c''::=N 0; WHILE (Less (V ''c'') (V ''y'')) DO ( ''z''::=Plus (V ''z'') (V ''x''); ''c''::=Plus (V ''c'') (N 1))" lemma "\ {\s. 0 \ s ''y''} MUL {\s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_def apply (rule If Seq Skip fwd_Assign fwd_Assign')+ apply (rule conseq[OF _ While, where P="%s. s ''c'' \ s ''y'' \ s ''z'' = s ''x'' * s ''c'' "]) apply auto [] apply (rule If Seq Skip fwd_Assign fwd_Assign')+ apply (auto simp: algebra_simps) [] apply (auto simp: algebra_simps) [] done text {* \Exercise{More Hoare-Rules} Which of the following Hoare-rules are correct? Proof or counterexample! *} (*<*) lemma hoare_by_sem: "\ {P}c{Q} \ \ {P}c{Q}" by (blast intro: hoare_sound hoare_relative_complete) lemma "\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}" apply (simp only: hoare_by_sem hoare_valid_def) apply blast done lemma "\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}" apply (simp only: hoare_by_sem hoare_valid_def) apply blast done lemma "\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}" apply (simp only: hoare_by_sem hoare_valid_def) nitpick oops lemma defines "P\\x. False" and "Q\\x. True" and "P'\\x. False" and "Q'\\x. False" and "c\SKIP" shows "\ {P} c {Q} \ \ {P'} c {Q'} \ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}" apply (simp add: hoare_by_sem) unfolding hoare_valid_def P_def Q_def P'_def Q'_def c_def by blast (*<*) lemma defines "P\\x. False" and "Q\\x. True" and "P'\\x. False" and "Q'\\x. False" and "c\SKIP" shows "(\\ {P} c {Q}; \ {P'} c {Q'}\ \ \ {\s. P s \ P' s} c {\s. Q s \ Q' s}) \ False" apply (simp add: hoare_by_sem) unfolding hoare_valid_def P_def Q_def P'_def Q'_def c_def apply blast done end (*>*)