author  wenzelm 
Fri, 04 Jan 2002 19:29:30 +0100  
changeset 12633  ad9277743664 
parent 12338  de0f4a63baa5 
child 12897  f4d10ad0ea7b 
permissions  rwrr 
923  1 
(* Title: HOL/Set.thy 
2 
ID: $Id$ 

12257  3 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 
12020  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
923  5 
*) 
6 

11979  7 
header {* Set theory for higherorder logic *} 
8 

9 
theory Set = HOL 

10 
files ("subset.ML") ("equalities.ML") ("mono.ML"): 

11 

12 
text {* A set in HOL is simply a predicate. *} 

923  13 

2261  14 

11979  15 
subsection {* Basic syntax *} 
2261  16 

3947  17 
global 
18 

11979  19 
typedecl 'a set 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12257
diff
changeset

20 
arities set :: (type) type 
3820  21 

923  22 
consts 
11979  23 
"{}" :: "'a set" ("{}") 
24 
UNIV :: "'a set" 

25 
insert :: "'a => 'a set => 'a set" 

26 
Collect :: "('a => bool) => 'a set"  "comprehension" 

27 
Int :: "'a set => 'a set => 'a set" (infixl 70) 

28 
Un :: "'a set => 'a set => 'a set" (infixl 65) 

29 
UNION :: "'a set => ('a => 'b set) => 'b set"  "general union" 

30 
INTER :: "'a set => ('a => 'b set) => 'b set"  "general intersection" 

31 
Union :: "'a set set => 'a set"  "union of a set" 

32 
Inter :: "'a set set => 'a set"  "intersection of a set" 

33 
Pow :: "'a set => 'a set set"  "powerset" 

34 
Ball :: "'a set => ('a => bool) => bool"  "bounded universal quantifiers" 

35 
Bex :: "'a set => ('a => bool) => bool"  "bounded existential quantifiers" 

36 
image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) 

37 

38 
syntax 

39 
"op :" :: "'a => 'a set => bool" ("op :") 

40 
consts 

41 
"op :" :: "'a => 'a set => bool" ("(_/ : _)" [50, 51] 50)  "membership" 

42 

43 
local 

44 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12257
diff
changeset

45 
instance set :: (type) ord .. 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12257
diff
changeset

46 
instance set :: (type) minus .. 
923  47 

48 

11979  49 
subsection {* Additional concrete syntax *} 
2261  50 

923  51 
syntax 
11979  52 
range :: "('a => 'b) => 'b set"  "of function" 
923  53 

11979  54 
"op ~:" :: "'a => 'a set => bool" ("op ~:")  "nonmembership" 
55 
"op ~:" :: "'a => 'a set => bool" ("(_/ ~: _)" [50, 51] 50) 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

56 

11979  57 
"@Finset" :: "args => 'a set" ("{(_)}") 
58 
"@Coll" :: "pttrn => bool => 'a set" ("(1{_./ _})") 

59 
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ /_./ _})") 

923  60 

11979  61 
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" 10) 
62 
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" 10) 

63 
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" 10) 

64 
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" 10) 

923  65 

11979  66 
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10) 
67 
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10) 

923  68 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

69 
syntax (HOL) 
11979  70 
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3! _:_./ _)" [0, 0, 10] 10) 
71 
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3? _:_./ _)" [0, 0, 10] 10) 

923  72 

73 
translations 

10832  74 
"range f" == "f`UNIV" 
923  75 
"x ~: y" == "~ (x : y)" 
76 
"{x, xs}" == "insert x {xs}" 

77 
"{x}" == "insert x {}" 

78 
"{x. P}" == "Collect (%x. P)" 

4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

79 
"UN x y. B" == "UN x. UN y. B" 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

80 
"UN x. B" == "UNION UNIV (%x. B)" 
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

81 
"INT x y. B" == "INT x. INT y. B" 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

82 
"INT x. B" == "INTER UNIV (%x. B)" 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4151
diff
changeset

83 
"UN x:A. B" == "UNION A (%x. B)" 
923  84 
"INT x:A. B" == "INTER A (%x. B)" 
7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

85 
"ALL x:A. P" == "Ball A (%x. P)" 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

86 
"EX x:A. P" == "Bex A (%x. P)" 
923  87 

12633  88 
syntax (output) 
11979  89 
"_setle" :: "'a set => 'a set => bool" ("op <=") 
90 
"_setle" :: "'a set => 'a set => bool" ("(_/ <= _)" [50, 51] 50) 

91 
"_setless" :: "'a set => 'a set => bool" ("op <") 

92 
"_setless" :: "'a set => 'a set => bool" ("(_/ < _)" [50, 51] 50) 

923  93 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12023
diff
changeset

94 
syntax (xsymbols) 
11979  95 
"_setle" :: "'a set => 'a set => bool" ("op \<subseteq>") 
96 
"_setle" :: "'a set => 'a set => bool" ("(_/ \<subseteq> _)" [50, 51] 50) 

97 
"_setless" :: "'a set => 'a set => bool" ("op \<subset>") 

98 
"_setless" :: "'a set => 'a set => bool" ("(_/ \<subset> _)" [50, 51] 50) 

99 
"op Int" :: "'a set => 'a set => 'a set" (infixl "\<inter>" 70) 

100 
"op Un" :: "'a set => 'a set => 'a set" (infixl "\<union>" 65) 

101 
"op :" :: "'a => 'a set => bool" ("op \<in>") 

102 
"op :" :: "'a => 'a set => bool" ("(_/ \<in> _)" [50, 51] 50) 

103 
"op ~:" :: "'a => 'a set => bool" ("op \<notin>") 

