src/HOL/Ord.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10753 e43e017df8c1
permissions -rw-r--r--
improved theory reference in comment
clasohm@1465
     1
(*  Title:      HOL/Ord.ML
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
The type class for ordered types
clasohm@923
     7
*)
clasohm@923
     8
paulson@5449
     9
(*Tell Blast_tac about overloading of < and <= to reduce the risk of
paulson@5449
    10
  its applying a rule for the wrong type*)
paulson@5449
    11
Blast.overloaded ("op <", domain_type); 
paulson@5449
    12
Blast.overloaded ("op <=", domain_type);
paulson@5449
    13
nipkow@2608
    14
(** mono **)
clasohm@923
    15
paulson@5316
    16
val [prem] = Goalw [mono_def]
clasohm@923
    17
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
clasohm@923
    18
by (REPEAT (ares_tac [allI, impI, prem] 1));
clasohm@923
    19
qed "monoI";
wenzelm@6956
    20
AddXIs [monoI];
clasohm@923
    21
paulson@5316
    22
Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
paulson@5316
    23
by (Fast_tac 1);
clasohm@923
    24
qed "monoD";
wenzelm@6956
    25
AddXDs [monoD];
clasohm@923
    26
nipkow@2608
    27
nipkow@2608
    28
section "Orders";
nipkow@2608
    29
paulson@5538
    30
(** Reflexivity **)
paulson@5538
    31
nipkow@6115
    32
AddIffs [order_refl];
nipkow@2608
    33
paulson@4600
    34
(*This form is useful with the classical reasoner*)
wenzelm@5069
    35
Goal "!!x::'a::order. x = y ==> x <= y";
paulson@4600
    36
by (etac ssubst 1);
paulson@4600
    37
by (rtac order_refl 1);
paulson@4600
    38
qed "order_eq_refl";
paulson@4600
    39
wenzelm@5069
    40
Goal "~ x < (x::'a::order)";
wenzelm@4089
    41
by (simp_tac (simpset() addsimps [order_less_le]) 1);
nipkow@2608
    42
qed "order_less_irrefl";
paulson@5449
    43
Addsimps [order_less_irrefl];
nipkow@2608
    44
wenzelm@5069
    45
Goal "(x::'a::order) <= y = (x < y | x = y)";
wenzelm@4089
    46
