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