0

1 
(* Title: ZF/pair


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Ordered pairs in ZermeloFraenkel Set Theory


7 
*)


8 


9 
(** Lemmas for showing that <a,b> uniquely determines a and b **)


10 


11 
val doubleton_iff = prove_goal ZF.thy


12 
"{a,b} = {c,d} <> (a=c & b=d)  (a=d & b=c)"


13 
(fn _=> [ (resolve_tac [extension RS iff_trans] 1),


14 
(fast_tac upair_cs 1) ]);


15 


16 
val Pair_iff = prove_goalw ZF.thy [Pair_def]


17 
"<a,b> = <c,d> <> a=c & b=d"


18 
(fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),


19 
(fast_tac FOL_cs 1) ]);


20 


21 
val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);


22 


23 
val Pair_inject1 = prove_goal ZF.thy "<a,b> = <c,d> ==> a=c"


24 
(fn [major]=>


25 
[ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);


26 


27 
val Pair_inject2 = prove_goal ZF.thy "<a,b> = <c,d> ==> b=d"


28 
(fn [major]=>


29 
[ (rtac (major RS Pair_inject) 1), (assume_tac 1) ]);


30 


31 
val Pair_neq_0 = prove_goalw ZF.thy [Pair_def] "<a,b>=0 ==> P"


32 
(fn [major]=>


33 
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),


34 
(rtac consI1 1) ]);


35 


36 
val Pair_neq_fst = prove_goalw ZF.thy [Pair_def] "<a,b>=a ==> P"


37 
(fn [major]=>


38 
[ (rtac (consI1 RS mem_anti_sym RS FalseE) 1),


39 
(rtac (major RS subst) 1),


40 
(rtac consI1 1) ]);


41 


42 
val Pair_neq_snd = prove_goalw ZF.thy [Pair_def] "<a,b>=b ==> P"


43 
(fn [major]=>


44 
[ (rtac (consI1 RS consI2 RS mem_anti_sym RS FalseE) 1),


45 
(rtac (major RS subst) 1),


46 
(rtac (consI1 RS consI2) 1) ]);


47 


48 


49 
(*** Sigma: Disjoint union of a family of sets


50 
Generalizes Cartesian product ***)


51 


52 
val SigmaI = prove_goalw ZF.thy [Sigma_def]


53 
"[ a:A; b:B(a) ] ==> <a,b> : Sigma(A,B)"


54 
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);


55 


56 
(*The general elimination rule*)


57 
val SigmaE = prove_goalw ZF.thy [Sigma_def]


58 
"[ c: Sigma(A,B); \


59 
\ !!x y.[ x:A; y:B(x); c=<x,y> ] ==> P \


60 
\ ] ==> P"


61 
(fn major::prems=>


62 
[ (cut_facts_tac [major] 1),


63 
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);


64 


65 
(** Elimination of <a,b>:A*B  introduces no eigenvariables **)


66 
val SigmaD1 = prove_goal ZF.thy "<a,b> : Sigma(A,B) ==> a : A"


67 
(fn [major]=>


68 
[ (rtac (major RS SigmaE) 1),


69 
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);


70 


71 
val SigmaD2 = prove_goal ZF.thy "<a,b> : Sigma(A,B) ==> b : B(a)"


72 
(fn [major]=>


73 
[ (rtac (major RS SigmaE) 1),


74 
(REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);


75 


76 
(*Also provable via


77 
rule_by_tactic (REPEAT_FIRST (etac Pair_inject ORELSE' bound_hyp_subst_tac)


78 
THEN prune_params_tac)


79 
(read_instantiate [("c","<a,b>")] SigmaE); *)


80 
val SigmaE2 = prove_goal ZF.thy


81 
"[ <a,b> : Sigma(A,B); \


82 
\ [ a:A; b:B(a) ] ==> P \


83 
\ ] ==> P"


84 
(fn [major,minor]=>


85 
[ (rtac minor 1),


86 
(rtac (major RS SigmaD1) 1),


87 
(rtac (major RS SigmaD2) 1) ]);


88 


89 
val Sigma_cong = prove_goalw ZF.thy [Sigma_def]


90 
"[ A=A'; !!x. x:A' ==> B(x)=B'(x) ] ==> \


91 
\ Sigma(A,B) = Sigma(A',B')"


92 
(fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);


93 


94 
val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"


95 
(fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);


96 


97 
val Sigma_empty2 = prove_goal ZF.thy "A*0 = 0"


98 
(fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);


99 


100 


101 
(*** Eliminator  split ***)


102 


103 
val split = prove_goalw ZF.thy [split_def]


104 
"split(%x y.c(x,y), <a,b>) = c(a,b)"


105 
(fn _ =>


106 
[ (fast_tac (upair_cs addIs [the_equality] addEs [Pair_inject]) 1) ]);


107 


108 
val split_type = prove_goal ZF.thy


109 
"[ p:Sigma(A,B); \


110 
\ !!x y.[ x:A; y:B(x) ] ==> c(x,y):C(<x,y>) \


111 
\ ] ==> split(%x y.c(x,y), p) : C(p)"


112 
(fn major::prems=>


113 
[ (rtac (major RS SigmaE) 1),


114 
(etac ssubst 1),


115 
(REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);


116 


117 
(*This congruence rule uses NO typing information...*)


118 
val split_cong = prove_goalw ZF.thy [split_def]


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


120 
\ split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"


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


122 


123 


124 
(*** conversions for fst and snd ***)


125 


126 
val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"


127 
(fn _=> [ (rtac split 1) ]);


128 


129 
val snd_conv = prove_goalw ZF.thy [snd_def] "snd(<a,b>) = b"


130 
(fn _=> [ (rtac split 1) ]);


131 


132 


133 
(*** split for predicates: result type o ***)


134 


135 
goalw ZF.thy [fsplit_def] "!!R a b. R(a,b) ==> fsplit(R, <a,b>)";


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


137 
val fsplitI = result();


138 


139 
val major::prems = goalw ZF.thy [fsplit_def]


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


141 
by (cut_facts_tac [major] 1);


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


143 
val fsplitE = result();


144 


145 
goal ZF.thy "!!R a b. fsplit(R,<a,b>) ==> R(a,b)";


146 
by (REPEAT (eresolve_tac [asm_rl,fsplitE,Pair_inject,ssubst] 1));


147 
val fsplitD = result();


148 


149 
val pair_cs = upair_cs


150 
addSIs [SigmaI]


151 
addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject,


152 
Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0];


153 
