src/HOL/Hoare/Examples.thy
author nipkow
Fri, 29 Nov 2002 09:48:28 +0100
changeset 13737 e564c3d2d174
parent 13684 48bfc2cc0938
child 13789 d37f66755f47
permissions -rw-r--r--
added a few lemmas
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
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
    15
lemma multiply_by_add: "VARS m s a b
13682
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
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
    27
lemma Euclid_GCD: "VARS a b
13682
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
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
    52
lemma gcd_scm: "VARS a b x y
13682
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
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
    67
lemma power_by_mult: "VARS a b c
13682
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
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
    86
lemma factorial: "VARS a b
13682
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
13684
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
    97
lemma [simp]: "1 \<le> i \<Longrightarrow> fac (i - Suc 0) * i = fac i"
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
    98
by(induct i, simp_all)
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
    99
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   100
lemma "VARS i f
13684
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   101
 {True}
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   102
 i := (1::nat); f := 1;
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   103
 WHILE i <= n INV {f = fac(i - 1) & 1 <= i & i <= n+1}
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   104
 DO f := f*i; i := i+1 OD
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   105
 {f = fac n}"
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   106
apply vcg_simp
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   107
apply(subgoal_tac "i = Suc n")
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   108
apply simp
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   109
apply arith
48bfc2cc0938 moved fac example
nipkow
parents: 13682
diff changeset
   110
done
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   111
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   112
(** Square root **)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   113
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   114
(* the easy way: *)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   115
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   116
lemma sqrt: "VARS r x
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   117
 {True}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   118
 x := X; r := (0::nat);
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   119
 WHILE (r+1)*(r+1) <= x
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   120
 INV {r*r <= x & x=X}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   121
 DO r := r+1 OD
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   122
 {r*r <= X & X < (r+1)*(r+1)}"
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   123
apply vcg_simp
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   124
apply auto
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   125
done
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   126
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   127
(* without multiplication *)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   128
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   129
lemma sqrt_without_multiplication: "VARS u w r x
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   130
 {True}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   131
 x := X; u := 1; w := 1; r := (0::nat);
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   132
 WHILE w <= x
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   133
 INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   134
 DO r := r + 1; w := w + u + 2; u := u + 2 OD
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   135
 {r*r <= X & X < (r+1)*(r+1)}"
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   136
apply vcg_simp
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   137
apply auto
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   138
done
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   139
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   140
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   141
(*** LISTS ***)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   142
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   143
lemma imperative_reverse: "VARS y x
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   144
 {x=X}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   145
 y:=[];
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   146
 WHILE x ~= []
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   147
 INV {rev(x)@y = rev(X)}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   148
 DO y := (hd x # y); x := tl x OD
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   149
 {y=rev(X)}"
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
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   155
lemma imperative_append: "VARS x y
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   156
 {x=X & y=Y}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   157
 x := rev(x);
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   158
 WHILE x~=[]
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   159
 INV {rev(x)@y = X@Y}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   160
 DO y := (hd x # y);
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   161
    x := tl x
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   162
 OD
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   163
 {y = X@Y}"
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   164
apply vcg_simp
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   165
apply(simp add: neq_Nil_conv)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   166
apply auto
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   167
done
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   168
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   169
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   170
(*** ARRAYS ***)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   171
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   172
(* Search for a key *)
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   173
lemma zero_search: "VARS A i
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   174
 {True}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   175
 i := 0;
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   176
 WHILE i < length A & A!i ~= key
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   177
 INV {!j. j<i --> A!j ~= key}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   178
 DO i := i+1 OD
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   179
 {(i < length A --> A!i = key) &
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   180
  (i = length A --> (!j. j < length A --> A!j ~= key))}"
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   181
apply vcg_simp
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   182
apply(blast elim!: less_SucE)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   183
done
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   184
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   185
(* 
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   186
The `partition' procedure for quicksort.
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   187
`A' is the array to be sorted (modelled as a list).
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   188
Elements of A must be of class order to infer at the end
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   189
that the elements between u and l are equal to pivot.
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   190
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   191
Ambiguity warnings of parser are due to := being used
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   192
both for assignment and list update.
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   193
*)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   194
lemma lem: "m - Suc 0 < n ==> m < Suc n"
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   195
by arith
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   196
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   197
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   198
lemma Partition:
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   199
"[| leq == %A i. !k. k<i --> A!k <= pivot;
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   200
    geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==>
13737
e564c3d2d174 added a few lemmas
nipkow
parents: 13684
diff changeset
   201
 VARS A u l
13682
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   202
 {0 < length(A::('a::order)list)}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   203
 l := 0; u := length A - Suc 0;
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   204
 WHILE l <= u
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   205
  INV {leq A l & geq A u & u<length A & l<=length A}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   206
  DO WHILE l < length A & A!l <= pivot
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   207
     INV {leq A l & geq A u & u<length A & l<=length A}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   208
     DO l := l+1 OD;
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   209
     WHILE 0 < u & pivot <= A!u
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   210
     INV {leq A l & geq A u  & u<length A & l<=length A}
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   211
     DO u := u - 1 OD;
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   212
     IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   213
  OD
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   214
 {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   215
(* expand and delete abbreviations first *)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   216
apply (simp);
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   217
apply (erule thin_rl)+
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   218
apply vcg_simp
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   219
    apply (force simp: neq_Nil_conv)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   220
   apply (blast elim!: less_SucE intro: Suc_leI)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   221
  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   222
 apply (force simp: nth_list_update)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   223
apply (auto intro: order_antisym)
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   224
done
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   225
91674c8a008b conversion ML -> thy
nipkow
parents: 5646
diff changeset
   226
end