author  wenzelm 
Fri, 09 Oct 2015 20:26:03 +0200  
changeset 61378  3e04c9ca001a 
parent 61169  4de9ff3ea29a 
child 61605  1bf7b186542e 
permissions  rwrr 
28685  1 
(* Title: HOL/Orderings.thy 
15524  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

4 

60758  5 
section \<open>Abstract orderings\<close> 
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 

60758  15 
subsection \<open>Abstract ordering\<close> 
51487  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" 

60758  21 
assumes refl: "a \<preceq> a"  \<open>not @{text iff}: makes problems due to multiple (dual) interpretations\<close> 
51487  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 

60758  42 
lemma irrefl:  \<open>not @{text iff}: makes problems due to multiple (dual) interpretations\<close> 
51487  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 

60758  88 
subsection \<open>Syntactic orders\<close> 
35092
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 
abbreviation (input) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

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

107 
"x >= y \<equiv> y <= x" 
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 
notation (input) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

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

111 

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

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

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

114 
"x > y \<equiv> y < x" 
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 
end 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35028
diff
changeset

117 

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

118 

60758  119 
subsection \<open>Quasi orders\<close> 
15524  120 

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

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

21248  125 
begin 
126 

60758  127 
text \<open>Reflexivity.\<close> 
15524  128 

25062  129 
lemma eq_refl: "x = y \<Longrightarrow> x \<le> y" 
60758  130 
 \<open>This form is useful with the classical reasoner.\<close> 
23212  131 
by (erule ssubst) (rule order_refl) 
15524  132 

25062  133 
lemma less_irrefl [iff]: "\<not> x < x" 
27682  134 
by (simp add: less_le_not_le) 
135 

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

137 
unfolding less_le_not_le by blast 

138 

139 

60758  140 
text \<open>Asymmetry.\<close> 
27682  141 

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

143 
by (simp add: less_le_not_le) 

144 

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

146 
by (drule less_not_sym, erule contrapos_np) simp 

147 

148 

60758  149 
text \<open>Transitivity.\<close> 
27682  150 

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

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

153 

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

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

156 

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

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

159 

160 

60758  161 
text \<open>Useful for simplification, but too risky to include by default.\<close> 
27682  162 

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

164 
by (blast elim: less_asym) 

165 

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

167 
by (blast elim: less_asym) 

168 

169 

60758  170 
text \<open>Transitivity rules for calculational reasoning\<close> 
27682  171 

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

173 
by (rule less_asym) 

174 

175 

60758  176 
text \<open>Dual order\<close> 
27682  177 

178 
lemma dual_preorder: 

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

179 
"class.preorder (op \<ge>) (op >)" 
28823  180 
proof qed (auto simp add: less_le_not_le intro: order_trans) 
27682  181 

182 
end 

183 

184 

60758  185 
subsection \<open>Partial orders\<close> 
27682  186 

187 
class order = preorder + 

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

189 
begin 

190 

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

193 

54868  194 
sublocale order!: ordering less_eq less + dual_order!: ordering greater_eq greater 
61169  195 
by standard (auto intro: antisym order_trans simp add: less_le) 
51487  196 

197 

60758  198 
text \<open>Reflexivity.\<close> 
15524  199 

25062  200 
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y" 
60758  201 
 \<open>NOT suitable for iff, since it can cause PROOF FAILED.\<close> 
51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

202 
by (fact order.order_iff_strict) 
15524  203 

25062  204 
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y" 
23212  205 
unfolding less_le by blast 
15524  206 

21329  207 

60758  208 
text \<open>Useful for simplification, but too risky to include by default.\<close> 
21329  209 

25062  210 
lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 
23212  211 
by auto 
21329  212 

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

216 

60758  217 
text \<open>Transitivity rules for calculational reasoning\<close> 
21329  218 

25062  219 
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

220 
by (fact order.not_eq_order_implies_strict) 
21329  221 

25062  222 
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

223 
by (rule order.not_eq_order_implies_strict) 
21329  224 

15524  225 

60758  226 
text \<open>Asymmetry.\<close> 
15524  227 

25062  228 
lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x" 
23212  229 
by (blast intro: antisym) 
15524  230 

25062  231 
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y" 
23212  232 
by (blast intro: antisym) 
15524  233 

25062  234 
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

235 
by (fact order.strict_implies_not_eq) 
21248  236 

21083  237 

60758  238 
text \<open>Least value operator\<close> 
27107  239 

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

243 

244 
lemma Least_equality: 

245 
assumes "P x" 

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

247 
shows "Least P = x" 

248 
unfolding Least_def by (rule the_equality) 

249 
(blast intro: assms antisym)+ 

250 

251 
lemma LeastI2_order: 

252 
assumes "P x" 

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

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

255 
shows "Q (Least P)" 

256 
unfolding Least_def by (rule theI2) 

257 
(blast intro: assms antisym)+ 

258 

259 

60758  260 
text \<open>Dual order\<close> 
22916  261 

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

263 
"class.order (op \<ge>) (op >)" 
27682  264 
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym) 
22916  265 

