23 |
23 |
24 (**** Quine ordered pairing ****) |
24 (**** Quine ordered pairing ****) |
25 |
25 |
26 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
26 (** Lemmas for showing that <a;b> uniquely determines a and b **) |
27 |
27 |
28 val QPair_iff = prove_goalw QPair.thy [QPair_def] |
28 qed_goalw "QPair_iff" QPair.thy [QPair_def] |
29 "<a;b> = <c;d> <-> a=c & b=d" |
29 "<a;b> = <c;d> <-> a=c & b=d" |
30 (fn _=> [rtac sum_equal_iff 1]); |
30 (fn _=> [rtac sum_equal_iff 1]); |
31 |
31 |
32 val QPair_inject = standard (QPair_iff RS iffD1 RS conjE); |
32 val QPair_inject = standard (QPair_iff RS iffD1 RS conjE); |
33 |
33 |
34 val QPair_inject1 = prove_goal QPair.thy "<a;b> = <c;d> ==> a=c" |
34 qed_goal "QPair_inject1" QPair.thy "<a;b> = <c;d> ==> a=c" |
35 (fn [major]=> |
35 (fn [major]=> |
36 [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); |
36 [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); |
37 |
37 |
38 val QPair_inject2 = prove_goal QPair.thy "<a;b> = <c;d> ==> b=d" |
38 qed_goal "QPair_inject2" QPair.thy "<a;b> = <c;d> ==> b=d" |
39 (fn [major]=> |
39 (fn [major]=> |
40 [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); |
40 [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]); |
41 |
41 |
42 |
42 |
43 (*** QSigma: Disjoint union of a family of sets |
43 (*** QSigma: Disjoint union of a family of sets |
44 Generalizes Cartesian product ***) |
44 Generalizes Cartesian product ***) |
45 |
45 |
46 val QSigmaI = prove_goalw QPair.thy [QSigma_def] |
46 qed_goalw "QSigmaI" QPair.thy [QSigma_def] |
47 "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)" |
47 "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)" |
48 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); |
48 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]); |
49 |
49 |
50 (*The general elimination rule*) |
50 (*The general elimination rule*) |
51 val QSigmaE = prove_goalw QPair.thy [QSigma_def] |
51 qed_goalw "QSigmaE" QPair.thy [QSigma_def] |
52 "[| c: QSigma(A,B); \ |
52 "[| c: QSigma(A,B); \ |
53 \ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P \ |
53 \ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P \ |
54 \ |] ==> P" |
54 \ |] ==> P" |
55 (fn major::prems=> |
55 (fn major::prems=> |
56 [ (cut_facts_tac [major] 1), |
56 [ (cut_facts_tac [major] 1), |
61 val QSigmaE2 = |
61 val QSigmaE2 = |
62 rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac) |
62 rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac) |
63 THEN prune_params_tac) |
63 THEN prune_params_tac) |
64 (read_instantiate [("c","<a;b>")] QSigmaE); |
64 (read_instantiate [("c","<a;b>")] QSigmaE); |
65 |
65 |
66 val QSigmaD1 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> a : A" |
66 qed_goal "QSigmaD1" QPair.thy "<a;b> : QSigma(A,B) ==> a : A" |
67 (fn [major]=> |
67 (fn [major]=> |
68 [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); |
68 [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); |
69 |
69 |
70 val QSigmaD2 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)" |
70 qed_goal "QSigmaD2" QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)" |
71 (fn [major]=> |
71 (fn [major]=> |
72 [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); |
72 [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); |
73 |
73 |
74 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject]; |
74 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject]; |
75 |
75 |
76 |
76 |
77 val QSigma_cong = prove_goalw QPair.thy [QSigma_def] |
77 qed_goalw "QSigma_cong" QPair.thy [QSigma_def] |
78 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
78 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
79 \ QSigma(A,B) = QSigma(A',B')" |
79 \ QSigma(A,B) = QSigma(A',B')" |
80 (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]); |
80 (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]); |
81 |
81 |
82 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0" |
82 qed_goal "QSigma_empty1" QPair.thy "QSigma(0,B) = 0" |
83 (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]); |
83 (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]); |
84 |
84 |
85 val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0" |
85 qed_goal "QSigma_empty2" QPair.thy "A <*> 0 = 0" |
86 (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]); |
86 (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]); |
87 |
87 |
88 |
88 |
89 (*** Eliminator - qsplit ***) |
89 (*** Eliminator - qsplit ***) |
90 |
90 |
91 val qsplit = prove_goalw QPair.thy [qsplit_def] |
91 qed_goalw "qsplit" QPair.thy [qsplit_def] |
92 "qsplit(%x y.c(x,y), <a;b>) = c(a,b)" |
92 "qsplit(%x y.c(x,y), <a;b>) = c(a,b)" |
93 (fn _ => [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]); |
93 (fn _ => [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]); |
94 |
94 |
95 val qsplit_type = prove_goal QPair.thy |
95 qed_goal "qsplit_type" QPair.thy |
96 "[| p:QSigma(A,B); \ |
96 "[| p:QSigma(A,B); \ |
97 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \ |
97 \ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \ |
98 \ |] ==> qsplit(%x y.c(x,y), p) : C(p)" |
98 \ |] ==> qsplit(%x y.c(x,y), p) : C(p)" |
99 (fn major::prems=> |
99 (fn major::prems=> |
100 [ (rtac (major RS QSigmaE) 1), |
100 [ (rtac (major RS QSigmaE) 1), |
102 (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]); |
102 (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]); |
103 |
103 |
104 |
104 |
105 (*** qconverse ***) |
105 (*** qconverse ***) |
106 |
106 |
107 val qconverseI = prove_goalw QPair.thy [qconverse_def] |
107 qed_goalw "qconverseI" QPair.thy [qconverse_def] |
108 "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)" |
108 "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)" |
109 (fn _ => [ (fast_tac qpair_cs 1) ]); |
109 (fn _ => [ (fast_tac qpair_cs 1) ]); |
110 |
110 |
111 val qconverseD = prove_goalw QPair.thy [qconverse_def] |
111 qed_goalw "qconverseD" QPair.thy [qconverse_def] |
112 "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r" |
112 "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r" |
113 (fn _ => [ (fast_tac qpair_cs 1) ]); |
113 (fn _ => [ (fast_tac qpair_cs 1) ]); |
114 |
114 |
115 val qconverseE = prove_goalw QPair.thy [qconverse_def] |
115 qed_goalw "qconverseE" QPair.thy [qconverse_def] |
116 "[| yx : qconverse(r); \ |
116 "[| yx : qconverse(r); \ |
117 \ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P \ |
117 \ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P \ |
118 \ |] ==> P" |
118 \ |] ==> P" |
119 (fn [major,minor]=> |
119 (fn [major,minor]=> |
120 [ (rtac (major RS ReplaceE) 1), |
120 [ (rtac (major RS ReplaceE) 1), |
123 (assume_tac 1) ]); |
123 (assume_tac 1) ]); |
124 |
124 |
125 val qconverse_cs = qpair_cs addSIs [qconverseI] |
125 val qconverse_cs = qpair_cs addSIs [qconverseI] |
126 addSEs [qconverseD,qconverseE]; |
126 addSEs [qconverseD,qconverseE]; |
127 |
127 |
128 val qconverse_of_qconverse = prove_goal QPair.thy |
128 qed_goal "qconverse_of_qconverse" QPair.thy |
129 "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" |
129 "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r" |
130 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); |
130 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); |
131 |
131 |
132 val qconverse_type = prove_goal QPair.thy |
132 qed_goal "qconverse_type" QPair.thy |
133 "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A" |
133 "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A" |
134 (fn _ => [ (fast_tac qconverse_cs 1) ]); |
134 (fn _ => [ (fast_tac qconverse_cs 1) ]); |
135 |
135 |
136 val qconverse_of_prod = prove_goal QPair.thy "qconverse(A <*> B) = B <*> A" |
136 qed_goal "qconverse_of_prod" QPair.thy "qconverse(A <*> B) = B <*> A" |
137 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); |
137 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); |
138 |
138 |
139 val qconverse_empty = prove_goal QPair.thy "qconverse(0) = 0" |
139 qed_goal "qconverse_empty" QPair.thy "qconverse(0) = 0" |
140 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); |
140 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]); |
141 |
141 |
142 |
142 |
143 (*** qsplit for predicates: result type o ***) |
143 (*** qsplit for predicates: result type o ***) |
144 |
144 |
145 goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)"; |
145 goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)"; |
146 by (REPEAT (ares_tac [refl,exI,conjI] 1)); |
146 by (REPEAT (ares_tac [refl,exI,conjI] 1)); |
147 val qfsplitI = result(); |
147 qed "qfsplitI"; |
148 |
148 |
149 val major::prems = goalw QPair.thy [qfsplit_def] |
149 val major::prems = goalw QPair.thy [qfsplit_def] |
150 "[| qfsplit(R,z); !!x y. [| z = <x;y>; R(x,y) |] ==> P |] ==> P"; |
150 "[| qfsplit(R,z); !!x y. [| z = <x;y>; R(x,y) |] ==> P |] ==> P"; |
151 by (cut_facts_tac [major] 1); |
151 by (cut_facts_tac [major] 1); |
152 by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1)); |
152 by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1)); |
153 val qfsplitE = result(); |
153 qed "qfsplitE"; |
154 |
154 |
155 goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)"; |
155 goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)"; |
156 by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1)); |
156 by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1)); |
157 val qfsplitD = result(); |
157 qed "qfsplitD"; |
158 |
158 |
159 |
159 |
160 (**** The Quine-inspired notion of disjoint sum ****) |
160 (**** The Quine-inspired notion of disjoint sum ****) |
161 |
161 |
162 val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def]; |
162 val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def]; |
163 |
163 |
164 (** Introduction rules for the injections **) |
164 (** Introduction rules for the injections **) |
165 |
165 |
166 goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B"; |
166 goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B"; |
167 by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1)); |
167 by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1)); |
168 val QInlI = result(); |
168 qed "QInlI"; |
169 |
169 |
170 goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B"; |
170 goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B"; |
171 by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1)); |
171 by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1)); |
172 val QInrI = result(); |
172 qed "QInrI"; |
173 |
173 |
174 (** Elimination rules **) |
174 (** Elimination rules **) |
175 |
175 |
176 val major::prems = goalw QPair.thy qsum_defs |
176 val major::prems = goalw QPair.thy qsum_defs |
177 "[| u: A <+> B; \ |
177 "[| u: A <+> B; \ |
179 \ !!y. [| y:B; u=QInr(y) |] ==> P \ |
179 \ !!y. [| y:B; u=QInr(y) |] ==> P \ |
180 \ |] ==> P"; |
180 \ |] ==> P"; |
181 by (rtac (major RS UnE) 1); |
181 by (rtac (major RS UnE) 1); |
182 by (REPEAT (rtac refl 1 |
182 by (REPEAT (rtac refl 1 |
183 ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1)); |
183 ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1)); |
184 val qsumE = result(); |
184 qed "qsumE"; |
185 |
185 |
186 (** Injection and freeness equivalences, for rewriting **) |
186 (** Injection and freeness equivalences, for rewriting **) |
187 |
187 |
188 goalw QPair.thy qsum_defs "QInl(a)=QInl(b) <-> a=b"; |
188 goalw QPair.thy qsum_defs "QInl(a)=QInl(b) <-> a=b"; |
189 by (simp_tac (ZF_ss addsimps [QPair_iff]) 1); |
189 by (simp_tac (ZF_ss addsimps [QPair_iff]) 1); |
190 val QInl_iff = result(); |
190 qed "QInl_iff"; |
191 |
191 |
192 goalw QPair.thy qsum_defs "QInr(a)=QInr(b) <-> a=b"; |
192 goalw QPair.thy qsum_defs "QInr(a)=QInr(b) <-> a=b"; |
193 by (simp_tac (ZF_ss addsimps [QPair_iff]) 1); |
193 by (simp_tac (ZF_ss addsimps [QPair_iff]) 1); |
194 val QInr_iff = result(); |
194 qed "QInr_iff"; |
195 |
195 |
196 goalw QPair.thy qsum_defs "QInl(a)=QInr(b) <-> False"; |
196 goalw QPair.thy qsum_defs "QInl(a)=QInr(b) <-> False"; |
197 by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1); |
197 by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1); |
198 val QInl_QInr_iff = result(); |
198 qed "QInl_QInr_iff"; |
199 |
199 |
200 goalw QPair.thy qsum_defs "QInr(b)=QInl(a) <-> False"; |
200 goalw QPair.thy qsum_defs "QInr(b)=QInl(a) <-> False"; |
201 by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1); |
201 by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1); |
202 val QInr_QInl_iff = result(); |
202 qed "QInr_QInl_iff"; |
203 |
203 |
204 (*Injection and freeness rules*) |
204 (*Injection and freeness rules*) |
205 |
205 |
206 val QInl_inject = standard (QInl_iff RS iffD1); |
206 val QInl_inject = standard (QInl_iff RS iffD1); |
207 val QInr_inject = standard (QInr_iff RS iffD1); |
207 val QInr_inject = standard (QInr_iff RS iffD1); |
213 addSEs [PartE, qsumE, QInl_neq_QInr, QInr_neq_QInl] |
213 addSEs [PartE, qsumE, QInl_neq_QInr, QInr_neq_QInl] |
214 addSDs [QInl_inject, QInr_inject]; |
214 addSDs [QInl_inject, QInr_inject]; |
215 |
215 |
216 goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A"; |
216 goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A"; |
217 by (fast_tac qsum_cs 1); |
217 by (fast_tac qsum_cs 1); |
218 val QInlD = result(); |
218 qed "QInlD"; |
219 |
219 |
220 goal QPair.thy "!!A B. QInr(b): A<+>B ==> b: B"; |
220 goal QPair.thy "!!A B. QInr(b): A<+>B ==> b: B"; |
221 by (fast_tac qsum_cs 1); |
221 by (fast_tac qsum_cs 1); |
222 val QInrD = result(); |
222 qed "QInrD"; |
223 |
223 |
224 (** <+> is itself injective... who cares?? **) |
224 (** <+> is itself injective... who cares?? **) |
225 |
225 |
226 goal QPair.thy |
226 goal QPair.thy |
227 "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"; |
227 "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"; |
228 by (fast_tac qsum_cs 1); |
228 by (fast_tac qsum_cs 1); |
229 val qsum_iff = result(); |
229 qed "qsum_iff"; |
230 |
230 |
231 goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D"; |
231 goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D"; |
232 by (fast_tac qsum_cs 1); |
232 by (fast_tac qsum_cs 1); |
233 val qsum_subset_iff = result(); |
233 qed "qsum_subset_iff"; |
234 |
234 |
235 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D"; |
235 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D"; |
236 by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1); |
236 by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1); |
237 by (fast_tac ZF_cs 1); |
237 by (fast_tac ZF_cs 1); |
238 val qsum_equal_iff = result(); |
238 qed "qsum_equal_iff"; |
239 |
239 |
240 (*** Eliminator -- qcase ***) |
240 (*** Eliminator -- qcase ***) |
241 |
241 |
242 goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)"; |
242 goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)"; |
243 by (rtac (qsplit RS trans) 1); |
243 by (rtac (qsplit RS trans) 1); |
244 by (rtac cond_0 1); |
244 by (rtac cond_0 1); |
245 val qcase_QInl = result(); |
245 qed "qcase_QInl"; |
246 |
246 |
247 goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)"; |
247 goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)"; |
248 by (rtac (qsplit RS trans) 1); |
248 by (rtac (qsplit RS trans) 1); |
249 by (rtac cond_1 1); |
249 by (rtac cond_1 1); |
250 val qcase_QInr = result(); |
250 qed "qcase_QInr"; |
251 |
251 |
252 val major::prems = goal QPair.thy |
252 val major::prems = goal QPair.thy |
253 "[| u: A <+> B; \ |
253 "[| u: A <+> B; \ |
254 \ !!x. x: A ==> c(x): C(QInl(x)); \ |
254 \ !!x. x: A ==> c(x): C(QInl(x)); \ |
255 \ !!y. y: B ==> d(y): C(QInr(y)) \ |
255 \ !!y. y: B ==> d(y): C(QInr(y)) \ |
256 \ |] ==> qcase(c,d,u) : C(u)"; |
256 \ |] ==> qcase(c,d,u) : C(u)"; |
257 by (rtac (major RS qsumE) 1); |
257 by (rtac (major RS qsumE) 1); |
258 by (ALLGOALS (etac ssubst)); |
258 by (ALLGOALS (etac ssubst)); |
259 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
259 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
260 (prems@[qcase_QInl,qcase_QInr])))); |
260 (prems@[qcase_QInl,qcase_QInr])))); |
261 val qcase_type = result(); |
261 qed "qcase_type"; |
262 |
262 |
263 (** Rules for the Part primitive **) |
263 (** Rules for the Part primitive **) |
264 |
264 |
265 goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}"; |
265 goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}"; |
266 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
266 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
267 val Part_QInl = result(); |
267 qed "Part_QInl"; |
268 |
268 |
269 goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}"; |
269 goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}"; |
270 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
270 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
271 val Part_QInr = result(); |
271 qed "Part_QInr"; |
272 |
272 |
273 goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}"; |
273 goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}"; |
274 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
274 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
275 val Part_QInr2 = result(); |
275 qed "Part_QInr2"; |
276 |
276 |
277 goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"; |
277 goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"; |
278 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
278 by (fast_tac (qsum_cs addIs [equalityI]) 1); |
279 val Part_qsum_equality = result(); |
279 qed "Part_qsum_equality"; |