src/ZF/Constructible/Formula.thy
 author wenzelm Thu Dec 14 11:24:26 2017 +0100 (21 months ago) changeset 67198 694f29a5433b parent 65449 c82e63b11b8b child 67443 3abf6a722518 permissions -rw-r--r--
merged
```     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
```