author  haftmann 
Fri, 27 Dec 2013 14:35:14 +0100  
changeset 54868  bab6cade3cc5 
parent 54861  00d551179872 
child 56020  f92479477c52 
permissions  rwrr 
28685  1 
(* Title: HOL/Orderings.thy 
15524  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

4 

25614  5 
header {* Abstract orderings *} 
15524  6 

7 
theory Orderings 

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

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

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

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

14 

51487  15 
subsection {* Abstract ordering *} 
16 

17 
locale ordering = 

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

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

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

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

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

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

24 
begin 

25 

26 
lemma strict_implies_order: 

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

28 
by (simp add: strict_iff_order) 

29 

30 
lemma strict_implies_not_eq: 

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

32 
by (simp add: strict_iff_order) 

33 

34 
lemma not_eq_order_implies_strict: 

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

36 
by (simp add: strict_iff_order) 

37 

38 
lemma order_iff_strict: 

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

40 
by (auto simp add: strict_iff_order refl) 

41 

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

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

44 
by (simp add: strict_iff_order) 

45 

46 
lemma asym: 

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

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

49 

50 
lemma strict_trans1: 

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

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

53 

54 
lemma strict_trans2: 

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

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

57 

58 
lemma strict_trans: 

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

60 
by (auto intro: strict_trans1 strict_implies_order) 

61 

62 
end 

63 

64 
locale ordering_top = ordering + 

65 
fixes top :: "'a" 

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

67 
begin 

68 

69 
lemma extremum_uniqueI: 

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

71 
by (rule antisym) auto 

72 

73 
lemma extremum_unique: 

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

75 
by (auto intro: antisym) 

76 

77 
lemma extremum_strict [simp]: 

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

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

80 

81 
lemma not_eq_extremum: 

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

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

84 

85 
end 

86 

87 

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

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

89 

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

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

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

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

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

94 

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

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

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

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

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

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

100 

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

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

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

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

104 

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

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

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

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

108 

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

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

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

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

112 

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

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

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

115 

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

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

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

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

119 

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

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

121 

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

122 

27682  123 
subsection {* Quasi orders *} 
15524  124 

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

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

21248  129 
begin 
130 

15524  131 
text {* Reflexivity. *} 
132 

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

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

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

141 
unfolding less_le_not_le by blast 

142 

143 

144 
text {* Asymmetry. *} 

145 

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

147 
by (simp add: less_le_not_le) 

148 

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

150 
by (drule less_not_sym, erule contrapos_np) simp 

151 

152 

153 
text {* Transitivity. *} 

154 

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

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

157 

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

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

160 

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

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

163 

164 

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

166 

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

168 
by (blast elim: less_asym) 

169 

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

171 
by (blast elim: less_asym) 

172 

173 

174 
text {* Transitivity rules for calculational reasoning *} 

175 

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

177 
by (rule less_asym) 

178 

179 

180 
text {* Dual order *} 

181 

182 
lemma dual_preorder: 

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

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

186 
end 

187 

188 

189 
subsection {* Partial orders *} 

190 

191 
class order = preorder + 

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

193 
begin 

194 

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

197 

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

201 

202 
text {* Reflexivity. *} 

15524  203 

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

206 
by (fact order.order_iff_strict) 
15524  207 

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

21329  211 

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

213 

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

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

220 

221 
text {* Transitivity rules for calculational reasoning *} 

222 

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

224 
by (fact order.not_eq_order_implies_strict) 
21329  225 

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

227 
by (rule order.not_eq_order_implies_strict) 
21329  228 

15524  229 

230 
text {* Asymmetry. *} 

231 

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

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

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

239 
by (fact order.strict_implies_not_eq) 
21248  240 

21083  241 

27107  242 
text {* Least value operator *} 
243 

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

247 

248 
lemma Least_equality: 

249 
assumes "P x" 

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

251 
shows "Least P = x" 

252 
unfolding Least_def by (rule the_equality) 

253 
(blast intro: assms antisym)+ 

254 

255 
lemma LeastI2_order: 

256 
assumes "P x" 

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

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

259 
shows "Q (Least P)" 

260 
unfolding Least_def by (rule theI2) 

261 
(blast intro: assms antisym)+ 

262 

263 

26014  264 
text {* Dual order *} 
22916  265 

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

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

21248  270 
end 
15524  271 

21329  272 

273 
subsection {* Linear (total) orders *} 

274 

22316  275 
class linorder = order + 
25207  276 
assumes linear: "x \<le> y \<or> y \<le> x" 
21248  277 
begin 
278 

25062  279 
lemma less_linear: "x < y \<or> x = y \<or> y < x" 
23212  280 
unfolding less_le using less_le linear by blast 
21248  281 

25062  282 
lemma le_less_linear: "x \<le> y \<or> y < x" 
23212  283 
by (simp add: le_less less_linear) 
21248  284 

285 
lemma le_cases [case_names le ge]: 

25062  286 
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  287 
using linear by blast 
21248  288 

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

289 
lemma linorder_cases [case_names less equal greater]: 
25062  290 
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  291 
using less_linear by blast 
21248  292 

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

296 
done 

297 

298 
lemma not_less_iff_gr_or_eq: 

25062  299 
"\<not>(x < y) \<longleftrightarrow> (x > y  x = y)" 
23212  300 
apply(simp add:not_less le_less) 
301 
apply blast 

302 
done 

15524  303 

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

307 
done 

15524  308 

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

25062  312 
lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R" 
23212  313 
by (simp add: neq_iff) blast 
15524  314 

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

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

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

25062  324 
lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x" 
23212  325 
unfolding not_less . 
16796  326 

25062  327 
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y" 
23212  328 
unfolding not_less . 
16796  329 

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

25062  331 
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y" 
23212  332 
unfolding not_le . 
21248  333 

22916  334 

26014  335 
text {* Dual order *} 
22916  336 

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

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

339 
by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear) 
22916  340 

