author  paulson 
Wed, 02 Dec 1998 15:53:05 +0100  
changeset 6006  d2e271b8d651 
parent 5931  325300576da7 
child 6171  cd237a10cbf8 
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 

9 
open Set; 

10 

1548  11 
section "Relating predicates and sets"; 
12 

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

13 
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

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

15 

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

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

17 
by (Asm_simp_tac 1); 
923  18 
qed "CollectI"; 
19 

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

21 
by (Asm_full_simp_tac 1); 
923  22 
qed "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 

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

923  49 
qed "bspec"; 
50 

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

54 
by (REPEAT (eresolve_tac prems 1)); 

55 
qed "ballE"; 

56 

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

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

59 

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

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

61 
AddEs [ballE]; 
5521  62 
(* gives better instantiation for bound: *) 
63 
claset_ref() := claset() addWrapper ("bspec", fn tac2 => 

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

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

65 

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

923  69 
qed "bexI"; 
70 

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

73 
by (Blast_tac 1); 

74 
qed "rev_bexI"; 

75 

923  76 
qed_goal "bexCI" Set.thy 
5521  77 
"[ ! x:A. ~P(x) ==> P(a); a:A ] ==> ? x:A. P(x)" (fn prems => 
923  78 
[ (rtac classical 1), 
79 
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); 

80 

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

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

85 
qed "bexE"; 

86 

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

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

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

89 

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

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

3420  100 
Addsimps [ball_triv, bex_triv]; 
923  101 

102 
(** Congruence rules **) 

103 

5316  104 
val prems = Goal 
923  105 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 
106 
\ (! x:A. P(x)) = (! x:B. Q(x))"; 

107 
by (resolve_tac (prems RL [ssubst]) 1); 

108 
by (REPEAT (ares_tac [ballI,iffI] 1 

109 
ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); 

110 
qed "ball_cong"; 

111 

5316  112 
val prems = Goal 
923  113 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 
114 
\ (? x:A. P(x)) = (? x:B. Q(x))"; 

115 
by (resolve_tac (prems RL [ssubst]) 1); 

116 
by (REPEAT (etac bexE 1 

117 
ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); 

118 
qed "bex_cong"; 

119 

1548  120 
section "Subsets"; 
923  121 

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

125 

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

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

129 

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

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

132 
Blast.overloaded ("op :", domain_type); 
5649  133 

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

135 
overload_1st_set "Bex"; 

4059  136 

4469  137 
(*Image: retain the type of the set being expressed*) 
5336  138 
Blast.overloaded ("op ``", domain_type); 
2881  139 

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

923  143 
qed "subsetD"; 
144 

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

146 
qed_goal "rev_subsetD" Set.thy "[ c:A; A <= B ] ==> c:B" 

147 
(fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]); 

148 

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

151 

1841  152 
qed_goal "contra_subsetD" Set.thy "!!c. [ A <= B; c ~: B ] ==> c ~: A" 
153 
(fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); 

154 

155 
qed_goal "rev_contra_subsetD" Set.thy "!!c. [ c ~: B; A <= B ] ==> c ~: A" 

156 
(fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]); 

157 

923  158 
(*Classical elimination rule*) 
5316  159 
val major::prems = Goalw [subset_def] 
923  160 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P"; 
161 
by (rtac (major RS ballE) 1); 

162 
by (REPEAT (eresolve_tac prems 1)); 

163 
qed "subsetCE"; 

164 

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

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

167 

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

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

169 
AddEs [subsetD, subsetCE]; 
923  170 

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

171 
qed_goal "subset_refl" Set.thy "A <= (A::'a set)" 
4059  172 
(fn _=> [Fast_tac 1]); (*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

173 

5316  174 
Goal "[ A<=B; B<=C ] ==> A<=(C::'a set)"; 
2891  175 
by (Blast_tac 1); 
923  176 
qed "subset_trans"; 
177 

178 

1548  179 
section "Equality"; 
923  180 

181 
(*Antisymmetry of the subset relation*) 

5316  182 
Goal "[ A <= B; B <= A ] ==> A = (B::'a set)"; 
5318  183 
by (rtac set_ext 1); 
5316  184 
by (blast_tac (claset() addIs [subsetD]) 1); 
923  185 
qed "subset_antisym"; 
186 
val equalityI = subset_antisym; 

187 

1762  188 
AddSIs [equalityI]; 
189 

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

923  193 
by (rtac subset_refl 1); 
194 
qed "equalityD1"; 

195 

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

923  198 
by (rtac subset_refl 1); 
199 
qed "equalityD2"; 

200 

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

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

205 
qed "equalityE"; 

206 

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

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

211 
qed "equalityCE"; 

212 

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

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

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

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

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

220 
qed "setup_induction"; 

221 

222 

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

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

224 

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

225 
qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV" 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

226 
(fn _ => [rtac CollectI 1, rtac TrueI 1]); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

227 

4434  228 
Addsimps [UNIV_I]; 
229 
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

230 

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

231 
qed_goal "subset_UNIV" Set.thy "A <= UNIV" 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

232 
(fn _ => [rtac subsetI 1, rtac UNIV_I 1]); 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

233 

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

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

235 
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

236 

5069  237 
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

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

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

240 

5069  241 
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

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

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

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

245 

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

246 

2858  247 
section "The empty set  {}"; 
248 

249 
qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False" 

2891  250 
(fn _ => [ (Blast_tac 1) ]); 
2858  251 

252 
Addsimps [empty_iff]; 

253 

254 
qed_goal "emptyE" Set.thy "!!a. a:{} ==> P" 

255 
(fn _ => [Full_simp_tac 1]); 

256 

257 
AddSEs [emptyE]; 

258 

259 
qed_goal "empty_subsetI" Set.thy "{} <= A" 

2891  260 
(fn _ => [ (Blast_tac 1) ]); 
2858  261 

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

264 

2858  265 
qed_goal "equals0I" Set.thy "[ !!y. y:A ==> False ] ==> A={}" 
266 
(fn [prem]=> 

4089  267 
[ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); 
2858  268 

5256  269 
(*Use for reasoning about disjointness: A Int B = {} *) 
5450
fe9d103464a4
Changed equals0E back to equals0D and gave it the correct destruct form
paulson
parents:
5336
diff
changeset

270 
qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A" 
2891  271 
(fn _ => [ (Blast_tac 1) ]); 
2858  272 

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

273 
AddDs [equals0D, sym RS equals0D]; 
5256  274 

5069  275 
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

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

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

278 

5069  279 
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

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

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

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

283 

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

285 
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

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

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

288 

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

289 

2858  290 

291 
section "The Powerset operator  Pow"; 

292 

293 
qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)" 

294 
(fn _ => [ (Asm_simp_tac 1) ]); 

295 

296 
AddIffs [Pow_iff]; 

297 

298 
qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)" 

299 
(fn _ => [ (etac CollectI 1) ]); 

300 

301 
qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B" 

302 
(fn _=> [ (etac CollectD 1) ]); 

303 

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

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

306 

307 

5931  308 
section "Set complement"; 
923  309 

5490  310 
qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : A) = (c~:A)" 
2891  311 
(fn _ => [ (Blast_tac 1) ]); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

312 

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

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

314 

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

318 

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

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

321 
turnstile...*) 

