72 [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); |
72 [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]); |
73 |
73 |
74 val QSigma_cong = prove_goalw QPair.thy [QSigma_def] |
74 val QSigma_cong = prove_goalw QPair.thy [QSigma_def] |
75 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
75 "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \ |
76 \ QSigma(A,B) = QSigma(A',B')" |
76 \ QSigma(A,B) = QSigma(A',B')" |
77 (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]); |
77 (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]); |
78 |
78 |
79 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0" |
79 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0" |
80 (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]); |
80 (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]); |
81 |
81 |
82 val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0" |
82 val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0" |
95 \ |] ==> qsplit(%x y.c(x,y), p) : C(p)" |
95 \ |] ==> qsplit(%x y.c(x,y), p) : C(p)" |
96 (fn major::prems=> |
96 (fn major::prems=> |
97 [ (rtac (major RS QSigmaE) 1), |
97 [ (rtac (major RS QSigmaE) 1), |
98 (etac ssubst 1), |
98 (etac ssubst 1), |
99 (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]); |
99 (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]); |
100 |
|
101 (*This congruence rule uses NO typing information...*) |
|
102 val qsplit_cong = prove_goalw QPair.thy [qsplit_def] |
|
103 "[| p=p'; !!x y.c(x,y) = c'(x,y) |] ==> \ |
|
104 \ qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')" |
|
105 (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]); |
|
106 |
100 |
107 |
101 |
108 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject]; |
102 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject]; |
109 |
103 |
110 (*** qconverse ***) |
104 (*** qconverse ***) |
241 goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D"; |
235 goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D"; |
242 by (fast_tac qsum_cs 1); |
236 by (fast_tac qsum_cs 1); |
243 val qsum_subset_iff = result(); |
237 val qsum_subset_iff = result(); |
244 |
238 |
245 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D"; |
239 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D"; |
246 by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1); |
240 by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1); |
247 by (fast_tac ZF_cs 1); |
241 by (fast_tac ZF_cs 1); |
248 val qsum_equal_iff = result(); |
242 val qsum_equal_iff = result(); |
249 |
243 |
250 (*** Eliminator -- qcase ***) |
244 (*** Eliminator -- qcase ***) |
251 |
245 |
256 |
250 |
257 goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)"; |
251 goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)"; |
258 by (rtac (qsplit RS trans) 1); |
252 by (rtac (qsplit RS trans) 1); |
259 by (rtac cond_1 1); |
253 by (rtac cond_1 1); |
260 val qcase_QInr = result(); |
254 val qcase_QInr = result(); |
261 |
|
262 val prems = goalw QPair.thy [qcase_def] |
|
263 "[| u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) |] ==> \ |
|
264 \ qcase(c,d,u)=qcase(c',d',u')"; |
|
265 by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1)); |
|
266 val qcase_cong = result(); |
|
267 |
255 |
268 val major::prems = goal QPair.thy |
256 val major::prems = goal QPair.thy |
269 "[| u: A <+> B; \ |
257 "[| u: A <+> B; \ |
270 \ !!x. x: A ==> c(x): C(QInl(x)); \ |
258 \ !!x. x: A ==> c(x): C(QInl(x)); \ |
271 \ !!y. y: B ==> d(y): C(QInr(y)) \ |
259 \ !!y. y: B ==> d(y): C(QInr(y)) \ |
272 \ |] ==> qcase(c,d,u) : C(u)"; |
260 \ |] ==> qcase(c,d,u) : C(u)"; |
273 by (rtac (major RS qsumE) 1); |
261 by (rtac (major RS qsumE) 1); |
274 by (ALLGOALS (etac ssubst)); |
262 by (ALLGOALS (etac ssubst)); |
275 by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews |
263 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
276 (prems@[qcase_QInl,qcase_QInr])))); |
264 (prems@[qcase_QInl,qcase_QInr])))); |
277 val qcase_type = result(); |
265 val qcase_type = result(); |
278 |
266 |
279 (** Rules for the Part primitive **) |
267 (** Rules for the Part primitive **) |
280 |
268 |