author nipkow Sat May 21 07:08:46 2016 +0200 (2016-05-21 ago) changeset 63106 412140038d3c parent 63102 71059cf60658 child 63107 932cf444f2fe
```     1.1 --- a/src/HOL/Hoare/Examples.thy	Fri May 20 07:54:54 2016 +0200
1.2 +++ b/src/HOL/Hoare/Examples.thy	Sat May 21 07:08:46 2016 +0200
1.3 @@ -20,7 +20,16 @@
1.4    {s = A*B}"
1.5  by vcg_simp
1.6
1.7 -lemma "VARS M N P :: int
1.8 +lemma multiply_by_add_time: "VARS m s a b t
1.9 +  {a=A & b=B & t=0}
1.10 +  m := 0; t := t+1; s := 0; t := t+1;
1.11 +  WHILE m~=a
1.12 +  INV {s=m*b & a=A & b=B & t = 2*m + 2}
1.13 +  DO s := s+b; t := t+1; m := m+(1::nat); t := t+1 OD
1.14 +  {s = A*B \<and> t = 2*A + 2}"
1.15 +by vcg_simp
1.16 +
1.17 +lemma multiply_by_add2: "VARS M N P :: int
1.18   {m=M & n=N}
1.19   IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
1.20   P := 0;
1.21 @@ -29,11 +38,19 @@
1.22   DO P := P+N; M := M - 1 OD
1.23   {P = m*n}"
1.24  apply vcg_simp
1.26 -apply clarsimp
1.27 -apply(rule conjI)
1.28 - apply clarsimp
1.29 -apply clarsimp
1.30 + apply (auto simp add:int_distrib)
1.31 +done
1.32 +
1.33 +lemma multiply_by_add2_time: "VARS M N P t :: int
1.34 + {m=M & n=N & t=0}
1.35 + IF M < 0 THEN M := -M; t := t+1; N := -N; t := t+1 ELSE SKIP FI;
1.36 + P := 0; t := t+1;
1.37 + WHILE 0 < M
1.38 + 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)}
1.39 + DO P := P+N; t := t+1; M := M - 1; t := t+1 OD
1.40 + {P = m*n & t \<le> 2*abs m + 3}"
1.41 +apply vcg_simp
1.42 + apply (auto simp add:int_distrib)
1.43  done
1.44
1.45  (** Euclid's algorithm for GCD **)
1.46 @@ -53,6 +70,21 @@
1.47  apply(erule gcd_nnn)
1.48  done
1.49
1.50 +lemma Euclid_GCD_time: "VARS a b t
1.51 + {0<A & 0<B & t=0}
1.52 + a := A; t := t+1; b := B; t := t+1;
1.53 + WHILE  a \<noteq> b
1.54 + 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}
1.55 + DO IF a<b THEN b := b-a; t := t+1 ELSE a := a-b; t := t+1 FI OD
1.56 + {a = gcd A B & t \<le> max A B + 2}"
1.57 +apply vcg
1.58 +(*Now prove the verification conditions*)
1.59 +  apply auto
1.60 +  apply(simp add: gcd_diff_r less_imp_le)
1.61 + apply(simp add: linorder_not_less gcd_diff_l)
1.62 +apply(erule gcd_nnn)
1.63 +done
1.64 +
1.65  (** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
1.66  (* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
1.67     where it is given without the invariant. Instead of defining scm
1.68 @@ -99,7 +131,7 @@
1.69  lemma factorial: "VARS a b
1.70   {a=A}
1.71   b := 1;
1.72 - WHILE a ~= 0
1.73 + WHILE a > 0
1.74   INV {fac A = b * fac a}
1.75   DO b := b*a; a := a - 1 OD
1.76   {b = fac A}"
1.77 @@ -107,10 +139,21 @@
1.78  apply(clarsimp split: nat_diff_split)
1.79  done
1.80
1.81 +lemma factorial_time: "VARS a b t
1.82 + {a=A & t=0}
1.83 + b := 1; t := t+1;
1.84 + WHILE a > 0
1.85 + INV {fac A = b * fac a & a \<le> A & t = 2*(A-a)+1}
1.86 + DO b := b*a; t := t+1; a := a - 1; t := t+1 OD
1.87 + {b = fac A & t = 2*A + 1}"
1.88 +apply vcg_simp
1.89 +apply(clarsimp split: nat_diff_split)
1.90 +done
1.91 +
1.92  lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
1.93  by(induct i, simp_all)
1.94
1.95 -lemma "VARS i f
1.96 +lemma factorial2: "VARS i f
1.97   {True}
1.98   i := (1::nat); f := 1;
1.99   WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
1.100 @@ -122,27 +165,50 @@
1.101  apply arith
1.102  done
1.103
1.104 +lemma factorial2_time: "VARS i f t
1.105 + {t=0}
1.106 + i := (1::nat); t := t+1; f := 1; t := t+1;
1.107 + WHILE i \<le> n INV {f = fac(i - 1) & 1 \<le> i & i \<le> n+1 & t = 2*(i-1)+2}
1.108 + DO f := f*i; t := t+1; i := i+1; t := t+1 OD
1.109 + {f = fac n & t = 2*n+2}"
1.110 +apply vcg_simp
1.111 + apply auto
1.112 +apply(subgoal_tac "i = Suc n")
1.113 + apply simp
1.114 +apply arith
1.115 +done
1.116 +
1.117  (** Square root **)
1.118
1.119  (* the easy way: *)
1.120
1.121  lemma sqrt: "VARS r x
1.122   {True}
1.123 - x := X; r := (0::nat);
1.124 - WHILE (r+1)*(r+1) <= x
1.125 - INV {r*r <= x & x=X}
1.126 + r := (0::nat);
1.127 + WHILE (r+1)*(r+1) <= X
1.128 + INV {r*r \<le> X}
1.129   DO r := r+1 OD
1.130   {r*r <= X & X < (r+1)*(r+1)}"
1.131  apply vcg_simp
1.132  done
1.133
1.134 +lemma sqrt_time: "VARS r t
1.135 + {t=0}
1.136 + r := (0::nat); t := t+1;
1.137 + WHILE (r+1)*(r+1) <= X
1.138 + INV {r*r \<le> X & t = r+1}
1.139 + DO r := r+1; t := t+1 OD
1.140 + {r*r <= X & X < (r+1)*(r+1) & (t-1)*(t-1) \<le> X}"
1.141 +apply vcg_simp
1.142 +done
1.143 +
1.144  (* without multiplication *)
1.145
1.146 -lemma sqrt_without_multiplication: "VARS u w r x
1.147 - {True}
1.148 - x := X; u := 1; w := 1; r := (0::nat);
1.149 - WHILE w <= x
1.150 - INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
1.151 +lemma sqrt_without_multiplication: "VARS u w r
1.152 + {x=X}
1.153 + u := 1; w := 1; r := (0::nat);
1.154 + WHILE w <= X
1.155 + INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= X}
1.156   DO r := r + 1; w := w + u + 2; u := u + 2 OD
1.157   {r*r <= X & X < (r+1)*(r+1)}"
1.158  apply vcg_simp
1.159 @@ -163,6 +229,18 @@
1.160   apply auto
1.161  done
1.162
1.163 +lemma imperative_reverse_time: "VARS y x t
1.164 + {x=X & t=0}
1.165 + y:=[]; t := t+1;
1.166 + WHILE x ~= []
1.167 + INV {rev(x)@y = rev(X) & t = 2*(length y) + 1}
1.168 + DO y := (hd x # y); t := t+1; x := tl x; t := t+1 OD
1.169 + {y=rev(X) & t = 2*length X + 1}"
1.170 +apply vcg_simp
1.172 + apply auto
1.173 +done
1.174 +
1.175  lemma imperative_append: "VARS x y
1.176   {x=X & y=Y}
1.177   x := rev(x);
1.178 @@ -177,6 +255,20 @@
1.179  apply auto
1.180  done
1.181
1.182 +lemma imperative_append_time_no_rev: "VARS x y t
1.183 + {x=X & y=Y}
1.184 + x := rev(x); t := 0;
1.185 + WHILE x~=[]
1.186 + INV {rev(x)@y = X@Y & length x \<le> length X & t = 2 * (length X - length x)}
1.187 + DO y := (hd x # y); t := t+1;
1.188 +    x := tl x; t := t+1
1.189 + OD
1.190 + {y = X@Y & t = 2 * length X}"
1.191 +apply vcg_simp
1.193 +apply auto
1.194 +done
1.195 +
1.196
1.197  (*** ARRAYS ***)
1.198
1.199 @@ -193,6 +285,18 @@
1.200  apply(blast elim!: less_SucE)
1.201  done
1.202
1.203 +lemma zero_search_time: "VARS A i t
1.204 + {t=0}
1.205 + i := 0; t := t+1;
1.206 + WHILE i < length A & A!i ~= key
1.207 + INV {(\<forall>j. j<i --> A!j ~= key) & i \<le> length A & t = i+1}
1.208 + DO i := i+1; t := t+1 OD
1.209 + {(i < length A --> A!i = key) &
1.210 +  (i = length A --> (!j. j < length A --> A!j ~= key)) & t \<le> length A + 1}"
1.211 +apply vcg_simp
1.212 +apply(blast elim!: less_SucE)
1.213 +done
1.214 +
1.215  (*
1.216  The `partition' procedure for quicksort.
1.217  `A' is the array to be sorted (modelled as a list).
```