author  haftmann 
Mon, 13 Nov 2006 15:43:06 +0100  
changeset 21329  7338206d75f1 
parent 21259  63ab016c99ca 
child 21383  17e6275e13f5 
permissions  rwrr 
15524  1 
(* Title: HOL/Orderings.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 

4 
*) 

5 

21329  6 
header {* Syntactic and abstract orders *} 
15524  7 

8 
theory Orderings 

21329  9 
imports HOL 
15524  10 
begin 
11 

21329  12 
section {* Abstract orders *} 
21083  13 

21329  14 
subsection {* Order syntax *} 
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 

21329  70 
subsection {* Quasiorders (preorders) *} 
15524  71 

21329  72 
locale preorder = 
21216
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" 
21248  77 
and less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y" 
78 
begin 

79 

80 
abbreviation (input) 

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

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

83 

84 
abbreviation (input) 

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

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

87 

15524  88 
text {* Reflexivity. *} 
89 

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

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

15524  96 

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

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

15524  103 

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

106 

21329  107 
lemma less_imp_neq: "x \<sqsubset> y \<Longrightarrow> x \<noteq> y" 
108 
by (erule contrapos_pn, erule subst, rule less_irrefl) 

109 

110 

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

112 

113 
lemma less_imp_not_eq: "x \<sqsubset> y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 

114 
by auto 

115 

116 
lemma less_imp_not_eq2: "x \<sqsubset> y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 

117 
by auto 

118 

119 

120 
text {* Transitivity rules for calculational reasoning *} 

121 

122 
lemma neq_le_trans: "\<lbrakk> a \<noteq> b; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b" 

123 
by (simp add: less_le) 

124 

125 
lemma le_neq_trans: "\<lbrakk> a \<sqsubseteq> b; a \<noteq> b \<rbrakk> \<Longrightarrow> a \<sqsubset> b" 

126 
by (simp add: less_le) 

127 

128 
end 

129 

130 

131 
subsection {* Partial orderings *} 

132 

133 
locale partial_order = preorder + 

134 
assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y" 

135 

136 
context partial_order 

137 
begin 

15524  138 

139 
text {* Asymmetry. *} 

140 

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

15524  143 

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

15524  146 

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

15524  149 

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

15524  152 

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

155 

21083  156 

15524  157 
text {* Transitivity. *} 
158 

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

15524  161 

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

15524  164 

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

15524  167 

168 

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

170 

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

15524  173 

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

15524  176 

21248  177 

21083  178 
text {* Transitivity rules for calculational reasoning *} 
15524  179 

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

182 

183 
end 

15524  184 

21329  185 
axclass order < ord 
186 
order_refl [iff]: "x <= x" 

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

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

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

15524  190 

21329  191 
interpretation order: 
192 
partial_order ["op \<le> \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>order \<Rightarrow> 'a \<Rightarrow> bool"] 

193 
apply unfold_locales 

194 
apply (rule order_refl) 

195 
apply (erule (1) order_trans) 

196 
apply (rule order_less_le) 

197 
apply (erule (1) order_antisym) 

198 
done 

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

199 

21329  200 

201 
subsection {* Linear (total) orders *} 

202 

203 
locale linorder = partial_order + 

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

204 
assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" 
15524  205 

21329  206 
context linorder 
21248  207 
begin 
208 

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

210 
unfolding less_le using less_le linear by blast 

211 

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

213 
by (simp add: le_less trichotomy) 

214 

215 
lemma le_cases [case_names le ge]: 

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

217 
using linear by blast 

218 

219 
lemma cases [case_names less equal greater]: 

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

221 
using trichotomy by blast 

222 

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

224 
apply (simp add: less_le) 

225 
using linear apply (blast intro: antisym) 

15524  226 
done 
227 

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

230 
using linear apply (blast intro: antisym) 

15524  231 
done 
232 

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

15524  235 

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

15524  238 

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

15524  241 

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

15524  244 

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

15524  247 

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

16796  251 

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

16796  254 

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

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

258 

259 
end 

260 

21329  261 
axclass linorder < order 
262 
linorder_linear: "x <= y  y <= x" 

263 

264 
interpretation linorder: 

265 
linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op < \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool"] 

266 
by unfold_locales (rule linorder_linear) 

267 

21248  268 

269 
subsection {* Name duplicates *} 

270 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

16796  305 

21083  306 

307 
subsection {* Reasoning tools setup *} 

308 

