src/ZF/Constructible/Formula.thy
 changeset 13223 45be08fbdcff child 13245 714f7a423a15
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/ZF/Constructible/Formula.thy	Wed Jun 19 11:48:01 2002 +0200
1.3 @@ -0,0 +1,1006 @@
1.4 +header {* First-Order Formulas and the Definition of the Class L *}
1.5 +
1.6 +theory Formula = Main:
1.7 +
1.8 +
1.9 +(*??for Bool.thy**)
1.10 +constdefs bool_of_o :: "o=>i"
1.11 +   "bool_of_o(P) == (if P then 1 else 0)"
1.12 +
1.13 +lemma [simp]: "bool_of_o(True) = 1"
1.15 +
1.16 +lemma [simp]: "bool_of_o(False) = 0"
1.18 +
1.19 +lemma [simp,TC]: "bool_of_o(P) \<in> bool"
1.21 +
1.22 +lemma [simp]: "(bool_of_o(P) = 1) <-> P"
1.24 +
1.25 +lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
1.27 +
1.28 +(*????????????????Cardinal.ML*)
1.29 +lemma Finite_cons_iff [iff]:  "Finite(cons(y,x)) <-> Finite(x)"
1.30 +by (blast intro: Finite_cons subset_Finite)
1.31 +
1.32 +lemma Finite_succ_iff [iff]:  "Finite(succ(x)) <-> Finite(x)"
1.34 +
1.35 +declare Finite_0 [simp]
1.36 +
1.37 +lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
1.38 +by (erule Finite_induct, simp_all)
1.39 +
1.40 +lemma Finite_RepFun_lemma [rule_format]:
1.41 +     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|]
1.42 +      ==> \<forall>A. x = RepFun(A,f) --> Finite(A)"
1.43 +apply (erule Finite_induct)
1.44 + apply clarify
1.45 + apply (case_tac "A=0", simp)
1.46 + apply (blast del: allE, clarify)
1.47 +apply (subgoal_tac "\<exists>z\<in>A. x = f(z)")
1.48 + prefer 2 apply (blast del: allE elim: equalityE, clarify)
1.49 +apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
1.50 + apply (blast intro: Diff_sing_Finite)
1.51 +apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)")
1.52 +apply (rule equalityI)
1.53 + apply (blast intro: elim: equalityE)
1.54 +apply (blast intro: elim: equalityCE)
1.55 +done
1.56 +
1.57 +text{*I don't know why, but if the premise is expressed using meta-connectives
1.58 +then  the simplifier cannot prove it automatically in conditional rewriting.*}
1.59 +lemma Finite_RepFun_iff:
1.60 +     "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
1.61 +by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f])
1.62 +
1.63 +lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
1.64 +apply (erule Finite_induct)
1.65 +apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
1.66 +done
1.67 +
1.68 +lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
1.69 +apply (subgoal_tac "Finite({{x} . x \<in> A})")
1.70 + apply (simp add: Finite_RepFun_iff )
1.71 +apply (blast intro: subset_Finite)
1.72 +done
1.73 +
1.74 +lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
1.75 +by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
1.76 +
1.77 +lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
1.78 +apply (erule nat_induct)
1.79 + apply (simp add: Vfrom_0)
1.81 +done
1.82 +
1.83 +(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)
1.84 +text{*Every ordinal is exceeded by some limit ordinal.*}
1.85 +lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
1.86 +apply (rule_tac x="i ++ nat" in exI)
1.88 +done
1.89 +
1.90 +lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
1.91 +apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
1.93 +done
1.94 +
1.95 +
1.96 +
1.97 +(*Internalized formulas of FOL. De Bruijn representation.
1.98 +  Unbound variables get their denotations from an environment.*)
1.99 +
1.100 +consts   formula :: i
1.101 +datatype
1.102 +  "formula" = Member ("x: nat", "y: nat")
1.103 +            | Equal  ("x: nat", "y: nat")
1.104 +            | Neg ("p: formula")
1.105 +            | And ("p: formula", "q: formula")
1.106 +            | Forall ("p: formula")
1.107 +
1.108 +declare formula.intros [TC]
1.109 +
1.110 +constdefs Or :: "[i,i]=>i"
1.111 +    "Or(p,q) == Neg(And(Neg(p),Neg(q)))"
1.112 +
1.113 +constdefs Implies :: "[i,i]=>i"
1.114 +    "Implies(p,q) == Neg(And(p,Neg(q)))"
1.115 +
1.116 +constdefs Exists :: "i=>i"
1.117 +    "Exists(p) == Neg(Forall(Neg(p)))";
1.118 +
1.119 +lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
1.121 +
1.122 +lemma Implies_type [TC]:
1.123 +     "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
1.125 +
1.126 +lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
1.128 +
1.129 +
1.130 +consts   satisfies :: "[i,i]=>i"
1.131 +primrec (*explicit lambda is required because the environment varies*)
1.132 +  "satisfies(A,Member(x,y)) =
1.133 +      (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"
1.134 +
1.135 +  "satisfies(A,Equal(x,y)) =
1.136 +      (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
1.137 +
1.138 +  "satisfies(A,Neg(p)) =
1.139 +      (\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"
1.140 +
1.141 +  "satisfies(A,And(p,q)) =
1.142 +      (\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"
1.143 +
1.144 +  "satisfies(A,Forall(p)) =
1.145 +      (\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
1.146 +
1.147 +
1.148 +lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
1.149 +by (induct_tac p, simp_all)
1.150 +
1.151 +syntax sats :: "[i,i,i] => o"
1.152 +translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
1.153 +
1.154 +lemma [simp]:
1.155 +  "env \<in> list(A)
1.156 +   ==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)"
1.157 +by simp
1.158 +
1.159 +lemma [simp]:
1.160 +  "env \<in> list(A)
1.161 +   ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
1.162 +by simp
1.163 +
1.164 +lemma sats_Neg_iff [simp]:
1.165 +  "env \<in> list(A)
1.166 +   ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
1.167 +by (simp add: Bool.not_def cond_def)
1.168 +
1.169 +lemma sats_And_iff [simp]:
1.170 +  "env \<in> list(A)
1.171 +   ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
1.172 +by (simp add: Bool.and_def cond_def)
1.173 +
1.174 +lemma sats_Forall_iff [simp]:
1.175 +  "env \<in> list(A)
1.176 +   ==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
1.177 +by simp
1.178 +
1.179 +declare satisfies.simps [simp del];
1.180 +
1.181 +(**** DIVIDING LINE BETWEEN PRIMITIVE AND DERIVED CONNECTIVES ****)
1.182 +
1.183 +lemma sats_Or_iff [simp]:
1.184 +  "env \<in> list(A)
1.185 +   ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
1.187 +
1.188 +lemma sats_Implies_iff [simp]:
1.189 +  "env \<in> list(A)
1.190 +   ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
1.191 +apply (simp add: Implies_def, blast)
1.192 +done
1.193 +
1.194 +lemma sats_Exists_iff [simp]:
1.195 +  "env \<in> list(A)
1.196 +   ==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
1.198 +
1.199 +
1.200 +
1.201 +
1.202 +(*pretty but unnecessary
1.203 +constdefs sat     :: "[i,i] => o"
1.204 +  "sat(A,p) == satisfies(A,p)`[] = 1"
1.205 +
1.206 +syntax "_sat"  :: "[i,i] => o"    (infixl "|=" 50)
1.207 +translations "A |= p" == "sat(A,p)"
1.208 +
1.209 +lemma [simp]: "(A |= Neg(p)) <-> ~ (A |= p)"
1.211 +
1.212 +lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
1.214 +*)
1.215 +
1.216 +
1.217 +constdefs incr_var :: "[i,i]=>i"
1.218 +    "incr_var(x,lev) == if x<lev then x else succ(x)"
1.219 +
1.220 +lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
1.222 +
1.223 +lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
1.225 +apply (blast dest: lt_trans1)
1.226 +done
1.227 +
1.228 +consts   incr_bv :: "i=>i"
1.229 +primrec
1.230 +  "incr_bv(Member(x,y)) =
1.231 +      (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
1.232 +
1.233 +  "incr_bv(Equal(x,y)) =
1.234 +      (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
1.235 +
1.236 +  "incr_bv(Neg(p)) =
1.237 +      (\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"
1.238 +
1.239 +  "incr_bv(And(p,q)) =
1.240 +      (\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"
1.241 +
1.242 +  "incr_bv(Forall(p)) =
1.243 +      (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
1.244 +
1.245 +
1.246 +constdefs incr_boundvars :: "i => i"
1.247 +    "incr_boundvars(p) == incr_bv(p)`0"
1.248 +
1.249 +
1.250 +lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
1.252 +
1.253 +lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
1.254 +by (induct_tac p, simp_all)
1.255 +
1.256 +lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
1.258 +
1.259 +(*Obviously DPow is closed under complements and finite intersections and
1.260 +unions.  Needs an inductive lemma to allow two lists of parameters to
1.261 +be combined.*)
1.262 +
1.263 +lemma sats_incr_bv_iff [rule_format]:
1.264 +  "[| p \<in> formula; env \<in> list(A); x \<in> A |]
1.265 +   ==> \<forall>bvs \<in> list(A).
1.266 +           sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <->
1.267 +           sats(A, p, bvs@env)"
1.268 +apply (induct_tac p)
1.269 +apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)
1.270 +apply (auto simp add: diff_succ not_lt_iff_le)
1.271 +done
1.272 +
1.273 +(*UNUSED*)
1.274 +lemma sats_incr_boundvars_iff:
1.275 +  "[| p \<in> formula; env \<in> list(A); x \<in> A |]
1.276 +   ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
1.277 +apply (insert sats_incr_bv_iff [of p env A x Nil])
1.279 +done
1.280 +
1.281 +(*UNUSED
1.283 +  "[| p \<in> formula; n \<in> nat |]
1.284 +   ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
1.285 +         length(bvs) = n -->
1.286 +         sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
1.287 +apply (induct_tac n, simp, clarify)
1.288 +apply (erule list.cases)
1.289 +apply (auto simp add: sats_incr_boundvars_iff)
1.290 +done
1.291 +*)
1.292 +
1.293 +consts   arity :: "i=>i"
1.294 +primrec
1.295 +  "arity(Member(x,y)) = succ(x) \<union> succ(y)"
1.296 +
1.297 +  "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
1.298 +
1.299 +  "arity(Neg(p)) = arity(p)"
1.300 +
1.301 +  "arity(And(p,q)) = arity(p) \<union> arity(q)"
1.302 +
1.303 +  "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"
1.304 +
1.305 +
1.306 +lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
1.307 +by (induct_tac p, simp_all)
1.308 +
1.309 +lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
1.311 +
1.312 +lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
1.314 +
1.315 +lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
1.317 +
1.318 +
1.319 +lemma arity_sats_iff [rule_format]:
1.320 +  "[| p \<in> formula; extra \<in> list(A) |]
1.321 +   ==> \<forall>env \<in> list(A).
1.322 +           arity(p) \<le> length(env) -->
1.323 +           sats(A, p, env @ extra) <-> sats(A, p, env)"
1.324 +apply (induct_tac p)
1.325 +apply (simp_all add: nth_append Un_least_lt_iff arity_type
1.326 +                split: split_nat_case3, auto)
1.327 +done
1.328 +
1.329 +lemma arity_sats1_iff:
1.330 +  "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
1.331 +    extra \<in> list(A) |]
1.332 +   ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
1.333 +apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
1.334 +apply simp
1.335 +done
1.336 +
1.337 +(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
1.338 +lemma incr_var_lemma:
1.339 +     "[| x \<in> nat; y \<in> nat; lev \<le> x |]
1.340 +      ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
1.341 +apply (simp add: incr_var_def Ord_Un_if, auto)
1.342 +  apply (blast intro: leI)
1.343 + apply (simp add: not_lt_iff_le)
1.344 + apply (blast intro: le_anti_sym)
1.345 +apply (blast dest: lt_trans2)
1.346 +done
1.347 +
1.348 +lemma incr_And_lemma:
1.349 +     "y < x ==> y \<union> succ(x) = succ(x \<union> y)"
1.350 +apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)
1.351 +apply (blast dest: lt_asym)
1.352 +done
1.353 +
1.354 +lemma arity_incr_bv_lemma [rule_format]:
1.355 +  "p \<in> formula
1.356 +   ==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =
1.357 +                 (if n < arity(p) then succ(arity(p)) else arity(p))"
1.358 +apply (induct_tac p)
1.359 +apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
1.360 +                     succ_Un_distrib [symmetric] incr_var_lt incr_var_le
1.361 +                     Un_commute incr_var_lemma arity_type
1.362 +            split: split_nat_case3)
1.363 +(*left with the And case*)
1.364 +apply safe
1.365 + apply (blast intro: incr_And_lemma lt_trans1)
1.366 +apply (subst incr_And_lemma)
1.367 + apply (blast intro:  lt_trans1)
1.369 +done
1.370 +
1.371 +lemma arity_incr_boundvars_eq:
1.372 +  "p \<in> formula
1.373 +   ==> arity(incr_boundvars(p)) =
1.374 +        (if 0 < arity(p) then succ(arity(p)) else arity(p))"
1.375 +apply (insert arity_incr_bv_lemma [of p 0])
1.377 +done
1.378 +
1.379 +lemma arity_iterates_incr_boundvars_eq:
1.380 +  "[| p \<in> formula; n \<in> nat |]
1.381 +   ==> arity(incr_boundvars^n(p)) =
1.382 +         (if 0 < arity(p) then n #+ arity(p) else arity(p))"
1.383 +apply (induct_tac n)
1.384 +apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le)
1.385 +done
1.386 +
1.387 +
1.388 +(**** TRYING INCR_BV1 AGAIN ****)
1.389 +
1.390 +constdefs incr_bv1 :: "i => i"
1.391 +    "incr_bv1(p) == incr_bv(p)`1"
1.392 +
1.393 +
1.394 +lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
1.396 +
1.397 +(*For renaming all but the bound variable at level 0*)
1.398 +lemma sats_incr_bv1_iff [rule_format]:
1.399 +  "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
1.400 +   ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <->
1.401 +       sats(A, p, Cons(x,env))"
1.402 +apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
1.404 +done
1.405 +
1.407 +  "[| p \<in> formula; n \<in> nat; x \<in> A |]
1.408 +   ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
1.409 +          length(bvs) = n -->
1.410 +          sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <->
1.411 +          sats(A, p, Cons(x,env))"
1.412 +apply (induct_tac n, simp, clarify)
1.413 +apply (erule list.cases)
1.415 +done
1.416 +
1.417 +
1.418 +lemma arity_incr_bv1_eq:
1.419 +  "p \<in> formula
1.420 +   ==> arity(incr_bv1(p)) =
1.421 +        (if 1 < arity(p) then succ(arity(p)) else arity(p))"
1.422 +apply (insert arity_incr_bv_lemma [of p 1])
1.424 +done
1.425 +
1.426 +lemma arity_iterates_incr_bv1_eq:
1.427 +  "[| p \<in> formula; n \<in> nat |]
1.428 +   ==> arity(incr_bv1^n(p)) =
1.429 +         (if 1 < arity(p) then n #+ arity(p) else arity(p))"
1.430 +apply (induct_tac n)
1.431 +apply (simp_all add: arity_incr_bv1_eq )
1.433 +apply (blast intro: le_trans add_le_self2 arity_type)
1.434 +done
1.435 +
1.436 +
1.437 +(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
1.438 +constdefs DPow :: "i => i"
1.439 +  "DPow(A) == {X \<in> Pow(A).
1.440 +               \<exists>env \<in> list(A). \<exists>p \<in> formula.
1.441 +                 arity(p) \<le> succ(length(env)) &
1.442 +                 X = {x\<in>A. sats(A, p, Cons(x,env))}}"
1.443 +
1.444 +lemma DPowI:
1.445 +  "[|X <= A;  env \<in> list(A);  p \<in> formula;
1.446 +     arity(p) \<le> succ(length(env))|]
1.447 +   ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
1.448 +by (simp add: DPow_def, blast)
1.449 +
1.450 +lemma DPowD:
1.451 +  "X \<in> DPow(A)
1.452 +   ==> X <= A &
1.453 +       (\<exists>env \<in> list(A).
1.454 +        \<exists>p \<in> formula. arity(p) \<le> succ(length(env)) &
1.455 +                      X = {x\<in>A. sats(A, p, Cons(x,env))})"
1.457 +
1.458 +lemmas DPow_imp_subset = DPowD [THEN conjunct1]
1.459 +
1.460 +(*Lemma 1.2*)
1.461 +lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |]
1.462 +       ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
1.463 +by (blast intro: DPowI)
1.464 +
1.465 +lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"
1.466 +by (simp add: DPow_def, blast)
1.467 +
1.468 +lemma empty_in_DPow: "0 \<in> DPow(A)"
1.470 +apply (rule_tac x="Nil" in bexI)
1.471 + apply (rule_tac x="Neg(Equal(0,0))" in bexI)
1.472 +  apply (auto simp add: Un_least_lt_iff)
1.473 +done
1.474 +
1.475 +lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
1.476 +apply (simp add: DPow_def, clarify, auto)
1.477 +apply (rule bexI)
1.478 + apply (rule_tac x="Neg(p)" in bexI)
1.479 +  apply auto
1.480 +done
1.481 +
1.482 +lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)"
1.483 +apply (simp add: DPow_def, auto)
1.484 +apply (rename_tac envp p envq q)
1.485 +apply (rule_tac x="envp@envq" in bexI)
1.486 + apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)
1.487 +  apply typecheck
1.488 +apply (rule conjI)
1.489 +(*finally check the arity!*)
1.490 + apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
1.491 + apply (force intro: add_le_self le_trans)
1.493 +done
1.494 +
1.495 +lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)"
1.496 +apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))")
1.497 +apply (simp add: Int_in_DPow Compl_in_DPow)
1.498 +apply (simp add: DPow_def, blast)
1.499 +done
1.500 +
1.501 +lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
1.503 +apply (rule_tac x="Cons(x,Nil)" in bexI)
1.504 + apply (rule_tac x="Equal(0,1)" in bexI)
1.505 +  apply typecheck
1.506 +apply (force simp add: succ_Un_distrib [symmetric])
1.507 +done
1.508 +
1.509 +lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
1.510 +apply (rule cons_eq [THEN subst])
1.511 +apply (blast intro: singleton_in_DPow Un_in_DPow)
1.512 +done
1.513 +
1.514 +(*Part of Lemma 1.3*)
1.515 +lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
1.516 +apply (erule Fin.induct)
1.517 + apply (rule empty_in_DPow)
1.518 +apply (blast intro: cons_in_DPow)
1.519 +done
1.520 +
1.521 +(*DPow is not monotonic.  For example, let A be some non-constructible set
1.522 +  of natural numbers, and let B be nat.  Then A<=B and obviously A : DPow(A)
1.523 +  but A ~: DPow(B).*)
1.524 +lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
1.525 +apply (simp add: DPow_def, auto)
1.526 +(*must use the formula defining A in B to relativize the new formula...*)
1.527 +oops
1.528 +
1.529 +lemma DPow_0: "DPow(0) = {0}"
1.530 +by (blast intro: empty_in_DPow dest: DPow_imp_subset)
1.531 +
1.532 +lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)"
1.533 +by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
1.534 +
1.535 +lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
1.536 +apply (rule equalityI)
1.537 +apply (rule DPow_subset_Pow)
1.538 +apply (erule Finite_Pow_subset_Pow)
1.539 +done
1.540 +
1.541 +(*This may be true but the proof looks difficult, requiring relativization
1.542 +lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
1.543 +apply (rule equalityI, safe)
1.544 +oops
1.545 +*)
1.546 +
1.547 +subsection{* Constant Lset: Levels of the Constructible Universe *}
1.548 +
1.549 +constdefs Lset :: "i=>i"
1.550 +    "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
1.551 +
1.552 +text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
1.553 +lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
1.554 +by (subst Lset_def [THEN def_transrec], simp)
1.555 +
1.556 +lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
1.557 +by (subst Lset, blast)
1.558 +
1.559 +lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
1.560 +apply (insert Lset [of x])
1.561 +apply (blast intro: elim: equalityE)
1.562 +done
1.563 +
1.564 +subsubsection{* Transitivity *}
1.565 +
1.566 +lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)"
1.567 +apply (simp add: Transset_def DPow_def)
1.568 +apply (rule_tac x="[X]" in bexI)
1.569 + apply (rule_tac x="Member(0,1)" in bexI)
1.570 +  apply (auto simp add: Un_least_lt_iff)
1.571 +done
1.572 +
1.573 +lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"
1.574 +apply clarify
1.576 +apply (blast intro: elem_subset_in_DPow)
1.577 +done
1.578 +
1.579 +lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
1.581 +apply (blast intro: elem_subset_in_DPow dest: DPowD)
1.582 +done
1.583 +
1.584 +text{*Kunen's VI, 1.6 (a)*}
1.585 +lemma Transset_Lset: "Transset(Lset(i))"
1.586 +apply (rule_tac a=i in eps_induct)
1.587 +apply (subst Lset)
1.588 +apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
1.589 +done
1.590 +
1.591 +subsubsection{* Monotonicity *}
1.592 +
1.593 +text{*Kunen's VI, 1.6 (b)*}
1.594 +lemma Lset_mono [rule_format]:
1.595 +     "ALL j. i<=j --> Lset(i) <= Lset(j)"
1.596 +apply (rule_tac a=i in eps_induct)
1.597 +apply (rule impI [THEN allI])
1.598 +apply (subst Lset)
1.599 +apply (subst Lset, blast)
1.600 +done
1.601 +
1.602 +text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
1.603 +lemma Lset_mono_mem [rule_format]:
1.604 +     "ALL j. i:j --> Lset(i) <= Lset(j)"
1.605 +apply (rule_tac a=i in eps_induct)
1.606 +apply (rule impI [THEN allI])
1.607 +apply (subst Lset, auto)
1.608 +apply (rule rev_bexI, assumption)
1.609 +apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD)
1.610 +done
1.611 +
1.612 +subsubsection{* 0, successor and limit equations fof Lset *}
1.613 +
1.614 +lemma Lset_0 [simp]: "Lset(0) = 0"
1.615 +by (subst Lset, blast)
1.616 +
1.617 +lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
1.618 +by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
1.619 +
1.620 +lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"
1.621 +apply (subst Lset, rule UN_least)
1.622 +apply (erule succE)
1.623 + apply blast
1.624 +apply clarify
1.625 +apply (rule elem_subset_in_DPow)
1.626 + apply (subst Lset)
1.627 + apply blast
1.628 +apply (blast intro: dest: DPowD Lset_mono_mem)
1.629 +done
1.630 +
1.631 +lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
1.632 +by (intro equalityI Lset_succ_subset1 Lset_succ_subset2)
1.633 +
1.634 +lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"
1.635 +apply (subst Lset)
1.636 +apply (rule equalityI)
1.637 + txt{*first inclusion*}
1.638 + apply (rule UN_least)
1.639 + apply (erule UnionE)
1.640 + apply (rule subset_trans)
1.641 +  apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)
1.642 +txt{*opposite inclusion*}
1.643 +apply (rule UN_least)
1.644 +apply (subst Lset, blast)
1.645 +done
1.646 +
1.647 +subsubsection{* Lset applied to Limit ordinals *}
1.648 +
1.649 +lemma Limit_Lset_eq:
1.650 +    "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
1.651 +by (simp add: Lset_Union [symmetric] Limit_Union_eq)
1.652 +
1.653 +lemma lt_LsetI: "[| a: Lset(j);  j<i |] ==> a : Lset(i)"
1.654 +by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
1.655 +
1.656 +lemma Limit_LsetE:
1.657 +    "[| a: Lset(i);  ~R ==> Limit(i);
1.658 +        !!x. [| x<i;  a: Lset(x) |] ==> R
1.659 +     |] ==> R"
1.660 +apply (rule classical)
1.661 +apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
1.662 +  prefer 2 apply assumption
1.663 + apply blast
1.664 +apply (blast intro: ltI  Limit_is_Ord)
1.665 +done
1.666 +
1.667 +subsubsection{* Basic closure properties *}
1.668 +
1.669 +lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
1.670 +by (subst Lset, blast intro: empty_in_DPow)
1.671 +
1.672 +lemma notin_Lset: "x \<notin> Lset(x)"
1.673 +apply (rule_tac a=x in eps_induct)
1.674 +apply (subst Lset)
1.675 +apply (blast dest: DPowD)
1.676 +done
1.677 +
1.678 +
1.679 +
1.680 +text{*Kunen's VI, 1.9 (b)*}
1.681 +
1.682 +constdefs subset_fm :: "[i,i]=>i"
1.683 +    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
1.684 +
1.685 +lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
1.687 +
1.688 +lemma arity_subset_fm [simp]:
1.689 +     "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
1.690 +by (simp add: subset_fm_def succ_Un_distrib [symmetric])
1.691 +
1.692 +lemma sats_subset_fm [simp]:
1.693 +   "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
1.694 +    ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
1.695 +apply (frule lt_nat_in_nat, erule length_type)
1.696 +apply (simp add: subset_fm_def Transset_def)
1.697 +apply (blast intro: nth_type )
1.698 +done
1.699 +
1.700 +constdefs transset_fm :: "i=>i"
1.701 +   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
1.702 +
1.703 +lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
1.705 +
1.706 +lemma arity_transset_fm [simp]:
1.707 +     "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
1.708 +by (simp add: transset_fm_def succ_Un_distrib [symmetric])
1.709 +
1.710 +lemma sats_transset_fm [simp]:
1.711 +   "[|x < length(env); env \<in> list(A); Transset(A)|]
1.712 +    ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
1.713 +apply (frule lt_nat_in_nat, erule length_type)
1.714 +apply (simp add: transset_fm_def Transset_def)
1.715 +apply (blast intro: nth_type )
1.716 +done
1.717 +
1.718 +constdefs ordinal_fm :: "i=>i"
1.719 +   "ordinal_fm(x) ==
1.720 +      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
1.721 +
1.722 +lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
1.724 +
1.725 +lemma arity_ordinal_fm [simp]:
1.726 +     "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
1.727 +by (simp add: ordinal_fm_def succ_Un_distrib [symmetric])
1.728 +
1.729 +lemma sats_ordinal_fm [simp]:
1.730 +   "[|x < length(env); env \<in> list(A); Transset(A)|]
1.731 +    ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
1.732 +apply (frule lt_nat_in_nat, erule length_type)
1.733 +apply (simp add: ordinal_fm_def Ord_def Transset_def)
1.734 +apply (blast intro: nth_type )
1.735 +done
1.736 +
1.737 +text{*The subset consisting of the ordinals is definable.*}
1.738 +lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
1.739 +apply (simp add: DPow_def Collect_subset)
1.740 +apply (rule_tac x="Nil" in bexI)
1.741 + apply (rule_tac x="ordinal_fm(0)" in bexI)
1.743 +done
1.744 +
1.745 +lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
1.746 +apply (erule trans_induct3)
1.747 +  apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
1.748 +txt{*The successor case remains.*}
1.749 +apply (rule equalityI)
1.750 +txt{*First inclusion*}
1.751 + apply clarify
1.752 + apply (erule Ord_linear_lt, assumption)
1.753 +   apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset])
1.754 +  apply blast
1.755 + apply (blast dest: ltD)
1.756 +txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
1.757 +apply auto
1.758 +txt{*Key case: *}
1.759 +  apply (erule subst, rule Ords_in_DPow [OF Transset_Lset])
1.760 + apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE)
1.761 +apply (blast intro: Ord_in_Ord)
1.762 +done
1.763 +
1.764 +
1.765 +lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
1.766 +by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
1.767 +
1.768 +lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
1.770 +apply (subst Ords_of_Lset_eq [symmetric], assumption,
1.771 +       rule Ords_in_DPow [OF Transset_Lset])
1.772 +done
1.773 +
1.774 +subsubsection{* Unions *}
1.775 +
1.776 +lemma Union_in_Lset:
1.777 +     "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
1.778 +apply (insert Transset_Lset)
1.779 +apply (rule LsetI [OF succI1])
1.780 +apply (simp add: Transset_def DPow_def)
1.781 +apply (intro conjI, blast)
1.782 +txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
1.783 +apply (rule_tac x="Cons(X,Nil)" in bexI)
1.784 + apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI)
1.785 +  apply typecheck
1.786 +apply (simp add: succ_Un_distrib [symmetric], blast)
1.787 +done
1.788 +
1.789 +lemma Union_in_LLimit:
1.790 +     "[| X: Lset(i);  Limit(i) |] ==> Union(X) : Lset(i)"
1.791 +apply (rule Limit_LsetE, assumption+)
1.792 +apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
1.793 +done
1.794 +
1.795 +subsubsection{* Finite sets and ordered pairs *}
1.796 +
1.797 +lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
1.798 +by (simp add: Lset_succ singleton_in_DPow)
1.799 +
1.800 +lemma doubleton_in_Lset:
1.801 +     "[| a: Lset(i);  b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
1.802 +by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
1.803 +
1.804 +lemma Pair_in_Lset:
1.805 +    "[| a: Lset(i);  b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
1.806 +apply (unfold Pair_def)
1.807 +apply (blast intro: doubleton_in_Lset)
1.808 +done
1.809 +
1.810 +lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
1.811 +
1.812 +lemma singleton_in_LLimit:
1.813 +    "[| a: Lset(i);  Limit(i) |] ==> {a} : Lset(i)"
1.814 +apply (erule Limit_LsetE, assumption)
1.815 +apply (erule singleton_in_Lset [THEN lt_LsetI])
1.816 +apply (blast intro: Limit_has_succ)
1.817 +done
1.818 +
1.819 +lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
1.820 +lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
1.821 +
1.822 +text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
1.823 +lemma doubleton_in_LLimit:
1.824 +    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> {a,b} : Lset(i)"
1.825 +apply (erule Limit_LsetE, assumption)
1.826 +apply (erule Limit_LsetE, assumption)
1.827 +apply (blast intro:  lt_LsetI [OF doubleton_in_Lset]
1.828 +                     Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
1.829 +done
1.830 +
1.831 +lemma Pair_in_LLimit:
1.832 +    "[| a: Lset(i);  b: Lset(i);  Limit(i) |] ==> <a,b> : Lset(i)"
1.833 +txt{*Infer that a, b occur at ordinals x,xa < i.*}
1.834 +apply (erule Limit_LsetE, assumption)
1.835 +apply (erule Limit_LsetE, assumption)
1.836 +txt{*Infer that succ(succ(x Un xa)) < i *}
1.837 +apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
1.838 +                    Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
1.839 +done
1.840 +
1.841 +lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
1.842 +by (blast intro: Pair_in_LLimit)
1.843 +
1.844 +lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
1.845 +
1.846 +lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
1.847 +by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
1.848 +
1.849 +lemma nat_into_LLimit: "[| n: nat;  Limit(i) |] ==> n : Lset(i)"
1.850 +by (blast intro: nat_subset_LLimit [THEN subsetD])
1.851 +
1.852 +
1.853 +subsubsection{* Closure under disjoint union *}
1.854 +
1.855 +lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
1.856 +
1.857 +lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
1.858 +by (blast intro: nat_into_LLimit)
1.859 +
1.860 +lemma Inl_in_LLimit:
1.861 +    "[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
1.862 +apply (unfold Inl_def)
1.863 +apply (blast intro: zero_in_LLimit Pair_in_LLimit)
1.864 +done
1.865 +
1.866 +lemma Inr_in_LLimit:
1.867 +    "[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
1.868 +apply (unfold Inr_def)
1.869 +apply (blast intro: one_in_LLimit Pair_in_LLimit)
1.870 +done
1.871 +
1.872 +lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
1.873 +by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
1.874 +
1.875 +lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
1.876 +
1.877 +
1.878 +text{*The constructible universe and its rank function*}
1.879 +constdefs
1.880 +  L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
1.881 +    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
1.882 +
1.883 +  lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
1.884 +    "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
1.885 +
1.886 +lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
1.887 +by (simp add: L_def, blast)
1.888 +
1.889 +lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
1.891 +
1.892 +lemma Ord_lrank [simp]: "Ord(lrank(a))"
1.894 +
1.895 +lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
1.896 +apply (erule trans_induct3)
1.897 +  apply simp
1.898 + apply (simp only: lrank_def)
1.899 + apply (blast intro: Least_le)
1.901 +apply (blast intro: ltI Limit_is_Ord lt_trans)
1.902 +done
1.903 +
1.904 +text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
1.905 +would suggest.  For a start it need the previous lemma, proved by induction.*}
1.906 +lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
1.907 +apply (simp add: L_def, auto)
1.908 + apply (blast intro: Lset_lrank_lt)
1.909 + apply (unfold lrank_def)
1.910 +apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])
1.911 +apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)
1.912 +apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
1.913 +done
1.914 +
1.915 +lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
1.917 +
1.918 +text{*Kunen's VI, 1.9 (a)*}
1.919 +lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
1.920 +apply (unfold lrank_def)
1.921 +apply (rule Least_equality)
1.922 +  apply (erule Ord_in_Lset)
1.923 + apply assumption
1.924 +apply (insert notin_Lset [of i])
1.925 +apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
1.926 +done
1.927 +
1.928 +text{*This is lrank(lrank(a)) = lrank(a) *}
1.929 +declare Ord_lrank [THEN lrank_of_Ord, simp]
1.930 +
1.931 +text{*Kunen's VI, 1.10 *}
1.932 +lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
1.933 +apply (simp add: Lset_succ DPow_def)
1.934 +apply (rule_tac x="Nil" in bexI)
1.935 + apply (rule_tac x="Equal(0,0)" in bexI)
1.936 +apply auto
1.937 +done
1.938 +
1.939 +lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
1.940 +apply (unfold lrank_def)
1.941 +apply (rule Least_equality)
1.942 +  apply (rule Lset_in_Lset_succ)
1.943 + apply assumption
1.944 +apply clarify
1.945 +apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
1.946 + apply (blast dest: mem_irrefl)
1.947 +apply (blast intro!: le_imp_subset Lset_mono)
1.948 +done
1.949 +
1.950 +text{*Kunen's VI, 1.11 *}
1.951 +lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
1.952 +apply (erule trans_induct)
1.953 +apply (subst Lset)
1.954 +apply (subst Vset)
1.955 +apply (rule UN_mono [OF subset_refl])
1.956 +apply (rule subset_trans [OF DPow_subset_Pow])
1.957 +apply (rule Pow_mono, blast)
1.958 +done
1.959 +
1.960 +text{*Kunen's VI, 1.12 *}
1.961 +lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
1.962 +apply (erule nat_induct)
1.963 + apply (simp add: Vfrom_0)
1.964 +apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
1.965 +done
1.966 +
1.967 +subsection{*For L to satisfy the ZF axioms*}
1.968 +
1.969 +lemma Union_in_L: "L(X) ==> L(Union(X))"
1.970 +apply (simp add: L_def, clarify)
1.971 +apply (drule Ord_imp_greater_Limit)
1.972 +apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)
1.973 +done
1.974 +
1.975 +lemma doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
1.976 +apply (simp add: L_def, clarify)
1.977 +apply (drule Ord2_imp_greater_Limit, assumption)
1.978 +apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
1.979 +done
1.980 +
1.981 +subsubsection{*For L to satisfy Powerset *}
1.982 +
1.983 +lemma LPow_env_typing:
1.984 +     "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
1.985 +by (auto intro: L_I iff: Lset_succ_lrank_iff)
1.986 +
1.987 +lemma LPow_in_Lset:
1.988 +     "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
1.989 +apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
1.990 +apply simp
1.991 +apply (rule LsetI [OF succI1])
1.993 +apply (intro conjI, clarify)
1.994 +apply (rule_tac a="x" in UN_I, simp+)
1.995 +txt{*Now to create the formula @{term "y \<subseteq> X"} *}
1.996 +apply (rule_tac x="Cons(X,Nil)" in bexI)
1.997 + apply (rule_tac x="subset_fm(0,1)" in bexI)
1.998 +  apply typecheck
1.999 +apply (rule conjI)
1.1000 +apply (simp add: succ_Un_distrib [symmetric])
1.1001 +apply (rule equality_iffI)
1.1002 +apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
1.1003 +apply (auto intro: L_I iff: Lset_succ_lrank_iff)
1.1004 +done
1.1005 +
1.1006 +lemma LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
1.1007 +by (blast intro: L_I dest: L_D LPow_in_Lset)
1.1008 +
1.1009 +end
```