0

1 
(* Title: ZF/upair


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 


6 
UNORDERED pairs in ZermeloFraenkel Set Theory


7 


8 
Observe the order of dependence:


9 
Upair is defined in terms of Replace


10 
Un is defined in terms of Upair and Union (similarly for Int)


11 
cons is defined in terms of Upair and Un


12 
Ordered pairs and descriptions are defined using cons ("set notation")


13 
*)


14 


15 
(*** Lemmas about power sets ***)


16 


17 
val Pow_bottom = empty_subsetI RS PowI; (* 0 : Pow(B) *)


18 
val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)


19 
val Pow_neq_0 = Pow_top RSN (2,equals0D); (* Pow(a)=0 ==> P *)


20 


21 


22 
(*** Unordered pairs  Upair ***)


23 


24 
val pairing = prove_goalw ZF.thy [Upair_def]


25 
"c : Upair(a,b) <> (c=a  c=b)"


26 
(fn _ => [ (fast_tac (lemmas_cs addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);


27 


28 
val UpairI1 = prove_goal ZF.thy "a : Upair(a,b)"


29 
(fn _ => [ (rtac (refl RS disjI1 RS (pairing RS iffD2)) 1) ]);


30 


31 
val UpairI2 = prove_goal ZF.thy "b : Upair(a,b)"


32 
(fn _ => [ (rtac (refl RS disjI2 RS (pairing RS iffD2)) 1) ]);


33 


34 
val UpairE = prove_goal ZF.thy


35 
"[ a : Upair(b,c); a=b ==> P; a=c ==> P ] ==> P"


36 
(fn major::prems=>


37 
[ (rtac (major RS (pairing RS iffD1 RS disjE)) 1),


38 
(REPEAT (eresolve_tac prems 1)) ]);


39 


40 
(*** Rules for binary union  Un  defined via Upair ***)


41 


42 
val UnI1 = prove_goalw ZF.thy [Un_def] "c : A ==> c : A Un B"


43 
(fn [prem]=> [ (rtac (prem RS (UpairI1 RS UnionI)) 1) ]);


44 


45 
val UnI2 = prove_goalw ZF.thy [Un_def] "c : B ==> c : A Un B"


46 
(fn [prem]=> [ (rtac (prem RS (UpairI2 RS UnionI)) 1) ]);


47 


48 
val UnE = prove_goalw ZF.thy [Un_def]


49 
"[ c : A Un B; c:A ==> P; c:B ==> P ] ==> P"


50 
(fn major::prems=>


51 
[ (rtac (major RS UnionE) 1),


52 
(etac UpairE 1),


53 
(REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]);


54 


55 
val Un_iff = prove_goal ZF.thy "c : A Un B <> (c:A  c:B)"


56 
(fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);


57 


58 
(*Classical introduction rule: no commitment to A vs B*)


59 
val UnCI = prove_goal ZF.thy "(~c : B ==> c : A) ==> c : A Un B"


60 
(fn [prem]=>


61 
[ (rtac (disjCI RS (Un_iff RS iffD2)) 1),


62 
(etac prem 1) ]);


63 


64 


65 
(*** Rules for small intersection  Int  defined via Upair ***)


66 


67 
val IntI = prove_goalw ZF.thy [Int_def]


68 
"[ c : A; c : B ] ==> c : A Int B"


69 
(fn prems=>


70 
[ (REPEAT (resolve_tac (prems @ [UpairI1,InterI]) 1


71 
ORELSE eresolve_tac [UpairE, ssubst] 1)) ]);


72 


73 
val IntD1 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : A"


74 
(fn [major]=>


75 
[ (rtac (UpairI1 RS (major RS InterD)) 1) ]);


76 


77 
val IntD2 = prove_goalw ZF.thy [Int_def] "c : A Int B ==> c : B"


78 
(fn [major]=>


79 
[ (rtac (UpairI2 RS (major RS InterD)) 1) ]);


80 


81 
val IntE = prove_goal ZF.thy


82 
"[ c : A Int B; [ c:A; c:B ] ==> P ] ==> P"


83 
(fn prems=>


84 
[ (resolve_tac prems 1),


85 
(REPEAT (resolve_tac (prems RL [IntD1,IntD2]) 1)) ]);


86 


87 
val Int_iff = prove_goal ZF.thy "c : A Int B <> (c:A & c:B)"


88 
(fn _ => [ (fast_tac (lemmas_cs addSIs [IntI] addSEs [IntE]) 1) ]);


89 


90 


91 
(*** Rules for set difference  defined via Upair ***)


92 


93 
val DiffI = prove_goalw ZF.thy [Diff_def]


94 
"[ c : A; ~ c : B ] ==> c : A  B"


95 
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI]) 1)) ]);


