# HG changeset patch # User paulson # Date 1024912761 -7200 # Node ID 714f7a423a15f60629902d3238450e297625de91 # Parent 7b37e218f298ac6f650d158b58b4095f11ff58a3 development and tweaks diff -r 7b37e218f298 -r 714f7a423a15 src/ZF/AC/AC15_WO6.thy --- a/src/ZF/AC/AC15_WO6.thy Mon Jun 24 11:59:14 2002 +0200 +++ b/src/ZF/AC/AC15_WO6.thy Mon Jun 24 11:59:21 2002 +0200 @@ -40,10 +40,9 @@ lemma cons_times_nat_not_Finite: "0\A ==> \B \ {cons(0,x*nat). x \ A}. ~Finite(B)" apply clarify -apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite]) apply (rule nat_not_Finite [THEN notE] ) apply (subgoal_tac "x ~= 0") -apply (blast intro: lepoll_Sigma [THEN lepoll_Finite], blast) + apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+ done lemma lemma1: "[| Union(C)=A; a \ A |] ==> \B \ C. a \ B & B \ A" diff -r 7b37e218f298 -r 714f7a423a15 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Mon Jun 24 11:59:14 2002 +0200 +++ b/src/ZF/Constructible/Formula.thy Mon Jun 24 11:59:21 2002 +0200 @@ -22,54 +22,7 @@ lemma [simp]: "(bool_of_o(P) = 0) <-> ~P" by (simp add: bool_of_o_def) -(*????????????????Cardinal.ML*) -lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)" -by (blast intro: Finite_cons subset_Finite) - -lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)" -by (simp add: succ_def) - -declare Finite_0 [simp] - -lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))" -by (erule Finite_induct, simp_all) - -lemma Finite_RepFun_lemma [rule_format]: - "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|] - ==> \A. x = RepFun(A,f) --> Finite(A)" -apply (erule Finite_induct) - apply clarify - apply (case_tac "A=0", simp) - apply (blast del: allE, clarify) -apply (subgoal_tac "\z\A. x = f(z)") - prefer 2 apply (blast del: allE elim: equalityE, clarify) -apply (subgoal_tac "B = {f(u) . u \ A - {z}}") - apply (blast intro: Diff_sing_Finite) -apply (thin_tac "\A. ?P(A) --> Finite(A)") -apply (rule equalityI) - apply (blast intro: elim: equalityE) -apply (blast intro: elim: equalityCE) -done - -text{*I don't know why, but if the premise is expressed using meta-connectives -then the simplifier cannot prove it automatically in conditional rewriting.*} -lemma Finite_RepFun_iff: - "(\x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)" -by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f]) - -lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))" -apply (erule Finite_induct) -apply (simp_all add: Pow_insert Finite_Un Finite_RepFun) -done - -lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)" -apply (subgoal_tac "Finite({{x} . x \ A})") - apply (simp add: Finite_RepFun_iff ) -apply (blast intro: subset_Finite) -done - -lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)" -by (blast intro: Finite_Pow Finite_Pow_imp_Finite) +(*????????????????CardinalArith *) lemma Finite_Vset: "i \ nat ==> Finite(Vset(i))"; apply (erule nat_induct) @@ -922,6 +875,10 @@ apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) done + +lemma Ord_in_L: "Ord(i) ==> L(i)" +by (blast intro: Ord_in_Lset L_I) + text{*This is lrank(lrank(a)) = lrank(a) *} declare Ord_lrank [THEN lrank_of_Ord, simp] @@ -963,13 +920,13 @@ subsection{*For L to satisfy the ZF axioms*} -lemma Union_in_L: "L(X) ==> L(Union(X))" +theorem Union_in_L: "L(X) ==> L(Union(X))" apply (simp add: L_def, clarify) apply (drule Ord_imp_greater_Limit) apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) done -lemma doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})" +theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})" apply (simp add: L_def, clarify) apply (drule Ord2_imp_greater_Limit, assumption) apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) @@ -1000,7 +957,7 @@ apply (auto intro: L_I iff: Lset_succ_lrank_iff) done -lemma LPow_in_L: "L(X) ==> L({y \ Pow(X). L(y)})" +theorem LPow_in_L: "L(X) ==> L({y \ Pow(X). L(y)})" by (blast intro: L_I dest: L_D LPow_in_Lset) end diff -r 7b37e218f298 -r 714f7a423a15 src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Mon Jun 24 11:59:14 2002 +0200 +++ b/src/ZF/Constructible/ROOT.ML Mon Jun 24 11:59:21 2002 +0200 @@ -1,4 +1,11 @@ +(* Title: ZF/Constructible/ROOT.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2002 University of Cambridge + +Inner Models and Absoluteness +*) + use_thy "Reflection"; use_thy "WFrec"; -use_thy "WF_extras"; use_thy "L_axioms"; diff -r 7b37e218f298 -r 714f7a423a15 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Mon Jun 24 11:59:14 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Mon Jun 24 11:59:21 2002 +0200 @@ -18,15 +18,15 @@ "pair(M,a,b,z) == \x. M(x) & upair(M,a,a,x) & (\y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))" + union :: "[i=>o,i,i,i] => o" + "union(M,a,b,z) == \x. M(x) --> (x \ z <-> x \ a | x \ b)" + successor :: "[i=>o,i,i] => o" "successor(M,a,z) == \x. M(x) & upair(M,a,a,x) & union(M,x,a,z)" powerset :: "[i=>o,i,i] => o" "powerset(M,A,z) == \x. M(x) --> (x \ z <-> subset(M,x,A))" - union :: "[i=>o,i,i,i] => o" - "union(M,a,b,z) == \x. M(x) --> (x \ z <-> x \ a | x \ b)" - inter :: "[i=>o,i,i,i] => o" "inter(M,a,b,z) == \x. M(x) --> (x \ z <-> x \ a & x \ b)" @@ -72,6 +72,11 @@ "is_range(M,r,z) == \y. M(y) --> (y \ z <-> (\w\r. M(w) & (\x. M(x) & pair(M,x,y,w))))" + is_field :: "[i=>o,i,i] => o" + "is_field(M,r,z) == + \dr. M(dr) & is_domain(M,r,dr) & + (\rr. M(rr) & is_range(M,r,rr) & union(M,dr,rr,z))" + is_relation :: "[i=>o,i] => o" "is_relation(M,r) == (\z\r. M(z) --> (\x y. M(x) & M(y) & pair(M,x,y,z)))" @@ -91,6 +96,13 @@ is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & (\u\r. M(u) --> (\x y. M(x) & M(y) & pair(M,x,y,u) --> y\B))" + composition :: "[i=>o,i,i,i] => o" + "composition(M,r,s,t) == + \p. M(p) --> (p \ t <-> + (\x. M(x) & (\y. M(y) & (\z. M(z) & + p = \x,z\ & \x,y\ \ s & \y,z\ \ r))))" + + injection :: "[i=>o,i,i,i] => o" "injection(M,A,B,f) == typed_function(M,A,B,f) & @@ -373,6 +385,7 @@ and Union_ax: "Union_ax(M)" and power_ax: "power_ax(M)" and replacement: "replacement(M,P)" + and M_nat: "M(nat)" (*i.e. the axiom of infinity*) and Inter_separation: "M(A) ==> separation(M, \x. \y\A. M(y) --> x\y)" and cartprod_separation: @@ -398,7 +411,7 @@ and pred_separation: "[| M(r); M(x) |] ==> separation(M, \y. \p\r. M(p) & pair(M,y,x,p))" and Memrel_separation: - "separation(M, \z. \x y. M(x) & M(y) & pair(M,x,y,z) \ x \ y)" + "separation(M, \z. \x y. M(x) & M(y) & pair(M,x,y,z) & x \ y)" and obase_separation: --{*part of the order type formalization*} "[| M(A); M(r) |] @@ -407,8 +420,8 @@ order_isomorphism(M,par,r,x,mx,g))" and well_ord_iso_separation: "[| M(A); M(f); M(r) |] - ==> separation (M, \x. x\A --> (\y. M(y) \ (\p. M(p) \ - fun_apply(M,f,x,y) \ pair(M,y,x,p) \ p \ r)))" + ==> separation (M, \x. x\A --> (\y. M(y) & (\p. M(p) & + fun_apply(M,f,x,y) & pair(M,y,x,p) & p \ r)))" and obase_equals_separation: "[| M(A); M(r) |] ==> separation @@ -419,7 +432,7 @@ and is_recfun_separation: --{*for well-founded recursion. NEEDS RELATIVIZATION*} "[| M(A); M(f); M(g); M(a); M(b) |] - ==> separation(M, \x. x \ A --> \x,a\ \ r \ \x,b\ \ r \ f`x \ g`x)" + ==> separation(M, \x. x \ A --> \x,a\ \ r & \x,b\ \ r & f`x \ g`x)" and omap_replacement: "[| M(A); M(r) |] ==> strong_replacement(M, @@ -440,6 +453,12 @@ (\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) @@ -516,15 +535,15 @@ apply (blast intro!: equalityI dest: transM) done -lemma (in M_axioms) Union_closed [intro]: +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]: +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]: +lemma (in M_axioms) cons_closed [intro,simp]: "[| M(a); M(A) |] ==> M(cons(a,A))" by (subst cons_eq [symmetric], blast) @@ -538,7 +557,7 @@ apply (blast intro: transM) done -lemma (in M_axioms) separation_closed [intro]: +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) @@ -565,7 +584,7 @@ (*The last premise expresses that P takes M to M*) -lemma (in M_axioms) strong_replacement_closed [intro]: +lemma (in M_axioms) strong_replacement_closed [intro,simp]: "[| strong_replacement(M,P); M(A); univalent(M,A,P); !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))" apply (simp add: strong_replacement_def) @@ -589,7 +608,7 @@ 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]: +lemma (in M_axioms) RepFun_closed [intro,simp]: "[| strong_replacement(M, \x y. y = f(x)); M(A); \x. M(x) --> M(f(x)) |] ==> M(RepFun(A,f))" apply (simp add: RepFun_def) @@ -669,20 +688,20 @@ prefer 6 apply (rule refl) prefer 4 apply assumption prefer 4 apply assumption -apply (insert cartprod_separation [of A B], simp, blast+) +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]: +lemma (in M_axioms) cartprod_closed [intro,simp]: "[| M(A); M(B) |] ==> M(A*B)" by (frule cartprod_closed_lemma, assumption, force) -lemma (in M_axioms) image_closed [intro]: +lemma (in M_axioms) image_closed [intro,simp]: "[| M(A); M(r) |] ==> M(r``A)" apply (simp add: image_iff_Collect) -apply (insert image_separation [of A r], simp, blast) +apply (insert image_separation [of A r], simp) done lemma (in M_axioms) vimage_abs [simp]: @@ -692,10 +711,10 @@ apply (blast intro!: equalityI dest: transM, blast) done -lemma (in M_axioms) vimage_closed [intro]: +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, blast) +apply (insert vimage_separation [of A r], simp) done lemma (in M_axioms) domain_abs [simp]: @@ -704,10 +723,9 @@ apply (blast intro!: equalityI dest: transM) done -lemma (in M_axioms) domain_closed [intro]: +lemma (in M_axioms) domain_closed [intro,simp]: "M(r) ==> M(domain(r))" apply (simp add: domain_eq_vimage) -apply (blast intro: vimage_closed) done lemma (in M_axioms) range_abs [simp]: @@ -716,24 +734,31 @@ apply (blast intro!: equalityI dest: transM) done -lemma (in M_axioms) range_closed [intro]: +lemma (in M_axioms) range_closed [intro,simp]: "M(r) ==> M(range(r))" apply (simp add: range_eq_image) -apply (blast intro: image_closed) done +lemma (in M_axioms) field_abs [simp]: + "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)" +by (simp add: domain_closed range_closed is_field_def field_def) + +lemma (in M_axioms) field_closed [intro,simp]: + "M(r) ==> M(field(r))" +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(x) \ (\y. M(y) \ p = \x,y\ \ z = \y,x\)}" + \p\r. \x. M(x) & (\y. M(y) & p = \x,y\ & z = \y,x\)}" by (blast dest: transM) -lemma (in M_axioms) converse_closed [intro]: +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) -apply (blast intro: image_closed) +apply (insert converse_separation [of r], simp) done lemma (in M_axioms) relation_abs [simp]: @@ -749,10 +774,9 @@ apply (blast dest: pair_components_in_M)+ done -lemma (in M_axioms) apply_closed [intro]: +lemma (in M_axioms) apply_closed [intro,simp]: "[|M(f); M(a)|] ==> M(f`a)" -apply (simp add: apply_def) -apply (blast intro: elim:); +apply (simp add: apply_def) done lemma (in M_axioms) apply_abs: @@ -808,19 +832,18 @@ "M(r) ==> restrict(r,A) = {z \ r . \x\A. \y. M(y) & z = \x, y\}" by (simp add: restrict_def, blast dest: transM) -lemma (in M_axioms) restrict_closed [intro]: +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, blast) +apply (insert restrict_separation [of A], simp) done - lemma (in M_axioms) M_comp_iff: "[| M(r); M(s) |] ==> r O s = {xz \ domain(s) * range(r). - \x. M(x) \ (\y. M(y) \ (\z. M(z) \ - xz = \x,z\ \ \x,y\ \ s \ \y,z\ \ r))}" + \x. M(x) & (\y. M(y) & (\z. M(z) & + xz = \x,z\ & \x,y\ \ s & \y,z\ \ r))}" apply (simp add: comp_def) apply (rule equalityI) apply (clarify ); @@ -828,10 +851,24 @@ apply (blast dest: transM)+ done -lemma (in M_axioms) comp_closed [intro]: +lemma (in M_axioms) comp_closed [intro,simp]: "[| M(r); M(s) |] ==> M(r O s)" apply (simp add: M_comp_iff) -apply (insert comp_separation [of r s], simp, blast) +apply (insert comp_separation [of r s], simp) +done + +lemma (in M_axioms) composition_abs [simp]: + "[| M(r); M(s); M(t) |] + ==> composition(M,r,s,t) <-> t = r O s" +apply safe; + txt{*Proving @{term "composition(M, r, s, r O s)"}*} + prefer 2 + apply (simp add: composition_def comp_def) + apply (blast dest: transM) +txt{*Opposite implication*} +apply (rule M_equalityI) + apply (simp add: composition_def comp_def) + apply (blast del: allE dest: transM)+ done lemma (in M_axioms) nat_into_M [intro]: @@ -852,16 +889,34 @@ apply (blast intro!: equalityI dest: transM) done -lemma (in M_axioms) Inter_closed [intro]: +lemma (in M_axioms) Inter_closed [intro,simp]: "M(A) ==> M(Inter(A))" -by (insert Inter_separation, simp add: Inter_def, blast) +by (insert Inter_separation, simp add: Inter_def) -lemma (in M_axioms) Int_closed [intro]: +lemma (in M_axioms) Int_closed [intro,simp]: "[| M(A); M(B) |] ==> M(A Int B)" apply (subgoal_tac "M({A,B})") apply (frule Inter_closed, force+); done +text{*M contains all finite functions*} +lemma (in M_axioms) finite_fun_closed_lemma [rule_format]: + "[| n \ nat; M(A) |] ==> \f \ n -> A. M(f)" +apply (induct_tac n, simp) +apply (rule ballI) +apply (simp add: succ_def) +apply (frule fun_cons_restrict_eq) +apply (erule ssubst) +apply (subgoal_tac "M(f`x) & restrict(f,x) \ x -> A") + apply (simp add: cons_closed nat_into_M apply_closed) +apply (blast intro: apply_funtype transM restrict_type2) +done + +lemma (in M_axioms) finite_fun_closed [rule_format]: + "[| f \ n -> A; n \ nat; M(A) |] ==> M(f)" +by (blast intro: finite_fun_closed_lemma) + + subsection{*Absoluteness for ordinals*} text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} diff -r 7b37e218f298 -r 714f7a423a15 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Mon Jun 24 11:59:14 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Mon Jun 24 11:59:21 2002 +0200 @@ -1,7 +1,7 @@ theory WFrec = Wellorderings: -(*WF.thy??*) +(*FIXME: could move these to WF.thy*) lemma is_recfunI: "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)" @@ -27,6 +27,16 @@ apply (fast intro: lam_type, simp) done +lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \x,i\ \ f|] ==> \x, a\ \ r" +by (blast dest: is_recfun_type fun_is_rel) + +lemma apply_recfun2: + "[| is_recfun(r,a,H,f); :f |] ==> i = H(x, restrict(f,r-``{x}))" +apply (frule apply_recfun) + apply (blast dest: is_recfun_type fun_is_rel) +apply (simp add: function_apply_equality [OF _ is_recfun_imp_function]) +done + lemma trans_on_Int_eq [simp]: "[| trans[A](r); \ r; r \ A*A |] ==> r -`` {y} \ r -`` {x} = r -`` {y}" @@ -38,11 +48,6 @@ by (blast intro: trans_onD) -constdefs - M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i" - "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))" - - text{*Stated using @{term "trans[A](r)"} rather than @{term "transitive_rel(M,A,r)"} because the latter rewrites to the former anyway, by @{text transitive_rel_abs}. @@ -178,6 +183,16 @@ apply_recfun is_recfun_type [THEN apply_iff]) done +(*FIXME: use this lemma just below*) +text{*For typical applications of Replacement for recursive definitions*} +lemma (in M_axioms) univalent_is_recfun: + "[|wellfounded_on(M,A,r); trans[A](r); r \ A*A; M(r); M(A)|] + ==> univalent (M, A, \x p. \y. M(y) & + (\f. M(f) & p = \x, y\ & is_recfun(r,x,H,f) & y = H(x,f)))" +apply (simp add: univalent_def) +apply (blast dest: is_recfun_functional) +done + text{*Proof of the inductive step for @{text exists_is_recfun}, since we must prove two versions.*} lemma (in M_axioms) exists_is_recfun_indstep: @@ -240,23 +255,28 @@ pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); M(A); M(r); r \ A*A; \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] - ==> \f. M(f) & is_recfun(r,a,H,f)" + ==> \f. M(f) & is_recfun(r,a,H,f)" apply (rule wf_on_induct2, assumption+) apply (frule wf_on_imp_relativized) apply (rule exists_is_recfun_indstep, assumption+) done -(*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *) -lemma (in M_axioms) M_is_the_recfun: - "[|is_recfun(r,a,H,f); - wellfounded_on(M,A,r); trans[A](r); - M(A); M(f); M(a); r \ A*A |] - ==> M(M_the_recfun(M,r,a,H)) & - is_recfun(r, a, H, M_the_recfun(M,r,a,H))" -apply (unfold M_the_recfun_def) -apply (rule ex1I [THEN theI2], fast) -apply (blast intro: is_recfun_functional, blast) -done + (*????????????????NOT USED????????????????*) + constdefs + M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i" + "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))" + + (*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *) + lemma (in M_axioms) M_is_the_recfun: + "[|is_recfun(r,a,H,f); + wellfounded_on(M,A,r); trans[A](r); + M(A); M(f); M(a); r \ A*A |] + ==> M(M_the_recfun(M,r,a,H)) & + is_recfun(r, a, H, M_the_recfun(M,r,a,H))" + apply (unfold M_the_recfun_def) + apply (rule ex1I [THEN theI2], fast) + apply (blast intro: is_recfun_functional, blast) + done constdefs M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o" @@ -432,7 +452,7 @@ apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd) done -lemma (in M_recursion) oadd_closed [intro]: +lemma (in M_recursion) oadd_closed [intro,simp]: "[| M(i); M(j) |] ==> M(i++j)" apply (simp add: oadd_eq_if_raw_oadd, clarify) apply (simp add: raw_oadd_eq_oadd) @@ -485,7 +505,6 @@ apply (simp add: omult_eqns_0) apply (simp add: omult_eqns_succ apply_closed oadd_closed) apply (simp add: omult_eqns_Limit) -apply (simp add: Union_closed image_closed) done lemma (in M_recursion) exists_omult: diff -r 7b37e218f298 -r 714f7a423a15 src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Mon Jun 24 11:59:14 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Mon Jun 24 11:59:21 2002 +0200 @@ -144,10 +144,10 @@ apply (blast dest: transM) done -lemma (in M_axioms) pred_closed [intro]: +lemma (in M_axioms) pred_closed [intro,simp]: "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))" apply (simp add: Order.pred_def) -apply (insert pred_separation [of r x], simp, blast) +apply (insert pred_separation [of r x], simp) done lemma (in M_axioms) membership_abs [simp]: @@ -170,10 +170,10 @@ apply (blast dest: transM) done -lemma (in M_axioms) Memrel_closed [intro]: +lemma (in M_axioms) Memrel_closed [intro,simp]: "M(A) ==> M(Memrel(A))" apply (simp add: M_Memrel_iff) -apply (insert Memrel_separation, simp, blast) +apply (insert Memrel_separation, simp) done