# HG changeset patch
# User nipkow
# Date 1463807339 -7200
# Node ID 932cf444f2fe6d661d3cae3b5d7dfd342f2c88ca
# Parent  c445b0924e3ab18f6e57bac46dfac4a63bb3e1f3# Parent  412140038d3c6c309cb97bba403a670d83cb76aa
merged

diff -r c445b0924e3a -r 932cf444f2fe src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Fri May 20 22:01:42 2016 +0200
+++ b/src/HOL/Hoare/Examples.thy	Sat May 21 07:08:59 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).