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