--- a/src/ZF/QPair.ML Fri Nov 25 00:00:35 1994 +0100
+++ b/src/ZF/QPair.ML Fri Nov 25 00:01:04 1994 +0100
@@ -1,9 +1,9 @@
-(* Title: ZF/qpair.ML
+(* Title: ZF/QPair.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For qpair.thy.
+For QPair.thy.
Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
structures in ZF. Does not precisely follow Quine's construction. Thanks
@@ -71,23 +71,26 @@
(fn [major]=>
[ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
+val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
+
+
val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
"[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
\ QSigma(A,B) = QSigma(A',B')"
(fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
- (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
+ (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]);
val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0"
- (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
+ (fn _ => [ (fast_tac (qpair_cs addIs [equalityI]) 1) ]);
(*** Eliminator - qsplit ***)
val qsplit = prove_goalw QPair.thy [qsplit_def]
"qsplit(%x y.c(x,y), <a;b>) = c(a,b)"
- (fn _ => [ (fast_tac (ZF_cs addIs [the_equality] addEs [QPair_inject]) 1) ]);
+ (fn _ => [ (fast_tac (qpair_cs addIs [the_equality]) 1) ]);
val qsplit_type = prove_goal QPair.thy
"[| p:QSigma(A,B); \
@@ -99,8 +102,6 @@
(REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
-val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
-
(*** qconverse ***)
val qconverseI = prove_goalw QPair.thy [qconverse_def]
@@ -208,8 +209,9 @@
val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
val qsum_cs =
- qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
- addSDs [QInl_inject,QInr_inject];
+ qpair_cs addSIs [PartI, QInlI, QInrI]
+ addSEs [PartE, qsumE, QInl_neq_QInr, QInr_neq_QInl]
+ addSDs [QInl_inject, QInr_inject];
goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
by (fast_tac qsum_cs 1);
@@ -261,21 +263,17 @@
(** Rules for the Part primitive **)
goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
val Part_QInl = result();
goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
val Part_QInr = result();
goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
val Part_QInr2 = result();
goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (rtac equalityI 1);
-by (rtac Un_least 1);
-by (rtac Part_subset 1);
-by (rtac Part_subset 1);
-by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);
+by (fast_tac (qsum_cs addIs [equalityI]) 1);
val Part_qsum_equality = result();