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();
```