5490  322 
Goalw [Compl_def] "c : A ==> c~:A"; 
5316  323 
by (etac CollectD 1); 
923  324 
qed "ComplD"; 
325 

326 
val ComplE = make_elim ComplD; 

327 

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

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

329 
AddSEs [ComplE]; 
1640  330 

923  331 

1548  332 
section "Binary union  Un"; 
923  333 

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

334 
qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A  c:B)" 
2891  335 
(fn _ => [ Blast_tac 1 ]); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

336 

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

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

338 

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

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

340 
by (Asm_simp_tac 1); 
923  341 
qed "UnI1"; 
342 

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

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

344 
by (Asm_simp_tac 1); 
923  345 
qed "UnI2"; 
346 

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

348 
qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B" 

349 
(fn prems=> 

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

350 
[ (Simp_tac 1), 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

351 
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]); 
923  352 

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

356 
by (REPEAT (eresolve_tac prems 1)); 

357 
qed "UnE"; 

358 

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

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

360 
AddSEs [UnE]; 
1640  361 

923  362 

1548  363 
section "Binary intersection  Int"; 
923  364 

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

365 
qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)" 
2891  366 
(fn _ => [ (Blast_tac 1) ]); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

367 

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

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

369 

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

370 
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

371 
by (Asm_simp_tac 1); 
923  372 
qed "IntI"; 
373 

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

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

