Relativized right up to L satisfies V=L!
authorpaulson
Fri Aug 16 16:41:48 2002 +0200 (2002-08-16)
changeset 1350552a16cb7fefb
parent 13504 59066e97b551
child 13506 acc18a5d2b1a
Relativized right up to L satisfies V=L!
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/MetaExists.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
     1.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
     1.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4  apply (subgoal_tac "L(env) & L(p)") 
     1.5   prefer 2 apply (blast intro: transL) 
     1.6  apply (rule separation_CollectI)
     1.7 -apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast )
     1.8 +apply (rule_tac A="{A,env,p,z}" in subset_LsetE, blast)
     1.9  apply (rule ReflectsE [OF DPow_body_reflection], assumption)
    1.10  apply (drule subset_Lset_ltD, assumption)
    1.11  apply (erule reflection_imp_L_separation)
    1.12 @@ -316,4 +316,351 @@
    1.13  lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L]
    1.14    and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L]
    1.15  
    1.16 +
    1.17 +subsubsection{*The Operator @{term is_Collect}*}
    1.18 +
    1.19 +text{*The formula @{term is_P} has one free variable, 0, and it is
    1.20 +enclosed within a single quantifier.*}
    1.21 +
    1.22 +(* is_Collect :: "[i=>o,i,i=>o,i] => o"
    1.23 +    "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
    1.24 +
    1.25 +constdefs Collect_fm :: "[i, i, i]=>i"
    1.26 + "Collect_fm(A,is_P,z) == 
    1.27 +        Forall(Iff(Member(0,succ(z)),
    1.28 +                   And(Member(0,succ(A)), is_P)))"
    1.29 +
    1.30 +lemma is_Collect_type [TC]:
    1.31 +     "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
    1.32 +      ==> Collect_fm(x,is_P,y) \<in> formula"
    1.33 +by (simp add: Collect_fm_def)
    1.34 +
    1.35 +lemma sats_Collect_fm:
    1.36 +  assumes is_P_iff_sats: 
    1.37 +      "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
    1.38 +  shows 
    1.39 +      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
    1.40 +       ==> sats(A, Collect_fm(x,p,y), env) <->
    1.41 +           is_Collect(**A, nth(x,env), is_P, nth(y,env))"
    1.42 +by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
    1.43 +
    1.44 +lemma Collect_iff_sats:
    1.45 +  assumes is_P_iff_sats: 
    1.46 +      "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
    1.47 +  shows 
    1.48 +  "[| nth(i,env) = x; nth(j,env) = y;
    1.49 +      i \<in> nat; j \<in> nat; env \<in> list(A)|]
    1.50 +   ==> is_Collect(**A, x, is_P, y) <-> sats(A, Collect_fm(i,p,j), env)"
    1.51 +by (simp add: sats_Collect_fm [OF is_P_iff_sats])
    1.52 +
    1.53 +
    1.54 +text{*The second argument of @{term is_P} gives it direct access to @{term x},
    1.55 +  which is essential for handling free variable references.*}
    1.56 +theorem Collect_reflection:
    1.57 +  assumes is_P_reflection:
    1.58 +    "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
    1.59 +                     \<lambda>i x. is_P(**Lset(i), f(x), g(x))]"
    1.60 +  shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
    1.61 +               \<lambda>i x. is_Collect(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
    1.62 +apply (simp (no_asm_use) only: is_Collect_def setclass_simps)
    1.63 +apply (intro FOL_reflections is_P_reflection)
    1.64 +done
    1.65 +
    1.66 +
    1.67 +subsubsection{*The Operator @{term is_Replace}*}
    1.68 +
    1.69 +text{*BEWARE!  The formula @{term is_P} has free variables 0, 1
    1.70 + and not the usual 1, 0!  It is enclosed within two quantifiers.*}
    1.71 +
    1.72 +(*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
    1.73 +    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
    1.74 +
    1.75 +constdefs Replace_fm :: "[i, i, i]=>i"
    1.76 + "Replace_fm(A,is_P,z) == 
    1.77 +        Forall(Iff(Member(0,succ(z)),
    1.78 +                   Exists(And(Member(0,A#+2), is_P))))"
    1.79 +
    1.80 +lemma is_Replace_type [TC]:
    1.81 +     "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
    1.82 +      ==> Replace_fm(x,is_P,y) \<in> formula"
    1.83 +by (simp add: Replace_fm_def)
    1.84 +
    1.85 +lemma sats_Replace_fm:
    1.86 +  assumes is_P_iff_sats: 
    1.87 +      "!!a b. [|a \<in> A; b \<in> A|] 
    1.88 +              ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
    1.89 +  shows 
    1.90 +      "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
    1.91 +       ==> sats(A, Replace_fm(x,p,y), env) <->
    1.92 +           is_Replace(**A, nth(x,env), is_P, nth(y,env))"
    1.93 +by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
    1.94 +
    1.95 +lemma Replace_iff_sats:
    1.96 +  assumes is_P_iff_sats: 
    1.97 +      "!!a b. [|a \<in> A; b \<in> A|] 
    1.98 +              ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
    1.99 +  shows 
   1.100 +  "[| nth(i,env) = x; nth(j,env) = y;
   1.101 +      i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.102 +   ==> is_Replace(**A, x, is_P, y) <-> sats(A, Replace_fm(i,p,j), env)"
   1.103 +by (simp add: sats_Replace_fm [OF is_P_iff_sats])
   1.104 +
   1.105 +
   1.106 +text{*The second argument of @{term is_P} gives it direct access to @{term x},
   1.107 +  which is essential for handling free variable references.*}
   1.108 +theorem Replace_reflection:
   1.109 +  assumes is_P_reflection:
   1.110 +    "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
   1.111 +                     \<lambda>i x. is_P(**Lset(i), f(x), g(x), h(x))]"
   1.112 +  shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
   1.113 +               \<lambda>i x. is_Replace(**Lset(i), f(x), is_P(**Lset(i), x), g(x))]"
   1.114 +apply (simp (no_asm_use) only: is_Replace_def setclass_simps)
   1.115 +apply (intro FOL_reflections is_P_reflection)
   1.116 +done
   1.117 +
   1.118 +
   1.119 +
   1.120 +subsubsection{*The Operator @{term is_DPow'}, Internalized*}
   1.121 +
   1.122 +(*  "is_DPow'(M,A,Z) == 
   1.123 +       \<forall>X[M]. X \<in> Z <-> 
   1.124 +         subset(M,X,A) & 
   1.125 +           (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   1.126 +                    is_Collect(M, A, is_DPow_body(M,A,env,p), X))" *)
   1.127 +
   1.128 +constdefs DPow'_fm :: "[i,i]=>i"
   1.129 +    "DPow'_fm(A,Z) == 
   1.130 +      Forall(
   1.131 +       Iff(Member(0,succ(Z)),
   1.132 +        And(subset_fm(0,succ(A)),
   1.133 +         Exists(Exists(
   1.134 +          And(mem_formula_fm(0),
   1.135 +           And(mem_list_fm(A#+3,1),
   1.136 +            Collect_fm(A#+3, 
   1.137 +                       DPow_body_fm(A#+4, 2, 1, 0), 2))))))))"
   1.138 +
   1.139 +lemma is_DPow'_type [TC]:
   1.140 +     "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
   1.141 +by (simp add: DPow'_fm_def)
   1.142 +
   1.143 +lemma sats_DPow'_fm [simp]:
   1.144 +   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   1.145 +    ==> sats(A, DPow'_fm(x,y), env) <->
   1.146 +        is_DPow'(**A, nth(x,env), nth(y,env))"
   1.147 +by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
   1.148 +
   1.149 +lemma DPow'_iff_sats:
   1.150 +      "[| nth(i,env) = x; nth(j,env) = y; 
   1.151 +          i \<in> nat; j \<in> nat; env \<in> list(A)|]
   1.152 +       ==> is_DPow'(**A, x, y) <-> sats(A, DPow'_fm(i,j), env)"
   1.153 +by (simp add: sats_DPow'_fm)
   1.154 +
   1.155 +theorem DPow'_reflection:
   1.156 +     "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
   1.157 +               \<lambda>i x. is_DPow'(**Lset(i),f(x),g(x))]"
   1.158 +apply (simp only: is_DPow'_def setclass_simps)
   1.159 +apply (intro FOL_reflections function_reflections mem_formula_reflection
   1.160 +             mem_list_reflection Collect_reflection DPow_body_reflection)
   1.161 +done
   1.162 +
   1.163 +(*????????????????move up*)
   1.164 +
   1.165 +
   1.166 +
   1.167 +
   1.168 +
   1.169 +subsection{*Additional Constraints on the Class Model @{term M}*}
   1.170 +
   1.171 +constdefs
   1.172 +  transrec_body :: "[i=>o,i,i,i,i] => o"
   1.173 +    "transrec_body(M,g,x) ==
   1.174 +      \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
   1.175 +
   1.176 +lemma (in M_DPow) transrec_body_abs:
   1.177 +     "[|M(x); M(g); M(z)|]
   1.178 +    ==> transrec_body(M,g,x,y,z) <-> y \<in> x & z = DPow'(g`y)"
   1.179 +by (simp add: transrec_body_def DPow'_abs transM [of _ x])
   1.180 +
   1.181 +locale M_Lset = M_DPow +
   1.182 + assumes strong_rep:
   1.183 +   "[|M(x); M(g)|] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
   1.184 + and transrec_rep: 
   1.185 +    "M(i) ==> transrec_replacement(M, \<lambda>x f u. 
   1.186 +              \<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) & 
   1.187 +                     big_union(M, r, u), i)"
   1.188 +
   1.189 +
   1.190 +lemma (in M_Lset) strong_rep':
   1.191 +   "[|M(x); M(g)|]
   1.192 +    ==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
   1.193 +by (insert strong_rep [of x g], simp add: transrec_body_abs)
   1.194 +
   1.195 +lemma (in M_Lset) DPow_apply_closed:
   1.196 +   "[|M(f); M(x); y\<in>x|] ==> M(DPow'(f`y))"
   1.197 +by (blast intro: DPow'_closed dest: transM) 
   1.198 +
   1.199 +lemma (in M_Lset) RepFun_DPow_apply_closed:
   1.200 +   "[|M(f); M(x)|] ==> M({DPow'(f`y). y\<in>x})"
   1.201 +by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep') 
   1.202 +
   1.203 +lemma (in M_Lset) RepFun_DPow_abs:
   1.204 +     "[|M(x); M(f); M(r) |]
   1.205 +      ==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) <->
   1.206 +          r =  {DPow'(f`y). y\<in>x}"
   1.207 +apply (simp add: transrec_body_abs RepFun_def) 
   1.208 +apply (rule iff_trans) 
   1.209 +apply (rule Replace_abs) 
   1.210 +apply (simp_all add: DPow_apply_closed strong_rep') 
   1.211 +done
   1.212 +
   1.213 +lemma (in M_Lset) transrec_rep':
   1.214 +   "M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
   1.215 +apply (insert transrec_rep [of i]) 
   1.216 +apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs 
   1.217 +       transrec_replacement_def) 
   1.218 +done
   1.219 +
   1.220 +
   1.221 +
   1.222 +constdefs
   1.223 +
   1.224 +  is_Lset :: "[i=>o, i, i] => o"
   1.225 +   "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
   1.226 +
   1.227 +lemma (in M_Lset) Lset_abs:
   1.228 +  "[|Ord(i);  M(i);  M(z)|] 
   1.229 +   ==> is_Lset(M,i,z) <-> z = Lset(i)"
   1.230 +apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
   1.231 +apply (rule transrec_abs)  
   1.232 +apply (simp_all add: transrec_rep' relativize2_def RepFun_DPow_apply_closed)
   1.233 +done
   1.234 +
   1.235 +lemma (in M_Lset) Lset_closed:
   1.236 +  "[|Ord(i);  M(i)|] ==> M(Lset(i))"
   1.237 +apply (simp add: Lset_eq_transrec_DPow') 
   1.238 +apply (rule transrec_closed [OF transrec_rep']) 
   1.239 +apply (simp_all add: relativize2_def RepFun_DPow_apply_closed)
   1.240 +done
   1.241 +
   1.242 +
   1.243 +subsection{*Instantiating the Locale @{text M_Lset}*}
   1.244 +
   1.245 +
   1.246 +subsubsection{*The First Instance of Replacement*}
   1.247 +
   1.248 +lemma strong_rep_Reflects:
   1.249 + "REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
   1.250 +                          v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
   1.251 +   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
   1.252 +            v \<in> x & fun_apply(**Lset(i),g,v,gy) & is_DPow'(**Lset(i),gy,u))]"
   1.253 +by (intro FOL_reflections function_reflections DPow'_reflection)
   1.254 +
   1.255 +lemma strong_rep:
   1.256 +   "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
   1.257 +apply (unfold transrec_body_def)  
   1.258 +apply (rule strong_replacementI) 
   1.259 +apply (rule rallI)
   1.260 +apply (rename_tac B)  
   1.261 +apply (rule separation_CollectI) 
   1.262 +apply (rule_tac A="{x,g,B,z}" in subset_LsetE, blast) 
   1.263 +apply (rule ReflectsE [OF strong_rep_Reflects], assumption)
   1.264 +apply (drule subset_Lset_ltD, assumption) 
   1.265 +apply (erule reflection_imp_L_separation)
   1.266 +  apply (simp_all add: lt_Ord2)
   1.267 +apply (rule DPow_LsetI)
   1.268 +apply (rename_tac u) 
   1.269 +apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
   1.270 +apply (rule_tac env = "[v,u,x,g,B,z]" in mem_iff_sats) 
   1.271 +apply (rule sep_rules DPow'_iff_sats | simp)+
   1.272 +done
   1.273 +
   1.274 +
   1.275 +subsubsection{*The Second Instance of Replacement*}
   1.276 +
   1.277 +lemma transrec_rep_Reflects:
   1.278 + "REFLECTS [\<lambda>x. \<exists>v[L]. v \<in> B &
   1.279 +              (\<exists>y[L]. pair(L,v,y,x) &
   1.280 +             is_wfrec (L, \<lambda>x f u. \<exists>r[L].
   1.281 +                is_Replace (L, x, \<lambda>y z. 
   1.282 +                     \<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 
   1.283 +                      is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
   1.284 +    \<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
   1.285 +              (\<exists>y \<in> Lset(i). pair(**Lset(i),v,y,x) &
   1.286 +             is_wfrec (**Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
   1.287 +                is_Replace (**Lset(i), x, \<lambda>y z. 
   1.288 +                     \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(**Lset(i),f,y,gy) & 
   1.289 +                      is_DPow'(**Lset(i),gy,z), r) & 
   1.290 +                      big_union(**Lset(i),r,u), mr, v, y))]" 
   1.291 +apply (simp only: setclass_simps [symmetric])
   1.292 +  --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[**Lset(i)]"} within the body
   1.293 +       of the @{term is_wfrec} application. *}
   1.294 +apply (intro FOL_reflections function_reflections 
   1.295 +          is_wfrec_reflection Replace_reflection DPow'_reflection) 
   1.296 +done
   1.297 +
   1.298 +
   1.299 +
   1.300 +lemma transrec_rep: 
   1.301 +    "[|L(j)|]
   1.302 +    ==> transrec_replacement(L, \<lambda>x f u. 
   1.303 +              \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
   1.304 +                     big_union(L, r, u), j)"
   1.305 +apply (subgoal_tac "L(Memrel(eclose({j})))")
   1.306 + prefer 2 apply simp
   1.307 +apply (rule transrec_replacementI, assumption)
   1.308 +apply (rule strong_replacementI)
   1.309 +apply (unfold transrec_body_def)  
   1.310 +apply (rule rallI)
   1.311 +apply (rename_tac B)
   1.312 +apply (rule separation_CollectI)
   1.313 +apply (rule_tac A="{j,B,z,Memrel(eclose({j}))}" in subset_LsetE, blast)
   1.314 +apply (rule ReflectsE [OF transrec_rep_Reflects], assumption)
   1.315 +apply (drule subset_Lset_ltD, assumption)
   1.316 +apply (erule reflection_imp_L_separation)
   1.317 +  apply (simp_all add: lt_Ord2 Memrel_closed)
   1.318 +apply (elim conjE)
   1.319 +apply (rule DPow_LsetI)
   1.320 +apply (rename_tac w)
   1.321 +apply (rule bex_iff_sats conj_iff_sats)+
   1.322 +apply (rule_tac env = "[v,w,j,B,Memrel(eclose({j}))]" in mem_iff_sats)
   1.323 +apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
   1.324 +       simp)+
   1.325 +done
   1.326 +
   1.327 +
   1.328 +subsubsection{*Actually Instantiating @{text M_Lset}*}
   1.329 +
   1.330 +lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
   1.331 +  apply (rule M_Lset_axioms.intro)
   1.332 +       apply (assumption | rule strong_rep transrec_rep)+
   1.333 +  done
   1.334 +
   1.335 +theorem M_Lset_L: "PROP M_Lset(L)"
   1.336 +apply (rule M_Lset.intro) 
   1.337 +     apply (rule M_DPow.axioms [OF M_DPow_L])+
   1.338 +apply (rule M_Lset_axioms_L) 
   1.339 +done
   1.340 +
   1.341 +text{*Finally: the point of the whole theory!*}
   1.342 +lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
   1.343 +   and Lset_abs = M_Lset.Lset_abs [OF M_Lset_L]
   1.344 +
   1.345 +
   1.346 +subsection{*The Notion of Constructible Set*}
   1.347 +
   1.348 +
   1.349 +constdefs
   1.350 +  constructible :: "[i=>o,i] => o"
   1.351 +    "constructible(M,x) ==
   1.352 +       \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
   1.353 +
   1.354 +
   1.355 +theorem V_equals_L_in_L:
   1.356 +  "L(x) ==> constructible(L,x)"
   1.357 +apply (simp add: constructible_def Lset_abs Lset_closed) 
   1.358 +apply (simp add: L_def)
   1.359 +apply (blast intro: Ord_in_L) 
   1.360 +done
   1.361 +
   1.362 +
   1.363  end
     2.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
     2.3 @@ -1,3 +1,9 @@
     2.4 +(*  Title:      ZF/Constructible/Datatype_absolute.thy
     2.5 +    ID: $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2002  University of Cambridge
     2.8 +*)
     2.9 +
    2.10  header {*Absoluteness Properties for Recursive Datatypes*}
    2.11  
    2.12  theory Datatype_absolute = Formula + WF_absolute:
     3.1 --- a/src/ZF/Constructible/Formula.thy	Fri Aug 16 12:48:49 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Formula.thy	Fri Aug 16 16:41:48 2002 +0200
     3.3 @@ -1,3 +1,9 @@
     3.4 +(*  Title:      ZF/Constructible/Formula.thy
     3.5 +    ID: $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   2002  University of Cambridge
     3.8 +*)
     3.9 +
    3.10  header {* First-Order Formulas and the Definition of the Class L *}
    3.11  
    3.12  theory Formula = Main:
     4.1 --- a/src/ZF/Constructible/Internalize.thy	Fri Aug 16 12:48:49 2002 +0200
     4.2 +++ b/src/ZF/Constructible/Internalize.thy	Fri Aug 16 16:41:48 2002 +0200
     4.3 @@ -1,3 +1,9 @@
     4.4 +(*  Title:      ZF/Constructible/Internalize.thy
     4.5 +    ID: $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   2002  University of Cambridge
     4.8 +*)
     4.9 +
    4.10  theory Internalize = L_axioms + Datatype_absolute:
    4.11  
    4.12  subsection{*Internalized Forms of Data Structuring Operators*}
     5.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 12:48:49 2002 +0200
     5.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
     5.3 @@ -1,3 +1,8 @@
     5.4 +(*  Title:      ZF/Constructible/L_axioms.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   2002  University of Cambridge
     5.8 +*)
     5.9  
    5.10  header {* The ZF Axioms (Except Separation) in L *}
    5.11  
    5.12 @@ -1079,7 +1084,7 @@
    5.13      ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))"
    5.14  by (simp add: function_fm_def is_function_def)
    5.15  
    5.16 -lemma function_iff_sats:
    5.17 +lemma is_function_iff_sats:
    5.18        "[| nth(i,env) = x; nth(j,env) = y;
    5.19            i \<in> nat; env \<in> list(A)|]
    5.20         ==> is_function(**A, x) <-> sats(A, function_fm(i), env)"
    5.21 @@ -1141,11 +1146,11 @@
    5.22  lemmas function_iff_sats =
    5.23          empty_iff_sats number1_iff_sats
    5.24          upair_iff_sats pair_iff_sats union_iff_sats
    5.25 -        cons_iff_sats successor_iff_sats
    5.26 +        big_union_iff_sats cons_iff_sats successor_iff_sats
    5.27          fun_apply_iff_sats  Memrel_iff_sats
    5.28          pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats
    5.29          image_iff_sats pre_image_iff_sats
    5.30 -        relation_iff_sats function_iff_sats
    5.31 +        relation_iff_sats is_function_iff_sats
    5.32  
    5.33  
    5.34  theorem typed_function_reflection:
     6.1 --- a/src/ZF/Constructible/MetaExists.thy	Fri Aug 16 12:48:49 2002 +0200
     6.2 +++ b/src/ZF/Constructible/MetaExists.thy	Fri Aug 16 16:41:48 2002 +0200
     6.3 @@ -1,3 +1,9 @@
     6.4 +(*  Title:      ZF/Constructible/MetaExists.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   2002  University of Cambridge
     6.8 +*)
     6.9 +
    6.10  header{*The meta-existential quantifier*}
    6.11  
    6.12  theory MetaExists = Main:
     7.1 --- a/src/ZF/Constructible/Normal.thy	Fri Aug 16 12:48:49 2002 +0200
     7.2 +++ b/src/ZF/Constructible/Normal.thy	Fri Aug 16 16:41:48 2002 +0200
     7.3 @@ -1,3 +1,9 @@
     7.4 +(*  Title:      ZF/Constructible/Normal.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   2002  University of Cambridge
     7.8 +*)
     7.9 +
    7.10  header {*Closed Unbounded Classes and Normal Functions*}
    7.11  
    7.12  theory Normal = Main:
     8.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 12:48:49 2002 +0200
     8.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 16:41:48 2002 +0200
     8.3 @@ -82,7 +82,7 @@
     8.4  lemma rtrancl_separation:
     8.5       "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
     8.6  apply (rule separation_CollectI)
     8.7 -apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
     8.8 +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast)
     8.9  apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
    8.10  apply (drule subset_Lset_ltD, assumption)
    8.11  apply (erule reflection_imp_L_separation)
    8.12 @@ -190,7 +190,7 @@
    8.13                \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
    8.14                 w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp)"
    8.15  apply (rule separation_CollectI)
    8.16 -apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast )
    8.17 +apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast)
    8.18  apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption)
    8.19  apply (drule subset_Lset_ltD, assumption)
    8.20  apply (erule reflection_imp_L_separation)
    8.21 @@ -252,7 +252,7 @@
    8.22        separation (L, \<lambda>x. \<forall>rplus[L]. tran_closure(L,r,rplus) -->
    8.23           ~ (\<exists>f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))"
    8.24  apply (rule separation_CollectI)
    8.25 -apply (rule_tac A="{r,z}" in subset_LsetE, blast )
    8.26 +apply (rule_tac A="{r,z}" in subset_LsetE, blast)
    8.27  apply (rule ReflectsE [OF wfrank_Reflects], assumption)
    8.28  apply (drule subset_Lset_ltD, assumption)
    8.29  apply (erule reflection_imp_L_separation)
    8.30 @@ -294,7 +294,7 @@
    8.31  apply (rule rallI)
    8.32  apply (rename_tac B)
    8.33  apply (rule separation_CollectI)
    8.34 -apply (rule_tac A="{B,r,z}" in subset_LsetE, blast )
    8.35 +apply (rule_tac A="{B,r,z}" in subset_LsetE, blast)
    8.36  apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption)
    8.37  apply (drule subset_Lset_ltD, assumption)
    8.38  apply (erule reflection_imp_L_separation)
    8.39 @@ -333,7 +333,7 @@
    8.40               M_is_recfun(L, \<lambda>x f y. is_range(L,f,y), rplus, x, f) -->
    8.41               ordinal(L,rangef)))"
    8.42  apply (rule separation_CollectI)
    8.43 -apply (rule_tac A="{r,z}" in subset_LsetE, blast )
    8.44 +apply (rule_tac A="{r,z}" in subset_LsetE, blast)
    8.45  apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption)
    8.46  apply (drule subset_Lset_ltD, assumption)
    8.47  apply (erule reflection_imp_L_separation)
    8.48 @@ -411,7 +411,7 @@
    8.49  apply (rule separation_CollectI)
    8.50  apply (insert nonempty)
    8.51  apply (subgoal_tac "L(Memrel(succ(n)))")
    8.52 -apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
    8.53 +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
    8.54  apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
    8.55  apply (drule subset_Lset_ltD, assumption)
    8.56  apply (erule reflection_imp_L_separation)
    8.57 @@ -492,7 +492,7 @@
    8.58  apply (rule separation_CollectI)
    8.59  apply (insert nonempty)
    8.60  apply (subgoal_tac "L(Memrel(succ(n)))")
    8.61 -apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast )
    8.62 +apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast)
    8.63  apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
    8.64  apply (drule subset_Lset_ltD, assumption)
    8.65  apply (erule reflection_imp_L_separation)
    8.66 @@ -612,7 +612,7 @@
    8.67  apply (rule rallI)
    8.68  apply (rule separation_CollectI)
    8.69  apply (subgoal_tac "L(Memrel(succ(n)))")
    8.70 -apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast )
    8.71 +apply (rule_tac A="{A,n,w,z,Memrel(succ(n))}" in subset_LsetE, blast)
    8.72  apply (rule ReflectsE [OF nth_replacement_Reflects], assumption)
    8.73  apply (drule subset_Lset_ltD, assumption)
    8.74  apply (erule reflection_imp_L_separation)
    8.75 @@ -680,7 +680,7 @@
    8.76  apply (rename_tac B)
    8.77  apply (rule separation_CollectI)
    8.78  apply (subgoal_tac "L(Memrel(succ(n)))")
    8.79 -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast )
    8.80 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast)
    8.81  apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
    8.82  apply (drule subset_Lset_ltD, assumption)
    8.83  apply (erule reflection_imp_L_separation)
     9.1 --- a/src/ZF/Constructible/Reflection.thy	Fri Aug 16 12:48:49 2002 +0200
     9.2 +++ b/src/ZF/Constructible/Reflection.thy	Fri Aug 16 16:41:48 2002 +0200
     9.3 @@ -1,3 +1,9 @@
     9.4 +(*  Title:      ZF/Constructible/Reflection.thy
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   2002  University of Cambridge
     9.8 +*)
     9.9 +
    9.10  header {* The Reflection Theorem*}
    9.11  
    9.12  theory Reflection = Normal:
    10.1 --- a/src/ZF/Constructible/Relative.thy	Fri Aug 16 12:48:49 2002 +0200
    10.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Aug 16 16:41:48 2002 +0200
    10.3 @@ -1,3 +1,9 @@
    10.4 +(*  Title:      ZF/Constructible/Relative.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 +    Copyright   2002  University of Cambridge
    10.8 +*)
    10.9 +
   10.10  header {*Relativization and Absoluteness*}
   10.11  
   10.12  theory Relative = Main:
   10.13 @@ -43,6 +49,9 @@
   10.14    is_Collect :: "[i=>o,i,i=>o,i] => o"
   10.15      "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)"
   10.16  
   10.17 +  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
   10.18 +    "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))"
   10.19 +
   10.20    inter :: "[i=>o,i,i,i] => o"
   10.21      "inter(M,a,b,z) == \<forall>x[M]. x \<in> z <-> x \<in> a & x \<in> b"
   10.22  
   10.23 @@ -294,12 +303,20 @@
   10.24        ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))"
   10.25  by (simp add: separation_def) 
   10.26  
   10.27 -text{*Congruence rules for replacement*}
   10.28  lemma univalent_cong [cong]:
   10.29       "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   10.30        ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))"
   10.31  by (simp add: univalent_def) 
   10.32  
   10.33 +lemma univalent_triv [intro,simp]:
   10.34 +     "univalent(M, A, \<lambda>x y. y = f(x))"
   10.35 +by (simp add: univalent_def) 
   10.36 +
   10.37 +lemma univalent_conjI2 [intro,simp]:
   10.38 +     "univalent(M,A,Q) ==> univalent(M, A, \<lambda>x y. P(x,y) & Q(x,y))"
   10.39 +by (simp add: univalent_def, blast) 
   10.40 +
   10.41 +text{*Congruence rule for replacement*}
   10.42  lemma strong_replacement_cong [cong]:
   10.43       "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   10.44        ==> strong_replacement(M, %x y. P(x,y)) <-> 
   10.45 @@ -616,21 +633,46 @@
   10.46  done
   10.47  
   10.48  
   10.49 +subsubsection{*The Operator @{term is_Replace}*}
   10.50 +
   10.51 +
   10.52 +lemma is_Replace_cong [cong]:
   10.53 +     "[| A=A'; 
   10.54 +         !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y);
   10.55 +         z=z' |] 
   10.56 +      ==> is_Replace(M, A, %x y. P(x,y), z) <-> 
   10.57 +          is_Replace(M, A', %x y. P'(x,y), z')" 
   10.58 +by (simp add: is_Replace_def) 
   10.59 +
   10.60 +lemma (in M_triv_axioms) univalent_Replace_iff: 
   10.61 +     "[| M(A); univalent(M,A,P);
   10.62 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] 
   10.63 +      ==> u \<in> Replace(A,P) <-> (\<exists>x. x\<in>A & P(x,u))"
   10.64 +apply (simp add: Replace_iff univalent_def) 
   10.65 +apply (blast dest: transM)
   10.66 +done
   10.67 +
   10.68  (*The last premise expresses that P takes M to M*)
   10.69  lemma (in M_triv_axioms) strong_replacement_closed [intro,simp]:
   10.70       "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   10.71 -       !!x y. [| x\<in>A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   10.72 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
   10.73  apply (simp add: strong_replacement_def) 
   10.74 -apply (drule rspec, auto) 
   10.75 +apply (drule_tac x=A in rspec, safe) 
   10.76  apply (subgoal_tac "Replace(A,P) = Y")
   10.77   apply simp 
   10.78 -apply (rule equality_iffI) 
   10.79 -apply (simp add: Replace_iff, safe)
   10.80 - apply (blast dest: transM) 
   10.81 -apply (frule transM, assumption) 
   10.82 - apply (simp add: univalent_def)
   10.83 - apply (drule rspec [THEN iffD1], assumption, assumption)
   10.84 - apply (blast dest: transM) 
   10.85 +apply (rule equality_iffI)
   10.86 +apply (simp add: univalent_Replace_iff)
   10.87 +apply (blast dest: transM) 
   10.88 +done
   10.89 +
   10.90 +lemma (in M_triv_axioms) Replace_abs: 
   10.91 +     "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P);
   10.92 +         !!x y. [| x\<in>A; P(x,y) |] ==> M(y)  |] 
   10.93 +      ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)"
   10.94 +apply (simp add: is_Replace_def)
   10.95 +apply (rule iffI) 
   10.96 +apply (rule M_equalityI) 
   10.97 +apply (simp_all add: univalent_Replace_iff, blast, blast) 
   10.98  done
   10.99  
  10.100  (*The first premise can't simply be assumed as a schema.
  10.101 @@ -1490,34 +1532,34 @@
  10.102  subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
  10.103  
  10.104  lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
  10.105 -by (simp add: is_hd_def )
  10.106 +by (simp add: is_hd_def)
  10.107  
  10.108  lemma (in M_triv_axioms) is_hd_Cons:
  10.109       "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
  10.110 -by (force simp add: is_hd_def ) 
  10.111 +by (force simp add: is_hd_def) 
  10.112  
  10.113  lemma (in M_triv_axioms) hd_abs [simp]:
  10.114       "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
  10.115  apply (simp add: hd'_def)
  10.116  apply (intro impI conjI)
  10.117   prefer 2 apply (force simp add: is_hd_def) 
  10.118 -apply (simp add: quasilist_def is_hd_def )
  10.119 +apply (simp add: quasilist_def is_hd_def)
  10.120  apply (elim disjE exE, auto)
  10.121  done 
  10.122  
  10.123  lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
  10.124 -by (simp add: is_tl_def )
  10.125 +by (simp add: is_tl_def)
  10.126  
  10.127  lemma (in M_triv_axioms) is_tl_Cons:
  10.128       "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
  10.129 -by (force simp add: is_tl_def ) 
  10.130 +by (force simp add: is_tl_def) 
  10.131  
  10.132  lemma (in M_triv_axioms) tl_abs [simp]:
  10.133       "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
  10.134  apply (simp add: tl'_def)
  10.135  apply (intro impI conjI)
  10.136   prefer 2 apply (force simp add: is_tl_def) 
  10.137 -apply (simp add: quasilist_def is_tl_def )
  10.138 +apply (simp add: quasilist_def is_tl_def)
  10.139  apply (elim disjE exE, auto)
  10.140  done 
  10.141  
    11.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
    11.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
    11.3 @@ -852,7 +852,7 @@
    11.4  theorem satisfies_is_d_reflection:
    11.5       "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
    11.6                 \<lambda>i x. satisfies_is_d(**Lset(i),f(x),g(x),h(x),g'(x))]"
    11.7 -apply (unfold satisfies_is_d_def ) 
    11.8 +apply (unfold satisfies_is_d_def) 
    11.9  apply (intro FOL_reflections function_reflections is_lambda_reflection
   11.10               extra_reflections nth_reflection depth_apply_reflection 
   11.11               is_list_reflection)
   11.12 @@ -944,7 +944,7 @@
   11.13  apply (rule rallI)
   11.14  apply (rename_tac B)  
   11.15  apply (rule separation_CollectI) 
   11.16 -apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
   11.17 +apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
   11.18  apply (rule ReflectsE [OF Member_Reflects], assumption)
   11.19  apply (drule subset_Lset_ltD, assumption) 
   11.20  apply (erule reflection_imp_L_separation)
   11.21 @@ -986,7 +986,7 @@
   11.22  apply (rule rallI)
   11.23  apply (rename_tac B)  
   11.24  apply (rule separation_CollectI) 
   11.25 -apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
   11.26 +apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast) 
   11.27  apply (rule ReflectsE [OF Equal_Reflects], assumption)
   11.28  apply (drule subset_Lset_ltD, assumption) 
   11.29  apply (erule reflection_imp_L_separation)
   11.30 @@ -1030,7 +1030,7 @@
   11.31  apply (rule rallI)
   11.32  apply (rename_tac B)  
   11.33  apply (rule separation_CollectI) 
   11.34 -apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast ) 
   11.35 +apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast) 
   11.36  apply (rule ReflectsE [OF Nand_Reflects], assumption)
   11.37  apply (drule subset_Lset_ltD, assumption) 
   11.38  apply (erule reflection_imp_L_separation)
   11.39 @@ -1079,7 +1079,7 @@
   11.40  apply (rule rallI)
   11.41  apply (rename_tac B)  
   11.42  apply (rule separation_CollectI) 
   11.43 -apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast ) 
   11.44 +apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast) 
   11.45  apply (rule ReflectsE [OF Forall_Reflects], assumption)
   11.46  apply (drule subset_Lset_ltD, assumption) 
   11.47  apply (erule reflection_imp_L_separation)
   11.48 @@ -1113,7 +1113,7 @@
   11.49  apply (rule rallI)
   11.50  apply (rename_tac B)
   11.51  apply (rule separation_CollectI)
   11.52 -apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast )
   11.53 +apply (rule_tac A="{B,A,n,z,Memrel(eclose({n}))}" in subset_LsetE, blast)
   11.54  apply (rule ReflectsE [OF formula_rec_replacement_Reflects], assumption)
   11.55  apply (drule subset_Lset_ltD, assumption)
   11.56  apply (erule reflection_imp_L_separation)
    12.1 --- a/src/ZF/Constructible/Separation.thy	Fri Aug 16 12:48:49 2002 +0200
    12.2 +++ b/src/ZF/Constructible/Separation.thy	Fri Aug 16 16:41:48 2002 +0200
    12.3 @@ -62,7 +62,7 @@
    12.4  lemma Inter_separation:
    12.5       "L(A) ==> separation(L, \<lambda>x. \<forall>y[L]. y\<in>A --> x\<in>y)"
    12.6  apply (rule separation_CollectI)
    12.7 -apply (rule_tac A="{A,z}" in subset_LsetE, blast )
    12.8 +apply (rule_tac A="{A,z}" in subset_LsetE, blast)
    12.9  apply (rule ReflectsE [OF Inter_Reflects], assumption)
   12.10  apply (drule subset_Lset_ltD, assumption)
   12.11  apply (erule reflection_imp_L_separation)
   12.12 @@ -84,7 +84,7 @@
   12.13  lemma Diff_separation:
   12.14       "L(B) ==> separation(L, \<lambda>x. x \<notin> B)"
   12.15  apply (rule separation_CollectI) 
   12.16 -apply (rule_tac A="{B,z}" in subset_LsetE, blast ) 
   12.17 +apply (rule_tac A="{B,z}" in subset_LsetE, blast) 
   12.18  apply (rule ReflectsE [OF Diff_Reflects], assumption)
   12.19  apply (drule subset_Lset_ltD, assumption) 
   12.20  apply (erule reflection_imp_L_separation)
   12.21 @@ -107,7 +107,7 @@
   12.22       "[| L(A); L(B) |]
   12.23        ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. y\<in>B & pair(L,x,y,z)))"
   12.24  apply (rule separation_CollectI)
   12.25 -apply (rule_tac A="{A,B,z}" in subset_LsetE, blast )
   12.26 +apply (rule_tac A="{A,B,z}" in subset_LsetE, blast)
   12.27  apply (rule ReflectsE [OF cartprod_Reflects], assumption)
   12.28  apply (drule subset_Lset_ltD, assumption)
   12.29  apply (erule reflection_imp_L_separation)
   12.30 @@ -131,7 +131,7 @@
   12.31       "[| L(A); L(r) |]
   12.32        ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & (\<exists>x[L]. x\<in>A & pair(L,x,y,p)))"
   12.33  apply (rule separation_CollectI)
   12.34 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
   12.35 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
   12.36  apply (rule ReflectsE [OF image_Reflects], assumption)
   12.37  apply (drule subset_Lset_ltD, assumption)
   12.38  apply (erule reflection_imp_L_separation)
   12.39 @@ -156,7 +156,7 @@
   12.40       "L(r) ==> separation(L,
   12.41           \<lambda>z. \<exists>p[L]. p\<in>r & (\<exists>x[L]. \<exists>y[L]. pair(L,x,y,p) & pair(L,y,x,z)))"
   12.42  apply (rule separation_CollectI)
   12.43 -apply (rule_tac A="{r,z}" in subset_LsetE, blast )
   12.44 +apply (rule_tac A="{r,z}" in subset_LsetE, blast)
   12.45  apply (rule ReflectsE [OF converse_Reflects], assumption)
   12.46  apply (drule subset_Lset_ltD, assumption)
   12.47  apply (erule reflection_imp_L_separation)
   12.48 @@ -180,7 +180,7 @@
   12.49  lemma restrict_separation:
   12.50     "L(A) ==> separation(L, \<lambda>z. \<exists>x[L]. x\<in>A & (\<exists>y[L]. pair(L,x,y,z)))"
   12.51  apply (rule separation_CollectI)
   12.52 -apply (rule_tac A="{A,z}" in subset_LsetE, blast )
   12.53 +apply (rule_tac A="{A,z}" in subset_LsetE, blast)
   12.54  apply (rule ReflectsE [OF restrict_Reflects], assumption)
   12.55  apply (drule subset_Lset_ltD, assumption)
   12.56  apply (erule reflection_imp_L_separation)
   12.57 @@ -211,7 +211,7 @@
   12.58                    pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) &
   12.59                    xy\<in>s & yz\<in>r)"
   12.60  apply (rule separation_CollectI)
   12.61 -apply (rule_tac A="{r,s,z}" in subset_LsetE, blast )
   12.62 +apply (rule_tac A="{r,s,z}" in subset_LsetE, blast)
   12.63  apply (rule ReflectsE [OF comp_Reflects], assumption)
   12.64  apply (drule subset_Lset_ltD, assumption)
   12.65  apply (erule reflection_imp_L_separation)
   12.66 @@ -235,7 +235,7 @@
   12.67  lemma pred_separation:
   12.68       "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p[L]. p\<in>r & pair(L,y,x,p))"
   12.69  apply (rule separation_CollectI)
   12.70 -apply (rule_tac A="{r,x,z}" in subset_LsetE, blast )
   12.71 +apply (rule_tac A="{r,x,z}" in subset_LsetE, blast)
   12.72  apply (rule ReflectsE [OF pred_Reflects], assumption)
   12.73  apply (drule subset_Lset_ltD, assumption)
   12.74  apply (erule reflection_imp_L_separation)
   12.75 @@ -259,7 +259,7 @@
   12.76  lemma Memrel_separation:
   12.77       "separation(L, \<lambda>z. \<exists>x[L]. \<exists>y[L]. pair(L,x,y,z) & x \<in> y)"
   12.78  apply (rule separation_CollectI)
   12.79 -apply (rule_tac A="{z}" in subset_LsetE, blast )
   12.80 +apply (rule_tac A="{z}" in subset_LsetE, blast)
   12.81  apply (rule ReflectsE [OF Memrel_Reflects], assumption)
   12.82  apply (drule subset_Lset_ltD, assumption)
   12.83  apply (erule reflection_imp_L_separation)
   12.84 @@ -292,7 +292,7 @@
   12.85  apply (rule strong_replacementI)
   12.86  apply (rule rallI)
   12.87  apply (rule separation_CollectI)
   12.88 -apply (rule_tac A="{n,A,z}" in subset_LsetE, blast )
   12.89 +apply (rule_tac A="{n,A,z}" in subset_LsetE, blast)
   12.90  apply (rule ReflectsE [OF funspace_succ_Reflects], assumption)
   12.91  apply (drule subset_Lset_ltD, assumption)
   12.92  apply (erule reflection_imp_L_separation)
   12.93 @@ -320,7 +320,7 @@
   12.94        ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y[L]. (\<exists>p[L].
   12.95                       fun_apply(L,f,x,y) & pair(L,y,x,p) & p \<in> r)))"
   12.96  apply (rule separation_CollectI)
   12.97 -apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast )
   12.98 +apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast)
   12.99  apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption)
  12.100  apply (drule subset_Lset_ltD, assumption)
  12.101  apply (erule reflection_imp_L_separation)
  12.102 @@ -351,7 +351,7 @@
  12.103               ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
  12.104               order_isomorphism(L,par,r,x,mx,g))"
  12.105  apply (rule separation_CollectI)
  12.106 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
  12.107 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
  12.108  apply (rule ReflectsE [OF obase_reflects], assumption)
  12.109  apply (drule subset_Lset_ltD, assumption)
  12.110  apply (erule reflection_imp_L_separation)
  12.111 @@ -386,7 +386,7 @@
  12.112                                membership(L,y,my) & pred_set(L,A,x,r,pxr) &
  12.113                                order_isomorphism(L,pxr,r,y,my,g))))"
  12.114  apply (rule separation_CollectI)
  12.115 -apply (rule_tac A="{A,r,z}" in subset_LsetE, blast )
  12.116 +apply (rule_tac A="{A,r,z}" in subset_LsetE, blast)
  12.117  apply (rule ReflectsE [OF obase_equals_reflects], assumption)
  12.118  apply (drule subset_Lset_ltD, assumption)
  12.119  apply (erule reflection_imp_L_separation)
  12.120 @@ -422,7 +422,7 @@
  12.121  apply (rule rallI)
  12.122  apply (rename_tac B)
  12.123  apply (rule separation_CollectI)
  12.124 -apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast )
  12.125 +apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast)
  12.126  apply (rule ReflectsE [OF omap_reflects], assumption)
  12.127  apply (drule subset_Lset_ltD, assumption)
  12.128  apply (erule reflection_imp_L_separation)
  12.129 @@ -457,7 +457,7 @@
  12.130                  (\<exists>fx[L]. \<exists>gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) &
  12.131                                     fx \<noteq> gx))"
  12.132  apply (rule separation_CollectI)
  12.133 -apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast )
  12.134 +apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast)
  12.135  apply (rule ReflectsE [OF is_recfun_reflects], assumption)
  12.136  apply (drule subset_Lset_ltD, assumption)
  12.137  apply (erule reflection_imp_L_separation)
    13.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 12:48:49 2002 +0200
    13.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
    13.3 @@ -1,3 +1,9 @@
    13.4 +(*  Title:      ZF/Constructible/WF_absolute.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   2002  University of Cambridge
    13.8 +*)
    13.9 +
   13.10  header {*Absoluteness for Well-Founded Relations and Well-Founded Recursion*}
   13.11  
   13.12  theory WF_absolute = WFrec:
   13.13 @@ -310,7 +316,8 @@
   13.14   apply (rule univalent_is_recfun)
   13.15     apply (blast intro: wellfounded_trancl)
   13.16    apply (rule trans_trancl)
   13.17 - apply (simp add: trancl_subset_times, blast)
   13.18 + apply (simp add: trancl_subset_times) 
   13.19 +apply (blast dest: transM) 
   13.20  done
   13.21  
   13.22  lemma (in M_wfrank) Ord_wfrank_range [rule_format]:
   13.23 @@ -569,7 +576,7 @@
   13.24  apply (drule_tac x1=x and x="\<lambda>x\<in>r -`` {x}. wfrec(r, x, H)" 
   13.25         in rspec [THEN rspec]) 
   13.26  apply (simp_all add: function_lam) 
   13.27 -apply (blast intro: lam_closed dest: pair_components_in_M ) 
   13.28 +apply (blast intro: lam_closed dest: pair_components_in_M) 
   13.29  done
   13.30  
   13.31  text{*Eliminates one instance of replacement.*}
    14.1 --- a/src/ZF/Constructible/WFrec.thy	Fri Aug 16 12:48:49 2002 +0200
    14.2 +++ b/src/ZF/Constructible/WFrec.thy	Fri Aug 16 16:41:48 2002 +0200
    14.3 @@ -1,3 +1,9 @@
    14.4 +(*  Title:      ZF/Constructible/WFrec.thy
    14.5 +    ID:         $Id$
    14.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 +    Copyright   2002  University of Cambridge
    14.8 +*)
    14.9 +
   14.10  header{*Relativized Well-Founded Recursion*}
   14.11  
   14.12  theory WFrec = Wellorderings:
   14.13 @@ -190,7 +196,7 @@
   14.14   apply (frule is_recfun_type [THEN fun_is_rel], blast)
   14.15  apply (frule pair_components_in_M, assumption, clarify) 
   14.16  apply (rule iffI)
   14.17 - apply (frule_tac y="<y,z>" in transM, assumption )
   14.18 + apply (frule_tac y="<y,z>" in transM, assumption)
   14.19   apply (rotate_tac -1)   
   14.20   apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
   14.21  			   apply_recfun is_recfun_cut) 
    15.1 --- a/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 12:48:49 2002 +0200
    15.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Fri Aug 16 16:41:48 2002 +0200
    15.3 @@ -1,3 +1,9 @@
    15.4 +(*  Title:      ZF/Constructible/Wellorderings.thy
    15.5 +    ID:         $Id$
    15.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 +    Copyright   2002  University of Cambridge
    15.8 +*)
    15.9 +
   15.10  header {*Relativized Wellorderings*}
   15.11  
   15.12  theory Wellorderings = Relative:
   15.13 @@ -57,15 +63,15 @@
   15.14  
   15.15  lemma (in M_axioms) wellordered_is_trans_on: 
   15.16      "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
   15.17 -by (auto simp add: wellordered_def )
   15.18 +by (auto simp add: wellordered_def)
   15.19  
   15.20  lemma (in M_axioms) wellordered_is_linear: 
   15.21      "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
   15.22 -by (auto simp add: wellordered_def )
   15.23 +by (auto simp add: wellordered_def)
   15.24  
   15.25  lemma (in M_axioms) wellordered_is_wellfounded_on: 
   15.26      "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
   15.27 -by (auto simp add: wellordered_def )
   15.28 +by (auto simp add: wellordered_def)
   15.29  
   15.30  lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
   15.31      "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
   15.32 @@ -629,7 +635,7 @@
   15.33  lemma (in M_axioms) relativized_imp_well_ord: 
   15.34       "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
   15.35  apply (insert ordertype_exists [of A r], simp)
   15.36 -apply (blast intro: well_ord_ord_iso well_ord_Memrel )  
   15.37 +apply (blast intro: well_ord_ord_iso well_ord_Memrel)  
   15.38  done
   15.39  
   15.40  subsection {*Kunen's theorem 5.4, poage 127*}