deleted redundant material (quasiformula, ...) and rationalized
authorpaulson
Tue Sep 03 18:49:10 2002 +0200 (2002-09-03)
changeset 135576061d0045409
parent 13556 d17f6474eed0
child 13558 18acbbd4d225
deleted redundant material (quasiformula, ...) and rationalized
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Satisfies_absolute.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Sep 03 18:43:15 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Sep 03 18:49:10 2002 +0200
     1.3 @@ -861,99 +861,6 @@
     1.4     apply (simp_all add: Relativize1_def Relativize2_def) 
     1.5  done
     1.6  
     1.7 -
     1.8 -subsubsection{*@{term quasiformula}: For Case-Splitting with @{term formula_case'}*}
     1.9 -
    1.10 -constdefs
    1.11 -
    1.12 -  quasiformula :: "i => o"
    1.13 -    "quasiformula(p) == 
    1.14 -	(\<exists>x y. p = Member(x,y)) |
    1.15 -	(\<exists>x y. p = Equal(x,y)) |
    1.16 -	(\<exists>x y. p = Nand(x,y)) |
    1.17 -	(\<exists>x. p = Forall(x))"
    1.18 -
    1.19 -  is_quasiformula :: "[i=>o,i] => o"
    1.20 -    "is_quasiformula(M,p) == 
    1.21 -	(\<exists>x[M]. \<exists>y[M]. is_Member(M,x,y,p)) |
    1.22 -	(\<exists>x[M]. \<exists>y[M]. is_Equal(M,x,y,p)) |
    1.23 -	(\<exists>x[M]. \<exists>y[M]. is_Nand(M,x,y,p)) |
    1.24 -	(\<exists>x[M]. is_Forall(M,x,p))"
    1.25 -
    1.26 -lemma [iff]: "quasiformula(Member(x,y))"
    1.27 -by (simp add: quasiformula_def)
    1.28 -
    1.29 -lemma [iff]: "quasiformula(Equal(x,y))"
    1.30 -by (simp add: quasiformula_def)
    1.31 -
    1.32 -lemma [iff]: "quasiformula(Nand(x,y))"
    1.33 -by (simp add: quasiformula_def)
    1.34 -
    1.35 -lemma [iff]: "quasiformula(Forall(x))"
    1.36 -by (simp add: quasiformula_def)
    1.37 -
    1.38 -lemma formula_imp_quasiformula: "p \<in> formula ==> quasiformula(p)"
    1.39 -by (erule formula.cases, simp_all)
    1.40 -
    1.41 -lemma (in M_triv_axioms) quasiformula_abs [simp]: 
    1.42 -     "M(z) ==> is_quasiformula(M,z) <-> quasiformula(z)"
    1.43 -by (auto simp add: is_quasiformula_def quasiformula_def)
    1.44 -
    1.45 -constdefs
    1.46 -
    1.47 -  formula_case' :: "[[i,i]=>i, [i,i]=>i, [i,i]=>i, i=>i, i] => i"
    1.48 -    --{*A version of @{term formula_case} that's always defined.*}
    1.49 -    "formula_case'(a,b,c,d,p) == 
    1.50 -       if quasiformula(p) then formula_case(a,b,c,d,p) else 0"  
    1.51 -
    1.52 -  is_formula_case' :: 
    1.53 -      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
    1.54 -    --{*Returns 0 for non-formulas*}
    1.55 -    "is_formula_case'(M, is_a, is_b, is_c, is_d, p, z) == 
    1.56 -	(\<forall>x[M]. \<forall>y[M]. is_Member(M,x,y,p) --> is_a(x,y,z)) &
    1.57 -	(\<forall>x[M]. \<forall>y[M]. is_Equal(M,x,y,p) --> is_b(x,y,z)) &
    1.58 -	(\<forall>x[M]. \<forall>y[M]. is_Nand(M,x,y,p) --> is_c(x,y,z)) &
    1.59 -	(\<forall>x[M]. is_Forall(M,x,p) --> is_d(x,z)) &
    1.60 -        (is_quasiformula(M,p) | empty(M,z))"
    1.61 -
    1.62 -subsubsection{*@{term formula_case'}, the Modified Version of @{term formula_case}*}
    1.63 -
    1.64 -lemma formula_case'_Member [simp]:
    1.65 -     "formula_case'(a,b,c,d,Member(x,y)) = a(x,y)"
    1.66 -by (simp add: formula_case'_def)
    1.67 -
    1.68 -lemma formula_case'_Equal [simp]:
    1.69 -     "formula_case'(a,b,c,d,Equal(x,y)) = b(x,y)"
    1.70 -by (simp add: formula_case'_def)
    1.71 -
    1.72 -lemma formula_case'_Nand [simp]:
    1.73 -     "formula_case'(a,b,c,d,Nand(x,y)) = c(x,y)"
    1.74 -by (simp add: formula_case'_def)
    1.75 -
    1.76 -lemma formula_case'_Forall [simp]:
    1.77 -     "formula_case'(a,b,c,d,Forall(x)) = d(x)"
    1.78 -by (simp add: formula_case'_def)
    1.79 -
    1.80 -lemma non_formula_case: "~ quasiformula(x) ==> formula_case'(a,b,c,d,x) = 0" 
    1.81 -by (simp add: quasiformula_def formula_case'_def) 
    1.82 -
    1.83 -lemma formula_case'_eq_formula_case [simp]:
    1.84 -     "p \<in> formula ==>formula_case'(a,b,c,d,p) = formula_case(a,b,c,d,p)"
    1.85 -by (erule formula.cases, simp_all)
    1.86 -
    1.87 -lemma (in M_axioms) formula_case'_closed [intro,simp]:
    1.88 -  "[|M(p); \<forall>x[M]. \<forall>y[M]. M(a(x,y)); 
    1.89 -           \<forall>x[M]. \<forall>y[M]. M(b(x,y)); 
    1.90 -           \<forall>x[M]. \<forall>y[M]. M(c(x,y)); 
    1.91 -           \<forall>x[M]. M(d(x))|] ==> M(formula_case'(a,b,c,d,p))"
    1.92 -apply (case_tac "quasiformula(p)") 
    1.93 - apply (simp add: quasiformula_def, force) 
    1.94 -apply (simp add: non_formula_case) 
    1.95 -done
    1.96 -
    1.97 -text{*Compared with @{text formula_case_closed'}, the premise on @{term p} is
    1.98 -      stronger while the other premises are weaker, incorporating typing 
    1.99 -      information.*}
   1.100  lemma (in M_datatypes) formula_case_closed [intro,simp]:
   1.101    "[|p \<in> formula; 
   1.102       \<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> M(a(x,y)); 
   1.103 @@ -962,46 +869,6 @@
   1.104       \<forall>x[M]. x\<in>formula --> M(d(x))|] ==> M(formula_case(a,b,c,d,p))"
   1.105  by (erule formula.cases, simp_all) 
   1.106  
   1.107 -lemma (in M_triv_axioms) formula_case'_abs [simp]: 
   1.108 -     "[| relativize2(M,is_a,a); relativize2(M,is_b,b); 
   1.109 -         relativize2(M,is_c,c); relativize1(M,is_d,d); M(p); M(z) |] 
   1.110 -      ==> is_formula_case'(M,is_a,is_b,is_c,is_d,p,z) <-> 
   1.111 -          z = formula_case'(a,b,c,d,p)"
   1.112 -apply (case_tac "quasiformula(p)") 
   1.113 - prefer 2 
   1.114 - apply (simp add: is_formula_case'_def non_formula_case) 
   1.115 - apply (force simp add: quasiformula_def) 
   1.116 -apply (simp add: quasiformula_def is_formula_case'_def)
   1.117 -apply (elim disjE exE) 
   1.118 - apply (simp_all add: relativize1_def relativize2_def) 
   1.119 -done
   1.120 -
   1.121 -
   1.122 -text{*Express @{term formula_rec} without using @{term rank} or @{term Vset},
   1.123 -neither of which is absolute.*}
   1.124 -lemma (in M_triv_axioms) formula_rec_eq:
   1.125 -  "p \<in> formula ==>
   1.126 -   formula_rec(a,b,c,d,p) = 
   1.127 -   transrec (succ(depth(p)),
   1.128 -      \<lambda>x h. Lambda (formula,
   1.129 -             formula_case' (a, b,
   1.130 -                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
   1.131 -                              h ` succ(depth(v)) ` v),
   1.132 -                \<lambda>u. d(u, h ` succ(depth(u)) ` u)))) 
   1.133 -   ` p"
   1.134 -apply (induct_tac p)
   1.135 -   txt{*Base case for @{term Member}*}
   1.136 -   apply (subst transrec, simp add: formula.intros) 
   1.137 -  txt{*Base case for @{term Equal}*}
   1.138 -  apply (subst transrec, simp add: formula.intros)
   1.139 - txt{*Inductive step for @{term Nand}*}
   1.140 - apply (subst transrec) 
   1.141 - apply (simp add: succ_Un_distrib formula.intros)
   1.142 -txt{*Inductive step for @{term Forall}*}
   1.143 -apply (subst transrec) 
   1.144 -apply (simp add: formula_imp_formula_N formula.intros) 
   1.145 -done
   1.146 -
   1.147  
   1.148  subsection{*Absoluteness for the Formula Operator @{term depth}*}
   1.149  constdefs
   1.150 @@ -1028,4 +895,134 @@
   1.151  by (simp add: nat_into_M) 
   1.152  
   1.153  
   1.154 +subsection {*Absoluteness for @{term formula_rec}*}
   1.155 +
   1.156 +constdefs
   1.157 +
   1.158 +  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
   1.159 +    --{* the instance of @{term formula_case} in @{term formula_rec}*}
   1.160 +   "formula_rec_case(a,b,c,d,h) ==
   1.161 +        formula_case (a, b,
   1.162 +                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
   1.163 +                              h ` succ(depth(v)) ` v),
   1.164 +                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
   1.165 +
   1.166 +  is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.167 +    --{* predicate to relativize the functional @{term formula_rec}*}
   1.168 +   "is_formula_rec(M,MH,p,z)  ==
   1.169 +      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
   1.170 +             successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
   1.171 +
   1.172 +text{*Unfold @{term formula_rec} to @{term formula_rec_case}.
   1.173 +     Express @{term formula_rec} without using @{term rank} or @{term Vset},
   1.174 +neither of which is absolute.*}
   1.175 +lemma (in M_triv_axioms) formula_rec_eq:
   1.176 +  "p \<in> formula ==>
   1.177 +   formula_rec(a,b,c,d,p) = 
   1.178 +   transrec (succ(depth(p)),
   1.179 +             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
   1.180 +apply (simp add: formula_rec_case_def)
   1.181 +apply (induct_tac p)
   1.182 +   txt{*Base case for @{term Member}*}
   1.183 +   apply (subst transrec, simp add: formula.intros) 
   1.184 +  txt{*Base case for @{term Equal}*}
   1.185 +  apply (subst transrec, simp add: formula.intros)
   1.186 + txt{*Inductive step for @{term Nand}*}
   1.187 + apply (subst transrec) 
   1.188 + apply (simp add: succ_Un_distrib formula.intros)
   1.189 +txt{*Inductive step for @{term Forall}*}
   1.190 +apply (subst transrec) 
   1.191 +apply (simp add: formula_imp_formula_N formula.intros) 
   1.192 +done
   1.193 +
   1.194 +
   1.195 +text{*Sufficient conditions to relative the instance of @{term formula_case}
   1.196 +      in @{term formula_rec}*}
   1.197 +lemma (in M_datatypes) Relativize1_formula_rec_case:
   1.198 +     "[|Relativize2(M, nat, nat, is_a, a);
   1.199 +        Relativize2(M, nat, nat, is_b, b);
   1.200 +        Relativize2 (M, formula, formula, 
   1.201 +           is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
   1.202 +        Relativize1(M, formula, 
   1.203 +           is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
   1.204 + 	M(h) |] 
   1.205 +      ==> Relativize1(M, formula,
   1.206 +                         is_formula_case (M, is_a, is_b, is_c, is_d),
   1.207 +                         formula_rec_case(a, b, c, d, h))"
   1.208 +apply (simp (no_asm) add: formula_rec_case_def Relativize1_def) 
   1.209 +apply (simp add: formula_case_abs) 
   1.210 +done
   1.211 +
   1.212 +
   1.213 +text{*This locale packages the premises of the following theorems,
   1.214 +      which is the normal purpose of locales.  It doesn't accumulate
   1.215 +      constraints on the class @{term M}, as in most of this deveopment.*}
   1.216 +locale Formula_Rec = M_eclose +
   1.217 +  fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
   1.218 +  defines
   1.219 +      "MH(u::i,f,z) ==
   1.220 +	\<forall>fml[M]. is_formula(M,fml) -->
   1.221 +             is_lambda
   1.222 +	 (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
   1.223 +
   1.224 +  assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
   1.225 +      and a_rel:    "Relativize2(M, nat, nat, is_a, a)"
   1.226 +      and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))"
   1.227 +      and b_rel:    "Relativize2(M, nat, nat, is_b, b)"
   1.228 +      and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
   1.229 +                     ==> M(c(x, y, gx, gy))"
   1.230 +      and c_rel:
   1.231 +         "M(f) ==> 
   1.232 +          Relativize2 (M, formula, formula, is_c(f),
   1.233 +             \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
   1.234 +      and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
   1.235 +      and d_rel:
   1.236 +         "M(f) ==> 
   1.237 +          Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
   1.238 +      and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
   1.239 +      and fr_lam_replace:
   1.240 +           "M(g) ==>
   1.241 +            strong_replacement
   1.242 +	      (M, \<lambda>x y. x \<in> formula &
   1.243 +		  y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)";
   1.244 +
   1.245 +lemma (in Formula_Rec) formula_rec_case_closed:
   1.246 +    "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
   1.247 +by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed) 
   1.248 +
   1.249 +lemma (in Formula_Rec) formula_rec_lam_closed:
   1.250 +    "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
   1.251 +by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)
   1.252 +
   1.253 +lemma (in Formula_Rec) MH_rel2:
   1.254 +     "relativize2 (M, MH,
   1.255 +             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
   1.256 +apply (simp add: relativize2_def MH_def, clarify) 
   1.257 +apply (rule lambda_abs2) 
   1.258 +apply (rule fr_lam_replace, assumption)
   1.259 +apply (rule Relativize1_formula_rec_case)  
   1.260 +apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) 
   1.261 +done
   1.262 +
   1.263 +lemma (in Formula_Rec) fr_transrec_closed:
   1.264 +    "n \<in> nat
   1.265 +     ==> M(transrec
   1.266 +          (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
   1.267 +by (simp add: transrec_closed [OF fr_replace MH_rel2]  
   1.268 +              nat_into_M formula_rec_lam_closed) 
   1.269 +
   1.270 +text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
   1.271 +theorem (in Formula_Rec) formula_rec_closed:
   1.272 +    "p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
   1.273 +by (simp add: formula_rec_eq fr_transrec_closed 
   1.274 +              transM [OF _ formula_closed])
   1.275 +
   1.276 +theorem (in Formula_Rec) formula_rec_abs:
   1.277 +  "[| p \<in> formula; M(z)|] 
   1.278 +   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)" 
   1.279 +by (simp add: is_formula_rec_def formula_rec_eq transM [OF _ formula_closed]
   1.280 +              transrec_abs [OF fr_replace MH_rel2] depth_type
   1.281 +              fr_transrec_closed formula_rec_lam_closed eq_commute)
   1.282 +
   1.283 +
   1.284  end
     2.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Sep 03 18:43:15 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Sep 03 18:49:10 2002 +0200
     2.3 @@ -171,122 +171,6 @@
     2.4  
     2.5  
     2.6  
     2.7 -subsection {*Absoluteness for @{term formula_rec}*}
     2.8 -
     2.9 -constdefs
    2.10 -
    2.11 -  formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
    2.12 -    --{* the instance of @{term formula_case} in @{term formula_rec}*}
    2.13 -   "formula_rec_case(a,b,c,d,h) ==
    2.14 -        formula_case (a, b,
    2.15 -                \<lambda>u v. c(u, v, h ` succ(depth(u)) ` u, 
    2.16 -                              h ` succ(depth(v)) ` v),
    2.17 -                \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
    2.18 -
    2.19 -  is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
    2.20 -    --{* predicate to relativize the functional @{term formula_rec}*}
    2.21 -   "is_formula_rec(M,MH,p,z)  ==
    2.22 -      \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
    2.23 -             successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
    2.24 -
    2.25 -text{*Unfold @{term formula_rec} to @{term formula_rec_case}*}
    2.26 -lemma (in M_triv_axioms) formula_rec_eq2:
    2.27 -  "p \<in> formula ==>
    2.28 -   formula_rec(a,b,c,d,p) = 
    2.29 -   transrec (succ(depth(p)),
    2.30 -             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h))) ` p"
    2.31 -by (simp add: formula_rec_eq  formula_rec_case_def)
    2.32 -
    2.33 -
    2.34 -text{*Sufficient conditions to relative the instance of @{term formula_case}
    2.35 -      in @{term formula_rec}*}
    2.36 -lemma (in M_datatypes) Relativize1_formula_rec_case:
    2.37 -     "[|Relativize2(M, nat, nat, is_a, a);
    2.38 -        Relativize2(M, nat, nat, is_b, b);
    2.39 -        Relativize2 (M, formula, formula, 
    2.40 -           is_c, \<lambda>u v. c(u, v, h`succ(depth(u))`u, h`succ(depth(v))`v));
    2.41 -        Relativize1(M, formula, 
    2.42 -           is_d, \<lambda>u. d(u, h ` succ(depth(u)) ` u));
    2.43 - 	M(h) |] 
    2.44 -      ==> Relativize1(M, formula,
    2.45 -                         is_formula_case (M, is_a, is_b, is_c, is_d),
    2.46 -                         formula_rec_case(a, b, c, d, h))"
    2.47 -apply (simp (no_asm) add: formula_rec_case_def Relativize1_def) 
    2.48 -apply (simp add: formula_case_abs) 
    2.49 -done
    2.50 -
    2.51 -
    2.52 -text{*This locale packages the premises of the following theorems,
    2.53 -      which is the normal purpose of locales.  It doesn't accumulate
    2.54 -      constraints on the class @{term M}, as in most of this deveopment.*}
    2.55 -locale Formula_Rec = M_eclose +
    2.56 -  fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
    2.57 -  defines
    2.58 -      "MH(u::i,f,z) ==
    2.59 -	\<forall>fml[M]. is_formula(M,fml) -->
    2.60 -             is_lambda
    2.61 -	 (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
    2.62 -
    2.63 -  assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
    2.64 -      and a_rel:    "Relativize2(M, nat, nat, is_a, a)"
    2.65 -      and b_closed: "[|x\<in>nat; y\<in>nat|] ==> M(b(x,y))"
    2.66 -      and b_rel:    "Relativize2(M, nat, nat, is_b, b)"
    2.67 -      and c_closed: "[|x \<in> formula; y \<in> formula; M(gx); M(gy)|]
    2.68 -                     ==> M(c(x, y, gx, gy))"
    2.69 -      and c_rel:
    2.70 -         "M(f) ==> 
    2.71 -          Relativize2 (M, formula, formula, is_c(f),
    2.72 -             \<lambda>u v. c(u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))"
    2.73 -      and d_closed: "[|x \<in> formula; M(gx)|] ==> M(d(x, gx))"
    2.74 -      and d_rel:
    2.75 -         "M(f) ==> 
    2.76 -          Relativize1(M, formula, is_d(f), \<lambda>u. d(u, f ` succ(depth(u)) ` u))"
    2.77 -      and fr_replace: "n \<in> nat ==> transrec_replacement(M,MH,n)"
    2.78 -      and fr_lam_replace:
    2.79 -           "M(g) ==>
    2.80 -            strong_replacement
    2.81 -	      (M, \<lambda>x y. x \<in> formula &
    2.82 -		  y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)";
    2.83 -
    2.84 -lemma (in Formula_Rec) formula_rec_case_closed:
    2.85 -    "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
    2.86 -by (simp add: formula_rec_case_def a_closed b_closed c_closed d_closed) 
    2.87 -
    2.88 -lemma (in Formula_Rec) formula_rec_lam_closed:
    2.89 -    "M(g) ==> M(Lambda (formula, formula_rec_case(a,b,c,d,g)))"
    2.90 -by (simp add: lam_closed2 fr_lam_replace formula_rec_case_closed)
    2.91 -
    2.92 -lemma (in Formula_Rec) MH_rel2:
    2.93 -     "relativize2 (M, MH,
    2.94 -             \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
    2.95 -apply (simp add: relativize2_def MH_def, clarify) 
    2.96 -apply (rule lambda_abs2) 
    2.97 -apply (rule fr_lam_replace, assumption)
    2.98 -apply (rule Relativize1_formula_rec_case)  
    2.99 -apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed) 
   2.100 -done
   2.101 -
   2.102 -lemma (in Formula_Rec) fr_transrec_closed:
   2.103 -    "n \<in> nat
   2.104 -     ==> M(transrec
   2.105 -          (n, \<lambda>x h. Lambda(formula, formula_rec_case(a, b, c, d, h))))"
   2.106 -by (simp add: transrec_closed [OF fr_replace MH_rel2]  
   2.107 -              nat_into_M formula_rec_lam_closed) 
   2.108 -
   2.109 -text{*The main two results: @{term formula_rec} is absolute for @{term M}.*}
   2.110 -theorem (in Formula_Rec) formula_rec_closed:
   2.111 -    "p \<in> formula ==> M(formula_rec(a,b,c,d,p))"
   2.112 -by (simp add: formula_rec_eq2 fr_transrec_closed 
   2.113 -              transM [OF _ formula_closed])
   2.114 -
   2.115 -theorem (in Formula_Rec) formula_rec_abs:
   2.116 -  "[| p \<in> formula; M(z)|] 
   2.117 -   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)" 
   2.118 -by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed]
   2.119 -              transrec_abs [OF fr_replace MH_rel2] depth_type
   2.120 -              fr_transrec_closed formula_rec_lam_closed eq_commute)
   2.121 -
   2.122 -
   2.123  subsection {*Absoluteness for the Function @{term satisfies}*}
   2.124  
   2.125  constdefs