21248  266 
end 
15524  267 

21329  268 

60758  269 
text \<open>Alternative introduction rule with bias towards strict order\<close> 
56545  270 

271 
lemma order_strictI: 

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

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

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

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

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

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

278 
shows "class.order less_eq less" 

279 
proof 

280 
fix a b 

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

282 
by (auto simp add: less_eq_less asym irrefl) 

283 
next 

284 
fix a 

285 
show "a \<sqsubseteq> a" 

286 
by (auto simp add: less_eq_less) 

287 
next 

288 
fix a b c 

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

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

291 
next 

292 
fix a b 

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

294 
by (auto simp add: less_eq_less asym) 

295 
qed 

296 

297 

60758  298 
subsection \<open>Linear (total) orders\<close> 
21329  299 

22316  300 
class linorder = order + 
25207  301 
assumes linear: "x \<le> y \<or> y \<le> x" 
21248  302 
begin 
303 

25062  304 
lemma less_linear: "x < y \<or> x = y \<or> y < x" 
23212  305 
unfolding less_le using less_le linear by blast 
21248  306 

25062  307 
lemma le_less_linear: "x \<le> y \<or> y < x" 
23212  308 
by (simp add: le_less less_linear) 
21248  309 

310 
lemma le_cases [case_names le ge]: 

25062  311 
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  312 
using linear by blast 
21248  313 

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

314 
lemma linorder_cases [case_names less equal greater]: 
25062  315 
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  316 
using less_linear by blast 
21248  317 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
56545
diff
changeset

318 
lemma linorder_wlog[case_names le sym]: 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
56545
diff
changeset

319 
"(\<And>a b. a \<le> b \<Longrightarrow> P a b) \<Longrightarrow> (\<And>a b. P b a \<Longrightarrow> P a b) \<Longrightarrow> P a b" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
56545
diff
changeset

320 
by (cases rule: le_cases[of a b]) blast+ 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
56545
diff
changeset

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 

60758  363 
text \<open>Dual order\<close> 
22916  364 

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

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

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

21248  369 
end 
370 

23948  371 

60758  372 
text \<open>Alternative introduction rule with bias towards strict order\<close> 
56545  373 

374 
lemma linorder_strictI: 

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

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

377 
assumes "class.order less_eq less" 

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

379 
shows "class.linorder less_eq less" 

380 
proof  

381 
interpret order less_eq less 

60758  382 
by (fact \<open>class.order less_eq less\<close>) 
56545  383 
show ?thesis 
384 
proof 

385 
fix a b 

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

387 
using trichotomy by (auto simp add: le_less) 

388 
qed 

389 
qed 

390 

391 

60758  392 
subsection \<open>Reasoning tools setup\<close> 
21083  393 

60758  394 
ML \<open> 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

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

397 
val print_structures: Proof.context > unit 
32215  398 
val order_tac: Proof.context > thm list > int > tactic 
58826  399 
val add_struct: string * term list > string > attribute 
400 
val del_struct: string * term list > attribute 

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

401 
end; 
21091  402 

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

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

405 

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

407 

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

408 
fun struct_eq ((s1: string, ts1), (s2, ts2)) = 
56508  409 
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

410 

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

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

413 
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

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

415 
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

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

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

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

419 
val extend = I; 
33519  420 
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

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

422 

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

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

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

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

