src/HOL/Hoare/Examples.ML
author nipkow
Tue, 08 Jun 1999 12:53:20 +0200
changeset 6802 655a16e16c01
parent 6162 484adda70b65
child 6816 4267539284be
permissions -rw-r--r--
added square root example.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1335
diff changeset
     1
(*  Title:      HOL/Hoare/Examples.thy
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
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    11
Goal "|- VARS m s. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    12
\  {m=0 & s=0} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    13
\  WHILE m~=a \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    14
\  INV {s=m*b} \  
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    15
\  DO s := s+b; m := m+1 OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    16
\  {s = a*b}";
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
    17
by (hoare_tac (Asm_full_simp_tac) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    18
qed "multiply_by_add";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    19
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    20
(** Euclid's algorithm for GCD **)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    21
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    22
Goal "|- VARS a b. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    23
\ {0<A & 0<B & a=A & b=B} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    24
\ WHILE  a~=b  \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    25
\ INV {0<a & 0<b & gcd A B = gcd a b} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    26
\ DO IF a<b THEN b := b-a ELSE a := a-b FI OD \
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    27
\ {a = gcd A B}";
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    28
by (hoare_tac (K all_tac) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    29
3372
6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents: 2031
diff changeset
    30
(*Now prove the verification conditions*)
5338
9f999cf852e0 Tidied, removing uses of less_imp_diff_positive
paulson
parents: 5183
diff changeset
    31
by Auto_tac;
9f999cf852e0 Tidied, removing uses of less_imp_diff_positive
paulson
parents: 5183
diff changeset
    32
by (etac gcd_nnn 4);
9f999cf852e0 Tidied, removing uses of less_imp_diff_positive
paulson
parents: 5183
diff changeset
    33
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
9f999cf852e0 Tidied, removing uses of less_imp_diff_positive
paulson
parents: 5183
diff changeset
    34
by (force_tac (claset(),
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    35
               simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    36
by (asm_simp_tac (simpset() addsimps [gcd_diff_r,less_imp_le]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    37
qed "Euclid_GCD";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    38
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    39
(** Power by iterated squaring and multiplication **)
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    40
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    41
Goal "|- VARS a b c. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    42
\ {a=A & b=B} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    43
\ c := 1; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    44
\ WHILE b ~= 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    45
\ INV {A^B = c * a^b} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    46
\ DO  WHILE b mod 2 = 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    47
\     INV {A^B = c * a^b} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    48
\     DO  a := a*a; b := b div 2 OD; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    49
\     c := c*a; b := b-1 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    50
\ OD \
4359
6f2986464280 Simplified proofs.
nipkow
parents: 4356
diff changeset
    51
\ {c = A^B}";
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
    52
by (hoare_tac (Asm_full_simp_tac) 1);
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    53
by (exhaust_tac "b" 1);
4356
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4153
diff changeset
    54
by (hyp_subst_tac 1);
0dfd34f0d33d Replaced n ~= 0 by 0 < n
nipkow
parents: 4153
diff changeset
    55
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
4359
6f2986464280 Simplified proofs.
nipkow
parents: 4356
diff changeset
    56
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    57
qed "power_by_mult";
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    58
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    59
(** Factorial **)
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    60
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    61
Goal "|- VARS a b. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    62
\ {a=A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    63
\ b := 1; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    64
\ WHILE a ~= 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    65
\ INV {fac A = b * fac a} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    66
\ DO b := b*a; a := a-1 OD \
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    67
\ {b = fac A}";
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    68
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
    69
by (Clarify_tac 1);
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5069
diff changeset
    70
by (exhaust_tac "a" 1);
1798
c055505f36d1 Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1465
diff changeset
    71
by (ALLGOALS
c055505f36d1 Explicitly included add_mult_distrib & add_mult_distrib2
paulson
parents: 1465
diff changeset
    72
    (asm_simp_tac
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3372
diff changeset
    73
     (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
    74
qed"factorial";
1335
5e1c0540f285 New directory.
nipkow
parents:
diff changeset
    75
6802
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    76
(** Square root **)
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    77
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    78
(* the easy way: *
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    79
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    80
Goal "|- VARS x r. \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    81
\ {u = 1 & w = 1 & r = 0} \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    82
\ WHILE (r+1)*(r+1) <= x \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    83
\ INV {r*r <= x} \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    84
\ DO r := r+1 OD \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    85
\ {r*r <= x & x < (r+1)*(r+1)}";
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    86
by (hoare_tac Asm_full_simp_tac 1);
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    87
by(arith_tac 1);
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    88
qed "sqrt";
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    89
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    90
(* without multiplication *)
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    91
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    92
Goal "|- VARS x u w r. \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    93
\ {u = 1 & w = 1 & r = 0} \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    94
\ WHILE w <= x \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    95
\ INV {u = r+r+1 & w = (r+1)*(r+1) & r*r <= x} \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    96
\ DO r := r+1; w := w+u+2; u := u+2 OD \
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    97
\ {r*r <= x & x < (r+1)*(r+1)}";
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    98
by (hoare_tac Asm_full_simp_tac 1);
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
    99
by(arith_tac 1);
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   100
by(arith_tac 1);
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   101
qed "sqrt_without_multiplication";
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   102
655a16e16c01 added square root example.
nipkow
parents: 6162
diff changeset
   103
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   104
(*** LISTS ***)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   105
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   106
Goal "|- VARS y x. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   107
\ {x=X} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   108
\ y:=[]; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   109
\ WHILE x ~= [] \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   110
\ INV {rev(x)@y = rev(X)} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   111
\ DO y := (hd x # y); x := tl x OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   112
\ {y=rev(X)}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   113
by (hoare_tac Asm_full_simp_tac 1);
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   114
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   115
by Safe_tac;
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   116
by (ALLGOALS(Asm_full_simp_tac ));
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   117
qed "imperative_reverse";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   118
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   119
Goal
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   120
"|- VARS x y. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   121
\ {x=X & y=Y} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   122
\ x := rev(x); \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   123
\ WHILE x~=[] \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   124
\ INV {rev(x)@y = X@Y} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   125
\ DO y := (hd x # y); \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   126
\    x := tl x \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   127
\ OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   128
\ {y = X@Y}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   129
by (hoare_tac Asm_full_simp_tac 1);
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   130
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   131
by Safe_tac;
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   132
by (ALLGOALS(Asm_full_simp_tac));
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   133
qed "imperative_append";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   134
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   135
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   136
(*** ARRAYS ***)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   137
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   138
(* Search for 0 *)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   139
Goal
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   140
"|- VARS A i. \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   141
\ {True} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   142
\ i := 0; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   143
\ WHILE i < length A & A!i ~= 0 \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   144
\ INV {!j. j<i --> A!j ~= 0} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   145
\ DO i := i+1 OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   146
\ {(i < length A --> A!i = 0) & \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   147
\  (i = length A --> (!j. j < length A --> A!j ~= 0))}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   148
by (hoare_tac Asm_full_simp_tac 1);
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   149
by (blast_tac (claset() addSEs [less_SucE]) 1);
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   150
qed "zero_search";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   151
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   152
(* 
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   153
The `partition' procedure for quicksort.
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   154
`A' is the array to be sorted (modelled as a list).
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   155
Elements of A must be of class order to infer at the end
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   156
that the elements between u and l are equal to pivot.
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   157
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   158
Ambiguity warnings of parser are due to := being used
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   159
both for assignment and list update.
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   160
*)
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   161
Goal
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   162
"[| leq == %A i. !k. k<i --> A!k <= pivot; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   163
\   geq == %A i. !k. i<k & k<length A --> pivot <= A!k |] ==> \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   164
\ |- VARS A u l.\
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   165
\ {0 < length(A::('a::order)list)} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   166
\ l := 0; u := length A - 1; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   167
\ WHILE l <= u \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   168
\  INV {leq A l & geq A u & u<length A & l<=length A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   169
\  DO WHILE l < length A & A!l <= pivot \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   170
\      INV {leq A l & geq A u & u<length A & l<=length A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   171
\      DO l := l+1 OD; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   172
\     WHILE 0 < u & pivot <= A!u \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   173
\      INV {leq A l & geq A u  & u<length A & l<=length A} \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   174
\      DO u := u-1 OD; \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   175
\     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
   176
\  OD \
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   177
\ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}";
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   178
(* expand and delete abbreviations first *)
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   179
by (asm_simp_tac HOL_basic_ss 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   180
by (REPEAT(etac thin_rl 1));
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   181
by (hoare_tac Asm_full_simp_tac 1);
6162
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   182
    by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   183
    by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   184
    by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   185
   by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   186
  by (rtac conjI 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   187
   by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   188
   by (dtac (pred_less_imp_le RS le_imp_less_Suc) 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   189
   by (blast_tac (claset() addSEs [less_SucE]) 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   190
  by (rtac less_imp_diff_less 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   191
  by (Blast_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   192
 by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   193
 by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   194
 by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   195
 by (Simp_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   196
by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   197
by (Asm_simp_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   198
by (rtac conjI 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   199
 by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   200
 by (rtac order_antisym 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   201
  by (Asm_simp_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   202
 by (Asm_simp_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   203
by (Clarify_tac 1);
484adda70b65 expandshort
paulson
parents: 5983
diff changeset
   204
by (Asm_simp_tac 1);
5646
7c2ddbaf8b8c New many-sorted version.
nipkow
parents: 5591
diff changeset
   205
qed "Partition";