merged
authornipkow
Sat May 21 07:08:59 2016 +0200 (2016-05-21 ago)
changeset 63107932cf444f2fe
parent 63105 c445b0924e3a
parent 63106 412140038d3c
child 63108 02b885591735
child 63114 27afe7af7379
merged
     1.1 --- a/src/HOL/Hoare/Examples.thy	Fri May 20 22:01:42 2016 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Sat May 21 07:08:59 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.25 - apply (simp add:int_distrib)
    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.171 + apply(simp add: neq_Nil_conv)
   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.192 +apply(simp add: neq_Nil_conv)
   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).