21248  341 
end 
342 

23948  343 

21083  344 
subsection {* Reasoning tools setup *} 
345 

21091  346 
ML {* 
347 

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

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

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

350 
val print_structures: Proof.context > unit 
47432  351 
val attrib_setup: theory > theory 
32215  352 
val order_tac: Proof.context > thm list > int > tactic 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

353 
end; 
21091  354 

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

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

357 

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

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

359 

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

360 
fun struct_eq ((s1: string, ts1), (s2, ts2)) = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

361 
(s1 = s2) andalso eq_list (op aconv) (ts1, ts2); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

362 

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

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

365 
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

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

367 
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

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

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

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

371 
val extend = I; 
33519  372 
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

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

374 

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

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

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

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

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

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

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

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

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

385 
in 
51579  386 
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

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

388 

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

389 

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

390 
(** Method **) 
21091  391 

32215  392 
fun struct_tac ((s, [eq, le, less]), thms) ctxt prems = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

393 
let 
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29823
diff
changeset

394 
fun decomp thy (@{const Trueprop} $ t) = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

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

397 
(* exclude numeric types: linear arithmetic subsumes transitivity *) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

398 
let val T = type_of t 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

399 
in 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32899
diff
changeset

400 
T = HOLogic.natT orelse T = HOLogic.intT orelse T = HOLogic.realT 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

401 
end; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32899
diff
changeset

402 
fun rel (bin_op $ t1 $ t2) = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

403 
if excluded t1 then NONE 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

404 
else if Pattern.matches thy (eq, bin_op) then SOME (t1, "=", t2) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

405 
else if Pattern.matches thy (le, bin_op) then SOME (t1, "<=", t2) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

406 
else if Pattern.matches thy (less, bin_op) then SOME (t1, "<", t2) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

407 
else NONE 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32899
diff
changeset

408 
 rel _ = NONE; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32899
diff
changeset

409 
fun dec (Const (@{const_name Not}, _) $ t) = (case rel t 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32899
diff
changeset

410 
of NONE => NONE 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32899
diff
changeset

411 
 SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) 
24741
a53f5db5acbb
Fixed setup of transitivity reasoner (function decomp).
ballarin
parents:
24704
diff
changeset

412 
 dec x = rel x; 
30107
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29823
diff
changeset

413 
in dec t end 
f3b3b0e3d184
Fixed nonexhaustive match problem in decomp, to make it fail more gracefully
berghofe
parents:
29823
diff
changeset

414 
 decomp thy _ = NONE; 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

416 
case s of 
32215  417 
"order" => Order_Tac.partial_tac decomp thms ctxt prems 
418 
 "linorder" => Order_Tac.linear_tac decomp thms ctxt prems 

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

419 
 _ => error ("Unknown kind of order `" ^ s ^ "' encountered in transitivity reasoner.") 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

421 

32215  422 
fun order_tac ctxt prems = 
423 
FIRST' (map (fn s => CHANGED o struct_tac s ctxt prems) (Data.get (Context.Proof ctxt))); 

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

424 

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

425 

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

426 
(** Attribute **) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

427 

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

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

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

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

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

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

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

434 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

435 
val attrib_setup = 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

436 
Attrib.setup @{binding order} 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

437 
(Scan.lift ((Args.add  Args.name >> (fn (_, s) => SOME s)  Args.del >> K NONE)  
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

438 
Args.colon (* FIXME  Scan.succeed true *) )  Scan.lift Args.name  
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

439 
Scan.repeat Args.term 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

440 
>> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

441 
 ((NONE, n), ts) => del_struct (n, ts))) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30528
