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