author  haftmann 
Thu, 13 Dec 2007 07:09:02 +0100  
changeset 25614  0b8baa94b866 
parent 25510  38c15efe603b 
child 26014  00c2c3525bef 
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 

25062  42 
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y" 
23212  43 
by (erule contrapos_pn, erule subst, rule less_irrefl) 
21329  44 

45 

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

47 

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

25062  51 
lemma less_imp_not_eq2: "x < y \<Longrightarrow> (y = x) \<longleftrightarrow> False" 
23212  52 
by auto 
21329  53 

54 

55 
text {* Transitivity rules for calculational reasoning *} 

56 

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

25062  60 
lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b" 
23212  61 
by (simp add: less_le) 
21329  62 

15524  63 

64 
text {* Asymmetry. *} 

65 

25062  66 
lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)" 
23212  67 
by (simp add: less_le antisym) 
15524  68 

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

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

25062  75 
lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y" 
23212  76 
by (blast intro: antisym) 
15524  77 

25062  78 
lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y" 
23212  79 
by (erule contrapos_pn, erule subst, rule less_irrefl) 
21248  80 

21083  81 

15524  82 
text {* Transitivity. *} 
83 

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

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

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

93 

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

95 

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

25062  99 
lemma less_imp_triv: "x < y \<Longrightarrow> (y < x \<longrightarrow> P) \<longleftrightarrow> True" 
23212  100 
by (blast elim: less_asym) 
15524  101 

21248  102 

21083  103 
text {* Transitivity rules for calculational reasoning *} 
15524  104 

25062  105 
lemma less_asym': "a < b \<Longrightarrow> b < a \<Longrightarrow> P" 
23212  106 
by (rule less_asym) 
21248  107 

22916  108 

109 
text {* Reverse order *} 

110 

111 
lemma order_reverse: 

25103  112 
"order (op \<ge>) (op >)" 
23212  113 
by unfold_locales 
114 
(simp add: less_le, auto intro: antisym order_trans) 

22916  115 

21248  116 
end 
15524  117 

21329  118 

119 
subsection {* Linear (total) orders *} 

120 

22316  121 
class linorder = order + 
25207  122 
assumes linear: "x \<le> y \<or> y \<le> x" 
21248  123 
begin 
124 

25062  125 
lemma less_linear: "x < y \<or> x = y \<or> y < x" 
23212  126 
unfolding less_le using less_le linear by blast 
21248  127 

25062  128 
lemma le_less_linear: "x \<le> y \<or> y < x" 
23212  129 
by (simp add: le_less less_linear) 
21248  130 

131 
lemma le_cases [case_names le ge]: 

25062  132 
"(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P" 
23212  133 
using linear by blast 
21248  134 

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

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

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

142 
done 

143 

144 
lemma not_less_iff_gr_or_eq: 

25062  145 
"\<not>(x < y) \<longleftrightarrow> (x > y  x = y)" 
23212  146 
apply(simp add:not_less le_less) 
147 
apply blast 

148 
done 

15524  149 

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

153 
done 

15524  154 

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

25062  158 
lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R" 
23212  159 
by (simp add: neq_iff) blast 
15524  160 

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

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

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

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

25062  174 
lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y" 
23212  175 
unfolding not_less . 
16796  176 

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

25062  178 
lemma not_leE: "\<not> y \<le> x \<Longrightarrow> x < y" 
23212  179 
unfolding not_le . 
21248  180 

22916  181 

182 
text {* Reverse order *} 

183 

184 
lemma linorder_reverse: 

25103  185 
"linorder (op \<ge>) (op >)" 
23212  186 
by unfold_locales 
187 
(simp add: less_le, auto intro: antisym order_trans simp add: linear) 

22916  188 

189 

23881  190 
text {* min/max *} 
191 

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

193 

194 
definition (in ord) 

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

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

198 
definition (in ord) 

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

