author | wenzelm |
Tue, 07 Nov 2006 11:46:46 +0100 | |
changeset 21204 | 1e96553668c6 |
parent 21194 | 7e48158e50f6 |
child 21216 | 1c8580913738 |
permissions | -rw-r--r-- |
15524 | 1 |
(* Title: HOL/Orderings.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson |
|
4 |
*) |
|
5 |
||
21083 | 6 |
header {* Abstract orderings *} |
15524 | 7 |
|
8 |
theory Orderings |
|
21044
9690be52ee5d
fixed print translations for bounded quantification
haftmann
parents:
20714
diff
changeset
|
9 |
imports Code_Generator Lattice_Locales |
15524 | 10 |
begin |
11 |
||
21083 | 12 |
section {* Abstract orderings *} |
13 |
||
14 |
subsection {* Order signatures *} |
|
15524 | 15 |
|
21194 | 16 |
class ord = |
20588 | 17 |
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
21204 | 18 |
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
19 |
begin |
|
20 |
||
21 |
notation |
|
22 |
less_eq ("op \<^loc><=") |
|
23 |
less_eq ("(_/ \<^loc><= _)" [50, 51] 50) |
|
24 |
less ("op \<^loc><") |
|
25 |
less ("(_/ \<^loc>< _)" [50, 51] 50) |
|
26 |
||
27 |
notation (xsymbols) |
|
28 |
less_eq ("op \<^loc>\<le>") |
|
29 |
less_eq ("(_/ \<^loc>\<le> _)" [50, 51] 50) |
|
15524 | 30 |
|
21204 | 31 |
notation (HTML output) |
32 |
less_eq ("op \<^loc>\<le>") |
|
33 |
less_eq ("(_/ \<^loc>\<le> _)" [50, 51] 50) |
|
34 |
||
35 |
abbreviation (input) |
|
36 |
greater (infix "\<^loc>>" 50) |
|
37 |
"x \<^loc>> y \<equiv> y \<^loc>< x" |
|
38 |
greater_eq (infix "\<^loc>>=" 50) |
|
39 |
"x \<^loc>>= y \<equiv> y \<^loc><= x" |
|
40 |
||
41 |
notation (xsymbols) |
|
42 |
greater_eq (infixl "\<^loc>\<ge>" 50) |
|
43 |
||
44 |
end |
|
45 |
||
46 |
notation |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
47 |
less_eq ("op <=") |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
48 |
less_eq ("(_/ <= _)" [50, 51] 50) |
21204 | 49 |
less ("op <") |
50 |
less ("(_/ < _)" [50, 51] 50) |
|
51 |
||
52 |
notation (xsymbols) |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
53 |
less_eq ("op \<le>") |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
54 |
less_eq ("(_/ \<le> _)" [50, 51] 50) |
15524 | 55 |
|
21204 | 56 |
notation (HTML output) |
57 |
less_eq ("op \<le>") |
|
58 |
less_eq ("(_/ \<le> _)" [50, 51] 50) |
|
20714 | 59 |
|
19536 | 60 |
abbreviation (input) |
61 |
greater (infixl ">" 50) |
|
20714 | 62 |
"x > y \<equiv> y < x" |
19536 | 63 |
greater_eq (infixl ">=" 50) |
20714 | 64 |
"x >= y \<equiv> y <= x" |
65 |
||
21204 | 66 |
notation (xsymbols) |
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset
|
67 |
greater_eq (infixl "\<ge>" 50) |
15524 | 68 |
|
69 |
||
21083 | 70 |
subsection {* Partial orderings *} |
15524 | 71 |
|
72 |
axclass order < ord |
|
73 |
order_refl [iff]: "x <= x" |
|
74 |
order_trans: "x <= y ==> y <= z ==> x <= z" |
|
75 |
order_antisym: "x <= y ==> y <= x ==> x = y" |
|
76 |
order_less_le: "(x < y) = (x <= y & x ~= y)" |
|
77 |
||
21083 | 78 |
text {* Connection to locale: *} |
15524 | 79 |
|
15837 | 80 |
interpretation order: |
15780 | 81 |
partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"] |
15524 | 82 |
apply(rule partial_order.intro) |
83 |
apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym) |
|
84 |
done |
|
85 |
||
86 |
text {* Reflexivity. *} |
|
87 |
||
88 |
lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y" |
|
89 |
-- {* This form is useful with the classical reasoner. *} |
|
90 |
apply (erule ssubst) |
|
91 |
apply (rule order_refl) |
|
92 |
done |
|
93 |
||
94 |
lemma order_less_irrefl [iff]: "~ x < (x::'a::order)" |
|
95 |
by (simp add: order_less_le) |
|
96 |
||
97 |
lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)" |
|
98 |
-- {* NOT suitable for iff, since it can cause PROOF FAILED. *} |
|
99 |
apply (simp add: order_less_le, blast) |
|
100 |
done |
|
101 |
||
102 |
lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] |
|
103 |
||
104 |
lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y" |
|
105 |
by (simp add: order_less_le) |
|
106 |
||
107 |
text {* Asymmetry. *} |
|
108 |
||
109 |
lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)" |
|
110 |
by (simp add: order_less_le order_antisym) |
|
111 |
||
112 |
lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P" |
|
113 |
apply (drule order_less_not_sym) |
|
114 |
apply (erule contrapos_np, simp) |
|
115 |
done |
|
116 |
||
117 |
lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)" |
|
118 |
by (blast intro: order_antisym) |
|
119 |
||
120 |
lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)" |
|
121 |
by(blast intro:order_antisym) |
|
122 |
||
21083 | 123 |
lemma less_imp_neq: "[| (x::'a::order) < y |] ==> x ~= y" |
124 |
by (erule contrapos_pn, erule subst, rule order_less_irrefl) |
|
125 |
||
15524 | 126 |
text {* Transitivity. *} |
127 |
||
128 |
lemma order_less_trans: "!!x::'a::order. [| x < y; y < z |] ==> x < z" |
|
129 |
apply (simp add: order_less_le) |
|
130 |
apply (blast intro: order_trans order_antisym) |
|
131 |
done |
|
132 |
||
133 |
lemma order_le_less_trans: "!!x::'a::order. [| x <= y; y < z |] ==> x < z" |
|
134 |
apply (simp add: order_less_le) |
|
135 |
apply (blast intro: order_trans order_antisym) |
|
136 |
done |
|
137 |
||
138 |
lemma order_less_le_trans: "!!x::'a::order. [| x < y; y <= z |] ==> x < z" |
|
139 |
apply (simp add: order_less_le) |
|
140 |
apply (blast intro: order_trans order_antisym) |
|
141 |
done |
|
142 |
||
21083 | 143 |
lemma eq_neq_eq_imp_neq: "[| x = a ; a ~= b; b = y |] ==> x ~= y" |
144 |
by (erule subst, erule ssubst, assumption) |
|
15524 | 145 |
|
146 |
text {* Useful for simplification, but too risky to include by default. *} |
|
147 |
||
148 |
lemma order_less_imp_not_less: "(x::'a::order) < y ==> (~ y < x) = True" |
|
149 |
by (blast elim: order_less_asym) |
|
150 |
||
151 |
lemma order_less_imp_triv: "(x::'a::order) < y ==> (y < x --> P) = True" |
|
152 |
by (blast elim: order_less_asym) |
|
153 |
||
154 |
lemma order_less_imp_not_eq: "(x::'a::order) < y ==> (x = y) = False" |
|
155 |
by auto |
|
156 |
||
157 |
lemma order_less_imp_not_eq2: "(x::'a::order) < y ==> (y = x) = False" |
|
158 |
by auto |
|
159 |
||
21083 | 160 |
text {* Transitivity rules for calculational reasoning *} |
15524 | 161 |
|
162 |
lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" |
|
163 |
by (simp add: order_less_le) |
|
164 |
||
165 |
lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b" |
|
166 |
by (simp add: order_less_le) |
|
167 |
||
168 |
lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P" |
|
169 |
by (rule order_less_asym) |
|
170 |
||
171 |
||
21083 | 172 |
subsection {* Total orderings *} |
15524 | 173 |
|
174 |
axclass linorder < order |
|
175 |
linorder_linear: "x <= y | y <= x" |
|
176 |
||
177 |
lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x" |
|
178 |
apply (simp add: order_less_le) |
|
179 |
apply (insert linorder_linear, blast) |
|
180 |
done |
|
181 |
||
182 |
lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y | y<x" |
|
183 |
by (simp add: order_le_less linorder_less_linear) |
|
184 |
||
185 |
lemma linorder_le_cases [case_names le ge]: |
|
186 |
"((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P" |
|
187 |
by (insert linorder_linear, blast) |
|
188 |
||
189 |
lemma linorder_cases [case_names less equal greater]: |
|
190 |
"((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P" |
|
191 |
by (insert linorder_less_linear, blast) |
|
192 |
||
193 |
lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)" |
|
194 |
apply (simp add: order_less_le) |
|
195 |
apply (insert linorder_linear) |
|
196 |
apply (blast intro: order_antisym) |
|
197 |
done |
|
198 |
||
199 |
lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)" |
|
200 |
apply (simp add: order_less_le) |
|
201 |
apply (insert linorder_linear) |
|
202 |
apply (blast intro: order_antisym) |
|
203 |
done |
|
204 |
||
205 |
lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y | y<x)" |
|
206 |
by (cut_tac x = x and y = y in linorder_less_linear, auto) |
|
207 |
||
208 |
lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R" |
|
209 |
by (simp add: linorder_neq_iff, blast) |
|
210 |
||
211 |
lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)" |
|
212 |
by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1]) |
|
213 |
||
214 |
lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)" |
|
215 |
by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1]) |
|
216 |
||
217 |
lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)" |
|
218 |
by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1]) |
|
219 |
||
16796 | 220 |
text{*Replacing the old Nat.leI*} |
221 |
lemma leI: "~ x < y ==> y <= (x::'a::linorder)" |
|
222 |
by (simp only: linorder_not_less) |
|
223 |
||
224 |
lemma leD: "y <= (x::'a::linorder) ==> ~ x < y" |
|
225 |
by (simp only: linorder_not_less) |
|
226 |
||
227 |
(*FIXME inappropriate name (or delete altogether)*) |
|
228 |
lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y" |
|
229 |
by (simp only: linorder_not_le) |
|
230 |
||
21083 | 231 |
|
232 |
subsection {* Reasoning tools setup *} |
|
233 |
||
21091 | 234 |
ML {* |
235 |
local |
|
236 |
||
237 |
fun decomp_gen sort thy (Trueprop $ t) = |
|
238 |
let fun of_sort t = let val T = type_of t in |
|
239 |
(* exclude numeric types: linear arithmetic subsumes transitivity *) |
|
240 |
T <> HOLogic.natT andalso T <> HOLogic.intT andalso |
|
241 |
T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end |
|
242 |
fun dec (Const ("Not", _) $ t) = ( |
|
243 |
case dec t of |
|
244 |
NONE => NONE |
|
245 |
| SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) |
|
246 |
| dec (Const ("op =", _) $ t1 $ t2) = |
|
247 |
if of_sort t1 |
|
248 |
then SOME (t1, "=", t2) |
|
249 |
else NONE |
|
250 |
| dec (Const ("Orderings.less_eq", _) $ t1 $ t2) = |
|
251 |
if of_sort t1 |
|
252 |
then SOME (t1, "<=", t2) |
|
253 |
else NONE |
|
254 |
| dec (Const ("Orderings.less", _) $ t1 $ t2) = |
|
255 |
if of_sort t1 |
|
256 |
then SOME (t1, "<", t2) |
|
257 |
else NONE |
|
258 |
| dec _ = NONE |
|
259 |
in dec t end; |
|
260 |
||
261 |
in |
|
262 |
||
263 |
structure Quasi_Tac = Quasi_Tac_Fun ( |
|
264 |
(* The setting up of Quasi_Tac serves as a demo. Since there is no |
|
265 |
class for quasi orders, the tactics Quasi_Tac.trans_tac and |
|
266 |
Quasi_Tac.quasi_tac are not of much use. *) |
|
267 |
struct |
|
268 |
val le_trans = thm "order_trans"; |
|
269 |
val le_refl = thm "order_refl"; |
|
270 |
val eqD1 = thm "order_eq_refl"; |
|
271 |
val eqD2 = thm "sym" RS thm "order_eq_refl"; |
|
272 |
val less_reflE = thm "order_less_irrefl" RS thm "notE"; |
|
273 |
val less_imp_le = thm "order_less_imp_le"; |
|
274 |
val le_neq_trans = thm "order_le_neq_trans"; |
|
275 |
val neq_le_trans = thm "order_neq_le_trans"; |
|
276 |
val less_imp_neq = thm "less_imp_neq"; |
|
277 |
val decomp_trans = decomp_gen ["Orderings.order"]; |
|
278 |
val decomp_quasi = decomp_gen ["Orderings.order"]; |
|
279 |
||
280 |
end); |
|
281 |
||
282 |
structure Order_Tac = Order_Tac_Fun ( |
|
283 |
struct |
|
284 |
val less_reflE = thm "order_less_irrefl" RS thm "notE"; |
|
285 |
val le_refl = thm "order_refl"; |
|
286 |
val less_imp_le = thm "order_less_imp_le"; |
|
287 |
val not_lessI = thm "linorder_not_less" RS thm "iffD2"; |
|
288 |
val not_leI = thm "linorder_not_le" RS thm "iffD2"; |
|
289 |
val not_lessD = thm "linorder_not_less" RS thm "iffD1"; |
|
290 |
val not_leD = thm "linorder_not_le" RS thm "iffD1"; |
|
291 |
val eqI = thm "order_antisym"; |
|
292 |
val eqD1 = thm "order_eq_refl"; |
|
293 |
val eqD2 = thm "sym" RS thm "order_eq_refl"; |
|
294 |
val less_trans = thm "order_less_trans"; |
|
295 |
val less_le_trans = thm "order_less_le_trans"; |
|
296 |
val le_less_trans = thm "order_le_less_trans"; |
|
297 |
val le_trans = thm "order_trans"; |
|
298 |
val le_neq_trans = thm "order_le_neq_trans"; |
|
299 |
val neq_le_trans = thm "order_neq_le_trans"; |
|
300 |
val less_imp_neq = thm "less_imp_neq"; |
|
301 |
val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; |
|
302 |
val not_sym = thm "not_sym"; |
|
303 |
val decomp_part = decomp_gen ["Orderings.order"]; |
|
304 |
val decomp_lin = decomp_gen ["Orderings.linorder"]; |
|
305 |
||
306 |
end); |
|
307 |
||
308 |
end; |
|
309 |
*} |
|
310 |
||
21083 | 311 |
setup {* |
312 |
let |
|
313 |
||
314 |
val order_antisym_conv = thm "order_antisym_conv" |
|
315 |
val linorder_antisym_conv1 = thm "linorder_antisym_conv1" |
|
316 |
val linorder_antisym_conv2 = thm "linorder_antisym_conv2" |
|
317 |
val linorder_antisym_conv3 = thm "linorder_antisym_conv3" |
|
318 |
||
319 |
fun prp t thm = (#prop (rep_thm thm) = t); |
|
15524 | 320 |
|
21083 | 321 |
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) = |
322 |
let val prems = prems_of_ss ss; |
|
323 |
val less = Const("Orderings.less",T); |
|
324 |
val t = HOLogic.mk_Trueprop(le $ s $ r); |
|
325 |
in case find_first (prp t) prems of |
|
326 |
NONE => |
|
327 |
let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) |
|
328 |
in case find_first (prp t) prems of |
|
329 |
NONE => NONE |
|
330 |
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1)) |
|
331 |
end |
|
332 |
| SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv)) |
|
333 |
end |
|
334 |
handle THM _ => NONE; |
|
15524 | 335 |
|
21083 | 336 |
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) = |
337 |
let val prems = prems_of_ss ss; |
|
338 |
val le = Const("Orderings.less_eq",T); |
|
339 |
val t = HOLogic.mk_Trueprop(le $ r $ s); |
|
340 |
in case find_first (prp t) prems of |
|
341 |
NONE => |
|
342 |
let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r)) |
|
343 |
in case find_first (prp t) prems of |
|
344 |
NONE => NONE |
|
345 |
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3)) |
|
346 |
end |
|
347 |
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2)) |
|
348 |
end |
|
349 |
handle THM _ => NONE; |
|
15524 | 350 |
|
21083 | 351 |
val antisym_le = Simplifier.simproc (the_context()) |
352 |
"antisym le" ["(x::'a::order) <= y"] prove_antisym_le; |
|
353 |
val antisym_less = Simplifier.simproc (the_context()) |
|
354 |
"antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less; |
|
355 |
||
356 |
in |
|
21091 | 357 |
(fn thy => (Simplifier.change_simpset_of thy |
358 |
(fn ss => ss |
|
359 |
addsimprocs [antisym_le, antisym_less] |
|
360 |
addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac)) |
|
361 |
addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac))) |
|
362 |
(* Adding the transitivity reasoners also as safe solvers showed a slight |
|
363 |
speed up, but the reasoning strength appears to be not higher (at least |
|
364 |
no breaking of additional proofs in the entire HOL distribution, as |
|
365 |
of 5 March 2004, was observed). *); thy)) |
|
21083 | 366 |
end |
367 |
*} |
|
15524 | 368 |
|
369 |
||
21083 | 370 |
subsection {* Bounded quantifiers *} |
371 |
||
372 |
syntax |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
373 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
374 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
375 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
376 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
21083 | 377 |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
378 |
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
379 |
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
380 |
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
381 |
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) |
21083 | 382 |
|
383 |
syntax (xsymbols) |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
384 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
385 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
386 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
387 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
21083 | 388 |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
389 |
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
390 |
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
391 |
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
392 |
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) |
21083 | 393 |
|
394 |
syntax (HOL) |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
395 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
396 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
397 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
398 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
21083 | 399 |
|
400 |
syntax (HTML output) |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
401 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
402 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
403 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
404 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
21083 | 405 |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
406 |
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
407 |
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
408 |
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
409 |
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) |
21083 | 410 |
|
411 |
translations |
|
412 |
"ALL x<y. P" => "ALL x. x < y \<longrightarrow> P" |
|
413 |
"EX x<y. P" => "EX x. x < y \<and> P" |
|
414 |
"ALL x<=y. P" => "ALL x. x <= y \<longrightarrow> P" |
|
415 |
"EX x<=y. P" => "EX x. x <= y \<and> P" |
|
416 |
"ALL x>y. P" => "ALL x. x > y \<longrightarrow> P" |
|
417 |
"EX x>y. P" => "EX x. x > y \<and> P" |
|
418 |
"ALL x>=y. P" => "ALL x. x >= y \<longrightarrow> P" |
|
419 |
"EX x>=y. P" => "EX x. x >= y \<and> P" |
|
420 |
||
421 |
print_translation {* |
|
422 |
let |
|
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
423 |
val syntax_name = Sign.const_syntax_name (the_context ()); |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
424 |
val impl = syntax_name "op -->"; |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
425 |
val conj = syntax_name "op &"; |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
426 |
val less = syntax_name "Orderings.less"; |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
427 |
val less_eq = syntax_name "Orderings.less_eq"; |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
428 |
|
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
429 |
val trans = |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
430 |
[(("ALL ", impl, less), ("_All_less", "_All_greater")), |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
431 |
(("ALL ", impl, less_eq), ("_All_less_eq", "_All_greater_eq")), |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
432 |
(("EX ", conj, less), ("_Ex_less", "_Ex_greater")), |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
433 |
(("EX ", conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
434 |
|
21083 | 435 |
fun mk v v' c n P = |
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
436 |
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n) |
21083 | 437 |
then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match; |
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
438 |
|
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
439 |
fun tr' q = (q, |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
440 |
fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] => |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
441 |
(case AList.lookup (op =) trans (q, c, d) of |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
442 |
NONE => raise Match |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
443 |
| SOME (l, g) => |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
444 |
(case (t, u) of |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
445 |
(Const ("_bound", _) $ Free (v', _), n) => mk v v' l n P |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
446 |
| (n, Const ("_bound", _) $ Free (v', _)) => mk v v' g n P |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
447 |
| _ => raise Match)) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
448 |
| _ => raise Match); |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
449 |
in [tr' "ALL ", tr' "EX "] end |
21083 | 450 |
*} |
451 |
||
452 |
||
453 |
subsection {* Transitivity reasoning on decreasing inequalities *} |
|
454 |
||
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
455 |
(* FIXME cleanup *) |
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset
|
456 |
|
21083 | 457 |
text {* These support proving chains of decreasing inequalities |
458 |
a >= b >= c ... in Isar proofs. *} |
|
459 |
||
460 |
lemma xt1: |
|
461 |
"a = b ==> b > c ==> a > c" |
|
462 |
"a > b ==> b = c ==> a > c" |
|
463 |
"a = b ==> b >= c ==> a >= c" |
|
464 |
"a >= b ==> b = c ==> a >= c" |
|
465 |
"(x::'a::order) >= y ==> y >= x ==> x = y" |
|
466 |
"(x::'a::order) >= y ==> y >= z ==> x >= z" |
|
467 |
"(x::'a::order) > y ==> y >= z ==> x > z" |
|
468 |
"(x::'a::order) >= y ==> y > z ==> x > z" |
|
469 |
"(a::'a::order) > b ==> b > a ==> ?P" |
|
470 |
"(x::'a::order) > y ==> y > z ==> x > z" |
|
471 |
"(a::'a::order) >= b ==> a ~= b ==> a > b" |
|
472 |
"(a::'a::order) ~= b ==> a >= b ==> a > b" |
|
473 |
"a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" |
|
474 |
"a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" |
|
475 |
"a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" |
|
476 |
"a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" |
|
477 |
by auto |
|
478 |
||
479 |
lemma xt2: |
|
480 |
"(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" |
|
481 |
by (subgoal_tac "f b >= f c", force, force) |
|
482 |
||
483 |
lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> |
|
484 |
(!!x y. x >= y ==> f x >= f y) ==> f a >= c" |
|
485 |
by (subgoal_tac "f a >= f b", force, force) |
|
486 |
||
487 |
lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> |
|
488 |
(!!x y. x >= y ==> f x >= f y) ==> a > f c" |
|
489 |
by (subgoal_tac "f b >= f c", force, force) |
|
490 |
||
491 |
lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==> |
|
492 |
(!!x y. x > y ==> f x > f y) ==> f a > c" |
|
493 |
by (subgoal_tac "f a > f b", force, force) |
|
494 |
||
495 |
lemma xt6: "(a::'a::order) >= f b ==> b > c ==> |
|
496 |
(!!x y. x > y ==> f x > f y) ==> a > f c" |
|
497 |
by (subgoal_tac "f b > f c", force, force) |
|
498 |
||
499 |
lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> |
|
500 |
(!!x y. x >= y ==> f x >= f y) ==> f a > c" |
|
501 |
by (subgoal_tac "f a >= f b", force, force) |
|
502 |
||
503 |
lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==> |
|
504 |
(!!x y. x > y ==> f x > f y) ==> a > f c" |
|
505 |
by (subgoal_tac "f b > f c", force, force) |
|
506 |
||
507 |
lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==> |
|
508 |
(!!x y. x > y ==> f x > f y) ==> f a > c" |
|
509 |
by (subgoal_tac "f a > f b", force, force) |
|
510 |
||
511 |
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 |
|
512 |
||
513 |
(* |
|
514 |
Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands |
|
515 |
for the wrong thing in an Isar proof. |
|
516 |
||
517 |
The extra transitivity rules can be used as follows: |
|
518 |
||
519 |
lemma "(a::'a::order) > z" |
|
520 |
proof - |
|
521 |
have "a >= b" (is "_ >= ?rhs") |
|
522 |
sorry |
|
523 |
also have "?rhs >= c" (is "_ >= ?rhs") |
|
524 |
sorry |
|
525 |
also (xtrans) have "?rhs = d" (is "_ = ?rhs") |
|
526 |
sorry |
|
527 |
also (xtrans) have "?rhs >= e" (is "_ >= ?rhs") |
|
528 |
sorry |
|
529 |
also (xtrans) have "?rhs > f" (is "_ > ?rhs") |
|
530 |
sorry |
|
531 |
also (xtrans) have "?rhs > z" |
|
532 |
sorry |
|
533 |
finally (xtrans) show ?thesis . |
|
534 |
qed |
|
535 |
||
536 |
Alternatively, one can use "declare xtrans [trans]" and then |
|
537 |
leave out the "(xtrans)" above. |
|
538 |
*) |
|
539 |
||
540 |
||
541 |
subsection {* Least value operator, monotonicity and min/max *} |
|
542 |
||
543 |
(*FIXME: derive more of the min/max laws generically via semilattices*) |
|
544 |
||
545 |
constdefs |
|
546 |
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) |
|
547 |
"Least P == THE x. P x & (ALL y. P y --> x <= y)" |
|
548 |
-- {* We can no longer use LeastM because the latter requires Hilbert-AC. *} |
|
549 |
||
550 |
lemma LeastI2_order: |
|
551 |
"[| P (x::'a::order); |
|
552 |
!!y. P y ==> x <= y; |
|
553 |
!!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |] |
|
554 |
==> Q (Least P)" |
|
555 |
apply (unfold Least_def) |
|
556 |
apply (rule theI2) |
|
557 |
apply (blast intro: order_antisym)+ |
|
558 |
done |
|
559 |
||
560 |
lemma Least_equality: |
|
561 |
"[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k" |
|
562 |
apply (simp add: Least_def) |
|
563 |
apply (rule the_equality) |
|
564 |
apply (auto intro!: order_antisym) |
|
565 |
done |
|
566 |
||
567 |
locale mono = |
|
568 |
fixes f |
|
569 |
assumes mono: "A <= B ==> f A <= f B" |
|
570 |
||
571 |
lemmas monoI [intro?] = mono.intro |
|
572 |
and monoD [dest?] = mono.mono |
|
573 |
||
574 |
constdefs |
|
575 |
min :: "['a::ord, 'a] => 'a" |
|
576 |
"min a b == (if a <= b then a else b)" |
|
577 |
max :: "['a::ord, 'a] => 'a" |
|
578 |
"max a b == (if a <= b then b else a)" |
|
579 |
||
580 |
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least" |
|
581 |
apply (simp add: min_def) |
|
582 |
apply (blast intro: order_antisym) |
|
583 |
done |
|
584 |
||
585 |
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x" |
|
586 |
apply (simp add: max_def) |
|
587 |
apply (blast intro: order_antisym) |
|
588 |
done |
|
589 |
||
590 |
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" |
|
591 |
by (simp add: min_def) |
|
592 |
||
593 |
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" |
|
594 |
by (simp add: max_def) |
|
595 |
||
596 |
lemma min_of_mono: |
|
597 |
"(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" |
|
598 |
by (simp add: min_def) |
|
599 |
||
600 |
lemma max_of_mono: |
|
601 |
"(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" |
|
602 |
by (simp add: max_def) |
|
15524 | 603 |
|
604 |
text{* Instantiate locales: *} |
|
605 |
||
15837 | 606 |
interpretation min_max: |
15780 | 607 |
lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
608 |
apply unfold_locales |
15524 | 609 |
apply(simp add:min_def linorder_not_le order_less_imp_le) |
610 |
apply(simp add:min_def linorder_not_le order_less_imp_le) |
|
611 |
apply(simp add:min_def linorder_not_le order_less_imp_le) |
|
612 |
done |
|
613 |
||
15837 | 614 |
interpretation min_max: |
15780 | 615 |
upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
616 |
apply unfold_locales |
15524 | 617 |
apply(simp add: max_def linorder_not_le order_less_imp_le) |
618 |
apply(simp add: max_def linorder_not_le order_less_imp_le) |
|
619 |
apply(simp add: max_def linorder_not_le order_less_imp_le) |
|
620 |
done |
|
621 |
||
15837 | 622 |
interpretation min_max: |
15780 | 623 |
lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
624 |
by unfold_locales |
15524 | 625 |
|
15837 | 626 |
interpretation min_max: |
15780 | 627 |
distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] |
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset
|
628 |
apply unfold_locales |
15524 | 629 |
apply(rule_tac x=x and y=y in linorder_le_cases) |
630 |
apply(rule_tac x=x and y=z in linorder_le_cases) |
|
631 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
|
632 |
apply(simp add:min_def max_def) |
|
633 |
apply(simp add:min_def max_def) |
|
634 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
|
635 |
apply(simp add:min_def max_def) |
|
636 |
apply(simp add:min_def max_def) |
|
637 |
apply(rule_tac x=x and y=z in linorder_le_cases) |
|
638 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
|
639 |
apply(simp add:min_def max_def) |
|
640 |
apply(simp add:min_def max_def) |
|
641 |
apply(rule_tac x=y and y=z in linorder_le_cases) |
|
642 |
apply(simp add:min_def max_def) |
|
643 |
apply(simp add:min_def max_def) |
|
644 |
done |
|
645 |
||
646 |
lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)" |
|
647 |
apply(simp add:max_def) |
|
648 |
apply (insert linorder_linear) |
|
649 |
apply (blast intro: order_trans) |
|
650 |
done |
|
651 |
||
15780 | 652 |
lemmas le_maxI1 = min_max.sup_ge1 |
653 |
lemmas le_maxI2 = min_max.sup_ge2 |
|
15524 | 654 |
|
655 |
lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)" |
|
656 |
apply (simp add: max_def order_le_less) |
|
657 |
apply (insert linorder_less_linear) |
|
658 |
apply (blast intro: order_less_trans) |
|
659 |
done |
|
660 |
||
661 |
lemma max_less_iff_conj [simp]: |
|
662 |
"!!z::'a::linorder. (max x y < z) = (x < z & y < z)" |
|
663 |
apply (simp add: order_le_less max_def) |
|
664 |
apply (insert linorder_less_linear) |
|
665 |
apply (blast intro: order_less_trans) |
|
666 |
done |
|
15791 | 667 |
|
15524 | 668 |
lemma min_less_iff_conj [simp]: |
669 |
"!!z::'a::linorder. (z < min x y) = (z < x & z < y)" |
|
670 |
apply (simp add: order_le_less min_def) |
|
671 |
apply (insert linorder_less_linear) |
|
672 |
apply (blast intro: order_less_trans) |
|
673 |
done |
|
674 |
||
675 |
lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)" |
|
676 |
apply (simp add: min_def) |
|
677 |
apply (insert linorder_linear) |
|
678 |
apply (blast intro: order_trans) |
|
679 |
done |
|
680 |
||
681 |
lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)" |
|
682 |
apply (simp add: min_def order_le_less) |
|
683 |
apply (insert linorder_less_linear) |
|
684 |
apply (blast intro: order_less_trans) |
|
685 |
done |
|
686 |
||
15780 | 687 |
lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
688 |
mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute] |
|
15524 | 689 |
|
15780 | 690 |
lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
691 |
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute] |
|
15524 | 692 |
|
693 |
lemma split_min: |
|
694 |
"P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))" |
|
695 |
by (simp add: min_def) |
|
696 |
||
697 |
lemma split_max: |
|
698 |
"P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))" |
|
699 |
by (simp add: max_def) |
|
700 |
||
701 |
end |