src/ZF/QPair.ML
changeset 2469 b50b8c0eec01
parent 1461 6bcb44e4d6e5
child 2493 bdeb5024353a
equal deleted inserted replaced
2468:428efffe8599 2469:b50b8c0eec01
    22 
    22 
    23 (**** Quine ordered pairing ****)
    23 (**** Quine ordered pairing ****)
    24 
    24 
    25 (** Lemmas for showing that <a;b> uniquely determines a and b **)
    25 (** Lemmas for showing that <a;b> uniquely determines a and b **)
    26 
    26 
       
    27 qed_goalw "QPair_empty" thy [QPair_def]
       
    28     "<0;0> = 0"
       
    29  (fn _=> [Simp_tac 1]);
       
    30 
    27 qed_goalw "QPair_iff" thy [QPair_def]
    31 qed_goalw "QPair_iff" thy [QPair_def]
    28     "<a;b> = <c;d> <-> a=c & b=d"
    32     "<a;b> = <c;d> <-> a=c & b=d"
    29  (fn _=> [rtac sum_equal_iff 1]);
    33  (fn _=> [rtac sum_equal_iff 1]);
    30 
    34 
    31 bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE));
    35 bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE));
    32 
    36 
       
    37 Addsimps [QPair_empty, QPair_iff];
       
    38 AddSEs   [QPair_inject];
       
    39 
    33 qed_goal "QPair_inject1" thy "<a;b> = <c;d> ==> a=c"
    40 qed_goal "QPair_inject1" thy "<a;b> = <c;d> ==> a=c"
    34  (fn [major]=>
    41  (fn [major]=>
    35   [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
    42   [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
    36 
    43 
    37 qed_goal "QPair_inject2" thy "<a;b> = <c;d> ==> b=d"
    44 qed_goal "QPair_inject2" thy "<a;b> = <c;d> ==> b=d"
    41 
    48 
    42 (*** QSigma: Disjoint union of a family of sets
    49 (*** QSigma: Disjoint union of a family of sets
    43      Generalizes Cartesian product ***)
    50      Generalizes Cartesian product ***)
    44 
    51 
    45 qed_goalw "QSigmaI" thy [QSigma_def]
    52 qed_goalw "QSigmaI" thy [QSigma_def]
    46     "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
    53     "!!A B. [| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
    47  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
    54  (fn _ => [ Fast_tac 1 ]);
       
    55 
       
    56 AddSIs [QSigmaI];
    48 
    57 
    49 (*The general elimination rule*)
    58 (*The general elimination rule*)
    50 qed_goalw "QSigmaE" thy [QSigma_def]
    59 qed_goalw "QSigmaE" thy [QSigma_def]
    51     "[| c: QSigma(A,B);  \
    60     "[| c: QSigma(A,B);  \
    52 \       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
    61 \       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
    68 
    77 
    69 qed_goal "QSigmaD2" thy "<a;b> : QSigma(A,B) ==> b : B(a)"
    78 qed_goal "QSigmaD2" thy "<a;b> : QSigma(A,B) ==> b : B(a)"
    70  (fn [major]=>
    79  (fn [major]=>
    71   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    80   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    72 
    81 
    73 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
    82 AddSEs [QSigmaE2, QSigmaE];
    74 
    83 
    75 
    84 
    76 qed_goalw "QSigma_cong" thy [QSigma_def]
    85 qed_goalw "QSigma_cong" thy [QSigma_def]
    77     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    86     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    78 \    QSigma(A,B) = QSigma(A',B')"
    87 \    QSigma(A,B) = QSigma(A',B')"
    79  (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
    88  (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
    80 
    89 
    81 qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
    90 qed_goal "QSigma_empty1" thy "QSigma(0,B) = 0"
    82  (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]);
    91  (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
    83 
    92 
    84 qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
    93 qed_goal "QSigma_empty2" thy "A <*> 0 = 0"
    85  (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]);
    94  (fn _ => [ (fast_tac (!claset addIs [equalityI]) 1) ]);
       
    95 
       
    96 Addsimps [QSigma_empty1, QSigma_empty2];
    86 
    97 
    87 
    98 
    88 (*** Projections: qfst, qsnd ***)
    99 (*** Projections: qfst, qsnd ***)
    89 
   100 
    90 qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
   101 qed_goalw "qfst_conv" thy [qfst_def] "qfst(<a;b>) = a"
    91  (fn _=> 
   102  (fn _=> 
    92   [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]);
   103   [ (fast_tac (!claset addIs [the_equality]) 1) ]);
    93 
   104 
    94 qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
   105 qed_goalw "qsnd_conv" thy [qsnd_def] "qsnd(<a;b>) = b"
    95  (fn _=> 
   106  (fn _=> 
    96   [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]);
   107   [ (fast_tac (!claset addIs [the_equality]) 1) ]);
    97 
   108 
    98 val qpair_ss = ZF_ss addsimps [qfst_conv,qsnd_conv];
   109 Addsimps [qfst_conv, qsnd_conv];
    99 
   110 
   100 qed_goal "qfst_type" thy
   111 qed_goal "qfst_type" thy
   101     "!!p. p:QSigma(A,B) ==> qfst(p) : A"
   112     "!!p. p:QSigma(A,B) ==> qfst(p) : A"
   102  (fn _=> [ (fast_tac (qpair_cs addss qpair_ss) 1) ]);
   113  (fn _=> [ Auto_tac() ]);
   103 
   114 
   104 qed_goal "qsnd_type" thy
   115 qed_goal "qsnd_type" thy
   105     "!!p. p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
   116     "!!p. p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
   106  (fn _=> [ (fast_tac (qpair_cs addss qpair_ss) 1) ]);
   117  (fn _=> [ Auto_tac() ]);
   107 
   118 
   108 goal thy "!!a A B. a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
   119 goal thy "!!a A B. a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
   109 by (etac QSigmaE 1);
   120 by (Auto_tac());
   110 by (asm_simp_tac qpair_ss 1);
       
   111 qed "QPair_qfst_qsnd_eq";
   121 qed "QPair_qfst_qsnd_eq";
   112 
   122 
   113 
   123 
   114 (*** Eliminator - qsplit ***)
   124 (*** Eliminator - qsplit ***)
   115 
   125 
   116 (*A META-equality, so that it applies to higher types as well...*)
   126 (*A META-equality, so that it applies to higher types as well...*)
   117 qed_goalw "qsplit" thy [qsplit_def]
   127 qed_goalw "qsplit" thy [qsplit_def]
   118     "qsplit(%x y.c(x,y), <a;b>) == c(a,b)"
   128     "qsplit(%x y.c(x,y), <a;b>) == c(a,b)"
   119  (fn _ => [ (simp_tac qpair_ss 1),
   129  (fn _ => [ (Simp_tac 1),
   120             (rtac reflexive_thm 1) ]);
   130             (rtac reflexive_thm 1) ]);
       
   131 
       
   132 Addsimps [qsplit];
   121 
   133 
   122 qed_goal "qsplit_type" thy
   134 qed_goal "qsplit_type" thy
   123     "[|  p:QSigma(A,B);   \
   135     "[|  p:QSigma(A,B);   \
   124 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
   136 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
   125 \    |] ==> qsplit(%x y.c(x,y), p) : C(p)"
   137 \    |] ==> qsplit(%x y.c(x,y), p) : C(p)"
   126  (fn major::prems=>
   138  (fn major::prems=>
   127   [ (rtac (major RS QSigmaE) 1),
   139   [ (rtac (major RS QSigmaE) 1),
   128     (asm_simp_tac (qpair_ss addsimps (qsplit::prems)) 1) ]);
   140     (asm_simp_tac (!simpset addsimps prems) 1) ]);
   129 
   141 
   130 goalw thy [qsplit_def]
   142 goalw thy [qsplit_def]
   131   "!!u. u: A<*>B ==>   \
   143   "!!u. u: A<*>B ==>   \
   132 \       R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
   144 \       R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
   133 by (etac QSigmaE 1);
   145 by (Auto_tac());
   134 by (asm_simp_tac qpair_ss 1);
       
   135 by (fast_tac qpair_cs 1);
       
   136 qed "expand_qsplit";
   146 qed "expand_qsplit";
   137 
   147 
   138 
   148 
   139 (*** qsplit for predicates: result type o ***)
   149 (*** qsplit for predicates: result type o ***)
   140 
   150 
   141 goalw thy [qsplit_def] "!!R a b. R(a,b) ==> qsplit(R, <a;b>)";
   151 goalw thy [qsplit_def] "!!R a b. R(a,b) ==> qsplit(R, <a;b>)";
   142 by (asm_simp_tac qpair_ss 1);
   152 by (Asm_simp_tac 1);
   143 qed "qsplitI";
   153 qed "qsplitI";
   144 
   154 
   145 val major::sigma::prems = goalw thy [qsplit_def]
   155 val major::sigma::prems = goalw thy [qsplit_def]
   146     "[| qsplit(R,z);  z:QSigma(A,B);                    \
   156     "[| qsplit(R,z);  z:QSigma(A,B);                    \
   147 \       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
   157 \       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
   148 \   |] ==> P";
   158 \   |] ==> P";
   149 by (rtac (sigma RS QSigmaE) 1);
   159 by (rtac (sigma RS QSigmaE) 1);
   150 by (cut_facts_tac [major] 1);
   160 by (cut_facts_tac [major] 1);
   151 by (asm_full_simp_tac (qpair_ss addsimps prems) 1);
   161 by (REPEAT (ares_tac prems 1));
       
   162 by (Asm_full_simp_tac 1);
   152 qed "qsplitE";
   163 qed "qsplitE";
   153 
   164 
   154 goalw thy [qsplit_def] "!!R a b. qsplit(R,<a;b>) ==> R(a,b)";
   165 goalw thy [qsplit_def] "!!R a b. qsplit(R,<a;b>) ==> R(a,b)";
   155 by (asm_full_simp_tac qpair_ss 1);
   166 by (Asm_full_simp_tac 1);
   156 qed "qsplitD";
   167 qed "qsplitD";
   157 
   168 
   158 
   169 
   159 (*** qconverse ***)
   170 (*** qconverse ***)
   160 
   171 
   161 qed_goalw "qconverseI" thy [qconverse_def]
   172 qed_goalw "qconverseI" thy [qconverse_def]
   162     "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
   173     "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
   163  (fn _ => [ (fast_tac qpair_cs 1) ]);
   174  (fn _ => [ (Fast_tac 1) ]);
   164 
   175 
   165 qed_goalw "qconverseD" thy [qconverse_def]
   176 qed_goalw "qconverseD" thy [qconverse_def]
   166     "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
   177     "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
   167  (fn _ => [ (fast_tac qpair_cs 1) ]);
   178  (fn _ => [ (Fast_tac 1) ]);
   168 
   179 
   169 qed_goalw "qconverseE" thy [qconverse_def]
   180 qed_goalw "qconverseE" thy [qconverse_def]
   170     "[| yx : qconverse(r);  \
   181     "[| yx : qconverse(r);  \
   171 \       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
   182 \       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
   172 \    |] ==> P"
   183 \    |] ==> P"
   174   [ (rtac (major RS ReplaceE) 1),
   185   [ (rtac (major RS ReplaceE) 1),
   175     (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   186     (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   176     (hyp_subst_tac 1),
   187     (hyp_subst_tac 1),
   177     (assume_tac 1) ]);
   188     (assume_tac 1) ]);
   178 
   189 
   179 val qconverse_cs = qpair_cs addSIs [qconverseI] 
   190 AddSIs [qconverseI];
   180                             addSEs [qconverseD,qconverseE];
   191 AddSEs [qconverseD, qconverseE];
   181 
   192 
   182 qed_goal "qconverse_qconverse" thy
   193 qed_goal "qconverse_qconverse" thy
   183     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   194     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   184  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   195  (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
   185 
   196 
   186 qed_goal "qconverse_type" thy
   197 qed_goal "qconverse_type" thy
   187     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
   198     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
   188  (fn _ => [ (fast_tac qconverse_cs 1) ]);
   199  (fn _ => [ (Fast_tac 1) ]);
   189 
   200 
   190 qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
   201 qed_goal "qconverse_prod" thy "qconverse(A <*> B) = B <*> A"
   191  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   202  (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
   192 
   203 
   193 qed_goal "qconverse_empty" thy "qconverse(0) = 0"
   204 qed_goal "qconverse_empty" thy "qconverse(0) = 0"
   194  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   205  (fn _ => [ (fast_tac (!claset addSIs [equalityI]) 1) ]);
   195 
   206 
   196 
   207 
   197 (**** The Quine-inspired notion of disjoint sum ****)
   208 (**** The Quine-inspired notion of disjoint sum ****)
   198 
   209 
   199 val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
   210 val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
   200 
   211 
   201 (** Introduction rules for the injections **)
   212 (** Introduction rules for the injections **)
   202 
   213 
   203 goalw thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
   214 goalw thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
   204 by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1));
   215 by (Fast_tac 1);
   205 qed "QInlI";
   216 qed "QInlI";
   206 
   217 
   207 goalw thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
   218 goalw thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
   208 by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1));
   219 by (Fast_tac 1);
   209 qed "QInrI";
   220 qed "QInrI";
   210 
   221 
   211 (** Elimination rules **)
   222 (** Elimination rules **)
   212 
   223 
   213 val major::prems = goalw thy qsum_defs
   224 val major::prems = goalw thy qsum_defs
   218 by (rtac (major RS UnE) 1);
   229 by (rtac (major RS UnE) 1);
   219 by (REPEAT (rtac refl 1
   230 by (REPEAT (rtac refl 1
   220      ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
   231      ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
   221 qed "qsumE";
   232 qed "qsumE";
   222 
   233 
       
   234 AddSIs [QInlI, QInrI];
       
   235 
   223 (** Injection and freeness equivalences, for rewriting **)
   236 (** Injection and freeness equivalences, for rewriting **)
   224 
   237 
   225 goalw thy qsum_defs "QInl(a)=QInl(b) <-> a=b";
   238 goalw thy qsum_defs "QInl(a)=QInl(b) <-> a=b";
   226 by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
   239 by (Simp_tac 1);
   227 qed "QInl_iff";
   240 qed "QInl_iff";
   228 
   241 
   229 goalw thy qsum_defs "QInr(a)=QInr(b) <-> a=b";
   242 goalw thy qsum_defs "QInr(a)=QInr(b) <-> a=b";
   230 by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
   243 by (Simp_tac 1);
   231 qed "QInr_iff";
   244 qed "QInr_iff";
   232 
   245 
   233 goalw thy qsum_defs "QInl(a)=QInr(b) <-> False";
   246 goalw thy qsum_defs "QInl(a)=QInr(b) <-> False";
   234 by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1);
   247 by (Simp_tac 1);
   235 qed "QInl_QInr_iff";
   248 qed "QInl_QInr_iff";
   236 
   249 
   237 goalw thy qsum_defs "QInr(b)=QInl(a) <-> False";
   250 goalw thy qsum_defs "QInr(b)=QInl(a) <-> False";
   238 by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1);
   251 by (Simp_tac 1);
   239 qed "QInr_QInl_iff";
   252 qed "QInr_QInl_iff";
       
   253 
       
   254 goalw thy qsum_defs "0<+>0 = 0";
       
   255 by (Simp_tac 1);
       
   256 qed "qsum_empty";
   240 
   257 
   241 (*Injection and freeness rules*)
   258 (*Injection and freeness rules*)
   242 
   259 
   243 bind_thm ("QInl_inject", (QInl_iff RS iffD1));
   260 bind_thm ("QInl_inject", (QInl_iff RS iffD1));
   244 bind_thm ("QInr_inject", (QInr_iff RS iffD1));
   261 bind_thm ("QInr_inject", (QInr_iff RS iffD1));
   245 bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
   262 bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
   246 bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
   263 bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
   247 
   264 
   248 val qsum_cs = 
   265 AddSEs [qsumE, QInl_neq_QInr, QInr_neq_QInl];
   249     qpair_cs addSIs [PartI, QInlI, QInrI] 
   266 AddSDs [QInl_inject, QInr_inject];
   250              addSEs [PartE, qsumE, QInl_neq_QInr, QInr_neq_QInl]
   267 Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty];
   251              addSDs [QInl_inject, QInr_inject];
       
   252 
   268 
   253 goal thy "!!A B. QInl(a): A<+>B ==> a: A";
   269 goal thy "!!A B. QInl(a): A<+>B ==> a: A";
   254 by (fast_tac qsum_cs 1);
   270 by (Fast_tac 1);
   255 qed "QInlD";
   271 qed "QInlD";
   256 
   272 
   257 goal thy "!!A B. QInr(b): A<+>B ==> b: B";
   273 goal thy "!!A B. QInr(b): A<+>B ==> b: B";
   258 by (fast_tac qsum_cs 1);
   274 by (Fast_tac 1);
   259 qed "QInrD";
   275 qed "QInrD";
   260 
   276 
   261 (** <+> is itself injective... who cares?? **)
   277 (** <+> is itself injective... who cares?? **)
   262 
   278 
   263 goal thy
   279 goal thy
   264     "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
   280     "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
   265 by (fast_tac qsum_cs 1);
   281 by (Fast_tac 1);
   266 qed "qsum_iff";
   282 qed "qsum_iff";
   267 
   283 
   268 goal thy "A <+> B <= C <+> D <-> A<=C & B<=D";
   284 goal thy "A <+> B <= C <+> D <-> A<=C & B<=D";
   269 by (fast_tac qsum_cs 1);
   285 by (Fast_tac 1);
   270 qed "qsum_subset_iff";
   286 qed "qsum_subset_iff";
   271 
   287 
   272 goal thy "A <+> B = C <+> D <-> A=C & B=D";
   288 goal thy "A <+> B = C <+> D <-> A=C & B=D";
   273 by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
   289 by (simp_tac (!simpset addsimps [extension,qsum_subset_iff]) 1);
   274 by (fast_tac ZF_cs 1);
   290 by (Fast_tac 1);
   275 qed "qsum_equal_iff";
   291 qed "qsum_equal_iff";
   276 
   292 
   277 (*** Eliminator -- qcase ***)
   293 (*** Eliminator -- qcase ***)
   278 
   294 
   279 goalw thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";
   295 goalw thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";
   280 by (simp_tac (ZF_ss addsimps [qsplit, cond_0]) 1);
   296 by (Simp_tac 1);
   281 qed "qcase_QInl";
   297 qed "qcase_QInl";
   282 
   298 
   283 goalw thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";
   299 goalw thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";
   284 by (simp_tac (ZF_ss addsimps [qsplit, cond_1]) 1);
   300 by (Simp_tac 1);
   285 qed "qcase_QInr";
   301 qed "qcase_QInr";
       
   302 
       
   303 Addsimps [qcase_QInl, qcase_QInr];
   286 
   304 
   287 val major::prems = goal thy
   305 val major::prems = goal thy
   288     "[| u: A <+> B; \
   306     "[| u: A <+> B; \
   289 \       !!x. x: A ==> c(x): C(QInl(x));   \
   307 \       !!x. x: A ==> c(x): C(QInl(x));   \
   290 \       !!y. y: B ==> d(y): C(QInr(y)) \
   308 \       !!y. y: B ==> d(y): C(QInr(y)) \
   291 \    |] ==> qcase(c,d,u) : C(u)";
   309 \    |] ==> qcase(c,d,u) : C(u)";
   292 by (rtac (major RS qsumE) 1);
   310 by (rtac (major RS qsumE) 1);
   293 by (ALLGOALS (etac ssubst));
   311 by (ALLGOALS (etac ssubst));
   294 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   312 by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
   295                             (prems@[qcase_QInl,qcase_QInr]))));
       
   296 qed "qcase_type";
   313 qed "qcase_type";
   297 
   314 
   298 (** Rules for the Part primitive **)
   315 (** Rules for the Part primitive **)
   299 
   316 
   300 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
   317 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
   301 by (fast_tac (qsum_cs addIs [equalityI]) 1);
   318 by (fast_tac (!claset addIs [equalityI]) 1);
   302 qed "Part_QInl";
   319 qed "Part_QInl";
   303 
   320 
   304 goal thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
   321 goal thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
   305 by (fast_tac (qsum_cs addIs [equalityI]) 1);
   322 by (fast_tac (!claset addIs [equalityI]) 1);
   306 qed "Part_QInr";
   323 qed "Part_QInr";
   307 
   324 
   308 goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
   325 goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
   309 by (fast_tac (qsum_cs addIs [equalityI]) 1);
   326 by (fast_tac (!claset addIs [equalityI]) 1);
   310 qed "Part_QInr2";
   327 qed "Part_QInr2";
   311 
   328 
   312 goal thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
   329 goal thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
   313 by (fast_tac (qsum_cs addIs [equalityI]) 1);
   330 by (fast_tac (!claset addIs [equalityI]) 1);
   314 qed "Part_qsum_equality";
   331 qed "Part_qsum_equality";