author  haftmann 
Sun, 19 Feb 2012 15:30:35 +0100  
changeset 46553  50a7e97fe653 
parent 45931  99cf6e470816 
child 46557  ae926869a311 
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 

23948  306 

21083  307 
subsection {* Reasoning tools setup *} 
308 

21091  309 
ML {* 
310 

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

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

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

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

314 
val setup: theory > theory 
32215  315 
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

316 
end; 
21091  317 

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

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

320 

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

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

322 

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

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

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

325 

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

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

328 
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

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

330 
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

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

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

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

334 
val extend = I; 
33519  335 
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

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

337 

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

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

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

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

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

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

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

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

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

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

349 
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

350 
end; 
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 

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

353 
(** Method **) 
21091  354 

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

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

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

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

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

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

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

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

363 
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

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

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

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

367 
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

368 
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

369 
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

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

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

372 
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

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

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

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

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

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

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

379 
case s of 
32215  380 
"order" => Order_Tac.partial_tac decomp thms ctxt prems 
381 
 "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

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

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

384 

32215  385 
fun order_tac ctxt prems = 
386 
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

387 

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

388 

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

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

390 

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

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

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

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

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

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

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

397 

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

398 
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

399 
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

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

401 
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

402 
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

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

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

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

406 

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

407 

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

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

409 

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

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

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

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

415 

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

416 

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

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

418 

24867  419 
val setup = 
32215  420 
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

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

422 
attrib_setup; 
21091  423 

424 
end; 

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

425 

21091  426 
*} 
427 

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

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

432 

25076  433 
context order 
434 
begin 

435 

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

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

437 
is not a parameter of the locale. *) 
25076  438 

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

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

442 

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

444 

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

446 

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

448 

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

450 

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

452 

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

454 

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

456 

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

458 

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

460 

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

462 

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

464 

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

466 

467 
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

468 

25076  469 
end 
470 

471 
context linorder 

472 
begin 

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

473 

27689  474 
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] 
475 

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

477 

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

479 

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

481 

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

483 

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

485 

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

487 

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

489 

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

491 

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

25076  493 

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

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

497 

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

499 

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

501 

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

503 

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

505 

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

507 

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

509 

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

511 

512 
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

513 

25076  514 
end 
515 

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

516 

21083  517 
setup {* 
518 
let 

519 

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

21083  522 
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) = 
43597  523 
let val prems = Simplifier.prems_of ss; 
22916  524 
val less = Const (@{const_name less}, T); 
21083  525 
val t = HOLogic.mk_Trueprop(le $ s $ r); 
526 
in case find_first (prp t) prems of 

527 
NONE => 

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

529 
in case find_first (prp t) prems of 

530 
NONE => NONE 

24422  531 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) 
21083  532 
end 
24422  533 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) 
21083  534 
end 
535 
handle THM _ => NONE; 

15524  536 

21083  537 
fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) = 
43597  538 
let val prems = Simplifier.prems_of ss; 
22916  539 
val le = Const (@{const_name less_eq}, T); 
21083  540 
val t = HOLogic.mk_Trueprop(le $ r $ s); 
541 
in case find_first (prp t) prems of 

542 
NONE => 

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

544 
in case find_first (prp t) prems of 

545 
NONE => NONE 

24422  546 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) 
21083  547 
end 
24422  548 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) 
21083  549 
end 
550 
handle THM _ => NONE; 

15524  551 

21248  552 
fun add_simprocs procs thy = 
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42287
diff
changeset

553 
Simplifier.map_simpset_global (fn ss => ss 
21248  554 
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

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

556 

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

557 
fun add_solver name tac = 
42795
66fcc9882784
clarified map_simpset versus Simplifier.map_simpset_global;
wenzelm
parents:
42287
diff
changeset

558 
Simplifier.map_simpset_global (fn ss => ss addSolver 
43597  559 
mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss))); 
21083  560 

561 
in 

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

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

565 
] 

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

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

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

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

21083  571 
end 
572 
*} 

15524  573 

574 

21083  575 
subsection {* Bounded quantifiers *} 
576 

577 
syntax 

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

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

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

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

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

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

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

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

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

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

588 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

599 
syntax (HOL) 

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

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

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

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

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

605 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

616 
translations 

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

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

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

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

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

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

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

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

625 

626 
print_translation {* 

627 
let 

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

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

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

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

631 
val conj = @{const_syntax HOL.conj}; 
22916  632 
val less = @{const_syntax less}; 
633 
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

634 

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

635 
val trans = 
35115  636 
[((All_binder, impl, less), 
637 
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})), 

638 
((All_binder, impl, less_eq), 

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

640 
((Ex_binder, conj, less), 

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

642 
((Ex_binder, conj, less_eq), 

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

644 

35115  645 
fun matches_bound v t = 
646 
(case t of 

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

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

651 

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

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

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

657 
 SOME (l, g) => 

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

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

660 
else raise Match) 

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

661 
 _ => raise Match); 
21524  662 
in [tr' All_binder, tr' Ex_binder] end 
21083  663 
*} 
664 

665 

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

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

667 

25193  668 
context ord 
669 
begin 

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

670 

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

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

673 

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

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

676 

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

679 

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

681 
by (rule ssubst) 

682 

683 
end 

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

684 

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

685 
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

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

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

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

689 
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

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

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

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

693 

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

694 
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

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

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

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

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

699 
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

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

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

702 

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

703 
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

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

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

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

707 
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

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

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

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

711 

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

712 
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

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

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

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

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

717 
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

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

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

720 

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

721 
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

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

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

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

725 
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

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

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

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

729 

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

730 
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

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

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

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

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

735 
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

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

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

738 

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

739 
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

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

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

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

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

744 
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

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

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

747 

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

748 
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

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

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

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

752 
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

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

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

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

756 

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

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

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

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

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

761 
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

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

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

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

765 

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

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

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

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

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

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

771 
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

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

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

774 

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

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

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

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

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

779 
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

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

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

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

783 

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

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

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

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

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

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

789 
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

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

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

792 

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

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

794 
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

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

796 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

813 
mp 
27682  814 

815 
lemmas (in order) [trans] = 

816 
neq_le_trans 

817 
le_neq_trans 

818 

819 
lemmas (in preorder) [trans] = 

820 
less_trans 

821 
less_asym' 

822 
le_less_trans 

823 
less_le_trans 

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

824 
order_trans 
27682  825 

826 
lemmas (in order) [trans] = 

827 
antisym 

828 

829 
lemmas (in ord) [trans] = 

830 
ord_le_eq_trans 

831 
ord_eq_le_trans 

832 
ord_less_eq_trans 

833 
ord_eq_less_trans 

834 

835 
lemmas [trans] = 

836 
trans 

837 

838 
lemmas order_trans_rules = 

839 
order_less_subst2 

840 
order_less_subst1 

841 
order_le_less_subst2 

842 
order_le_less_subst1 

843 
order_less_le_subst2 

844 
order_less_le_subst1 

845 
order_subst2 

846 
order_subst1 

847 
ord_le_eq_subst 

848 
ord_eq_le_subst 

849 
ord_less_eq_subst 

850 
ord_eq_less_subst 

851 
forw_subst 

852 
back_subst 

853 
rev_mp 

854 
mp 

855 
neq_le_trans 

856 
le_neq_trans 

857 
less_trans 

858 
less_asym' 

859 
le_less_trans 

860 
less_le_trans 

861 
order_trans 

862 
antisym 

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

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

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

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

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

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

868 

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

871 

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

872 
lemma xt1 [no_atp]: 
21083  873 
"a = b ==> b > c ==> a > c" 
874 
"a > b ==> b = c ==> a > c" 

875 
"a = b ==> b >= c ==> a >= c" 

876 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  881 
"(a::'a::order) > b ==> b > a ==> P" 
21083  882 
"(x::'a::order) > y ==> y > z ==> x > z" 
883 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  889 
by auto 
21083  890 

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

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

894 

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

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

898 

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

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

902 

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

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

906 

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

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

910 

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

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

914 

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

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

918 

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

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

922 

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

923 
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp] 
21083  924 

925 
(* 

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

927 
for the wrong thing in an Isar proof. 

928 

929 
The extra transitivity rules can be used as follows: 

930 

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

932 
proof  

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

934 
sorry 

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

936 
sorry 

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

938 
sorry 

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

940 
sorry 

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

942 
sorry 

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

944 
sorry 

945 
finally (xtrans) show ?thesis . 

946 
qed 

947 

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

949 
leave out the "(xtrans)" above. 

950 
*) 

951 

23881  952 

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

21083  954 

25076  955 
context order 
956 
begin 

957 

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

961 
lemma monoI [intro?]: 

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

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

964 
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

965 

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

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

969 
unfolding mono_def by iprover 

970 

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

973 

974 
lemma strict_monoI [intro?]: 

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

976 
shows "strict_mono f" 

977 
using assms unfolding strict_mono_def by auto 

978 

979 
lemma strict_monoD [dest?]: 

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