104 
"op ~:" :: "'a => 'a set => bool" ("(_/ \<notin> _)" [50, 51] 50) 

105 
"@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" 10) 

106 
"@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" 10) 

107 
"@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" 10) 

108 
"@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" 10) 

109 
Union :: "'a set set => 'a set" ("\<Union>_" [90] 90) 

110 
Inter :: "'a set set => 'a set" ("\<Inter>_" [90] 90) 

111 
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10) 

112 
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10) 

2261  113 

2412  114 
translations 
11979  115 
"op \<subseteq>" => "op <= :: _ set => _ set => bool" 
116 
"op \<subset>" => "op < :: _ set => _ set => bool" 

2261  117 

118 

11979  119 
typed_print_translation {* 
120 
let 

121 
fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = 

122 
list_comb (Syntax.const "_setle", ts) 

123 
 le_tr' _ _ _ = raise Match; 

124 

125 
fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts = 

126 
list_comb (Syntax.const "_setless", ts) 

127 
 less_tr' _ _ _ = raise Match; 

128 
in [("op <=", le_tr'), ("op <", less_tr')] end 

129 
*} 

2261  130 

11979  131 
text {* 
132 
\medskip Translate between @{text "{e  x1...xn. P}"} and @{text 

133 
"{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is 

134 
only translated if @{text "[0..n] subset bvs(e)"}. 

135 
*} 

136 

137 
parse_translation {* 

138 
let 

139 
val ex_tr = snd (mk_binder_tr ("EX ", "Ex")); 

3947  140 

11979  141 
fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1 
142 
 nvars _ = 1; 

143 

144 
fun setcompr_tr [e, idts, b] = 

145 
let 

146 
val eq = Syntax.const "op =" $ Bound (nvars idts) $ e; 

147 
val P = Syntax.const "op &" $ eq $ b; 

148 
val exP = ex_tr [idts, P]; 

149 
in Syntax.const "Collect" $ Abs ("", dummyT, exP) end; 

150 

151 
in [("@SetCompr", setcompr_tr)] end; 

152 
*} 

923  153 

11979  154 
print_translation {* 
155 
let 

156 
val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY")); 

157 

158 
fun setcompr_tr' [Abs (_, _, P)] = 

159 
let 

160 
fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1) 

161 
 check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) = 

162 
if n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso 

163 
((0 upto (n  1)) subset add_loose_bnos (e, 0, [])) then () 

164 
else raise Match; 

923  165 

11979  166 
fun tr' (_ $ abs) = 
167 
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs] 

168 
in Syntax.const "@SetCompr" $ e $ idts $ Q end; 

169 
in check (P, 0); tr' P end; 

170 
in [("Collect", setcompr_tr')] end; 

171 
*} 

172 

173 

174 
subsection {* Rules and definitions *} 

175 

176 
text {* Isomorphisms between predicates and sets. *} 

923  177 

11979  178 
axioms 
179 
mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)" 

180 
Collect_mem_eq [simp]: "{x. x:A} = A" 

181 

182 
defs 

183 
Ball_def: "Ball A P == ALL x. x:A > P(x)" 

184 
Bex_def: "Bex A P == EX x. x:A & P(x)" 

185 

186 
defs (overloaded) 

187 
subset_def: "A <= B == ALL x:A. x:B" 

188 
psubset_def: "A < B == (A::'a set) <= B & ~ A=B" 

189 
Compl_def: " A == {x. ~x:A}" 

12257  190 
set_diff_def: "A  B == {x. x:A & ~x:B}" 
923  191 

192 
defs 

11979  193 
Un_def: "A Un B == {x. x:A  x:B}" 
194 
Int_def: "A Int B == {x. x:A & x:B}" 

195 
INTER_def: "INTER A B == {y. ALL x:A. y: B(x)}" 

196 
UNION_def: "UNION A B == {y. EX x:A. y: B(x)}" 

197 
Inter_def: "Inter S == (INT x:S. x)" 

198 
Union_def: "Union S == (UN x:S. x)" 

199 
Pow_def: "Pow A == {B. B <= A}" 

200 
empty_def: "{} == {x. False}" 

201 
UNIV_def: "UNIV == {x. True}" 

202 
insert_def: "insert a B == {x. x=a} Un B" 

203 
image_def: "f`A == {y. EX x:A. y = f(x)}" 

204 

205 

206 
subsection {* Lemmas and proof tool setup *} 

207 

208 
subsubsection {* Relating predicates and sets *} 

209 

12257  210 
lemma CollectI: "P(a) ==> a : {x. P(x)}" 
11979  211 
by simp 
212 

213 
lemma CollectD: "a : {x. P(x)} ==> P(a)" 

214 
by simp 

215 

12257  216 
lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B" 
217 
apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals]) 

218 
apply (rule Collect_mem_eq) 

219 
apply (rule Collect_mem_eq) 

220 
done 

11979  221 

222 
lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" 

223 
by simp 

224 

12257  225 
lemmas CollectE = CollectD [elim_format] 
11979  226 

227 

228 
subsubsection {* Bounded quantifiers *} 

229 

230 
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" 

231 
by (simp add: Ball_def) 

232 

233 
lemmas strip = impI allI ballI 

234 

235 
lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x" 

236 
by (simp add: Ball_def) 

237 

238 
lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" 

239 
by (unfold Ball_def) blast 

240 

241 
text {* 

242 
\medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and 

243 
@{prop "a:A"}; creates assumption @{prop "P a"}. 

244 
*} 

245 

246 
ML {* 

247 
local val ballE = thm "ballE" 

248 
in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end; 

249 
*} 

