proof streamlining
authorpaulson
Fri Nov 01 17:44:26 2002 +0100 (2002-11-01)
changeset 1369227f3c83e2984
parent 13691 a6bc3001106a
child 13693 77052bb8aed3
proof streamlining
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/DPow_absolute.thy
     1.1 --- a/src/ZF/Constructible/AC_in_L.thy	Fri Nov 01 17:43:54 2002 +0100
     1.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Fri Nov 01 17:44:26 2002 +0100
     1.3 @@ -18,16 +18,16 @@
     1.4    domains "rlist(A,r)" \<subseteq> "list(A) * list(A)"
     1.5    intros
     1.6      shorterI:
     1.7 -      "[| length(l') < length(l); l' \<in> list(A); l \<in> list(A) |] 
     1.8 +      "[| length(l') < length(l); l' \<in> list(A); l \<in> list(A) |]
     1.9         ==> <l', l> \<in> rlist(A,r)"
    1.10  
    1.11      sameI:
    1.12 -      "[| <l',l> \<in> rlist(A,r); a \<in> A |] 
    1.13 +      "[| <l',l> \<in> rlist(A,r); a \<in> A |]
    1.14         ==> <Cons(a,l'), Cons(a,l)> \<in> rlist(A,r)"
    1.15  
    1.16      diffI:
    1.17 -      "[| length(l') = length(l); <a',a> \<in> r; 
    1.18 -          l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |] 
    1.19 +      "[| length(l') = length(l); <a',a> \<in> r;
    1.20 +          l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |]
    1.21         ==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)"
    1.22    type_intros list.intros
    1.23  
    1.24 @@ -42,24 +42,24 @@
    1.25  
    1.26  lemma rlist_Nil_Cons [intro]:
    1.27      "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)"
    1.28 -by (simp add: shorterI) 
    1.29 +by (simp add: shorterI)
    1.30  
    1.31  lemma linear_rlist:
    1.32      "linear(A,r) ==> linear(list(A),rlist(A,r))"
    1.33  apply (simp (no_asm_simp) add: linear_def)
    1.34 -apply (rule ballI)  
    1.35 -apply (induct_tac x) 
    1.36 - apply (rule ballI)  
    1.37 - apply (induct_tac y)  
    1.38 -  apply (simp_all add: shorterI) 
    1.39 -apply (rule ballI)  
    1.40 -apply (erule_tac a=y in list.cases) 
    1.41 - apply (rename_tac [2] a2 l2) 
    1.42 +apply (rule ballI)
    1.43 +apply (induct_tac x)
    1.44 + apply (rule ballI)
    1.45 + apply (induct_tac y)
    1.46 +  apply (simp_all add: shorterI)
    1.47 +apply (rule ballI)
    1.48 +apply (erule_tac a=y in list.cases)
    1.49 + apply (rename_tac [2] a2 l2)
    1.50   apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt)
    1.51 -     apply (simp_all add: shorterI) 
    1.52 -apply (erule_tac x=a and y=a2 in linearE) 
    1.53 -    apply (simp_all add: diffI) 
    1.54 -apply (blast intro: sameI) 
    1.55 +     apply (simp_all add: shorterI)
    1.56 +apply (erule_tac x=a and y=a2 in linearE)
    1.57 +    apply (simp_all add: diffI)
    1.58 +apply (blast intro: sameI)
    1.59  done
    1.60  
    1.61  
    1.62 @@ -75,27 +75,27 @@
    1.63  
    1.64  lemma rlist_imp_length_le: "<l',l> \<in> rlist(A,r) ==> length(l') \<le> length(l)"
    1.65  apply (erule rlist.induct)
    1.66 -apply (simp_all add: leI)  
    1.67 +apply (simp_all add: leI)
    1.68  done
    1.69  
    1.70  lemma wf_on_rlist_n:
    1.71    "[| n \<in> nat; wf[A](r) |] ==> wf[{l \<in> list(A). length(l) = n}](rlist(A,r))"
    1.72 -apply (induct_tac n) 
    1.73 - apply (rule wf_onI2, simp) 
    1.74 -apply (rule wf_onI2, clarify) 
    1.75 -apply (erule_tac a=y in list.cases, clarify) 
    1.76 +apply (induct_tac n)
    1.77 + apply (rule wf_onI2, simp)
    1.78 +apply (rule wf_onI2, clarify)
    1.79 +apply (erule_tac a=y in list.cases, clarify)
    1.80   apply (simp (no_asm_use))
    1.81 -apply clarify 
    1.82 +apply clarify
    1.83  apply (simp (no_asm_use))
    1.84  apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x --> Cons(a,l2) \<in> B", blast)
    1.85  apply (erule_tac a=a in wf_on_induct, assumption)
    1.86  apply (rule ballI)
    1.87 -apply (rule impI) 
    1.88 +apply (rule impI)
    1.89  apply (erule_tac a=l2 in wf_on_induct, blast, clarify)
    1.90 -apply (rename_tac a' l2 l') 
    1.91 -apply (drule_tac x="Cons(a',l')" in bspec, typecheck) 
    1.92 -apply simp 
    1.93 -apply (erule mp, clarify) 
    1.94 +apply (rename_tac a' l2 l')
    1.95 +apply (drule_tac x="Cons(a',l')" in bspec, typecheck)
    1.96 +apply simp
    1.97 +apply (erule mp, clarify)
    1.98  apply (erule rlist_ConsE, auto)
    1.99  done
   1.100  
   1.101 @@ -104,22 +104,22 @@
   1.102  
   1.103  
   1.104  lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))"
   1.105 -apply (subst list_eq_UN_length) 
   1.106 -apply (rule wf_on_Union) 
   1.107 +apply (subst list_eq_UN_length)
   1.108 +apply (rule wf_on_Union)
   1.109    apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]])
   1.110   apply (simp add: wf_on_rlist_n)
   1.111 -apply (frule rlist_type [THEN subsetD]) 
   1.112 -apply (simp add: length_type)   
   1.113 +apply (frule rlist_type [THEN subsetD])
   1.114 +apply (simp add: length_type)
   1.115  apply (drule rlist_imp_length_le)
   1.116 -apply (erule leE) 
   1.117 -apply (simp_all add: lt_def) 
   1.118 +apply (erule leE)
   1.119 +apply (simp_all add: lt_def)
   1.120  done
   1.121  
   1.122  
   1.123  lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))"
   1.124  apply (simp add: wf_iff_wf_on_field)
   1.125  apply (rule wf_on_subset_A [OF _ field_rlist])
   1.126 -apply (blast intro: wf_on_rlist) 
   1.127 +apply (blast intro: wf_on_rlist)
   1.128  done
   1.129  
   1.130  lemma well_ord_rlist:
   1.131 @@ -136,11 +136,15 @@
   1.132  nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k)
   1.133  enumerates the triangular numbers and can be defined by triangle(0)=0,
   1.134  triangle(succ(k)) = succ(k + triangle(k)).  Some small amount of effort is
   1.135 -needed to show that f is a bijection.  We already know (by the theorem @{text
   1.136 -InfCard_square_eqpoll}) that such a bijection exists, but as we have no direct
   1.137 -way to refer to it, we must use a locale.*}
   1.138 +needed to show that f is a bijection.  We already know that such a bijection exists by the theorem @{text well_ord_InfCard_square_eq}:
   1.139 +@{thm[display] well_ord_InfCard_square_eq[no_vars]}
   1.140  
   1.141 -text{*Locale for any arbitrary injection between @{term "nat*nat"} 
   1.142 +However, this result merely states that there is a bijection between the two
   1.143 +sets.  It provides no means of naming a specific bijection.  Therefore, we
   1.144 +conduct the proofs under the assumption that a bijection exists.  The simplest
   1.145 +way to organize this is to use a locale.*}
   1.146 +
   1.147 +text{*Locale for any arbitrary injection between @{term "nat*nat"}
   1.148        and @{term nat}*}
   1.149  locale Nat_Times_Nat =
   1.150    fixes fn
   1.151 @@ -156,45 +160,45 @@
   1.152  
   1.153  lemma (in Nat_Times_Nat) fn_type [TC,simp]:
   1.154      "[|x \<in> nat; y \<in> nat|] ==> fn`<x,y> \<in> nat"
   1.155 -by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) 
   1.156 +by (blast intro: inj_is_fun [OF fn_inj] apply_funtype)
   1.157  
   1.158  lemma (in Nat_Times_Nat) fn_iff:
   1.159 -    "[|x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat|] 
   1.160 +    "[|x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat|]
   1.161       ==> (fn`<x,y> = fn`<u,v>) <-> (x=u & y=v)"
   1.162 -by (blast dest: inj_apply_equality [OF fn_inj]) 
   1.163 +by (blast dest: inj_apply_equality [OF fn_inj])
   1.164  
   1.165  lemma (in Nat_Times_Nat) enum_type [TC,simp]:
   1.166      "p \<in> formula ==> enum(fn,p) \<in> nat"
   1.167 -by (induct_tac p, simp_all) 
   1.168 +by (induct_tac p, simp_all)
   1.169  
   1.170  lemma (in Nat_Times_Nat) enum_inject [rule_format]:
   1.171      "p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) --> p=q"
   1.172 -apply (induct_tac p, simp_all) 
   1.173 -   apply (rule ballI) 
   1.174 -   apply (erule formula.cases) 
   1.175 -   apply (simp_all add: fn_iff) 
   1.176 -  apply (rule ballI) 
   1.177 -  apply (erule formula.cases) 
   1.178 -  apply (simp_all add: fn_iff) 
   1.179 - apply (rule ballI) 
   1.180 - apply (erule_tac a=qa in formula.cases) 
   1.181 - apply (simp_all add: fn_iff) 
   1.182 - apply blast 
   1.183 -apply (rule ballI) 
   1.184 -apply (erule_tac a=q in formula.cases) 
   1.185 -apply (simp_all add: fn_iff, blast) 
   1.186 +apply (induct_tac p, simp_all)
   1.187 +   apply (rule ballI)
   1.188 +   apply (erule formula.cases)
   1.189 +   apply (simp_all add: fn_iff)
   1.190 +  apply (rule ballI)
   1.191 +  apply (erule formula.cases)
   1.192 +  apply (simp_all add: fn_iff)
   1.193 + apply (rule ballI)
   1.194 + apply (erule_tac a=qa in formula.cases)
   1.195 + apply (simp_all add: fn_iff)
   1.196 + apply blast
   1.197 +apply (rule ballI)
   1.198 +apply (erule_tac a=q in formula.cases)
   1.199 +apply (simp_all add: fn_iff, blast)
   1.200  done
   1.201  
   1.202  lemma (in Nat_Times_Nat) inj_formula_nat:
   1.203      "(\<lambda>p \<in> formula. enum(fn,p)) \<in> inj(formula, nat)"
   1.204 -apply (simp add: inj_def lam_type) 
   1.205 -apply (blast intro: enum_inject) 
   1.206 +apply (simp add: inj_def lam_type)
   1.207 +apply (blast intro: enum_inject)
   1.208  done
   1.209  
   1.210  lemma (in Nat_Times_Nat) well_ord_formula:
   1.211      "well_ord(formula, measure(formula, enum(fn)))"
   1.212  apply (rule well_ord_measure, simp)
   1.213 -apply (blast intro: enum_inject)   
   1.214 +apply (blast intro: enum_inject)
   1.215  done
   1.216  
   1.217  lemmas nat_times_nat_lepoll_nat =
   1.218 @@ -205,9 +209,150 @@
   1.219  theorem formula_lepoll_nat: "formula \<lesssim> nat"
   1.220  apply (insert nat_times_nat_lepoll_nat)
   1.221  apply (unfold lepoll_def)
   1.222 -apply (blast intro: exI Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
   1.223 +apply (blast intro: Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
   1.224 +done
   1.225 +
   1.226 +
   1.227 +subsection{*Defining the Wellordering on @{term "DPow(A)"}*}
   1.228 +
   1.229 +text{*The objective is to build a wellordering on @{term "DPow(A)"} from a
   1.230 +given one on @{term A}.  We first introduce wellorderings for environments,
   1.231 +which are lists built over @{term "A"}.  We combine it with the enumeration of
   1.232 +formulas.  The order type of the resulting wellordering gives us a map from
   1.233 +(environment, formula) pairs into the ordinals.  For each member of @{term
   1.234 +"DPow(A)"}, we take the minimum such ordinal.  This yields a wellordering of
   1.235 +@{term "DPow(A)-A"}, namely the set of elements just introduced, which we then
   1.236 +extend to the full set @{term "DPow(A)"}.*}
   1.237 +
   1.238 +constdefs
   1.239 +  env_form_r :: "[i,i,i]=>i"
   1.240 +    --{*wellordering on (environment, formula) pairs*}
   1.241 +   "env_form_r(f,r,A) ==
   1.242 +      rmult(list(A), rlist(A, r),
   1.243 +	    formula, measure(formula, enum(f)))"
   1.244 +
   1.245 +  env_form_map :: "[i,i,i,i]=>i"
   1.246 +    --{*map from (environment, formula) pairs to ordinals*}
   1.247 +   "env_form_map(f,r,A,z)
   1.248 +      == ordermap(list(A) * formula, env_form_r(f,r,A)) ` z"
   1.249 +
   1.250 +  DPow_new_ord :: "[i,i,i,i,i]=>o"
   1.251 +    --{*predicate that holds if @{term k} is a valid index for @{term X}*}
   1.252 +   "DPow_new_ord(f,r,A,X,k) ==
   1.253 +           \<exists>env \<in> list(A). \<exists>p \<in> formula.
   1.254 +             arity(p) \<le> succ(length(env)) &
   1.255 +             X = {x\<in>A. sats(A, p, Cons(x,env))} &
   1.256 +             env_form_map(f,r,A,<env,p>) = k"
   1.257 +
   1.258 +  DPow_new_least :: "[i,i,i,i]=>i"
   1.259 +    --{*function yielding the smallest index for @{term X}*}
   1.260 +   "DPow_new_least(f,r,A,X) == \<mu>k. DPow_new_ord(f,r,A,X,k)"
   1.261 +
   1.262 +  DPow_new_r :: "[i,i,i]=>i"
   1.263 +    --{*a wellordering on the difference set @{term "DPow(A)-A"}*}
   1.264 +   "DPow_new_r(f,r,A) == measure(DPow(A)-A, DPow_new_least(f,r,A))"
   1.265 +
   1.266 +  DPow_r :: "[i,i,i]=>i"
   1.267 +    --{*a wellordering on @{term "DPow(A)"}*}
   1.268 +   "DPow_r(f,r,A) == (DPow_new_r(f,r,A) Un (A * (DPow(A)-A))) Un r"
   1.269 +
   1.270 +
   1.271 +lemma (in Nat_Times_Nat) well_ord_env_form_r:
   1.272 +    "well_ord(A,r)
   1.273 +     ==> well_ord(list(A) * formula, env_form_r(fn,r,A))"
   1.274 +by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula)
   1.275 +
   1.276 +lemma (in Nat_Times_Nat) Ord_env_form_map:
   1.277 +    "[|well_ord(A,r); z \<in> list(A) * formula|]
   1.278 +     ==> Ord(env_form_map(fn,r,A,z))"
   1.279 +by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r)
   1.280 +
   1.281 +lemma DPow_imp_ex_DPow_new_ord:
   1.282 +    "X \<in> DPow(A) ==> \<exists>k. DPow_new_ord(fn,r,A,X,k)"
   1.283 +apply (simp add: DPow_new_ord_def)
   1.284 +apply (blast dest!: DPowD)
   1.285 +done
   1.286 +
   1.287 +lemma (in Nat_Times_Nat) DPow_new_ord_imp_Ord:
   1.288 +     "[|DPow_new_ord(fn,r,A,X,k); well_ord(A,r)|] ==> Ord(k)"
   1.289 +apply (simp add: DPow_new_ord_def, clarify)
   1.290 +apply (simp add: Ord_env_form_map)
   1.291  done
   1.292  
   1.293 +lemma (in Nat_Times_Nat) DPow_imp_DPow_new_least:
   1.294 +    "[|X \<in> DPow(A); well_ord(A,r)|]
   1.295 +     ==> DPow_new_ord(fn, r, A, X, DPow_new_least(fn,r,A,X))"
   1.296 +apply (simp add: DPow_new_least_def)
   1.297 +apply (blast dest: DPow_imp_ex_DPow_new_ord intro: DPow_new_ord_imp_Ord LeastI)
   1.298 +done
   1.299 +
   1.300 +lemma (in Nat_Times_Nat) env_form_map_inject:
   1.301 +    "[|env_form_map(fn,r,A,u) = env_form_map(fn,r,A,v); well_ord(A,r);
   1.302 +       u \<in> list(A) * formula;  v \<in> list(A) * formula|]
   1.303 +     ==> u=v"
   1.304 +apply (simp add: env_form_map_def)
   1.305 +apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij,
   1.306 +                                OF well_ord_env_form_r], assumption+)
   1.307 +done
   1.308 +
   1.309 +
   1.310 +lemma (in Nat_Times_Nat) DPow_new_ord_unique:
   1.311 +    "[|DPow_new_ord(fn,r,A,X,k); DPow_new_ord(fn,r,A,Y,k); well_ord(A,r)|]
   1.312 +     ==> X=Y"
   1.313 +apply (simp add: DPow_new_ord_def, clarify)
   1.314 +apply (drule env_form_map_inject, auto)
   1.315 +done
   1.316 +
   1.317 +lemma (in Nat_Times_Nat) well_ord_DPow_new_r:
   1.318 +    "well_ord(A,r) ==> well_ord(DPow(A)-A, DPow_new_r(fn,r,A))"
   1.319 +apply (simp add: DPow_new_r_def)
   1.320 +apply (rule well_ord_measure)
   1.321 + apply (simp add: DPow_new_least_def Ord_Least, clarify)
   1.322 +apply (drule DPow_imp_DPow_new_least, assumption)+
   1.323 +apply simp
   1.324 +apply (blast intro: DPow_new_ord_unique)
   1.325 +done
   1.326 +
   1.327 +lemma DPow_new_r_subset: "DPow_new_r(f,r,A) <= (DPow(A)-A) * (DPow(A)-A)"
   1.328 +by (simp add: DPow_new_r_def measure_type)
   1.329 +
   1.330 +lemma (in Nat_Times_Nat) linear_DPow_r:
   1.331 +    "well_ord(A,r)
   1.332 +     ==> linear(DPow(A), DPow_r(fn, r, A))"
   1.333 +apply (frule well_ord_DPow_new_r)
   1.334 +apply (drule well_ord_is_linear)+
   1.335 +apply (auto simp add: linear_def DPow_r_def)
   1.336 +done
   1.337 +
   1.338 +
   1.339 +lemma (in Nat_Times_Nat) wf_DPow_new_r:
   1.340 +    "well_ord(A,r) ==> wf(DPow_new_r(fn,r,A))"
   1.341 +apply (rule well_ord_DPow_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf],
   1.342 +       assumption+)
   1.343 +apply (rule DPow_new_r_subset)
   1.344 +done
   1.345 +
   1.346 +lemma (in Nat_Times_Nat) well_ord_DPow_r:
   1.347 +    "[|well_ord(A,r); r \<subseteq> A * A|]
   1.348 +     ==> well_ord(DPow(A), DPow_r(fn,r,A))"
   1.349 +apply (rule well_ordI [OF wf_imp_wf_on])
   1.350 + prefer 2 apply (blast intro: linear_DPow_r)
   1.351 +apply (simp add: DPow_r_def)
   1.352 +apply (rule wf_Un)
   1.353 +  apply (cut_tac DPow_new_r_subset [of fn r A], blast)
   1.354 + apply (rule wf_Un)
   1.355 +   apply (cut_tac DPow_new_r_subset [of fn r A], blast)
   1.356 +  apply (blast intro: wf_DPow_new_r)
   1.357 + apply (simp add: wf_times Diff_disjoint)
   1.358 +apply (blast intro: well_ord_is_wf wf_on_imp_wf)
   1.359 +done
   1.360 +
   1.361 +lemma (in Nat_Times_Nat) DPow_r_type:
   1.362 +    "[|r \<subseteq> A * A; A \<subseteq> DPow(A)|]
   1.363 +     ==> DPow_r(fn,r,A) \<subseteq> DPow(A) * DPow(A)"
   1.364 +apply (simp add: DPow_r_def DPow_new_r_def measure_def, blast)
   1.365 +done		
   1.366 +
   1.367  
   1.368  subsection{*Limit Construction for Well-Orderings*}
   1.369  
   1.370 @@ -215,299 +360,149 @@
   1.371  @{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
   1.372  of wellorderings for smaller ordinals.*}
   1.373  
   1.374 -text{*This constant denotes the set of elements introduced at level
   1.375 -@{term "succ(i)"}*}
   1.376  constdefs
   1.377 +  rlimit :: "[i,i=>i]=>i"
   1.378 +  --{*expresses the wellordering at limit ordinals.*}
   1.379 +    "rlimit(i,r) ==
   1.380 +       {z: Lset(i) * Lset(i).
   1.381 +        \<exists>x' x. z = <x',x> &
   1.382 +               (lrank(x') < lrank(x) |
   1.383 +                (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}"
   1.384 +
   1.385    Lset_new :: "i=>i"
   1.386 +  --{*This constant denotes the set of elements introduced at level
   1.387 +      @{term "succ(i)"}*}
   1.388      "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
   1.389  
   1.390  lemma Lset_new_iff_lrank_eq:
   1.391       "Ord(i) ==> x \<in> Lset_new(i) <-> L(x) & lrank(x) = i"
   1.392 -by (auto simp add: Lset_new_def Lset_iff_lrank_lt) 
   1.393 +by (auto simp add: Lset_new_def Lset_iff_lrank_lt)
   1.394  
   1.395  lemma Lset_new_eq:
   1.396       "Ord(i) ==> Lset_new(i) = Lset(succ(i)) - Lset(i)"
   1.397  apply (rule equality_iffI)
   1.398 -apply (simp add: Lset_new_iff_lrank_eq Lset_iff_lrank_lt, auto) 
   1.399 -apply (blast elim: leE) 
   1.400 +apply (simp add: Lset_new_iff_lrank_eq Lset_iff_lrank_lt, auto)
   1.401 +apply (blast elim: leE)
   1.402  done
   1.403  
   1.404  lemma Limit_Lset_eq2:
   1.405      "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))"
   1.406 -apply (simp add: Limit_Lset_eq) 
   1.407 +apply (simp add: Limit_Lset_eq)
   1.408  apply (rule equalityI)
   1.409   apply safe
   1.410   apply (subgoal_tac "Ord(y)")
   1.411    prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord)
   1.412 - apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
   1.413 -                      Ord_mem_iff_lt) 
   1.414 - apply (blast intro: lt_trans) 
   1.415 + apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def
   1.416 +                      Ord_mem_iff_lt)
   1.417 + apply (blast intro: lt_trans)
   1.418  apply (rule_tac x = "succ(lrank(x))" in bexI)
   1.419 - apply (simp add: Lset_succ_lrank_iff) 
   1.420 -apply (blast intro: Limit_has_succ ltD) 
   1.421 -done
   1.422 -
   1.423 -text{*This constant expresses the wellordering at limit ordinals.*}
   1.424 -constdefs
   1.425 -  rlimit :: "[i,i=>i]=>i"
   1.426 -    "rlimit(i,r) == 
   1.427 -       {z: Lset(i) * Lset(i).
   1.428 -        \<exists>x' x. z = <x',x> &         
   1.429 -               (lrank(x') < lrank(x) | 
   1.430 -                (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}"
   1.431 -
   1.432 -lemma rlimit_eqI:
   1.433 -     "[|Limit(i); \<forall>j<i. r'(j) = r(j)|] ==> rlimit(i,r) = rlimit(i,r')"
   1.434 -apply (simp add: rlimit_def) 
   1.435 -apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+
   1.436 -apply (simp add: Limit_is_Ord Lset_lrank_lt)  
   1.437 + apply (simp add: Lset_succ_lrank_iff)
   1.438 +apply (blast intro: Limit_has_succ ltD)
   1.439  done
   1.440  
   1.441  lemma wf_on_Lset:
   1.442      "wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))"
   1.443 -apply (simp add: wf_on_def Lset_new_def) 
   1.444 -apply (erule wf_subset) 
   1.445 -apply (force simp add: rlimit_def) 
   1.446 +apply (simp add: wf_on_def Lset_new_def)
   1.447 +apply (erule wf_subset)
   1.448 +apply (force simp add: rlimit_def)
   1.449  done
   1.450  
   1.451  lemma wf_on_rlimit:
   1.452      "[|Limit(i); \<forall>j<i. wf[Lset(j)](r(j)) |] ==> wf[Lset(i)](rlimit(i,r))"
   1.453  apply (simp add: Limit_Lset_eq2)
   1.454  apply (rule wf_on_Union)
   1.455 -  apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) 
   1.456 - apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) 
   1.457 +  apply (rule wf_imp_wf_on [OF wf_Memrel [of i]])
   1.458 + apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI)
   1.459  apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def
   1.460                         Ord_mem_iff_lt)
   1.461 -
   1.462  done
   1.463  
   1.464  lemma linear_rlimit:
   1.465      "[|Limit(i); \<forall>j<i. linear(Lset(j), r(j)) |]
   1.466       ==> linear(Lset(i), rlimit(i,r))"
   1.467 -apply (frule Limit_is_Ord) 
   1.468 -apply (simp add: Limit_Lset_eq2)
   1.469 -apply (simp add: linear_def Lset_new_def rlimit_def Ball_def) 
   1.470 -apply (simp add: lt_Ord Lset_iff_lrank_lt) 
   1.471 -apply (simp add: ltI, clarify) 
   1.472 -apply (rename_tac u v) 
   1.473 -apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt) 
   1.474 -apply simp_all
   1.475 -apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) 
   1.476 -apply (simp add: ltI)
   1.477 -apply (drule_tac x=u in spec, simp) 
   1.478 -apply (drule_tac x=v in spec, simp) 
   1.479 +apply (frule Limit_is_Ord)
   1.480 +apply (simp add: Limit_Lset_eq2 Lset_new_def)
   1.481 +apply (simp add: linear_def rlimit_def Ball_def lt_Ord Lset_iff_lrank_lt)
   1.482 +apply (simp add: ltI, clarify)
   1.483 +apply (rename_tac u v)
   1.484 +apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt, simp_all) 
   1.485 +apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec)
   1.486 + apply (simp add: ltI)
   1.487 +apply (drule_tac x=u in spec, simp)
   1.488 +apply (drule_tac x=v in spec, simp)
   1.489  done
   1.490  
   1.491 -
   1.492  lemma well_ord_rlimit:
   1.493      "[|Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) |]
   1.494       ==> well_ord(Lset(i), rlimit(i,r))"
   1.495 -by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf 
   1.496 -                           linear_rlimit well_ord_is_linear) 
   1.497 -
   1.498 -
   1.499 -subsection{*Defining the Wellordering on @{term "Lset(succ(i))"}*}
   1.500 -
   1.501 -text{*We introduce wellorderings for environments, which are lists built over
   1.502 -@{term "Lset(succ(i))"}.  We combine it with the enumeration of formulas.  The
   1.503 -order type of the resulting wellordering gives us a map from (environment,
   1.504 -formula) pairs into the ordinals.  For each member of @{term "DPow(Lset(i))"},
   1.505 -we take the minimum such ordinal.  This yields a wellordering of
   1.506 -@{term "DPow(Lset(i))"}, which we then extend to @{term "Lset(succ(i))"}*}
   1.507 -
   1.508 -constdefs
   1.509 -  env_form_r :: "[i,i,i]=>i"
   1.510 -    --{*wellordering on (environment, formula) pairs*}
   1.511 -   "env_form_r(f,r,i) ==
   1.512 -      rmult(list(Lset(i)), rlist(Lset(i), r),
   1.513 -	    formula, measure(formula, enum(f)))"
   1.514 -
   1.515 -  env_form_map :: "[i,i,i,i]=>i"
   1.516 -    --{*map from (environment, formula) pairs to ordinals*}
   1.517 -   "env_form_map(f,r,i,z) 
   1.518 -      == ordermap(list(Lset(i)) * formula, env_form_r(f,r,i)) ` z"
   1.519 -
   1.520 -  L_new_ord :: "[i,i,i,i,i]=>o"
   1.521 -    --{*predicate that holds if @{term k} is a valid index for @{term X}*}
   1.522 -   "L_new_ord(f,r,i,X,k) ==  
   1.523 -           \<exists>env \<in> list(Lset(i)). \<exists>p \<in> formula. 
   1.524 -             arity(p) \<le> succ(length(env)) & 
   1.525 -             X = {x\<in>Lset(i). sats(Lset(i), p, Cons(x,env))} &
   1.526 -             env_form_map(f,r,i,<env,p>) = k"
   1.527 -
   1.528 -  L_new_least :: "[i,i,i,i]=>i"
   1.529 -    --{*function yielding the smallest index for @{term X}*}
   1.530 -   "L_new_least(f,r,i,X) == \<mu>k. L_new_ord(f,r,i,X,k)"
   1.531 -
   1.532 -  L_new_r :: "[i,i,i]=>i"
   1.533 -    --{*a wellordering on @{term "DPow(Lset(i))"}*}
   1.534 -   "L_new_r(f,r,i) == measure(Lset_new(i), L_new_least(f,r,i))"
   1.535 -
   1.536 -  L_succ_r :: "[i,i,i]=>i"
   1.537 -    --{*a wellordering on @{term "Lset(succ(i))"}*}
   1.538 -   "L_succ_r(f,r,i) == (L_new_r(f,r,i) Un (Lset(i) * Lset_new(i))) Un r"
   1.539 -
   1.540 -
   1.541 -lemma (in Nat_Times_Nat) well_ord_env_form_r:
   1.542 -    "well_ord(Lset(i), r) 
   1.543 -     ==> well_ord(list(Lset(i)) * formula, env_form_r(fn,r,i))"
   1.544 -by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) 
   1.545 -
   1.546 -lemma (in Nat_Times_Nat) Ord_env_form_map:
   1.547 -    "[|well_ord(Lset(i), r); z \<in> list(Lset(i)) * formula|]
   1.548 -     ==> Ord(env_form_map(fn,r,i,z))"
   1.549 -by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) 
   1.550 -
   1.551 -
   1.552 -lemma DPow_imp_ex_L_new_ord:
   1.553 -    "X \<in> DPow(Lset(i)) ==> \<exists>k. L_new_ord(fn,r,i,X,k)"
   1.554 -apply (simp add: L_new_ord_def) 
   1.555 -apply (blast dest!: DPowD) 
   1.556 -done
   1.557 -
   1.558 -lemma (in Nat_Times_Nat) L_new_ord_imp_Ord:
   1.559 -     "[|L_new_ord(fn,r,i,X,k); well_ord(Lset(i), r)|] ==> Ord(k)"
   1.560 -apply (simp add: L_new_ord_def, clarify)
   1.561 -apply (simp add: Ord_env_form_map)  
   1.562 -done
   1.563 -
   1.564 -lemma (in Nat_Times_Nat) DPow_imp_L_new_least:
   1.565 -    "[|X \<in> DPow(Lset(i)); well_ord(Lset(i), r)|] 
   1.566 -     ==> L_new_ord(fn, r, i, X, L_new_least(fn,r,i,X))"
   1.567 -apply (simp add: L_new_least_def)
   1.568 -apply (blast dest!: DPow_imp_ex_L_new_ord intro: L_new_ord_imp_Ord LeastI)  
   1.569 -done
   1.570 -
   1.571 -lemma (in Nat_Times_Nat) env_form_map_inject:
   1.572 -    "[|env_form_map(fn,r,i,u) = env_form_map(fn,r,i,v); well_ord(Lset(i), r);  
   1.573 -       u \<in> list(Lset(i)) * formula;  v \<in> list(Lset(i)) * formula|] 
   1.574 -     ==> u=v"
   1.575 -apply (simp add: env_form_map_def) 
   1.576 -apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, 
   1.577 -                                OF well_ord_env_form_r], assumption+)
   1.578 -done
   1.579 -
   1.580 -
   1.581 -lemma (in Nat_Times_Nat) L_new_ord_unique:
   1.582 -    "[|L_new_ord(fn,r,i,X,k); L_new_ord(fn,r,i,Y,k); well_ord(Lset(i), r)|] 
   1.583 -     ==> X=Y"
   1.584 -apply (simp add: L_new_ord_def, clarify)
   1.585 -apply (drule env_form_map_inject, auto) 
   1.586 -done
   1.587 -
   1.588 -lemma (in Nat_Times_Nat) well_ord_L_new_r:
   1.589 -    "[|Ord(i); well_ord(Lset(i), r)|]
   1.590 -     ==> well_ord(Lset_new(i), L_new_r(fn,r,i))"
   1.591 -apply (simp add: L_new_r_def) 
   1.592 -apply (rule well_ord_measure) 
   1.593 - apply (simp add: L_new_least_def Ord_Least)
   1.594 -apply (simp add: Lset_new_eq Lset_succ, clarify) 
   1.595 -apply (drule DPow_imp_L_new_least, assumption)+
   1.596 -apply simp 
   1.597 -apply (blast intro: L_new_ord_unique) 
   1.598 -done
   1.599 -
   1.600 -lemma L_new_r_subset: "L_new_r(f,r,i) <= Lset_new(i) * Lset_new(i)"
   1.601 -by (simp add: L_new_r_def measure_type)
   1.602 -
   1.603 -lemma Lset_Lset_new_disjoint: "Ord(i) ==> Lset(i) \<inter> Lset_new(i) = 0"
   1.604 -by (simp add: Lset_new_eq, blast)
   1.605 -
   1.606 -lemma (in Nat_Times_Nat) linear_L_succ_r:
   1.607 -    "[|Ord(i); well_ord(Lset(i), r)|]
   1.608 -     ==> linear(Lset(succ(i)), L_succ_r(fn, r, i))"
   1.609 -apply (frule well_ord_L_new_r, assumption) 
   1.610 -apply (drule well_ord_is_linear)+
   1.611 -apply (simp add: linear_def L_succ_r_def Lset_new_eq, auto) 
   1.612 -done
   1.613 -
   1.614 -
   1.615 -lemma (in Nat_Times_Nat) wf_L_new_r:
   1.616 -    "[|Ord(i); well_ord(Lset(i), r)|] ==> wf(L_new_r(fn,r,i))"
   1.617 -apply (rule well_ord_L_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf], 
   1.618 -       assumption+)
   1.619 -apply (rule L_new_r_subset)
   1.620 -done
   1.621 -
   1.622 -
   1.623 -lemma (in Nat_Times_Nat) well_ord_L_succ_r:
   1.624 -    "[|Ord(i); well_ord(Lset(i), r); r \<subseteq> Lset(i) * Lset(i)|]
   1.625 -     ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))"
   1.626 -apply (rule well_ordI [OF wf_imp_wf_on])
   1.627 - prefer 2 apply (blast intro: linear_L_succ_r) 
   1.628 -apply (simp add: L_succ_r_def)
   1.629 -apply (rule wf_Un)
   1.630 -  apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast)
   1.631 - apply (rule wf_Un)  
   1.632 -   apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast)
   1.633 -  apply (blast intro: wf_L_new_r) 
   1.634 - apply (simp add: wf_times Lset_Lset_new_disjoint)
   1.635 -apply (blast intro: well_ord_is_wf wf_on_imp_wf)
   1.636 -done
   1.637 -
   1.638 -
   1.639 -lemma (in Nat_Times_Nat) L_succ_r_type:
   1.640 -    "[|Ord(i); r \<subseteq> Lset(i) * Lset(i)|]
   1.641 -     ==> L_succ_r(fn,r,i) \<subseteq> Lset(succ(i)) * Lset(succ(i))"
   1.642 -apply (simp add: L_succ_r_def L_new_r_def measure_def Lset_new_eq) 
   1.643 -apply (blast intro: Lset_mono_mem [OF succI1, THEN subsetD] ) 
   1.644 -done				   
   1.645 +by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf
   1.646 +                           linear_rlimit well_ord_is_linear)
   1.647  
   1.648  
   1.649  subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
   1.650  
   1.651  constdefs
   1.652   L_r :: "[i, i] => i"
   1.653 -  "L_r(f,i) == 
   1.654 -      transrec(i, \<lambda>x r. 
   1.655 +  "L_r(f,i) ==
   1.656 +      transrec(i, \<lambda>x r.
   1.657           if x=0 then 0
   1.658           else if Limit(x) then rlimit(x, \<lambda>y. r`y)
   1.659 -         else L_succ_r(f, r ` Arith.pred(x), Arith.pred(x)))"
   1.660 +         else DPow_r(f, r ` Arith.pred(x), Lset(Arith.pred(x))))"
   1.661  
   1.662  subsubsection{*The Corresponding Recursion Equations*}
   1.663  lemma [simp]: "L_r(f,0) = 0"
   1.664  by (simp add: def_transrec [OF L_r_def])
   1.665  
   1.666 -lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = L_succ_r(f, L_r(f,i), i)"
   1.667 +lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = DPow_r(f, L_r(f,i), Lset(i))"
   1.668  by (simp add: def_transrec [OF L_r_def])
   1.669  
   1.670  text{*Needed to handle the limit case*}
   1.671  lemma L_r_eq:
   1.672 -     "Ord(i) ==> 
   1.673 +     "Ord(i) ==>
   1.674        L_r(f, i) =
   1.675        (if i = 0 then 0
   1.676         else if Limit(i) then rlimit(i, op `(Lambda(i, L_r(f))))
   1.677 -       else L_succ_r (f, Lambda(i, L_r(f)) ` Arith.pred(i), Arith.pred(i)))"
   1.678 +       else DPow_r (f, Lambda(i, L_r(f)) ` Arith.pred(i),
   1.679 +                    Lset(Arith.pred(i))))"
   1.680  apply (induct i rule: trans_induct3_rule)
   1.681  apply (simp_all add: def_transrec [OF L_r_def])
   1.682  done
   1.683  
   1.684 +lemma rlimit_eqI:
   1.685 +     "[|Limit(i); \<forall>j<i. r'(j) = r(j)|] ==> rlimit(i,r) = rlimit(i,r')"
   1.686 +apply (simp add: rlimit_def)
   1.687 +apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+
   1.688 +apply (simp add: Limit_is_Ord Lset_lrank_lt)
   1.689 +done
   1.690 +
   1.691  text{*I don't know why the limit case is so complicated.*}
   1.692  lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))"
   1.693  apply (simp add: Limit_nonzero def_transrec [OF L_r_def])
   1.694  apply (rule rlimit_eqI, assumption)
   1.695  apply (rule oallI)
   1.696 -apply (frule lt_Ord) 
   1.697 -apply (simp only: beta ltD L_r_eq [symmetric])  
   1.698 +apply (frule lt_Ord)
   1.699 +apply (simp only: beta ltD L_r_eq [symmetric])
   1.700  done
   1.701  
   1.702  lemma (in Nat_Times_Nat) L_r_type:
   1.703      "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)"
   1.704  apply (induct i rule: trans_induct3_rule)
   1.705 -  apply (simp_all add: L_succ_r_type well_ord_L_succ_r rlimit_def, blast) 
   1.706 +  apply (simp_all add: Lset_succ DPow_r_type well_ord_DPow_r rlimit_def
   1.707 +                       Transset_subset_DPow [OF Transset_Lset], blast)
   1.708  done
   1.709  
   1.710  lemma (in Nat_Times_Nat) well_ord_L_r:
   1.711      "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))"
   1.712  apply (induct i rule: trans_induct3_rule)
   1.713 -apply (simp_all add: well_ord0 L_r_type well_ord_L_succ_r well_ord_rlimit ltD)
   1.714 +apply (simp_all add: well_ord0 Lset_succ L_r_type well_ord_DPow_r
   1.715 +                     well_ord_rlimit ltD)
   1.716  done
   1.717  
   1.718  lemma well_ord_L_r:
   1.719      "Ord(i) ==> \<exists>r. well_ord(Lset(i), r)"
   1.720  apply (insert nat_times_nat_lepoll_nat)
   1.721  apply (unfold lepoll_def)
   1.722 -apply (blast intro: exI Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
   1.723 +apply (blast intro: Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
   1.724  done
   1.725  
   1.726  
   1.727 @@ -518,9 +513,9 @@
   1.728  text{*The Axiom of Choice holds in @{term L}!  Or, to be precise, the
   1.729  Wellordering Theorem.*}
   1.730  theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)"
   1.731 -apply (insert Transset_Lset VL [of x]) 
   1.732 +apply (insert Transset_Lset VL [of x])
   1.733  apply (simp add: Transset_def L_def)
   1.734 -apply (blast dest!: well_ord_L_r intro: well_ord_subset) 
   1.735 +apply (blast dest!: well_ord_L_r intro: well_ord_subset)
   1.736  done
   1.737  
   1.738  end
     2.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Fri Nov 01 17:43:54 2002 +0100
     2.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Fri Nov 01 17:44:26 2002 +0100
     2.3 @@ -111,71 +111,72 @@
     2.4  subsection {*Relativization of the Operator @{term DPow'}*}
     2.5  
     2.6  lemma DPow'_eq: 
     2.7 -  "DPow'(A) = Replace(list(A) * formula,
     2.8 -              %ep z. \<exists>env \<in> list(A). \<exists>p \<in> formula. 
     2.9 -                     ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))})"
    2.10 -apply (simp add: DPow'_def, blast) 
    2.11 -done
    2.12 +  "DPow'(A) = {z . ep \<in> list(A) * formula, 
    2.13 +                    \<exists>env \<in> list(A). \<exists>p \<in> formula. 
    2.14 +                       ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))}}"
    2.15 +by (simp add: DPow'_def, blast) 
    2.16  
    2.17  
    2.18 +text{*Relativize the use of @{term sats} within @{term DPow'}
    2.19 +(the comprehension).*}
    2.20  constdefs
    2.21 -  is_DPow_body :: "[i=>o,i,i,i,i] => o"
    2.22 -   "is_DPow_body(M,A,env,p,x) ==
    2.23 +  is_DPow_sats :: "[i=>o,i,i,i,i] => o"
    2.24 +   "is_DPow_sats(M,A,env,p,x) ==
    2.25        \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
    2.26               is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
    2.27               fun_apply(M, sp, e, n1) --> number1(M, n1)"
    2.28  
    2.29 -lemma (in M_satisfies) DPow_body_abs:
    2.30 +lemma (in M_satisfies) DPow_sats_abs:
    2.31      "[| M(A); env \<in> list(A); p \<in> formula; M(x) |]
    2.32 -    ==> is_DPow_body(M,A,env,p,x) <-> sats(A, p, Cons(x,env))"
    2.33 +    ==> is_DPow_sats(M,A,env,p,x) <-> sats(A, p, Cons(x,env))"
    2.34  apply (subgoal_tac "M(env)") 
    2.35 - apply (simp add: is_DPow_body_def satisfies_closed satisfies_abs) 
    2.36 + apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs) 
    2.37  apply (blast dest: transM) 
    2.38  done
    2.39  
    2.40 -lemma (in M_satisfies) Collect_DPow_body_abs:
    2.41 +lemma (in M_satisfies) Collect_DPow_sats_abs:
    2.42      "[| M(A); env \<in> list(A); p \<in> formula |]
    2.43 -    ==> Collect(A, is_DPow_body(M,A,env,p)) = 
    2.44 +    ==> Collect(A, is_DPow_sats(M,A,env,p)) = 
    2.45          {x \<in> A. sats(A, p, Cons(x,env))}"
    2.46 -by (simp add: DPow_body_abs transM [of _ A])
    2.47 +by (simp add: DPow_sats_abs transM [of _ A])
    2.48  
    2.49  
    2.50 -subsubsection{*The Operator @{term is_DPow_body}, Internalized*}
    2.51 +subsubsection{*The Operator @{term is_DPow_sats}, Internalized*}
    2.52  
    2.53 -(* is_DPow_body(M,A,env,p,x) ==
    2.54 +(* is_DPow_sats(M,A,env,p,x) ==
    2.55        \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
    2.56               is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
    2.57               fun_apply(M, sp, e, n1) --> number1(M, n1) *)
    2.58  
    2.59 -constdefs DPow_body_fm :: "[i,i,i,i]=>i"
    2.60 - "DPow_body_fm(A,env,p,x) ==
    2.61 +constdefs DPow_sats_fm :: "[i,i,i,i]=>i"
    2.62 + "DPow_sats_fm(A,env,p,x) ==
    2.63     Forall(Forall(Forall(
    2.64       Implies(satisfies_fm(A#+3,p#+3,0), 
    2.65         Implies(Cons_fm(x#+3,env#+3,1), 
    2.66           Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))"
    2.67  
    2.68 -lemma is_DPow_body_type [TC]:
    2.69 +lemma is_DPow_sats_type [TC]:
    2.70       "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
    2.71 -      ==> DPow_body_fm(A,x,y,z) \<in> formula"
    2.72 -by (simp add: DPow_body_fm_def)
    2.73 +      ==> DPow_sats_fm(A,x,y,z) \<in> formula"
    2.74 +by (simp add: DPow_sats_fm_def)
    2.75  
    2.76 -lemma sats_DPow_body_fm [simp]:
    2.77 +lemma sats_DPow_sats_fm [simp]:
    2.78     "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.79 -    ==> sats(A, DPow_body_fm(u,x,y,z), env) <->
    2.80 -        is_DPow_body(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
    2.81 -by (simp add: DPow_body_fm_def is_DPow_body_def)
    2.82 +    ==> sats(A, DPow_sats_fm(u,x,y,z), env) <->
    2.83 +        is_DPow_sats(**A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
    2.84 +by (simp add: DPow_sats_fm_def is_DPow_sats_def)
    2.85  
    2.86 -lemma DPow_body_iff_sats:
    2.87 +lemma DPow_sats_iff_sats:
    2.88    "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
    2.89        u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    2.90 -   ==> is_DPow_body(**A,nu,nx,ny,nz) <->
    2.91 -       sats(A, DPow_body_fm(u,x,y,z), env)"
    2.92 +   ==> is_DPow_sats(**A,nu,nx,ny,nz) <->
    2.93 +       sats(A, DPow_sats_fm(u,x,y,z), env)"
    2.94  by simp
    2.95  
    2.96 -theorem DPow_body_reflection:
    2.97 -     "REFLECTS[\<lambda>x. is_DPow_body(L,f(x),g(x),h(x),g'(x)),
    2.98 -               \<lambda>i x. is_DPow_body(**Lset(i),f(x),g(x),h(x),g'(x))]"
    2.99 -apply (unfold is_DPow_body_def) 
   2.100 +theorem DPow_sats_reflection:
   2.101 +     "REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
   2.102 +               \<lambda>i x. is_DPow_sats(**Lset(i),f(x),g(x),h(x),g'(x))]"
   2.103 +apply (unfold is_DPow_sats_def) 
   2.104  apply (intro FOL_reflections function_reflections extra_reflections
   2.105               satisfies_reflection)
   2.106  done
   2.107 @@ -186,25 +187,25 @@
   2.108  locale M_DPow = M_satisfies +
   2.109   assumes sep:
   2.110     "[| M(A); env \<in> list(A); p \<in> formula |]
   2.111 -    ==> separation(M, \<lambda>x. is_DPow_body(M,A,env,p,x))"
   2.112 +    ==> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))"
   2.113   and rep: 
   2.114      "M(A)
   2.115      ==> strong_replacement (M, 
   2.116           \<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   2.117                    pair(M,env,p,ep) & 
   2.118 -                  is_Collect(M, A, \<lambda>x. is_DPow_body(M,A,env,p,x), z))"
   2.119 +                  is_Collect(M, A, \<lambda>x. is_DPow_sats(M,A,env,p,x), z))"
   2.120  
   2.121  lemma (in M_DPow) sep':
   2.122     "[| M(A); env \<in> list(A); p \<in> formula |]
   2.123      ==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
   2.124 -by (insert sep [of A env p], simp add: DPow_body_abs)
   2.125 +by (insert sep [of A env p], simp add: DPow_sats_abs)
   2.126  
   2.127  lemma (in M_DPow) rep':
   2.128     "M(A)
   2.129      ==> strong_replacement (M, 
   2.130           \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
   2.131                    ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})" 
   2.132 -by (insert rep [of A], simp add: Collect_DPow_body_abs) 
   2.133 +by (insert rep [of A], simp add: Collect_DPow_sats_abs) 
   2.134  
   2.135  
   2.136  lemma univalent_pair_eq:
   2.137 @@ -223,14 +224,14 @@
   2.138         \<forall>X[M]. X \<in> Z <-> 
   2.139           subset(M,X,A) & 
   2.140             (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   2.141 -                    is_Collect(M, A, is_DPow_body(M,A,env,p), X))"
   2.142 +                    is_Collect(M, A, is_DPow_sats(M,A,env,p), X))"
   2.143  
   2.144  lemma (in M_DPow) DPow'_abs:
   2.145      "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) <-> Z = DPow'(A)"
   2.146  apply (rule iffI)
   2.147 - prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs) 
   2.148 + prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs) 
   2.149  apply (rule M_equalityI) 
   2.150 -apply (simp add: is_DPow'_def DPow'_def Collect_DPow_body_abs, assumption)
   2.151 +apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs, assumption)
   2.152  apply (erule DPow'_closed)
   2.153  done
   2.154  
   2.155 @@ -241,11 +242,11 @@
   2.156  
   2.157  lemma DPow_separation:
   2.158      "[| L(A); env \<in> list(A); p \<in> formula |]
   2.159 -     ==> separation(L, \<lambda>x. is_DPow_body(L,A,env,p,x))"
   2.160 -apply (rule gen_separation_multi [OF DPow_body_reflection, of "{A,env,p}"], 
   2.161 +     ==> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))"
   2.162 +apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"], 
   2.163         auto intro: transL)
   2.164  apply (rule_tac env="[A,env,p]" in DPow_LsetI)
   2.165 -apply (rule DPow_body_iff_sats sep_rules | simp)+
   2.166 +apply (rule DPow_sats_iff_sats sep_rules | simp)+
   2.167  done
   2.168  
   2.169  
   2.170 @@ -256,15 +257,15 @@
   2.171   "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
   2.172               (\<exists>env[L]. \<exists>p[L].
   2.173                 mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) &
   2.174 -               is_Collect (L, A, is_DPow_body(L,A,env,p), x)),
   2.175 +               is_Collect (L, A, is_DPow_sats(L,A,env,p), x)),
   2.176      \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
   2.177               (\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
   2.178                 mem_formula(**Lset(i),p) & mem_list(**Lset(i),A,env) & 
   2.179                 pair(**Lset(i),env,p,u) &
   2.180 -               is_Collect (**Lset(i), A, is_DPow_body(**Lset(i),A,env,p), x))]"
   2.181 +               is_Collect (**Lset(i), A, is_DPow_sats(**Lset(i),A,env,p), x))]"
   2.182  apply (unfold is_Collect_def) 
   2.183  apply (intro FOL_reflections function_reflections mem_formula_reflection
   2.184 -          mem_list_reflection DPow_body_reflection)
   2.185 +          mem_list_reflection DPow_sats_reflection)
   2.186  done
   2.187  
   2.188  lemma DPow_replacement:
   2.189 @@ -272,7 +273,7 @@
   2.190      ==> strong_replacement (L, 
   2.191           \<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
   2.192                    pair(L,env,p,ep) & 
   2.193 -                  is_Collect(L, A, \<lambda>x. is_DPow_body(L,A,env,p,x), z))"
   2.194 +                  is_Collect(L, A, \<lambda>x. is_DPow_sats(L,A,env,p,x), z))"
   2.195  apply (rule strong_replacementI)
   2.196  apply (rule_tac u="{A,B}" 
   2.197           in gen_separation_multi [OF DPow_replacement_Reflects], 
   2.198 @@ -280,7 +281,7 @@
   2.199  apply (unfold is_Collect_def) 
   2.200  apply (rule_tac env="[A,B]" in DPow_LsetI)
   2.201  apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
   2.202 -            DPow_body_iff_sats | simp)+
   2.203 +            DPow_sats_iff_sats | simp)+
   2.204  done
   2.205  
   2.206  
   2.207 @@ -410,7 +411,7 @@
   2.208         \<forall>X[M]. X \<in> Z <-> 
   2.209           subset(M,X,A) & 
   2.210             (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   2.211 -                    is_Collect(M, A, is_DPow_body(M,A,env,p), X))" *)
   2.212 +                    is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
   2.213  
   2.214  constdefs DPow'_fm :: "[i,i]=>i"
   2.215      "DPow'_fm(A,Z) == 
   2.216 @@ -421,7 +422,7 @@
   2.217            And(mem_formula_fm(0),
   2.218             And(mem_list_fm(A#+3,1),
   2.219              Collect_fm(A#+3, 
   2.220 -                       DPow_body_fm(A#+4, 2, 1, 0), 2))))))))"
   2.221 +                       DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))"
   2.222  
   2.223  lemma is_DPow'_type [TC]:
   2.224       "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
   2.225 @@ -444,7 +445,7 @@
   2.226                 \<lambda>i x. is_DPow'(**Lset(i),f(x),g(x))]"
   2.227  apply (simp only: is_DPow'_def)
   2.228  apply (intro FOL_reflections function_reflections mem_formula_reflection
   2.229 -             mem_list_reflection Collect_reflection DPow_body_reflection)
   2.230 +             mem_list_reflection Collect_reflection DPow_sats_reflection)
   2.231  done
   2.232  
   2.233  
   2.234 @@ -501,9 +502,12 @@
   2.235  
   2.236  
   2.237  text{*Relativization of the Operator @{term Lset}*}
   2.238 +
   2.239  constdefs
   2.240 -
   2.241    is_Lset :: "[i=>o, i, i] => o"
   2.242 +   --{*We can use the term language below because @{term is_Lset} will
   2.243 +       not have to be internalized: it isn't used in any instance of
   2.244 +       separation.*}
   2.245     "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
   2.246  
   2.247  lemma (in M_Lset) Lset_abs: