0

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 
Quineinspired ordered pairs and disjoint sums, for nonwellfounded 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=> [ (prove_cong_tac (prems@[RepFun_cong]) 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 
(*This congruence rule uses NO typing information...*)


102 
val qsplit_cong = prove_goalw QPair.thy [qsplit_def]


103 
"[ p=p'; !!x y.c(x,y) = c'(x,y) ] ==> \


104 
\ qsplit(%x y.c(x,y), p) = qsplit(%x y.c'(x,y), p')"


105 
(fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);


106 


107 


108 
val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];


109 


110 
(*** qconverse ***)


111 


112 
val qconverseI = prove_goalw QPair.thy [qconverse_def]


113 
"!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"


114 
(fn _ => [ (fast_tac qpair_cs 1) ]);


115 


116 
val qconverseD = prove_goalw QPair.thy [qconverse_def]


117 
"!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"


118 
(fn _ => [ (fast_tac qpair_cs 1) ]);


119 


120 
val qconverseE = prove_goalw QPair.thy [qconverse_def]


121 
"[ yx : qconverse(r); \


122 
\ !!x y. [ yx=<y;x>; <x;y>:r ] ==> P \


123 
\ ] ==> P"


124 
(fn [major,minor]=>


125 
[ (rtac (major RS ReplaceE) 1),


126 
(REPEAT (eresolve_tac [exE, conjE, minor] 1)),


127 
(hyp_subst_tac 1),


128 
(assume_tac 1) ]);


129 


130 
val qconverse_cs = qpair_cs addSIs [qconverseI]


131 
addSEs [qconverseD,qconverseE];


132 


133 
val qconverse_of_qconverse = prove_goal QPair.thy


134 
"!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"


135 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);


136 


137 
val qconverse_type = prove_goal QPair.thy


138 
"!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"


139 
(fn _ => [ (fast_tac qconverse_cs 1) ]);


140 


141 
val qconverse_of_prod = prove_goal QPair.thy "qconverse(A <*> B) = B <*> A"


142 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);


143 


144 
val qconverse_empty = prove_goal QPair.thy "qconverse(0) = 0"


145 
(fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);


146 


147 


148 
(*** qsplit for predicates: result type o ***)


149 


150 
goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)";


151 
by (REPEAT (ares_tac [refl,exI,conjI] 1));


152 
val qfsplitI = result();


153 


154 
val major::prems = goalw QPair.thy [qfsplit_def]


155 
"[ qfsplit(R,z); !!x y. [ z = <x;y>; R(x,y) ] ==> P ] ==> P";


156 
by (cut_facts_tac [major] 1);


157 
by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1));


158 
val qfsplitE = result();


159 


160 
goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)";


161 
by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1));


162 
val qfsplitD = result();


163 


164 


165 
(**** The Quineinspired notion of disjoint sum ****)


166 


167 
val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];


168 


169 
(** Introduction rules for the injections **)


170 


171 
goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";


172 
by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1));


173 
val QInlI = result();


174 


175 
goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";


176 
by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1));


177 
val QInrI = result();


178 


179 
(** Elimination rules **)


180 


181 
val major::prems = goalw QPair.thy qsum_defs


182 
"[ u: A <+> B; \


183 
\ !!x. [ x:A; u=QInl(x) ] ==> P; \


184 
\ !!y. [ y:B; u=QInr(y) ] ==> P \


185 
\ ] ==> P";


186 
by (rtac (major RS UnE) 1);


187 
by (REPEAT (rtac refl 1


188 
ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));


189 
val qsumE = result();


190 


191 
(** QInjection and freeness rules **)


192 


193 
val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInl(b) ==> a=b";


194 
by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);


195 
val QInl_inject = result();


196 


197 
val [major] = goalw QPair.thy qsum_defs "QInr(a)=QInr(b) ==> a=b";


198 
by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);


199 
val QInr_inject = result();


200 


201 
val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInr(b) ==> P";


202 
by (rtac (major RS QPair_inject) 1);


