--- a/src/HOL/Hoare/Examples.thy Fri May 20 07:54:54 2016 +0200
+++ b/src/HOL/Hoare/Examples.thy Sat May 21 07:08:46 2016 +0200
@@ -20,7 +20,16 @@
{s = A*B}"
by vcg_simp
-lemma "VARS M N P :: int
+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 \<and> 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;
@@ -29,11 +38,19 @@
DO P := P+N; M := M - 1 OD
{P = m*n}"
apply vcg_simp
- apply (simp add:int_distrib)
-apply clarsimp
-apply(rule conjI)
- apply clarsimp
-apply clarsimp
+ apply (auto simp add:int_distrib)
+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 \<le> M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N & t \<ge> 0 & t \<le> 2*(p-M)+3)}
+ DO P := P+N; t := t+1; M := M - 1; t := t+1 OD
+ {P = m*n & t \<le> 2*abs m + 3}"
+apply vcg_simp
+ apply (auto simp add:int_distrib)
done
(** Euclid's algorithm for GCD **)
@@ -53,6 +70,21 @@
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 \<noteq> b
+ INV {0<a & 0<b & gcd A B = gcd a b & a\<le>A & b\<le>B & t \<le> 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 \<le> max A B + 2}"
+apply vcg
+(*Now prove the verification conditions*)
+ apply auto
+ apply(simp add: gcd_diff_r less_imp_le)
+ apply(simp add: linorder_not_less gcd_diff_l)
+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
@@ -99,7 +131,7 @@
lemma factorial: "VARS a b
{a=A}
b := 1;
- WHILE a ~= 0
+ WHILE a > 0
INV {fac A = b * fac a}
DO b := b*a; a := a - 1 OD
{b = fac A}"
@@ -107,10 +139,21 @@
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 \<le> 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 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
by(induct i, simp_all)
-lemma "VARS i f
+lemma factorial2: "VARS i f
{True}
i := (1::nat); f := 1;
WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
@@ -122,27 +165,50 @@
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 \<le> n INV {f = fac(i - 1) & 1 \<le> i & i \<le> 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}
- x := X; r := (0::nat);
- WHILE (r+1)*(r+1) <= x
- INV {r*r <= x & x=X}
+ r := (0::nat);
+ WHILE (r+1)*(r+1) <= X
+ INV {r*r \<le> 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 \<le> X & t = r+1}
+ DO r := r+1; t := t+1 OD
+ {r*r <= X & X < (r+1)*(r+1) & (t-1)*(t-1) \<le> X}"
+apply vcg_simp
+done
+
(* without multiplication *)
-lemma sqrt_without_multiplication: "VARS u w r x
- {True}
- 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 & x=X}
+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
@@ -163,6 +229,18 @@
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(simp add: neq_Nil_conv)
+ apply auto
+done
+
lemma imperative_append: "VARS x y
{x=X & y=Y}
x := rev(x);
@@ -177,6 +255,20 @@
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 \<le> 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(simp add: neq_Nil_conv)
+apply auto
+done
+
(*** ARRAYS ***)
@@ -193,6 +285,18 @@
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 {(\<forall>j. j<i --> A!j ~= key) & i \<le> 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 \<le> 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).