250 

251 
text {* 

252 
Gives better instantiation for bound: 

253 
*} 

254 

255 
ML_setup {* 

256 
claset_ref() := claset() addbefore ("bspec", datac (thm "bspec") 1); 

257 
*} 

258 

259 
lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" 

260 
 {* Normally the best argument order: @{prop "P x"} constrains the 

261 
choice of @{prop "x:A"}. *} 

262 
by (unfold Bex_def) blast 

263 

264 
lemma rev_bexI: "x:A ==> P x ==> EX x:A. P x" 

265 
 {* The best argument order when there is only one @{prop "x:A"}. *} 

266 
by (unfold Bex_def) blast 

267 

268 
lemma bexCI: "(ALL x:A. ~P x ==> P a) ==> a:A ==> EX x:A. P x" 

269 
by (unfold Bex_def) blast 

270 

271 
lemma bexE [elim!]: "EX x:A. P x ==> (!!x. x:A ==> P x ==> Q) ==> Q" 

272 
by (unfold Bex_def) blast 

273 

274 
lemma ball_triv [simp]: "(ALL x:A. P) = ((EX x. x:A) > P)" 

275 
 {* Trival rewrite rule. *} 

276 
by (simp add: Ball_def) 

277 

278 
lemma bex_triv [simp]: "(EX x:A. P) = ((EX x. x:A) & P)" 

279 
 {* Dual form for existentials. *} 

280 
by (simp add: Bex_def) 

281 

282 
lemma bex_triv_one_point1 [simp]: "(EX x:A. x = a) = (a:A)" 

283 
by blast 

284 

285 
lemma bex_triv_one_point2 [simp]: "(EX x:A. a = x) = (a:A)" 

286 
by blast 

287 

288 
lemma bex_one_point1 [simp]: "(EX x:A. x = a & P x) = (a:A & P a)" 

289 
by blast 

290 

291 
lemma bex_one_point2 [simp]: "(EX x:A. a = x & P x) = (a:A & P a)" 

292 
by blast 

293 

294 
lemma ball_one_point1 [simp]: "(ALL x:A. x = a > P x) = (a:A > P a)" 

295 
by blast 

296 

297 
lemma ball_one_point2 [simp]: "(ALL x:A. a = x > P x) = (a:A > P a)" 

298 
by blast 

299 

300 
ML_setup {* 

301 
let 

302 
val Ball_def = thm "Ball_def"; 

303 
val Bex_def = thm "Bex_def"; 

304 

305 
val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

306 
("EX x:A. P x & Q x", HOLogic.boolT); 

307 

308 
val prove_bex_tac = 

309 
rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac; 

310 
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; 

311 

312 
val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) 

313 
("ALL x:A. P x > Q x", HOLogic.boolT); 

314 

315 
val prove_ball_tac = 

316 
rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac; 

317 
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; 

318 

319 
val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex; 

320 
val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball; 

321 
in 

322 
Addsimprocs [defBALL_regroup, defBEX_regroup] 

323 
end; 

324 
*} 

325 

326 

327 
subsubsection {* Congruence rules *} 

328 

329 
lemma ball_cong [cong]: 

330 
"A = B ==> (!!x. x:B ==> P x = Q x) ==> 

331 
(ALL x:A. P x) = (ALL x:B. Q x)" 

332 
by (simp add: Ball_def) 

333 

334 
lemma bex_cong [cong]: 

335 
"A = B ==> (!!x. x:B ==> P x = Q x) ==> 

336 
(EX x:A. P x) = (EX x:B. Q x)" 

337 
by (simp add: Bex_def cong: conj_cong) 

1273  338 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

339 

11979  340 
subsubsection {* Subsets *} 
341 

342 
lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B" 

343 
by (simp add: subset_def) 

344 

345 
text {* 

346 
\medskip Map the type @{text "'a set => anything"} to just @{typ 

347 
'a}; for overloading constants whose first argument has type @{typ 

348 
"'a set"}. 

349 
*} 

350 

351 
ML {* 

352 
fun overload_1st_set s = Blast.overloaded (s, HOLogic.dest_setT o domain_type); 

353 
*} 

354 

355 
ML " 

356 
(* While (:) is not, its type must be kept 

357 
for overloading of = to work. *) 

358 
Blast.overloaded (\"op :\", domain_type); 

359 

360 
overload_1st_set \"Ball\"; (*need UNION, INTER also?*) 

361 
overload_1st_set \"Bex\"; 

362 

363 
(*Image: retain the type of the set being expressed*) 

364 
Blast.overloaded (\"image\", domain_type); 

365 
" 

366 

367 
lemma subsetD [elim]: "A <= B ==> c:A ==> c:B" 

368 
 {* Rule in Modus Ponens style. *} 

369 
by (unfold subset_def) blast 

370 

371 
declare subsetD [intro?]  FIXME 

372 

373 
lemma rev_subsetD: "c:A ==> A <= B ==> c:B" 

374 
 {* The same, with reversed premises for use with @{text erule}  

375 
cf @{text rev_mp}. *} 

376 
by (rule subsetD) 

377 

378 
declare rev_subsetD [intro?]  FIXME 

379 

380 
text {* 

381 
\medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}. 

382 
*} 

383 

384 
ML {* 

385 
local val rev_subsetD = thm "rev_subsetD" 

386 
in fun impOfSubs th = th RSN (2, rev_subsetD) end; 

387 
*} 

388 

389 
lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P" 

390 
 {* Classical elimination rule. *} 

391 
by (unfold subset_def) blast 

392 

393 
text {* 

394 
\medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and 

395 
creates the assumption @{prop "c:B"}. 

396 
*} 

397 

398 
ML {* 

399 
local val subsetCE = thm "subsetCE" 

400 
in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; 

401 
*} 

402 

403 
lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A" 

404 
by blast 

405 

406 
lemma subset_refl: "A <= (A::'a set)" 

407 
by fast 

408 

409 
lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)" 

