new definitions of fun_apply and M_is_recfun
authorpaulson
Fri Jul 12 11:24:40 2002 +0200 (2002-07-12)
changeset 133523cd767f8d78b
parent 13351 bc1fb6941b54
child 13353 1800e7134d2e
new definitions of fun_apply and M_is_recfun
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 11 17:56:28 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 12 11:24:40 2002 +0200
     1.3 @@ -95,9 +95,9 @@
     1.4  lemma (in M_trancl) iterates_relativize:
     1.5    "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
     1.6       strong_replacement(M, 
     1.7 -       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
     1.8 -              is_recfun (Memrel(succ(n)), x,
     1.9 -                         \<lambda>n f. nat_case(v, \<lambda>m. F(f`m), n), g) &
    1.10 +       \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M,x,y,z) &
    1.11 +              M_is_recfun(M, \<lambda>n f z. z = nat_case(v, \<lambda>m. F(f`m), n), 
    1.12 +                          Memrel(succ(n)), x, g) &
    1.13                y = nat_case(v, \<lambda>m. F(g`m), x))|] 
    1.14     ==> iterates(F,n,v) = z <-> 
    1.15         (\<exists>g[M]. is_recfun(Memrel(succ(n)), n, 
    1.16 @@ -105,7 +105,8 @@
    1.17              z = nat_case(v, \<lambda>m. F(g`m), n))"
    1.18  by (simp add: iterates_nat_def recursor_def transrec_def 
    1.19                eclose_sing_Ord_eq trans_wfrec_relativize nat_into_M
    1.20 -              wf_Memrel trans_Memrel relation_Memrel)
    1.21 +              wf_Memrel trans_Memrel relation_Memrel
    1.22 +              is_recfun_abs [of "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.23  
    1.24  lemma (in M_wfrank) iterates_closed [intro,simp]:
    1.25    "[|n \<in> nat; M(v); \<forall>x[M]. M(F(x));
    1.26 @@ -126,8 +127,9 @@
    1.27          \<exists>n1[M]. \<exists>AX[M]. 
    1.28           number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)"
    1.29  
    1.30 -  is_list_case :: "[i=>o,i,i,i,i] => o"
    1.31 -    "is_list_case(M,A,g,x,y) == 
    1.32 +  list_functor_case :: "[i=>o,i,i,i,i] => o"
    1.33 +    --{*Abbreviation for the definition of lists below*}
    1.34 +    "list_functor_case(M,A,g,x,y) == 
    1.35          is_nat_case(M, 0, 
    1.36               \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & is_list_functor(M,A,gm,u),
    1.37               x, y)"
    1.38 @@ -136,6 +138,12 @@
    1.39       "[| M(A); M(X); M(Z) |] ==> is_list_functor(M,A,X,Z) <-> (Z = {0} + A*X)"
    1.40  by (simp add: is_list_functor_def singleton_0 nat_into_M)
    1.41  
    1.42 +lemma (in M_axioms) list_functor_case_abs: 
    1.43 +     "[| M(A); M(n); M(y); M(g) |] 
    1.44 +      ==> list_functor_case(M,A,g,n,y) <-> 
    1.45 +          y = nat_case(0, \<lambda>m. {0} + A * g`m, n)"
    1.46 +by (simp add: list_functor_case_def nat_into_M)
    1.47 +
    1.48  
    1.49  locale M_datatypes = M_wfrank +
    1.50    assumes list_replacement1: 
    1.51 @@ -144,10 +152,9 @@
    1.52  	  \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M]. 
    1.53  		 pair(M,x,y,z) & successor(M,n,sucn) & 
    1.54  		 membership(M,sucn,memr) &
    1.55 -		 M_is_recfun (M, memr, x,
    1.56 -	              \<lambda>n f z. z = nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
    1.57 -		 is_nat_case(M, 0, 
    1.58 -                      \<lambda>m u. is_list_functor(M,A,g`m,u), x, y))"
    1.59 +		 M_is_recfun(M, \<lambda>n f z. list_functor_case(M,A,f,n,z), 
    1.60 +                             memr, x, g) &
    1.61 +                 list_functor_case(M,A,g,x,y))"
    1.62  (*THEY NEED RELATIVIZATION*)
    1.63        and list_replacement2: 
    1.64             "M(A) ==> strong_replacement(M, \<lambda>x y. y = (\<lambda>X. {0} + A * X)^x (0))"
    1.65 @@ -162,7 +169,7 @@
    1.66  		          \<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n), g) &
    1.67   	       y = nat_case(0, \<lambda>m. {0} + A * g ` m, x)))"
    1.68  apply (insert list_replacement1 [of A n], simp add: nat_into_M)
    1.69 -apply (simp add: nat_into_M apply_abs
    1.70 +apply (simp add: nat_into_M list_functor_case_abs
    1.71                   is_recfun_abs [of "\<lambda>n f. nat_case(0, \<lambda>m. {0} + A * f`m, n)"])
    1.72  done
    1.73  
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Jul 11 17:56:28 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Jul 12 11:24:40 2002 +0200
     2.3 @@ -563,40 +563,40 @@
     2.4  done
     2.5  
     2.6  
     2.7 -subsubsection{*Function Application, Internalized*}
     2.8 +subsubsection{*Big Union, Internalized*}
     2.9  
    2.10 -constdefs fun_apply_fm :: "[i,i,i]=>i"
    2.11 -    "fun_apply_fm(f,x,y) == 
    2.12 -       Forall(Iff(Exists(And(Member(0,succ(succ(f))),
    2.13 -                             pair_fm(succ(succ(x)), 1, 0))),
    2.14 -                  Equal(succ(y),0)))"
    2.15 +(*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
    2.16 +constdefs big_union_fm :: "[i,i]=>i"
    2.17 +    "big_union_fm(A,z) == 
    2.18 +       Forall(Iff(Member(0,succ(z)),
    2.19 +                  Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
    2.20  
    2.21 -lemma fun_apply_type [TC]:
    2.22 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
    2.23 -by (simp add: fun_apply_fm_def) 
    2.24 +lemma big_union_type [TC]:
    2.25 +     "[| x \<in> nat; y \<in> nat |] ==> big_union_fm(x,y) \<in> formula"
    2.26 +by (simp add: big_union_fm_def) 
    2.27  
    2.28 -lemma arity_fun_apply_fm [simp]:
    2.29 -     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    2.30 -      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.31 -by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) 
    2.32 +lemma arity_big_union_fm [simp]:
    2.33 +     "[| x \<in> nat; y \<in> nat |] 
    2.34 +      ==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)"
    2.35 +by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac)
    2.36  
    2.37 -lemma sats_fun_apply_fm [simp]:
    2.38 -   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.39 -    ==> sats(A, fun_apply_fm(x,y,z), env) <-> 
    2.40 -        fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
    2.41 -by (simp add: fun_apply_fm_def fun_apply_def)
    2.42 +lemma sats_big_union_fm [simp]:
    2.43 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    2.44 +    ==> sats(A, big_union_fm(x,y), env) <-> 
    2.45 +        big_union(**A, nth(x,env), nth(y,env))"
    2.46 +by (simp add: big_union_fm_def big_union_def)
    2.47  
    2.48 -lemma fun_apply_iff_sats:
    2.49 -      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    2.50 -          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    2.51 -       ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
    2.52 +lemma big_union_iff_sats:
    2.53 +      "[| nth(i,env) = x; nth(j,env) = y; 
    2.54 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
    2.55 +       ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)"
    2.56  by simp
    2.57  
    2.58 -theorem fun_apply_reflection:
    2.59 -     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), 
    2.60 -               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" 
    2.61 -apply (simp only: fun_apply_def setclass_simps)
    2.62 -apply (intro FOL_reflections pair_reflection)  
    2.63 +theorem big_union_reflection:
    2.64 +     "REFLECTS[\<lambda>x. big_union(L,f(x),g(x)), 
    2.65 +               \<lambda>i x. big_union(**Lset(i),f(x),g(x))]"
    2.66 +apply (simp only: big_union_def setclass_simps)
    2.67 +apply (intro FOL_reflections)  
    2.68  done
    2.69  
    2.70  
    2.71 @@ -924,6 +924,47 @@
    2.72  done
    2.73  
    2.74  
    2.75 +subsubsection{*Function Application, Internalized*}
    2.76 +
    2.77 +(* "fun_apply(M,f,x,y) == 
    2.78 +        (\<exists>xs[M]. \<exists>fxs[M]. 
    2.79 +         upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
    2.80 +constdefs fun_apply_fm :: "[i,i,i]=>i"
    2.81 +    "fun_apply_fm(f,x,y) == 
    2.82 +       Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
    2.83 +                         And(image_fm(succ(succ(f)), 1, 0), 
    2.84 +                             big_union_fm(0,succ(succ(y)))))))"
    2.85 +
    2.86 +lemma fun_apply_type [TC]:
    2.87 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> fun_apply_fm(x,y,z) \<in> formula"
    2.88 +by (simp add: fun_apply_fm_def) 
    2.89 +
    2.90 +lemma arity_fun_apply_fm [simp]:
    2.91 +     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
    2.92 +      ==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    2.93 +by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) 
    2.94 +
    2.95 +lemma sats_fun_apply_fm [simp]:
    2.96 +   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.97 +    ==> sats(A, fun_apply_fm(x,y,z), env) <-> 
    2.98 +        fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"
    2.99 +by (simp add: fun_apply_fm_def fun_apply_def)
   2.100 +
   2.101 +lemma fun_apply_iff_sats:
   2.102 +      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   2.103 +          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   2.104 +       ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)"
   2.105 +by simp
   2.106 +
   2.107 +theorem fun_apply_reflection:
   2.108 +     "REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), 
   2.109 +               \<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" 
   2.110 +apply (simp only: fun_apply_def setclass_simps)
   2.111 +apply (intro FOL_reflections upair_reflection image_reflection
   2.112 +             big_union_reflection)  
   2.113 +done
   2.114 +
   2.115 +
   2.116  subsubsection{*The Concept of Relation, Internalized*}
   2.117  
   2.118  (* "is_relation(M,r) == 
   2.119 @@ -1036,7 +1077,7 @@
   2.120  
   2.121  lemmas function_reflections = 
   2.122          empty_reflection upair_reflection pair_reflection union_reflection
   2.123 -	cons_reflection successor_reflection 
   2.124 +	big_union_reflection cons_reflection successor_reflection 
   2.125          fun_apply_reflection subset_reflection
   2.126  	transitive_set_reflection membership_reflection
   2.127  	pred_set_reflection domain_reflection range_reflection field_reflection
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 11 17:56:28 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Jul 12 11:24:40 2002 +0200
     3.3 @@ -196,8 +196,8 @@
     3.4  
     3.5  subsection{*Well-Founded Recursion!*}
     3.6  
     3.7 -(* M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o"
     3.8 -   "M_is_recfun(M,r,a,MH,f) == 
     3.9 +(* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    3.10 +   "M_is_recfun(M,MH,r,a,f) == 
    3.11       \<forall>z[M]. z \<in> f <-> 
    3.12              5      4       3       2       1           0
    3.13              (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
    3.14 @@ -252,7 +252,7 @@
    3.15    shows 
    3.16        "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    3.17         ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> 
    3.18 -           M_is_recfun(**A, nth(x,env), nth(y,env), MH, nth(z,env))"
    3.19 +           M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
    3.20  by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
    3.21  
    3.22  lemma is_recfun_iff_sats:
    3.23 @@ -261,15 +261,15 @@
    3.24                          sats(A, p(x,y,z), env));
    3.25        nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    3.26        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    3.27 -   ==> M_is_recfun(**A, x, y, MH, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" 
    3.28 +   ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" 
    3.29  by (simp add: sats_is_recfun_fm [of A MH])
    3.30  
    3.31  theorem is_recfun_reflection:
    3.32    assumes MH_reflection:
    3.33      "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)), 
    3.34                       \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
    3.35 -  shows "REFLECTS[\<lambda>x. M_is_recfun(L, f(x), g(x), MH(L), h(x)), 
    3.36 -               \<lambda>i x. M_is_recfun(**Lset(i), f(x), g(x), MH(**Lset(i)), h(x))]"
    3.37 +  shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)), 
    3.38 +               \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
    3.39  apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
    3.40  apply (intro FOL_reflections function_reflections 
    3.41               restriction_reflection MH_reflection)  
    3.42 @@ -279,15 +279,17 @@
    3.43  
    3.44  lemma wfrank_Reflects:
    3.45   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    3.46 -              ~ (\<exists>f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)),
    3.47 +              ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
    3.48        \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
    3.49 -         ~ (\<exists>f \<in> Lset(i). M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f))]"
    3.50 +         ~ (\<exists>f \<in> Lset(i). 
    3.51 +            M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), 
    3.52 +                        rplus, x, f))]"
    3.53  by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)  
    3.54  
    3.55  lemma wfrank_separation:
    3.56       "L(r) ==>
    3.57        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    3.58 -         ~ (\<exists>f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)))"
    3.59 +         ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
    3.60  apply (rule separation_CollectI) 
    3.61  apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
    3.62  apply (rule ReflectsE [OF wfrank_Reflects], assumption)
    3.63 @@ -309,12 +311,12 @@
    3.64   "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A & 
    3.65          (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
    3.66           (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
    3.67 -                        M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) &
    3.68 +                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
    3.69                          is_range(L,f,y))),
    3.70   \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A & 
    3.71        (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
    3.72         (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  & 
    3.73 -         M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f) &
    3.74 +         M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
    3.75           is_range(**Lset(i),f,y)))]"
    3.76  by (intro FOL_reflections function_reflections fun_plus_reflections
    3.77               is_recfun_reflection tran_closure_reflection)
    3.78 @@ -325,7 +327,7 @@
    3.79        strong_replacement(L, \<lambda>x z. 
    3.80           \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    3.81           (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  & 
    3.82 -                        M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) &
    3.83 +                        M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
    3.84                          is_range(L,f,y)))"
    3.85  apply (rule strong_replacementI) 
    3.86  apply (rule rallI)
    3.87 @@ -351,12 +353,13 @@
    3.88   "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
    3.89            ~ (\<forall>f[L]. \<forall>rangef[L]. 
    3.90               is_range(L,f,rangef) -->
    3.91 -             M_is_recfun(L, rplus, x, \<lambda>x f y. is_range(L,f,y), f) -->
    3.92 +             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
    3.93               ordinal(L,rangef)),
    3.94        \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) --> 
    3.95            ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i). 
    3.96               is_range(**Lset(i),f,rangef) -->
    3.97 -             M_is_recfun(**Lset(i), rplus, x, \<lambda>x f y. is_range(**Lset(i),f,y), f) -->
    3.98 +             M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y), 
    3.99 +                         rplus, x, f) -->
   3.100               ordinal(**Lset(i),rangef))]"
   3.101  by (intro FOL_reflections function_reflections is_recfun_reflection 
   3.102            tran_closure_reflection ordinal_reflection)
   3.103 @@ -367,7 +370,7 @@
   3.104           \<forall>rplus[L]. tran_closure(L,r,rplus) --> 
   3.105            ~ (\<forall>f[L]. \<forall>rangef[L]. 
   3.106               is_range(L,f,rangef) -->
   3.107 -             M_is_recfun(L, rplus, x, \<lambda>x f y. is_range(L,f,y), f) -->
   3.108 +             M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
   3.109               ordinal(L,rangef)))" 
   3.110  apply (rule separation_CollectI) 
   3.111  apply (rule_tac A="{r,z}" in subset_LsetE, blast ) 
     4.1 --- a/src/ZF/Constructible/Relative.thy	Thu Jul 11 17:56:28 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Jul 12 11:24:40 2002 +0200
     4.3 @@ -96,7 +96,8 @@
     4.4  
     4.5    fun_apply :: "[i=>o,i,i,i] => o"
     4.6      "fun_apply(M,f,x,y) == 
     4.7 -	(\<forall>y'[M]. (\<exists>u[M]. u\<in>f & pair(M,x,y',u)) <-> y=y')"
     4.8 +        (\<exists>xs[M]. \<exists>fxs[M]. 
     4.9 +         upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))"
    4.10  
    4.11    typed_function :: "[i=>o,i,i,i] => o"
    4.12      "typed_function(M,A,B,r) == 
    4.13 @@ -646,6 +647,13 @@
    4.14   apply (simp_all add: b_abs) 
    4.15  done
    4.16  
    4.17 +(*Needed?  surely better to replace by nat_case?*)
    4.18 +lemma (in M_triv_axioms) is_nat_case_cong [cong]:
    4.19 +     "[| a = a'; k = k';  z = z';  M(z');
    4.20 +       !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
    4.21 +      ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"
    4.22 +by (simp add: is_nat_case_def) 
    4.23 +
    4.24  lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
    4.25       "M(Inl(a)) <-> M(a)"
    4.26  by (simp add: Inl_def) 
    4.27 @@ -970,18 +978,12 @@
    4.28       "[|M(f); M(a)|] ==> M(f`a)"
    4.29  by (simp add: apply_def)
    4.30  
    4.31 -lemma (in M_axioms) apply_abs: 
    4.32 -     "[| function(f); M(f); M(y) |] 
    4.33 -      ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
    4.34 -apply (simp add: fun_apply_def)
    4.35 -apply (blast intro: function_apply_equality function_apply_Pair) 
    4.36 +lemma (in M_axioms) apply_abs [simp]: 
    4.37 +     "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y"
    4.38 +apply (simp add: fun_apply_def apply_def)
    4.39 +apply (blast intro: elim:); 
    4.40  done
    4.41  
    4.42 -lemma (in M_axioms) typed_apply_abs: 
    4.43 -     "[| f \<in> A -> B; M(f); M(y) |] 
    4.44 -      ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
    4.45 -by (simp add: apply_abs fun_is_function domain_of_fun) 
    4.46 -
    4.47  lemma (in M_axioms) typed_function_abs [simp]: 
    4.48       "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
    4.49  apply (auto simp add: typed_function_def relation_def Pi_iff) 
    4.50 @@ -996,7 +998,7 @@
    4.51  
    4.52  lemma (in M_axioms) surjection_abs [simp]: 
    4.53       "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
    4.54 -by (simp add: typed_apply_abs surjection_def surj_def)
    4.55 +by (simp add: surjection_def surj_def)
    4.56  
    4.57  lemma (in M_axioms) bijection_abs [simp]: 
    4.58       "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
     5.1 --- a/src/ZF/Constructible/Separation.thy	Thu Jul 11 17:56:28 2002 +0200
     5.2 +++ b/src/ZF/Constructible/Separation.thy	Fri Jul 12 11:24:40 2002 +0200
     5.3 @@ -503,7 +503,6 @@
     5.4  bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs"));
     5.5  bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed"));
     5.6  bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs"));
     5.7 -bind_thm ("typed_apply_abs", axiomsL (thm "M_axioms.typed_apply_abs"));
     5.8  bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs"));
     5.9  bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs"));
    5.10  bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs"));
     6.1 --- a/src/ZF/Constructible/WF_absolute.thy	Thu Jul 11 17:56:28 2002 +0200
     6.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Jul 12 11:24:40 2002 +0200
     6.3 @@ -140,9 +140,8 @@
     6.4             (\<exists>f[M]. f \<in> succ(n) -> A &
     6.5              (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
     6.6                             (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
     6.7 -apply (simp add: rtran_closure_mem_def typed_apply_abs
     6.8 -                 Ord_succ_mem_iff nat_0_le [THEN ltD], blast) 
     6.9 -done
    6.10 +by (simp add: rtran_closure_mem_def Ord_succ_mem_iff nat_0_le [THEN ltD]) 
    6.11 +
    6.12  
    6.13  locale M_trancl = M_axioms +
    6.14    assumes rtrancl_separation:
    6.15 @@ -237,13 +236,13 @@
    6.16       "M(r) ==>
    6.17        separation (M, \<lambda>x. 
    6.18           \<forall>rplus[M]. tran_closure(M,r,rplus) -->
    6.19 -         ~ (\<exists>f[M]. M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f)))"
    6.20 +         ~ (\<exists>f[M]. M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f)))"
    6.21   and wfrank_strong_replacement:
    6.22       "M(r) ==>
    6.23        strong_replacement(M, \<lambda>x z. 
    6.24           \<forall>rplus[M]. tran_closure(M,r,rplus) -->
    6.25           (\<exists>y[M]. \<exists>f[M]. pair(M,x,y,z)  & 
    6.26 -                        M_is_recfun(M, rplus, x, %x f y. is_range(M,f,y), f) &
    6.27 +                        M_is_recfun(M, %x f y. is_range(M,f,y), rplus, x, f) &
    6.28                          is_range(M,f,y)))"
    6.29   and Ord_wfrank_separation:
    6.30       "M(r) ==>
    6.31 @@ -251,7 +250,7 @@
    6.32           \<forall>rplus[M]. tran_closure(M,r,rplus) --> 
    6.33            ~ (\<forall>f[M]. \<forall>rangef[M]. 
    6.34               is_range(M,f,rangef) -->
    6.35 -             M_is_recfun(M, rplus, x, \<lambda>x f y. is_range(M,f,y), f) -->
    6.36 +             M_is_recfun(M, \<lambda>x f y. is_range(M,f,y), rplus, x, f) -->
    6.37               ordinal(M,rangef)))" 
    6.38  
    6.39  text{*Proving that the relativized instances of Separation or Replacement
     7.1 --- a/src/ZF/Constructible/WFrec.thy	Thu Jul 11 17:56:28 2002 +0200
     7.2 +++ b/src/ZF/Constructible/WFrec.thy	Fri Jul 12 11:24:40 2002 +0200
     7.3 @@ -69,7 +69,7 @@
     7.4          M(r); M(f); M(g); M(a); M(b) |] 
     7.5       ==> separation(M, \<lambda>x. \<not> (\<langle>x, a\<rangle> \<in> r \<longrightarrow> \<langle>x, b\<rangle> \<in> r \<longrightarrow> f ` x = g ` x))"
     7.6  apply (insert is_recfun_separation [of r f g a b]) 
     7.7 -apply (simp add: typed_apply_abs vimage_singleton_iff)
     7.8 +apply (simp add: vimage_singleton_iff)
     7.9  done
    7.10  
    7.11  text{*Stated using @{term "trans(r)"} rather than
    7.12 @@ -275,8 +275,8 @@
    7.13  done
    7.14  
    7.15  constdefs
    7.16 - M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o"
    7.17 -   "M_is_recfun(M,r,a,MH,f) == 
    7.18 + M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    7.19 +   "M_is_recfun(M,MH,r,a,f) == 
    7.20       \<forall>z[M]. z \<in> f <-> 
    7.21              (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M]. 
    7.22  	       pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
    7.23 @@ -286,7 +286,7 @@
    7.24  lemma (in M_axioms) is_recfun_abs:
    7.25       "[| \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g));  M(r); M(a); M(f); 
    7.26           \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(x,g,y) <-> y = H(x,g) |] 
    7.27 -      ==> M_is_recfun(M,r,a,MH,f) <-> is_recfun(r,a,H,f)"
    7.28 +      ==> M_is_recfun(M,MH,r,a,f) <-> is_recfun(r,a,H,f)"
    7.29  apply (simp add: M_is_recfun_def is_recfun_relativize)
    7.30  apply (rule rall_cong)
    7.31  apply (blast dest: transM)
    7.32 @@ -295,7 +295,7 @@
    7.33  lemma M_is_recfun_cong [cong]:
    7.34       "[| r = r'; a = a'; f = f'; 
    7.35         !!x g y. [| M(x); M(g); M(y) |] ==> MH(x,g,y) <-> MH'(x,g,y) |]
    7.36 -      ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')"
    7.37 +      ==> M_is_recfun(M,MH,r,a,f) <-> M_is_recfun(M,MH',r',a',f')"
    7.38  by (simp add: M_is_recfun_def) 
    7.39  
    7.40  
    7.41 @@ -308,9 +308,9 @@
    7.42      "is_oadd_fun(M,i,j,x,f) == 
    7.43         (\<forall>sj msj. M(sj) --> M(msj) --> 
    7.44                   successor(M,j,sj) --> membership(M,sj,msj) --> 
    7.45 -	         M_is_recfun(M, msj, x, 
    7.46 +	         M_is_recfun(M, 
    7.47  		     %x g y. \<exists>gx[M]. image(M,g,x,gx) & union(M,i,gx,y),
    7.48 -		     f))"
    7.49 +		     msj, x, f))"
    7.50  
    7.51   is_oadd :: "[i=>o,i,i,i] => o"
    7.52      "is_oadd(M,i,j,k) == 
    7.53 @@ -422,14 +422,9 @@
    7.54  apply (blast intro: lt_trans ltI lt_Ord) 
    7.55  done
    7.56  
    7.57 -lemma (in M_ord_arith) oadd_abs_fun_apply_iff:
    7.58 -    "[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |] 
    7.59 -     ==> fun_apply(M,f,j,k) <-> f`j = k"
    7.60 -by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs) 
    7.61 -
    7.62  lemma (in M_ord_arith) Ord_oadd_abs:
    7.63      "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
    7.64 -apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
    7.65 +apply (simp add: is_oadd_def is_oadd_fun_iff_oadd)
    7.66  apply (frule exists_oadd_fun [of j i], blast+)
    7.67  done
    7.68  
    7.69 @@ -547,14 +542,9 @@
    7.70  apply (blast intro: lt_trans ltI lt_Ord) 
    7.71  done
    7.72  
    7.73 -lemma (in M_ord_arith) omult_abs_fun_apply_iff:
    7.74 -    "[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |] 
    7.75 -     ==> fun_apply(M,f,j,k) <-> f`j = k"
    7.76 -by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs) 
    7.77 -
    7.78  lemma (in M_ord_arith) omult_abs:
    7.79      "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
    7.80 -apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
    7.81 +apply (simp add: is_omult_def is_omult_fun_eq_omult)
    7.82  apply (frule exists_omult_fun [of j i], blast+)
    7.83  done
    7.84  
     8.1 --- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 11 17:56:28 2002 +0200
     8.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Jul 12 11:24:40 2002 +0200
     8.3 @@ -161,9 +161,7 @@
     8.4  lemma (in M_axioms) order_isomorphism_abs [simp]: 
     8.5       "[| M(A); M(B); M(f) |] 
     8.6        ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
     8.7 -by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed 
     8.8 -              order_isomorphism_def ord_iso_def)
     8.9 -
    8.10 +by (simp add: apply_closed order_isomorphism_def ord_iso_def)
    8.11  
    8.12  lemma (in M_axioms) pred_set_abs [simp]: 
    8.13       "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
    8.14 @@ -236,7 +234,7 @@
    8.15  apply (elim conjE CollectE) 
    8.16  apply (erule wellfounded_on_induct, assumption+)
    8.17   apply (insert well_ord_iso_separation [of A f r])
    8.18 - apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify) 
    8.19 + apply (simp, clarify) 
    8.20  apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
    8.21  done
    8.22