Polishing.
authorpaulson
Fri Nov 08 10:34:40 2002 +0100 (2002-11-08)
changeset 13702c7cf8fa66534
parent 13701 0a9228532106
child 13703 a36a0d417133
Polishing.
lambda_abs2 doesn't need an instance of replacement
various renamings & restructurings
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Fri Nov 08 10:28:29 2002 +0100
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Fri Nov 08 10:34:40 2002 +0100
     1.3 @@ -220,9 +220,7 @@
     1.4  which are lists built over @{term "A"}.  We combine it with the enumeration of
     1.5  formulas.  The order type of the resulting wellordering gives us a map from
     1.6  (environment, formula) pairs into the ordinals.  For each member of @{term
     1.7 -"DPow(A)"}, we take the minimum such ordinal.  This yields a wellordering of
     1.8 -@{term "DPow(A)-A"}, namely the set of elements just introduced, which we then
     1.9 -extend to the full set @{term "DPow(A)"}.*}
    1.10 +"DPow(A)"}, we take the minimum such ordinal.*}
    1.11  
    1.12  constdefs
    1.13    env_form_r :: "[i,i,i]=>i"
    1.14 @@ -236,25 +234,21 @@
    1.15     "env_form_map(f,r,A,z)
    1.16        == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
    1.17  
    1.18 -  DPow_new_ord :: "[i,i,i,i,i]=>o"
    1.19 +  DPow_ord :: "[i,i,i,i,i]=>o"
    1.20      --{*predicate that holds if @{term k} is a valid index for @{term X}*}
    1.21 -   "DPow_new_ord(f,r,A,X,k) ==
    1.22 +   "DPow_ord(f,r,A,X,k) ==
    1.23             \<exists>env \<in> list(A). \<exists>p \<in> formula.
    1.24               arity(p) \<le> succ(length(env)) &
    1.25               X = {x\<in>A. sats(A, p, Cons(x,env))} &
    1.26               env_form_map(f,r,A,<env,p>) = k"
    1.27  
    1.28 -  DPow_new_least :: "[i,i,i,i]=>i"
    1.29 +  DPow_least :: "[i,i,i,i]=>i"
    1.30      --{*function yielding the smallest index for @{term X}*}
    1.31 -   "DPow_new_least(f,r,A,X) == \<mu>k. DPow_new_ord(f,r,A,X,k)"
    1.32 -
    1.33 -  DPow_new_r :: "[i,i,i]=>i"
    1.34 -    --{*a wellordering on the difference set @{term "DPow(A)-A"}*}
    1.35 -   "DPow_new_r(f,r,A) == measure(DPow(A)-A, DPow_new_least(f,r,A))"
    1.36 +   "DPow_least(f,r,A,X) == \<mu>k. DPow_ord(f,r,A,X,k)"
    1.37  
    1.38    DPow_r :: "[i,i,i]=>i"
    1.39      --{*a wellordering on @{term "DPow(A)"}*}
    1.40 -   "DPow_r(f,r,A) == (DPow_new_r(f,r,A) Un (A * (DPow(A)-A))) Un r"
    1.41 +   "DPow_r(f,r,A) == measure(DPow(A), DPow_least(f,r,A))"
    1.42  
    1.43  
    1.44  lemma (in Nat_Times_Nat) well_ord_env_form_r:
    1.45 @@ -267,23 +261,23 @@
    1.46       ==> Ord(env_form_map(fn,r,A,z))"
    1.47  by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r)
    1.48  
    1.49 -lemma DPow_imp_ex_DPow_new_ord:
    1.50 -    "X \<in> DPow(A) ==> \<exists>k. DPow_new_ord(fn,r,A,X,k)"
    1.51 -apply (simp add: DPow_new_ord_def)
    1.52 +lemma DPow_imp_ex_DPow_ord:
    1.53 +    "X \<in> DPow(A) ==> \<exists>k. DPow_ord(fn,r,A,X,k)"
    1.54 +apply (simp add: DPow_ord_def)
    1.55  apply (blast dest!: DPowD)
    1.56  done
    1.57  
    1.58 -lemma (in Nat_Times_Nat) DPow_new_ord_imp_Ord:
    1.59 -     "[|DPow_new_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)"
    1.60 -apply (simp add: DPow_new_ord_def, clarify)
    1.61 +lemma (in Nat_Times_Nat) DPow_ord_imp_Ord:
    1.62 +     "[|DPow_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)"
    1.63 +apply (simp add: DPow_ord_def, clarify)
    1.64  apply (simp add: Ord_env_form_map)
    1.65  done
    1.66  
    1.67 -lemma (in Nat_Times_Nat) DPow_imp_DPow_new_least:
    1.68 +lemma (in Nat_Times_Nat) DPow_imp_DPow_least:
    1.69      "[|X \<in> DPow(A); well_ord(A,r)|]
    1.70 -     ==> DPow_new_ord(fn, r, A, X, DPow_new_least(fn,r,A,X))"
    1.71 -apply (simp add: DPow_new_least_def)
    1.72 -apply (blast dest: DPow_imp_ex_DPow_new_ord intro: DPow_new_ord_imp_Ord LeastI)
    1.73 +     ==> DPow_ord(fn, r, A, X, DPow_least(fn,r,A,X))"
    1.74 +apply (simp add: DPow_least_def)
    1.75 +apply (blast dest: DPow_imp_ex_DPow_ord intro: DPow_ord_imp_Ord LeastI)
    1.76  done
    1.77  
    1.78  lemma (in Nat_Times_Nat) env_form_map_inject:
    1.79 @@ -295,63 +289,26 @@
    1.80                                  OF well_ord_env_form_r], assumption+)
    1.81  done
    1.82  
    1.83 -
    1.84 -lemma (in Nat_Times_Nat) DPow_new_ord_unique:
    1.85 -    "[|DPow_new_ord(fn,r,A,X,k); DPow_new_ord(fn,r,A,Y,k); well_ord(A,r)|]
    1.86 +lemma (in Nat_Times_Nat) DPow_ord_unique:
    1.87 +    "[|DPow_ord(fn,r,A,X,k); DPow_ord(fn,r,A,Y,k); well_ord(A,r)|]
    1.88       ==> X=Y"
    1.89 -apply (simp add: DPow_new_ord_def, clarify)
    1.90 +apply (simp add: DPow_ord_def, clarify)
    1.91  apply (drule env_form_map_inject, auto)
    1.92  done
    1.93  
    1.94 -lemma (in Nat_Times_Nat) well_ord_DPow_new_r:
    1.95 -    "well_ord(A,r) ==> well_ord(DPow(A)-A, DPow_new_r(fn,r,A))"
    1.96 -apply (simp add: DPow_new_r_def)
    1.97 +lemma (in Nat_Times_Nat) well_ord_DPow_r:
    1.98 +    "well_ord(A,r) ==> well_ord(DPow(A), DPow_r(fn,r,A))"
    1.99 +apply (simp add: DPow_r_def)
   1.100  apply (rule well_ord_measure)
   1.101 - apply (simp add: DPow_new_least_def Ord_Least, clarify)
   1.102 -apply (drule DPow_imp_DPow_new_least, assumption)+
   1.103 + apply (simp add: DPow_least_def Ord_Least)
   1.104 +apply (drule DPow_imp_DPow_least, assumption)+
   1.105  apply simp
   1.106 -apply (blast intro: DPow_new_ord_unique)
   1.107 -done
   1.108 -
   1.109 -lemma DPow_new_r_subset: "DPow_new_r(f,r,A) <= (DPow(A)-A) * (DPow(A)-A)"
   1.110 -by (simp add: DPow_new_r_def measure_type)
   1.111 -
   1.112 -lemma (in Nat_Times_Nat) linear_DPow_r:
   1.113 -    "well_ord(A,r)
   1.114 -     ==> linear(DPow(A), DPow_r(fn, r, A))"
   1.115 -apply (frule well_ord_DPow_new_r)
   1.116 -apply (drule well_ord_is_linear)+
   1.117 -apply (auto simp add: linear_def DPow_r_def)
   1.118 -done
   1.119 -
   1.120 -
   1.121 -lemma (in Nat_Times_Nat) wf_DPow_new_r:
   1.122 -    "well_ord(A,r) ==> wf(DPow_new_r(fn,r,A))"
   1.123 -apply (rule well_ord_DPow_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf],
   1.124 -       assumption+)
   1.125 -apply (rule DPow_new_r_subset)
   1.126 -done
   1.127 -
   1.128 -lemma (in Nat_Times_Nat) well_ord_DPow_r:
   1.129 -    "[|well_ord(A,r); r \<subseteq> A * A|]
   1.130 -     ==> well_ord(DPow(A), DPow_r(fn,r,A))"
   1.131 -apply (rule well_ordI [OF wf_imp_wf_on])
   1.132 - prefer 2 apply (blast intro: linear_DPow_r)
   1.133 -apply (simp add: DPow_r_def)
   1.134 -apply (rule wf_Un)
   1.135 -  apply (cut_tac DPow_new_r_subset [of fn r A], blast)
   1.136 - apply (rule wf_Un)
   1.137 -   apply (cut_tac DPow_new_r_subset [of fn r A], blast)
   1.138 -  apply (blast intro: wf_DPow_new_r)
   1.139 - apply (simp add: wf_times Diff_disjoint)
   1.140 -apply (blast intro: well_ord_is_wf wf_on_imp_wf)
   1.141 +apply (blast intro: DPow_ord_unique)
   1.142  done
   1.143  
   1.144  lemma (in Nat_Times_Nat) DPow_r_type:
   1.145 -    "[|r \<subseteq> A * A; A \<subseteq> DPow(A)|]
   1.146 -     ==> DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)"
   1.147 -apply (simp add: DPow_r_def DPow_new_r_def measure_def, blast)
   1.148 -done		
   1.149 +    "DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)"
   1.150 +by (simp add: DPow_r_def measure_def, blast)
   1.151  
   1.152  
   1.153  subsection{*Limit Construction for Well-Orderings*}
   1.154 @@ -362,29 +319,21 @@
   1.155  
   1.156  constdefs
   1.157    rlimit :: "[i,i=>i]=>i"
   1.158 -  --{*expresses the wellordering at limit ordinals.*}
   1.159 +  --{*Expresses the wellordering at limit ordinals.  The conditional
   1.160 +      lets us remove the premise @{term "Limit(i)"} from some theorems.*}
   1.161      "rlimit(i,r) ==
   1.162 -       {z: Lset(i) * Lset(i).
   1.163 -        \<exists>x' x. z = <x',x> &
   1.164 -               (lrank(x') < lrank(x) |
   1.165 -                (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}"
   1.166 +       if Limit(i) then 
   1.167 +	 {z: Lset(i) * Lset(i).
   1.168 +	  \<exists>x' x. z = <x',x> &
   1.169 +		 (lrank(x') < lrank(x) |
   1.170 +		  (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}
   1.171 +       else 0"
   1.172  
   1.173    Lset_new :: "i=>i"
   1.174    --{*This constant denotes the set of elements introduced at level
   1.175        @{term "succ(i)"}*}
   1.176      "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
   1.177  
   1.178 -lemma Lset_new_iff_lrank_eq:
   1.179 -     "Ord(i) ==> x \<in> Lset_new(i) <-> L(x) & lrank(x) = i"
   1.180 -by (auto simp add: Lset_new_def Lset_iff_lrank_lt)
   1.181 -
   1.182 -lemma Lset_new_eq:
   1.183 -     "Ord(i) ==> Lset_new(i) = Lset(succ(i)) - Lset(i)"
   1.184 -apply (rule equality_iffI)
   1.185 -apply (simp add: Lset_new_iff_lrank_eq Lset_iff_lrank_lt, auto)
   1.186 -apply (blast elim: leE)
   1.187 -done
   1.188 -
   1.189  lemma Limit_Lset_eq2:
   1.190      "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))"
   1.191  apply (simp add: Limit_Lset_eq)
   1.192 @@ -404,11 +353,14 @@
   1.193      "wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))"
   1.194  apply (simp add: wf_on_def Lset_new_def)
   1.195  apply (erule wf_subset)
   1.196 -apply (force simp add: rlimit_def)
   1.197 +apply (simp add: rlimit_def, force)
   1.198  done
   1.199  
   1.200  lemma wf_on_rlimit:
   1.201 -    "[|Limit(i); \<forall>j<i. wf[Lset(j)](r(j)) |] ==> wf[Lset(i)](rlimit(i,r))"
   1.202 +    "(\<forall>j<i. wf[Lset(j)](r(j))) ==> wf[Lset(i)](rlimit(i,r))"
   1.203 +apply (case_tac "Limit(i)") 
   1.204 + prefer 2
   1.205 + apply (simp add: rlimit_def wf_on_any_0)
   1.206  apply (simp add: Limit_Lset_eq2)
   1.207  apply (rule wf_on_Union)
   1.208    apply (rule wf_imp_wf_on [OF wf_Memrel [of i]])
   1.209 @@ -438,51 +390,33 @@
   1.210  by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf
   1.211                             linear_rlimit well_ord_is_linear)
   1.212  
   1.213 +lemma rlimit_cong:
   1.214 +     "(!!j. j<i ==> r'(j) = r(j)) ==> rlimit(i,r) = rlimit(i,r')"
   1.215 +apply (simp add: rlimit_def, clarify) 
   1.216 +apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+
   1.217 +apply (simp add: Limit_is_Ord Lset_lrank_lt)
   1.218 +done
   1.219 +
   1.220  
   1.221  subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
   1.222  
   1.223  constdefs
   1.224   L_r :: "[i, i] => i"
   1.225 -  "L_r(f,i) ==
   1.226 -      transrec(i, \<lambda>x r.
   1.227 -         if x=0 then 0
   1.228 -         else if Limit(x) then rlimit(x, \<lambda>y. r`y)
   1.229 -         else DPow_r(f, r ` Arith.pred(x), Lset(Arith.pred(x))))"
   1.230 +  "L_r(f) == %i.
   1.231 +      transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), 
   1.232 +                \<lambda>x r. rlimit(x, \<lambda>y. r`y))"
   1.233  
   1.234  subsubsection{*The Corresponding Recursion Equations*}
   1.235  lemma [simp]: "L_r(f,0) = 0"
   1.236 -by (simp add: def_transrec [OF L_r_def])
   1.237 +by (simp add: L_r_def)
   1.238  
   1.239 -lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))"
   1.240 -by (simp add: def_transrec [OF L_r_def])
   1.241 +lemma [simp]: "L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))"
   1.242 +by (simp add: L_r_def)
   1.243  
   1.244 -text{*Needed to handle the limit case*}
   1.245 -lemma L_r_eq:
   1.246 -     "Ord(i) ==>
   1.247 -      L_r(f, i) =
   1.248 -      (if i = 0 then 0
   1.249 -       else if Limit(i) then rlimit(i, op `(Lambda(i, L_r(f))))
   1.250 -       else DPow_r (f, Lambda(i, L_r(f)) ` Arith.pred(i),
   1.251 -                    Lset(Arith.pred(i))))"
   1.252 -apply (induct i rule: trans_induct3_rule)
   1.253 -apply (simp_all add: def_transrec [OF L_r_def])
   1.254 -done
   1.255 -
   1.256 -lemma rlimit_eqI:
   1.257 -     "[|Limit(i); \<forall>j<i. r'(j) = r(j)|] ==> rlimit(i,r) = rlimit(i,r')"
   1.258 -apply (simp add: rlimit_def)
   1.259 -apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+
   1.260 -apply (simp add: Limit_is_Ord Lset_lrank_lt)
   1.261 -done
   1.262 -
   1.263 -text{*I don't know why the limit case is so complicated.*}
   1.264 +text{*The limit case is non-trivial because of the distinction between
   1.265 +object-level and meta-level abstraction.*}
   1.266  lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))"
   1.267 -apply (simp add: Limit_nonzero def_transrec [OF L_r_def])
   1.268 -apply (rule rlimit_eqI, assumption)
   1.269 -apply (rule oallI)
   1.270 -apply (frule lt_Ord)
   1.271 -apply (simp only: beta ltD L_r_eq [symmetric])
   1.272 -done
   1.273 +by (simp cong: rlimit_cong add: transrec3_Limit L_r_def ltD)
   1.274  
   1.275  lemma (in Nat_Times_Nat) L_r_type:
   1.276      "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)"
     2.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Nov 08 10:28:29 2002 +0100
     2.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Nov 08 10:34:40 2002 +0100
     2.3 @@ -980,7 +980,6 @@
     2.4               \<lambda>x h. Lambda (formula, formula_rec_case(a,b,c,d,h)))"
     2.5  apply (simp add: relation2_def MH_def, clarify)
     2.6  apply (rule lambda_abs2)
     2.7 -apply (rule fr_lam_replace, assumption)
     2.8  apply (rule Relation1_formula_rec_case)
     2.9  apply (simp_all add: a_rel b_rel c_rel d_rel formula_rec_case_closed)
    2.10  done
     3.1 --- a/src/ZF/Constructible/Internalize.thy	Fri Nov 08 10:28:29 2002 +0100
     3.2 +++ b/src/ZF/Constructible/Internalize.thy	Fri Nov 08 10:34:40 2002 +0100
     3.3 @@ -303,8 +303,8 @@
     3.4  
     3.5  theorem is_lambda_reflection:
     3.6    assumes is_b_reflection:
     3.7 -    "!!f' f g h. REFLECTS[\<lambda>x. is_b(L, f'(x), f(x), g(x)), 
     3.8 -                     \<lambda>i x. is_b(**Lset(i), f'(x), f(x), g(x))]"
     3.9 +    "!!f g h. REFLECTS[\<lambda>x. is_b(L, f(x), g(x), h(x)), 
    3.10 +                     \<lambda>i x. is_b(**Lset(i), f(x), g(x), h(x))]"
    3.11    shows "REFLECTS[\<lambda>x. is_lambda(L, A(x), is_b(L,x), f(x)), 
    3.12                 \<lambda>i x. is_lambda(**Lset(i), A(x), is_b(**Lset(i),x), f(x))]"
    3.13  apply (simp (no_asm_use) only: is_lambda_def)
     4.1 --- a/src/ZF/Constructible/Relative.thy	Fri Nov 08 10:28:29 2002 +0100
     4.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Nov 08 10:34:40 2002 +0100
     4.3 @@ -493,7 +493,9 @@
     4.4  by (blast intro: transM)
     4.5  
     4.6  text{*Simplifies proofs of equalities when there's an iff-equality
     4.7 -      available for rewriting, universally quantified over M. *}
     4.8 +      available for rewriting, universally quantified over M.  
     4.9 +      But it's not the only way to prove such equalities: its
    4.10 +      premises @{term "M(A)"} and  @{term "M(B)"} can be too strong.*}
    4.11  lemma (in M_trivial) M_equalityI:
    4.12       "[| !!x. M(x) ==> x\<in>A <-> x\<in>B; M(A); M(B) |] ==> A=B"
    4.13  by (blast intro!: equalityI dest: transM)
    4.14 @@ -669,15 +671,17 @@
    4.15  done
    4.16  
    4.17  lemma (in M_trivial) Replace_abs:
    4.18 -     "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
    4.19 +     "[| M(A); M(z); univalent(M,A,P); 
    4.20           !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |]
    4.21        ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
    4.22  apply (simp add: is_Replace_def)
    4.23  apply (rule iffI)
    4.24 -apply (rule M_equalityI)
    4.25 -apply (simp_all add: univalent_Replace_iff, blast, blast)
    4.26 + apply (rule equality_iffI)
    4.27 + apply (simp_all add: univalent_Replace_iff) 
    4.28 + apply (blast dest: transM)+
    4.29  done
    4.30  
    4.31 +
    4.32  (*The first premise can't simply be assumed as a schema.
    4.33    It is essential to take care when asserting instances of Replacement.
    4.34    Let K be a nonconstructible subset of nat and define
    4.35 @@ -727,16 +731,17 @@
    4.36  apply (blast intro: RepFun_closed2 dest: transM)
    4.37  done
    4.38  
    4.39 -lemma (in M_trivial) lambda_abs2 [simp]:
    4.40 -     "[| strong_replacement(M, \<lambda>x y. x\<in>A & y = \<langle>x, b(x)\<rangle>);
    4.41 -         Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
    4.42 +lemma (in M_trivial) lambda_abs2:
    4.43 +     "[| Relation1(M,A,is_b,b); M(A); \<forall>m[M]. m\<in>A --> M(b(m)); M(z) |]
    4.44        ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)"
    4.45  apply (simp add: Relation1_def is_lambda_def)
    4.46  apply (rule iffI)
    4.47   prefer 2 apply (simp add: lam_def)
    4.48 -apply (rule M_equalityI)
    4.49 -  apply (simp add: lam_def)
    4.50 - apply (simp add: lam_closed2)+
    4.51 +apply (rule equality_iffI)
    4.52 +apply (simp add: lam_def) 
    4.53 +apply (rule iffI) 
    4.54 + apply (blast dest: transM) 
    4.55 +apply (auto simp add: transM [of _ A]) 
    4.56  done
    4.57  
    4.58  lemma is_lambda_cong [cong]:
    4.59 @@ -1159,8 +1164,7 @@
    4.60  done
    4.61  
    4.62  lemma (in M_basic) composition_abs [simp]:
    4.63 -     "[| M(r); M(s); M(t) |]
    4.64 -      ==> composition(M,r,s,t) <-> t = r O s"
    4.65 +     "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) <-> t = r O s"
    4.66  apply safe
    4.67   txt{*Proving @{term "composition(M, r, s, r O s)"}*}
    4.68   prefer 2
     5.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Fri Nov 08 10:28:29 2002 +0100
     5.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Fri Nov 08 10:34:40 2002 +0100
     5.3 @@ -369,7 +369,7 @@
     5.4  lemma (in M_satisfies) a_rel:
     5.5       "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
     5.6  apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
     5.7 -apply (simp add: lambda_abs2 [OF Member_replacement'] Relation1_def)
     5.8 +apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
     5.9  done
    5.10  
    5.11  lemma (in M_satisfies) b_closed:
    5.12 @@ -381,7 +381,7 @@
    5.13  lemma (in M_satisfies) b_rel:
    5.14       "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
    5.15  apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
    5.16 -apply (simp add: lambda_abs2 [OF Equal_replacement'] Relation1_def)
    5.17 +apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
    5.18  done
    5.19  
    5.20  lemma (in M_satisfies) c_closed:
    5.21 @@ -400,8 +400,8 @@
    5.22  	       \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
    5.23  					  f ` succ(depth(v)) ` v))"
    5.24  apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
    5.25 -apply (simp add: lambda_abs2 [OF Nand_replacement' triv_Relation1] 
    5.26 -                 formula_into_M)
    5.27 +apply (auto del: iffI intro!: lambda_abs2 
    5.28 +            simp add: Relation1_def formula_into_M) 
    5.29  done
    5.30  
    5.31  lemma (in M_satisfies) d_closed:
    5.32 @@ -418,8 +418,7 @@
    5.33       \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
    5.34  apply (simp del: rall_abs 
    5.35              add: Relation1_def satisfies_is_d_def satisfies_d_def)
    5.36 -apply (simp add: lambda_abs2 [OF Forall_replacement' triv_Relation1] 
    5.37 -                 formula_into_M)
    5.38 +apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
    5.39  done
    5.40  
    5.41