author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8913  0bc13d5e60b8 
child 9041  3730ae0f513a 
permissions  rwrr 
1465  1 
(* Title: HOL/set 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1991 University of Cambridge 
5 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1937
diff
changeset

6 
Set theory for higherorder logic. A set is simply a predicate. 
923  7 
*) 
8 

1548  9 
section "Relating predicates and sets"; 
10 

3469
61d927bd57ec
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
paulson
parents:
3420
diff
changeset

11 
Addsimps [Collect_mem_eq]; 
61d927bd57ec
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
paulson
parents:
3420
diff
changeset

12 
AddIffs [mem_Collect_eq]; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

13 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

14 
Goal "P(a) ==> a : {x. P(x)}"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

15 
by (Asm_simp_tac 1); 
923  16 
qed "CollectI"; 
17 

5316  18 
Goal "a : {x. P(x)} ==> P(a)"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

19 
by (Asm_full_simp_tac 1); 
923  20 
qed "CollectD"; 
21 

7658  22 
bind_thm ("CollectE", make_elim CollectD); 
23 

5316  24 
val [prem] = Goal "[ !!x. (x:A) = (x:B) ] ==> A = B"; 
923  25 
by (rtac (prem RS ext RS arg_cong RS box_equals) 1); 
26 
by (rtac Collect_mem_eq 1); 

27 
by (rtac Collect_mem_eq 1); 

28 
qed "set_ext"; 

29 

5316  30 
val [prem] = Goal "[ !!x. P(x)=Q(x) ] ==> {x. P(x)} = {x. Q(x)}"; 
923  31 
by (rtac (prem RS ext RS arg_cong) 1); 
32 
qed "Collect_cong"; 

33 

34 
val CollectE = make_elim CollectD; 

35 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

