author  haftmann 
Sat, 12 Apr 2014 11:27:36 +0200  
changeset 56545  8f1e7596deb7 
parent 56509  e050d42dc21d 
child 57447  87429bdecad5 
permissions  rwrr 
28685  1 
(* Title: HOL/Orderings.thy 
15524  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

4 

25614  5 
header {* Abstract orderings *} 
15524  6 

7 
theory Orderings 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35115
diff
changeset

8 
imports HOL 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46884
diff
changeset

9 
keywords "print_orders" :: diag 
15524  10 
begin 
11 

48891  12 
ML_file "~~/src/Provers/order.ML" 
13 
ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *) 

14 

51487  15 
subsection {* Abstract ordering *} 
16 

17 
locale ordering = 

18 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50) 

19 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50) 

20 
assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b" 

21 
assumes refl: "a \<preceq> a"  {* not @{text iff}: makes problems due to multiple (dual) interpretations *} 

22 
and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b" 

23 
and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c" 

24 
begin 

25 

26 
lemma strict_implies_order: 

27 
"a \<prec> b \<Longrightarrow> a \<preceq> b" 

28 
by (simp add: strict_iff_order) 

29 

30 
lemma strict_implies_not_eq: 

31 
"a \<prec> b \<Longrightarrow> a \<noteq> b" 

32 
by (simp add: strict_iff_order) 

33 

34 
lemma not_eq_order_implies_strict: 

35 
"a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b" 

36 
by (simp add: strict_iff_order) 

37 

38 
lemma order_iff_strict: 

39 
"a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b" 

40 
by (auto simp add: strict_iff_order refl) 

41 

42 
lemma irrefl:  {* not @{text iff}: makes problems due to multiple (dual) interpretations *} 

43 
"\<not> a \<prec> a" 

44 
by (simp add: strict_iff_order) 

45 

46 
lemma asym: 

47 
"a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False" 

48 
by (auto simp add: strict_iff_order intro: antisym) 

49 

50 
lemma strict_trans1: 

51 
"a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c" 

52 
by (auto simp add: strict_iff_order intro: trans antisym) 

53 

54 
lemma strict_trans2: 

55 
"a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c" 

56 
by (auto simp add: strict_iff_order intro: trans antisym) 

57 

58 
lemma strict_trans: 

59 
"a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c" 

60 
by (auto intro: strict_trans1 strict_implies_order) 

61 

62 
end 

63 

64 
locale ordering_top = ordering + 

65 
fixes top :: "'a" 

66 
assumes extremum [simp]: "a \<preceq> top" 

67 
begin 

68 

69 
lemma extremum_uniqueI: 

70 
"top \<preceq> a \<Longrightarrow> a = top" 

71 
by (rule antisym) auto 

72 

73 
lemma extremum_unique: 

74 
"top \<preceq> a \<longleftrightarrow> a = top" 

75 
by (auto intro: antisym) 

76 

77 
lemma extremum_strict [simp]: 

78 
"\<not> (top \<prec> a)" 

79 
using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl) 

80 

81 
lemma not_eq_extremum: 

82 
"a \<noteq> top \<longleftrightarrow> a \<prec> top" 

83 
by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum) 

84 

85 
end 

86 

87 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

88 
subsection {* Syntactic orders *} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

89 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

90 
class ord = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

91 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

92 
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

93 
begin 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

94 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

95 
notation 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

96 
less_eq ("op <=") and 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

97 
less_eq ("(_/ <= _)" [51, 51] 50) and 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

98 
less ("op <") and 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

99 
less ("(_/ < _)" [51, 51] 50) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

100 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

101 
notation (xsymbols) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

102 
less_eq ("op \<le>") and 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

103 
less_eq ("(_/ \<le> _)" [51, 51] 50) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

104 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

105 
notation (HTML output) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

106 
less_eq ("op \<le>") and 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

107 
less_eq ("(_/ \<le> _)" [51, 51] 50) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

108 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

109 
abbreviation (input) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

110 
greater_eq (infix ">=" 50) where 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

111 
"x >= y \<equiv> y <= x" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

112 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

113 
notation (input) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

114 
greater_eq (infix "\<ge>" 50) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

115 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

116 
abbreviation (input) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

117 
greater (infix ">" 50) where 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

118 
"x > y \<equiv> y < x" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

119 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

120 
end 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

121 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

122 

27682  123 
subsection {* Quasi orders *} 
15524  124 

27682  125 
class preorder = ord + 
126 
assumes less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> (y \<le> x)" 

25062  127 
and order_refl [iff]: "x \<le> x" 
128 
and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z" 

21248  129 
begin 
130 

15524  131 
text {* Reflexivity. *} 
132 

25062  133 
lemma eq_refl: "x = y \<Longrightarrow> x \<le> y" 
15524  134 
 {* This form is useful with the classical reasoner. *} 
23212  135 
by (erule ssubst) (rule order_refl) 
15524  136 

25062  137 
lemma less_irrefl [iff]: "\<not> x < x" 
27682  138 
by (simp add: less_le_not_le) 
139 

140 
lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y" 

141 
unfolding less_le_not_le by blast 

142 

143 

144 
text {* Asymmetry. *} 

145 

146 
lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)" 

147 
by (simp add: less_le_not_le) 

148 

149 
lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P" 

150 
by (drule less_not_sym, erule contrapos_np) simp 

151 

152 

153 
text {* Transitivity. *} 

154 

155 
lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" 

156 
by (auto simp add: less_le_not_le intro: order_trans) 

157 

158 
lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z" 

159 
by (auto simp add: less_le_not_le intro: order_trans) 

160 

161 
lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z" 

162 
by (auto simp add: less_le_not_le intro: order_trans) 

163 

164 

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

166 

167 
lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True" 

168 
by (blast elim: less_asym) 

169 

170 
lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True" 

171 
by (blast elim: less_asym) 

172 

173 

174 
text {* Transitivity rules for calculational reasoning *} 

175 

176 
lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P" 

