author  haftmann 
Mon, 23 Oct 2006 11:05:07 +0200  
changeset 21091  5061e3e56484 
parent 21083  a1de02f047d0 
child 21180  f27f12bcafb8 
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 

21091  238 
ML {* 
239 
local 

240 

241 
fun decomp_gen sort thy (Trueprop $ t) = 

242 
let fun of_sort t = let val T = type_of t in 

243 
(* exclude numeric types: linear arithmetic subsumes transitivity *) 

244 
T <> HOLogic.natT andalso T <> HOLogic.intT andalso 

245 
T <> HOLogic.realT andalso Sign.of_sort thy (T, sort) end 

246 
fun dec (Const ("Not", _) $ t) = ( 

247 
case dec t of 

248 
NONE => NONE 

249 
 SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2)) 

250 
 dec (Const ("op =", _) $ t1 $ t2) = 

251 
if of_sort t1 

252 
then SOME (t1, "=", t2) 

253 
else NONE 

254 
 dec (Const ("Orderings.less_eq", _) $ t1 $ t2) = 

255 
if of_sort t1 

256 
then SOME (t1, "<=", t2) 

257 
else NONE 

258 
 dec (Const ("Orderings.less", _) $ t1 $ t2) = 

259 
if of_sort t1 

260 
then SOME (t1, "<", t2) 

261 
else NONE 

262 
 dec _ = NONE 

263 
in dec t end; 

264 

265 
in 

266 

267 
structure Quasi_Tac = Quasi_Tac_Fun ( 

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

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

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

271 
struct 

272 
val le_trans = thm "order_trans"; 

273 
val le_refl = thm "order_refl"; 

274 
val eqD1 = thm "order_eq_refl"; 

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

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

277 
val less_imp_le = thm "order_less_imp_le"; 

278 
val le_neq_trans = thm "order_le_neq_trans"; 

279 
val neq_le_trans = thm "order_neq_le_trans"; 

280 
val less_imp_neq = thm "less_imp_neq"; 

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

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

283 

284 
end); 

285 

286 
structure Order_Tac = Order_Tac_Fun ( 

287 
struct 

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

289 
val le_refl = thm "order_refl"; 

290 
val less_imp_le = thm "order_less_imp_le"; 

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

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

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

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

295 
val eqI = thm "order_antisym"; 

296 
val eqD1 = thm "order_eq_refl"; 

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

298 
val less_trans = thm "order_less_trans"; 

299 
val less_le_trans = thm "order_less_le_trans"; 

300 
val le_less_trans = thm "order_le_less_trans"; 

301 
val le_trans = thm "order_trans"; 

302 
val le_neq_trans = thm "order_le_neq_trans"; 

303 
val neq_le_trans = thm "order_neq_le_trans"; 

304 
val less_imp_neq = thm "less_imp_neq"; 

305 
val eq_neq_eq_imp_neq = thm "eq_neq_eq_imp_neq"; 

306 
val not_sym = thm "not_sym"; 

307 
val decomp_part = decomp_gen ["Orderings.order"]; 

308 
val decomp_lin = decomp_gen ["Orderings.linorder"]; 

309 

310 
end); 

311 

312 
end; 

313 
*} 

314 

21083  315 
setup {* 
316 
let 

317 

318 
val order_antisym_conv = thm "order_antisym_conv" 

319 
val linorder_antisym_conv1 = thm "linorder_antisym_conv1" 

320 
val linorder_antisym_conv2 = thm "linorder_antisym_conv2" 

321 
val linorder_antisym_conv3 = thm "linorder_antisym_conv3" 

322 

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

15524  324 

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

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

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

329 
in case find_first (prp t) prems of 

330 
NONE => 

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

332 
in case find_first (prp t) prems of 

333 
NONE => NONE 

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

335 
end 

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

337 
end 

338 
handle THM _ => NONE; 

15524  339 

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

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

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

344 
in case find_first (prp t) prems of 

345 
NONE => 

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

347 
in case find_first (prp t) prems of 

348 
NONE => NONE 

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

350 
end 

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

352 
end 

353 
handle THM _ => NONE; 

15524  354 

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

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

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

359 

360 
in 

21091  361 
(fn thy => (Simplifier.change_simpset_of thy 
362 
(fn ss => ss 

363 
addsimprocs [antisym_le, antisym_less] 

364 
addSolver (mk_solver "Trans_linear" (fn _ => Order_Tac.linear_tac)) 

365 
addSolver (mk_solver "Trans_partial" (fn _ => Order_Tac.partial_tac))) 

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). *); thy)) 

21083  370 
end 
371 
*} 

15524  372 

373 

21083  374 
subsection {* Bounded quantifiers *} 
375 

376 
syntax 

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

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

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

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

381 

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

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

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

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

386 

387 
syntax (xsymbols) 

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

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

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

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

392 

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

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

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

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

397 

398 
syntax (HOL) 

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

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

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

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

403 

404 
syntax (HTML output) 

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

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

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

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

409 

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

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

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

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

414 

415 
translations 

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

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

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

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

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

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

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

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

424 

425 
print_translation {* 

426 
let 

427 
fun mk v v' c n P = 

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

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

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

431 
f ("_lessAll", "_gtAll") 

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

433 
f ("_leAll", "_geAll") 

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

435 
f ("_lessEx", "_gtEx") 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

450 
in 

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

452 
end 

453 
*} 

454 

455 

456 
subsection {* Transitivity reasoning on decreasing inequalities *} 

457 