981 
unfolding strict_mono_def by auto 

982 

983 
lemma strict_mono_mono [dest?]: 

984 
assumes "strict_mono f" 

985 
shows "mono f" 

986 
proof (rule monoI) 

987 
fix x y 

988 
assume "x \<le> y" 

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

990 
proof (cases "x = y") 

991 
case True then show ?thesis by simp 

992 
next 

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

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

995 
then show ?thesis by simp 

996 
qed 

997 
qed 

998 

25076  999 
end 
1000 

1001 
context linorder 

1002 
begin 

1003 

30298  1004 
lemma strict_mono_eq: 
1005 
assumes "strict_mono f" 

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

1007 
proof 

1008 
assume "f x = f y" 

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

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

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

1012 
next 

1013 
case equal then show ?thesis . 

1014 
next 

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

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

1017 
qed 

1018 
qed simp 

1019 

1020 
lemma strict_mono_less_eq: 

1021 
assumes "strict_mono f" 

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

1023 
proof 

1024 
assume "x \<le> y" 

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

1026 
next 

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

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

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

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

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

1032 
qed 

1033 
qed 

1034 

1035 
lemma strict_mono_less: 

1036 
assumes "strict_mono f" 

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

1038 
using assms 

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

1040 

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

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

1046 
lemma max_of_mono: 

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

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

1051 
end 

21083  1052 