410 
by blast 

923  411 

2261  412 

11979  413 
subsubsection {* Equality *} 
414 

415 
lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)" 

416 
 {* Antisymmetry of the subset relation. *} 

417 
by (rule set_ext) (blast intro: subsetD) 

418 

419 
lemmas equalityI = subset_antisym 

420 

421 
text {* 

422 
\medskip Equality rules from ZF set theory  are they appropriate 

423 
here? 

424 
*} 

425 

426 
lemma equalityD1: "A = B ==> A <= (B::'a set)" 

427 
by (simp add: subset_refl) 

428 

429 
lemma equalityD2: "A = B ==> B <= (A::'a set)" 

430 
by (simp add: subset_refl) 

431 

432 
text {* 

433 
\medskip Be careful when adding this to the claset as @{text 

434 
subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{} 

435 
<= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}! 

436 
*} 

437 

438 
lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P" 

439 
by (simp add: subset_refl) 

923  440 

11979  441 
lemma equalityCE [elim]: 
442 
"A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P" 

443 
by blast 

444 

445 
text {* 

446 
\medskip Lemma for creating induction formulae  for "pattern 

447 
matching" on @{text p}. To make the induction hypotheses usable, 

448 
apply @{text spec} or @{text bspec} to put universal quantifiers over the free 

449 
variables in @{text p}. 

450 
*} 

451 

452 
lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z > R) ==> R" 

453 
by simp 

923  454 

11979  455 
lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)" 
456 
by simp 

457 

458 

459 
subsubsection {* The universal set  UNIV *} 

460 

461 
lemma UNIV_I [simp]: "x : UNIV" 

462 
by (simp add: UNIV_def) 

463 

464 
declare UNIV_I [intro]  {* unsafe makes it less likely to cause problems *} 

465 

466 
lemma UNIV_witness [intro?]: "EX x. x : UNIV" 

467 
by simp 

468 

469 
lemma subset_UNIV: "A <= UNIV" 

470 
by (rule subsetI) (rule UNIV_I) 

2388  471 

11979  472 
text {* 
473 
\medskip Etacontracting these two rules (to remove @{text P}) 

474 
causes them to be ignored because of their interaction with 

475 
congruence rules. 

476 
*} 

477 

478 
lemma ball_UNIV [simp]: "Ball UNIV P = All P" 

479 
by (simp add: Ball_def) 

480 

481 
lemma bex_UNIV [simp]: "Bex UNIV P = Ex P" 

482 
by (simp add: Bex_def) 

483 

484 

485 
subsubsection {* The empty set *} 

486 

487 
lemma empty_iff [simp]: "(c : {}) = False" 

488 
by (simp add: empty_def) 

489 

490 
lemma emptyE [elim!]: "a : {} ==> P" 

491 
by simp 

492 

493 
lemma empty_subsetI [iff]: "{} <= A" 

494 
 {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *} 

495 
by blast 

496 

497 
lemma equals0I: "(!!y. y:A ==> False) ==> A = {}" 

498 
by blast 

2388  499 

11979  500 
lemma equals0D: "A={} ==> a ~: A" 
501 
 {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *} 

502 
by blast 

503 

504 
lemma ball_empty [simp]: "Ball {} P = True" 

505 
by (simp add: Ball_def) 

506 

507 
lemma bex_empty [simp]: "Bex {} P = False" 

508 
by (simp add: Bex_def) 

509 

510 
lemma UNIV_not_empty [iff]: "UNIV ~= {}" 

511 
by (blast elim: equalityE) 

512 

513 

12023  514 
subsubsection {* The Powerset operator  Pow *} 
11979  515 

516 
lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)" 

517 
by (simp add: Pow_def) 

518 

519 
lemma PowI: "A <= B ==> A : Pow B" 

520 
by (simp add: Pow_def) 

521 

522 
lemma PowD: "A : Pow B ==> A <= B" 

523 
by (simp add: Pow_def) 

524 

525 
lemma Pow_bottom: "{}: Pow B" 

526 
by simp 

527 

528 
lemma Pow_top: "A : Pow A" 

529 
by (simp add: subset_refl) 

2684  530 

2388  531 

11979  532 
subsubsection {* Set complement *} 
533 

534 
lemma Compl_iff [simp]: "(c : A) = (c~:A)" 

535 
by (unfold Compl_def) blast 

536 

537 
lemma ComplI [intro!]: "(c:A ==> False) ==> c : A" 

538 
by (unfold Compl_def) blast 

539 

540 
text {* 

541 
\medskip This form, with negated conclusion, works well with the 

542 
Classical prover. Negated assumptions behave like formulae on the 

543 
right side of the notional turnstile ... *} 

544 

545 
lemma ComplD: "c : A ==> c~:A" 

546 
by (unfold Compl_def) blast 

547 

548 
lemmas ComplE [elim!] = ComplD [elim_format] 

549 

550 

551 
subsubsection {* Binary union  Un *} 

923  552 

11979  553 
lemma Un_iff [simp]: "(c : A Un B) = (c:A  c:B)" 
554 
by (unfold Un_def) blast 

555 

556 
lemma UnI1 [elim?]: "c:A ==> c : A Un B" 

557 
by simp 

558 

