author  wenzelm 
Sat, 29 Sep 2012 18:23:46 +0200  
changeset 49660  de49d9b4d7bc 
parent 48891  c0eafbd55de3 
child 49769  c7c2152322f2 
permissions  rwrr 
28685  1 
(* Title: HOL/Orderings.thy 
15524  2 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 
3 
*) 

4 

25614  5 
header {* Abstract orderings *} 
15524  6 

7 
theory Orderings 

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

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

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

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

14 

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

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

16 

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

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

18 
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

19 
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

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

21 

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

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

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

24 
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

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

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

27 

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

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

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

30 
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

31 

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

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

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

34 
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

35 

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

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

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

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

39 

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

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

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

42 

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

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

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

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

46 

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

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

48 

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

49 

27682  50 
subsection {* Quasi orders *} 
15524  51 

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

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

21248  56 
begin 
57 

15524  58 
text {* Reflexivity. *} 
59 

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

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

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

68 
unfolding less_le_not_le by blast 

69 

70 

71 
text {* Asymmetry. *} 

72 

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

74 
by (simp add: less_le_not_le) 

75 

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

77 
by (drule less_not_sym, erule contrapos_np) simp 

78 

79 

80 
text {* Transitivity. *} 

81 

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

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

84 

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

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

87 

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

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

90 

91 

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

93 

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

95 
by (blast elim: less_asym) 

96 

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

98 
by (blast elim: less_asym) 

99 

100 

101 
text {* Transitivity rules for calculational reasoning *} 

102 

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

104 
by (rule less_asym) 

105 

106 

107 
text {* Dual order *} 

108 

109 
lemma dual_preorder: 

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

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

113 
end 

114 

115 

116 
subsection {* Partial orders *} 

117 

118 
class order = preorder + 

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

120 
begin 

121 

122 
text {* Reflexivity. *} 

123 

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

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

15524  126 

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

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

21329  134 

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

136 

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

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

143 

144 
text {* Transitivity rules for calculational reasoning *} 

145 

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

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

15524  152 

153 
text {* Asymmetry. *} 

154 

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

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

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

21083  164 

27107  165 
text {* Least value operator *} 
166 

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

170 

171 
lemma Least_equality: 

172 
assumes "P x" 

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

174 
shows "Least P = x" 

175 
unfolding Least_def by (rule the_equality) 

176 
(blast intro: assms antisym)+ 

177 

178 
lemma LeastI2_order: 

179 
assumes "P x" 

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

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

182 
shows "Q (Least P)" 

183 
unfolding Least_def by (rule theI2) 

184 
(blast intro: assms antisym)+ 

185 

186 

26014  187 
text {* Dual order *} 
22916  188 

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

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

21248  193 
end 
15524  194 

21329  195 

196 
subsection {* Linear (total) orders *} 

197 

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

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

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

208 
lemma le_cases [case_names le ge]: 

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

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

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

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

219 
done 

220 

221 
lemma not_less_iff_gr_or_eq: 

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

225 
done 

15524  226 

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

230 
done 

15524  231 

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

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

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

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

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

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

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

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

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

22916  257 

26014  258 
text {* Dual order *} 
22916  259 

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

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

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

264 

23881  265 
text {* min/max *} 
266 

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

27299  270 
definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 
37767  271 
"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

272 

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

273 
lemma min_le_iff_disj: 
25062  274 
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" 
23212  275 
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

276 

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

277 
lemma le_max_iff_disj: 
25062  278 
"z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" 
23212  279 
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

280 

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

281 
lemma min_less_iff_disj: 
25062  282 
"min x y < z \<longleftrightarrow> x < z \<or> y < z" 
23212  283 
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

284 

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

285 
lemma less_max_iff_disj: 
25062  286 
"z < max x y \<longleftrightarrow> z < x \<or> z < y" 
23212  287 
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

288 

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

289 
lemma min_less_iff_conj [simp]: 
25062  290 
"z < min x y \<longleftrightarrow> z < x \<and> z < y" 
23212  291 
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

292 

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

293 
lemma max_less_iff_conj [simp]: 
25062  294 
"max x y < z \<longleftrightarrow> x < z \<and> y < z" 
23212  295 
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

296 

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

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

300 

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

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

304 

21248  305 
end 
306 

23948  307 

21083  308 
subsection {* Reasoning tools setup *} 
309 