203 
by (etac (sym RS one_neq_0) 1);


204 
val QInl_neq_QInr = result();


205 


206 
val QInr_neq_QInl = sym RS QInl_neq_QInr;


207 


208 
(** Injection and freeness equivalences, for rewriting **)


209 


210 
goal QPair.thy "QInl(a)=QInl(b) <> a=b";


211 
by (rtac iffI 1);


212 
by (REPEAT (eresolve_tac [QInl_inject,subst_context] 1));


213 
val QInl_iff = result();


214 


215 
goal QPair.thy "QInr(a)=QInr(b) <> a=b";


216 
by (rtac iffI 1);


217 
by (REPEAT (eresolve_tac [QInr_inject,subst_context] 1));


218 
val QInr_iff = result();


219 


220 
goal QPair.thy "QInl(a)=QInr(b) <> False";


221 
by (rtac iffI 1);


222 
by (REPEAT (eresolve_tac [QInl_neq_QInr,FalseE] 1));


223 
val QInl_QInr_iff = result();


224 


225 
goal QPair.thy "QInr(b)=QInl(a) <> False";


226 
by (rtac iffI 1);


227 
by (REPEAT (eresolve_tac [QInr_neq_QInl,FalseE] 1));


228 
val QInr_QInl_iff = result();


229 


230 
val qsum_cs =


231 
ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]


232 
addSDs [QInl_inject,QInr_inject];


233 


234 
(** <+> is itself injective... who cares?? **)


235 


236 
goal QPair.thy


237 
"u: A <+> B <> (EX x. x:A & u=QInl(x))  (EX y. y:B & u=QInr(y))";


238 
by (fast_tac qsum_cs 1);


239 
val qsum_iff = result();


240 


241 
goal QPair.thy "A <+> B <= C <+> D <> A<=C & B<=D";


242 
by (fast_tac qsum_cs 1);


243 
val qsum_subset_iff = result();


244 


245 
goal QPair.thy "A <+> B = C <+> D <> A=C & B=D";


246 
by (SIMP_TAC (ZF_ss addrews [extension,qsum_subset_iff]) 1);


247 
by (fast_tac ZF_cs 1);


248 
val qsum_equal_iff = result();


249 


250 
(*** Eliminator  qcase ***)


251 


252 
goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";


253 
by (rtac (qsplit RS trans) 1);


254 
by (rtac cond_0 1);


255 
val qcase_QInl = result();


256 


257 
goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";


258 
by (rtac (qsplit RS trans) 1);


259 
by (rtac cond_1 1);


260 
val qcase_QInr = result();


261 


262 
val prems = goalw QPair.thy [qcase_def]


263 
"[ u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) ] ==> \


264 
\ qcase(c,d,u)=qcase(c',d',u')";


265 
by (REPEAT (resolve_tac ([refl,qsplit_cong,cond_cong] @ prems) 1));


266 
val qcase_cong = result();


267 


268 
val major::prems = goal QPair.thy


269 
"[ u: A <+> B; \


270 
\ !!x. x: A ==> c(x): C(QInl(x)); \


271 
\ !!y. y: B ==> d(y): C(QInr(y)) \


272 
\ ] ==> qcase(c,d,u) : C(u)";


273 
by (rtac (major RS qsumE) 1);


274 
by (ALLGOALS (etac ssubst));


275 
by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews


276 
(prems@[qcase_QInl,qcase_QInr]))));


277 
val qcase_type = result();


278 


279 
(** Rules for the Part primitive **)


280 


281 
goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";


282 
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


283 
val Part_QInl = result();


284 


285 
goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";


286 
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


287 
val Part_QInr = result();


288 


289 
goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";


290 
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


291 
val Part_QInr2 = result();


292 


293 
goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";


294 
by (rtac equalityI 1);


295 
by (rtac Un_least 1);


296 
by (rtac Part_subset 1);


297 
by (rtac Part_subset 1);


298 
by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);


299 
val Part_qsum_equality = result();
