author  wenzelm 
Thu, 09 Nov 2006 11:58:13 +0100  
changeset 21259  63ab016c99ca 
parent 21248  3fd22b0939ff 
child 21329  7338206d75f1 
permissions  rwrr 
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 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

9 
imports Code_Generator 
15524  10 
begin 
11 

21083  12 
section {* Abstract orderings *} 
13 

14 
subsection {* Order signatures *} 

15524  15 

21194  16 
class ord = 
20588  17 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
21204  18 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
19 
begin 

20 

21 
notation 

22 
less_eq ("op \<^loc><=") 

21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

23 
less_eq ("(_/ \<^loc><= _)" [51, 51] 50) 
21204  24 
less ("op \<^loc><") 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

25 
less ("(_/ \<^loc>< _)" [51, 51] 50) 
21204  26 

27 
notation (xsymbols) 

28 
less_eq ("op \<^loc>\<le>") 

21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

29 
less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50) 
15524  30 

21204  31 
notation (HTML output) 
32 
less_eq ("op \<^loc>\<le>") 

21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

33 
less_eq ("(_/ \<^loc>\<le> _)" [51, 51] 50) 
21204  34 

35 
abbreviation (input) 

36 
greater (infix "\<^loc>>" 50) 

37 
"x \<^loc>> y \<equiv> y \<^loc>< x" 

38 
greater_eq (infix "\<^loc>>=" 50) 

39 
"x \<^loc>>= y \<equiv> y \<^loc><= x" 

40 

41 
notation (xsymbols) 

21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

42 
greater_eq (infix "\<^loc>\<ge>" 50) 
21204  43 

44 
end 

45 

46 
notation 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

47 
less_eq ("op <=") 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

48 
less_eq ("(_/ <= _)" [51, 51] 50) 
21204  49 
less ("op <") 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

50 
less ("(_/ < _)" [51, 51] 50) 
21204  51 

52 
notation (xsymbols) 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

53 
less_eq ("op \<le>") 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

54 
less_eq ("(_/ \<le> _)" [51, 51] 50) 
15524  55 

21204  56 
notation (HTML output) 
57 
less_eq ("op \<le>") 

21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

58 
less_eq ("(_/ \<le> _)" [51, 51] 50) 
20714  59 

19536  60 
abbreviation (input) 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

61 
greater (infix ">" 50) 
20714  62 
"x > y \<equiv> y < x" 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

63 
greater_eq (infix ">=" 50) 
20714  64 
"x >= y \<equiv> y <= x" 
65 

21204  66 
notation (xsymbols) 
21259
63ab016c99ca
modified less/less_eq syntax to avoid "x < y < z" etc.;
wenzelm
parents:
21248
diff
changeset

67 
greater_eq (infix "\<ge>" 50) 
15524  68 

69 

21083  70 
subsection {* Partial orderings *} 
15524  71 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

72 
locale partial_order = 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

73 
fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50) 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

74 
fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50) 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

75 
assumes refl [iff]: "x \<sqsubseteq> x" 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

76 
and trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

77 
and antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y" 
21248  78 
and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y" 
79 
begin 

80 

81 
abbreviation (input) 

82 
greater_eq (infixl "\<sqsupseteq>" 50) 

83 
"x \<sqsupseteq> y \<equiv> y \<sqsubseteq> x" 

84 

85 
abbreviation (input) 

86 
greater (infixl "\<sqsupset>" 50) 

87 
"x \<sqsupset> y \<equiv> y \<sqsubset> x" 

88 

89 
end 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

90 

15524  91 
axclass order < ord 
92 
order_refl [iff]: "x <= x" 

93 
order_trans: "x <= y ==> y <= z ==> x <= z" 

94 
order_antisym: "x <= y ==> y <= x ==> x = y" 

95 
order_less_le: "(x < y) = (x <= y & x ~= y)" 

96 

15837  97 
interpretation order: 
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

98 
partial_order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"] 
15524  99 
apply(rule partial_order.intro) 
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

100 
apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym, rule order_less_le) 
15524  101 
done 
102 

21248  103 
context partial_order 
104 
begin 

105 

15524  106 
text {* Reflexivity. *} 
107 

21248  108 
lemma eq_refl: "x = y \<Longrightarrow> x \<sqsubseteq> y" 
15524  109 
 {* This form is useful with the classical reasoner. *} 