426 
fun pretty_term t = Pretty.block 
24920  427 
[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

428 
Pretty.str "::", Pretty.brk 1, 
24920  429 
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

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

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

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

433 
in 
51579  434 
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

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

436 

56508  437 
val _ = 
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59582
diff
changeset

438 
Outer_Syntax.command @{command_keyword print_orders} 
56508  439 
"print order structures available to transitivity reasoner" 
60097
d20ca79d50e4
discontinued pointless warnings: commands are only defined inside a theory context;
wenzelm
parents:
59936
diff
changeset

440 
(Scan.succeed (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 

58826  483 
fun add_struct s tag = 
24641
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 

21091  490 
end; 
60758  491 
\<close> 
21091  492 

60758  493 
attribute_setup order = \<open> 
58826  494 
Scan.lift ((Args.add  Args.name >> (fn (_, s) => SOME s)  Args.del >> K NONE)  
495 
Args.colon (* FIXME  Scan.succeed true *) )  Scan.lift Args.name  

496 
Scan.repeat Args.term 

497 
>> (fn ((SOME tag, n), ts) => Orders.add_struct (n, ts) tag 

498 
 ((NONE, n), ts) => Orders.del_struct (n, ts)) 

60758  499 
\<close> "theorems controlling transitivity reasoner" 
58826  500 

60758  501 
method_setup order = \<open> 
47432  502 
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt [])) 
60758  503 
\<close> "transitivity reasoner" 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

504 

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

505 

60758  506 
text \<open>Declarations to set up transitivity reasoner of partial and linear orders.\<close> 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

507 

25076  508 
context order 
509 
begin 

510 

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

511 
(* 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

512 
is not a parameter of the locale. *) 
25076  513 

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

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

517 

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

519 

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

521 

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

523 

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

525 

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

527 

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

529 

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

531 

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

533 

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

535 

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

537 

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

539 

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

541 

542 
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

543 

25076  544 
end 
545 

546 
context linorder 

547 
begin 

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

548 

27689  549 
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] 
550 

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

552 

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

554 

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

556 

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

558 

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

560 

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

562 

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

564 

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

566 

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

25076  568 

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

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

572 

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

574 

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

576 

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

578 

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

580 

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

582 

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

584 

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

586 

587 
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

588 

25076  589 
end 
590 

60758  591 
setup \<open> 
56509  592 
map_theory_simpset (fn ctxt0 => ctxt0 addSolver 
593 
mk_solver "Transitivity" (fn ctxt => Orders.order_tac ctxt (Simplifier.prems_of ctxt))) 

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

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

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

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

60758  598 
\<close> 
15524  599 

60758  600 
ML \<open> 
56509  601 
local 
602 
fun prp t thm = Thm.prop_of thm = t; (* FIXME proper aconv!? *) 

603 
in 

15524  604 

