src/ZF/Constructible/Rec_Separation.thy
changeset 13807 a28a8fbc76d4
parent 13687 22dce9134953
child 15766 b08feb003f3c
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Feb 05 13:35:32 2003 +0100
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Feb 06 11:01:05 2003 +0100
     1.3 @@ -56,18 +56,18 @@
     1.4  lemma sats_rtran_closure_mem_fm [simp]:
     1.5     "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
     1.6      ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
     1.7 -        rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
     1.8 +        rtran_closure_mem(##A, nth(x,env), nth(y,env), nth(z,env))"
     1.9  by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
    1.10  
    1.11  lemma rtran_closure_mem_iff_sats:
    1.12        "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
    1.13            i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.14 -       ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
    1.15 +       ==> rtran_closure_mem(##A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
    1.16  by (simp add: sats_rtran_closure_mem_fm)
    1.17  
    1.18  lemma rtran_closure_mem_reflection:
    1.19       "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
    1.20 -               \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
    1.21 +               \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]"
    1.22  apply (simp only: rtran_closure_mem_def)
    1.23  apply (intro FOL_reflections function_reflections fun_plus_reflections)
    1.24  done
    1.25 @@ -100,18 +100,18 @@
    1.26  lemma sats_rtran_closure_fm [simp]:
    1.27     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    1.28      ==> sats(A, rtran_closure_fm(x,y), env) <->
    1.29 -        rtran_closure(**A, nth(x,env), nth(y,env))"
    1.30 +        rtran_closure(##A, nth(x,env), nth(y,env))"
    1.31  by (simp add: rtran_closure_fm_def rtran_closure_def)
    1.32  
    1.33  lemma rtran_closure_iff_sats:
    1.34        "[| nth(i,env) = x; nth(j,env) = y;
    1.35            i \<in> nat; j \<in> nat; env \<in> list(A)|]
    1.36 -       ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
    1.37 +       ==> rtran_closure(##A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
    1.38  by simp
    1.39  
    1.40  theorem rtran_closure_reflection:
    1.41       "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
    1.42 -               \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
    1.43 +               \<lambda>i x. rtran_closure(##Lset(i),f(x),g(x))]"
    1.44  apply (simp only: rtran_closure_def)
    1.45  apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
    1.46  done
    1.47 @@ -132,18 +132,18 @@
    1.48  lemma sats_tran_closure_fm [simp]:
    1.49     "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
    1.50      ==> sats(A, tran_closure_fm(x,y), env) <->
    1.51 -        tran_closure(**A, nth(x,env), nth(y,env))"
    1.52 +        tran_closure(##A, nth(x,env), nth(y,env))"
    1.53  by (simp add: tran_closure_fm_def tran_closure_def)
    1.54  
    1.55  lemma tran_closure_iff_sats:
    1.56        "[| nth(i,env) = x; nth(j,env) = y;
    1.57            i \<in> nat; j \<in> nat; env \<in> list(A)|]
    1.58 -       ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
    1.59 +       ==> tran_closure(##A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
    1.60  by simp
    1.61  
    1.62  theorem tran_closure_reflection:
    1.63       "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
    1.64 -               \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
    1.65 +               \<lambda>i x. tran_closure(##Lset(i),f(x),g(x))]"
    1.66  apply (simp only: tran_closure_def)
    1.67  apply (intro FOL_reflections function_reflections
    1.68               rtran_closure_reflection composition_reflection)
    1.69 @@ -156,7 +156,7 @@
    1.70    "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
    1.71                   w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
    1.72     \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
    1.73 -       w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
    1.74 +       w \<in> Z & pair(##Lset(i),w,x,wx) & tran_closure(##Lset(i),r,rp) &
    1.75         wx \<in> rp]"
    1.76  by (intro FOL_reflections function_reflections fun_plus_reflections
    1.77            tran_closure_reflection)
    1.78 @@ -199,10 +199,10 @@
    1.79   "REFLECTS
    1.80     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
    1.81           is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),
    1.82 -    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
    1.83 -         is_wfrec(**Lset(i),
    1.84 -                  iterates_MH(**Lset(i),
    1.85 -                          is_list_functor(**Lset(i), A), 0), memsn, u, y))]"
    1.86 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
    1.87 +         is_wfrec(##Lset(i),
    1.88 +                  iterates_MH(##Lset(i),
    1.89 +                          is_list_functor(##Lset(i), A), 0), memsn, u, y))]"
    1.90  by (intro FOL_reflections function_reflections is_wfrec_reflection
    1.91            iterates_MH_reflection list_functor_reflection)
    1.92  
    1.93 @@ -225,7 +225,7 @@
    1.94     [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
    1.95                  is_iterates(L, is_list_functor(L, A), 0, u, x),
    1.96      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
    1.97 -               is_iterates(**Lset(i), is_list_functor(**Lset(i), A), 0, u, x)]"
    1.98 +               is_iterates(##Lset(i), is_list_functor(##Lset(i), A), 0, u, x)]"
    1.99  by (intro FOL_reflections 
   1.100            is_iterates_reflection list_functor_reflection)
   1.101  
   1.102 @@ -251,10 +251,10 @@
   1.103   "REFLECTS
   1.104     [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
   1.105           is_wfrec(L, iterates_MH(L, is_formula_functor(L), 0), memsn, u, y)),
   1.106 -    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
   1.107 -         is_wfrec(**Lset(i),
   1.108 -                  iterates_MH(**Lset(i),
   1.109 -                          is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
   1.110 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
   1.111 +         is_wfrec(##Lset(i),
   1.112 +                  iterates_MH(##Lset(i),
   1.113 +                          is_formula_functor(##Lset(i)), 0), memsn, u, y))]"
   1.114  by (intro FOL_reflections function_reflections is_wfrec_reflection
   1.115            iterates_MH_reflection formula_functor_reflection)
   1.116  
   1.117 @@ -275,7 +275,7 @@
   1.118     [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
   1.119                  is_iterates(L, is_formula_functor(L), 0, u, x),
   1.120      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
   1.121 -               is_iterates(**Lset(i), is_formula_functor(**Lset(i)), 0, u, x)]"
   1.122 +               is_iterates(##Lset(i), is_formula_functor(##Lset(i)), 0, u, x)]"
   1.123  by (intro FOL_reflections 
   1.124            is_iterates_reflection formula_functor_reflection)
   1.125  
   1.126 @@ -310,7 +310,7 @@
   1.127  lemma sats_nth_fm [simp]:
   1.128     "[| x < length(env); y \<in> nat; z \<in> nat; env \<in> list(A)|]
   1.129      ==> sats(A, nth_fm(x,y,z), env) <->
   1.130 -        is_nth(**A, nth(x,env), nth(y,env), nth(z,env))"
   1.131 +        is_nth(##A, nth(x,env), nth(y,env), nth(z,env))"
   1.132  apply (frule lt_length_in_nat, assumption)  
   1.133  apply (simp add: nth_fm_def is_nth_def sats_is_iterates_fm) 
   1.134  done
   1.135 @@ -318,12 +318,12 @@
   1.136  lemma nth_iff_sats:
   1.137        "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.138            i < length(env); j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.139 -       ==> is_nth(**A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
   1.140 +       ==> is_nth(##A, x, y, z) <-> sats(A, nth_fm(i,j,k), env)"
   1.141  by (simp add: sats_nth_fm)
   1.142  
   1.143  theorem nth_reflection:
   1.144       "REFLECTS[\<lambda>x. is_nth(L, f(x), g(x), h(x)),  
   1.145 -               \<lambda>i x. is_nth(**Lset(i), f(x), g(x), h(x))]"
   1.146 +               \<lambda>i x. is_nth(##Lset(i), f(x), g(x), h(x))]"
   1.147  apply (simp only: is_nth_def)
   1.148  apply (intro FOL_reflections is_iterates_reflection
   1.149               hd_reflection tl_reflection) 
   1.150 @@ -338,10 +338,10 @@
   1.151   "REFLECTS
   1.152     [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
   1.153           is_wfrec(L, iterates_MH(L, is_tl(L), z), memsn, u, y)),
   1.154 -    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
   1.155 -         is_wfrec(**Lset(i),
   1.156 -                  iterates_MH(**Lset(i),
   1.157 -                          is_tl(**Lset(i)), z), memsn, u, y))]"
   1.158 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
   1.159 +         is_wfrec(##Lset(i),
   1.160 +                  iterates_MH(##Lset(i),
   1.161 +                          is_tl(##Lset(i)), z), memsn, u, y))]"
   1.162  by (intro FOL_reflections function_reflections is_wfrec_reflection
   1.163            iterates_MH_reflection tl_reflection)
   1.164  
   1.165 @@ -395,9 +395,9 @@
   1.166   "REFLECTS
   1.167     [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
   1.168           is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
   1.169 -    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) &
   1.170 -         is_wfrec(**Lset(i),
   1.171 -                  iterates_MH(**Lset(i), big_union(**Lset(i)), A),
   1.172 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) &
   1.173 +         is_wfrec(##Lset(i),
   1.174 +                  iterates_MH(##Lset(i), big_union(##Lset(i)), A),
   1.175                    memsn, u, y))]"
   1.176  by (intro FOL_reflections function_reflections is_wfrec_reflection
   1.177            iterates_MH_reflection)
   1.178 @@ -419,7 +419,7 @@
   1.179     [\<lambda>x. \<exists>u[L]. u \<in> B & u \<in> nat &
   1.180                  is_iterates(L, big_union(L), A, u, x),
   1.181      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & u \<in> nat &
   1.182 -               is_iterates(**Lset(i), big_union(**Lset(i)), A, u, x)]"
   1.183 +               is_iterates(##Lset(i), big_union(##Lset(i)), A, u, x)]"
   1.184  by (intro FOL_reflections function_reflections is_iterates_reflection)
   1.185  
   1.186  lemma eclose_replacement2: