author  haftmann 
Thu, 26 Aug 2010 20:51:17 +0200  
changeset 38786  e46e7a9cb622 
parent 38715  6513ea67d95d 
child 38795  848be46708dc 
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 
32215  9 
uses 
10 
"~~/src/Provers/order.ML" 

11 
"~~/src/Provers/quasi.ML" (* FIXME unused? *) 

15524  12 
begin 
13 

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

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

15 

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

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

17 
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

18 
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

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

20 

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

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

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

23 
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

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

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

26 

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

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

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

29 
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

30 

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

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

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

33 
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

34 

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

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

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

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

38 

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

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

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

41 

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

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

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

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

45 

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

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

47 

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

48 

27682  49 
subsection {* Quasi orders *} 
15524  50 

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

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

21248  55 
begin 
56 

15524  57 
text {* Reflexivity. *} 
58 

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

25062  63 
lemma less_irrefl [iff]: "\<not> x < x" 
27682  64 
by (simp add: less_le_not_le) 
65 

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

67 
unfolding less_le_not_le by blast 

68 

69 

70 
text {* Asymmetry. *} 

71 

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

73 
by (simp add: less_le_not_le) 

74 

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

76 
by (drule less_not_sym, erule contrapos_np) simp 

77 

78 

79 
text {* Transitivity. *} 

80 

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

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

83 

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

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

86 

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

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

89 

90 

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

92 

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

94 
by (blast elim: less_asym) 

95 

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

97 
by (blast elim: less_asym) 

98 

99 

100 
text {* Transitivity rules for calculational reasoning *} 

101 

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

103 
by (rule less_asym) 

104 

105 

106 
text {* Dual order *} 

107 

108 
lemma dual_preorder: 

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

109 
"class.preorder (op \<ge>) (op >)" 
28823  110 
proof qed (auto simp add: less_le_not_le intro: order_trans) 
27682  111 

112 
end 

113 

114 

115 
subsection {* Partial orders *} 

116 

117 
class order = preorder + 

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

119 
begin 

120 

121 
text {* Reflexivity. *} 

122 

123 
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" 

124 
by (auto simp add: less_le_not_le intro: antisym) 

15524  125 

25062  126 
lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y" 
15524  127 
 {* NOT suitable for iff, since it can cause PROOF FAILED. *} 
23212  128 
by (simp add: less_le) blast 
15524  129 

25062  130 
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y" 
23212  131 
unfolding less_le by blast 
15524  132 

21329  133 

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

135 

25062  136 
lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 
23212  137 
by auto 
21329  138 

25062  139 
lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 
23212  140 
by auto 
21329  141 

142 

143 
text {* Transitivity rules for calculational reasoning *} 

144 

25062  145 
lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" 
23212  146 
by (simp add: less_le) 
21329  147 

25062  148 
lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b" 
23212  149 
by (simp add: less_le) 
21329  150 

15524  151 

152 
text {* Asymmetry. *} 

153 

25062  154 
lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x" 
23212  155 
by (blast intro: antisym) 
15524  156 

25062  157 
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y" 
23212  158 
by (blast intro: antisym) 
15524  159 

25062  160 
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y" 
23212  161 
by (erule contrapos_pn, erule subst, rule less_irrefl) 
21248  162 

21083  163 

27107  164 
text {* Least value operator *} 
165 

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

169 

170 
lemma Least_equality: 

171 
assumes "P x" 

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

173 
shows "Least P = x" 

174 
unfolding Least_def by (rule the_equality) 

175 
(blast intro: assms antisym)+ 

176 

177 
lemma LeastI2_order: 

178 
assumes "P x" 

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

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

181 
shows "Q (Least P)" 

182 
unfolding Least_def by (rule theI2) 

183 
(blast intro: assms antisym)+ 

184 

185 

26014  186 
text {* Dual order *} 
22916  187 

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

189 
"class.order (op \<ge>) (op >)" 
27682  190 
by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym) 
22916  191 

21248  192 
end 
15524  193 

21329  194 

195 
subsection {* Linear (total) orders *} 

196 

22316  197 
class linorder = order + 
25207  198 
assumes linear: "x \<le> y \<or> y \<le> x" 
21248  199 
begin 
200 

25062  201 
lemma less_linear: "x < y \<or> x = y \<or> y < x" 
23212  202 
unfolding less_le using less_le linear by blast 
21248  203 

25062  204 
lemma le_less_linear: "x \<le> y \<or> y < x" 
23212  205 
by (simp add: le_less less_linear) 
21248  206 

207 
lemma le_cases [case_names le ge]: 

25062  208 
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  209 
using linear by blast 
21248  210 

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

211 
lemma linorder_cases [case_names less equal greater]: 
25062  212 
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  213 
using less_linear by blast 
21248  214 

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

218 
done 

219 

220 
lemma not_less_iff_gr_or_eq: 

25062  221 
"\<not>(x < y) \<longleftrightarrow> (x > y  x = y)" 
23212  222 
apply(simp add:not_less le_less) 
223 
apply blast 

224 
done 

15524  225 

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

229 
done 

15524  230 

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

25062  234 
lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R" 
23212  235 
by (simp add: neq_iff) blast 
15524  236 

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

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

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

25062  246 
lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x" 
23212  247 
unfolding not_less . 
16796  248 

25062  249 
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y" 
23212  250 
unfolding not_less . 
16796  251 

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

25062  253 
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y" 
23212  254 
unfolding not_le . 
21248  255 

22916  256 

26014  257 
text {* Dual order *} 
22916  258 

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

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

261 
by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear) 
22916  262 

263 

23881  264 
text {* min/max *} 
265 

27299  266 
definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 
37767  267 
"min a b = (if a \<le> b then a else b)" 
23881  268 

27299  269 
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 
37767  270 
"max a b = (if a \<le> b then b else a)" 
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22377
diff
changeset

271 

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

272 
lemma min_le_iff_disj: 
25062  273 
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" 
23212  274 
unfolding min_def using linear by (auto intro: order_trans) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

275 

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

276 
lemma le_max_iff_disj: 
25062  277 
"z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" 
23212  278 
unfolding max_def using linear by (auto intro: order_trans) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

279 

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

280 
lemma min_less_iff_disj: 
25062  281 
"min x y < z \<longleftrightarrow> x < z \<or> y < z" 
23212  282 
unfolding min_def le_less using less_linear by (auto intro: less_trans) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

283 

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

284 
lemma less_max_iff_disj: 
25062  285 
"z < max x y \<longleftrightarrow> z < x \<or> z < y" 
23212  286 
unfolding max_def le_less using less_linear by (auto intro: less_trans) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

287 

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

288 
lemma min_less_iff_conj [simp]: 
25062  289 
"z < min x y \<longleftrightarrow> z < x \<and> z < y" 
23212  290 
unfolding min_def le_less using less_linear by (auto intro: less_trans) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

291 

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

292 
lemma max_less_iff_conj [simp]: 
25062  293 
"max x y < z \<longleftrightarrow> x < z \<and> y < z" 
23212  294 
unfolding max_def le_less using less_linear by (auto intro: less_trans) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

295 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35579
diff
changeset