by (simp_tac (simpset() addsimps [order_less_le]) 1);
paulson@5449
    47
   (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
paulson@5449
    48
by (blast_tac (claset() addSIs [order_refl]) 1);
nipkow@2608
    49
qed "order_le_less";
nipkow@2608
    50
paulson@10753
    51
bind_thm ("order_le_imp_less_or_eq", order_le_less RS iffD1);
paulson@10753
    52
paulson@8214
    53
Goal "!!x::'a::order. x < y ==> x <= y";
paulson@8214
    54
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
paulson@8214
    55
qed "order_less_imp_le";
paulson@8214
    56
paulson@5538
    57
(** Asymmetry **)
paulson@5538
    58
paulson@5538
    59
Goal "(x::'a::order) < y ==> ~ (y<x)";
paulson@5538
    60
by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
paulson@5538
    61
qed "order_less_not_sym";
paulson@5538
    62
paulson@5538
    63
(* [| n<m;  ~P ==> m<n |] ==> P *)
paulson@10231
    64
bind_thm ("order_less_asym", order_less_not_sym RS contrapos_np);
paulson@5538
    65
nipkow@6073
    66
(* Transitivity *)
nipkow@6073
    67
nipkow@6073
    68
Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
nipkow@6073
    69
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
nipkow@6073
    70
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
nipkow@6073
    71
qed "order_less_trans";
nipkow@6073
    72
wenzelm@6780
    73
Goal "!!x::'a::order. [| x <= y; y < z |] ==> x < z";
wenzelm@6780
    74
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
wenzelm@6780
    75
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
wenzelm@6780
    76
qed "order_le_less_trans";
wenzelm@6780
    77
wenzelm@6780
    78
Goal "!!x::'a::order. [| x < y; y <= z |] ==> x < z";
wenzelm@6780
    79
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
wenzelm@6780
    80
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
wenzelm@6780
    81
qed "order_less_le_trans";
wenzelm@6780
    82
paulson@5538
    83
paulson@5538
    84
(** Useful for simplification, but too risky to include by default. **)
paulson@5538
    85
paulson@5538
    86
Goal "(x::'a::order) < y ==>  (~ y < x) = True";
paulson@5538
    87
by (blast_tac (claset() addEs [order_less_asym]) 1);
paulson@5538
    88
qed "order_less_imp_not_less";
paulson@5538
    89
paulson@5538
    90
Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
paulson@5538
    91
by (blast_tac (claset() addEs [order_less_asym]) 1);
paulson@5538
    92
qed "order_less_imp_triv";
paulson@5538
    93
paulson@5538
    94
Goal "(x::'a::order) < y ==>  (x = y) = False";
paulson@5538
    95
by Auto_tac;
paulson@5538
    96
qed "order_less_imp_not_eq";
paulson@5538
    97
paulson@5538
    98
Goal "(x::'a::order) < y ==>  (y = x) = False";
paulson@5538
    99
by Auto_tac;
paulson@5538
   100
qed "order_less_imp_not_eq2";
paulson@5538
   101
paulson@5538
   102
nipkow@2608
   103
(** min **)
nipkow@2608
   104
paulson@5143
   105
val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
paulson@5143
   106
by (simp_tac (simpset() addsimps prems) 1);
nipkow@2608
   107
qed "min_leastL";
nipkow@2608
   108
paulson@5316
   109
val prems = Goalw [min_def]
nipkow@2608
   110
 "(!!x::'a::order. least <= x) ==> min x least = least";
paulson@2935
   111
by (cut_facts_tac prems 1);
paulson@2935
   112
by (Asm_simp_tac 1);
wenzelm@4089
   113
by (blast_tac (claset() addIs [order_antisym]) 1);
nipkow@2608
   114
qed "min_leastR";
nipkow@4640
   115
nipkow@4640
   116
nipkow@4640
   117
section "Linear/Total Orders";
nipkow@4640
   118
wenzelm@5069
   119
Goal "!!x::'a::linorder. x<y | x=y | y<x";
nipkow@4640
   120
by (simp_tac (simpset() addsimps [order_less_le]) 1);
wenzelm@5132
   121
by (cut_facts_tac [linorder_linear] 1);
nipkow@4640
   122
by (Blast_tac 1);
nipkow@4640
   123
qed "linorder_less_linear";
nipkow@4640
   124
paulson@9969
   125
val prems = Goal "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
paulson@9969
   126
by (cut_facts_tac [linorder_less_linear] 1);
paulson@9969
   127
by (REPEAT(eresolve_tac (prems@[disjE]) 1));
nipkow@8024
   128
qed "linorder_less_split";
nipkow@8024
   129
nipkow@6128
   130
Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
nipkow@6128
   131
by (simp_tac (simpset() addsimps [order_less_le]) 1);
nipkow@6128
   132
by (cut_facts_tac [linorder_linear] 1);
nipkow@6128
   133
by (blast_tac (claset() addIs [order_antisym]) 1);
nipkow@6128
   134
qed "linorder_not_less";
nipkow@6128
   135
nipkow@6128
   136
Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
nipkow@6128
   137
by (simp_tac (simpset() addsimps [order_less_le]) 1);
nipkow@6128
   138
by (cut_facts_tac [linorder_linear] 1);
nipkow@6128
   139
by (blast_tac (claset() addIs [order_antisym]) 1);
nipkow@6128
   140
qed "linorder_not_le";
nipkow@6128
   141
nipkow@6128
   142
Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
nipkow@6128
   143
by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
nipkow@6128
   144
by Auto_tac;
nipkow@6128
   145
qed "linorder_neq_iff";
nipkow@6128
   146
nipkow@6128
   147
(* eliminates ~= in premises *)
nipkow@6128
   148
bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
nipkow@6128
   149
nipkow@6128
   150
(** min & max **)
nipkow@6128
   151
nipkow@6433
   152
Goalw [min_def] "min (x::'a::order) x = x";
paulson@6814
   153
by (Simp_tac 1);
nipkow@6433
   154
qed "min_same";
nipkow@6433
   155
Addsimps [min_same];
nipkow@6433
   156
nipkow@6433
   157
Goalw [max_def] "max (x::'a::order) x = x";
paulson@6814
   158
by (Simp_tac 1);
nipkow@6433
   159
qed "max_same";
nipkow@6433
   160
Addsimps [max_same];
nipkow@6433
   161
wenzelm@5069
   162
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
nipkow@4686
   163
by (Simp_tac 1);
wenzelm@5132
   164
by (cut_facts_tac [linorder_linear] 1);
nipkow@4640
   165
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
   166
qed "le_max_iff_disj";
nipkow@4640
   167
paulson@8529
   168
Goal "(x::'a::linorder) <= max x y";
paulson@8529
   169
by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
paulson@8529
   170
qed "le_maxI1";
paulson@8529
   171
paulson@8529
   172
Goal "(y::'a::linorder) <= max x y";
paulson@8529
   173
by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
paulson@8529
   174
qed "le_maxI2";
paulson@7617
   175
(*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*)
oheimb@7494
   176
nipkow@6073
   177
Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
nipkow@6073
   178
by (simp_tac (simpset() addsimps [order_le_less]) 1);
nipkow@6073
   179
by (cut_facts_tac [linorder_less_linear] 1);
nipkow@6073
   180
by (blast_tac (claset() addIs [order_less_trans]) 1);
nipkow@6073
   181
qed "less_max_iff_disj";
nipkow@6073
   182
wenzelm@5069
   183
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
nipkow@4686
   184
by (Simp_tac 1);
wenzelm@5132
   185
by (cut_facts_tac [linorder_linear] 1);
nipkow@4640
   186
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
   187
qed "max_le_iff_conj";
nipkow@5673
   188
Addsimps [max_le_iff_conj];
nipkow@4640
   189
nipkow@6433
   190
Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)";
nipkow@6433
   191
