0

1 
(* Title: ZF/zf.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Basic introduction and elimination rules for ZermeloFraenkel Set Theory


7 
*)


8 


9 
open ZF;


10 


11 
signature ZF_LEMMAS =


12 
sig


13 
val ballE : thm


14 
val ballI : thm


15 
val ball_cong : thm


16 
val ball_rew : thm


17 
val ball_tac : int > tactic


18 
val basic_ZF_congs : thm list


19 
val bexCI : thm


20 
val bexE : thm


21 
val bexI : thm


22 
val bex_cong : thm


23 
val bspec : thm


24 
val CollectD1 : thm


25 
val CollectD2 : thm


26 
val CollectE : thm


27 
val CollectI : thm


28 
val Collect_cong : thm


29 
val emptyE : thm


30 
val empty_subsetI : thm


31 
val equalityCE : thm


32 
val equalityD1 : thm


33 
val equalityD2 : thm


34 
val equalityE : thm


35 
val equalityI : thm


36 
val equality_iffI : thm


37 
val equals0D : thm


38 
val equals0I : thm


39 
val ex1_functional : thm


40 
val InterD : thm


41 
val InterE : thm


42 
val InterI : thm


43 
val INT_E : thm


44 
val INT_I : thm


45 
val lemmas_cs : claset


46 
val PowD : thm


47 
val PowI : thm


48 
val prove_cong_tac : thm list > int > tactic


49 
val RepFunE : thm


50 
val RepFunI : thm


51 
val RepFun_eqI : thm


52 
val RepFun_cong : thm


53 
val ReplaceE : thm


54 
val ReplaceI : thm


55 
val Replace_iff : thm


56 
val Replace_cong : thm


57 
val rev_ballE : thm


58 
val rev_bspec : thm


59 
val rev_subsetD : thm


60 
val separation : thm


61 
val setup_induction : thm


62 
val set_mp_tac : int > tactic


63 
val subsetCE : thm


64 
val subsetD : thm


65 
val subsetI : thm


66 
val subset_refl : thm


67 
val subset_trans : thm


68 
val UnionE : thm


69 
val UnionI : thm


70 
val UN_E : thm


71 
val UN_I : thm


72 
end;


73 


74 


75 
structure ZF_Lemmas : ZF_LEMMAS =


76 
struct


77 


78 
val basic_ZF_congs = mk_congs ZF.thy


79 
["op `", "op ``", "op Int", "op Un", "op ", "op <=", "op :",


80 
"Pow", "Union", "Inter", "fst", "snd", "succ", "Pair", "Upair", "cons",


81 
"domain", "range", "restrict"];


82 


83 
fun prove_cong_tac prems i =


84 
REPEAT (ares_tac (prems@[refl]@FOL_congs@basic_ZF_congs) i);


85 


86 
(*** Bounded universal quantifier ***)


87 


88 
val ballI = prove_goalw ZF.thy [Ball_def]


89 
"[ !!x. x:A ==> P(x) ] ==> ALL x:A. P(x)"


90 
(fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);


91 


92 
val bspec = prove_goalw ZF.thy [Ball_def]


93 
"[ ALL x:A. P(x); x: A ] ==> P(x)"


94 
(fn major::prems=>


95 
[ (rtac (major RS spec RS mp) 1),


96 
(resolve_tac prems 1) ]);


97 


98 
val ballE = prove_goalw ZF.thy [Ball_def]


99 
"[ ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q ] ==> Q"


