src/HOL/Hoare/Examples.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63106 412140038d3c
child 67410 64d928bacddd
permissions -rw-r--r--
executable domain membership checks
clasohm@1476
     1
(*  Title:      HOL/Hoare/Examples.thy
clasohm@1476
     2
    Author:     Norbert Galm
nipkow@5646
     3
    Copyright   1998 TUM
nipkow@1335
     4
nipkow@5646
     5
Various examples.
nipkow@1335
     6
*)
nipkow@1335
     7
haftmann@35316
     8
theory Examples imports Hoare_Logic Arith2 begin
nipkow@13682
     9
nipkow@13682
    10
(*** ARITHMETIC ***)
nipkow@13682
    11
nipkow@13682
    12
(** multiplication by successive addition **)
nipkow@13682
    13
nipkow@13737
    14
lemma multiply_by_add: "VARS m s a b
nipkow@13682
    15
  {a=A & b=B}
nipkow@13682
    16
  m := 0; s := 0;
nipkow@13682
    17
  WHILE m~=a
nipkow@13682
    18
  INV {s=m*b & a=A & b=B}
nipkow@13682
    19
  DO s := s+b; m := m+(1::nat) OD
nipkow@13682
    20
  {s = A*B}"
nipkow@13682
    21
by vcg_simp
nipkow@13682
    22
nipkow@63106
    23
lemma multiply_by_add_time: "VARS m s a b t
nipkow@63106
    24
  {a=A & b=B & t=0}
nipkow@63106
    25
  m := 0; t := t+1; s := 0; t := t+1;
nipkow@63106
    26
  WHILE m~=a
nipkow@63106
    27
  INV {s=m*b & a=A & b=B & t = 2*m + 2}
nipkow@63106
    28
  DO s := s+b; t := t+1; m := m+(1::nat); t := t+1 OD
nipkow@63106
    29
  {s = A*B \<and> t = 2*A + 2}"
nipkow@63106
    30
by vcg_simp
nipkow@63106
    31
nipkow@63106
    32
lemma multiply_by_add2: "VARS M N P :: int
nipkow@13789
    33
 {m=M & n=N}
nipkow@13789
    34
 IF M < 0 THEN M := -M; N := -N ELSE SKIP FI;
nipkow@13789
    35
 P := 0;
nipkow@13789
    36
 WHILE 0 < M
nipkow@13789
    37
 INV {0 <= M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N)}
nipkow@13789
    38
 DO P := P+N; M := M - 1 OD
nipkow@13789
    39
 {P = m*n}"
nipkow@13789
    40
apply vcg_simp
nipkow@63106
    41
 apply (auto simp add:int_distrib)
nipkow@63106
    42
done
nipkow@63106
    43
nipkow@63106
    44
lemma multiply_by_add2_time: "VARS M N P t :: int
nipkow@63106
    45
 {m=M & n=N & t=0}
nipkow@63106
    46
 IF M < 0 THEN M := -M; t := t+1; N := -N; t := t+1 ELSE SKIP FI;
nipkow@63106
    47
 P := 0; t := t+1;
nipkow@63106
    48
 WHILE 0 < M
nipkow@63106
    49
 INV {0 \<le> M & (EX p. p = (if m<0 then -m else m) & p*N = m*n & P = (p-M)*N & t \<ge> 0 & t \<le> 2*(p-M)+3)}
nipkow@63106
    50
 DO P := P+N; t := t+1; M := M - 1; t := t+1 OD
nipkow@63106
    51
 {P = m*n & t \<le> 2*abs m + 3}"
nipkow@63106
    52
apply vcg_simp
nipkow@63106
    53
 apply (auto simp add:int_distrib)
nipkow@13789
    54
done
nipkow@13682
    55
nipkow@13682
    56