177 
by (rule less_asym) 

178 

179 

180 
text {* Dual order *} 

181 

182 
lemma dual_preorder: 

36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35828
diff
changeset

183 
"class.preorder (op \<ge>) (op >)" 
28823  184 
proof qed (auto simp add: less_le_not_le intro: order_trans) 
27682  185 

186 
end 

187 

188 

189 
subsection {* Partial orders *} 

190 

191 
class order = preorder + 

192 
assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y" 

193 
begin 

194 

51487  195 
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" 
196 
by (auto simp add: less_le_not_le intro: antisym) 

197 

54868  198 
sublocale order!: ordering less_eq less + dual_order!: ordering greater_eq greater 
51487  199 
by default (auto intro: antisym order_trans simp add: less_le) 
200 

201 

202 
text {* Reflexivity. *} 

15524  203 

25062  204 
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y" 
15524  205 
 {* NOT suitable for iff, since it can cause PROOF FAILED. *} 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

206 
by (fact order.order_iff_strict) 
15524  207 

25062  208 
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y" 
23212  209 
unfolding less_le by blast 
15524  210 

21329  211 

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

213 

25062  214 
lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 
23212  215 
by auto 
21329  216 

25062  217 
lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 
23212  218 
by auto 
21329  219 

220 

221 
text {* Transitivity rules for calculational reasoning *} 

222 

25062  223 
lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

224 
by (fact order.not_eq_order_implies_strict) 
21329  225 

25062  226 
lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b" 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

227 
by (rule order.not_eq_order_implies_strict) 
21329  228 

15524  229 

230 
text {* Asymmetry. *} 

231 

25062  232 
lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x" 
23212  233 
by (blast intro: antisym) 
15524  234 

25062  235 
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y" 
23212  236 
by (blast intro: antisym) 
15524  237 

25062  238 
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y" 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

239 
by (fact order.strict_implies_not_eq) 
21248  240 

21083  241 

27107  242 
text {* Least value operator *} 
243 

27299  244 
definition (in ord) 
27107  245 
Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where 
246 
"Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))" 

247 

248 
lemma Least_equality: 

249 
assumes "P x" 

250 
and "\<And>y. P y \<Longrightarrow> x \<le> y" 

251 
shows "Least P = x" 

252 
unfolding Least_def by (rule the_equality) 

253 
(blast intro: assms antisym)+ 

254 

255 
lemma LeastI2_order: 

256 
assumes "P x" 

257 
and "\<And>y. P y \<Longrightarrow> x \<le> y" 

258 
and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x" 

259 
shows "Q (Least P)" 

260 
unfolding Least_def by (rule theI2) 

261 
(blast intro: assms antisym)+ 

262 

263 

26014  264 
text {* Dual order *} 
22916  265 

26014  266 
lemma dual_order: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35828
diff
changeset

267 
"class.order (op \<ge>) (op >)" 
27682  268 
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym) 
22916  269 

21248  270 
end 
15524  271 

21329  272 

56545  273 
text {* Alternative introduction rule with bias towards strict order *} 
274 

275 
lemma order_strictI: 

276 
fixes less (infix "\<sqsubset>" 50) 

277 
and less_eq (infix "\<sqsubseteq>" 50) 

278 
assumes less_eq_less: "\<And>a b. a \<sqsubseteq> b \<longleftrightarrow> a \<sqsubset> b \<or> a = b" 

279 
assumes asym: "\<And>a b. a \<sqsubset> b \<Longrightarrow> \<not> b \<sqsubset> a" 

280 
assumes irrefl: "\<And>a. \<not> a \<sqsubset> a" 

281 
assumes trans: "\<And>a b c. a \<sqsubset> b \<Longrightarrow> b \<sqsubset> c \<Longrightarrow> a \<sqsubset> c" 

282 
shows "class.order less_eq less" 

283 
proof 

284 
fix a b 

285 
show "a \<sqsubset> b \<longleftrightarrow> a \<sqsubseteq> b \<and> \<not> b \<sqsubseteq> a" 

286 
by (auto simp add: less_eq_less asym irrefl) 

287 
next 

288 
fix a 

289 
show "a \<sqsubseteq> a" 

290 
by (auto simp add: less_eq_less) 

291 
next 

292 
fix a b c 

293 
assume "a \<sqsubseteq> b" and "b \<sqsubseteq> c" then show "a \<sqsubseteq> c" 

294 
by (auto simp add: less_eq_less intro: trans) 

295 
next 

296 
fix a b 

297 
assume "a \<sqsubseteq> b" and "b \<sqsubseteq> a" then show "a = b" 

298 
by (auto simp add: less_eq_less asym) 

299 
qed 

300 

301 

21329  302 
subsection {* Linear (total) orders *} 
303 

22316  304 
class linorder = order + 
25207  305 
assumes linear: "x \<le> y \<or> y \<le> x" 
21248  306 
begin 
307 

25062  308 
lemma less_linear: "x < y \<or> x = y \<or> y < x" 
23212  309 
unfolding less_le using less_le linear by blast 
21248  310 

25062  311 
lemma le_less_linear: "x \<le> y \<or> y < x" 
23212  312 
by (simp add: le_less less_linear) 
21248  313 

314 
lemma le_cases [case_names le ge]: 

25062  315 
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  316 
using linear by blast 
21248  317 

22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22377
diff
changeset

318 
lemma linorder_cases [case_names less equal greater]: 
25062  319 
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  320 
using less_linear by blast 
21248  321 

25062  322 
lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x" 
23212  323 
apply (simp add: less_le) 
324 
using linear apply (blast intro: antisym) 

325 
done 

326 

327 
lemma not_less_iff_gr_or_eq: 

25062  328 
"\<not>(x < y) \<longleftrightarrow> (x > y  x = y)" 
23212  329 
apply(simp add:not_less le_less) 
330 
apply blast 

331 
done 

15524  332 

25062  333 
lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x" 
23212  334 
apply (simp add: less_le) 
335 
using linear apply (blast intro: antisym) 

