src/ZF/Constructible/Formula.thy
author paulson
Thu Jul 04 16:59:54 2002 +0200 (2002-07-04)
changeset 13298 b4f370679c65
parent 13291 a73ab154f75c
child 13306 6eebcddee32b
permissions -rw-r--r--
Constructible: some separation axioms
     1 header {* First-Order Formulas and the Definition of the Class L *}
     2 
     3 theory Formula = Main:
     4 
     5 subsection{*Internalized formulas of FOL*}
     6 
     7 text{*De Bruijn representation.
     8   Unbound variables get their denotations from an environment.*}
     9 
    10 consts   formula :: i
    11 datatype
    12   "formula" = Member ("x: nat", "y: nat")
    13             | Equal  ("x: nat", "y: nat")
    14             | Neg ("p: formula")
    15             | And ("p: formula", "q: formula")
    16             | Forall ("p: formula")
    17 
    18 declare formula.intros [TC]
    19 
    20 constdefs Or :: "[i,i]=>i"
    21     "Or(p,q) == Neg(And(Neg(p),Neg(q)))"
    22 
    23 constdefs Implies :: "[i,i]=>i"
    24     "Implies(p,q) == Neg(And(p,Neg(q)))"
    25 
    26 constdefs Iff :: "[i,i]=>i"
    27     "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
    28 
    29 constdefs Exists :: "i=>i"
    30     "Exists(p) == Neg(Forall(Neg(p)))";
    31 
    32 lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
    33 by (simp add: Or_def) 
    34 
    35 lemma Implies_type [TC]:
    36      "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
    37 by (simp add: Implies_def) 
    38 
    39 lemma Iff_type [TC]:
    40      "[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
    41 by (simp add: Iff_def) 
    42 
    43 lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
    44 by (simp add: Exists_def) 
    45 
    46 
    47 consts   satisfies :: "[i,i]=>i"
    48 primrec (*explicit lambda is required because the environment varies*)
    49   "satisfies(A,Member(x,y)) = 
    50       (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"
    51 
    52   "satisfies(A,Equal(x,y)) = 
    53       (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
    54 
    55   "satisfies(A,Neg(p)) = 
    56       (\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"
    57 
    58   "satisfies(A,And(p,q)) =
    59       (\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"
    60 
    61   "satisfies(A,Forall(p)) = 
    62       (\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
    63 
    64 
    65 lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
    66 by (induct_tac p, simp_all) 
    67 
    68 syntax sats :: "[i,i,i] => o"
    69 translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
    70 
    71 lemma [simp]:
    72   "env \<in> list(A) 
    73    ==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)"
    74 by simp
    75 
    76 lemma [simp]:
    77   "env \<in> list(A) 
    78    ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
    79 by simp
    80 
    81 lemma sats_Neg_iff [simp]:
    82   "env \<in> list(A) 
    83    ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
    84 by (simp add: Bool.not_def cond_def) 
    85 
    86 lemma sats_And_iff [simp]:
    87   "env \<in> list(A) 
    88    ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
    89 by (simp add: Bool.and_def cond_def) 
    90 
    91 lemma sats_Forall_iff [simp]:
    92   "env \<in> list(A) 
    93    ==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
    94 by simp
    95 
    96 declare satisfies.simps [simp del]; 
    97 
    98 subsection{*Dividing line between primitive and derived connectives*}
    99 
   100 lemma sats_Or_iff [simp]:
   101   "env \<in> list(A) 
   102    ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
   103 by (simp add: Or_def)
   104 
   105 lemma sats_Implies_iff [simp]:
   106   "env \<in> list(A) 
   107    ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
   108 by (simp add: Implies_def, blast) 
   109 
   110 lemma sats_Iff_iff [simp]:
   111   "env \<in> list(A) 
   112    ==> (sats(A, Iff(p,q), env)) <-> (sats(A,p,env) <-> sats(A,q,env))"
   113 by (simp add: Iff_def, blast) 
   114 
   115 lemma sats_Exists_iff [simp]:
   116   "env \<in> list(A) 
   117    ==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
   118 by (simp add: Exists_def)
   119 
   120 
   121 subsubsection{*Derived rules to help build up formulas*}
   122 
   123 lemma mem_iff_sats:
   124       "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
   125        ==> (x\<in>y) <-> sats(A, Member(i,j), env)" 
   126 by (simp add: satisfies.simps)
   127 
   128 lemma equal_iff_sats:
   129       "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
   130        ==> (x=y) <-> sats(A, Equal(i,j), env)" 
   131 by (simp add: satisfies.simps)
   132 
   133 lemma conj_iff_sats:
   134       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
   135        ==> (P & Q) <-> sats(A, And(p,q), env)"
   136 by (simp add: sats_And_iff)
   137 
   138 lemma disj_iff_sats:
   139       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
   140        ==> (P | Q) <-> sats(A, Or(p,q), env)"
   141 by (simp add: sats_Or_iff)
   142 
   143 lemma imp_iff_sats:
   144       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
   145        ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
   146 by (simp add: sats_Forall_iff) 
   147 
   148 lemma iff_iff_sats:
   149       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
   150        ==> (P <-> Q) <-> sats(A, Iff(p,q), env)"
   151 by (simp add: sats_Forall_iff) 
   152 
   153 lemma imp_iff_sats:
   154       "[| P <-> sats(A,p,env); Q <-> sats(A,q,env); env \<in> list(A)|]
   155        ==> (P --> Q) <-> sats(A, Implies(p,q), env)"
   156 by (simp add: sats_Forall_iff) 
   157 
   158 lemma ball_iff_sats:
   159       "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
   160        ==> (\<forall>x\<in>A. P(x)) <-> sats(A, Forall(p), env)"
   161 by (simp add: sats_Forall_iff) 
   162 
   163 lemma bex_iff_sats:
   164       "[| !!x. x\<in>A ==> P(x) <-> sats(A, p, Cons(x, env)); env \<in> list(A)|]
   165        ==> (\<exists>x\<in>A. P(x)) <-> sats(A, Exists(p), env)"
   166 by (simp add: sats_Exists_iff) 
   167 
   168 
   169 constdefs incr_var :: "[i,i]=>i"
   170     "incr_var(x,lev) == if x<lev then x else succ(x)"
   171 
   172 lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
   173 by (simp add: incr_var_def)
   174 
   175 lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
   176 apply (simp add: incr_var_def) 
   177 apply (blast dest: lt_trans1) 
   178 done
   179 
   180 consts   incr_bv :: "i=>i"
   181 primrec
   182   "incr_bv(Member(x,y)) = 
   183       (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
   184 
   185   "incr_bv(Equal(x,y)) = 
   186       (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
   187 
   188   "incr_bv(Neg(p)) = 
   189       (\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"
   190 
   191   "incr_bv(And(p,q)) =
   192       (\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"
   193 
   194   "incr_bv(Forall(p)) = 
   195       (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
   196 
   197 
   198 constdefs incr_boundvars :: "i => i"
   199     "incr_boundvars(p) == incr_bv(p)`0"
   200 
   201 
   202 lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
   203 by (simp add: incr_var_def) 
   204 
   205 lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
   206 by (induct_tac p, simp_all) 
   207 
   208 lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
   209 by (simp add: incr_boundvars_def) 
   210 
   211 (*Obviously DPow is closed under complements and finite intersections and
   212 unions.  Needs an inductive lemma to allow two lists of parameters to 
   213 be combined.*)
   214 
   215 lemma sats_incr_bv_iff [rule_format]:
   216   "[| p \<in> formula; env \<in> list(A); x \<in> A |]
   217    ==> \<forall>bvs \<in> list(A). 
   218            sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <-> 
   219            sats(A, p, bvs@env)"
   220 apply (induct_tac p)
   221 apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)
   222 apply (auto simp add: diff_succ not_lt_iff_le)
   223 done
   224 
   225 (*UNUSED*)
   226 lemma sats_incr_boundvars_iff:
   227   "[| p \<in> formula; env \<in> list(A); x \<in> A |]
   228    ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
   229 apply (insert sats_incr_bv_iff [of p env A x Nil])
   230 apply (simp add: incr_boundvars_def) 
   231 done
   232 
   233 (*UNUSED
   234 lemma formula_add_params [rule_format]:
   235   "[| p \<in> formula; n \<in> nat |]
   236    ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
   237          length(bvs) = n --> 
   238          sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
   239 apply (induct_tac n, simp, clarify) 
   240 apply (erule list.cases)
   241 apply (auto simp add: sats_incr_boundvars_iff)  
   242 done
   243 *)
   244 
   245 consts   arity :: "i=>i"
   246 primrec
   247   "arity(Member(x,y)) = succ(x) \<union> succ(y)"
   248 
   249   "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
   250 
   251   "arity(Neg(p)) = arity(p)"
   252 
   253   "arity(And(p,q)) = arity(p) \<union> arity(q)"
   254 
   255   "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
   256 
   257 
   258 lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
   259 by (induct_tac p, simp_all) 
   260 
   261 lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
   262 by (simp add: Or_def) 
   263 
   264 lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
   265 by (simp add: Implies_def) 
   266 
   267 lemma arity_Iff [simp]: "arity(Iff(p,q)) = arity(p) \<union> arity(q)"
   268 by (simp add: Iff_def, blast)
   269 
   270 lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
   271 by (simp add: Exists_def) 
   272 
   273 
   274 lemma arity_sats_iff [rule_format]:
   275   "[| p \<in> formula; extra \<in> list(A) |]
   276    ==> \<forall>env \<in> list(A). 
   277            arity(p) \<le> length(env) --> 
   278            sats(A, p, env @ extra) <-> sats(A, p, env)"
   279 apply (induct_tac p)
   280 apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
   281                 split: split_nat_case, auto) 
   282 done
   283 
   284 lemma arity_sats1_iff:
   285   "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A); 
   286     extra \<in> list(A) |]
   287    ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
   288 apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
   289 apply simp 
   290 done
   291 
   292 (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
   293 lemma incr_var_lemma:
   294      "[| x \<in> nat; y \<in> nat; lev \<le> x |]
   295       ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
   296 apply (simp add: incr_var_def Ord_Un_if, auto)
   297   apply (blast intro: leI)
   298  apply (simp add: not_lt_iff_le)  
   299  apply (blast intro: le_anti_sym) 
   300 apply (blast dest: lt_trans2) 
   301 done
   302 
   303 lemma incr_And_lemma:
   304      "y < x ==> y \<union> succ(x) = succ(x \<union> y)"
   305 apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff) 
   306 apply (blast dest: lt_asym) 
   307 done
   308 
   309 lemma arity_incr_bv_lemma [rule_format]:
   310   "p \<in> formula 
   311    ==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) = 
   312                  (if n < arity(p) then succ(arity(p)) else arity(p))"
   313 apply (induct_tac p) 
   314 apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
   315                      succ_Un_distrib [symmetric] incr_var_lt incr_var_le
   316                      Un_commute incr_var_lemma arity_type nat_imp_quasinat
   317             split: split_nat_case) 
   318  txt{*the Forall case reduces to linear arithmetic*}
   319  prefer 2
   320  apply clarify 
   321  apply (blast dest: lt_trans1) 
   322 txt{*left with the And case*}
   323 apply safe
   324  apply (blast intro: incr_And_lemma lt_trans1) 
   325 apply (subst incr_And_lemma)
   326  apply (blast intro: lt_trans1) 
   327 apply (simp add: Un_commute)
   328 done
   329 
   330 lemma arity_incr_boundvars_eq:
   331   "p \<in> formula
   332    ==> arity(incr_boundvars(p)) =
   333         (if 0 < arity(p) then succ(arity(p)) else arity(p))"
   334 apply (insert arity_incr_bv_lemma [of p 0])
   335 apply (simp add: incr_boundvars_def) 
   336 done
   337 
   338 lemma arity_iterates_incr_boundvars_eq:
   339   "[| p \<in> formula; n \<in> nat |]
   340    ==> arity(incr_boundvars^n(p)) =
   341          (if 0 < arity(p) then n #+ arity(p) else arity(p))"
   342 apply (induct_tac n) 
   343 apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le) 
   344 done
   345 
   346 
   347 subsection{*Renaming all but the first bound variable*}
   348 
   349 constdefs incr_bv1 :: "i => i"
   350     "incr_bv1(p) == incr_bv(p)`1"
   351 
   352 
   353 lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
   354 by (simp add: incr_bv1_def) 
   355 
   356 (*For renaming all but the bound variable at level 0*)
   357 lemma sats_incr_bv1_iff [rule_format]:
   358   "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
   359    ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <-> 
   360        sats(A, p, Cons(x,env))"
   361 apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
   362 apply (simp add: incr_bv1_def) 
   363 done
   364 
   365 lemma formula_add_params1 [rule_format]:
   366   "[| p \<in> formula; n \<in> nat; x \<in> A |]
   367    ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A). 
   368           length(bvs) = n --> 
   369           sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <-> 
   370           sats(A, p, Cons(x,env))"
   371 apply (induct_tac n, simp, clarify) 
   372 apply (erule list.cases)
   373 apply (simp_all add: sats_incr_bv1_iff) 
   374 done
   375 
   376 
   377 lemma arity_incr_bv1_eq:
   378   "p \<in> formula
   379    ==> arity(incr_bv1(p)) =
   380         (if 1 < arity(p) then succ(arity(p)) else arity(p))"
   381 apply (insert arity_incr_bv_lemma [of p 1])
   382 apply (simp add: incr_bv1_def) 
   383 done
   384 
   385 lemma arity_iterates_incr_bv1_eq:
   386   "[| p \<in> formula; n \<in> nat |]
   387    ==> arity(incr_bv1^n(p)) =
   388          (if 1 < arity(p) then n #+ arity(p) else arity(p))"
   389 apply (induct_tac n) 
   390 apply (simp_all add: arity_incr_bv1_eq)
   391 apply (simp add: not_lt_iff_le)
   392 apply (blast intro: le_trans add_le_self2 arity_type) 
   393 done
   394 
   395 
   396 (*Definable powerset operation: Kunen's definition 1.1, page 165.*)
   397 constdefs DPow :: "i => i"
   398   "DPow(A) == {X \<in> Pow(A). 
   399                \<exists>env \<in> list(A). \<exists>p \<in> formula. 
   400                  arity(p) \<le> succ(length(env)) & 
   401                  X = {x\<in>A. sats(A, p, Cons(x,env))}}"
   402 
   403 lemma DPowI:
   404   "[|env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
   405    ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
   406 by (simp add: DPow_def, blast) 
   407 
   408 text{*With this rule we can specify @{term p} later.*}
   409 lemma DPowI2 [rule_format]:
   410   "[|\<forall>x\<in>A. P(x) <-> sats(A, p, Cons(x,env));
   411      env \<in> list(A);  p \<in> formula;  arity(p) \<le> succ(length(env))|]
   412    ==> {x\<in>A. P(x)} \<in> DPow(A)"
   413 by (simp add: DPow_def, blast) 
   414 
   415 lemma DPowD:
   416   "X \<in> DPow(A) 
   417    ==> X <= A &
   418        (\<exists>env \<in> list(A). 
   419         \<exists>p \<in> formula. arity(p) \<le> succ(length(env)) & 
   420                       X = {x\<in>A. sats(A, p, Cons(x,env))})"
   421 by (simp add: DPow_def) 
   422 
   423 lemmas DPow_imp_subset = DPowD [THEN conjunct1]
   424 
   425 (*Lemma 1.2*)
   426 lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |] 
   427        ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
   428 by (blast intro: DPowI)
   429 
   430 lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"
   431 by (simp add: DPow_def, blast)
   432 
   433 lemma empty_in_DPow: "0 \<in> DPow(A)"
   434 apply (simp add: DPow_def)
   435 apply (rule_tac x="Nil" in bexI) 
   436  apply (rule_tac x="Neg(Equal(0,0))" in bexI) 
   437   apply (auto simp add: Un_least_lt_iff) 
   438 done
   439 
   440 lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
   441 apply (simp add: DPow_def, clarify, auto) 
   442 apply (rule bexI) 
   443  apply (rule_tac x="Neg(p)" in bexI) 
   444   apply auto 
   445 done
   446 
   447 lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)"
   448 apply (simp add: DPow_def, auto) 
   449 apply (rename_tac envp p envq q) 
   450 apply (rule_tac x="envp@envq" in bexI) 
   451  apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)
   452   apply typecheck
   453 apply (rule conjI) 
   454 (*finally check the arity!*)
   455  apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
   456  apply (force intro: add_le_self le_trans) 
   457 apply (simp add: arity_sats1_iff formula_add_params1, blast) 
   458 done
   459 
   460 lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)"
   461 apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))") 
   462 apply (simp add: Int_in_DPow Compl_in_DPow) 
   463 apply (simp add: DPow_def, blast) 
   464 done
   465 
   466 lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
   467 apply (simp add: DPow_def)
   468 apply (rule_tac x="Cons(x,Nil)" in bexI) 
   469  apply (rule_tac x="Equal(0,1)" in bexI) 
   470   apply typecheck
   471 apply (force simp add: succ_Un_distrib [symmetric])  
   472 done
   473 
   474 lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
   475 apply (rule cons_eq [THEN subst]) 
   476 apply (blast intro: singleton_in_DPow Un_in_DPow) 
   477 done
   478 
   479 (*Part of Lemma 1.3*)
   480 lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
   481 apply (erule Fin.induct) 
   482  apply (rule empty_in_DPow) 
   483 apply (blast intro: cons_in_DPow) 
   484 done
   485 
   486 (*DPow is not monotonic.  For example, let A be some non-constructible set
   487   of natural numbers, and let B be nat.  Then A<=B and obviously A : DPow(A)
   488   but A ~: DPow(B).*)
   489 lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
   490 apply (simp add: DPow_def, auto) 
   491 (*must use the formula defining A in B to relativize the new formula...*)
   492 oops
   493 
   494 lemma DPow_0: "DPow(0) = {0}" 
   495 by (blast intro: empty_in_DPow dest: DPow_imp_subset)
   496 
   497 lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)" 
   498 by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
   499 
   500 lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
   501 apply (rule equalityI) 
   502 apply (rule DPow_subset_Pow) 
   503 apply (erule Finite_Pow_subset_Pow) 
   504 done
   505 
   506 (*This may be true but the proof looks difficult, requiring relativization 
   507 lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
   508 apply (rule equalityI, safe)
   509 oops
   510 *)
   511 
   512 
   513 subsection{*Internalized formulas for basic concepts*}
   514 
   515 subsubsection{*The subset relation*}
   516 
   517 lemma lt_length_in_nat:
   518    "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
   519 apply (frule lt_nat_in_nat, typecheck) 
   520 done
   521 
   522 constdefs subset_fm :: "[i,i]=>i"
   523     "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
   524 
   525 lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
   526 by (simp add: subset_fm_def) 
   527 
   528 lemma arity_subset_fm [simp]:
   529      "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
   530 by (simp add: subset_fm_def succ_Un_distrib [symmetric]) 
   531 
   532 lemma sats_subset_fm [simp]:
   533    "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
   534     ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
   535 apply (frule lt_length_in_nat, assumption)  
   536 apply (simp add: subset_fm_def Transset_def) 
   537 apply (blast intro: nth_type) 
   538 done
   539 
   540 subsubsection{*Transitive sets*}
   541 
   542 constdefs transset_fm :: "i=>i"
   543    "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
   544 
   545 lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
   546 by (simp add: transset_fm_def) 
   547 
   548 lemma arity_transset_fm [simp]:
   549      "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
   550 by (simp add: transset_fm_def succ_Un_distrib [symmetric]) 
   551 
   552 lemma sats_transset_fm [simp]:
   553    "[|x < length(env); env \<in> list(A); Transset(A)|]
   554     ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
   555 apply (frule lt_nat_in_nat, erule length_type) 
   556 apply (simp add: transset_fm_def Transset_def) 
   557 apply (blast intro: nth_type) 
   558 done
   559 
   560 subsubsection{*Ordinals*}
   561 
   562 constdefs ordinal_fm :: "i=>i"
   563    "ordinal_fm(x) == 
   564       And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
   565 
   566 lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
   567 by (simp add: ordinal_fm_def) 
   568 
   569 lemma arity_ordinal_fm [simp]:
   570      "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
   571 by (simp add: ordinal_fm_def succ_Un_distrib [symmetric]) 
   572 
   573 lemma sats_ordinal_fm [simp]:
   574    "[|x < length(env); env \<in> list(A); Transset(A)|]
   575     ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
   576 apply (frule lt_nat_in_nat, erule length_type) 
   577 apply (simp add: ordinal_fm_def Ord_def Transset_def)
   578 apply (blast intro: nth_type) 
   579 done
   580 
   581 
   582 subsection{* Constant Lset: Levels of the Constructible Universe *}
   583 
   584 constdefs Lset :: "i=>i"
   585     "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
   586 
   587 text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
   588 lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
   589 by (subst Lset_def [THEN def_transrec], simp)
   590 
   591 lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
   592 by (subst Lset, blast)
   593 
   594 lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
   595 apply (insert Lset [of x]) 
   596 apply (blast intro: elim: equalityE) 
   597 done
   598 
   599 subsubsection{* Transitivity *}
   600 
   601 lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)"
   602 apply (simp add: Transset_def DPow_def)
   603 apply (rule_tac x="[X]" in bexI) 
   604  apply (rule_tac x="Member(0,1)" in bexI) 
   605   apply (auto simp add: Un_least_lt_iff) 
   606 done
   607 
   608 lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"
   609 apply clarify  
   610 apply (simp add: Transset_def)
   611 apply (blast intro: elem_subset_in_DPow) 
   612 done
   613 
   614 lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
   615 apply (simp add: Transset_def) 
   616 apply (blast intro: elem_subset_in_DPow dest: DPowD) 
   617 done
   618 
   619 text{*Kunen's VI, 1.6 (a)*}
   620 lemma Transset_Lset: "Transset(Lset(i))"
   621 apply (rule_tac a=i in eps_induct)
   622 apply (subst Lset)
   623 apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
   624 done
   625 
   626 lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"
   627 apply (insert Transset_Lset) 
   628 apply (simp add: Transset_def) 
   629 done
   630 
   631 subsubsection{* Monotonicity *}
   632 
   633 text{*Kunen's VI, 1.6 (b)*}
   634 lemma Lset_mono [rule_format]:
   635      "ALL j. i<=j --> Lset(i) <= Lset(j)"
   636 apply (rule_tac a=i in eps_induct)
   637 apply (rule impI [THEN allI])
   638 apply (subst Lset)
   639 apply (subst Lset, blast) 
   640 done
   641 
   642 text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
   643 lemma Lset_mono_mem [rule_format]:
   644      "ALL j. i:j --> Lset(i) <= Lset(j)"
   645 apply (rule_tac a=i in eps_induct)
   646 apply (rule impI [THEN allI])
   647 apply (subst Lset, auto) 
   648 apply (rule rev_bexI, assumption)
   649 apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD) 
   650 done
   651 
   652 text{*Useful with Reflection to bump up the ordinal*}
   653 lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
   654 by (blast dest: ltD [THEN Lset_mono_mem]) 
   655 
   656 subsubsection{* 0, successor and limit equations fof Lset *}
   657 
   658 lemma Lset_0 [simp]: "Lset(0) = 0"
   659 by (subst Lset, blast)
   660 
   661 lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
   662 by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
   663 
   664 lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"
   665 apply (subst Lset, rule UN_least)
   666 apply (erule succE) 
   667  apply blast 
   668 apply clarify
   669 apply (rule elem_subset_in_DPow)
   670  apply (subst Lset)
   671  apply blast 
   672 apply (blast intro: dest: DPowD Lset_mono_mem) 
   673 done
   674 
   675 lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
   676 by (intro equalityI Lset_succ_subset1 Lset_succ_subset2) 
   677 
   678 lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"
   679 apply (subst Lset)
   680 apply (rule equalityI)
   681  txt{*first inclusion*}
   682  apply (rule UN_least)
   683  apply (erule UnionE)
   684  apply (rule subset_trans)
   685   apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)
   686 txt{*opposite inclusion*}
   687 apply (rule UN_least)
   688 apply (subst Lset, blast)
   689 done
   690 
   691 subsubsection{* Lset applied to Limit ordinals *}
   692 
   693 lemma Limit_Lset_eq:
   694     "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
   695 by (simp add: Lset_Union [symmetric] Limit_Union_eq)
   696 
   697 lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a : Lset(i)"
   698 by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
   699 
   700 lemma Limit_LsetE:
   701     "[| a: Lset(i);  ~R ==> Limit(i);
   702         !!x. [| x<i;  a: Lset(x) |] ==> R
   703      |] ==> R"
   704 apply (rule classical)
   705 apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
   706   prefer 2 apply assumption
   707  apply blast 
   708 apply (blast intro: ltI  Limit_is_Ord)
   709 done
   710 
   711 subsubsection{* Basic closure properties *}
   712 
   713 lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
   714 by (subst Lset, blast intro: empty_in_DPow)
   715 
   716 lemma notin_Lset: "x \<notin> Lset(x)"
   717 apply (rule_tac a=x in eps_induct)
   718 apply (subst Lset)
   719 apply (blast dest: DPowD)  
   720 done
   721 
   722 
   723 subsection{*Constructible Ordinals: Kunen's VI, 1.9 (b)*}
   724 
   725 text{*The subset consisting of the ordinals is definable.*}
   726 lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
   727 apply (simp add: DPow_def Collect_subset) 
   728 apply (rule_tac x="Nil" in bexI) 
   729  apply (rule_tac x="ordinal_fm(0)" in bexI) 
   730 apply (simp_all add: sats_ordinal_fm)
   731 done 
   732 
   733 lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
   734 apply (erule trans_induct3)
   735   apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
   736 txt{*The successor case remains.*} 
   737 apply (rule equalityI)
   738 txt{*First inclusion*}
   739  apply clarify  
   740  apply (erule Ord_linear_lt, assumption) 
   741    apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset]) 
   742   apply blast 
   743  apply (blast dest: ltD)
   744 txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
   745 apply auto
   746 txt{*Key case: *}
   747   apply (erule subst, rule Ords_in_DPow [OF Transset_Lset]) 
   748  apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE) 
   749 apply (blast intro: Ord_in_Ord) 
   750 done
   751 
   752 
   753 lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
   754 by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
   755 
   756 lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
   757 apply (simp add: Lset_succ)
   758 apply (subst Ords_of_Lset_eq [symmetric], assumption, 
   759        rule Ords_in_DPow [OF Transset_Lset]) 
   760 done
   761 
   762 subsubsection{* Unions *}
   763 
   764 lemma Union_in_Lset:
   765      "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
   766 apply (insert Transset_Lset)
   767 apply (rule LsetI [OF succI1])
   768 apply (simp add: Transset_def DPow_def) 
   769 apply (intro conjI, blast)
   770 txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
   771 apply (rule_tac x="Cons(X,Nil)" in bexI) 
   772  apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI) 
   773   apply typecheck
   774 apply (simp add: succ_Un_distrib [symmetric], blast) 
   775 done
   776 
   777 lemma Union_in_LLimit:
   778      "[| X: Lset(i);  Limit(i) |] ==> Union(X) : Lset(i)"
   779 apply (rule Limit_LsetE, assumption+)
   780 apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
   781 done
   782 
   783 subsubsection{* Finite sets and ordered pairs *}
   784 
   785 lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
   786 by (simp add: Lset_succ singleton_in_DPow) 
   787 
   788 lemma doubleton_in_Lset:
   789      "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
   790 by (simp add: Lset_succ empty_in_DPow cons_in_DPow) 
   791 
   792 lemma Pair_in_Lset:
   793     "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
   794 apply (unfold Pair_def)
   795 apply (blast intro: doubleton_in_Lset) 
   796 done
   797 
   798 lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
   799 
   800 lemma singleton_in_LLimit:
   801     "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
   802 apply (erule Limit_LsetE, assumption)
   803 apply (erule singleton_in_Lset [THEN lt_LsetI])
   804 apply (blast intro: Limit_has_succ) 
   805 done
   806 
   807 lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
   808 lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
   809 
   810 text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
   811 lemma doubleton_in_LLimit:
   812     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} : Lset(i)"
   813 apply (erule Limit_LsetE, assumption)
   814 apply (erule Limit_LsetE, assumption)
   815 apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
   816                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   817 done
   818 
   819 lemma Pair_in_LLimit:
   820     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> : Lset(i)"
   821 txt{*Infer that a, b occur at ordinals x,xa < i.*}
   822 apply (erule Limit_LsetE, assumption)
   823 apply (erule Limit_LsetE, assumption)
   824 txt{*Infer that succ(succ(x Un xa)) < i *}
   825 apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
   826                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   827 done
   828 
   829 lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
   830 by (blast intro: Pair_in_LLimit)
   831 
   832 lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
   833 
   834 lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
   835 by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
   836 
   837 lemma nat_into_LLimit: "[| n: nat;  Limit(i) |] ==> n : Lset(i)"
   838 by (blast intro: nat_subset_LLimit [THEN subsetD])
   839 
   840 
   841 subsubsection{* Closure under disjoint union *}
   842 
   843 lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
   844 
   845 lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
   846 by (blast intro: nat_into_LLimit)
   847 
   848 lemma Inl_in_LLimit:
   849     "[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
   850 apply (unfold Inl_def)
   851 apply (blast intro: zero_in_LLimit Pair_in_LLimit)
   852 done
   853 
   854 lemma Inr_in_LLimit:
   855     "[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
   856 apply (unfold Inr_def)
   857 apply (blast intro: one_in_LLimit Pair_in_LLimit)
   858 done
   859 
   860 lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
   861 by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
   862 
   863 lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
   864 
   865 
   866 text{*The constructible universe and its rank function*}
   867 constdefs
   868   L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
   869     "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
   870   
   871   lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
   872     "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
   873 
   874 lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
   875 by (simp add: L_def, blast)
   876 
   877 lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
   878 by (simp add: L_def)
   879 
   880 lemma Ord_lrank [simp]: "Ord(lrank(a))"
   881 by (simp add: lrank_def)
   882 
   883 lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
   884 apply (erule trans_induct3)
   885   apply simp   
   886  apply (simp only: lrank_def) 
   887  apply (blast intro: Least_le) 
   888 apply (simp_all add: Limit_Lset_eq) 
   889 apply (blast intro: ltI Limit_is_Ord lt_trans) 
   890 done
   891 
   892 text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
   893 would suggest.  For a start it need the previous lemma, proved by induction.*}
   894 lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
   895 apply (simp add: L_def, auto) 
   896  apply (blast intro: Lset_lrank_lt) 
   897  apply (unfold lrank_def) 
   898 apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD]) 
   899 apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption) 
   900 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
   901 done
   902 
   903 lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
   904 by (simp add: Lset_iff_lrank_lt)
   905 
   906 text{*Kunen's VI, 1.9 (a)*}
   907 lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
   908 apply (unfold lrank_def) 
   909 apply (rule Least_equality) 
   910   apply (erule Ord_in_Lset) 
   911  apply assumption
   912 apply (insert notin_Lset [of i]) 
   913 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
   914 done
   915 
   916 
   917 lemma Ord_in_L: "Ord(i) ==> L(i)"
   918 by (blast intro: Ord_in_Lset L_I)
   919 
   920 text{*This is lrank(lrank(a)) = lrank(a) *}
   921 declare Ord_lrank [THEN lrank_of_Ord, simp]
   922 
   923 text{*Kunen's VI, 1.10 *}
   924 lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
   925 apply (simp add: Lset_succ DPow_def) 
   926 apply (rule_tac x="Nil" in bexI) 
   927  apply (rule_tac x="Equal(0,0)" in bexI) 
   928 apply auto 
   929 done
   930 
   931 lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
   932 apply (unfold lrank_def) 
   933 apply (rule Least_equality) 
   934   apply (rule Lset_in_Lset_succ) 
   935  apply assumption
   936 apply clarify 
   937 apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
   938  apply (blast dest: mem_irrefl) 
   939 apply (blast intro!: le_imp_subset Lset_mono) 
   940 done
   941 
   942 text{*Kunen's VI, 1.11 *}
   943 lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
   944 apply (erule trans_induct)
   945 apply (subst Lset) 
   946 apply (subst Vset) 
   947 apply (rule UN_mono [OF subset_refl]) 
   948 apply (rule subset_trans [OF DPow_subset_Pow]) 
   949 apply (rule Pow_mono, blast) 
   950 done
   951 
   952 text{*Kunen's VI, 1.12 *}
   953 lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
   954 apply (erule nat_induct)
   955  apply (simp add: Vfrom_0) 
   956 apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 
   957 done
   958 
   959 text{*Every set of constructible sets is included in some @{term Lset}*} 
   960 lemma subset_Lset:
   961      "(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
   962 by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
   963 
   964 lemma subset_LsetE:
   965      "[|\<forall>x\<in>A. L(x);
   966         !!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
   967       ==> P"
   968 by (blast dest: subset_Lset) 
   969 
   970 subsection{*For L to satisfy the ZF axioms*}
   971 
   972 theorem Union_in_L: "L(X) ==> L(Union(X))"
   973 apply (simp add: L_def, clarify) 
   974 apply (drule Ord_imp_greater_Limit) 
   975 apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) 
   976 done
   977 
   978 theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
   979 apply (simp add: L_def, clarify) 
   980 apply (drule Ord2_imp_greater_Limit, assumption) 
   981 apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
   982 done
   983 
   984 subsubsection{*For L to satisfy Powerset *}
   985 
   986 lemma LPow_env_typing:
   987      "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
   988 by (auto intro: L_I iff: Lset_succ_lrank_iff) 
   989 
   990 lemma LPow_in_Lset:
   991      "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
   992 apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
   993 apply simp 
   994 apply (rule LsetI [OF succI1])
   995 apply (simp add: DPow_def) 
   996 apply (intro conjI, clarify) 
   997 apply (rule_tac a="x" in UN_I, simp+)  
   998 txt{*Now to create the formula @{term "y \<subseteq> X"} *}
   999 apply (rule_tac x="Cons(X,Nil)" in bexI) 
  1000  apply (rule_tac x="subset_fm(0,1)" in bexI) 
  1001   apply typecheck
  1002 apply (rule conjI) 
  1003 apply (simp add: succ_Un_distrib [symmetric]) 
  1004 apply (rule equality_iffI) 
  1005 apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
  1006 apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
  1007 done
  1008 
  1009 theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
  1010 by (blast intro: L_I dest: L_D LPow_in_Lset)
  1011 
  1012 end