diff --git a/src/HOL/Hoare/ExamplesTC.thy b/src/HOL/Hoare/ExamplesTC.thy --- a/src/HOL/Hoare/ExamplesTC.thy +++ b/src/HOL/Hoare/ExamplesTC.thy @@ -1,133 +1,133 @@ (* Title: Examples using Hoare Logic for Total Correctness Author: Walter Guttmann *) section \Examples using Hoare Logic for Total Correctness\ theory ExamplesTC imports Hoare_Logic begin text \ This theory demonstrates a few simple partial- and total-correctness proofs. The first example is taken from HOL/Hoare/Examples.thy written by N. Galm. We have added the invariant \m \ a\. \ lemma multiply_by_add: "VARS m s a b {a=A \ b=B} m := 0; s := 0; WHILE m\a INV {s=m*b \ a=A \ b=B \ m\a} DO s := s+b; m := m+(1::nat) OD {s = A*B}" by vcg_simp text \ Here is the total-correctness proof for the same program. It needs the additional invariant \m \ a\. \ -ML \\<^const_syntax>\HOL.eq\\ + lemma multiply_by_add_tc: "VARS m s a b [a=A \ b=B] m := 0; s := 0; WHILE m\a INV {s=m*b \ a=A \ b=B \ m\a} VAR {a-m} DO s := s+b; m := m+(1::nat) OD [s = A*B]" apply vcg_tc_simp by auto text \ Next, we prove partial correctness of a program that computes powers. \ lemma power: "VARS (p::int) i { True } p := 1; i := 0; WHILE i < n INV { p = x^i \ i \ n } DO p := p * x; i := i + 1 OD { p = x^n }" apply vcg_simp by auto text \ Here is its total-correctness proof. \ lemma power_tc: "VARS (p::int) i [ True ] p := 1; i := 0; WHILE i < n INV { p = x^i \ i \ n } VAR { n - i } DO p := p * x; i := i + 1 OD [ p = x^n ]" apply vcg_tc by auto text \ The last example is again taken from HOL/Hoare/Examples.thy. We have modified it to integers so it requires precondition \0 \ x\. \ lemma sqrt_tc: "VARS r [0 \ (x::int)] r := 0; WHILE (r+1)*(r+1) <= x INV {r*r \ x} VAR { nat (x-r)} DO r := r+1 OD [r*r \ x \ x < (r+1)*(r+1)]" apply vcg_tc_simp by (smt (verit) div_pos_pos_trivial mult_less_0_iff nonzero_mult_div_cancel_left) text \ A total-correctness proof allows us to extract a function for further use. For every input satisfying the precondition the function returns an output satisfying the postcondition. \ lemma sqrt_exists: "0 \ (x::int) \ \r' . r'*r' \ x \ x < (r'+1)*(r'+1)" using tc_extract_function sqrt_tc by blast definition "sqrt (x::int) \ (SOME r' . r'*r' \ x \ x < (r'+1)*(r'+1))" lemma sqrt_function: assumes "0 \ (x::int)" and "r' = sqrt x" shows "r'*r' \ x \ x < (r'+1)*(r'+1)" proof - let ?P = "\r' . r'*r' \ x \ x < (r'+1)*(r'+1)" have "?P (SOME z . ?P z)" by (metis (mono_tags, lifting) assms(1) sqrt_exists some_eq_imp) thus ?thesis using assms(2) sqrt_def by auto qed text \Nested loops!\ lemma "VARS (i::nat) j [ True ] WHILE 0 < i INV { True } VAR { z = i } DO i := i - 1; j := i; WHILE 0 < j INV { z = i+1 } VAR { j } DO j := j - 1 OD OD [ i \ 0 ]" apply vcg_tc by auto end