author  paulson 
Wed, 05 Nov 1997 13:32:07 +0100  
changeset 4159  4aff9b7e5597 
parent 4135  4830f1f5f6ea 
child 4229  551684f275b9 
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 

3842  16 
goal Set.thy "!!a. 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 

3842  20 
val prems = goal Set.thy "!!a. 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 

24 
val [prem] = goal Set.thy "[ !!x. (x:A) = (x:B) ] ==> A = B"; 

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 

30 
val [prem] = goal Set.thy "[ !!x. P(x)=Q(x) ] ==> {x. P(x)} = {x. Q(x)}"; 

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 

42 
val prems = goalw Set.thy [Ball_def] 

43 
"[ !!x. x:A ==> P(x) ] ==> ! x:A. P(x)"; 

44 
by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); 

45 
qed "ballI"; 

46 

47 
val [major,minor] = goalw Set.thy [Ball_def] 

48 
"[ ! x:A. P(x); x:A ] ==> P(x)"; 

49 
by (rtac (minor RS (major RS spec RS mp)) 1); 

50 
qed "bspec"; 

51 

52 
val major::prems = goalw Set.thy [Ball_def] 

53 
"[ ! x:A. P(x); P(x) ==> Q; x~:A ==> Q ] ==> Q"; 

54 
by (rtac (major RS spec RS impCE) 1); 

55 
by (REPEAT (eresolve_tac prems 1)); 

56 
qed "ballE"; 

57 

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

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

60 

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

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

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

63 

923  64 
val prems = goalw Set.thy [Bex_def] 
65 
"[ P(x); x:A ] ==> ? x:A. P(x)"; 

66 
by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); 

67 
qed "bexI"; 

68 

69 
qed_goal "bexCI" Set.thy 

