author  haftmann 
Fri, 24 Aug 2007 14:14:18 +0200  
changeset 24422  c0b5ff9e9e4d 
parent 24286  7619080e49f0 
child 24641  448edc627ee4 
permissions  rwrr 
15524  1 
(* Title: HOL/Orderings.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, Markus Wenzel, and Larry Paulson 

4 
*) 

5 

21329  6 
header {* Syntactic and abstract orders *} 
15524  7 

8 
theory Orderings 

23881  9 
imports Set Fun 
23263  10 
uses 
11 
(*"~~/src/Provers/quasi.ML"*) 

12 
"~~/src/Provers/order.ML" 

15524  13 
begin 
14 

22841  15 
subsection {* Partial orders *} 
15524  16 

22841  17 
class order = ord + 
22316  18 
assumes less_le: "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y" 
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22377
diff
changeset

19 
and order_refl [iff]: "x \<sqsubseteq> x" 
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22377
diff
changeset

20 
and order_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" 
22841  21 
assumes antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y" 
22 

21248  23 
begin 
24 

15524  25 
text {* Reflexivity. *} 
26 

22841  27 
lemma eq_refl: "x = y \<Longrightarrow> x \<^loc>\<le> y" 
15524  28 
 {* This form is useful with the classical reasoner. *} 
23212  29 
by (erule ssubst) (rule order_refl) 
15524  30 

22841  31 
lemma less_irrefl [iff]: "\<not> x \<^loc>< x" 
23212  32 
by (simp add: less_le) 
15524  33 

22841  34 
lemma le_less: "x \<^loc>\<le> y \<longleftrightarrow> x \<^loc>< y \<or> x = y" 
15524  35 
 {* NOT suitable for iff, since it can cause PROOF FAILED. *} 
23212  36 
by (simp add: less_le) blast 
15524  37 

22841  38 
lemma le_imp_less_or_eq: "x \<^loc>\<le> y \<Longrightarrow> x \<^loc>< y \<or> x = y" 
23212  39 
unfolding less_le by blast 
15524  40 

22841  41 
lemma less_imp_le: "x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y" 
23212  42 
unfolding less_le by blast 
21248  43 

22841  44 
lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y" 
23212  45 
by (erule contrapos_pn, erule subst, rule less_irrefl) 
21329  46 

47 

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

49 

22841  50 
lemma less_imp_not_eq: "x \<^loc>< y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 
23212  51 
by auto 
21329  52 

22841  53 
lemma less_imp_not_eq2: "x \<^loc>< y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 
23212  54 
by auto 
21329  55 

56 

57 
text {* Transitivity rules for calculational reasoning *} 

58 

22841  59 
lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<^loc>\<le> b \<Longrightarrow> a \<^loc>< b" 
23212  60 
by (simp add: less_le) 
21329  61 

22841  62 
lemma le_neq_trans: "a \<^loc>\<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a \<^loc>< b" 
23212  63 
by (simp add: less_le) 
21329  64 

15524  65 

66 
text {* Asymmetry. *} 

67 

22841  68 
lemma less_not_sym: "x \<^loc>< y \<Longrightarrow> \<not> (y \<^loc>< x)" 
23212  69 
by (simp add: less_le antisym) 
15524  70 

22841  71 
lemma less_asym: "x \<^loc>< y \<Longrightarrow> (\<not> P \<Longrightarrow> y \<^loc>< x) \<Longrightarrow> P" 
23212  72 
by (drule less_not_sym, erule contrapos_np) simp 
15524  73 

22841  74 
lemma eq_iff: "x = y \<longleftrightarrow> x \<^loc>\<le> y \<and> y \<^loc>\<le> x" 
23212  75 
by (blast intro: antisym) 
15524  76 

22841  77 
lemma antisym_conv: "y \<^loc>\<le> x \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y" 
23212  78 
by (blast intro: antisym) 
15524  79 

22841  80 
lemma less_imp_neq: "x \<^loc>< y \<Longrightarrow> x \<noteq> y" 
23212  81 
by (erule contrapos_pn, erule subst, rule less_irrefl) 
21248  82 

21083  83 

15524  84 
text {* Transitivity. *} 
85 

22841  86 
lemma less_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z" 
23212  87 
by (simp add: less_le) (blast intro: order_trans antisym) 
15524  88 

