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