author  haftmann 
Fri, 20 Oct 2006 18:20:22 +0200  
changeset 21083  a1de02f047d0 
parent 21044  9690be52ee5d 
child 21091  5061e3e56484 
permissions  rwrr 
15524  1 
(* Title: HOL/Orderings.thy 
2 
ID: $Id$ 

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

4 
*) 

5 

21083  6 
header {* Abstract orderings *} 
15524  7 

8 
theory Orderings 

21044
9690be52ee5d
fixed print translations for bounded quantification
haftmann
parents:
20714
diff
changeset

9 
imports Code_Generator Lattice_Locales 
15524  10 
begin 
11 

21083  12 
section {* Abstract orderings *} 
13 

14 
subsection {* Order signatures *} 

15524  15 

20588  16 
class ord = eq + 
20714  17 
constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (*FIXME: class_package should do the job*) 
20588  18 
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
19 
fixes less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

15524  20 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

21 
const_syntax 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

22 
less ("op <") 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

23 
less ("(_/ < _)" [50, 51] 50) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

24 
less_eq ("op <=") 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

25 
less_eq ("(_/ <= _)" [50, 51] 50) 
15524  26 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

27 
const_syntax (xsymbols) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

28 
less_eq ("op \<le>") 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

29 
less_eq ("(_/ \<le> _)" [50, 51] 50) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

30 

09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

31 
const_syntax (HTML output) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

32 
less_eq ("op \<le>") 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

33 
less_eq ("(_/ \<le> _)" [50, 51] 50) 
15524  34 

20714  35 

36 
abbreviation (in ord) 

37 
"less_eq_syn \<equiv> less_eq" 

38 
"less_syn \<equiv> less" 

39 

40 
const_syntax (in ord) 

41 
less_eq_syn ("op \<^loc><=") 

42 
less_eq_syn ("(_/ \<^loc><= _)" [50, 51] 50) 

43 
less_syn ("op \<^loc><") 

44 
less_syn ("(_/ \<^loc>< _)" [50, 51] 50) 

45 

46 
const_syntax (in ord) (xsymbols) 

47 
less_eq_syn ("op \<^loc>\<le>") 

48 
less_eq_syn ("(_/ \<^loc>\<le> _)" [50, 51] 50) 

49 

50 
const_syntax (in ord) (HTML output) 

51 
less_eq_syn ("op \<^loc>\<le>") 

52 
less_eq_syn ("(_/ \<^loc>\<le> _)" [50, 51] 50) 

53 

54 

19536  55 
abbreviation (input) 
56 
greater (infixl ">" 50) 

20714  57 
"x > y \<equiv> y < x" 
19536  58 
greater_eq (infixl ">=" 50) 
20714  59 
"x >= y \<equiv> y <= x" 
60 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

61 
const_syntax (xsymbols) 
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19637
diff
changeset

62 
greater_eq (infixl "\<ge>" 50) 
15524  63 

20714  64 
abbreviation (in ord) (input) 
65 
greater (infix "\<^loc>>" 50) 

66 
"x \<^loc>> y \<equiv> y \<^loc>< x" 

67 
greater_eq (infix "\<^loc>>=" 50) 

68 
"x \<^loc>>= y \<equiv> y \<^loc><= x" 

69 

70 
const_syntax (in ord) (xsymbols) 

71 
greater_eq (infixl "\<^loc>\<ge>" 50) 

72 

15524  73 

21083  74 
subsection {* Partial orderings *} 
15524  75 

76 
axclass order < ord 

77 
order_refl [iff]: "x <= x" 

78 
order_trans: "x <= y ==> y <= z ==> x <= z" 

79 
order_antisym: "x <= y ==> y <= x ==> x = y" 

80 
order_less_le: "(x < y) = (x <= y & x ~= y)" 

81 

21083  82 
text {* Connection to locale: *} 
15524  83 

15837  84 
interpretation order: 
15780  85 
partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"] 
15524  86 
apply(rule partial_order.intro) 
87 
apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym) 

88 
done 

89 

90 
text {* Reflexivity. *} 

91 

92 
lemma order_eq_refl: "!!x::'a::order. x = y ==> x <= y" 

93 
 {* This form is useful with the classical reasoner. *} 

94 
apply (erule ssubst) 

95 
apply (rule order_refl) 

96 
done 

97 

98 
lemma order_less_irrefl [iff]: "~ x < (x::'a::order)" 

99 
by (simp add: order_less_le) 

100 

101 
lemma order_le_less: "((x::'a::order) <= y) = (x < y  x = y)" 

102 
 {* NOT suitable for iff, since it can cause PROOF FAILED. *} 

103 
apply (simp add: order_less_le, blast) 

104 
done 

105 

106 
lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard] 

107 

108 
lemma order_less_imp_le: "!!x::'a::order. x < y ==> x <= y" 

109 
by (simp add: order_less_le) 

110 

111 
text {* Asymmetry. *} 

112 

113 
lemma order_less_not_sym: "(x::'a::order) < y ==> ~ (y < x)" 

114 
by (simp add: order_less_le order_antisym) 

115 

116 
lemma order_less_asym: "x < (y::'a::order) ==> (~P ==> y < x) ==> P" 

117 
apply (drule order_less_not_sym) 

118 
apply (erule contrapos_np, simp) 

119 
done 

120 

121 
lemma order_eq_iff: "!!x::'a::order. (x = y) = (x \<le> y & y \<le> x)" 

122 
by (blast intro: order_antisym) 

123 

124 
lemma order_antisym_conv: "(y::'a::order) <= x ==> (x <= y) = (x = y)" 

125 
by(blast intro:order_antisym) 

126 

21083  127 
lemma less_imp_neq: "[ (x::'a::order) < y ] ==> x ~= y" 
128 
by (erule contrapos_pn, erule subst, rule order_less_irrefl) 

129 

15524  130 
text {* Transitivity. *} 
131 

132 
lemma order_less_trans: "!!x::'a::order. [ x < y; y < z ] ==> x < z" 

133 
apply (simp add: order_less_le) 

134 
apply (blast intro: order_trans order_antisym) 

135 
done 

136 

137 
lemma order_le_less_trans: "!!x::'a::order. [ x <= y; y < z ] ==> x < z" 

138 
apply (simp add: order_less_le) 

139 
apply (blast intro: order_trans order_antisym) 

140 
done 

141 

142 
lemma order_less_le_trans: "!!x::'a::order. [ x < y; y <= z ] ==> x < z" 

143 
apply (simp add: order_less_le) 

144 
apply (blast intro: order_trans order_antisym) 

145 
done 

146 

21083  147 
lemma eq_neq_eq_imp_neq: "[ x = a ; a ~= b; b = y ] ==> x ~= y" 
148 
by (erule subst, erule ssubst, assumption) 

15524  149 

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

151 

152 
lemma order_less_imp_not_less: "(x::'a::order) < y ==> (~ y < x) = True" 

153 
by (blast elim: order_less_asym) 

154 

155 
lemma order_less_imp_triv: "(x::'a::order) < y ==> (y < x > P) = True" 

156 
by (blast elim: order_less_asym) 

157 

158 
lemma order_less_imp_not_eq: "(x::'a::order) < y ==> (x = y) = False" 

159 
by auto 

160 

161 
lemma order_less_imp_not_eq2: "(x::'a::order) < y ==> (y = x) = False" 

162 
by auto 

163 

21083  164 
text {* Transitivity rules for calculational reasoning *} 
15524  165 

166 
lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b" 

167 
by (simp add: order_less_le) 

168 

169 
lemma order_le_neq_trans: "(a::'a::order) <= b ==> a ~= b ==> a < b" 

170 
by (simp add: order_less_le) 

171 

172 
lemma order_less_asym': "(a::'a::order) < b ==> b < a ==> P" 

173 
by (rule order_less_asym) 

174 

175 

21083  176 
subsection {* Total orderings *} 
15524  177 

178 
axclass linorder < order 

179 
linorder_linear: "x <= y  y <= x" 

180 

181 
lemma linorder_less_linear: "!!x::'a::linorder. x<y  x=y  y<x" 

182 
apply (simp add: order_less_le) 

183 
apply (insert linorder_linear, blast) 

184 
done 

185 

186 
lemma linorder_le_less_linear: "!!x::'a::linorder. x\<le>y  y<x" 

187 
by (simp add: order_le_less linorder_less_linear) 

188 

189 
lemma linorder_le_cases [case_names le ge]: 

190 
"((x::'a::linorder) \<le> y ==> P) ==> (y \<le> x ==> P) ==> P" 

191 
by (insert linorder_linear, blast) 

192 

193 
lemma linorder_cases [case_names less equal greater]: 

194 
"((x::'a::linorder) < y ==> P) ==> (x = y ==> P) ==> (y < x ==> P) ==> P" 

195 
by (insert linorder_less_linear, blast) 

196 

197 
lemma linorder_not_less: "!!x::'a::linorder. (~ x < y) = (y <= x)" 

198 
apply (simp add: order_less_le) 

199 
apply (insert linorder_linear) 

200 
apply (blast intro: order_antisym) 

201 
done 

202 

203 
lemma linorder_not_le: "!!x::'a::linorder. (~ x <= y) = (y < x)" 

204 
apply (simp add: order_less_le) 

205 
apply (insert linorder_linear) 

206 
apply (blast intro: order_antisym) 

207 
done 

208 

209 
lemma linorder_neq_iff: "!!x::'a::linorder. (x ~= y) = (x<y  y<x)" 

210 
by (cut_tac x = x and y = y in linorder_less_linear, auto) 

211 

212 
lemma linorder_neqE: "x ~= (y::'a::linorder) ==> (x < y ==> R) ==> (y < x ==> R) ==> R" 

213 
by (simp add: linorder_neq_iff, blast) 

214 

215 
lemma linorder_antisym_conv1: "~ (x::'a::linorder) < y ==> (x <= y) = (x = y)" 

216 
by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1]) 

217 

218 
lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)" 

219 
by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1]) 

220 

221 
lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)" 

222 
by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1]) 

223 

16796  224 
text{*Replacing the old Nat.leI*} 
225 
lemma leI: "~ x < y ==> y <= (x::'a::linorder)" 

226 
by (simp only: linorder_not_less) 

227 

228 
lemma leD: "y <= (x::'a::linorder) ==> ~ x < y" 

229 
by (simp only: linorder_not_less) 

230 

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

232 
lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y" 

233 
by (simp only: linorder_not_le) 

234 

21083  235 

236 
subsection {* Reasoning tools setup *} 

237 

238 
setup {* 

239 
let 

240 

241 
val order_antisym_conv = thm "order_antisym_conv" 

242 
val linorder_antisym_conv1 = thm "linorder_antisym_conv1" 

243 
val linorder_antisym_conv2 = thm "linorder_antisym_conv2" 

244 
val linorder_antisym_conv3 = thm "linorder_antisym_conv3" 

245 

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

15524  247 

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

250 
val less = Const("Orderings.less",T); 

251 
val t = HOLogic.mk_Trueprop(le $ s $ r); 

252 
in case find_first (prp t) prems of 

253 
NONE => 

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

255 
in case find_first (prp t) prems of 

256 
NONE => NONE 

257 
 SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1)) 

258 
end 

259 
 SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv)) 

260 
end 

261 
handle THM _ => NONE; 

15524  262 

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

265 
val le = Const("Orderings.less_eq",T); 

266 
val t = HOLogic.mk_Trueprop(le $ r $ s); 

267 
in case find_first (prp t) prems of 

268 
NONE => 

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

270 
in case find_first (prp t) prems of 

271 
NONE => NONE 

272 
 SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3)) 

273 
end 

274 
 SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2)) 

275 
end 

276 
handle THM _ => NONE; 

15524  277 

