author  paulson 
Thu, 15 Oct 1998 11:38:39 +0200  
changeset 5649  1bac26652f45 
parent 5600  34b3366b83ac 
child 5931  325300576da7 
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 

5316  66 
Goalw [Bex_def] "[ P(x); x:A ] ==> ? x:A. P(x)"; 
67 
by (Blast_tac 1); 

923  68 
qed "bexI"; 
69 

70 
qed_goal "bexCI" Set.thy 

5521  71 
"[ ! x:A. ~P(x) ==> P(a); a:A ] ==> ? x:A. P(x)" (fn prems => 
923  72 
[ (rtac classical 1), 
73 
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); 

74 

5316  75 
val major::prems = Goalw [Bex_def] 
923  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*) 
5069  85 
Goal "(! 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*) 
5069  90 
Goal "(? 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 

5316  98 
val prems = Goal 
923  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 

5316  106 
val prems = Goal 
923  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 

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

119 

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

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

123 

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

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

126 
Blast.overloaded ("op :", domain_type); 
5649  127 

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

129 
overload_1st_set "Bex"; 

4059  130 

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

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

923  137 
qed "subsetD"; 
138 

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

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

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

142 

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

145 

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

148 

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

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

151 

923  152 
(*Classical elimination rule*) 
5316  153 
val major::prems = Goalw [subset_def] 
923  154 
"[ A <= B; c~:A ==> P; c:B ==> P ] ==> P"; 
155 
by (rtac (major RS ballE) 1); 

156 
by (REPEAT (eresolve_tac prems 1)); 

157 
qed "subsetCE"; 

158 

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

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

161 

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

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

163 
AddEs [subsetD, subsetCE]; 
923  164 

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

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

167 

5316  168 
Goal "[ A<=B; B<=C ] ==> A<=(C::'a set)"; 
2891  169 
by (Blast_tac 1); 
923  170 
qed "subset_trans"; 
171 

172 

1548  173 
section "Equality"; 
923  174 

175 
(*Antisymmetry of the subset relation*) 

5316  176 
Goal "[ A <= B; B <= A ] ==> A = (B::'a set)"; 
5318  177 
by (rtac set_ext 1); 
5316  178 
by (blast_tac (claset() addIs [subsetD]) 1); 
923  179 
qed "subset_antisym"; 
180 
val equalityI = subset_antisym; 

181 

1762  182 
AddSIs [equalityI]; 
183 

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

923  187 
by (rtac subset_refl 1); 
188 
qed "equalityD1"; 

189 

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

923  192 
by (rtac subset_refl 1); 
193 
qed "equalityD2"; 

194 

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

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

199 
qed "equalityE"; 

200 

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

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

205 
qed "equalityCE"; 

206 

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

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

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

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

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

214 
qed "setup_induction"; 

215 

216 

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

217 
section "The universal set  UNIV"; 
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 
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

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

221 

4434  222 
Addsimps [UNIV_I]; 
223 
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

224 

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

225 
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

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

227 

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

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

229 
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

230 

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

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 "ball_UNIV"; 
4aff9b7e5597
UNIV now a constant; UNION1, INTER1 now translations and no longer have
paulson
parents:
4135
diff
changeset

234 

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

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

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

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

239 

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

240 

2858  241 
section "The empty set  {}"; 
242 

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

2891  244 
(fn _ => [ (Blast_tac 1) ]); 
2858  245 

246 
Addsimps [empty_iff]; 

247 

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

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

250 

251 
AddSEs [emptyE]; 

252 

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

2891  254 
(fn _ => [ (Blast_tac 1) ]); 
2858  255 

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

258 

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

4089  261 
[ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]); 
2858  262 