296 
lemma split_min [no_atp]: 
25062  297 
"P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)" 
23212  298 
by (simp add: min_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

299 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35579
diff
changeset

300 
lemma split_max [no_atp]: 
25062  301 
"P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)" 
23212  302 
by (simp add: max_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

303 

21248  304 
end 
305 

28516  306 
text {* Explicit dictionaries for code generation *} 
307 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
30929
diff
changeset

308 
lemma min_ord_min [code, code_unfold, code_inline del]: 
28516  309 
"min = ord.min (op \<le>)" 
310 
by (rule ext)+ (simp add: min_def ord.min_def) 

311 

312 
declare ord.min_def [code] 

313 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
30929
diff
changeset

314 
lemma max_ord_max [code, code_unfold, code_inline del]: 
28516  315 
"max = ord.max (op \<le>)" 
316 
by (rule ext)+ (simp add: max_def ord.max_def) 

317 

318 
declare ord.max_def [code] 

319 

23948  320 

21083  321 
subsection {* Reasoning tools setup *} 
322 

21091  323 
ML {* 
324 

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

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

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

327 
val print_structures: Proof.context > unit 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

328 
val setup: theory > theory 
32215  329 
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

330 
end; 
21091  331 

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

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

334 

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

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

336 

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

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

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

339 

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

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

342 
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

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

344 
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

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

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

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

348 
val extend = I; 
33519  349 
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

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

351 

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

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

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

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

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

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

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

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

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

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

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

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

365 

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

366 

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

367 
(** Method **) 
21091  368 

32215  369 
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

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

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

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

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

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

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

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

377 
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

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

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

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

381 
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

382 
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

383 
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

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

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

386 
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

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

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

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

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

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

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

393 
case s of 
32215  394 
"order" => Order_Tac.partial_tac decomp thms ctxt prems 
395 
 "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

396 
 _ => 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

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

398 

32215  399 
fun order_tac ctxt prems = 
400 
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

401 

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

402 

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

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

404 

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

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

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

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

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

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

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

411 

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

412 
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

413 
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

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

415 
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

416 
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

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

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

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

420 

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

421 

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

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

423 

24867  424 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36635
diff
changeset

425 
Outer_Syntax.improper_command "print_orders" 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36635
diff
changeset

426 
"print order structures available to transitivity reasoner" Keyword.diag 
30806  427 
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o 
428 
Toplevel.keep (print_structures o Toplevel.context_of))); 

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

429 

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

430 

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

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

432 

24867  433 
val setup = 
32215  434 
Method.setup @{binding order} (Scan.succeed (fn ctxt => SIMPLE_METHOD' (order_tac ctxt []))) 
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 
"transitivity reasoner" #> 
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; 
21091  437 

438 
end; 

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

439 

21091  440 
*} 
441 

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

442 
setup Orders.setup 
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 
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

446 

25076  447 
context order 
448 
begin 

449 

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

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

451 
is not a parameter of the locale. *) 
25076  452 

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

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

456 

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

458 

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

460 

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

462 

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

464 

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

466 

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

468 

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

470 

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

472 

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

474 

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

476 

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

478 

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

480 

481 
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

482 

25076  483 
end 
484 

485 
context linorder 

486 
begin 

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

487 

27689  488 
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] 
489 

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

491 

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

493 

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

495 

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

497 

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

499 

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

501 

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

503 

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

505 

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

25076  507 

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

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

511 

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

513 

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

515 

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

517 

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

519 

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

521 

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

523 

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

525 

526 
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

527 

25076  528 
end 
529 

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

530 

21083  531 
setup {* 
532 
let 

533 

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

15524  535 

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

22916  538 
val less = Const (@{const_name less}, T); 
21083  539 
val t = HOLogic.mk_Trueprop(le $ s $ r); 
540 
in case find_first (prp t) prems of 

541 
NONE => 

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

543 
in case find_first (prp t) prems of 

544 
NONE => NONE 

24422  545 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) 
21083  546 
end 
24422  547 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) 
21083  548 
end 
549 
handle THM _ => NONE; 

15524  550 

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

22916  553 
val le = Const (@{const_name less_eq}, T); 
21083  554 
val t = HOLogic.mk_Trueprop(le $ r $ s); 
555 
in case find_first (prp t) prems of 

556 
NONE => 

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

558 
in case find_first (prp t) prems of 

559 
NONE => NONE 

24422  560 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) 
21083  561 
end 
24422  562 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) 
21083  563 
end 
564 
handle THM _ => NONE; 

15524  565 

21248  566 
fun add_simprocs procs thy = 
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26324
diff
changeset

567 
Simplifier.map_simpset (fn ss => ss 
21248  568 
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

569 
Simplifier.simproc_global thy name raw_ts proc) procs)) thy; 
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26324
diff
changeset