336 
done 

15524  337 

25062  338 
lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x" 
23212  339 
by (cut_tac x = x and y = y in less_linear, auto) 
15524  340 

25062  341 
lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R" 
23212  342 
by (simp add: neq_iff) blast 
15524  343 

25062  344 
lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y" 
23212  345 
by (blast intro: antisym dest: not_less [THEN iffD1]) 
15524  346 

25062  347 
lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y" 
23212  348 
by (blast intro: antisym dest: not_less [THEN iffD1]) 
15524  349 

25062  350 
lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y" 
23212  351 
by (blast intro: antisym dest: not_less [THEN iffD1]) 
15524  352 

25062  353 
lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x" 
23212  354 
unfolding not_less . 
16796  355 

25062  356 
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y" 
23212  357 
unfolding not_less . 
16796  358 

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

25062  360 
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y" 
23212  361 
unfolding not_le . 
21248  362 

22916  363 

26014  364 
text {* Dual order *} 
22916  365 

26014  366 
lemma dual_linorder: 
36635
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35828
diff
changeset

367 
"class.linorder (op \<ge>) (op >)" 
080b755377c0
locale predicates of classes carry a mandatory "class" prefix
haftmann
parents:
35828
diff
changeset

368 
by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear) 
22916  369 

21248  370 
end 
371 

23948  372 

56545  373 
text {* Alternative introduction rule with bias towards strict order *} 
374 

375 
lemma linorder_strictI: 

376 
fixes less (infix "\<sqsubset>" 50) 

377 
and less_eq (infix "\<sqsubseteq>" 50) 

378 
assumes "class.order less_eq less" 

379 
assumes trichotomy: "\<And>a b. a \<sqsubset> b \<or> a = b \<or> b \<sqsubset> a" 

380 
shows "class.linorder less_eq less" 

381 
proof  

382 
interpret order less_eq less 

383 
by (fact `class.order less_eq less`) 

384 
show ?thesis 

385 
proof 

386 
fix a b 

387 
show "a \<sqsubseteq> b \<or> b \<sqsubseteq> a" 

388 
using trichotomy by (auto simp add: le_less) 

389 
qed 

390 
qed 

391 

392 

21083  393 
subsection {* Reasoning tools setup *} 
394 

21091  395 
ML {* 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

396 
signature ORDERS = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

397 
sig 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

398 
val print_structures: Proof.context > unit 
32215  399 
val order_tac: Proof.context > thm list > int > tactic 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

400 
end; 
21091  401 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

402 
structure Orders: ORDERS = 
21248  403 
struct 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

404 

56508  405 
(* context data *) 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

406 

448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

407 
fun struct_eq ((s1: string, ts1), (s2, ts2)) = 
56508  408 
s1 = s2 andalso eq_list (op aconv) (ts1, ts2); 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

409 

33519  410 
structure Data = Generic_Data 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

411 
( 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

412 
type T = ((string * term list) * Order_Tac.less_arith) list; 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

413 
(* Order structures: 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

414 
identifier of the structure, list of operations and record of theorems 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

415 
needed to set up the transitivity reasoner, 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

416 
identifier and operations identify the structure uniquely. *) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

417 
val empty = []; 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

418 
val extend = I; 
33519  419 
fun merge data = AList.join struct_eq (K fst) data; 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

420 
); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

421 

448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

422 
fun print_structures ctxt = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

423 
let 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

424 
val structs = Data.get (Context.Proof ctxt); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

425 
fun pretty_term t = Pretty.block 
24920  426 
[Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1, 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

427 
Pretty.str "::", Pretty.brk 1, 
24920  428 
Pretty.quote (Syntax.pretty_typ ctxt (type_of t))]; 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

429 
fun pretty_struct ((s, ts), _) = Pretty.block 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

430 
[Pretty.str s, Pretty.str ":", Pretty.brk 1, 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

431 
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))]; 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

432 
in 
51579  433 
Pretty.writeln (Pretty.big_list "order structures:" (map pretty_struct structs)) 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

434 
end; 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

435 

56508  436 
val _ = 
437 
Outer_Syntax.improper_command @{command_spec "print_orders"} 

438 
"print order structures available to transitivity reasoner" 

439 
(Scan.succeed (Toplevel.unknown_context o 

440 
Toplevel.keep (print_structures o Toplevel.context_of))); 

21091  441 

56508  442 

443 
(* tactics *) 

444 

445 
fun struct_tac ((s, ops), thms) ctxt facts = 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

446 
let 
56508  447 
val [eq, le, less] = ops; 
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29823
diff
changeset

448 
fun decomp thy (@{const Trueprop} $ t) = 
56508  449 
let 
450 
fun excluded t = 

451 
(* exclude numeric types: linear arithmetic subsumes transitivity *) 

452 
let val T = type_of t 

453 
in 

454 
T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT 

455 
end; 

456 
fun rel (bin_op $ t1 $ t2) = 

457 
if excluded t1 then NONE 

458 
else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2) 

459 
else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2) 

460 
else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2) 

461 
else NONE 

462 
 rel _ = NONE; 

463 
fun dec (Const (@{const_name Not}, _) $ t) = 

