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