src/HOL/Hoare/Examples.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10123 9469c039ff57
child 10700 b18f417d0b62
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9393
c97111953a66 corrected header
oheimb
parents: 9147
diff changeset
     1
(*  Title:      HOL/Hoare/Examples.ML
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
     3
    Author:     Norbert Galm & Tobias Nipkow
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
     4
    Copyright   1998 TUM
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     5
*)
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     6
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
     7
(*** ARITHMETIC ***)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
     8
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
     9
(** multiplication by successive addition **)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    10
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    11
Goal "|- VARS m s a b. \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    12
\  {a=A & b=B} \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    13
\  m := 0; s := 0; \
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    14
\  WHILE m~=a \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    15
\  INV {s=m*b & a=A & b=B} \  
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    16
\  DO s := s+b; m := m+1 OD \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    17
\  {s = A*B}"; 
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
    18
by (hoare_tac (Asm_full_simp_tac) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
qed "multiply_by_add";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    20
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    21
(** Euclid's algorithm for GCD **)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    22
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    23
Goal "|- VARS a b. \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    24
\ {0<A & 0<B} \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    25
\ a := A; b := B; \
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    26
\ WHILE  a~=b  \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    27
\ INV {0<a & 0<b & gcd A B = gcd a b} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    28
\ DO IF a<b THEN b := b-a ELSE a := a-b FI OD \
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
\ {a = gcd A B}";
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    30
by (hoare_tac (K all_tac) 1);
3372
6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents: 2031
diff changeset
    31
(*Now prove the verification conditions*)
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    32
by   Auto_tac;
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    33
by    (etac gcd_nnn 4);
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    34
by   (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    35
by  (force_tac (claset(),
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    36
               simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    37
by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    38
qed "Euclid_GCD";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    39
10123
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    40
(** Dijkstra's extension of Euclid's algorithm for simultaneous GCD and SCM **)
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    41
(* From E.W. Disjkstra. Selected Writings on Computing, p 98 (EWD474),
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    42
   where it is given without the invariant. Instead of defining scm
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    43
   explicitly we have used the theorem scm x y = x*y/gcd x y and avoided
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    44
   division by mupltiplying with gcd x y.
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    45
*)
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    46
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    47
val distribs =
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    48
  [diff_mult_distrib,diff_mult_distrib2,add_mult_distrib,add_mult_distrib2];
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    49
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    50
Goal "|- VARS a b x y. \
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    51
\ {0<A & 0<B & a=A & b=B & x=B & y=A} \
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    52
\ WHILE  a ~= b  \
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    53
\ INV {0<a & 0<b & gcd A B = gcd a b & #2*A*B = a*x + b*y} \
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    54
\ DO IF a<b THEN (b := b-a; x := x+y) ELSE (a := a-b; y := y+x) FI OD \
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    55
\ {a = gcd A B & #2*A*B = a*(x+y)}";
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    56
by (hoare_tac (K all_tac) 1);
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    57
by(Asm_simp_tac 1);
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    58
by(asm_simp_tac (simpset() addsimps
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    59
    (distribs @ [gcd_diff_r,not_less_iff_le, gcd_diff_l])) 1);
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    60
by(arith_tac 1);
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    61
by(asm_full_simp_tac (simpset() addsimps (distribs @ [gcd_nnn])) 1);
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    62
qed "gcd_scm";
9469c039ff57 *** empty log message ***
nipkow
parents: 9393
diff changeset
    63
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    64
(** Power by iterated squaring and multiplication **)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    65
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    66
Goal "|- VARS a b c. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    67
\ {a=A & b=B} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    68
\ c := 1; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    69
\ WHILE b ~= 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    70
\ INV {A^B = c * a^b} \
8791
50b650d19641 changed 2 to #2
paulson
parents: 8442
diff changeset
    71
\ DO  WHILE b mod #2 = 0 \
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    72
\     INV {A^B = c * a^b} \
8791
50b650d19641 changed 2 to #2
paulson
parents: 8442
diff changeset
    73
\     DO  a := a*a; b := b div #2 OD; \
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    74
\     c := c*a; b := b-1 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    75
\ OD \
4359
6f2986464280 Simplified proofs.
nipkow
parents: 4356
diff changeset
    76
\ {c = A^B}";
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
    77
by (hoare_tac (Asm_full_simp_tac) 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    78
by (case_tac "b" 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    79
by  (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
8791
50b650d19641 changed 2 to #2
paulson
parents: 8442
diff changeset
    80
by (Asm_simp_tac 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    81
qed "power_by_mult";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    82
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    83
(** Factorial **)
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    84
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    85
Goal "|- VARS a b. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    86
\ {a=A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    87
\ b := 1; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    88
\ WHILE a ~= 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    89
\ INV {fac A = b * fac a} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    90
\ DO b := b*a; a := a-1 OD \
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    91
\ {b = fac A}";
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    92
by (hoare_tac Asm_full_simp_tac 1);
5655
afd75136b236 Mods because of: Installed trans_tac in solver of simpset().
nipkow
parents: 5646
diff changeset
    93
by (Clarify_tac 1);
8442
96023903c2df case_tac now subsumes both boolean and datatype cases;
wenzelm
parents: 8423
diff changeset
    94
by (case_tac "a" 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    95
by  (ALLGOALS (asm_simp_tac
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3372
diff changeset
    96
     (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
    97
qed "factorial";
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    98
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    99
(** Square root **)
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   100
6816
4267539284be unclosed comment.
nipkow
parents: 6802
diff changeset
   101
(* the easy way: *)
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   102
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   103
Goal "|- VARS r x. \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   104
\ {True} \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   105
\ x := X; r := 0; \
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   106
\ WHILE (r+1)*(r+1) <= x \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   107
\ INV {r*r <= x & x=X} \
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   108
\ DO r := r+1 OD \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   109
\ {r*r <= X & X < (r+1)*(r+1)}";
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   110
by (hoare_tac (SELECT_GOAL Auto_tac) 1);
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   111
qed "sqrt";
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   112
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   113
(* without multiplication *)
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   114
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   115
Goal "|- VARS u w r x. \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   116
\ {True} \
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   117
\ x := X; u := 1; w := 1; r := 0; \
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   118
\ WHILE w <= x \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   119
\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x & x=X} \
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   120
\ DO r := r+1; w := w+u+2; u := u+2 OD \
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   121
\ {r*r <= X & X < (r+1)*(r+1)}";
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   122
by (hoare_tac (SELECT_GOAL Auto_tac) 1);
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   123
qed "sqrt_without_multiplication";
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   124
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   125
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   126
(*** LISTS ***)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   127
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   128
Goal "|- VARS y x. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   129
\ {x=X} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   130
\ y:=[]; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   131
\ WHILE x ~= [] \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   132
\ INV {rev(x)@y = rev(X)} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   133
\ DO y := (hd x # y); x := tl x OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   134
\ {y=rev(X)}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   135
by (hoare_tac Asm_full_simp_tac 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   136
by  (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   137
by  Auto_tac;
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   138
qed "imperative_reverse";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   139
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   140
Goal
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   141
"|- VARS x y. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   142
\ {x=X & y=Y} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   143
\ x := rev(x); \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   144
\ WHILE x~=[] \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   145
\ INV {rev(x)@y = X@Y} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   146
\ DO y := (hd x # y); \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   147
\    x := tl x \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   148
\ OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   149
\ {y = X@Y}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   150
by (hoare_tac Asm_full_simp_tac 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   151
by  (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   152
by  Auto_tac;
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   153
qed "imperative_append";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   154
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   155
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   156
(*** ARRAYS ***)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   157
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   158
(* Search for 0 *)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   159
Goal
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   160
"|- VARS A i. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   161
\ {True} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   162
\ i := 0; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   163
\ WHILE i < length A & A!i ~= 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   164
\ INV {!j. j<i --> A!j ~= 0} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   165
\ DO i := i+1 OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   166
\ {(i < length A --> A!i = 0) & \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   167
\  (i = length A --> (!j. j < length A --> A!j ~= 0))}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   168
by (hoare_tac Asm_full_simp_tac 1);
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   169
by (blast_tac (claset() addSEs [less_SucE]) 1);
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   170
qed "zero_search";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   171
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   172
(* 
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   173
The `partition' procedure for quicksort.
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   174
`A' is the array to be sorted (modelled as a list).
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   175
Elements of A must be of class order to infer at the end
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   176
that the elements between u and l are equal to pivot.
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   177
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   178
Ambiguity warnings of parser are due to := being used
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   179
both for assignment and list update.
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   180
*)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   181
Goal
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   182
"[| leq == %A i. !k. k<i --> A!k <= pivot; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   183
\   geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   184
\ |- VARS A u l.\
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   185
\ {0 < length(A::('a::order)list)} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   186
\ l := 0; u := length A - 1; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   187
\ WHILE l <= u \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   188
\  INV {leq A l & geq A u & u<length A & l<=length A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   189
\  DO WHILE l < length A & A!l <= pivot \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   190
\      INV {leq A l & geq A u & u<length A & l<=length A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   191
\      DO l := l+1 OD; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   192
\     WHILE 0 < u & pivot <= A!u \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   193
\      INV {leq A l & geq A u  & u<length A & l<=length A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   194
\      DO u := u-1 OD; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   195
\     IF l <= u THEN A := A[l := A!u, u := A!l] ELSE SKIP FI \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   196
\  OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   197
\ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   198
(* expand and delete abbreviations first *)
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   199
by (asm_simp_tac HOL_basic_ss 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   200
by (REPEAT (etac thin_rl 1));
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   201
by (hoare_tac Asm_full_simp_tac 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   202
    by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])) 1);
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   203
   by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
9147
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   204
  by (blast_tac (claset() addSEs [less_SucE] addIs [less_imp_diff_less]
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   205
                          addDs [pred_less_imp_le RS le_imp_less_Suc] ) 1);
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   206
 by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [nth_list_update])) 1);
9a64807da023 corrected specifications and simplified proofs
oheimb
parents: 8791
diff changeset
   207
by (SELECT_GOAL (auto_tac (claset() addIs [order_antisym], simpset())) 1);
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   208
qed "Partition";