570 
fun add_solver name tac = 
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26324
diff
changeset

571 
Simplifier.map_simpset (fn ss => ss addSolver 
32215  572 
mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss))); 
21083  573 

574 
in 

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

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

578 
] 

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

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

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

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

21083  584 
end 
585 
*} 

15524  586 

587 

21083  588 
subsection {* Bounded quantifiers *} 
589 

590 
syntax 

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

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

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

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

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

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

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

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

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

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

601 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

612 
syntax (HOL) 

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

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

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

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

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

618 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

629 
translations 

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

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

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

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

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

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

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

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

638 

639 
print_translation {* 

640 
let 

22916  641 
val All_binder = Syntax.binder_name @{const_syntax All}; 
642 
val Ex_binder = Syntax.binder_name @{const_syntax Ex}; 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38715
diff
changeset

643 
val impl = @{const_syntax HOL.implies}; 
22377  644 
val conj = @{const_syntax "op &"}; 
22916  645 
val less = @{const_syntax less}; 
646 
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

647 

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

648 
val trans = 
35115  649 
[((All_binder, impl, less), 
650 
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})), 

651 
((All_binder, impl, less_eq), 

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

653 
((Ex_binder, conj, less), 

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

655 
((Ex_binder, conj, less_eq), 

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

657 

35115  658 
fun matches_bound v t = 
659 
(case t of 

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

663 
fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P; 

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

664 

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

665 
fun tr' q = (q, 
35364  666 
fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _), 
667 
Const (c, _) $ (Const (d, _) $ t $ u) $ P] => 

35115  668 
(case AList.lookup (op =) trans (q, c, d) of 
669 
NONE => raise Match 

670 
 SOME (l, g) => 

671 
if matches_bound v t andalso not (contains_var v u) then mk v l u P 

672 
else if matches_bound v u andalso not (contains_var v t) then mk v g t P 

673 
else raise Match) 

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

674 
 _ => raise Match); 
21524  675 
in [tr' All_binder, tr' Ex_binder] end 
21083  676 
*} 
677 

678 

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

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

680 

25193  681 
context ord 
682 
begin 

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

683 

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

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

686 

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

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

689 

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

692 

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

694 
by (rule ssubst) 

695 

696 
end 

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

697 

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

698 
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

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

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

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

702 
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

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

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

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

706 

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

707 
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

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

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

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

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

712 
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

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

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

715 

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

716 
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

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

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

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

720 
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

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

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

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

724 

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

725 
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

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

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

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

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

730 
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

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

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

733 

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

734 
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

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

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

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

738 
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

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

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

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

742 

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

743 
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

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

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

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

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

748 
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

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

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

751 

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

752 
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

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

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

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

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

757 
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

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

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

760 

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

761 
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

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

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

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

765 
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

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

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

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

769 

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

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

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

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

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

774 
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

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

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

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

778 

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

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

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

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

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

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

784 
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

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

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

787 

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

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

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

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

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

792 
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

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

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

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

796 

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

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

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

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

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

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

802 
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

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

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

805 

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

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

807 
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

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

809 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

826 
mp 
27682  827 

828 
lemmas (in order) [trans] = 

829 
neq_le_trans 

830 
le_neq_trans 

831 

832 
lemmas (in preorder) [trans] = 

833 
less_trans 

834 
less_asym' 

835 
le_less_trans 

836 
less_le_trans 

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

837 
order_trans 
27682  838 

839 
lemmas (in order) [trans] = 

840 
antisym 

841 

842 
lemmas (in ord) [trans] = 

843 
ord_le_eq_trans 

844 
ord_eq_le_trans 

845 
ord_less_eq_trans 

846 
ord_eq_less_trans 

847 

848 
lemmas [trans] = 

849 
trans 

850 

851 
lemmas order_trans_rules = 

852 
order_less_subst2 

853 
order_less_subst1 

854 
order_le_less_subst2 