22841  89 
lemma le_less_trans: "x \<^loc>\<le> y \<Longrightarrow> y \<^loc>< z \<Longrightarrow> x \<^loc>< z" 
23212  90 
by (simp add: less_le) (blast intro: order_trans antisym) 
15524  91 

22841  92 
lemma less_le_trans: "x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<^loc>< z" 
23212  93 
by (simp add: less_le) (blast intro: order_trans antisym) 
15524  94 

95 

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

97 

22841  98 
lemma less_imp_not_less: "x \<^loc>< y \<Longrightarrow> (\<not> y \<^loc>< x) \<longleftrightarrow> True" 
23212  99 
by (blast elim: less_asym) 
15524  100 

22841  101 
lemma less_imp_triv: "x \<^loc>< y \<Longrightarrow> (y \<^loc>< x \<longrightarrow> P) \<longleftrightarrow> True" 
23212  102 
by (blast elim: less_asym) 
15524  103 

21248  104 

21083  105 
text {* Transitivity rules for calculational reasoning *} 
15524  106 

22841  107 
lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P" 
23212  108 
by (rule less_asym) 
21248  109 

22916  110 

111 
text {* Reverse order *} 

112 

113 
lemma order_reverse: 

23018
1d29bc31b0cb
no special treatment in naming of locale predicates stemming form classes
haftmann
parents:
22997
diff
changeset

114 
"order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)" 
23212  115 
by unfold_locales 
116 
(simp add: less_le, auto intro: antisym order_trans) 

22916  117 

21248  118 
end 
15524  119 

21329  120 

121 
subsection {* Linear (total) orders *} 

122 

22316  123 
class linorder = order + 
21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

124 
assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x" 
21248  125 
begin 
126 

22841  127 
lemma less_linear: "x \<^loc>< y \<or> x = y \<or> y \<^loc>< x" 
23212  128 
unfolding less_le using less_le linear by blast 
21248  129 

22841  130 
lemma le_less_linear: "x \<^loc>\<le> y \<or> y \<^loc>< x" 
23212  131 
by (simp add: le_less less_linear) 
21248  132 

133 
lemma le_cases [case_names le ge]: 

22841  134 
"(x \<^loc>\<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>\<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  135 
using linear by blast 
21248  136 

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

137 
lemma linorder_cases [case_names less equal greater]: 
23212  138 
"(x \<^loc>< y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> P) \<Longrightarrow> P" 
139 
using less_linear by blast 

21248  140 

22841  141 
lemma not_less: "\<not> x \<^loc>< y \<longleftrightarrow> y \<^loc>\<le> x" 
23212  142 
apply (simp add: less_le) 
143 
using linear apply (blast intro: antisym) 

144 
done 

145 

146 
lemma not_less_iff_gr_or_eq: 

147 
"\<not>(x \<^loc>< y) \<longleftrightarrow> (x \<^loc>> y  x = y)" 

148 
apply(simp add:not_less le_less) 

149 
apply blast 

150 
done 

15524  151 

22841  152 
lemma not_le: "\<not> x \<^loc>\<le> y \<longleftrightarrow> y \<^loc>< x" 
23212  153 
apply (simp add: less_le) 
154 
using linear apply (blast intro: antisym) 

155 
done 

15524  156 

22841  157 
lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x \<^loc>< y \<or> y \<^loc>< x" 
23212  158 
by (cut_tac x = x and y = y in less_linear, auto) 
15524  159 

22841  160 
lemma neqE: "x \<noteq> y \<Longrightarrow> (x \<^loc>< y \<Longrightarrow> R) \<Longrightarrow> (y \<^loc>< x \<Longrightarrow> R) \<Longrightarrow> R" 
23212  161 
by (simp add: neq_iff) blast 
15524  162 

22841  163 
lemma antisym_conv1: "\<not> x \<^loc>< y \<Longrightarrow> x \<^loc>\<le> y \<longleftrightarrow> x = y" 
23212  164 
by (blast intro: antisym dest: not_less [THEN iffD1]) 
15524  165 

22841  166 
lemma antisym_conv2: "x \<^loc>\<le> y \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y" 
23212  167 
by (blast intro: antisym dest: not_less [THEN iffD1]) 
15524  168 