diff
changeset

442 
"theorems controlling transitivity reasoner"; 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

443 

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

444 

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

445 
(** Diagnostic command **) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

446 

24867  447 
val _ = 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46950
diff
changeset

448 
Outer_Syntax.improper_command @{command_spec "print_orders"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46950
diff
changeset

449 
"print order structures available to transitivity reasoner" 
51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51579
diff
changeset

450 
(Scan.succeed (Toplevel.unknown_context o 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51579
diff
changeset

451 
Toplevel.keep (print_structures o Toplevel.context_of))); 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

452 

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

454 

21091  455 
*} 
456 

47432  457 
setup Orders.attrib_setup 
458 

459 
method_setup order = {* 

460 
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Orders.order_tac ctxt [])) 

461 
*} "transitivity reasoner" 

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

462 

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

463 

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

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

465 

25076  466 
context order 
467 
begin 

468 

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

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

470 
is not a parameter of the locale. *) 
25076  471 

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

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

475 

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

477 

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

479 

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

481 

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

483 

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

485 

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

487 

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

489 

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

491 

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

493 

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

495 

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

497 

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

499 

500 
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

501 

25076  502 
end 
503 

504 
context linorder 

505 
begin 

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

506 

27689  507 
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] 
508 

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

510 

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

512 

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

514 

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

516 

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

518 

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

520 

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

522 

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

524 

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

25076  526 

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

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

530 

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

532 

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

534 

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

536 

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

538 

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

540 

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

542 

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

544 

545 
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

546 

25076  547 
end 
548 

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

549 

21083  550 
setup {* 
551 
let 

552 

44058  553 
fun prp t thm = Thm.prop_of thm = t; (* FIXME aconv!? *) 
15524  554 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

555 
fun prove_antisym_le ctxt ((le as Const(_,T)) $ r $ s) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

556 
let val prems = Simplifier.prems_of ctxt; 
22916  557 
val less = Const (@{const_name less}, T); 
21083  558 
val t = HOLogic.mk_Trueprop(le $ s $ r); 
559 
in case find_first (prp t) prems of 

560 
NONE => 

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

562 
in case find_first (prp t) prems of 

563 
NONE => NONE 

24422  564 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) 
21083  565 
end 
24422  566 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) 
21083  567 
end 
568 
handle THM _ => NONE; 

15524  569 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

570 
fun prove_antisym_less ctxt (NotC $ ((less as Const(_,T)) $ r $ s)) = 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

571 
let val prems = Simplifier.prems_of ctxt; 
22916  572 
val le = Const (@{const_name less_eq}, T); 
21083  573 
val t = HOLogic.mk_Trueprop(le $ r $ s); 
574 
in case find_first (prp t) prems of 

575 
NONE => 

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

577 
in case find_first (prp t) prems of 

578 
NONE => NONE 

