src/ZF/Constructible/DPow_absolute.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 21404 eb85850d3eb7
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/DPow_absolute.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header {*Absoluteness for the Definable Powerset Function*}
     7 
     8 
     9 theory DPow_absolute imports Satisfies_absolute begin
    10 
    11 
    12 subsection{*Preliminary Internalizations*}
    13 
    14 subsubsection{*The Operator @{term is_formula_rec}*}
    15 
    16 text{*The three arguments of @{term p} are always 2, 1, 0.  It is buried
    17    within 11 quantifiers!!*}
    18 
    19 (* is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
    20    "is_formula_rec(M,MH,p,z)  ==
    21       \<exists>dp[M]. \<exists>i[M]. \<exists>f[M]. finite_ordinal(M,dp) & is_depth(M,p,dp) & 
    22        2       1      0
    23              successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
    24 *)
    25 
    26 definition
    27   formula_rec_fm :: "[i, i, i]=>i" where
    28  "formula_rec_fm(mh,p,z) == 
    29     Exists(Exists(Exists(
    30       And(finite_ordinal_fm(2),
    31        And(depth_fm(p#+3,2),
    32         And(succ_fm(2,1), 
    33           And(fun_apply_fm(0,p#+3,z#+3), is_transrec_fm(mh,1,0))))))))"
    34 
    35 lemma is_formula_rec_type [TC]:
    36      "[| p \<in> formula; x \<in> nat; z \<in> nat |] 
    37       ==> formula_rec_fm(p,x,z) \<in> formula"
    38 by (simp add: formula_rec_fm_def) 
    39 
    40 lemma sats_formula_rec_fm:
    41   assumes MH_iff_sats: 
    42       "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 
    43         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
    44         ==> MH(a2, a1, a0) <-> 
    45             sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
    46                           Cons(a4,Cons(a5,Cons(a6,Cons(a7,
    47                                   Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
    48   shows 
    49       "[|x \<in> nat; z \<in> nat; env \<in> list(A)|]
    50        ==> sats(A, formula_rec_fm(p,x,z), env) <-> 
    51            is_formula_rec(##A, MH, nth(x,env), nth(z,env))"
    52 by (simp add: formula_rec_fm_def sats_is_transrec_fm is_formula_rec_def 
    53               MH_iff_sats [THEN iff_sym])
    54 
    55 lemma formula_rec_iff_sats:
    56   assumes MH_iff_sats: 
    57       "!!a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10. 
    58         [|a0\<in>A; a1\<in>A; a2\<in>A; a3\<in>A; a4\<in>A; a5\<in>A; a6\<in>A; a7\<in>A; a8\<in>A; a9\<in>A; a10\<in>A|]
    59         ==> MH(a2, a1, a0) <-> 
    60             sats(A, p, Cons(a0,Cons(a1,Cons(a2,Cons(a3,
    61                           Cons(a4,Cons(a5,Cons(a6,Cons(a7,
    62                                   Cons(a8,Cons(a9,Cons(a10,env))))))))))))"
    63   shows
    64   "[|nth(i,env) = x; nth(k,env) = z; 
    65       i \<in> nat; k \<in> nat; env \<in> list(A)|]
    66    ==> is_formula_rec(##A, MH, x, z) <-> sats(A, formula_rec_fm(p,i,k), env)" 
    67 by (simp add: sats_formula_rec_fm [OF MH_iff_sats])
    68 
    69 theorem formula_rec_reflection:
    70   assumes MH_reflection:
    71     "!!f' f g h. REFLECTS[\<lambda>x. MH(L, f'(x), f(x), g(x), h(x)), 
    72                      \<lambda>i x. MH(##Lset(i), f'(x), f(x), g(x), h(x))]"
    73   shows "REFLECTS[\<lambda>x. is_formula_rec(L, MH(L,x), f(x), h(x)), 
    74                \<lambda>i x. is_formula_rec(##Lset(i), MH(##Lset(i),x), f(x), h(x))]"
    75 apply (simp (no_asm_use) only: is_formula_rec_def)
    76 apply (intro FOL_reflections function_reflections fun_plus_reflections
    77              depth_reflection is_transrec_reflection MH_reflection)
    78 done
    79 
    80 
    81 subsubsection{*The Operator @{term is_satisfies}*}
    82 
    83 (* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
    84 definition
    85   satisfies_fm :: "[i,i,i]=>i" where
    86     "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
    87 
    88 lemma is_satisfies_type [TC]:
    89      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> satisfies_fm(x,y,z) \<in> formula"
    90 by (simp add: satisfies_fm_def)
    91 
    92 lemma sats_satisfies_fm [simp]:
    93    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
    94     ==> sats(A, satisfies_fm(x,y,z), env) <->
    95         is_satisfies(##A, nth(x,env), nth(y,env), nth(z,env))"
    96 by (simp add: satisfies_fm_def is_satisfies_def sats_satisfies_MH_fm
    97               sats_formula_rec_fm)
    98 
    99 lemma satisfies_iff_sats:
   100       "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   101           i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   102        ==> is_satisfies(##A, x, y, z) <-> sats(A, satisfies_fm(i,j,k), env)"
   103 by (simp add: sats_satisfies_fm)
   104 
   105 theorem satisfies_reflection:
   106      "REFLECTS[\<lambda>x. is_satisfies(L,f(x),g(x),h(x)),
   107                \<lambda>i x. is_satisfies(##Lset(i),f(x),g(x),h(x))]"
   108 apply (simp only: is_satisfies_def)
   109 apply (intro formula_rec_reflection satisfies_MH_reflection)
   110 done
   111 
   112 
   113 subsection {*Relativization of the Operator @{term DPow'}*}
   114 
   115 lemma DPow'_eq: 
   116   "DPow'(A) = {z . ep \<in> list(A) * formula, 
   117                     \<exists>env \<in> list(A). \<exists>p \<in> formula. 
   118                        ep = <env,p> & z = {x\<in>A. sats(A, p, Cons(x,env))}}"
   119 by (simp add: DPow'_def, blast) 
   120 
   121 
   122 text{*Relativize the use of @{term sats} within @{term DPow'}
   123 (the comprehension).*}
   124 definition
   125   is_DPow_sats :: "[i=>o,i,i,i,i] => o" where
   126    "is_DPow_sats(M,A,env,p,x) ==
   127       \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
   128              is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
   129              fun_apply(M, sp, e, n1) --> number1(M, n1)"
   130 
   131 lemma (in M_satisfies) DPow_sats_abs:
   132     "[| M(A); env \<in> list(A); p \<in> formula; M(x) |]
   133     ==> is_DPow_sats(M,A,env,p,x) <-> sats(A, p, Cons(x,env))"
   134 apply (subgoal_tac "M(env)") 
   135  apply (simp add: is_DPow_sats_def satisfies_closed satisfies_abs) 
   136 apply (blast dest: transM) 
   137 done
   138 
   139 lemma (in M_satisfies) Collect_DPow_sats_abs:
   140     "[| M(A); env \<in> list(A); p \<in> formula |]
   141     ==> Collect(A, is_DPow_sats(M,A,env,p)) = 
   142         {x \<in> A. sats(A, p, Cons(x,env))}"
   143 by (simp add: DPow_sats_abs transM [of _ A])
   144 
   145 
   146 subsubsection{*The Operator @{term is_DPow_sats}, Internalized*}
   147 
   148 (* is_DPow_sats(M,A,env,p,x) ==
   149       \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
   150              is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
   151              fun_apply(M, sp, e, n1) --> number1(M, n1) *)
   152 
   153 definition
   154   DPow_sats_fm :: "[i,i,i,i]=>i" where
   155   "DPow_sats_fm(A,env,p,x) ==
   156    Forall(Forall(Forall(
   157      Implies(satisfies_fm(A#+3,p#+3,0), 
   158        Implies(Cons_fm(x#+3,env#+3,1), 
   159          Implies(fun_apply_fm(0,1,2), number1_fm(2)))))))"
   160 
   161 lemma is_DPow_sats_type [TC]:
   162      "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   163       ==> DPow_sats_fm(A,x,y,z) \<in> formula"
   164 by (simp add: DPow_sats_fm_def)
   165 
   166 lemma sats_DPow_sats_fm [simp]:
   167    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   168     ==> sats(A, DPow_sats_fm(u,x,y,z), env) <->
   169         is_DPow_sats(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
   170 by (simp add: DPow_sats_fm_def is_DPow_sats_def)
   171 
   172 lemma DPow_sats_iff_sats:
   173   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
   174       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   175    ==> is_DPow_sats(##A,nu,nx,ny,nz) <->
   176        sats(A, DPow_sats_fm(u,x,y,z), env)"
   177 by simp
   178 
   179 theorem DPow_sats_reflection:
   180      "REFLECTS[\<lambda>x. is_DPow_sats(L,f(x),g(x),h(x),g'(x)),
   181                \<lambda>i x. is_DPow_sats(##Lset(i),f(x),g(x),h(x),g'(x))]"
   182 apply (unfold is_DPow_sats_def) 
   183 apply (intro FOL_reflections function_reflections extra_reflections
   184              satisfies_reflection)
   185 done
   186 
   187 
   188 subsection{*A Locale for Relativizing the Operator @{term DPow'}*}
   189 
   190 locale M_DPow = M_satisfies +
   191  assumes sep:
   192    "[| M(A); env \<in> list(A); p \<in> formula |]
   193     ==> separation(M, \<lambda>x. is_DPow_sats(M,A,env,p,x))"
   194  and rep: 
   195     "M(A)
   196     ==> strong_replacement (M, 
   197          \<lambda>ep z. \<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   198                   pair(M,env,p,ep) & 
   199                   is_Collect(M, A, \<lambda>x. is_DPow_sats(M,A,env,p,x), z))"
   200 
   201 lemma (in M_DPow) sep':
   202    "[| M(A); env \<in> list(A); p \<in> formula |]
   203     ==> separation(M, \<lambda>x. sats(A, p, Cons(x,env)))"
   204 by (insert sep [of A env p], simp add: DPow_sats_abs)
   205 
   206 lemma (in M_DPow) rep':
   207    "M(A)
   208     ==> strong_replacement (M, 
   209          \<lambda>ep z. \<exists>env\<in>list(A). \<exists>p\<in>formula.
   210                   ep = <env,p> & z = {x \<in> A . sats(A, p, Cons(x, env))})" 
   211 by (insert rep [of A], simp add: Collect_DPow_sats_abs) 
   212 
   213 
   214 lemma univalent_pair_eq:
   215      "univalent (M, A, \<lambda>xy z. \<exists>x\<in>B. \<exists>y\<in>C. xy = \<langle>x,y\<rangle> \<and> z = f(x,y))"
   216 by (simp add: univalent_def, blast) 
   217 
   218 lemma (in M_DPow) DPow'_closed: "M(A) ==> M(DPow'(A))"
   219 apply (simp add: DPow'_eq)
   220 apply (fast intro: rep' sep' univalent_pair_eq)  
   221 done
   222 
   223 text{*Relativization of the Operator @{term DPow'}*}
   224 definition 
   225   is_DPow' :: "[i=>o,i,i] => o" where
   226     "is_DPow'(M,A,Z) == 
   227        \<forall>X[M]. X \<in> Z <-> 
   228          subset(M,X,A) & 
   229            (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   230                     is_Collect(M, A, is_DPow_sats(M,A,env,p), X))"
   231 
   232 lemma (in M_DPow) DPow'_abs:
   233     "[|M(A); M(Z)|] ==> is_DPow'(M,A,Z) <-> Z = DPow'(A)"
   234 apply (rule iffI)
   235  prefer 2 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs) 
   236 apply (rule M_equalityI) 
   237 apply (simp add: is_DPow'_def DPow'_def Collect_DPow_sats_abs, assumption)
   238 apply (erule DPow'_closed)
   239 done
   240 
   241 
   242 subsection{*Instantiating the Locale @{text M_DPow}*}
   243 
   244 subsubsection{*The Instance of Separation*}
   245 
   246 lemma DPow_separation:
   247     "[| L(A); env \<in> list(A); p \<in> formula |]
   248      ==> separation(L, \<lambda>x. is_DPow_sats(L,A,env,p,x))"
   249 apply (rule gen_separation_multi [OF DPow_sats_reflection, of "{A,env,p}"], 
   250        auto intro: transL)
   251 apply (rule_tac env="[A,env,p]" in DPow_LsetI)
   252 apply (rule DPow_sats_iff_sats sep_rules | simp)+
   253 done
   254 
   255 
   256 
   257 subsubsection{*The Instance of Replacement*}
   258 
   259 lemma DPow_replacement_Reflects:
   260  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
   261              (\<exists>env[L]. \<exists>p[L].
   262                mem_formula(L,p) & mem_list(L,A,env) & pair(L,env,p,u) &
   263                is_Collect (L, A, is_DPow_sats(L,A,env,p), x)),
   264     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B &
   265              (\<exists>env \<in> Lset(i). \<exists>p \<in> Lset(i).
   266                mem_formula(##Lset(i),p) & mem_list(##Lset(i),A,env) & 
   267                pair(##Lset(i),env,p,u) &
   268                is_Collect (##Lset(i), A, is_DPow_sats(##Lset(i),A,env,p), x))]"
   269 apply (unfold is_Collect_def) 
   270 apply (intro FOL_reflections function_reflections mem_formula_reflection
   271           mem_list_reflection DPow_sats_reflection)
   272 done
   273 
   274 lemma DPow_replacement:
   275     "L(A)
   276     ==> strong_replacement (L, 
   277          \<lambda>ep z. \<exists>env[L]. \<exists>p[L]. mem_formula(L,p) & mem_list(L,A,env) &
   278                   pair(L,env,p,ep) & 
   279                   is_Collect(L, A, \<lambda>x. is_DPow_sats(L,A,env,p,x), z))"
   280 apply (rule strong_replacementI)
   281 apply (rule_tac u="{A,B}" 
   282          in gen_separation_multi [OF DPow_replacement_Reflects], 
   283        auto)
   284 apply (unfold is_Collect_def) 
   285 apply (rule_tac env="[A,B]" in DPow_LsetI)
   286 apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats 
   287             DPow_sats_iff_sats | simp)+
   288 done
   289 
   290 
   291 subsubsection{*Actually Instantiating the Locale*}
   292 
   293 lemma M_DPow_axioms_L: "M_DPow_axioms(L)"
   294   apply (rule M_DPow_axioms.intro)
   295    apply (assumption | rule DPow_separation DPow_replacement)+
   296   done
   297 
   298 theorem M_DPow_L: "PROP M_DPow(L)"
   299   apply (rule M_DPow.intro)
   300    apply (rule M_satisfies_L)
   301   apply (rule M_DPow_axioms_L)
   302   done
   303 
   304 lemmas DPow'_closed [intro, simp] = M_DPow.DPow'_closed [OF M_DPow_L]
   305   and DPow'_abs [intro, simp] = M_DPow.DPow'_abs [OF M_DPow_L]
   306 
   307 
   308 subsubsection{*The Operator @{term is_Collect}*}
   309 
   310 text{*The formula @{term is_P} has one free variable, 0, and it is
   311 enclosed within a single quantifier.*}
   312 
   313 (* is_Collect :: "[i=>o,i,i=>o,i] => o"
   314     "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
   315 
   316 definition
   317   Collect_fm :: "[i, i, i]=>i" where
   318  "Collect_fm(A,is_P,z) == 
   319         Forall(Iff(Member(0,succ(z)),
   320                    And(Member(0,succ(A)), is_P)))"
   321 
   322 lemma is_Collect_type [TC]:
   323      "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
   324       ==> Collect_fm(x,is_P,y) \<in> formula"
   325 by (simp add: Collect_fm_def)
   326 
   327 lemma sats_Collect_fm:
   328   assumes is_P_iff_sats: 
   329       "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
   330   shows 
   331       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
   332        ==> sats(A, Collect_fm(x,p,y), env) <->
   333            is_Collect(##A, nth(x,env), is_P, nth(y,env))"
   334 by (simp add: Collect_fm_def is_Collect_def is_P_iff_sats [THEN iff_sym])
   335 
   336 lemma Collect_iff_sats:
   337   assumes is_P_iff_sats: 
   338       "!!a. a \<in> A ==> is_P(a) <-> sats(A, p, Cons(a, env))"
   339   shows 
   340   "[| nth(i,env) = x; nth(j,env) = y;
   341       i \<in> nat; j \<in> nat; env \<in> list(A)|]
   342    ==> is_Collect(##A, x, is_P, y) <-> sats(A, Collect_fm(i,p,j), env)"
   343 by (simp add: sats_Collect_fm [OF is_P_iff_sats])
   344 
   345 
   346 text{*The second argument of @{term is_P} gives it direct access to @{term x},
   347   which is essential for handling free variable references.*}
   348 theorem Collect_reflection:
   349   assumes is_P_reflection:
   350     "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x)),
   351                      \<lambda>i x. is_P(##Lset(i), f(x), g(x))]"
   352   shows "REFLECTS[\<lambda>x. is_Collect(L, f(x), is_P(L,x), g(x)),
   353                \<lambda>i x. is_Collect(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
   354 apply (simp (no_asm_use) only: is_Collect_def)
   355 apply (intro FOL_reflections is_P_reflection)
   356 done
   357 
   358 
   359 subsubsection{*The Operator @{term is_Replace}*}
   360 
   361 text{*BEWARE!  The formula @{term is_P} has free variables 0, 1
   362  and not the usual 1, 0!  It is enclosed within two quantifiers.*}
   363 
   364 (*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
   365     "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
   366 
   367 definition
   368   Replace_fm :: "[i, i, i]=>i" where
   369   "Replace_fm(A,is_P,z) == 
   370         Forall(Iff(Member(0,succ(z)),
   371                    Exists(And(Member(0,A#+2), is_P))))"
   372 
   373 lemma is_Replace_type [TC]:
   374      "[| is_P \<in> formula; x \<in> nat; y \<in> nat |] 
   375       ==> Replace_fm(x,is_P,y) \<in> formula"
   376 by (simp add: Replace_fm_def)
   377 
   378 lemma sats_Replace_fm:
   379   assumes is_P_iff_sats: 
   380       "!!a b. [|a \<in> A; b \<in> A|] 
   381               ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
   382   shows 
   383       "[|x \<in> nat; y \<in> nat; env \<in> list(A)|]
   384        ==> sats(A, Replace_fm(x,p,y), env) <->
   385            is_Replace(##A, nth(x,env), is_P, nth(y,env))"
   386 by (simp add: Replace_fm_def is_Replace_def is_P_iff_sats [THEN iff_sym])
   387 
   388 lemma Replace_iff_sats:
   389   assumes is_P_iff_sats: 
   390       "!!a b. [|a \<in> A; b \<in> A|] 
   391               ==> is_P(a,b) <-> sats(A, p, Cons(a,Cons(b,env)))"
   392   shows 
   393   "[| nth(i,env) = x; nth(j,env) = y;
   394       i \<in> nat; j \<in> nat; env \<in> list(A)|]
   395    ==> is_Replace(##A, x, is_P, y) <-> sats(A, Replace_fm(i,p,j), env)"
   396 by (simp add: sats_Replace_fm [OF is_P_iff_sats])
   397 
   398 
   399 text{*The second argument of @{term is_P} gives it direct access to @{term x},
   400   which is essential for handling free variable references.*}
   401 theorem Replace_reflection:
   402   assumes is_P_reflection:
   403     "!!h f g. REFLECTS[\<lambda>x. is_P(L, f(x), g(x), h(x)),
   404                      \<lambda>i x. is_P(##Lset(i), f(x), g(x), h(x))]"
   405   shows "REFLECTS[\<lambda>x. is_Replace(L, f(x), is_P(L,x), g(x)),
   406                \<lambda>i x. is_Replace(##Lset(i), f(x), is_P(##Lset(i), x), g(x))]"
   407 apply (simp (no_asm_use) only: is_Replace_def)
   408 apply (intro FOL_reflections is_P_reflection)
   409 done
   410 
   411 
   412 
   413 subsubsection{*The Operator @{term is_DPow'}, Internalized*}
   414 
   415 (*  "is_DPow'(M,A,Z) == 
   416        \<forall>X[M]. X \<in> Z <-> 
   417          subset(M,X,A) & 
   418            (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
   419                     is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
   420 
   421 definition
   422   DPow'_fm :: "[i,i]=>i" where
   423     "DPow'_fm(A,Z) == 
   424       Forall(
   425        Iff(Member(0,succ(Z)),
   426         And(subset_fm(0,succ(A)),
   427          Exists(Exists(
   428           And(mem_formula_fm(0),
   429            And(mem_list_fm(A#+3,1),
   430             Collect_fm(A#+3, 
   431                        DPow_sats_fm(A#+4, 2, 1, 0), 2))))))))"
   432 
   433 lemma is_DPow'_type [TC]:
   434      "[| x \<in> nat; y \<in> nat |] ==> DPow'_fm(x,y) \<in> formula"
   435 by (simp add: DPow'_fm_def)
   436 
   437 lemma sats_DPow'_fm [simp]:
   438    "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
   439     ==> sats(A, DPow'_fm(x,y), env) <->
   440         is_DPow'(##A, nth(x,env), nth(y,env))"
   441 by (simp add: DPow'_fm_def is_DPow'_def sats_subset_fm' sats_Collect_fm)
   442 
   443 lemma DPow'_iff_sats:
   444       "[| nth(i,env) = x; nth(j,env) = y; 
   445           i \<in> nat; j \<in> nat; env \<in> list(A)|]
   446        ==> is_DPow'(##A, x, y) <-> sats(A, DPow'_fm(i,j), env)"
   447 by (simp add: sats_DPow'_fm)
   448 
   449 theorem DPow'_reflection:
   450      "REFLECTS[\<lambda>x. is_DPow'(L,f(x),g(x)),
   451                \<lambda>i x. is_DPow'(##Lset(i),f(x),g(x))]"
   452 apply (simp only: is_DPow'_def)
   453 apply (intro FOL_reflections function_reflections mem_formula_reflection
   454              mem_list_reflection Collect_reflection DPow_sats_reflection)
   455 done
   456 
   457 
   458 subsection{*A Locale for Relativizing the Operator @{term Lset}*}
   459 
   460 definition
   461   transrec_body :: "[i=>o,i,i,i,i] => o" where
   462     "transrec_body(M,g,x) ==
   463       \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
   464 
   465 lemma (in M_DPow) transrec_body_abs:
   466      "[|M(x); M(g); M(z)|]
   467     ==> transrec_body(M,g,x,y,z) <-> y \<in> x & z = DPow'(g`y)"
   468 by (simp add: transrec_body_def DPow'_abs transM [of _ x])
   469 
   470 locale M_Lset = M_DPow +
   471  assumes strong_rep:
   472    "[|M(x); M(g)|] ==> strong_replacement(M, \<lambda>y z. transrec_body(M,g,x,y,z))"
   473  and transrec_rep: 
   474     "M(i) ==> transrec_replacement(M, \<lambda>x f u. 
   475               \<exists>r[M]. is_Replace(M, x, transrec_body(M,f,x), r) & 
   476                      big_union(M, r, u), i)"
   477 
   478 
   479 lemma (in M_Lset) strong_rep':
   480    "[|M(x); M(g)|]
   481     ==> strong_replacement(M, \<lambda>y z. y \<in> x & z = DPow'(g`y))"
   482 by (insert strong_rep [of x g], simp add: transrec_body_abs)
   483 
   484 lemma (in M_Lset) DPow_apply_closed:
   485    "[|M(f); M(x); y\<in>x|] ==> M(DPow'(f`y))"
   486 by (blast intro: DPow'_closed dest: transM) 
   487 
   488 lemma (in M_Lset) RepFun_DPow_apply_closed:
   489    "[|M(f); M(x)|] ==> M({DPow'(f`y). y\<in>x})"
   490 by (blast intro: DPow_apply_closed RepFun_closed2 strong_rep') 
   491 
   492 lemma (in M_Lset) RepFun_DPow_abs:
   493      "[|M(x); M(f); M(r) |]
   494       ==> is_Replace(M, x, \<lambda>y z. transrec_body(M,f,x,y,z), r) <->
   495           r =  {DPow'(f`y). y\<in>x}"
   496 apply (simp add: transrec_body_abs RepFun_def) 
   497 apply (rule iff_trans) 
   498 apply (rule Replace_abs) 
   499 apply (simp_all add: DPow_apply_closed strong_rep') 
   500 done
   501 
   502 lemma (in M_Lset) transrec_rep':
   503    "M(i) ==> transrec_replacement(M, \<lambda>x f u. u = (\<Union>y\<in>x. DPow'(f ` y)), i)"
   504 apply (insert transrec_rep [of i]) 
   505 apply (simp add: RepFun_DPow_apply_closed RepFun_DPow_abs 
   506        transrec_replacement_def) 
   507 done
   508 
   509 
   510 text{*Relativization of the Operator @{term Lset}*}
   511 
   512 definition
   513   is_Lset :: "[i=>o, i, i] => o" where
   514    --{*We can use the term language below because @{term is_Lset} will
   515        not have to be internalized: it isn't used in any instance of
   516        separation.*}
   517    "is_Lset(M,a,z) == is_transrec(M, %x f u. u = (\<Union>y\<in>x. DPow'(f`y)), a, z)"
   518 
   519 lemma (in M_Lset) Lset_abs:
   520   "[|Ord(i);  M(i);  M(z)|] 
   521    ==> is_Lset(M,i,z) <-> z = Lset(i)"
   522 apply (simp add: is_Lset_def Lset_eq_transrec_DPow') 
   523 apply (rule transrec_abs)  
   524 apply (simp_all add: transrec_rep' relation2_def RepFun_DPow_apply_closed)
   525 done
   526 
   527 lemma (in M_Lset) Lset_closed:
   528   "[|Ord(i);  M(i)|] ==> M(Lset(i))"
   529 apply (simp add: Lset_eq_transrec_DPow') 
   530 apply (rule transrec_closed [OF transrec_rep']) 
   531 apply (simp_all add: relation2_def RepFun_DPow_apply_closed)
   532 done
   533 
   534 
   535 subsection{*Instantiating the Locale @{text M_Lset}*}
   536 
   537 subsubsection{*The First Instance of Replacement*}
   538 
   539 lemma strong_rep_Reflects:
   540  "REFLECTS [\<lambda>u. \<exists>v[L]. v \<in> B & (\<exists>gy[L].
   541                           v \<in> x & fun_apply(L,g,v,gy) & is_DPow'(L,gy,u)),
   542    \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B & (\<exists>gy \<in> Lset(i).
   543             v \<in> x & fun_apply(##Lset(i),g,v,gy) & is_DPow'(##Lset(i),gy,u))]"
   544 by (intro FOL_reflections function_reflections DPow'_reflection)
   545 
   546 lemma strong_rep:
   547    "[|L(x); L(g)|] ==> strong_replacement(L, \<lambda>y z. transrec_body(L,g,x,y,z))"
   548 apply (unfold transrec_body_def)  
   549 apply (rule strong_replacementI) 
   550 apply (rule_tac u="{x,g,B}" 
   551          in gen_separation_multi [OF strong_rep_Reflects], auto)
   552 apply (rule_tac env="[x,g,B]" in DPow_LsetI)
   553 apply (rule sep_rules DPow'_iff_sats | simp)+
   554 done
   555 
   556 
   557 subsubsection{*The Second Instance of Replacement*}
   558 
   559 lemma transrec_rep_Reflects:
   560  "REFLECTS [\<lambda>x. \<exists>v[L]. v \<in> B &
   561               (\<exists>y[L]. pair(L,v,y,x) &
   562              is_wfrec (L, \<lambda>x f u. \<exists>r[L].
   563                 is_Replace (L, x, \<lambda>y z. 
   564                      \<exists>gy[L]. y \<in> x & fun_apply(L,f,y,gy) & 
   565                       is_DPow'(L,gy,z), r) & big_union(L,r,u), mr, v, y)),
   566     \<lambda>i x. \<exists>v \<in> Lset(i). v \<in> B &
   567               (\<exists>y \<in> Lset(i). pair(##Lset(i),v,y,x) &
   568              is_wfrec (##Lset(i), \<lambda>x f u. \<exists>r \<in> Lset(i).
   569                 is_Replace (##Lset(i), x, \<lambda>y z. 
   570                      \<exists>gy \<in> Lset(i). y \<in> x & fun_apply(##Lset(i),f,y,gy) & 
   571                       is_DPow'(##Lset(i),gy,z), r) & 
   572                       big_union(##Lset(i),r,u), mr, v, y))]" 
   573 apply (simp only: rex_setclass_is_bex [symmetric])
   574   --{*Convert @{text "\<exists>y\<in>Lset(i)"} to @{text "\<exists>y[##Lset(i)]"} within the body
   575        of the @{term is_wfrec} application. *}
   576 apply (intro FOL_reflections function_reflections 
   577           is_wfrec_reflection Replace_reflection DPow'_reflection) 
   578 done
   579 
   580 
   581 lemma transrec_rep: 
   582     "[|L(j)|]
   583     ==> transrec_replacement(L, \<lambda>x f u. 
   584               \<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) & 
   585                      big_union(L, r, u), j)"
   586 apply (rule transrec_replacementI, assumption)
   587 apply (unfold transrec_body_def)  
   588 apply (rule strong_replacementI)
   589 apply (rule_tac u="{j,B,Memrel(eclose({j}))}" 
   590          in gen_separation_multi [OF transrec_rep_Reflects], auto)
   591 apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI)
   592 apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | 
   593        simp)+
   594 done
   595 
   596 
   597 subsubsection{*Actually Instantiating @{text M_Lset}*}
   598 
   599 lemma M_Lset_axioms_L: "M_Lset_axioms(L)"
   600   apply (rule M_Lset_axioms.intro)
   601        apply (assumption | rule strong_rep transrec_rep)+
   602   done
   603 
   604 theorem M_Lset_L: "PROP M_Lset(L)"
   605   apply (rule M_Lset.intro) 
   606    apply (rule M_DPow_L)
   607   apply (rule M_Lset_axioms_L) 
   608   done
   609 
   610 text{*Finally: the point of the whole theory!*}
   611 lemmas Lset_closed = M_Lset.Lset_closed [OF M_Lset_L]
   612    and Lset_abs = M_Lset.Lset_abs [OF M_Lset_L]
   613 
   614 
   615 subsection{*The Notion of Constructible Set*}
   616 
   617 
   618 definition
   619   constructible :: "[i=>o,i] => o" where
   620     "constructible(M,x) ==
   621        \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
   622 
   623 theorem V_equals_L_in_L:
   624   "L(x) ==> constructible(L,x)"
   625 apply (simp add: constructible_def Lset_abs Lset_closed) 
   626 apply (simp add: L_def)
   627 apply (blast intro: Ord_in_L) 
   628 done
   629 
   630 end