855 
order_le_less_subst1 

856 
order_less_le_subst2 

857 
order_less_le_subst1 

858 
order_subst2 

859 
order_subst1 

860 
ord_le_eq_subst 

861 
ord_eq_le_subst 

862 
ord_less_eq_subst 

863 
ord_eq_less_subst 

864 
forw_subst 

865 
back_subst 

866 
rev_mp 

867 
mp 

868 
neq_le_trans 

869 
le_neq_trans 

870 
less_trans 

871 
less_asym' 

872 
le_less_trans 

873 
less_le_trans 

874 
order_trans 

875 
antisym 

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

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

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

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

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

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

881 

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

884 

885 
lemma xt1: 

886 
"a = b ==> b > c ==> a > c" 

887 
"a > b ==> b = c ==> a > c" 

888 
"a = b ==> b >= c ==> a >= c" 

889 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  894 
"(a::'a::order) > b ==> b > a ==> P" 
21083  895 
"(x::'a::order) > y ==> y > z ==> x > z" 
896 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  902 
by auto 
21083  903 

904 
lemma xt2: 

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

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

907 

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

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

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

911 

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

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

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

915 

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

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

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

919 

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

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

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

923 

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

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

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

927 

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

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

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

931 

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

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

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

935 

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

937 

938 
(* 

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

940 
for the wrong thing in an Isar proof. 

941 

942 
The extra transitivity rules can be used as follows: 

943 

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

945 
proof  

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

947 
sorry 

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

949 
sorry 

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

951 
sorry 

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

953 
sorry 

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

955 
sorry 

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

957 
sorry 

958 
finally (xtrans) show ?thesis . 

959 
qed 

960 

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

962 
leave out the "(xtrans)" above. 

963 
*) 

964 

23881  965 

966 
subsection {* Monotonicity, least value operator and min/max *} 

21083  967 

25076  968 
context order 
969 
begin 

970 

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

974 
lemma monoI [intro?]: 

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

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

977 
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

978 

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

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

982 
unfolding mono_def by iprover 

983 

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

986 

987 
lemma strict_monoI [intro?]: 

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

989 
shows "strict_mono f" 

990 
using assms unfolding strict_mono_def by auto 

991 

992 
lemma strict_monoD [dest?]: 

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

994 
unfolding strict_mono_def by auto 

995 

996 
lemma strict_mono_mono [dest?]: 

997 
assumes "strict_mono f" 

998 
shows "mono f" 

999 
proof (rule monoI) 

1000 
fix x y 

1001 
assume "x \<le> y" 

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

1003 
proof (cases "x = y") 

1004 
case True then show ?thesis by simp 

1005 
next 

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

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

1008 
then show ?thesis by simp 

1009 
qed 

1010 
qed 

1011 

25076  1012 
end 
1013 

1014 
context linorder 

1015 
begin 

1016 

30298  1017 
lemma strict_mono_eq: 
1018 
assumes "strict_mono f" 

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

1020 
proof 

1021 
assume "f x = f y" 

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

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

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

1025 
next 

1026 
case equal then show ?thesis . 

1027 
next 

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

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

1030 
qed 

1031 
qed simp 

1032 

1033 
lemma strict_mono_less_eq: 

1034 
assumes "strict_mono f" 

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

1036 
proof 

1037 
assume "x \<le> y" 

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

1039 
next 

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

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

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

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

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

1045 
qed 

1046 
qed 

1047 

1048 
lemma strict_mono_less: 

1049 
assumes "strict_mono f" 

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

1051 
using assms 

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

1053 

25076  1054 
lemma min_of_mono: 
1055 
fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder" 

25377  1056 
shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" 
25076  1057 
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) 
1058 

1059 
lemma max_of_mono: 

1060 
fixes f :: "'a \<Rightarrow> 'b\<Colon>linorder" 

25377  1061 
shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" 
25076  1062 
by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) 
1063 

1064 
end 

21083  1065 

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

1066 
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" 
23212  1067 
by (simp add: min_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1068 

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

1069 
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" 
23212  1070 
by (simp add: max_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1071 

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

1072 
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least" 
23212  1073 
apply (simp add: min_def) 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1074 
apply (blast intro: antisym) 
23212  1075 
done 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1076 

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

1077 
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x" 
23212  1078 
apply (simp add: max_def) 
34250
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1079 
apply (blast intro: antisym) 
23212  1080 
done 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1081 

27823  1082 

28685  1083 
subsection {* Top and bottom elements *} 
1084 

1085 
class top = preorder + 

1086 
fixes top :: 'a 

1087 
assumes top_greatest [simp]: "x \<le> top" 

1088 

1089 
class bot = preorder + 

1090 
fixes bot :: 'a 

1091 
assumes bot_least [simp]: "bot \<le> x" 

1092 

1093 

27823  1094 
subsection {* Dense orders *} 
1095 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34974
diff
changeset

1096 
class dense_linorder = linorder + 
27823  1097 
assumes gt_ex: "\<exists>y. x < y" 
1098 
and lt_ex: "\<exists>y. y < x" 

1099 
and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)" 

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

1100 
begin 
27823  1101 

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

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

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

1104 
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

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

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

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

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

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

1110 
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

1111 
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

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

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

1114 

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

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

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

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

1118 
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

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

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

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

1122 
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

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

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

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

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

1127 
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

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

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

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

1131 
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

1132 
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

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

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

1135 

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

1136 
end 
27823  1137 

1138 
subsection {* Wellorders *} 

1139 

1140 
class wellorder = linorder + 

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

1142 
begin 

1143 

1144 
lemma wellorder_Least_lemma: 

1145 
fixes k :: 'a 

1146 
assumes "P k" 

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

1147 
shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k" 
27823  1148 
proof  
1149 
have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k" 

1150 
using assms proof (induct k rule: less_induct) 

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

1152 
show ?case proof (rule classical) 

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

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

1155 
proof (rule classical) 

1156 
fix y 

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

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

1161 
by auto 

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

1163 
qed 

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

1165 
by (rule Least_equality) 

1166 
with `P x` show ?thesis by simp 

1167 
qed 

1168 
qed 

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

1170 
qed 

1171 

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

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

1174 
by (erule exE) (erule LeastI) 

1175 

1176 
lemma LeastI2: 

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

1178 
by (blast intro: LeastI) 

1179 

1180 
lemma LeastI2_ex: 

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

1182 
by (blast intro: LeastI_ex) 

1183 

38705  1184 
lemma LeastI2_wellorder: 
1185 
assumes "P a" 

1186 
and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a" 

1187 
shows "Q (Least P)" 

1188 
proof (rule LeastI2_order) 

1189 
show "P (Least P)" using `P a` by (rule LeastI) 

1190 
next 

1191 
fix y assume "P y" thus "Least P \<le> y" by (rule Least_le) 

1192 
next 

1193 
fix x assume "P x" "\<forall>y. P y \<longrightarrow> x \<le> y" thus "Q x" by (rule assms(2)) 

1194 
qed 

1195 

27823  1196 
lemma not_less_Least: "k < (LEAST x. P x) \<Longrightarrow> \<not> P k" 
1197 
apply (simp (no_asm_use) add: not_le [symmetric]) 

1198 
apply (erule contrapos_nn) 

1199 
apply (erule Least_le) 

1200 
done 

1201 

38705  1202 
end 
27823  1203 

28685  1204 

1205 
subsection {* Order on bool *} 

1206 

1207 
instantiation bool :: "{order, top, bot}" 

1208 
begin 

1209 

1210 
definition 

37767  1211 
le_bool_def: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q" 
28685  1212 

1213 
definition 

37767  1214 
less_bool_def: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q" 
28685  1215 

1216 
definition 

1217 
top_bool_eq: "top = True" 

1218 

1219 
definition 

1220 
bot_bool_eq: "bot = False" 

1221 

1222 
instance proof 

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

1223 
qed (auto simp add: bot_bool_eq top_bool_eq less_bool_def, auto simp add: le_bool_def) 
28685  1224 

15524  1225 
end 
28685  1226 

1227 
lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q" 

32899  1228 
by (simp add: le_bool_def) 
28685  1229 

1230 
lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q" 

32899  1231 
by (simp add: le_bool_def) 
28685  1232 

1233 
lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" 

32899  1234 
by (simp add: le_bool_def) 
28685  1235 

1236 
lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q" 

32899  1237 
by (simp add: le_bool_def) 
1238 

1239 
lemma bot_boolE: "bot \<Longrightarrow> P" 

1240 
by (simp add: bot_bool_eq) 

1241 

1242 
lemma top_boolI: top 

1243 
by (simp add: top_bool_eq) 

28685  1244 

1245 
lemma [code]: 

1246 
"False \<le> b \<longleftrightarrow> True" 

1247 
"True \<le> b \<longleftrightarrow> b" 

1248 
"False < b \<longleftrightarrow> b" 

1249 
"True < b \<longleftrightarrow> False" 

1250 
unfolding le_bool_def less_bool_def by simp_all 

1251 

1252 

1253 
subsection {* Order on functions *} 

1254 

1255 
instantiation "fun" :: (type, ord) ord 

1256 
begin 

1257 

1258 
definition 

37767  1259 
le_fun_def: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)" 
28685  1260 

1261 
definition 

37767  1262 
less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)" 
28685  1263 

1264 
instance .. 

1265 

1266 
end 

1267 

1268 
instance "fun" :: (type, preorder) preorder proof 

1269 
qed (auto simp add: le_fun_def less_fun_def 

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

1270 
intro: order_trans antisym intro!: ext) 
28685  1271 

1272 
instance "fun" :: (type, order) order proof 

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

1273 
qed (auto simp add: le_fun_def intro: antisym ext) 
28685  1274 

1275 
instantiation "fun" :: (type, top) top 

1276 
begin 

1277 

1278 
definition 

38650
f22a564ac820
"no_atp" fact that leads to unsound proofs in Sledgehammer
blanchet
parents:
37767
diff
changeset

1279 
top_fun_eq [no_atp]: "top = (\<lambda>x. top)" 
f22a564ac820
"no_atp" fact that leads to unsound proofs in Sledgehammer
blanchet
parents:
37767
diff
changeset

1280 
declare top_fun_eq_raw [no_atp] 
28685  1281 

1282 
instance proof 

1283 
qed (simp add: top_fun_eq le_fun_def) 

1284 

1285 
end 

1286 

1287 
instantiation "fun" :: (type, bot) bot 

1288 
begin 

1289 

1290 
definition 

1291 
bot_fun_eq: "bot = (\<lambda>x. bot)" 

1292 

1293 
instance proof 

1294 
qed (simp add: bot_fun_eq le_fun_def) 

1295 

1296 
end 

1297 

1298 
lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g" 

1299 
unfolding le_fun_def by simp 

1300 

1301 
lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P" 

1302 
unfolding le_fun_def by simp 

1303 

1304 
lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x" 

1305 
unfolding le_fun_def by simp 

1306 

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

1307 

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

1308 
subsection {* Name duplicates *} 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1309 

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

1310 
lemmas order_eq_refl = preorder_class.eq_refl 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1311 
lemmas order_less_irrefl = preorder_class.less_irrefl 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1312 
lemmas order_less_imp_le = preorder_class.less_imp_le 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1313 
lemmas order_less_not_sym = preorder_class.less_not_sym 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1314 
lemmas order_less_asym = preorder_class.less_asym 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1315 
lemmas order_less_trans = preorder_class.less_trans 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1316 
lemmas order_le_less_trans = preorder_class.le_less_trans 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
haftmann
parents:
34065
diff
changeset

1317 
lemmas order_less_le_trans = preorder_class.less_le_trans 
3b619abaa67a
moved name duplicates to end of theory; reduced warning noise
ha& 