by (simp_tac (simpset() addsimps [order_le_less]) 1);
nipkow@6433
   192
by (cut_facts_tac [linorder_less_linear] 1);
nipkow@6433
   193
by (blast_tac (claset() addIs [order_less_trans]) 1);
nipkow@6433
   194
qed "max_less_iff_conj";
nipkow@6433
   195
Addsimps [max_less_iff_conj];
nipkow@6433
   196
wenzelm@5069
   197
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
nipkow@4686
   198
by (Simp_tac 1);
wenzelm@5132
   199
by (cut_facts_tac [linorder_linear] 1);
nipkow@4640
   200
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
   201
qed "le_min_iff_conj";
nipkow@5673
   202
Addsimps [le_min_iff_conj];
nipkow@5673
   203
(* AddIffs screws up a blast_tac in MiniML *)
nipkow@4640
   204
nipkow@6433
   205
Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)";
nipkow@6433
   206
by (simp_tac (simpset() addsimps [order_le_less]) 1);
nipkow@6433
   207
by (cut_facts_tac [linorder_less_linear] 1);
nipkow@6433
   208
by (blast_tac (claset() addIs [order_less_trans]) 1);
nipkow@6433
   209
qed "min_less_iff_conj";
nipkow@6433
   210
Addsimps [min_less_iff_conj];
nipkow@6433
   211
wenzelm@5069
   212
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
nipkow@4686
   213
by (Simp_tac 1);
wenzelm@5132
   214
by (cut_facts_tac [linorder_linear] 1);
nipkow@4640
   215
by (blast_tac (claset() addIs [order_trans]) 1);
nipkow@4640
   216
qed "min_le_iff_disj";
nipkow@6157
   217
nipkow@9242
   218
Goalw [min_def] "!!z::'a::linorder. (min x y < z) = (x < z | y < z)";
nipkow@9242
   219
by (simp_tac (simpset() addsimps [order_le_less]) 1);
nipkow@9242
   220
by (cut_facts_tac [linorder_less_linear] 1);
nipkow@9242
   221
by (blast_tac (claset() addIs [order_less_trans]) 1);
nipkow@9242
   222
qed "min_less_iff_disj";
nipkow@9242
   223
nipkow@6157
   224
Goalw [min_def]
nipkow@6157
   225
 "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
paulson@6301
   226
by (Simp_tac 1);
nipkow@6157
   227
qed "split_min";
nipkow@6157
   228
nipkow@6157
   229
Goalw [max_def]
nipkow@6157
   230
 "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
paulson@6301
   231
by (Simp_tac 1);
nipkow@6157
   232
qed "split_max";