author | paulson |
Wed, 25 Jul 2001 17:58:26 +0200 | |
changeset 11454 | 7514e5e21cb8 |
parent 11451 | 8abfb4f7bd02 |
child 11653 | 93aaafb6431b |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Ord.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
2624 | 6 |
Type classes for order signatures and orders. |
923 | 7 |
*) |
8 |
||
11140 | 9 |
theory Ord = HOL: |
923 | 10 |
|
5889 | 11 |
|
923 | 12 |
axclass |
11140 | 13 |
ord < "term" |
923 | 14 |
|
3820 | 15 |
syntax |
11140 | 16 |
"op <" :: "['a::ord, 'a] => bool" ("op <") |
17 |
"op <=" :: "['a::ord, 'a] => bool" ("op <=") |
|
3820 | 18 |
|
8882 | 19 |
global |
20 |
||
923 | 21 |
consts |
11140 | 22 |
"op <" :: "['a::ord, 'a] => bool" ("(_/ < _)" [50, 51] 50) |
23 |
"op <=" :: "['a::ord, 'a] => bool" ("(_/ <= _)" [50, 51] 50) |
|
923 | 24 |
|
8882 | 25 |
local |
2608 | 26 |
|
3820 | 27 |
syntax (symbols) |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
28 |
"op <=" :: "['a::ord, 'a] => bool" ("op \\<le>") |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
29 |
"op <=" :: "['a::ord, 'a] => bool" ("(_/ \\<le> _)" [50, 51] 50) |
11140 | 30 |
|
31 |
(*Tell Blast_tac about overloading of < and <= to reduce the risk of |
|
32 |
its applying a rule for the wrong type*) |
|
33 |
ML {* |
|
34 |
Blast.overloaded ("op <" , domain_type); |
|
35 |
Blast.overloaded ("op <=", domain_type); |
|
36 |
*} |
|
37 |
||
38 |
||
39 |
constdefs |
|
40 |
mono :: "['a::ord => 'b::ord] => bool" (*monotonicity*) |
|
41 |
"mono(f) == (!A B. A <= B --> f(A) <= f(B))" |
|
42 |
||
43 |
lemma monoI [intro?]: "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)" |
|
44 |
apply (unfold mono_def) |
|
45 |
apply fast |
|
46 |
done |
|
47 |
||
48 |
lemma monoD [dest?]: "[| mono(f); A <= B |] ==> f(A) <= f(B)" |
|
49 |
apply (unfold mono_def) |
|
50 |
apply fast |
|
51 |
done |
|
52 |
||
53 |
||
54 |
constdefs |
|
55 |
min :: "['a::ord, 'a] => 'a" |
|
56 |
"min a b == (if a <= b then a else b)" |
|
57 |
max :: "['a::ord, 'a] => 'a" |
|
58 |
"max a b == (if a <= b then b else a)" |
|
2259 | 59 |
|
11140 | 60 |
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
61 |
apply (simp add: min_def) |
|
62 |
done |
|
63 |
||
64 |
lemma min_of_mono: |
|
65 |
"!x y. (f x <= f y) = (x <= y) ==> min (f m) (f n) = f (min m n)" |
|
66 |
apply (simp add: min_def) |
|
67 |
done |
|
68 |
||
69 |
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
|
70 |
apply (simp add: max_def) |
|
71 |
done |
|
72 |
||
73 |
lemma max_of_mono: |
|
74 |
"!x y. (f x <= f y) = (x <= y) ==> max (f m) (f n) = f (max m n)" |
|
75 |
apply (simp add: max_def) |
|
76 |
done |
|
3947 | 77 |
|
11367 | 78 |
|
11140 | 79 |
section "Orders" |
80 |
||
2608 | 81 |
axclass order < ord |
11140 | 82 |
order_refl [iff]: "x <= x" |
83 |
order_trans: "[| x <= y; y <= z |] ==> x <= z" |
|
84 |
order_antisym: "[| x <= y; y <= x |] ==> x = y" |
|
85 |
order_less_le: "x < y = (x <= y & x ~= y)" |
|
86 |
||
87 |
(** Reflexivity **) |
|
88 |
||
89 |
(*This form is useful with the classical reasoner*) |
|
90 |
lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y" |
|
91 |
apply (erule ssubst) |
|
92 |
apply (rule order_refl) |
|
93 |
done |
|
94 |
||
95 |
lemma order_less_irrefl [simp]: "~ x < (x::'a::order)" |
|
96 |
apply (simp (no_asm) add: order_less_le) |
|
97 |
done |
|
98 |
||
99 |
lemma order_le_less: "(x::'a::order) <= y = (x < y | x = y)" |
|
100 |
apply (simp (no_asm) add: order_less_le) |
|
101 |
(*NOT suitable for AddIffs, since it can cause PROOF FAILED*) |
|
102 |
apply (blast intro!: order_refl) |
|
103 |
done |
|
104 |
||
105 |
lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] |
|
106 |
||
107 |
lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y" |
|
108 |
apply (simp add: order_less_le) |
|
109 |
done |
|
110 |
||
111 |
(** Asymmetry **) |
|
112 |
||
113 |
lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y<x)" |
|
114 |
apply (simp add: order_less_le order_antisym) |
|
115 |
done |
|
116 |
||
117 |
(* [| n<m; ~P ==> m<n |] ==> P *) |
|
118 |
lemmas order_less_asym = order_less_not_sym [THEN contrapos_np, standard] |
|
119 |
||
120 |
(* Transitivity *) |
|
121 |
||
122 |
lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z" |
|
123 |
apply (simp add: order_less_le) |
|
124 |
apply (blast intro: order_trans order_antisym) |
|
125 |
done |
|
126 |
||
127 |
lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z" |
|
128 |
apply (simp add: order_less_le) |
|
129 |
apply (blast intro: order_trans order_antisym) |
|
130 |
done |
|
131 |
||
132 |
lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z" |
|
133 |
apply (simp add: order_less_le) |
|
134 |
apply (blast intro: order_trans order_antisym) |
|
135 |
done |
|
136 |
||
137 |
||
138 |
(** Useful for simplification, but too risky to include by default. **) |
|
139 |
||
140 |
lemma order_less_imp_not_less: "(x::'a::order) < y ==> (~ y < x) = True" |
|
141 |
apply (blast elim: order_less_asym) |
|
142 |
done |
|
143 |
||
144 |
lemma order_less_imp_triv: "(x::'a::order) < y ==> (y < x --> P) = True" |
|
145 |
apply (blast elim: order_less_asym) |
|
146 |
done |
|
147 |
||
148 |
lemma order_less_imp_not_eq: "(x::'a::order) < y ==> (x = y) = False" |
|
149 |
apply auto |
|
150 |
done |
|
151 |
||
152 |
lemma order_less_imp_not_eq2: "(x::'a::order) < y ==> (y = x) = False" |
|
153 |
apply auto |
|
154 |
done |
|
155 |
||
156 |
(* Other operators *) |
|
157 |
||
158 |
lemma min_leastR: "(!!x::'a::order. least <= x) ==> min x least = least" |
|
159 |
apply (simp (no_asm_simp) add: min_def) |
|
160 |
apply (blast intro: order_antisym) |
|
161 |
done |
|
162 |
||
163 |
lemma max_leastR: "(!!x::'a::order. least <= x) ==> max x least = x" |
|
164 |
apply (simp add: max_def) |
|
165 |
apply (blast intro: order_antisym) |
|
166 |
done |
|
167 |
||
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
168 |
|
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
169 |
(** Least value operator **) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
170 |
|
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
171 |
(*We can no longer use LeastM because the latter requires Hilbert-AC*) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
172 |
constdefs |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
173 |
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
174 |
"Least P == THE x. P x & (ALL y. P y --> x <= y)" |
11140 | 175 |
|
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
176 |
lemma LeastI2: |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
177 |
"[| P (x::'a::order); |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
178 |
!!y. P y ==> x <= y; |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
179 |
!!x. [| P x; \\<forall>y. P y --> x \\<le> y |] ==> Q x |] |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
180 |
==> Q (Least P)"; |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
181 |
apply (unfold Least_def) |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
182 |
apply (rule theI2) |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
183 |
apply (blast intro: order_antisym)+ |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
184 |
done |
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
185 |
|
11140 | 186 |
lemma Least_equality: |
187 |
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"; |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
188 |
apply (simp add: Least_def) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
189 |
apply (rule the_equality) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
190 |
apply (auto intro!: order_antisym) |
11367 | 191 |
done |
192 |
||
11140 | 193 |
section "Linear/Total Orders" |
923 | 194 |
|
4640 | 195 |
axclass linorder < order |
11140 | 196 |
linorder_linear: "x <= y | y <= x" |
197 |
||
198 |
lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x" |
|
199 |
apply (simp (no_asm) add: order_less_le) |
|
200 |
apply (cut_tac linorder_linear) |
|
201 |
apply blast |
|
202 |
done |
|
203 |
||
204 |
lemma linorder_less_split: |
|
205 |
"[| (x::'a::linorder)<y ==> P; x=y ==> P; y<x ==> P |] ==> P" |
|
206 |
apply (cut_tac linorder_less_linear) |
|
207 |
apply blast |
|
208 |
done |
|
209 |
||
210 |
lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)" |
|
211 |
apply (simp (no_asm) add: order_less_le) |
|
212 |
apply (cut_tac linorder_linear) |
|
213 |
apply (blast intro: order_antisym) |
|
214 |
done |
|
215 |
||
216 |
lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)" |
|
217 |
apply (simp (no_asm) add: order_less_le) |
|
218 |
apply (cut_tac linorder_linear) |
|
219 |
apply (blast intro: order_antisym) |
|
220 |
done |
|
221 |
||
222 |
lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)" |
|
223 |
apply (cut_tac x = "x" and y = "y" in linorder_less_linear) |
|
224 |
apply auto |
|
225 |
done |
|
226 |
||
227 |
(* eliminates ~= in premises *) |
|
228 |
lemmas linorder_neqE = linorder_neq_iff [THEN iffD1, THEN disjE, standard] |
|
229 |
||
230 |
section "min & max on (linear) orders" |
|
231 |
||
232 |
lemma min_same [simp]: "min (x::'a::order) x = x" |
|
233 |
apply (simp add: min_def) |
|
234 |
done |
|
235 |
||
236 |
lemma max_same [simp]: "max (x::'a::order) x = x" |
|
237 |
apply (simp add: max_def) |
|
238 |
done |
|
239 |
||
240 |
lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)" |
|
241 |
apply (unfold max_def) |
|
242 |
apply (simp (no_asm)) |
|
243 |
apply (cut_tac linorder_linear) |
|
244 |
apply (blast intro: order_trans) |
|
245 |
done |
|
246 |
||
247 |
lemma le_maxI1: "(x::'a::linorder) <= max x y" |
|
248 |
apply (simp (no_asm) add: le_max_iff_disj) |
|
249 |
done |
|
250 |
||
251 |
lemma le_maxI2: "(y::'a::linorder) <= max x y" |
|
252 |
apply (simp (no_asm) add: le_max_iff_disj) |
|
253 |
done |
|
254 |
(*CANNOT use with AddSIs because blast_tac will give PROOF FAILED.*) |
|
255 |
||
256 |
lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)" |
|
257 |
apply (simp (no_asm) add: max_def order_le_less) |
|
258 |
apply (cut_tac linorder_less_linear) |
|
259 |
apply (blast intro: order_less_trans) |
|
260 |
done |
|
261 |
||
262 |
lemma max_le_iff_conj [simp]: |
|
263 |
"!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)" |
|
264 |
apply (simp (no_asm) add: max_def) |
|
265 |
apply (cut_tac linorder_linear) |
|
266 |
apply (blast intro: order_trans) |
|
267 |
done |
|
268 |
||
269 |
lemma max_less_iff_conj [simp]: |
|
270 |
"!!z::'a::linorder. (max x y < z) = (x < z & y < z)" |
|
271 |
apply (simp (no_asm) add: order_le_less max_def) |
|
272 |
apply (cut_tac linorder_less_linear) |
|
273 |
apply (blast intro: order_less_trans) |
|
274 |
done |
|
275 |
||
276 |
lemma le_min_iff_conj [simp]: |
|
277 |
"!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)" |
|
278 |
apply (simp (no_asm) add: min_def) |
|
279 |
apply (cut_tac linorder_linear) |
|
280 |
apply (blast intro: order_trans) |
|
281 |
done |
|
282 |
(* AddIffs screws up a blast_tac in MiniML *) |
|
283 |
||
284 |
lemma min_less_iff_conj [simp]: |
|
285 |
"!!z::'a::linorder. (z < min x y) = (z < x & z < y)" |
|
286 |
apply (simp (no_asm) add: order_le_less min_def) |
|
287 |
apply (cut_tac linorder_less_linear) |
|
288 |
apply (blast intro: order_less_trans) |
|
289 |
done |
|
290 |
||
291 |
lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)" |
|
292 |
apply (unfold min_def) |
|
293 |
apply (simp (no_asm)) |
|
294 |
apply (cut_tac linorder_linear) |
|
295 |
apply (blast intro: order_trans) |
|
296 |
done |
|
297 |
||
298 |
lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)" |
|
299 |
apply (unfold min_def) |
|
300 |
apply (simp (no_asm) add: order_le_less) |
|
301 |
apply (cut_tac linorder_less_linear) |
|
302 |
apply (blast intro: order_less_trans) |
|
303 |
done |
|
304 |
||
305 |
lemma split_min: |
|
306 |
"P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
|
307 |
apply (simp (no_asm) add: min_def) |
|
308 |
done |
|
309 |
||
310 |
lemma split_max: |
|
311 |
"P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))" |
|
312 |
apply (simp (no_asm) add: max_def) |
|
313 |
done |
|
4640 | 314 |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
315 |
|
11140 | 316 |
section "bounded quantifiers" |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
317 |
|
6402 | 318 |
syntax |
11140 | 319 |
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
320 |
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
|
321 |
"_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
|
322 |
"_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
323 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
324 |
syntax (symbols) |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
325 |
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\\<forall>_<_./ _)" [0, 0, 10] 10) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
326 |
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\\<exists>_<_./ _)" [0, 0, 10] 10) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
327 |
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10) |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
328 |
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10) |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
329 |
|
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
330 |
syntax (HOL) |
11140 | 331 |
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
332 |
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
|
333 |
"_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
|
334 |
"_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
|
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
335 |
|
6402 | 336 |
translations |
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
337 |
"ALL x<y. P" => "ALL x. x < y --> P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
338 |
"EX x<y. P" => "EX x. x < y & P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
339 |
"ALL x<=y. P" => "ALL x. x <= y --> P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
340 |
"EX x<=y. P" => "EX x. x <= y & P" |
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
6855
diff
changeset
|
341 |
|
6402 | 342 |
|
11140 | 343 |
ML |
344 |
{* |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
345 |
val Least_def = thm "Least_def"; |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11367
diff
changeset
|
346 |
val Least_equality = thm "Least_equality"; |
11140 | 347 |
val mono_def = thm "mono_def"; |
348 |
val monoI = thm "monoI"; |
|
349 |
val monoD = thm "monoD"; |
|
350 |
val min_def = thm "min_def"; |
|
351 |
val min_of_mono = thm "min_of_mono"; |
|
352 |
val max_def = thm "max_def"; |
|
353 |
val max_of_mono = thm "max_of_mono"; |
|
354 |
val min_leastL = thm "min_leastL"; |
|
355 |
val max_leastL = thm "max_leastL"; |
|
356 |
val min_leastR = thm "min_leastR"; |
|
357 |
val max_leastR = thm "max_leastR"; |
|
358 |
val order_eq_refl = thm "order_eq_refl"; |
|
359 |
val order_less_irrefl = thm "order_less_irrefl"; |
|
360 |
val order_le_less = thm "order_le_less"; |
|
361 |
val order_le_imp_less_or_eq = thm "order_le_imp_less_or_eq"; |
|
362 |
val order_less_imp_le = thm "order_less_imp_le"; |
|
363 |
val order_less_not_sym = thm "order_less_not_sym"; |
|
364 |
val order_less_asym = thm "order_less_asym"; |
|
365 |
val order_less_trans = thm "order_less_trans"; |
|
366 |
val order_le_less_trans = thm "order_le_less_trans"; |
|
367 |
val order_less_le_trans = thm "order_less_le_trans"; |
|
368 |
val order_less_imp_not_less = thm "order_less_imp_not_less"; |
|
369 |
val order_less_imp_triv = thm "order_less_imp_triv"; |
|
370 |
val order_less_imp_not_eq = thm "order_less_imp_not_eq"; |
|
371 |
val order_less_imp_not_eq2 = thm "order_less_imp_not_eq2"; |
|
372 |
val linorder_less_linear = thm "linorder_less_linear"; |
|
373 |
val linorder_less_split = thm "linorder_less_split"; |
|
374 |
val linorder_not_less = thm "linorder_not_less"; |
|
375 |
val linorder_not_le = thm "linorder_not_le"; |
|
376 |
val linorder_neq_iff = thm "linorder_neq_iff"; |
|
377 |
val linorder_neqE = thm "linorder_neqE"; |
|
378 |
val min_same = thm "min_same"; |
|
379 |
val max_same = thm "max_same"; |
|
380 |
val le_max_iff_disj = thm "le_max_iff_disj"; |
|
381 |
val le_maxI1 = thm "le_maxI1"; |
|
382 |
val le_maxI2 = thm "le_maxI2"; |
|
383 |
val less_max_iff_disj = thm "less_max_iff_disj"; |
|
384 |
val max_le_iff_conj = thm "max_le_iff_conj"; |
|
385 |
val max_less_iff_conj = thm "max_less_iff_conj"; |
|
386 |
val le_min_iff_conj = thm "le_min_iff_conj"; |
|
387 |
val min_less_iff_conj = thm "min_less_iff_conj"; |
|
388 |
val min_le_iff_disj = thm "min_le_iff_disj"; |
|
389 |
val min_less_iff_disj = thm "min_less_iff_disj"; |
|
390 |
val split_min = thm "split_min"; |
|
391 |
val split_max = thm "split_max"; |
|
392 |
val order_refl = thm "order_refl"; |
|
393 |
val order_trans = thm "order_trans"; |
|
394 |
val order_antisym = thm "order_antisym"; |
|
395 |
val order_less_le = thm "order_less_le"; |
|
396 |
val linorder_linear = thm "linorder_linear"; |
|
397 |
*} |
|
398 |
||
923 | 399 |
end |