5256  263 
(*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

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

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

267 
AddDs [equals0D, sym RS equals0D]; 
5256  268 

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

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

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

272 

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

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

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

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

277 

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

279 
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

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

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

282 

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

283 

2858  284 

285 
section "The Powerset operator  Pow"; 

286 

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

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

289 

290 
AddIffs [Pow_iff]; 

291 

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

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

294 

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

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

297 

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

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

300 

301 

1548  302 
section "Set complement  Compl"; 
923  303 

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

306 

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

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

308 

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

312 

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

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

315 
turnstile...*) 

5490  316 
Goalw [Compl_def] "c : A ==> c~:A"; 
5316  317 
by (etac CollectD 1); 
923  318 
qed "ComplD"; 
319 

320 
val ComplE = make_elim ComplD; 

321 

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

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

323 
AddSEs [ComplE]; 
1640  324 

923  325 

1548  326 
section "Binary union  Un"; 
923  327 

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

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

330 

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

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

332 

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

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

334 
by (Asm_simp_tac 1); 
923  335 
qed "UnI1"; 
336 

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

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

338 
by (Asm_simp_tac 1); 
923  339 
qed "UnI2"; 
340 

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

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

343 
(fn prems=> 

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

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

345 
(REPEAT (ares_tac (prems@[disjCI]) 1)) ]); 
923  346 

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

350 
by (REPEAT (eresolve_tac prems 1)); 

351 
qed "UnE"; 

352 

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

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

354 
AddSEs [UnE]; 
1640  355 

923  356 

1548  357 
section "Binary intersection  Int"; 
923  358 

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

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

361 

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

362 
Addsimps [Int_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:B ] ==> c : A Int 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 "IntI"; 
367 

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

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

369 
by (Asm_full_simp_tac 1); 
923  370 
qed "IntD1"; 
371 

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

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

373 
by (Asm_full_simp_tac 1); 
923  374 
qed "IntD2"; 
375 

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

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

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

381 
qed "IntE"; 

382 

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

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

384 
AddSEs [IntE]; 
923  385 

1548  386 
section "Set difference"; 
923  387 

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

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

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

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

392 

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

393 
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

394 
(fn _=> [ Asm_simp_tac 1 ]); 
923  395 

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

396 
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

397 
(fn _=> [ (Asm_full_simp_tac 1) ]); 
923  398 

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

399 
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

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

401 

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

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

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

406 

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

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

408 
AddSEs [DiffE]; 
923  409 

410 

1548  411 
section "Augmenting a set  insert"; 
923  412 

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

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

415 

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

416 
Addsimps [insert_iff]; 
923  417 

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

418 
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

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

420 

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

421 
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

422 
(fn _=> [Asm_simp_tac 1]); 
923  423 

424 
qed_goalw "insertE" Set.thy [insert_def] 

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

426 
(fn major::prems=> 

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

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

429 

430 
(*Classical introduction rule*) 

431 
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

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

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

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

435 

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

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

437 
AddSEs [insertE]; 
923  438 

1548  439 
section "Singletons, using insert"; 
923  440 

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

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

443 

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

444 
Goal "b : {a} ==> b=a"; 
2891  445 
by (Blast_tac 1); 
923  446 
qed "singletonD"; 
447 

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

448 
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

449 

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

450 
qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
2891  451 
(fn _ => [Blast_tac 1]); 
923  452 

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

453 
Goal "{a}={b} ==> a=b"; 
4089  454 
by (blast_tac (claset() addEs [equalityE]) 1); 
923  455 
qed "singleton_inject"; 
456 

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

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

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

461 

5069  462 
Goal "{x. x=a} = {a}"; 
4423  463 
by (Blast_tac 1); 
3582  464 
qed "singleton_conv"; 
465 
Addsimps [singleton_conv]; 

1531  466 

5600  467 
Goal "{x. a=x} = {a}"; 
468 
by(Blast_tac 1); 

469 
qed "singleton_conv2"; 

470 
Addsimps [singleton_conv2]; 

471 

1531  472 

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

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

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

478 

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

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

480 

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

482 
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

483 
by Auto_tac; 
923  484 
qed "UN_I"; 
485 

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

489 
by (REPEAT (ares_tac prems 1)); 

490 
qed "UN_E"; 

491 

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

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

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

494 

5316  495 
val prems = Goal 
923  496 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 
497 
\ (UN x:A. C(x)) = (UN x:B. D(x))"; 

498 
by (REPEAT (etac UN_E 1 

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

1465  500 
(prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); 
923  501 
qed "UN_cong"; 
502 

503 

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

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

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

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

509 

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

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

511 

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

515 
qed "INT_I"; 

516 

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

517 
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

518 
by Auto_tac; 
923  519 
qed "INT_D"; 
520 

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

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

525 
by (REPEAT (eresolve_tac prems 1)); 

526 
qed "INT_E"; 

527 

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

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

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

530 

5316  531 
val prems = Goal 
923  532 
"[ A=B; !!x. x:B ==> C(x) = D(x) ] ==> \ 
533 
\ (INT x:A. C(x)) = (INT x:B. D(x))"; 

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

535 
by (REPEAT (dtac INT_D 1 

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

537 
qed "INT_cong"; 

538 

539 

1548  540 
section "Union"; 
923  541 

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

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

545 

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

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

547 

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

549 
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

550 
by Auto_tac; 
923  551 
qed "UnionI"; 
552 

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

556 
by (REPEAT (ares_tac prems 1)); 

557 
qed "UnionE"; 

558 

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

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

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

561 

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

562 

1548  563 
section "Inter"; 
923  564 

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

567 
qed "Inter_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 [Inter_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:C ==> A:X ] ==> A : Inter(C)"; 
573 
by (REPEAT (ares_tac ([INT_I] @ prems) 1)); 

574 
qed "InterI"; 

575 

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

577 
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

578 
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

579 
by Auto_tac; 
923  580 
qed "InterD"; 
581 

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

5316  583 
val major::prems = Goalw [Inter_def] 
2721  584 
"[ A : Inter(C); X~:C ==> R; A:X ==> R ] ==> R"; 
923  585 
by (rtac (major RS INT_E) 1); 
586 
by (REPEAT (eresolve_tac prems 1)); 

587 
qed "InterE"; 

588 

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

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

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

591 

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

592 

2912  593 
(*** Image of a set under a function ***) 
594 

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

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

2912  598 
qed "image_eqI"; 
3909  599 
Addsimps [image_eqI]; 
2912  600 

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

602 

603 
(*The etaexpansion gives variablename preservation.*) 

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

608 
qed "imageE"; 

609 

610 
AddIs [image_eqI]; 

611 
AddSEs [imageE]; 

612 

5069  613 
Goal "f``(A Un B) = f``A Un f``B"; 
2935  614 
by (Blast_tac 1); 
2912  615 
qed "image_Un"; 
616 

5069  617 
Goal "(z : f``A) = (EX x:A. z = f x)"; 
3960  618 
by (Blast_tac 1); 
619 
qed "image_iff"; 

620 

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

625 

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

627 
many existing proofs.*) 

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

631 

2912  632 

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

634 

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

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

638 

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

640 

5316  641 
val [major,minor] = Goal 
3842  642 
"[ b : range(%x. f(x)); !!x. b=f(x) ==> P ] ==> P"; 
2912  643 
by (rtac (major RS imageE) 1); 
644 
by (etac minor 1); 

645 
qed "rangeE"; 

646 

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

647 

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

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

649 

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

650 

3912  651 
(** Rewrite rules for boolean casesplitting: faster than 
4830  652 
addsplits[split_if] 
3912  653 
**) 
654 

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

3912  657 

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

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

662 
bind_thm ("split_if_mem2", 

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

3912  664 

4830  665 
val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2, 
666 
split_if_mem1, split_if_mem2]; 

3912  667 

668 

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

670 
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

671 
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

672 

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

673 
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

674 

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

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

677 

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

679 

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

680 

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

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

682 

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

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

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

686 

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

687 
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

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

689 
qed "psubset_insertD"; 
4059  690 

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