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