100 
(fn major::prems=>


101 
[ (rtac (major RS allE) 1),


102 
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);


103 


104 
(*Used in the datatype package*)


105 
val rev_bspec = prove_goal ZF.thy


106 
"!!x A P. [ x: A; ALL x:A. P(x) ] ==> P(x)"


107 
(fn _ =>


108 
[ REPEAT (ares_tac [bspec] 1) ]);


109 


110 
(*Instantiates x first: better for automatic theorem proving?*)


111 
val rev_ballE = prove_goal ZF.thy


112 
"[ ALL x:A. P(x); ~ x:A ==> Q; P(x) ==> Q ] ==> Q"


113 
(fn major::prems=>


114 
[ (rtac (major RS ballE) 1),


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


116 


117 
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)


118 
val ball_tac = dtac bspec THEN' assume_tac;


119 


120 
(*Trival rewrite rule; (ALL x:A.P)<>P holds only if A is nonempty!*)


121 
val ball_rew = prove_goal ZF.thy "(ALL x:A. True) <> True"


122 
(fn prems=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);


123 


124 
(*Congruence rule for rewriting*)


125 
val ball_cong = prove_goalw ZF.thy [Ball_def]


126 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) \


127 
\ ] ==> (ALL x:A. P(x)) <> (ALL x:A'. P'(x))"


128 
(fn prems=> [ (prove_cong_tac prems 1) ]);


129 


130 
(*** Bounded existential quantifier ***)


131 


132 
val bexI = prove_goalw ZF.thy [Bex_def]


133 
"[ P(x); x: A ] ==> EX x:A. P(x)"


134 
(fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);


135 


136 
(*Not of the general form for such rules; ~EX has become ALL~ *)


137 
val bexCI = prove_goal ZF.thy


138 
"[ ALL x:A. ~P(x) ==> P(a); a: A ] ==> EX x:A.P(x)"


139 
(fn prems=>


140 
[ (rtac classical 1),


141 
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);


142 


143 
val bexE = prove_goalw ZF.thy [Bex_def]


144 
"[ EX x:A. P(x); !!x. [ x:A; P(x) ] ==> Q \


145 
\ ] ==> Q"


146 
(fn major::prems=>


147 
[ (rtac (major RS exE) 1),


148 
(REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);


149 


150 
(*We do not even have (EX x:A. True) <> True unless A is nonempty!!*)


151 


152 
val bex_cong = prove_goalw ZF.thy [Bex_def]


153 
"[ A=A'; !!x. x:A' ==> P(x) <> P'(x) \


154 
\ ] ==> (EX x:A. P(x)) <> (EX x:A'. P'(x))"


155 
(fn prems=> [ (prove_cong_tac prems 1) ]);


156 


157 
(*** Rules for subsets ***)


158 


159 
val subsetI = prove_goalw ZF.thy [subset_def]


160 
"(!!x.x:A ==> x:B) ==> A <= B"


161 
(fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);


162 


163 
(*Rule in Modus Ponens style [was called subsetE] *)


164 
val subsetD = prove_goalw ZF.thy [subset_def] "[ A <= B; c:A ] ==> c:B"


165 
(fn major::prems=>


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


167 
(resolve_tac prems 1) ]);


168 


169 
(*Classical elimination rule*)


170 
val subsetCE = prove_goalw ZF.thy [subset_def]


171 
"[ A <= B; ~(c:A) ==> P; c:B ==> P ] ==> P"


172 
(fn major::prems=>


173 
[ (rtac (major RS ballE) 1),


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


175 


176 
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)


177 
val set_mp_tac = dtac subsetD THEN' assume_tac;


178 


179 
(*Sometimes useful with premises in this order*)


180 
val rev_subsetD = prove_goal ZF.thy "!!A B c. [ c:A; A<=B ] ==> c:B"


181 
(fn _=> [REPEAT (ares_tac [subsetD] 1)]);


182 


183 
val subset_refl = prove_goal ZF.thy "A <= A"


184 
(fn _=> [ (rtac subsetI 1), atac 1 ]);


185 


186 
val subset_trans = prove_goal ZF.thy "[ A<=B; B<=C ] ==> A<=C"


187 
(fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]);


188 


189 


190 
(*** Rules for equality ***)


191 


192 
(*Antisymmetry of the subset relation*)


193 
val equalityI = prove_goal ZF.thy "[ A <= B; B <= A ] ==> A = B"


194 
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);


195 


196 
val equality_iffI = prove_goal ZF.thy "(!!x. x:A <> x:B) ==> A = B"