3842  70 
"[ ! x:A. ~P(x) ==> P(a); a:A ] ==> ? x:A. P(x)" 
923  71 
(fn prems=> 
72 
[ (rtac classical 1), 

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

74 

75 
val major::prems = goalw Set.thy [Bex_def] 

76 
"[ ? x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q"; 

77 
by (rtac (major RS exE) 1); 

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

79 
qed "bexE"; 

80 

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

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

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

83 

3420  84 
(*Trival rewrite rule*) 
3842  85 
goal Set.thy "(! x:A. P) = ((? x. x:A) > P)"; 
4089  86 
by (simp_tac (simpset() addsimps [Ball_def]) 1); 
3420  87 
qed "ball_triv"; 
1816  88 

1882  89 
(*Dual form for existentials*) 
3842  90 
goal Set.thy "(? x:A. P) = ((? x. x:A) & P)"; 
4089  91 
by (simp_tac (simpset() addsimps [Bex_def]) 1); 
3420  92 
qed "bex_triv"; 
1882  93 

3420  94 
Addsimps [ball_triv, bex_triv]; 
923  95 

96 
(** Congruence rules **) 

97 

98 
val prems = goal Set.thy 

99 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 

100 
\ (! x:A. P(x)) = (! x:B. Q(x))"; 

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

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

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

104 
qed "ball_cong"; 

105 

106 
val prems = goal Set.thy 

107 
"[ A=B; !!x. x:B ==> P(x) = Q(x) ] ==> \ 

108 
\ (? x:A. P(x)) = (? x:B. Q(x))"; 

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

110 
by (REPEAT (etac bexE 1 

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

112 
qed "bex_cong"; 

113 

1548  114 
section "Subsets"; 
923  115 

3842  116 
val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; 
923  117 
by (REPEAT (ares_tac (prems @ [ballI]) 1)); 
118 
qed "subsetI"; 

119 

4059  120 
Blast.overload ("op <=", domain_type); (*The <= relation is overloaded*) 
121 

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

123 
for overloading of = to work.*) 

124 
Blast.overload ("op :", domain_type); 

125 
seq (fn a => Blast.overload (a, HOLogic.dest_setT o domain_type)) 

126 
["Ball", "Bex"]; 

127 
(*need UNION, INTER also?*) 

128 

2881  129 

923  130 
(*Rule in Modus Ponens style*) 
131 
val major::prems = goalw Set.thy [subset_def] "[ A <= B; c:A ] ==> c:B"; 

132 
by (rtac (major RS bspec) 1); 

133 
by (resolve_tac prems 1); 

134 
qed "subsetD"; 

135 

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

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

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

139 

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

142 

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

145 

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

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

148 

923  149 
(*Classical elimination rule*) 
150 
val major::prems = goalw Set.thy [subset_def] 

151 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P"; 

152 
by (rtac (major RS ballE) 1); 

153 
by (REPEAT (eresolve_tac prems 1)); 

154 
qed "subsetCE"; 

155 

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

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

158 

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

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

160 
AddEs [subsetD, subsetCE]; 
923  161 

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

162 
qed_goal "subset_refl" Set.thy "A <= (A::'a set)" 
4059  163 
(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

164 

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

165 
val prems = goal Set.thy "!!B. [ A<=B; B<=C ] ==> A<=(C::'a set)"; 
2891  166 
by (Blast_tac 1); 
923  167 
qed "subset_trans"; 
168 

169 

1548  170 
section "Equality"; 
923  171 

172 
(*Antisymmetry of the subset relation*) 

173 
val prems = goal Set.thy "[ A <= B; B <= A ] ==> A = (B::'a set)"; 

174 
by (rtac (iffI RS set_ext) 1); 

175 
by (REPEAT (ares_tac (prems RL [subsetD]) 1)); 

176 
qed "subset_antisym"; 

177 
val equalityI = subset_antisym; 

178 

1762  179 
AddSIs [equalityI]; 
180 

923  181 
(* Equality rules from ZF set theory  are they appropriate here? *) 
182 
val prems = goal Set.thy "A = B ==> A<=(B::'a set)"; 

183 
by (resolve_tac (prems RL [subst]) 1); 

184 
by (rtac subset_refl 1); 

185 
qed "equalityD1"; 

186 

187 
val prems = goal Set.thy "A = B ==> B<=(A::'a set)"; 

188 
by (resolve_tac (prems RL [subst]) 1); 

189 
by (rtac subset_refl 1); 

190 
qed "equalityD2"; 

191 

192 
val prems = goal Set.thy 

193 
"[ A = B; [ A<=B; B<=(A::'a set) ] ==> P ] ==> P"; 

194 
by (resolve_tac prems 1); 

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

196 
qed "equalityE"; 

197 

198 
val major::prems = goal Set.thy 

199 
"[ A = B; [ c:A; c:B ] ==> P; [ c~:A; c~:B ] ==> P ] ==> P"; 

200 
by (rtac (major RS equalityE) 1); 

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

202 
qed "equalityCE"; 

203 

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

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

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

207 
val prems = goal Set.thy 

208 
"[ p:A; !!z. z:A ==> p=z > R ] ==> R"; 

209 
by (rtac mp 1); 

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

211 
qed "setup_induction"; 

212 

213 

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

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

215 

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

216 
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

217 
(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

218 

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

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

220 

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

221 
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

222 
(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

223 

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

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

225 
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

226 

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

227 
goalw Set.thy [Ball_def] "Ball UNIV P = All P"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

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

229 
qed "ball_UNIV"; 
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 
goalw Set.thy [Bex_def] "Bex UNIV P = Ex P"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

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

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

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

235 

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

236 

2858  237 
section "The empty set  {}"; 
238 

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

2891  240 
(fn _ => [ (Blast_tac 1) ]); 
2858  241 

242 
Addsimps [empty_iff]; 

243 

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

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

246 

247 
AddSEs [emptyE]; 

248 

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

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

252 
qed_goal "equals0I" Set.thy "[ !!y. y:A ==> False ] ==> A={}" 

253 
(fn [prem]=> 

4089  254 
[ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); 
2858  255 

256 
qed_goal "equals0D" Set.thy "!!a. [ A={}; a:A ] ==> P" 

2891  257 
(fn _ => [ (Blast_tac 1) ]); 
2858  258 

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

259 
goalw Set.thy [Ball_def] "Ball {} P = True"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

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

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

262 

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

263 
goalw Set.thy [Bex_def] "Bex {} P = False"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

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

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

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

267 

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

268 
goal thy "UNIV ~= {}"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

269 
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

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

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

272 

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

273 

2858  274 

275 
section "The Powerset operator  Pow"; 

276 

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

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

279 

280 
AddIffs [Pow_iff]; 

281 

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

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

284 

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

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

287 

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

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

290 

291 

1548  292 
section "Set complement  Compl"; 
923  293 

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

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

296 

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

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

298 

923  299 
val prems = goalw Set.thy [Compl_def] 
300 
"[ c:A ==> False ] ==> c : Compl(A)"; 

301 
by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); 

302 
qed "ComplI"; 

303 

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

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

306 
turnstile...*) 

307 
val major::prems = goalw Set.thy [Compl_def] 

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

308 
"c : Compl(A) ==> c~:A"; 
923  309 
by (rtac (major RS CollectD) 1); 
310 
qed "ComplD"; 

311 

312 
val ComplE = make_elim ComplD; 

313 

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

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

315 
AddSEs [ComplE]; 
1640  316 

923  317 

1548  318 
section "Binary union  Un"; 
923  319 

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

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

322 

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

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

324 

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

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

326 
by (Asm_simp_tac 1); 
923  327 
qed "UnI1"; 
328 

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

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

330 
by (Asm_simp_tac 1); 
923  331 
qed "UnI2"; 
332 

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

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

335 
(fn prems=> 

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

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

337 
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]); 
923  338 

339 
val major::prems = goalw Set.thy [Un_def] 

340 
"[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P"; 

341 
by (rtac (major RS CollectD RS disjE) 1); 

342 
by (REPEAT (eresolve_tac prems 1)); 

343 
qed "UnE"; 

344 

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

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

346 
AddSEs [UnE]; 
1640  347 

923  348 

1548  349 
section "Binary intersection  Int"; 
923  350 

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

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

353 

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

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

355 

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

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

357 
by (Asm_simp_tac 1); 
923  358 
qed "IntI"; 
359 

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

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

361 
by (Asm_full_simp_tac 1); 
923  362 
qed "IntD1"; 
363 

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

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

365 
by (Asm_full_simp_tac 1); 
923  366 
qed "IntD2"; 
367 

368 
val [major,minor] = goal Set.thy 

369 
"[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P"; 

370 
by (rtac minor 1); 

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

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

373 
qed "IntE"; 

374 

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

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

376 
AddSEs [IntE]; 
923  377 

1548  378 
section "Set difference"; 
923  379 

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

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

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

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

384 

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

385 
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

386 
(fn _=> [ Asm_simp_tac 1 ]); 
923  387 

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

388 
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

389 
(fn _=> [ (Asm_full_simp_tac 1) ]); 
923  390 

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

391 
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

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

393 

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

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

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

398 

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

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

400 
AddSEs [DiffE]; 
923  401 

402 

1548  403 
section "Augmenting a set  insert"; 
923  404 

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

405 
qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b  a:A)" 
2891  406 
(fn _ => [Blast_tac 1]); 
2499
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 
Addsimps [insert_iff]; 
923  409 

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

410 
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

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

412 

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

413 
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

414 
(fn _=> [Asm_simp_tac 1]); 
923  415 

416 
qed_goalw "insertE" Set.thy [insert_def] 

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

418 
(fn major::prems=> 

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

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

421 

422 
(*Classical introduction rule*) 

423 
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

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

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

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

427 

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

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

429 
AddSEs [insertE]; 
923  430 

1548  431 
section "Singletons, using insert"; 
923  432 

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

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

435 

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

436 
goal Set.thy "!!a. b : {a} ==> b=a"; 
2891  437 
by (Blast_tac 1); 
923  438 
qed "singletonD"; 
439 

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

440 
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

441 

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

442 
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
2891  443 
(fn _ => [Blast_tac 1]); 
923  444 

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

445 
goal Set.thy "!!a b. {a}={b} ==> a=b"; 
4089  446 
by (blast_tac (claset() addEs [equalityE]) 1); 
923  447 
qed "singleton_inject"; 
448 

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

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

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

453 

3842  454 
goal Set.thy "{x. x=a} = {a}"; 
3582  455 
by(Blast_tac 1); 
456 
qed "singleton_conv"; 

457 
Addsimps [singleton_conv]; 

1531  458 

459 

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

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

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

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

465 

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

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

467 

923  468 
(*The order of the premises presupposes that A is rigid; b may be flexible*) 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

469 
goal Set.thy "!!b. [ a:A; b: B(a) ] ==> b: (UN x:A. B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

470 
by (Auto_tac()); 
923  471 
qed "UN_I"; 
472 

473 
val major::prems = goalw Set.thy [UNION_def] 

474 
"[ b : (UN x:A. B(x)); !!x.[ x:A; b: B(x) ] ==> R ] ==> R"; 

475 
by (rtac (major RS CollectD RS bexE) 1); 

476 
by (REPEAT (ares_tac prems 1)); 

477 
qed "UN_E"; 

478 

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

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

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

481 

923  482 
val prems = goal Set.thy 
483 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 

484 
\ (UN x:A. C(x)) = (UN x:B. D(x))"; 

485 
by (REPEAT (etac UN_E 1 

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

1465  487 
(prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); 
923  488 
qed "UN_cong"; 
489 

490 

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

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

493 
goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

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

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

496 

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

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

498 

923  499 
val prems = goalw Set.thy [INTER_def] 
500 
"(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; 

501 
by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); 

502 
qed "INT_I"; 

503 

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

504 
goal Set.thy "!!b. [ b : (INT x:A. B(x)); a:A ] ==> b: B(a)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

505 
by (Auto_tac()); 
923  506 
qed "INT_D"; 
507 

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

509 
val major::prems = goalw Set.thy [INTER_def] 

510 
"[ b : (INT x:A. B(x)); b: B(a) ==> R; a~:A ==> R ] ==> R"; 

511 
by (rtac (major RS CollectD RS ballE) 1); 

512 
by (REPEAT (eresolve_tac prems 1)); 

513 
qed "INT_E"; 

514 

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

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

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

517 

923  518 
val prems = goal Set.thy 
519 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 

520 
\ (INT x:A. C(x)) = (INT x:B. D(x))"; 

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

522 
by (REPEAT (dtac INT_D 1 

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

524 
qed "INT_cong"; 

525 

526 

1548  527 
section "Union"; 
923  528 

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

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

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

532 

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

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

534 

923  535 
(*The order of the premises presupposes that C is rigid; A may be flexible*) 
2499
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

536 
goal Set.thy "!!X. [ X:C; A:X ] ==> A : Union(C)"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

537 
by (Auto_tac()); 
923  538 
qed "UnionI"; 
539 

540 
val major::prems = goalw Set.thy [Union_def] 

541 
"[ A : Union(C); !!X.[ A:X; X:C ] ==> R ] ==> R"; 

542 
by (rtac (major RS UN_E) 1); 

543 
by (REPEAT (ares_tac prems 1)); 

544 
qed "UnionE"; 

545 

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

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

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

548 

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

549 

1548  550 
section "Inter"; 
923  551 

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

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

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

555 

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

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

557 

923  558 
val prems = goalw Set.thy [Inter_def] 
559 
"[ !!X. X:C ==> A:X ] ==> A : Inter(C)"; 

560 
by (REPEAT (ares_tac ([INT_I] @ prems) 1)); 

561 
qed "InterI"; 

562 

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

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

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

565 
goal Set.thy "!!X. [ A : Inter(C); X:C ] ==> A:X"; 
0bc87b063447
Tidying of proofs. New theorems are enterred immediately into the
paulson
parents:
2031
diff
changeset

566 
by (Auto_tac()); 
923  567 
qed "InterD"; 
568 

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

570 
val major::prems = goalw Set.thy [Inter_def] 

2721  571 
"[ A : Inter(C); X~:C ==> R; A:X ==> R ] ==> R"; 
923  572 
by (rtac (major RS INT_E) 1); 
573 
by (REPEAT (eresolve_tac prems 1)); 

574 
qed "InterE"; 

575 

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

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

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

578 

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

579 

2912  580 
(*** Image of a set under a function ***) 
581 

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

583 
val prems = goalw thy [image_def] "[ b=f(x); x:A ] ==> b : f``A"; 

584 
by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1)); 

585 
qed "image_eqI"; 

3909  586 
Addsimps [image_eqI]; 
2912  587 

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

589 

590 
(*The etaexpansion gives variablename preservation.*) 

591 
val major::prems = goalw thy [image_def] 

3842  592 
"[ b : (%x. f(x))``A; !!x.[ b=f(x); x:A ] ==> P ] ==> P"; 
2912  593 
by (rtac (major RS CollectD RS bexE) 1); 
594 
by (REPEAT (ares_tac prems 1)); 

595 
qed "imageE"; 

596 

597 
AddIs [image_eqI]; 

598 
AddSEs [imageE]; 

599 

600 
goalw thy [o_def] "(f o g)``r = f``(g``r)"; 

2935  601 
by (Blast_tac 1); 
2912  602 
qed "image_compose"; 
603 

604 
goal thy "f``(A Un B) = f``A Un f``B"; 

2935  605 
by (Blast_tac 1); 
2912  606 
qed "image_Un"; 
607 

3960  608 
goal Set.thy "(z : f``A) = (EX x:A. z = f x)"; 
609 
by (Blast_tac 1); 

610 
qed "image_iff"; 

611 

2912  612 

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

614 

615 
goal thy "!!b. b=f(x) ==> b : range(f)"; 

616 
by (EVERY1 [etac image_eqI, rtac UNIV_I]); 

617 
bind_thm ("range_eqI", UNIV_I RSN (2,image_eqI)); 

618 

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

620 

621 
val [major,minor] = goal thy 

3842  622 
"[ b : range(%x. f(x)); !!x. b=f(x) ==> P ] ==> P"; 
2912  623 
by (rtac (major RS imageE) 1); 
624 
by (etac minor 1); 

625 
qed "rangeE"; 

626 

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

627 

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

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

629 

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

630 

3912  631 
(** Rewrite rules for boolean casesplitting: faster than 
3919  632 
addsplits[expand_if] 
3912  633 
**) 
634 

635 
bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if); 

636 
bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if); 

637 

638 
bind_thm ("expand_if_mem1", 

639 
read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if); 

640 
bind_thm ("expand_if_mem2", 

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

642 

643 
val expand_ifs = [if_bool_eq, expand_if_eq1, expand_if_eq2, 

644 
expand_if_mem1, expand_if_mem2]; 

645 

646 

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

648 
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

649 
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

650 

1937  651 
(*Not for Addsimps  it can cause goals to blow up!*) 
652 
goal Set.thy "(a : (if Q then x else y)) = ((Q > a:x) & (~Q > a : y))"; 

4089  653 
by (simp_tac (simpset() addsplits [expand_if]) 1); 
1937  654 
qed "mem_if"; 
655 

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

656 
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

657 

4089  658 
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

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

660 

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

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

662 

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

663 

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

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

665 

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

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

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

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

669 

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

670 
goalw Set.thy [psubset_def] 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

671 
"!!x. A < insert x B ==> (x ~: A) & A<=B  x:A & A{x}<B"; 
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
2935
diff
changeset

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

673 
qed "psubset_insertD"; 
4059  674 

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