458 
text {* These support proving chains of decreasing inequalities 

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

460 

461 
lemma xt1: 

462 
"a = b ==> b > c ==> a > c" 

463 
"a > b ==> b = c ==> a > c" 

464 
"a = b ==> b >= c ==> a >= c" 

465 
"a >= b ==> b = c ==> a >= c" 

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

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

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

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

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

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

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

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

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

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

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

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

478 
by auto 

479 

480 
lemma xt2: 

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

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

483 

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

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

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

487 

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

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

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

491 

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

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

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

495 

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

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

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

499 

500 
lemma xt7: "(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 xt8: "(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 xt9: "(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 
lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 

513 

514 
(* 

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

516 
for the wrong thing in an Isar proof. 

517 

518 
The extra transitivity rules can be used as follows: 

519 

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

521 
proof  

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

523 
sorry 

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

525 
sorry 

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

527 
sorry 

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

529 
sorry 

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

531 
sorry 

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

533 
sorry 

534 
finally (xtrans) show ?thesis . 

535 
qed 

536 

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

538 
leave out the "(xtrans)" above. 

539 
*) 

540 

541 

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

543 

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

545 

546 
constdefs 

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

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

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

550 

551 
lemma LeastI2_order: 

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

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

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

555 
==> Q (Least P)" 

556 
apply (unfold Least_def) 

557 
apply (rule theI2) 

558 
apply (blast intro: order_antisym)+ 

559 
done 

560 

561 
lemma Least_equality: 

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

563 
apply (simp add: Least_def) 

564 
apply (rule the_equality) 

565 
apply (auto intro!: order_antisym) 

566 
done 

567 

568 
locale mono = 

569 
fixes f 

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

571 

572 
lemmas monoI [intro?] = mono.intro 

573 
and monoD [dest?] = mono.mono 

574 

575 
constdefs 

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

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

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

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

580 

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

582 
apply (simp add: min_def) 

583 
apply (blast intro: order_antisym) 

584 
done 

585 

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

587 
apply (simp add: max_def) 

588 
apply (blast intro: order_antisym) 

589 
done 

590 

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

592 
by (simp add: min_def) 

593 

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

595 
by (simp add: max_def) 

596 

597 
lemma min_of_mono: 

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

599 
by (simp add: min_def) 

600 

601 
lemma max_of_mono: 

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

603 
by (simp add: max_def) 

15524  604 

605 
text{* Instantiate locales: *} 

606 

15837  607 
interpretation min_max: 
15780  608 
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

609 
apply unfold_locales 
15524  610 
apply(simp add:min_def linorder_not_le order_less_imp_le) 
611 
apply(simp add:min_def linorder_not_le order_less_imp_le) 

612 
apply(simp add:min_def linorder_not_le order_less_imp_le) 

613 
done 

614 

15837  615 
interpretation min_max: 
15780  616 
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

617 
apply unfold_locales 
15524  618 
apply(simp add: max_def linorder_not_le order_less_imp_le) 
619 
apply(simp add: max_def linorder_not_le order_less_imp_le) 

620 
apply(simp add: max_def linorder_not_le order_less_imp_le) 

621 
done 

622 

15837  623 
interpretation min_max: 
15780  624 
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

625 
by unfold_locales 
15524  626 

15837  627 
interpretation min_max: 
15780  628 
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

629 
apply unfold_locales 
15524  630 
apply(rule_tac x=x and y=y in linorder_le_cases) 
631 
apply(rule_tac x=x and y=z in linorder_le_cases) 

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

633 
apply(simp add:min_def max_def) 

634 
apply(simp add:min_def max_def) 

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

636 
apply(simp add:min_def max_def) 

637 
apply(simp add:min_def max_def) 

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

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

640 
apply(simp add:min_def max_def) 

641 
apply(simp add:min_def max_def) 

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

643 
apply(simp add:min_def max_def) 

644 
apply(simp add:min_def max_def) 

645 
done 

646 

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

648 
apply(simp add:max_def) 

649 
apply (insert linorder_linear) 

650 
apply (blast intro: order_trans) 

651 
done 

652 

15780  653 
lemmas le_maxI1 = min_max.sup_ge1 
654 
lemmas le_maxI2 = min_max.sup_ge2 

15524  655 

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

657 
apply (simp add: max_def order_le_less) 

658 
apply (insert linorder_less_linear) 

659 
apply (blast intro: order_less_trans) 

660 
done 

661 

662 
lemma max_less_iff_conj [simp]: 

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

664 
apply (simp add: order_le_less max_def) 

665 
apply (insert linorder_less_linear) 

666 
apply (blast intro: order_less_trans) 

667 
done 

15791  668 

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

671 
apply (simp add: order_le_less min_def) 

672 
apply (insert linorder_less_linear) 

673 
apply (blast intro: order_less_trans) 

674 
done 

675 

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

677 
apply (simp add: min_def) 

678 
apply (insert linorder_linear) 

679 
apply (blast intro: order_trans) 

680 
done 

681 

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

683 
apply (simp add: min_def order_le_less) 

684 
apply (insert linorder_less_linear) 

685 
apply (blast intro: order_less_trans) 

686 
done 

687 

15780  688 
lemmas max_ac = min_max.sup_assoc min_max.sup_commute 
689 
mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute] 

15524  690 

15780  691 
lemmas min_ac = min_max.inf_assoc min_max.inf_commute 
692 
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute] 

15524  693 

694 
lemma split_min: 

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

696 
by (simp add: min_def) 

697 

698 
lemma split_max: 

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

700 
by (simp add: max_def) 

701 

702 
end 