21248  110 
by (erule ssubst) (rule refl) 
15524  111 

21248  112 
lemma less_irrefl [iff]: "\<not> x \<sqsubset> x" 
113 
by (simp add: less_le) 

15524  114 

21248  115 
lemma le_less: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubset> y \<or> x = y" 
15524  116 
 {* NOT suitable for iff, since it can cause PROOF FAILED. *} 
21248  117 
by (simp add: less_le) blast 
15524  118 

21248  119 
lemma le_imp_less_or_eq: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubset> y \<or> x = y" 
120 
unfolding less_le by blast 

15524  121 

21248  122 
lemma less_imp_le: "x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y" 
123 
unfolding less_le by blast 

124 

15524  125 

126 
text {* Asymmetry. *} 

127 

21248  128 
lemma less_not_sym: "x \<sqsubset> y \<Longrightarrow> \<not> (y \<sqsubset> x)" 
129 
by (simp add: less_le antisym) 

15524  130 

21248  131 
lemma less_asym: "x \<sqsubset> y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<sqsubset> x) \<Longrightarrow> P" 
132 
by (drule less_not_sym, erule contrapos_np) simp 

15524  133 

21248  134 
lemma eq_iff: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" 
135 
by (blast intro: antisym) 

15524  136 

21248  137 
lemma antisym_conv: "y \<sqsubseteq> x \<Longrightarrow> x \<sqsubseteq> y \<longleftrightarrow> x = y" 
138 
by (blast intro: antisym) 

15524  139 

21248  140 
lemma less_imp_neq: "x \<sqsubset> y \<Longrightarrow> x \<noteq> y" 
141 
by (erule contrapos_pn, erule subst, rule less_irrefl) 

142 

21083  143 

15524  144 
text {* Transitivity. *} 
145 

21248  146 
lemma less_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z" 
147 
by (simp add: less_le) (blast intro: trans antisym) 

15524  148 

21248  149 
lemma le_less_trans: "\<lbrakk> x \<sqsubseteq> y; y \<sqsubset> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z" 
150 
by (simp add: less_le) (blast intro: trans antisym) 

15524  151 

21248  152 
lemma less_le_trans: "\<lbrakk> x \<sqsubset> y; y \<sqsubseteq> z \<rbrakk> \<Longrightarrow> x \<sqsubset> z" 
153 
by (simp add: less_le) (blast intro: trans antisym) 

15524  154 

155 

156 
text {* Useful for simplification, but too risky to include by default. *} 

157 

21248  158 
lemma less_imp_not_less: "x \<sqsubset> y \<Longrightarrow> (\<not> y \<sqsubset> x) \<longleftrightarrow> True" 
159 
by (blast elim: less_asym) 

15524  160 

21248  161 
lemma less_imp_triv: "x \<sqsubset> y \<Longrightarrow> (y \<sqsubset> x \<longrightarrow> P) \<longleftrightarrow> True" 
162 
by (blast elim: less_asym) 

15524  163 

21248  164 
lemma less_imp_not_eq: "x \<sqsubset> y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 
15524  165 
by auto 
166 

21248  167 
lemma less_imp_not_eq2: "x \<sqsubset> y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 
15524  168 
by auto 
169 

21248  170 

21083  171 
text {* Transitivity rules for calculational reasoning *} 
15524  172 

21248  173 
lemma neq_le_trans: "\<lbrakk> a \<noteq> b; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b" 
174 
by (simp add: less_le) 

15524  175 

21248  176 
lemma le_neq_trans: "\<lbrakk> a \<sqsubseteq> b; a \<noteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b" 
177 
by (simp add: less_le) 

15524  178 

21248  179 
lemma less_asym': "\<lbrakk> a \<sqsubset> b; b \<sqsubset> a \<rbrakk> \<Longrightarrow> P" 
180 
by (rule less_asym) 

181 

182 
end 

15524  183 

184 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

185 
subsection {* Linear (total) orderings *} 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

186 

1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

187 
locale linear_order = partial_order + 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

188 
assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" 
15524  189 

190 
axclass linorder < order 

191 
linorder_linear: "x <= y  y <= x" 

192 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

193 
interpretation linorder: 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

194 
linear_order ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"] 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

