# HG changeset patch # User paulson # Date 1025540178 -7200 # Node ID 240509babf00d8b2aa32179a8d3256d770f8f104 # Parent 502f69ea6627776f661d4e8c2fb332a22baaf3b1 more use of relativized quantifiers list_closed diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/Datatype_absolute.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Constructible/Datatype_absolute.thy Mon Jul 01 18:16:18 2002 +0200 @@ -0,0 +1,173 @@ +theory Datatype_absolute = WF_absolute: + +(*Epsilon.thy*) +lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})" +apply (insert arg_subset_eclose [of "{i}"], simp) +apply (frule eclose_subset, blast) +done + +lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)" +apply (rule equalityI) +apply (erule eclose_sing_Ord) +apply (rule succ_subset_eclose_sing) +done + +(*Ordinal.thy*) +lemma relation_Memrel: "relation(Memrel(A))" +by (simp add: relation_def Memrel_def, blast) + +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)") +apply force +apply (simp add: nat_case_def) +done + + +subsection{*The lfp of a continuous function can be expressed as a union*} + +constdefs + contin :: "[i=>i]=>o" + "contin(h) == (\A. A\0 --> h(\A) = (\X\A. h(X)))" + +lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \ nat|] ==> h^n (0) <= D" +apply (induct_tac n) + apply (simp_all add: bnd_mono_def, blast) +done + + +lemma contin_iterates_eq: + "contin(h) \ h(\n\nat. h^n (0)) = (\n\nat. h^n (0))" +apply (simp add: contin_def) +apply (rule trans) +apply (rule equalityI) + apply (simp_all add: UN_subset_iff) + apply safe + apply (erule_tac [2] natE) + apply (rule_tac a="succ(x)" in UN_I) + apply simp_all +apply blast +done + +lemma lfp_subset_Union: + "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) <= (\n\nat. h^n(0))" +apply (rule lfp_lowerbound) + apply (simp add: contin_iterates_eq) +apply (simp add: contin_def bnd_mono_iterates_subset UN_subset_iff) +done + +lemma Union_subset_lfp: + "bnd_mono(D,h) ==> (\n\nat. h^n(0)) <= lfp(D,h)" +apply (simp add: UN_subset_iff) +apply (rule ballI) +apply (induct_tac x, simp_all) +apply (rule subset_trans [of _ "h(lfp(D,h))"]) + apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] ) +apply (erule lfp_lemma2) +done + +lemma lfp_eq_Union: + "[|bnd_mono(D, h); contin(h)|] ==> lfp(D,h) = (\n\nat. h^n(0))" +by (blast del: subsetI + intro: lfp_subset_Union Union_subset_lfp) + + +subsection {*lists without univ*} + +lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ + Pair_in_univ zero_in_univ + +lemma list_fun_bnd_mono: "bnd_mono(univ(A), \X. {0} + A*X)" +apply (rule bnd_monoI) + apply (intro subset_refl zero_subset_univ A_subset_univ + sum_subset_univ Sigma_subset_univ) + apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI) +done + +lemma list_fun_contin: "contin(\X. {0} + A*X)" +by (simp add: contin_def, blast) + +text{*Re-expresses lists using sum and product*} +lemma list_eq_lfp2: "list(A) = lfp(univ(A), \X. {0} + A*X)" +apply (simp add: list_def) +apply (rule equalityI) + apply (rule lfp_lowerbound) + prefer 2 apply (rule lfp_subset) + apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono]) + apply (simp add: Nil_def Cons_def) + apply blast +txt{*Opposite inclusion*} +apply (rule lfp_lowerbound) + prefer 2 apply (rule lfp_subset) +apply (clarify, subst lfp_unfold [OF list.bnd_mono]) +apply (simp add: Nil_def Cons_def) +apply (blast intro: datatype_univs + dest: lfp_subset [THEN subsetD]) +done + +text{*Re-expresses lists using "iterates", no univ.*} +lemma list_eq_Union: + "list(A) = (\n\nat. (\X. {0} + A*X) ^ n (0))" +by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin) + + +subsection {*Absoluteness for "Iterates"*} + +lemma (in M_trancl) iterates_relativize: + "[|n \ nat; M(v); \x[M]. M(F(x)); + strong_replacement(M, + \x z. \y[M]. \g[M]. pair(M, x, y, z) & + is_recfun (Memrel(succ(n)), x, + \n f. nat_case(v, \m. F(f`m), n), g) & + y = nat_case(v, \m. F(g`m), x))|] + ==> iterates(F,n,v) = z <-> + (\g[M]. is_recfun(Memrel(succ(n)), n, + \n g. nat_case(v, \m. F(g`m), n), g) & + z = nat_case(v, \m. F(g`m), n))" +by (simp add: iterates_nat_def recursor_def transrec_def + eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M + wf_Memrel trans_Memrel relation_Memrel nat_case_closed) + + +lemma (in M_wfrank) iterates_closed [intro,simp]: + "[|n \ nat; M(v); \x[M]. M(F(x)); + strong_replacement(M, + \x z. \y[M]. \g[M]. pair(M, x, y, z) & + is_recfun (Memrel(succ(n)), x, + \n f. nat_case(v, \m. F(f`m), n), g) & + y = nat_case(v, \m. F(g`m), x))|] + ==> M(iterates(F,n,v))" +by (simp add: iterates_nat_def recursor_def transrec_def + eclose_sing_Ord_eq trans_wfrec_closed nat_into_M + wf_Memrel trans_Memrel relation_Memrel nat_case_closed) + + +locale M_datatypes = M_wfrank + +(*THEY NEED RELATIVIZATION*) + assumes list_replacement1: + "[|M(A); n \ nat|] ==> + strong_replacement(M, + \x z. \y[M]. \g[M]. pair(M, x, y, z) & + is_recfun (Memrel(succ(n)), x, + \n f. nat_case(0, \m. {0} + A \ f`m, n), g) & + y = nat_case(0, \m. {0} + A \ g`m, x))" + and list_replacement2': + "M(A) ==> strong_replacement(M, \x y. y = (\X. {0} + A \ X)^x (0))" + + +lemma (in M_datatypes) list_replacement1': + "[|M(A); n \ nat|] + ==> strong_replacement + (M, \x y. \z[M]. \g[M]. y = \x, z\ & + is_recfun (Memrel(succ(n)), x, + \n f. nat_case(0, \m. {0} + A \ f ` m, n), g) & + z = nat_case(0, \m. {0} + A \ g ` m, x))" +by (insert list_replacement1, simp) + + +lemma (in M_datatypes) list_closed [intro,simp]: + "M(A) ==> M(list(A))" +by (simp add: list_eq_Union list_replacement1' list_replacement2') + +end diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Mon Jul 01 18:16:18 2002 +0200 @@ -62,8 +62,7 @@ lemma replacement: "replacement(L,P)" apply (simp add: replacement_def, clarify) -apply (frule LReplace_in_L, assumption+) -apply clarify +apply (frule LReplace_in_L, assumption+, clarify) apply (rule_tac x=Y in exI) apply (simp add: Replace_iff univalent_def, blast) done diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/Normal.thy --- a/src/ZF/Constructible/Normal.thy Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/Normal.thy Mon Jul 01 18:16:18 2002 +0200 @@ -316,8 +316,7 @@ --"this lemma is @{thm increasing_LimitI [no_vars]}" apply (blast intro: UN_upper_lt [of "1"] Normal_imp_Ord Ord_UN Ord_iterates lt_imp_0_lt - iterates_Normal_increasing) -apply clarify + iterates_Normal_increasing, clarify) apply (rule bexI) apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) apply (rule UN_I, erule nat_succI) diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/ROOT.ML Mon Jul 01 18:16:18 2002 +0200 @@ -9,3 +9,4 @@ use_thy "Reflection"; use_thy "WF_absolute"; use_thy "L_axioms"; +use_thy "Datatype_absolute"; diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/Reflection.thy --- a/src/ZF/Constructible/Reflection.thy Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/Reflection.thy Mon Jul 01 18:16:18 2002 +0200 @@ -55,7 +55,7 @@ theorem (in reflection) Not_reflection [intro]: "Reflects(Cl,P,Q) ==> Reflects(Cl, \x. ~P(x), \a x. ~Q(a,x))" -by (simp add: Reflects_def); +by (simp add: Reflects_def) theorem (in reflection) And_reflection [intro]: "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Mon Jul 01 18:16:18 2002 +0200 @@ -2,6 +2,11 @@ theory Relative = Main: +(*func.thy*) +lemma succ_fun_eq: "succ(n) -> B = (\f \ n->B. \b\B. {cons(, f)})" +by (simp add: succ_def mem_not_refl cons_fun_eq) + + subsection{* Relativized versions of standard set-theoretic concepts *} constdefs @@ -96,6 +101,10 @@ 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))" + is_funspace :: "[i=>o,i,i,i] => o" + "is_funspace(M,A,B,F) == + \f[M]. f \ F <-> typed_function(M,A,B,f)" + composition :: "[i=>o,i,i,i] => o" "composition(M,r,s,t) == \p. M(p) --> (p \ t <-> @@ -385,29 +394,28 @@ 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 M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*) and Inter_separation: - "M(A) ==> separation(M, \x. \y\A. M(y) --> x\y)" + "M(A) ==> separation(M, \x. \y[M]. y\A --> x\y)" and cartprod_separation: "[| M(A); M(B) |] ==> separation(M, \z. \x\A. \y\B. M(x) & M(y) & pair(M,x,y,z))" and image_separation: "[| M(A); M(r) |] - ==> separation(M, \y. \p\r. M(p) & (\x\A. M(x) & pair(M,x,y,p)))" + ==> 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\r. M(p) & (\y\A. M(x) & pair(M,x,y,p)))" + ==> 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)))" and restrict_separation: - "M(A) - ==> separation(M, \z. \x\A. M(x) & (\y. M(y) & pair(M,x,y,z)))" + "M(A) ==> separation(M, \z. \x[M]. x\A & (\y[M]. pair(M,x,y,z)))" and comp_separation: "[| M(r); M(s) |] - ==> separation(M, \xz. \x y z. M(x) & M(y) & M(z) & - (\xy\s. \yz\r. M(xy) & M(yz) & - pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))" + ==> separation(M, \xz. \x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. + pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & + xy\s & yz\r)" and pred_separation: "[| M(r); M(x) |] ==> separation(M, \y. \p\r. M(p) & pair(M,y,x,p))" and Memrel_separation: @@ -418,6 +426,10 @@ ==> separation(M, \a. \x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" + and funspace_succ_replacement: + "M(n) ==> + strong_replacement(M, \p z. \f[M]. \b[M]. \nb[M]. + pair(M,f,b,p) & pair(M,n,b,nb) & z = {cons(nb,f)})" and well_ord_iso_separation: "[| M(A); M(f); M(r) |] ==> separation (M, \x. x\A --> (\y. M(y) & (\p. M(p) & @@ -440,15 +452,23 @@ 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]: +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) Bex_abs [simp]: +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) Ball_iff_equiv: +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) @@ -570,11 +590,9 @@ "[| \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) -apply clarify +apply (frule replacementD [OF replacement], assumption, clarify) apply (drule_tac x=A in spec, clarify) -apply (drule_tac z=Y in separationD, assumption) -apply clarify +apply (drule_tac z=Y in separationD, assumption, clarify) apply (blast dest: transM) done @@ -692,6 +710,10 @@ "[| M(A); M(B) |] ==> M(A*B)" by (frule cartprod_closed_lemma, assumption, force) +lemma (in M_axioms) sum_closed [intro,simp]: + "[| M(A); M(B) |] ==> M(A+B)" +by (simp add: sum_def) + lemma (in M_axioms) image_closed [intro,simp]: "[| M(A); M(r) |] ==> M(r``A)" apply (simp add: image_iff_Collect) @@ -758,9 +780,9 @@ "[| 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 intro: elim:); + prefer 2 apply blast apply (rule M_equalityI) - apply (simp add: ) + apply simp apply (blast dest: transM)+ done @@ -819,20 +841,20 @@ "[| 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 (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 (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(y) & z = \x, y\}" + "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]: @@ -845,8 +867,7 @@ "[| 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]. \y[M]. \z[M]. xz = \x,z\ & \x,y\ \ s & \y,z\ \ r}" apply (simp add: comp_def) apply (rule equalityI) apply clarify @@ -902,6 +923,8 @@ apply (frule Inter_closed, force+) done +subsection{*Functions and function space*} + 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)" @@ -919,6 +942,39 @@ "[| f \ n -> A; n \ nat; M(A) |] ==> M(f)" by (blast intro: finite_fun_closed_lemma) +text{*The assumption @{term "M(A->B)"} is unusual, but essential: in +all but trivial cases, A->B cannot be expected to belong to @{term M}.*} +lemma (in M_axioms) is_funspace_abs [simp]: + "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B"; +apply (simp add: is_funspace_def) +apply (rule iffI) + prefer 2 apply blast +apply (rule M_equalityI) + apply simp_all +done + +lemma (in M_axioms) succ_fun_eq2: + "[|M(B); M(n->B)|] ==> + succ(n) -> B = + \{z. p \ (n->B)*B, \f[M]. \b[M]. p = & z = {cons(, f)}}" +apply (simp add: succ_fun_eq) +apply (blast dest: transM) +done + +lemma (in M_axioms) funspace_succ: + "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)" +apply (insert funspace_succ_replacement [of n]) +apply (force simp add: succ_fun_eq2 univalent_def) +done + +text{*@{term M} contains all finite function spaces. Needed to prove the +absoluteness of transitive closure.*} +lemma (in M_axioms) finite_funspace_closed [intro,simp]: + "[|n\nat; M(B)|] ==> M(n->B)" +apply (induct_tac n, simp) +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).*} diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Mon Jul 01 18:16:18 2002 +0200 @@ -1,5 +1,20 @@ theory WF_absolute = WFrec: +(*????move to Wellorderings.thy*) +lemma (in M_axioms) wellfounded_on_field_imp_wellfounded: + "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)" +by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast) + +lemma (in M_axioms) wellfounded_iff_wellfounded_on_field: + "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)" +by (blast intro: wellfounded_imp_wellfounded_on + wellfounded_on_field_imp_wellfounded) + +lemma (in M_axioms) wellfounded_on_subset_A: + "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)" +by (simp add: wellfounded_on_def, blast) + + subsection{*Every well-founded relation is a subset of some inverse image of an ordinal*} @@ -127,7 +142,7 @@ tran_closure :: "[i=>o,i,i] => o" "tran_closure(M,r,t) == - \s. M(s) & rtran_closure(M,r,s) & composition(M,r,s,t)" + \s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" locale M_trancl = M_axioms + @@ -135,11 +150,14 @@ assumes rtrancl_separation: "[| M(r); M(A) |] ==> separation - (M, \p. \n\nat. \f \ succ(n) -> A. - (\x y. p = & f`0 = x & f`n = y) & - (\i\n. \ r))" + (M, \p. \n[M]. n\nat & + (\f[M]. + f \ succ(n) -> A & + (\x[M]. \y[M]. pair(M,x,y,p) & + f`0 = x & f`n = y) & + (\i\n. \ r)))" and wellfounded_trancl_separation: - "[| M(r); M(Z) |] ==> separation (M, \x. \w. M(w) & \w,x\ \ r^+ & w \ Z)" + "[| M(r); M(Z) |] ==> separation (M, \x. \w[M]. w \ Z & \w,x\ \ r^+)" lemma (in M_trancl) rtran_closure_rtrancl: @@ -165,7 +183,7 @@ apply (insert rtrancl_separation [of r "field(r)"]) apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def field_closed typed_apply_abs apply_closed - Ord_succ_mem_iff M_nat + Ord_succ_mem_iff M_nat nat_into_M nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) done @@ -215,11 +233,10 @@ apply (simp add: wellfounded_on_def) apply (safe intro!: equalityI) apply (rename_tac Z x) -apply (subgoal_tac "M({x\A. \w. M(w) & \w,x\ \ r^+ & w \ Z})") +apply (subgoal_tac "M({x\A. \w[M]. w \ Z & \w,x\ \ r^+})") prefer 2 - apply (simp add: wellfounded_trancl_separation) -apply (drule_tac x = "{x\A. \w. M(w) & \w,x\ \ r^+ & w \ Z}" in spec) -apply safe + apply (blast intro: wellfounded_trancl_separation) +apply (drule_tac x = "{x\A. \w[M]. w \ Z & \w,x\ \ r^+}" in spec, safe) apply (blast dest: transM, simp) apply (rename_tac y w) apply (drule_tac x=w in bspec, assumption, clarify) @@ -228,22 +245,6 @@ apply blast done -(*????move to Wellorderings.thy*) -lemma (in M_axioms) wellfounded_on_field_imp_wellfounded: - "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)" -by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast) - -lemma (in M_axioms) wellfounded_iff_wellfounded_on_field: - "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)" -by (blast intro: wellfounded_imp_wellfounded_on - wellfounded_on_field_imp_wellfounded) - -lemma (in M_axioms) wellfounded_on_subset_A: - "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)" -by (simp add: wellfounded_on_def, blast) - - - lemma (in M_trancl) wellfounded_trancl: "[|wellfounded(M,r); M(r)|] ==> wellfounded(M,r^+)" apply (rotate_tac -1) @@ -259,14 +260,14 @@ (*NEEDS RELATIVIZATION*) -locale M_recursion = M_trancl + +locale M_wfrank = M_trancl + assumes wfrank_separation': "M(r) ==> separation - (M, \x. ~ (\f. M(f) & is_recfun(r^+, x, %x f. range(f), f)))" + (M, \x. ~ (\f[M]. is_recfun(r^+, x, %x f. range(f), f)))" and wfrank_strong_replacement': "M(r) ==> - strong_replacement(M, \x z. \y f. M(y) & M(f) & + strong_replacement(M, \x z. \y[M]. \f[M]. pair(M,x,y,z) & is_recfun(r^+, x, %x f. range(f), f) & y = range(f))" and Ord_wfrank_separation: @@ -279,13 +280,13 @@ constdefs wellfoundedrank :: "[i=>o,i,i] => i" "wellfoundedrank(M,r,A) == - {p. x\A, \y f. M(y) & M(f) & + {p. x\A, \y[M]. \f[M]. p = & is_recfun(r^+, x, %x f. range(f), f) & y = range(f)}" -lemma (in M_recursion) exists_wfrank: +lemma (in M_wfrank) exists_wfrank: "[| wellfounded(M,r); M(a); M(r) |] - ==> \f. M(f) & is_recfun(r^+, a, %x f. range(f), f)" + ==> \f[M]. is_recfun(r^+, a, %x f. range(f), f)" apply (rule wellfounded_exists_is_recfun) apply (blast intro: wellfounded_trancl) apply (rule trans_trancl) @@ -294,7 +295,7 @@ apply (simp_all add: trancl_subset_times) done -lemma (in M_recursion) M_wellfoundedrank: +lemma (in M_wfrank) M_wellfoundedrank: "[| wellfounded(M,r); M(r); M(A) |] ==> M(wellfoundedrank(M,r,A))" apply (insert wfrank_strong_replacement' [of r]) apply (simp add: wellfoundedrank_def) @@ -306,7 +307,7 @@ apply (simp add: trancl_subset_times, blast) done -lemma (in M_recursion) Ord_wfrank_range [rule_format]: +lemma (in M_wfrank) Ord_wfrank_range [rule_format]: "[| wellfounded(M,r); a\A; M(r); M(A) |] ==> \f. M(f) --> is_recfun(r^+, a, %x f. range(f), f) --> Ord(range(f))" apply (drule wellfounded_trancl, assumption) @@ -337,7 +338,7 @@ apply (blast dest: pair_components_in_M) done -lemma (in M_recursion) Ord_range_wellfoundedrank: +lemma (in M_wfrank) Ord_range_wellfoundedrank: "[| wellfounded(M,r); r \ A*A; M(r); M(A) |] ==> Ord (range(wellfoundedrank(M,r,A)))" apply (frule wellfounded_trancl, assumption) @@ -349,23 +350,23 @@ apply (blast intro: Ord_wfrank_range) txt{*We still must show that the range is a transitive set.*} apply (simp add: Transset_def, clarify, simp) -apply (rename_tac x i f u) +apply (rename_tac x f i u) apply (frule is_recfun_imp_in_r, assumption) apply (subgoal_tac "M(u) & M(i) & M(x)") prefer 2 apply (blast dest: transM, clarify) apply (rule_tac a=u in rangeI) apply (rule ReplaceI) - apply (rule_tac x=i in exI, simp) - apply (rule_tac x="restrict(f, r^+ -`` {u})" in exI) - apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) - apply blast + apply (rule_tac x=i in rexI, simp) + apply (rule_tac x="restrict(f, r^+ -`` {u})" in rexI) + apply (blast intro: is_recfun_restrict trans_trancl dest: apply_recfun2) + apply (simp, simp, blast) txt{*Unicity requirement of Replacement*} apply clarify apply (frule apply_recfun2, assumption) apply (simp add: trans_trancl is_recfun_cut)+ done -lemma (in M_recursion) function_wellfoundedrank: +lemma (in M_wfrank) function_wellfoundedrank: "[| wellfounded(M,r); M(r); M(A)|] ==> function(wellfoundedrank(M,r,A))" apply (simp add: wellfoundedrank_def function_def, clarify) @@ -375,7 +376,7 @@ apply (simp_all add: trancl_subset_times trans_trancl) done -lemma (in M_recursion) domain_wellfoundedrank: +lemma (in M_wfrank) domain_wellfoundedrank: "[| wellfounded(M,r); M(r); M(A)|] ==> domain(wellfoundedrank(M,r,A)) = A" apply (simp add: wellfoundedrank_def function_def) @@ -384,9 +385,9 @@ apply (frule_tac a=x in exists_wfrank, assumption+, clarify) apply (rule domainI) apply (rule ReplaceI) - apply (rule_tac x="range(f)" in exI) + apply (rule_tac x="range(f)" in rexI) apply simp - apply (rule_tac x=f in exI, blast, assumption) + apply (rule_tac x=f in rexI, blast, simp_all) txt{*Uniqueness (for Replacement): repeated above!*} apply clarify apply (drule is_recfun_functional, assumption) @@ -394,7 +395,7 @@ apply (simp_all add: trancl_subset_times trans_trancl) done -lemma (in M_recursion) wellfoundedrank_type: +lemma (in M_wfrank) wellfoundedrank_type: "[| wellfounded(M,r); M(r); M(A)|] ==> wellfoundedrank(M,r,A) \ A -> range(wellfoundedrank(M,r,A))" apply (frule function_wellfoundedrank [of r A], assumption+) @@ -404,13 +405,13 @@ apply (simp add: domain_wellfoundedrank) done -lemma (in M_recursion) Ord_wellfoundedrank: +lemma (in M_wfrank) Ord_wellfoundedrank: "[| wellfounded(M,r); a \ A; r \ A*A; M(r); M(A) |] ==> Ord(wellfoundedrank(M,r,A) ` a)" by (blast intro: apply_funtype [OF wellfoundedrank_type] Ord_in_Ord [OF Ord_range_wellfoundedrank]) -lemma (in M_recursion) wellfoundedrank_eq: +lemma (in M_wfrank) wellfoundedrank_eq: "[| is_recfun(r^+, a, %x. range, f); wellfounded(M,r); a \ A; M(f); M(r); M(A)|] ==> wellfoundedrank(M,r,A) ` a = range(f)" @@ -418,9 +419,9 @@ prefer 2 apply (blast intro: wellfoundedrank_type) apply (simp add: wellfoundedrank_def) apply (rule ReplaceI) - apply (rule_tac x="range(f)" in exI) + apply (rule_tac x="range(f)" in rexI) apply blast - apply assumption + apply simp_all txt{*Unicity requirement of Replacement*} apply clarify apply (drule is_recfun_functional, assumption) @@ -429,7 +430,7 @@ done -lemma (in M_recursion) wellfoundedrank_lt: +lemma (in M_wfrank) wellfoundedrank_lt: "[| \ r; wellfounded(M,r); r \ A*A; M(r); M(A)|] ==> wellfoundedrank(M,r,A) ` a < wellfoundedrank(M,r,A) ` b" @@ -454,7 +455,7 @@ done -lemma (in M_recursion) wellfounded_imp_subset_rvimage: +lemma (in M_wfrank) wellfounded_imp_subset_rvimage: "[|wellfounded(M,r); r \ A*A; M(r); M(A)|] ==> \i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" apply (rule_tac x="range(wellfoundedrank(M,r,A))" in exI) @@ -465,12 +466,12 @@ apply (blast intro: apply_rangeI wellfoundedrank_type) done -lemma (in M_recursion) wellfounded_imp_wf: +lemma (in M_wfrank) wellfounded_imp_wf: "[|wellfounded(M,r); relation(r); M(r)|] ==> wf(r)" by (blast dest!: relation_field_times_field wellfounded_imp_subset_rvimage intro: wf_rvimage_Ord [THEN wf_subset]) -lemma (in M_recursion) wellfounded_on_imp_wf_on: +lemma (in M_wfrank) wellfounded_on_imp_wf_on: "[|wellfounded_on(M,A,r); relation(r); M(r); M(A)|] ==> wf[A](r)" apply (simp add: wellfounded_on_iff_wellfounded wf_on_def) apply (rule wellfounded_imp_wf) @@ -478,11 +479,11 @@ done -theorem (in M_recursion) wf_abs [simp]: +theorem (in M_wfrank) wf_abs [simp]: "[|relation(r); M(r)|] ==> wellfounded(M,r) <-> wf(r)" by (blast intro: wellfounded_imp_wf wf_imp_relativized) -theorem (in M_recursion) wf_on_abs [simp]: +theorem (in M_wfrank) wf_on_abs [simp]: "[|relation(r); M(r); M(A)|] ==> wellfounded_on(M,A,r) <-> wf[A](r)" by (blast intro: wellfounded_on_imp_wf_on wf_on_imp_relativized) @@ -493,20 +494,20 @@ lemma (in M_trancl) wfrec_relativize: "[|wf(r); M(a); M(r); - strong_replacement(M, \x z. \y g. M(y) & M(g) & + strong_replacement(M, \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r^+, x, \x f. H(x, restrict(f, r -`` {x})), g) & y = H(x, restrict(g, r -`` {x}))); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> wfrec(r,a,H) = z <-> - (\f. M(f) & is_recfun(r^+, a, \x f. H(x, restrict(f, r -`` {x})), f) & + (\f[M]. is_recfun(r^+, a, \x f. H(x, restrict(f, r -`` {x})), f) & z = H(a,restrict(f,r-``{a})))" apply (frule wf_trancl) apply (simp add: wftrec_def wfrec_def, safe) apply (frule wf_exists_is_recfun [of concl: "r^+" a "\x f. H(x, restrict(f, r -`` {x}))"]) apply (simp_all add: trans_trancl function_restrictI trancl_subset_times) - apply (clarify, rule_tac x=f in exI) + apply (clarify, rule_tac x=x in rexI) apply (simp_all add: the_recfun_eq trans_trancl trancl_subset_times) done @@ -516,10 +517,10 @@ before we can replace @{term "r^+"} by @{term r}. *} theorem (in M_trancl) trans_wfrec_relativize: "[|wf(r); trans(r); relation(r); M(r); M(a); - strong_replacement(M, \x z. \y g. M(y) & M(g) & + strong_replacement(M, \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); \x[M]. \g[M]. function(g) --> M(H(x,g))|] - ==> wfrec(r,a,H) = z <-> (\f. M(f) & is_recfun(r,a,H,f) & z = H(a,f))" + ==> wfrec(r,a,H) = z <-> (\f[M]. is_recfun(r,a,H,f) & z = H(a,f))" by (simp cong: is_recfun_cong add: wfrec_relativize trancl_eq_r is_recfun_restrict_idem domain_restrict_idem) @@ -527,11 +528,11 @@ lemma (in M_trancl) trans_eq_pair_wfrec_iff: "[|wf(r); trans(r); relation(r); M(r); M(y); - strong_replacement(M, \x z. \y g. M(y) & M(g) & + strong_replacement(M, \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> y = <-> - (\f. M(f) & is_recfun(r,x,H,f) & y = )" + (\f[M]. is_recfun(r,x,H,f) & y = )" apply safe apply (simp add: trans_wfrec_relativize [THEN iff_sym]) txt{*converse direction*} @@ -543,7 +544,7 @@ subsection{*M is closed under well-founded recursion*} text{*Lemma with the awkward premise mentioning @{text wfrec}.*} -lemma (in M_recursion) wfrec_closed_lemma [rule_format]: +lemma (in M_wfrank) wfrec_closed_lemma [rule_format]: "[|wf(r); M(r); strong_replacement(M, \x y. y = \x, wfrec(r, x, H)\); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] @@ -557,20 +558,20 @@ done text{*Eliminates one instance of replacement.*} -lemma (in M_recursion) wfrec_replacement_iff: - "strong_replacement(M, \x z. \y g. M(y) & M(g) & +lemma (in M_wfrank) wfrec_replacement_iff: + "strong_replacement(M, \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)) <-> strong_replacement(M, - \x y. \f. M(f) & is_recfun(r,x,H,f) & y = )" + \x y. \f[M]. is_recfun(r,x,H,f) & y = )" apply simp apply (rule strong_replacement_cong, blast) done text{*Useful version for transitive relations*} -theorem (in M_recursion) trans_wfrec_closed: +theorem (in M_wfrank) trans_wfrec_closed: "[|wf(r); trans(r); relation(r); M(r); M(a); strong_replacement(M, - \x z. \y g. M(y) & M(g) & + \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] ==> M(wfrec(r,a,H))" @@ -582,13 +583,13 @@ section{*Absoluteness without assuming transitivity*} lemma (in M_trancl) eq_pair_wfrec_iff: "[|wf(r); M(r); M(y); - strong_replacement(M, \x z. \y g. M(y) & M(g) & + strong_replacement(M, \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r^+, x, \x f. H(x, restrict(f, r -`` {x})), g) & y = H(x, restrict(g, r -`` {x}))); \x[M]. \g[M]. function(g) --> M(H(x,g))|] ==> y = <-> - (\f. M(f) & is_recfun(r^+, x, \x f. H(x, restrict(f, r -`` {x})), f) & + (\f[M]. is_recfun(r^+, x, \x f. H(x, restrict(f, r -`` {x})), f) & y = )" apply safe apply (simp add: wfrec_relativize [THEN iff_sym]) @@ -597,7 +598,7 @@ apply (simp add: wfrec_relativize, blast) done -lemma (in M_recursion) wfrec_closed_lemma [rule_format]: +lemma (in M_wfrank) wfrec_closed_lemma [rule_format]: "[|wf(r); M(r); strong_replacement(M, \x y. y = \x, wfrec(r, x, H)\); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] @@ -611,9 +612,9 @@ done text{*Full version not assuming transitivity, but maybe not very useful.*} -theorem (in M_recursion) wfrec_closed: +theorem (in M_wfrank) wfrec_closed: "[|wf(r); M(r); M(a); - strong_replacement(M, \x z. \y g. M(y) & M(g) & + strong_replacement(M, \x z. \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r^+, x, \x f. H(x, restrict(f, r -`` {x})), g) & y = H(x, restrict(g, r -`` {x}))); diff -r 502f69ea6627 -r 240509babf00 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Mon Jul 01 18:10:53 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Mon Jul 01 18:16:18 2002 +0200 @@ -117,9 +117,7 @@ lemma (in M_axioms) is_recfun_functional: "[|is_recfun(r,a,H,f); is_recfun(r,a,H,g); - wellfounded(M,r); trans(r); - M(f); M(g); M(r) |] - ==> f=g" + wellfounded(M,r); trans(r); M(f); M(g); M(r) |] ==> f=g" apply (rule fun_extension) apply (erule is_recfun_type)+ apply (blast intro!: is_recfun_equal dest: transM) @@ -183,9 +181,8 @@ \x[M]. \g[M]. function(g) --> M(H(x,g)); M(Y); \b. M(b) --> b \ Y <-> - (\x\r -`` {a1}. - \y. M(y) \ - (\g. M(g) \ b = \x,y\ \ is_recfun(r,x,H,g) \ y = H(x,g))); + (\x\r -`` {a1}. \y[M]. \g[M]. + b = \x,y\ & is_recfun(r,x,H,g) \ y = H(x,g)); \x,a1\ \ r; M(f); is_recfun(r,x,H,f) |] ==> restrict(Y, r -`` {x}) = f" apply (subgoal_tac "\y \ r-``{x}. \z. :Y <-> :f") @@ -203,17 +200,17 @@ apply (frule_tac y="" in transM, assumption, simp) apply (rule_tac x=y in bexI) prefer 2 apply (blast dest: transD) -apply (rule_tac x=z in exI, simp) -apply (rule_tac x="restrict(f, r -`` {y})" in exI) -apply (simp add: vimage_closed restrict_closed is_recfun_restrict - apply_recfun is_recfun_type [THEN apply_iff]) +apply (rule_tac x=z in rexI) +apply (rule_tac x="restrict(f, r -`` {y})" in rexI) +apply (simp_all add: is_recfun_restrict + apply_recfun is_recfun_type [THEN apply_iff]) done text{*For typical applications of Replacement for recursive definitions*} lemma (in M_axioms) univalent_is_recfun: "[|wellfounded(M,r); trans(r); M(r)|] - ==> univalent (M, A, \x p. \y. M(y) & - (\f. M(f) & p = \x, y\ & is_recfun(r,x,H,f) & y = H(x,f)))" + ==> univalent (M, A, \x p. + \y[M]. \f[M]. 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 @@ -221,60 +218,60 @@ 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: - "[|\y. \y, a1\ \ r --> (\f. M(f) & is_recfun(r, y, H, f)); + "[|\y. \y, a1\ \ r --> (\f[M]. is_recfun(r, y, H, f)); wellfounded(M,r); trans(r); M(r); M(a1); - strong_replacement(M, \x z. \y g. M(y) & M(g) & - pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); + strong_replacement(M, \x z. + \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); \x[M]. \g[M]. function(g) --> M(H(x,g))|] - ==> \f. M(f) & is_recfun(r,a1,H,f)" + ==> \f[M]. is_recfun(r,a1,H,f)" apply (drule_tac A="r-``{a1}" in strong_replacementD) apply blast txt{*Discharge the "univalent" obligation of Replacement*} apply (simp add: univalent_is_recfun) txt{*Show that the constructed object satisfies @{text is_recfun}*} apply clarify -apply (rule_tac x=Y in exI) +apply (rule_tac x=Y in rexI) txt{*Unfold only the top-level occurrence of @{term is_recfun}*} apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1]) -txt{*The big iff-formula defininng @{term Y} is now redundant*} +txt{*The big iff-formula defining @{term Y} is now redundant*} apply safe apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H]) txt{*one more case*} apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff) apply (rename_tac x) apply (rule_tac x=x in exI, simp) -apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) +apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in rexI) apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) -apply (rule_tac x=f in exI) -apply (simp add: restrict_Y_lemma [of r H]) +apply (rename_tac f) +apply (rule_tac x=f in rexI) +apply (simp add: restrict_Y_lemma [of r H], simp_all) done text{*Relativized version, when we have the (currently weaker) premise @{term "wellfounded(M,r)"}*} lemma (in M_axioms) wellfounded_exists_is_recfun: "[|wellfounded(M,r); trans(r); - separation(M, \x. ~ (\f. M(f) \ is_recfun(r, x, H, f))); - strong_replacement(M, \x z. \y g. M(y) & M(g) & - pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); + separation(M, \x. ~ (\f[M]. is_recfun(r, x, H, f))); + strong_replacement(M, \x z. + \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); M(r); M(a); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] - ==> \f. M(f) & is_recfun(r,a,H,f)" + ==> \f[M]. is_recfun(r,a,H,f)" apply (rule wellfounded_induct, assumption+, clarify) apply (rule exists_is_recfun_indstep, assumption+) done lemma (in M_axioms) wf_exists_is_recfun [rule_format]: - "[|wf(r); trans(r); - strong_replacement(M, \x z. \y g. M(y) & M(g) & - pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); - M(r); + "[|wf(r); trans(r); M(r); + strong_replacement(M, \x z. + \y[M]. \g[M]. pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); \x[M]. \g[M]. function(g) --> M(H(x,g)) |] - ==> M(a) --> (\f. M(f) & is_recfun(r,a,H,f))" + ==> M(a) --> (\f[M]. is_recfun(r,a,H,f))" apply (rule wf_induct, assumption+) apply (frule wf_imp_relativized) apply (intro impI) -apply (rule exists_is_recfun_indstep) - apply (blast dest: pair_components_in_M)+ +apply (rule exists_is_recfun_indstep) + apply (blast dest: transM del: rev_rallE, assumption+) done constdefs @@ -346,24 +343,23 @@ fun_apply(M,f,j,fj) & fj = k" -locale M_recursion = M_axioms + +locale M_ord_arith = M_axioms + assumes oadd_strong_replacement: "[| M(i); M(j) |] ==> strong_replacement(M, - \x z. \y f fx. M(y) & M(f) & M(fx) & - pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & - image(M,f,x,fx) & y = i Un fx)" + \x z. \y[M]. \f[M]. \fx[M]. pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & + image(M,f,x,fx) & y = i Un fx)" and omult_strong_replacement': "[| M(i); M(j) |] ==> - strong_replacement(M, \x z. \y g. M(y) & M(g) & - pair(M,x,y,z) & + strong_replacement(M, \x z. \y[M]. \g[M]. + z = & is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & y = (THE z. omult_eqns(i, x, g, z)))" text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*} -lemma (in M_recursion) is_oadd_fun_iff: +lemma (in M_ord_arith) is_oadd_fun_iff: "[| a\j; M(i); M(j); M(a); M(f) |] ==> is_oadd_fun(M,i,j,a,f) <-> f \ a \ range(f) & (\x. M(x) --> x < a --> f`x = i Un f``x)" @@ -377,10 +373,10 @@ done -lemma (in M_recursion) oadd_strong_replacement': +lemma (in M_ord_arith) oadd_strong_replacement': "[| M(i); M(j) |] ==> - strong_replacement(M, \x z. \y g. M(y) & M(g) & - pair(M,x,y,z) & + strong_replacement(M, \x z. \y[M]. \g[M]. + z = & is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & y = i Un g``x)" apply (insert oadd_strong_replacement [of i j]) @@ -389,28 +385,25 @@ done -lemma (in M_recursion) exists_oadd: +lemma (in M_ord_arith) exists_oadd: "[| Ord(j); M(i); M(j) |] - ==> \f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" + ==> \f[M]. is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)" apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) - apply simp - apply (blast intro: oadd_strong_replacement') - apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) + apply (simp_all add: Memrel_type oadd_strong_replacement') +done + +lemma (in M_ord_arith) exists_oadd_fun: + "[| Ord(j); M(i); M(j) |] ==> \f[M]. is_oadd_fun(M,i,succ(j),succ(j),f)" +apply (rule exists_oadd [THEN rexE]) +apply (erule Ord_succ, assumption, simp) +apply (rename_tac f) +apply (frule is_recfun_type) +apply (rule_tac x=f in rexI) + apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def + is_oadd_fun_iff Ord_trans [OF _ succI1], assumption) done -lemma (in M_recursion) exists_oadd_fun: - "[| Ord(j); M(i); M(j) |] - ==> \f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)" -apply (rule exists_oadd [THEN exE]) -apply (erule Ord_succ, assumption, simp) -apply (rename_tac f, clarify) -apply (frule is_recfun_type) -apply (rule_tac x=f in exI) -apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def - is_oadd_fun_iff Ord_trans [OF _ succI1]) -done - -lemma (in M_recursion) is_oadd_fun_apply: +lemma (in M_ord_arith) is_oadd_fun_apply: "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] ==> f`x = i Un (\k\x. {f ` k})" apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) @@ -419,7 +412,7 @@ apply (simp add: image_fun, blast) done -lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]: +lemma (in M_ord_arith) is_oadd_fun_iff_oadd [rule_format]: "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] ==> j f`j = i++j" apply (erule_tac i=j in trans_induct, clarify) @@ -428,25 +421,25 @@ apply (blast intro: lt_trans ltI lt_Ord) done -lemma (in M_recursion) oadd_abs_fun_apply_iff: +lemma (in M_ord_arith) oadd_abs_fun_apply_iff: "[| M(i); M(J); M(f); M(k); j fun_apply(M,f,j,k) <-> f`j = k" by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs) -lemma (in M_recursion) Ord_oadd_abs: +lemma (in M_ord_arith) Ord_oadd_abs: "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j" apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd) apply (frule exists_oadd_fun [of j i], blast+) done -lemma (in M_recursion) oadd_abs: +lemma (in M_ord_arith) oadd_abs: "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j" apply (case_tac "Ord(i) & Ord(j)") apply (simp add: Ord_oadd_abs) apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd) done -lemma (in M_recursion) oadd_closed [intro,simp]: +lemma (in M_ord_arith) 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) @@ -490,7 +483,7 @@ by (simp add: omult_eqns_def) -lemma (in M_recursion) the_omult_eqns_closed: +lemma (in M_ord_arith) the_omult_eqns_closed: "[| M(i); M(x); M(g); function(g) |] ==> M(THE z. omult_eqns(i, x, g, z))" apply (case_tac "Ord(x)") @@ -501,39 +494,37 @@ apply (simp add: omult_eqns_Limit) done -lemma (in M_recursion) exists_omult: +lemma (in M_ord_arith) exists_omult: "[| Ord(j); M(i); M(j) |] - ==> \f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" + ==> \f[M]. is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)" apply (rule wf_exists_is_recfun [OF wf_Memrel trans_Memrel]) - apply simp - apply (blast intro: omult_strong_replacement') - apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed) + apply (simp_all add: Memrel_type omult_strong_replacement') apply (blast intro: the_omult_eqns_closed) done -lemma (in M_recursion) exists_omult_fun: - "[| Ord(j); M(i); M(j) |] ==> \f. M(f) & is_omult_fun(M,i,succ(j),f)" -apply (rule exists_omult [THEN exE]) +lemma (in M_ord_arith) exists_omult_fun: + "[| Ord(j); M(i); M(j) |] ==> \f[M]. is_omult_fun(M,i,succ(j),f)" +apply (rule exists_omult [THEN rexE]) apply (erule Ord_succ, assumption, simp) -apply (rename_tac f, clarify) +apply (rename_tac f) apply (frule is_recfun_type) -apply (rule_tac x=f in exI) +apply (rule_tac x=f in rexI) apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def is_omult_fun_def Ord_trans [OF _ succI1]) -apply (force dest: Ord_in_Ord' - simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ - the_omult_eqns_Limit) + apply (force dest: Ord_in_Ord' + simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ + the_omult_eqns_Limit, assumption) done -lemma (in M_recursion) is_omult_fun_apply_0: +lemma (in M_ord_arith) is_omult_fun_apply_0: "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0" by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib) -lemma (in M_recursion) is_omult_fun_apply_succ: +lemma (in M_ord_arith) is_omult_fun_apply_succ: "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i" by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) -lemma (in M_recursion) is_omult_fun_apply_Limit: +lemma (in M_ord_arith) is_omult_fun_apply_Limit: "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] ==> f ` x = (\y\x. f`y)" apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify) @@ -541,7 +532,7 @@ apply (simp add: ball_conj_distrib omult_Limit image_function) done -lemma (in M_recursion) is_omult_fun_eq_omult: +lemma (in M_ord_arith) is_omult_fun_eq_omult: "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] ==> j f`j = i**j" apply (erule_tac i=j in trans_induct3) @@ -555,12 +546,12 @@ apply (blast intro: lt_trans ltI lt_Ord) done -lemma (in M_recursion) omult_abs_fun_apply_iff: +lemma (in M_ord_arith) omult_abs_fun_apply_iff: "[| M(i); M(J); M(f); M(k); j fun_apply(M,f,j,k) <-> f`j = k" by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs) -lemma (in M_recursion) omult_abs: +lemma (in M_ord_arith) omult_abs: "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j" apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult) apply (frule exists_omult_fun [of j i], blast+)