src/ZF/Constructible/Datatype_absolute.thy
changeset 13398 1cadd412da48
parent 13397 6e5f4d911435
child 13409 d4ea094c650e
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:29:22 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 18:06:31 2002 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4       "[|i \<in> nat; j \<in> nat; bnd_mono(D,h)|] ==> i \<le> j --> h^i(0) \<subseteq> h^j(0)"
     1.5  apply (rule_tac m=i and n=j in diff_induct, simp_all)
     1.6  apply (blast del: subsetI
     1.7 -	     intro: bnd_mono_iterates_subset bnd_monoD2 [of concl: h] ) 
     1.8 +	     intro: bnd_mono_iterates_subset bnd_monoD2 [of concl: h]) 
     1.9  done
    1.10  
    1.11  lemma directed_iterates: "bnd_mono(D,h) ==> directed({h^n (0). n\<in>nat})"
    1.12 @@ -63,7 +63,7 @@
    1.13  apply (rule ballI)  
    1.14  apply (induct_tac n, simp_all) 
    1.15  apply (rule subset_trans [of _ "h(lfp(D,h))"])
    1.16 - apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset] )  
    1.17 + apply (blast dest: bnd_monoD2 [OF _ _ lfp_subset])  
    1.18  apply (erule lfp_lemma2) 
    1.19  done
    1.20  
    1.21 @@ -212,7 +212,7 @@
    1.22  subsection {*formulas without univ*}
    1.23  
    1.24  lemma formula_fun_bnd_mono:
    1.25 -     "bnd_mono(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
    1.26 +     "bnd_mono(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))"
    1.27  apply (rule bnd_monoI)
    1.28   apply (intro subset_refl zero_subset_univ A_subset_univ 
    1.29  	      sum_subset_univ Sigma_subset_univ nat_subset_univ) 
    1.30 @@ -220,25 +220,25 @@
    1.31  done
    1.32  
    1.33  lemma formula_fun_contin:
    1.34 -     "contin(\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
    1.35 +     "contin(\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))"
    1.36  by (intro sum_contin prod_contin id_contin const_contin) 
    1.37  
    1.38  
    1.39  text{*Re-expresses formulas using sum and product*}
    1.40  lemma formula_eq_lfp2:
    1.41 -    "formula = lfp(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
    1.42 +    "formula = lfp(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))"
    1.43  apply (simp add: formula_def) 
    1.44  apply (rule equalityI) 
    1.45   apply (rule lfp_lowerbound) 
    1.46    prefer 2 apply (rule lfp_subset)
    1.47   apply (clarify, subst lfp_unfold [OF formula_fun_bnd_mono])
    1.48 - apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)
    1.49 + apply (simp add: Member_def Equal_def Nand_def Forall_def)
    1.50   apply blast 
    1.51  txt{*Opposite inclusion*}
    1.52  apply (rule lfp_lowerbound) 
    1.53   prefer 2 apply (rule lfp_subset, clarify) 
    1.54  apply (subst lfp_unfold [OF formula.bnd_mono, simplified]) 
    1.55 -apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)  
    1.56 +apply (simp add: Member_def Equal_def Nand_def Forall_def)  
    1.57  apply (elim sumE SigmaE, simp_all) 
    1.58  apply (blast intro: datatype_univs dest: lfp_subset [THEN subsetD])+  
    1.59  done
    1.60 @@ -246,7 +246,7 @@
    1.61  text{*Re-expresses formulas using "iterates", no univ.*}
    1.62  lemma formula_eq_Union:
    1.63       "formula = 
    1.64 -      (\<Union>n\<in>nat. (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))) ^ n (0))"
    1.65 +      (\<Union>n\<in>nat. (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0))"
    1.66  by (simp add: formula_eq_lfp2 lfp_eq_Union formula_fun_bnd_mono 
    1.67                formula_fun_contin)
    1.68  
    1.69 @@ -254,16 +254,16 @@
    1.70  constdefs
    1.71    is_formula_functor :: "[i=>o,i,i] => o"
    1.72      "is_formula_functor(M,X,Z) == 
    1.73 -        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. \<exists>X4[M]. 
    1.74 +        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. 
    1.75            omega(M,nat') & cartprod(M,nat',nat',natnat) & 
    1.76            is_sum(M,natnat,natnat,natnatsum) &
    1.77 -          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & is_sum(M,X,X3,X4) &
    1.78 -          is_sum(M,natnatsum,X4,Z)"
    1.79 +          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & 
    1.80 +          is_sum(M,natnatsum,X3,Z)"
    1.81  
    1.82  lemma (in M_axioms) formula_functor_abs [simp]: 
    1.83       "[| M(X); M(Z) |] 
    1.84        ==> is_formula_functor(M,X,Z) <-> 
    1.85 -          Z = ((nat*nat) + (nat*nat)) + (X + (X*X + X))"
    1.86 +          Z = ((nat*nat) + (nat*nat)) + (X*X + X)"
    1.87  by (simp add: is_formula_functor_def) 
    1.88  
    1.89  
    1.90 @@ -429,7 +429,7 @@
    1.91  subsubsection{*Absoluteness of Formulas*}
    1.92  
    1.93  lemma (in M_datatypes) formula_replacement2': 
    1.94 -  "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))"
    1.95 +  "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))"
    1.96  apply (insert formula_replacement2) 
    1.97  apply (rule strong_replacement_cong [THEN iffD1])  
    1.98  apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) 
    1.99 @@ -447,11 +447,11 @@
   1.100  lemma (in M_datatypes) is_formula_n_abs [simp]:
   1.101       "[|n\<in>nat; M(Z)|] 
   1.102        ==> is_formula_n(M,n,Z) <-> 
   1.103 -          Z = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0)"
   1.104 +          Z = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0)"
   1.105  apply (insert formula_replacement1)
   1.106  apply (simp add: is_formula_n_def relativize1_def nat_into_M
   1.107                   iterates_abs [of "is_formula_functor(M)" _ 
   1.108 -                        "\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))"])
   1.109 +                        "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.110  done
   1.111  
   1.112  lemma (in M_datatypes) mem_formula_abs [simp]:
   1.113 @@ -609,7 +609,7 @@
   1.114  text{*Proof is trivial since @{term length} returns natural numbers.*}
   1.115  lemma (in M_triv_axioms) length_closed [intro,simp]:
   1.116       "l \<in> list(A) ==> M(length(l))"
   1.117 -by (simp add: nat_into_M ) 
   1.118 +by (simp add: nat_into_M) 
   1.119  
   1.120  
   1.121  subsection {*Absoluteness for @{term nth}*}
   1.122 @@ -661,4 +661,336 @@
   1.123  done
   1.124  
   1.125  
   1.126 +
   1.127 +
   1.128 +subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
   1.129 +
   1.130 +constdefs
   1.131 +  is_Member :: "[i=>o,i,i,i] => o"
   1.132 +     --{* because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}*}
   1.133 +    "is_Member(M,x,y,Z) ==
   1.134 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)"
   1.135 +
   1.136 +lemma (in M_triv_axioms) Member_abs [simp]:
   1.137 +     "[|M(x); M(y); M(Z)|] ==> is_Member(M,x,y,Z) <-> (Z = Member(x,y))"
   1.138 +by (simp add: is_Member_def Member_def)
   1.139 +
   1.140 +lemma (in M_triv_axioms) Member_in_M_iff [iff]:
   1.141 +     "M(Member(x,y)) <-> M(x) & M(y)"
   1.142 +by (simp add: Member_def) 
   1.143 +
   1.144 +constdefs
   1.145 +  is_Equal :: "[i=>o,i,i,i] => o"
   1.146 +     --{* because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}*}
   1.147 +    "is_Equal(M,x,y,Z) ==
   1.148 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)"
   1.149 +
   1.150 +lemma (in M_triv_axioms) Equal_abs [simp]:
   1.151 +     "[|M(x); M(y); M(Z)|] ==> is_Equal(M,x,y,Z) <-> (Z = Equal(x,y))"
   1.152 +by (simp add: is_Equal_def Equal_def)
   1.153 +
   1.154 +lemma (in M_triv_axioms) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
   1.155 +by (simp add: Equal_def) 
   1.156 +
   1.157 +constdefs
   1.158 +  is_Nand :: "[i=>o,i,i,i] => o"
   1.159 +     --{* because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}*}
   1.160 +    "is_Nand(M,x,y,Z) ==
   1.161 +	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)"
   1.162 +
   1.163 +lemma (in M_triv_axioms) Nand_abs [simp]:
   1.164 +     "[|M(x); M(y); M(Z)|] ==> is_Nand(M,x,y,Z) <-> (Z = Nand(x,y))"
   1.165 +by (simp add: is_Nand_def Nand_def)
   1.166 +
   1.167 +lemma (in M_triv_axioms) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
   1.168 +by (simp add: Nand_def) 
   1.169 +
   1.170 +constdefs
   1.171 +  is_Forall :: "[i=>o,i,i] => o"
   1.172 +     --{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
   1.173 +    "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
   1.174 +
   1.175 +lemma (in M_triv_axioms) Forall_abs [simp]:
   1.176 +     "[|M(x); M(Z)|] ==> is_Forall(M,x,Z) <-> (Z = Forall(x))"
   1.177 +by (simp add: is_Forall_def Forall_def)
   1.178 +
   1.179 +lemma (in M_triv_axioms) Forall_in_M_iff [iff]: "M(Forall(x)) <-> M(x)"
   1.180 +by (simp add: Forall_def)
   1.181 +
   1.182 +
   1.183 +subsection {*Absoluteness for @{term formula_rec}*}
   1.184 +
   1.185 +subsubsection{*@{term quasiformula}: For Case-Splitting with @{term formula_case'}*}
   1.186 +
   1.187 +constdefs
   1.188 +
   1.189 +  quasiformula :: "i => o"
   1.190 +    "quasiformula(p) == 
   1.191 +	(\<exists>x y. p = Member(x,y)) |
   1.192 +	(\<exists>x y. p = Equal(x,y)) |
   1.193 +	(\<exists>x y. p = Nand(x,y)) |
   1.194 +	(\<exists>x. p = Forall(x))"
   1.195 +
   1.196 +  is_quasiformula :: "[i=>o,i] => o"
   1.197 +    "is_quasiformula(M,p) == 
   1.198 +	(\<exists>x[M]. \<exists>y[M]. is_Member(M,x,y,p)) |
   1.199 +	(\<exists>x[M]. \<exists>y[M]. is_Equal(M,x,y,p)) |
   1.200 +	(\<exists>x[M]. \<exists>y[M]. is_Nand(M,x,y,p)) |
   1.201 +	(\<exists>x[M]. is_Forall(M,x,p))"
   1.202 +
   1.203 +lemma [iff]: "quasiformula(Member(x,y))"
   1.204 +by (simp add: quasiformula_def)
   1.205 +
   1.206 +lemma [iff]: "quasiformula(Equal(x,y))"
   1.207 +by (simp add: quasiformula_def)
   1.208 +
   1.209 +lemma [iff]: "quasiformula(Nand(x,y))"
   1.210 +by (simp add: quasiformula_def)
   1.211 +
   1.212 +lemma [iff]: "quasiformula(Forall(x))"
   1.213 +by (simp add: quasiformula_def)
   1.214 +
   1.215 +lemma formula_imp_quasiformula: "p \<in> formula ==> quasiformula(p)"
   1.216 +by (erule formula.cases, simp_all)
   1.217 +
   1.218 +lemma (in M_triv_axioms) quasiformula_abs [simp]: 
   1.219 +     "M(z) ==> is_quasiformula(M,z) <-> quasiformula(z)"
   1.220 +by (auto simp add: is_quasiformula_def quasiformula_def)
   1.221 +
   1.222 +constdefs
   1.223 +
   1.224 +  formula_case' :: "[[i,i]=>i, [i,i]=>i, [i,i]=>i, i=>i, i] => i"
   1.225 +    --{*A version of @{term formula_case} that's always defined.*}
   1.226 +    "formula_case'(a,b,c,d,p) == 
   1.227 +       if quasiformula(p) then formula_case(a,b,c,d,p) else 0"  
   1.228 +
   1.229 +  is_formula_case :: 
   1.230 +      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   1.231 +    --{*Returns 0 for non-formulas*}
   1.232 +    "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
   1.233 +	(\<forall>x[M]. \<forall>y[M]. is_Member(M,x,y,p) --> is_a(x,y,z)) &
   1.234 +	(\<forall>x[M]. \<forall>y[M]. is_Equal(M,x,y,p) --> is_b(x,y,z)) &
   1.235 +	(\<forall>x[M]. \<forall>y[M]. is_Nand(M,x,y,p) --> is_c(x,y,z)) &
   1.236 +	(\<forall>x[M]. is_Forall(M,x,p) --> is_d(x,z)) &
   1.237 +        (is_quasiformula(M,p) | empty(M,z))"
   1.238 +
   1.239 +subsubsection{*@{term formula_case'}, the Modified Version of @{term formula_case}*}
   1.240 +
   1.241 +lemma formula_case'_Member [simp]:
   1.242 +     "formula_case'(a,b,c,d,Member(x,y)) = a(x,y)"
   1.243 +by (simp add: formula_case'_def)
   1.244 +
   1.245 +lemma formula_case'_Equal [simp]:
   1.246 +     "formula_case'(a,b,c,d,Equal(x,y)) = b(x,y)"
   1.247 +by (simp add: formula_case'_def)
   1.248 +
   1.249 +lemma formula_case'_Nand [simp]:
   1.250 +     "formula_case'(a,b,c,d,Nand(x,y)) = c(x,y)"
   1.251 +by (simp add: formula_case'_def)
   1.252 +
   1.253 +lemma formula_case'_Forall [simp]:
   1.254 +     "formula_case'(a,b,c,d,Forall(x)) = d(x)"
   1.255 +by (simp add: formula_case'_def)
   1.256 +
   1.257 +lemma non_formula_case: "~ quasiformula(x) ==> formula_case'(a,b,c,d,x) = 0" 
   1.258 +by (simp add: quasiformula_def formula_case'_def) 
   1.259 +
   1.260 +lemma formula_case'_eq_formula_case [simp]:
   1.261 +     "p \<in> formula ==>formula_case'(a,b,c,d,p) = formula_case(a,b,c,d,p)"
   1.262 +by (erule formula.cases, simp_all)
   1.263 +
   1.264 +lemma (in M_axioms) formula_case'_closed [intro,simp]:
   1.265 +  "[|M(p); \<forall>x[M]. \<forall>y[M]. M(a(x,y)); 
   1.266 +           \<forall>x[M]. \<forall>y[M]. M(b(x,y)); 
   1.267 +           \<forall>x[M]. \<forall>y[M]. M(c(x,y)); 
   1.268 +           \<forall>x[M]. M(d(x))|] ==> M(formula_case'(a,b,c,d,p))"
   1.269 +apply (case_tac "quasiformula(p)") 
   1.270 + apply (simp add: quasiformula_def, force) 
   1.271 +apply (simp add: non_formula_case) 
   1.272 +done
   1.273 +
   1.274 +lemma (in M_triv_axioms) formula_case_abs [simp]: 
   1.275 +     "[| relativize2(M,is_a,a); relativize2(M,is_b,b); 
   1.276 +         relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |] 
   1.277 +      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
   1.278 +          z = formula_case'(a,b,c,d,p)"
   1.279 +apply (case_tac "quasiformula(p)") 
   1.280 + prefer 2 
   1.281 + apply (simp add: is_formula_case_def non_formula_case) 
   1.282 + apply (force simp add: quasiformula_def) 
   1.283 +apply (simp add: quasiformula_def is_formula_case_def)
   1.284 +apply (elim disjE exE) 
   1.285 + apply (simp_all add: relativize1_def relativize2_def) 
   1.286 +done
   1.287 +
   1.288 +
   1.289 +subsubsection{*Towards Absoluteness of @{term formula_rec}*}
   1.290 +
   1.291 +consts   depth :: "i=>i"
   1.292 +primrec
   1.293 +  "depth(Member(x,y)) = 0"
   1.294 +  "depth(Equal(x,y))  = 0"
   1.295 +  "depth(Nand(p,q)) = succ(depth(p) \<union> depth(q))"
   1.296 +  "depth(Forall(p)) = succ(depth(p))"
   1.297 +
   1.298 +lemma depth_type [TC]: "p \<in> formula ==> depth(p) \<in> nat"
   1.299 +by (induct_tac p, simp_all) 
   1.300 +
   1.301 +
   1.302 +constdefs
   1.303 +  formula_N :: "i => i"
   1.304 +    "formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
   1.305 +
   1.306 +lemma Member_in_formula_N [simp]:
   1.307 +     "Member(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"
   1.308 +by (simp add: formula_N_def Member_def) 
   1.309 +
   1.310 +lemma Equal_in_formula_N [simp]:
   1.311 +     "Equal(x,y) \<in> formula_N(succ(n)) <-> x \<in> nat & y \<in> nat"
   1.312 +by (simp add: formula_N_def Equal_def) 
   1.313 +
   1.314 +lemma Nand_in_formula_N [simp]:
   1.315 +     "Nand(x,y) \<in> formula_N(succ(n)) <-> x \<in> formula_N(n) & y \<in> formula_N(n)"
   1.316 +by (simp add: formula_N_def Nand_def) 
   1.317 +
   1.318 +lemma Forall_in_formula_N [simp]:
   1.319 +     "Forall(x) \<in> formula_N(succ(n)) <-> x \<in> formula_N(n)"
   1.320 +by (simp add: formula_N_def Forall_def) 
   1.321 +
   1.322 +text{*These two aren't simprules because they reveal the underlying
   1.323 +formula representation.*}
   1.324 +lemma formula_N_0: "formula_N(0) = 0"
   1.325 +by (simp add: formula_N_def)
   1.326 +
   1.327 +lemma formula_N_succ:
   1.328 +     "formula_N(succ(n)) = 
   1.329 +      ((nat*nat) + (nat*nat)) + (formula_N(n) * formula_N(n) + formula_N(n))"
   1.330 +by (simp add: formula_N_def)
   1.331 +
   1.332 +lemma formula_N_imp_formula:
   1.333 +  "[| p \<in> formula_N(n); n \<in> nat |] ==> p \<in> formula"
   1.334 +by (force simp add: formula_eq_Union formula_N_def)
   1.335 +
   1.336 +lemma formula_N_imp_depth_lt [rule_format]:
   1.337 +     "n \<in> nat ==> \<forall>p \<in> formula_N(n). depth(p) < n"
   1.338 +apply (induct_tac n)  
   1.339 +apply (auto simp add: formula_N_0 formula_N_succ 
   1.340 +                      depth_type formula_N_imp_formula Un_least_lt_iff
   1.341 +                      Member_def [symmetric] Equal_def [symmetric]
   1.342 +                      Nand_def [symmetric] Forall_def [symmetric]) 
   1.343 +done
   1.344 +
   1.345 +lemma formula_imp_formula_N [rule_format]:
   1.346 +     "p \<in> formula ==> \<forall>n\<in>nat. depth(p) < n --> p \<in> formula_N(n)"
   1.347 +apply (induct_tac p)
   1.348 +apply (simp_all add: succ_Un_distrib Un_least_lt_iff) 
   1.349 +apply (force elim: natE)+
   1.350 +done
   1.351 +
   1.352 +lemma formula_N_imp_eq_depth:
   1.353 +      "[|n \<in> nat; p \<notin> formula_N(n); p \<in> formula_N(succ(n))|] 
   1.354 +       ==> n = depth(p)"
   1.355 +apply (rule le_anti_sym) 
   1.356 + prefer 2 apply (simp add: formula_N_imp_depth_lt) 
   1.357 +apply (frule formula_N_imp_formula, simp)
   1.358 +apply (simp add: not_lt_iff_le [symmetric]) 
   1.359 +apply (blast intro: formula_imp_formula_N) 
   1.360 +done
   1.361 +
   1.362 +
   1.363 +
   1.364 +lemma formula_N_mono [rule_format]:
   1.365 +  "[| m \<in> nat; n \<in> nat |] ==> m\<le>n --> formula_N(m) \<subseteq> formula_N(n)"
   1.366 +apply (rule_tac m = m and n = n in diff_induct)
   1.367 +apply (simp_all add: formula_N_0 formula_N_succ, blast) 
   1.368 +done
   1.369 +
   1.370 +lemma formula_N_distrib:
   1.371 +  "[| m \<in> nat; n \<in> nat |] ==> formula_N(m \<union> n) = formula_N(m) \<union> formula_N(n)"
   1.372 +apply (rule_tac i = m and j = n in Ord_linear_le, auto) 
   1.373 +apply (simp_all add: subset_Un_iff [THEN iffD1] subset_Un_iff2 [THEN iffD1] 
   1.374 +                     le_imp_subset formula_N_mono)
   1.375 +done
   1.376 +
   1.377 +lemma Nand_in_formula_N:
   1.378 +    "[|p \<in> formula; q \<in> formula|]
   1.379 +     ==> Nand(p,q) \<in> formula_N(succ(succ(depth(p))) \<union> succ(succ(depth(q))))"
   1.380 +by (simp add: succ_Un_distrib [symmetric] formula_imp_formula_N le_Un_iff) 
   1.381 +
   1.382 +
   1.383 +text{*Express @{term formula_rec} without using @{term rank} or @{term Vset},
   1.384 +neither of which is absolute.*}
   1.385 +lemma (in M_triv_axioms) formula_rec_eq:
   1.386 +  "p \<in> formula ==>
   1.387 +   formula_rec(a,b,c,d,p) = 
   1.388 +   transrec (succ(depth(p)),
   1.389 +      \<lambda>x h. Lambda (formula_N(x),
   1.390 +             formula_case' (a, b,
   1.391 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
   1.392 +                              h ` succ(depth(v)) ` v),
   1.393 +                \<lambda>u. d(u, h ` succ(depth(u)) ` u)))) 
   1.394 +   ` p"
   1.395 +apply (induct_tac p)
   1.396 +txt{*Base case for @{term Member}*}
   1.397 +apply (subst transrec, simp) 
   1.398 +txt{*Base case for @{term Equal}*}
   1.399 +apply (subst transrec, simp)
   1.400 +txt{*Inductive step for @{term Nand}*}
   1.401 +apply (subst transrec)
   1.402 +apply (simp add: succ_Un_distrib Nand_in_formula_N)
   1.403 +txt{*Inductive step for @{term Forall}*}
   1.404 +apply (subst transrec) 
   1.405 +apply (simp add: formula_imp_formula_N) 
   1.406 +done
   1.407 +
   1.408 +
   1.409 +constdefs
   1.410 +  is_formula_N :: "[i=>o,i,i] => o"
   1.411 +    "is_formula_N(M,n,Z) == 
   1.412 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
   1.413 +       empty(M,zero) & 
   1.414 +       successor(M,n,sn) & membership(M,sn,msn) &
   1.415 +       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
   1.416 +  
   1.417 +
   1.418 +lemma (in M_datatypes) formula_N_abs [simp]:
   1.419 +     "[|n\<in>nat; M(Z)|] 
   1.420 +      ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
   1.421 +apply (insert formula_replacement1)
   1.422 +apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.423 +                 iterates_abs [of "is_formula_functor(M)" _ 
   1.424 +                                  "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.425 +done
   1.426 +
   1.427 +lemma (in M_datatypes) formula_N_closed [intro,simp]:
   1.428 +     "n\<in>nat ==> M(formula_N(n))"
   1.429 +apply (insert formula_replacement1)
   1.430 +apply (simp add: is_formula_N_def formula_N_def relativize1_def nat_into_M
   1.431 +                 iterates_closed [of "is_formula_functor(M)"])
   1.432 +done
   1.433 +
   1.434 +subsection{*Absoluteness for the Formula Operator @{term depth}*}
   1.435 +constdefs
   1.436 +
   1.437 +  is_depth :: "[i=>o,i,i] => o"
   1.438 +    "is_depth(M,p,n) == 
   1.439 +       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
   1.440 +        is_formula_N(M,n,formula_n) & p \<notin> formula_n &
   1.441 +        successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
   1.442 +
   1.443 +
   1.444 +lemma (in M_datatypes) depth_abs [simp]:
   1.445 +     "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
   1.446 +apply (subgoal_tac "M(p) & M(n)")
   1.447 + prefer 2 apply (blast dest: transM)  
   1.448 +apply (simp add: is_depth_def)
   1.449 +apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
   1.450 +             dest: formula_N_imp_depth_lt)
   1.451 +done
   1.452 +
   1.453 +text{*Proof is trivial since @{term depth} returns natural numbers.*}
   1.454 +lemma (in M_triv_axioms) depth_closed [intro,simp]:
   1.455 +     "p \<in> formula ==> M(depth(p))"
   1.456 +by (simp add: nat_into_M) 
   1.457 +
   1.458  end