(** Euclid's algorithm for GCD **)
nipkow@13682
    57
nipkow@13737
    58
lemma Euclid_GCD: "VARS a b
nipkow@13682
    59
 {0<A & 0<B}
nipkow@13682
    60
 a := A; b := B;
nipkow@13857
    61
 WHILE  a \<noteq> b
nipkow@13682
    62
 INV {0<a & 0<b & gcd A B = gcd a b}
nipkow@13682
    63
 DO IF a<b THEN b := b-a ELSE a := a-b FI OD
nipkow@13682
    64
 {a = gcd A B}"
nipkow@13682
    65
apply vcg
nipkow@13682
    66
(*Now prove the verification conditions*)
nipkow@13682
    67
  apply auto
nipkow@13682
    68
  apply(simp add: gcd_diff_r less_imp_le)
paulson@16796
    69
 apply(simp add: linorder_not_less gcd_diff_l)
nipkow@13682
    70
apply(erule gcd_nnn)
nipkow@13682
    71
done
nipkow@13682
    72
nipkow@63106
    73
lemma Euclid_GCD_time: "VARS a b t
nipkow@63106
    74
 {0<A & 0<B & t=0}
nipkow@63106
    75
 a := A; t := t+1; b := B; t := t+1; 
nipkow@63106
    76
 WHILE  a \<noteq> b
nipkow@63106
    77
 INV {0<a & 0<b & gcd A B = gcd a b & a\<le>A & b\<le>B & t \<le> max A B - max a b + 2}
nipkow@63106
    78
 DO IF a<b THEN b := b-a; t := t+1 ELSE a := a-b; t := t+1 FI OD
nipkow@63106
    79
 {a = gcd A B & t \<le> max A B + 2}"
nipkow@63106
    80
apply vcg
nipkow@63106
    81
(*Now prove the verification conditions*)
nipkow@63106
    82
  apply auto
nipkow@63106
    83
  apply(simp add: gcd_diff_r less_imp_le)
nipkow@63106
    84
 apply(simp add: linorder_not_less gcd_diff_l)
nipkow@63106
    85
apply(erule gcd_nnn)
nipkow@63106
    86
done
nipkow@63106
    87
nipkow@13682
    88
(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
nipkow@13682
    89
(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
nipkow@13682
    90
   where it is given without the invariant. Instead of defining scm
nipkow@13682
    91
   explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
nipkow@13682
    92
   division by mupltiplying with gcd x y.
nipkow@13682
    93
*)
nipkow@13682
    94
nipkow@13682
    95
lemmas distribs =
nipkow@13682
    96
  diff_mult_distrib diff_mult_distrib2 add_mult_distrib add_mult_distrib2
nipkow@13682
    97
nipkow@13737
    98
lemma gcd_scm: "VARS a b x y
nipkow@13682
    99
 {0<A & 0<B & a=A & b=B & x=B & y=A}
nipkow@13682
   100
 WHILE  a ~= b
nipkow@13682
   101
 INV {0<a & 0<b & gcd A B = gcd a b & 2*A*B = a*x + b*y}
nipkow@13682
   102
 DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD
nipkow@13682
   103
 {a = gcd A B & 2*A*B = a*(x+y)}"
nipkow@13682
   104
apply vcg
nipkow@13682
   105
  apply simp
paulson@16796
   106
 apply(simp add: distribs gcd_diff_r linorder_not_less gcd_diff_l)
nipkow@13682
   107
apply(simp add: distribs gcd_nnn)
nipkow@13682
   108
done
nipkow@13682
   109
nipkow@13682
   110
(** Power by iterated squaring and multiplication **)
nipkow@13682
   111
nipkow@13737
   112
lemma power_by_mult: "VARS a b c
nipkow@13682
   113
 {a=A & b=B}
nipkow@13682
   114
 c := (1::nat);
nipkow@13682
   115
 WHILE b ~= 0
nipkow@13682
   116
 INV {A^B = c * a^b}
nipkow@13682
   117
 DO  WHILE b mod 2 = 0
nipkow@13682
   118
     INV {A^B = c * a^b}
nipkow@13682
   119
     DO  a := a*a; b := b div 2 OD;
nipkow@13682
   120
     c := c*a; b := b - 1
nipkow@13682
   121
 OD
nipkow@13682
   122
 {c = A^B}"
nipkow@13682
   123
apply vcg_simp
nipkow@13682
   124
apply(case_tac "b")
wenzelm@42154
   125
 apply simp
nipkow@13682
   126
apply simp
nipkow@13682
   127
done
nipkow@13682
   128
nipkow@13682
   129
(** Factorial **)
nipkow@13682
   130
nipkow@13737
   131
lemma factorial: "VARS a b
nipkow@13682
   132
 {a=A}
nipkow@13682
   133
 b := 1;
nipkow@63106
   134
 WHILE a > 0
nipkow@13682
   135
 INV {fac A = b * fac a}
nipkow@13682
   136
 DO b := b*a; a := a - 1 OD
nipkow@13682
   137
 {b = fac A}"
nipkow@13682
   138
apply vcg_simp
nipkow@13682
   139
apply(clarsimp split: nat_diff_split)
nipkow@13682
   140
done
nipkow@13682
   141
nipkow@63106
   142
lemma factorial_time: "VARS a b t
nipkow@63106
   143
 {a=A & t=0}
nipkow@63106
   144
 b := 1; t := t+1;
nipkow@63106
   145
 WHILE a > 0
nipkow@63106
   146
 INV {fac A = b * fac a & a \<le> A & t = 2*(A-a)+1}
nipkow@63106
   147
 DO b := b*a; t := t+1; a := a - 1; t := t+1 OD
nipkow@63106
   148
 {b = fac A & t = 2*A + 1}"
nipkow@63106
   149
apply vcg_simp
nipkow@63106
   150
apply(clarsimp split: nat_diff_split)
nipkow@63106
   151
done
nipkow@63106
   152
nipkow@13684
   153
lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
nipkow@13684
   154
by(induct i, simp_all)
nipkow@13684
   155
nipkow@63106
   156
lemma factorial2: "VARS i f
nipkow@13684
   157
 {True}
nipkow@13684
   158
 i := (1::nat); f := 1;
nipkow@13684
   159
 WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
nipkow@13684
   160
 DO f := f*i; i := i+1 OD
nipkow@13684
   161
 {f = fac n}"
nipkow@13684
   162
apply vcg_simp
nipkow@13684
   163
apply(subgoal_tac "i = Suc n")
nipkow@13684
   164
apply simp
nipkow@13684
   165
apply arith
nipkow@13684
   166
done
nipkow@13682
   167
nipkow@63106
   168
lemma factorial2_time: "VARS i f t
nipkow@63106
   169
 {t=0}
nipkow@63106
   170
 i := (1::nat); t := t+1; f := 1; t := t+1;
nipkow@63106
   171
 WHILE i \<le> n INV {f = fac(i - 1) & 1 \<le> i & i \<le> n+1 & t = 2*(i-1)+2}
nipkow@63106
   172
 DO f := f*i; t := t+1; i := i+1; t := t+1 OD
nipkow@63106
   173
 {f = fac n & t = 2*n+2}"
nipkow@63106
   174
apply vcg_simp
nipkow@63106
   175
 apply auto
nipkow@63106
   176
apply(subgoal_tac "i = Suc n")
nipkow@63106
   177
 apply simp
nipkow@63106
   178
apply arith
nipkow@63106
   179
done
nipkow@63106
   180
nipkow@13682
   181
(** Square root **)
nipkow@13682
   182
nipkow@13682
   183
(* the easy way: *)
nipkow@13682
   184
nipkow@13737
   185
lemma sqrt: "VARS r x
nipkow@13682
   186
 {True}
nipkow@63106
   187
 r := (0::nat);
nipkow@63106
   188
 WHILE (r+1)*(r+1) <= X
nipkow@63106
   189
 INV {r*r \<le> X}
nipkow@13682
   190
 DO r := r+1 OD
nipkow@13682
   191
 {r*r <= X & X < (r+1)*(r+1)}"
nipkow@13682
   192
apply vcg_simp
nipkow@13682
   193
done
nipkow@13682
   194
nipkow@63106
   195
lemma sqrt_time: "VARS r t
nipkow@63106
   196
 {t=0}
nipkow@63106
   197
 r := (0::nat); t := t+1;
nipkow@63106
   198
 WHILE (r+1)*(r+1) <= X
nipkow@63106
   199
 INV {r*r \<le> X & t = r+1}
nipkow@63106
   200
 DO r := r+1; t := t+1 OD
nipkow@63106
   201
 {r*r <= X & X < (r+1)*(r+1) & (t-1)*(t-1) \<le> X}"
nipkow@63106
   202
apply vcg_simp
nipkow@63106
   203
done
nipkow@63106
   204
nipkow@13682
   205
(* without multiplication *)
nipkow@13682
   206
nipkow@63106
   207
lemma sqrt_without_multiplication: "VARS u w r
nipkow@63106
   208
 {x=X}
nipkow@63106
   209
 u := 1; w := 1; r := (0::nat);
nipkow@63106
   210
 WHILE w <= X
nipkow@63106
   211
 INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= X}
nipkow@13682
   212
 DO r := r + 1; w := w + u + 2; u := u + 2 OD
nipkow@13682
   213
 {r*r <= X & X < (r+1)*(r+1)}"
nipkow@13682
   214
apply vcg_simp
nipkow@13682
   215
done
nipkow@13682
   216
nipkow@13682
   217
nipkow@13682
   218
(*** LISTS ***)
nipkow@13682
   219
nipkow@13737
   220
lemma imperative_reverse: "VARS y x
nipkow@13682
   221
 {x=X}
nipkow@13682
   222
 y:=[];
nipkow@13682
   223
 WHILE x ~= []
nipkow@13682
   224
 INV {rev(x)@y = rev(X)}
nipkow@13682
   225
 DO y := (hd x # y); x := tl x OD
nipkow@13682
   226
 {y=rev(X)}"
nipkow@13682
   227
apply vcg_simp
nipkow@13682
   228
 apply(simp add: neq_Nil_conv)
nipkow@13682
   229
 apply auto
nipkow@13682
   230
done
nipkow@13682
   231
nipkow@63106
   232
lemma imperative_reverse_time: "VARS y x t
nipkow@63106
   233
 {x=X & t=0}
nipkow@63106
   234
 y:=[]; t := t+1;
nipkow@63106
   235
 WHILE x ~= []
nipkow@63106
   236
 INV {rev(x)@y = rev(X) & t = 2*(length y) + 1}
nipkow@63106
   237
 DO y := (hd x # y); t := t+1; x := tl x; t := t+1 OD
nipkow@63106
   238
 {y=rev(X) & t = 2*length X + 1}"
nipkow@63106
   239
apply vcg_simp
nipkow@63106
   240
 apply(simp add: neq_Nil_conv)
nipkow@63106
   241
 apply auto
nipkow@63106
   242
done
nipkow@63106
   243
nipkow@13737
   244
lemma imperative_append: "VARS x y
nipkow@13682
   245
 {x=X & y=Y}
nipkow@13682
   246
 x := rev(x);
nipkow@13682
   247
 WHILE x~=[]
nipkow@13682
   248
 INV {rev(x)@y = X@Y}
nipkow@13682
   249
 DO y := (hd x # y);
nipkow@13682
   250
    x := tl x
nipkow@13682
   251
 OD
nipkow@13682
   252
 {y = X@Y}"
nipkow@13682
   253
apply vcg_simp
nipkow@13682
   254
apply(simp add: neq_Nil_conv)
nipkow@13682
   255
apply auto
nipkow@13682
   256
done
nipkow@13682
   257
nipkow@63106
   258
lemma imperative_append_time_no_rev: "VARS x y t
nipkow@63106
   259
 {x=X & y=Y}
nipkow@63106
   260
 x := rev(x); t := 0;
nipkow@63106
   261
 WHILE x~=[]
nipkow@63106
   262
 INV {rev(x)@y = X@Y & length x \<le> length X & t = 2 * (length X - length x)}
nipkow@63106
   263
 DO y := (hd x # y); t := t+1;
nipkow@63106
   264
    x := tl x; t := t+1
nipkow@63106
   265
 OD
nipkow@63106
   266
 {y = X@Y & t = 2 * length X}"
nipkow@63106
   267
apply vcg_simp
nipkow@63106
   268
apply(simp add: neq_Nil_conv)
nipkow@63106
   269
apply auto
nipkow@63106
   270
done
nipkow@63106
   271
nipkow@13682
   272
nipkow@13682
   273
(*** ARRAYS ***)
nipkow@13682
   274
nipkow@13682
   275
(* Search for a key *)
nipkow@13737
   276
lemma zero_search: "VARS A i
nipkow@13682
   277
 {True}
nipkow@13682
   278
 i := 0;
nipkow@13682
   279
 WHILE i < length A & A!i ~= key
nipkow@13682
   280
 INV {!j. j<i --> A!j ~= key}
nipkow@13682
   281
 DO i := i+1 OD
nipkow@13682
   282
 {(i < length A --> A!i = key) &
nipkow@13682
   283
  (i = length A --> (!j. j < length A --> A!j ~= key))}"
nipkow@13682
   284
apply vcg_simp
nipkow@13682
   285
apply(blast elim!: less_SucE)
nipkow@13682
   286
done
nipkow@13682
   287
nipkow@63106
   288
lemma zero_search_time: "VARS A i t
nipkow@63106
   289
 {t=0}
nipkow@63106
   290
 i := 0; t := t+1;
nipkow@63106
   291
 WHILE i < length A & A!i ~= key
nipkow@63106
   292
 INV {(\<forall>j. j<i --> A!j ~= key) & i \<le> length A & t = i+1}
nipkow@63106
   293
 DO i := i+1; t := t+1 OD
nipkow@63106
   294
 {(i < length A --> A!i = key) &
nipkow@63106
   295
  (i = length A --> (!j. j < length A --> A!j ~= key)) & t \<le> length A + 1}"
nipkow@63106
   296
apply vcg_simp
nipkow@63106
   297
apply(blast elim!: less_SucE)
nipkow@63106
   298
done
nipkow@63106
   299
nipkow@13682
   300
(* 
nipkow@13682
   301
The `partition' procedure for quicksort.
nipkow@13682
   302
`A' is the array to be sorted (modelled as a list).
nipkow@13682
   303
Elements of A must be of class order to infer at the end
nipkow@13682
   304
that the elements between u and l are equal to pivot.
nipkow@13682
   305
nipkow@13682
   306
Ambiguity warnings of parser are due to := being used
nipkow@13682
   307
both for assignment and list update.
nipkow@13682
   308
*)
nipkow@13682
   309
lemma lem: "m - Suc 0 < n ==> m < Suc n"
nipkow@13682
   310
by arith
nipkow@13682
   311
nipkow@13682
   312
nipkow@13682
   313
lemma Partition:
nipkow@13682
   314
"[| leq == %A i. !k. k<i --> A!k <= pivot;
nipkow@13682
   315
    geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
nipkow@13737
   316
 VARS A u l
nipkow@13682
   317
 {0 < length(A::('a::order)list)}
nipkow@13682
   318
 l := 0; u := length A - Suc 0;
nipkow@13682
   319
 WHILE l <= u
nipkow@13682
   320
  INV {leq A l & geq A u & u<length A & l<=length A}
nipkow@13682
   321
  DO WHILE l < length A & A!l <= pivot
nipkow@13682
   322
     INV {leq A l & geq A u & u<length A & l<=length A}
nipkow@13682
   323
     DO l := l+1 OD;
nipkow@13682
   324
     WHILE 0 < u & pivot <= A!u
nipkow@13682
   325
     INV {leq A l & geq A u  & u<length A & l<=length A}
nipkow@13682
   326
     DO u := u - 1 OD;
nipkow@13682
   327
     IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
nipkow@13682
   328
  OD
nipkow@13682
   329
 {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
nipkow@13682
   330
(* expand and delete abbreviations first *)
wenzelm@58860
   331
apply (simp)
nipkow@13682
   332
apply (erule thin_rl)+
nipkow@13682
   333
apply vcg_simp
nipkow@16733
   334
   apply (force simp: neq_Nil_conv)
nipkow@16733
   335
  apply (blast elim!: less_SucE intro: Suc_leI)
nipkow@16733
   336
 apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
nipkow@16733
   337
apply (force simp: nth_list_update)
nipkow@13682
   338
done
nipkow@13682
   339
nipkow@62390
   340
end