src/HOL/Hoare/Examples.thy
 author paulson Wed Jul 13 15:06:20 2005 +0200 (2005-07-13) changeset 16796 140f1e0ea846 parent 16733 236dfafbeb63 child 35316 870dfea4f9c0 permissions -rw-r--r--
generlization of some "nat" theorems
```     1 (*  Title:      HOL/Hoare/Examples.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Norbert Galm
```
```     4     Copyright   1998 TUM
```
```     5
```
```     6 Various examples.
```
```     7 *)
```
```     8
```
```     9 theory Examples imports Hoare Arith2 begin
```
```    10
```
```    11 (*** ARITHMETIC ***)
```
```    12
```
```    13 (** multiplication by successive addition **)
```
```    14
```
```    15 lemma multiply_by_add: "VARS m s a b
```
```    16   {a=A & b=B}
```
```    17   m := 0; s := 0;
```
```    18   WHILE m~=a
```
```    19   INV {s=m*b & a=A & b=B}
```
```    20   DO s := s+b; m := m+(1::nat) OD
```
```    21   {s = A*B}"
```
```    22 by vcg_simp
```
```    23
```
```    24 lemma "VARS M N P :: int
```
```    25  {m=M & n=N}
```
```    26  IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
```
```    27  P := 0;
```
```    28  WHILE 0 < M
```
```    29  INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
```
```    30  DO P := P+N; M := M - 1 OD
```
```    31  {P = m*n}"
```
```    32 apply vcg_simp
```
```    33  apply (simp add:int_distrib)
```
```    34 apply clarsimp
```
```    35 apply(rule conjI)
```
```    36  apply clarsimp
```
```    37 apply clarsimp
```
```    38 done
```
```    39
```
```    40 (** Euclid's algorithm for GCD **)
```
```    41
```
```    42 lemma Euclid_GCD: "VARS a b
```
```    43  {0<A & 0<B}
```
```    44  a := A; b := B;
```
```    45  WHILE  a \<noteq> b
```
```    46  INV {0<a & 0<b & gcd A B = gcd a b}
```
```    47  DO IF a<b THEN b := b-a ELSE a := a-b FI OD
```
```    48  {a = gcd A B}"
```
```    49 apply vcg
```
```    50 (*Now prove the verification conditions*)
```
```    51   apply auto
```
```    52   apply(simp add: gcd_diff_r less_imp_le)
```
```    53  apply(simp add: linorder_not_less gcd_diff_l)
```
```    54 apply(erule gcd_nnn)
```
```    55 done
```
```    56
```
```    57 (** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
```
```    58 (* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
```
```    59    where it is given without the invariant. Instead of defining scm
```
```    60    explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
```
```    61    division by mupltiplying with gcd x y.
```
```    62 *)
```
```    63
```
```    64 lemmas distribs =
```
```    65   diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
```
```    66
```
```    67 lemma gcd_scm: "VARS a b x y
```
```    68  {0<A & 0<B & a=A & b=B & x=B & y=A}
```
```    69  WHILE  a ~= b
```
```    70  INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
```
```    71  DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
```
```    72  {a = gcd A B & 2*A*B = a*(x+y)}"
```
```    73 apply vcg
```
```    74   apply simp
```
```    75  apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
```
```    76 apply(simp add: distribs gcd_nnn)
```
```    77 done
```
```    78
```
```    79 (** Power by iterated squaring and multiplication **)
```
```    80
```
```    81 lemma power_by_mult: "VARS a b c
```
```    82  {a=A & b=B}
```
```    83  c := (1::nat);
```
```    84  WHILE b ~= 0
```
```    85  INV {A^B = c * a^b}
```
```    86  DO  WHILE b mod 2 = 0
```
```    87      INV {A^B = c * a^b}
```
```    88      DO  a := a*a; b := b div 2 OD;
```
```    89      c := c*a; b := b - 1
```
```    90  OD
```
```    91  {c = A^B}"
```
```    92 apply vcg_simp
```
```    93 apply(case_tac "b")
```
```    94  apply(simp add: mod_less)
```
```    95 apply simp
```
```    96 done
```
```    97
```
```    98 (** Factorial **)
```
```    99
```
```   100 lemma factorial: "VARS a b
```
```   101  {a=A}
```
```   102  b := 1;
```
```   103  WHILE a ~= 0
```
```   104  INV {fac A = b * fac a}
```
```   105  DO b := b*a; a := a - 1 OD
```
```   106  {b = fac A}"
```
```   107 apply vcg_simp
```
```   108 apply(clarsimp split: nat_diff_split)
```
```   109 done
```
```   110
```
```   111 lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
```
```   112 by(induct i, simp_all)
```
```   113
```
```   114 lemma "VARS i f
```
```   115  {True}
```
```   116  i := (1::nat); f := 1;
```
```   117  WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
```
```   118  DO f := f*i; i := i+1 OD
```
```   119  {f = fac n}"
```
```   120 apply vcg_simp
```
```   121 apply(subgoal_tac "i = Suc n")
```
```   122 apply simp
```
```   123 apply arith
```
```   124 done
```
```   125
```
```   126 (** Square root **)
```
```   127
```
```   128 (* the easy way: *)
```
```   129
```
```   130 lemma sqrt: "VARS r x
```
```   131  {True}
```
```   132  x := X; r := (0::nat);
```
```   133  WHILE (r+1)*(r+1) <= x
```
```   134  INV {r*r <= x & x=X}
```
```   135  DO r := r+1 OD
```
```   136  {r*r <= X & X < (r+1)*(r+1)}"
```
```   137 apply vcg_simp
```
```   138 done
```
```   139
```
```   140 (* without multiplication *)
```
```   141
```
```   142 lemma sqrt_without_multiplication: "VARS u w r x
```
```   143  {True}
```
```   144  x := X; u := 1; w := 1; r := (0::nat);
```
```   145  WHILE w <= x
```
```   146  INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
```
```   147  DO r := r + 1; w := w + u + 2; u := u + 2 OD
```
```   148  {r*r <= X & X < (r+1)*(r+1)}"
```
```   149 apply vcg_simp
```
```   150 done
```
```   151
```
```   152
```
```   153 (*** LISTS ***)
```
```   154
```
```   155 lemma imperative_reverse: "VARS y x
```
```   156  {x=X}
```
```   157  y:=[];
```
```   158  WHILE x ~= []
```
```   159  INV {rev(x)@y = rev(X)}
```
```   160  DO y := (hd x # y); x := tl x OD
```
```   161  {y=rev(X)}"
```
```   162 apply vcg_simp
```
```   163  apply(simp add: neq_Nil_conv)
```
```   164  apply auto
```
```   165 done
```
```   166
```
```   167 lemma imperative_append: "VARS x y
```
```   168  {x=X & y=Y}
```
```   169  x := rev(x);
```
```   170  WHILE x~=[]
```
```   171  INV {rev(x)@y = X@Y}
```
```   172  DO y := (hd x # y);
```
```   173     x := tl x
```
```   174  OD
```
```   175  {y = X@Y}"
```
```   176 apply vcg_simp
```
```   177 apply(simp add: neq_Nil_conv)
```
```   178 apply auto
```
```   179 done
```
```   180
```
```   181
```
```   182 (*** ARRAYS ***)
```
```   183
```
```   184 (* Search for a key *)
```
```   185 lemma zero_search: "VARS A i
```
```   186  {True}
```
```   187  i := 0;
```
```   188  WHILE i < length A & A!i ~= key
```
```   189  INV {!j. j<i --> A!j ~= key}
```
```   190  DO i := i+1 OD
```
```   191  {(i < length A --> A!i = key) &
```
```   192   (i = length A --> (!j. j < length A --> A!j ~= key))}"
```
```   193 apply vcg_simp
```
```   194 apply(blast elim!: less_SucE)
```
```   195 done
```
```   196
```
```   197 (*
```
```   198 The `partition' procedure for quicksort.
```
```   199 `A' is the array to be sorted (modelled as a list).
```
```   200 Elements of A must be of class order to infer at the end
```
```   201 that the elements between u and l are equal to pivot.
```
```   202
```
```   203 Ambiguity warnings of parser are due to := being used
```
```   204 both for assignment and list update.
```
```   205 *)
```
```   206 lemma lem: "m - Suc 0 < n ==> m < Suc n"
```
```   207 by arith
```
```   208
```
```   209
```
```   210 lemma Partition:
```
```   211 "[| leq == %A i. !k. k<i --> A!k <= pivot;
```
```   212     geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
```
```   213  VARS A u l
```
```   214  {0 < length(A::('a::order)list)}
```
```   215  l := 0; u := length A - Suc 0;
```
```   216  WHILE l <= u
```
```   217   INV {leq A l & geq A u & u<length A & l<=length A}
```
```   218   DO WHILE l < length A & A!l <= pivot
```
```   219      INV {leq A l & geq A u & u<length A & l<=length A}
```
```   220      DO l := l+1 OD;
```
```   221      WHILE 0 < u & pivot <= A!u
```
```   222      INV {leq A l & geq A u  & u<length A & l<=length A}
```
```   223      DO u := u - 1 OD;
```
```   224      IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
```
```   225   OD
```
```   226  {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
```
```   227 (* expand and delete abbreviations first *)
```
```   228 apply (simp);
```
```   229 apply (erule thin_rl)+
```
```   230 apply vcg_simp
```
```   231    apply (force simp: neq_Nil_conv)
```
```   232   apply (blast elim!: less_SucE intro: Suc_leI)
```
```   233  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
```
```   234 apply (force simp: nth_list_update)
```
```   235 done
```
```   236
```
`   237 end`