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