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