src/ZF/Constructible/Rec_Separation.thy
changeset 13434 78b93a667c01
parent 13429 2232810416fc
child 13437 01b3fc0cc1b8
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 30 11:38:33 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 30 11:39:57 2002 +0200
     1.3 @@ -239,8 +239,9 @@
     1.4                 xa \<in> r & MH(x, f_r_sx, y))"
     1.5  *)
     1.6  
     1.7 -constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i"
     1.8 - "is_recfun_fm(p,r,a,f) ==
     1.9 +text{*The three arguments of @{term p} are always 5, 0, 4.*}
    1.10 +constdefs is_recfun_fm :: "[i, i, i, i]=>i"
    1.11 + "is_recfun_fm(p,r,a,f) == 
    1.12     Forall(Iff(Member(0,succ(f)),
    1.13      Exists(Exists(Exists(Exists(Exists(Exists(
    1.14       And(pair_fm(5,4,6),
    1.15 @@ -248,54 +249,54 @@
    1.16         And(upair_fm(5,5,2),
    1.17          And(pre_image_fm(r#+7,2,1),
    1.18           And(restriction_fm(f#+7,1,0),
    1.19 -          And(Member(3,r#+7), p(5,0,4)))))))))))))))"
    1.20 +          And(Member(3,r#+7), p))))))))))))))"
    1.21  
    1.22  
    1.23 -lemma is_recfun_type_0:
    1.24 -     "[| !!x y z. [| x \<in> nat; y \<in> nat; z \<in> nat |] ==> p(x,y,z) \<in> formula;
    1.25 -         x \<in> nat; y \<in> nat; z \<in> nat |]
    1.26 -      ==> is_recfun_fm(p,x,y,z) \<in> formula"
    1.27 -apply (unfold is_recfun_fm_def)
    1.28 -(*FIXME: FIND OUT why simp loops!*)
    1.29 -apply typecheck
    1.30 -by simp
    1.31 -
    1.32  lemma is_recfun_type [TC]:
    1.33 -     "[| p(5,0,4) \<in> formula;
    1.34 -         x \<in> nat; y \<in> nat; z \<in> nat |]
    1.35 +     "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
    1.36        ==> is_recfun_fm(p,x,y,z) \<in> formula"
    1.37  by (simp add: is_recfun_fm_def)
    1.38  
    1.39 -lemma arity_is_recfun_fm [simp]:
    1.40 -     "[| arity(p(5,0,4)) le 8; x \<in> nat; y \<in> nat; z \<in> nat |]
    1.41 -      ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
    1.42 -apply (frule lt_nat_in_nat, simp)
    1.43 -apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] )
    1.44 -apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1])
    1.45 -apply (rule le_imp_subset)
    1.46 -apply (erule le_trans, simp)
    1.47 -apply (simp add: succ_Un_distrib [symmetric] Un_ac)
    1.48 -done
    1.49 -
    1.50  lemma sats_is_recfun_fm:
    1.51 -  assumes MH_iff_sats:
    1.52 -      "!!x y z env.
    1.53 -         [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.54 -         ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)"
    1.55 -  shows
    1.56 +  assumes MH_iff_sats: 
    1.57 +      "!!a0 a1 a2 a3 a4 a5 a6. 
    1.58 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A|] ==> 
    1.59 +        MH(a5, a0, a4) <-> 
    1.60 +       sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))"
    1.61 +  shows 
    1.62        "[|x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.63         ==> sats(A, is_recfun_fm(p,x,y,z), env) <->
    1.64             M_is_recfun(**A, MH, nth(x,env), nth(y,env), nth(z,env))"
    1.65  by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym])
    1.66 +(*
    1.67 +apply (rule ball_cong bex_cong iff_cong conj_cong refl iff_refl) +
    1.68 + sats(A, p,
    1.69 +   Cons(xf, Cons(xe, Cons(xd, Cons(xc, Cons(xb, Cons(xaa, Cons(xa, env)))))))) 
    1.70 +\<longleftrightarrow> MH(xaa, xf, xb)
    1.71 +
    1.72 +MH(nth(5,env), nth(0,env), nth(4,env)) <-> sats(A, p, env);
    1.73 +*)
    1.74 +
    1.75 +(*      "!!x y z. [|x\<in>A; y\<in>A; z\<in>A|] ==> MH(x,y,z) <-> sats(A, p, env)"
    1.76 +*)
    1.77  
    1.78  lemma is_recfun_iff_sats:
    1.79 -  "[| (!!x y z env. [| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    1.80 -                    ==> MH(nth(x,env), nth(y,env), nth(z,env)) <->
    1.81 -                        sats(A, p(x,y,z), env));
    1.82 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
    1.83 +  assumes MH_iff_sats: 
    1.84 +      "!!a0 a1 a2 a3 a4 a5 a6. 
    1.85 +        [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A|] ==> 
    1.86 +        MH(a5, a0, a4) <-> 
    1.87 +       sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,Cons(a4,Cons(a5,Cons(a6,env))))))))"
    1.88 +  shows
    1.89 +  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
    1.90        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
    1.91     ==> M_is_recfun(**A, MH, x, y, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)"
    1.92 -by (simp add: sats_is_recfun_fm [of A MH])
    1.93 +apply (rule iff_sym) 
    1.94 +apply (rule iff_trans)
    1.95 +apply (rule sats_is_recfun_fm [of A MH]) 
    1.96 +apply (rule MH_iff_sats, simp_all) 
    1.97 +done
    1.98 +(*FIXME: surely proof can be improved?*)
    1.99 +
   1.100  
   1.101  theorem is_recfun_reflection:
   1.102    assumes MH_reflection:
   1.103 @@ -588,6 +589,9 @@
   1.104  
   1.105  
   1.106  subsubsection{*The Operator @{term is_nat_case}*}
   1.107 +text{*I could not get it to work with the more natural assumption that 
   1.108 + @{term is_b} takes two arguments.  Instead it must be a formula where 1 and 0
   1.109 + stand for @{term m} and @{term b}, respectively.*}
   1.110  
   1.111  (* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o"
   1.112      "is_nat_case(M, a, is_b, k, z) ==
   1.113 @@ -595,36 +599,24 @@
   1.114         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   1.115         (is_quasinat(M,k) | empty(M,z))" *)
   1.116  text{*The formula @{term is_b} has free variables 1 and 0.*}
   1.117 -constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i"
   1.118 - "is_nat_case_fm(a,is_b,k,z) ==
   1.119 +constdefs is_nat_case_fm :: "[i, i, i, i]=>i"
   1.120 + "is_nat_case_fm(a,is_b,k,z) == 
   1.121      And(Implies(empty_fm(k), Equal(z,a)),
   1.122 -        And(Forall(Implies(succ_fm(0,succ(k)),
   1.123 -                   Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))),
   1.124 +        And(Forall(Implies(succ_fm(0,succ(k)), 
   1.125 +                   Forall(Implies(Equal(0,succ(succ(z))), is_b)))),
   1.126              Or(quasinat_fm(k), empty_fm(z))))"
   1.127  
   1.128  lemma is_nat_case_type [TC]:
   1.129 -     "[| is_b(1,0) \<in> formula;
   1.130 -         x \<in> nat; y \<in> nat; z \<in> nat |]
   1.131 +     "[| is_b \<in> formula;  
   1.132 +         x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.133        ==> is_nat_case_fm(x,is_b,y,z) \<in> formula"
   1.134  by (simp add: is_nat_case_fm_def)
   1.135  
   1.136 -lemma arity_is_nat_case_fm [simp]:
   1.137 -     "[| is_b(1,0) \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.138 -      ==> arity(is_nat_case_fm(x,is_b,y,z)) =
   1.139 -          succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(is_b(1,0)) #- 2)"
   1.140 -apply (subgoal_tac "arity(is_b(1,0)) \<in> nat")
   1.141 -apply typecheck
   1.142 -(*FIXME: could nat_diff_split work?*)
   1.143 -apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat
   1.144 -                 succ_Un_distrib [symmetric] Un_ac
   1.145 -                 split: split_nat_case)
   1.146 -done
   1.147 -
   1.148  lemma sats_is_nat_case_fm:
   1.149 -  assumes is_b_iff_sats:
   1.150 -      "!!a b. [| a \<in> A; b \<in> A|]
   1.151 -              ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))"
   1.152 -  shows
   1.153 +  assumes is_b_iff_sats: 
   1.154 +      "!!a. a \<in> A ==> is_b(a,nth(z, env)) <-> 
   1.155 +                      sats(A, p, Cons(nth(z,env), Cons(a, env)))"
   1.156 +  shows 
   1.157        "[|x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   1.158         ==> sats(A, is_nat_case_fm(x,p,y,z), env) <->
   1.159             is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))"
   1.160 @@ -633,9 +625,9 @@
   1.161  done
   1.162  
   1.163  lemma is_nat_case_iff_sats:
   1.164 -  "[| (!!a b. [| a \<in> A; b \<in> A|]
   1.165 -              ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env))));
   1.166 -      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.167 +  "[| (!!a. a \<in> A ==> is_b(a,z) <->
   1.168 +                      sats(A, p, Cons(z, Cons(a,env))));
   1.169 +      nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.170        i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   1.171     ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)"
   1.172  by (simp add: sats_is_nat_case_fm [of A is_b])
   1.173 @@ -663,59 +655,51 @@
   1.174     "iterates_MH(M,isF,v,n,g,z) ==
   1.175          is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   1.176                      n, z)" *)
   1.177 -constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i"
   1.178 - "iterates_MH_fm(isF,v,n,g,z) ==
   1.179 -    is_nat_case_fm(v,
   1.180 -      \<lambda>m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0),
   1.181 -                     Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))),
   1.182 +constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i"
   1.183 + "iterates_MH_fm(isF,v,n,g,z) == 
   1.184 +    is_nat_case_fm(v, 
   1.185 +      Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0), 
   1.186 +                     Forall(Implies(Equal(0,2), isF)))), 
   1.187        n, z)"
   1.188  
   1.189  lemma iterates_MH_type [TC]:
   1.190 -     "[| p(1,0) \<in> formula;
   1.191 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.192 +     "[| p \<in> formula;  
   1.193 +         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |] 
   1.194        ==> iterates_MH_fm(p,v,x,y,z) \<in> formula"
   1.195  by (simp add: iterates_MH_fm_def)
   1.196  
   1.197 -
   1.198 -lemma arity_iterates_MH_fm [simp]:
   1.199 -     "[| p(1,0) \<in> formula;
   1.200 -         v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   1.201 -      ==> arity(iterates_MH_fm(p,v,x,y,z)) =
   1.202 -          succ(v) \<union> succ(x) \<union> succ(y) \<union> succ(z) \<union> (arity(p(1,0)) #- 4)"
   1.203 -apply (subgoal_tac "arity(p(1,0)) \<in> nat")
   1.204 -apply typecheck
   1.205 -apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac
   1.206 -            split: split_nat_case, clarify)
   1.207 -apply (rename_tac i j)
   1.208 -apply (drule eq_succ_imp_eq_m1, simp)
   1.209 -apply (drule eq_succ_imp_eq_m1, simp)
   1.210 -apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left)
   1.211 -done
   1.212 -
   1.213  lemma sats_iterates_MH_fm:
   1.214    assumes is_F_iff_sats:
   1.215        "!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   1.216                ==> is_F(a,b) <->
   1.217 -                  sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   1.218 -  shows
   1.219 +                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env)))))"
   1.220 +  shows 
   1.221        "[|v \<in> nat; x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A)|]
   1.222         ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <->
   1.223             iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))"
   1.224 -by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm
   1.225 +apply (frule lt_length_in_nat, assumption)  
   1.226 +apply (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm 
   1.227                is_F_iff_sats [symmetric])
   1.228 +apply (rule is_nat_case_cong) 
   1.229 +apply (simp_all add: setclass_def)
   1.230 +done
   1.231 +
   1.232  
   1.233  lemma iterates_MH_iff_sats:
   1.234    "[| (!!a b c d. [| a \<in> A; b \<in> A; c \<in> A; d \<in> A|]
   1.235                ==> is_F(a,b) <->
   1.236 -                  sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env))))));
   1.237 -      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   1.238 +                  sats(A, p, Cons(b, Cons(a, Cons(c, Cons(d,env))))));
   1.239 +      nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
   1.240        i' \<in> nat; i \<in> nat; j \<in> nat; k < length(env); env \<in> list(A)|]
   1.241     ==> iterates_MH(**A, is_F, v, x, y, z) <->
   1.242         sats(A, iterates_MH_fm(p,i',i,j,k), env)"
   1.243 -apply (rule iff_sym)
   1.244 +apply (rule iff_sym) 
   1.245  apply (rule iff_trans)
   1.246 -apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all)
   1.247 +apply (rule sats_iterates_MH_fm [of A is_F], blast)  
   1.248 +apply simp_all 
   1.249  done
   1.250 +(*FIXME: surely proof can be improved?*)
   1.251 +
   1.252  
   1.253  theorem iterates_MH_reflection:
   1.254    assumes p_reflection:
   1.255 @@ -811,12 +795,11 @@
   1.256  apply (rule bex_iff_sats conj_iff_sats)+
   1.257  apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   1.258  apply (rule sep_rules | simp)+
   1.259 -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   1.260 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.261 -apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   1.262 +apply (simp add: is_wfrec_def)
   1.263 +apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
   1.264 +            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.265  done
   1.266  
   1.267 -
   1.268  lemma list_replacement2_Reflects:
   1.269   "REFLECTS
   1.270     [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
   1.271 @@ -855,8 +838,9 @@
   1.272  apply (rule bex_iff_sats conj_iff_sats)+
   1.273  apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
   1.274  apply (rule sep_rules | simp)+
   1.275 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.276 -apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
   1.277 +apply (simp add: is_wfrec_def)
   1.278 +apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats
   1.279 +            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.280  done
   1.281  
   1.282  
   1.283 @@ -936,10 +920,9 @@
   1.284  apply (rule bex_iff_sats conj_iff_sats)+
   1.285  apply (rule_tac env = "[u,v,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
   1.286  apply (rule sep_rules | simp)+
   1.287 -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   1.288 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.289 -apply (rule sep_rules formula_functor_iff_sats quasinat_iff_sats | simp)+
   1.290 -txt{*SLOW: like 40 seconds!*}
   1.291 +apply (simp add: is_wfrec_def)
   1.292 +apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
   1.293 +            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.294  done
   1.295  
   1.296  lemma formula_replacement2_Reflects:
   1.297 @@ -980,8 +963,9 @@
   1.298  apply (rule bex_iff_sats conj_iff_sats)+
   1.299  apply (rule_tac env = "[u,v,B,0,nat]" in mem_iff_sats)
   1.300  apply (rule sep_rules | simp)+
   1.301 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.302 -apply (rule sep_rules formula_functor_iff_sats quasinat_iff_sats | simp)+
   1.303 +apply (simp add: is_wfrec_def)
   1.304 +apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats
   1.305 +            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.306  done
   1.307  
   1.308  text{*NB The proofs for type @{term formula} are virtually identical to those
   1.309 @@ -1206,8 +1190,9 @@
   1.310  apply (rule bex_iff_sats conj_iff_sats)+
   1.311  apply (rule_tac env = "[u,v,A,z,w,Memrel(succ(n))]" in mem_iff_sats)
   1.312  apply (rule sep_rules | simp)+
   1.313 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.314 -apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+
   1.315 +apply (simp add: is_wfrec_def)
   1.316 +apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
   1.317 +            is_recfun_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
   1.318  done
   1.319  
   1.320  
   1.321 @@ -1271,9 +1256,9 @@
   1.322  apply (rule bex_iff_sats conj_iff_sats)+
   1.323  apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
   1.324  apply (rule sep_rules | simp)+
   1.325 -txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
   1.326 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.327 -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   1.328 +apply (simp add: is_wfrec_def)
   1.329 +apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats
   1.330 +             is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.331  done
   1.332  
   1.333  
   1.334 @@ -1314,8 +1299,9 @@
   1.335  apply (rule bex_iff_sats conj_iff_sats)+
   1.336  apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
   1.337  apply (rule sep_rules | simp)+
   1.338 -apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
   1.339 -apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
   1.340 +apply (simp add: is_wfrec_def)
   1.341 +apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
   1.342 +              is_recfun_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+
   1.343  done
   1.344  
   1.345