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