21091  309 
ML {* 
310 
local 

311 

312 
fun decomp_gen sort thy (Trueprop $ t) = 

21248  313 
let 
314 
fun of_sort t = 

315 
let 

316 
val T = type_of t 

317 
in 

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

321 
end; 

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

323 
of NONE => NONE 

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

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

326 
if of_sort t1 

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

328 
else NONE 

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

330 
if of_sort t1 

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

332 
else NONE 

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

334 
if of_sort t1 

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

336 
else NONE 

337 
 dec _ = NONE; 

21091  338 
in dec t end; 
339 

340 
in 

341 

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

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

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

345 

21248  346 
structure Quasi_Tac = Quasi_Tac_Fun ( 
347 
struct 

348 
val le_trans = thm "order_trans"; 

349 
val le_refl = thm "order_refl"; 

350 
val eqD1 = thm "order_eq_refl"; 

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

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

353 
val less_imp_le = thm "order_less_imp_le"; 

354 
val le_neq_trans = thm "order_le_neq_trans"; 

355 
val neq_le_trans = thm "order_neq_le_trans"; 

356 
val less_imp_neq = thm "less_imp_neq"; 

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

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

359 
end); 

21091  360 

361 
structure Order_Tac = Order_Tac_Fun ( 

21248  362 
struct 
363 
val less_reflE = thm "order_less_irrefl" RS thm "notE"; 

364 
val le_refl = thm "order_refl"; 

365 
val less_imp_le = thm "order_less_imp_le"; 

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

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

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

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

370 
val eqI = thm "order_antisym"; 

371 
val eqD1 = thm "order_eq_refl"; 

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

373 
val less_trans = thm "order_less_trans"; 

374 
val less_le_trans = thm "order_less_le_trans"; 

375 
val le_less_trans = thm "order_le_less_trans"; 

376 
val le_trans = thm "order_trans"; 

377 
val le_neq_trans = thm "order_le_neq_trans"; 

378 
val neq_le_trans = thm "order_neq_le_trans"; 

379 
val less_imp_neq = thm "less_imp_neq"; 

380 
val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; 

381 
val not_sym = thm "not_sym"; 

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

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

384 
end); 

21091  385 

386 
end; 

387 
*} 

388 

21083  389 
setup {* 
390 
let 

391 

392 
val order_antisym_conv = thm "order_antisym_conv" 

393 
val linorder_antisym_conv1 = thm "linorder_antisym_conv1" 

394 
val linorder_antisym_conv2 = thm "linorder_antisym_conv2" 

395 
val linorder_antisym_conv3 = thm "linorder_antisym_conv3" 

396 

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

15524  398 

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

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

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

403 
in case find_first (prp t) prems of 

404 
NONE => 

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

406 
in case find_first (prp t) prems of 

407 
NONE => NONE 

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

409 
end 

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

411 
end 

412 
handle THM _ => NONE; 

15524  413 

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

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

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

418 
in case find_first (prp t) prems of 

419 
NONE => 

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

421 
in case find_first (prp t) prems of 

422 
NONE => NONE 

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

424 
end 

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

426 
end 

427 
handle THM _ => NONE; 

15524  428 

21248  429 
fun add_simprocs procs thy = 
430 
(Simplifier.change_simpset_of thy (fn ss => ss 

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

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

433 
fun add_solver name tac thy = 

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

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

21083  436 

437 
in 

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

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

441 
] 

442 
#> add_solver "Trans_linear" Order_Tac.linear_tac 

443 
#> add_solver "Trans_partial" Order_Tac.partial_tac 

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

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

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

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

21083  448 
end 
449 
*} 

15524  450 

451 

21083  452 
subsection {* Bounded quantifiers *} 
453 

454 
syntax 

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

455 
"_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

456 
"_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

457 
"_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

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

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

460 
"_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

461 
"_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

462 
"_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

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

465 
syntax (xsymbols) 

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

466 
"_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

467 
"_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

468 
"_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

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

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

471 
"_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

472 
"_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

473 
"_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

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

476 
syntax (HOL) 

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

477 
"_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

478 
"_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

479 
"_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

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

482 
syntax (HTML output) 

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

483 
"_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

484 
"_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

485 
"_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

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

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

488 
"_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

489 
"_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

490 
"_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

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

493 
translations 

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

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

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

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

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

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

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

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

502 

503 
print_translation {* 

504 
let 

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

505 
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

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

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

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

509 
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

510 

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

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

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

513 
(("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

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

515 
(("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

516 

21083  517 
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

518 
if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v  _ => false) n) 
21083  519 
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

520 

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

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

522 
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

523 
(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

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

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

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

527 
(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

528 
 (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

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

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

531 
in [tr' "ALL ", tr' "EX "] end 
21083  532 
*} 
533 

534 

535 
subsection {* Transitivity reasoning on decreasing inequalities *} 

536 

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

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

538 

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

541 

542 
lemma xt1: 

543 
"a = b ==> b > c ==> a > c" 

544 
"a > b ==> b = c ==> a > c" 

545 
"a = b ==> b >= c ==> a >= c" 

546 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

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

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

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

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

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

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

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

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

559 
by auto 

560 

561 
lemma xt2: 

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

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

564 

565 
lemma xt3: "(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 xt4: "(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 xt5: "(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 
lemma xt6: "(a::'a::order) >= f b ==> b > c ==> 

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

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

580 

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

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

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

584 

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

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

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

588 

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

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

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

592 

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

594 

595 
(* 

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

597 
for the wrong thing in an Isar proof. 

598 

599 
The extra transitivity rules can be used as follows: 

600 

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

602 
proof  

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

604 
sorry 

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

606 
sorry 

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

608 
sorry 

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

610 
sorry 

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

612 
sorry 

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

614 
sorry 

615 
finally (xtrans) show ?thesis . 

616 
qed 

617 

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

619 
leave out the "(xtrans)" above. 

620 
*) 

621 

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

622 
subsection {* Monotonicity, syntactic least value operator and syntactic min/max *} 
21083  623 

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

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

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

626 
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

627 

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

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

629 
and monoD [dest?] = mono.mono 
21083  630 

631 
constdefs 

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

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

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

635 

636 
constdefs 

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

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

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

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

641 

15524  642 
end 