559 
lemma UnI2 [elim?]: "c:B ==> c : A Un B" 

560 
by simp 

923  561 

11979  562 
text {* 
563 
\medskip Classical introduction rule: no commitment to @{prop A} vs 

564 
@{prop B}. 

565 
*} 

566 

567 
lemma UnCI [intro!]: "(c~:B ==> c:A) ==> c : A Un B" 

568 
by auto 

569 

570 
lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P" 

571 
by (unfold Un_def) blast 

572 

573 

12023  574 
subsubsection {* Binary intersection  Int *} 
923  575 

11979  576 
lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)" 
577 
by (unfold Int_def) blast 

578 

579 
lemma IntI [intro!]: "c:A ==> c:B ==> c : A Int B" 

580 
by simp 

581 

582 
lemma IntD1: "c : A Int B ==> c:A" 

583 
by simp 

584 

585 
lemma IntD2: "c : A Int B ==> c:B" 

586 
by simp 

587 

588 
lemma IntE [elim!]: "c : A Int B ==> (c:A ==> c:B ==> P) ==> P" 

589 
by simp 

590 

591 

12023  592 
subsubsection {* Set difference *} 
11979  593 

594 
lemma Diff_iff [simp]: "(c : A  B) = (c:A & c~:B)" 

595 
by (unfold set_diff_def) blast 

923  596 

11979  597 
lemma DiffI [intro!]: "c : A ==> c ~: B ==> c : A  B" 
598 
by simp 

599 

600 
lemma DiffD1: "c : A  B ==> c : A" 

601 
by simp 

602 

603 
lemma DiffD2: "c : A  B ==> c : B ==> P" 

604 
by simp 

605 

606 
lemma DiffE [elim!]: "c : A  B ==> (c:A ==> c~:B ==> P) ==> P" 

607 
by simp 

608 

609 

610 
subsubsection {* Augmenting a set  insert *} 

611 

612 
lemma insert_iff [simp]: "(a : insert b A) = (a = b  a:A)" 

613 
by (unfold insert_def) blast 

614 

615 
lemma insertI1: "a : insert a B" 

616 
by simp 

617 

618 
lemma insertI2: "a : B ==> a : insert b B" 

619 
by simp 

923  620 

11979  621 
lemma insertE [elim!]: "a : insert b A ==> (a = b ==> P) ==> (a:A ==> P) ==> P" 
622 
by (unfold insert_def) blast 

623 

624 
lemma insertCI [intro!]: "(a~:B ==> a = b) ==> a: insert b B" 

625 
 {* Classical introduction rule. *} 

626 
by auto 

627 

628 
lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A  {x} <= B else A <= B)" 

629 
by auto 

630 

631 

632 
subsubsection {* Singletons, using insert *} 

633 

634 
lemma singletonI [intro!]: "a : {a}" 

635 
 {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *} 

636 
by (rule insertI1) 

637 

638 
lemma singletonD: "b : {a} ==> b = a" 

639 
by blast 

640 

641 
lemmas singletonE [elim!] = singletonD [elim_format] 

642 

643 
lemma singleton_iff: "(b : {a}) = (b = a)" 

644 
by blast 

645 

646 
lemma singleton_inject [dest!]: "{a} = {b} ==> a = b" 

647 
by blast 

648 

649 
lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})" 

650 
by blast 

651 

652 
lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})" 

653 
by blast 

654 

655 
lemma subset_singletonD: "A <= {x} ==> A={}  A = {x}" 

656 
by fast 

657 

658 
lemma singleton_conv [simp]: "{x. x = a} = {a}" 

659 
by blast 

660 

661 
lemma singleton_conv2 [simp]: "{x. a = x} = {a}" 

662 
by blast 

923  663 

11979  664 
lemma diff_single_insert: "A  {x} <= B ==> x : A ==> A <= insert x B" 
665 
by blast 

666 

667 

668 
subsubsection {* Unions of families *} 

669 

670 
text {* 

671 
@{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}. 

672 
*} 

673 

674 
lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)" 

675 
by (unfold UNION_def) blast 

676 

677 
lemma UN_I [intro]: "a:A ==> b: B a ==> b: (UN x:A. B x)" 

678 
 {* The order of the premises presupposes that @{term A} is rigid; 

679 
@{term b} may be flexible. *} 

680 
by auto 

681 

682 
lemma UN_E [elim!]: "b : (UN x:A. B x) ==> (!!x. x:A ==> b: B x ==> R) ==> R" 

683 
by (unfold UNION_def) blast 

923  684 

11979  685 
lemma UN_cong [cong]: 
686 
"A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)" 

687 
by (simp add: UNION_def) 

688 

689 

690 
subsubsection {* Intersections of families *} 

691 

692 
text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *} 

693 

694 
lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" 

695 
by (unfold INTER_def) blast 

923  696 

11979  697 
lemma INT_I [intro!]: "(!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)" 
698 
by (unfold INTER_def) blast 

699 

700 
lemma INT_D [elim]: "b : (INT x:A. B x) ==> a:A ==> b: B a" 

701 
by auto 

702 

703 
lemma INT_E [elim]: "b : (INT x:A. B x) ==> (b: B a ==> R) ==> (a~:A ==> R) ==> R" 

704 
 {* "Classical" elimination  by the Excluded Middle on @{prop "a:A"}. *} 

705 
by (unfold INTER_def) blast 

706 

707 
lemma INT_cong [cong]: 

708 
"A = B ==> (!!x. x:B ==> C x = D x) ==> (INT x:A. C x) = (INT x:B. D x)" 

709 
by (simp add: INTER_def) 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
5931
diff
changeset

