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