25062  200 
[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

201 

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

202 
lemma min_le_iff_disj: 
25062  203 
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z" 
23212  204 
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

205 

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

206 
lemma le_max_iff_disj: 
25062  207 
"z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y" 
23212  208 
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

209 

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

210 
lemma min_less_iff_disj: 
25062  211 
"min x y < z \<longleftrightarrow> x < z \<or> y < z" 
23212  212 
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

213 

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

214 
lemma less_max_iff_disj: 
25062  215 
"z < max x y \<longleftrightarrow> z < x \<or> z < y" 
23212  216 
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

217 

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

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

221 

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

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

225 

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

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

229 

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

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

233 

21248  234 
end 
235 

23948  236 

21083  237 
subsection {* Reasoning tools setup *} 
238 

21091  239 
ML {* 
240 

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

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

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

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

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

245 
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

246 
end; 
21091  247 

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

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

250 

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

251 
(** Theory and context data **) 
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 
fun struct_eq ((s1: string, ts1), (s2, ts2)) = 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

255 

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

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

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

258 
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

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

260 
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

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

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

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

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

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

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

267 

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

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

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

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

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

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

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

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

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

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

279 
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

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

281 

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

282 

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

283 
(** Method **) 
21091  284 

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

285 
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

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

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

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

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

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

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

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

293 
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

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

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

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

297 
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

298 
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

299 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

313 

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

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

315 
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

316 

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

317 

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

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

319 

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

320 
fun add_struct_thm s tag = 
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 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

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

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

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

326 

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

327 
val attribute = Attrib.syntax 
448edc627ee4
Transitivity reasoner set up for locales order and linorder.
ballarin
parents:
24422
diff
changeset

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

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

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

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

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

333 
 ((NONE, n), ts) => del_struct (n, ts))); 
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 

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

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

337 

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

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

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

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

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

342 

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

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

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

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

347 

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

348 

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

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

350 

24867  351 
val setup = 
352 
Method.add_methods 

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

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

21091  355 

356 
end; 

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

357 

21091  358 
*} 
359 

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

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

361 

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

362 

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

363 
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

364 

25076  365 
context order 
366 
begin 

367 

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

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

369 
is not a parameter of the locale. *) 
25076  370 

371 
lemmas 

