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