1 (* Title: set/set |
1 (* Title: Set/Set.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 |
|
4 For set.thy. |
|
5 |
|
6 Modified version of |
|
7 Title: HOL/set |
|
8 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
9 Copyright 1991 University of Cambridge |
|
10 |
|
11 For set.thy. Set theory for higher-order logic. A set is simply a predicate. |
|
12 *) |
3 *) |
13 |
4 |
14 open Set; |
5 val [prem] = goal (the_context ()) "[| P(a) |] ==> a : {x. P(x)}"; |
15 |
|
16 val [prem] = goal Set.thy "[| P(a) |] ==> a : {x. P(x)}"; |
|
17 by (rtac (mem_Collect_iff RS iffD2) 1); |
6 by (rtac (mem_Collect_iff RS iffD2) 1); |
18 by (rtac prem 1); |
7 by (rtac prem 1); |
19 qed "CollectI"; |
8 qed "CollectI"; |
20 |
9 |
21 val prems = goal Set.thy "[| a : {x. P(x)} |] ==> P(a)"; |
10 val prems = goal (the_context ()) "[| a : {x. P(x)} |] ==> P(a)"; |
22 by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1); |
11 by (resolve_tac (prems RL [mem_Collect_iff RS iffD1]) 1); |
23 qed "CollectD"; |
12 qed "CollectD"; |
24 |
13 |
25 val CollectE = make_elim CollectD; |
14 val CollectE = make_elim CollectD; |
26 |
15 |
27 val [prem] = goal Set.thy "[| !!x. x:A <-> x:B |] ==> A = B"; |
16 val [prem] = goal (the_context ()) "[| !!x. x:A <-> x:B |] ==> A = B"; |
28 by (rtac (set_extension RS iffD2) 1); |
17 by (rtac (set_extension RS iffD2) 1); |
29 by (rtac (prem RS allI) 1); |
18 by (rtac (prem RS allI) 1); |
30 qed "set_ext"; |
19 qed "set_ext"; |
31 |
20 |
32 (*** Bounded quantifiers ***) |
21 (*** Bounded quantifiers ***) |
33 |
22 |
34 val prems = goalw Set.thy [Ball_def] |
23 val prems = goalw (the_context ()) [Ball_def] |
35 "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"; |
24 "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"; |
36 by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); |
25 by (REPEAT (ares_tac (prems @ [allI,impI]) 1)); |
37 qed "ballI"; |
26 qed "ballI"; |
38 |
27 |
39 val [major,minor] = goalw Set.thy [Ball_def] |
28 val [major,minor] = goalw (the_context ()) [Ball_def] |
40 "[| ALL x:A. P(x); x:A |] ==> P(x)"; |
29 "[| ALL x:A. P(x); x:A |] ==> P(x)"; |
41 by (rtac (minor RS (major RS spec RS mp)) 1); |
30 by (rtac (minor RS (major RS spec RS mp)) 1); |
42 qed "bspec"; |
31 qed "bspec"; |
43 |
32 |
44 val major::prems = goalw Set.thy [Ball_def] |
33 val major::prems = goalw (the_context ()) [Ball_def] |
45 "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"; |
34 "[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"; |
46 by (rtac (major RS spec RS impCE) 1); |
35 by (rtac (major RS spec RS impCE) 1); |
47 by (REPEAT (eresolve_tac prems 1)); |
36 by (REPEAT (eresolve_tac prems 1)); |
48 qed "ballE"; |
37 qed "ballE"; |
49 |
38 |
50 (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*) |
39 (*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*) |
51 fun ball_tac i = etac ballE i THEN contr_tac (i+1); |
40 fun ball_tac i = etac ballE i THEN contr_tac (i+1); |
52 |
41 |
53 val prems = goalw Set.thy [Bex_def] |
42 val prems = goalw (the_context ()) [Bex_def] |
54 "[| P(x); x:A |] ==> EX x:A. P(x)"; |
43 "[| P(x); x:A |] ==> EX x:A. P(x)"; |
55 by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); |
44 by (REPEAT (ares_tac (prems @ [exI,conjI]) 1)); |
56 qed "bexI"; |
45 qed "bexI"; |
57 |
46 |
58 qed_goal "bexCI" Set.thy |
47 qed_goal "bexCI" (the_context ()) |
59 "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" |
48 "[| EX x:A. ~P(x) ==> P(a); a:A |] ==> EX x:A. P(x)" |
60 (fn prems=> |
49 (fn prems=> |
61 [ (rtac classical 1), |
50 [ (rtac classical 1), |
62 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |
51 (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]); |
63 |
52 |
64 val major::prems = goalw Set.thy [Bex_def] |
53 val major::prems = goalw (the_context ()) [Bex_def] |
65 "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; |
54 "[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q"; |
66 by (rtac (major RS exE) 1); |
55 by (rtac (major RS exE) 1); |
67 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); |
56 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)); |
68 qed "bexE"; |
57 qed "bexE"; |
69 |
58 |
70 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
59 (*Trival rewrite rule; (! x:A.P)=P holds only if A is nonempty!*) |
71 val prems = goal Set.thy |
60 val prems = goal (the_context ()) |
72 "(ALL x:A. True) <-> True"; |
61 "(ALL x:A. True) <-> True"; |
73 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); |
62 by (REPEAT (ares_tac [TrueI,ballI,iffI] 1)); |
74 qed "ball_rew"; |
63 qed "ball_rew"; |
75 |
64 |
76 (** Congruence rules **) |
65 (** Congruence rules **) |
77 |
66 |
78 val prems = goal Set.thy |
67 val prems = goal (the_context ()) |
79 "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ |
68 "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ |
80 \ (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"; |
69 \ (ALL x:A. P(x)) <-> (ALL x:A'. P'(x))"; |
81 by (resolve_tac (prems RL [ssubst,iffD2]) 1); |
70 by (resolve_tac (prems RL [ssubst,iffD2]) 1); |
82 by (REPEAT (ares_tac [ballI,iffI] 1 |
71 by (REPEAT (ares_tac [ballI,iffI] 1 |
83 ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); |
72 ORELSE eresolve_tac ([make_elim bspec, mp] @ (prems RL [iffE])) 1)); |
84 qed "ball_cong"; |
73 qed "ball_cong"; |
85 |
74 |
86 val prems = goal Set.thy |
75 val prems = goal (the_context ()) |
87 "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ |
76 "[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> \ |
88 \ (EX x:A. P(x)) <-> (EX x:A'. P'(x))"; |
77 \ (EX x:A. P(x)) <-> (EX x:A'. P'(x))"; |
89 by (resolve_tac (prems RL [ssubst,iffD2]) 1); |
78 by (resolve_tac (prems RL [ssubst,iffD2]) 1); |
90 by (REPEAT (etac bexE 1 |
79 by (REPEAT (etac bexE 1 |
91 ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); |
80 ORELSE ares_tac ([bexI,iffI] @ (prems RL [iffD1,iffD2])) 1)); |
92 qed "bex_cong"; |
81 qed "bex_cong"; |
93 |
82 |
94 (*** Rules for subsets ***) |
83 (*** Rules for subsets ***) |
95 |
84 |
96 val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; |
85 val prems = goalw (the_context ()) [subset_def] "(!!x. x:A ==> x:B) ==> A <= B"; |
97 by (REPEAT (ares_tac (prems @ [ballI]) 1)); |
86 by (REPEAT (ares_tac (prems @ [ballI]) 1)); |
98 qed "subsetI"; |
87 qed "subsetI"; |
99 |
88 |
100 (*Rule in Modus Ponens style*) |
89 (*Rule in Modus Ponens style*) |
101 val major::prems = goalw Set.thy [subset_def] "[| A <= B; c:A |] ==> c:B"; |
90 val major::prems = goalw (the_context ()) [subset_def] "[| A <= B; c:A |] ==> c:B"; |
102 by (rtac (major RS bspec) 1); |
91 by (rtac (major RS bspec) 1); |
103 by (resolve_tac prems 1); |
92 by (resolve_tac prems 1); |
104 qed "subsetD"; |
93 qed "subsetD"; |
105 |
94 |
106 (*Classical elimination rule*) |
95 (*Classical elimination rule*) |
107 val major::prems = goalw Set.thy [subset_def] |
96 val major::prems = goalw (the_context ()) [subset_def] |
108 "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"; |
97 "[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"; |
109 by (rtac (major RS ballE) 1); |
98 by (rtac (major RS ballE) 1); |
110 by (REPEAT (eresolve_tac prems 1)); |
99 by (REPEAT (eresolve_tac prems 1)); |
111 qed "subsetCE"; |
100 qed "subsetCE"; |
112 |
101 |
113 (*Takes assumptions A<=B; c:A and creates the assumption c:B *) |
102 (*Takes assumptions A<=B; c:A and creates the assumption c:B *) |
114 fun set_mp_tac i = etac subsetCE i THEN mp_tac i; |
103 fun set_mp_tac i = etac subsetCE i THEN mp_tac i; |
115 |
104 |
116 qed_goal "subset_refl" Set.thy "A <= A" |
105 qed_goal "subset_refl" (the_context ()) "A <= A" |
117 (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); |
106 (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]); |
118 |
107 |
119 Goal "[| A<=B; B<=C |] ==> A<=C"; |
108 Goal "[| A<=B; B<=C |] ==> A<=C"; |
120 by (rtac subsetI 1); |
109 by (rtac subsetI 1); |
121 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1)); |
110 by (REPEAT (eresolve_tac [asm_rl, subsetD] 1)); |
123 |
112 |
124 |
113 |
125 (*** Rules for equality ***) |
114 (*** Rules for equality ***) |
126 |
115 |
127 (*Anti-symmetry of the subset relation*) |
116 (*Anti-symmetry of the subset relation*) |
128 val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = B"; |
117 val prems = goal (the_context ()) "[| A <= B; B <= A |] ==> A = B"; |
129 by (rtac (iffI RS set_ext) 1); |
118 by (rtac (iffI RS set_ext) 1); |
130 by (REPEAT (ares_tac (prems RL [subsetD]) 1)); |
119 by (REPEAT (ares_tac (prems RL [subsetD]) 1)); |
131 qed "subset_antisym"; |
120 qed "subset_antisym"; |
132 val equalityI = subset_antisym; |
121 val equalityI = subset_antisym; |
133 |
122 |
134 (* Equality rules from ZF set theory -- are they appropriate here? *) |
123 (* Equality rules from ZF set theory -- are they appropriate here? *) |
135 val prems = goal Set.thy "A = B ==> A<=B"; |
124 val prems = goal (the_context ()) "A = B ==> A<=B"; |
136 by (resolve_tac (prems RL [subst]) 1); |
125 by (resolve_tac (prems RL [subst]) 1); |
137 by (rtac subset_refl 1); |
126 by (rtac subset_refl 1); |
138 qed "equalityD1"; |
127 qed "equalityD1"; |
139 |
128 |
140 val prems = goal Set.thy "A = B ==> B<=A"; |
129 val prems = goal (the_context ()) "A = B ==> B<=A"; |
141 by (resolve_tac (prems RL [subst]) 1); |
130 by (resolve_tac (prems RL [subst]) 1); |
142 by (rtac subset_refl 1); |
131 by (rtac subset_refl 1); |
143 qed "equalityD2"; |
132 qed "equalityD2"; |
144 |
133 |
145 val prems = goal Set.thy |
134 val prems = goal (the_context ()) |
146 "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"; |
135 "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"; |
147 by (resolve_tac prems 1); |
136 by (resolve_tac prems 1); |
148 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); |
137 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1)); |
149 qed "equalityE"; |
138 qed "equalityE"; |
150 |
139 |
151 val major::prems = goal Set.thy |
140 val major::prems = goal (the_context ()) |
152 "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"; |
141 "[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"; |
153 by (rtac (major RS equalityE) 1); |
142 by (rtac (major RS equalityE) 1); |
154 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); |
143 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)); |
155 qed "equalityCE"; |
144 qed "equalityCE"; |
156 |
145 |
157 (*Lemma for creating induction formulae -- for "pattern matching" on p |
146 (*Lemma for creating induction formulae -- for "pattern matching" on p |
158 To make the induction hypotheses usable, apply "spec" or "bspec" to |
147 To make the induction hypotheses usable, apply "spec" or "bspec" to |
159 put universal quantifiers over the free variables in p. *) |
148 put universal quantifiers over the free variables in p. *) |
160 val prems = goal Set.thy |
149 val prems = goal (the_context ()) |
161 "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; |
150 "[| p:A; !!z. z:A ==> p=z --> R |] ==> R"; |
162 by (rtac mp 1); |
151 by (rtac mp 1); |
163 by (REPEAT (resolve_tac (refl::prems) 1)); |
152 by (REPEAT (resolve_tac (refl::prems) 1)); |
164 qed "setup_induction"; |
153 qed "setup_induction"; |
165 |
154 |
167 by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1)); |
156 by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1)); |
168 qed "trivial_set"; |
157 qed "trivial_set"; |
169 |
158 |
170 (*** Rules for binary union -- Un ***) |
159 (*** Rules for binary union -- Un ***) |
171 |
160 |
172 val prems = goalw Set.thy [Un_def] "c:A ==> c : A Un B"; |
161 val prems = goalw (the_context ()) [Un_def] "c:A ==> c : A Un B"; |
173 by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1)); |
162 by (REPEAT (resolve_tac (prems @ [CollectI,disjI1]) 1)); |
174 qed "UnI1"; |
163 qed "UnI1"; |
175 |
164 |
176 val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B"; |
165 val prems = goalw (the_context ()) [Un_def] "c:B ==> c : A Un B"; |
177 by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1)); |
166 by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1)); |
178 qed "UnI2"; |
167 qed "UnI2"; |
179 |
168 |
180 (*Classical introduction rule: no commitment to A vs B*) |
169 (*Classical introduction rule: no commitment to A vs B*) |
181 qed_goal "UnCI" Set.thy "(~c:B ==> c:A) ==> c : A Un B" |
170 qed_goal "UnCI" (the_context ()) "(~c:B ==> c:A) ==> c : A Un B" |
182 (fn prems=> |
171 (fn prems=> |
183 [ (rtac classical 1), |
172 [ (rtac classical 1), |
184 (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), |
173 (REPEAT (ares_tac (prems@[UnI1,notI]) 1)), |
185 (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]); |
174 (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]); |
186 |
175 |
187 val major::prems = goalw Set.thy [Un_def] |
176 val major::prems = goalw (the_context ()) [Un_def] |
188 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; |
177 "[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P"; |
189 by (rtac (major RS CollectD RS disjE) 1); |
178 by (rtac (major RS CollectD RS disjE) 1); |
190 by (REPEAT (eresolve_tac prems 1)); |
179 by (REPEAT (eresolve_tac prems 1)); |
191 qed "UnE"; |
180 qed "UnE"; |
192 |
181 |
193 |
182 |
194 (*** Rules for small intersection -- Int ***) |
183 (*** Rules for small intersection -- Int ***) |
195 |
184 |
196 val prems = goalw Set.thy [Int_def] |
185 val prems = goalw (the_context ()) [Int_def] |
197 "[| c:A; c:B |] ==> c : A Int B"; |
186 "[| c:A; c:B |] ==> c : A Int B"; |
198 by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)); |
187 by (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)); |
199 qed "IntI"; |
188 qed "IntI"; |
200 |
189 |
201 val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:A"; |
190 val [major] = goalw (the_context ()) [Int_def] "c : A Int B ==> c:A"; |
202 by (rtac (major RS CollectD RS conjunct1) 1); |
191 by (rtac (major RS CollectD RS conjunct1) 1); |
203 qed "IntD1"; |
192 qed "IntD1"; |
204 |
193 |
205 val [major] = goalw Set.thy [Int_def] "c : A Int B ==> c:B"; |
194 val [major] = goalw (the_context ()) [Int_def] "c : A Int B ==> c:B"; |
206 by (rtac (major RS CollectD RS conjunct2) 1); |
195 by (rtac (major RS CollectD RS conjunct2) 1); |
207 qed "IntD2"; |
196 qed "IntD2"; |
208 |
197 |
209 val [major,minor] = goal Set.thy |
198 val [major,minor] = goal (the_context ()) |
210 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; |
199 "[| c : A Int B; [| c:A; c:B |] ==> P |] ==> P"; |
211 by (rtac minor 1); |
200 by (rtac minor 1); |
212 by (rtac (major RS IntD1) 1); |
201 by (rtac (major RS IntD1) 1); |
213 by (rtac (major RS IntD2) 1); |
202 by (rtac (major RS IntD2) 1); |
214 qed "IntE"; |
203 qed "IntE"; |
215 |
204 |
216 |
205 |
217 (*** Rules for set complement -- Compl ***) |
206 (*** Rules for set complement -- Compl ***) |
218 |
207 |
219 val prems = goalw Set.thy [Compl_def] |
208 val prems = goalw (the_context ()) [Compl_def] |
220 "[| c:A ==> False |] ==> c : Compl(A)"; |
209 "[| c:A ==> False |] ==> c : Compl(A)"; |
221 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); |
210 by (REPEAT (ares_tac (prems @ [CollectI,notI]) 1)); |
222 qed "ComplI"; |
211 qed "ComplI"; |
223 |
212 |
224 (*This form, with negated conclusion, works well with the Classical prover. |
213 (*This form, with negated conclusion, works well with the Classical prover. |
225 Negated assumptions behave like formulae on the right side of the notional |
214 Negated assumptions behave like formulae on the right side of the notional |
226 turnstile...*) |
215 turnstile...*) |
227 val major::prems = goalw Set.thy [Compl_def] |
216 val major::prems = goalw (the_context ()) [Compl_def] |
228 "[| c : Compl(A) |] ==> ~c:A"; |
217 "[| c : Compl(A) |] ==> ~c:A"; |
229 by (rtac (major RS CollectD) 1); |
218 by (rtac (major RS CollectD) 1); |
230 qed "ComplD"; |
219 qed "ComplD"; |
231 |
220 |
232 val ComplE = make_elim ComplD; |
221 val ComplE = make_elim ComplD; |
255 Goalw [singleton_def] "a : {a}"; |
244 Goalw [singleton_def] "a : {a}"; |
256 by (rtac CollectI 1); |
245 by (rtac CollectI 1); |
257 by (rtac refl 1); |
246 by (rtac refl 1); |
258 qed "singletonI"; |
247 qed "singletonI"; |
259 |
248 |
260 val [major] = goalw Set.thy [singleton_def] "b : {a} ==> b=a"; |
249 val [major] = goalw (the_context ()) [singleton_def] "b : {a} ==> b=a"; |
261 by (rtac (major RS CollectD) 1); |
250 by (rtac (major RS CollectD) 1); |
262 qed "singletonD"; |
251 qed "singletonD"; |
263 |
252 |
264 val singletonE = make_elim singletonD; |
253 val singletonE = make_elim singletonD; |
265 |
254 |
266 (*** Unions of families ***) |
255 (*** Unions of families ***) |
267 |
256 |
268 (*The order of the premises presupposes that A is rigid; b may be flexible*) |
257 (*The order of the premises presupposes that A is rigid; b may be flexible*) |
269 val prems = goalw Set.thy [UNION_def] |
258 val prems = goalw (the_context ()) [UNION_def] |
270 "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))"; |
259 "[| a:A; b: B(a) |] ==> b: (UN x:A. B(x))"; |
271 by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1)); |
260 by (REPEAT (resolve_tac (prems @ [bexI,CollectI]) 1)); |
272 qed "UN_I"; |
261 qed "UN_I"; |
273 |
262 |
274 val major::prems = goalw Set.thy [UNION_def] |
263 val major::prems = goalw (the_context ()) [UNION_def] |
275 "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R"; |
264 "[| b : (UN x:A. B(x)); !!x.[| x:A; b: B(x) |] ==> R |] ==> R"; |
276 by (rtac (major RS CollectD RS bexE) 1); |
265 by (rtac (major RS CollectD RS bexE) 1); |
277 by (REPEAT (ares_tac prems 1)); |
266 by (REPEAT (ares_tac prems 1)); |
278 qed "UN_E"; |
267 qed "UN_E"; |
279 |
268 |
280 val prems = goal Set.thy |
269 val prems = goal (the_context ()) |
281 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ |
270 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ |
282 \ (UN x:A. C(x)) = (UN x:B. D(x))"; |
271 \ (UN x:A. C(x)) = (UN x:B. D(x))"; |
283 by (REPEAT (etac UN_E 1 |
272 by (REPEAT (etac UN_E 1 |
284 ORELSE ares_tac ([UN_I,equalityI,subsetI] @ |
273 ORELSE ares_tac ([UN_I,equalityI,subsetI] @ |
285 (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); |
274 (prems RL [equalityD1,equalityD2] RL [subsetD])) 1)); |
286 qed "UN_cong"; |
275 qed "UN_cong"; |
287 |
276 |
288 (*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *) |
277 (*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *) |
289 |
278 |
290 val prems = goalw Set.thy [INTER_def] |
279 val prems = goalw (the_context ()) [INTER_def] |
291 "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; |
280 "(!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))"; |
292 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); |
281 by (REPEAT (ares_tac ([CollectI,ballI] @ prems) 1)); |
293 qed "INT_I"; |
282 qed "INT_I"; |
294 |
283 |
295 val major::prems = goalw Set.thy [INTER_def] |
284 val major::prems = goalw (the_context ()) [INTER_def] |
296 "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; |
285 "[| b : (INT x:A. B(x)); a:A |] ==> b: B(a)"; |
297 by (rtac (major RS CollectD RS bspec) 1); |
286 by (rtac (major RS CollectD RS bspec) 1); |
298 by (resolve_tac prems 1); |
287 by (resolve_tac prems 1); |
299 qed "INT_D"; |
288 qed "INT_D"; |
300 |
289 |
301 (*"Classical" elimination rule -- does not require proving X:C *) |
290 (*"Classical" elimination rule -- does not require proving X:C *) |
302 val major::prems = goalw Set.thy [INTER_def] |
291 val major::prems = goalw (the_context ()) [INTER_def] |
303 "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R"; |
292 "[| b : (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R"; |
304 by (rtac (major RS CollectD RS ballE) 1); |
293 by (rtac (major RS CollectD RS ballE) 1); |
305 by (REPEAT (eresolve_tac prems 1)); |
294 by (REPEAT (eresolve_tac prems 1)); |
306 qed "INT_E"; |
295 qed "INT_E"; |
307 |
296 |
308 val prems = goal Set.thy |
297 val prems = goal (the_context ()) |
309 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ |
298 "[| A=B; !!x. x:B ==> C(x) = D(x) |] ==> \ |
310 \ (INT x:A. C(x)) = (INT x:B. D(x))"; |
299 \ (INT x:A. C(x)) = (INT x:B. D(x))"; |
311 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); |
300 by (REPEAT_FIRST (resolve_tac [INT_I,equalityI,subsetI])); |
312 by (REPEAT (dtac INT_D 1 |
301 by (REPEAT (dtac INT_D 1 |
313 ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); |
302 ORELSE ares_tac (prems RL [equalityD1,equalityD2] RL [subsetD]) 1)); |
314 qed "INT_cong"; |
303 qed "INT_cong"; |
315 |
304 |
316 (*** Rules for Unions ***) |
305 (*** Rules for Unions ***) |
317 |
306 |
318 (*The order of the premises presupposes that C is rigid; A may be flexible*) |
307 (*The order of the premises presupposes that C is rigid; A may be flexible*) |
319 val prems = goalw Set.thy [Union_def] |
308 val prems = goalw (the_context ()) [Union_def] |
320 "[| X:C; A:X |] ==> A : Union(C)"; |
309 "[| X:C; A:X |] ==> A : Union(C)"; |
321 by (REPEAT (resolve_tac (prems @ [UN_I]) 1)); |
310 by (REPEAT (resolve_tac (prems @ [UN_I]) 1)); |
322 qed "UnionI"; |
311 qed "UnionI"; |
323 |
312 |
324 val major::prems = goalw Set.thy [Union_def] |
313 val major::prems = goalw (the_context ()) [Union_def] |
325 "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; |
314 "[| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R"; |
326 by (rtac (major RS UN_E) 1); |
315 by (rtac (major RS UN_E) 1); |
327 by (REPEAT (ares_tac prems 1)); |
316 by (REPEAT (ares_tac prems 1)); |
328 qed "UnionE"; |
317 qed "UnionE"; |
329 |
318 |
330 (*** Rules for Inter ***) |
319 (*** Rules for Inter ***) |
331 |
320 |
332 val prems = goalw Set.thy [Inter_def] |
321 val prems = goalw (the_context ()) [Inter_def] |
333 "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; |
322 "[| !!X. X:C ==> A:X |] ==> A : Inter(C)"; |
334 by (REPEAT (ares_tac ([INT_I] @ prems) 1)); |
323 by (REPEAT (ares_tac ([INT_I] @ prems) 1)); |
335 qed "InterI"; |
324 qed "InterI"; |
336 |
325 |
337 (*A "destruct" rule -- every X in C contains A as an element, but |
326 (*A "destruct" rule -- every X in C contains A as an element, but |
338 A:X can hold when X:C does not! This rule is analogous to "spec". *) |
327 A:X can hold when X:C does not! This rule is analogous to "spec". *) |
339 val major::prems = goalw Set.thy [Inter_def] |
328 val major::prems = goalw (the_context ()) [Inter_def] |
340 "[| A : Inter(C); X:C |] ==> A:X"; |
329 "[| A : Inter(C); X:C |] ==> A:X"; |
341 by (rtac (major RS INT_D) 1); |
330 by (rtac (major RS INT_D) 1); |
342 by (resolve_tac prems 1); |
331 by (resolve_tac prems 1); |
343 qed "InterD"; |
332 qed "InterD"; |
344 |
333 |
345 (*"Classical" elimination rule -- does not require proving X:C *) |
334 (*"Classical" elimination rule -- does not require proving X:C *) |
346 val major::prems = goalw Set.thy [Inter_def] |
335 val major::prems = goalw (the_context ()) [Inter_def] |
347 "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R"; |
336 "[| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R"; |
348 by (rtac (major RS INT_E) 1); |
337 by (rtac (major RS INT_E) 1); |
349 by (REPEAT (eresolve_tac prems 1)); |
338 by (REPEAT (eresolve_tac prems 1)); |
350 qed "InterE"; |
339 qed "InterE"; |