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