22841  169 
lemma antisym_conv3: "\<not> y \<^loc>< x \<Longrightarrow> \<not> x \<^loc>< y \<longleftrightarrow> x = y" 
23212  170 
by (blast intro: antisym dest: not_less [THEN iffD1]) 
15524  171 

16796  172 
text{*Replacing the old Nat.leI*} 
22841  173 
lemma leI: "\<not> x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x" 
23212  174 
unfolding not_less . 
16796  175 

22841  176 
lemma leD: "y \<^loc>\<le> x \<Longrightarrow> \<not> x \<^loc>< y" 
23212  177 
unfolding not_less . 
16796  178 

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

22841  180 
lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y" 
23212  181 
unfolding not_le . 
21248  182 

22916  183 

184 
text {* Reverse order *} 

185 

186 
lemma linorder_reverse: 

23018
1d29bc31b0cb
no special treatment in naming of locale predicates stemming form classes
haftmann
parents:
22997
diff
changeset

187 
"linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)" 
23212  188 
by unfold_locales 
189 
(simp add: less_le, auto intro: antisym order_trans simp add: linear) 

22916  190 

191 

23881  192 
text {* min/max *} 
193 

194 
text {* for historic reasons, definitions are done in context ord *} 

195 

196 
definition (in ord) 

197 
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

23948  198 
[code unfold, code inline del]: "min a b = (if a \<^loc>\<le> b then a else b)" 
23881  199 

200 
definition (in ord) 

201 
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 

23948  202 
[code unfold, code inline del]: "max a b = (if a \<^loc>\<le> b then b else a)" 
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22377
diff
changeset

203 

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

204 
lemma min_le_iff_disj: 
22841  205 
"min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z" 
23212  206 
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

207 

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

208 
lemma le_max_iff_disj: 
22841  209 
"z \<^loc>\<le> max x y \<longleftrightarrow> z \<^loc>\<le> x \<or> z \<^loc>\<le> y" 
23212  210 
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

211 

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

212 
lemma min_less_iff_disj: 
22841  213 
"min x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<or> y \<^loc>< z" 
23212  214 
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

215 

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

216 
lemma less_max_iff_disj: 
22841  217 
"z \<^loc>< max x y \<longleftrightarrow> z \<^loc>< x \<or> z \<^loc>< y" 
23212  218 
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

219 

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

220 
lemma min_less_iff_conj [simp]: 
22841  221 
"z \<^loc>< min x y \<longleftrightarrow> z \<^loc>< x \<and> z \<^loc>< y" 
23212  222 
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

223 

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

224 
lemma max_less_iff_conj [simp]: 
22841  225 
"max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z" 
23212  226 
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

227 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23948
diff
changeset

