src/ZF/Constructible/Rec_Separation.thy
 author paulson Fri Jul 12 11:24:40 2002 +0200 (2002-07-12) changeset 13352 3cd767f8d78b parent 13348 374d05460db4 child 13363 c26eeb000470 permissions -rw-r--r--
new definitions of fun_apply and M_is_recfun
```     1 header{*Separation for the Absoluteness of Recursion*}
```
```     2
```
```     3 theory Rec_Separation = Separation:
```
```     4
```
```     5 text{*This theory proves all instances needed for locales @{text
```
```     6 "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*}
```
```     7
```
```     8 subsection{*The Locale @{text "M_trancl"}*}
```
```     9
```
```    10 subsubsection{*Separation for Reflexive/Transitive Closure*}
```
```    11
```
```    12 text{*First, The Defining Formula*}
```
```    13
```
```    14 (* "rtran_closure_mem(M,A,r,p) ==
```
```    15       \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
```
```    16        omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
```
```    17        (\<exists>f[M]. typed_function(M,n',A,f) &
```
```    18 	(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
```
```    19 	  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
```
```    20 	(\<forall>j[M]. j\<in>n -->
```
```    21 	  (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
```
```    22 	    fun_apply(M,f,j,fj) & successor(M,j,sj) &
```
```    23 	    fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
```
```    24 constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
```
```    25  "rtran_closure_mem_fm(A,r,p) ==
```
```    26    Exists(Exists(Exists(
```
```    27     And(omega_fm(2),
```
```    28      And(Member(1,2),
```
```    29       And(succ_fm(1,0),
```
```    30        Exists(And(typed_function_fm(1, A#+4, 0),
```
```    31 	And(Exists(Exists(Exists(
```
```    32 	      And(pair_fm(2,1,p#+7),
```
```    33 	       And(empty_fm(0),
```
```    34 		And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
```
```    35 	    Forall(Implies(Member(0,3),
```
```    36 	     Exists(Exists(Exists(Exists(
```
```    37 	      And(fun_apply_fm(5,4,3),
```
```    38 	       And(succ_fm(4,2),
```
```    39 		And(fun_apply_fm(5,2,1),
```
```    40 		 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
```
```    41
```
```    42
```
```    43 lemma rtran_closure_mem_type [TC]:
```
```    44  "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
```
```    45 by (simp add: rtran_closure_mem_fm_def)
```
```    46
```
```    47 lemma arity_rtran_closure_mem_fm [simp]:
```
```    48      "[| x \<in> nat; y \<in> nat; z \<in> nat |]
```
```    49       ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
```
```    50 by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
```
```    51
```
```    52 lemma sats_rtran_closure_mem_fm [simp]:
```
```    53    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
```
```    54     ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
```
```    55         rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
```
```    56 by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def)
```
```    57
```
```    58 lemma rtran_closure_mem_iff_sats:
```
```    59       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
```
```    60           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
```
```    61        ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
```
```    62 by (simp add: sats_rtran_closure_mem_fm)
```
```    63
```
```    64 theorem rtran_closure_mem_reflection:
```
```    65      "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
```
```    66                \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
```
```    67 apply (simp only: rtran_closure_mem_def setclass_simps)
```
```    68 apply (intro FOL_reflections function_reflections fun_plus_reflections)
```
```    69 done
```
```    70
```
```    71 text{*Separation for @{term "rtrancl(r)"}.*}
```
```    72 lemma rtrancl_separation:
```
```    73      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
```
```    74 apply (rule separation_CollectI)
```
```    75 apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
```
```    76 apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
```
```    77 apply (drule subset_Lset_ltD, assumption)
```
```    78 apply (erule reflection_imp_L_separation)
```
```    79   apply (simp_all add: lt_Ord2)
```
```    80 apply (rule DPowI2)
```
```    81 apply (rename_tac u)
```
```    82 apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
```
```    83 apply (rule sep_rules | simp)+
```
```    84 apply (simp_all add: succ_Un_distrib [symmetric])
```
```    85 done
```
```    86
```
```    87
```
```    88 subsubsection{*Reflexive/Transitive Closure, Internalized*}
```
```    89
```
```    90 (*  "rtran_closure(M,r,s) ==
```
```    91         \<forall>A[M]. is_field(M,r,A) -->
```
```    92  	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
```
```    93 constdefs rtran_closure_fm :: "[i,i]=>i"
```
```    94  "rtran_closure_fm(r,s) ==
```
```    95    Forall(Implies(field_fm(succ(r),0),
```
```    96                   Forall(Iff(Member(0,succ(succ(s))),
```
```    97                              rtran_closure_mem_fm(1,succ(succ(r)),0)))))"
```
```    98
```
```    99 lemma rtran_closure_type [TC]:
```
```   100      "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula"
```
```   101 by (simp add: rtran_closure_fm_def)
```
```   102
```
```   103 lemma arity_rtran_closure_fm [simp]:
```
```   104      "[| x \<in> nat; y \<in> nat |]
```
```   105       ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
```
```   106 by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
```
```   107
```
```   108 lemma sats_rtran_closure_fm [simp]:
```
```   109    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
```
```   110     ==> sats(A, rtran_closure_fm(x,y), env) <->
```
```   111         rtran_closure(**A, nth(x,env), nth(y,env))"
```
```   112 by (simp add: rtran_closure_fm_def rtran_closure_def)
```
```   113
```
```   114 lemma rtran_closure_iff_sats:
```
```   115       "[| nth(i,env) = x; nth(j,env) = y;
```
```   116           i \<in> nat; j \<in> nat; env \<in> list(A)|]
```
```   117        ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)"
```
```   118 by simp
```
```   119
```
```   120 theorem rtran_closure_reflection:
```
```   121      "REFLECTS[\<lambda>x. rtran_closure(L,f(x),g(x)),
```
```   122                \<lambda>i x. rtran_closure(**Lset(i),f(x),g(x))]"
```
```   123 apply (simp only: rtran_closure_def setclass_simps)
```
```   124 apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
```
```   125 done
```
```   126
```
```   127
```
```   128 subsubsection{*Transitive Closure of a Relation, Internalized*}
```
```   129
```
```   130 (*  "tran_closure(M,r,t) ==
```
```   131          \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
```
```   132 constdefs tran_closure_fm :: "[i,i]=>i"
```
```   133  "tran_closure_fm(r,s) ==
```
```   134    Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
```
```   135
```
```   136 lemma tran_closure_type [TC]:
```
```   137      "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula"
```
```   138 by (simp add: tran_closure_fm_def)
```
```   139
```
```   140 lemma arity_tran_closure_fm [simp]:
```
```   141      "[| x \<in> nat; y \<in> nat |]
```
```   142       ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)"
```
```   143 by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac)
```
```   144
```
```   145 lemma sats_tran_closure_fm [simp]:
```
```   146    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
```
```   147     ==> sats(A, tran_closure_fm(x,y), env) <->
```
```   148         tran_closure(**A, nth(x,env), nth(y,env))"
```
```   149 by (simp add: tran_closure_fm_def tran_closure_def)
```
```   150
```
```   151 lemma tran_closure_iff_sats:
```
```   152       "[| nth(i,env) = x; nth(j,env) = y;
```
```   153           i \<in> nat; j \<in> nat; env \<in> list(A)|]
```
```   154        ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)"
```
```   155 by simp
```
```   156
```
```   157 theorem tran_closure_reflection:
```
```   158      "REFLECTS[\<lambda>x. tran_closure(L,f(x),g(x)),
```
```   159                \<lambda>i x. tran_closure(**Lset(i),f(x),g(x))]"
```
```   160 apply (simp only: tran_closure_def setclass_simps)
```
```   161 apply (intro FOL_reflections function_reflections
```
```   162              rtran_closure_reflection composition_reflection)
```
```   163 done
```
```   164
```
```   165
```
```   166 subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
```
```   167
```
```   168 lemma wellfounded_trancl_reflects:
```
```   169   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
```
```   170 	         w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
```
```   171    \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).
```
```   172        w \<in> Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) &
```
```   173        wx \<in> rp]"
```
```   174 by (intro FOL_reflections function_reflections fun_plus_reflections
```
```   175           tran_closure_reflection)
```
```   176
```
```   177
```
```   178 lemma wellfounded_trancl_separation:
```
```   179 	 "[| L(r); L(Z) |] ==>
```
```   180 	  separation (L, \<lambda>x.
```
```   181 	      \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
```
```   182 	       w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
```
```   183 apply (rule separation_CollectI)
```
```   184 apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast )
```
```   185 apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
```
```   186 apply (drule subset_Lset_ltD, assumption)
```
```   187 apply (erule reflection_imp_L_separation)
```
```   188   apply (simp_all add: lt_Ord2)
```
```   189 apply (rule DPowI2)
```
```   190 apply (rename_tac u)
```
```   191 apply (rule bex_iff_sats conj_iff_sats)+
```
```   192 apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats)
```
```   193 apply (rule sep_rules tran_closure_iff_sats | simp)+
```
```   194 apply (simp_all add: succ_Un_distrib [symmetric])
```
```   195 done
```
```   196
```
```   197 subsection{*Well-Founded Recursion!*}
```
```   198
```
```   199 (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
```
```   200    "M_is_recfun(M,MH,r,a,f) ==
```
```   201      \<forall>z[M]. z \<in> f <->
```
```   202             5      4       3       2       1           0
```
```   203             (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
```
```   204 	       pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
```
```   205                pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
```
```   206                xa \<in> r & MH(x, f_r_sx, y))"
```
```   207 *)
```
```   208
```
```   209 constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i"
```
```   210  "is_recfun_fm(p,r,a,f) ==
```
```   211    Forall(Iff(Member(0,succ(f)),
```
```   212     Exists(Exists(Exists(Exists(Exists(Exists(
```
```   213      And(pair_fm(5,4,6),
```
```   214       And(pair_fm(5,a#+7,3),
```
```   215        And(upair_fm(5,5,2),
```
```   216         And(pre_image_fm(r#+7,2,1),
```
```   217          And(restriction_fm(f#+7,1,0),
```
```   218           And(Member(3,r#+7), p(5,0,4)))))))))))))))"
```
```   219
```
```   220
```
```   221 lemma is_recfun_type_0:
```
```   222      "[| !!x y z. [| x \<in> nat; y \<in> nat; z \<in> nat |] ==> p(x,y,z) \<in> formula;
```
```   223          x \<in> nat; y \<in> nat; z \<in> nat |]
```
```   224       ==> is_recfun_fm(p,x,y,z) \<in> formula"
```
```   225 apply (unfold is_recfun_fm_def)
```
```   226 (*FIXME: FIND OUT why simp loops!*)
```
```   227 apply typecheck
```
```   228 by simp
```
```   229
```
```   230 lemma is_recfun_type [TC]:
```
```   231      "[| p(5,0,4) \<in> formula;
```
```   232          x \<in> nat; y \<in> nat; z \<in> nat |]
```
```   233       ==> is_recfun_fm(p,x,y,z) \<in> formula"
```
```   234 by (simp add: is_recfun_fm_def)
```
```   235
```
```   236 lemma arity_is_recfun_fm [simp]:
```
```   237      "[| arity(p(5,0,4)) le 8; x \<in> nat; y \<in> nat; z \<in> nat |]
```
```   238       ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
```
```   239 apply (frule lt_nat_in_nat, simp)
```
```   240 apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] )
```
```   241 apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1])
```
```   242 apply (rule le_imp_subset)
```
```   243 apply (erule le_trans, simp)
```
```   244 apply (simp add: succ_Un_distrib [symmetric] Un_ac)
```
```   245 done
```
```   246
```
```   247 lemma sats_is_recfun_fm:
```
```   248   assumes MH_iff_sats:
```
```   249       "!!x y z env.
```
```   250 	 [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
```
```   251 	 ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)"
```
```   252   shows
```
```   253       "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
```
```   254        ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
```
```   255            M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
```
```   256 by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
```
```   257
```
```   258 lemma is_recfun_iff_sats:
```
```   259   "[| (!!x y z env. [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
```
```   260                     ==> MH(nth(x,env), nth(y,env), nth(z,env)) <->
```
```   261                         sats(A, p(x,y,z), env));
```
```   262       nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
```
```   263       i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
```
```   264    ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
```
```   265 by (simp add: sats_is_recfun_fm [of A MH])
```
```   266
```
```   267 theorem is_recfun_reflection:
```
```   268   assumes MH_reflection:
```
```   269     "!!f g h. REFLECTS[\<lambda>x. MH(L, f(x), g(x), h(x)),
```
```   270                      \<lambda>i x. MH(**Lset(i), f(x), g(x), h(x))]"
```
```   271   shows "REFLECTS[\<lambda>x. M_is_recfun(L, MH(L), f(x), g(x), h(x)),
```
```   272                \<lambda>i x. M_is_recfun(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]"
```
```   273 apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps)
```
```   274 apply (intro FOL_reflections function_reflections
```
```   275              restriction_reflection MH_reflection)
```
```   276 done
```
```   277
```
```   278 subsection{*Separation for  @{term "wfrank"}*}
```
```   279
```
```   280 lemma wfrank_Reflects:
```
```   281  "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   282               ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)),
```
```   283       \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
```
```   284          ~ (\<exists>f \<in> Lset(i).
```
```   285             M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y),
```
```   286                         rplus, x, f))]"
```
```   287 by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection)
```
```   288
```
```   289 lemma wfrank_separation:
```
```   290      "L(r) ==>
```
```   291       separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   292          ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
```
```   293 apply (rule separation_CollectI)
```
```   294 apply (rule_tac A="{r,z}" in subset_LsetE, blast )
```
```   295 apply (rule ReflectsE [OF wfrank_Reflects], assumption)
```
```   296 apply (drule subset_Lset_ltD, assumption)
```
```   297 apply (erule reflection_imp_L_separation)
```
```   298   apply (simp_all add: lt_Ord2, clarify)
```
```   299 apply (rule DPowI2)
```
```   300 apply (rename_tac u)
```
```   301 apply (rule ball_iff_sats imp_iff_sats)+
```
```   302 apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
```
```   303 apply (rule sep_rules is_recfun_iff_sats | simp)+
```
```   304 apply (simp_all add: succ_Un_distrib [symmetric])
```
```   305 done
```
```   306
```
```   307
```
```   308 subsection{*Replacement for @{term "wfrank"}*}
```
```   309
```
```   310 lemma wfrank_replacement_Reflects:
```
```   311  "REFLECTS[\<lambda>z. \<exists>x[L]. x \<in> A &
```
```   312         (\<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   313          (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
```
```   314                         M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
```
```   315                         is_range(L,f,y))),
```
```   316  \<lambda>i z. \<exists>x \<in> Lset(i). x \<in> A &
```
```   317       (\<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
```
```   318        (\<exists>y \<in> Lset(i). \<exists>f \<in> Lset(i). pair(**Lset(i),x,y,z)  &
```
```   319          M_is_recfun(**Lset(i), %x f y. is_range(**Lset(i),f,y), rplus, x, f) &
```
```   320          is_range(**Lset(i),f,y)))]"
```
```   321 by (intro FOL_reflections function_reflections fun_plus_reflections
```
```   322              is_recfun_reflection tran_closure_reflection)
```
```   323
```
```   324
```
```   325 lemma wfrank_strong_replacement:
```
```   326      "L(r) ==>
```
```   327       strong_replacement(L, \<lambda>x z.
```
```   328          \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   329          (\<exists>y[L]. \<exists>f[L]. pair(L,x,y,z)  &
```
```   330                         M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) &
```
```   331                         is_range(L,f,y)))"
```
```   332 apply (rule strong_replacementI)
```
```   333 apply (rule rallI)
```
```   334 apply (rename_tac B)
```
```   335 apply (rule separation_CollectI)
```
```   336 apply (rule_tac A="{B,r,z}" in subset_LsetE, blast )
```
```   337 apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
```
```   338 apply (drule subset_Lset_ltD, assumption)
```
```   339 apply (erule reflection_imp_L_separation)
```
```   340   apply (simp_all add: lt_Ord2)
```
```   341 apply (rule DPowI2)
```
```   342 apply (rename_tac u)
```
```   343 apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
```
```   344 apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
```
```   345 apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
```
```   346 apply (simp_all add: succ_Un_distrib [symmetric])
```
```   347 done
```
```   348
```
```   349
```
```   350 subsection{*Separation for  @{term "wfrank"}*}
```
```   351
```
```   352 lemma Ord_wfrank_Reflects:
```
```   353  "REFLECTS[\<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   354           ~ (\<forall>f[L]. \<forall>rangef[L].
```
```   355              is_range(L,f,rangef) -->
```
```   356              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
```
```   357              ordinal(L,rangef)),
```
```   358       \<lambda>i x. \<forall>rplus \<in> Lset(i). tran_closure(**Lset(i),r,rplus) -->
```
```   359           ~ (\<forall>f \<in> Lset(i). \<forall>rangef \<in> Lset(i).
```
```   360              is_range(**Lset(i),f,rangef) -->
```
```   361              M_is_recfun(**Lset(i), \<lambda>x f y. is_range(**Lset(i),f,y),
```
```   362                          rplus, x, f) -->
```
```   363              ordinal(**Lset(i),rangef))]"
```
```   364 by (intro FOL_reflections function_reflections is_recfun_reflection
```
```   365           tran_closure_reflection ordinal_reflection)
```
```   366
```
```   367 lemma  Ord_wfrank_separation:
```
```   368      "L(r) ==>
```
```   369       separation (L, \<lambda>x.
```
```   370          \<forall>rplus[L]. tran_closure(L,r,rplus) -->
```
```   371           ~ (\<forall>f[L]. \<forall>rangef[L].
```
```   372              is_range(L,f,rangef) -->
```
```   373              M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
```
```   374              ordinal(L,rangef)))"
```
```   375 apply (rule separation_CollectI)
```
```   376 apply (rule_tac A="{r,z}" in subset_LsetE, blast )
```
```   377 apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
```
```   378 apply (drule subset_Lset_ltD, assumption)
```
```   379 apply (erule reflection_imp_L_separation)
```
```   380   apply (simp_all add: lt_Ord2, clarify)
```
```   381 apply (rule DPowI2)
```
```   382 apply (rename_tac u)
```
```   383 apply (rule ball_iff_sats imp_iff_sats)+
```
```   384 apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
```
```   385 apply (rule sep_rules is_recfun_iff_sats | simp)+
```
```   386 apply (simp_all add: succ_Un_distrib [symmetric])
```
```   387 done
```
```   388
```
```   389
```
```   390 end
```