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@5538
|
51 |
(** Asymmetry **)
|
paulson@5538
|
52 |
|
paulson@5538
|
53 |
Goal "(x::'a::order) < y ==> ~ (y<x)";
|
paulson@5538
|
54 |
by (asm_full_simp_tac (simpset() addsimps [order_less_le, order_antisym]) 1);
|
paulson@5538
|
55 |
qed "order_less_not_sym";
|
paulson@5538
|
56 |
|
paulson@5538
|
57 |
(* [| n<m; ~P ==> m<n |] ==> P *)
|
paulson@5538
|
58 |
bind_thm ("order_less_asym", order_less_not_sym RS swap);
|
paulson@5538
|
59 |
|
nipkow@6073
|
60 |
(* Transitivity *)
|
nipkow@6073
|
61 |
|
nipkow@6073
|
62 |
Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
|
nipkow@6073
|
63 |
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
|
nipkow@6073
|
64 |
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
|
nipkow@6073
|
65 |
qed "order_less_trans";
|
nipkow@6073
|
66 |
|
wenzelm@6780
|
67 |
Goal "!!x::'a::order. [| x <= y; y < z |] ==> x < z";
|
wenzelm@6780
|
68 |
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
|
wenzelm@6780
|
69 |
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
|
wenzelm@6780
|
70 |
qed "order_le_less_trans";
|
wenzelm@6780
|
71 |
|
wenzelm@6780
|
72 |
Goal "!!x::'a::order. [| x < y; y <= z |] ==> x < z";
|
wenzelm@6780
|
73 |
by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
|
wenzelm@6780
|
74 |
by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
|
wenzelm@6780
|
75 |
qed "order_less_le_trans";
|
wenzelm@6780
|
76 |
|
paulson@5538
|
77 |
|
paulson@5538
|
78 |
(** Useful for simplification, but too risky to include by default. **)
|
paulson@5538
|
79 |
|
paulson@5538
|
80 |
Goal "(x::'a::order) < y ==> (~ y < x) = True";
|
paulson@5538
|
81 |
by (blast_tac (claset() addEs [order_less_asym]) 1);
|
paulson@5538
|
82 |
qed "order_less_imp_not_less";
|
paulson@5538
|
83 |
|
paulson@5538
|
84 |
Goal "(x::'a::order) < y ==> (y < x --> P) = True";
|
paulson@5538
|
85 |
by (blast_tac (claset() addEs [order_less_asym]) 1);
|
paulson@5538
|
86 |
qed "order_less_imp_triv";
|
paulson@5538
|
87 |
|
paulson@5538
|
88 |
Goal "(x::'a::order) < y ==> (x = y) = False";
|
paulson@5538
|
89 |
by Auto_tac;
|
paulson@5538
|
90 |
qed "order_less_imp_not_eq";
|
paulson@5538
|
91 |
|
paulson@5538
|
92 |
Goal "(x::'a::order) < y ==> (y = x) = False";
|
paulson@5538
|
93 |
by Auto_tac;
|
paulson@5538
|
94 |
qed "order_less_imp_not_eq2";
|
paulson@5538
|
95 |
|
paulson@5538
|
96 |
|
nipkow@2608
|
97 |
(** min **)
|
nipkow@2608
|
98 |
|
paulson@5143
|
99 |
val prems = Goalw [min_def] "(!!x. least <= x) ==> min least x = least";
|
paulson@5143
|
100 |
by (simp_tac (simpset() addsimps prems) 1);
|
nipkow@2608
|
101 |
qed "min_leastL";
|
nipkow@2608
|
102 |
|
paulson@5316
|
103 |
val prems = Goalw [min_def]
|
nipkow@2608
|
104 |
"(!!x::'a::order. least <= x) ==> min x least = least";
|
paulson@2935
|
105 |
by (cut_facts_tac prems 1);
|
paulson@2935
|
106 |
by (Asm_simp_tac 1);
|
wenzelm@4089
|
107 |
by (blast_tac (claset() addIs [order_antisym]) 1);
|
nipkow@2608
|
108 |
qed "min_leastR";
|
nipkow@4640
|
109 |
|
nipkow@4640
|
110 |
|
nipkow@4640
|
111 |
section "Linear/Total Orders";
|
nipkow@4640
|
112 |
|
wenzelm@5069
|
113 |
Goal "!!x::'a::linorder. x<y | x=y | y<x";
|
nipkow@4640
|
114 |
by (simp_tac (simpset() addsimps [order_less_le]) 1);
|
wenzelm@5132
|
115 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@4640
|
116 |
by (Blast_tac 1);
|
nipkow@4640
|
117 |
qed "linorder_less_linear";
|
nipkow@4640
|
118 |
|
nipkow@8024
|
119 |
val prems = goal thy
|
nipkow@8024
|
120 |
"[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P";
|
nipkow@8024
|
121 |
by(cut_facts_tac [linorder_less_linear] 1);
|
nipkow@8024
|
122 |
by(REPEAT(eresolve_tac (prems@[disjE]) 1));
|
nipkow@8024
|
123 |
qed "linorder_less_split";
|
nipkow@8024
|
124 |
|
nipkow@6128
|
125 |
Goal "!!x::'a::linorder. (~ x < y) = (y <= x)";
|
nipkow@6128
|
126 |
by (simp_tac (simpset() addsimps [order_less_le]) 1);
|
nipkow@6128
|
127 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@6128
|
128 |
by (blast_tac (claset() addIs [order_antisym]) 1);
|
nipkow@6128
|
129 |
qed "linorder_not_less";
|
nipkow@6128
|
130 |
|
nipkow@6128
|
131 |
Goal "!!x::'a::linorder. (~ x <= y) = (y < x)";
|
nipkow@6128
|
132 |
by (simp_tac (simpset() addsimps [order_less_le]) 1);
|
nipkow@6128
|
133 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@6128
|
134 |
by (blast_tac (claset() addIs [order_antisym]) 1);
|
nipkow@6128
|
135 |
qed "linorder_not_le";
|
nipkow@6128
|
136 |
|
nipkow@6128
|
137 |
Goal "!!x::'a::linorder. (x ~= y) = (x<y | y<x)";
|
nipkow@6128
|
138 |
by (cut_inst_tac [("x","x"),("y","y")] linorder_less_linear 1);
|
nipkow@6128
|
139 |
by Auto_tac;
|
nipkow@6128
|
140 |
qed "linorder_neq_iff";
|
nipkow@6128
|
141 |
|
nipkow@6128
|
142 |
(* eliminates ~= in premises *)
|
nipkow@6128
|
143 |
bind_thm("linorder_neqE", linorder_neq_iff RS iffD1 RS disjE);
|
nipkow@6128
|
144 |
|
nipkow@6128
|
145 |
(** min & max **)
|
nipkow@6128
|
146 |
|
nipkow@6433
|
147 |
Goalw [min_def] "min (x::'a::order) x = x";
|
paulson@6814
|
148 |
by (Simp_tac 1);
|
nipkow@6433
|
149 |
qed "min_same";
|
nipkow@6433
|
150 |
Addsimps [min_same];
|
nipkow@6433
|
151 |
|
nipkow@6433
|
152 |
Goalw [max_def] "max (x::'a::order) x = x";
|
paulson@6814
|
153 |
by (Simp_tac 1);
|
nipkow@6433
|
154 |
qed "max_same";
|
nipkow@6433
|
155 |
Addsimps [max_same];
|
nipkow@6433
|
156 |
|
wenzelm@5069
|
157 |
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
|
nipkow@4686
|
158 |
by (Simp_tac 1);
|
wenzelm@5132
|
159 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@4640
|
160 |
by (blast_tac (claset() addIs [order_trans]) 1);
|
nipkow@4640
|
161 |
qed "le_max_iff_disj";
|
nipkow@4640
|
162 |
|
oheimb@7494
|
163 |
qed_goal "le_maxI1" Ord.thy "(x::'a::linorder) <= max x y"
|
oheimb@7494
|
164 |
(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI1) 1]);
|
oheimb@7494
|
165 |
qed_goal "le_maxI2" Ord.thy "(y::'a::linorder) <= max x y"
|
oheimb@7494
|
166 |
(K [rtac (le_max_iff_disj RS iffD2) 1, rtac (order_refl RS disjI2) 1]);
|
paulson@7617
|
167 |
(*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*)
|
oheimb@7494
|
168 |
|
nipkow@6073
|
169 |
Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
|
nipkow@6073
|
170 |
by (simp_tac (simpset() addsimps [order_le_less]) 1);
|
nipkow@6073
|
171 |
by (cut_facts_tac [linorder_less_linear] 1);
|
nipkow@6073
|
172 |
by (blast_tac (claset() addIs [order_less_trans]) 1);
|
nipkow@6073
|
173 |
qed "less_max_iff_disj";
|
nipkow@6073
|
174 |
|
wenzelm@5069
|
175 |
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
|
nipkow@4686
|
176 |
by (Simp_tac 1);
|
wenzelm@5132
|
177 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@4640
|
178 |
by (blast_tac (claset() addIs [order_trans]) 1);
|
nipkow@4640
|
179 |
qed "max_le_iff_conj";
|
nipkow@5673
|
180 |
Addsimps [max_le_iff_conj];
|
nipkow@4640
|
181 |
|
nipkow@6433
|
182 |
Goalw [max_def] "!!z::'a::linorder. (max x y < z) = (x < z & y < z)";
|
nipkow@6433
|
183 |
by (simp_tac (simpset() addsimps [order_le_less]) 1);
|
nipkow@6433
|
184 |
by (cut_facts_tac [linorder_less_linear] 1);
|
nipkow@6433
|
185 |
by (blast_tac (claset() addIs [order_less_trans]) 1);
|
nipkow@6433
|
186 |
qed "max_less_iff_conj";
|
nipkow@6433
|
187 |
Addsimps [max_less_iff_conj];
|
nipkow@6433
|
188 |
|
wenzelm@5069
|
189 |
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
|
nipkow@4686
|
190 |
by (Simp_tac 1);
|
wenzelm@5132
|
191 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@4640
|
192 |
by (blast_tac (claset() addIs [order_trans]) 1);
|
nipkow@4640
|
193 |
qed "le_min_iff_conj";
|
nipkow@5673
|
194 |
Addsimps [le_min_iff_conj];
|
nipkow@5673
|
195 |
(* AddIffs screws up a blast_tac in MiniML *)
|
nipkow@4640
|
196 |
|
nipkow@6433
|
197 |
Goalw [min_def] "!!z::'a::linorder. (z < min x y) = (z < x & z < y)";
|
nipkow@6433
|
198 |
by (simp_tac (simpset() addsimps [order_le_less]) 1);
|
nipkow@6433
|
199 |
by (cut_facts_tac [linorder_less_linear] 1);
|
nipkow@6433
|
200 |
by (blast_tac (claset() addIs [order_less_trans]) 1);
|
nipkow@6433
|
201 |
qed "min_less_iff_conj";
|
nipkow@6433
|
202 |
Addsimps [min_less_iff_conj];
|
nipkow@6433
|
203 |
|
wenzelm@5069
|
204 |
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
|
nipkow@4686
|
205 |
by (Simp_tac 1);
|
wenzelm@5132
|
206 |
by (cut_facts_tac [linorder_linear] 1);
|
nipkow@4640
|
207 |
by (blast_tac (claset() addIs [order_trans]) 1);
|
nipkow@4640
|
208 |
qed "min_le_iff_disj";
|
nipkow@6157
|
209 |
|
nipkow@6157
|
210 |
Goalw [min_def]
|
nipkow@6157
|
211 |
"P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
|
paulson@6301
|
212 |
by (Simp_tac 1);
|
nipkow@6157
|
213 |
qed "split_min";
|
nipkow@6157
|
214 |
|
nipkow@6157
|
215 |
Goalw [max_def]
|
nipkow@6157
|
216 |
"P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
|
paulson@6301
|
217 |
by (Simp_tac 1);
|
nipkow@6157
|
218 |
qed "split_max";
|