195 
by unfold_locales (rule linorder_linear) 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

196 

21248  197 
context linear_order 
198 
begin 

199 

200 
lemma trichotomy: "x \<sqsubset> y \<or> x = y \<or> y \<sqsubset> x" 

201 
unfolding less_le using less_le linear by blast 

202 

203 
lemma le_less_linear: "x \<sqsubseteq> y \<or> y \<sqsubset> x" 

204 
by (simp add: le_less trichotomy) 

205 

206 
lemma le_cases [case_names le ge]: 

207 
"\<lbrakk> x \<sqsubseteq> y \<Longrightarrow> P; y \<sqsubseteq> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

208 
using linear by blast 

209 

210 
lemma cases [case_names less equal greater]: 

211 
"\<lbrakk> x \<sqsubset> y \<Longrightarrow> P; x = y \<Longrightarrow> P; y \<sqsubset> x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 

212 
using trichotomy by blast 

213 

214 
lemma not_less: "\<not> x \<sqsubset> y \<longleftrightarrow> y \<sqsubseteq> x" 

215 
apply (simp add: less_le) 

216 
using linear apply (blast intro: antisym) 

15524  217 
done 
218 

21248  219 
lemma not_le: "\<not> x \<sqsubseteq> y \<longleftrightarrow> y \<sqsubset> x" 
220 
apply (simp add: less_le) 

221 
using linear apply (blast intro: antisym) 

15524  222 
done 
223 

21248  224 
lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<sqsubset> y \<or> y \<sqsubset> x" 
225 
by (cut_tac x = x and y = y in trichotomy, auto) 

15524  226 

21248  227 
lemma neqE: "\<lbrakk> x \<noteq> y; x \<sqsubset> y \<Longrightarrow> R; y \<sqsubset> x \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 
228 
by (simp add: neq_iff) blast 

15524  229 

21248  230 
lemma antisym_conv1: "\<not> x \<sqsubset> y \<Longrightarrow> x \<sqsubseteq> y \<longleftrightarrow> x = y" 
231 
by (blast intro: antisym dest: not_less [THEN iffD1]) 

15524  232 

21248  233 
lemma antisym_conv2: "x \<sqsubseteq> y \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> x = y" 
234 
by (blast intro: antisym dest: not_less [THEN iffD1]) 

15524  235 

21248  236 
lemma antisym_conv3: "\<not> y \<sqsubset> x \<Longrightarrow> \<not> x \<sqsubset> y \<longleftrightarrow> x = y" 
237 
by (blast intro: antisym dest: not_less [THEN iffD1]) 

15524  238 

16796  239 
text{*Replacing the old Nat.leI*} 
21248  240 
lemma leI: "\<not> x \<sqsubset> y \<Longrightarrow> y \<sqsubseteq> x" 
241 
unfolding not_less . 

16796  242 

21248  243 
lemma leD: "y \<sqsubseteq> x \<Longrightarrow> \<not> x \<sqsubset> y" 
244 
unfolding not_less . 

16796  245 

246 
(*FIXME inappropriate name (or delete altogether)*) 

21248  247 
lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y" 
248 
unfolding not_le . 

249 

250 
end 

251 

252 

253 
subsection {* Name duplicates *} 

254 

