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.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.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.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.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.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
```