src/ZF/Constructible/Formula.thy
author paulson
Tue Feb 01 18:01:57 2005 +0100 (2005-02-01)
changeset 15481 fc075ae929e4
parent 14171 0cab06e3bbd0
child 16417 9bc16273c2d4
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
     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 \<in> 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 proof (induct i rule: eps_induct, intro allI impI)
   637   fix x j
   638   assume "\<forall>y\<in>x. \<forall>j. y \<subseteq> j \<longrightarrow> Lset(y) \<subseteq> Lset(j)"
   639      and "x \<subseteq> j"
   640   thus "Lset(x) \<subseteq> Lset(j)"
   641     by (force simp add: Lset [of x] Lset [of j]) 
   642 qed
   643 
   644 text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
   645 lemma Lset_mono_mem [rule_format]:
   646      "ALL j. i:j --> Lset(i) <= Lset(j)"
   647 proof (induct i rule: eps_induct, intro allI impI)
   648   fix x j
   649   assume "\<forall>y\<in>x. \<forall>j. y \<in> j \<longrightarrow> Lset(y) \<subseteq> Lset(j)"
   650      and "x \<in> j"
   651   thus "Lset(x) \<subseteq> Lset(j)"
   652     by (force simp add: Lset [of j] 
   653               intro!: bexI intro: elem_subset_in_DPow dest: LsetD DPowD) 
   654 qed
   655 
   656 
   657 text{*Useful with Reflection to bump up the ordinal*}
   658 lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
   659 by (blast dest: ltD [THEN Lset_mono_mem]) 
   660 
   661 subsubsection{* 0, successor and limit equations for Lset *}
   662 
   663 lemma Lset_0 [simp]: "Lset(0) = 0"
   664 by (subst Lset, blast)
   665 
   666 lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
   667 by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
   668 
   669 lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"
   670 apply (subst Lset, rule UN_least)
   671 apply (erule succE) 
   672  apply blast 
   673 apply clarify
   674 apply (rule elem_subset_in_DPow)
   675  apply (subst Lset)
   676  apply blast 
   677 apply (blast intro: dest: DPowD Lset_mono_mem) 
   678 done
   679 
   680 lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
   681 by (intro equalityI Lset_succ_subset1 Lset_succ_subset2) 
   682 
   683 lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"
   684 apply (subst Lset)
   685 apply (rule equalityI)
   686  txt{*first inclusion*}
   687  apply (rule UN_least)
   688  apply (erule UnionE)
   689  apply (rule subset_trans)
   690   apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)
   691 txt{*opposite inclusion*}
   692 apply (rule UN_least)
   693 apply (subst Lset, blast)
   694 done
   695 
   696 subsubsection{* Lset applied to Limit ordinals *}
   697 
   698 lemma Limit_Lset_eq:
   699     "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
   700 by (simp add: Lset_Union [symmetric] Limit_Union_eq)
   701 
   702 lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a \<in> Lset(i)"
   703 by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
   704 
   705 lemma Limit_LsetE:
   706     "[| a: Lset(i);  ~R ==> Limit(i);
   707         !!x. [| x<i;  a: Lset(x) |] ==> R
   708      |] ==> R"
   709 apply (rule classical)
   710 apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
   711   prefer 2 apply assumption
   712  apply blast 
   713 apply (blast intro: ltI  Limit_is_Ord)
   714 done
   715 
   716 subsubsection{* Basic closure properties *}
   717 
   718 lemma zero_in_Lset: "y:x ==> 0 \<in> Lset(x)"
   719 by (subst Lset, blast intro: empty_in_DPow)
   720 
   721 lemma notin_Lset: "x \<notin> Lset(x)"
   722 apply (rule_tac a=x in eps_induct)
   723 apply (subst Lset)
   724 apply (blast dest: DPowD)  
   725 done
   726 
   727 
   728 subsection{*Constructible Ordinals: Kunen's VI 1.9 (b)*}
   729 
   730 lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
   731 apply (erule trans_induct3)
   732   apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
   733 txt{*The successor case remains.*} 
   734 apply (rule equalityI)
   735 txt{*First inclusion*}
   736  apply clarify  
   737  apply (erule Ord_linear_lt, assumption) 
   738    apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset]) 
   739   apply blast 
   740  apply (blast dest: ltD)
   741 txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
   742 apply auto
   743 txt{*Key case: *}
   744   apply (erule subst, rule Ords_in_DPow [OF Transset_Lset]) 
   745  apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE) 
   746 apply (blast intro: Ord_in_Ord) 
   747 done
   748 
   749 
   750 lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
   751 by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
   752 
   753 lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
   754 apply (simp add: Lset_succ)
   755 apply (subst Ords_of_Lset_eq [symmetric], assumption, 
   756        rule Ords_in_DPow [OF Transset_Lset]) 
   757 done
   758 
   759 lemma Ord_in_L: "Ord(i) ==> L(i)"
   760 by (simp add: L_def, blast intro: Ord_in_Lset)
   761 
   762 subsubsection{* Unions *}
   763 
   764 lemma Union_in_Lset:
   765      "X \<in> Lset(i) ==> Union(X) \<in> Lset(succ(i))"
   766 apply (insert Transset_Lset)
   767 apply (rule LsetI [OF succI1])
   768 apply (simp add: Transset_def DPow_def) 
   769 apply (intro conjI, blast)
   770 txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
   771 apply (rule_tac x="Cons(X,Nil)" in bexI) 
   772  apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI) 
   773   apply typecheck
   774 apply (simp add: succ_Un_distrib [symmetric], blast) 
   775 done
   776 
   777 theorem Union_in_L: "L(X) ==> L(Union(X))"
   778 by (simp add: L_def, blast dest: Union_in_Lset) 
   779 
   780 subsubsection{* Finite sets and ordered pairs *}
   781 
   782 lemma singleton_in_Lset: "a: Lset(i) ==> {a} \<in> Lset(succ(i))"
   783 by (simp add: Lset_succ singleton_in_DPow) 
   784 
   785 lemma doubleton_in_Lset:
   786      "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} \<in> Lset(succ(i))"
   787 by (simp add: Lset_succ empty_in_DPow cons_in_DPow) 
   788 
   789 lemma Pair_in_Lset:
   790     "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> \<in> Lset(succ(succ(i)))"
   791 apply (unfold Pair_def)
   792 apply (blast intro: doubleton_in_Lset) 
   793 done
   794 
   795 lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
   796 lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
   797 
   798 text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
   799 lemma doubleton_in_LLimit:
   800     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} \<in> Lset(i)"
   801 apply (erule Limit_LsetE, assumption)
   802 apply (erule Limit_LsetE, assumption)
   803 apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
   804                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   805 done
   806 
   807 theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
   808 apply (simp add: L_def, clarify) 
   809 apply (drule Ord2_imp_greater_Limit, assumption) 
   810 apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord) 
   811 done
   812 
   813 lemma Pair_in_LLimit:
   814     "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> \<in> Lset(i)"
   815 txt{*Infer that a, b occur at ordinals x,xa < i.*}
   816 apply (erule Limit_LsetE, assumption)
   817 apply (erule Limit_LsetE, assumption)
   818 txt{*Infer that succ(succ(x Un xa)) < i *}
   819 apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
   820                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
   821 done
   822 
   823 
   824 
   825 text{*The rank function for the constructible universe*}
   826 constdefs
   827   lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
   828     "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
   829 
   830 lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
   831 by (simp add: L_def, blast)
   832 
   833 lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
   834 by (simp add: L_def)
   835 
   836 lemma Ord_lrank [simp]: "Ord(lrank(a))"
   837 by (simp add: lrank_def)
   838 
   839 lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
   840 apply (erule trans_induct3)
   841   apply simp   
   842  apply (simp only: lrank_def) 
   843  apply (blast intro: Least_le) 
   844 apply (simp_all add: Limit_Lset_eq) 
   845 apply (blast intro: ltI Limit_is_Ord lt_trans) 
   846 done
   847 
   848 text{*Kunen's VI 1.8.  The proof is much harder than the text would
   849 suggest.  For a start, it needs the previous lemma, which is proved by
   850 induction.*}
   851 lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
   852 apply (simp add: L_def, auto) 
   853  apply (blast intro: Lset_lrank_lt) 
   854  apply (unfold lrank_def) 
   855 apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD]) 
   856 apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption) 
   857 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
   858 done
   859 
   860 lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
   861 by (simp add: Lset_iff_lrank_lt)
   862 
   863 text{*Kunen's VI 1.9 (a)*}
   864 lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
   865 apply (unfold lrank_def) 
   866 apply (rule Least_equality) 
   867   apply (erule Ord_in_Lset) 
   868  apply assumption
   869 apply (insert notin_Lset [of i]) 
   870 apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) 
   871 done
   872 
   873 
   874 text{*This is lrank(lrank(a)) = lrank(a) *}
   875 declare Ord_lrank [THEN lrank_of_Ord, simp]
   876 
   877 text{*Kunen's VI 1.10 *}
   878 lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
   879 apply (simp add: Lset_succ DPow_def) 
   880 apply (rule_tac x=Nil in bexI) 
   881  apply (rule_tac x="Equal(0,0)" in bexI) 
   882 apply auto 
   883 done
   884 
   885 lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
   886 apply (unfold lrank_def) 
   887 apply (rule Least_equality) 
   888   apply (rule Lset_in_Lset_succ) 
   889  apply assumption
   890 apply clarify 
   891 apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
   892  apply (blast dest: mem_irrefl) 
   893 apply (blast intro!: le_imp_subset Lset_mono) 
   894 done
   895 
   896 text{*Kunen's VI 1.11 *}
   897 lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
   898 apply (erule trans_induct)
   899 apply (subst Lset) 
   900 apply (subst Vset) 
   901 apply (rule UN_mono [OF subset_refl]) 
   902 apply (rule subset_trans [OF DPow_subset_Pow]) 
   903 apply (rule Pow_mono, blast) 
   904 done
   905 
   906 text{*Kunen's VI 1.12 *}
   907 lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
   908 apply (erule nat_induct)
   909  apply (simp add: Vfrom_0) 
   910 apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow) 
   911 done
   912 
   913 text{*Every set of constructible sets is included in some @{term Lset}*} 
   914 lemma subset_Lset:
   915      "(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
   916 by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
   917 
   918 lemma subset_LsetE:
   919      "[|\<forall>x\<in>A. L(x);
   920         !!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
   921       ==> P"
   922 by (blast dest: subset_Lset) 
   923 
   924 subsubsection{*For L to satisfy the Powerset axiom *}
   925 
   926 lemma LPow_env_typing:
   927     "[| y \<in> Lset(i); Ord(i); y \<subseteq> X |] 
   928      ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
   929 by (auto intro: L_I iff: Lset_succ_lrank_iff) 
   930 
   931 lemma LPow_in_Lset:
   932      "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
   933 apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
   934 apply simp 
   935 apply (rule LsetI [OF succI1])
   936 apply (simp add: DPow_def) 
   937 apply (intro conjI, clarify) 
   938  apply (rule_tac a=x in UN_I, simp+)  
   939 txt{*Now to create the formula @{term "y \<subseteq> X"} *}
   940 apply (rule_tac x="Cons(X,Nil)" in bexI) 
   941  apply (rule_tac x="subset_fm(0,1)" in bexI) 
   942   apply typecheck
   943  apply (rule conjI) 
   944 apply (simp add: succ_Un_distrib [symmetric]) 
   945 apply (rule equality_iffI) 
   946 apply (simp add: Transset_UN [OF Transset_Lset] LPow_env_typing)
   947 apply (auto intro: L_I iff: Lset_succ_lrank_iff) 
   948 done
   949 
   950 theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
   951 by (blast intro: L_I dest: L_D LPow_in_Lset)
   952 
   953 
   954 subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
   955 
   956 lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
   957 by (induct_tac n, auto)
   958 
   959 lemma sats_app_0_iff [rule_format]:
   960   "[| p \<in> formula; 0 \<in> A |]
   961    ==> \<forall>env \<in> list(A). sats(A,p, env@[0]) <-> sats(A,p,env)"
   962 apply (induct_tac p)
   963 apply (simp_all del: app_Cons add: app_Cons [symmetric]
   964 		add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0)
   965 done
   966 
   967 lemma sats_app_zeroes_iff:
   968   "[| p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat |]
   969    ==> sats(A,p,env @ repeat(0,n)) <-> sats(A,p,env)"
   970 apply (induct_tac n, simp) 
   971 apply (simp del: repeat.simps
   972             add: repeat_succ_app sats_app_0_iff app_assoc [symmetric]) 
   973 done
   974 
   975 lemma exists_bigger_env:
   976   "[| p \<in> formula; 0 \<in> A; env \<in> list(A) |]
   977    ==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) & 
   978               (\<forall>a\<in>A. sats(A,p,Cons(a,env')) <-> sats(A,p,Cons(a,env)))"
   979 apply (rule_tac x="env @ repeat(0,arity(p))" in bexI) 
   980 apply (simp del: app_Cons add: app_Cons [symmetric]
   981 	    add: length_repeat sats_app_zeroes_iff, typecheck)
   982 done
   983 
   984 
   985 text{*A simpler version of @{term DPow}: no arity check!*}
   986 constdefs DPow' :: "i => i"
   987   "DPow'(A) == {X \<in> Pow(A). 
   988                 \<exists>env \<in> list(A). \<exists>p \<in> formula. 
   989                     X = {x\<in>A. sats(A, p, Cons(x,env))}}"
   990 
   991 lemma DPow_subset_DPow': "DPow(A) <= DPow'(A)";
   992 by (simp add: DPow_def DPow'_def, blast)
   993 
   994 lemma DPow'_0: "DPow'(0) = {0}"
   995 by (auto simp add: DPow'_def)
   996 
   997 lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)"
   998 apply (auto simp add: DPow'_def DPow_def) 
   999 apply (frule exists_bigger_env, assumption+, force)  
  1000 done
  1001 
  1002 lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
  1003 apply (drule Transset_0_disj) 
  1004 apply (erule disjE) 
  1005  apply (simp add: DPow'_0 Finite_DPow_eq_Pow) 
  1006 apply (rule equalityI)
  1007  apply (rule DPow_subset_DPow') 
  1008 apply (erule DPow'_subset_DPow) 
  1009 done
  1010 
  1011 text{*And thus we can relativize @{term Lset} without bothering with
  1012       @{term arity} and @{term length}*}
  1013 lemma Lset_eq_transrec_DPow': "Lset(i) = transrec(i, %x f. \<Union>y\<in>x. DPow'(f`y))"
  1014 apply (rule_tac a=i in eps_induct)
  1015 apply (subst Lset)
  1016 apply (subst transrec)
  1017 apply (simp only: DPow_eq_DPow' [OF Transset_Lset], simp) 
  1018 done
  1019 
  1020 text{*With this rule we can specify @{term p} later and don't worry about
  1021       arities at all!*}
  1022 lemma DPow_LsetI [rule_format]:
  1023   "[|\<forall>x\<in>Lset(i). P(x) <-> sats(Lset(i), p, Cons(x,env));
  1024      env \<in> list(Lset(i));  p \<in> formula|]
  1025    ==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))"
  1026 by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast) 
  1027 
  1028 end