# HG changeset patch # User paulson # Date 1025772712 -7200 # Node ID 28ce81eff3de92f223d6f3222d3a79ab48113704 # Parent 53e201efdaa21f3d829ea69fc7a98901260e7463 separation of M_axioms into M_triv_axioms and M_axioms diff -r 53e201efdaa2 -r 28ce81eff3de src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Thu Jul 04 10:50:24 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Thu Jul 04 10:51:52 2002 +0200 @@ -171,13 +171,13 @@ extensionality :: "(i=>o) => o" "extensionality(M) == - \x y. M(x) --> M(y) --> (\z. M(z) --> (z \ x <-> z \ y)) --> x=y" + \x[M]. \y[M]. (\z[M]. z \ x <-> z \ y) --> x=y" separation :: "[i=>o, i=>o] => o" --{*Big problem: the formula @{text P} should only involve parameters belonging to @{text M}. Don't see how to enforce that.*} "separation(M,P) == - \z. M(z) --> (\y. M(y) & (\x. M(x) --> (x \ y <-> x \ z & P(x))))" + \z[M]. \y[M]. \x[M]. x \ y <-> x \ z & P(x)" upair_ax :: "(i=>o) => o" "upair_ax(M) == \x y. M(x) --> M(y) --> (\z. M(z) & upair(M,x,y,z))" @@ -269,8 +269,9 @@ by (simp add: univ_def Collect_in_VLimit Limit_nat) lemma "separation(\x. x \ univ(0), P)" -apply (simp add: separation_def) -apply (blast intro: Collect_in_univ Transset_0) +apply (simp add: separation_def, clarify) +apply (rule_tac x = "Collect(x,P)" in bexI) +apply (blast intro: Collect_in_univ Transset_0)+ done text{*Unordered pairing axiom*} @@ -350,8 +351,7 @@ by (simp add: strong_replacement_def) lemma separationD: - "[| separation(M,P); M(z) |] - ==> \y. M(y) & (\x. M(x) --> (x \ y <-> x \ z & P(x)))" + "[| separation(M,P); M(z) |] ==> \y[M]. \x[M]. x \ y <-> x \ z & P(x)" by (simp add: separation_def) @@ -381,7 +381,7 @@ text{*The class M is assumed to be transitive and to satisfy some relativized ZF axioms*} -locale M_axioms = +locale M_triv_axioms = fixes M assumes transM: "[| y\x; M(x) |] ==> M(y)" and nonempty [simp]: "M(0)" @@ -390,7 +390,326 @@ and power_ax: "power_ax(M)" and replacement: "replacement(M,P)" and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*) - and Inter_separation: + +lemma (in M_triv_axioms) ball_abs [simp]: + "M(A) ==> (\x\A. M(x) --> P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_triv_axioms) rall_abs [simp]: + "M(A) ==> (\x[M]. x\A --> P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_triv_axioms) bex_abs [simp]: + "M(A) ==> (\x\A. M(x) & P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_triv_axioms) rex_abs [simp]: + "M(A) ==> (\x[M]. x\A & P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_triv_axioms) ball_iff_equiv: + "M(A) ==> (\x. M(x) --> (x\A <-> P(x))) <-> + (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\A)" +by (blast intro: transM) + +text{*Simplifies proofs of equalities when there's an iff-equality + available for rewriting, universally quantified over M. *} +lemma (in M_triv_axioms) M_equalityI: + "[| !!x. M(x) ==> x\A <-> x\B; M(A); M(B) |] ==> A=B" +by (blast intro!: equalityI dest: transM) + +lemma (in M_triv_axioms) empty_abs [simp]: + "M(z) ==> empty(M,z) <-> z=0" +apply (simp add: empty_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) subset_abs [simp]: + "M(A) ==> subset(M,A,B) <-> A \ B" +apply (simp add: subset_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) upair_abs [simp]: + "M(z) ==> upair(M,a,b,z) <-> z={a,b}" +apply (simp add: upair_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) upair_in_M_iff [iff]: + "M({a,b}) <-> M(a) & M(b)" +apply (insert upair_ax, simp add: upair_ax_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) singleton_in_M_iff [iff]: + "M({a}) <-> M(a)" +by (insert upair_in_M_iff [of a a], simp) + +lemma (in M_triv_axioms) pair_abs [simp]: + "M(z) ==> pair(M,a,b,z) <-> z=" +apply (simp add: pair_def ZF.Pair_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) pair_in_M_iff [iff]: + "M() <-> M(a) & M(b)" +by (simp add: ZF.Pair_def) + +lemma (in M_triv_axioms) pair_components_in_M: + "[| \ A; M(A) |] ==> M(x) & M(y)" +apply (simp add: Pair_def) +apply (blast dest: transM) +done + +lemma (in M_triv_axioms) cartprod_abs [simp]: + "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B" +apply (simp add: cartprod_def) +apply (rule iffI) + apply (blast intro!: equalityI intro: transM dest!: rspec) +apply (blast dest: transM) +done + +lemma (in M_triv_axioms) union_abs [simp]: + "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b" +apply (simp add: union_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) inter_abs [simp]: + "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b" +apply (simp add: inter_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) setdiff_abs [simp]: + "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b" +apply (simp add: setdiff_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) Union_abs [simp]: + "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)" +apply (simp add: big_union_def) +apply (blast intro!: equalityI dest: transM) +done + +lemma (in M_triv_axioms) Union_closed [intro,simp]: + "M(A) ==> M(Union(A))" +by (insert Union_ax, simp add: Union_ax_def) + +lemma (in M_triv_axioms) Un_closed [intro,simp]: + "[| M(A); M(B) |] ==> M(A Un B)" +by (simp only: Un_eq_Union, blast) + +lemma (in M_triv_axioms) cons_closed [intro,simp]: + "[| M(a); M(A) |] ==> M(cons(a,A))" +by (subst cons_eq [symmetric], blast) + +lemma (in M_triv_axioms) successor_abs [simp]: + "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)" +by (simp add: successor_def, blast) + +lemma (in M_triv_axioms) succ_in_M_iff [iff]: + "M(succ(a)) <-> M(a)" +apply (simp add: succ_def) +apply (blast intro: transM) +done + +lemma (in M_triv_axioms) separation_closed [intro,simp]: + "[| separation(M,P); M(A) |] ==> M(Collect(A,P))" +apply (insert separation, simp add: separation_def) +apply (drule rspec, assumption, clarify) +apply (subgoal_tac "y = Collect(A,P)", blast) +apply (blast dest: transM) +done + +text{*Probably the premise and conclusion are equivalent*} +lemma (in M_triv_axioms) strong_replacementI [rule_format]: + "[| \A. M(A) --> separation(M, %u. \x\A. P(x,u)) |] + ==> strong_replacement(M,P)" +apply (simp add: strong_replacement_def, clarify) +apply (frule replacementD [OF replacement], assumption, clarify) +apply (drule_tac x=A in spec, clarify) +apply (drule_tac z=Y in separationD, assumption, clarify) +apply (blast dest: transM) +done + + +(*The last premise expresses that P takes M to M*) +lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]: + "[| strong_replacement(M,P); M(A); univalent(M,A,P); + !!x y. [| x\A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))" +apply (simp add: strong_replacement_def) +apply (drule spec [THEN mp], auto) +apply (subgoal_tac "Replace(A,P) = Y") + apply simp +apply (rule equality_iffI) +apply (simp add: Replace_iff, safe) + apply (blast dest: transM) +apply (frule transM, assumption) + apply (simp add: univalent_def) + apply (drule spec [THEN mp, THEN iffD1], assumption, assumption) + apply (blast dest: transM) +done + +(*The first premise can't simply be assumed as a schema. + It is essential to take care when asserting instances of Replacement. + Let K be a nonconstructible subset of nat and define + f(x) = x if x:K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a + nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f)) + even for f : M -> M. +*) +lemma (in M_triv_axioms) RepFun_closed [intro,simp]: + "[| strong_replacement(M, \x y. y = f(x)); M(A); \x\A. M(f(x)) |] + ==> M(RepFun(A,f))" +apply (simp add: RepFun_def) +apply (rule strong_replacement_closed) +apply (auto dest: transM simp add: univalent_def) +done + +lemma (in M_triv_axioms) lam_closed [intro,simp]: + "[| strong_replacement(M, \x y. y = ); M(A); \x\A. M(b(x)) |] + ==> M(\x\A. b(x))" +by (simp add: lam_def, blast dest: transM) + +lemma (in M_triv_axioms) image_abs [simp]: + "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A" +apply (simp add: image_def) +apply (rule iffI) + apply (blast intro!: equalityI dest: transM, blast) +done + +text{*What about @{text Pow_abs}? Powerset is NOT absolute! + This result is one direction of absoluteness.*} + +lemma (in M_triv_axioms) powerset_Pow: + "powerset(M, x, Pow(x))" +by (simp add: powerset_def) + +text{*But we can't prove that the powerset in @{text M} includes the + real powerset.*} +lemma (in M_triv_axioms) powerset_imp_subset_Pow: + "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)" +apply (simp add: powerset_def) +apply (blast dest: transM) +done + +lemma (in M_triv_axioms) nat_into_M [intro]: + "n \ nat ==> M(n)" +by (induct n rule: nat_induct, simp_all) + +lemma (in M_triv_axioms) nat_case_closed: + "[|M(k); M(a); \m[M]. M(b(m))|] ==> M(nat_case(a,b,k))" +apply (case_tac "k=0", simp) +apply (case_tac "\m. k = succ(m)", force) +apply (simp add: nat_case_def) +done + +lemma (in M_triv_axioms) Inl_in_M_iff [iff]: + "M(Inl(a)) <-> M(a)" +by (simp add: Inl_def) + +lemma (in M_triv_axioms) Inr_in_M_iff [iff]: + "M(Inr(a)) <-> M(a)" +by (simp add: Inr_def) + + +subsection{*Absoluteness for ordinals*} +text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} + +lemma (in M_triv_axioms) lt_closed: + "[| j M(j)" +by (blast dest: ltD intro: transM) + +lemma (in M_triv_axioms) transitive_set_abs [simp]: + "M(a) ==> transitive_set(M,a) <-> Transset(a)" +by (simp add: transitive_set_def Transset_def) + +lemma (in M_triv_axioms) ordinal_abs [simp]: + "M(a) ==> ordinal(M,a) <-> Ord(a)" +by (simp add: ordinal_def Ord_def) + +lemma (in M_triv_axioms) limit_ordinal_abs [simp]: + "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" +apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) +apply (simp add: lt_def, blast) +done + +lemma (in M_triv_axioms) successor_ordinal_abs [simp]: + "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\b. M(b) & a = succ(b))" +apply (simp add: successor_ordinal_def, safe) +apply (drule Ord_cases_disj, auto) +done + +lemma finite_Ord_is_nat: + "[| Ord(a); ~ Limit(a); \x\a. ~ Limit(x) |] ==> a \ nat" +by (induct a rule: trans_induct3, simp_all) + +lemma naturals_not_limit: "a \ nat ==> ~ Limit(a)" +by (induct a rule: nat_induct, auto) + +lemma (in M_triv_axioms) finite_ordinal_abs [simp]: + "M(a) ==> finite_ordinal(M,a) <-> a \ nat" +apply (simp add: finite_ordinal_def) +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord + dest: Ord_trans naturals_not_limit) +done + +lemma Limit_non_Limit_implies_nat: + "[| Limit(a); \x\a. ~ Limit(x) |] ==> a = nat" +apply (rule le_anti_sym) +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord) + apply (simp add: lt_def) + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) +apply (erule nat_le_Limit) +done + +lemma (in M_triv_axioms) omega_abs [simp]: + "M(a) ==> omega(M,a) <-> a = nat" +apply (simp add: omega_def) +apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit) +done + +lemma (in M_triv_axioms) number1_abs [simp]: + "M(a) ==> number1(M,a) <-> a = 1" +by (simp add: number1_def) + +lemma (in M_triv_axioms) number1_abs [simp]: + "M(a) ==> number2(M,a) <-> a = succ(1)" +by (simp add: number2_def) + +lemma (in M_triv_axioms) number3_abs [simp]: + "M(a) ==> number3(M,a) <-> a = succ(succ(1))" +by (simp add: number3_def) + +text{*Kunen continued to 20...*} + +(*Could not get this to work. The \x\nat is essential because everything + but the recursion variable must stay unchanged. But then the recursion + equations only hold for x\nat (or in some other set) and not for the + whole of the class M. + consts + natnumber_aux :: "[i=>o,i] => i" + + primrec + "natnumber_aux(M,0) = (\x\nat. if empty(M,x) then 1 else 0)" + "natnumber_aux(M,succ(n)) = + (\x\nat. if (\y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) + then 1 else 0)" + + constdefs + natnumber :: "[i=>o,i,i] => o" + "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1" + + lemma (in M_triv_axioms) [simp]: + "natnumber(M,0,x) == x=0" +*) + +subsection{*Some instances of separation and strong replacement*} + +locale M_axioms = M_triv_axioms + +assumes Inter_separation: "M(A) ==> separation(M, \x. \y[M]. y\A --> x\y)" and cartprod_separation: "[| M(A); M(B) |] @@ -398,9 +717,6 @@ and image_separation: "[| M(A); M(r) |] ==> separation(M, \y. \p[M]. p\r & (\x[M]. x\A & pair(M,x,y,p)))" - and vimage_separation: - "[| M(A); M(r) |] - ==> separation(M, \x. \p[M]. p\r & (\y[M]. y\A & pair(M,x,y,p)))" and converse_separation: "M(r) ==> separation(M, \z. \p\r. M(p) & (\x[M]. \y[M]. pair(M,x,y,p) & pair(M,y,x,z)))" @@ -447,219 +763,13 @@ ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" -lemma (in M_axioms) ball_abs [simp]: - "M(A) ==> (\x\A. M(x) --> P(x)) <-> (\x\A. P(x))" -by (blast intro: transM) - -lemma (in M_axioms) rall_abs [simp]: - "M(A) ==> (\x[M]. x\A --> P(x)) <-> (\x\A. P(x))" -by (blast intro: transM) - -lemma (in M_axioms) bex_abs [simp]: - "M(A) ==> (\x\A. M(x) & P(x)) <-> (\x\A. P(x))" -by (blast intro: transM) - -lemma (in M_axioms) rex_abs [simp]: - "M(A) ==> (\x[M]. x\A & P(x)) <-> (\x\A. P(x))" -by (blast intro: transM) - -lemma (in M_axioms) ball_iff_equiv: - "M(A) ==> (\x. M(x) --> (x\A <-> P(x))) <-> - (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\A)" -by (blast intro: transM) - -text{*Simplifies proofs of equalities when there's an iff-equality - available for rewriting, universally quantified over M. *} -lemma (in M_axioms) M_equalityI: - "[| !!x. M(x) ==> x\A <-> x\B; M(A); M(B) |] ==> A=B" -by (blast intro!: equalityI dest: transM) - -lemma (in M_axioms) empty_abs [simp]: - "M(z) ==> empty(M,z) <-> z=0" -apply (simp add: empty_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) subset_abs [simp]: - "M(A) ==> subset(M,A,B) <-> A \ B" -apply (simp add: subset_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) upair_abs [simp]: - "M(z) ==> upair(M,a,b,z) <-> z={a,b}" -apply (simp add: upair_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) upair_in_M_iff [iff]: - "M({a,b}) <-> M(a) & M(b)" -apply (insert upair_ax, simp add: upair_ax_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) singleton_in_M_iff [iff]: - "M({a}) <-> M(a)" -by (insert upair_in_M_iff [of a a], simp) - -lemma (in M_axioms) pair_abs [simp]: - "M(z) ==> pair(M,a,b,z) <-> z=" -apply (simp add: pair_def ZF.Pair_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) pair_in_M_iff [iff]: - "M() <-> M(a) & M(b)" -by (simp add: ZF.Pair_def) - -lemma (in M_axioms) pair_components_in_M: - "[| \ A; M(A) |] ==> M(x) & M(y)" -apply (simp add: Pair_def) -apply (blast dest: transM) -done - -lemma (in M_axioms) cartprod_abs [simp]: - "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B" -apply (simp add: cartprod_def) -apply (rule iffI) - apply (blast intro!: equalityI intro: transM dest!: rspec) -apply (blast dest: transM) -done - -lemma (in M_axioms) union_abs [simp]: - "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b" -apply (simp add: union_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) inter_abs [simp]: - "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b" -apply (simp add: inter_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) setdiff_abs [simp]: - "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b" -apply (simp add: setdiff_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) Union_abs [simp]: - "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)" -apply (simp add: big_union_def) -apply (blast intro!: equalityI dest: transM) -done - -lemma (in M_axioms) Union_closed [intro,simp]: - "M(A) ==> M(Union(A))" -by (insert Union_ax, simp add: Union_ax_def) - -lemma (in M_axioms) Un_closed [intro,simp]: - "[| M(A); M(B) |] ==> M(A Un B)" -by (simp only: Un_eq_Union, blast) - -lemma (in M_axioms) cons_closed [intro,simp]: - "[| M(a); M(A) |] ==> M(cons(a,A))" -by (subst cons_eq [symmetric], blast) - -lemma (in M_axioms) successor_abs [simp]: - "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)" -by (simp add: successor_def, blast) - -lemma (in M_axioms) succ_in_M_iff [iff]: - "M(succ(a)) <-> M(a)" -apply (simp add: succ_def) -apply (blast intro: transM) -done - -lemma (in M_axioms) separation_closed [intro,simp]: - "[| separation(M,P); M(A) |] ==> M(Collect(A,P))" -apply (insert separation, simp add: separation_def) -apply (drule spec [THEN mp], assumption, clarify) -apply (subgoal_tac "y = Collect(A,P)", blast) -apply (blast dest: transM) -done - -text{*Probably the premise and conclusion are equivalent*} -lemma (in M_axioms) strong_replacementI [rule_format]: - "[| \A. M(A) --> separation(M, %u. \x\A. P(x,u)) |] - ==> strong_replacement(M,P)" -apply (simp add: strong_replacement_def, clarify) -apply (frule replacementD [OF replacement], assumption, clarify) -apply (drule_tac x=A in spec, clarify) -apply (drule_tac z=Y in separationD, assumption, clarify) -apply (blast dest: transM) -done - - -(*The last premise expresses that P takes M to M*) -lemma (in M_axioms) strong_replacement_closed [intro,simp]: - "[| strong_replacement(M,P); M(A); univalent(M,A,P); - !!x y. [| x\A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))" -apply (simp add: strong_replacement_def) -apply (drule spec [THEN mp], auto) -apply (subgoal_tac "Replace(A,P) = Y") - apply simp -apply (rule equality_iffI) -apply (simp add: Replace_iff, safe) - apply (blast dest: transM) -apply (frule transM, assumption) - apply (simp add: univalent_def) - apply (drule spec [THEN mp, THEN iffD1], assumption, assumption) - apply (blast dest: transM) -done - -(*The first premise can't simply be assumed as a schema. - It is essential to take care when asserting instances of Replacement. - Let K be a nonconstructible subset of nat and define - f(x) = x if x:K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a - nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f)) - even for f : M -> M. -*) -lemma (in M_axioms) RepFun_closed [intro,simp]: - "[| strong_replacement(M, \x y. y = f(x)); M(A); \x\A. M(f(x)) |] - ==> M(RepFun(A,f))" -apply (simp add: RepFun_def) -apply (rule strong_replacement_closed) -apply (auto dest: transM simp add: univalent_def) -done - -lemma (in M_axioms) lam_closed [intro,simp]: - "[| strong_replacement(M, \x y. y = ); M(A); \x\A. M(b(x)) |] - ==> M(\x\A. b(x))" -by (simp add: lam_def, blast dest: transM) - -lemma (in M_axioms) image_abs [simp]: - "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A" -apply (simp add: image_def) -apply (rule iffI) - apply (blast intro!: equalityI dest: transM, blast) -done - -text{*What about @{text Pow_abs}? Powerset is NOT absolute! - This result is one direction of absoluteness.*} - -lemma (in M_axioms) powerset_Pow: - "powerset(M, x, Pow(x))" -by (simp add: powerset_def) - -text{*But we can't prove that the powerset in @{text M} includes the - real powerset.*} -lemma (in M_axioms) powerset_imp_subset_Pow: - "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)" -apply (simp add: powerset_def) -apply (blast dest: transM) -done - lemma (in M_axioms) cartprod_iff_lemma: "[| M(C); \u[M]. u \ C <-> (\x\A. \y\B. u = {{x}, {x,y}}); powerset(M, A \ B, p1); powerset(M, p1, p2); M(p2) |] ==> C = {u \ p2 . \x\A. \y\B. u = {{x}, {x,y}}}" apply (simp add: powerset_def) apply (rule equalityI, clarify, simp) - apply (frule transM, assumption) - apply (frule transM, assumption, simp) apply blast apply clarify @@ -698,7 +808,6 @@ apply (insert cartprod_separation [of A B], auto) done - text{*All the lemmas above are necessary because Powerset is not absolute. I should have used Replacement instead!*} lemma (in M_axioms) cartprod_closed [intro,simp]: @@ -709,6 +818,39 @@ "[| M(A); M(B) |] ==> M(A+B)" by (simp add: sum_def) + +subsubsection {*converse of a relation*} + +lemma (in M_axioms) M_converse_iff: + "M(r) ==> + converse(r) = + {z \ Union(Union(r)) * Union(Union(r)). + \p\r. \x[M]. \y[M]. p = \x,y\ & z = \y,x\}" +apply (rule equalityI) + prefer 2 apply (blast dest: transM, clarify, simp) +apply (simp add: Pair_def) +apply (blast dest: transM) +done + +lemma (in M_axioms) converse_closed [intro,simp]: + "M(r) ==> M(converse(r))" +apply (simp add: M_converse_iff) +apply (insert converse_separation [of r], simp) +done + +lemma (in M_axioms) converse_abs [simp]: + "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)" +apply (simp add: is_converse_def) +apply (rule iffI) + prefer 2 apply blast +apply (rule M_equalityI) + apply simp + apply (blast dest: transM)+ +done + + +subsubsection {*image, preimage, domain, range*} + lemma (in M_axioms) image_closed [intro,simp]: "[| M(A); M(r) |] ==> M(r``A)" apply (simp add: image_iff_Collect) @@ -724,9 +866,10 @@ lemma (in M_axioms) vimage_closed [intro,simp]: "[| M(A); M(r) |] ==> M(r-``A)" -apply (simp add: vimage_iff_Collect) -apply (insert vimage_separation [of A r], simp) -done +by (simp add: vimage_def) + + +subsubsection{*Domain, range and field*} lemma (in M_axioms) domain_abs [simp]: "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)" @@ -759,27 +902,7 @@ by (simp add: domain_closed range_closed Un_closed field_def) -lemma (in M_axioms) M_converse_iff: - "M(r) ==> - converse(r) = - {z \ range(r) * domain(r). \p\r. \x[M]. \y[M]. p = \x,y\ & z = \y,x\}" -by (blast dest: transM) - -lemma (in M_axioms) converse_closed [intro,simp]: - "M(r) ==> M(converse(r))" -apply (simp add: M_converse_iff) -apply (insert converse_separation [of r], simp) -done - -lemma (in M_axioms) converse_abs [simp]: - "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)" -apply (simp add: is_converse_def) -apply (rule iffI) - prefer 2 apply blast -apply (rule M_equalityI) - apply simp - apply (blast dest: transM)+ -done +subsubsection{*Relations, functions and application*} lemma (in M_axioms) relation_abs [simp]: "M(r) ==> is_relation(M,r) <-> relation(r)" @@ -796,8 +919,7 @@ lemma (in M_axioms) apply_closed [intro,simp]: "[|M(f); M(a)|] ==> M(f`a)" -apply (simp add: apply_def) -done +by (simp add: apply_def) lemma (in M_axioms) apply_abs: "[| function(f); M(f); M(y) |] @@ -831,32 +953,8 @@ "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \ bij(A,B)" by (simp add: bijection_def bij_def) -text{*no longer needed*} -lemma (in M_axioms) restriction_is_function: - "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] - ==> function(z)" -apply (rotate_tac 1) -apply (simp add: restriction_def ball_iff_equiv) -apply (unfold function_def, blast) -done -lemma (in M_axioms) restriction_abs [simp]: - "[| M(f); M(A); M(z) |] - ==> restriction(M,f,A,z) <-> z = restrict(f,A)" -apply (simp add: ball_iff_equiv restriction_def restrict_def) -apply (blast intro!: equalityI dest: transM) -done - - -lemma (in M_axioms) M_restrict_iff: - "M(r) ==> restrict(r,A) = {z \ r . \x\A. \y[M]. z = \x, y\}" -by (simp add: restrict_def, blast dest: transM) - -lemma (in M_axioms) restrict_closed [intro,simp]: - "[| M(A); M(r) |] ==> M(restrict(r,A))" -apply (simp add: M_restrict_iff) -apply (insert restrict_separation [of A], simp) -done +subsubsection{*Composition of relations*} lemma (in M_axioms) M_comp_iff: "[| M(r); M(s) |] @@ -890,24 +988,32 @@ apply (blast del: allE dest: transM)+ done -lemma (in M_axioms) nat_into_M [intro]: - "n \ nat ==> M(n)" -by (induct n rule: nat_induct, simp_all) - -lemma (in M_axioms) nat_case_closed: - "[|M(k); M(a); \m[M]. M(b(m))|] ==> M(nat_case(a,b,k))" -apply (case_tac "k=0", simp) -apply (case_tac "\m. k = succ(m)", force) -apply (simp add: nat_case_def) +text{*no longer needed*} +lemma (in M_axioms) restriction_is_function: + "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] + ==> function(z)" +apply (rotate_tac 1) +apply (simp add: restriction_def ball_iff_equiv) +apply (unfold function_def, blast) done -lemma (in M_axioms) Inl_in_M_iff [iff]: - "M(Inl(a)) <-> M(a)" -by (simp add: Inl_def) +lemma (in M_axioms) restriction_abs [simp]: + "[| M(f); M(A); M(z) |] + ==> restriction(M,f,A,z) <-> z = restrict(f,A)" +apply (simp add: ball_iff_equiv restriction_def restrict_def) +apply (blast intro!: equalityI dest: transM) +done + -lemma (in M_axioms) Inr_in_M_iff [iff]: - "M(Inr(a)) <-> M(a)" -by (simp add: Inr_def) +lemma (in M_axioms) M_restrict_iff: + "M(r) ==> restrict(r,A) = {z \ r . \x\A. \y[M]. z = \x, y\}" +by (simp add: restrict_def, blast dest: transM) + +lemma (in M_axioms) restrict_closed [intro,simp]: + "[| M(A); M(r) |] ==> M(restrict(r,A))" +apply (simp add: M_restrict_iff) +apply (insert restrict_separation [of A], simp) +done lemma (in M_axioms) Inter_abs [simp]: "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)" @@ -925,7 +1031,7 @@ apply (frule Inter_closed, force+) done -subsection{*Functions and function space*} +subsubsection{*Functions and function space*} text{*M contains all finite functions*} lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: @@ -977,96 +1083,4 @@ apply (simp add: funspace_succ nat_into_M) done - -subsection{*Absoluteness for ordinals*} -text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} - -lemma (in M_axioms) lt_closed: - "[| j M(j)" -by (blast dest: ltD intro: transM) - -lemma (in M_axioms) transitive_set_abs [simp]: - "M(a) ==> transitive_set(M,a) <-> Transset(a)" -by (simp add: transitive_set_def Transset_def) - -lemma (in M_axioms) ordinal_abs [simp]: - "M(a) ==> ordinal(M,a) <-> Ord(a)" -by (simp add: ordinal_def Ord_def) - -lemma (in M_axioms) limit_ordinal_abs [simp]: - "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" -apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) -apply (simp add: lt_def, blast) -done - -lemma (in M_axioms) successor_ordinal_abs [simp]: - "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\b. M(b) & a = succ(b))" -apply (simp add: successor_ordinal_def, safe) -apply (drule Ord_cases_disj, auto) -done - -lemma finite_Ord_is_nat: - "[| Ord(a); ~ Limit(a); \x\a. ~ Limit(x) |] ==> a \ nat" -by (induct a rule: trans_induct3, simp_all) - -lemma naturals_not_limit: "a \ nat ==> ~ Limit(a)" -by (induct a rule: nat_induct, auto) - -lemma (in M_axioms) finite_ordinal_abs [simp]: - "M(a) ==> finite_ordinal(M,a) <-> a \ nat" -apply (simp add: finite_ordinal_def) -apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord - dest: Ord_trans naturals_not_limit) -done - -lemma Limit_non_Limit_implies_nat: "[| Limit(a); \x\a. ~ Limit(x) |] ==> a = nat" -apply (rule le_anti_sym) -apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord) - apply (simp add: lt_def) - apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) -apply (erule nat_le_Limit) -done - -lemma (in M_axioms) omega_abs [simp]: - "M(a) ==> omega(M,a) <-> a = nat" -apply (simp add: omega_def) -apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit) -done - -lemma (in M_axioms) number1_abs [simp]: - "M(a) ==> number1(M,a) <-> a = 1" -by (simp add: number1_def) - -lemma (in M_axioms) number1_abs [simp]: - "M(a) ==> number2(M,a) <-> a = succ(1)" -by (simp add: number2_def) - -lemma (in M_axioms) number3_abs [simp]: - "M(a) ==> number3(M,a) <-> a = succ(succ(1))" -by (simp add: number3_def) - -text{*Kunen continued to 20...*} - -(*Could not get this to work. The \x\nat is essential because everything - but the recursion variable must stay unchanged. But then the recursion - equations only hold for x\nat (or in some other set) and not for the - whole of the class M. - consts - natnumber_aux :: "[i=>o,i] => i" - - primrec - "natnumber_aux(M,0) = (\x\nat. if empty(M,x) then 1 else 0)" - "natnumber_aux(M,succ(n)) = - (\x\nat. if (\y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) - then 1 else 0)" - - constdefs - natnumber :: "[i=>o,i,i] => o" - "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1" - - lemma (in M_axioms) [simp]: - "natnumber(M,0,x) == x=0" -*) - - end