56509  605 
fun antisym_le_simproc ctxt ct = 
59582  606 
(case Thm.term_of ct of 
56509  607 
(le as Const (_, T)) $ r $ s => 
608 
(let 

609 
val prems = Simplifier.prems_of ctxt; 

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

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

612 
in 

613 
(case find_first (prp t) prems of 

614 
NONE => 

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

616 
(case find_first (prp t) prems of 

617 
NONE => NONE 

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

619 
end 

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

621 
end handle THM _ => NONE) 

622 
 _ => NONE); 

15524  623 

56509  624 
fun antisym_less_simproc ctxt ct = 
59582  625 
(case Thm.term_of ct of 
56509  626 
NotC $ ((less as Const(_,T)) $ r $ s) => 
627 
(let 

628 
val prems = Simplifier.prems_of ctxt; 

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

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

631 
in 

632 
(case find_first (prp t) prems of 

633 
NONE => 

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

635 
(case find_first (prp t) prems of 

636 
NONE => NONE 

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

638 
end 

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

640 
end handle THM _ => NONE) 

641 
 _ => NONE); 

21083  642 

56509  643 
end; 
60758  644 
\<close> 
15524  645 

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

648 

15524  649 

60758  650 
subsection \<open>Bounded quantifiers\<close> 
21083  651 

652 
syntax 

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

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

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

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

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

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

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

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

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

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

663 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

674 
syntax (HOL) 

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

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

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

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

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

680 
translations 

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

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

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

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

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

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

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

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

689 

60758  690 
print_translation \<open> 
21083  691 
let 
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42284
diff
changeset

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

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

694 
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

695 
val conj = @{const_syntax HOL.conj}; 
22916  696 
val less = @{const_syntax less}; 
697 
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

698 

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

699 
val trans = 
35115  700 
[((All_binder, impl, less), 
701 
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})), 

702 
((All_binder, impl, less_eq), 

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

704 
((Ex_binder, conj, less), 

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

706 
((Ex_binder, conj, less_eq), 

707 
(@{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

708 

35115  709 
fun matches_bound v t = 
710 
(case t of 

35364  711 
Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v' 
35115  712 
 _ => false); 
713 
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

714 
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

715 

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

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

721 
 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

722 
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

723 
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P 
35115  724 
else raise Match) 
52143  725 
 _ => raise Match)); 
21524  726 
in [tr' All_binder, tr' Ex_binder] end 
60758  727 
\<close> 
21083  728 

729 

60758  730 
subsection \<open>Transitivity reasoning\<close> 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

731 

25193  732 
context ord 
733 
begin 

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

734 

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

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

737 

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

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

740 

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

743 

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

745 
by (rule ssubst) 

746 

747 
end 

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

748 

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

749 
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

750 
(!!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

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

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

753 
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

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

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

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

757 

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

758 
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

759 
(!!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

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

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

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

763 
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

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

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

766 

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

767 
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

768 
(!!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

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

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

771 
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

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

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

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

775 

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

776 
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

777 
(!!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

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

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

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

781 
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

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

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

784 

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

785 
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

786 
(!!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

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

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

789 
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

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

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

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

793 

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

794 
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

795 
(!!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

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

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

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

799 
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

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

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

802 

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

803 
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

804 
(!!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

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

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

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

808 
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

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

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

811 

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

812 
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

813 
(!!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

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

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

816 
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

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

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

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

820 

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

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

822 
(!!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

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

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

825 
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

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

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

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

829 

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

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

831 
(!!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

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

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

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

835 
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

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

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

838 

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

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

840 
(!!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

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

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

843 
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

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

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

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

847 

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

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

849 
(!!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

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

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

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

853 
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

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

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

856 

60758  857 
text \<open> 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

858 
Note that this list of rules is in reverse order of priorities. 
60758  859 
\<close> 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

860 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

877 
mp 
27682  878 

879 
lemmas (in order) [trans] = 

880 
neq_le_trans 

881 
le_neq_trans 

882 

883 
lemmas (in preorder) [trans] = 

884 
less_trans 

885 
less_asym' 

886 
le_less_trans 

887 
less_le_trans 

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

888 
order_trans 
27682  889 

890 
lemmas (in order) [trans] = 

891 
antisym 

892 

893 
lemmas (in ord) [trans] = 

894 
ord_le_eq_trans 

895 
ord_eq_le_trans 

896 
ord_less_eq_trans 

897 
ord_eq_less_trans 

898 

899 
lemmas [trans] = 

900 
trans 

901 

902 
lemmas order_trans_rules = 

903 
order_less_subst2 

904 
order_less_subst1 

905 
order_le_less_subst2 

906 
order_le_less_subst1 

907 
order_less_le_subst2 

908 
order_less_le_subst1 

909 
order_subst2 

910 
order_subst1 

911 
ord_le_eq_subst 

912 
ord_eq_le_subst 

913 
ord_less_eq_subst 

914 
ord_eq_less_subst 

915 
forw_subst 

916 
back_subst 

917 
rev_mp 

918 
mp 

919 
neq_le_trans 

920 
le_neq_trans 

921 
less_trans 

922 
less_asym' 

923 
le_less_trans 

924 
less_le_trans 

925 
order_trans 

926 
antisym 

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

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

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

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

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

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

932 

60758  933 
text \<open>These support proving chains of decreasing inequalities 
934 
a >= b >= c ... in Isar proofs.\<close> 

21083  935 

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

936 
lemma xt1 [no_atp]: 
21083  937 
"a = b ==> b > c ==> a > c" 
938 
"a > b ==> b = c ==> a > c" 

939 
"a = b ==> b >= c ==> a >= c" 

940 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  945 
"(a::'a::order) > b ==> b > a ==> P" 
21083  946 
"(x::'a::order) > y ==> y > z ==> x > z" 
947 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  953 
by auto 
21083  954 

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

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

958 

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

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

962 

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

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

966 

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

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

970 

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

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

974 

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

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

978 

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

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

982 

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

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

986 

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

987 
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 
21083  988 

989 
(* 

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

991 
for the wrong thing in an Isar proof. 

992 

993 
The extra transitivity rules can be used as follows: 

994 

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

996 
proof  

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

998 
sorry 

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

1000 
sorry 

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

1002 
sorry 

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

1004 
sorry 

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

1006 
sorry 

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

1008 
sorry 

1009 
finally (xtrans) show ?thesis . 

1010 
qed 

1011 

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

1013 
leave out the "(xtrans)" above. 

1014 
*) 

1015 

23881  1016 

60758  1017 
subsection \<open>Monotonicity\<close> 
21083  1018 

25076  1019 
context order 
1020 
begin 

1021 

61076  1022 
definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where 
25076  1023 
"mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)" 
1024 

1025 
lemma monoI [intro?]: 

61076  1026 
fixes f :: "'a \<Rightarrow> 'b::order" 
25076  1027 
shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f" 
1028 
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

1029 

25076  1030 
lemma monoD [dest?]: 
61076  1031 
fixes f :: "'a \<Rightarrow> 'b::order" 
25076  1032 
shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y" 
1033 
unfolding mono_def by iprover 

1034 

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

1035 
lemma monoE: 
61076  1036 
fixes f :: "'a \<Rightarrow> 'b::order" 
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

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

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

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

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

1041 
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

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

1043 

61076  1044 
definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where 
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

1045 
"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

1046 

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

1047 
lemma antimonoI [intro?]: 
61076  1048 
fixes f :: "'a \<Rightarrow> 'b::order" 
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

1049 
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

1050 
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

1051 

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

1052 
lemma antimonoD [dest?]: 
61076  1053 
fixes f :: "'a \<Rightarrow> 'b::order" 
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

1054 
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

1055 
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

1056 

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 
lemma antimonoE: 
61076  1058 
fixes f :: "'a \<Rightarrow> 'b::order" 
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

1059 
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

1060 
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

1061 
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

1062 
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

1063 
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

1064 
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

1065 

61076  1066 
definition strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where 
30298  1067 
"strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)" 
1068 

1069 
lemma strict_monoI [intro?]: 

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

1071 
shows "strict_mono f" 

1072 
using assms unfolding strict_mono_def by auto 

1073 

1074 
lemma strict_monoD [dest?]: 

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

1076 
unfolding strict_mono_def by auto 

1077 

1078 
lemma strict_mono_mono [dest?]: 

1079 
assumes "strict_mono f" 

1080 
shows "mono f" 

1081 
proof (rule monoI) 

1082 
fix x y 

1083 
assume "x \<le> y" 

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

1085 
proof (cases "x = y") 

1086 
case True then show ?thesis by simp 

1087 
next 

60758  1088 
case False with \<open>x \<le> y\<close> have "x < y" by simp 
30298  1089 
with assms strict_monoD have "f x < f y" by auto 
1090 
then show ?thesis by simp 

1091 
qed 

1092 
qed 

1093 

25076  1094 
end 
1095 

1096 
context linorder 

1097 
begin 

1098 

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

1099 
lemma mono_invE: 
61076  1100 
fixes f :: "'a \<Rightarrow> 'b::order" 
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49769
diff
changeset

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

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

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

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

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

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

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

1108 
then have "y \<le> x" by simp 
60758  1109 
with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE) 
1110 
with \<open>f x < f y\<close> show False by simp 

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

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

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

1113 

30298  1114 
lemma strict_mono_eq: 
1115 
assumes "strict_mono f" 

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

1117 
proof 

1118 
assume "f x = f y" 

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

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

60758  1121 
with \<open>f x = f y\<close> show ?thesis by simp 
30298  1122 
next 
1123 
case equal then show ?thesis . 

1124 
next 

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

60758  1126 
with \<open>f x = f y\<close> show ?thesis by simp 
30298  1127 
qed 
1128 
qed simp 

1129 

1130 
lemma strict_mono_less_eq: 

1131 
assumes "strict_mono f" 

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

1133 
proof 

1134 
assume "x \<le> y" 

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

1136 
next 

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

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

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

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

60758  1141 
with \<open>f x \<le> f y\<close> show False by simp 
30298  1142 
qed 
1143 
qed 

1144 

1145 
lemma strict_mono_less: 

1146 
assumes "strict_mono f" 

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

1148 
using assms 

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

1150 

54860  1151 
end 
1152 

1153 

60758  1154 
subsection \<open>min and max  fundamental\<close> 
54860  1155 

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

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

1158 

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

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

1161 

45931  1162 
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

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

1164 

54857  1165 
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

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

1167 

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

1169 
by (simp add:min_def) 
45893  1170 

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

1172 
by (simp add: max_def) 
45893  1173 

1174 

60758  1175 
subsection \<open>(Unique) top and bottom elements\<close> 
28685  1176 

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

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

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

1179 

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

1180 
class order_bot = order + bot + 
51487  1181 
assumes bot_least: "\<bottom> \<le> a" 
54868  1182 
begin 
51487  1183 

54868  1184 
sublocale bot!: ordering_top greater_eq greater bot 
61169  1185 
by standard (fact bot_least) 
51487  1186 

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

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

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

1190 

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

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

1194 

51487  1195 
lemma not_less_bot: 
1196 
"\<not> a < \<bottom>" 

1197 
by (fact bot.extremum_strict) 

43816  1198 

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

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

1200 
"a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a" 
51487  1201 
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

1202 

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

1203 
end 
41082  1204 

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

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

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

1207 

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

1208 
class order_top = order + top + 
51487  1209 
assumes top_greatest: "a \<le> \<top>" 
54868  1210 
begin 
51487  1211 

54868  1212 
sublocale top!: ordering_top less_eq less top 
61169  1213 
by standard (fact top_greatest) 
51487  1214 

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

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

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

1218 

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

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

1222 

51487  1223 
lemma not_top_less: 
1224 
"\<not> \<top> < a" 

1225 
by (fact top.extremum_strict) 

43816  1226 

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

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

1228 
"a \<noteq> \<top> \<longleftrightarrow> a < \<top>" 
51487  1229 
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

1230 

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

1231 
end 
28685  1232 

1233 

60758  1234 
subsection \<open>Dense orders\<close> 
27823  1235 

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

1237 
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

1238 

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

1240 
begin 
27823  1241 

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

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

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

1244 
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

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

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

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

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

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

1250 
obtain x where "x < y" and "z < x" by safe 
60758  1251 
moreover have "x \<le> z" using assms[OF \<open>x < y\<close>] . 
35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

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

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

1254 

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

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

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

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

1258 
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

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

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

1261 
fix w assume "w < y" 
60758  1262 
from dense[OF \<open>x < y\<close>] obtain u where "x < u" "u < y" by safe 
35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

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

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

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

1266 
assume "u \<le> w" 
60758  1267 
from less_le_trans[OF \<open>x < u\<close> \<open>u \<le> w\<close>] \<open>w < y\<close> 
35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

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

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

1270 
assume "w \<le> u" 
60758  1271 
from \<open>w \<le> u\<close> *[OF \<open>x < u\<close> \<open>u < y\<close>] 
35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

1272 
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

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

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

1275 

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

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

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

1278 
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

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

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

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

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

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

1284 
obtain x where "x < y" and "z < x" by safe 
60758  1285 
moreover have "y \<le> x" using assms[OF \<open>z < x\<close>] . 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

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

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

1288 

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

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

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

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

1292 
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

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

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

1295 
fix w assume "z < w" 
60758  1296 
from dense[OF \<open>z < x\<close>] obtain u where "z < u" "u < x" by safe 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

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

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

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

1300 
assume "w \<le> u" 
60758  1301 
from \<open>z < w\<close> le_less_trans[OF \<open>w \<le> u\<close> \<open>u < x\<close>] 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

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

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

1304 
assume "u \<le> w" 
60758  1305 
from *[OF \<open>z < u\<close> \<open>u < x\<close>] \<open>u \<le> w\<close> 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1306 
show "y \<le> w" by (rule order_trans) 