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