464 
(case rel t of NONE => 

465 
NONE 

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

467 
 dec x = rel x; 

468 
in dec t end 

469 
 decomp _ _ = NONE; 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

470 
in 
56508  471 
(case s of 
472 
"order" => Order_Tac.partial_tac decomp thms ctxt facts 

473 
 "linorder" => Order_Tac.linear_tac decomp thms ctxt facts 

474 
 _ => error ("Unknown order kind " ^ quote s ^ " encountered in transitivity reasoner")) 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

475 
end 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

476 

56508  477 
fun order_tac ctxt facts = 
478 
FIRST' (map (fn s => CHANGED o struct_tac s ctxt facts) (Data.get (Context.Proof ctxt))); 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

479 

448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

480 

56508  481 
(* attributes *) 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

482 

448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

483 
fun add_struct_thm s tag = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

484 
Thm.declaration_attribute 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

485 
(fn thm => Data.map (AList.map_default struct_eq (s, Order_Tac.empty TrueI) (Order_Tac.update tag thm))); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

486 
fun del_struct s = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

487 
Thm.declaration_attribute 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

488 
(fn _ => Data.map (AList.delete struct_eq s)); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

489 

24867  490 
val _ = 
56508  491 
Theory.setup 
492 
(Attrib.setup @{binding order} 

493 
(Scan.lift ((Args.add  Args.name >> (fn (_, s) => SOME s)  Args.del >> K NONE)  

494 
Args.colon (* FIXME  Scan.succeed true *) )  Scan.lift Args.name  

495 
Scan.repeat Args.term 

496 
>> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag 

497 
 ((NONE, n), ts) => del_struct (n, ts))) 

498 
"theorems controlling transitivity reasoner"); 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

499 

21091  500 
end; 
501 
*} 

502 

47432  503 
method_setup order = {* 
504 
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt [])) 

505 
*} "transitivity reasoner" 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

506 

448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

507 

448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

508 
text {* Declarations to set up transitivity reasoner of partial and linear orders. *} 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

509 

25076  510 
context order 
511 
begin 

512 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

513 
(* The type constraint on @{term op =} below is necessary since the operation 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

514 
is not a parameter of the locale. *) 
25076  515 

27689  516 
declare less_irrefl [THEN notE, order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] 
517 