197 
(fn [prem] =>


198 
[ (rtac equalityI 1),


199 
(REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]);


200 


201 
val equalityD1 = prove_goal ZF.thy "A = B ==> A<=B"


202 
(fn prems=>


203 
[ (rtac (extension RS iffD1 RS conjunct1) 1),


204 
(resolve_tac prems 1) ]);


205 


206 
val equalityD2 = prove_goal ZF.thy "A = B ==> B<=A"


207 
(fn prems=>


208 
[ (rtac (extension RS iffD1 RS conjunct2) 1),


209 
(resolve_tac prems 1) ]);


210 


211 
val equalityE = prove_goal ZF.thy


212 
"[ A = B; [ A<=B; B<=A ] ==> P ] ==> P"


213 
(fn prems=>


214 
[ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);


215 


216 
val equalityCE = prove_goal ZF.thy


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


218 
(fn major::prems=>


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


220 
(REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);


221 


222 
(*Lemma for creating induction formulae  for "pattern matching" on p


223 
To make the induction hypotheses usable, apply "spec" or "bspec" to


224 
put universal quantifiers over the free variables in p.


225 
Would it be better to do subgoal_tac "ALL z. p = f(z) > R(z)" ??*)


226 
val setup_induction = prove_goal ZF.thy


227 
"[ p: A; !!z. z: A ==> p=z > R ] ==> R"


228 
(fn prems=>


229 
[ (rtac mp 1),


230 
(REPEAT (resolve_tac (refl::prems) 1)) ]);


231 


232 


233 
(*** Rules for Replace  the derived form of replacement ***)


234 


235 
val ex1_functional = prove_goal ZF.thy


236 
"[ EX! z. P(a,z); P(a,b); P(a,c) ] ==> b = c"


237 
(fn prems=>


238 
[ (cut_facts_tac prems 1),


239 
(best_tac FOL_dup_cs 1) ]);


240 


241 
val Replace_iff = prove_goalw ZF.thy [Replace_def]


242 
"b : {y. x:A, P(x,y)} <> (EX x:A. P(x,b) & (ALL y. P(x,y) > y=b))"


243 
(fn _=>


244 
[ (rtac (replacement RS iff_trans) 1),


245 
(REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1


246 
ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);


247 


248 
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)


249 
val ReplaceI = prove_goal ZF.thy


250 
"[ x: A; P(x,b); !!y. P(x,y) ==> y=b ] ==> \


251 
\ b : {y. x:A, P(x,y)}"


252 
(fn prems=>


253 
[ (rtac (Replace_iff RS iffD2) 1),


254 
(REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]);


255 


256 
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)


257 
val ReplaceE = prove_goal ZF.thy


258 
"[ b : {y. x:A, P(x,y)}; \


259 
\ !!x. [ x: A; P(x,b); ALL y. P(x,y)>y=b ] ==> R \


260 
\ ] ==> R"


261 
(fn prems=>


262 
[ (rtac (Replace_iff RS iffD1 RS bexE) 1),


263 
(etac conjE 2),


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


265 


266 
val Replace_cong = prove_goal ZF.thy


267 
"[ A=B; !!x y. x:B ==> P(x,y) <> Q(x,y) ] ==> \


268 
\ {y. x:A, P(x,y)} = {y. x:B, Q(x,y)}"


269 
(fn prems=>


270 
let val substprems = prems RL [subst, ssubst]


271 
and iffprems = prems RL [iffD1,iffD2]


272 
in [ (rtac equalityI 1),


273 
(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1


274 
ORELSE resolve_tac [subsetI, ReplaceI] 1


275 
ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]


276 
end);


277 


278 


279 
(*** Rules for RepFun ***)


280 


281 
val RepFunI = prove_goalw ZF.thy [RepFun_def]


282 
"!!a A. a : A ==> f(a) : {f(x). x:A}"


283 
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);


284 


285 
(*Useful for coinduction proofs*)


286 
val RepFun_eqI = prove_goal ZF.thy


287 
"!!b a f. [ b=f(a); a : A ] ==> b : {f(x). x:A}"


288 
(fn _ => [ etac ssubst 1, etac RepFunI 1 ]);


289 


290 
val RepFunE = prove_goalw ZF.thy [RepFun_def]


291 
"[ b : {f(x). x:A}; \


292 
\ !!x.[ x:A; b=f(x) ] ==> P ] ==> \


293 
\ P"


294 
(fn major::prems=>


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


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


297 


298 
val RepFun_cong = prove_goalw ZF.thy [RepFun_def]


299 
"[ A=B; !!x. x:B ==> f(x)=g(x) ] ==> \


300 
\ {f(x). x:A} = {g(x). x:B}"


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


302 


303 


304 
(*** Rules for Collect  forming a subset by separation ***)


305 


306 
(*Separation is derivable from Replacement*)


307 
val separation = prove_goalw ZF.thy [Collect_def]


308 
"a : {x:A. P(x)} <> a:A & P(a)"


309 
(fn _=> [ (fast_tac (FOL_cs addIs [bexI,ReplaceI]


310 
addSEs [bexE,ReplaceE]) 1) ]);


311 


312 
val CollectI = prove_goal ZF.thy


313 
"[ a:A; P(a) ] ==> a : {x:A. P(x)}"


314 
(fn prems=>


315 
[ (rtac (separation RS iffD2) 1),


316 
(REPEAT (resolve_tac (prems@[conjI]) 1)) ]);


317 


318 
val CollectE = prove_goal ZF.thy


319 
"[ a : {x:A. P(x)}; [ a:A; P(a) ] ==> R ] ==> R"


320 
(fn prems=>


321 
[ (rtac (separation RS iffD1 RS conjE) 1),


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


323 


324 
val CollectD1 = prove_goal ZF.thy "a : {x:A. P(x)} ==> a:A"


325 
(fn [major]=>


326 
[ (rtac (major RS CollectE) 1),


327 
(assume_tac 1) ]);


328 


329 
val CollectD2 = prove_goal ZF.thy "a : {x:A. P(x)} ==> P(a)"


330 
(fn [major]=>


331 
[ (rtac (major RS CollectE) 1),


332 
(assume_tac 1) ]);


333 


334 
val Collect_cong = prove_goalw ZF.thy [Collect_def]


335 
"[ A=B; !!x. x:B ==> P(x) <> Q(x) ] ==> \


336 
\ {x:A. P(x)} = {x:B. Q(x)}"


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


338 


339 
(*** Rules for Unions ***)


340 


341 
(*The order of the premises presupposes that C is rigid; A may be flexible*)


342 
val UnionI = prove_goal ZF.thy "[ B: C; A: B ] ==> A: Union(C)"


343 
(fn prems=>


344 
[ (resolve_tac [union_iff RS iffD2] 1),


345 
(REPEAT (resolve_tac (prems @ [bexI]) 1)) ]);


346 


347 
val UnionE = prove_goal ZF.thy


348 
"[ A : Union(C); !!B.[ A: B; B: C ] ==> R ] ==> R"


349 
(fn prems=>


350 
[ (resolve_tac [union_iff RS iffD1 RS bexE] 1),


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


352 


353 
(*** Rules for Inter ***)


354 


355 
(*Not obviously useful towards proving InterI, InterD, InterE*)


356 
val Inter_iff = prove_goalw ZF.thy [Inter_def,Ball_def]


357 
"A : Inter(C) <> (ALL x:C. A: x) & (EX x. x:C)"


358 
(fn _=> [ (rtac (separation RS iff_trans) 1),


359 
(fast_tac (FOL_cs addIs [UnionI] addSEs [UnionE]) 1) ]);


360 


361 
(* Intersection is wellbehaved only if the family is nonempty! *)


362 
val InterI = prove_goalw ZF.thy [Inter_def]


363 
"[ !!x. x: C ==> A: x; c:C ] ==> A : Inter(C)"


364 
(fn prems=>


365 
[ (DEPTH_SOLVE (ares_tac ([CollectI,UnionI,ballI] @ prems) 1)) ]);


366 


367 
(*A "destruct" rule  every B in C contains A as an element, but


368 
A:B can hold when B:C does not! This rule is analogous to "spec". *)


369 
val InterD = prove_goalw ZF.thy [Inter_def]


370 
"[ A : Inter(C); B : C ] ==> A : B"


371 
(fn [major,minor]=>


372 
[ (rtac (major RS CollectD2 RS bspec) 1),


373 
(rtac minor 1) ]);


374 


375 
(*"Classical" elimination rule  does not require exhibiting B:C *)


376 
val InterE = prove_goalw ZF.thy [Inter_def]


377 
"[ A : Inter(C); A:B ==> R; ~ B:C ==> R ] ==> R"


378 
(fn major::prems=>


379 
[ (rtac (major RS CollectD2 RS ballE) 1),


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


381 


382 
(*** Rules for Unions of families ***)


383 
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)


384 


385 
(*The order of the premises presupposes that A is rigid; b may be flexible*)


386 
val UN_I = prove_goal ZF.thy "[ a: A; b: B(a) ] ==> b: (UN x:A. B(x))"


387 
(fn prems=>


388 
[ (REPEAT (resolve_tac (prems@[UnionI,RepFunI]) 1)) ]);


389 


390 
val UN_E = prove_goal ZF.thy


391 
"[ b : (UN x:A. B(x)); !!x.[ x: A; b: B(x) ] ==> R ] ==> R"


392 
(fn major::prems=>


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


394 
(REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);


395 


396 


397 
(*** Rules for Intersections of families ***)


398 
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)


399 


400 
val INT_I = prove_goal ZF.thy


401 
"[ !!x. x: A ==> b: B(x); a: A ] ==> b: (INT x:A. B(x))"


402 
(fn prems=>


403 
[ (REPEAT (ares_tac (prems@[InterI,RepFunI]) 1


404 
ORELSE eresolve_tac [RepFunE,ssubst] 1)) ]);


405 


406 
val INT_E = prove_goal ZF.thy


407 
"[ b : (INT x:A. B(x)); a: A ] ==> b : B(a)"


408 
(fn [major,minor]=>


409 
[ (rtac (major RS InterD) 1),


410 
(rtac (minor RS RepFunI) 1) ]);


411 


412 


413 
(*** Rules for Powersets ***)


414 


415 
val PowI = prove_goal ZF.thy "A <= B ==> A : Pow(B)"


416 
(fn [prem]=> [ (rtac (prem RS (power_set RS iffD2)) 1) ]);


417 


418 
val PowD = prove_goal ZF.thy "A : Pow(B) ==> A<=B"


419 
(fn [major]=> [ (rtac (major RS (power_set RS iffD1)) 1) ]);


420 


421 


422 
(*** Rules for the empty set ***)


423 


424 
(*The set {x:0.False} is empty; by foundation it equals 0


425 
See Suppes, page 21.*)


426 
val emptyE = prove_goal ZF.thy "a:0 ==> P"


427 
(fn [major]=>


428 
[ (rtac (foundation RS disjE) 1),


429 
(etac (equalityD2 RS subsetD RS CollectD2 RS FalseE) 1),


430 
(rtac major 1),


431 
(etac bexE 1),


432 
(etac (CollectD2 RS FalseE) 1) ]);


433 


434 
val empty_subsetI = prove_goal ZF.thy "0 <= A"


435 
(fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]);


436 


437 
val equals0I = prove_goal ZF.thy "[ !!y. y:A ==> False ] ==> A=0"


438 
(fn prems=>


439 
[ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1


440 
ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]);


441 


442 
val equals0D = prove_goal ZF.thy "[ A=0; a:A ] ==> P"


443 
(fn [major,minor]=>


444 
[ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);


445 


446 
val lemmas_cs = FOL_cs


447 
addSIs [ballI, InterI, CollectI, PowI, subsetI]


448 
addIs [bexI, UnionI, ReplaceI, RepFunI]


449 
addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,


450 
CollectE, emptyE]


451 
addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];


452 


453 
end;


454 


455 
open ZF_Lemmas;
