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