45931  1053 
lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x" 
23212  1054 
by (simp add: min_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1055 

45931  1056 
lemma max_absorb2: "x \<le> y ==> max x y = y" 
23212  1057 
by (simp add: max_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1058 

45931  1059 
lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y" 
1060 
by (simp add:min_def) 

45893  1061 

45931  1062 
lemma max_absorb1: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> max x y = x" 
45893  1063 
by (simp add: max_def) 
1064 

1065 

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

1066 

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

1067 
subsection {* (Unique) top and bottom elements *} 
28685  1068 

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

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

1070 
fixes bot :: 'a ("\<bottom>") 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1071 
assumes bot_least [simp]: "\<bottom> \<le> a" 
43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

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

1073 

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

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

1075 
"a \<le> \<bottom> \<Longrightarrow> a = \<bottom>" 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1076 
by (auto intro: antisym) 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1077 

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

1079 
"a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>" 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1080 
by (auto intro: antisym) 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1081 

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

1082 
lemma not_less_bot [simp]: 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1083 
"\<not> (a < \<bottom>)" 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1084 
using bot_least [of a] by (auto simp: le_less) 
43816  1085 

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

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

1087 
"a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a" 
43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1088 
by (auto simp add: less_le_not_le intro!: antisym) 
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1089 

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

1090 
end 
41082  1091 

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

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

1093 
fixes top :: 'a ("\<top>") 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1094 
assumes top_greatest [simp]: "a \<le> \<top>" 
43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

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

1096 

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

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

1098 
"\<top> \<le> a \<Longrightarrow> a = \<top>" 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1099 
by (rule antisym) auto 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1100 

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

1102 
"\<top> \<le> a \<longleftrightarrow> a = \<top>" 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1103 
by (auto intro: antisym) 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1104 

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

1105 
lemma not_top_less [simp]: "\<not> (\<top> < a)" 
020ddc6a9508
consolidated bot and top classes, tuned notation
haftmann
parents:
43816
diff
changeset

1106 
using top_greatest [of a] by (auto simp: le_less) 
43816  1107 

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

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

1109 
"a \<noteq> \<top> \<longleftrightarrow> a < \<top>" 
43814
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1110 
by (auto simp add: less_le_not_le intro!: antisym) 
58791b75cf1f
moved lemmas bot_less and less_top to classes bot and top respectively
haftmann
parents:
43813
diff
changeset

1111 

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

1112 
end 
28685  1113 

1114 

27823  1115 
subsection {* Dense orders *} 
1116 

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

1117 
class dense_linorder = linorder + 
27823  1118 
assumes gt_ex: "\<exists>y. x < y" 
1119 
and lt_ex: "\<exists>y. y < x" 

1120 
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

1121 
begin 
27823  1122 

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

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

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

1125 
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

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

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

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

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

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

1131 
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

1132 
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

1133 
ultimately show False by auto 
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 
lemma dense_le_bounded: 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35364
diff
changeset

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

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

1139 
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

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

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

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

1143 
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

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

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

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

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

1148 
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

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

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

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

1152 
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

1153 
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

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

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

1156 

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

1157 
end 
27823  1158 

1159 
subsection {* Wellorders *} 

1160 

1161 
class wellorder = linorder + 

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

1163 
begin 

1164 

1165 
lemma wellorder_Least_lemma: 

1166 
fixes k :: 'a 

1167 
assumes "P k" 

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

1168 
shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k" 
27823  1169 
proof  
1170 
have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k" 

1171 
using assms proof (induct k rule: less_induct) 

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

1173 
show ?case proof (rule classical) 

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

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

1176 
proof (rule classical) 

1177 
fix y 

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

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

1182 
by auto 

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

1184 
qed 

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

1186 
by (rule Least_equality) 

1187 
with `P x` show ?thesis by simp 

1188 
qed 

1189 
qed 

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

1191 
qed 

1192 

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

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

1195 
by (erule exE) (erule LeastI) 

1196 

1197 
lemma LeastI2: 

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

1199 
by (blast intro: LeastI) 

1200 

1201 
lemma LeastI2_ex: 

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

1203 
by (blast intro: LeastI_ex) 

1204 

38705  1205 
lemma LeastI2_wellorder: 
1206 
assumes "P a" 

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

1208 
shows "Q (Least P)" 

1209 
proof (rule LeastI2_order) 

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

1211 
next 

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

1213 
next 

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

1215 
qed 

1216 

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

1219 
apply (erule contrapos_nn) 

1220 
apply (erule Least_le) 

1221 
done 

1222 

38705  1223 
end 
27823  1224 

28685  1225 

1226 
subsection {* Order on bool *} 

1227 

45262  1228 
instantiation bool :: "{bot, top, linorder}" 
28685  1229 
begin 
1230 

1231 
definition 

41080  1232 
le_bool_def [simp]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q" 
28685  1233 

1234 
definition 

41080  1235 
[simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q" 
28685  1236 

1237 
definition 

46553
50a7e97fe653
distributed lattice properties of predicates to places of instantiation
haftmann
parents:
45931
diff
changeset

1238 
[simp]: "\<bottom> \<longleftrightarrow> False" 
28685  1239 

1240 
definition 

46553
50a7e97fe653
distributed lattice properties of predicates to places of instantiation
haftmann
parents:
45931
diff
changeset

1241 
[simp]: "\<top> \<longleftrightarrow> True" 
28685  1242 

1243 
instance proof 

41080  1244 
qed auto 
28685  1245 

15524  1246 
end 
28685  1247 

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

41080  1249 
by simp 
28685  1250 

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

41080  1252 
by simp 
28685  1253 

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

41080  1255 
by simp 
28685  1256 

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

41080  1258 
by simp 
32899  1259 

46553
50a7e97fe653
distributed lattice properties of predicates to places of instantiation
haftmann
parents:
45931
diff
changeset

1260 
lemma bot_boolE: "\<bottom> \<Longrightarrow> P" 
41080  1261 
by simp 
32899  1262 

46553
50a7e97fe653
distributed lattice properties of predicates to places of instantiation
haftmann
parents:
45931
diff
changeset

1263 
lemma top_boolI: \<top> 
41080  1264 
by simp 
28685  1265 

1266 
lemma [code]: 

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

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

1269 
"False < b \<longleftrightarrow> b" 

1270 
"True < b \<longleftrightarrow> False" 

41080  1271 
by simp_all 
28685  1272 

1273 

1274 
subsection {* Order on functions *} 

1275 

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

1277 
begin 

1278 

1279 
definition 

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

1282 
definition 

41080  1283 
"(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)" 
28685  1284 

1285 
instance .. 

1286 

1287 
end 

1288 

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

1290 
qed (auto simp add: le_fun_def less_fun_def 

44921  1291 
intro: order_trans antisym) 
28685  1292 

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

44921  1294 
qed (auto simp add: le_fun_def intro: antisym) 
28685  1295 

41082  1296 
instantiation "fun" :: (type, bot) bot 
1297 
begin 

1298 

1299 
definition 

46553
50a7e97fe653
distributed lattice properties of predicates to places of instantiation
haftmann
parents:
45931
diff
changeset

1300 
"\<bottom> = (\<lambda>x. \<bottom>)" 
41082  1301 

1302 
lemma bot_apply: 

46553
50a7e97fe653
distributed lattice properties of predicates to places of instantiation
haftmann
parents:
45931
diff
changeset

1303 
"\<bottom> x = \<bottom>" 
41082  1304 
by (simp add: bot_fun_def) 
1305 

1306 
instance proof 

1307 
qed (simp add: le_fun_def bot_apply) 

1308 

1309 
end 