21083  278 
val antisym_le = Simplifier.simproc (the_context()) 
279 
"antisym le" ["(x::'a::order) <= y"] prove_antisym_le; 

280 
val antisym_less = Simplifier.simproc (the_context()) 

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

282 

283 
in 

284 

285 
(fn thy => (Simplifier.change_simpset_of thy 

286 
(fn ss => ss addsimprocs [antisym_le, antisym_less]); thy)) 

287 

288 
end 

289 
*} 

15524  290 

291 
ML_setup {* 

292 

293 
(* The setting up of Quasi_Tac serves as a demo. Since there is no 

294 
class for quasi orders, the tactics Quasi_Tac.trans_tac and 

295 
Quasi_Tac.quasi_tac are not of much use. *) 

296 

21044
9690be52ee5d
fixed print translations for bounded quantification
haftmann
parents:
20714
diff
changeset

297 
fun decomp_gen sort thy (Trueprop $ t) = 
15622
4723248c982b
Transitivity reasoner ignores types amenable to linear arithmetic.
ballarin
parents:
15531
diff
changeset

298 
let fun of_sort t = let val T = type_of t in 
4723248c982b
Transitivity reasoner ignores types amenable to linear arithmetic.
ballarin
parents:
15531
diff
changeset

299 
(* exclude numeric types: linear arithmetic subsumes transitivity *) 
4723248c982b
Transitivity reasoner ignores types amenable to linear arithmetic.
ballarin
parents:
15531
diff
changeset

300 
T <> HOLogic.natT andalso T <> HOLogic.intT andalso 
21044
9690be52ee5d
fixed print translations for bounded quantification
haftmann
parents:
20714
diff
changeset

301 
T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end 
15524  302 
fun dec (Const ("Not", _) $ t) = ( 
303 
case dec t of 

15531  304 
NONE => NONE 
305 
 SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) 

15524  306 
 dec (Const ("op =", _) $ t1 $ t2) = 
307 
if of_sort t1 

15531  308 
then SOME (t1, "=", t2) 
309 
else NONE 

19277  310 
 dec (Const ("Orderings.less_eq", _) $ t1 $ t2) = 
15524  311 
if of_sort t1 
15531  312 
then SOME (t1, "<=", t2) 
313 
else NONE 

19277  314 
 dec (Const ("Orderings.less", _) $ t1 $ t2) = 
15524  315 
if of_sort t1 
15531  316 
then SOME (t1, "<", t2) 
317 
else NONE 

318 
 dec _ = NONE 

15524  319 
in dec t end; 
320 

321 
structure Quasi_Tac = Quasi_Tac_Fun ( 

322 
struct 

323 
val le_trans = thm "order_trans"; 

324 
val le_refl = thm "order_refl"; 

325 
val eqD1 = thm "order_eq_refl"; 

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

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

328 
val less_imp_le = thm "order_less_imp_le"; 

329 
val le_neq_trans = thm "order_le_neq_trans"; 

330 
val neq_le_trans = thm "order_neq_le_trans"; 

331 
val less_imp_neq = thm "less_imp_neq"; 

332 
val decomp_trans = decomp_gen ["Orderings.order"]; 

333 
val decomp_quasi = decomp_gen ["Orderings.order"]; 

334 

335 
end); (* struct *) 

336 

337 
structure Order_Tac = Order_Tac_Fun ( 

338 
struct 

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

340 
val le_refl = thm "order_refl"; 

341 
val less_imp_le = thm "order_less_imp_le"; 

342 
val not_lessI = thm "linorder_not_less" RS thm "iffD2"; 

343 
val not_leI = thm "linorder_not_le" RS thm "iffD2"; 

344 
val not_lessD = thm "linorder_not_less" RS thm "iffD1"; 

345 
val not_leD = thm "linorder_not_le" RS thm "iffD1"; 

346 
val eqI = thm "order_antisym"; 

347 
val eqD1 = thm "order_eq_refl"; 

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

349 
val less_trans = thm "order_less_trans"; 

350 
val less_le_trans = thm "order_less_le_trans"; 

351 
val le_less_trans = thm "order_le_less_trans"; 

352 
val le_trans = thm "order_trans"; 

353 
val le_neq_trans = thm "order_le_neq_trans"; 

354 
val neq_le_trans = thm "order_neq_le_trans"; 

355 
val less_imp_neq = thm "less_imp_neq"; 

356 
val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; 

16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16417
diff
changeset

357 
val not_sym = thm "not_sym"; 
15524  358 
val decomp_part = decomp_gen ["Orderings.order"]; 
359 
val decomp_lin = decomp_gen ["Orderings.linorder"]; 

360 

361 
end); (* struct *) 

362 

17876  363 
change_simpset (fn ss => ss 
15524  364 
addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac)) 
17876  365 
addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac))); 
15524  366 
(* Adding the transitivity reasoners also as safe solvers showed a slight 
367 
speed up, but the reasoning strength appears to be not higher (at least 

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

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

370 
*} 

371 

372 
(* Optional setup of methods *) 

373 

374 
(* 

375 
method_setup trans_partial = 

376 
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.partial_tac)) *} 