228 
lemma split_min [noatp]: 
22841  229 
"P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)" 
23212  230 
by (simp add: min_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

231 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
23948
diff
changeset

232 
lemma split_max [noatp]: 
22841  233 
"P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)" 
23212  234 
by (simp add: max_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

235 

21248  236 
end 
237 

23948  238 

21083  239 
subsection {* Reasoning tools setup *} 
240 

21091  241 
ML {* 
242 
local 

243 

244 
fun decomp_gen sort thy (Trueprop $ t) = 

21248  245 
let 
246 
fun of_sort t = 

247 
let 

248 
val T = type_of t 

249 
in 

21091  250 
(* exclude numeric types: linear arithmetic subsumes transitivity *) 
21248  251 
T <> HOLogic.natT andalso T <> HOLogic.intT 
252 
andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) 

253 
end; 

22916  254 
fun dec (Const (@{const_name Not}, _) $ t) = (case dec t 
21248  255 
of NONE => NONE 
256 
 SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) 

22916  257 
 dec (Const (@{const_name "op ="}, _) $ t1 $ t2) = 
21248  258 
if of_sort t1 
259 
then SOME (t1, "=", t2) 

260 
else NONE 

23881  261 
 dec (Const (@{const_name HOL.less_eq}, _) $ t1 $ t2) = 
21248  262 
if of_sort t1 
263 
then SOME (t1, "<=", t2) 

264 
else NONE 

23881  265 
 dec (Const (@{const_name HOL.less}, _) $ t1 $ t2) = 
21248  266 
if of_sort t1 
267 
then SOME (t1, "<", t2) 

268 
else NONE 

269 
 dec _ = NONE; 

21091  270 
in dec t end; 
271 

272 
in 

273 

22841  274 
(* sorry  there is no preorder class 
21248  275 
structure Quasi_Tac = Quasi_Tac_Fun ( 
276 
struct 

277 
val le_trans = thm "order_trans"; 

278 
val le_refl = thm "order_refl"; 

279 
val eqD1 = thm "order_eq_refl"; 

280 
val eqD2 = thm "sym" RS thm "order_eq_refl"; 

281 
val less_reflE = thm "order_less_irrefl" RS thm "notE"; 

282 
val less_imp_le = thm "order_less_imp_le"; 

283 
val le_neq_trans = thm "order_le_neq_trans"; 

284 
val neq_le_trans = thm "order_neq_le_trans"; 

285 
val less_imp_neq = thm "less_imp_neq"; 

22738  286 
val decomp_trans = decomp_gen ["Orderings.preorder"]; 
287 
val decomp_quasi = decomp_gen ["Orderings.preorder"]; 

22841  288 
end);*) 
21091  289 

290 
structure Order_Tac = Order_Tac_Fun ( 

21248  291 
struct 
24422  292 
val less_reflE = @{thm less_irrefl} RS @{thm notE}; 
293 
val le_refl = @{thm order_refl}; 

294 
val less_imp_le = @{thm less_imp_le}; 

295 
val not_lessI = @{thm not_less} RS @{thm iffD2}; 

296 
val not_leI = @{thm not_le} RS @{thm iffD2}; 

297 
val not_lessD = @{thm not_less} RS @{thm iffD1}; 

298 
val not_leD = @{thm not_le} RS @{thm iffD1}; 

299 
val eqI = @{thm antisym}; 

300 
val eqD1 = @{thm eq_refl}; 

301 
val eqD2 = @{thm sym} RS @{thm eq_refl}; 

302 
val less_trans = @{thm less_trans}; 

303 
val less_le_trans = @{thm less_le_trans}; 

304 
val le_less_trans = @{thm le_less_trans}; 

305 
val le_trans = @{thm order_trans}; 

306 
val le_neq_trans = @{thm le_neq_trans}; 

307 
val neq_le_trans = @{thm neq_le_trans}; 

308 
val less_imp_neq = @{thm less_imp_neq}; 

309 
val eq_neq_eq_imp_neq = @{thm eq_neq_eq_imp_neq}; 

310 
val not_sym = @{thm not_sym}; 

21248  311 
val decomp_part = decomp_gen ["Orderings.order"]; 
312 
val decomp_lin = decomp_gen ["Orderings.linorder"]; 

313 
end); 

21091  314 

315 
end; 

316 
*} 

317 

21083  318 
setup {* 
319 
let 

320 

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

15524  322 

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

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

328 
NONE => 

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

330 
in case find_first (prp t) prems of 

331 
NONE => NONE 

24422  332 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) 
21083  333 
end 
24422  334 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) 
21083  335 
end 
336 
handle THM _ => NONE; 

15524  337 

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

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

343 
NONE => 

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

345 
in case find_first (prp t) prems of 

346 
NONE => NONE 

24422  347 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) 
21083  348 
end 
24422  349 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) 
21083  350 
end 
351 
handle THM _ => NONE; 

15524  352 

21248  353 
fun add_simprocs procs thy = 
354 
(Simplifier.change_simpset_of thy (fn ss => ss 

355 
addsimprocs (map (fn (name, raw_ts, proc) => 

356 
Simplifier.simproc thy name raw_ts proc)) procs); thy); 

357 
fun add_solver name tac thy = 

358 
(Simplifier.change_simpset_of thy (fn ss => ss addSolver 

359 
(mk_solver name (K tac))); thy); 

21083  360 

361 
in 

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

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

365 
] 

366 
#> add_solver "Trans_linear" Order_Tac.linear_tac 

367 
#> add_solver "Trans_partial" Order_Tac.partial_tac 

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

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

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

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

21083  372 
end 
373 
*} 

15524  374 

375 

24422  376 
subsection {* Dense orders *} 
377 

378 
class dense_linear_order = linorder + 

