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