(*<*) theory tut12 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 ''c'' * s ''x'' \ 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 (simp_all add: MUL_annot_def) apply (simp add: algebra_simps) by auto 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 \ (\v. v\{''s'',''r''} \ s v = sorig v) \ s ''s'' = (s ''r'' + 1) * (s ''r'' + 1) \ (s ''r'')^2 \ s ''x'' \ s ''r'' \ 0 " definition SQRT_annot where "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_annot_SQRT: "strip (SQRT_annot sorig) = SQRT" unfolding SQRT_annot_def SQRT_def by simp lemma aux: "n \ 0 \ 1 + (2 * (n :: int) + n * n) = (n + 1) ^ 2" by algebra 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_annot_SQRT[symmetric, of sorig] apply (rule vc_sound') apply (simp_all add: SQRT_annot_def) apply (simp_all add: algebra_simps) apply auto apply (auto simp add: aux) apply (simp_all add: algebra_simps) done end