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.14 +by (simp add: bool_of_o_def) 
    1.15 +
    1.16 +lemma [simp]: "bool_of_o(False) = 0"
    1.17 +by (simp add: bool_of_o_def) 
    1.18 +
    1.19 +lemma [simp,TC]: "bool_of_o(P) \<in> bool"
    1.20 +by (simp add: bool_of_o_def) 
    1.21 +
    1.22 +lemma [simp]: "(bool_of_o(P) = 1) <-> P"
    1.23 +by (simp add: bool_of_o_def) 
    1.24 +
    1.25 +lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
    1.26 +by (simp add: bool_of_o_def) 
    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.33 +by (simp add: succ_def)
    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.80 +apply (simp add: Vset_succ) 
    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.87 +apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])
    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.92 +apply (simp add: Un_least_lt_iff) 
    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.120 +by (simp add: Or_def) 
   1.121 +
   1.122 +lemma Implies_type [TC]:
   1.123 +     "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
   1.124 +by (simp add: Implies_def) 
   1.125 +
   1.126 +lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
   1.127 +by (simp add: Exists_def) 
   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.186 +by (simp add: Or_def)
   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.197 +by (simp add: Exists_def)
   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.210 +by (simp add: sat_def)
   1.211 +
   1.212 +lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
   1.213 +by (simp add: sat_def)
   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.221 +by (simp add: incr_var_def)
   1.222 +
   1.223 +lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
   1.224 +apply (simp add: incr_var_def) 
   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.251 +by (simp add: incr_var_def) 
   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.257 +by (simp add: incr_boundvars_def) 
   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.278 +apply (simp add: incr_boundvars_def) 
   1.279 +done
   1.280 +
   1.281 +(*UNUSED
   1.282 +lemma formula_add_params [rule_format]:
   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.310 +by (simp add: Or_def) 
   1.311 +
   1.312 +lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
   1.313 +by (simp add: Implies_def) 
   1.314 +
   1.315 +lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
   1.316 +by (simp add: Exists_def) 
   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.368 +apply (simp add:  Un_commute)
   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.376 +apply (simp add: incr_boundvars_def) 
   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.395 +by (simp add: incr_bv1_def) 
   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.403 +apply (simp add: incr_bv1_def) 
   1.404 +done
   1.405 +
   1.406 +lemma formula_add_params1 [rule_format]:
   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.414 +apply (simp_all add: sats_incr_bv1_iff) 
   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.423 +apply (simp add: incr_bv1_def) 
   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.432 +apply (simp add: not_lt_iff_le)
   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.456 +by (simp add: DPow_def) 
   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.469 +apply (simp add: DPow_def)
   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.492 +apply (simp add: arity_sats1_iff formula_add_params1, blast) 
   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.502 +apply (simp add: DPow_def)
   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.575 +apply (simp add: Transset_def)
   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.580 +apply (simp add: Transset_def) 
   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.686 +by (simp add: subset_fm_def) 
   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.704 +by (simp add: transset_fm_def) 
   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.723 +by (simp add: ordinal_fm_def) 
   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.742 +apply (simp_all add: sats_ordinal_fm)
   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.769 +apply (simp add: Lset_succ)
   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.890 +by (simp add: L_def)
   1.891 +
   1.892 +lemma Ord_lrank [simp]: "Ord(lrank(a))"
   1.893 +by (simp add: lrank_def)
   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.900 +apply (simp_all add: Limit_Lset_eq) 
   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.916 +by (simp add: Lset_iff_lrank_lt)
   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.992 +apply (simp add: DPow_def) 
   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