src/ZF/qpair.ML
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 55 331d93292ee0
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
     1 (*  Title: 	ZF/qpair.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 For qpair.thy.  
     7 
     8 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
     9 structures in ZF.  Does not precisely follow Quine's construction.  Thanks
    10 to Thomas Forster for suggesting this approach!
    11 
    12 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
    13 1966.
    14 
    15 Many proofs are borrowed from pair.ML and sum.ML
    16 
    17 Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
    18     is not a limit ordinal? 
    19 *)
    20 
    21 
    22 open QPair;
    23 
    24 (**** Quine ordered pairing ****)
    25 
    26 (** Lemmas for showing that <a;b> uniquely determines a and b **)
    27 
    28 val QPair_iff = prove_goalw QPair.thy [QPair_def]
    29     "<a;b> = <c;d> <-> a=c & b=d"
    30  (fn _=> [rtac sum_equal_iff 1]);
    31 
    32 val QPair_inject = standard (QPair_iff RS iffD1 RS conjE);
    33 
    34 val QPair_inject1 = prove_goal QPair.thy "<a;b> = <c;d> ==> a=c"
    35  (fn [major]=>
    36   [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
    37 
    38 val QPair_inject2 = prove_goal QPair.thy "<a;b> = <c;d> ==> b=d"
    39  (fn [major]=>
    40   [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
    41 
    42 
    43 (*** QSigma: Disjoint union of a family of sets
    44      Generalizes Cartesian product ***)
    45 
    46 val QSigmaI = prove_goalw QPair.thy [QSigma_def]
    47     "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
    48  (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
    49 
    50 (*The general elimination rule*)
    51 val QSigmaE = prove_goalw QPair.thy [QSigma_def]
    52     "[| c: QSigma(A,B);  \
    53 \       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
    54 \    |] ==> P"
    55  (fn major::prems=>
    56   [ (cut_facts_tac [major] 1),
    57     (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
    58 
    59 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
    60 
    61 val QSigmaE2 = 
    62   rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
    63 		  THEN prune_params_tac)
    64       (read_instantiate [("c","<a;b>")] QSigmaE);  
    65 
    66 val QSigmaD1 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> a : A"
    67  (fn [major]=>
    68   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    69 
    70 val QSigmaD2 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)"
    71  (fn [major]=>
    72   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
    73 
    74 val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
    75     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    76 \    QSigma(A,B) = QSigma(A',B')"
    77  (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
    78 
    79 val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
    80  (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
    81 
    82 val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0"
    83  (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
    84 
    85 
    86 (*** Eliminator - qsplit ***)
    87 
    88 val qsplit = prove_goalw QPair.thy [qsplit_def]
    89     "qsplit(%x y.c(x,y), <a;b>) = c(a,b)"
    90  (fn _ => [ (fast_tac (ZF_cs addIs [the_equality] addEs [QPair_inject]) 1) ]);
    91 
    92 val qsplit_type = prove_goal QPair.thy
    93     "[|  p:QSigma(A,B);   \
    94 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
    95 \    |] ==> qsplit(%x y.c(x,y), p) : C(p)"
    96  (fn major::prems=>
    97   [ (rtac (major RS QSigmaE) 1),
    98     (etac ssubst 1),
    99     (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
   100 
   101 
   102 val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
   103 
   104 (*** qconverse ***)
   105 
   106 val qconverseI = prove_goalw QPair.thy [qconverse_def]
   107     "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
   108  (fn _ => [ (fast_tac qpair_cs 1) ]);
   109 
   110 val qconverseD = prove_goalw QPair.thy [qconverse_def]
   111     "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
   112  (fn _ => [ (fast_tac qpair_cs 1) ]);
   113 
   114 val qconverseE = prove_goalw QPair.thy [qconverse_def]
   115     "[| yx : qconverse(r);  \
   116 \       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
   117 \    |] ==> P"
   118  (fn [major,minor]=>
   119   [ (rtac (major RS ReplaceE) 1),
   120     (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
   121     (hyp_subst_tac 1),
   122     (assume_tac 1) ]);
   123 
   124 val qconverse_cs = qpair_cs addSIs [qconverseI] 
   125 			    addSEs [qconverseD,qconverseE];
   126 
   127 val qconverse_of_qconverse = prove_goal QPair.thy
   128     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   129  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   130 
   131 val qconverse_type = prove_goal QPair.thy
   132     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
   133  (fn _ => [ (fast_tac qconverse_cs 1) ]);
   134 
   135 val qconverse_of_prod = prove_goal QPair.thy "qconverse(A <*> B) = B <*> A"
   136  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   137 
   138 val qconverse_empty = prove_goal QPair.thy "qconverse(0) = 0"
   139  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
   140 
   141 
   142 (*** qsplit for predicates: result type o ***)
   143 
   144 goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)";
   145 by (REPEAT (ares_tac [refl,exI,conjI] 1));
   146 val qfsplitI = result();
   147 
   148 val major::prems = goalw QPair.thy [qfsplit_def]
   149     "[| qfsplit(R,z);  !!x y. [| z = <x;y>;  R(x,y) |] ==> P |] ==> P";
   150 by (cut_facts_tac [major] 1);
   151 by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1));
   152 val qfsplitE = result();
   153 
   154 goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)";
   155 by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1));
   156 val qfsplitD = result();
   157 
   158 
   159 (**** The Quine-inspired notion of disjoint sum ****)
   160 
   161 val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
   162 
   163 (** Introduction rules for the injections **)
   164 
   165 goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
   166 by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1));
   167 val QInlI = result();
   168 
   169 goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
   170 by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1));
   171 val QInrI = result();
   172 
   173 (** Elimination rules **)
   174 
   175 val major::prems = goalw QPair.thy qsum_defs
   176     "[| u: A <+> B;  \
   177 \       !!x. [| x:A;  u=QInl(x) |] ==> P; \
   178 \       !!y. [| y:B;  u=QInr(y) |] ==> P \
   179 \    |] ==> P";
   180 by (rtac (major RS UnE) 1);
   181 by (REPEAT (rtac refl 1
   182      ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
   183 val qsumE = result();
   184 
   185 (** QInjection and freeness rules **)
   186 
   187 val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInl(b) ==> a=b";
   188 by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
   189 val QInl_inject = result();
   190 
   191 val [major] = goalw QPair.thy qsum_defs "QInr(a)=QInr(b) ==> a=b";
   192 by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
   193 val QInr_inject = result();
   194 
   195 val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInr(b) ==> P";
   196 by (rtac (major RS QPair_inject) 1);
   197 by (etac (sym RS one_neq_0) 1);
   198 val QInl_neq_QInr = result();
   199 
   200 val QInr_neq_QInl = sym RS QInl_neq_QInr;
   201 
   202 (** Injection and freeness equivalences, for rewriting **)
   203 
   204 goal QPair.thy "QInl(a)=QInl(b) <-> a=b";
   205 by (rtac iffI 1);
   206 by (REPEAT (eresolve_tac [QInl_inject,subst_context] 1));
   207 val QInl_iff = result();
   208 
   209 goal QPair.thy "QInr(a)=QInr(b) <-> a=b";
   210 by (rtac iffI 1);
   211 by (REPEAT (eresolve_tac [QInr_inject,subst_context] 1));
   212 val QInr_iff = result();
   213 
   214 goal QPair.thy "QInl(a)=QInr(b) <-> False";
   215 by (rtac iffI 1);
   216 by (REPEAT (eresolve_tac [QInl_neq_QInr,FalseE] 1));
   217 val QInl_QInr_iff = result();
   218 
   219 goal QPair.thy "QInr(b)=QInl(a) <-> False";
   220 by (rtac iffI 1);
   221 by (REPEAT (eresolve_tac [QInr_neq_QInl,FalseE] 1));
   222 val QInr_QInl_iff = result();
   223 
   224 val qsum_cs = 
   225     ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
   226           addSDs [QInl_inject,QInr_inject];
   227 
   228 (** <+> is itself injective... who cares?? **)
   229 
   230 goal QPair.thy
   231     "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
   232 by (fast_tac qsum_cs 1);
   233 val qsum_iff = result();
   234 
   235 goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D";
   236 by (fast_tac qsum_cs 1);
   237 val qsum_subset_iff = result();
   238 
   239 goal QPair.thy "A <+> B = C <+> D <-> A=C & B=D";
   240 by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
   241 by (fast_tac ZF_cs 1);
   242 val qsum_equal_iff = result();
   243 
   244 (*** Eliminator -- qcase ***)
   245 
   246 goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";
   247 by (rtac (qsplit RS trans) 1);
   248 by (rtac cond_0 1);
   249 val qcase_QInl = result();
   250 
   251 goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";
   252 by (rtac (qsplit RS trans) 1);
   253 by (rtac cond_1 1);
   254 val qcase_QInr = result();
   255 
   256 val major::prems = goal QPair.thy
   257     "[| u: A <+> B; \
   258 \       !!x. x: A ==> c(x): C(QInl(x));   \
   259 \       !!y. y: B ==> d(y): C(QInr(y)) \
   260 \    |] ==> qcase(c,d,u) : C(u)";
   261 by (rtac (major RS qsumE) 1);
   262 by (ALLGOALS (etac ssubst));
   263 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
   264 			    (prems@[qcase_QInl,qcase_QInr]))));
   265 val qcase_type = result();
   266 
   267 (** Rules for the Part primitive **)
   268 
   269 goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
   270 by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   271 val Part_QInl = result();
   272 
   273 goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
   274 by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   275 val Part_QInr = result();
   276 
   277 goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
   278 by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   279 val Part_QInr2 = result();
   280 
   281 goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
   282 by (rtac equalityI 1);
   283 by (rtac Un_least 1);
   284 by (rtac Part_subset 1);
   285 by (rtac Part_subset 1);
   286 by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);
   287 val Part_qsum_equality = result();