377 
{* transitivity reasoner for partial orders *} 

378 
method_setup trans_linear = 

379 
{* Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (Order_Tac.linear_tac)) *} 

380 
{* transitivity reasoner for linear orders *} 

381 
*) 

382 

383 
(* 

384 
declare order.order_refl [simp del] order_less_irrefl [simp del] 

385 

386 
can currently not be removed, abel_cancel relies on it. 

387 
*) 

388 

389 

21083  390 
subsection {* Bounded quantifiers *} 
391 

392 
syntax 

393 
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) 

394 
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) 

395 
"_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) 

396 
"_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) 

397 

398 
"_gtAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) 

399 
"_gtEx" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) 

400 
"_geAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) 

401 
"_geEx" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) 

402 

403 
syntax (xsymbols) 

404 
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) 

405 
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) 

406 
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) 

407 
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) 

408 

409 
"_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) 

410 
"_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) 

411 
"_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) 

412 
"_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) 

413 

414 
syntax (HOL) 

415 
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) 

416 
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) 

417 
"_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) 

418 
"_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) 

419 

420 
syntax (HTML output) 

421 
"_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) 

422 
"_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) 

423 
"_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) 

424 
"_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) 

425 

426 
"_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) 

427 
"_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) 

428 
"_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) 

429 
"_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) 

430 

431 
translations 

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

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

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

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

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

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

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

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

440 

