Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
(* Title: ZF/zf.ML
ID: $Id$
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
Copyright 1992 University of Cambridge
Basic introduction and elimination rules for Zermelo-Fraenkel Set Theory
*)
open ZF;
signature ZF_LEMMAS =
sig
val ballE : thm
val ballI : thm
val ball_cong : thm
val ball_simp : thm
val ball_tac : int -> tactic
val bexCI : thm
val bexE : thm
val bexI : thm
val bex_cong : thm
val bspec : thm
val CollectD1 : thm
val CollectD2 : thm
val CollectE : thm
val CollectI : thm
val Collect_cong : thm
val emptyE : thm
val empty_subsetI : thm
val equalityCE : thm
val equalityD1 : thm
val equalityD2 : thm
val equalityE : thm
val equalityI : thm
val equality_iffI : thm
val equals0D : thm
val equals0I : thm
val ex1_functional : thm
val InterD : thm
val InterE : thm
val InterI : thm
val INT_E : thm
val INT_I : thm
val lemmas_cs : claset
val PowD : thm
val PowI : thm
val RepFunE : thm
val RepFunI : thm
val RepFun_eqI : thm
val RepFun_cong : thm
val ReplaceE : thm
val ReplaceI : thm
val Replace_iff : thm
val Replace_cong : thm
val rev_ballE : thm
val rev_bspec : thm
val rev_subsetD : thm
val separation : thm
val setup_induction : thm
val set_mp_tac : int -> tactic
val subsetCE : thm
val subsetD : thm
val subsetI : thm
val subset_refl : thm
val subset_trans : thm
val UnionE : thm
val UnionI : thm
val UN_E : thm
val UN_I : thm
end;
structure ZF_Lemmas : ZF_LEMMAS =
struct
(*** Bounded universal quantifier ***)
val ballI = prove_goalw ZF.thy [Ball_def]
"[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)"
(fn prems=> [ (REPEAT (ares_tac (prems @ [allI,impI]) 1)) ]);
val bspec = prove_goalw ZF.thy [Ball_def]
"[| ALL x:A. P(x); x: A |] ==> P(x)"
(fn major::prems=>
[ (rtac (major RS spec RS mp) 1),
(resolve_tac prems 1) ]);
val ballE = prove_goalw ZF.thy [Ball_def]
"[| ALL x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q"
(fn major::prems=>
[ (rtac (major RS allE) 1),
(REPEAT (eresolve_tac (prems@[asm_rl,impCE]) 1)) ]);
(*Used in the datatype package*)
val rev_bspec = prove_goal ZF.thy
"!!x A P. [| x: A; ALL x:A. P(x) |] ==> P(x)"
(fn _ =>
[ REPEAT (ares_tac [bspec] 1) ]);
(*Instantiates x first: better for automatic theorem proving?*)
val rev_ballE = prove_goal ZF.thy
"[| ALL x:A. P(x); ~ x:A ==> Q; P(x) ==> Q |] ==> Q"
(fn major::prems=>
[ (rtac (major RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
val ball_tac = dtac bspec THEN' assume_tac;
(*Trival rewrite rule; (ALL x:A.P)<->P holds only if A is nonempty!*)
val ball_simp = prove_goal ZF.thy "(ALL x:A. True) <-> True"
(fn _=> [ (REPEAT (ares_tac [TrueI,ballI,iffI] 1)) ]);
(*Congruence rule for rewriting*)
val ball_cong = prove_goalw ZF.thy [Ball_def]
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> Ball(A,P) <-> Ball(A',P')"
(fn prems=> [ (simp_tac (FOL_ss addsimps prems) 1) ]);
(*** Bounded existential quantifier ***)
val bexI = prove_goalw ZF.thy [Bex_def]
"[| P(x); x: A |] ==> EX x:A. P(x)"
(fn prems=> [ (REPEAT (ares_tac (prems @ [exI,conjI]) 1)) ]);
(*Not of the general form for such rules; ~EX has become ALL~ *)
val bexCI = prove_goal ZF.thy
"[| ALL x:A. ~P(x) ==> P(a); a: A |] ==> EX x:A.P(x)"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
val bexE = prove_goalw ZF.thy [Bex_def]
"[| EX x:A. P(x); !!x. [| x:A; P(x) |] ==> Q \
\ |] ==> Q"
(fn major::prems=>
[ (rtac (major RS exE) 1),
(REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1)) ]);
(*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
val bex_cong = prove_goalw ZF.thy [Bex_def]
"[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) \
\ |] ==> Bex(A,P) <-> Bex(A',P')"
(fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [conj_cong]) 1) ]);
(*** Rules for subsets ***)
val subsetI = prove_goalw ZF.thy [subset_def]
"(!!x.x:A ==> x:B) ==> A <= B"
(fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
(*Rule in Modus Ponens style [was called subsetE] *)
val subsetD = prove_goalw ZF.thy [subset_def] "[| A <= B; c:A |] ==> c:B"
(fn major::prems=>
[ (rtac (major RS bspec) 1),
(resolve_tac prems 1) ]);
(*Classical elimination rule*)
val subsetCE = prove_goalw ZF.thy [subset_def]
"[| A <= B; ~(c:A) ==> P; c:B ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
val set_mp_tac = dtac subsetD THEN' assume_tac;
(*Sometimes useful with premises in this order*)
val rev_subsetD = prove_goal ZF.thy "!!A B c. [| c:A; A<=B |] ==> c:B"
(fn _=> [REPEAT (ares_tac [subsetD] 1)]);
val subset_refl = prove_goal ZF.thy "A <= A"
(fn _=> [ (rtac subsetI 1), atac 1 ]);
val subset_trans = prove_goal ZF.thy "[| A<=B; B<=C |] ==> A<=C"
(fn prems=> [ (REPEAT (ares_tac ([subsetI]@(prems RL [subsetD])) 1)) ]);
(*** Rules for equality ***)
(*Anti-symmetry of the subset relation*)
val equalityI = prove_goal ZF.thy "[| A <= B; B <= A |] ==> A = B"
(fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
val equality_iffI = prove_goal ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
(fn [prem] =>
[ (rtac equalityI 1),
(REPEAT (ares_tac [subsetI, prem RS iffD1, prem RS iffD2] 1)) ]);
val equalityD1 = prove_goal ZF.thy "A = B ==> A<=B"
(fn prems=>
[ (rtac (extension RS iffD1 RS conjunct1) 1),
(resolve_tac prems 1) ]);
val equalityD2 = prove_goal ZF.thy "A = B ==> B<=A"
(fn prems=>
[ (rtac (extension RS iffD1 RS conjunct2) 1),
(resolve_tac prems 1) ]);
val equalityE = prove_goal ZF.thy
"[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"
(fn prems=>
[ (DEPTH_SOLVE (resolve_tac (prems@[equalityD1,equalityD2]) 1)) ]);
val equalityCE = prove_goal ZF.thy
"[| A = B; [| c:A; c:B |] ==> P; [| ~ c:A; ~ c:B |] ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS equalityE) 1),
(REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1)) ]);
(*Lemma for creating induction formulae -- for "pattern matching" on p
To make the induction hypotheses usable, apply "spec" or "bspec" to
put universal quantifiers over the free variables in p.
Would it be better to do subgoal_tac "ALL z. p = f(z) --> R(z)" ??*)
val setup_induction = prove_goal ZF.thy
"[| p: A; !!z. z: A ==> p=z --> R |] ==> R"
(fn prems=>
[ (rtac mp 1),
(REPEAT (resolve_tac (refl::prems) 1)) ]);
(*** Rules for Replace -- the derived form of replacement ***)
val ex1_functional = prove_goal ZF.thy
"[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
(fn prems=>
[ (cut_facts_tac prems 1),
(best_tac FOL_dup_cs 1) ]);
val Replace_iff = prove_goalw ZF.thy [Replace_def]
"b : {y. x:A, P(x,y)} <-> (EX x:A. P(x,b) & (ALL y. P(x,y) --> y=b))"
(fn _=>
[ (rtac (replacement RS iff_trans) 1),
(REPEAT (ares_tac [refl,bex_cong,iffI,ballI,allI,conjI,impI,ex1I] 1
ORELSE eresolve_tac [conjE, spec RS mp, ex1_functional] 1)) ]);
(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
val ReplaceI = prove_goal ZF.thy
"[| x: A; P(x,b); !!y. P(x,y) ==> y=b |] ==> \
\ b : {y. x:A, P(x,y)}"
(fn prems=>
[ (rtac (Replace_iff RS iffD2) 1),
(REPEAT (ares_tac (prems@[bexI,conjI,allI,impI]) 1)) ]);
(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
val ReplaceE = prove_goal ZF.thy
"[| b : {y. x:A, P(x,y)}; \
\ !!x. [| x: A; P(x,b); ALL y. P(x,y)-->y=b |] ==> R \
\ |] ==> R"
(fn prems=>
[ (rtac (Replace_iff RS iffD1 RS bexE) 1),
(etac conjE 2),
(REPEAT (ares_tac prems 1)) ]);
val Replace_cong = prove_goal ZF.thy
"[| A=B; !!x y. x:B ==> P(x,y) <-> Q(x,y) |] ==> \
\ Replace(A,P) = Replace(B,Q)"
(fn prems=>
let val substprems = prems RL [subst, ssubst]
and iffprems = prems RL [iffD1,iffD2]
in [ (rtac equalityI 1),
(REPEAT (eresolve_tac (substprems@[asm_rl, ReplaceE, spec RS mp]) 1
ORELSE resolve_tac [subsetI, ReplaceI] 1
ORELSE (resolve_tac iffprems 1 THEN assume_tac 2))) ]
end);
(*** Rules for RepFun ***)
val RepFunI = prove_goalw ZF.thy [RepFun_def]
"!!a A. a : A ==> f(a) : {f(x). x:A}"
(fn _ => [ (REPEAT (ares_tac [ReplaceI,refl] 1)) ]);
(*Useful for co-induction proofs*)
val RepFun_eqI = prove_goal ZF.thy
"!!b a f. [| b=f(a); a : A |] ==> b : {f(x). x:A}"
(fn _ => [ etac ssubst 1, etac RepFunI 1 ]);
val RepFunE = prove_goalw ZF.thy [RepFun_def]
"[| b : {f(x). x:A}; \
\ !!x.[| x:A; b=f(x) |] ==> P |] ==> \
\ P"
(fn major::prems=>
[ (rtac (major RS ReplaceE) 1),
(REPEAT (ares_tac prems 1)) ]);
val RepFun_cong = prove_goalw ZF.thy [RepFun_def]
"[| A=B; !!x. x:B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
(fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
(*** Rules for Collect -- forming a subset by separation ***)
(*Separation is derivable from Replacement*)
val separation = prove_goalw ZF.thy [Collect_def]
"a : {x:A. P(x)} <-> a:A & P(a)"
(fn _=> [ (fast_tac (FOL_cs addIs [bexI,ReplaceI]
addSEs [bexE,ReplaceE]) 1) ]);
val CollectI = prove_goal ZF.thy
"[| a:A; P(a) |] ==> a : {x:A. P(x)}"
(fn prems=>
[ (rtac (separation RS iffD2) 1),
(REPEAT (resolve_tac (prems@[conjI]) 1)) ]);
val CollectE = prove_goal ZF.thy
"[| a : {x:A. P(x)}; [| a:A; P(a) |] ==> R |] ==> R"
(fn prems=>
[ (rtac (separation RS iffD1 RS conjE) 1),
(REPEAT (ares_tac prems 1)) ]);
val CollectD1 = prove_goal ZF.thy "a : {x:A. P(x)} ==> a:A"
(fn [major]=>
[ (rtac (major RS CollectE) 1),
(assume_tac 1) ]);
val CollectD2 = prove_goal ZF.thy "a : {x:A. P(x)} ==> P(a)"
(fn [major]=>
[ (rtac (major RS CollectE) 1),
(assume_tac 1) ]);
val Collect_cong = prove_goalw ZF.thy [Collect_def]
"[| A=B; !!x. x:B ==> P(x) <-> Q(x) |] ==> Collect(A,P) = Collect(B,Q)"
(fn prems=> [ (simp_tac (FOL_ss addcongs [Replace_cong] addsimps prems) 1) ]);
(*** Rules for Unions ***)
(*The order of the premises presupposes that C is rigid; A may be flexible*)
val UnionI = prove_goal ZF.thy "[| B: C; A: B |] ==> A: Union(C)"
(fn prems=>
[ (resolve_tac [union_iff RS iffD2] 1),
(REPEAT (resolve_tac (prems @ [bexI]) 1)) ]);
val UnionE = prove_goal ZF.thy
"[| A : Union(C); !!B.[| A: B; B: C |] ==> R |] ==> R"
(fn prems=>
[ (resolve_tac [union_iff RS iffD1 RS bexE] 1),
(REPEAT (ares_tac prems 1)) ]);
(*** Rules for Inter ***)
(*Not obviously useful towards proving InterI, InterD, InterE*)
val Inter_iff = prove_goalw ZF.thy [Inter_def,Ball_def]
"A : Inter(C) <-> (ALL x:C. A: x) & (EX x. x:C)"
(fn _=> [ (rtac (separation RS iff_trans) 1),
(fast_tac (FOL_cs addIs [UnionI] addSEs [UnionE]) 1) ]);
(* Intersection is well-behaved only if the family is non-empty! *)
val InterI = prove_goalw ZF.thy [Inter_def]
"[| !!x. x: C ==> A: x; c:C |] ==> A : Inter(C)"
(fn prems=>
[ (DEPTH_SOLVE (ares_tac ([CollectI,UnionI,ballI] @ prems) 1)) ]);
(*A "destruct" rule -- every B in C contains A as an element, but
A:B can hold when B:C does not! This rule is analogous to "spec". *)
val InterD = prove_goalw ZF.thy [Inter_def]
"[| A : Inter(C); B : C |] ==> A : B"
(fn [major,minor]=>
[ (rtac (major RS CollectD2 RS bspec) 1),
(rtac minor 1) ]);
(*"Classical" elimination rule -- does not require exhibiting B:C *)
val InterE = prove_goalw ZF.thy [Inter_def]
"[| A : Inter(C); A:B ==> R; ~ B:C ==> R |] ==> R"
(fn major::prems=>
[ (rtac (major RS CollectD2 RS ballE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
(*** Rules for Unions of families ***)
(* UN x:A. B(x) abbreviates Union({B(x). x:A}) *)
(*The order of the premises presupposes that A is rigid; b may be flexible*)
val UN_I = prove_goal ZF.thy "[| a: A; b: B(a) |] ==> b: (UN x:A. B(x))"
(fn prems=>
[ (REPEAT (resolve_tac (prems@[UnionI,RepFunI]) 1)) ]);
val UN_E = prove_goal ZF.thy
"[| b : (UN x:A. B(x)); !!x.[| x: A; b: B(x) |] ==> R |] ==> R"
(fn major::prems=>
[ (rtac (major RS UnionE) 1),
(REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
(*** Rules for Intersections of families ***)
(* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)
val INT_I = prove_goal ZF.thy
"[| !!x. x: A ==> b: B(x); a: A |] ==> b: (INT x:A. B(x))"
(fn prems=>
[ (REPEAT (ares_tac (prems@[InterI,RepFunI]) 1
ORELSE eresolve_tac [RepFunE,ssubst] 1)) ]);
val INT_E = prove_goal ZF.thy
"[| b : (INT x:A. B(x)); a: A |] ==> b : B(a)"
(fn [major,minor]=>
[ (rtac (major RS InterD) 1),
(rtac (minor RS RepFunI) 1) ]);
(*** Rules for Powersets ***)
val PowI = prove_goal ZF.thy "A <= B ==> A : Pow(B)"
(fn [prem]=> [ (rtac (prem RS (power_set RS iffD2)) 1) ]);
val PowD = prove_goal ZF.thy "A : Pow(B) ==> A<=B"
(fn [major]=> [ (rtac (major RS (power_set RS iffD1)) 1) ]);
(*** Rules for the empty set ***)
(*The set {x:0.False} is empty; by foundation it equals 0
See Suppes, page 21.*)
val emptyE = prove_goal ZF.thy "a:0 ==> P"
(fn [major]=>
[ (rtac (foundation RS disjE) 1),
(etac (equalityD2 RS subsetD RS CollectD2 RS FalseE) 1),
(rtac major 1),
(etac bexE 1),
(etac (CollectD2 RS FalseE) 1) ]);
val empty_subsetI = prove_goal ZF.thy "0 <= A"
(fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]);
val equals0I = prove_goal ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
(fn prems=>
[ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1
ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]);
val equals0D = prove_goal ZF.thy "[| A=0; a:A |] ==> P"
(fn [major,minor]=>
[ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
val lemmas_cs = FOL_cs
addSIs [ballI, InterI, CollectI, PowI, subsetI]
addIs [bexI, UnionI, ReplaceI, RepFunI]
addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE,
CollectE, emptyE]
addEs [rev_ballE, InterD, make_elim InterD, subsetD, subsetCE];
end;
open ZF_Lemmas;