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