src/HOL/Ord.ML
author nipkow
Wed, 27 Jan 1999 17:11:39 +0100
changeset 6157 29942d3a1818
parent 6128 2acc5d36610c
child 6301 08245f5a436d
permissions -rw-r--r--
arith_tac for min/max
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 923
diff changeset
     1
(*  Title:      HOL/Ord.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 923
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
The type class for ordered types
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
5449
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
     9
(*Tell Blast_tac about overloading of < and <= to reduce the risk of
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    10
  its applying a rule for the wrong type*)
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    11
Blast.overloaded ("op <", domain_type); 
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    12
Blast.overloaded ("op <=", domain_type);
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    13
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    14
(** mono **)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
    16
val [prem] = Goalw [mono_def]
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
by (REPEAT (ares_tac [allI, impI, prem] 1));
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
qed "monoI";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
    21
Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
    22
by (Fast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
qed "monoD";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    25
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    26
section "Orders";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    27
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    28
(** Reflexivity **)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    29
6115
c70bce7deb0f Refined arithmetic.
nipkow
parents: 6109
diff changeset
    30
AddIffs [order_refl];
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    31
4600
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    32
(*This form is useful with the classical reasoner*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    33
Goal "!!x::'a::order. x = y ==> x <= y";
4600
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    34
by (etac ssubst 1);
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    35
by (rtac order_refl 1);
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    36
qed "order_eq_refl";
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    37
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    38
Goal "~ x < (x::'a::order)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2935
diff changeset
    39
by (simp_tac (simpset() addsimps [order_less_le]) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    40
qed "order_less_irrefl";
5449
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    41
Addsimps [order_less_irrefl];
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    42
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    43
Goal "(x::'a::order) <= y = (x < y | x = y)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2935
diff changeset
    44
by (simp_tac (simpset() addsimps [order_less_le]) 1);
5449
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    45
   (*NOT suitable for AddIffs, since it can cause PROOF FAILED*)
d853d1ac85a3 Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
paulson
parents: 5316
diff changeset
    46
by (blast_tac (claset() addSIs [order_refl]) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    47
qed "order_le_less";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    48
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    49
(** Asymmetry **)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    50
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    51
Goal "(x::'a::order) < y ==> ~ (y<x)";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    52
by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    53
qed "order_less_not_sym";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    54
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    55
(* [| n<m;  ~P ==> m<n |] ==> P *)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    56
bind_thm ("order_less_asym", order_less_not_sym RS swap);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    57
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    58
(* Transitivity *)
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    59
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    60
Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    61
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    62
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    63
qed "order_less_trans";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    64
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    65
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    66
(** Useful for simplification, but too risky to include by default. **)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    67
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    68
Goal "(x::'a::order) < y ==>  (~ y < x) = True";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    69
by (blast_tac (claset() addEs [order_less_asym]) 1);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    70
qed "order_less_imp_not_less";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    71
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    72
Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    73
by (blast_tac (claset() addEs [order_less_asym]) 1);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    74
qed "order_less_imp_triv";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    75
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    76
Goal "(x::'a::order) < y ==>  (x = y) = False";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    77
by Auto_tac;
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    78
qed "order_less_imp_not_eq";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    79
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    80
Goal "(x::'a::order) < y ==>  (y = x) = False";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    81
by Auto_tac;
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    82
qed "order_less_imp_not_eq2";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    83
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    84
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    85
(** min **)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    86
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
    87
val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
    88
by (simp_tac (simpset() addsimps prems) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    89
qed "min_leastL";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    90
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
    91
val prems = Goalw [min_def]
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    92
 "(!!x::'a::order. least <= x) ==> min x least = least";
2935
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2608
diff changeset
    93
by (cut_facts_tac prems 1);
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2608
diff changeset
    94
by (Asm_simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2935
diff changeset
    95
by (blast_tac (claset() addIs [order_antisym]) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    96
qed "min_leastR";
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
    97
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
    98
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
    99
section "Linear/Total Orders";
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   100
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   101
Goal "!!x::'a::linorder. x<y | x=y | y<x";
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   102
by (simp_tac (simpset() addsimps [order_less_le]) 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   103
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   104
by (Blast_tac 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   105
qed "linorder_less_linear";
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   106
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   107
Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   108
by (simp_tac (simpset() addsimps [order_less_le]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   109
by (cut_facts_tac [linorder_linear] 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   110
by (blast_tac (claset() addIs [order_antisym]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   111
qed "linorder_not_less";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   112
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   113
Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   114
by (simp_tac (simpset() addsimps [order_less_le]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   115
by (cut_facts_tac [linorder_linear] 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   116
by (blast_tac (claset() addIs [order_antisym]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   117
qed "linorder_not_le";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   118
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   119
Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   120
by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   121
by Auto_tac;
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   122
qed "linorder_neq_iff";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   123
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   124
(* eliminates ~= in premises *)
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   125
bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   126
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   127
(** min & max **)
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   128
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   129
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4640
diff changeset
   130
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   131
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   132
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   133
qed "le_max_iff_disj";
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   134
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   135
Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   136
by (simp_tac (simpset() addsimps [order_le_less]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   137
by (cut_facts_tac [linorder_less_linear] 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   138
by (blast_tac (claset() addIs [order_less_trans]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   139
qed "less_max_iff_disj";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   140
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   141
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4640
diff changeset
   142
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   143
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   144
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   145
qed "max_le_iff_conj";
5673
5dc45f449198 Addsimps [max_le_iff_conj];
nipkow
parents: 5625
diff changeset
   146
Addsimps [max_le_iff_conj];
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   147
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   148
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4640
diff changeset
   149
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   150
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   151
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   152
qed "le_min_iff_conj";
5673
5dc45f449198 Addsimps [max_le_iff_conj];
nipkow
parents: 5625
diff changeset
   153
Addsimps [le_min_iff_conj];
5dc45f449198 Addsimps [max_le_iff_conj];
nipkow
parents: 5625
diff changeset
   154
(* AddIffs screws up a blast_tac in MiniML *)
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   155
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   156
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4640
diff changeset
   157
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   158
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   159
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   160
qed "min_le_iff_disj";
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   161
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   162
Goalw [min_def]
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   163
 "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   164
by(Simp_tac 1);
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   165
qed "split_min";
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   166
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   167
Goalw [max_def]
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   168
 "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   169
by(Simp_tac 1);
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   170
qed "split_max";