379 
assumes gt_ex: "\<exists>y. x \<sqsubset> y" 

380 
and lt_ex: "\<exists>y. y \<sqsubset> x" 

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

382 
(*see further theory Dense_Linear_Order*) 

383 

384 
lemma interval_empty_iff: 

385 
fixes x y z :: "'a\<Colon>dense_linear_order" 

386 
shows "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" 

387 
by (auto dest: dense) 

388 

389 
subsection {* Name duplicates *} 

390 

391 
lemmas order_less_le = less_le 

392 
lemmas order_eq_refl = order_class.eq_refl 

393 
lemmas order_less_irrefl = order_class.less_irrefl 

394 
lemmas order_le_less = order_class.le_less 

395 
lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq 

396 
lemmas order_less_imp_le = order_class.less_imp_le 

397 
lemmas order_less_imp_not_eq = order_class.less_imp_not_eq 

398 
lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 

399 
lemmas order_neq_le_trans = order_class.neq_le_trans 

400 
lemmas order_le_neq_trans = order_class.le_neq_trans 

401 

402 
lemmas order_antisym = antisym 

403 
lemmas order_less_not_sym = order_class.less_not_sym 

404 
lemmas order_less_asym = order_class.less_asym 

405 
lemmas order_eq_iff = order_class.eq_iff 

406 
lemmas order_antisym_conv = order_class.antisym_conv 

407 
lemmas order_less_trans = order_class.less_trans 

408 
lemmas order_le_less_trans = order_class.le_less_trans 

409 
lemmas order_less_le_trans = order_class.less_le_trans 

410 
lemmas order_less_imp_not_less = order_class.less_imp_not_less 

411 
lemmas order_less_imp_triv = order_class.less_imp_triv 

412 
lemmas order_less_asym' = order_class.less_asym' 

413 

414 
lemmas linorder_linear = linear 

415 
lemmas linorder_less_linear = linorder_class.less_linear 

416 
lemmas linorder_le_less_linear = linorder_class.le_less_linear 

417 
lemmas linorder_le_cases = linorder_class.le_cases 

418 
lemmas linorder_not_less = linorder_class.not_less 

419 
lemmas linorder_not_le = linorder_class.not_le 

420 
lemmas linorder_neq_iff = linorder_class.neq_iff 

421 
lemmas linorder_neqE = linorder_class.neqE 

422 
lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 

423 
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 

424 
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 

425 

426 
lemmas min_le_iff_disj = linorder_class.min_le_iff_disj 

427 
lemmas le_max_iff_disj = linorder_class.le_max_iff_disj 

428 
lemmas min_less_iff_disj = linorder_class.min_less_iff_disj 

429 
lemmas less_max_iff_disj = linorder_class.less_max_iff_disj 

430 
lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj 

431 
lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj 

432 
lemmas split_min = linorder_class.split_min 

433 
lemmas split_max = linorder_class.split_max 

434 

435 

21083  436 
subsection {* Bounded quantifiers *} 
437 

438 
syntax 

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

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

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

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

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

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

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

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

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

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

449 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

460 
syntax (HOL) 

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

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

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

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

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

466 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

477 
translations 

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

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

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

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

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

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

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

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

486 

487 
print_translation {* 

488 
let 

22916  489 
val All_binder = Syntax.binder_name @{const_syntax All}; 
490 
val Ex_binder = Syntax.binder_name @{const_syntax Ex}; 

22377  491 
val impl = @{const_syntax "op >"}; 
492 
val conj = @{const_syntax "op &"}; 

22916  493 
val less = @{const_syntax less}; 
494 
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

495 

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

496 
val trans = 
21524  497 
[((All_binder, impl, less), ("_All_less", "_All_greater")), 
498 
((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), 

499 
((Ex_binder, conj, less), ("_Ex_less", "_Ex_greater")), 

500 
((Ex_binder, conj, less_eq), ("_Ex_less_eq", "_Ex_greater_eq"))]; 

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

501 

22344
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

502 
fun matches_bound v t = 
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

503 
case t of (Const ("_bound", _) $ Free (v', _)) => (v = v') 
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

504 
 _ => false 
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

505 
fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v  _ => false) 
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

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

507 

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

508 
fun tr' q = (q, 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

509 
fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] => 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

510 
(case AList.lookup (op =) trans (q, c, d) of 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

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

512 
 SOME (l, g) => 
22344
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

513 
if matches_bound v t andalso not (contains_var v u) then mk v l u P 
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

514 
else if matches_bound v u andalso not (contains_var v t) then mk v g t P 
eddeabf16b5d
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
krauss
parents:
22316
diff
changeset

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

516 
 _ => raise Match); 
21524  517 
in [tr' All_binder, tr' Ex_binder] end 
21083  518 
*} 
519 

