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