21091  310 
ML {* 
311 

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

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

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

314 
val print_structures: Proof.context > unit 
47432  315 
val attrib_setup: theory > theory 
32215  316 
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

317 
end; 
21091  318 

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

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

321 

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

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

323 

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

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

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

326 

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

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

329 
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

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

331 
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

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

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

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

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

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

338 

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

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

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

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

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

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

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

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

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

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

350 
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

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

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

354 
(** Method **) 
21091  355 

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

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

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

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

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

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

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

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

364 
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

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

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

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

368 
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

369 
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

370 
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

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

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

373 
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

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

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

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

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

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

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

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

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

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

385 

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

388 

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

389 

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

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

391 

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

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

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

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

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

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

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

398 

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

399 
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

400 
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

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

402 
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

403 
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

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

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

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

407 

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

408 

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

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

410 

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

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

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

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

416 

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

418 

21091  419 
*} 
420 

47432  421 
setup Orders.attrib_setup 
422 

423 
method_setup order = {* 

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

425 
*} "transitivity reasoner" 

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

426 

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

427 

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

428 
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

429 

25076  430 
context order 
431 
begin 

432 

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

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

434 
is not a parameter of the locale. *) 
25076  435 

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

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

439 

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

441 

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

443 

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

445 

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

447 

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

449 

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

451 

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

453 

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

455 

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

457 

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

459 

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

461 

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

463 

464 
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

465 

25076  466 
end 
467 

468 
context linorder 

469 
begin 

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

470 

27689  471 
declare [[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"]] 
472 

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

474 

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

476 

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

478 

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

480 

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

482 

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

484 

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

486 

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

488 

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

25076  490 

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

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

494 

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

496 

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

498 

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

500 

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

502 

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

504 

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

506 

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

508 

509 
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

510 

25076  511 
end 
512 

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

513 

21083  514 
setup {* 
515 
let 

516 

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

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

524 
NONE => 

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

526 
in case find_first (prp t) prems of 

527 
NONE => NONE 

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

15524  533 

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

539 
NONE => 

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

541 
in case find_first (prp t) prems of 

542 
NONE => NONE 

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

15524  548 

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

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

552 
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

553 

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

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

555 
Simplifier.map_simpset_global (fn ss => ss addSolver 
43597  556 
mk_solver name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of ss))); 
21083  557 

558 
in 

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

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

562 
] 

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

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

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

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

21083  568 
end 
569 
*} 

15524  570 

571 

21083  572 
subsection {* Bounded quantifiers *} 
573 

574 
syntax 

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

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

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

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

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

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

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

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

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

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

585 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

596 
syntax (HOL) 

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

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

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

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

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

602 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

613 
translations 

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

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

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

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

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

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

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

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

622 