520 

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

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

522 

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

523 
lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" 
23212  524 
by (rule subst) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

525 

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

526 
lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" 
23212  527 
by (rule ssubst) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

528 

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

529 
lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" 
23212  530 
by (rule subst) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

531 

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

532 
lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" 
23212  533 
by (rule ssubst) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

534 

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

535 
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

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

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

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

539 
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

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

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

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

543 

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

544 
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

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

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

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

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

549 
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

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

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

552 

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

553 
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

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

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

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

557 
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

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

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

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

561 

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

562 
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

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

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

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

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

567 
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

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

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

570 

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

571 
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

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

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

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

575 
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

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

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

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

579 

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

580 
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

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

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

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

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

585 
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

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

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

588 

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

589 
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

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

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

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

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

594 
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

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

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

597 

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

598 
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

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

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

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

602 
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

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

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

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

606 

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

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

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

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

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

611 
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

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

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

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

615 

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

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

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

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

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

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

621 
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

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

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

624 

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

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

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

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

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

629 
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

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

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

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

633 

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

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

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

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

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

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

639 
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

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

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

642 

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

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

644 
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

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

646 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

677 

21083  678 

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

679 
(* FIXME cleanup *) 
f27f12bcafb8
fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
wenzelm
parents:
21091
diff
changeset

680 

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

683 

684 
lemma xt1: 

685 
"a = b ==> b > c ==> a > c" 

686 
"a > b ==> b = c ==> a > c" 

687 
"a = b ==> b >= c ==> a >= c" 

688 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  693 
"(a::'a::order) > b ==> b > a ==> P" 
21083  694 
"(x::'a::order) > y ==> y > z ==> x > z" 
695 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

701 
by auto 

702 

703 
lemma xt2: 

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

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

706 

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

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

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

710 

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

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

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

714 

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

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

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

718 

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

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

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

722 

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

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

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

726 

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

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

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

730 

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

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

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

734 

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

736 

737 
(* 

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

739 
for the wrong thing in an Isar proof. 

740 

741 
The extra transitivity rules can be used as follows: 

742 

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

744 
proof  

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

746 
sorry 

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

748 
sorry 

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

750 
sorry 

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

752 
sorry 

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

754 
sorry 

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

756 
sorry 

757 
finally (xtrans) show ?thesis . 

758 
qed 

759 

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

761 
leave out the "(xtrans)" above. 

762 
*) 

763 

21546  764 
subsection {* Order on bool *} 
765 

22886  766 
instance bool :: order 
21546  767 
le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q" 
768 
less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q" 

22916  769 
by intro_classes (auto simp add: le_bool_def less_bool_def) 
24422  770 
lemmas [code func del] = le_bool_def less_bool_def 
21546  771 

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

23212  773 
by (simp add: le_bool_def) 
21546  774 

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

23212  776 
by (simp add: le_bool_def) 
21546  777 

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

23212  779 
by (simp add: le_bool_def) 
21546  780 

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

23212  782 
by (simp add: le_bool_def) 
21546  783 

22348  784 
lemma [code func]: 
785 
"False \<le> b \<longleftrightarrow> True" 

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

787 
"False < b \<longleftrightarrow> b" 

788 
"True < b \<longleftrightarrow> False" 

789 
unfolding le_bool_def less_bool_def by simp_all 

790 

22424  791 

23881  792 
subsection {* Order on sets *} 
793 

794 
instance set :: (type) order 

795 
by (intro_classes, 

796 
(assumption  rule subset_refl subset_trans subset_antisym psubset_eq)+) 

797 

798 
lemmas basic_trans_rules [trans] = 

799 
order_trans_rules set_rev_mp set_mp 

800 

801 

802 
subsection {* Order on functions *} 

803 