96 


97 
val DiffD1 = prove_goalw ZF.thy [Diff_def]


98 
"c : A  B ==> c : A"


99 
(fn [major]=> [ (rtac (major RS CollectD1) 1) ]);


100 


101 
val DiffD2 = prove_goalw ZF.thy [Diff_def]


102 
"[ c : A  B; c : B ] ==> P"


103 
(fn [major,minor]=> [ (rtac (minor RS (major RS CollectD2 RS notE)) 1) ]);


104 


105 
val DiffE = prove_goal ZF.thy


106 
"[ c : A  B; [ c:A; ~ c:B ] ==> P ] ==> P"


107 
(fn prems=>


108 
[ (resolve_tac prems 1),


109 
(REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);


110 


111 
val Diff_iff = prove_goal ZF.thy "c : AB <> (c:A & ~ c:B)"


112 
(fn _ => [ (fast_tac (lemmas_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);


113 


114 
(*** Rules for cons  defined via Un and Upair ***)


115 


116 
val consI1 = prove_goalw ZF.thy [cons_def] "a : cons(a,B)"


117 
(fn _ => [ (rtac (UpairI1 RS UnI1) 1) ]);


118 


119 
val consI2 = prove_goalw ZF.thy [cons_def] "a : B ==> a : cons(b,B)"


120 
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);


121 


122 
val consE = prove_goalw ZF.thy [cons_def]


123 
"[ a : cons(b,A); a=b ==> P; a:A ==> P ] ==> P"


124 
(fn major::prems=>


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


126 
(REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);


127 


128 
val cons_iff = prove_goal ZF.thy "a : cons(b,A) <> (a=b  a:A)"


129 
(fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);


130 


131 
(*Classical introduction rule*)


132 
val consCI = prove_goal ZF.thy "(~ a:B ==> a=b) ==> a: cons(b,B)"


133 
(fn [prem]=>


134 
[ (rtac (disjCI RS (cons_iff RS iffD2)) 1),


135 
(etac prem 1) ]);


136 


137 
(*** Singletons  using cons ***)


138 


139 
val singletonI = prove_goal ZF.thy "a : {a}"


140 
(fn _=> [ (rtac consI1 1) ]);


141 


142 
val singletonE = prove_goal ZF.thy "[ a: {b}; a=b ==> P ] ==> P"


143 
(fn major::prems=>


144 
[ (rtac (major RS consE) 1),


145 
(REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);


146 


147 


148 
(*** Rules for Descriptions ***)


149 


150 
val the_equality = prove_goalw ZF.thy [the_def]


151 
"[ P(a); !!x. P(x) ==> x=a ] ==> (THE x. P(x)) = a"


152 
(fn prems=>


153 
[ (fast_tac (lemmas_cs addIs ([equalityI,singletonI]@prems)


154 
addEs (prems RL [subst])) 1) ]);


155 


156 
(* Only use this if you already know EX!x. P(x) *)


157 
val the_equality2 = prove_goal ZF.thy


158 
"[ EX! x. P(x); P(a) ] ==> (THE x. P(x)) = a"


159 
(fn major::prems=>


160 
[ (rtac the_equality 1),


161 
(rtac (major RS ex1_equalsE) 2),


162 
(REPEAT (ares_tac prems 1)) ]);


163 


164 
val theI = prove_goal ZF.thy "EX! x. P(x) ==> P(THE x. P(x))"


165 
(fn [major]=>


166 
[ (rtac (major RS ex1E) 1),


167 
(resolve_tac [major RS the_equality2 RS ssubst] 1),


168 
(REPEAT (assume_tac 1)) ]);


169 


170 
val the_cong = prove_goalw ZF.thy [the_def]


171 
"[ !!y. P(y) <> Q(y) ] ==> (THE x. P(x)) = (THE x. Q(x))"


172 
(fn prems=> [ (prove_cong_tac (prems@[Replace_cong]) 1) ]);


173 


174 


175 
(*** if  a conditional expression for formulae ***)


176 


177 
goalw ZF.thy [if_def] "if(True,a,b) = a";


178 
by (fast_tac (lemmas_cs addIs [the_equality]) 1);


179 
val if_true = result();


180 


181 
goalw ZF.thy [if_def] "if(False,a,b) = b";


182 
by (fast_tac (lemmas_cs addIs [the_equality]) 1);


183 
val if_false = result();


184 


185 
val prems = goalw ZF.thy [if_def]


186 
"[ P<>Q; a=c; b=d ] ==> if(P,a,b) = if(Q,c,d)";


187 
by (REPEAT (resolve_tac (prems@[refl,the_cong]@FOL_congs) 1));


188 
val if_cong = result();


189 


190 
(*Not needed for rewriting, since P would rewrite to True anyway*)


191 
val prems = goalw ZF.thy [if_def] "P ==> if(P,a,b) = a";


192 
by (cut_facts_tac prems 1);


193 
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);


194 
val if_P = result();


195 


196 
(*Not needed for rewriting, since P would rewrite to False anyway*)


197 
val prems = goalw ZF.thy [if_def] "~P ==> if(P,a,b) = b";


198 
by (cut_facts_tac prems 1);


199 
by (fast_tac (lemmas_cs addSIs [the_equality]) 1);


200 
val if_not_P = result();


201 


202 
val if_ss =


203 
FOL_ss addcongs (if_cong :: mk_typed_congs ZF.thy [("P", "i=>o")]


204 
@ basic_ZF_congs)


205 
addrews [if_true,if_false];


206 


207 
val expand_if = prove_goal ZF.thy


208 
"P(if(Q,x,y)) <> ((Q > P(x)) & (~Q > P(y)))"


209 
(fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),


210 
(ASM_SIMP_TAC if_ss 1),


211 
(ASM_SIMP_TAC if_ss 1) ]);


212 


213 
val prems = goal ZF.thy


214 
"[ P ==> a: A; ~P ==> b: A ] ==> if(P,a,b): A";


215 
by (res_inst_tac [("Q","P")] (excluded_middle RS disjE) 1);


216 
by (ALLGOALS (ASM_SIMP_TAC (if_ss addrews prems)));


217 
val if_type = result();


218 


219 


220 
(*** Foundation lemmas ***)


221 


222 
val mem_anti_sym = prove_goal ZF.thy "[ a:b; b:a ] ==> P"


223 
(fn prems=>


224 
[ (rtac disjE 1),


225 
(res_inst_tac [("A","{a,b}")] foundation 1),


226 
(etac equals0D 1),


227 
(rtac consI1 1),


228 
(fast_tac (lemmas_cs addIs (prems@[consI1,consI2])


229 
addSEs [consE,equalityE]) 1) ]);


230 


231 
val mem_anti_refl = prove_goal ZF.thy "a:a ==> P"


232 
(fn [major]=> [ (rtac (major RS (major RS mem_anti_sym)) 1) ]);


233 


234 
val mem_not_refl = prove_goal ZF.thy "~ a:a"


235 
(K [ (rtac notI 1), (etac mem_anti_refl 1) ]);


236 


237 
(*** Rules for succ ***)


238 


239 
val succI1 = prove_goalw ZF.thy [succ_def] "i : succ(i)"


240 
(fn _=> [ (rtac consI1 1) ]);


241 


242 
val succI2 = prove_goalw ZF.thy [succ_def]


243 
"i : j ==> i : succ(j)"


244 
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);


245 


246 
(*Classical introduction rule*)


247 
val succCI = prove_goalw ZF.thy [succ_def]


248 
"(~ i:j ==> i=j) ==> i: succ(j)"


249 
(fn prems=> [ (rtac consCI 1), (eresolve_tac prems 1) ]);


250 


251 
val succE = prove_goalw ZF.thy [succ_def]


252 
"[ i : succ(j); i=j ==> P; i:j ==> P ] ==> P"


253 
(fn major::prems=>


254 
[ (rtac (major RS consE) 1),


255 
(REPEAT (eresolve_tac prems 1)) ]);


256 


257 
val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"


258 
(fn [major]=>


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


260 
(rtac succI1 1) ]);


261 


262 
(*Useful for rewriting*)


263 
val succ_not_0 = prove_goal ZF.thy "~ succ(n)=0"


264 
(fn _=> [ (rtac notI 1), (etac succ_neq_0 1) ]);


265 


266 
(* succ(c) <= B ==> c : B *)


267 
val succ_subsetD = succI1 RSN (2,subsetD);


268 


269 
val succ_inject = prove_goal ZF.thy "succ(m) = succ(n) ==> m=n"


270 
(fn [major]=>


271 
[ (rtac (major RS equalityE) 1),


272 
(REPEAT (eresolve_tac [asm_rl, sym, succE, make_elim succ_subsetD,


273 
mem_anti_sym] 1)) ]);


274 


275 
val succ_inject_iff = prove_goal ZF.thy "succ(m) = succ(n) <> m=n"


276 
(fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);


277 


278 
(*UpairI1/2 should become UpairCI; mem_anti_refl as a hazE? *)


279 
val upair_cs = lemmas_cs


280 
addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]


281 
addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];


282 
