src/HOL/Hoare/Examples.thy
changeset 13682 91674c8a008b
parent 5646 7c2ddbaf8b8c
child 13684 48bfc2cc0938
     1.1 --- a/src/HOL/Hoare/Examples.thy	Sun Oct 27 23:34:02 2002 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Mon Oct 28 14:29:51 2002 +0100
     1.3 @@ -6,4 +6,207 @@
     1.4  Various examples.
     1.5  *)
     1.6  
     1.7 -Examples = Hoare + Arith2
     1.8 +theory Examples = Hoare + Arith2:
     1.9 +
    1.10 +(*** ARITHMETIC ***)
    1.11 +
    1.12 +(** multiplication by successive addition **)
    1.13 +
    1.14 +lemma multiply_by_add: "|- VARS m s a b.
    1.15 +  {a=A & b=B}
    1.16 +  m := 0; s := 0;
    1.17 +  WHILE m~=a
    1.18 +  INV {s=m*b & a=A & b=B}
    1.19 +  DO s := s+b; m := m+(1::nat) OD
    1.20 +  {s = A*B}"
    1.21 +by vcg_simp
    1.22 +
    1.23 +
    1.24 +(** Euclid's algorithm for GCD **)
    1.25 +
    1.26 +lemma Euclid_GCD: "|- VARS a b.
    1.27 + {0<A & 0<B}
    1.28 + a := A; b := B;
    1.29 + WHILE  a~=b
    1.30 + INV {0<a & 0<b & gcd A B = gcd a b}
    1.31 + DO IF a<b THEN b := b-a ELSE a := a-b FI OD
    1.32 + {a = gcd A B}"
    1.33 +apply vcg
    1.34 +(*Now prove the verification conditions*)
    1.35 +  apply auto
    1.36 +  apply(simp add: gcd_diff_r less_imp_le)
    1.37 + apply(simp add: not_less_iff_le gcd_diff_l)
    1.38 +apply(erule gcd_nnn)
    1.39 +done
    1.40 +
    1.41 +(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
    1.42 +(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
    1.43 +   where it is given without the invariant. Instead of defining scm
    1.44 +   explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
    1.45 +   division by mupltiplying with gcd x y.
    1.46 +*)
    1.47 +
    1.48 +lemmas distribs =
    1.49 +  diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
    1.50 +
    1.51 +lemma gcd_scm: "|- VARS a b x y.
    1.52 + {0<A & 0<B & a=A & b=B & x=B & y=A}
    1.53 + WHILE  a ~= b
    1.54 + INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
    1.55 + DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
    1.56 + {a = gcd A B & 2*A*B = a*(x+y)}"
    1.57 +apply vcg
    1.58 +  apply simp
    1.59 + apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
    1.60 + apply arith
    1.61 +apply(simp add: distribs gcd_nnn)
    1.62 +done
    1.63 +
    1.64 +(** Power by iterated squaring and multiplication **)
    1.65 +
    1.66 +lemma power_by_mult: "|- VARS a b c.
    1.67 + {a=A & b=B}
    1.68 + c := (1::nat);
    1.69 + WHILE b ~= 0
    1.70 + INV {A^B = c * a^b}
    1.71 + DO  WHILE b mod 2 = 0
    1.72 +     INV {A^B = c * a^b}
    1.73 +     DO  a := a*a; b := b div 2 OD;
    1.74 +     c := c*a; b := b - 1
    1.75 + OD
    1.76 + {c = A^B}"
    1.77 +apply vcg_simp
    1.78 +apply(case_tac "b")
    1.79 + apply(simp add: mod_less)
    1.80 +apply simp
    1.81 +done
    1.82 +
    1.83 +(** Factorial **)
    1.84 +
    1.85 +lemma factorial: "|- VARS a b.
    1.86 + {a=A}
    1.87 + b := 1;
    1.88 + WHILE a ~= 0
    1.89 + INV {fac A = b * fac a}
    1.90 + DO b := b*a; a := a - 1 OD
    1.91 + {b = fac A}"
    1.92 +apply vcg_simp
    1.93 +apply(clarsimp split: nat_diff_split)
    1.94 +done
    1.95 +
    1.96 +
    1.97 +(** Square root **)
    1.98 +
    1.99 +(* the easy way: *)
   1.100 +
   1.101 +lemma sqrt: "|- VARS r x.
   1.102 + {True}
   1.103 + x := X; r := (0::nat);
   1.104 + WHILE (r+1)*(r+1) <= x
   1.105 + INV {r*r <= x & x=X}
   1.106 + DO r := r+1 OD
   1.107 + {r*r <= X & X < (r+1)*(r+1)}"
   1.108 +apply vcg_simp
   1.109 +apply auto
   1.110 +done
   1.111 +
   1.112 +(* without multiplication *)
   1.113 +
   1.114 +lemma sqrt_without_multiplication: "|- VARS u w r x.
   1.115 + {True}
   1.116 + x := X; u := 1; w := 1; r := (0::nat);
   1.117 + WHILE w <= x
   1.118 + INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
   1.119 + DO r := r + 1; w := w + u + 2; u := u + 2 OD
   1.120 + {r*r <= X & X < (r+1)*(r+1)}"
   1.121 +apply vcg_simp
   1.122 +apply auto
   1.123 +done
   1.124 +
   1.125 +
   1.126 +(*** LISTS ***)
   1.127 +
   1.128 +lemma imperative_reverse: "|- VARS y x.
   1.129 + {x=X}
   1.130 + y:=[];
   1.131 + WHILE x ~= []
   1.132 + INV {rev(x)@y = rev(X)}
   1.133 + DO y := (hd x # y); x := tl x OD
   1.134 + {y=rev(X)}"
   1.135 +apply vcg_simp
   1.136 + apply(simp add: neq_Nil_conv)
   1.137 + apply auto
   1.138 +done
   1.139 +
   1.140 +lemma imperative_append: "|- VARS x y.
   1.141 + {x=X & y=Y}
   1.142 + x := rev(x);
   1.143 + WHILE x~=[]
   1.144 + INV {rev(x)@y = X@Y}
   1.145 + DO y := (hd x # y);
   1.146 +    x := tl x
   1.147 + OD
   1.148 + {y = X@Y}"
   1.149 +apply vcg_simp
   1.150 +apply(simp add: neq_Nil_conv)
   1.151 +apply auto
   1.152 +done
   1.153 +
   1.154 +
   1.155 +(*** ARRAYS ***)
   1.156 +
   1.157 +(* Search for a key *)
   1.158 +lemma zero_search: "|- VARS A i.
   1.159 + {True}
   1.160 + i := 0;
   1.161 + WHILE i < length A & A!i ~= key
   1.162 + INV {!j. j<i --> A!j ~= key}
   1.163 + DO i := i+1 OD
   1.164 + {(i < length A --> A!i = key) &
   1.165 +  (i = length A --> (!j. j < length A --> A!j ~= key))}"
   1.166 +apply vcg_simp
   1.167 +apply(blast elim!: less_SucE)
   1.168 +done
   1.169 +
   1.170 +(* 
   1.171 +The `partition' procedure for quicksort.
   1.172 +`A' is the array to be sorted (modelled as a list).
   1.173 +Elements of A must be of class order to infer at the end
   1.174 +that the elements between u and l are equal to pivot.
   1.175 +
   1.176 +Ambiguity warnings of parser are due to := being used
   1.177 +both for assignment and list update.
   1.178 +*)
   1.179 +lemma lem: "m - Suc 0 < n ==> m < Suc n"
   1.180 +by arith
   1.181 +
   1.182 +
   1.183 +lemma Partition:
   1.184 +"[| leq == %A i. !k. k<i --> A!k <= pivot;
   1.185 +    geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
   1.186 + |- VARS A u l.
   1.187 + {0 < length(A::('a::order)list)}
   1.188 + l := 0; u := length A - Suc 0;
   1.189 + WHILE l <= u
   1.190 +  INV {leq A l & geq A u & u<length A & l<=length A}
   1.191 +  DO WHILE l < length A & A!l <= pivot
   1.192 +     INV {leq A l & geq A u & u<length A & l<=length A}
   1.193 +     DO l := l+1 OD;
   1.194 +     WHILE 0 < u & pivot <= A!u
   1.195 +     INV {leq A l & geq A u  & u<length A & l<=length A}
   1.196 +     DO u := u - 1 OD;
   1.197 +     IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
   1.198 +  OD
   1.199 + {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
   1.200 +(* expand and delete abbreviations first *)
   1.201 +apply (simp);
   1.202 +apply (erule thin_rl)+
   1.203 +apply vcg_simp
   1.204 +    apply (force simp: neq_Nil_conv)
   1.205 +   apply (blast elim!: less_SucE intro: Suc_leI)
   1.206 +  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
   1.207 + apply (force simp: nth_list_update)
   1.208 +apply (auto intro: order_antisym)
   1.209 +done
   1.210 +
   1.211 +end
   1.212 \ No newline at end of file