src/ZF/QPair.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 55 331d93292ee0
equal deleted inserted replaced
5:75e163863e16 6:8ce8c4d13d4d
    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