# Theory Examples

theory Examples
imports Hoare_Logic Arith2
```(*  Title:      HOL/Hoare/Examples.thy
Author:     Norbert Galm

Various examples.
*)

theory Examples imports Hoare_Logic Arith2 begin

(*** ARITHMETIC ***)

(** multiplication by successive addition **)

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}
DO s := s+b; m := m+(1::nat) OD
{s = A*B}"
by vcg_simp

lemma multiply_by_add_time: "VARS m s a b t
{a=A & b=B & t=0}
m := 0; t := t+1; s := 0; t := t+1;
WHILE m~=a
INV {s=m*b & a=A & b=B & t = 2*m + 2}
DO s := s+b; t := t+1; m := m+(1::nat); t := t+1 OD
{s = A*B ∧ t = 2*A + 2}"
by vcg_simp

lemma multiply_by_add2: "VARS M N P :: int
{m=M & n=N}
IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
P := 0;
WHILE 0 < M
INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
DO P := P+N; M := M - 1 OD
{P = m*n}"
apply vcg_simp
done

lemma multiply_by_add2_time: "VARS M N P t :: int
{m=M & n=N & t=0}
IF M < 0 THEN M := -M; t := t+1; N := -N; t := t+1 ELSE SKIP FI;
P := 0; t := t+1;
WHILE 0 < M
INV {0 ≤ M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N & t ≥ 0 & t ≤ 2*(p-M)+3)}
DO P := P+N; t := t+1; M := M - 1; t := t+1 OD
{P = m*n & t ≤ 2*abs m + 3}"
apply vcg_simp
done

(** Euclid's algorithm for GCD **)

lemma Euclid_GCD: "VARS a b
{0<A & 0<B}
a := A; b := B;
WHILE  a ≠ b
INV {0<a & 0<b & gcd A B = gcd a b}
DO IF a<b THEN b := b-a ELSE a := a-b FI OD
{a = gcd A B}"
apply vcg
(*Now prove the verification conditions*)
apply auto
apply(erule gcd_nnn)
done

lemma Euclid_GCD_time: "VARS a b t
{0<A & 0<B & t=0}
a := A; t := t+1; b := B; t := t+1;
WHILE  a ≠ b
INV {0<a & 0<b & gcd A B = gcd a b & a≤A & b≤B & t ≤ max A B - max a b + 2}
DO IF a<b THEN b := b-a; t := t+1 ELSE a := a-b; t := t+1 FI OD
{a = gcd A B & t ≤ max A B + 2}"
apply vcg
(*Now prove the verification conditions*)
apply auto
apply(erule gcd_nnn)
done

(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
where it is given without the invariant. Instead of defining scm
explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
division by mupltiplying with gcd x y.
*)

lemmas distribs =

lemma gcd_scm: "VARS a b x y
{0<A & 0<B & a=A & b=B & x=B & y=A}
WHILE  a ~= b
INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
{a = gcd A B & 2*A*B = a*(x+y)}"
apply vcg
apply simp
apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
done

(** Power by iterated squaring and multiplication **)

lemma power_by_mult: "VARS a b c
{a=A & b=B}
c := (1::nat);
WHILE b ~= 0
INV {A^B = c * a^b}
DO  WHILE b mod 2 = 0
INV {A^B = c * a^b}
DO  a := a*a; b := b div 2 OD;
c := c*a; b := b - 1
OD
{c = A^B}"
apply vcg_simp
apply(case_tac "b")
apply simp
apply simp
done

(** Factorial **)

lemma factorial: "VARS a b
{a=A}
b := 1;
WHILE a > 0
INV {fac A = b * fac a}
DO b := b*a; a := a - 1 OD
{b = fac A}"
apply vcg_simp
apply(clarsimp split: nat_diff_split)
done

lemma factorial_time: "VARS a b t
{a=A & t=0}
b := 1; t := t+1;
WHILE a > 0
INV {fac A = b * fac a & a ≤ A & t = 2*(A-a)+1}
DO b := b*a; t := t+1; a := a - 1; t := t+1 OD
{b = fac A & t = 2*A + 1}"
apply vcg_simp
apply(clarsimp split: nat_diff_split)
done

lemma [simp]: "1 ≤ i ⟹ fac (i - Suc 0) * i = fac i"
by(induct i, simp_all)

lemma factorial2: "VARS i f
{True}
i := (1::nat); f := 1;
WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
DO f := f*i; i := i+1 OD
{f = fac n}"
apply vcg_simp
apply(subgoal_tac "i = Suc n")
apply simp
apply arith
done

lemma factorial2_time: "VARS i f t
{t=0}
i := (1::nat); t := t+1; f := 1; t := t+1;
WHILE i ≤ n INV {f = fac(i - 1) & 1 ≤ i & i ≤ n+1 & t = 2*(i-1)+2}
DO f := f*i; t := t+1; i := i+1; t := t+1 OD
{f = fac n & t = 2*n+2}"
apply vcg_simp
apply auto
apply(subgoal_tac "i = Suc n")
apply simp
apply arith
done

(** Square root **)

(* the easy way: *)

lemma sqrt: "VARS r x
{True}
r := (0::nat);
WHILE (r+1)*(r+1) <= X
INV {r*r ≤ X}
DO r := r+1 OD
{r*r <= X & X < (r+1)*(r+1)}"
apply vcg_simp
done

lemma sqrt_time: "VARS r t
{t=0}
r := (0::nat); t := t+1;
WHILE (r+1)*(r+1) <= X
INV {r*r ≤ X & t = r+1}
DO r := r+1; t := t+1 OD
{r*r <= X & X < (r+1)*(r+1) & (t-1)*(t-1) ≤ X}"
apply vcg_simp
done

(* without multiplication *)

lemma sqrt_without_multiplication: "VARS u w r
{x=X}
u := 1; w := 1; r := (0::nat);
WHILE w <= X
INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= X}
DO r := r + 1; w := w + u + 2; u := u + 2 OD
{r*r <= X & X < (r+1)*(r+1)}"
apply vcg_simp
done

(*** LISTS ***)

lemma imperative_reverse: "VARS y x
{x=X}
y:=[];
WHILE x ~= []
INV {rev(x)@y = rev(X)}
DO y := (hd x # y); x := tl x OD
{y=rev(X)}"
apply vcg_simp
apply auto
done

lemma imperative_reverse_time: "VARS y x t
{x=X & t=0}
y:=[]; t := t+1;
WHILE x ~= []
INV {rev(x)@y = rev(X) & t = 2*(length y) + 1}
DO y := (hd x # y); t := t+1; x := tl x; t := t+1 OD
{y=rev(X) & t = 2*length X + 1}"
apply vcg_simp
apply auto
done

lemma imperative_append: "VARS x y
{x=X & y=Y}
x := rev(x);
WHILE x~=[]
INV {rev(x)@y = X@Y}
DO y := (hd x # y);
x := tl x
OD
{y = X@Y}"
apply vcg_simp
apply auto
done

lemma imperative_append_time_no_rev: "VARS x y t
{x=X & y=Y}
x := rev(x); t := 0;
WHILE x~=[]
INV {rev(x)@y = X@Y & length x ≤ length X & t = 2 * (length X - length x)}
DO y := (hd x # y); t := t+1;
x := tl x; t := t+1
OD
{y = X@Y & t = 2 * length X}"
apply vcg_simp
apply auto
done

(*** ARRAYS ***)

(* Search for a key *)
lemma zero_search: "VARS A i
{True}
i := 0;
WHILE i < length A & A!i ~= key
INV {!j. j<i --> A!j ~= key}
DO i := i+1 OD
{(i < length A --> A!i = key) &
(i = length A --> (!j. j < length A --> A!j ~= key))}"
apply vcg_simp
apply(blast elim!: less_SucE)
done

lemma zero_search_time: "VARS A i t
{t=0}
i := 0; t := t+1;
WHILE i < length A & A!i ~= key
INV {(∀j. j<i --> A!j ~= key) & i ≤ length A & t = i+1}
DO i := i+1; t := t+1 OD
{(i < length A --> A!i = key) &
(i = length A --> (!j. j < length A --> A!j ~= key)) & t ≤ length A + 1}"
apply vcg_simp
apply(blast elim!: less_SucE)
done

(*
The `partition' procedure for quicksort.
`A' is the array to be sorted (modelled as a list).
Elements of A must be of class order to infer at the end
that the elements between u and l are equal to pivot.

Ambiguity warnings of parser are due to := being used
both for assignment and list update.
*)
lemma lem: "m - Suc 0 < n ==> m < Suc n"
by arith

lemma Partition:
"[| leq == %A i. !k. k<i --> A!k <= pivot;
geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
VARS A u l
{0 < length(A::('a::order)list)}
l := 0; u := length A - Suc 0;
WHILE l <= u
INV {leq A l & geq A u & u<length A & l<=length A}
DO WHILE l < length A & A!l <= pivot
INV {leq A l & geq A u & u<length A & l<=length A}
DO l := l+1 OD;
WHILE 0 < u & pivot <= A!u
INV {leq A l & geq A u  & u<length A & l<=length A}
DO u := u - 1 OD;
IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
OD
{leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
(* expand and delete abbreviations first *)
apply (simp)
apply (erule thin_rl)+
apply vcg_simp
apply (force simp: neq_Nil_conv)
apply (blast elim!: less_SucE intro: Suc_leI)
apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
apply (force simp: nth_list_update)
done

end
```