haftmann@28685
|
1 |
(* Title: HOL/Orderings.thy
|
nipkow@15524
|
2 |
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson
|
nipkow@15524
|
3 |
*)
|
nipkow@15524
|
4 |
|
haftmann@25614
|
5 |
header {* Abstract orderings *}
|
nipkow@15524
|
6 |
|
nipkow@15524
|
7 |
theory Orderings
|
haftmann@35301
|
8 |
imports HOL
|
wenzelm@32215
|
9 |
uses
|
wenzelm@32215
|
10 |
"~~/src/Provers/order.ML"
|
wenzelm@32215
|
11 |
"~~/src/Provers/quasi.ML" (* FIXME unused? *)
|
nipkow@15524
|
12 |
begin
|
nipkow@15524
|
13 |
|
haftmann@35092
|
14 |
subsection {* Syntactic orders *}
|
haftmann@35092
|
15 |
|
haftmann@35092
|
16 |
class ord =
|
haftmann@35092
|
17 |
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
haftmann@35092
|
18 |
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
haftmann@35092
|
19 |
begin
|
haftmann@35092
|
20 |
|
haftmann@35092
|
21 |
notation
|
haftmann@35092
|
22 |
less_eq ("op <=") and
|
haftmann@35092
|
23 |
less_eq ("(_/ <= _)" [51, 51] 50) and
|
haftmann@35092
|
24 |
less ("op <") and
|
haftmann@35092
|
25 |
less ("(_/ < _)" [51, 51] 50)
|
haftmann@35092
|
26 |
|
haftmann@35092
|
27 |
notation (xsymbols)
|
haftmann@35092
|
28 |
less_eq ("op \<le>") and
|
haftmann@35092
|
29 |
less_eq ("(_/ \<le> _)" [51, 51] 50)
|
haftmann@35092
|
30 |
|
haftmann@35092
|
31 |
notation (HTML output)
|
haftmann@35092
|
32 |
less_eq ("op \<le>") and
|
haftmann@35092
|
33 |
less_eq ("(_/ \<le> _)" [51, 51] 50)
|
haftmann@35092
|
34 |
|
haftmann@35092
|
35 |
abbreviation (input)
|
haftmann@35092
|
36 |
greater_eq (infix ">=" 50) where
|
haftmann@35092
|
37 |
"x >= y \<equiv> y <= x"
|
haftmann@35092
|
38 |
|
haftmann@35092
|
39 |
notation (input)
|
haftmann@35092
|
40 |
greater_eq (infix "\<ge>" 50)
|
haftmann@35092
|
41 |
|
haftmann@35092
|
42 |
abbreviation (input)
|
haftmann@35092
|
43 |
greater (infix ">" 50) where
|
haftmann@35092
|
44 |
"x > y \<equiv> y < x"
|
haftmann@35092
|
45 |
|
haftmann@35092
|
46 |
end
|
haftmann@35092
|
47 |
|
haftmann@35092
|
48 |
|
haftmann@27682
|
49 |
subsection {* Quasi orders *}
|
nipkow@15524
|
50 |
|
haftmann@27682
|
51 |
class preorder = ord +
|
haftmann@27682
|
52 |
assumes less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)"
|
haftmann@25062
|
53 |
and order_refl [iff]: "x \<le> x"
|
haftmann@25062
|
54 |
and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
|
haftmann@21248
|
55 |
begin
|
haftmann@21248
|
56 |
|
nipkow@15524
|
57 |
text {* Reflexivity. *}
|
nipkow@15524
|
58 |
|
haftmann@25062
|
59 |
lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
|
nipkow@15524
|
60 |
-- {* This form is useful with the classical reasoner. *}
|
nipkow@23212
|
61 |
by (erule ssubst) (rule order_refl)
|
nipkow@15524
|
62 |
|
haftmann@25062
|
63 |
lemma less_irrefl [iff]: "\<not> x < x"
|
haftmann@27682
|
64 |
by (simp add: less_le_not_le)
|
haftmann@27682
|
65 |
|
haftmann@27682
|
66 |
lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
|
haftmann@27682
|
67 |
unfolding less_le_not_le by blast
|
haftmann@27682
|
68 |
|
haftmann@27682
|
69 |
|
haftmann@27682
|
70 |
text {* Asymmetry. *}
|
haftmann@27682
|
71 |
|
haftmann@27682
|
72 |
lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"
|
haftmann@27682
|
73 |
by (simp add: less_le_not_le)
|
haftmann@27682
|
74 |
|
haftmann@27682
|
75 |
lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P"
|
haftmann@27682
|
76 |
by (drule less_not_sym, erule contrapos_np) simp
|
haftmann@27682
|
77 |
|
haftmann@27682
|
78 |
|
haftmann@27682
|
79 |
text {* Transitivity. *}
|
haftmann@27682
|
80 |
|
haftmann@27682
|
81 |
lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
|
haftmann@27682
|
82 |
by (auto simp add: less_le_not_le intro: order_trans)
|
haftmann@27682
|
83 |
|
haftmann@27682
|
84 |
lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
|
haftmann@27682
|
85 |
by (auto simp add: less_le_not_le intro: order_trans)
|
haftmann@27682
|
86 |
|
haftmann@27682
|
87 |
lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z"
|
haftmann@27682
|
88 |
by (auto simp add: less_le_not_le intro: order_trans)
|
haftmann@27682
|
89 |
|
haftmann@27682
|
90 |
|
haftmann@27682
|
91 |
text {* Useful for simplification, but too risky to include by default. *}
|
haftmann@27682
|
92 |
|
haftmann@27682
|
93 |
lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True"
|
haftmann@27682
|
94 |
by (blast elim: less_asym)
|
haftmann@27682
|
95 |
|
haftmann@27682
|
96 |
lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True"
|
haftmann@27682
|
97 |
by (blast elim: less_asym)
|
haftmann@27682
|
98 |
|
haftmann@27682
|
99 |
|
haftmann@27682
|
100 |
text {* Transitivity rules for calculational reasoning *}
|
haftmann@27682
|
101 |
|
haftmann@27682
|
102 |
lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P"
|
haftmann@27682
|
103 |
by (rule less_asym)
|
haftmann@27682
|
104 |
|
haftmann@27682
|
105 |
|
haftmann@27682
|
106 |
text {* Dual order *}
|
haftmann@27682
|
107 |
|
haftmann@27682
|
108 |
lemma dual_preorder:
|
haftmann@36623
|
109 |
"class.preorder (op \<ge>) (op >)"
|
haftmann@28823
|
110 |
proof qed (auto simp add: less_le_not_le intro: order_trans)
|
haftmann@27682
|
111 |
|
haftmann@27682
|
112 |
end
|
haftmann@27682
|
113 |
|
haftmann@27682
|
114 |
|
haftmann@27682
|
115 |
subsection {* Partial orders *}
|
haftmann@27682
|
116 |
|
haftmann@27682
|
117 |
class order = preorder +
|
haftmann@27682
|
118 |
assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
|
haftmann@27682
|
119 |
begin
|
haftmann@27682
|
120 |
|
haftmann@27682
|
121 |
text {* Reflexivity. *}
|
haftmann@27682
|
122 |
|
haftmann@27682
|
123 |
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
|
haftmann@27682
|
124 |
by (auto simp add: less_le_not_le intro: antisym)
|
nipkow@15524
|
125 |
|
haftmann@25062
|
126 |
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
|
nipkow@15524
|
127 |
-- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
|
nipkow@23212
|
128 |
by (simp add: less_le) blast
|
nipkow@15524
|
129 |
|
haftmann@25062
|
130 |
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
|
nipkow@23212
|
131 |
unfolding less_le by blast
|
nipkow@15524
|
132 |
|
haftmann@21329
|
133 |
|
haftmann@21329
|
134 |
text {* Useful for simplification, but too risky to include by default. *}
|
haftmann@21329
|
135 |
|
haftmann@25062
|
136 |
lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False"
|
nipkow@23212
|
137 |
by auto
|
haftmann@21329
|
138 |
|
haftmann@25062
|
139 |
lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False"
|
nipkow@23212
|
140 |
by auto
|
haftmann@21329
|
141 |
|
haftmann@21329
|
142 |
|
haftmann@21329
|
143 |
text {* Transitivity rules for calculational reasoning *}
|
haftmann@21329
|
144 |
|
haftmann@25062
|
145 |
lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
|
nipkow@23212
|
146 |
by (simp add: less_le)
|
haftmann@21329
|
147 |
|
haftmann@25062
|
148 |
lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
|
nipkow@23212
|
149 |
by (simp add: less_le)
|
haftmann@21329
|
150 |
|
nipkow@15524
|
151 |
|
nipkow@15524
|
152 |
text {* Asymmetry. *}
|
nipkow@15524
|
153 |
|
haftmann@25062
|
154 |
lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
|
nipkow@23212
|
155 |
by (blast intro: antisym)
|
nipkow@15524
|
156 |
|
haftmann@25062
|
157 |
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
|
nipkow@23212
|
158 |
by (blast intro: antisym)
|
nipkow@15524
|
159 |
|
haftmann@25062
|
160 |
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
|
nipkow@23212
|
161 |
by (erule contrapos_pn, erule subst, rule less_irrefl)
|
haftmann@21248
|
162 |
|
haftmann@21083
|
163 |
|
haftmann@27107
|
164 |
text {* Least value operator *}
|
haftmann@27107
|
165 |
|
haftmann@27299
|
166 |
definition (in ord)
|
haftmann@27107
|
167 |
Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
|
haftmann@27107
|
168 |
"Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
|
haftmann@27107
|
169 |
|
haftmann@27107
|
170 |
lemma Least_equality:
|
haftmann@27107
|
171 |
assumes "P x"
|
haftmann@27107
|
172 |
and "\<And>y. P y \<Longrightarrow> x \<le> y"
|
haftmann@27107
|
173 |
shows "Least P = x"
|
haftmann@27107
|
174 |
unfolding Least_def by (rule the_equality)
|
haftmann@27107
|
175 |
(blast intro: assms antisym)+
|
haftmann@27107
|
176 |
|
haftmann@27107
|
177 |
lemma LeastI2_order:
|
haftmann@27107
|
178 |
assumes "P x"
|
haftmann@27107
|
179 |
and "\<And>y. P y \<Longrightarrow> x \<le> y"
|
haftmann@27107
|
180 |
and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
|
haftmann@27107
|
181 |
shows "Q (Least P)"
|
haftmann@27107
|
182 |
unfolding Least_def by (rule theI2)
|
haftmann@27107
|
183 |
(blast intro: assms antisym)+
|
haftmann@27107
|
184 |
|
haftmann@27107
|
185 |
|
haftmann@26014
|
186 |
text {* Dual order *}
|
haftmann@22916
|
187 |
|
haftmann@26014
|
188 |
lemma dual_order:
|
haftmann@36623
|
189 |
"class.order (op \<ge>) (op >)"
|
haftmann@27682
|
190 |
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
|
haftmann@22916
|
191 |
|
haftmann@21248
|
192 |
end
|
nipkow@15524
|
193 |
|
haftmann@21329
|
194 |
|
haftmann@21329
|
195 |
subsection {* Linear (total) orders *}
|
haftmann@21329
|
196 |
|
haftmann@22316
|
197 |
class linorder = order +
|
haftmann@25207
|
198 |
assumes linear: "x \<le> y \<or> y \<le> x"
|
haftmann@21248
|
199 |
begin
|
haftmann@21248
|
200 |
|
haftmann@25062
|
201 |
lemma less_linear: "x < y \<or> x = y \<or> y < x"
|
nipkow@23212
|
202 |
unfolding less_le using less_le linear by blast
|
haftmann@21248
|
203 |
|
haftmann@25062
|
204 |
lemma le_less_linear: "x \<le> y \<or> y < x"
|
nipkow@23212
|
205 |
by (simp add: le_less less_linear)
|
haftmann@21248
|
206 |
|
haftmann@21248
|
207 |
lemma le_cases [case_names le ge]:
|
haftmann@25062
|
208 |
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
|
nipkow@23212
|
209 |
using linear by blast
|
haftmann@21248
|
210 |
|
haftmann@22384
|
211 |
lemma linorder_cases [case_names less equal greater]:
|
haftmann@25062
|
212 |
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
|
nipkow@23212
|
213 |
using less_linear by blast
|
haftmann@21248
|
214 |
|
haftmann@25062
|
215 |
lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
|
nipkow@23212
|
216 |
apply (simp add: less_le)
|
nipkow@23212
|
217 |
using linear apply (blast intro: antisym)
|
nipkow@23212
|
218 |
done
|
nipkow@23212
|
219 |
|
nipkow@23212
|
220 |
lemma not_less_iff_gr_or_eq:
|
haftmann@25062
|
221 |
"\<not>(x < y) \<longleftrightarrow> (x > y | x = y)"
|
nipkow@23212
|
222 |
apply(simp add:not_less le_less)
|
nipkow@23212
|
223 |
apply blast
|
nipkow@23212
|
224 |
done
|
nipkow@15524
|
225 |
|
haftmann@25062
|
226 |
lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
|
nipkow@23212
|
227 |
apply (simp add: less_le)
|
nipkow@23212
|
228 |
using linear apply (blast intro: antisym)
|
nipkow@23212
|
229 |
done
|
nipkow@15524
|
230 |
|
haftmann@25062
|
231 |
lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
|
nipkow@23212
|
232 |
by (cut_tac x = x and y = y in less_linear, auto)
|
nipkow@15524
|
233 |
|
haftmann@25062
|
234 |
lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
|
nipkow@23212
|
235 |
by (simp add: neq_iff) blast
|
nipkow@15524
|
236 |
|
haftmann@25062
|
237 |
lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
|
nipkow@23212
|
238 |
by (blast intro: antisym dest: not_less [THEN iffD1])
|
nipkow@15524
|
239 |
|
haftmann@25062
|
240 |
lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
|
nipkow@23212
|
241 |
by (blast intro: antisym dest: not_less [THEN iffD1])
|
nipkow@15524
|
242 |
|
haftmann@25062
|
243 |
lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
|
nipkow@23212
|
244 |
by (blast intro: antisym dest: not_less [THEN iffD1])
|
nipkow@15524
|
245 |
|
haftmann@25062
|
246 |
lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
|
nipkow@23212
|
247 |
unfolding not_less .
|
paulson@16796
|
248 |
|
haftmann@25062
|
249 |
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
|
nipkow@23212
|
250 |
unfolding not_less .
|
paulson@16796
|
251 |
|
paulson@16796
|
252 |
(*FIXME inappropriate name (or delete altogether)*)
|
haftmann@25062
|
253 |
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y"
|
nipkow@23212
|
254 |
unfolding not_le .
|
haftmann@21248
|
255 |
|
haftmann@22916
|
256 |
|
haftmann@26014
|
257 |
text {* Dual order *}
|
haftmann@22916
|
258 |
|
haftmann@26014
|
259 |
lemma dual_linorder:
|
haftmann@36623
|
260 |
"class.linorder (op \<ge>) (op >)"
|
haftmann@36623
|
261 |
by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
|
haftmann@22916
|
262 |
|
haftmann@22916
|
263 |
|
haftmann@23881
|
264 |
text {* min/max *}
|
haftmann@23881
|
265 |
|
haftmann@27299
|
266 |
definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
|
haftmann@37767
|
267 |
"min a b = (if a \<le> b then a else b)"
|
haftmann@23881
|
268 |
|
haftmann@27299
|
269 |
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
|
haftmann@37767
|
270 |
"max a b = (if a \<le> b then b else a)"
|
haftmann@22384
|
271 |
|
haftmann@21383
|
272 |
lemma min_le_iff_disj:
|
haftmann@25062
|
273 |
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
|
nipkow@23212
|
274 |
unfolding min_def using linear by (auto intro: order_trans)
|
haftmann@21383
|
275 |
|
haftmann@21383
|
276 |
lemma le_max_iff_disj:
|
haftmann@25062
|
277 |
"z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
|
nipkow@23212
|
278 |
unfolding max_def using linear by (auto intro: order_trans)
|
haftmann@21383
|
279 |
|
haftmann@21383
|
280 |
lemma min_less_iff_disj:
|
haftmann@25062
|
281 |
"min x y < z \<longleftrightarrow> x < z \<or> y < z"
|
nipkow@23212
|
282 |
unfolding min_def le_less using less_linear by (auto intro: less_trans)
|
haftmann@21383
|
283 |
|
haftmann@21383
|
284 |
lemma less_max_iff_disj:
|
haftmann@25062
|
285 |
"z < max x y \<longleftrightarrow> z < x \<or> z < y"
|
nipkow@23212
|
286 |
unfolding max_def le_less using less_linear by (auto intro: less_trans)
|
haftmann@21383
|
287 |
|
haftmann@21383
|
288 |
lemma min_less_iff_conj [simp]:
|
haftmann@25062
|
289 |
"z < min x y \<longleftrightarrow> z < x \<and> z < y"
|
nipkow@23212
|
290 |
unfolding min_def le_less using less_linear by (auto intro: less_trans)
|
haftmann@21383
|
291 |
|
haftmann@21383
|
292 |
lemma max_less_iff_conj [simp]:
|
haftmann@25062
|
293 |
"max x y < z \<longleftrightarrow> x < z \<and> y < z"
|
nipkow@23212
|
294 |
unfolding max_def le_less using less_linear by (auto intro: less_trans)
|
haftmann@21383
|
295 |
|
blanchet@35828
|
296 |
lemma split_min [no_atp]:
|
haftmann@25062
|
297 |
"P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
|
nipkow@23212
|
298 |
by (simp add: min_def)
|
haftmann@21383
|
299 |
|
blanchet@35828
|
300 |
lemma split_max [no_atp]:
|
haftmann@25062
|
301 |
"P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
|
nipkow@23212
|
302 |
by (simp add: max_def)
|
haftmann@21383
|
303 |
|
haftmann@21248
|
304 |
end
|
haftmann@21248
|
305 |
|
haftmann@28516
|
306 |
text {* Explicit dictionaries for code generation *}
|
haftmann@28516
|
307 |
|
haftmann@31998
|
308 |
lemma min_ord_min [code, code_unfold, code_inline del]:
|
haftmann@28516
|
309 |
"min = ord.min (op \<le>)"
|
haftmann@28516
|
310 |
by (rule ext)+ (simp add: min_def ord.min_def)
|
haftmann@28516
|
311 |
|
haftmann@28516
|
312 |
declare ord.min_def [code]
|
haftmann@28516
|
313 |
|
haftmann@31998
|
314 |
lemma max_ord_max [code, code_unfold, code_inline del]:
|
haftmann@28516
|
315 |
"max = ord.max (op \<le>)"
|
haftmann@28516
|
316 |
by (rule ext)+ (simp add: max_def ord.max_def)
|
haftmann@28516
|
317 |
|
haftmann@28516
|
318 |
declare ord.max_def [code]
|
haftmann@28516
|
319 |
|
haftmann@23948
|
320 |
|
haftmann@21083
|
321 |
subsection {* Reasoning tools setup *}
|
nipkow@15524
|
322 |
|
haftmann@21091
|
323 |
ML {*
|
haftmann@21091
|
324 |
|
ballarin@24641
|
325 |
signature ORDERS =
|
ballarin@24641
|
326 |
sig
|
ballarin@24641
|
327 |
val print_structures: Proof.context -> unit
|
ballarin@24641
|
328 |
val setup: theory -> theory
|
wenzelm@32215
|
329 |
val order_tac: Proof.context -> thm list -> int -> tactic
|
ballarin@24641
|
330 |
end;
|
ballarin@24641
|
331 |
|
ballarin@24641
|
332 |
structure Orders: ORDERS =
|
ballarin@24641
|
333 |
struct
|
ballarin@24641
|
334 |
|
ballarin@24641
|
335 |
(** Theory and context data **)
|
ballarin@24641
|
336 |
|
ballarin@24641
|
337 |
fun struct_eq ((s1: string, ts1), (s2, ts2)) =
|
ballarin@24641
|
338 |
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
|
ballarin@24641
|
339 |
|
wenzelm@33519
|
340 |
structure Data = Generic_Data
|
ballarin@24641
|
341 |
(
|
ballarin@24641
|
342 |
type T = ((string * term list) * Order_Tac.less_arith) list;
|
ballarin@24641
|
343 |
(* Order structures:
|
ballarin@24641
|
344 |
identifier of the structure, list of operations and record of theorems
|
ballarin@24641
|
345 |
needed to set up the transitivity reasoner,
|
ballarin@24641
|
346 |
identifier and operations identify the structure uniquely. *)
|
ballarin@24641
|
347 |
val empty = [];
|
ballarin@24641
|
348 |
val extend = I;
|
wenzelm@33519
|
349 |
fun merge data = AList.join struct_eq (K fst) data;
|
ballarin@24641
|
350 |
);
|
ballarin@24641
|
351 |
|
ballarin@24641
|
352 |
fun print_structures ctxt =
|
haftmann@21248
|
353 |
let
|
ballarin@24641
|
354 |
val structs = Data.get (Context.Proof ctxt);
|
ballarin@24641
|
355 |
fun pretty_term t = Pretty.block
|
wenzelm@24920
|
356 |
[Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
|
ballarin@24641
|
357 |
Pretty.str "::", Pretty.brk 1,
|
wenzelm@24920
|
358 |
Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
|
ballarin@24641
|
359 |
fun pretty_struct ((s, ts), _) = Pretty.block
|
ballarin@24641
|
360 |
[Pretty.str s, Pretty.str ":", Pretty.brk 1,
|
ballarin@24641
|
361 |
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
|
ballarin@24641
|
362 |
in
|
ballarin@24641
|
363 |
Pretty.writeln (Pretty.big_list "Order structures:" (map pretty_struct structs))
|
ballarin@24641
|
364 |
end;
|
ballarin@24641
|
365 |
|
ballarin@24641
|
366 |
|
ballarin@24641
|
367 |
(** Method **)
|
ballarin@24641
|
368 |
|
wenzelm@32215
|
369 |
fun struct_tac ((s, [eq, le, less]), thms) ctxt prems =
|
ballarin@24641
|
370 |
let
|
berghofe@30107
|
371 |
fun decomp thy (@{const Trueprop} $ t) =
|
haftmann@21248
|
372 |
let
|
ballarin@24641
|
373 |
fun excluded t =
|
ballarin@24641
|
374 |
(* exclude numeric types: linear arithmetic subsumes transitivity *)
|
ballarin@24641
|
375 |
let val T = type_of t
|
ballarin@24641
|
376 |
in
|
wenzelm@32962
|
377 |
T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT
|
ballarin@24641
|
378 |
end;
|
wenzelm@32962
|
379 |
fun rel (bin_op $ t1 $ t2) =
|
ballarin@24641
|
380 |
if excluded t1 then NONE
|
ballarin@24641
|
381 |
else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2)
|
ballarin@24641
|
382 |
else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2)
|
ballarin@24641
|
383 |
else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2)
|
ballarin@24641
|
384 |
else NONE
|
wenzelm@32962
|
385 |
| rel _ = NONE;
|
wenzelm@32962
|
386 |
fun dec (Const (@{const_name Not}, _) $ t) = (case rel t
|
wenzelm@32962
|
387 |
of NONE => NONE
|
wenzelm@32962
|
388 |
| SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
|
ballarin@24741
|
389 |
| dec x = rel x;
|
berghofe@30107
|
390 |
in dec t end
|
berghofe@30107
|
391 |
| decomp thy _ = NONE;
|
ballarin@24641
|
392 |
in
|
ballarin@24641
|
393 |
case s of
|
wenzelm@32215
|
394 |
"order" => Order_Tac.partial_tac decomp thms ctxt prems
|
wenzelm@32215
|
395 |
| "linorder" => Order_Tac.linear_tac decomp thms ctxt prems
|
ballarin@24641
|
396 |
| _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.")
|
ballarin@24641
|
397 |
end
|
haftmann@21091
|
398 |
|
wenzelm@32215
|
399 |
fun order_tac ctxt prems =
|
wenzelm@32215
|
400 |
FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt)));
|
haftmann@21091
|
401 |
|
haftmann@21091
|
402 |
|
ballarin@24641
|
403 |
(** Attribute **)
|
ballarin@24641
|
404 |
|
ballarin@24641
|
405 |
fun add_struct_thm s tag =
|
ballarin@24641
|
406 |
Thm.declaration_attribute
|
ballarin@24641
|
407 |
(fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm)));
|
ballarin@24641
|
408 |
fun del_struct s =
|
ballarin@24641
|
409 |
Thm.declaration_attribute
|
ballarin@24641
|
410 |
(fn _ => Data.map (AList.delete struct_eq s));
|
ballarin@24641
|
411 |
|
wenzelm@30722
|
412 |
val attrib_setup =
|
wenzelm@30722
|
413 |
Attrib.setup @{binding order}
|
wenzelm@30722
|
414 |
(Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) || Args.del >> K NONE) --|
|
wenzelm@30722
|
415 |
Args.colon (* FIXME || Scan.succeed true *) ) -- Scan.lift Args.name --
|
wenzelm@30722
|
416 |
Scan.repeat Args.term
|
wenzelm@30722
|
417 |
>> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
|
wenzelm@30722
|
418 |
| ((NONE, n), ts) => del_struct (n, ts)))
|
wenzelm@30722
|
419 |
"theorems controlling transitivity reasoner";
|
ballarin@24641
|
420 |
|
ballarin@24641
|
421 |
|
ballarin@24641
|
422 |
(** Diagnostic command **)
|
ballarin@24641
|
423 |
|
wenzelm@24867
|
424 |
val _ =
|
wenzelm@36970
|
425 |
Outer_Syntax.improper_command "print_orders"
|
wenzelm@36970
|
426 |
"print order structures available to transitivity reasoner" Keyword.diag
|
wenzelm@30808
|
427 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
|
wenzelm@30808
|
428 |
Toplevel.keep (print_structures o Toplevel.context_of)));
|
ballarin@24641
|
429 |
|
ballarin@24641
|
430 |
|
ballarin@24641
|
431 |
(** Setup **)
|
ballarin@24641
|
432 |
|
wenzelm@24867
|
433 |
val setup =
|
wenzelm@32215
|
434 |
Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt [])))
|
wenzelm@30722
|
435 |
"transitivity reasoner" #>
|
wenzelm@30722
|
436 |
attrib_setup;
|
haftmann@21091
|
437 |
|
haftmann@21091
|
438 |
end;
|
ballarin@24641
|
439 |
|
haftmann@21091
|
440 |
*}
|
haftmann@21091
|
441 |
|
ballarin@24641
|
442 |
setup Orders.setup
|
ballarin@24641
|
443 |
|
ballarin@24641
|
444 |
|
ballarin@24641
|
445 |
text {* Declarations to set up transitivity reasoner of partial and linear orders. *}
|
ballarin@24641
|
446 |
|
haftmann@25076
|
447 |
context order
|
haftmann@25076
|
448 |
begin
|
haftmann@25076
|
449 |
|
ballarin@24641
|
450 |
(* The type constraint on @{term op =} below is necessary since the operation
|
ballarin@24641
|
451 |
is not a parameter of the locale. *)
|
haftmann@25076
|
452 |
|
haftmann@27689
|
453 |
declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"]
|
haftmann@27689
|
454 |
|
haftmann@27689
|
455 |
declare order_refl [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
456 |
|
haftmann@27689
|
457 |
declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
458 |
|
haftmann@27689
|
459 |
declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
460 |
|
haftmann@27689
|
461 |
declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
462 |
|
haftmann@27689
|
463 |
declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
464 |
|
haftmann@27689
|
465 |
declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
466 |
|
haftmann@27689
|
467 |
declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
468 |
|
haftmann@27689
|
469 |
declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
470 |
|
haftmann@27689
|
471 |
declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
472 |
|
haftmann@27689
|
473 |
declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
474 |
|
haftmann@27689
|
475 |
declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
476 |
|
haftmann@27689
|
477 |
declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
478 |
|
haftmann@27689
|
479 |
declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
480 |
|
haftmann@27689
|
481 |
declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"]
|
ballarin@24641
|
482 |
|
haftmann@25076
|
483 |
end
|
ballarin@24641
|
484 |
|
haftmann@25076
|
485 |
context linorder
|
haftmann@25076
|
486 |
begin
|
haftmann@25076
|
487 |
|
haftmann@27689
|
488 |
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]]
|
haftmann@25076
|
489 |
|
haftmann@27689
|
490 |
declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
491 |
|
haftmann@27689
|
492 |
declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
493 |
|
haftmann@27689
|
494 |
declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
495 |
|
haftmann@27689
|
496 |
declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
497 |
|
haftmann@27689
|
498 |
declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
499 |
|
haftmann@27689
|
500 |
declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
501 |
|
haftmann@27689
|
502 |
declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
503 |
|
haftmann@27689
|
504 |
declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
505 |
|
haftmann@27689
|
506 |
declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
507 |
|
haftmann@27689
|
508 |
declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
509 |
|
haftmann@27689
|
510 |
declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
511 |
|
haftmann@27689
|
512 |
declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
513 |
|
haftmann@27689
|
514 |
declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
515 |
|
haftmann@27689
|
516 |
declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
517 |
|
haftmann@27689
|
518 |
declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
519 |
|
haftmann@27689
|
520 |
declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
521 |
|
haftmann@27689
|
522 |
declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
523 |
|
haftmann@27689
|
524 |
declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
haftmann@27689
|
525 |
|
haftmann@27689
|
526 |
declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"]
|
ballarin@24641
|
527 |
|
haftmann@25076
|
528 |
end
|
haftmann@25076
|
529 |
|
ballarin@24641
|
530 |
|
haftmann@21083
|
531 |
setup {*
|
haftmann@21083
|
532 |
let
|
nipkow@15524
|
533 |
|
haftmann@21083
|
534 |
fun prp t thm = (#prop (rep_thm thm) = t);
|
haftmann@21083
|
535 |
|
haftmann@21083
|
536 |
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
|
wenzelm@44470
|
537 |
let val prems = Simplifier.prems_of ss;
|
haftmann@22916
|
538 |
val less = Const (@{const_name less}, T);
|
haftmann@21083
|
539 |
val t = HOLogic.mk_Trueprop(le $ s $ r);
|
haftmann@21083
|
540 |
in case find_first (prp t) prems of
|
haftmann@21083
|
541 |
NONE =>
|
haftmann@21083
|
542 |
let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
|
haftmann@21083
|
543 |
in case find_first (prp t) prems of
|
haftmann@21083
|
544 |
NONE => NONE
|
haftmann@24422
|
545 |
| SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))
|
haftmann@21083
|
546 |
end
|
haftmann@24422
|
547 |
| SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv}))
|
haftmann@21083
|
548 |
end
|
haftmann@21083
|
549 |
handle THM _ => NONE;
|
haftmann@21083
|
550 |
|
haftmann@21083
|
551 |
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
|
wenzelm@44470
|
552 |
let val prems = Simplifier.prems_of ss;
|
haftmann@22916
|
553 |
val le = Const (@{const_name less_eq}, T);
|
haftmann@21083
|
554 |
val t = HOLogic.mk_Trueprop(le $ r $ s);
|
haftmann@21083
|
555 |
in case find_first (prp t) prems of
|
haftmann@21083
|
556 |
NONE =>
|
haftmann@21083
|
557 |
let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
|
haftmann@21083
|
558 |
in case find_first (prp t) prems of
|
haftmann@21083
|
559 |
NONE => NONE
|
haftmann@24422
|
560 |
| SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))
|
haftmann@21083
|
561 |
end
|
haftmann@24422
|
562 |
| SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2}))
|
haftmann@21083
|
563 |
end
|
haftmann@21083
|
564 |
handle THM _ => NONE;
|
haftmann@21083
|
565 |
|
haftmann@21248
|
566 |
fun add_simprocs procs thy =
|
wenzelm@43667
|
567 |
Simplifier.map_simpset_global (fn ss => ss
|
haftmann@21248
|
568 |
addsimprocs (map (fn (name, raw_ts, proc) =>
|
wenzelm@38963
|
569 |
Simplifier.simproc_global thy name raw_ts proc) procs)) thy;
|
wenzelm@43667
|
570 |
|
wenzelm@26496
|
571 |
fun add_solver name tac =
|
wenzelm@43667
|
572 |
Simplifier.map_simpset_global (fn ss => ss addSolver
|
wenzelm@44470
|
573 |
mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss)));
|
haftmann@21083
|
574 |
|
haftmann@21083
|
575 |
in
|
haftmann@21248
|
576 |
add_simprocs [
|
haftmann@21248
|
577 |
("antisym le", ["(x::'a::order) <= y"], prove_antisym_le),
|
haftmann@21248
|
578 |
("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less)
|
haftmann@21248
|
579 |
]
|
ballarin@24641
|
580 |
#> add_solver "Transitivity" Orders.order_tac
|
haftmann@21248
|
581 |
(* Adding the transitivity reasoners also as safe solvers showed a slight
|
haftmann@21248
|
582 |
speed up, but the reasoning strength appears to be not higher (at least
|
haftmann@21248
|
583 |
no breaking of additional proofs in the entire HOL distribution, as
|
haftmann@21248
|
584 |
of 5 March 2004, was observed). *)
|
haftmann@21083
|
585 |
end
|
haftmann@21083
|
586 |
*}
|
nipkow@15524
|
587 |
|
nipkow@15524
|
588 |
|
haftmann@21083
|
589 |
subsection {* Bounded quantifiers *}
|
nipkow@15524
|
590 |
|
nipkow@15524
|
591 |
syntax
|
wenzelm@21180
|
592 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
593 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
594 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
595 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
596 |
|
wenzelm@21180
|
597 |
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
598 |
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
599 |
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
600 |
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
601 |
|
nipkow@15524
|
602 |
syntax (xsymbols)
|
wenzelm@21180
|
603 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
604 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
605 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
606 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
607 |
|
wenzelm@21180
|
608 |
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
609 |
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
610 |
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
611 |
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
612 |
|
nipkow@15524
|
613 |
syntax (HOL)
|
wenzelm@21180
|
614 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
615 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
616 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
617 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
618 |
|
nipkow@15524
|
619 |
syntax (HTML output)
|
wenzelm@21180
|
620 |
"_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
621 |
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
622 |
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
623 |
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
624 |
|
wenzelm@21180
|
625 |
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
626 |
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
627 |
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
|
wenzelm@21180
|
628 |
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
|
nipkow@15524
|
629 |
|
nipkow@15524
|
630 |
translations
|
haftmann@21044
|
631 |
"ALL x<y. P" => "ALL x. x < y \<longrightarrow> P"
|
haftmann@21044
|
632 |
"EX x<y. P" => "EX x. x < y \<and> P"
|
haftmann@21044
|
633 |
"ALL x<=y. P" => "ALL x. x <= y \<longrightarrow> P"
|
haftmann@21044
|
634 |
"EX x<=y. P" => "EX x. x <= y \<and> P"
|
haftmann@21044
|
635 |
"ALL x>y. P" => "ALL x. x > y \<longrightarrow> P"
|
haftmann@21044
|
636 |
"EX x>y. P" => "EX x. x > y \<and> P"
|
haftmann@21044
|
637 |
"ALL x>=y. P" => "ALL x. x >= y \<longrightarrow> P"
|
haftmann@21044
|
638 |
"EX x>=y. P" => "EX x. x >= y \<and> P"
|
nipkow@15524
|
639 |
|
nipkow@15524
|
640 |
print_translation {*
|
nipkow@15524
|
641 |
let
|
wenzelm@43159
|
642 |
val All_binder = Mixfix.binder_name @{const_syntax All};
|
wenzelm@43159
|
643 |
val Ex_binder = Mixfix.binder_name @{const_syntax Ex};
|
haftmann@39019
|
644 |
val impl = @{const_syntax HOL.implies};
|
haftmann@39028
|
645 |
val conj = @{const_syntax HOL.conj};
|
haftmann@22916
|
646 |
val less = @{const_syntax less};
|
haftmann@22916
|
647 |
val less_eq = @{const_syntax less_eq};
|
wenzelm@21180
|
648 |
|
wenzelm@21180
|
649 |
val trans =
|
wenzelm@35118
|
650 |
[((All_binder, impl, less),
|
wenzelm@35118
|
651 |
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})),
|
wenzelm@35118
|
652 |
((All_binder, impl, less_eq),
|
wenzelm@35118
|
653 |
(@{syntax_const "_All_less_eq"}, @{syntax_const "_All_greater_eq"})),
|
wenzelm@35118
|
654 |
((Ex_binder, conj, less),
|
wenzelm@35118
|
655 |
(@{syntax_const "_Ex_less"}, @{syntax_const "_Ex_greater"})),
|
wenzelm@35118
|
656 |
((Ex_binder, conj, less_eq),
|
wenzelm@35118
|
657 |
(@{syntax_const "_Ex_less_eq"}, @{syntax_const "_Ex_greater_eq"}))];
|
wenzelm@21180
|
658 |
|
wenzelm@35118
|
659 |
fun matches_bound v t =
|
wenzelm@35118
|
660 |
(case t of
|
wenzelm@35364
|
661 |
Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
|
wenzelm@35118
|
662 |
| _ => false);
|
wenzelm@35118
|
663 |
fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
|
wenzelm@43156
|
664 |
fun mk v c n P = Syntax.const c $ Syntax_Trans.mark_bound v $ n $ P;
|
wenzelm@21180
|
665 |
|
wenzelm@21180
|
666 |
fun tr' q = (q,
|
wenzelm@35364
|
667 |
fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
|
wenzelm@35364
|
668 |
Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
|
wenzelm@35118
|
669 |
(case AList.lookup (op =) trans (q, c, d) of
|
wenzelm@35118
|
670 |
NONE => raise Match
|
wenzelm@35118
|
671 |
| SOME (l, g) =>
|
wenzelm@35118
|
672 |
if matches_bound v t andalso not (contains_var v u) then mk v l u P
|
wenzelm@35118
|
673 |
else if matches_bound v u andalso not (contains_var v t) then mk v g t P
|
wenzelm@35118
|
674 |
else raise Match)
|
wenzelm@21180
|
675 |
| _ => raise Match);
|
wenzelm@21524
|
676 |
in [tr' All_binder, tr' Ex_binder] end
|
nipkow@15524
|
677 |
*}
|
nipkow@15524
|
678 |
|
haftmann@21044
|
679 |
|
haftmann@21383
|
680 |
subsection {* Transitivity reasoning *}
|
haftmann@21383
|
681 |
|
haftmann@25193
|
682 |
context ord
|
haftmann@25193
|
683 |
begin
|
haftmann@21383
|
684 |
|
haftmann@25193
|
685 |
lemma ord_le_eq_trans: "a \<le> b \<Longrightarrow> b = c \<Longrightarrow> a \<le> c"
|
haftmann@25193
|
686 |
by (rule subst)
|
haftmann@21383
|
687 |
|
haftmann@25193
|
688 |
lemma ord_eq_le_trans: "a = b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
|
haftmann@25193
|
689 |
by (rule ssubst)
|
haftmann@21383
|
690 |
|
haftmann@25193
|
691 |
lemma ord_less_eq_trans: "a < b \<Longrightarrow> b = c \<Longrightarrow> a < c"
|
haftmann@25193
|
692 |
by (rule subst)
|
haftmann@25193
|
693 |
|
haftmann@25193
|
694 |
lemma ord_eq_less_trans: "a = b \<Longrightarrow> b < c \<Longrightarrow> a < c"
|
haftmann@25193
|
695 |
by (rule ssubst)
|
haftmann@25193
|
696 |
|
haftmann@25193
|
697 |
end
|
haftmann@21383
|
698 |
|
haftmann@21383
|
699 |
lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
|
haftmann@21383
|
700 |
(!!x y. x < y ==> f x < f y) ==> f a < c"
|
haftmann@21383
|
701 |
proof -
|
haftmann@21383
|
702 |
assume r: "!!x y. x < y ==> f x < f y"
|
haftmann@21383
|
703 |
assume "a < b" hence "f a < f b" by (rule r)
|
haftmann@21383
|
704 |
also assume "f b < c"
|
haftmann@34245
|
705 |
finally (less_trans) show ?thesis .
|
haftmann@21383
|
706 |
qed
|
haftmann@21383
|
707 |
|
haftmann@21383
|
708 |
lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==>
|
haftmann@21383
|
709 |
(!!x y. x < y ==> f x < f y) ==> a < f c"
|
haftmann@21383
|
710 |
proof -
|
haftmann@21383
|
711 |
assume r: "!!x y. x < y ==> f x < f y"
|
haftmann@21383
|
712 |
assume "a < f b"
|
haftmann@21383
|
713 |
also assume "b < c" hence "f b < f c" by (rule r)
|
haftmann@34245
|
714 |
finally (less_trans) show ?thesis .
|
haftmann@21383
|
715 |
qed
|
haftmann@21383
|
716 |
|
haftmann@21383
|
717 |
lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==>
|
haftmann@21383
|
718 |
(!!x y. x <= y ==> f x <= f y) ==> f a < c"
|
haftmann@21383
|
719 |
proof -
|
haftmann@21383
|
720 |
assume r: "!!x y. x <= y ==> f x <= f y"
|
haftmann@21383
|
721 |
assume "a <= b" hence "f a <= f b" by (rule r)
|
haftmann@21383
|
722 |
also assume "f b < c"
|
haftmann@34245
|
723 |
finally (le_less_trans) show ?thesis .
|
haftmann@21383
|
724 |
qed
|
haftmann@21383
|
725 |
|
haftmann@21383
|
726 |
lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==>
|
haftmann@21383
|
727 |
(!!x y. x < y ==> f x < f y) ==> a < f c"
|
haftmann@21383
|
728 |
proof -
|
haftmann@21383
|
729 |
assume r: "!!x y. x < y ==> f x < f y"
|
haftmann@21383
|
730 |
assume "a <= f b"
|
haftmann@21383
|
731 |
also assume "b < c" hence "f b < f c" by (rule r)
|
haftmann@34245
|
732 |
finally (le_less_trans) show ?thesis .
|
haftmann@21383
|
733 |
qed
|
haftmann@21383
|
734 |
|
haftmann@21383
|
735 |
lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==>
|
haftmann@21383
|
736 |
(!!x y. x < y ==> f x < f y) ==> f a < c"
|
haftmann@21383
|
737 |
proof -
|
haftmann@21383
|
738 |
assume r: "!!x y. x < y ==> f x < f y"
|
haftmann@21383
|
739 |
assume "a < b" hence "f a < f b" by (rule r)
|
haftmann@21383
|
740 |
also assume "f b <= c"
|
haftmann@34245
|
741 |
finally (less_le_trans) show ?thesis .
|
haftmann@21383
|
742 |
qed
|
haftmann@21383
|
743 |
|
haftmann@21383
|
744 |
lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==>
|
haftmann@21383
|
745 |
(!!x y. x <= y ==> f x <= f y) ==> a < f c"
|
haftmann@21383
|
746 |
proof -
|
haftmann@21383
|
747 |
assume r: "!!x y. x <= y ==> f x <= f y"
|
haftmann@21383
|
748 |
assume "a < f b"
|
haftmann@21383
|
749 |
also assume "b <= c" hence "f b <= f c" by (rule r)
|
haftmann@34245
|
750 |
finally (less_le_trans) show ?thesis .
|
haftmann@21383
|
751 |
qed
|
haftmann@21383
|
752 |
|
haftmann@21383
|
753 |
lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==>
|
haftmann@21383
|
754 |
(!!x y. x <= y ==> f x <= f y) ==> a <= f c"
|
haftmann@21383
|
755 |
proof -
|
haftmann@21383
|
756 |
assume r: "!!x y. x <= y ==> f x <= f y"
|
haftmann@21383
|
757 |
assume "a <= f b"
|
haftmann@21383
|
758 |
also assume "b <= c" hence "f b <= f c" by (rule r)
|
haftmann@21383
|
759 |
finally (order_trans) show ?thesis .
|
haftmann@21383
|
760 |
qed
|
haftmann@21383
|
761 |
|
haftmann@21383
|
762 |
lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==>
|
haftmann@21383
|
763 |
(!!x y. x <= y ==> f x <= f y) ==> f a <= c"
|
haftmann@21383
|
764 |
proof -
|
haftmann@21383
|
765 |
assume r: "!!x y. x <= y ==> f x <= f y"
|
haftmann@21383
|
766 |
assume "a <= b" hence "f a <= f b" by (rule r)
|
haftmann@21383
|
767 |
also assume "f b <= c"
|
haftmann@21383
|
768 |
finally (order_trans) show ?thesis .
|
haftmann@21383
|
769 |
qed
|
haftmann@21383
|
770 |
|
haftmann@21383
|
771 |
lemma ord_le_eq_subst: "a <= b ==> f b = c ==>
|
haftmann@21383
|
772 |
(!!x y. x <= y ==> f x <= f y) ==> f a <= c"
|
haftmann@21383
|
773 |
proof -
|
haftmann@21383
|
774 |
assume r: "!!x y. x <= y ==> f x <= f y"
|
haftmann@21383
|
775 |
assume "a <= b" hence "f a <= f b" by (rule r)
|
haftmann@21383
|
776 |
also assume "f b = c"
|
haftmann@21383
|
777 |
finally (ord_le_eq_trans) show ?thesis .
|
haftmann@21383
|
778 |
qed
|
haftmann@21383
|
779 |
|
haftmann@21383
|
780 |
lemma ord_eq_le_subst: "a = f b ==> b <= c ==>
|
haftmann@21383
|
781 |
(!!x y. x <= y ==> f x <= f y) ==> a <= f c"
|
haftmann@21383
|
782 |
proof -
|
haftmann@21383
|
783 |
assume r: "!!x y. x <= y ==> f x <= f y"
|
haftmann@21383
|
784 |
assume "a = f b"
|
haftmann@21383
|
785 |
also assume "b <= c" hence "f b <= f c" by (rule r)
|
haftmann@21383
|
786 |
finally (ord_eq_le_trans) show ?thesis .
|
haftmann@21383
|
787 |
qed
|
haftmann@21383
|
788 |
|
haftmann@21383
|
789 |
lemma ord_less_eq_subst: "a < b ==> f b = c ==>
|
haftmann@21383
|
790 |
(!!x y. x < y ==> f x < f y) ==> f a < c"
|
haftmann@21383
|
791 |
proof -
|
haftmann@21383
|
792 |
assume r: "!!x y. x < y ==> f x < f y"
|
haftmann@21383
|
793 |
assume "a < b" hence "f a < f b" by (rule r)
|
haftmann@21383
|
794 |
also assume "f b = c"
|
haftmann@21383
|
795 |
finally (ord_less_eq_trans) show ?thesis .
|
haftmann@21383
|
796 |
qed
|
haftmann@21383
|
797 |
|
haftmann@21383
|
798 |
lemma ord_eq_less_subst: "a = f b ==> b < c ==>
|
haftmann@21383
|
799 |
(!!x y. x < y ==> f x < f y) ==> a < f c"
|
haftmann@21383
|
800 |
proof -
|
haftmann@21383
|
801 |
assume r: "!!x y. x < y ==> f x < f y"
|
haftmann@21383
|
802 |
assume "a = f b"
|
haftmann@21383
|
803 |
also assume "b < c" hence "f b < f c" by (rule r)
|
haftmann@21383
|
804 |
finally (ord_eq_less_trans) show ?thesis .
|
haftmann@21383
|
805 |
qed
|
haftmann@21383
|
806 |
|
haftmann@21383
|
807 |
text {*
|
haftmann@21383
|
808 |
Note that this list of rules is in reverse order of priorities.
|
haftmann@21383
|
809 |
*}
|
haftmann@21383
|
810 |
|
haftmann@27682
|
811 |
lemmas [trans] =
|
haftmann@21383
|
812 |
order_less_subst2
|
haftmann@21383
|
813 |
order_less_subst1
|
haftmann@21383
|
814 |
order_le_less_subst2
|
haftmann@21383
|
815 |
order_le_less_subst1
|
haftmann@21383
|
816 |
order_less_le_subst2
|
haftmann@21383
|
817 |
order_less_le_subst1
|
haftmann@21383
|
818 |
order_subst2
|
haftmann@21383
|
819 |
order_subst1
|
haftmann@21383
|
820 |
ord_le_eq_subst
|
haftmann@21383
|
821 |
ord_eq_le_subst
|
haftmann@21383
|
822 |
ord_less_eq_subst
|
haftmann@21383
|
823 |
ord_eq_less_subst
|
haftmann@21383
|
824 |
forw_subst
|
haftmann@21383
|
825 |
back_subst
|
haftmann@21383
|
826 |
rev_mp
|
haftmann@21383
|
827 |
mp
|
haftmann@27682
|
828 |
|
haftmann@27682
|
829 |
lemmas (in order) [trans] =
|
haftmann@27682
|
830 |
neq_le_trans
|
haftmann@27682
|
831 |
le_neq_trans
|
haftmann@27682
|
832 |
|
haftmann@27682
|
833 |
lemmas (in preorder) [trans] =
|
haftmann@27682
|
834 |
less_trans
|
haftmann@27682
|
835 |
less_asym'
|
haftmann@27682
|
836 |
le_less_trans
|
haftmann@27682
|
837 |
less_le_trans
|
haftmann@21383
|
838 |
order_trans
|
haftmann@27682
|
839 |
|
haftmann@27682
|
840 |
lemmas (in order) [trans] =
|
haftmann@27682
|
841 |
antisym
|
haftmann@27682
|
842 |
|
haftmann@27682
|
843 |
lemmas (in ord) [trans] =
|
haftmann@27682
|
844 |
ord_le_eq_trans
|
haftmann@27682
|
845 |
ord_eq_le_trans
|
haftmann@27682
|
846 |
ord_less_eq_trans
|
haftmann@27682
|
847 |
ord_eq_less_trans
|
haftmann@27682
|
848 |
|
haftmann@27682
|
849 |
lemmas [trans] =
|
haftmann@27682
|
850 |
trans
|
haftmann@27682
|
851 |
|
haftmann@27682
|
852 |
lemmas order_trans_rules =
|
haftmann@27682
|
853 |
order_less_subst2
|
haftmann@27682
|
854 |
order_less_subst1
|
haftmann@27682
|
855 |
order_le_less_subst2
|
haftmann@27682
|
856 |
order_le_less_subst1
|
haftmann@27682
|
857 |
order_less_le_subst2
|
haftmann@27682
|
858 |
order_less_le_subst1
|
haftmann@27682
|
859 |
order_subst2
|
haftmann@27682
|
860 |
order_subst1
|
haftmann@27682
|
861 |
ord_le_eq_subst
|
haftmann@27682
|
862 |
ord_eq_le_subst
|
haftmann@27682
|
863 |
ord_less_eq_subst
|
haftmann@27682
|
864 |
ord_eq_less_subst
|
haftmann@27682
|
865 |
forw_subst
|
haftmann@27682
|
866 |
back_subst
|
haftmann@27682
|
867 |
rev_mp
|
haftmann@27682
|
868 |
mp
|
haftmann@27682
|
869 |
neq_le_trans
|
haftmann@27682
|
870 |
le_neq_trans
|
haftmann@27682
|
871 |
less_trans
|
haftmann@27682
|
872 |
less_asym'
|
haftmann@27682
|
873 |
le_less_trans
|
haftmann@27682
|
874 |
less_le_trans
|
haftmann@27682
|
875 |
order_trans
|
haftmann@27682
|
876 |
antisym
|
haftmann@21383
|
877 |
ord_le_eq_trans
|
haftmann@21383
|
878 |
ord_eq_le_trans
|
haftmann@21383
|
879 |
ord_less_eq_trans
|
haftmann@21383
|
880 |
ord_eq_less_trans
|
haftmann@21383
|
881 |
trans
|
haftmann@21383
|
882 |
|
avigad@17012
|
883 |
text {* These support proving chains of decreasing inequalities
|
avigad@17012
|
884 |
a >= b >= c ... in Isar proofs. *}
|
avigad@17012
|
885 |
|
haftmann@21083
|
886 |
lemma xt1:
|
haftmann@21083
|
887 |
"a = b ==> b > c ==> a > c"
|
haftmann@21083
|
888 |
"a > b ==> b = c ==> a > c"
|
haftmann@21083
|
889 |
"a = b ==> b >= c ==> a >= c"
|
haftmann@21083
|
890 |
"a >= b ==> b = c ==> a >= c"
|
haftmann@21083
|
891 |
"(x::'a::order) >= y ==> y >= x ==> x = y"
|
haftmann@21083
|
892 |
"(x::'a::order) >= y ==> y >= z ==> x >= z"
|
haftmann@21083
|
893 |
"(x::'a::order) > y ==> y >= z ==> x > z"
|
haftmann@21083
|
894 |
"(x::'a::order) >= y ==> y > z ==> x > z"
|
wenzelm@23417
|
895 |
"(a::'a::order) > b ==> b > a ==> P"
|
haftmann@21083
|
896 |
"(x::'a::order) > y ==> y > z ==> x > z"
|
haftmann@21083
|
897 |
"(a::'a::order) >= b ==> a ~= b ==> a > b"
|
haftmann@21083
|
898 |
"(a::'a::order) ~= b ==> a >= b ==> a > b"
|
haftmann@21083
|
899 |
"a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c"
|
haftmann@21083
|
900 |
"a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c"
|
haftmann@21083
|
901 |
"a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
|
haftmann@21083
|
902 |
"a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c"
|
haftmann@25076
|
903 |
by auto
|
avigad@17012
|
904 |
|
haftmann@21083
|
905 |
lemma xt2:
|
haftmann@21083
|
906 |
"(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c"
|
avigad@17012
|
907 |
by (subgoal_tac "f b >= f c", force, force)
|
avigad@17012
|
908 |
|
haftmann@21083
|
909 |
lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==>
|
avigad@17012
|
910 |
(!!x y. x >= y ==> f x >= f y) ==> f a >= c"
|
avigad@17012
|
911 |
by (subgoal_tac "f a >= f b", force, force)
|
avigad@17012
|
912 |
|
haftmann@21083
|
913 |
lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==>
|
avigad@17012
|
914 |
(!!x y. x >= y ==> f x >= f y) ==> a > f c"
|
avigad@17012
|
915 |
by (subgoal_tac "f b >= f c", force, force)
|
avigad@17012
|
916 |
|
haftmann@21083
|
917 |
lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==>
|
avigad@17012
|
918 |
(!!x y. x > y ==> f x > f y) ==> f a > c"
|
avigad@17012
|
919 |
by (subgoal_tac "f a > f b", force, force)
|
avigad@17012
|
920 |
|
haftmann@21083
|
921 |
lemma xt6: "(a::'a::order) >= f b ==> b > c ==>
|
avigad@17012
|
922 |
(!!x y. x > y ==> f x > f y) ==> a > f c"
|
avigad@17012
|
923 |
by (subgoal_tac "f b > f c", force, force)
|
avigad@17012
|
924 |
|
haftmann@21083
|
925 |
lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==>
|
avigad@17012
|
926 |
(!!x y. x >= y ==> f x >= f y) ==> f a > c"
|
avigad@17012
|
927 |
by (subgoal_tac "f a >= f b", force, force)
|
avigad@17012
|
928 |
|
haftmann@21083
|
929 |
lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==>
|
avigad@17012
|
930 |
(!!x y. x > y ==> f x > f y) ==> a > f c"
|
avigad@17012
|
931 |
by (subgoal_tac "f b > f c", force, force)
|
avigad@17012
|
932 |
|
haftmann@21083
|
933 |
lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==>
|
avigad@17012
|
934 |
(!!x y. x > y ==> f x > f y) ==> f a > c"
|
avigad@17012
|
935 |
by (subgoal_tac "f a > f b", force, force)
|
avigad@17012
|
936 |
|
haftmann@21083
|
937 |
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
|
avigad@17012
|
938 |
|
avigad@17012
|
939 |
(*
|
avigad@17012
|
940 |
Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
|
avigad@17012
|
941 |
for the wrong thing in an Isar proof.
|
avigad@17012
|
942 |
|
avigad@17012
|
943 |
The extra transitivity rules can be used as follows:
|
avigad@17012
|
944 |
|
avigad@17012
|
945 |
lemma "(a::'a::order) > z"
|
avigad@17012
|
946 |
proof -
|
avigad@17012
|
947 |
have "a >= b" (is "_ >= ?rhs")
|
avigad@17012
|
948 |
sorry
|
avigad@17012
|
949 |
also have "?rhs >= c" (is "_ >= ?rhs")
|
avigad@17012
|
950 |
sorry
|
avigad@17012
|
951 |
also (xtrans) have "?rhs = d" (is "_ = ?rhs")
|
avigad@17012
|
952 |
sorry
|
avigad@17012
|
953 |
also (xtrans) have "?rhs >= e" (is "_ >= ?rhs")
|
avigad@17012
|
954 |
sorry
|
avigad@17012
|
955 |
also (xtrans) have "?rhs > f" (is "_ > ?rhs")
|
avigad@17012
|
956 |
sorry
|
avigad@17012
|
957 |
also (xtrans) have "?rhs > z"
|
avigad@17012
|
958 |
sorry
|
avigad@17012
|
959 |
finally (xtrans) show ?thesis .
|
avigad@17012
|
960 |
qed
|
avigad@17012
|
961 |
|
avigad@17012
|
962 |
Alternatively, one can use "declare xtrans [trans]" and then
|
avigad@17012
|
963 |
leave out the "(xtrans)" above.
|
avigad@17012
|
964 |
*)
|
avigad@17012
|
965 |
|
haftmann@23881
|
966 |
|
haftmann@23881
|
967 |
subsection {* Monotonicity, least value operator and min/max *}
|
haftmann@21083
|
968 |
|
haftmann@25076
|
969 |
context order
|
haftmann@25076
|
970 |
begin
|
haftmann@21216
|
971 |
|
haftmann@30298
|
972 |
definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
|
haftmann@25076
|
973 |
"mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
|
haftmann@25076
|
974 |
|
haftmann@25076
|
975 |
lemma monoI [intro?]:
|
haftmann@25076
|
976 |
fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
|
haftmann@25076
|
977 |
shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
|
haftmann@25076
|
978 |
unfolding mono_def by iprover
|
haftmann@25076
|
979 |
|
haftmann@25076
|
980 |
lemma monoD [dest?]:
|
haftmann@25076
|
981 |
fixes f :: "'a \<Rightarrow> 'b\<Colon>order"
|
haftmann@25076
|
982 |
shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
|
haftmann@25076
|
983 |
unfolding mono_def by iprover
|
haftmann@25076
|
984 |
|
haftmann@30298
|
985 |
definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where
|
haftmann@30298
|
986 |
"strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
|
haftmann@30298
|
987 |
|
haftmann@30298
|
988 |
lemma strict_monoI [intro?]:
|
haftmann@30298
|
989 |
assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
|
haftmann@30298
|
990 |
shows "strict_mono f"
|
haftmann@30298
|
991 |
using assms unfolding strict_mono_def by auto
|
haftmann@30298
|
992 |
|
haftmann@30298
|
993 |
lemma strict_monoD [dest?]:
|
haftmann@30298
|
994 |
"strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
|
haftmann@30298
|
995 |
unfolding strict_mono_def by auto
|
haftmann@30298
|
996 |
|
haftmann@30298
|
997 |
lemma strict_mono_mono [dest?]:
|
haftmann@30298
|
998 |
assumes "strict_mono f"
|
haftmann@30298
|
999 |
shows "mono f"
|
haftmann@30298
|
1000 |
proof (rule monoI)
|
haftmann@30298
|
1001 |
fix x y
|
haftmann@30298
|
1002 |
assume "x \<le> y"
|
haftmann@30298
|
1003 |
show "f x \<le> f y"
|
haftmann@30298
|
1004 |
proof (cases "x = y")
|
haftmann@30298
|
1005 |
case True then show ?thesis by simp
|
haftmann@30298
|
1006 |
next
|
haftmann@30298
|
1007 |
case False with `x \<le> y` have "x < y" by simp
|
haftmann@30298
|
1008 |
with assms strict_monoD have "f x < f y" by auto
|
haftmann@30298
|
1009 |
then show ?thesis by simp
|
haftmann@30298
|
1010 |
qed
|
haftmann@30298
|
1011 |
qed
|
haftmann@30298
|
1012 |
|
haftmann@25076
|
1013 |
end
|
haftmann@25076
|
1014 |
|
haftmann@25076
|
1015 |
context linorder
|
haftmann@25076
|
1016 |
begin
|
haftmann@25076
|
1017 |
|
haftmann@30298
|
1018 |
lemma strict_mono_eq:
|
haftmann@30298
|
1019 |
assumes "strict_mono f"
|
haftmann@30298
|
1020 |
shows "f x = f y \<longleftrightarrow> x = y"
|
haftmann@30298
|
1021 |
proof
|
haftmann@30298
|
1022 |
assume "f x = f y"
|
haftmann@30298
|
1023 |
show "x = y" proof (cases x y rule: linorder_cases)
|
haftmann@30298
|
1024 |
case less with assms strict_monoD have "f x < f y" by auto
|
haftmann@30298
|
1025 |
with `f x = f y` show ?thesis by simp
|
haftmann@30298
|
1026 |
next
|
haftmann@30298
|
1027 |
case equal then show ?thesis .
|
haftmann@30298
|
1028 |
next
|
haftmann@30298
|
1029 |
case greater with assms strict_monoD have "f y < f x" by auto
|
haftmann@30298
|
1030 |
with `f x = f y` show ?thesis by simp
|
haftmann@30298
|
1031 |
qed
|
haftmann@30298
|
1032 |
qed simp
|
haftmann@30298
|
1033 |
|
haftmann@30298
|
1034 |
lemma strict_mono_less_eq:
|
haftmann@30298
|
1035 |
assumes "strict_mono f"
|
haftmann@30298
|
1036 |
shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
|
haftmann@30298
|
1037 |
proof
|
haftmann@30298
|
1038 |
assume "x \<le> y"
|
haftmann@30298
|
1039 |
with assms strict_mono_mono monoD show "f x \<le> f y" by auto
|
haftmann@30298
|
1040 |
next
|
haftmann@30298
|
1041 |
assume "f x \<le> f y"
|
haftmann@30298
|
1042 |
show "x \<le> y" proof (rule ccontr)
|
haftmann@30298
|
1043 |
assume "\<not> x \<le> y" then have "y < x" by simp
|
haftmann@30298
|
1044 |
with assms strict_monoD have "f y < f x" by auto
|
haftmann@30298
|
1045 |
with `f x \<le> f y` show False by simp
|
haftmann@30298
|
1046 |
qed
|
haftmann@30298
|
1047 |
qed
|
haftmann@30298
|
1048 |
|
haftmann@30298
|
1049 |
lemma strict_mono_less:
|
haftmann@30298
|
1050 |
assumes "strict_mono f"
|
haftmann@30298
|
1051 |
shows "f x < f y \<longleftrightarrow> x < y"
|
haftmann@30298
|
1052 |
using assms
|
haftmann@30298
|
1053 |
by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
|
haftmann@30298
|
1054 |
|
haftmann@25076
|
1055 |
lemma min_of_mono:
|
haftmann@25076
|
1056 |
fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
|
wenzelm@25377
|
1057 |
shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
|
haftmann@25076
|
1058 |
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
|
haftmann@25076
|
1059 |
|
haftmann@25076
|
1060 |
lemma max_of_mono:
|
haftmann@25076
|
1061 |
fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder"
|
wenzelm@25377
|
1062 |
shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
|
haftmann@25076
|
1063 |
by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
|
haftmann@25076
|
1064 |
|
haftmann@25076
|
1065 |
end
|
haftmann@21083
|
1066 |
|
haftmann@21383
|
1067 |
lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
|
nipkow@23212
|
1068 |
by (simp add: min_def)
|
haftmann@21383
|
1069 |
|
haftmann@21383
|
1070 |
lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
|
nipkow@23212
|
1071 |
by (simp add: max_def)
|
haftmann@21383
|
1072 |
|
haftmann@21383
|
1073 |
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
|
nipkow@23212
|
1074 |
apply (simp add: min_def)
|
haftmann@34245
|
1075 |
apply (blast intro: antisym)
|
nipkow@23212
|
1076 |
done
|
haftmann@21383
|
1077 |
|
haftmann@21383
|
1078 |
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
|
nipkow@23212
|
1079 |
apply (simp add: max_def)
|
haftmann@34245
|
1080 |
apply (blast intro: antisym)
|
nipkow@23212
|
1081 |
done
|
haftmann@21383
|
1082 |
|
haftmann@27823
|
1083 |
|
haftmann@28685
|
1084 |
subsection {* Top and bottom elements *}
|
haftmann@28685
|
1085 |
|
haftmann@41330
|
1086 |
class bot = preorder +
|
haftmann@41330
|
1087 |
fixes bot :: 'a
|
haftmann@41330
|
1088 |
assumes bot_least [simp]: "bot \<le> x"
|
haftmann@41330
|
1089 |
|
haftmann@28685
|
1090 |
class top = preorder +
|
haftmann@28685
|
1091 |
fixes top :: 'a
|
haftmann@28685
|
1092 |
assumes top_greatest [simp]: "x \<le> top"
|
haftmann@28685
|
1093 |
|
haftmann@28685
|
1094 |
|
haftmann@27823
|
1095 |
subsection {* Dense orders *}
|
haftmann@27823
|
1096 |
|
haftmann@35028
|
1097 |
class dense_linorder = linorder +
|
haftmann@27823
|
1098 |
assumes gt_ex: "\<exists>y. x < y"
|
haftmann@27823
|
1099 |
and lt_ex: "\<exists>y. y < x"
|
haftmann@27823
|
1100 |
and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
|
hoelzl@35579
|
1101 |
begin
|
haftmann@27823
|
1102 |
|
hoelzl@35579
|
1103 |
lemma dense_le:
|
hoelzl@35579
|
1104 |
fixes y z :: 'a
|
hoelzl@35579
|
1105 |
assumes "\<And>x. x < y \<Longrightarrow> x \<le> z"
|
hoelzl@35579
|
1106 |
shows "y \<le> z"
|
hoelzl@35579
|
1107 |
proof (rule ccontr)
|
hoelzl@35579
|
1108 |
assume "\<not> ?thesis"
|
hoelzl@35579
|
1109 |
hence "z < y" by simp
|
hoelzl@35579
|
1110 |
from dense[OF this]
|
hoelzl@35579
|
1111 |
obtain x where "x < y" and "z < x" by safe
|
hoelzl@35579
|
1112 |
moreover have "x \<le> z" using assms[OF `x < y`] .
|
hoelzl@35579
|
1113 |
ultimately show False by auto
|
hoelzl@35579
|
1114 |
qed
|
hoelzl@35579
|
1115 |
|
hoelzl@35579
|
1116 |
lemma dense_le_bounded:
|
hoelzl@35579
|
1117 |
fixes x y z :: 'a
|
hoelzl@35579
|
1118 |
assumes "x < y"
|
hoelzl@35579
|
1119 |
assumes *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z"
|
hoelzl@35579
|
1120 |
shows "y \<le> z"
|
hoelzl@35579
|
1121 |
proof (rule dense_le)
|
hoelzl@35579
|
1122 |
fix w assume "w < y"
|
hoelzl@35579
|
1123 |
from dense[OF `x < y`] obtain u where "x < u" "u < y" by safe
|
hoelzl@35579
|
1124 |
from linear[of u w]
|
hoelzl@35579
|
1125 |
show "w \<le> z"
|
hoelzl@35579
|
1126 |
proof (rule disjE)
|
hoelzl@35579
|
1127 |
assume "u \<le> w"
|
hoelzl@35579
|
1128 |
from less_le_trans[OF `x < u` `u \<le> w`] `w < y`
|
hoelzl@35579
|
1129 |
show "w \<le> z" by (rule *)
|
hoelzl@35579
|
1130 |
next
|
hoelzl@35579
|
1131 |
assume "w \<le> u"
|
hoelzl@35579
|
1132 |
from `w \<le> u` *[OF `x < u` `u < y`]
|
hoelzl@35579
|
1133 |
show "w \<le> z" by (rule order_trans)
|
hoelzl@35579
|
1134 |
qed
|
hoelzl@35579
|
1135 |
qed
|
hoelzl@35579
|
1136 |
|
hoelzl@35579
|
1137 |
end
|
haftmann@27823
|
1138 |
|
haftmann@27823
|
1139 |
subsection {* Wellorders *}
|
haftmann@27823
|
1140 |
|
haftmann@27823
|
1141 |
class wellorder = linorder +
|
haftmann@27823
|
1142 |
assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a"
|
haftmann@27823
|
1143 |
begin
|
haftmann@27823
|
1144 |
|
haftmann@27823
|
1145 |
lemma wellorder_Least_lemma:
|
haftmann@27823
|
1146 |
fixes k :: 'a
|
haftmann@27823
|
1147 |
assumes "P k"
|
haftmann@34245
|
1148 |
shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k"
|
haftmann@27823
|
1149 |
proof -
|
haftmann@27823
|
1150 |
have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k"
|
haftmann@27823
|
1151 |
using assms proof (induct k rule: less_induct)
|
haftmann@27823
|
1152 |
case (less x) then have "P x" by simp
|
haftmann@27823
|
1153 |
show ?case proof (rule classical)
|
haftmann@27823
|
1154 |
assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)"
|
haftmann@27823
|
1155 |
have "\<And>y. P y \<Longrightarrow> x \<le> y"
|
haftmann@27823
|
1156 |
proof (rule classical)
|
haftmann@27823
|
1157 |
fix y
|
hoelzl@38943
|
1158 |
assume "P y" and "\<not> x \<le> y"
|
haftmann@27823
|
1159 |
with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
|
haftmann@27823
|
1160 |
by (auto simp add: not_le)
|
haftmann@27823
|
1161 |
with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y"
|
haftmann@27823
|
1162 |
by auto
|
haftmann@27823
|
1163 |
then show "x \<le> y" by auto
|
haftmann@27823
|
1164 |
qed
|
haftmann@27823
|
1165 |
with `P x` have Least: "(LEAST a. P a) = x"
|
haftmann@27823
|
1166 |
by (rule Least_equality)
|
haftmann@27823
|
1167 |
with `P x` show ?thesis by simp
|
haftmann@27823
|
1168 |
qed
|
haftmann@27823
|
1169 |
qed
|
haftmann@27823
|
1170 |
then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto
|
haftmann@27823
|
1171 |
qed
|
haftmann@27823
|
1172 |
|
haftmann@27823
|
1173 |
-- "The following 3 lemmas are due to Brian Huffman"
|
haftmann@27823
|
1174 |
lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)"
|
haftmann@27823
|
1175 |
by (erule exE) (erule LeastI)
|
haftmann@27823
|
1176 |
|
haftmann@27823
|
1177 |
lemma LeastI2:
|
haftmann@27823
|
1178 |
"P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
|
haftmann@27823
|
1179 |
by (blast intro: LeastI)
|
haftmann@27823
|
1180 |
|
haftmann@27823
|
1181 |
lemma LeastI2_ex:
|
haftmann@27823
|
1182 |
"\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)"
|
haftmann@27823
|
1183 |
by (blast intro: LeastI_ex)
|
haftmann@27823
|
1184 |
|
hoelzl@38943
|
1185 |
lemma LeastI2_wellorder:
|
hoelzl@38943
|
1186 |
assumes "P a"
|
hoelzl@38943
|
1187 |
and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
|
hoelzl@38943
|
1188 |
shows "Q (Least P)"
|
hoelzl@38943
|
1189 |
proof (rule LeastI2_order)
|
hoelzl@38943
|
1190 |
show "P (Least P)" using `P a` by (rule LeastI)
|
hoelzl@38943
|
1191 |
next
|
hoelzl@38943
|
1192 |
fix y assume "P y" thus "Least P \<le> y" by (rule Least_le)
|
hoelzl@38943
|
1193 |
next
|
hoelzl@38943
|
1194 |
fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2))
|
hoelzl@38943
|
1195 |
qed
|
hoelzl@38943
|
1196 |
|
haftmann@27823
|
1197 |
lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k"
|
haftmann@27823
|
1198 |
apply (simp (no_asm_use) add: not_le [symmetric])
|
haftmann@27823
|
1199 |
apply (erule contrapos_nn)
|
haftmann@27823
|
1200 |
apply (erule Least_le)
|
haftmann@27823
|
1201 |
done
|
haftmann@27823
|
1202 |
|
hoelzl@38943
|
1203 |
end
|
haftmann@27823
|
1204 |
|
haftmann@28685
|
1205 |
|
haftmann@28685
|
1206 |
subsection {* Order on bool *}
|
haftmann@28685
|
1207 |
|
haftmann@41330
|
1208 |
instantiation bool :: "{order, bot, top}"
|
haftmann@28685
|
1209 |
begin
|
haftmann@28685
|
1210 |
|
haftmann@28685
|
1211 |
definition
|
haftmann@41328
|
1212 |
le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
|
haftmann@28685
|
1213 |
|
haftmann@28685
|
1214 |
definition
|
haftmann@41328
|
1215 |
[simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
|
haftmann@28685
|
1216 |
|
haftmann@28685
|
1217 |
definition
|
haftmann@41330
|
1218 |
[simp]: "bot \<longleftrightarrow> False"
|
haftmann@28685
|
1219 |
|
haftmann@28685
|
1220 |
definition
|
haftmann@41330
|
1221 |
[simp]: "top \<longleftrightarrow> True"
|
haftmann@28685
|
1222 |
|
haftmann@28685
|
1223 |
instance proof
|
haftmann@41328
|
1224 |
qed auto
|
haftmann@28685
|
1225 |
|
nipkow@15524
|
1226 |
end
|
haftmann@28685
|
1227 |
|
haftmann@28685
|
1228 |
lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
|
haftmann@41328
|
1229 |
by simp
|
haftmann@28685
|
1230 |
|
haftmann@28685
|
1231 |
lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
|
haftmann@41328
|
1232 |
by simp
|
haftmann@28685
|
1233 |
|
haftmann@28685
|
1234 |
lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
|
haftmann@41328
|
1235 |
by simp
|
haftmann@28685
|
1236 |
|
haftmann@28685
|
1237 |
lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
|
haftmann@41328
|
1238 |
by simp
|
haftmann@32899
|
1239 |
|
haftmann@32899
|
1240 |
lemma bot_boolE: "bot \<Longrightarrow> P"
|
haftmann@41328
|
1241 |
by simp
|
haftmann@32899
|
1242 |
|
haftmann@32899
|
1243 |
lemma top_boolI: top
|
haftmann@41328
|
1244 |
by simp
|
haftmann@28685
|
1245 |
|
haftmann@28685
|
1246 |
lemma [code]:
|
haftmann@28685
|
1247 |
"False \<le> b \<longleftrightarrow> True"
|
haftmann@28685
|
1248 |
"True \<le> b \<longleftrightarrow> b"
|
haftmann@28685
|
1249 |
"False < b \<longleftrightarrow> b"
|
haftmann@28685
|
1250 |
"True < b \<longleftrightarrow> False"
|
haftmann@41328
|
1251 |
by simp_all
|
haftmann@28685
|
1252 |
|
haftmann@28685
|
1253 |
|
haftmann@28685
|
1254 |
subsection {* Order on functions *}
|
haftmann@28685
|
1255 |
|
haftmann@28685
|
1256 |
instantiation "fun" :: (type, ord) ord
|
haftmann@28685
|
1257 |
begin
|
haftmann@28685
|
1258 |
|
haftmann@28685
|
1259 |
definition
|
haftmann@37767
|
1260 |
le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
|
haftmann@28685
|
1261 |
|
haftmann@28685
|
1262 |
definition
|
haftmann@41328
|
1263 |
"(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
|
haftmann@28685
|
1264 |
|
haftmann@28685
|
1265 |
instance ..
|
haftmann@28685
|
1266 |
|
haftmann@28685
|
1267 |
end
|
haftmann@28685
|
1268 |
|
haftmann@28685
|
1269 |
instance "fun" :: (type, preorder) preorder proof
|
haftmann@28685
|
1270 |
qed (auto simp add: le_fun_def less_fun_def
|
haftmann@34245
|
1271 |
intro: order_trans antisym intro!: ext)
|
haftmann@28685
|
1272 |
|
haftmann@28685
|
1273 |
instance "fun" :: (type, order) order proof
|
haftmann@34245
|
1274 |
qed (auto simp add: le_fun_def intro: antisym ext)
|
haftmann@28685
|
1275 |
|
haftmann@41330
|
1276 |
instantiation "fun" :: (type, bot) bot
|
haftmann@41330
|
1277 |
begin
|
haftmann@41330
|
1278 |
|
haftmann@41330
|
1279 |
definition
|
haftmann@41330
|
1280 |
"bot = (\<lambda>x. bot)"
|
haftmann@41330
|
1281 |
|
haftmann@41330
|
1282 |
lemma bot_apply:
|
haftmann@41330
|
1283 |
"bot x = bot"
|
haftmann@41330
|
1284 |
by (simp add: bot_fun_def)
|
haftmann@41330
|
1285 |
|
haftmann@41330
|
1286 |
instance proof
|
haftmann@41330
|
1287 |
qed (simp add: le_fun_def bot_apply)
|
haftmann@41330
|
1288 |
|
haftmann@41330
|
1289 |
end
|
haftmann@41330
|
1290 |
|
haftmann@28685
|
1291 |
instantiation "fun" :: (type, top) top
|
haftmann@28685
|
1292 |
begin
|
haftmann@28685
|
1293 |
|
haftmann@28685
|
1294 |
definition
|
haftmann@41328
|
1295 |
[no_atp]: "top = (\<lambda>x. top)"
|
haftmann@41323
|
1296 |
declare top_fun_def_raw [no_atp]
|
haftmann@28685
|
1297 |
|
haftmann@41328
|
1298 |
lemma top_apply:
|
haftmann@41328
|
1299 |
"top x = top"
|
haftmann@41328
|
1300 |
by (simp add: top_fun_def)
|
haftmann@41328
|
1301 |
|
haftmann@28685
|
1302 |
instance proof
|
haftmann@41328
|
1303 |
qed (simp add: le_fun_def top_apply)
|
haftmann@28685
|
1304 |
|
haftmann@28685
|
1305 |
end
|
haftmann@28685
|
1306 |
|
haftmann@28685
|
1307 |
lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
|
haftmann@28685
|
1308 |
unfolding le_fun_def by simp
|
haftmann@28685
|
1309 |
|
haftmann@28685
|
1310 |
lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
|
haftmann@28685
|
1311 |
unfolding le_fun_def by simp
|
haftmann@28685
|
1312 |
|
haftmann@28685
|
1313 |
lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
|
haftmann@28685
|
1314 |
unfolding le_fun_def by simp
|
haftmann@28685
|
1315 |
|
haftmann@34245
|
1316 |
|
haftmann@34245
|
1317 |
subsection {* Name duplicates *}
|
haftmann@34245
|
1318 |
|
haftmann@34245
|
1319 |
lemmas order_eq_refl = preorder_class.eq_refl
|
haftmann@34245
|
1320 |
lemmas order_less_irrefl = preorder_class.less_irrefl
|
haftmann@34245
|
1321 |
lemmas order_less_imp_le = preorder_class.less_imp_le
|
haftmann@34245
|
1322 |
lemmas order_less_not_sym = preorder_class.less_not_sym
|
haftmann@34245
|
1323 |
lemmas order_less_asym = preorder_class.less_asym
|
haftmann@34245
|
1324 |
lemmas order_less_trans = preorder_class.less_trans
|
haftmann@34245
|
1325 |
lemmas order_le_less_trans = preorder_class.le_less_trans
|
haftmann@34245
|
1326 |
lemmas order_less_le_trans = preorder_class.less_le_trans
|
haftmann@34245
|
1327 |
lemmas order_less_imp_not_less = preorder_class.less_imp_not_less
|
haftmann@34245
|
1328 |
lemmas order_less_imp_triv = preorder_class.less_imp_triv
|
haftmann@34245
|
1329 |
lemmas order_less_asym' = preorder_class.less_asym'
|
haftmann@34245
|
1330 |
|
haftmann@34245
|
1331 |
lemmas order_less_le = order_class.less_le
|
haftmann@34245
|
1332 |
lemmas order_le_less = order_class.le_less
|
haftmann@34245
|
1333 |
lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq
|
haftmann@34245
|
1334 |
lemmas order_less_imp_not_eq = order_class.less_imp_not_eq
|
haftmann@34245
|
1335 |
lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
|
haftmann@34245
|
1336 |
lemmas order_neq_le_trans = order_class.neq_le_trans
|
haftmann@34245
|
1337 |
lemmas order_le_neq_trans = order_class.le_neq_trans
|
haftmann@34245
|
1338 |
lemmas order_antisym = order_class.antisym
|
haftmann@34245
|
1339 |
lemmas order_eq_iff = order_class.eq_iff
|
haftmann@34245
|
1340 |
lemmas order_antisym_conv = order_class.antisym_conv
|
haftmann@34245
|
1341 |
|
haftmann@34245
|
1342 |
lemmas linorder_linear = linorder_class.linear
|
haftmann@34245
|
1343 |
lemmas linorder_less_linear = linorder_class.less_linear
|
haftmann@34245
|
1344 |
lemmas linorder_le_less_linear = linorder_class.le_less_linear
|
haftmann@34245
|
1345 |
lemmas linorder_le_cases = linorder_class.le_cases
|
haftmann@34245
|
1346 |
lemmas linorder_not_less = linorder_class.not_less
|
haftmann@34245
|
1347 |
lemmas linorder_not_le = linorder_class.not_le
|
haftmann@34245
|
1348 |
lemmas linorder_neq_iff = linorder_class.neq_iff
|
haftmann@34245
|
1349 |
lemmas linorder_neqE = linorder_class.neqE
|
haftmann@34245
|
1350 |
lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
|
haftmann@34245
|
1351 |
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
|
haftmann@34245
|
1352 |
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
|
haftmann@34245
|
1353 |
|
haftmann@28685
|
1354 |
end
|