375 
by (Asm_full_simp_tac 1); 
923  376 
qed "IntD1"; 
377 

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

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

379 
by (Asm_full_simp_tac 1); 
923  380 
qed "IntD2"; 
381 

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

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

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

387 
qed "IntE"; 

388 

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

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

390 
AddSEs [IntE]; 
923  391 

1548  392 
section "Set difference"; 
923  393 

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

394 
qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : AB) = (c:A & c~:B)" 
2891  395 
(fn _ => [ (Blast_tac 1) ]); 
923  396 

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

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

398 

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

399 
qed_goal "DiffI" Set.thy "!!c. [ c : A; c ~: B ] ==> c : A  B" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

400 
(fn _=> [ Asm_simp_tac 1 ]); 
923  401 

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

402 
qed_goal "DiffD1" Set.thy "!!c. c : A  B ==> c : A" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

403 
(fn _=> [ (Asm_full_simp_tac 1) ]); 
923  404 

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

405 
qed_goal "DiffD2" Set.thy "!!c. [ c : A  B; c : B ] ==> P" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

406 
(fn _=> [ (Asm_full_simp_tac 1) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

407 

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

408 
qed_goal "DiffE" Set.thy "[ c : A  B; [ c:A; c~:B ] ==> P ] ==> P" 
923  409 
(fn prems=> 
410 
[ (resolve_tac prems 1), 

411 
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]); 

412 

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

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

414 
AddSEs [DiffE]; 
923  415 

416 

1548  417 
section "Augmenting a set  insert"; 
923  418 

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

419 
qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b  a:A)" 
2891  420 
(fn _ => [Blast_tac 1]); 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

421 

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

422 
Addsimps [insert_iff]; 
923  423 

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

424 
qed_goal "insertI1" Set.thy "a : insert a B" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

425 
(fn _ => [Simp_tac 1]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

426 

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

427 
qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B" 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

428 
(fn _=> [Asm_simp_tac 1]); 
923  429 

430 
qed_goalw "insertE" Set.thy [insert_def] 

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

432 
(fn major::prems=> 

433 
[ (rtac (major RS UnE) 1), 

434 
(REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]); 

435 

436 
(*Classical introduction rule*) 

437 
qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B" 

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

438 
(fn prems=> 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

439 
[ (Simp_tac 1), 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

440 
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]); 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

441 

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

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

443 
AddSEs [insertE]; 
923  444 

1548  445 
section "Singletons, using insert"; 
923  446 

447 
qed_goal "singletonI" Set.thy "a : {a}" 

448 
(fn _=> [ (rtac insertI1 1) ]); 

449 

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

450 
Goal "b : {a} ==> b=a"; 
2891  451 
by (Blast_tac 1); 
923  452 
qed "singletonD"; 
453 

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

454 
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

455 

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

456 
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
2891  457 
(fn _ => [Blast_tac 1]); 
923  458 

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

459 
Goal "{a}={b} ==> a=b"; 
4089  460 
by (blast_tac (claset() addEs [equalityE]) 1); 
923  461 
qed "singleton_inject"; 
462 

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

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

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

467 

5069  468 
Goal "{x. x=a} = {a}"; 
4423  469 
by (Blast_tac 1); 
3582  470 
qed "singleton_conv"; 
471 
Addsimps [singleton_conv]; 

1531  472 

5600  473 
Goal "{x. a=x} = {a}"; 
474 
by(Blast_tac 1); 

475 
qed "singleton_conv2"; 

476 
Addsimps [singleton_conv2]; 

477 

1531  478 

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

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

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

484 

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

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

486 

923  487 
(*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

488 
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

489 
by Auto_tac; 
923  490 
qed "UN_I"; 
491 

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

495 
by (REPEAT (ares_tac prems 1)); 

496 
qed "UN_E"; 

497 

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

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

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

500 

5316  501 
val prems = Goal 
923  502 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 
503 
\ (UN x:A. C(x)) = (UN x:B. D(x))"; 

504 
by (REPEAT (etac UN_E 1 

505 
ORELSE ares_tac ([UN_I,equalityI,subsetI] @ 

1465  506 
(prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); 
923  507 
qed "UN_cong"; 
508 

509 

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

5069  512 
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

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

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

515 

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

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

517 

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

521 
qed "INT_I"; 

522 

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

523 
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

524 
by Auto_tac; 
923  525 
qed "INT_D"; 
526 

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

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

531 
by (REPEAT (eresolve_tac prems 1)); 

532 
qed "INT_E"; 

533 

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

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

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

536 

5316  537 
val prems = Goal 
923  538 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 
539 
\ (INT x:A. C(x)) = (INT x:B. D(x))"; 

540 
by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); 

541 
by (REPEAT (dtac INT_D 1 

542 
ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); 

543 
qed "INT_cong"; 

544 

545 

1548  546 
section "Union"; 
923  547 

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

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

551 

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

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

553 

923  554 
(*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

555 
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

556 
by Auto_tac; 
923  557 
qed "UnionI"; 
558 

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

562 
by (REPEAT (ares_tac prems 1)); 

563 
qed "UnionE"; 

564 

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

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

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

567 

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

568 

1548  569 
section "Inter"; 
923  570 

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

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

574 

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

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

576 

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

580 
qed "InterI"; 

581 

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

583 
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

584 
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

585 
by Auto_tac; 
923  586 
qed "InterD"; 
587 

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

5316  589 
val major::prems = Goalw [Inter_def] 
2721  590 
"[ A : Inter(C); X~:C ==> R; A:X ==> R ] ==> R"; 
923  591 
by (rtac (major RS INT_E) 1); 
592 
by (REPEAT (eresolve_tac prems 1)); 

593 
qed "InterE"; 

594 

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

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

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

597 

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

598 

2912  599 
(*** Image of a set under a function ***) 
600 

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

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

2912  604 
qed "image_eqI"; 
3909  605 
Addsimps [image_eqI]; 
2912  606 

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

608 

609 
(*The etaexpansion gives variablename preservation.*) 

5316  610 
val major::prems = Goalw [image_def] 
3842  611 
"[ b : (%x. f(x))``A; !!x.[ b=f(x); x:A ] ==> P ] ==> P"; 
2912  612 
by (rtac (major RS CollectD RS bexE) 1); 
613 
by (REPEAT (ares_tac prems 1)); 

614 
qed "imageE"; 

615 

616 
AddIs [image_eqI]; 

617 
AddSEs [imageE]; 

618 

5069  619 
Goal "f``(A Un B) = f``A Un f``B"; 
2935  620 
by (Blast_tac 1); 
2912  621 
qed "image_Un"; 
622 

5069  623 
Goal "(z : f``A) = (EX x:A. z = f x)"; 
3960  624 
by (Blast_tac 1); 
625 
qed "image_iff"; 

626 

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

631 

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

633 
many existing proofs.*) 

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

637 

2912  638 

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

640 

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

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

644 

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

646 

5316  647 
val [major,minor] = Goal 
3842  648 
"[ b : range(%x. f(x)); !!x. b=f(x) ==> P ] ==> P"; 
2912  649 
by (rtac (major RS imageE) 1); 
650 
by (etac minor 1); 

651 
qed "rangeE"; 

652 

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

653 

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

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

655 

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

656 

3912  657 
(** Rewrite rules for boolean casesplitting: faster than 
4830  658 
addsplits[split_if] 
3912  659 
**) 
660 

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

3912  663 

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

4830  666 
bind_thm ("split_if_mem1", 
667 
read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if); 

668 
bind_thm ("split_if_mem2", 

669 
read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if); 

3912  670 

4830  671 
val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2, 
672 
split_if_mem1, split_if_mem2]; 

3912  673 

674 

4089  675 
(*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

676 
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

677 
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

678 

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

679 
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

680 

4089  681 
simpset_ref() := simpset() addcongs [ball_cong,bex_cong] 
1776
d7e77cb8ce5c
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
oheimb
parents:
1762
diff
changeset

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

683 

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

685 

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

686 

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

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

688 

5069  689 
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

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

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

692 

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

693 
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

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

695 
qed "psubset_insertD"; 
4059  696 

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