src/ZF/Constructible/Datatype_absolute.thy
changeset 13655 95b95cdb4704
parent 13647 7f6f0ffc45c3
child 13687 22dce9134953
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Oct 18 09:53:18 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Oct 18 17:50:13 2002 +0200
     1.3 @@ -125,6 +125,11 @@
     1.4        \<forall>n[M]. n\<in>nat --> 
     1.5           wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))"
     1.6  
     1.7 +  is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o"
     1.8 +    "is_iterates(M,isF,v,n,Z) == 
     1.9 +      \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.10 +                       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"
    1.11 +
    1.12  lemma (in M_basic) iterates_MH_abs:
    1.13    "[| relation1(M,isF,F); M(n); M(g); M(z) |] 
    1.14     ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \<lambda>m. F(g`m), n)"
    1.15 @@ -140,11 +145,10 @@
    1.16  theorem (in M_trancl) iterates_abs:
    1.17    "[| iterates_replacement(M,isF,v); relation1(M,isF,F);
    1.18        n \<in> nat; M(v); M(z); \<forall>x[M]. M(F(x)) |] 
    1.19 -   ==> is_wfrec(M, iterates_MH(M,isF,v), Memrel(succ(n)), n, z) <->
    1.20 -       z = iterates(F,n,v)" 
    1.21 +   ==> is_iterates(M,isF,v,n,z) <-> z = iterates(F,n,v)" 
    1.22  apply (frule iterates_imp_wfrec_replacement, assumption+)
    1.23  apply (simp add: wf_Memrel trans_Memrel relation_Memrel nat_into_M
    1.24 -                 relation2_def iterates_MH_abs 
    1.25 +                 is_iterates_def relation2_def iterates_MH_abs 
    1.26                   iterates_nat_def recursor_def transrec_def 
    1.27                   eclose_sing_Ord_eq nat_into_M
    1.28           trans_wfrec_abs [of _ _ _ _ "\<lambda>n g. nat_case(v, \<lambda>m. F(g`m), n)"])
    1.29 @@ -338,10 +342,8 @@
    1.30  constdefs
    1.31    is_list_N :: "[i=>o,i,i,i] => o"
    1.32      "is_list_N(M,A,n,Z) == 
    1.33 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.34 -       empty(M,zero) & 
    1.35 -       successor(M,n,sn) & membership(M,sn,msn) &
    1.36 -       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
    1.37 +      \<exists>zero[M]. empty(M,zero) & 
    1.38 +                is_iterates(M, is_list_functor(M,A), zero, n, Z)"
    1.39    
    1.40    mem_list :: "[i=>o,i,i] => o"
    1.41      "mem_list(M,A,l) == 
    1.42 @@ -442,11 +444,9 @@
    1.43  constdefs
    1.44    is_formula_N :: "[i=>o,i,i] => o"
    1.45      "is_formula_N(M,n,Z) == 
    1.46 -      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.47 -       empty(M,zero) & 
    1.48 -       successor(M,n,sn) & membership(M,sn,msn) &
    1.49 -       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
    1.50 -  
    1.51 +      \<exists>zero[M]. empty(M,zero) & 
    1.52 +                is_iterates(M, is_formula_functor(M), zero, n, Z)"
    1.53 +
    1.54  
    1.55  constdefs
    1.56    
    1.57 @@ -459,40 +459,34 @@
    1.58      "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
    1.59  
    1.60  locale M_datatypes = M_trancl +
    1.61 - assumes list_replacement1: 
    1.62 + assumes list_replacement1:
    1.63     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.64 -  and list_replacement2: 
    1.65 -   "M(A) ==> strong_replacement(M, 
    1.66 -         \<lambda>n y. n\<in>nat & 
    1.67 -               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.68 -               is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), 
    1.69 -                        msn, n, y)))"
    1.70 -  and formula_replacement1: 
    1.71 +  and list_replacement2:
    1.72 +   "M(A) ==> strong_replacement(M,
    1.73 +         \<lambda>n y. n\<in>nat & is_iterates(M, is_list_functor(M,A), 0, n, y))"
    1.74 +  and formula_replacement1:
    1.75     "iterates_replacement(M, is_formula_functor(M), 0)"
    1.76 -  and formula_replacement2: 
    1.77 -   "strong_replacement(M, 
    1.78 -         \<lambda>n y. n\<in>nat & 
    1.79 -               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
    1.80 -               is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), 
    1.81 -                        msn, n, y)))"
    1.82 +  and formula_replacement2:
    1.83 +   "strong_replacement(M,
    1.84 +         \<lambda>n y. n\<in>nat & is_iterates(M, is_formula_functor(M), 0, n, y))"
    1.85    and nth_replacement:
    1.86     "M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)"
    1.87 -        
    1.88 +
    1.89  
    1.90  subsubsection{*Absoluteness of the List Construction*}
    1.91  
    1.92 -lemma (in M_datatypes) list_replacement2': 
    1.93 +lemma (in M_datatypes) list_replacement2':
    1.94    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
    1.95 -apply (insert list_replacement2 [of A]) 
    1.96 -apply (rule strong_replacement_cong [THEN iffD1])  
    1.97 -apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) 
    1.98 -apply (simp_all add: list_replacement1 relation1_def) 
    1.99 +apply (insert list_replacement2 [of A])
   1.100 +apply (rule strong_replacement_cong [THEN iffD1])
   1.101 +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]])
   1.102 +apply (simp_all add: list_replacement1 relation1_def)
   1.103  done
   1.104  
   1.105  lemma (in M_datatypes) list_closed [intro,simp]:
   1.106       "M(A) ==> M(list(A))"
   1.107  apply (insert list_replacement1)
   1.108 -by  (simp add: RepFun_closed2 list_eq_Union 
   1.109 +by  (simp add: RepFun_closed2 list_eq_Union
   1.110                 list_replacement2' relation1_def
   1.111                 iterates_closed [of "is_list_functor(M,A)"])
   1.112  
   1.113 @@ -500,7 +494,7 @@
   1.114  lemmas (in M_datatypes) list_into_M = transM [OF _ list_closed]
   1.115  
   1.116  lemma (in M_datatypes) list_N_abs [simp]:
   1.117 -     "[|M(A); n\<in>nat; M(Z)|] 
   1.118 +     "[|M(A); n\<in>nat; M(Z)|]
   1.119        ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
   1.120  apply (insert list_replacement1)
   1.121  apply (simp add: is_list_N_def list_N_def relation1_def nat_into_M
   1.122 @@ -518,7 +512,7 @@
   1.123       "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
   1.124  apply (insert list_replacement1)
   1.125  apply (simp add: mem_list_def list_N_def relation1_def list_eq_Union
   1.126 -                 iterates_closed [of "is_list_functor(M,A)"]) 
   1.127 +                 iterates_closed [of "is_list_functor(M,A)"])
   1.128  done
   1.129  
   1.130  lemma (in M_datatypes) list_abs [simp]:
   1.131 @@ -529,18 +523,18 @@
   1.132  
   1.133  subsubsection{*Absoluteness of Formulas*}
   1.134  
   1.135 -lemma (in M_datatypes) formula_replacement2': 
   1.136 +lemma (in M_datatypes) formula_replacement2':
   1.137    "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X))^n (0))"
   1.138 -apply (insert formula_replacement2) 
   1.139 -apply (rule strong_replacement_cong [THEN iffD1])  
   1.140 -apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) 
   1.141 -apply (simp_all add: formula_replacement1 relation1_def) 
   1.142 +apply (insert formula_replacement2)
   1.143 +apply (rule strong_replacement_cong [THEN iffD1])
   1.144 +apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]])
   1.145 +apply (simp_all add: formula_replacement1 relation1_def)
   1.146  done
   1.147  
   1.148  lemma (in M_datatypes) formula_closed [intro,simp]:
   1.149       "M(formula)"
   1.150  apply (insert formula_replacement1)
   1.151 -apply  (simp add: RepFun_closed2 formula_eq_Union 
   1.152 +apply  (simp add: RepFun_closed2 formula_eq_Union
   1.153                    formula_replacement2' relation1_def
   1.154                    iterates_closed [of "is_formula_functor(M)"])
   1.155  done
   1.156 @@ -548,11 +542,11 @@
   1.157  lemmas (in M_datatypes) formula_into_M = transM [OF _ formula_closed]
   1.158  
   1.159  lemma (in M_datatypes) formula_N_abs [simp]:
   1.160 -     "[|n\<in>nat; M(Z)|] 
   1.161 +     "[|n\<in>nat; M(Z)|]
   1.162        ==> is_formula_N(M,n,Z) <-> Z = formula_N(n)"
   1.163  apply (insert formula_replacement1)
   1.164  apply (simp add: is_formula_N_def formula_N_def relation1_def nat_into_M
   1.165 -                 iterates_abs [of "is_formula_functor(M)" _ 
   1.166 +                 iterates_abs [of "is_formula_functor(M)" _
   1.167                                    "\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)"])
   1.168  done
   1.169  
   1.170 @@ -567,7 +561,7 @@
   1.171       "mem_formula(M,l) <-> l \<in> formula"
   1.172  apply (insert formula_replacement1)
   1.173  apply (simp add: mem_formula_def relation1_def formula_eq_Union formula_N_def
   1.174 -                 iterates_closed [of "is_formula_functor(M)"]) 
   1.175 +                 iterates_closed [of "is_formula_functor(M)"])
   1.176  done
   1.177  
   1.178  lemma (in M_datatypes) formula_abs [simp]:
   1.179 @@ -582,24 +576,21 @@
   1.180  text{*Re-expresses eclose using "iterates"*}
   1.181  lemma eclose_eq_Union:
   1.182       "eclose(A) = (\<Union>n\<in>nat. Union^n (A))"
   1.183 -apply (simp add: eclose_def) 
   1.184 -apply (rule UN_cong) 
   1.185 +apply (simp add: eclose_def)
   1.186 +apply (rule UN_cong)
   1.187  apply (rule refl)
   1.188  apply (induct_tac n)
   1.189 -apply (simp add: nat_rec_0)  
   1.190 -apply (simp add: nat_rec_succ) 
   1.191 +apply (simp add: nat_rec_0)
   1.192 +apply (simp add: nat_rec_succ)
   1.193  done
   1.194  
   1.195  constdefs
   1.196    is_eclose_n :: "[i=>o,i,i,i] => o"
   1.197 -    "is_eclose_n(M,A,n,Z) == 
   1.198 -      \<exists>sn[M]. \<exists>msn[M]. 
   1.199 -       successor(M,n,sn) & membership(M,sn,msn) &
   1.200 -       is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)"
   1.201 -  
   1.202 +    "is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)"
   1.203 +
   1.204    mem_eclose :: "[i=>o,i,i] => o"
   1.205 -    "mem_eclose(M,A,l) == 
   1.206 -      \<exists>n[M]. \<exists>eclosen[M]. 
   1.207 +    "mem_eclose(M,A,l) ==
   1.208 +      \<exists>n[M]. \<exists>eclosen[M].
   1.209         finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen"
   1.210  
   1.211    is_eclose :: "[i=>o,i,i] => o"
   1.212 @@ -607,27 +598,24 @@
   1.213  
   1.214  
   1.215  locale M_eclose = M_datatypes +
   1.216 - assumes eclose_replacement1: 
   1.217 + assumes eclose_replacement1:
   1.218     "M(A) ==> iterates_replacement(M, big_union(M), A)"
   1.219 -  and eclose_replacement2: 
   1.220 -   "M(A) ==> strong_replacement(M, 
   1.221 -         \<lambda>n y. n\<in>nat & 
   1.222 -               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   1.223 -               is_wfrec(M, iterates_MH(M,big_union(M), A), 
   1.224 -                        msn, n, y)))"
   1.225 +  and eclose_replacement2:
   1.226 +   "M(A) ==> strong_replacement(M,
   1.227 +         \<lambda>n y. n\<in>nat & is_iterates(M, big_union(M), A, n, y))"
   1.228  
   1.229 -lemma (in M_eclose) eclose_replacement2': 
   1.230 +lemma (in M_eclose) eclose_replacement2':
   1.231    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = Union^n (A))"
   1.232 -apply (insert eclose_replacement2 [of A]) 
   1.233 -apply (rule strong_replacement_cong [THEN iffD1])  
   1.234 -apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) 
   1.235 -apply (simp_all add: eclose_replacement1 relation1_def) 
   1.236 +apply (insert eclose_replacement2 [of A])
   1.237 +apply (rule strong_replacement_cong [THEN iffD1])
   1.238 +apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]])
   1.239 +apply (simp_all add: eclose_replacement1 relation1_def)
   1.240  done
   1.241  
   1.242  lemma (in M_eclose) eclose_closed [intro,simp]:
   1.243       "M(A) ==> M(eclose(A))"
   1.244  apply (insert eclose_replacement1)
   1.245 -by  (simp add: RepFun_closed2 eclose_eq_Union 
   1.246 +by  (simp add: RepFun_closed2 eclose_eq_Union
   1.247                 eclose_replacement2' relation1_def
   1.248                 iterates_closed [of "big_union(M)"])
   1.249  
   1.250 @@ -642,7 +630,7 @@
   1.251       "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
   1.252  apply (insert eclose_replacement1)
   1.253  apply (simp add: mem_eclose_def relation1_def eclose_eq_Union
   1.254 -                 iterates_closed [of "big_union(M)"]) 
   1.255 +                 iterates_closed [of "big_union(M)"])
   1.256  done
   1.257  
   1.258  lemma (in M_eclose) eclose_abs [simp]:
   1.259 @@ -652,54 +640,52 @@
   1.260  done
   1.261  
   1.262  
   1.263 -
   1.264 -
   1.265  subsection {*Absoluteness for @{term transrec}*}
   1.266  
   1.267 -
   1.268  text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
   1.269  constdefs
   1.270  
   1.271    is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.272 -   "is_transrec(M,MH,a,z) == 
   1.273 -      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
   1.274 +   "is_transrec(M,MH,a,z) ==
   1.275 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
   1.276         upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.277         is_wfrec(M,MH,mesa,a,z)"
   1.278  
   1.279    transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
   1.280     "transrec_replacement(M,MH,a) ==
   1.281 -      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
   1.282 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M].
   1.283         upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.284         wfrec_replacement(M,MH,mesa)"
   1.285  
   1.286 -text{*The condition @{term "Ord(i)"} lets us use the simpler 
   1.287 +text{*The condition @{term "Ord(i)"} lets us use the simpler
   1.288    @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   1.289    which I haven't even proved yet. *}
   1.290  theorem (in M_eclose) transrec_abs:
   1.291    "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   1.292       Ord(i);  M(i);  M(z);
   1.293 -     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.294 -   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
   1.295 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
   1.296 +   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)"
   1.297  by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
   1.298         transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
   1.299  
   1.300  
   1.301  theorem (in M_eclose) transrec_closed:
   1.302       "[|transrec_replacement(M,MH,i);  relation2(M,MH,H);
   1.303 -	Ord(i);  M(i);  
   1.304 -	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.305 +	Ord(i);  M(i);
   1.306 +	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|]
   1.307        ==> M(transrec(i,H))"
   1.308  by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
   1.309          transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
   1.310  
   1.311  
   1.312  text{*Helps to prove instances of @{term transrec_replacement}*}
   1.313 -lemma (in M_eclose) transrec_replacementI: 
   1.314 +lemma (in M_eclose) transrec_replacementI:
   1.315     "[|M(a);
   1.316 -    strong_replacement (M, 
   1.317 -                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) \<and> is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
   1.318 +      strong_replacement (M,
   1.319 +                  \<lambda>x z. \<exists>y[M]. pair(M, x, y, z) &
   1.320 +                               is_wfrec(M,MH,Memrel(eclose({a})),x,y))|]
   1.321      ==> transrec_replacement(M,MH,a)"
   1.322 -by (simp add: transrec_replacement_def wfrec_replacement_def) 
   1.323 +by (simp add: transrec_replacement_def wfrec_replacement_def)
   1.324  
   1.325  
   1.326  subsection{*Absoluteness for the List Operator @{term length}*}
   1.327 @@ -707,8 +693,8 @@
   1.328  
   1.329  constdefs
   1.330    is_length :: "[i=>o,i,i,i] => o"
   1.331 -    "is_length(M,A,l,n) == 
   1.332 -       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M]. 
   1.333 +    "is_length(M,A,l,n) ==
   1.334 +       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
   1.335          is_list_N(M,A,n,list_n) & l \<notin> list_n &
   1.336          successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \<in> list_sn"
   1.337  
   1.338 @@ -716,7 +702,7 @@
   1.339  lemma (in M_datatypes) length_abs [simp]:
   1.340       "[|M(A); l \<in> list(A); n \<in> nat|] ==> is_length(M,A,l,n) <-> n = length(l)"
   1.341  apply (subgoal_tac "M(l) & M(n)")
   1.342 - prefer 2 apply (blast dest: transM)  
   1.343 + prefer 2 apply (blast dest: transM)
   1.344  apply (simp add: is_length_def)
   1.345  apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
   1.346               dest: list_N_imp_length_lt)
   1.347 @@ -725,29 +711,29 @@
   1.348  text{*Proof is trivial since @{term length} returns natural numbers.*}
   1.349  lemma (in M_trivial) length_closed [intro,simp]:
   1.350       "l \<in> list(A) ==> M(length(l))"
   1.351 -by (simp add: nat_into_M) 
   1.352 +by (simp add: nat_into_M)
   1.353  
   1.354  
   1.355  subsection {*Absoluteness for the List Operator @{term nth}*}
   1.356  
   1.357  lemma nth_eq_hd_iterates_tl [rule_format]:
   1.358       "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
   1.359 -apply (induct_tac xs) 
   1.360 -apply (simp add: iterates_tl_Nil hd'_Nil, clarify) 
   1.361 +apply (induct_tac xs)
   1.362 +apply (simp add: iterates_tl_Nil hd'_Nil, clarify)
   1.363  apply (erule natE)
   1.364 -apply (simp add: hd'_Cons) 
   1.365 -apply (simp add: tl'_Cons iterates_commute) 
   1.366 +apply (simp add: hd'_Cons)
   1.367 +apply (simp add: tl'_Cons iterates_commute)
   1.368  done
   1.369  
   1.370  lemma (in M_basic) iterates_tl'_closed:
   1.371       "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
   1.372 -apply (induct_tac n, simp) 
   1.373 -apply (simp add: tl'_Cons tl'_closed) 
   1.374 +apply (induct_tac n, simp)
   1.375 +apply (simp add: tl'_Cons tl'_closed)
   1.376  done
   1.377  
   1.378  text{*Immediate by type-checking*}
   1.379  lemma (in M_datatypes) nth_closed [intro,simp]:
   1.380 -     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))" 
   1.381 +     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
   1.382  apply (case_tac "n < length(xs)")
   1.383   apply (blast intro: nth_type transM)
   1.384  apply (simp add: not_lt_iff_le nth_eq_0)
   1.385 @@ -755,19 +741,16 @@
   1.386  
   1.387  constdefs
   1.388    is_nth :: "[i=>o,i,i,i] => o"
   1.389 -    "is_nth(M,n,l,Z) == 
   1.390 -      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M]. 
   1.391 -       successor(M,n,sn) & membership(M,sn,msn) &
   1.392 -       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
   1.393 -       is_hd(M,X,Z)"
   1.394 - 
   1.395 +    "is_nth(M,n,l,Z) ==
   1.396 +      \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"
   1.397 +
   1.398  lemma (in M_datatypes) nth_abs [simp]:
   1.399 -     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|] 
   1.400 +     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
   1.401        ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
   1.402 -apply (subgoal_tac "M(l)") 
   1.403 +apply (subgoal_tac "M(l)")
   1.404   prefer 2 apply (blast intro: transM)
   1.405  apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
   1.406 -                 tl'_closed iterates_tl'_closed 
   1.407 +                 tl'_closed iterates_tl'_closed
   1.408                   iterates_abs [OF _ relation1_tl] nth_replacement)
   1.409  done
   1.410  
   1.411 @@ -786,7 +769,7 @@
   1.412  
   1.413  lemma (in M_trivial) Member_in_M_iff [iff]:
   1.414       "M(Member(x,y)) <-> M(x) & M(y)"
   1.415 -by (simp add: Member_def) 
   1.416 +by (simp add: Member_def)
   1.417  
   1.418  constdefs
   1.419    is_Equal :: "[i=>o,i,i,i] => o"
   1.420 @@ -799,7 +782,7 @@
   1.421  by (simp add: is_Equal_def Equal_def)
   1.422  
   1.423  lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
   1.424 -by (simp add: Equal_def) 
   1.425 +by (simp add: Equal_def)
   1.426  
   1.427  constdefs
   1.428    is_Nand :: "[i=>o,i,i,i] => o"
   1.429 @@ -812,7 +795,7 @@
   1.430  by (simp add: is_Nand_def Nand_def)
   1.431  
   1.432  lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
   1.433 -by (simp add: Nand_def) 
   1.434 +by (simp add: Nand_def)
   1.435  
   1.436  constdefs
   1.437    is_Forall :: "[i=>o,i,i] => o"
   1.438 @@ -836,7 +819,7 @@
   1.439      --{* the instance of @{term formula_case} in @{term formula_rec}*}
   1.440     "formula_rec_case(a,b,c,d,h) ==
   1.441          formula_case (a, b,
   1.442 -                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
   1.443 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u,
   1.444                                h ` succ(depth(v)) ` v),
   1.445                  \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
   1.446  
   1.447 @@ -845,21 +828,21 @@
   1.448  neither of which is absolute.*}
   1.449  lemma (in M_trivial) formula_rec_eq:
   1.450    "p \<in> formula ==>
   1.451 -   formula_rec(a,b,c,d,p) = 
   1.452 +   formula_rec(a,b,c,d,p) =
   1.453     transrec (succ(depth(p)),
   1.454               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
   1.455  apply (simp add: formula_rec_case_def)
   1.456  apply (induct_tac p)
   1.457     txt{*Base case for @{term Member}*}
   1.458 -   apply (subst transrec, simp add: formula.intros) 
   1.459 +   apply (subst transrec, simp add: formula.intros)
   1.460    txt{*Base case for @{term Equal}*}
   1.461    apply (subst transrec, simp add: formula.intros)
   1.462   txt{*Inductive step for @{term Nand}*}
   1.463 - apply (subst transrec) 
   1.464 + apply (subst transrec)
   1.465   apply (simp add: succ_Un_distrib formula.intros)
   1.466  txt{*Inductive step for @{term Forall}*}
   1.467 -apply (subst transrec) 
   1.468 -apply (simp add: formula_imp_formula_N formula.intros) 
   1.469 +apply (subst transrec)
   1.470 +apply (simp add: formula_imp_formula_N formula.intros)
   1.471  done
   1.472  
   1.473  
   1.474 @@ -867,8 +850,8 @@
   1.475  constdefs
   1.476  
   1.477    is_depth :: "[i=>o,i,i] => o"
   1.478 -    "is_depth(M,p,n) == 
   1.479 -       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
   1.480 +    "is_depth(M,p,n) ==
   1.481 +       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
   1.482          is_formula_N(M,n,formula_n) & p \<notin> formula_n &
   1.483          successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn"
   1.484  
   1.485 @@ -876,7 +859,7 @@
   1.486  lemma (in M_datatypes) depth_abs [simp]:
   1.487       "[|p \<in> formula; n \<in> nat|] ==> is_depth(M,p,n) <-> n = depth(p)"
   1.488  apply (subgoal_tac "M(p) & M(n)")
   1.489 - prefer 2 apply (blast dest: transM)  
   1.490 + prefer 2 apply (blast dest: transM)
   1.491  apply (simp add: is_depth_def)
   1.492  apply (blast intro: formula_imp_formula_N nat_into_Ord formula_N_imp_eq_depth
   1.493               dest: formula_N_imp_depth_lt)
   1.494 @@ -885,43 +868,43 @@
   1.495  text{*Proof is trivial since @{term depth} returns natural numbers.*}
   1.496  lemma (in M_trivial) depth_closed [intro,simp]:
   1.497       "p \<in> formula ==> M(depth(p))"
   1.498 -by (simp add: nat_into_M) 
   1.499 +by (simp add: nat_into_M)
   1.500  
   1.501  
   1.502  subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
   1.503  
   1.504  constdefs
   1.505  
   1.506 - is_formula_case :: 
   1.507 + is_formula_case ::
   1.508      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   1.509    --{*no constraint on non-formulas*}
   1.510 -  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) == 
   1.511 -      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> 
   1.512 +  "is_formula_case(M, is_a, is_b, is_c, is_d, p, z) ==
   1.513 +      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
   1.514                        is_Member(M,x,y,p) --> is_a(x,y,z)) &
   1.515 -      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) --> 
   1.516 +      (\<forall>x[M]. \<forall>y[M]. finite_ordinal(M,x) --> finite_ordinal(M,y) -->
   1.517                        is_Equal(M,x,y,p) --> is_b(x,y,z)) &
   1.518 -      (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) --> 
   1.519 +      (\<forall>x[M]. \<forall>y[M]. mem_formula(M,x) --> mem_formula(M,y) -->
   1.520                       is_Nand(M,x,y,p) --> is_c(x,y,z)) &
   1.521        (\<forall>x[M]. mem_formula(M,x) --> is_Forall(M,x,p) --> is_d(x,z))"
   1.522  
   1.523 -lemma (in M_datatypes) formula_case_abs [simp]: 
   1.524 -     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b); 
   1.525 -         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d); 
   1.526 -         p \<in> formula; M(z) |] 
   1.527 -      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <-> 
   1.528 +lemma (in M_datatypes) formula_case_abs [simp]:
   1.529 +     "[| Relation2(M,nat,nat,is_a,a); Relation2(M,nat,nat,is_b,b);
   1.530 +         Relation2(M,formula,formula,is_c,c); Relation1(M,formula,is_d,d);
   1.531 +         p \<in> formula; M(z) |]
   1.532 +      ==> is_formula_case(M,is_a,is_b,is_c,is_d,p,z) <->
   1.533            z = formula_case(a,b,c,d,p)"
   1.534  apply (simp add: formula_into_M is_formula_case_def)
   1.535 -apply (erule formula.cases) 
   1.536 -   apply (simp_all add: Relation1_def Relation2_def) 
   1.537 +apply (erule formula.cases)
   1.538 +   apply (simp_all add: Relation1_def Relation2_def)
   1.539  done
   1.540  
   1.541  lemma (in M_datatypes) formula_case_closed [intro,simp]:
   1.542 -  "[|p \<in> formula; 
   1.543 -     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y)); 
   1.544 -     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y)); 
   1.545 -     \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y)); 
   1.546 +  "[|p \<in> formula;
   1.547 +     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y));
   1.548 +     \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(b(x,y));
   1.549 +     \<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> M(c(x,y));
   1.550       \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
   1.551 -by (erule formula.cases, simp_all) 
   1.552 +by (erule formula.cases, simp_all)
   1.553  
   1.554  
   1.555  subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
   1.556 @@ -930,7 +913,7 @@
   1.557    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.558      --{* predicate to relativize the functional @{term formula_rec}*}
   1.559     "is_formula_rec(M,MH,p,z)  ==
   1.560 -      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
   1.561 +      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) &
   1.562               successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
   1.563  
   1.564  
   1.565 @@ -939,16 +922,16 @@
   1.566  lemma (in M_datatypes) Relation1_formula_rec_case:
   1.567       "[|Relation2(M, nat, nat, is_a, a);
   1.568          Relation2(M, nat, nat, is_b, b);
   1.569 -        Relation2 (M, formula, formula, 
   1.570 +        Relation2 (M, formula, formula,
   1.571             is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
   1.572 -        Relation1(M, formula, 
   1.573 +        Relation1(M, formula,
   1.574             is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
   1.575 - 	M(h) |] 
   1.576 + 	M(h) |]
   1.577        ==> Relation1(M, formula,
   1.578                           is_formula_case (M, is_a, is_b, is_c, is_d),
   1.579                           formula_rec_case(a, b, c, d, h))"
   1.580 -apply (simp (no_asm) add: formula_rec_case_def Relation1_def) 
   1.581 -apply (simp add: formula_case_abs) 
   1.582 +apply (simp (no_asm) add: formula_rec_case_def Relation1_def)
   1.583 +apply (simp add: formula_case_abs)
   1.584  done
   1.585  
   1.586  
   1.587 @@ -970,12 +953,12 @@
   1.588        and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
   1.589                       ==> M(c(x, y, gx, gy))"
   1.590        and c_rel:
   1.591 -         "M(f) ==> 
   1.592 +         "M(f) ==>
   1.593            Relation2 (M, formula, formula, is_c(f),
   1.594               \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
   1.595        and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
   1.596        and d_rel:
   1.597 -         "M(f) ==> 
   1.598 +         "M(f) ==>
   1.599            Relation1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   1.600        and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
   1.601        and fr_lam_replace:
   1.602 @@ -986,7 +969,7 @@
   1.603  
   1.604  lemma (in Formula_Rec) formula_rec_case_closed:
   1.605      "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
   1.606 -by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed) 
   1.607 +by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed)
   1.608  
   1.609  lemma (in Formula_Rec) formula_rec_lam_closed:
   1.610      "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
   1.611 @@ -995,29 +978,29 @@
   1.612  lemma (in Formula_Rec) MH_rel2:
   1.613       "relation2 (M, MH,
   1.614               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
   1.615 -apply (simp add: relation2_def MH_def, clarify) 
   1.616 -apply (rule lambda_abs2) 
   1.617 +apply (simp add: relation2_def MH_def, clarify)
   1.618 +apply (rule lambda_abs2)
   1.619  apply (rule fr_lam_replace, assumption)
   1.620 -apply (rule Relation1_formula_rec_case)  
   1.621 -apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) 
   1.622 +apply (rule Relation1_formula_rec_case)
   1.623 +apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
   1.624  done
   1.625  
   1.626  lemma (in Formula_Rec) fr_transrec_closed:
   1.627      "n \<in> nat
   1.628       ==> M(transrec
   1.629            (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
   1.630 -by (simp add: transrec_closed [OF fr_replace MH_rel2]  
   1.631 -              nat_into_M formula_rec_lam_closed) 
   1.632 +by (simp add: transrec_closed [OF fr_replace MH_rel2]
   1.633 +              nat_into_M formula_rec_lam_closed)
   1.634  
   1.635  text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
   1.636  theorem (in Formula_Rec) formula_rec_closed:
   1.637      "p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
   1.638 -by (simp add: formula_rec_eq fr_transrec_closed 
   1.639 +by (simp add: formula_rec_eq fr_transrec_closed
   1.640                transM [OF _ formula_closed])
   1.641  
   1.642  theorem (in Formula_Rec) formula_rec_abs:
   1.643 -  "[| p \<in> formula; M(z)|] 
   1.644 -   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)" 
   1.645 +  "[| p \<in> formula; M(z)|]
   1.646 +   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)"
   1.647  by (simp add: is_formula_rec_def formula_rec_eq transM [OF _ formula_closed]
   1.648                transrec_abs [OF fr_replace MH_rel2] depth_type
   1.649                fr_transrec_closed formula_rec_lam_closed eq_commute)