372 
[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

373 
less_irrefl [THEN notE] 
25076  374 
lemmas 
25062  375 
[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

376 
order_refl 
25076  377 
lemmas 
25062  378 
[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

379 
less_imp_le 
25076  380 
lemmas 
25062  381 
[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

382 
antisym 
25076  383 
lemmas 
25062  384 
[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

385 
eq_refl 
25076  386 
lemmas 
25062  387 
[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

388 
sym [THEN eq_refl] 
25076  389 
lemmas 
25062  390 
[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

391 
less_trans 
25076  392 
lemmas 
25062  393 
[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

394 
less_le_trans 
25076  395 
lemmas 
25062  396 
[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

397 
le_less_trans 
25076  398 
lemmas 
25062  399 
[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

400 
order_trans 
25076  401 
lemmas 
25062  402 
[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

403 
le_neq_trans 
25076  404 
lemmas 
25062  405 
[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

406 
neq_le_trans 
25076  407 
lemmas 
25062  408 
[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

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

412 
eq_neq_eq_imp_neq 
25076  413 
lemmas 
25062  414 
[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

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

416 

25076  417 
end 
418 

419 
context linorder 

420 
begin 

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

421 

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

424 

425 
lemmas 

25062  426 
[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

427 
less_irrefl [THEN notE] 
25076  428 
lemmas 
25062  429 
[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

430 
order_refl 
25076  431 
lemmas 
25062  432 
[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

433 
less_imp_le 
25076  434 
lemmas 
25062  435 
[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

436 
not_less [THEN iffD2] 
25076  437 
lemmas 
25062  438 
[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

439 
not_le [THEN iffD2] 
25076  440 
lemmas 
25062  441 
[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

442 
not_less [THEN iffD1] 
25076  443 
lemmas 
25062  444 
[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

445 
not_le [THEN iffD1] 
25076  446 
lemmas 
25062  447 
[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

448 
antisym 
25076  449 
lemmas 
25062  450 
[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

451 
eq_refl 
25076  452 
lemmas 
25062  453 
[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

454 
sym [THEN eq_refl] 
25076  455 
lemmas 
25062  456 
[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

457 
less_trans 
25076  458 
lemmas 
25062  459 
[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

460 
less_le_trans 
25076  461 
lemmas 
25062  462 
[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

463 
le_less_trans 
25076  464 
lemmas 
25062  465 
[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

466 
order_trans 
25076  467 
lemmas 
25062  468 
[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

469 
le_neq_trans 
25076  470 
lemmas 
25062  471 
[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

472 
neq_le_trans 
25076  473 
lemmas 
25062  474 
[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

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

478 
eq_neq_eq_imp_neq 
25076  479 
lemmas 
25062  480 
[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

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

482 

25076  483 
end 
484 

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

485 

21083  486 
setup {* 
487 
let 

488 

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

15524  490 

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

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

496 
NONE => 

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

498 
in case find_first (prp t) prems of 

499 
NONE => NONE 

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

15524  505 

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

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

511 
NONE => 

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

513 
in case find_first (prp t) prems of 

514 
NONE => NONE 

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

15524  520 

21248  521 
fun add_simprocs procs thy = 
522 
(Simplifier.change_simpset_of thy (fn ss => ss 

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

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

525 
fun add_solver name tac thy = 

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

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

529 
in 

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

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

533 
] 

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

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

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

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

21083  539 
end 
540 
*} 

15524  541 

542 

24422  543 
subsection {* Dense orders *} 
544 

545 
class dense_linear_order = linorder + 

25076  546 
assumes gt_ex: "\<exists>y. x < y" 
547 
and lt_ex: "\<exists>y. y < x" 

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

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

551 

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

25076  556 
end 
557 

24422  558 
subsection {* Name duplicates *} 
559 

560 
lemmas order_less_le = less_le 

561 
lemmas order_eq_refl = order_class.eq_refl 

562 
lemmas order_less_irrefl = order_class.less_irrefl 

563 
lemmas order_le_less = order_class.le_less 

564 
lemmas order_le_imp_less_or_eq = order_class.le_imp_less_or_eq 

565 
lemmas order_less_imp_le = order_class.less_imp_le 

566 
lemmas order_less_imp_not_eq = order_class.less_imp_not_eq 

567 
lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2 

568 
lemmas order_neq_le_trans = order_class.neq_le_trans 

569 
lemmas order_le_neq_trans = order_class.le_neq_trans 

570 

571 
lemmas order_antisym = antisym 

572 
lemmas order_less_not_sym = order_class.less_not_sym 

573 
lemmas order_less_asym = order_class.less_asym 

574 
lemmas order_eq_iff = order_class.eq_iff 

575 
lemmas order_antisym_conv = order_class.antisym_conv 

576 
lemmas order_less_trans = order_class.less_trans 

577 
lemmas order_le_less_trans = order_class.le_less_trans 

578 
lemmas order_less_le_trans = order_class.less_le_trans 

579 
lemmas order_less_imp_not_less = order_class.less_imp_not_less 

580 
lemmas order_less_imp_triv = order_class.less_imp_triv 

581 
lemmas order_less_asym' = order_class.less_asym' 

582 

583 
lemmas linorder_linear = linear 

584 
lemmas linorder_less_linear = linorder_class.less_linear 

585 
lemmas linorder_le_less_linear = linorder_class.le_less_linear 

586 
lemmas linorder_le_cases = linorder_class.le_cases 

587 
lemmas linorder_not_less = linorder_class.not_less 

588 
lemmas linorder_not_le = linorder_class.not_le 

589 
lemmas linorder_neq_iff = linorder_class.neq_iff 

590 
lemmas linorder_neqE = linorder_class.neqE 

591 
lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1 

592 
lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2 

593 
lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3 

594 

595 

21083  596 
subsection {* Bounded quantifiers *} 
597 

598 
syntax 

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

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

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

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

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

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

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

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

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

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

609 
syntax (xsymbols) 

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

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

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

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

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

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

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

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

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

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

620 
syntax (HOL) 

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

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

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

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

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

626 
syntax (HTML output) 

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

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

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

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

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

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

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

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

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

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

637 
translations 

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

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

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

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

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

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

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

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

646 

647 
print_translation {* 

648 
let 

22916  649 
val All_binder = Syntax.binder_name @{const_syntax All}; 
650 
val Ex_binder = Syntax.binder_name @{const_syntax Ex}; 

22377  651 
val impl = @{const_syntax "op >"}; 
652 
val conj = @{const_syntax "op &"}; 

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

655 

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

656 
val trans = 
21524  657 
[((All_binder, impl, less), ("_All_less", "_All_greater")), 
658 
((All_binder, impl, less_eq), ("_All_less_eq", "_All_greater_eq")), 

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

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

661 

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

662 
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

663 
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

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

665 
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

666 
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

667 

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

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

669 
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

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

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

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

673 
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

674 
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

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

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

680 

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

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

682 

25193  683 
context ord 
684 
begin 

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

685 

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

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

688 

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

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

691 

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

694 

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

696 
by (rule ssubst) 

697 

698 
end 

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

699 

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

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

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

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

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

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

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

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

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

708 

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

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

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

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

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

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

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

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

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

717 

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

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

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

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

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

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

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

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

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

726 

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

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

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

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

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

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

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

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

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

735 

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

736 
lemma order_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

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

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

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

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

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

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

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

744 

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

745 
lemma order_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

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

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

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

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

750 
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

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

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

753 

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

754 
lemma 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

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

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

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

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

759 
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

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

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

762 

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

763 
lemma 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

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

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

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

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

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

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

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

771 

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

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

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

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

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

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

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

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

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

780 

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

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

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

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

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

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

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

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

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

789 

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

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

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

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

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

794 
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

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

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

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

798 

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

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

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

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

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

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

804 
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

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

806 
qed 
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 
text {* 
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

809 
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

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

811 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

842 

21083  843 

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

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

845 

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

848 

849 
lemma xt1: 

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

851 
"a > b ==> b = c ==> a > c" 

852 
"a = b ==> b >= c ==> a >= c" 

853 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

23417  858 
"(a::'a::order) > b ==> b > a ==> P" 
21083  859 
"(x::'a::order) > y ==> y > z ==> x > z" 
860 
"(a::'a::order) >= b ==> a ~= b ==> a > b" 

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

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

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

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

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

25076  866 
by auto 
21083  867 

868 
lemma xt2: 

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

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

871 

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

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

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

875 

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

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

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

879 

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

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

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

883 

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

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

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

887 

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

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

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

891 

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

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

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

895 

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

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

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

899 

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

901 

902 
(* 

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

904 
for the wrong thing in an Isar proof. 

905 

906 
The extra transitivity rules can be used as follows: 

907 

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

909 
proof  

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

911 
sorry 

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

913 
sorry 

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

915 
sorry 

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

917 
sorry 

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

919 
sorry 

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

921 
sorry 

922 
finally (xtrans) show ?thesis . 

923 
qed 

924 

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

926 
leave out the "(xtrans)" above. 

927 
*) 

928 

21546  929 
subsection {* Order on bool *} 
930 

25510  931 
instantiation bool :: order 
932 
begin 

933 

934 
definition 

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

936 

937 
definition 

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

939 

940 
instance 

22916  941 
by intro_classes (auto simp add: le_bool_def less_bool_def) 
25510  942 

943 
end 

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_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q" 

23212  949 
by (simp add: le_bool_def) 
21546  950 

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

23212  952 
by (simp add: le_bool_def) 
21546  953 

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

23212  955 
by (simp add: le_bool_def) 
21546  956 

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

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

960 
"False < b \<longleftrightarrow> b" 

961 
"True < b \<longleftrightarrow> False" 

962 
unfolding le_bool_def less_bool_def by simp_all 

963 

22424  964 

23881  965 
subsection {* Order on sets *} 
966 

967 
instance set :: (type) order 

968 
by (intro_classes, 

969 
(assumption  rule subset_refl subset_trans subset_antisym psubset_eq)+) 

970 

971 
lemmas basic_trans_rules [trans] = 

972 
order_trans_rules set_rev_mp set_mp 

973 

974 

975 
subsection {* Order on functions *} 

976 

25510  977 
instantiation "fun" :: (type, ord) ord 
978 
begin 

979 

980 
definition 

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

23881  982 

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

985 

986 
instance .. 

987 

988 
end 

23881  989 

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

991 
by default 

992 
(auto simp add: le_fun_def less_fun_def expand_fun_eq 

993 
intro: order_trans order_antisym) 

994 

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

996 
unfolding le_fun_def by simp 

997 

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

999 
unfolding le_fun_def by simp 

1000 

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

1002 
unfolding le_fun_def by simp 

1003 

1004 
text {* 

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

1006 
on unary and binary predicates 

1007 
*} 

1008 

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

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

1011 
shows "P \<le> Q" 

1012 
apply (rule le_funI) 

1013 
apply (rule le_boolI) 

1014 
apply (rule PQ) 

1015 
apply assumption 

1016 
done 

1017 

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

1019 
apply (erule le_funE) 

1020 
apply (erule le_boolE) 

1021 
apply assumption+ 

1022 
done 

1023 

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

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

1026 
shows "P \<le> Q" 

1027 
apply (rule le_funI)+ 

1028 
apply (rule le_boolI) 

1029 
apply (rule PQ) 

1030 
apply assumption 

1031 
done 

1032 

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

1034 
apply (erule le_funE)+ 

1035 
apply (erule le_boolE) 

1036 
apply assumption+ 

1037 
done 

1038 

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

1040 
by (rule predicate1D) 

1041 

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

1043 
by (rule predicate2D) 

1044 

1045 

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

21083  1047 

25076  1048 
context order 
1049 
begin 

1050 

1051 
definition 

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

1053 
where 

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

1055 

1056 
lemma monoI [intro?]: 

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

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

1059 
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

1060 

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

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

1064 
unfolding mono_def by iprover 

1065 

1066 
end 

1067 

1068 
context linorder 

1069 
begin 

1070 

1071 
lemma min_of_mono: 

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

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

1076 
lemma max_of_mono: 

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

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

1081 
end 

21083  1082 

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

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

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

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

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

1087 
==> Q (Least P)" 
23212  1088 
apply (unfold Least_def) 
1089 
apply (rule theI2) 

1090 
apply (blast intro: order_antisym)+ 

1091 
done 

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

1092 

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

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

1096 
 {* Courtesy of Stephan Merz *} 

1097 
apply clarify 

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

1099 
apply (rule LeastI2_order) 

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

1101 
done 

1102 

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

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

1106 
apply (rule the_equality) 

1107 
apply (auto intro!: order_antisym) 

1108 
done 

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 min_leastL: "(!!x. least <= x) ==> min least x = least" 
23212  1111 
by (simp add: min_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 max_leastL: "(!!x. least <= x) ==> max least x = x" 
23212  1114 
by (simp add: max_def) 
21383
17e6275e13f5
added transitivity rules, reworking of min/max lemmas
haftmann
parents:
21329
diff
changeset

1115 

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

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

1119 
done 

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

1120 

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

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

1124 
done 

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

1125 

15524  1126 
end 