36 
AddSIs [CollectI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

37 
AddSEs [CollectE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

38 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

39 

1548  40 
section "Bounded quantifiers"; 
923  41 

5316  42 
val prems = Goalw [Ball_def] 
923  43 
"[ !!x. x:A ==> P(x) ] ==> ! x:A. P(x)"; 
44 
by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); 

45 
qed "ballI"; 

46 

8839  47 
bind_thms ("strip", [impI, allI, ballI]); 
48 

5316  49 
Goalw [Ball_def] "[ ! x:A. P(x); x:A ] ==> P(x)"; 
50 
by (Blast_tac 1); 

923  51 
qed "bspec"; 
52 

5316  53 
val major::prems = Goalw [Ball_def] 
923  54 
"[ ! x:A. P(x); P(x) ==> Q; x~:A ==> Q ] ==> Q"; 
55 
by (rtac (major RS spec RS impCE) 1); 

56 
by (REPEAT (eresolve_tac prems 1)); 

57 
qed "ballE"; 

58 

59 
(*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*) 

60 
fun ball_tac i = etac ballE i THEN contr_tac (i+1); 

61 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

62 
AddSIs [ballI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

63 
AddEs [ballE]; 
7441  64 
AddXDs [bspec]; 
5521  65 
(* gives better instantiation for bound: *) 
66 
claset_ref() := claset() addWrapper ("bspec", fn tac2 => 

67 
(dtac bspec THEN' atac) APPEND' tac2); 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

68 

6006  69 
(*Normally the best argument order: P(x) constrains the choice of x:A*) 
5316  70 
Goalw [Bex_def] "[ P(x); x:A ] ==> ? x:A. P(x)"; 
71 
by (Blast_tac 1); 

923  72 
qed "bexI"; 
73 

6006  74 
(*The best argument order when there is only one x:A*) 
75 
Goalw [Bex_def] "[ x:A; P(x) ] ==> ? x:A. P(x)"; 

76 
by (Blast_tac 1); 

77 
qed "rev_bexI"; 

78 

7031  79 
val prems = Goal 
7007  80 
"[ ! x:A. ~P(x) ==> P(a); a:A ] ==> ? x:A. P(x)"; 
81 
by (rtac classical 1); 

82 
by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ; 

83 
qed "bexCI"; 

923  84 

5316  85 
val major::prems = Goalw [Bex_def] 
923  86 
"[ ? x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q"; 
87 
by (rtac (major RS exE) 1); 

88 
by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); 

89 
qed "bexE"; 

90 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

91 
AddIs [bexI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

92 
AddSEs [bexE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

93 

3420  94 
(*Trival rewrite rule*) 
5069  95 
Goal "(! x:A. P) = ((? x. x:A) > P)"; 
4089  96 
by (simp_tac (simpset() addsimps [Ball_def]) 1); 
3420  97 
qed "ball_triv"; 
1816  98 

1882  99 
(*Dual form for existentials*) 
5069  100 
Goal "(? x:A. P) = ((? x. x:A) & P)"; 
4089  101 
by (simp_tac (simpset() addsimps [Bex_def]) 1); 
3420  102 
qed "bex_triv"; 
1882  103 

3420  104 
Addsimps [ball_triv, bex_triv]; 
923  105 

106 
(** Congruence rules **) 

107 

6291  108 
val prems = Goalw [Ball_def] 
923  109 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 
110 
\ (! x:A. P(x)) = (! x:B. Q(x))"; 

6291  111 
by (asm_simp_tac (simpset() addsimps prems) 1); 
923  112 
qed "ball_cong"; 
113 

6291  114 
val prems = Goalw [Bex_def] 
923  115 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 
116 
\ (? x:A. P(x)) = (? x:B. Q(x))"; 

6291  117 
by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps prems) 1); 
923  118 
qed "bex_cong"; 
119 

6291  120 
Addcongs [ball_cong,bex_cong]; 
121 

1548  122 
section "Subsets"; 
923  123 

5316  124 
val prems = Goalw [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; 
923  125 
by (REPEAT (ares_tac (prems @ [ballI]) 1)); 
126 
qed "subsetI"; 

127 

5649  128 
(*Map the type ('a set => anything) to just 'a. 
129 
For overloading constants whose first argument has type "'a set" *) 

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

131 

4059  132 
(*While (:) is not, its type must be kept 
133 
for overloading of = to work.*) 

4240
8ba60a4cd380
Renamed "overload" to "overloaded" for sml/nj compatibility
paulson
parents:
4231
diff
changeset

134 
Blast.overloaded ("op :", domain_type); 
5649  135 

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

137 
overload_1st_set "Bex"; 

4059  138 

4469  139 
(*Image: retain the type of the set being expressed*) 
8005  140 
Blast.overloaded ("image", domain_type); 
2881  141 

923  142 
(*Rule in Modus Ponens style*) 
5316  143 
Goalw [subset_def] "[ A <= B; c:A ] ==> c:B"; 
144 
by (Blast_tac 1); 

923  145 
qed "subsetD"; 
7658  146 
AddXIs [subsetD]; 
923  147 

148 
(*The same, with reversed premises for use with etac  cf rev_mp*) 

7007  149 
Goal "[ c:A; A <= B ] ==> c:B"; 
150 
by (REPEAT (ares_tac [subsetD] 1)) ; 

151 
qed "rev_subsetD"; 

7658  152 
AddXIs [rev_subsetD]; 
923  153 

1920  154 
(*Converts A<=B to x:A ==> x:B*) 
155 
fun impOfSubs th = th RSN (2, rev_subsetD); 

156 

7007  157 
Goal "[ A <= B; c ~: B ] ==> c ~: A"; 
158 
by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ; 

159 
qed "contra_subsetD"; 

1841  160 

7007  161 
Goal "[ c ~: B; A <= B ] ==> c ~: A"; 
162 
by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ; 

163 
qed "rev_contra_subsetD"; 

1841  164 

923  165 
(*Classical elimination rule*) 
5316  166 
val major::prems = Goalw [subset_def] 
923  167 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P"; 
168 
by (rtac (major RS ballE) 1); 

169 
by (REPEAT (eresolve_tac prems 1)); 

170 
qed "subsetCE"; 

171 

172 
(*Takes assumptions A<=B; c:A and creates the assumption c:B *) 

173 
fun set_mp_tac i = etac subsetCE i THEN mp_tac i; 

174 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

175 
AddSIs [subsetI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

176 
AddEs [subsetD, subsetCE]; 
923  177 

7007  178 
Goal "A <= (A::'a set)"; 
179 
by (Fast_tac 1); 

180 
qed "subset_refl"; (*Blast_tac would try order_refl and fail*) 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

181 

5316  182 
Goal "[ A<=B; B<=C ] ==> A<=(C::'a set)"; 
2891  183 
by (Blast_tac 1); 
923  184 
qed "subset_trans"; 
185 

186 

1548  187 
section "Equality"; 
923  188 

189 
(*Antisymmetry of the subset relation*) 

5316  190 
Goal "[ A <= B; B <= A ] ==> A = (B::'a set)"; 
5318  191 
by (rtac set_ext 1); 
5316  192 
by (blast_tac (claset() addIs [subsetD]) 1); 
923  193 
qed "subset_antisym"; 
194 
val equalityI = subset_antisym; 

195 

1762  196 
AddSIs [equalityI]; 
197 

923  198 
(* Equality rules from ZF set theory  are they appropriate here? *) 
5316  199 
Goal "A = B ==> A<=(B::'a set)"; 
200 
by (etac ssubst 1); 

923  201 
by (rtac subset_refl 1); 
202 
qed "equalityD1"; 

203 

5316  204 
Goal "A = B ==> B<=(A::'a set)"; 
205 
by (etac ssubst 1); 

923  206 
by (rtac subset_refl 1); 
207 
qed "equalityD2"; 

208 

5316  209 
val prems = Goal 
923  210 
"[ A = B; [ A<=B; B<=(A::'a set) ] ==> P ] ==> P"; 
211 
by (resolve_tac prems 1); 

212 
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); 

213 
qed "equalityE"; 

214 

5316  215 
val major::prems = Goal 
923  216 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P"; 
217 
by (rtac (major RS equalityE) 1); 

218 
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); 

219 
qed "equalityCE"; 

220 

221 
(*Lemma for creating induction formulae  for "pattern matching" on p 

222 
To make the induction hypotheses usable, apply "spec" or "bspec" to 

223 
put universal quantifiers over the free variables in p. *) 

5316  224 
val prems = Goal 
923  225 
"[ p:A; !!z. z:A ==> p=z > R ] ==> R"; 
226 
by (rtac mp 1); 

227 
by (REPEAT (resolve_tac (refl::prems) 1)); 

228 
qed "setup_induction"; 

229 

8053  230 
Goal "A = B ==> (x : A) = (x : B)"; 
231 
by (Asm_simp_tac 1); 

232 
qed "eqset_imp_iff"; 

233 

923  234 

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

235 
section "The universal set  UNIV"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

236 

7031  237 
Goalw [UNIV_def] "x : UNIV"; 
238 
by (rtac CollectI 1); 

239 
by (rtac TrueI 1); 

240 
qed "UNIV_I"; 

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

241 

4434  242 
Addsimps [UNIV_I]; 
243 
AddIs [UNIV_I]; (*unsafe makes it less likely to cause problems*) 

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

244 

7031  245 
Goal "A <= UNIV"; 
246 
by (rtac subsetI 1); 

247 
by (rtac UNIV_I 1); 

248 
qed "subset_UNIV"; 

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

249 

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

250 
(** Etacontracting these two rules (to remove P) causes them to be ignored 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

251 
because of their interaction with congruence rules. **) 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

252 

5069  253 
Goalw [Ball_def] "Ball UNIV P = All P"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

254 
by (Simp_tac 1); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

255 
qed "ball_UNIV"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

256 

5069  257 
Goalw [Bex_def] "Bex UNIV P = Ex P"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

258 
by (Simp_tac 1); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

259 
qed "bex_UNIV"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

260 
Addsimps [ball_UNIV, bex_UNIV]; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

261 

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

262 

2858  263 
section "The empty set  {}"; 
264 

7007  265 
Goalw [empty_def] "(c : {}) = False"; 
266 
by (Blast_tac 1) ; 

267 
qed "empty_iff"; 

2858  268 

269 
Addsimps [empty_iff]; 

270 

7007  271 
Goal "a:{} ==> P"; 
272 
by (Full_simp_tac 1); 

273 
qed "emptyE"; 

2858  274 

275 
AddSEs [emptyE]; 

276 

7007  277 
Goal "{} <= A"; 
278 
by (Blast_tac 1) ; 

279 
qed "empty_subsetI"; 

2858  280 

5256  281 
(*One effect is to delete the ASSUMPTION {} <= A*) 
282 
AddIffs [empty_subsetI]; 

283 

7031  284 
val [prem]= Goal "[ !!y. y:A ==> False ] ==> A={}"; 
7007  285 
by (blast_tac (claset() addIs [prem RS FalseE]) 1) ; 
286 
qed "equals0I"; 

2858  287 

5256  288 
(*Use for reasoning about disjointness: A Int B = {} *) 
7007  289 
Goal "A={} ==> a ~: A"; 
290 
by (Blast_tac 1) ; 

291 
qed "equals0D"; 

2858  292 

5450
fe9d103464a4
Changed equals0E back to equals0D and gave it the correct destruct form
paulson
parents:
5336
diff
changeset

293 
AddDs [equals0D, sym RS equals0D]; 
5256  294 

5069  295 
Goalw [Ball_def] "Ball {} P = True"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

296 
by (Simp_tac 1); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

297 
qed "ball_empty"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

298 

5069  299 
Goalw [Bex_def] "Bex {} P = False"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

300 
by (Simp_tac 1); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

301 
qed "bex_empty"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

302 
Addsimps [ball_empty, bex_empty]; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

303 

5069  304 
Goal "UNIV ~= {}"; 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

305 
by (blast_tac (claset() addEs [equalityE]) 1); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

306 
qed "UNIV_not_empty"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

307 
AddIffs [UNIV_not_empty]; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

308 

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

309 

2858  310 

311 
section "The Powerset operator  Pow"; 

312 

7007  313 
Goalw [Pow_def] "(A : Pow(B)) = (A <= B)"; 
314 
by (Asm_simp_tac 1); 

315 
qed "Pow_iff"; 

2858  316 

317 
AddIffs [Pow_iff]; 

318 

7031  319 
Goalw [Pow_def] "A <= B ==> A : Pow(B)"; 
7007  320 
by (etac CollectI 1); 
321 
qed "PowI"; 

2858  322 

7031  323 
Goalw [Pow_def] "A : Pow(B) ==> A<=B"; 
7007  324 
by (etac CollectD 1); 
325 
qed "PowD"; 

326 

2858  327 

328 
val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *) 

329 
val Pow_top = subset_refl RS PowI; (* A : Pow(A) *) 

330 

331 

5931  332 
section "Set complement"; 
923  333 

7031  334 
Goalw [Compl_def] "(c : A) = (c~:A)"; 
335 
by (Blast_tac 1); 

336 
qed "Compl_iff"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

337 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

338 
Addsimps [Compl_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

339 

5490  340 
val prems = Goalw [Compl_def] "[ c:A ==> False ] ==> c : A"; 
923  341 
by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); 
342 
qed "ComplI"; 

343 

344 
(*This form, with negated conclusion, works well with the Classical prover. 

345 
Negated assumptions behave like formulae on the right side of the notional 

346 
turnstile...*) 

5490  347 
Goalw [Compl_def] "c : A ==> c~:A"; 
5316  348 
by (etac CollectD 1); 
923  349 
qed "ComplD"; 
350 

351 
val ComplE = make_elim ComplD; 

352 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

353 
AddSIs [ComplI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

354 
AddSEs [ComplE]; 
1640  355 

923  356 

1548  357 
section "Binary union  Un"; 
923  358 

7031  359 
Goalw [Un_def] "(c : A Un B) = (c:A  c:B)"; 
360 
by (Blast_tac 1); 

361 
qed "Un_iff"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

362 
Addsimps [Un_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

363 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

364 
Goal "c:A ==> c : A Un B"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

365 
by (Asm_simp_tac 1); 
923  366 
qed "UnI1"; 
367 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

368 
Goal "c:B ==> c : A Un B"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

369 
by (Asm_simp_tac 1); 
923  370 
qed "UnI2"; 
371 

372 
(*Classical introduction rule: no commitment to A vs B*) 

7007  373 

7031  374 
val prems = Goal "(c~:B ==> c:A) ==> c : A Un B"; 
7007  375 
by (Simp_tac 1); 
376 
by (REPEAT (ares_tac (prems@[disjCI]) 1)) ; 

377 
qed "UnCI"; 

923  378 

5316  379 
val major::prems = Goalw [Un_def] 
923  380 
"[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P"; 
381 
by (rtac (major RS CollectD RS disjE) 1); 

382 
by (REPEAT (eresolve_tac prems 1)); 

383 
qed "UnE"; 

384 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

385 
AddSIs [UnCI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

386 
AddSEs [UnE]; 
1640  387 

923  388 

1548  389 
section "Binary intersection  Int"; 
923  390 

7031  391 
Goalw [Int_def] "(c : A Int B) = (c:A & c:B)"; 
392 
by (Blast_tac 1); 

393 
qed "Int_iff"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

394 
Addsimps [Int_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

395 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

396 
Goal "[ c:A; c:B ] ==> c : A Int B"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

397 
by (Asm_simp_tac 1); 
923  398 
qed "IntI"; 
399 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

400 
Goal "c : A Int B ==> c:A"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

401 
by (Asm_full_simp_tac 1); 
923  402 
qed "IntD1"; 
403 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

404 
Goal "c : A Int B ==> c:B"; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

405 
by (Asm_full_simp_tac 1); 
923  406 
qed "IntD2"; 
407 

5316  408 
val [major,minor] = Goal 
923  409 
"[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P"; 
410 
by (rtac minor 1); 

411 
by (rtac (major RS IntD1) 1); 

412 
by (rtac (major RS IntD2) 1); 

413 
qed "IntE"; 

414 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

415 
AddSIs [IntI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

416 
AddSEs [IntE]; 
923  417 

1548  418 
section "Set difference"; 
923  419 

7031  420 
Goalw [set_diff_def] "(c : AB) = (c:A & c~:B)"; 
421 
by (Blast_tac 1); 

422 
qed "Diff_iff"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

423 
Addsimps [Diff_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

424 

7007  425 
Goal "[ c : A; c ~: B ] ==> c : A  B"; 
426 
by (Asm_simp_tac 1) ; 

427 
qed "DiffI"; 

923  428 

7007  429 
Goal "c : A  B ==> c : A"; 
430 
by (Asm_full_simp_tac 1) ; 

431 
qed "DiffD1"; 

923  432 

7007  433 
Goal "[ c : A  B; c : B ] ==> P"; 
434 
by (Asm_full_simp_tac 1) ; 

435 
qed "DiffD2"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

436 

7031  437 
val prems = Goal "[ c : A  B; [ c:A; c~:B ] ==> P ] ==> P"; 
7007  438 
by (resolve_tac prems 1); 
439 
by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ; 

440 
qed "DiffE"; 

923  441 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

442 
AddSIs [DiffI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

443 
AddSEs [DiffE]; 
923  444 

445 

1548  446 
section "Augmenting a set  insert"; 
923  447 

7031  448 
Goalw [insert_def] "a : insert b A = (a=b  a:A)"; 
449 
by (Blast_tac 1); 

450 
qed "insert_iff"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

451 
Addsimps [insert_iff]; 
923  452 

7031  453 
Goal "a : insert a B"; 
7007  454 
by (Simp_tac 1); 
455 
qed "insertI1"; 

923  456 

7007  457 
Goal "!!a. a : B ==> a : insert b B"; 
458 
by (Asm_simp_tac 1); 

459 
qed "insertI2"; 

460 

461 
val major::prems = Goalw [insert_def] 

462 
"[ a : insert b A; a=b ==> P; a:A ==> P ] ==> P"; 

463 
by (rtac (major RS UnE) 1); 

464 
by (REPEAT (eresolve_tac (prems @ [CollectE]) 1)); 

465 
qed "insertE"; 

923  466 

467 
(*Classical introduction rule*) 

7031  468 
val prems = Goal "(a~:B ==> a=b) ==> a: insert b B"; 
7007  469 
by (Simp_tac 1); 
470 
by (REPEAT (ares_tac (prems@[disjCI]) 1)) ; 

471 
qed "insertCI"; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

472 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

473 
AddSIs [insertCI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

474 
AddSEs [insertE]; 
923  475 

7496
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

476 
Goal "A <= insert x B ==> A <= B & x ~: A  (? B'. A = insert x B' & B' <= B)"; 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

477 
by (case_tac "x:A" 1); 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

478 
by (Fast_tac 2); 
7499  479 
by (rtac disjI2 1); 
7496
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

480 
by (res_inst_tac [("x","A{x}")] exI 1); 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

481 
by (Fast_tac 1); 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

482 
qed "subset_insertD"; 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

483 

1548  484 
section "Singletons, using insert"; 
923  485 

7007  486 
Goal "a : {a}"; 
487 
by (rtac insertI1 1) ; 

488 
qed "singletonI"; 

923  489 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

490 
Goal "b : {a} ==> b=a"; 
2891  491 
by (Blast_tac 1); 
923  492 
qed "singletonD"; 
493 

1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

494 
bind_thm ("singletonE", make_elim singletonD); 
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

495 

7007  496 
Goal "(b : {a}) = (b=a)"; 
497 
by (Blast_tac 1); 

498 
qed "singleton_iff"; 

923  499 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

500 
Goal "{a}={b} ==> a=b"; 
4089  501 
by (blast_tac (claset() addEs [equalityE]) 1); 
923  502 
qed "singleton_inject"; 
503 

2858  504 
(*Redundant? But unlike insertCI, it proves the subgoal immediately!*) 
505 
AddSIs [singletonI]; 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

506 
AddSDs [singleton_inject]; 
3718  507 
AddSEs [singletonE]; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

508 

7969  509 
Goal "{b} = insert a A = (a = b & A <= {b})"; 
8326
0e329578b0ef
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
paulson
parents:
8053
diff
changeset

510 
by (blast_tac (claset() addSEs [equalityE]) 1); 
7496
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

511 
qed "singleton_insert_inj_eq"; 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

512 

8326
0e329578b0ef
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
paulson
parents:
8053
diff
changeset

513 
Goal "(insert a A = {b}) = (a = b & A <= {b})"; 
0e329578b0ef
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
paulson
parents:
8053
diff
changeset

514 
by (blast_tac (claset() addSEs [equalityE]) 1); 
7969  515 
qed "singleton_insert_inj_eq'"; 
516 

8326
0e329578b0ef
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
paulson
parents:
8053
diff
changeset

517 
AddIffs [singleton_insert_inj_eq, singleton_insert_inj_eq']; 
0e329578b0ef
tidied the proofs of singleton_insert_inj_eq, singleton_insert_inj_eq' and
paulson
parents:
8053
diff
changeset

518 

7496
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

519 
Goal "A <= {x} ==> A={}  A = {x}"; 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

520 
by (Fast_tac 1); 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

521 
qed "subset_singletonD"; 
93ae11d887ff
added theorems subset_insertD, singleton_insert_inj_eq, subset_singletonD
oheimb
parents:
7441
diff
changeset

522 

5069  523 
Goal "{x. x=a} = {a}"; 
4423  524 
by (Blast_tac 1); 
3582  525 
qed "singleton_conv"; 
526 
Addsimps [singleton_conv]; 

1531  527 

5600  528 
Goal "{x. a=x} = {a}"; 
6301  529 
by (Blast_tac 1); 
5600  530 
qed "singleton_conv2"; 
531 
Addsimps [singleton_conv2]; 

532 

1531  533 

1548  534 
section "Unions of families  UNION x:A. B(x) is Union(B``A)"; 
923  535 

5069  536 
Goalw [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))"; 
2891  537 
by (Blast_tac 1); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

538 
qed "UN_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

539 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

540 
Addsimps [UN_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

541 

923  542 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

543 
Goal "[ a:A; b: B(a) ] ==> b: (UN x:A. B(x))"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4469
diff
changeset

544 
by Auto_tac; 
923  545 
qed "UN_I"; 
546 

5316  547 
val major::prems = Goalw [UNION_def] 
923  548 
"[ b : (UN x:A. B(x)); !!x.[ x:A; b: B(x) ] ==> R ] ==> R"; 
549 
by (rtac (major RS CollectD RS bexE) 1); 

550 
by (REPEAT (ares_tac prems 1)); 

551 
qed "UN_E"; 

552 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

553 
AddIs [UN_I]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

554 
AddSEs [UN_E]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

555 

6291  556 
val prems = Goalw [UNION_def] 
923  557 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 
558 
\ (UN x:A. C(x)) = (UN x:B. D(x))"; 

6291  559 
by (asm_simp_tac (simpset() addsimps prems) 1); 
923  560 
qed "UN_cong"; 
561 

562 

1548  563 
section "Intersections of families  INTER x:A. B(x) is Inter(B``A)"; 
923  564 

5069  565 
Goalw [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4469
diff
changeset

566 
by Auto_tac; 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

567 
qed "INT_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

568 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

569 
Addsimps [INT_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

570 

5316  571 
val prems = Goalw [INTER_def] 
923  572 
"(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; 
573 
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); 

574 
qed "INT_I"; 

575 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

576 
Goal "[ b : (INT x:A. B(x)); a:A ] ==> b: B(a)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4469
diff
changeset

577 
by Auto_tac; 
923  578 
qed "INT_D"; 
579 

580 
(*"Classical" elimination  by the Excluded Middle on a:A *) 

5316  581 
val major::prems = Goalw [INTER_def] 
923  582 
"[ b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R ] ==> R"; 
583 
by (rtac (major RS CollectD RS ballE) 1); 

584 
by (REPEAT (eresolve_tac prems 1)); 

585 
qed "INT_E"; 

586 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

587 
AddSIs [INT_I]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

588 
AddEs [INT_D, INT_E]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

589 

6291  590 
val prems = Goalw [INTER_def] 
923  591 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 
592 
\ (INT x:A. C(x)) = (INT x:B. D(x))"; 

6291  593 
by (asm_simp_tac (simpset() addsimps prems) 1); 
923  594 
qed "INT_cong"; 
595 

596 

1548  597 
section "Union"; 
923  598 

5069  599 
Goalw [Union_def] "(A : Union(C)) = (EX X:C. A:X)"; 
2891  600 
by (Blast_tac 1); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

601 
qed "Union_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

602 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

603 
Addsimps [Union_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

604 

923  605 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

606 
Goal "[ X:C; A:X ] ==> A : Union(C)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4469
diff
changeset

607 
by Auto_tac; 
923  608 
qed "UnionI"; 
609 

5316  610 
val major::prems = Goalw [Union_def] 
923  611 
"[ A : Union(C); !!X.[ A:X; X:C ] ==> R ] ==> R"; 
612 
by (rtac (major RS UN_E) 1); 

613 
by (REPEAT (ares_tac prems 1)); 

614 
qed "UnionE"; 

615 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

616 
AddIs [UnionI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

617 
AddSEs [UnionE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

618 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

619 

1548  620 
section "Inter"; 
923  621 

5069  622 
Goalw [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)"; 
2891  623 
by (Blast_tac 1); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

624 
qed "Inter_iff"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

625 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

626 
Addsimps [Inter_iff]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

627 

5316  628 
val prems = Goalw [Inter_def] 
923  629 
"[ !!X. X:C ==> A:X ] ==> A : Inter(C)"; 
630 
by (REPEAT (ares_tac ([INT_I] @ prems) 1)); 

631 
qed "InterI"; 

632 

633 
(*A "destruct" rule  every X in C contains A as an element, but 

634 
A:X can hold when X:C does not! This rule is analogous to "spec". *) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

635 
Goal "[ A : Inter(C); X:C ] ==> A:X"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4469
diff
changeset

636 
by Auto_tac; 
923  637 
qed "InterD"; 
638 

639 
(*"Classical" elimination rule  does not require proving X:C *) 

5316  640 
val major::prems = Goalw [Inter_def] 
2721  641 
"[ A : Inter(C); X~:C ==> R; A:X ==> R ] ==> R"; 
923  642 
by (rtac (major RS INT_E) 1); 
643 
by (REPEAT (eresolve_tac prems 1)); 

644 
qed "InterE"; 

645 

2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

646 
AddSIs [InterI]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

647 
AddEs [InterD, InterE]; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

648 

0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

649 

2912  650 
(*** Image of a set under a function ***) 
651 

652 
(*Frequently b does not have the syntactic form of f(x).*) 

5316  653 
Goalw [image_def] "[ b=f(x); x:A ] ==> b : f``A"; 
654 
by (Blast_tac 1); 

2912  655 
qed "image_eqI"; 
3909  656 
Addsimps [image_eqI]; 
2912  657 

658 
bind_thm ("imageI", refl RS image_eqI); 

659 

8025  660 
(*This version's more effective when we already have the required x*) 
661 
Goalw [image_def] "[ x:A; b=f(x) ] ==> b : f``A"; 

662 
by (Blast_tac 1); 

663 
qed "rev_image_eqI"; 

664 

2912  665 
(*The etaexpansion gives variablename preservation.*) 
5316  666 
val major::prems = Goalw [image_def] 
3842  667 
"[ b : (%x. f(x))``A; !!x.[ b=f(x); x:A ] ==> P ] ==> P"; 
2912  668 
by (rtac (major RS CollectD RS bexE) 1); 
669 
by (REPEAT (ares_tac prems 1)); 

670 
qed "imageE"; 

671 

672 
AddIs [image_eqI]; 

673 
AddSEs [imageE]; 

674 

5069  675 
Goal "f``(A Un B) = f``A Un f``B"; 
2935  676 
by (Blast_tac 1); 
2912  677 
qed "image_Un"; 
678 

5069  679 
Goal "(z : f``A) = (EX x:A. z = f x)"; 
3960  680 
by (Blast_tac 1); 
681 
qed "image_iff"; 

682 

4523  683 
(*This rewrite rule would confuse users if made default.*) 
5069  684 
Goal "(f``A <= B) = (ALL x:A. f(x): B)"; 
4523  685 
by (Blast_tac 1); 
686 
qed "image_subset_iff"; 

687 

688 
(*Replaces the three steps subsetI, imageE, hyp_subst_tac, but breaks too 

689 
many existing proofs.*) 

5316  690 
val prems = Goal "(!!x. x:A ==> f(x) : B) ==> f``A <= B"; 
4510  691 
by (blast_tac (claset() addIs prems) 1); 
692 
qed "image_subsetI"; 

693 

2912  694 

695 
(*** Range of a function  just a translation for image! ***) 

696 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

697 
Goal "b=f(x) ==> b : range(f)"; 
2912  698 
by (EVERY1 [etac image_eqI, rtac UNIV_I]); 
699 
bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI)); 

700 

701 
bind_thm ("rangeI", UNIV_I RS imageI); 

702 

5316  703 
val [major,minor] = Goal 
3842  704 
"[ b : range(%x. f(x)); !!x. b=f(x) ==> P ] ==> P"; 
2912  705 
by (rtac (major RS imageE) 1); 
706 
by (etac minor 1); 

707 
qed "rangeE"; 

708 

1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

709 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

710 
(*** Set reasoning tools ***) 
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

711 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

712 

3912  713 
(** Rewrite rules for boolean casesplitting: faster than 
4830  714 
addsplits[split_if] 
3912  715 
**) 
716 

4830  717 
bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if); 
718 
bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if); 

3912  719 

5237  720 
(*Split ifs on either side of the membership relation. 
721 
Not for Addsimps  can cause goals to blow up!*) 

4830  722 
bind_thm ("split_if_mem1", 
6394  723 
read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if); 
4830  724 
bind_thm ("split_if_mem2", 
6394  725 
read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if); 
3912  726 

4830  727 
val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2, 
728 
split_if_mem1, split_if_mem2]; 

3912  729 

730 

4089  731 
(*Each of these has ALREADY been added to simpset() above.*) 
2024
909153d8318f
Rationalized the rewriting of membership for {} and insert
paulson
parents:
1985
diff
changeset

732 
val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
4159
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

733 
mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff]; 
1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

734 

d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

735 
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs; 
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

736 

6291  737 
simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs); 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

738 

5256  739 
Addsimps[subset_UNIV, subset_refl]; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

740 

726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

741 

8001  742 
(*** The 'proper subset' relation (<) ***) 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

743 

5069  744 
Goalw [psubset_def] "!!A::'a set. [ A <= B; A ~= B ] ==> A<B"; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

745 
by (Blast_tac 1); 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

746 
qed "psubsetI"; 
8913  747 
AddSIs [psubsetI]; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

748 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

749 
Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B  x:A & A{x}<B"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4469
diff
changeset

750 
by Auto_tac; 
3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

751 
qed "psubset_insertD"; 
4059  752 

753 
bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq); 

6443  754 

755 
bind_thm ("psubset_imp_subset", psubset_eq RS iffD1 RS conjunct1); 

756 

757 
Goal"[ (A::'a set) < B; B <= C ] ==> A < C"; 

758 
by (auto_tac (claset(), simpset() addsimps [psubset_eq])); 

759 
qed "psubset_subset_trans"; 

760 

761 
Goal"[ (A::'a set) <= B; B < C] ==> A < C"; 

762 
by (auto_tac (claset(), simpset() addsimps [psubset_eq])); 

763 
qed "subset_psubset_trans"; 

7717
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

764 

8001  765 
Goalw [psubset_def] "A < B ==> EX b. b : (B  A)"; 
766 
by (Blast_tac 1); 

767 
qed "psubset_imp_ex_mem"; 

768 

7717
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

769 

e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

770 
(* attributes *) 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

771 

e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

772 
local 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

773 

e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

774 
fun gen_rulify_prems x = 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

775 
Attrib.no_args (Drule.rule_attribute (fn _ => (standard o 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

776 
rule_by_tactic (REPEAT (ALLGOALS (resolve_tac [allI, ballI, impI])))))) x; 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

777 

e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

778 
in 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

779 

e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

780 
val rulify_prems_attrib_setup = 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

781 
[Attrib.add_attributes 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

782 
[("rulify_prems", (gen_rulify_prems, gen_rulify_prems), "put theorem into standard rule form")]]; 
e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

783 

e7ecfa617443
Added attribute rulify_prems (useful for modifying premises of introduction
berghofe
parents:
7658
diff
changeset

784 
end; 