710 

923  711 

11979  712 
subsubsection {* Union *} 
713 

714 
lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)" 

715 
by (unfold Union_def) blast 

716 

717 
lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C" 

718 
 {* The order of the premises presupposes that @{term C} is rigid; 

719 
@{term A} may be flexible. *} 

720 
by auto 

721 

722 
lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R" 

723 
by (unfold Union_def) blast 

724 

725 

726 
subsubsection {* Inter *} 

727 

728 
lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)" 

729 
by (unfold Inter_def) blast 

730 

731 
lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" 

732 
by (simp add: Inter_def) 

733 

734 
text {* 

735 
\medskip A ``destruct'' rule  every @{term X} in @{term C} 

736 
contains @{term A} as an element, but @{prop "A:X"} can hold when 

737 
@{prop "X:C"} does not! This rule is analogous to @{text spec}. 

738 
*} 

739 

740 
lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" 

741 
by auto 

742 

743 
lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" 

744 
 {* ``Classical'' elimination rule  does not require proving 

745 
@{prop "X:C"}. *} 

746 
by (unfold Inter_def) blast 

747 

748 
text {* 

749 
\medskip Image of a set under a function. Frequently @{term b} does 

750 
not have the syntactic form of @{term "f x"}. 

751 
*} 

752 

753 
lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A" 

754 
by (unfold image_def) blast 

755 

756 
lemma imageI: "x : A ==> f x : f ` A" 

757 
by (rule image_eqI) (rule refl) 

758 

759 
lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A" 

760 
 {* This version's more effective when we already have the 

761 
required @{term x}. *} 

762 
by (unfold image_def) blast 

763 

764 
lemma imageE [elim!]: 

765 
"b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P" 

766 
 {* The etaexpansion gives variablename preservation. *} 

767 
by (unfold image_def) blast 

768 

769 
lemma image_Un: "f`(A Un B) = f`A Un f`B" 

770 
by blast 

771 

772 
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)" 

773 
by blast 

774 

775 
lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)" 

776 
 {* This rewrite rule would confuse users if made default. *} 

777 
by blast 

778 

779 
lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)" 

780 
apply safe 

781 
prefer 2 apply fast 

782 
apply (rule_tac x = "{a. a : A & f a : B}" in exI) 

783 
apply fast 

784 
done 

785 

786 
lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B" 

787 
 {* Replaces the three steps @{text subsetI}, @{text imageE}, 

788 
@{text hypsubst}, but breaks too many existing proofs. *} 

789 
by blast 

790 

791 
text {* 

792 
\medskip Range of a function  just a translation for image! 

793 
*} 

794 

795 
lemma range_eqI: "b = f x ==> b : range f" 

796 
by simp 

797 

798 
lemma rangeI: "f x : range f" 

799 
by simp 

800 

801 
lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P" 

802 
by blast 

803 

804 

805 
subsubsection {* Set reasoning tools *} 

806 

807 
text {* 

808 
Rewrite rules for boolean casesplitting: faster than @{text 

809 
"split_if [split]"}. 

810 
*} 

811 

812 
lemma split_if_eq1: "((if Q then x else y) = b) = ((Q > x = b) & (~ Q > y = b))" 

813 
by (rule split_if) 

814 

815 
lemma split_if_eq2: "(a = (if Q then x else y)) = ((Q > a = x) & (~ Q > a = y))" 

816 
by (rule split_if) 

817 

818 
text {* 

819 
Split ifs on either side of the membership relation. Not for @{text 

820 
"[simp]"}  can cause goals to blow up! 

821 
*} 

822 

823 
lemma split_if_mem1: "((if Q then x else y) : b) = ((Q > x : b) & (~ Q > y : b))" 

824 
by (rule split_if) 

825 

826 
lemma split_if_mem2: "(a : (if Q then x else y)) = ((Q > a : x) & (~ Q > a : y))" 

827 
by (rule split_if) 

828 

829 
lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 

830 

831 
lemmas mem_simps = 

832 
insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff 

833 
mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff 

834 
 {* Each of these has ALREADY been added @{text "[simp]"} above. *} 

835 

836 
(*Would like to add these, but the existing code only searches for the 

837 
outerlevel constant, which in this case is just "op :"; we instead need 

838 
to use termnets to associate patterns with rules. Also, if a rule fails to 

839 
apply, then the formula should be kept. 

840 
[("uminus", Compl_iff RS iffD1), ("op ", [Diff_iff RS iffD1]), 

841 
("op Int", [IntD1,IntD2]), 

842 
("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] 

843 
*) 

844 

845 
ML_setup {* 

846 
val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs; 

847 
simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs); 

848 
*} 

849 

850 
declare subset_UNIV [simp] subset_refl [simp] 

851 

852 

853 
subsubsection {* The ``proper subset'' relation *} 

854 

855 
lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B" 

856 
by (unfold psubset_def) blast 

857 

858 
lemma psubset_insert_iff: 

859 
"(A < insert x B) = (if x:B then A < B else if x:A then A  {x} < B else A <= B)" 

860 
apply (simp add: psubset_def subset_insert_iff) 

861 
apply blast 

862 
done 

863 

864 
lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)" 

865 
by (simp only: psubset_def) 

866 

867 
lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B" 

868 
by (simp add: psubset_eq) 

869 

870 
lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C" 

871 
by (auto simp add: psubset_eq) 

872 

873 
lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C" 

874 
by (auto simp add: psubset_eq) 

875 

876 
lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B  A)" 

877 
by (unfold psubset_def) blast 

878 

879 
lemma atomize_ball: 