623 
print_translation {* 

624 
let 

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

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

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

627 
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

628 
val conj = @{const_syntax HOL.conj}; 
22916  629 
val less = @{const_syntax less}; 
630 
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

631 

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

632 
val trans = 
35115  633 
[((All_binder, impl, less), 
634 
(@{syntax_const "_All_less"}, @{syntax_const "_All_greater"})), 

635 
((All_binder, impl, less_eq), 

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

637 
((Ex_binder, conj, less), 

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

639 
((Ex_binder, conj, less_eq), 

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

641 

35115  642 
fun matches_bound v t = 
643 
(case t of 

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

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

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

648 

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

649 
fun tr' q = (q, 
49660
de49d9b4d7bc
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents:
48891
diff
changeset

650 
fn [Const (@{syntax_const "_bound"}, _) $ Free (v, T), 
35364  651 
Const (c, _) $ (Const (d, _) $ t $ u) $ P] => 
35115  652 
(case AList.lookup (op =) trans (q, c, d) of 
653 
NONE => raise Match 

654 
 SOME (l, g) => 

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

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

656 
else if matches_bound v u andalso not (contains_var v t) then mk (v, T) g t P 
35115  657 
else raise Match) 
21180
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

658 
 _ => raise Match); 
21524  659 
in [tr' All_binder, tr' Ex_binder] end 
21083  660 
*} 
661 

662 

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

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

664 

25193  665 
context ord 
666 
begin 

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

667 

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

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

670 

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

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

673 

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

676 

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

678 
by (rule ssubst) 

679 

680 
end 

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

681 

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

682 
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

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

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

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

686 
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

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

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

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

690 

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

691 
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

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

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

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

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

696 
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

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

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

699 

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

700 
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

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

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

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

704 
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

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

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

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

708 

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

709 
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

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

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

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

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

714 
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

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

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

717 

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

718 
lemma order_less_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

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

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

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

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

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

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

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

726 

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

727 
lemma order_less_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

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

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

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

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

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

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

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

735 

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

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

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

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

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

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

741 
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

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

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

744 

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

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

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

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

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

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

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

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

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

753 

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

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

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

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

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

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

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

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

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

762 

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

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

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

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

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

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

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

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

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

771 

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

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

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

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

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

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

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

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

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

780 

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

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

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

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

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

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

786 
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

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

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

789 

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

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

791 
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

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

793 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

810 
mp 
27682  811 

812 
lemmas (in order) [trans] = 

813 
neq_le_trans 

814 
le_neq_trans 

815 

816 
lemmas (in preorder) [trans] = 

817 
less_trans 

818 
less_asym' 

819 
le_less_trans 

820 
less_le_trans 

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

821 
order_trans 
27682  822 

823 
lemmas (in order) [trans] = 

824 
antisym 

825 

826 
lemmas (in ord) [trans] = 

827 
ord_le_eq_trans 

828 
ord_eq_le_trans 

829 
ord_less_eq_trans 

830 
ord_eq_less_trans 

831 

832 
lemmas [trans] = 

833 
trans 

834 

835 
lemmas order_trans_rules = 

836 
order_less_subst2 

837 
order_less_subst1 

838 
order_le_less_subst2 

839 
order_le_less_subst1 

840 
order_less_le_subst2 

841 
order_less_le_subst1 

842 
order_subst2 

843 
order_subst1 

844 
ord_le_eq_subst 

845 
ord_eq_le_subst 

846 
ord_less_eq_subst 

847 
ord_eq_less_subst 

848 
forw_subst 

849 
back_subst 

850 
rev_mp 

851 
mp 

852 
neq_le_trans 

853 
le_neq_trans 

854 
less_trans 

855 
less_asym' 

856 
le_less_trans 

857 
less_le_trans 

858 
order_trans 

859 
antisym 

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

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

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

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

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

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

865 

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

868 

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

869 
lemma xt1 [no_atp]: 
21083  870 
"a = b ==> b > c ==> a > c" 
871 
"a > b ==> b = c ==> a > c" 

872 
"a = b ==> b >= c ==> a >= c" 

873 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  878 
"(a::'a::order) > b ==> b > a ==> P" 
21083  879 
"(x::'a::order) > y ==> y > z ==> x > z" 
880 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  886 
by auto 
21083  887 

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

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

891 

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

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

895 

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

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

899 

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

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

903 

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

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

907 

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

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

911 

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

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

915 

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

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

919 

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

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

922 
(* 

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

924 
for the wrong thing in an Isar proof. 

925 

926 
The extra transitivity rules can be used as follows: 

927 

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

929 
proof  

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

931 
sorry 

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

933 
sorry 

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

935 
sorry 

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

937 
sorry 

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

939 
sorry 

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

941 
sorry 

942 
finally (xtrans) show ?thesis . 

943 
qed 

944 

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

946 
leave out the "(xtrans)" above. 

947 
*) 

948 

23881  949 

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

21083  951 

25076  952 
context order 
953 
begin 

954 

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

958 
lemma monoI [intro?]: 

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

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

961 
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

962 

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

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

966 
unfolding mono_def by iprover 

967 

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

970 

971 
lemma strict_monoI [intro?]: 

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

973 
shows "strict_mono f" 

974 
using assms unfolding strict_mono_def by auto 

975 

976 
lemma strict_monoD [dest?]: 

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

978 
unfolding strict_mono_def by auto 

979 

980 
lemma strict_mono_mono [dest?]: 

981 
assumes "strict_mono f" 

982 
shows "mono f" 

983 
proof (rule monoI) 

984 
fix x y 

985 
assume "x \<le> y" 

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

987 
proof (cases "x = y") 

988 
case True then show ?thesis by simp 

989 
next 

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

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

992 
then show ?thesis by simp 

993 
qed 

994 
qed 

995 

25076  996 
end 
997 

998 
context linorder 

999 
begin 

1000 

30298  1001 
lemma strict_mono_eq: 
1002 
assumes "strict_mono f" 

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

1004 
proof 

1005 
assume "f x = f y" 

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

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

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

1009 
next 

1010 
case equal then show ?thesis . 

1011 
next 

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

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

1014 
qed 

1015 
qed simp 

1016 

1017 
lemma strict_mono_less_eq: 

1018 
assumes "strict_mono f" 

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

1020 
proof 

1021 
assume "x \<le> y" 

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

1023 
next 

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

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

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

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

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

1029 
qed 

1030 
qed 

1031 

1032 
lemma strict_mono_less: 

1033 
assumes "strict_mono f" 

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

1035 
using assms 

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

1037 

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

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

1043 
lemma max_of_mono: 

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

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

1048 
end 

21083  1049 

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

1052 

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

1055 

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

45893  1058 

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

1062 

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

1063 

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

1064 
subsection {* (Unique) top and bottom elements *} 
28685  1065 

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

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

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

1068 
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

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

1070 

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

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

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

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

1074 

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

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

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

1078 

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

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

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

1081 
using bot_least [of a] by (auto simp: le_less) 
43816  1082 

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

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

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

1085 
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

1086 

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

1087 
end 
41082  1088 

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

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

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

1091 
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

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

1093 

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

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

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

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

1097 

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

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

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

1101 

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

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

1103 
using top_greatest [of a] by (auto simp: le_less) 
43816  1104 

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

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

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

1107 
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

1108 

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

1109 
end 
28685  1110 

1111 

27823  1112 
subsection {* Dense orders *} 
1113 

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

1114 
class dense_linorder = linorder + 
27823  1115 
assumes gt_ex: "\<exists>y. x < y" 
1116 
and lt_ex: "\<exists>y. y < x" 

1117 
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

1118 
begin 
27823  1119 

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

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

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

1122 
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

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

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

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

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

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

1128 
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

1129 
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

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

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

1132 

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

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

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

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

1136 
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

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

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

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

1140 
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

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

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

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

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

1145 
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

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

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

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

1149 
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

1150 
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

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

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

1153 

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

1154 
end 
27823  1155 

1156 
subsection {* Wellorders *} 

1157 

1158 
class wellorder = linorder + 

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

1160 
begin 

1161 

1162 
lemma wellorder_Least_lemma: 

1163 
fixes k :: 'a 

1164 
assumes "P k" 

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

1165 
shows LeastI: "P (LEAST x. P x)" and Least_le: "(LEAST x. P x) \<le> k" 
27823  1166 
proof  
1167 
have "P (LEAST x. P x) \<and> (LEAST x. P x) \<le> k" 

1168 
using assms proof (induct k rule: less_induct) 

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

1170 
show ?case proof (rule classical) 

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

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

1173 
proof (rule classical) 

1174 
fix y 

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

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

1179 
by auto 

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

1181 
qed 

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

1183 
by (rule Least_equality) 

1184 
with `P x` show ?thesis by simp 

1185 
qed 

1186 
qed 

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

1188 
qed 

1189 

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

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

1192 
by (erule exE) (erule LeastI) 

1193 

1194 
lemma LeastI2: 

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

1196 
by (blast intro: LeastI) 

1197 

1198 
lemma LeastI2_ex: 

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

1200 
by (blast intro: LeastI_ex) 

1201 

38705  1202 
lemma LeastI2_wellorder: 
1203 
assumes "P a" 

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

1205 
shows "Q (Least P)" 

1206 
proof (rule LeastI2_order) 

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

1208 
next 

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

1210 
next 

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

1212 
qed 

1213 

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

1216 
apply (erule contrapos_nn) 

1217 
apply (erule Least_le) 

1218 
done 

1219 

38705  1220 
end 
27823  1221 

28685  1222 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1223 
subsection {* Order on @{typ bool} *} 
28685  1224 

45262  1225 
instantiation bool :: "{bot, top, linorder}" 
28685  1226 
begin 
1227 

1228 
definition 

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

1231 
definition 

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

1234 
definition 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1235 
[simp]: "\<bottom> \<longleftrightarrow> False" 
28685  1236 

1237 
definition 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1238 
[simp]: "\<top> \<longleftrightarrow> True" 
28685  1239 

1240 
instance proof 

41080  1241 
qed auto 
28685  1242 

15524  1243 
end 
28685  1244 

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

41080  1246 
by simp 
28685  1247 

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

41080  1249 
by simp 
28685  1250 

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

41080  1252 
by simp 
28685  1253 

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

41080  1255 
by simp 
32899  1256 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1257 
lemma bot_boolE: "\<bottom> \<Longrightarrow> P" 
41080  1258 
by simp 
32899  1259 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1260 
lemma top_boolI: \<top> 
41080  1261 
by simp 
28685  1262 

1263 
lemma [code]: 

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

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

1266 
"False < b \<longleftrightarrow> b" 

1267 
"True < b \<longleftrightarrow> False" 

41080  1268 
by simp_all 
28685  1269 

1270 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1271 
subsection {* Order on @{typ "_ \<Rightarrow> _"} *} 
28685  1272 

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

1274 
begin 

1275 

1276 
definition 

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

1279 
definition 

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

1282 
instance .. 

1283 

1284 
end 

1285 

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

1287 
qed (auto simp add: le_fun_def less_fun_def 

44921  1288 
intro: order_trans antisym) 
28685  1289 

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

44921  1291 
qed (auto simp add: le_fun_def intro: antisym) 
28685  1292 

41082  1293 
instantiation "fun" :: (type, bot) bot 
1294 
begin 

1295 

1296 
definition 

46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1297 
"\<bottom> = (\<lambda>x. \<bottom>)" 
41082  1298 

46882  1299 
lemma bot_apply [simp] (* CANDIDATE [code] *): 
46631
2c5c003cee35
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
haftmann
parents:
46557
diff
changeset

1300 
"\<bottom> x = \<bottom>" 
41082  1301 
by (simp add: bot_fun_def) 
1302 

1303 
instance proof 

46884  1304 
qed (simp add: le_fun_def) 
41082  1305 

1306 
end 