255 
lemmas order_eq_refl [where 'b = "?'a::order"] = order.eq_refl 

256 
lemmas order_less_irrefl [where 'b = "?'a::order"] = order.less_irrefl 

257 
lemmas order_le_less [where 'b = "?'a::order"] = order.le_less 

258 
lemmas order_le_imp_less_or_eq [where 'b = "?'a::order"] = order.le_imp_less_or_eq 

259 
lemmas order_less_imp_le [where 'b = "?'a::order"] = order.less_imp_le 

260 
lemmas order_less_not_sym [where 'b = "?'a::order"] = order.less_not_sym 

261 
lemmas order_less_asym [where 'b = "?'a::order"] = order.less_asym 

262 
lemmas order_eq_iff [where 'b = "?'a::order"] = order.eq_iff 

263 
lemmas order_antisym_conv [where 'b = "?'a::order"] = order.antisym_conv 

264 
lemmas less_imp_neq [where 'b = "?'a::order"] = order.less_imp_neq 

265 
lemmas order_less_trans [where 'b = "?'a::order"] = order.less_trans 

266 
lemmas order_le_less_trans [where 'b = "?'a::order"] = order.le_less_trans 

267 
lemmas order_less_le_trans [where 'b = "?'a::order"] = order.less_le_trans 

268 
lemmas order_less_imp_not_less [where 'b = "?'a::order"] = order.less_imp_not_less 

269 
lemmas order_less_imp_triv [where 'b = "?'a::order"] = order.less_imp_triv 

270 
lemmas order_less_imp_not_eq [where 'b = "?'a::order"] = order.less_imp_not_eq 

271 
lemmas order_less_imp_not_eq2 [where 'b = "?'a::order"] = order.less_imp_not_eq2 

272 
lemmas order_neq_le_trans [where 'b = "?'a::order"] = order.neq_le_trans 

273 
lemmas order_le_neq_trans [where 'b = "?'a::order"] = order.le_neq_trans 

274 
lemmas order_less_asym' [where 'b = "?'a::order"] = order.less_asym' 

275 
lemmas linorder_less_linear [where 'b = "?'a::linorder"] = linorder.trichotomy 

276 
lemmas linorder_le_less_linear [where 'b = "?'a::linorder"] = linorder.le_less_linear 

277 
lemmas linorder_le_cases [where 'b = "?'a::linorder"] = linorder.le_cases 

278 
lemmas linorder_cases [where 'b = "?'a::linorder"] = linorder.cases 

279 
lemmas linorder_not_less [where 'b = "?'a::linorder"] = linorder.not_less 

280 
lemmas linorder_not_le [where 'b = "?'a::linorder"] = linorder.not_le 

281 
lemmas linorder_neq_iff [where 'b = "?'a::linorder"] = linorder.neq_iff 

282 
lemmas linorder_neqE [where 'b = "?'a::linorder"] = linorder.neqE 

283 
lemmas linorder_antisym_conv1 [where 'b = "?'a::linorder"] = linorder.antisym_conv1 

284 
lemmas linorder_antisym_conv2 [where 'b = "?'a::linorder"] = linorder.antisym_conv2 

285 
lemmas linorder_antisym_conv3 [where 'b = "?'a::linorder"] = linorder.antisym_conv3 

286 
lemmas leI [where 'b = "?'a::linorder"] = linorder.leI 

287 
lemmas leD [where 'b = "?'a::linorder"] = linorder.leD 

288 
lemmas not_leE [where 'b = "?'a::linorder"] = linorder.not_leE 

16796  289 

21083  290 

291 
subsection {* Reasoning tools setup *} 

292 

21091  293 
ML {* 
294 
local 

295 

296 
fun decomp_gen sort thy (Trueprop $ t) = 

21248  297 
let 
298 
fun of_sort t = 

299 
let 

300 
val T = type_of t 

301 
in 

21091  302 
(* exclude numeric types: linear arithmetic subsumes transitivity *) 
21248  303 
T <> HOLogic.natT andalso T <> HOLogic.intT 
304 
andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) 

305 
end; 

306 
fun dec (Const ("Not", _) $ t) = (case dec t 

307 
of NONE => NONE 

308 
 SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) 

309 
 dec (Const ("op =", _) $ t1 $ t2) = 

310 
if of_sort t1 

311 
then SOME (t1, "=", t2) 

312 
else NONE 

313 
 dec (Const ("Orderings.less_eq", _) $ t1 $ t2) = 

314 
if of_sort t1 

315 
then SOME (t1, "<=", t2) 

316 
else NONE 

317 
 dec (Const ("Orderings.less", _) $ t1 $ t2) = 

318 
if of_sort t1 

319 
then SOME (t1, "<", t2) 

320 
else NONE 

321 
 dec _ = NONE; 

21091  322 
in dec t end; 
323 

324 
in 

325 

326 
(* The setting up of Quasi_Tac serves as a demo. Since there is no 

327 
class for quasi orders, the tactics Quasi_Tac.trans_tac and 

328 
Quasi_Tac.quasi_tac are not of much use. *) 

329 

21248  330 
structure Quasi_Tac = Quasi_Tac_Fun ( 
331 
struct 

332 
val le_trans = thm "order_trans"; 

333 
val le_refl = thm "order_refl"; 

334 
val eqD1 = thm "order_eq_refl"; 

335 
val eqD2 = thm "sym" RS thm "order_eq_refl"; 

336 
val less_reflE = thm "order_less_irrefl" RS thm "notE"; 

337 
val less_imp_le = thm "order_less_imp_le"; 

338 
val le_neq_trans = thm "order_le_neq_trans"; 

339 
val neq_le_trans = thm "order_neq_le_trans"; 

340 
val less_imp_neq = thm "less_imp_neq"; 

341 
val decomp_trans = decomp_gen ["Orderings.order"]; 

342 
val decomp_quasi = decomp_gen ["Orderings.order"]; 

343 
end); 

21091  344 

345 
structure Order_Tac = Order_Tac_Fun ( 

21248  346 
struct 
347 
val less_reflE = thm "order_less_irrefl" RS thm "notE"; 

348 
val le_refl = thm "order_refl"; 

349 
val less_imp_le = thm "order_less_imp_le"; 

350 
val not_lessI = thm "linorder_not_less" RS thm "iffD2"; 

351 
val not_leI = thm "linorder_not_le" RS thm "iffD2"; 

352 
val not_lessD = thm "linorder_not_less" RS thm "iffD1"; 

353 
val not_leD = thm "linorder_not_le" RS thm "iffD1"; 

354 
val eqI = thm "order_antisym"; 

355 
val eqD1 = thm "order_eq_refl"; 

356 
val eqD2 = thm "sym" RS thm "order_eq_refl"; 

357 
val less_trans = thm "order_less_trans"; 

358 
val less_le_trans = thm "order_less_le_trans"; 

359 
val le_less_trans = thm "order_le_less_trans"; 

360 
val le_trans = thm "order_trans"; 

361 
val le_neq_trans = thm "order_le_neq_trans"; 

362 
val neq_le_trans = thm "order_neq_le_trans"; 

363 
val less_imp_neq = thm "less_imp_neq"; 

364 
val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; 

365 
val not_sym = thm "not_sym"; 

366 
val decomp_part = decomp_gen ["Orderings.order"]; 

367 
val decomp_lin = decomp_gen ["Orderings.linorder"]; 

368 
end); 

21091  369 

370 
end; 

371 
*} 

372 

21083  373 
setup {* 
374 
let 

375 

376 
val order_antisym_conv = thm "order_antisym_conv" 

377 
val linorder_antisym_conv1 = thm "linorder_antisym_conv1" 

378 
val linorder_antisym_conv2 = thm "linorder_antisym_conv2" 

379 
val linorder_antisym_conv3 = thm "linorder_antisym_conv3" 

380 

381 
fun prp t thm = (#prop (rep_thm thm) = t); 

15524  382 

21083  383 
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) = 
384 
let val prems = prems_of_ss ss; 

385 
val less = Const("Orderings.less",T); 

386 
val t = HOLogic.mk_Trueprop(le $ s $ r); 

387 
in case find_first (prp t) prems of 

388 
NONE => 

389 
let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) 

390 
in case find_first (prp t) prems of 

391 
NONE => NONE 

392 
 SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1)) 

393 
end 

394 
 SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv)) 

395 
end 

396 
handle THM _ => NONE; 

15524  397 

21083  398 
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) = 
399 
let val prems = prems_of_ss ss; 

400 
val le = Const("Orderings.less_eq",T); 

401 
val t = HOLogic.mk_Trueprop(le $ r $ s); 

402 
in case find_first (prp t) prems of 

403 
NONE => 

404 
let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r)) 

405 
in case find_first (prp t) prems of 

406 
NONE => NONE 

407 
 SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3)) 

408 
end 

409 
 SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2)) 

410 
end 

411 
handle THM _ => NONE; 

15524  412 

21248  413 
fun add_simprocs procs thy = 
414 
(Simplifier.change_simpset_of thy (fn ss => ss 

415 
addsimprocs (map (fn (name, raw_ts, proc) => 

416 
Simplifier.simproc thy name raw_ts proc)) procs); thy); 

417 
fun add_solver name tac thy = 

418 
(Simplifier.change_simpset_of thy (fn ss => ss addSolver 

419 
(mk_solver name (K tac))); thy); 

21083  420 

421 
in 

21248  422 
add_simprocs [ 
423 
("antisym le", ["(x::'a::order) <= y"], prove_antisym_le), 

424 
("antisym less", ["~ (x::'a::linorder) < y"], prove_antisym_less) 

425 
] 

426 
#> add_solver "Trans_linear" Order_Tac.linear_tac 

427 
#> add_solver "Trans_partial" Order_Tac.partial_tac 

428 
(* Adding the transitivity reasoners also as safe solvers showed a slight 

429 
speed up, but the reasoning strength appears to be not higher (at least 

430 
no breaking of additional proofs in the entire HOL distribution, as 

431 
of 5 March 2004, was observed). *) 

21083  432 
end 
433 
*} 

15524  434 

435 

21083  436 
subsection {* Bounded quantifiers *} 
437 

438 
syntax 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

439 
"_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

440 
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

441 
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

442 
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) 
21083  443 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

444 
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

445 
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

446 
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

447 
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) 
21083  448 

449 
syntax (xsymbols) 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

450 
"_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

451 
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

452 
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

453 
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) 
21083  454 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

455 
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

456 
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

457 
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

458 
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) 
21083  459 

460 
syntax (HOL) 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

461 
"_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

462 
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

463 
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

464 
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) 
21083  465 

466 
syntax (HTML output) 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

467 
"_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

468 
"_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

469 
"_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

470 
"_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) 
21083  471 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

472 
"_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

473 
"_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

474 
"_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

475 
"_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) 
21083  476 

477 
translations 

478 
"ALL x<y. P" => "ALL x. x < y \<longrightarrow> P" 

479 
"EX x<y. P" => "EX x. x < y \<and> P" 

480 
"ALL x<=y. P" => "ALL x. x <= y \<longrightarrow> P" 

481 
"EX x<=y. P" => "EX x. x <= y \<and> P" 

482 
"ALL x>y. P" => "ALL x. x > y \<longrightarrow> P" 

483 
"EX x>y. P" => "EX x. x > y \<and> P" 

484 
"ALL x>=y. P" => "ALL x. x >= y \<longrightarrow> P" 

485 
"EX x>=y. P" => "EX x. x >= y \<and> P" 

486 

487 
print_translation {* 

488 
let 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

489 
val syntax_name = Sign.const_syntax_name (the_context ()); 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

490 
val impl = syntax_name "op >"; 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

491 
val conj = syntax_name "op &"; 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

492 
val less = syntax_name "Orderings.less"; 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

493 
val less_eq = syntax_name "Orderings.less_eq"; 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

494 

f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

495 
val trans = 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

496 
[(("ALL ", impl, less), ("_All_less", "_All_greater")), 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

497 
(("ALL ", impl, less_eq), ("_All_less_eq", "_All_greater_eq")), 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

498 
(("EX ", conj, less), ("_Ex_less", "_Ex_greater")), 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

499 
(("EX ", conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

500 

21083  501 
fun mk v v' c n P = 
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

502 
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v  _ => false) n) 
21083  503 
then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match; 
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

504 

f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

505 
fun tr' q = (q, 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

506 
fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] => 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

507 
(case AList.lookup (op =) trans (q, c, d) of 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

508 
NONE => raise Match 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

509 
 SOME (l, g) => 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

510 
(case (t, u) of 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

511 
(Const ("_bound", _) $ Free (v', _), n) => mk v v' l n P 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

512 
 (n, Const ("_bound", _) $ Free (v', _)) => mk v v' g n P 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

513 
 _ => raise Match)) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

514 
 _ => raise Match); 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

515 
in [tr' "ALL ", tr' "EX "] end 
21083  516 
*} 
517 

518 

519 
subsection {* Transitivity reasoning on decreasing inequalities *} 

520 

21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

521 
(* FIXME cleanup *) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

522 

21083  523 
text {* These support proving chains of decreasing inequalities 
524 
a >= b >= c ... in Isar proofs. *} 

525 

526 
lemma xt1: 

527 
"a = b ==> b > c ==> a > c" 

528 
"a > b ==> b = c ==> a > c" 

529 
"a = b ==> b >= c ==> a >= c" 

530 
"a >= b ==> b = c ==> a >= c" 

531 
"(x::'a::order) >= y ==> y >= x ==> x = y" 

532 
"(x::'a::order) >= y ==> y >= z ==> x >= z" 

533 
"(x::'a::order) > y ==> y >= z ==> x > z" 

534 
"(x::'a::order) >= y ==> y > z ==> x > z" 

535 
"(a::'a::order) > b ==> b > a ==> ?P" 

536 
"(x::'a::order) > y ==> y > z ==> x > z" 

537 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

538 
"(a::'a::order) ~= b ==> a >= b ==> a > b" 

539 
"a = f b ==> b > c ==> (!!x y. x > y ==> f x > f y) ==> a > f c" 

540 
"a > b ==> f b = c ==> (!!x y. x > y ==> f x > f y) ==> f a > c" 

541 
"a = f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" 

542 
"a >= b ==> f b = c ==> (!! x y. x >= y ==> f x >= f y) ==> f a >= c" 

543 
by auto 

544 

545 
lemma xt2: 

546 
"(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" 

547 
by (subgoal_tac "f b >= f c", force, force) 

548 

549 
lemma xt3: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> 

550 
(!!x y. x >= y ==> f x >= f y) ==> f a >= c" 

551 
by (subgoal_tac "f a >= f b", force, force) 

552 

553 
lemma xt4: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> 

554 
(!!x y. x >= y ==> f x >= f y) ==> a > f c" 

555 
by (subgoal_tac "f b >= f c", force, force) 

556 

557 
lemma xt5: "(a::'a::order) > b ==> (f b::'b::order) >= c==> 

558 
(!!x y. x > y ==> f x > f y) ==> f a > c" 

559 
by (subgoal_tac "f a > f b", force, force) 

560 

561 
lemma xt6: "(a::'a::order) >= f b ==> b > c ==> 

562 
(!!x y. x > y ==> f x > f y) ==> a > f c" 

563 
by (subgoal_tac "f b > f c", force, force) 

564 

565 
lemma xt7: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> 

566 
(!!x y. x >= y ==> f x >= f y) ==> f a > c" 

567 
by (subgoal_tac "f a >= f b", force, force) 

568 

569 
lemma xt8: "(a::'a::order) > f b ==> (b::'b::order) > c ==> 

570 
(!!x y. x > y ==> f x > f y) ==> a > f c" 

571 
by (subgoal_tac "f b > f c", force, force) 

572 

573 
lemma xt9: "(a::'a::order) > b ==> (f b::'b::order) > c ==> 

574 
(!!x y. x > y ==> f x > f y) ==> f a > c" 

575 
by (subgoal_tac "f a > f b", force, force) 

576 

577 
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 

578 

579 
(* 

580 
Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands 

581 
for the wrong thing in an Isar proof. 

582 

583 
The extra transitivity rules can be used as follows: 

584 

585 
lemma "(a::'a::order) > z" 

586 
proof  

587 
have "a >= b" (is "_ >= ?rhs") 

588 
sorry 

589 
also have "?rhs >= c" (is "_ >= ?rhs") 

590 
sorry 

591 
also (xtrans) have "?rhs = d" (is "_ = ?rhs") 

592 
sorry 

593 
also (xtrans) have "?rhs >= e" (is "_ >= ?rhs") 

594 
sorry 

595 
also (xtrans) have "?rhs > f" (is "_ > ?rhs") 

596 
sorry 

597 
also (xtrans) have "?rhs > z" 

598 
sorry 

599 
finally (xtrans) show ?thesis . 

600 
qed 

601 

602 
Alternatively, one can use "declare xtrans [trans]" and then 

603 
leave out the "(xtrans)" above. 

604 
*) 

605 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

606 
subsection {* Monotonicity, syntactic least value operator and syntactic min/max *} 
21083  607 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

608 
locale mono = 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

609 
fixes f 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

610 
assumes mono: "A \<le> B \<Longrightarrow> f A \<le> f B" 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

611 

1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

612 
lemmas monoI [intro?] = mono.intro 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

613 
and monoD [dest?] = mono.mono 
21083  614 

615 
constdefs 

616 
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) 

617 
"Least P == THE x. P x & (ALL y. P y > x <= y)" 

618 
 {* We can no longer use LeastM because the latter requires HilbertAC. *} 

619 

620 
constdefs 

621 
min :: "['a::ord, 'a] => 'a" 

622 
"min a b == (if a <= b then a else b)" 

623 
max :: "['a::ord, 'a] => 'a" 

624 
"max a b == (if a <= b then b else a)" 

625 

15524  626 
end 