theory sol09 imports "HOL-IMP.Hoare_Sound_Complete" begin definition Max :: com where "Max \ IF Less (V ''a'') (V ''b'') THEN ''c'' ::= V ''b'' ELSE ''c'' ::= V ''a''" lemma [simp]: "(a :: int) < b \ max a b = b" by auto lemma [simp]: "\ (a :: int) < b \ max a b = a" by auto lemma "\ {\ s. True} Max {\ s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding Max_def apply (rule If) apply (rule Assign') apply simp apply (rule Assign') apply simp done definition MUL :: com where "MUL \ ''c'' ::= N 0;; ''z'' ::= 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 proof let ?Q = "\ s. s ''c'' \ s ''y'' \ s ''z'' = s ''c'' * s ''x''" show "\ {\ s. 0 \ s ''y''} ''c'' ::= N 0;; ''z'' ::= N 0 {?Q}" apply (rule Seq[rotated]) apply (rule Assign) apply (rule Assign') apply simp done show " \ {?Q} WHILE Less (V ''c'') (V ''y'') DO (''z'' ::= Plus (V ''z'') (V ''x'');; ''c'' ::= Plus (V ''c'') (N 1)) {\ s. s ''z'' = s ''x'' * s ''y''}" apply (rule While') apply (rule Seq[rotated]) apply (rule Assign) apply (rule Assign') apply (auto simp: algebra_simps) done qed definition "MAX_wrong \ ''a'' ::= N 0;; ''b'' ::= N 0;; ''c'' ::= N 0" lemma "\ {\ s. True} MAX_wrong {\ s. s ''c'' = max (s ''a'') (s ''b'')}" unfolding MAX_wrong_def apply (rule Seq[rotated]) apply (rule Assign) apply (rule Seq[rotated]) apply (rule Assign) apply (rule Assign') apply simp done lemma "\ {\ s. a = s ''a'' \ b = s ''b''} Max {\ s. s ''c'' = max a b \ a = s ''a'' \ b = s ''b''}" unfolding Max_def apply (rule If) apply (rule Assign') apply simp apply (rule Assign') apply simp done lemma "\ {\ s. x = s ''x'' \ y = s ''y'' \ 0 \ y} MUL {\ s. x = s ''x'' \ y = s ''y'' \ s ''z'' = x * y}" unfolding MUL_def proof let ?Q = "\ s. x = s ''x'' \ y = s ''y'' \ s ''c'' \ y \ s ''z'' = s ''c'' * x" show "\ {\ s. x = s ''x'' \ y = s ''y'' \ 0 \ y} ''c'' ::= N 0;; ''z'' ::= N 0 {?Q}" apply (rule Seq[rotated]) apply (rule Assign) apply (rule Assign') apply simp done show " \ {?Q} WHILE Less (V ''c'') (V ''y'') DO (''z'' ::= Plus (V ''z'') (V ''x'');; ''c'' ::= Plus (V ''c'') (N 1)) {\ s. x = s ''x'' \ y = s ''y'' \ s ''z'' = x * y}" apply (rule While') apply (rule Seq[rotated]) apply (rule Assign) apply (rule Assign') apply (auto simp: algebra_simps) done qed lemma fwd_Assign: "\ {P} x ::= a {\ s'. \ s. s' = s[a/x] \ P s}" unfolding hoare_sound_complete hoare_valid_def by auto lemmas fwd_Assign' = weaken_post[OF 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 lemma "\ {\ s. 0 \ s ''y''} MUL {\ s. s ''z'' = s ''x'' * s ''y''}" unfolding MUL_def proof let ?Q = "\ s. s ''c'' \ s ''y'' \ s ''z'' = s ''c'' * s ''x''" show "\ {\ s. 0 \ s ''y''} ''c'' ::= N 0;; ''z'' ::= N 0 {?Q}" apply (rule Seq) apply (rule fwd_Assign) apply (rule fwd_Assign') apply auto done show " \ {?Q} WHILE Less (V ''c'') (V ''y'') DO (''z'' ::= Plus (V ''z'') (V ''x'');; ''c'' ::= Plus (V ''c'') (N 1)) {\ s. s ''z'' = s ''x'' * s ''y''}" apply (rule While') apply (rule Seq) apply (rule fwd_Assign) apply (rule fwd_Assign') apply (auto simp: algebra_simps) done qed end