24422  579 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) 
21083  580 
end 
24422  581 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) 
21083  582 
end 
583 
handle THM _ => NONE; 

15524  584 

21248  585 
fun add_simprocs procs thy = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

586 
map_theory_simpset (fn ctxt => ctxt 
21248  587 
addsimprocs (map (fn (name, raw_ts, proc) => 
38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
38705
diff
changeset

588 
Simplifier.simproc_global thy name raw_ts proc) procs)) thy; 
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42287
diff
changeset

589 

26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26324
diff
changeset

590 
fun add_solver name tac = 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

591 
map_theory_simpset (fn ctxt0 => ctxt0 addSolver 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset

592 
mk_solver name (fn ctxt => tac ctxt (Simplifier.prems_of ctxt))); 
21083  593 

594 
in 

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

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

598 
] 

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

599 
#> add_solver "Transitivity" Orders.order_tac 
21248  600 
(* Adding the transitivity reasoners also as safe solvers showed a slight 
601 
speed up, but the reasoning strength appears to be not higher (at least 

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

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

21083  604 
end 
605 
*} 

15524  606 

607 

21083  608 
subsection {* Bounded quantifiers *} 
609 

610 
syntax 

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

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

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

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

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

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

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

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

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

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

621 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

632 
syntax (HOL) 

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

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

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

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

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

638 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

649 
translations 

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

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

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

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

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

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

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

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

658 

659 
print_translation {* 

660 
let 

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

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

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

663 
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

664 
val conj = @{const_syntax HOL.conj}; 
22916  665 
val less = @{const_syntax less}; 
666 
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

667 

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

668 
val trans = 
35115  669 
[((All_binder, impl, less), 
670 
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})), 

671 
((All_binder, impl, less_eq), 

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

673 
((Ex_binder, conj, less), 

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

675 
((Ex_binder, conj, less_eq), 

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

677 

35115  678 
fun matches_bound v t = 
679 
(case t of 

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

683 
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

684 

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

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

690 
 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

691 
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

692 
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P 
35115  693 
else raise Match) 
52143  694 
 _ => raise Match)); 
21524  695 
in [tr' All_binder, tr' Ex_binder] end 
21083  696 
*} 
697 

698 

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

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

700 

25193  701 
context ord 
702 
begin 

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

703 

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

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

706 

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

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

709 

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

712 

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

714 
by (rule ssubst) 

715 

716 
end 

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

717 

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

718 
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

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

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

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

722 
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

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

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

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

726 

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

727 
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

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

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

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

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

732 
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

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

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

735 

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

736 
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

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

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

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

740 
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

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

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

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

744 

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

745 
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

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

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

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

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

750 
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

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

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

753 

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

754 
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

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

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

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

758 
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

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

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

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

762 

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

763 
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

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

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

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

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

768 
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

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

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

771 

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

772 
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

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

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

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

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

777 
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

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

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

780 

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

781 
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

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

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

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

785 
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

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

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

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

789 

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

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

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

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

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

794 
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

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

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

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

798 

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

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

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

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

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

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

804 
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

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

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

807 

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

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

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

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

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

812 
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

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

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

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

816 

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

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

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

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

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

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

822 
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

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

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

825 

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

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

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

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

829 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

846 
mp 
27682  847 

848 
lemmas (in order) [trans] = 

849 
neq_le_trans 

850 
le_neq_trans 

851 

852 
lemmas (in preorder) [trans] = 

853 
less_trans 

854 
less_asym' 

855 
le_less_trans 

856 
less_le_trans 

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

857 
order_trans 
27682  858 

859 
lemmas (in order) [trans] = 

860 
antisym 

861 

862 
lemmas (in ord) [trans] = 

863 
ord_le_eq_trans 

864 
ord_eq_le_trans 

865 
ord_less_eq_trans 

866 
ord_eq_less_trans 

867 

868 
lemmas [trans] = 

869 
trans 

870 

871 
lemmas order_trans_rules = 

872 
order_less_subst2 

873 
order_less_subst1 

874 
order_le_less_subst2 

875 
order_le_less_subst1 

876 
order_less_le_subst2 

877 
order_less_le_subst1 

878 
order_subst2 

879 
order_subst1 

880 
ord_le_eq_subst 

881 
ord_eq_le_subst 

882 
ord_less_eq_subst 

883 
ord_eq_less_subst 

884 
forw_subst 

885 
back_subst 

886 
rev_mp 

887 
mp 

888 
neq_le_trans 

889 
le_neq_trans 

890 
less_trans 

891 
less_asym' 

892 
le_less_trans 

893 
less_le_trans 

894 
order_trans 

895 
antisym 

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

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

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

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

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

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

901 

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

904 

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

905 
lemma xt1 [no_atp]: 
21083  906 
"a = b ==> b > c ==> a > c" 
907 
"a > b ==> b = c ==> a > c" 

908 
"a = b ==> b >= c ==> a >= c" 

909 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  914 
"(a::'a::order) > b ==> b > a ==> P" 
21083  915 
"(x::'a::order) > y ==> y > z ==> x > z" 
916 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  922 
by auto 
21083  923 

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

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

927 

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

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

931 

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

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

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 xt5 [no_atp]: "(a::'a::order) > b ==> (f b::'b::order) >= c==> 
21083  937 
(!!x y. x > y ==> f x > f y) ==> f a > c" 
938 
by (subgoal_tac "f a > f b", force, force) 

939 

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

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

943 

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

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

947 

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

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

951 

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

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

955 

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

956 
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 
21083  957 

958 
(* 

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

960 
for the wrong thing in an Isar proof. 

961 

962 
The extra transitivity rules can be used as follows: 

963 

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

965 
proof  

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

967 
sorry 

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

969 
sorry 

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

971 
sorry 

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

973 
sorry 

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

975 
sorry 

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

977 
sorry 

978 
finally (xtrans) show ?thesis . 

979 
qed 

980 

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

982 
leave out the "(xtrans)" above. 

983 
*) 

984 

23881  985 

54860  986 
subsection {* Monotonicity *} 
21083  987 

25076  988 
context order 
989 
begin 

990 

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

994 
lemma monoI [intro?]: 

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

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

997 
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

998 

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

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

1002 
unfolding mono_def by iprover 

1003 

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

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

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

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

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

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

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

1010 
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

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

1012 

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

1015 

1016 
lemma strict_monoI [intro?]: 

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

1018 
shows "strict_mono f" 

1019 
using assms unfolding strict_mono_def by auto 

1020 

1021 
lemma strict_monoD [dest?]: 

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

1023 
unfolding strict_mono_def by auto 

1024 

1025 
lemma strict_mono_mono [dest?]: 

1026 
assumes "strict_mono f" 

1027 
shows "mono f" 

1028 
proof (rule monoI) 

1029 
fix x y 

1030 
assume "x \<le> y" 

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

1032 
proof (cases "x = y") 

1033 
case True then show ?thesis by simp 

1034 
next 

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

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

1037 
then show ?thesis by simp 

1038 
qed 

1039 
qed 

1040 

25076  1041 
end 
1042 

1043 
context linorder 

1044 
begin 

1045 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1060 

30298  1061 
lemma strict_mono_eq: 
1062 
assumes "strict_mono f" 

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

1064 
proof 

1065 
assume "f x = f y" 

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

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

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

1069 
next 

1070 
case equal then show ?thesis . 

1071 
next 

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

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

1074 
qed 

1075 
qed simp 

1076 

1077 
lemma strict_mono_less_eq: 

1078 
assumes "strict_mono f" 

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

1080 
proof 

1081 
assume "x \<le> y" 

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

1083 
next 

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

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

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

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

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

1089 
qed 

1090 
qed 

1091 

1092 
lemma strict_mono_less: 

1093 
assumes "strict_mono f" 

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

1095 
using assms 

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

1097 

54860  1098 
end 
1099 

1100 

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

1101 
subsection {* min and max  fundamental *} 
54860  1102 

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

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

1105 

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

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

1108 

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

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

1111 

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

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

1114 

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

1116 
by (simp add:min_def) 
45893  1117 

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

1119 
by (simp add: max_def) 
45893  1120 

1121 

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

1122 
subsection {* (Unique) top and bottom elements *} 
28685  1123 

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

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

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

1126 

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

1127 
class order_bot = order + bot + 
51487  1128 
assumes bot_least: "\<bottom> \<le> a" 
54868  1129 
begin 
51487  1130 

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

1132 
by default (fact bot_least) 
51487  1133 

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

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

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

1137 

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

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

1141 

51487  1142 
lemma not_less_bot: 
1143 
"\<not> a < \<bottom>" 

1144 
by (fact bot.extremum_strict) 

43816  1145 

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

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

1147 
"a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a" 
51487  1148 
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

1149 

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

1150 
end 
41082  1151 

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

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

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

1154 

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

1155 
class order_top = order + top + 
51487  1156 
assumes top_greatest: "a \<le> \<top>" 
54868  1157 
begin 
51487  1158 

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

1160 
by default (fact top_greatest) 
51487  1161 

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

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

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

1165 

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

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

1169 

51487  1170 
lemma not_top_less: 
1171 
"\<not> \<top> < a" 

1172 
by (fact top.extremum_strict) 

43816  1173 

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

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

1175 
"a \<noteq> \<top> \<longleftrightarrow> a < \<top>" 
51487  1176 
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

1177 

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

1178 
end 
28685  1179 

1180 

27823  1181 
subsection {* Dense orders *} 
1182 

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

1184 
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

1185 

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

1187 
begin 
27823  1188 

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

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

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

1191 
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

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

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

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

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

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

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

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

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

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

1201 

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

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

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

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

1205 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

1219 
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

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

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

1222 

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

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

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

1225 
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

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

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

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

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

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

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

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

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

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

1235 

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

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

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

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

1239 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1256 

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

1257 
end 
27823  1258 

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

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

1260 
assumes gt_ex: "\<exists>y. x < y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1261 

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

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

1263 
assumes lt_ex: "\<exists>y. y < x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1264 

53216  1265 
class unbounded_dense_linorder = dense_linorder + no_top + no_bot 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

1266 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
51487
diff
changeset

1267 

27823  1268 
subsection {* Wellorders *} 
1269 

1270 
class wellorder = linorder + 

1271 
assumes less_induct [case_names less]: "(\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P a" 

1272 
begin 

1273 

1274 
lemma wellorder_Least_lemma: 

1275 
fixes k :: 'a 

1276 
assumes "P k" 

34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1277 
shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k" 
27823  1278 
proof  
1279 
have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k" 

1280 
using assms proof (induct k rule: less_induct) 

1281 
case (less x) then have "P x" by simp 

1282 
show ?case proof (rule classical) 

1283 
assume assm: "\<not> (P (LEAST a. P a) \<and> (LEAST a. P a) \<le> x)" 

1284 
have "\<And>y. P y \<Longrightarrow> x \<le> y" 

1285 
proof (rule classical) 

1286 
fix y 

38705  1287 
assume "P y" and "\<not> x \<le> y" 
27823  1288 
with less have "P (LEAST a. P a)" and "(LEAST a. P a) \<le> y" 
1289 
by (auto simp add: not_le) 

1290 
with assm have "x < (LEAST a. P a)" and "(LEAST a. P a) \<le> y" 

1291 
by auto 

1292 
then show "x \<le> y" by auto 

1293 
qed 

1294 
with `P x` have Least: "(LEAST a. P a) = x" 

1295 
by (rule Least_equality) 

1296 
with `P x` show ?thesis by simp 

1297 
qed 

1298 
qed 

1299 
then show "P (LEAST x. P x)" and "(LEAST x. P x) \<le> k" by auto 

1300 
qed 

1301 

1302 
 "The following 3 lemmas are due to Brian Huffman" 

1303 
lemma LeastI_ex: "\<exists>x. P x \<Longrightarrow> P (Least P)" 

1304 
by (erule exE) (erule LeastI) 

1305 

1306 
lemma LeastI2: 

1307 
"P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)" 

1308 
by (blast intro: LeastI) 

1309 

1310 
lemma LeastI2_ex: 

1311 
"\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (Least P)" 

1312 
by (blast intro: LeastI_ex) 

1313 

38705  1314 