author  haftmann 
Wed, 19 Mar 2008 07:20:28 +0100  
changeset 26324  456f726a11e4 
parent 26300  03def556e26e 
child 26496  49ae9456eba9 
permissions  rwrr 
15524  1 
(* Title: HOL/Orderings.thy 
2 
ID: $Id$ 

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

4 
*) 

5 

25614  6 
header {* Abstract orderings *} 
15524  7 

8 
theory Orderings 

23881  9 
imports Set Fun 
23263  10 
uses 
11 
"~~/src/Provers/order.ML" 

15524  12 
begin 
13 

22841  14 
subsection {* Partial orders *} 
15524  15 

22841  16 
class order = ord + 
25062  17 
assumes less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y" 
18 
and order_refl [iff]: "x \<le> x" 

19 
and order_trans: "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z" 

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

21248  21 
begin 
22 

15524  23 
text {* Reflexivity. *} 
24 

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

25062  29 
lemma less_irrefl [iff]: "\<not> x < x" 
23212  30 
by (simp add: less_le) 
15524  31 

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

25062  36 
lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y" 
23212  37 
unfolding less_le by blast 
15524  38 

25062  39 
lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y" 
23212  40 
unfolding less_le by blast 
21248  41 

21329  42 

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

44 

25062  45 
lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False" 
23212  46 
by auto 
21329  47 

25062  48 
lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 
23212  49 
by auto 
21329  50 

51 

52 
text {* Transitivity rules for calculational reasoning *} 

53 

25062  54 
lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b" 
23212  55 
by (simp add: less_le) 
21329  56 

25062  57 
lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b" 
23212  58 
by (simp add: less_le) 
21329  59 

15524  60 

61 
text {* Asymmetry. *} 

62 

25062  63 
lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)" 
23212  64 
by (simp add: less_le antisym) 
15524  65 

25062  66 
lemma less_asym: "x < y \<Longrightarrow> (\<not> P \<Longrightarrow> y < x) \<Longrightarrow> P" 
23212  67 
by (drule less_not_sym, erule contrapos_np) simp 
15524  68 

25062  69 
lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x" 
23212  70 
by (blast intro: antisym) 
15524  71 

25062  72 
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y" 
23212  73 
by (blast intro: antisym) 
15524  74 

25062  75 
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y" 
23212  76 
by (erule contrapos_pn, erule subst, rule less_irrefl) 
21248  77 

21083  78 

15524  79 
text {* Transitivity. *} 
80 

25062  81 
lemma less_trans: "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" 
23212  82 
by (simp add: less_le) (blast intro: order_trans antisym) 
15524  83 

25062  84 
lemma le_less_trans: "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z" 
23212  85 
by (simp add: less_le) (blast intro: order_trans antisym) 
15524  86 

25062  87 
lemma less_le_trans: "x < y \<Longrightarrow> y \<le> z \<Longrightarrow> x < z" 
23212  88 
by (simp add: less_le) (blast intro: order_trans antisym) 
15524  89 

90 

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

92 

25062  93 
lemma less_imp_not_less: "x < y \<Longrightarrow> (\<not> y < x) \<longleftrightarrow> True" 
23212  94 
by (blast elim: less_asym) 
15524  95 

25062  96 
lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True" 
23212  97 
by (blast elim: less_asym) 
15524  98 

21248  99 

21083  100 
text {* Transitivity rules for calculational reasoning *} 
15524  101 

25062  102 
lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P" 
23212  103 
by (rule less_asym) 
21248  104 

22916  105 

26014  106 
text {* Dual order *} 
22916  107 

26014  108 
lemma dual_order: 
25103  109 
"order (op \<ge>) (op >)" 
23212  110 
by unfold_locales 
111 
(simp add: less_le, auto intro: antisym order_trans) 

22916  112 

21248  113 
end 
15524  114 

21329  115 

116 
subsection {* Linear (total) orders *} 

117 

22316  118 
class linorder = order + 
25207  119 
assumes linear: "x \<le> y \<or> y \<le> x" 
21248  120 
begin 
121 

25062  122 
lemma less_linear: "x < y \<or> x = y \<or> y < x" 
23212  123 
unfolding less_le using less_le linear by blast 
21248  124 