518 
declare order_refl [order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

519 

520 
declare less_imp_le [order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

521 

522 
declare antisym [order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

523 

524 
declare eq_refl [order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

525 

526 
declare sym [THEN eq_refl, order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

527 

528 
declare less_trans [order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

529 

530 
declare less_le_trans [order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

531 

532 
declare le_less_trans [order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

533 

534 
declare order_trans [order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

535 

536 
declare le_neq_trans [order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

537 

538 
declare neq_le_trans [order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

539 

540 
declare less_imp_neq [order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

541 

542 
declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

543 

544 
declare not_sym [order add not_sym: order "op = :: 'a => 'a => bool" "op <=" "op <"] 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

545 

25076  546 
end 
547 

548 
context linorder 

549 
begin 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

550 

27689  551 
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] 
552 

553 
declare less_irrefl [THEN notE, order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

554 

555 
declare order_refl [order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

556 

557 
declare less_imp_le [order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

558 

559 
declare not_less [THEN iffD2, order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

560 

561 
declare not_le [THEN iffD2, order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

562 

563 
declare not_less [THEN iffD1, order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

564 

565 
declare not_le [THEN iffD1, order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

566 

567 
declare antisym [order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

568 

569 
declare eq_refl [order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

25076  570 

27689  571 
declare sym [THEN eq_refl, order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 
572 

573 
declare less_trans [order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

574 

575 
declare less_le_trans [order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

576 

577 
declare le_less_trans [order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

578 

579 
declare order_trans [order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

580 

581 
declare le_neq_trans [order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

582 

583 
declare neq_le_trans [order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

584 

585 
declare less_imp_neq [order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

586 

587 
declare eq_neq_eq_imp_neq [order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

588 

589 
declare not_sym [order add not_sym: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] 

24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

590 

25076  591 
end 
592 

21083  593 
setup {* 
56509  594 
map_theory_simpset (fn ctxt0 => ctxt0 addSolver 
595 
mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt))) 

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

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

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

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

600 
*} 

15524  601 

56509  602 
ML {* 
603 
local 

604 
fun prp t thm = Thm.prop_of thm = t; (* FIXME proper aconv!? *) 

605 
in 

15524  606 

56509  607 
fun antisym_le_simproc ctxt ct = 
608 
(case term_of ct of 

609 
(le as Const (_, T)) $ r $ s => 

610 
(let 

611 
val prems = Simplifier.prems_of ctxt; 

612 
val less = Const (@{const_name less}, T); 

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

614 
in 

615 
(case find_first (prp t) prems of 

616 
NONE => 

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

618 
(case find_first (prp t) prems of 

619 
NONE => NONE 

620 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1}))) 

621 
end 

622 
 SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv}))) 

623 
end handle THM _ => NONE) 

624 
 _ => NONE); 

15524  625 

56509  626 
fun antisym_less_simproc ctxt ct = 
627 
(case term_of ct of 

628 
NotC $ ((less as Const(_,T)) $ r $ s) => 

629 
(let 

630 
val prems = Simplifier.prems_of ctxt; 

631 
val le = Const (@{const_name less_eq}, T); 

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

633 
in 

634 
(case find_first (prp t) prems of 

635 
NONE => 

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

637 
(case find_first (prp t) prems of 

638 
NONE => NONE 

639 
 SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3}))) 

640 
end 

641 
 SOME thm => SOME (mk_meta_eq (thm RS @{thm linorder_class.antisym_conv2}))) 

642 
end handle THM _ => NONE) 

643 
 _ => NONE); 

21083  644 

56509  645 
end; 
21083  646 
*} 
15524  647 

56509  648 
simproc_setup antisym_le ("(x::'a::order) \<le> y") = "K antisym_le_simproc" 
649 
simproc_setup antisym_less ("\<not> (x::'a::linorder) < y") = "K antisym_less_simproc" 

650 

15524  651 

21083  652 
subsection {* Bounded quantifiers *} 
653 

654 
syntax 

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

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

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

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

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

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

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

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

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

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

665 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

676 
syntax (HOL) 

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

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

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

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

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

682 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

693 
translations 

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

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

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

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

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

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

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

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

702 

703 
print_translation {* 

704 
let 

42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42284
diff
changeset

705 
val All_binder = Mixfix.binder_name @{const_syntax All}; 
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42284
diff
changeset

706 
val Ex_binder = Mixfix.binder_name @{const_syntax Ex}; 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38715
diff
changeset

707 
val impl = @{const_syntax HOL.implies}; 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

708 
val conj = @{const_syntax HOL.conj}; 
22916  709 
val less = @{const_syntax less}; 
710 
val less_eq = @{const_syntax less_eq}; 

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

711 

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

712 
val trans = 
35115  713 
[((All_binder, impl, less), 
714 
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})), 

715 
((All_binder, impl, less_eq), 

716 
(@{syntax_const "_All_less_eq"}, @{syntax_const "_All_greater_eq"})), 

717 
((Ex_binder, conj, less), 

718 
(@{syntax_const "_Ex_less"}, @{syntax_const "_Ex_greater"})), 

719 
((Ex_binder, conj, less_eq), 

720 
(@{syntax_const "_Ex_less_eq"}, @{syntax_const "_Ex_greater_eq"}))]; 

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

721 

35115  722 
fun matches_bound v t = 
723 
(case t of 

35364  724 
Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v' 
35115  725 
 _ => false); 
726 
fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v  _ => false); 

49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
48891
diff
changeset

727 
fun mk x c n P = Syntax.const c $ Syntax_Trans.mark_bound_body x $ n $ P; 
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

728 

52143  729 
fun tr' q = (q, fn _ => 
730 
(fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T), 

35364  731 
Const (c, _) $ (Const (d, _) $ t $ u) $ P] => 
35115  732 
(case AList.lookup (op =) trans (q, c, d) of 
733 
NONE => raise Match 

734 
 SOME (l, g) => 

49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
48891
diff
changeset

735 
if matches_bound v t andalso not (contains_var v u) then mk (v, T) l u P 
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
48891
diff
changeset

736 
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P 
35115  737 
else raise Match) 
52143  738 
 _ => raise Match)); 
21524  739 
in [tr' All_binder, tr' Ex_binder] end 
21083  740 
*} 
741 

742 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

743 
subsection {* Transitivity reasoning *} 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

744 

25193  745 
context ord 
746 
begin 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

747 

25193  748 
lemma ord_le_eq_trans: "a \<le> b \<Longrightarrow> b = c \<Longrightarrow> a \<le> c" 
749 
by (rule subst) 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

750 

25193  751 
lemma ord_eq_le_trans: "a = b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c" 
752 
by (rule ssubst) 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

753 

25193  754 
lemma ord_less_eq_trans: "a < b \<Longrightarrow> b = c \<Longrightarrow> a < c" 
755 
by (rule subst) 

756 

757 
lemma ord_eq_less_trans: "a = b \<Longrightarrow> b < c \<Longrightarrow> a < c" 

758 
by (rule ssubst) 

759 

760 
end 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

761 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

762 
lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

763 
(!!x y. x < y ==> f x < f y) ==> f a < c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

764 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

765 
assume r: "!!x y. x < y ==> f x < f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

766 
assume "a < b" hence "f a < f b" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

767 
also assume "f b < c" 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

768 
finally (less_trans) show ?thesis . 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

769 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

770 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

771 
lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

772 
(!!x y. x < y ==> f x < f y) ==> a < f c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

773 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

774 
assume r: "!!x y. x < y ==> f x < f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

775 
assume "a < f b" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

776 
also assume "b < c" hence "f b < f c" by (rule r) 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

777 
finally (less_trans) show ?thesis . 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

778 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

779 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

780 
lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

781 
(!!x y. x <= y ==> f x <= f y) ==> f a < c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

782 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

783 
assume r: "!!x y. x <= y ==> f x <= f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

784 
assume "a <= b" hence "f a <= f b" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

785 
also assume "f b < c" 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

786 
finally (le_less_trans) show ?thesis . 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

787 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

788 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

789 
lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

790 
(!!x y. x < y ==> f x < f y) ==> a < f c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

791 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

792 
assume r: "!!x y. x < y ==> f x < f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

793 
assume "a <= f b" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

794 
also assume "b < c" hence "f b < f c" by (rule r) 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

795 
finally (le_less_trans) show ?thesis . 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

796 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

797 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

798 
lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

799 
(!!x y. x < y ==> f x < f y) ==> f a < c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

800 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

801 
assume r: "!!x y. x < y ==> f x < f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

802 
assume "a < b" hence "f a < f b" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

803 
also assume "f b <= c" 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

804 
finally (less_le_trans) show ?thesis . 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

805 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

806 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

807 
lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

808 
(!!x y. x <= y ==> f x <= f y) ==> a < f c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

809 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

810 
assume r: "!!x y. x <= y ==> f x <= f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

811 
assume "a < f b" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

812 
also assume "b <= c" hence "f b <= f c" by (rule r) 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

813 
finally (less_le_trans) show ?thesis . 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

814 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

815 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

816 
lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

817 
(!!x y. x <= y ==> f x <= f y) ==> a <= f c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

818 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

819 
assume r: "!!x y. x <= y ==> f x <= f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

820 
assume "a <= f b" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

821 
also assume "b <= c" hence "f b <= f c" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

822 
finally (order_trans) show ?thesis . 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

823 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

824 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

825 
lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

826 
(!!x y. x <= y ==> f x <= f y) ==> f a <= c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

827 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

828 
assume r: "!!x y. x <= y ==> f x <= f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

829 
assume "a <= b" hence "f a <= f b" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

830 
also assume "f b <= c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

831 
finally (order_trans) show ?thesis . 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

832 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

833 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

834 
lemma ord_le_eq_subst: "a <= b ==> f b = c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

835 
(!!x y. x <= y ==> f x <= f y) ==> f a <= c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

836 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

837 
assume r: "!!x y. x <= y ==> f x <= f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

838 
assume "a <= b" hence "f a <= f b" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

839 
also assume "f b = c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

840 
finally (ord_le_eq_trans) show ?thesis . 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

841 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

842 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

843 
lemma ord_eq_le_subst: "a = f b ==> b <= c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

844 
(!!x y. x <= y ==> f x <= f y) ==> a <= f c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

845 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

846 
assume r: "!!x y. x <= y ==> f x <= f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

847 
assume "a = f b" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

848 
also assume "b <= c" hence "f b <= f c" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

849 
finally (ord_eq_le_trans) show ?thesis . 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

850 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

851 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

852 
lemma ord_less_eq_subst: "a < b ==> f b = c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

853 
(!!x y. x < y ==> f x < f y) ==> f a < c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

854 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

855 
assume r: "!!x y. x < y ==> f x < f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

856 
assume "a < b" hence "f a < f b" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

857 
also assume "f b = c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

858 
finally (ord_less_eq_trans) show ?thesis . 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

859 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

860 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

861 
lemma ord_eq_less_subst: "a = f b ==> b < c ==> 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

862 
(!!x y. x < y ==> f x < f y) ==> a < f c" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

863 
proof  
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

864 
assume r: "!!x y. x < y ==> f x < f y" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

865 
assume "a = f b" 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

866 
also assume "b < c" hence "f b < f c" by (rule r) 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

867 
finally (ord_eq_less_trans) show ?thesis . 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

868 
qed 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

869 

17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

870 
text {* 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

871 
Note that this list of rules is in reverse order of priorities. 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

872 
*} 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

873 

27682  874 
lemmas [trans] = 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

875 
order_less_subst2 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

876 
order_less_subst1 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

877 
order_le_less_subst2 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

878 
order_le_less_subst1 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

879 
order_less_le_subst2 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

880 
order_less_le_subst1 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

881 
order_subst2 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

882 
order_subst1 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

883 
ord_le_eq_subst 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

884 
ord_eq_le_subst 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

885 
ord_less_eq_subst 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

886 
ord_eq_less_subst 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

887 
forw_subst 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

888 
back_subst 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

889 
rev_mp 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

890 
mp 
27682  891 

892 
lemmas (in order) [trans] = 

893 
neq_le_trans 

894 
le_neq_trans 

895 

896 
lemmas (in preorder) [trans] = 

897 
less_trans 

898 
less_asym' 

899 
le_less_trans 

900 
less_le_trans 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

901 
order_trans 
27682  902 

903 
lemmas (in order) [trans] = 

904 
antisym 

905 

906 
lemmas (in ord) [trans] = 

907 
ord_le_eq_trans 

908 
ord_eq_le_trans 

909 
ord_less_eq_trans 

910 
ord_eq_less_trans 

911 

912 
lemmas [trans] = 

913 
trans 

914 

915 
lemmas order_trans_rules = 

916 
order_less_subst2 

917 
order_less_subst1 

918 
order_le_less_subst2 

919 
order_le_less_subst1 

920 
order_less_le_subst2 

921 
order_less_le_subst1 

922 
order_subst2 

923 
order_subst1 

924 
ord_le_eq_subst 

925 
ord_eq_le_subst 

926 
ord_less_eq_subst 

927 
ord_eq_less_subst 

928 
forw_subst 

929 
back_subst 

930 
rev_mp 

931 
mp 

932 
neq_le_trans 

933 
le_neq_trans 

934 
less_trans 

935 
less_asym' 

936 
le_less_trans 

937 
less_le_trans 

938 
order_trans 

939 
antisym 

21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

940 
ord_le_eq_trans 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

941 
ord_eq_le_trans 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

942 
ord_less_eq_trans 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

943 
ord_eq_less_trans 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

944 
trans 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

945 

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

948 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

949 
lemma xt1 [no_atp]: 
21083  950 
"a = b ==> b > c ==> a > c" 
951 
"a > b ==> b = c ==> a > c" 

952 
"a = b ==> b >= c ==> a >= c" 

953 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  958 
"(a::'a::order) > b ==> b > a ==> P" 
21083  959 
"(x::'a::order) > y ==> y > z ==> x > z" 
960 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  966 
by auto 
21083  967 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

968 
lemma xt2 [no_atp]: 
21083  969 
"(a::'a::order) >= f b ==> b >= c ==> (!!x y. x >= y ==> f x >= f y) ==> a >= f c" 
970 
by (subgoal_tac "f b >= f c", force, force) 

971 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

972 
lemma xt3 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) >= c ==> 
21083  973 
(!!x y. x >= y ==> f x >= f y) ==> f a >= c" 
974 
by (subgoal_tac "f a >= f b", force, force) 

975 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

976 
lemma xt4 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) >= c ==> 
21083  977 
(!!x y. x >= y ==> f x >= f y) ==> a > f c" 
978 
by (subgoal_tac "f b >= f c", force, force) 

979 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

980 
lemma xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==> 
21083  981 
(!!x y. x > y ==> f x > f y) ==> f a > c" 
982 
by (subgoal_tac "f a > f b", force, force) 

983 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

984 
lemma xt6 [no_atp]: "(a::'a::order) >= f b ==> b > c ==> 
21083  985 
(!!x y. x > y ==> f x > f y) ==> a > f c" 
986 
by (subgoal_tac "f b > f c", force, force) 

987 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

988 
lemma xt7 [no_atp]: "(a::'a::order) >= b ==> (f b::'b::order) > c ==> 
21083  989 
(!!x y. x >= y ==> f x >= f y) ==> f a > c" 
990 
by (subgoal_tac "f a >= f b", force, force) 

991 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

992 
lemma xt8 [no_atp]: "(a::'a::order) > f b ==> (b::'b::order) > c ==> 
21083  993 
(!!x y. x > y ==> f x > f y) ==> a > f c" 
994 
by (subgoal_tac "f b > f c", force, force) 

995 

45221
3eadb9b6a055
mark "xt..." rules as "no_atp", since they are easy consequences of other better named properties
blanchet
parents:
44921
diff
changeset

996 
lemma xt9 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) > c ==> 
21083  997 
(!!x y. x > y ==> f x > f y) ==> f a > c" 
998 
by (subgoal_tac "f a > f b", force, force) 

999 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53216
diff
changeset

1000 
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 
21083  1001 

1002 
(* 

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

1004 
for the wrong thing in an Isar proof. 

1005 

1006 
The extra transitivity rules can be used as follows: 

1007 

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

1009 
proof  

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

1011 
sorry 

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

1013 
sorry 

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

1015 
sorry 

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

1017 
sorry 

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

1019 
sorry 

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

1021 
sorry 

1022 
finally (xtrans) show ?thesis . 

1023 
qed 

1024 

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

1026 
leave out the "(xtrans)" above. 

1027 
*) 

1028 

23881  1029 

54860  1030 
subsection {* Monotonicity *} 
21083  1031 

25076  1032 
context order 
1033 
begin 

1034 

30298  1035 
definition mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where 
25076  1036 
"mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)" 
1037 

1038 
lemma monoI [intro?]: 

1039 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 

1040 
shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f" 

1041 
unfolding mono_def by iprover 

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

1042 

25076  1043 
lemma monoD [dest?]: 
1044 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 

1045 
shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 

1046 
unfolding mono_def by iprover 

1047 

51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1048 
lemma monoE: 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1049 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1050 
assumes "mono f" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1051 
assumes "x \<le> y" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1052 
obtains "f x \<le> f y" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1053 
proof 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1054 
from assms show "f x \<le> f y" by (simp add: mono_def) 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1055 
qed 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1056 

56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1057 
definition antimono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1058 
"antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1059 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1060 
lemma antimonoI [intro?]: 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1061 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1062 
shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<ge> f y) \<Longrightarrow> antimono f" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1063 
unfolding antimono_def by iprover 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1064 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1065 
lemma antimonoD [dest?]: 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1066 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1067 
shows "antimono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1068 
unfolding antimono_def by iprover 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1069 

f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1070 
lemma antimonoE: 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1071 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1072 
assumes "antimono f" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1073 
assumes "x \<le> y" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1074 
obtains "f x \<ge> f y" 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1075 
proof 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1076 
from assms show "f x \<ge> f y" by (simp add: antimono_def) 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1077 
qed 
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
54868
diff
changeset

1078 

30298  1079 
definition strict_mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" where 
1080 
"strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)" 

1081 

1082 
lemma strict_monoI [intro?]: 

1083 
assumes "\<And>x y. x < y \<Longrightarrow> f x < f y" 

1084 
shows "strict_mono f" 

1085 
using assms unfolding strict_mono_def by auto 

1086 

1087 
lemma strict_monoD [dest?]: 

1088 
"strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y" 

1089 
unfolding strict_mono_def by auto 

1090 

1091 
lemma strict_mono_mono [dest?]: 

1092 
assumes "strict_mono f" 

1093 
shows "mono f" 

1094 
proof (rule monoI) 

1095 
fix x y 

1096 
assume "x \<le> y" 

1097 
show "f x \<le> f y" 

1098 
proof (cases "x = y") 

1099 
case True then show ?thesis by simp 

1100 
next 

1101 
case False with `x \<le> y` have "x < y" by simp 

1102 
with assms strict_monoD have "f x < f y" by auto 

1103 
then show ?thesis by simp 

1104 
qed 

1105 
qed 

1106 

25076  1107 
end 
1108 

1109 
context linorder 

1110 
begin 

1111 

51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1112 
lemma mono_invE: 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1113 
fixes f :: "'a \<Rightarrow> 'b\<Colon>order" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1114 
assumes "mono f" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1115 
assumes "f x < f y" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1116 
obtains "x \<le> y" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1117 
proof 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1118 
show "x \<le> y" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1119 
proof (rule ccontr) 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1120 
assume "\<not> x \<le> y" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1121 
then have "y \<le> x" by simp 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1122 
with `mono f` obtain "f y \<le> f x" by (rule monoE) 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1123 
with `f x < f y` show False by simp 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1124 
qed 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1125 
qed 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

1126 

30298  1127 
lemma strict_mono_eq: 
1128 
assumes "strict_mono f" 

1129 
shows "f x = f y \<longleftrightarrow> x = y" 

1130 
proof 

1131 
assume "f x = f y" 

1132 
show "x = y" proof (cases x y rule: linorder_cases) 

1133 
case less with assms strict_monoD have "f x < f y" by auto 

1134 
with `f x = f y` show ?thesis by simp 

1135 
next 

1136 
case equal then show ?thesis . 

1137 
next 

1138 
case greater with assms strict_monoD have "f y < f x" by auto 

1139 
with `f x = f y` show ?thesis by simp 

1140 
qed 

1141 
qed simp 

1142 

1143 
lemma strict_mono_less_eq: 

1144 
assumes "strict_mono f" 

1145 
shows "f x \<le> f y \<longleftrightarrow> x \<le> y" 

1146 
proof 

1147 
assume "x \<le> y" 

1148 
with assms strict_mono_mono monoD show "f x \<le> f y" by auto 

1149 
next 

1150 
assume "f x \<le> f y" 

1151 
show "x \<le> y" proof (rule ccontr) 

1152 
assume "\<not> x \<le> y" then have "y < x" by simp 

1153 
with assms strict_monoD have "f y < f x" by auto 

1154 
with `f x \<le> f y` show False by simp 

1155 
qed 

1156 
qed 

1157 

1158 
lemma strict_mono_less: 

1159 
assumes "strict_mono f" 

1160 
shows "f x < f y \<longleftrightarrow> x < y" 

1161 
using assms 

1162 
by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq) 

1163 

54860  1164 
end 
1165 

1166 

54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54860
diff
changeset

1167 
subsection {* min and max  fundamental *} 
54860  1168 

1169 
definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

1170 
"min a b = (if a \<le> b then a else b)" 

1171 

1172 
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

1173 
"max a b = (if a \<le> b then b else a)" 

1174 

45931  1175 
lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x" 
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54860
diff
changeset

1176 
by (simp add: min_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1177 

54857  1178 
lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y" 
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54860
diff
changeset

1179 
by (simp add: max_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1180 

45931  1181 
lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y" 
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54860
diff
changeset

1182 
by (simp add:min_def) 
45893  1183 

45931  1184 
lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x" 
54861
00d551179872
postponed min/max lemmas until abstract lattice is available
haftmann
parents:
54860
diff
changeset

1185 
by (simp add: max_def) 
45893  1186 

1187 

43813
07f0650146f2
tightened specification of classes bot and top: uniqueness of top and bot elements
haftmann
parents:
43597
diff
changeset

1188 
subsection {* (Unique) top and bottom elements *} 
28685  1189 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52143
diff
changeset

1190 
class bot = 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1191 
fixes bot :: 'a ("\<bottom>") 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52143
diff
changeset

1192 

412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52143
diff
changeset

1193 
class order_bot = order + bot + 
51487  1194 
assumes bot_least: "\<bottom> \<le> a" 
54868  1195 
begin 
51487  1196 

54868  1197 
sublocale bot!: ordering_top greater_eq greater bot 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

1198 
by default (fact bot_least) 
51487  1199 

43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1200 
lemma le_bot: 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1201 
"a \<le> \<bottom> \<Longrightarrow> a = \<bottom>" 
51487  1202 
by (fact bot.extremum_uniqueI) 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1203 

43816  1204 
lemma bot_unique: 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1205 
"a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>" 
51487  1206 
by (fact bot.extremum_unique) 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1207 

51487  1208 
lemma not_less_bot: 
1209 
"\<not> a < \<bottom>" 

1210 
by (fact bot.extremum_strict) 

43816  1211 

43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1212 
lemma bot_less: 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1213 
"a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a" 
51487  1214 
by (fact bot.not_eq_extremum) 
43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1215 

58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1216 
end 
41082  1217 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52143
diff
changeset

1218 
class top = 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1219 
fixes top :: 'a ("\<top>") 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52143
diff
changeset

1220 

412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52143
diff
changeset

1221 
class order_top = order + top + 
51487  1222 
assumes top_greatest: "a \<le> \<top>" 
54868  1223 
begin 
51487  1224 

54868  1225 
sublocale top!: ordering_top less_eq less top 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

1226 
by default (fact top_greatest) 
51487  1227 

43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1228 
lemma top_le: 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1229 
"\<top> \<le> a \<Longrightarrow> a = \<top>" 
51487  1230 
by (fact top.extremum_uniqueI) 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1231 

43816  1232 
lemma top_unique: 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1233 
"\<top> \<le> a \<longleftrightarrow> a = \<top>" 
51487  1234 
by (fact top.extremum_unique) 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1235 

51487  1236 
lemma not_top_less: 
1237 
"\<not> \<top> < a" 

1238 
by (fact top.extremum_strict) 

43816  1239 

43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1240 
lemma less_top: 
43853
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1241 
"a \<noteq> \<top> \<longleftrightarrow> a < \<top>" 
51487  1242 
by (fact top.not_eq_extremum) 
43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1243 

58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1244 
end 
28685  1245 

1246 

27823  1247 
subsection {* Dense orders *} 
1248 

53216  1249 
class dense_order = order + 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1250 
assumes dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1251 

53216  1252 
class dense_linorder = linorder + dense_order 
35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1253 
begin 
27823  1254 

35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1255 
lemma dense_le: 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1256 
fixes y z :: 'a 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1257 
assumes "\<And>x. x < y \<Longrightarrow> x \<le> z" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1258 
shows "y \<le> z" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1259 
proof (rule ccontr) 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1260 
assume "\<not> ?thesis" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1261 
hence "z < y" by simp 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1262 
from dense[OF this] 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1263 
obtain x where "x < y" and "z < x" by safe 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1264 
moreover have "x \<le> z" using assms[OF `x < y`] . 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1265 
ultimately show False by auto 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1266 
qed 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1267 

cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1268 
lemma dense_le_bounded: 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1269 
fixes x y z :: 'a 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1270 
assumes "x < y" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1271 
assumes *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1272 
shows "y \<le> z" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1273 
proof (rule dense_le) 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1274 
fix w assume "w < y" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1275 
from dense[OF `x < y`] obtain u where "x < u" "u < y" by safe 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1276 
from linear[of u w] 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1277 
show "w \<le> z" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1278 
proof (rule disjE) 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1279 
assume "u \<le> w" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1280 
from less_le_trans[OF `x < u` `u \<le> w`] `w < y` 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1281 
show "w \<le> z" by (rule *) 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1282 
next 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1283 
assume "w \<le> u" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1284 
from `w \<le> u` *[OF `x < u` `u < y`] 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1285 
show "w \<le> z" by (rule order_trans) 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1286 
qed 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1287 
qed 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1288 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1289 
lemma dense_ge: 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1290 
fixes y z :: 'a 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1291 
assumes "\<And>x. z < x \<Longrightarrow> y \<le> x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1292 
shows "y \<le> z" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1293 
proof (rule ccontr) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1294 
assume "\<not> ?thesis" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1295 
hence "z < y" by simp 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1296 
from dense[OF this] 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1297 
obtain x where "x < y" and "z < x" by safe 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1298 
moreover have "y \<le> x" using assms[OF `z < x`] . 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1299 
ultimately show False by auto 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1300 
qed 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1301 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1302 
lemma dense_ge_bounded: 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1303 
fixes x y z :: 'a 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1304 
assumes "z < x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1305 
assumes *: "\<And>w. \<lbrakk> z < w ; w < x \<rbrakk> \<Longrightarrow> y \<le> w" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1306 
shows "y \<le> z" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1307 
proof (rule dense_ge) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1308 
fix w assume "z < w" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1309 
from dense[OF `z < x`] obtain u where "z < u" "u < x" by safe 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1310 
from linear[of u w] 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1311 
show "y \<le> w" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1312 
proof (rule disjE) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1313 
assume "w \<le> u" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1314 
from `z < w` le_less_trans[OF `w \<le> u` `u < x`] 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1315 
show "y \<le> w" by (rule *) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1316 
next 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset
