src/ZF/qpair.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/qpair.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,299 @@
     1.4 +(*  Title: 	ZF/qpair.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +For qpair.thy.  
    1.10 +
    1.11 +Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
    1.12 +structures in ZF.  Does not precisely follow Quine's construction.  Thanks
    1.13 +to Thomas Forster for suggesting this approach!
    1.14 +
    1.15 +W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
    1.16 +1966.
    1.17 +
    1.18 +Many proofs are borrowed from pair.ML and sum.ML
    1.19 +
    1.20 +Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
    1.21 +    is not a limit ordinal? 
    1.22 +*)
    1.23 +
    1.24 +
    1.25 +open QPair;
    1.26 +
    1.27 +(**** Quine ordered pairing ****)
    1.28 +
    1.29 +(** Lemmas for showing that <a;b> uniquely determines a and b **)
    1.30 +
    1.31 +val QPair_iff = prove_goalw QPair.thy [QPair_def]
    1.32 +    "<a;b> = <c;d> <-> a=c & b=d"
    1.33 + (fn _=> [rtac sum_equal_iff 1]);
    1.34 +
    1.35 +val QPair_inject = standard (QPair_iff RS iffD1 RS conjE);
    1.36 +
    1.37 +val QPair_inject1 = prove_goal QPair.thy "<a;b> = <c;d> ==> a=c"
    1.38 + (fn [major]=>
    1.39 +  [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
    1.40 +
    1.41 +val QPair_inject2 = prove_goal QPair.thy "<a;b> = <c;d> ==> b=d"
    1.42 + (fn [major]=>
    1.43 +  [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
    1.44 +
    1.45 +
    1.46 +(*** QSigma: Disjoint union of a family of sets
    1.47 +     Generalizes Cartesian product ***)
    1.48 +
    1.49 +val QSigmaI = prove_goalw QPair.thy [QSigma_def]
    1.50 +    "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
    1.51 + (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
    1.52 +
    1.53 +(*The general elimination rule*)
    1.54 +val QSigmaE = prove_goalw QPair.thy [QSigma_def]
    1.55 +    "[| c: QSigma(A,B);  \
    1.56 +\       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
    1.57 +\    |] ==> P"
    1.58 + (fn major::prems=>
    1.59 +  [ (cut_facts_tac [major] 1),
    1.60 +    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
    1.61 +
    1.62 +(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
    1.63 +
    1.64 +val QSigmaE2 = 
    1.65 +  rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
    1.66 +		  THEN prune_params_tac)
    1.67 +      (read_instantiate [("c","<a;b>")] QSigmaE);  
    1.68 +
    1.69 +val QSigmaD1 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> a : A"
    1.70 + (fn [major]=>
    1.71 +  [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    1.72 +
    1.73 +val QSigmaD2 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)"
    1.74 + (fn [major]=>
    1.75 +  [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    1.76 +
    1.77 +val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
    1.78 +    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    1.79 +\    QSigma(A,B) = QSigma(A',B')"
    1.80 + (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
    1.81 +
    1.82 +val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
    1.83 + (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
    1.84 +
    1.85 +val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0"
    1.86 + (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
    1.87 +
    1.88 +
    1.89 +(*** Eliminator - qsplit ***)
    1.90 +
    1.91 +val qsplit = prove_goalw QPair.thy [qsplit_def]
    1.92 +    "qsplit(%x y.c(x,y), <a;b>) = c(a,b)"
    1.93 + (fn _ => [ (fast_tac (ZF_cs addIs [the_equality] addEs [QPair_inject]) 1) ]);
    1.94 +
    1.95 +val qsplit_type = prove_goal QPair.thy
    1.96 +    "[|  p:QSigma(A,B);   \
    1.97 +\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
    1.98 +\    |] ==> qsplit(%x y.c(x,y), p) : C(p)"
    1.99 + (fn major::prems=>
   1.100 +  [ (rtac (major RS QSigmaE) 1),
   1.101 +    (etac ssubst 1),
   1.102 +    (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
   1.103 +
   1.104 +(*This congruence rule uses NO typing information...*)
   1.105 +val qsplit_cong = prove_goalw QPair.thy [qsplit_def] 
   1.106 +    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
   1.107 +\    qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"
   1.108 + (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
   1.109 +
   1.110 +
   1.111 +val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
   1.112 +
   1.113 +(*** qconverse ***)
   1.114 +
   1.115 +val qconverseI = prove_goalw QPair.thy [qconverse_def]
   1.116 +    "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
   1.117 + (fn _ => [ (fast_tac qpair_cs 1) ]);
   1.118 +
   1.119 +val qconverseD = prove_goalw QPair.thy [qconverse_def]
   1.120 +    "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
   1.121 + (fn _ => [ (fast_tac qpair_cs 1) ]);
   1.122 +
   1.123 +val qconverseE = prove_goalw QPair.thy [qconverse_def]
   1.124 +    "[| yx : qconverse(r);  \
   1.125 +\       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
   1.126 +\    |] ==> P"
   1.127 + (fn [major,minor]=>
   1.128 +  [ (rtac (major RS ReplaceE) 1),
   1.129 +    (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   1.130 +    (hyp_subst_tac 1),
   1.131 +    (assume_tac 1) ]);
   1.132 +
   1.133 +val qconverse_cs = qpair_cs addSIs [qconverseI] 
   1.134 +			    addSEs [qconverseD,qconverseE];
   1.135 +
   1.136 +val qconverse_of_qconverse = prove_goal QPair.thy
   1.137 +    "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   1.138 + (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   1.139 +
   1.140 +val qconverse_type = prove_goal QPair.thy
   1.141 +    "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
   1.142 + (fn _ => [ (fast_tac qconverse_cs 1) ]);
   1.143 +
   1.144 +val qconverse_of_prod = prove_goal QPair.thy "qconverse(A <*> B) = B <*> A"
   1.145 + (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   1.146 +
   1.147 +val qconverse_empty = prove_goal QPair.thy "qconverse(0) = 0"
   1.148 + (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   1.149 +
   1.150 +
   1.151 +(*** qsplit for predicates: result type o ***)
   1.152 +
   1.153 +goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)";
   1.154 +by (REPEAT (ares_tac [refl,exI,conjI] 1));
   1.155 +val qfsplitI = result();
   1.156 +
   1.157 +val major::prems = goalw QPair.thy [qfsplit_def]
   1.158 +    "[| qfsplit(R,z);  !!x y. [| z = <x;y>;  R(x,y) |] ==> P |] ==> P";
   1.159 +by (cut_facts_tac [major] 1);
   1.160 +by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1));
   1.161 +val qfsplitE = result();
   1.162 +
   1.163 +goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)";
   1.164 +by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1));
   1.165 +val qfsplitD = result();
   1.166 +
   1.167 +
   1.168 +(**** The Quine-inspired notion of disjoint sum ****)
   1.169 +
   1.170 +val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
   1.171 +
   1.172 +(** Introduction rules for the injections **)
   1.173 +
   1.174 +goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
   1.175 +by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1));
   1.176 +val QInlI = result();
   1.177 +
   1.178 +goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
   1.179 +by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1));
   1.180 +val QInrI = result();
   1.181 +
   1.182 +(** Elimination rules **)
   1.183 +
   1.184 +val major::prems = goalw QPair.thy qsum_defs
   1.185 +    "[| u: A <+> B;  \
   1.186 +\       !!x. [| x:A;  u=QInl(x) |] ==> P; \
   1.187 +\       !!y. [| y:B;  u=QInr(y) |] ==> P \
   1.188 +\    |] ==> P";
   1.189 +by (rtac (major RS UnE) 1);
   1.190 +by (REPEAT (rtac refl 1
   1.191 +     ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
   1.192 +val qsumE = result();
   1.193 +
   1.194 +(** QInjection and freeness rules **)
   1.195 +
   1.196 +val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInl(b) ==> a=b";
   1.197 +by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
   1.198 +val QInl_inject = result();
   1.199 +
   1.200 +val [major] = goalw QPair.thy qsum_defs "QInr(a)=QInr(b) ==> a=b";
   1.201 +by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
   1.202 +val QInr_inject = result();
   1.203 +
   1.204 +val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInr(b) ==> P";
   1.205 +by (rtac (major RS QPair_inject) 1);
   1.206 +by (etac (sym RS one_neq_0) 1);
   1.207 +val QInl_neq_QInr = result();
   1.208 +
   1.209 +val QInr_neq_QInl = sym RS QInl_neq_QInr;
   1.210 +
   1.211 +(** Injection and freeness equivalences, for rewriting **)
   1.212 +
   1.213 +goal QPair.thy "QInl(a)=QInl(b) <-> a=b";
   1.214 +by (rtac iffI 1);
   1.215 +by (REPEAT (eresolve_tac [QInl_inject,subst_context] 1));
   1.216 +val QInl_iff = result();
   1.217 +
   1.218 +goal QPair.thy "QInr(a)=QInr(b) <-> a=b";
   1.219 +by (rtac iffI 1);
   1.220 +by (REPEAT (eresolve_tac [QInr_inject,subst_context] 1));
   1.221 +val QInr_iff = result();
   1.222 +
   1.223 +goal QPair.thy "QInl(a)=QInr(b) <-> False";
   1.224 +by (rtac iffI 1);
   1.225 +by (REPEAT (eresolve_tac [QInl_neq_QInr,FalseE] 1));
   1.226 +val QInl_QInr_iff = result();
   1.227 +
   1.228 +goal QPair.thy "QInr(b)=QInl(a) <-> False";
   1.229 +by (rtac iffI 1);
   1.230 +by (REPEAT (eresolve_tac [QInr_neq_QInl,FalseE] 1));
   1.231 +val QInr_QInl_iff = result();
   1.232 +
   1.233 +val qsum_cs = 
   1.234 +    ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
   1.235 +          addSDs [QInl_inject,QInr_inject];
   1.236 +
   1.237 +(** <+> is itself injective... who cares?? **)
   1.238 +
   1.239 +goal QPair.thy
   1.240 +    "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
   1.241 +by (fast_tac qsum_cs 1);
   1.242 +val qsum_iff = result();
   1.243 +
   1.244 +goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D";
   1.245 +by (fast_tac qsum_cs 1);
   1.246 +val qsum_subset_iff = result();
   1.247 +
   1.248 +goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
   1.249 +by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);
   1.250 +by (fast_tac ZF_cs 1);
   1.251 +val qsum_equal_iff = result();
   1.252 +
   1.253 +(*** Eliminator -- qcase ***)
   1.254 +
   1.255 +goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";
   1.256 +by (rtac (qsplit RS trans) 1);
   1.257 +by (rtac cond_0 1);
   1.258 +val qcase_QInl = result();
   1.259 +
   1.260 +goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";
   1.261 +by (rtac (qsplit RS trans) 1);
   1.262 +by (rtac cond_1 1);
   1.263 +val qcase_QInr = result();
   1.264 +
   1.265 +val prems = goalw QPair.thy [qcase_def]
   1.266 +    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
   1.267 +\    qcase(c,d,u)=qcase(c',d',u')";
   1.268 +by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));
   1.269 +val qcase_cong = result();
   1.270 +
   1.271 +val major::prems = goal QPair.thy
   1.272 +    "[| u: A <+> B; \
   1.273 +\       !!x. x: A ==> c(x): C(QInl(x));   \
   1.274 +\       !!y. y: B ==> d(y): C(QInr(y)) \
   1.275 +\    |] ==> qcase(c,d,u) : C(u)";
   1.276 +by (rtac (major RS qsumE) 1);
   1.277 +by (ALLGOALS (etac ssubst));
   1.278 +by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
   1.279 +			    (prems@[qcase_QInl,qcase_QInr]))));
   1.280 +val qcase_type = result();
   1.281 +
   1.282 +(** Rules for the Part primitive **)
   1.283 +
   1.284 +goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
   1.285 +by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.286 +val Part_QInl = result();
   1.287 +
   1.288 +goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
   1.289 +by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.290 +val Part_QInr = result();
   1.291 +
   1.292 +goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
   1.293 +by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.294 +val Part_QInr2 = result();
   1.295 +
   1.296 +goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
   1.297 +by (rtac equalityI 1);
   1.298 +by (rtac Un_least 1);
   1.299 +by (rtac Part_subset 1);
   1.300 +by (rtac Part_subset 1);
   1.301 +by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);
   1.302 +val Part_qsum_equality = result();