src/HOL/Ord.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10231 178a272bceeb
child 10753 e43e017df8c1
permissions -rw-r--r--
hide many names from Datatype_Universe.
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";
6956
18c0457efd3d mono: AddXI/Es;
wenzelm
parents: 6814
diff changeset
    20
AddXIs [monoI];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
    22
Goalw [mono_def] "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
    23
by (Fast_tac 1);
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
qed "monoD";
6956
18c0457efd3d mono: AddXI/Es;
wenzelm
parents: 6814
diff changeset
    25
AddXDs [monoD];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    27
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    28
section "Orders";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    29
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    30
(** Reflexivity **)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    31
6115
c70bce7deb0f Refined arithmetic.
nipkow
parents: 6109
diff changeset
    32
AddIffs [order_refl];
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    33
4600
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    34
(*This form is useful with the classical reasoner*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    35
Goal "!!x::'a::order. x = y ==> x <= y";
4600
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    36
by (etac ssubst 1);
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    37
by (rtac order_refl 1);
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    38
qed "order_eq_refl";
e3e7e901ce6c New theorem order_eq_refl
paulson
parents: 4089
diff changeset
    39
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    40
Goal "~ x < (x::'a::order)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2935
diff changeset
    41
by (simp_tac (simpset() addsimps [order_less_le]) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    42
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
    43
Addsimps [order_less_irrefl];
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    44
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    45
Goal "(x::'a::order) <= y = (x < y | x = y)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2935
diff changeset
    46
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
    47
   (*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
    48
by (blast_tac (claset() addSIs [order_refl]) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    49
qed "order_le_less";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
    50
8214
d612354445b6 new thm order_less_imp_le
paulson
parents: 8024
diff changeset
    51
Goal "!!x::'a::order. x < y ==> x <= y";
d612354445b6 new thm order_less_imp_le
paulson
parents: 8024
diff changeset
    52
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
d612354445b6 new thm order_less_imp_le
paulson
parents: 8024
diff changeset
    53
qed "order_less_imp_le";
d612354445b6 new thm order_less_imp_le
paulson
parents: 8024
diff changeset
    54
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    55
(** Asymmetry **)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    56
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    57
Goal "(x::'a::order) < y ==> ~ (y<x)";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    58
by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    59
qed "order_less_not_sym";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    60
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    61
(* [| n<m;  ~P ==> m<n |] ==> P *)
10231
178a272bceeb renaming of contrapos rules
paulson
parents: 9969
diff changeset
    62
bind_thm ("order_less_asym", order_less_not_sym RS contrapos_np);
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    63
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    64
(* Transitivity *)
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    65
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    66
Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    67
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    68
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    69
qed "order_less_trans";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
    70
6780
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    71
Goal "!!x::'a::order. [| x <= y; y < z |] ==> x < z";
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    72
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    73
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    74
qed "order_le_less_trans";
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    75
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    76
Goal "!!x::'a::order. [| x < y; y <= z |] ==> x < z";
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    77
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    78
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    79
qed "order_less_le_trans";
769cea1985e4 added order_le_less_trans, order_less_le_trans;
wenzelm
parents: 6433
diff changeset
    80
5538
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    81
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    82
(** Useful for simplification, but too risky to include by default. **)
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    83
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    84
Goal "(x::'a::order) < y ==>  (~ y < x) = True";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    85
by (blast_tac (claset() addEs [order_less_asym]) 1);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    86
qed "order_less_imp_not_less";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    87
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    88
Goal "(x::'a::order) < y ==>  (y < x --> P) = True";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    89
by (blast_tac (claset() addEs [order_less_asym]) 1);
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    90
qed "order_less_imp_triv";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    91
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    92
Goal "(x::'a::order) < y ==>  (x = y) = False";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    93
by Auto_tac;
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    94
qed "order_less_imp_not_eq";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    95
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    96
Goal "(x::'a::order) < y ==>  (y = x) = False";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    97
by Auto_tac;
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    98
qed "order_less_imp_not_eq2";
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
    99
c55bf0487abe a few new theorems
paulson
parents: 5449
diff changeset
   100
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
   101
(** min **)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
   102
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5132
diff changeset
   103
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
   104
by (simp_tac (simpset() addsimps prems) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
   105
qed "min_leastL";
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
   106
5316
7a8975451a89 even more tidying of Goal commands
paulson
parents: 5143
diff changeset
   107
val prems = Goalw [min_def]
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
   108
 "(!!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
   109
by (cut_facts_tac prems 1);
998cb95fdd43 Yet more fast_tac->blast_tac, and other tidying
paulson
parents: 2608
diff changeset
   110
by (Asm_simp_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2935
diff changeset
   111
by (blast_tac (claset() addIs [order_antisym]) 1);
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 1465
diff changeset
   112
qed "min_leastR";
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   113
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   114
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   115
section "Linear/Total Orders";
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   116
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   117
Goal "!!x::'a::linorder. x<y | x=y | y<x";
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   118
by (simp_tac (simpset() addsimps [order_less_le]) 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   119
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   120
by (Blast_tac 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   121
qed "linorder_less_linear";
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   122
9969
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9422
diff changeset
   123
val prems = Goal "[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9422
diff changeset
   124
by (cut_facts_tac [linorder_less_linear] 1);
4753185f1dd2 renamed (most of...) the select rules
paulson
parents: 9422
diff changeset
   125
by (REPEAT(eresolve_tac (prems@[disjE]) 1));
8024
199721f2eb2d Added linord_less_split
nipkow
parents: 7617
diff changeset
   126
qed "linorder_less_split";
199721f2eb2d Added linord_less_split
nipkow
parents: 7617
diff changeset
   127
6128
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   128
Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   129
by (simp_tac (simpset() addsimps [order_less_le]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   130
by (cut_facts_tac [linorder_linear] 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   131
by (blast_tac (claset() addIs [order_antisym]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   132
qed "linorder_not_less";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   133
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   134
Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   135
by (simp_tac (simpset() addsimps [order_less_le]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   136
by (cut_facts_tac [linorder_linear] 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   137
by (blast_tac (claset() addIs [order_antisym]) 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   138
qed "linorder_not_le";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   139
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   140
Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   141
by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   142
by Auto_tac;
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   143
qed "linorder_neq_iff";
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   144
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   145
(* eliminates ~= in premises *)
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   146
bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   147
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   148
(** min & max **)
2acc5d36610c More arith refinements.
nipkow
parents: 6115
diff changeset
   149
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   150
Goalw [min_def] "min (x::'a::order) x = x";
6814
d96d4977f94e expandshort
paulson
parents: 6780
diff changeset
   151
by (Simp_tac 1);
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   152
qed "min_same";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   153
Addsimps [min_same];
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   154
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   155
Goalw [max_def] "max (x::'a::order) x = x";
6814
d96d4977f94e expandshort
paulson
parents: 6780
diff changeset
   156
by (Simp_tac 1);
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   157
qed "max_same";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   158
Addsimps [max_same];
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   159
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   160
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
   161
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   162
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   163
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   164
qed "le_max_iff_disj";
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   165
8529
paulson
parents: 8214
diff changeset
   166
Goal "(x::'a::linorder) <= max x y";
paulson
parents: 8214
diff changeset
   167
by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
paulson
parents: 8214
diff changeset
   168
qed "le_maxI1";
paulson
parents: 8214
diff changeset
   169
paulson
parents: 8214
diff changeset
   170
Goal "(y::'a::linorder) <= max x y";
paulson
parents: 8214
diff changeset
   171
by (simp_tac (simpset() addsimps [le_max_iff_disj]) 1);
paulson
parents: 8214
diff changeset
   172
qed "le_maxI2";
7617
e783adccf39e removed order-sorted theorems from the default claset
paulson
parents: 7494
diff changeset
   173
(*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*)
7494
45905028bb1d added theorems le_maxI1 and le_maxI2, also in claset
oheimb
parents: 6956
diff changeset
   174
6073
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   175
Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   176
by (simp_tac (simpset() addsimps [order_le_less]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   177
by (cut_facts_tac [linorder_less_linear] 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   178
by (blast_tac (claset() addIs [order_less_trans]) 1);
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   179
qed "less_max_iff_disj";
fba734ba6894 Refined arith tactic.
nipkow
parents: 5673
diff changeset
   180
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   181
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
   182
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   183
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   184
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   185
qed "max_le_iff_conj";
5673
5dc45f449198 Addsimps [max_le_iff_conj];
nipkow
parents: 5625
diff changeset
   186
Addsimps [max_le_iff_conj];
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   187
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   188
Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   189
by (simp_tac (simpset() addsimps [order_le_less]) 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   190
by (cut_facts_tac [linorder_less_linear] 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   191
by (blast_tac (claset() addIs [order_less_trans]) 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   192
qed "max_less_iff_conj";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   193
Addsimps [max_less_iff_conj];
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   194
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   195
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
   196
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   197
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   198
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   199
qed "le_min_iff_conj";
5673
5dc45f449198 Addsimps [max_le_iff_conj];
nipkow
parents: 5625
diff changeset
   200
Addsimps [le_min_iff_conj];
5dc45f449198 Addsimps [max_le_iff_conj];
nipkow
parents: 5625
diff changeset
   201
(* AddIffs screws up a blast_tac in MiniML *)
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   202
6433
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   203
Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   204
by (simp_tac (simpset() addsimps [order_le_less]) 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   205
by (cut_facts_tac [linorder_less_linear] 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   206
by (blast_tac (claset() addIs [order_less_trans]) 1);
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   207
qed "min_less_iff_conj";
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   208
Addsimps [min_less_iff_conj];
228237ec56e5 Added new thms.
nipkow
parents: 6301
diff changeset
   209
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   210
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
   211
by (Simp_tac 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5069
diff changeset
   212
by (cut_facts_tac [linorder_linear] 1);
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   213
by (blast_tac (claset() addIs [order_trans]) 1);
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 4600
diff changeset
   214
qed "min_le_iff_disj";
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   215
9242
c472ed4edded added a thm.
nipkow
parents: 8529
diff changeset
   216
Goalw [min_def] "!!z::'a::linorder. (min x y < z) = (x < z | y < z)";
c472ed4edded added a thm.
nipkow
parents: 8529
diff changeset
   217
by (simp_tac (simpset() addsimps [order_le_less]) 1);
c472ed4edded added a thm.
nipkow
parents: 8529
diff changeset
   218
by (cut_facts_tac [linorder_less_linear] 1);
c472ed4edded added a thm.
nipkow
parents: 8529
diff changeset
   219
by (blast_tac (claset() addIs [order_less_trans]) 1);
c472ed4edded added a thm.
nipkow
parents: 8529
diff changeset
   220
qed "min_less_iff_disj";
c472ed4edded added a thm.
nipkow
parents: 8529
diff changeset
   221
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   222
Goalw [min_def]
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   223
 "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   224
by (Simp_tac 1);
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   225
qed "split_min";
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   226
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   227
Goalw [max_def]
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   228
 "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
6301
08245f5a436d expandshort
paulson
parents: 6157
diff changeset
   229
by (Simp_tac 1);
6157
29942d3a1818 arith_tac for min/max
nipkow
parents: 6128
diff changeset
   230
qed "split_max";