25062  125 
lemma le_less_linear: "x \<le> y \<or> y < x" 
23212  126 
by (simp add: le_less less_linear) 
21248  127 

128 
lemma le_cases [case_names le ge]: 

25062  129 
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  130 
using linear by blast 
21248  131 

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

132 
lemma linorder_cases [case_names less equal greater]: 
25062  133 
"(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  134 
using less_linear by blast 
21248  135 

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

139 
done 

140 

141 
lemma not_less_iff_gr_or_eq: 

25062  142 
"\<not>(x < y) \<longleftrightarrow> (x > y  x = y)" 
23212  143 
apply(simp add:not_less le_less) 
144 
apply blast 

145 
done 

15524  146 

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

150 
done 

15524  151 

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

25062  155 
lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R" 
23212  156 
by (simp add: neq_iff) blast 
15524  157 

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

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

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

16796  167 
text{*Replacing the old Nat.leI*} 
25062  168 
lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x" 
23212  169 
unfolding not_less . 
16796  170 

25062  171 
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y" 
23212  172 
unfolding not_less . 
16796  173 

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

25062  175 
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y" 
23212  176 
unfolding not_le . 
21248  177 

22916  178 

26014  179 
text {* Dual order *} 
22916  180 

26014  181 
lemma dual_linorder: 
25103  182 
"linorder (op \<ge>) (op >)" 
23212  183 
by unfold_locales 
184 
(simp add: less_le, auto intro: antisym order_trans simp add: linear) 

22916  185 

186 

23881  187 
text {* min/max *} 
188 

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

190 

191 
definition (in ord) 

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

25062  193 
[code unfold, code inline del]: "min a b = (if a \<le> b then a else b)" 
23881  194 

195 
definition (in ord) 

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

25062  197 
[code unfold, code inline del]: "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

198 

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

199 
lemma min_le_iff_disj: 
25062  200 
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" 
23212  201 
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

202 

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

203 
lemma le_max_iff_disj: 
25062  204 
"z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" 
23212  205 
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

206 

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

207 
lemma min_less_iff_disj: 
25062  208 
"min x y < z \<longleftrightarrow> x < z \<or> y < z" 
23212  209 
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

210 

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

211 
lemma less_max_iff_disj: 
25062  212 
"z < max x y \<longleftrightarrow> z < x \<or> z < y" 
23212  213 
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

214 

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

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

218 

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

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

222 

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

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

226 

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

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

230 

21248  231 
end 
232 

23948  233 

21083  234 
subsection {* Reasoning tools setup *} 
235 