804 
instance "fun" :: (type, ord) ord 

805 
le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x" 

806 
less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" .. 

807 

808 
lemmas [code func del] = le_fun_def less_fun_def 

809 

810 
instance "fun" :: (type, order) order 

811 
by default 

812 
(auto simp add: le_fun_def less_fun_def expand_fun_eq 

813 
intro: order_trans order_antisym) 

814 

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

816 
unfolding le_fun_def by simp 

817 

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

819 
unfolding le_fun_def by simp 

820 

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

822 
unfolding le_fun_def by simp 

823 

824 
text {* 

825 
Handy introduction and elimination rules for @{text "\<le>"} 

826 
on unary and binary predicates 

827 
*} 

828 

829 
lemma predicate1I [Pure.intro!, intro!]: 

830 
assumes PQ: "\<And>x. P x \<Longrightarrow> Q x" 

831 
shows "P \<le> Q" 

832 
apply (rule le_funI) 

833 
apply (rule le_boolI) 

834 
apply (rule PQ) 

835 
apply assumption 

836 
done 

837 

838 
lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x" 

839 
apply (erule le_funE) 

840 
apply (erule le_boolE) 

841 
apply assumption+ 

842 
done 

843 

844 
lemma predicate2I [Pure.intro!, intro!]: 

845 
assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y" 

846 
shows "P \<le> Q" 

847 
apply (rule le_funI)+ 

848 
apply (rule le_boolI) 

849 
apply (rule PQ) 

850 
apply assumption 

851 
done 

852 

853 
lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y" 

854 
apply (erule le_funE)+ 

855 
apply (erule le_boolE) 

856 
apply assumption+ 

857 
done 

858 

859 
lemma rev_predicate1D: "P x ==> P <= Q ==> Q x" 

860 
by (rule predicate1D) 

861 

862 
lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y" 

863 
by (rule predicate2D) 

864 

865 

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

21083  867 

21216
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

868 
locale mono = 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

869 
fixes f 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

870 
assumes mono: "A \<le> B \<Longrightarrow> f A \<le> f B" 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

871 

1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

872 
lemmas monoI [intro?] = mono.intro 
1c8580913738
made locale partial_order compatible with axclass order; changed import order; consecutive changes
haftmann
parents:
21204
diff
changeset

873 
and monoD [dest?] = mono.mono 
21083  874 

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

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

876 
"[ P (x::'a::order); 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

877 
!!y. P y ==> x <= y; 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

878 
!!x. [ P x; ALL y. P y > x \<le> y ] ==> Q x ] 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

879 
==> Q (Least P)" 
23212  880 
apply (unfold Least_def) 
881 
apply (rule theI2) 

882 
apply (blast intro: order_antisym)+ 

883 
done 

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

884 

23881  885 
lemma Least_mono: 
886 
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y 

887 
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" 

888 
 {* Courtesy of Stephan Merz *} 

889 
apply clarify 

890 
apply (erule_tac P = "%x. x : S" in LeastI2_order, fast) 

891 
apply (rule LeastI2_order) 

892 
apply (auto elim: monoD intro!: order_antisym) 

893 
done 

894 

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

895 
lemma Least_equality: 
23212  896 
"[ P (k::'a::order); !!x. P x ==> k <= x ] ==> (LEAST x. P x) = k" 
897 
apply (simp add: Least_def) 

898 
apply (rule the_equality) 

899 
apply (auto intro!: order_antisym) 

900 
done 

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

901 

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

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

904 

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

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

907 

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

908 
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least" 
23212  909 
apply (simp add: min_def) 
910 
apply (blast intro: order_antisym) 

911 
done 

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

912 

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

913 
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x" 
23212  914 
apply (simp add: max_def) 
915 
apply (blast intro: order_antisym) 

916 
done 

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

917 

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

918 
lemma min_of_mono: 
23212  919 
"(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" 
920 
by (simp add: min_def) 

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

921 

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

922 
lemma max_of_mono: 
23212  923 
"(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" 
924 
by (simp add: max_def) 

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

925 

22548  926 

927 
subsection {* legacy ML bindings *} 

21673  928 

929 
ML {* 

22548  930 
val monoI = @{thm monoI}; 
22886  931 
*} 
21673  932 

15524  933 
end 