better satisfies rules for is_recfun
authorpaulson
Thu Aug 01 18:22:46 2002 +0200 (2002-08-01)
changeset 13441d6d620639243
parent 13440 cdde97e1db1c
child 13442 70479ec9f44f
better satisfies rules for is_recfun
A satisfies rule for is_wfrec!
src/ZF/Constructible/Rec_Separation.thy
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 31 18:30:25 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Aug 01 18:22:46 2002 +0200
     1.3 @@ -237,63 +237,69 @@
     1.4  
     1.5  subsection{*Well-Founded Recursion!*}
     1.6  
     1.7 +
     1.8 +text{*Alternative definition, minimizing nesting of quantifiers around MH*}
     1.9 +lemma M_is_recfun_iff:
    1.10 +   "M_is_recfun(M,MH,r,a,f) <->
    1.11 +    (\<forall>z[M]. z \<in> f <-> 
    1.12 +     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M]. 
    1.13 +             MH(x, f_r_sx, y) & pair(M,x,y,z) &
    1.14 +             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. 
    1.15 +                pair(M,x,a,xa) & upair(M,x,x,sx) &
    1.16 +               pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
    1.17 +               xa \<in> r)))"
    1.18 +apply (simp add: M_is_recfun_def)
    1.19 +apply (rule rall_cong, blast) 
    1.20 +done
    1.21 +
    1.22 +
    1.23  (* M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    1.24     "M_is_recfun(M,MH,r,a,f) ==
    1.25       \<forall>z[M]. z \<in> f <->
    1.26 -            5      4       3       2       1           0
    1.27 -            (\<exists>x[M]. \<exists>y[M]. \<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. \<exists>f_r_sx[M].
    1.28 -               pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
    1.29 +               2      1           0
    1.30 +new def     (\<exists>x[M]. \<exists>f_r_sx[M]. \<exists>y[M]. 
    1.31 +             MH(x, f_r_sx, y) & pair(M,x,y,z) &
    1.32 +             (\<exists>xa[M]. \<exists>sx[M]. \<exists>r_sx[M]. 
    1.33 +                pair(M,x,a,xa) & upair(M,x,x,sx) &
    1.34                 pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
    1.35 -               xa \<in> r & MH(x, f_r_sx, y))"
    1.36 +               xa \<in> r)"
    1.37  *)
    1.38  
    1.39 -text{*The three arguments of @{term p} are always 5, 0, 4.*}
    1.40 +text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
    1.41  constdefs is_recfun_fm :: "[i, i, i, i]=>i"
    1.42   "is_recfun_fm(p,r,a,f) == 
    1.43     Forall(Iff(Member(0,succ(f)),
    1.44 -    Exists(Exists(Exists(Exists(Exists(Exists(
    1.45 -     And(pair_fm(5,4,6),
    1.46 -      And(pair_fm(5,a#+7,3),
    1.47 -       And(upair_fm(5,5,2),
    1.48 -        And(pre_image_fm(r#+7,2,1),
    1.49 -         And(restriction_fm(f#+7,1,0),
    1.50 -          And(Member(3,r#+7), p))))))))))))))"
    1.51 -
    1.52 +    Exists(Exists(Exists(
    1.53 +     And(p, 
    1.54 +      And(pair_fm(2,0,3),
    1.55 +       Exists(Exists(Exists(
    1.56 +	And(pair_fm(5,a#+7,2),
    1.57 +	 And(upair_fm(5,5,1),
    1.58 +	  And(pre_image_fm(r#+7,1,0),
    1.59 +	   And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"
    1.60  
    1.61  lemma is_recfun_type [TC]:
    1.62       "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
    1.63        ==> is_recfun_fm(p,x,y,z) \<in> formula"
    1.64  by (simp add: is_recfun_fm_def)
    1.65  
    1.66 +
    1.67  lemma sats_is_recfun_fm:
    1.68    assumes MH_iff_sats: 
    1.69 -      "!!a0 a1 a2 a3 a4 a5 a6. 
    1.70 -        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A|] ==> 
    1.71 -        MH(a5, a0, a4) <-> 
    1.72 -       sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))"
    1.73 +      "!!a0 a1 a2 a3. 
    1.74 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|] 
    1.75 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
    1.76    shows 
    1.77        "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.78         ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
    1.79             M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
    1.80 -by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
    1.81 -(*
    1.82 -apply (rule ball_cong bex_cong iff_cong conj_cong refl iff_refl) +
    1.83 - sats(A, p,
    1.84 -   Cons(xf, Cons(xe, Cons(xd, Cons(xc, Cons(xb, Cons(xaa, Cons(xa, env)))))))) 
    1.85 -\<longleftrightarrow> MH(xaa, xf, xb)
    1.86 -
    1.87 -MH(nth(5,env), nth(0,env), nth(4,env)) <-> sats(A, p, env);
    1.88 -*)
    1.89 -
    1.90 -(*      "!!x y z. [|x\<in>A; y\<in>A; z\<in>A|] ==> MH(x,y,z) <-> sats(A, p, env)"
    1.91 -*)
    1.92 +by (simp add: is_recfun_fm_def M_is_recfun_iff MH_iff_sats [THEN iff_sym])
    1.93  
    1.94  lemma is_recfun_iff_sats:
    1.95    assumes MH_iff_sats: 
    1.96 -      "!!a0 a1 a2 a3 a4 a5 a6. 
    1.97 -        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A|] ==> 
    1.98 -        MH(a5, a0, a4) <-> 
    1.99 -       sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))"
   1.100 +      "!!a0 a1 a2 a3. 
   1.101 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A|] 
   1.102 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,env)))))"
   1.103    shows
   1.104    "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.105        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   1.106 @@ -320,9 +326,56 @@
   1.107               restriction_reflection MH_reflection)
   1.108  done
   1.109  
   1.110 -text{*Currently, @{text sats}-theorems for higher-order operators don't seem
   1.111 -useful.  Reflection theorems do work, though.  This one avoids the repetition
   1.112 -of the @{text MH}-term. *}
   1.113 +subsubsection{*The Operator @{term is_wfrec}*}
   1.114 +
   1.115 +text{*The three arguments of @{term p} are always 2, 1, 0*}
   1.116 +
   1.117 +(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
   1.118 +    "is_wfrec(M,MH,r,a,z) == 
   1.119 +      \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
   1.120 +constdefs is_wfrec_fm :: "[i, i, i, i]=>i"
   1.121 + "is_wfrec_fm(p,r,a,z) == 
   1.122 +    Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
   1.123 +           Exists(Exists(Exists(Exists(
   1.124 +             And(Equal(2,a#+5), And(Equal(1,4), And(Equal(0,z#+5), p)))))))))"
   1.125 +
   1.126 +text{*We call @{term p} with arguments a, f, z by equating them with 
   1.127 +  the corresponding quantified variables with de Bruijn indices 2, 1, 0.*}
   1.128 +
   1.129 +text{*There's an additional existential quantifier to ensure that the
   1.130 +      environments in both calls to MH have the same length.*}
   1.131 +
   1.132 +lemma is_wfrec_type [TC]:
   1.133 +     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.134 +      ==> is_wfrec_fm(p,x,y,z) \<in> formula"
   1.135 +by (simp add: is_wfrec_fm_def) 
   1.136 +
   1.137 +lemma sats_is_wfrec_fm:
   1.138 +  assumes MH_iff_sats: 
   1.139 +      "!!a0 a1 a2 a3 a4. 
   1.140 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|] 
   1.141 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
   1.142 +  shows 
   1.143 +      "[|x \<in> nat; y < length(env); z < length(env); env \<in> list(A)|]
   1.144 +       ==> sats(A, is_wfrec_fm(p,x,y,z), env) <-> 
   1.145 +           is_wfrec(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
   1.146 +apply (frule_tac x=z in lt_length_in_nat, assumption)  
   1.147 +apply (frule lt_length_in_nat, assumption)  
   1.148 +apply (simp add: is_wfrec_fm_def sats_is_recfun_fm is_wfrec_def MH_iff_sats [THEN iff_sym], blast) 
   1.149 +done
   1.150 +
   1.151 +
   1.152 +lemma is_wfrec_iff_sats:
   1.153 +  assumes MH_iff_sats: 
   1.154 +      "!!a0 a1 a2 a3 a4. 
   1.155 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A|] 
   1.156 +        ==> MH(a2, a1, a0) <-> sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,env))))))"
   1.157 +  shows
   1.158 +  "[|nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.159 +      i \<in> nat; j < length(env); k < length(env); env \<in> list(A)|]
   1.160 +   ==> is_wfrec(**A, MH, x, y, z) <-> sats(A, is_wfrec_fm(p,i,j,k), env)" 
   1.161 +by (simp add: sats_is_wfrec_fm [OF MH_iff_sats])
   1.162 +
   1.163  theorem is_wfrec_reflection:
   1.164    assumes MH_reflection:
   1.165      "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
   1.166 @@ -360,6 +413,7 @@
   1.167  apply (rename_tac u)
   1.168  apply (rule ball_iff_sats imp_iff_sats)+
   1.169  apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
   1.170 +apply (rule sep_rules | simp)+
   1.171  apply (rule sep_rules is_recfun_iff_sats | simp)+
   1.172  done
   1.173  
   1.174 @@ -401,7 +455,7 @@
   1.175  apply (rename_tac u)
   1.176  apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
   1.177  apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats)
   1.178 -apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
   1.179 +apply (rule sep_rules list.intros app_type tran_closure_iff_sats is_recfun_iff_sats | simp)+
   1.180  done
   1.181  
   1.182  
   1.183 @@ -710,8 +764,7 @@
   1.184         sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   1.185  apply (rule iff_sym) 
   1.186  apply (rule iff_trans)
   1.187 -apply (rule sats_iterates_MH_fm [of A is_F], blast)  
   1.188 -apply simp_all 
   1.189 +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) 
   1.190  done
   1.191  (*FIXME: surely proof can be improved?*)
   1.192  
   1.193 @@ -790,6 +843,7 @@
   1.194  by (intro FOL_reflections function_reflections is_wfrec_reflection
   1.195            iterates_MH_reflection list_functor_reflection)
   1.196  
   1.197 +
   1.198  lemma list_replacement1:
   1.199     "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)"
   1.200  apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
   1.201 @@ -809,12 +863,11 @@
   1.202  apply (rename_tac v)
   1.203  apply (rule bex_iff_sats conj_iff_sats)+
   1.204  apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   1.205 -apply (rule sep_rules | simp)+
   1.206 -apply (simp add: is_wfrec_def)
   1.207  apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
   1.208 -            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.209 +            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.210  done
   1.211  
   1.212 +
   1.213  lemma list_replacement2_Reflects:
   1.214   "REFLECTS
   1.215     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
   1.216 @@ -852,10 +905,8 @@
   1.217  apply (rename_tac v)
   1.218  apply (rule bex_iff_sats conj_iff_sats)+
   1.219  apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
   1.220 -apply (rule sep_rules | simp)+
   1.221 -apply (simp add: is_wfrec_def)
   1.222  apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
   1.223 -            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.224 +            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.225  done
   1.226  
   1.227  
   1.228 @@ -934,10 +985,8 @@
   1.229  apply (rename_tac v)
   1.230  apply (rule bex_iff_sats conj_iff_sats)+
   1.231  apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   1.232 -apply (rule sep_rules | simp)+
   1.233 -apply (simp add: is_wfrec_def)
   1.234  apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
   1.235 -            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.236 +            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.237  done
   1.238  
   1.239  lemma formula_replacement2_Reflects:
   1.240 @@ -977,10 +1026,8 @@
   1.241  apply (rename_tac v)
   1.242  apply (rule bex_iff_sats conj_iff_sats)+
   1.243  apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
   1.244 -apply (rule sep_rules | simp)+
   1.245 -apply (simp add: is_wfrec_def)
   1.246  apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
   1.247 -            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.248 +            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.249  done
   1.250  
   1.251  text{*NB The proofs for type @{term formula} are virtually identical to those
   1.252 @@ -1239,8 +1286,7 @@
   1.253        REFLECTS[\<lambda>x. is_bool_of_o(L, P(L,x), f(x)),  
   1.254                 \<lambda>i x. is_bool_of_o(**Lset(i), P(**Lset(i),x), f(x))]"
   1.255  apply (simp (no_asm) only: is_bool_of_o_def setclass_simps)
   1.256 -apply (intro FOL_reflections function_reflections) 
   1.257 -apply assumption+
   1.258 +apply (intro FOL_reflections function_reflections, assumption+)
   1.259  done
   1.260  
   1.261  
   1.262 @@ -1274,10 +1320,8 @@
   1.263  apply (rename_tac v)
   1.264  apply (rule bex_iff_sats conj_iff_sats)+
   1.265  apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
   1.266 -apply (rule sep_rules | simp)+
   1.267 -apply (simp add: is_wfrec_def)
   1.268  apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
   1.269 -            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.270 +            is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.271  done
   1.272  
   1.273  
   1.274 @@ -1295,7 +1339,7 @@
   1.275  theorem M_datatypes_L: "PROP M_datatypes(L)"
   1.276    apply (rule M_datatypes.intro)
   1.277        apply (rule M_wfrank.axioms [OF M_wfrank_L])+
   1.278 - apply (rule M_datatypes_axioms_L); 
   1.279 + apply (rule M_datatypes_axioms_L) 
   1.280   done
   1.281  
   1.282  lemmas list_closed = M_datatypes.list_closed [OF M_datatypes_L]
   1.283 @@ -1344,10 +1388,8 @@
   1.284  apply (rename_tac v)
   1.285  apply (rule bex_iff_sats conj_iff_sats)+
   1.286  apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   1.287 -apply (rule sep_rules | simp)+
   1.288 -apply (simp add: is_wfrec_def)
   1.289  apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
   1.290 -             is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.291 +             is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.292  done
   1.293  
   1.294  
   1.295 @@ -1387,10 +1429,8 @@
   1.296  apply (rename_tac v)
   1.297  apply (rule bex_iff_sats conj_iff_sats)+
   1.298  apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   1.299 -apply (rule sep_rules | simp)+
   1.300 -apply (simp add: is_wfrec_def)
   1.301  apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
   1.302 -              is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.303 +              is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.304  done
   1.305  
   1.306