theory sol12 imports "~~/src/HOL/IMP/VCG" "~~/src/HOL/IMP/Hoare_Total" "~~/src/HOL/Complex_Main" begin text {* \ExerciseSheet{12}{24.~01.~2017} \Exercise{Using the VCG} Use the VCG to prove correct a multiplication and a square root program: *} 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))" abbreviation "MUL_invar sorig s \ s ''z'' = s ''x'' * s ''c'' \ s ''c'' \ s ''y'' \ (\v. v\{''z'',''c''} \ s v = sorig v)" definition MUL_annot :: "state \ acom" where "MUL_annot sorig \ ''z''::=N 0;; ''c''::=N 0;; {MUL_invar sorig} WHILE (Less (V ''c'') (V ''y'')) DO ( ''z''::=Plus (V ''z'') (V ''x'');; ''c''::=Plus (V ''c'') (N 1))" lemma MUL_annot_strip: "strip (MUL_annot sorig) = MUL" unfolding MUL_def MUL_annot_def by auto lemma "\ {\s. 0 \ s ''y'' \ s=sorig} MUL {\s. s ''z'' = s ''x'' * s ''y'' \ (\v. v\{''z'',''c''} \ s v = sorig v)}" unfolding MUL_annot_strip[of sorig,symmetric] apply (rule vc_sound') apply (auto simp: MUL_annot_def algebra_simps) done definition "SQRT \ ''r'' ::= N 0;; ''s'' ::= N 1;; WHILE (Not (Less (V ''x'') (V ''s''))) DO ( ''r'' ::= Plus (V ''r'') (N 1);; ''s'' ::= Plus (V ''s'') (V ''r'');; ''s'' ::= Plus (V ''s'') (V ''r'');; ''s'' ::= Plus (V ''s'') (N 1) )" abbreviation "SQRT_invar sorig s \ s ''s'' = (s ''r'' + 1)^2 \ s ''r'' \ 0 \ (s ''r'')^2 \ s ''x'' \ (\v. v\{''r'',''s''} \ s v = sorig v) " definition "SQRT_annot sorig \ ''r'' ::= N 0;; ''s'' ::= N 1;; {SQRT_invar sorig} WHILE (Not (Less (V ''x'') (V ''s''))) DO ( ''r'' ::= Plus (V ''r'') (N 1);; ''s'' ::= Plus (V ''s'') (V ''r'');; ''s'' ::= Plus (V ''s'') (V ''r'');; ''s'' ::= Plus (V ''s'') (N 1) )" lemma SQRT_strip: "strip (SQRT_annot sorig) = SQRT" unfolding SQRT_annot_def SQRT_def by auto lemma "\ {\s. s=sorig \ s ''x'' \ 0} SQRT {\s. (s ''r'')^2 \ s ''x'' \ s ''x'' < (s ''r''+1)^2 \ (\v. v\{''s'',''r''} \ s v = sorig v)}" unfolding SQRT_strip[of sorig, symmetric] apply (rule vc_sound') apply (auto simp add: SQRT_annot_def power2_eq_square algebra_simps) done text \ \Exercise{Total Correctness} Prove total correctness of the multiplication and the square root program. \ text {* Prove the following syntax-directed conditional rule (for total correctness): *} lemma IfT: assumes "\\<^sub>t {P1} c\<^sub>1 {Q}" and "\\<^sub>t {P2} c\<^sub>2 {Q}" shows "\\<^sub>t {\s. (bval b s \ P1 s) \ (\ bval b s \ P2 s)} IF b THEN c\<^sub>1 ELSE c\<^sub>2 {Q}" by (auto intro: assms hoaret.intros) lemmas Seq_bwd = Hoare_Total.Seq[rotated] lemmas hoareT_rule[intro?] = Seq_bwd Hoare_Total.Assign Hoare_Total.Assign' IfT lemma "\\<^sub>t {\s. 0 \ s ''y'' \ s=sorig} MUL {\s. s ''z'' = s ''x'' * s ''y'' \ (\v. v\{''z'',''c''} \ s v = sorig v)}" unfolding MUL_def by (rule hoareT_rule Hoare_Total.While_fun'[where P="MUL_invar sorig" and f="\s. nat (s ''y'' - s ''c'')"] | auto simp add: algebra_simps [])+ lemma "\\<^sub>t {\s. s=sorig \ s ''x'' \ 0} SQRT {\s. (s ''r'')^2 \ s ''x'' \ s ''x'' < (s ''r''+1)^2 \ (\v. v\{''s'',''r''} \ s v = sorig v)}" unfolding SQRT_def apply (rule hoareT_rule Hoare_Total.While_fun'[where P="SQRT_invar sorig" and f="\s. nat (s ''x'' - s ''r''* s ''r'')"] | auto simp add: algebra_simps power2_eq_square [])+ done end