21091  236 
ML {* 
237 

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

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

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

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

241 
val setup: theory > theory 
24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

242 
val order_tac: thm list > Proof.context > int > tactic 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

243 
end; 
21091  244 

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

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

247 

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

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

249 

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

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

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

252 

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

253 
structure Data = GenericDataFun 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

255 
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

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

257 
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

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

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

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

261 
val extend = I; 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

262 
fun merge _ = AList.join struct_eq (K fst); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

264 

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

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

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

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

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

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

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

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

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

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

276 
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

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

278 

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

279 

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

280 
(** Method **) 
21091  281 

24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

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

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

284 
fun decomp thy (Trueprop $ t) = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

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

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

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

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

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

291 
end; 
24741
a53f5db5acbb
Fixed setup of transitivity reasoner (function decomp).
ballarin
parents:
24704
diff
changeset

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

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

294 
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

295 
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

296 
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

297 
else NONE 
24741
a53f5db5acbb
Fixed setup of transitivity reasoner (function decomp).
ballarin
parents:
24704
diff
changeset

298 
 rel _ = NONE; 
a53f5db5acbb
Fixed setup of transitivity reasoner (function decomp).
ballarin
parents:
24704
diff
changeset

299 
fun dec (Const (@{const_name Not}, _) $ t) = (case rel t 
a53f5db5acbb
Fixed setup of transitivity reasoner (function decomp).
ballarin
parents:
24704
diff
changeset

300 
of NONE => NONE 
a53f5db5acbb
Fixed setup of transitivity reasoner (function decomp).
ballarin
parents:
24704
diff
changeset

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

302 
 dec x = rel x; 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

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

305 
case s of 
24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

306 
"order" => Order_Tac.partial_tac decomp thms prems 
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

307 
 "linorder" => Order_Tac.linear_tac decomp thms prems 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

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

310 

24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

311 
fun order_tac prems ctxt = 
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

312 
FIRST' (map (fn s => CHANGED o struct_tac s prems) (Data.get (Context.Proof ctxt))); 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

313 

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

314 

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

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

316 

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

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

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

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

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

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

322 
(fn _ => Data.map (AList.delete struct_eq s)); 
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 
val attribute = Attrib.syntax 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

325 
(Scan.lift ((Args.add  Args.name >> (fn (_, s) => SOME s)  
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

326 
Args.del >> K NONE)  Args.colon (* FIXME  
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

327 
Scan.succeed true *) )  Scan.lift Args.name  
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

328 
Scan.repeat Args.term 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

329 
>> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

330 
 ((NONE, n), ts) => del_struct (n, ts))); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

331 

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

332 

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

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

334 

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

335 
val print = Toplevel.unknown_context o 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

336 
Toplevel.keep (Toplevel.node_case 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

337 
(Context.cases (print_structures o ProofContext.init) print_structures) 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

339 

24867  340 
val _ = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

341 
OuterSyntax.improper_command "print_orders" 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

342 
"print order structures available to transitivity reasoner" OuterKeyword.diag 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

343 
(Scan.succeed (Toplevel.no_timing o print)); 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

344 

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

345 

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

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

347 

24867  348 
val setup = 
349 
Method.add_methods 

350 
[("order", Method.ctxt_args (Method.SIMPLE_METHOD' o order_tac []), "transitivity reasoner")] #> 

351 
Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")]; 

21091  352 

353 
end; 

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

354 

21091  355 
*} 
356 

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

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

358 

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

359 

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

360 
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

361 

25076  362 
context order 
363 
begin 

364 

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

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

366 
is not a parameter of the locale. *) 
25076  367 

368 
lemmas 

369 
[order add less_reflE: order "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <=" "op <"] = 

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

370 
less_irrefl [THEN notE] 
25076  371 
lemmas 
25062  372 
[order add le_refl: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

373 
order_refl 
25076  374 
lemmas 
25062  375 
[order add less_imp_le: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

376 
less_imp_le 
25076  377 
lemmas 
25062  378 
[order add eqI: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

379 
antisym 
25076  380 
lemmas 
25062  381 
[order add eqD1: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

382 
eq_refl 
25076  383 
lemmas 
25062  384 
[order add eqD2: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

385 
sym [THEN eq_refl] 
25076  386 
lemmas 
25062  387 
[order add less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

388 
less_trans 
25076  389 
lemmas 
25062  390 
[order add less_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

391 
less_le_trans 
25076  392 
lemmas 
25062  393 
[order add le_less_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

394 
le_less_trans 
25076  395 
lemmas 
25062  396 
[order add le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

397 
order_trans 
25076  398 
lemmas 
25062  399 
[order add le_neq_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

400 
le_neq_trans 
25076  401 
lemmas 
25062  402 
[order add neq_le_trans: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

403 
neq_le_trans 
25076  404 
lemmas 
25062  405 
[order add less_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

406 
less_imp_neq 
25076  407 
lemmas 
25062  408 
[order add eq_neq_eq_imp_neq: order "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

409 
eq_neq_eq_imp_neq 
25076  410 
lemmas 
25062  411 
[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

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

413 

25076  414 
end 
415 

416 
context linorder 

417 
begin 

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

418 

25076  419 
lemmas 
420 
[order del: order "op = :: 'a => 'a => bool" "op <=" "op <"] = _ 

421 

422 
lemmas 

25062  423 
[order add less_reflE: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

424 
less_irrefl [THEN notE] 
25076  425 
lemmas 
25062  426 
[order add le_refl: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

427 
order_refl 
25076  428 
lemmas 
25062  429 
[order add less_imp_le: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

430 
less_imp_le 
25076  431 
lemmas 
25062  432 
[order add not_lessI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

433 
not_less [THEN iffD2] 
25076  434 
lemmas 
25062  435 
[order add not_leI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

436 
not_le [THEN iffD2] 
25076  437 
lemmas 
25062  438 
[order add not_lessD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

439 
not_less [THEN iffD1] 
25076  440 
lemmas 
25062  441 
[order add not_leD: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

442 
not_le [THEN iffD1] 
25076  443 
lemmas 
25062  444 
[order add eqI: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

445 
antisym 
25076  446 
lemmas 
25062  447 
[order add eqD1: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

448 
eq_refl 
25076  449 
lemmas 
25062  450 
[order add eqD2: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

451 
sym [THEN eq_refl] 
25076  452 
lemmas 
25062  453 
[order add less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

454 
less_trans 
25076  455 
lemmas 
25062  456 
[order add less_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

457 
less_le_trans 
25076  458 
lemmas 
25062  459 
[order add le_less_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

460 
le_less_trans 
25076  461 
lemmas 
25062  462 
[order add le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

463 
order_trans 
25076  464 
lemmas 
25062  465 
[order add le_neq_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

466 
le_neq_trans 
25076  467 
lemmas 
25062  468 
[order add neq_le_trans: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

469 
neq_le_trans 
25076  470 
lemmas 
25062  471 
[order add less_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

472 
less_imp_neq 
25076  473 
lemmas 
25062  474 
[order add eq_neq_eq_imp_neq: linorder "op = :: 'a => 'a => bool" "op <=" "op <"] = 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

475 
eq_neq_eq_imp_neq 
25076  476 
lemmas 
25062  477 
[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

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

479 

25076  480 
end 
481 

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

482 

21083  483 
setup {* 
484 
let 

485 

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

15524  487 

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

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

493 
NONE => 

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

495 
in case find_first (prp t) prems of 

496 
NONE => NONE 

24422  497 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})) 
21083  498 
end 
24422  499 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm order_class.antisym_conv})) 
21083  500 
end 
501 
handle THM _ => NONE; 

15524  502 

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

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

508 
NONE => 

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

510 
in case find_first (prp t) prems of 

511 
NONE => NONE 

24422  512 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})) 
21083  513 
end 
24422  514 
 SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv2})) 
21083  515 
end 
516 
handle THM _ => NONE; 

15524  517 

21248  518 
fun add_simprocs procs thy = 
519 
(Simplifier.change_simpset_of thy (fn ss => ss 

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

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

522 
fun add_solver name tac thy = 

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

24704
9a95634ab135
Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
ballarin
parents:
24641
diff
changeset

524 
(mk_solver' name (fn ss => tac (MetaSimplifier.prems_of_ss ss) (MetaSimplifier.the_context ss)))); thy); 
21083  525 

526 
in 

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

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

530 
] 

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

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

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

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

21083  536 
end 
537 
*} 

15524  538 

539 

24422  540 
subsection {* Dense orders *} 
541 

542 
class dense_linear_order = linorder + 

25076  543 
assumes gt_ex: "\<exists>y. x < y" 
544 
and lt_ex: "\<exists>y. y < x" 

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

24422  546 
(*see further theory Dense_Linear_Order*) 
25076  547 
begin 
24641
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

548 

24422  549 
lemma interval_empty_iff: 
25076  550 
"{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z" 
24422  551 
by (auto dest: dense) 
552 

25076  553 
end 
554 

24422  555 
subsection {* Name duplicates *} 
556 

557 
lemmas order_less_le = less_le 

558 
lemmas order_eq_refl = order_class.eq_refl 

559 
lemmas order_less_irrefl = order_class.less_irrefl 

560 
lemmas order_le_less = order_class.le_less 

561 
lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq 

562 
lemmas order_less_imp_le = order_class.less_imp_le 

563 
lemmas order_less_imp_not_eq = order_class.less_imp_not_eq 

564 
lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 

565 
lemmas order_neq_le_trans = order_class.neq_le_trans 

566 
lemmas order_le_neq_trans = order_class.le_neq_trans 

567 

568 
lemmas order_antisym = antisym 

569 
lemmas order_less_not_sym = order_class.less_not_sym 

570 
lemmas order_less_asym = order_class.less_asym 

571 
lemmas order_eq_iff = order_class.eq_iff 

572 
lemmas order_antisym_conv = order_class.antisym_conv 

573 
lemmas order_less_trans = order_class.less_trans 

574 
lemmas order_le_less_trans = order_class.le_less_trans 

575 
lemmas order_less_le_trans = order_class.less_le_trans 

576 
lemmas order_less_imp_not_less = order_class.less_imp_not_less 

577 
lemmas order_less_imp_triv = order_class.less_imp_triv 

578 
lemmas order_less_asym' = order_class.less_asym' 

579 

580 
lemmas linorder_linear = linear 

581 
lemmas linorder_less_linear = linorder_class.less_linear 

582 
lemmas linorder_le_less_linear = linorder_class.le_less_linear 

583 
lemmas linorder_le_cases = linorder_class.le_cases 

584 
lemmas linorder_not_less = linorder_class.not_less 

585 
lemmas linorder_not_le = linorder_class.not_le 

586 
lemmas linorder_neq_iff = linorder_class.neq_iff 

587 
lemmas linorder_neqE = linorder_class.neqE 

588 
lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 

589 
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 

590 
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 

591 

592 

21083  593 
subsection {* Bounded quantifiers *} 
594 

595 
syntax 

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

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

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

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

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

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

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

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

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

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

606 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

617 
syntax (HOL) 

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

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

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

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

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

623 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

634 
translations 

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

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

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

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

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

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

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

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

643 

644 
print_translation {* 

645 
let 

22916  646 
val All_binder = Syntax.binder_name @{const_syntax All}; 
647 
val Ex_binder = Syntax.binder_name @{const_syntax Ex}; 

22377  648 
val impl = @{const_syntax "op >"}; 
649 
val conj = @{const_syntax "op &"}; 

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

652 

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

653 
val trans = 
21524  654 
[((All_binder, impl, less), ("_All_less", "_All_greater")), 
655 
((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), 

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

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

658 

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

659 
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

660 
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

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

662 
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

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

664 

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

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

666 
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

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

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

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

670 
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

671 
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

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

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

677 

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

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

679 

25193  680 
context ord 
681 
begin 

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

682 

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

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

685 

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

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

688 

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

691 

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

693 
by (rule ssubst) 

694 

695 
end 

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

696 

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

697 
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

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

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

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

701 
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

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

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

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

705 

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

706 
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

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

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

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

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

711 
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

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

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

714 

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

715 
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

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

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

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

719 
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

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

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

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

723 

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

724 
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

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

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

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

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

729 
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

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

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

732 

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

733 
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

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

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

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

737 
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

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

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

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

741 

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

742 
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

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

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

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

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

747 
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

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

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

750 

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

751 
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

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

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

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

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

756 
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

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

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

759 

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

760 
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

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

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

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

764 
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

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

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

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

768 

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

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

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

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

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

773 
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

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

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

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

777 

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

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

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

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

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

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

783 
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

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

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

786 

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

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

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

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

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

791 
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

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

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

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

795 

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

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

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

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

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

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

801 
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

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

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

804 

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

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

806 
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

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

808 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

839 

21083  840 

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

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

842 

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

845 

846 
lemma xt1: 

847 
"a = b ==> b > c ==> a > c" 

848 
"a > b ==> b = c ==> a > c" 

849 
"a = b ==> b >= c ==> a >= c" 

850 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  855 
"(a::'a::order) > b ==> b > a ==> P" 
21083  856 
"(x::'a::order) > y ==> y > z ==> x > z" 
857 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  863 
by auto 
21083  864 

865 
lemma xt2: 

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

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

868 

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

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

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

872 

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

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

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

876 

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

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

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

880 

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

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

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

884 

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

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

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

888 

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

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

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

892 

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

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

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

896 

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

898 

899 
(* 

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

901 
for the wrong thing in an Isar proof. 

902 

903 
The extra transitivity rules can be used as follows: 

904 

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

906 
proof  

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

908 
sorry 

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

910 
sorry 

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

912 
sorry 

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

914 
sorry 

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

916 
sorry 

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

918 
sorry 

919 
finally (xtrans) show ?thesis . 

920 
qed 

921 

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

923 
leave out the "(xtrans)" above. 

924 
*) 

925 

21546  926 
subsection {* Order on bool *} 
927 

26324  928 
instantiation bool :: order 
25510  929 
begin 
930 

931 
definition 

932 
le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q" 

933 

934 
definition 

935 
less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q" 

936 

937 
instance 

22916  938 
by intro_classes (auto simp add: le_bool_def less_bool_def) 
25510  939 

940 
end 

21546  941 

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

23212  943 
by (simp add: le_bool_def) 
21546  944 

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

23212  946 
by (simp add: le_bool_def) 
21546  947 

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

23212  949 
by (simp add: le_bool_def) 
21546  950 

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

23212  952 
by (simp add: le_bool_def) 
21546  953 

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

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

957 
"False < b \<longleftrightarrow> b" 

958 
"True < b \<longleftrightarrow> False" 

959 
unfolding le_bool_def less_bool_def by simp_all 

960 

22424  961 

23881  962 
subsection {* Order on sets *} 
963 

964 
instance set :: (type) order 

965 
by (intro_classes, 

966 
(assumption  rule subset_refl subset_trans subset_antisym psubset_eq)+) 

967 

968 
lemmas basic_trans_rules [trans] = 

969 
order_trans_rules set_rev_mp set_mp 

970 

971 

972 
subsection {* Order on functions *} 

973 

25510  974 
instantiation "fun" :: (type, ord) ord 
975 
begin 

976 

977 
definition 

978 
le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)" 

23881  979 

25510  980 
definition 
981 
less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g" 

982 

983 
instance .. 

984 

985 
end 

23881  986 

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

988 
by default 

989 
(auto simp add: le_fun_def less_fun_def expand_fun_eq 

990 
intro: order_trans order_antisym) 

991 

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

993 
unfolding le_fun_def by simp 

994 

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

996 
unfolding le_fun_def by simp 

997 

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

999 
unfolding le_fun_def by simp 

1000 

1001 
text {* 

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

1003 
on unary and binary predicates 

1004 
*} 

1005 

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

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

1008 
shows "P \<le> Q" 

1009 
apply (rule le_funI) 

1010 
apply (rule le_boolI) 

1011 
apply (rule PQ) 

1012 
apply assumption 

1013 
done 

1014 

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

1016 
apply (erule le_funE) 

1017 
apply (erule le_boolE) 

1018 
apply assumption+ 

1019 
done 

1020 

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

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

1023 
shows "P \<le> Q" 

1024 
apply (rule le_funI)+ 

1025 
apply (rule le_boolI) 

1026 
apply (rule PQ) 

1027 
apply assumption 

1028 
done 

1029 

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

1031 
apply (erule le_funE)+ 

1032 
apply (erule le_boolE) 

1033 
apply assumption+ 

1034 
done 

1035 

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

1037 
by (rule predicate1D) 

1038 

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

1040 
by (rule predicate2D) 

1041 

1042 

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

21083  1044 

25076  1045 
context order 
1046 
begin 

1047 

1048 
definition 

1049 
mono :: "('a \<Rightarrow> 'b\<Colon>order) \<Rightarrow> bool" 

1050 
where 

1051 
"mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)" 

1052 

1053 
lemma monoI [intro?]: 

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

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

1056 
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

1057 

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

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

1061 
unfolding mono_def by iprover 

1062 

1063 
end 

1064 

1065 
context linorder 

1066 
begin 

1067 

1068 
lemma min_of_mono: 

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

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

1073 
lemma max_of_mono: 

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

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

1078 
end 

21083  1079 

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

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

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

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

1083 
!!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

1084 
==> Q (Least P)" 
23212  1085 
apply (unfold Least_def) 
1086 
apply (rule theI2) 

1087 
apply (blast intro: order_antisym)+ 

1088 
done 

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

1089 

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

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

1093 
 {* Courtesy of Stephan Merz *} 

1094 
apply clarify 

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

1096 
apply (rule LeastI2_order) 

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

1098 
done 

1099 

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

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

1103 
apply (rule the_equality) 

1104 
apply (auto intro!: order_antisym) 

1105 
done 

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

1106 

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

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

1109 

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

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

1112 

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

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

1116 
done 

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

1117 

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

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

1121 
done 

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

1122 

15524  1123 
end 