# HG changeset patch # User paulson # Date 1026465880 -7200 # Node ID 3cd767f8d78b3600d4d6f2bcf5e734e2a5ca78c3 # Parent bc1fb6941b54370001e802251c65f6642bb956c6 new definitions of fun_apply and M_is_recfun diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Fri Jul 12 11:24:40 2002 +0200 @@ -95,9 +95,9 @@ 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) & + \x z. \y[M]. \g[M]. pair(M,x,y,z) & + M_is_recfun(M, \n f z. z = nat_case(v, \m. F(f`m), n), + Memrel(succ(n)), x, g) & y = nat_case(v, \m. F(g`m), x))|] ==> iterates(F,n,v) = z <-> (\g[M]. is_recfun(Memrel(succ(n)), n, @@ -105,7 +105,8 @@ 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) + wf_Memrel trans_Memrel relation_Memrel + is_recfun_abs [of "\n g. nat_case(v, \m. F(g`m), n)"]) lemma (in M_wfrank) iterates_closed [intro,simp]: "[|n \ nat; M(v); \x[M]. M(F(x)); @@ -126,8 +127,9 @@ \n1[M]. \AX[M]. number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" - is_list_case :: "[i=>o,i,i,i,i] => o" - "is_list_case(M,A,g,x,y) == + list_functor_case :: "[i=>o,i,i,i,i] => o" + --{*Abbreviation for the definition of lists below*} + "list_functor_case(M,A,g,x,y) == is_nat_case(M, 0, \m u. \gm[M]. fun_apply(M,g,m,gm) & is_list_functor(M,A,gm,u), x, y)" @@ -136,6 +138,12 @@ "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)" by (simp add: is_list_functor_def singleton_0 nat_into_M) +lemma (in M_axioms) list_functor_case_abs: + "[| M(A); M(n); M(y); M(g) |] + ==> list_functor_case(M,A,g,n,y) <-> + y = nat_case(0, \m. {0} + A * g`m, n)" +by (simp add: list_functor_case_def nat_into_M) + locale M_datatypes = M_wfrank + assumes list_replacement1: @@ -144,10 +152,9 @@ \x z. \y[M]. \g[M]. \sucn[M]. \memr[M]. pair(M,x,y,z) & successor(M,n,sucn) & membership(M,sucn,memr) & - M_is_recfun (M, memr, x, - \n f z. z = nat_case(0, \m. {0} + A * f`m, n), g) & - is_nat_case(M, 0, - \m u. is_list_functor(M,A,g`m,u), x, y))" + M_is_recfun(M, \n f z. list_functor_case(M,A,f,n,z), + memr, x, g) & + list_functor_case(M,A,g,x,y))" (*THEY NEED RELATIVIZATION*) and list_replacement2: "M(A) ==> strong_replacement(M, \x y. y = (\X. {0} + A * X)^x (0))" @@ -162,7 +169,7 @@ \n f. nat_case(0, \m. {0} + A * f`m, n), g) & y = nat_case(0, \m. {0} + A * g ` m, x)))" apply (insert list_replacement1 [of A n], simp add: nat_into_M) -apply (simp add: nat_into_M apply_abs +apply (simp add: nat_into_M list_functor_case_abs is_recfun_abs [of "\n f. nat_case(0, \m. {0} + A * f`m, n)"]) done diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Fri Jul 12 11:24:40 2002 +0200 @@ -563,40 +563,40 @@ done -subsubsection{*Function Application, Internalized*} +subsubsection{*Big Union, Internalized*} -constdefs fun_apply_fm :: "[i,i,i]=>i" - "fun_apply_fm(f,x,y) == - Forall(Iff(Exists(And(Member(0,succ(succ(f))), - pair_fm(succ(succ(x)), 1, 0))), - Equal(succ(y),0)))" +(* "big_union(M,A,z) == \x[M]. x \ z <-> (\y[M]. y\A & x \ y)" *) +constdefs big_union_fm :: "[i,i]=>i" + "big_union_fm(A,z) == + Forall(Iff(Member(0,succ(z)), + Exists(And(Member(0,succ(succ(A))), Member(1,0)))))" -lemma fun_apply_type [TC]: - "[| x \ nat; y \ nat; z \ nat |] ==> fun_apply_fm(x,y,z) \ formula" -by (simp add: fun_apply_fm_def) +lemma big_union_type [TC]: + "[| x \ nat; y \ nat |] ==> big_union_fm(x,y) \ formula" +by (simp add: big_union_fm_def) -lemma arity_fun_apply_fm [simp]: - "[| x \ nat; y \ nat; z \ nat |] - ==> arity(fun_apply_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" -by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) +lemma arity_big_union_fm [simp]: + "[| x \ nat; y \ nat |] + ==> arity(big_union_fm(x,y)) = succ(x) \ succ(y)" +by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac) -lemma sats_fun_apply_fm [simp]: - "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] - ==> sats(A, fun_apply_fm(x,y,z), env) <-> - fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: fun_apply_fm_def fun_apply_def) +lemma sats_big_union_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, big_union_fm(x,y), env) <-> + big_union(**A, nth(x,env), nth(y,env))" +by (simp add: big_union_fm_def big_union_def) -lemma fun_apply_iff_sats: - "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; - i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)" +lemma big_union_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)" by simp -theorem fun_apply_reflection: - "REFLECTS[\x. fun_apply(L,f(x),g(x),h(x)), - \i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: fun_apply_def setclass_simps) -apply (intro FOL_reflections pair_reflection) +theorem big_union_reflection: + "REFLECTS[\x. big_union(L,f(x),g(x)), + \i x. big_union(**Lset(i),f(x),g(x))]" +apply (simp only: big_union_def setclass_simps) +apply (intro FOL_reflections) done @@ -924,6 +924,47 @@ done +subsubsection{*Function Application, Internalized*} + +(* "fun_apply(M,f,x,y) == + (\xs[M]. \fxs[M]. + upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *) +constdefs fun_apply_fm :: "[i,i,i]=>i" + "fun_apply_fm(f,x,y) == + Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1), + And(image_fm(succ(succ(f)), 1, 0), + big_union_fm(0,succ(succ(y)))))))" + +lemma fun_apply_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> fun_apply_fm(x,y,z) \ formula" +by (simp add: fun_apply_fm_def) + +lemma arity_fun_apply_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(fun_apply_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_fun_apply_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, fun_apply_fm(x,y,z), env) <-> + fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: fun_apply_fm_def fun_apply_def) + +lemma fun_apply_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)" +by simp + +theorem fun_apply_reflection: + "REFLECTS[\x. fun_apply(L,f(x),g(x),h(x)), + \i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: fun_apply_def setclass_simps) +apply (intro FOL_reflections upair_reflection image_reflection + big_union_reflection) +done + + subsubsection{*The Concept of Relation, Internalized*} (* "is_relation(M,r) == @@ -1036,7 +1077,7 @@ lemmas function_reflections = empty_reflection upair_reflection pair_reflection union_reflection - cons_reflection successor_reflection + big_union_reflection cons_reflection successor_reflection fun_apply_reflection subset_reflection transitive_set_reflection membership_reflection pred_set_reflection domain_reflection range_reflection field_reflection diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Fri Jul 12 11:24:40 2002 +0200 @@ -196,8 +196,8 @@ subsection{*Well-Founded Recursion!*} -(* M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o" - "M_is_recfun(M,r,a,MH,f) == +(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" + "M_is_recfun(M,MH,r,a,f) == \z[M]. z \ f <-> 5 4 3 2 1 0 (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. @@ -252,7 +252,7 @@ shows "[|x \ nat; y \ nat; z \ nat; env \ list(A)|] ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> - M_is_recfun(**A, nth(x,env), nth(y,env), MH, nth(z,env))" + M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))" by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym]) lemma is_recfun_iff_sats: @@ -261,15 +261,15 @@ sats(A, p(x,y,z), env)); nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; i \ nat; j \ nat; k \ nat; env \ list(A)|] - ==> M_is_recfun(**A, x, y, MH, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" + ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" by (simp add: sats_is_recfun_fm [of A MH]) theorem is_recfun_reflection: assumes MH_reflection: "!!f g h. REFLECTS[\x. MH(L, f(x), g(x), h(x)), \i x. MH(**Lset(i), f(x), g(x), h(x))]" - shows "REFLECTS[\x. M_is_recfun(L, f(x), g(x), MH(L), h(x)), - \i x. M_is_recfun(**Lset(i), f(x), g(x), MH(**Lset(i)), h(x))]" + shows "REFLECTS[\x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), + \i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]" apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps) apply (intro FOL_reflections function_reflections restriction_reflection MH_reflection) @@ -279,15 +279,17 @@ lemma wfrank_Reflects: "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)), + ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)), \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> - ~ (\f \ Lset(i). M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f))]" + ~ (\f \ Lset(i). + M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), + rplus, x, f))]" by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) lemma wfrank_separation: "L(r) ==> separation (L, \x. \rplus[L]. tran_closure(L,r,rplus) --> - ~ (\f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)))" + ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" apply (rule separation_CollectI) apply (rule_tac A="{r,z}" in subset_LsetE, blast ) apply (rule ReflectsE [OF wfrank_Reflects], assumption) @@ -309,12 +311,12 @@ "REFLECTS[\z. \x[L]. x \ A & (\rplus[L]. tran_closure(L,r,rplus) --> (\y[L]. \f[L]. pair(L,x,y,z) & - M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) & + M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & is_range(L,f,y))), \i z. \x \ Lset(i). x \ A & (\rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> (\y \ Lset(i). \f \ Lset(i). pair(**Lset(i),x,y,z) & - M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f) & + M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) & is_range(**Lset(i),f,y)))]" by (intro FOL_reflections function_reflections fun_plus_reflections is_recfun_reflection tran_closure_reflection) @@ -325,7 +327,7 @@ strong_replacement(L, \x z. \rplus[L]. tran_closure(L,r,rplus) --> (\y[L]. \f[L]. pair(L,x,y,z) & - M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) & + M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & is_range(L,f,y)))" apply (rule strong_replacementI) apply (rule rallI) @@ -351,12 +353,13 @@ "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> ~ (\f[L]. \rangef[L]. is_range(L,f,rangef) --> - M_is_recfun(L, rplus, x, \x f y. is_range(L,f,y), f) --> + M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> ordinal(L,rangef)), \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> ~ (\f \ Lset(i). \rangef \ Lset(i). is_range(**Lset(i),f,rangef) --> - M_is_recfun(**Lset(i), rplus, x, \x f y. is_range(**Lset(i),f,y), f) --> + M_is_recfun(**Lset(i), \x f y. is_range(**Lset(i),f,y), + rplus, x, f) --> ordinal(**Lset(i),rangef))]" by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection ordinal_reflection) @@ -367,7 +370,7 @@ \rplus[L]. tran_closure(L,r,rplus) --> ~ (\f[L]. \rangef[L]. is_range(L,f,rangef) --> - M_is_recfun(L, rplus, x, \x f y. is_range(L,f,y), f) --> + M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> ordinal(L,rangef)))" apply (rule separation_CollectI) apply (rule_tac A="{r,z}" in subset_LsetE, blast ) diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Fri Jul 12 11:24:40 2002 +0200 @@ -96,7 +96,8 @@ fun_apply :: "[i=>o,i,i,i] => o" "fun_apply(M,f,x,y) == - (\y'[M]. (\u[M]. u\f & pair(M,x,y',u)) <-> y=y')" + (\xs[M]. \fxs[M]. + upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" typed_function :: "[i=>o,i,i,i] => o" "typed_function(M,A,B,r) == @@ -646,6 +647,13 @@ apply (simp_all add: b_abs) done +(*Needed? surely better to replace by nat_case?*) +lemma (in M_triv_axioms) is_nat_case_cong [cong]: + "[| a = a'; k = k'; z = z'; M(z'); + !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] + ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')" +by (simp add: is_nat_case_def) + lemma (in M_triv_axioms) Inl_in_M_iff [iff]: "M(Inl(a)) <-> M(a)" by (simp add: Inl_def) @@ -970,18 +978,12 @@ "[|M(f); M(a)|] ==> M(f`a)" by (simp add: apply_def) -lemma (in M_axioms) apply_abs: - "[| function(f); M(f); M(y) |] - ==> fun_apply(M,f,x,y) <-> x \ domain(f) & f`x = y" -apply (simp add: fun_apply_def) -apply (blast intro: function_apply_equality function_apply_Pair) +lemma (in M_axioms) apply_abs [simp]: + "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y" +apply (simp add: fun_apply_def apply_def) +apply (blast intro: elim:); done -lemma (in M_axioms) typed_apply_abs: - "[| f \ A -> B; M(f); M(y) |] - ==> fun_apply(M,f,x,y) <-> x \ A & f`x = y" -by (simp add: apply_abs fun_is_function domain_of_fun) - lemma (in M_axioms) typed_function_abs [simp]: "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \ A -> B" apply (auto simp add: typed_function_def relation_def Pi_iff) @@ -996,7 +998,7 @@ lemma (in M_axioms) surjection_abs [simp]: "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \ surj(A,B)" -by (simp add: typed_apply_abs surjection_def surj_def) +by (simp add: surjection_def surj_def) lemma (in M_axioms) bijection_abs [simp]: "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \ bij(A,B)" diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Fri Jul 12 11:24:40 2002 +0200 @@ -503,7 +503,6 @@ bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs")); bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed")); bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs")); -bind_thm ("typed_apply_abs", axiomsL (thm "M_axioms.typed_apply_abs")); bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs")); bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs")); bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs")); diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Fri Jul 12 11:24:40 2002 +0200 @@ -140,9 +140,8 @@ (\f[M]. f \ succ(n) -> A & (\x[M]. \y[M]. p = & f`0 = x & f`n = y) & (\i\n. \ r)))" -apply (simp add: rtran_closure_mem_def typed_apply_abs - Ord_succ_mem_iff nat_0_le [THEN ltD], blast) -done +by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) + locale M_trancl = M_axioms + assumes rtrancl_separation: @@ -237,13 +236,13 @@ "M(r) ==> separation (M, \x. \rplus[M]. tran_closure(M,r,rplus) --> - ~ (\f[M]. M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f)))" + ~ (\f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))" and wfrank_strong_replacement: "M(r) ==> strong_replacement(M, \x z. \rplus[M]. tran_closure(M,r,rplus) --> (\y[M]. \f[M]. pair(M,x,y,z) & - M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f) & + M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) & is_range(M,f,y)))" and Ord_wfrank_separation: "M(r) ==> @@ -251,7 +250,7 @@ \rplus[M]. tran_closure(M,r,rplus) --> ~ (\f[M]. \rangef[M]. is_range(M,f,rangef) --> - M_is_recfun(M, rplus, x, \x f y. is_range(M,f,y), f) --> + M_is_recfun(M, \x f y. is_range(M,f,y), rplus, x, f) --> ordinal(M,rangef)))" text{*Proving that the relativized instances of Separation or Replacement diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Fri Jul 12 11:24:40 2002 +0200 @@ -69,7 +69,7 @@ M(r); M(f); M(g); M(a); M(b) |] ==> separation(M, \x. \ (\x, a\ \ r \ \x, b\ \ r \ f ` x = g ` x))" apply (insert is_recfun_separation [of r f g a b]) -apply (simp add: typed_apply_abs vimage_singleton_iff) +apply (simp add: vimage_singleton_iff) done text{*Stated using @{term "trans(r)"} rather than @@ -275,8 +275,8 @@ done constdefs - M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o" - "M_is_recfun(M,r,a,MH,f) == + M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o" + "M_is_recfun(M,MH,r,a,f) == \z[M]. z \ f <-> (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & @@ -286,7 +286,7 @@ lemma (in M_axioms) is_recfun_abs: "[| \x[M]. \g[M]. function(g) --> M(H(x,g)); M(r); M(a); M(f); \x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] - ==> M_is_recfun(M,r,a,MH,f) <-> is_recfun(r,a,H,f)" + ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)" apply (simp add: M_is_recfun_def is_recfun_relativize) apply (rule rall_cong) apply (blast dest: transM) @@ -295,7 +295,7 @@ lemma M_is_recfun_cong [cong]: "[| r = r'; a = a'; f = f'; !!x g y. [| M(x); M(g); M(y) |] ==> MH(x,g,y) <-> MH'(x,g,y) |] - ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')" + ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')" by (simp add: M_is_recfun_def) @@ -308,9 +308,9 @@ "is_oadd_fun(M,i,j,x,f) == (\sj msj. M(sj) --> M(msj) --> successor(M,j,sj) --> membership(M,sj,msj) --> - M_is_recfun(M, msj, x, + M_is_recfun(M, %x g y. \gx[M]. image(M,g,x,gx) & union(M,i,gx,y), - f))" + msj, x, f))" is_oadd :: "[i=>o,i,i,i] => o" "is_oadd(M,i,j,k) == @@ -422,14 +422,9 @@ apply (blast intro: lt_trans ltI lt_Ord) done -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_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 (simp add: is_oadd_def is_oadd_fun_iff_oadd) apply (frule exists_oadd_fun [of j i], blast+) done @@ -547,14 +542,9 @@ apply (blast intro: lt_trans ltI lt_Ord) done -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_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 (simp add: is_omult_def is_omult_fun_eq_omult) apply (frule exists_omult_fun [of j i], blast+) done diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Thu Jul 11 17:56:28 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Fri Jul 12 11:24:40 2002 +0200 @@ -161,9 +161,7 @@ lemma (in M_axioms) order_isomorphism_abs [simp]: "[| M(A); M(B); M(f) |] ==> order_isomorphism(M,A,r,B,s,f) <-> f \ ord_iso(A,r,B,s)" -by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed - order_isomorphism_def ord_iso_def) - +by (simp add: apply_closed order_isomorphism_def ord_iso_def) lemma (in M_axioms) pred_set_abs [simp]: "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)" @@ -236,7 +234,7 @@ apply (elim conjE CollectE) apply (erule wellfounded_on_induct, assumption+) apply (insert well_ord_iso_separation [of A f r]) - apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify) + apply (simp, clarify) apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast) done