441 
print_translation {* 

442 
let 

443 
fun mk v v' c n P = 

444 
if v = v' andalso not (member (op =) (map fst (Term.add_frees n [])) v) 

445 
then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match; 

446 
fun mk_all "\\<^const>Scratch.less" f = 

447 
f ("_lessAll", "_gtAll") 

448 
 mk_all "\\<^const>Scratch.less_eq" f = 

449 
f ("_leAll", "_geAll") 

450 
fun mk_ex "\\<^const>Scratch.less" f = 

451 
f ("_lessEx", "_gtEx") 

452 
 mk_ex "\\<^const>Scratch.less_eq" f = 

453 
f ("_leEx", "_geEx"); 

454 
fun tr_all' [Const ("_bound", _) $ Free (v, _), Const("op >", _) 

455 
$ (Const (c, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] = 

456 
mk v v' (mk_all c fst) n P 

457 
 tr_all' [Const ("_bound", _) $ Free (v, _), Const("op >", _) 

458 
$ (Const (c, _) $ n $ (Const ("_bound", _) $ Free (v', _))) $ P] = 

459 
mk v v' (mk_all c snd) n P; 

460 
fun tr_ex' [Const ("_bound", _) $ Free (v, _), Const("op &", _) 

461 
$ (Const (c, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] = 

462 
mk v v' (mk_ex c fst) n P 

463 
 tr_ex' [Const ("_bound", _) $ Free (v, _), Const("op &", _) 

464 
$ (Const (c, _) $ n $ (Const ("_bound", _) $ Free (v', _))) $ P] = 

465 
mk v v' (mk_ex c snd) n P; 

466 
in 

467 
[("ALL ", tr_all'), ("EX ", tr_ex')] 

468 
end 

469 
*} 

470 

471 

472 
subsection {* Transitivity reasoning on decreasing inequalities *} 

473 

474 
text {* These support proving chains of decreasing inequalities 

475 
a >= b >= c ... in Isar proofs. *} 

476 

477 
lemma xt1: 

478 
"a = b ==> b > c ==> a > c" 

479 
"a > b ==> b = c ==> a > c" 

480 
"a = b ==> b >= c ==> a >= c" 

481 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

486 
"(a::'a::order) > b ==> b > a ==> ?P" 

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

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

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

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

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

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

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

494 
by auto 

495 

496 
lemma xt2: 

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

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

499 

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

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

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

503 

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

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

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

507 

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

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

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

511 

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

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

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

515 

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

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

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

519 

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

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

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

523 

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

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

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

527 

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

529 

530 
(* 

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

532 
for the wrong thing in an Isar proof. 

533 

534 
The extra transitivity rules can be used as follows: 

535 

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

537 
proof  

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

539 
sorry 

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

541 
sorry 

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

543 
sorry 

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

545 
sorry 

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

547 
sorry 

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

549 
sorry 

550 
finally (xtrans) show ?thesis . 

551 
qed 

552 

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

554 
leave out the "(xtrans)" above. 

555 
*) 

556 

557 

558 
subsection {* Least value operator, monotonicity and min/max *} 

559 

560 
(*FIXME: derive more of the min/max laws generically via semilattices*) 

561 

562 
constdefs 

563 
Least :: "('a::ord => bool) => 'a" (binder "LEAST " 10) 

564 
"Least P == THE x. P x & (ALL y. P y > x <= y)" 

565 
 {* We can no longer use LeastM because the latter requires HilbertAC. *} 

566 

567 
lemma LeastI2_order: 

568 
"[ P (x::'a::order); 

569 
!!y. P y ==> x <= y; 

570 
!!x. [ P x; ALL y. P y > x \<le> y ] ==> Q x ] 

571 
==> Q (Least P)" 

572 
apply (unfold Least_def) 

573 
apply (rule theI2) 

574 
apply (blast intro: order_antisym)+ 

575 
done 

576 

577 
lemma Least_equality: 

578 
"[ P (k::'a::order); !!x. P x ==> k <= x ] ==> (LEAST x. P x) = k" 

579 
apply (simp add: Least_def) 

580 
apply (rule the_equality) 

581 
apply (auto intro!: order_antisym) 

582 
done 

583 

584 
locale mono = 

585 
fixes f 

586 
assumes mono: "A <= B ==> f A <= f B" 

587 

588 
lemmas monoI [intro?] = mono.intro 

589 
and monoD [dest?] = mono.mono 

590 

591 
constdefs 

592 
min :: "['a::ord, 'a] => 'a" 

593 
"min a b == (if a <= b then a else b)" 

594 
max :: "['a::ord, 'a] => 'a" 

595 
"max a b == (if a <= b then b else a)" 

596 

597 
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least" 

598 
apply (simp add: min_def) 

599 
apply (blast intro: order_antisym) 

600 
done 

601 

602 
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x" 

603 
apply (simp add: max_def) 

604 
apply (blast intro: order_antisym) 

605 
done 

606 

607 
lemma min_leastL: "(!!x. least <= x) ==> min least x = least" 

608 
by (simp add: min_def) 

609 

610 
lemma max_leastL: "(!!x. least <= x) ==> max least x = x" 

611 
by (simp add: max_def) 

612 

613 
lemma min_of_mono: 

614 
"(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)" 

615 
by (simp add: min_def) 

616 

617 
lemma max_of_mono: 

618 
"(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)" 

619 
by (simp add: max_def) 

15524  620 

621 
text{* Instantiate locales: *} 

622 

15837  623 
interpretation min_max: 
15780  624 
lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

625 
apply unfold_locales 
15524  626 
apply(simp add:min_def linorder_not_le order_less_imp_le) 
627 
apply(simp add:min_def linorder_not_le order_less_imp_le) 

628 
apply(simp add:min_def linorder_not_le order_less_imp_le) 

629 
done 

630 

15837  631 
interpretation min_max: 
15780  632 
upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"] 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

633 
apply unfold_locales 
15524  634 
apply(simp add: max_def linorder_not_le order_less_imp_le) 
635 
apply(simp add: max_def linorder_not_le order_less_imp_le) 

636 
apply(simp add: max_def linorder_not_le order_less_imp_le) 

637 
done 

638 

15837  639 
interpretation min_max: 
15780  640 
lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

641 
by unfold_locales 
15524  642 

15837  643 
interpretation min_max: 
15780  644 
distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"] 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19931
diff
changeset

645 
apply unfold_locales 
15524  646 
apply(rule_tac x=x and y=y in linorder_le_cases) 
647 
apply(rule_tac x=x and y=z in linorder_le_cases) 

648 
apply(rule_tac x=y and y=z in linorder_le_cases) 

649 
apply(simp add:min_def max_def) 

650 
apply(simp add:min_def max_def) 

651 
apply(rule_tac x=y and y=z in linorder_le_cases) 

652 
apply(simp add:min_def max_def) 

653 
apply(simp add:min_def max_def) 

654 
apply(rule_tac x=x and y=z in linorder_le_cases) 

655 
apply(rule_tac x=y and y=z in linorder_le_cases) 

656 
apply(simp add:min_def max_def) 

657 
apply(simp add:min_def max_def) 

658 
apply(rule_tac x=y and y=z in linorder_le_cases) 

659 
apply(simp add:min_def max_def) 

660 
apply(simp add:min_def max_def) 

661 
done 

662 

663 
lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x  z <= y)" 

664 
apply(simp add:max_def) 

665 
apply (insert linorder_linear) 

666 
apply (blast intro: order_trans) 

667 
done 

668 

15780  669 
lemmas le_maxI1 = min_max.sup_ge1 
670 
lemmas le_maxI2 = min_max.sup_ge2 

15524  671 

672 
lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x  z < y)" 

673 
apply (simp add: max_def order_le_less) 

674 
apply (insert linorder_less_linear) 

675 
apply (blast intro: order_less_trans) 

676 
done 

677 

678 
lemma max_less_iff_conj [simp]: 

679 
"!!z::'a::linorder. (max x y < z) = (x < z & y < z)" 

680 
apply (simp add: order_le_less max_def) 

681 
apply (insert linorder_less_linear) 

682 
apply (blast intro: order_less_trans) 

683 
done 

15791  684 

15524  685 
lemma min_less_iff_conj [simp]: 
686 
"!!z::'a::linorder. (z < min x y) = (z < x & z < y)" 

687 
apply (simp add: order_le_less min_def) 

688 
apply (insert linorder_less_linear) 

689 
apply (blast intro: order_less_trans) 

690 
done 

691 

692 
lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z  y <= z)" 

693 
apply (simp add: min_def) 

694 
apply (insert linorder_linear) 

695 
apply (blast intro: order_trans) 

696 
done 

697 

698 
lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z  y < z)" 

699 
apply (simp add: min_def order_le_less) 

700 
apply (insert linorder_less_linear) 

701 
apply (blast intro: order_less_trans) 

702 
done 

703 

15780  704 
lemmas max_ac = min_max.sup_assoc min_max.sup_commute 
705 
mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute] 

15524  706 

15780  707 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute 
708 
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute] 

15524  709 

710 
lemma split_min: 

711 
"P (min (i::'a::linorder) j) = ((i <= j > P(i)) & (~ i <= j > P(j)))" 

712 
by (simp add: min_def) 

713 

714 
lemma split_max: 

715 
"P (max (i::'a::linorder) j) = ((i <= j > P(j)) & (~ i <= j > P(i)))" 

716 
by (simp add: max_def) 

717 

718 
end 