880 
"(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)" 

881 
by (simp only: Ball_def atomize_all atomize_imp) 

882 

883 
declare atomize_ball [symmetric, rulify] 

884 

885 

886 
subsection {* Further settheory lemmas *} 

887 

888 
use "subset.ML" 

889 
use "equalities.ML" 

890 
use "mono.ML" 

891 

11982
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

892 
lemma Least_mono: 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

893 
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

894 
==> (LEAST y. y : f ` S) = f (LEAST x. x : S)" 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

895 
 {* Courtesy of Stephan Merz *} 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

896 
apply clarify 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

897 
apply (erule_tac P = "%x. x : S" in LeastI2) 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

898 
apply fast 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

899 
apply (rule LeastI2) 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

900 
apply (auto elim: monoD intro!: order_antisym) 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

901 
done 
65e2822d83dd
lemma Least_mono moved from Typedef.thy to Set.thy;
wenzelm
parents:
11979
diff
changeset

902 

12020  903 

12257  904 
subsection {* Inverse image of a function *} 
905 

906 
constdefs 

907 
vimage :: "('a => 'b) => 'b set => 'a set" (infixr "`" 90) 

908 
"f ` B == {x. f x : B}" 

909 

910 

911 
subsubsection {* Basic rules *} 

912 

913 
lemma vimage_eq [simp]: "(a : f ` B) = (f a : B)" 

914 
by (unfold vimage_def) blast 

915 

916 
lemma vimage_singleton_eq: "(a : f ` {b}) = (f a = b)" 

917 
by simp 

918 

919 
lemma vimageI [intro]: "f a = b ==> b:B ==> a : f ` B" 

920 
by (unfold vimage_def) blast 

921 

922 
lemma vimageI2: "f a : A ==> a : f ` A" 

923 
by (unfold vimage_def) fast 

924 

925 
lemma vimageE [elim!]: "a: f ` B ==> (!!x. f a = x ==> x:B ==> P) ==> P" 

926 
by (unfold vimage_def) blast 

927 

928 
lemma vimageD: "a : f ` A ==> f a : A" 

929 
by (unfold vimage_def) fast 

930 

931 

932 
subsubsection {* Equations *} 

933 

934 
lemma vimage_empty [simp]: "f ` {} = {}" 

935 
by blast 

936 

937 
lemma vimage_Compl: "f ` (A) = (f ` A)" 

938 
by blast 

939 

940 
lemma vimage_Un [simp]: "f ` (A Un B) = (f ` A) Un (f ` B)" 

941 
by blast 

942 

943 
lemma vimage_Int [simp]: "f ` (A Int B) = (f ` A) Int (f ` B)" 

944 
by fast 

945 

946 
lemma vimage_Union: "f ` (Union A) = (UN X:A. f ` X)" 

947 
by blast 

948 

949 
lemma vimage_UN: "f`(UN x:A. B x) = (UN x:A. f ` B x)" 

950 
by blast 

951 

952 
lemma vimage_INT: "f`(INT x:A. B x) = (INT x:A. f ` B x)" 

953 
by blast 

954 

955 
lemma vimage_Collect_eq [simp]: "f ` Collect P = {y. P (f y)}" 

956 
by blast 

957 

958 
lemma vimage_Collect: "(!!x. P (f x) = Q x) ==> f ` (Collect P) = Collect Q" 

959 
by blast 

960 

961 
lemma vimage_insert: "f`(insert a B) = (f`{a}) Un (f`B)" 

962 
 {* NOT suitable for rewriting because of the recurrence of @{term "{a}"}. *} 

963 
by blast 

964 

965 
lemma vimage_Diff: "f ` (A  B) = (f ` A)  (f ` B)" 

966 
by blast 

967 

968 
lemma vimage_UNIV [simp]: "f ` UNIV = UNIV" 

969 
by blast 

970 

971 
lemma vimage_eq_UN: "f`B = (UN y: B. f`{y})" 

972 
 {* NOT suitable for rewriting *} 

973 
by blast 

974 

975 
lemma vimage_mono: "A <= B ==> f ` A <= f ` B" 

976 
 {* monotonicity *} 

977 
by blast 

978 

979 

12023  980 
subsection {* Transitivity rules for calculational reasoning *} 
12020  981 

982 
lemma forw_subst: "a = b ==> P b ==> P a" 

983 
by (rule ssubst) 

984 

985 
lemma back_subst: "P a ==> a = b ==> P b" 

986 
by (rule subst) 

987 

988 
lemma set_rev_mp: "x:A ==> A <= B ==> x:B" 

989 
by (rule subsetD) 

990 

991 
lemma set_mp: "A <= B ==> x:A ==> x:B" 

992 
by (rule subsetD) 

993 

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

995 
by (simp add: order_less_le) 

996 

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

998 
by (simp add: order_less_le) 

999 

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

1001 
by (rule order_less_asym) 

1002 

1003 
lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c" 

1004 
by (rule subst) 

1005 

1006 
lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c" 

1007 
by (rule ssubst) 

1008 

1009 
lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c" 

1010 
by (rule subst) 

1011 

1012 
lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c" 

1013 
by (rule ssubst) 

1014 

1015 
lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==> 

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

1017 
proof  

1018 
assume r: "!!x y. x < y ==> f x < f y" 

1019 
assume "a < b" hence "f a < f b" by (rule r) 

1020 
also assume "f b < c" 

1021 
finally (order_less_trans) show ?thesis . 

1022 
qed 

1023 

1024 
lemma order_less_subst1: "(a::'a::order) < f b ==> (b::'b::order) < c ==> 

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

1026 
proof  

1027 
assume r: "!!x y. x < y ==> f x < f y" 

1028 
assume "a < f b" 

1029 
also assume "b < c" hence "f b < f c" by (rule r) 

1030 
finally (order_less_trans) show ?thesis . 

1031 
qed 

1032 

1033 
lemma order_le_less_subst2: "(a::'a::order) <= b ==> f b < (c::'c::order) ==> 

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

1035 
proof  

1036 
assume r: "!!x y. x <= y ==> f x <= f y" 

1037 
assume "a <= b" hence "f a <= f b" by (rule r) 

1038 
also assume "f b < c" 

1039 
finally (order_le_less_trans) show ?thesis . 

1040 
qed 

1041 

1042 
lemma order_le_less_subst1: "(a::'a::order) <= f b ==> (b::'b::order) < c ==> 

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

1044 
proof  

1045 
assume r: "!!x y. x < y ==> f x < f y" 

1046 
assume "a <= f b" 

1047 
also assume "b < c" hence "f b < f c" by (rule r) 

1048 
finally (order_le_less_trans) show ?thesis . 

1049 
qed 

1050 

1051 
lemma order_less_le_subst2: "(a::'a::order) < b ==> f b <= (c::'c::order) ==> 

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

1053 
proof  

1054 
assume r: "!!x y. x < y ==> f x < f y" 

1055 
assume "a < b" hence "f a < f b" by (rule r) 

1056 
also assume "f b <= c" 

1057 
finally (order_less_le_trans) show ?thesis . 

1058 
qed 

1059 

1060 
lemma order_less_le_subst1: "(a::'a::order) < f b ==> (b::'b::order) <= c ==> 

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

1062 
proof  

1063 
assume r: "!!x y. x <= y ==> f x <= f y" 

1064 
assume "a < f b" 

1065 
also assume "b <= c" hence "f b <= f c" by (rule r) 

1066 
finally (order_less_le_trans) show ?thesis . 

1067 
qed 

1068 

1069 
lemma order_subst1: "(a::'a::order) <= f b ==> (b::'b::order) <= c ==> 

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

1071 
proof  

1072 
assume r: "!!x y. x <= y ==> f x <= f y" 

1073 
assume "a <= f b" 

1074 
also assume "b <= c" hence "f b <= f c" by (rule r) 

1075 
finally (order_trans) show ?thesis . 

1076 
qed 

1077 

1078 
lemma order_subst2: "(a::'a::order) <= b ==> f b <= (c::'c::order) ==> 

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

1080 
proof  

1081 
assume r: "!!x y. x <= y ==> f x <= f y" 

1082 
assume "a <= b" hence "f a <= f b" by (rule r) 

1083 
also assume "f b <= c" 

1084 
finally (order_trans) show ?thesis . 

1085 
qed 

1086 

1087 
lemma ord_le_eq_subst: "a <= b ==> f b = c ==> 

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

1089 
proof  

1090 
assume r: "!!x y. x <= y ==> f x <= f y" 

1091 
assume "a <= b" hence "f a <= f b" by (rule r) 

1092 
also assume "f b = c" 

1093 
finally (ord_le_eq_trans) show ?thesis . 

1094 
qed 

1095 

1096 
lemma ord_eq_le_subst: "a = f b ==> b <= c ==> 

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

1098 
proof  

1099 
assume r: "!!x y. x <= y ==> f x <= f y" 

1100 
assume "a = f b" 

1101 
also assume "b <= c" hence "f b <= f c" by (rule r) 

1102 
finally (ord_eq_le_trans) show ?thesis . 

1103 
qed 

1104 

1105 
lemma ord_less_eq_subst: "a < b ==> f b = c ==> 

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

1107 
proof  

1108 
assume r: "!!x y. x < y ==> f x < f y" 

1109 
assume "a < b" hence "f a < f b" by (rule r) 

1110 
also assume "f b = c" 

1111 
finally (ord_less_eq_trans) show ?thesis . 

1112 
qed 

1113 

1114 
lemma ord_eq_less_subst: "a = f b ==> b < c ==> 

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

1116 
proof  

1117 
assume r: "!!x y. x < y ==> f x < f y" 

1118 
assume "a = f b" 

1119 
also assume "b < c" hence "f b < f c" by (rule r) 

1120 
finally (ord_eq_less_trans) show ?thesis . 

1121 
qed 

1122 

1123 
text {* 

1124 
Note that this list of rules is in reverse order of priorities. 

1125 
*} 

1126 

1127 
lemmas basic_trans_rules [trans] = 

1128 
order_less_subst2 

1129 
order_less_subst1 

1130 
order_le_less_subst2 

1131 
order_le_less_subst1 

1132 
order_less_le_subst2 

1133 
order_less_le_subst1 

1134 
order_subst2 

1135 
order_subst1 

1136 
ord_le_eq_subst 

1137 
ord_eq_le_subst 

1138 
ord_less_eq_subst 

1139 
ord_eq_less_subst 

1140 
forw_subst 

1141 
back_subst 

1142 
rev_mp 

1143 
mp 

1144 
set_rev_mp 

1145 
set_mp 

1146 
order_neq_le_trans 

1147 
order_le_neq_trans 

1148 
order_less_trans 

1149 
order_less_asym' 

1150 
order_le_less_trans 

1151 
order_less_le_trans 

1152 
order_trans 

1153 
order_antisym 

1154 
ord_le_eq_trans 

1155 
ord_eq_le_trans 

1156 
ord_less_eq_trans 

1157 
ord_eq_less_trans 

1158 
trans 

1159 

11979  1160 
end 