new theory of inner models
authorpaulson
Wed Jun 19 11:48:01 2002 +0200 (2002-06-19)
changeset 1322345be08fbdcff
parent 13222 74d9144c452c
child 13224 6f0928a942d1
new theory of inner models
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/ROOT.ML
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
     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
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Wed Jun 19 11:48:01 2002 +0200
     2.3 @@ -0,0 +1,129 @@
     2.4 +header {* The class L satisfies the axioms of ZF*}
     2.5 +
     2.6 +theory L_axioms = Formula + Relative:
     2.7 +
     2.8 +
     2.9 +text {* The class L satisfies the premises of locale @{text M_axioms} *}
    2.10 +
    2.11 +lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
    2.12 +apply (insert Transset_Lset) 
    2.13 +apply (simp add: Transset_def L_def, blast) 
    2.14 +done
    2.15 +
    2.16 +lemma nonempty: "L(0)"
    2.17 +apply (simp add: L_def) 
    2.18 +apply (blast intro: zero_in_Lset) 
    2.19 +done
    2.20 +
    2.21 +lemma upair_ax: "upair_ax(L)"
    2.22 +apply (simp add: upair_ax_def upair_def, clarify)
    2.23 +apply (rule_tac x="{x,y}" in exI)  
    2.24 +apply (simp add: doubleton_in_L) 
    2.25 +done
    2.26 +
    2.27 +lemma Union_ax: "Union_ax(L)"
    2.28 +apply (simp add: Union_ax_def big_union_def, clarify)
    2.29 +apply (rule_tac x="Union(x)" in exI)  
    2.30 +apply (simp add: Union_in_L, auto) 
    2.31 +apply (blast intro: transL) 
    2.32 +done
    2.33 +
    2.34 +lemma power_ax: "power_ax(L)"
    2.35 +apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
    2.36 +apply (rule_tac x="{y \<in> Pow(x). L(y)}" in exI)  
    2.37 +apply (simp add: LPow_in_L, auto)
    2.38 +apply (blast intro: transL) 
    2.39 +done
    2.40 +
    2.41 +subsubsection{*For L to satisfy Replacement *}
    2.42 +
    2.43 +(*Can't move these to Formula unless the definition of univalent is moved
    2.44 +there too!*)
    2.45 +
    2.46 +lemma LReplace_in_Lset:
    2.47 +     "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|] 
    2.48 +      ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
    2.49 +apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
    2.50 +       in exI)
    2.51 +apply simp
    2.52 +apply clarify 
    2.53 +apply (rule_tac a="x" in UN_I)  
    2.54 + apply (simp_all add: Replace_iff univalent_def) 
    2.55 +apply (blast dest: transL L_I) 
    2.56 +done
    2.57 +
    2.58 +lemma LReplace_in_L: 
    2.59 +     "[|L(X); univalent(L,X,Q)|] 
    2.60 +      ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
    2.61 +apply (drule L_D, clarify) 
    2.62 +apply (drule LReplace_in_Lset, assumption+)
    2.63 +apply (blast intro: L_I Lset_in_Lset_succ)
    2.64 +done
    2.65 +
    2.66 +lemma replacement: "replacement(L,P)"
    2.67 +apply (simp add: replacement_def, clarify)
    2.68 +apply (frule LReplace_in_L, assumption+)
    2.69 +apply clarify 
    2.70 +apply (rule_tac x=Y in exI)   
    2.71 +apply (simp add: Replace_iff univalent_def, blast) 
    2.72 +done
    2.73 +
    2.74 +end
    2.75 +
    2.76 +(*
    2.77 +
    2.78 +  and Inter_separation:
    2.79 +     "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
    2.80 +  and cartprod_separation:
    2.81 +     "[| L(A); L(B) |] 
    2.82 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
    2.83 +  and image_separation:
    2.84 +     "[| L(A); L(r) |] 
    2.85 +      ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
    2.86 +  and vimage_separation:
    2.87 +     "[| L(A); L(r) |] 
    2.88 +      ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
    2.89 +  and converse_separation:
    2.90 +     "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) & 
    2.91 +				     pair(M,x,y,p) & pair(M,y,x,z)))"
    2.92 +  and restrict_separation:
    2.93 +     "L(A) 
    2.94 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
    2.95 +  and comp_separation:
    2.96 +     "[| L(r); L(s) |]
    2.97 +      ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
    2.98 +			   (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) & 
    2.99 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
   2.100 +  and pred_separation:
   2.101 +     "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
   2.102 +  and Memrel_separation:
   2.103 +     "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
   2.104 +  and obase_separation:
   2.105 +     --{*part of the order type formalization*}
   2.106 +     "[| L(A); L(r) |] 
   2.107 +      ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) & 
   2.108 +	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   2.109 +	     order_isomorphism(M,par,r,x,mx,g))"
   2.110 +  and well_ord_iso_separation:
   2.111 +     "[| L(A); L(f); L(r) |] 
   2.112 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and> 
   2.113 +		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
   2.114 +  and obase_equals_separation:
   2.115 +     "[| L(A); L(r) |] 
   2.116 +      ==> separation
   2.117 +      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
   2.118 +	      ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
   2.119 +	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   2.120 +	      order_isomorphism(M,pxr,r,y,my,g)))))"
   2.121 +  and is_recfun_separation:
   2.122 +     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
   2.123 +     "[| L(A); L(f); L(g); L(a); L(b) |] 
   2.124 +     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
   2.125 +  and omap_replacement:
   2.126 +     "[| L(A); L(r) |] 
   2.127 +      ==> strong_replacement(M,
   2.128 +             \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
   2.129 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   2.130 +	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   2.131 +
   2.132 +*)
   2.133 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Constructible/Normal.thy	Wed Jun 19 11:48:01 2002 +0200
     3.3 @@ -0,0 +1,457 @@
     3.4 +header {*Closed Unbounded Classes and Normal Functions*}
     3.5 +
     3.6 +theory Normal = Main:
     3.7 +
     3.8 +text{*
     3.9 +One source is the book
    3.10 +
    3.11 +Frank R. Drake.
    3.12 +\emph{Set Theory: An Introduction to Large Cardinals}.
    3.13 +North-Holland, 1974.
    3.14 +*}
    3.15 +
    3.16 +
    3.17 +subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
    3.18 +
    3.19 +constdefs
    3.20 +  Closed :: "(i=>o) => o"
    3.21 +    "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
    3.22 +
    3.23 +  Unbounded :: "(i=>o) => o"
    3.24 +    "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
    3.25 +
    3.26 +  Closed_Unbounded :: "(i=>o) => o"
    3.27 +    "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
    3.28 +
    3.29 +
    3.30 +subsubsection{*Simple facts about c.u. classes*}
    3.31 +
    3.32 +lemma ClosedI:
    3.33 +     "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |] 
    3.34 +      ==> Closed(P)"
    3.35 +by (simp add: Closed_def)
    3.36 +
    3.37 +lemma ClosedD:
    3.38 +     "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |] 
    3.39 +      ==> P(\<Union>(I))"
    3.40 +by (simp add: Closed_def)
    3.41 +
    3.42 +lemma UnboundedD:
    3.43 +     "[| Unbounded(P);  Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"
    3.44 +by (simp add: Unbounded_def)
    3.45 +
    3.46 +lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"
    3.47 +by (simp add: Closed_Unbounded_def) 
    3.48 +
    3.49 +
    3.50 +text{*The universal class, V, is closed and unbounded.
    3.51 +      A bit odd, since C. U. concerns only ordinals, but it's used below!*}
    3.52 +theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"
    3.53 +by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
    3.54 +
    3.55 +text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}
    3.56 +theorem Closed_Unbounded_Ord   [simp]: "Closed_Unbounded(Ord)"
    3.57 +by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
    3.58 +
    3.59 +text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}
    3.60 +theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
    3.61 +apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union, 
    3.62 +       clarify)
    3.63 +apply (rule_tac x="i++nat" in exI)  
    3.64 +apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0) 
    3.65 +done
    3.66 +
    3.67 +text{*The class of cardinals, @{term Card}, is closed and unbounded.*}
    3.68 +theorem Closed_Unbounded_Card  [simp]: "Closed_Unbounded(Card)"
    3.69 +apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
    3.70 +apply (blast intro: lt_csucc Card_csucc)
    3.71 +done
    3.72 +
    3.73 +
    3.74 +subsubsection{*The intersection of any set-indexed family of c.u. classes is
    3.75 +      c.u.*}
    3.76 +
    3.77 +text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
    3.78 +locale cub_family =
    3.79 +  fixes P and A
    3.80 +  fixes next_greater -- "the next ordinal satisfying class @{term A}"
    3.81 +  fixes sup_greater  -- "sup of those ordinals over all @{term A}"
    3.82 +  assumes closed:    "a\<in>A ==> Closed(P(a))"
    3.83 +      and unbounded: "a\<in>A ==> Unbounded(P(a))"
    3.84 +      and A_non0: "A\<noteq>0"
    3.85 +  defines "next_greater(a,x) == \<mu>y. x<y \<and> P(a,y)"
    3.86 +      and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
    3.87 + 
    3.88 +
    3.89 +text{*Trivial that the intersection is closed.*}
    3.90 +lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"
    3.91 +by (blast intro: ClosedI ClosedD [OF closed])
    3.92 +
    3.93 +text{*All remaining effort goes to show that the intersection is unbounded.*}
    3.94 +
    3.95 +lemma (in cub_family) Ord_sup_greater:
    3.96 +     "Ord(sup_greater(x))"
    3.97 +by (simp add: sup_greater_def next_greater_def)
    3.98 +
    3.99 +lemma (in cub_family) Ord_next_greater:
   3.100 +     "Ord(next_greater(a,x))"
   3.101 +by (simp add: next_greater_def Ord_Least)
   3.102 +
   3.103 +text{*@{term next_greater} works as expected: it returns a larger value
   3.104 +and one that belongs to class @{term "P(a)"}. *}
   3.105 +lemma (in cub_family) next_greater_lemma:
   3.106 +     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"
   3.107 +apply (simp add: next_greater_def)
   3.108 +apply (rule exE [OF UnboundedD [OF unbounded]])
   3.109 +  apply assumption+
   3.110 +apply (blast intro: LeastI2 lt_Ord2) 
   3.111 +done
   3.112 +
   3.113 +lemma (in cub_family) next_greater_in_P:
   3.114 +     "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"
   3.115 +by (blast dest: next_greater_lemma)
   3.116 +
   3.117 +lemma (in cub_family) next_greater_gt:
   3.118 +     "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"
   3.119 +by (blast dest: next_greater_lemma)
   3.120 +
   3.121 +lemma (in cub_family) sup_greater_gt:
   3.122 +     "Ord(x) ==> x < sup_greater(x)"
   3.123 +apply (simp add: sup_greater_def)
   3.124 +apply (insert A_non0)
   3.125 +apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
   3.126 +done
   3.127 +
   3.128 +lemma (in cub_family) next_greater_le_sup_greater:
   3.129 +     "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"
   3.130 +apply (simp add: sup_greater_def) 
   3.131 +apply (blast intro: UN_upper_le Ord_next_greater)
   3.132 +done
   3.133 +
   3.134 +lemma (in cub_family) omega_sup_greater_eq_UN:
   3.135 +     "[| Ord(x); a\<in>A |] 
   3.136 +      ==> sup_greater^\<omega> (x) = 
   3.137 +          (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"
   3.138 +apply (simp add: iterates_omega_def)
   3.139 +apply (rule le_anti_sym)
   3.140 +apply (rule le_implies_UN_le_UN) 
   3.141 +apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)  
   3.142 +txt{*Opposite bound:
   3.143 +@{subgoals[display,indent=0,margin=65]}
   3.144 +*}
   3.145 +apply (rule UN_least_le) 
   3.146 +apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
   3.147 +apply (rule_tac a="succ(n)" in UN_upper_le)
   3.148 +apply (simp_all add: next_greater_le_sup_greater) 
   3.149 +apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)  
   3.150 +done
   3.151 +
   3.152 +lemma (in cub_family) P_omega_sup_greater:
   3.153 +     "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"
   3.154 +apply (simp add: omega_sup_greater_eq_UN)
   3.155 +apply (rule ClosedD [OF closed]) 
   3.156 +apply (blast intro: ltD, auto)
   3.157 +apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
   3.158 +apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
   3.159 +done
   3.160 +
   3.161 +lemma (in cub_family) omega_sup_greater_gt:
   3.162 +     "Ord(x) ==> x < sup_greater^\<omega> (x)"
   3.163 +apply (simp add: iterates_omega_def)
   3.164 +apply (rule UN_upper_lt [of 1], simp_all) 
   3.165 + apply (blast intro: sup_greater_gt) 
   3.166 +apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
   3.167 +done
   3.168 +
   3.169 +lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
   3.170 +apply (unfold Unbounded_def)  
   3.171 +apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater) 
   3.172 +done
   3.173 +
   3.174 +lemma (in cub_family) Closed_Unbounded_INT: 
   3.175 +     "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
   3.176 +by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
   3.177 +
   3.178 +
   3.179 +theorem Closed_Unbounded_INT:
   3.180 +    "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
   3.181 +     ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
   3.182 +apply (case_tac "A=0", simp)
   3.183 +apply (rule cub_family.Closed_Unbounded_INT)
   3.184 +apply (simp_all add: Closed_Unbounded_def)
   3.185 +done
   3.186 +
   3.187 +lemma Int_iff_INT2:
   3.188 +     "P(x) \<and> Q(x)  <->  (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"
   3.189 +by auto
   3.190 +
   3.191 +theorem Closed_Unbounded_Int:
   3.192 +     "[| Closed_Unbounded(P); Closed_Unbounded(Q) |] 
   3.193 +      ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
   3.194 +apply (simp only: Int_iff_INT2)
   3.195 +apply (rule Closed_Unbounded_INT, auto) 
   3.196 +done
   3.197 +
   3.198 +
   3.199 +subsection {*Normal Functions*} 
   3.200 +
   3.201 +constdefs
   3.202 +  mono_le_subset :: "(i=>i) => o"
   3.203 +    "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
   3.204 +
   3.205 +  mono_Ord :: "(i=>i) => o"
   3.206 +    "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
   3.207 +
   3.208 +  cont_Ord :: "(i=>i) => o"
   3.209 +    "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
   3.210 +
   3.211 +  Normal :: "(i=>i) => o"
   3.212 +    "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
   3.213 +
   3.214 +
   3.215 +subsubsection{*Immediate properties of the definitions*}
   3.216 +
   3.217 +lemma NormalI:
   3.218 +     "[|!!i j. i<j ==> F(i) < F(j);  !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]
   3.219 +      ==> Normal(F)"
   3.220 +by (simp add: Normal_def mono_Ord_def cont_Ord_def)
   3.221 +
   3.222 +lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
   3.223 +apply (simp add: mono_Ord_def) 
   3.224 +apply (blast intro: lt_Ord) 
   3.225 +done
   3.226 +
   3.227 +lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"
   3.228 +by (simp add: mono_Ord_def)
   3.229 +
   3.230 +lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"
   3.231 +by (simp add: Normal_def mono_Ord_imp_Ord) 
   3.232 +
   3.233 +lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"
   3.234 +by (simp add: Normal_def cont_Ord_def)
   3.235 +
   3.236 +lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
   3.237 +by (simp add: Normal_def mono_Ord_def)
   3.238 +
   3.239 +lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
   3.240 +apply (induct i rule: trans_induct3_rule)
   3.241 +  apply (simp add: subset_imp_le)
   3.242 + apply (subgoal_tac "F(x) < F(succ(x))")
   3.243 +  apply (force intro: lt_trans1)
   3.244 + apply (simp add: Normal_def mono_Ord_def)
   3.245 +apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
   3.246 + apply (simp add: Normal_imp_cont Limit_OUN_eq) 
   3.247 +apply (blast intro: ltD le_implies_OUN_le_OUN)
   3.248 +done
   3.249 +
   3.250 +
   3.251 +subsubsection{*The class of fixedpoints is closed and unbounded*}
   3.252 +
   3.253 +text{*The proof is from Drake, pages 113--114.*}
   3.254 +
   3.255 +lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"
   3.256 +apply (simp add: mono_le_subset_def, clarify)
   3.257 +apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset) 
   3.258 +apply (simp add: le_iff) 
   3.259 +apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono) 
   3.260 +done
   3.261 +
   3.262 +text{*The following equation is taken for granted in any set theory text.*}
   3.263 +lemma cont_Ord_Union:
   3.264 +     "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |] 
   3.265 +      ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
   3.266 +apply (frule Ord_set_cases)
   3.267 +apply (erule disjE, force) 
   3.268 +apply (thin_tac "X=0 --> ?Q", auto)
   3.269 + txt{*The trival case of @{term "\<Union>X \<in> X"}*}
   3.270 + apply (rule equalityI, blast intro: Ord_Union_eq_succD) 
   3.271 + apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff) 
   3.272 + apply (blast elim: equalityE)
   3.273 +txt{*The limit case, @{term "Limit(\<Union>X)"}:
   3.274 +@{subgoals[display,indent=0,margin=65]}
   3.275 +*}
   3.276 +apply (simp add: OUN_Union_eq cont_Ord_def)
   3.277 +apply (rule equalityI) 
   3.278 +txt{*First inclusion:*}
   3.279 + apply (rule UN_least [OF OUN_least])
   3.280 + apply (simp add: mono_le_subset_def, blast intro: leI) 
   3.281 +txt{*Second inclusion:*}
   3.282 +apply (rule UN_least) 
   3.283 +apply (frule Union_upper_le, blast, blast intro: Ord_Union)
   3.284 +apply (erule leE, drule ltD, elim UnionE)
   3.285 + apply (simp add: OUnion_def)
   3.286 + apply blast+
   3.287 +done
   3.288 +
   3.289 +lemma Normal_Union:
   3.290 +     "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
   3.291 +apply (simp add: Normal_def) 
   3.292 +apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union) 
   3.293 +done
   3.294 +
   3.295 +lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"
   3.296 +apply (simp add: Closed_def ball_conj_distrib, clarify)
   3.297 +apply (frule Ord_set_cases)
   3.298 +apply (auto simp add: Normal_Union)
   3.299 +done
   3.300 +
   3.301 +
   3.302 +lemma iterates_Normal_increasing:
   3.303 +     "[| n\<in>nat;  x < F(x);  Normal(F) |] 
   3.304 +      ==> F^n (x) < F^(succ(n)) (x)"  
   3.305 +apply (induct n rule: nat_induct)
   3.306 +apply (simp_all add: Normal_imp_mono)
   3.307 +done
   3.308 +
   3.309 +lemma Ord_iterates_Normal:
   3.310 +     "[| n\<in>nat;  Normal(F);  Ord(x) |] ==> Ord(F^n (x))"  
   3.311 +by (simp add: Ord_iterates) 
   3.312 +
   3.313 +text{*THIS RESULT IS UNUSED*}
   3.314 +lemma iterates_omega_Limit:
   3.315 +     "[| Normal(F);  x < F(x) |] ==> Limit(F^\<omega> (x))"  
   3.316 +apply (frule lt_Ord) 
   3.317 +apply (simp add: iterates_omega_def)
   3.318 +apply (rule increasing_LimitI) 
   3.319 +   --"this lemma is @{thm increasing_LimitI [no_vars]}"
   3.320 + apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
   3.321 +                     Ord_UN Ord_iterates lt_imp_0_lt
   3.322 +                     iterates_Normal_increasing)
   3.323 +apply clarify
   3.324 +apply (rule bexI) 
   3.325 + apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
   3.326 +apply (rule UN_I, erule nat_succI) 
   3.327 +apply (blast intro:  iterates_Normal_increasing Ord_iterates_Normal
   3.328 +                     ltD [OF lt_trans1, OF succ_leI, OF ltI]) 
   3.329 +done
   3.330 +
   3.331 +lemma iterates_omega_fixedpoint:
   3.332 +     "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)" 
   3.333 +apply (frule Normal_increasing, assumption)
   3.334 +apply (erule leE) 
   3.335 + apply (simp_all add: iterates_omega_triv [OF sym])  (*for subgoal 2*)
   3.336 +apply (simp add:  iterates_omega_def Normal_Union) 
   3.337 +apply (rule equalityI, force simp add: nat_succI) 
   3.338 +txt{*Opposite inclusion:
   3.339 +@{subgoals[display,indent=0,margin=65]}
   3.340 +*}
   3.341 +apply clarify
   3.342 +apply (rule UN_I, assumption) 
   3.343 +apply (frule iterates_Normal_increasing, assumption, assumption, simp)
   3.344 +apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F]) 
   3.345 +done
   3.346 +
   3.347 +lemma iterates_omega_increasing:
   3.348 +     "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"   
   3.349 +apply (unfold iterates_omega_def)
   3.350 +apply (rule UN_upper_le [of 0], simp_all)
   3.351 +done
   3.352 +
   3.353 +lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"
   3.354 +apply (unfold Unbounded_def, clarify)
   3.355 +apply (rule_tac x="F^\<omega> (succ(i))" in exI)
   3.356 +apply (simp add: iterates_omega_fixedpoint) 
   3.357 +apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
   3.358 +done
   3.359 +
   3.360 +
   3.361 +theorem Normal_imp_fp_Closed_Unbounded: 
   3.362 +     "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"
   3.363 +by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed
   3.364 +              Normal_imp_fp_Unbounded)
   3.365 +
   3.366 +
   3.367 +subsubsection{*Function @{text normalize}*}
   3.368 +
   3.369 +text{*Function @{text normalize} maps a function @{text F} to a 
   3.370 +      normal function that bounds it above.  The result is normal if and
   3.371 +      only if @{text F} is continuous: succ is not bounded above by any 
   3.372 +      normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
   3.373 +*}
   3.374 +constdefs
   3.375 +  normalize :: "[i=>i, i] => i"
   3.376 +    "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
   3.377 +
   3.378 +
   3.379 +lemma Ord_normalize [simp, intro]:
   3.380 +     "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
   3.381 +apply (induct a rule: trans_induct3_rule)
   3.382 +apply (simp_all add: ltD def_transrec2 [OF normalize_def])
   3.383 +done
   3.384 +
   3.385 +lemma normalize_lemma [rule_format]:
   3.386 +     "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |] 
   3.387 +      ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"
   3.388 +apply (erule trans_induct3)
   3.389 +  apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
   3.390 + apply clarify
   3.391 +apply (rule Un_upper2_lt) 
   3.392 +  apply auto
   3.393 + apply (drule spec, drule mp, assumption) 
   3.394 + apply (erule leI) 
   3.395 +apply (drule Limit_has_succ, assumption)
   3.396 +apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
   3.397 +done  
   3.398 +
   3.399 +lemma normalize_increasing:
   3.400 +     "[| a < b;  !!x. Ord(x) ==> Ord(F(x)) |] 
   3.401 +      ==> normalize(F, a) < normalize(F, b)"
   3.402 +by (blast intro!: normalize_lemma intro: lt_Ord2) 
   3.403 +
   3.404 +theorem Normal_normalize:
   3.405 +     "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
   3.406 +apply (rule NormalI) 
   3.407 +apply (blast intro!: normalize_increasing)
   3.408 +apply (simp add: def_transrec2 [OF normalize_def])
   3.409 +done
   3.410 +
   3.411 +theorem le_normalize:
   3.412 +     "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |] 
   3.413 +      ==> F(a) \<le> normalize(F,a)"
   3.414 +apply (erule trans_induct3) 
   3.415 +apply (simp_all add: def_transrec2 [OF normalize_def])
   3.416 +apply (simp add: Un_upper1_le) 
   3.417 +apply (simp add: cont_Ord_def) 
   3.418 +apply (blast intro: ltD le_implies_OUN_le_OUN)
   3.419 +done
   3.420 +
   3.421 +
   3.422 +subsection {*The Alephs*}
   3.423 +text {*This is the well-known transfinite enumeration of the cardinal 
   3.424 +numbers.*}
   3.425 +
   3.426 +constdefs
   3.427 +  Aleph :: "i => i"
   3.428 +    "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
   3.429 +
   3.430 +syntax (xsymbols)
   3.431 +  Aleph :: "i => i"   ("\<aleph>_" [90] 90)
   3.432 +
   3.433 +lemma Card_Aleph [simp, intro]:
   3.434 +     "Ord(a) ==> Card(Aleph(a))"
   3.435 +apply (erule trans_induct3) 
   3.436 +apply (simp_all add: Card_csucc Card_nat Card_is_Ord
   3.437 +                     def_transrec2 [OF Aleph_def])
   3.438 +done
   3.439 +
   3.440 +lemma Aleph_lemma [rule_format]:
   3.441 +     "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"
   3.442 +apply (erule trans_induct3) 
   3.443 +apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])  
   3.444 +apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
   3.445 +apply (drule Limit_has_succ, assumption)
   3.446 +apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
   3.447 +done  
   3.448 +
   3.449 +lemma Aleph_increasing:
   3.450 +     "a < b ==> Aleph(a) < Aleph(b)"
   3.451 +by (blast intro!: Aleph_lemma intro: lt_Ord2) 
   3.452 +
   3.453 +theorem Normal_Aleph: "Normal(Aleph)"
   3.454 +apply (rule NormalI) 
   3.455 +apply (blast intro!: Aleph_increasing)
   3.456 +apply (simp add: def_transrec2 [OF Aleph_def])
   3.457 +done
   3.458 +
   3.459 +end
   3.460 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/Constructible/ROOT.ML	Wed Jun 19 11:48:01 2002 +0200
     4.3 @@ -0,0 +1,4 @@
     4.4 +use_thy "Reflection";
     4.5 +use_thy "WFrec";
     4.6 +use_thy "WF_extras";
     4.7 +use_thy "L_axioms";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/ZF/Constructible/Reflection.thy	Wed Jun 19 11:48:01 2002 +0200
     5.3 @@ -0,0 +1,321 @@
     5.4 +header {* The Reflection Theorem*}
     5.5 +
     5.6 +theory Reflection = Normal:
     5.7 +
     5.8 +lemma all_iff_not_ex_not: "(\<forall>x. P(x)) <-> (~ (\<exists>x. ~ P(x)))";
     5.9 +by blast
    5.10 +
    5.11 +lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) <-> (~ (\<exists>x\<in>A. ~ P(x)))";
    5.12 +by blast
    5.13 +
    5.14 +text{*From the notes of A. S. Kechris, page 6, and from 
    5.15 +      Andrzej Mostowski, \emph{Constructible Sets with Applications},
    5.16 +      North-Holland, 1969, page 23.*}
    5.17 +
    5.18 +
    5.19 +subsection{*Basic Definitions*}
    5.20 +
    5.21 +text{*First part: the cumulative hierarchy defining the class @{text M}.  
    5.22 +To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
    5.23 +closed under ordered pairing provided @{text l} is limit.  Possibly this
    5.24 +could be avoided: the induction hypothesis @{term Cl_reflects} 
    5.25 +(in locale @{text ex_reflection}) could be weakened to
    5.26 +@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
    5.27 +uses of @{term Pair_in_Mset}.  But there isn't much point in doing so, since 
    5.28 +ultimately the @{text ex_reflection} proof is packaged up using the
    5.29 +predicate @{text Reflects}.
    5.30 +*}
    5.31 +locale reflection =
    5.32 +  fixes Mset and M and Reflects
    5.33 +  assumes Mset_mono_le : "mono_le_subset(Mset)"
    5.34 +      and Mset_cont    : "cont_Ord(Mset)"
    5.35 +      and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] 
    5.36 +                          ==> <x,y> \<in> Mset(a)"
    5.37 +  defines "M(x) == \<exists>a. Ord(a) \<and> x \<in> Mset(a)"
    5.38 +      and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) \<and>
    5.39 +                              (\<forall>a. Cl(a) --> (\<forall>x\<in>Mset(a). P(x) <-> Q(a,x)))"
    5.40 +  fixes F0 --{*ordinal for a specific value @{term y}*}
    5.41 +  fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
    5.42 +  fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
    5.43 +  defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) \<and> P(<y,z>)) --> 
    5.44 +                               (\<exists>z\<in>Mset(b). P(<y,z>))"
    5.45 +      and "FF(P)   == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
    5.46 +      and "ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(FF(P),a) = a"
    5.47 +
    5.48 +lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) <= Mset(j)"
    5.49 +apply (insert Mset_mono_le) 
    5.50 +apply (simp add: mono_le_subset_def leI) 
    5.51 +done
    5.52 +
    5.53 +subsection{*Easy Cases of the Reflection Theorem*}
    5.54 +
    5.55 +theorem (in reflection) Triv_reflection [intro]:
    5.56 +     "Reflects(Ord, P, \<lambda>a x. P(x))"
    5.57 +by (simp add: Reflects_def)
    5.58 +
    5.59 +theorem (in reflection) Not_reflection [intro]:
    5.60 +     "Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
    5.61 +by (simp add: Reflects_def); 
    5.62 +
    5.63 +theorem (in reflection) And_reflection [intro]:
    5.64 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    5.65 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
    5.66 +                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
    5.67 +by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    5.68 +
    5.69 +theorem (in reflection) Or_reflection [intro]:
    5.70 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    5.71 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
    5.72 +                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
    5.73 +by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    5.74 +
    5.75 +theorem (in reflection) Imp_reflection [intro]:
    5.76 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    5.77 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
    5.78 +                   \<lambda>x. P(x) --> P'(x), 
    5.79 +                   \<lambda>a x. Q(a,x) --> Q'(a,x))"
    5.80 +by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    5.81 +
    5.82 +theorem (in reflection) Iff_reflection [intro]:
    5.83 +     "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    5.84 +      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
    5.85 +                   \<lambda>x. P(x) <-> P'(x), 
    5.86 +                   \<lambda>a x. Q(a,x) <-> Q'(a,x))"
    5.87 +by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
    5.88 +
    5.89 +subsection{*Reflection for Existential Quantifiers*}
    5.90 +
    5.91 +lemma (in reflection) F0_works:
    5.92 +     "[| y\<in>Mset(a); Ord(a); M(z); P(<y,z>) |] ==> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
    5.93 +apply (unfold F0_def M_def, clarify)
    5.94 +apply (rule LeastI2)
    5.95 +  apply (blast intro: Mset_mono [THEN subsetD])
    5.96 + apply (blast intro: lt_Ord2, blast)
    5.97 +done
    5.98 +
    5.99 +lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))"
   5.100 +by (simp add: F0_def)
   5.101 +
   5.102 +lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))"
   5.103 +by (simp add: FF_def)
   5.104 +
   5.105 +lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))"
   5.106 +apply (insert Mset_cont)
   5.107 +apply (simp add: cont_Ord_def FF_def, blast)
   5.108 +done
   5.109 +
   5.110 +text{*Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"}, 
   5.111 +while @{term FF} depends only upon @{term a}. *}
   5.112 +lemma (in reflection) FF_works:
   5.113 +     "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
   5.114 +apply (simp add: FF_def)
   5.115 +apply (simp_all add: cont_Ord_Union [of concl: Mset] 
   5.116 +                     Mset_cont Mset_mono_le not_emptyI Ord_F0)
   5.117 +apply (blast intro: F0_works)  
   5.118 +done
   5.119 +
   5.120 +lemma (in reflection) FFN_works:
   5.121 +     "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] 
   5.122 +      ==> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)"
   5.123 +apply (drule FF_works [of concl: P], assumption+) 
   5.124 +apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
   5.125 +done
   5.126 +
   5.127 +
   5.128 +text{*Locale for the induction hypothesis*}
   5.129 +
   5.130 +locale ex_reflection = reflection +
   5.131 +  fixes P  --"the original formula"
   5.132 +  fixes Q  --"the reflected formula"
   5.133 +  fixes Cl --"the class of reflecting ordinals"
   5.134 +  assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)"
   5.135 +
   5.136 +lemma (in ex_reflection) ClEx_downward:
   5.137 +     "[| M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a) |] 
   5.138 +      ==> \<exists>z\<in>Mset(a). Q(a,<y,z>)"
   5.139 +apply (simp add: ClEx_def, clarify) 
   5.140 +apply (frule Limit_is_Ord) 
   5.141 +apply (frule FFN_works [of concl: P], assumption+) 
   5.142 +apply (drule Cl_reflects, assumption+) 
   5.143 +apply (auto simp add: Limit_is_Ord Pair_in_Mset)
   5.144 +done
   5.145 +
   5.146 +lemma (in ex_reflection) ClEx_upward:
   5.147 +     "[| z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |] 
   5.148 +      ==> \<exists>z. M(z) \<and> P(<y,z>)"
   5.149 +apply (simp add: ClEx_def M_def)
   5.150 +apply (blast dest: Cl_reflects
   5.151 +	     intro: Limit_is_Ord Pair_in_Mset)
   5.152 +done
   5.153 +
   5.154 +text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
   5.155 +lemma (in ex_reflection) ZF_ClEx_iff:
   5.156 +     "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |] 
   5.157 +      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
   5.158 +by (blast intro: dest: ClEx_downward ClEx_upward) 
   5.159 +
   5.160 +text{*...and it is closed and unbounded*}
   5.161 +lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx:
   5.162 +     "Closed_Unbounded(ClEx(P))"
   5.163 +apply (simp add: ClEx_def)
   5.164 +apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded
   5.165 +                   Closed_Unbounded_Limit Normal_normalize)
   5.166 +done
   5.167 +
   5.168 +text{*The same two theorems, exported to locale @{text reflection}.*}
   5.169 +
   5.170 +text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
   5.171 +lemma (in reflection) ClEx_iff:
   5.172 +     "[| y\<in>Mset(a); Cl(a); ClEx(P,a);
   5.173 +        !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |] 
   5.174 +      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
   5.175 +apply (unfold ClEx_def FF_def F0_def M_def)
   5.176 +apply (rule Reflection.ZF_ClEx_iff [of Mset Cl], 
   5.177 +       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
   5.178 +done
   5.179 +
   5.180 +lemma (in reflection) Closed_Unbounded_ClEx:
   5.181 +     "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x))
   5.182 +      ==> Closed_Unbounded(ClEx(P))"
   5.183 +apply (unfold ClEx_def FF_def F0_def M_def)
   5.184 +apply (rule Reflection.ZF_Closed_Unbounded_ClEx, 
   5.185 +       simp_all add: Mset_mono_le Mset_cont Pair_in_Mset) 
   5.186 +done
   5.187 +
   5.188 +lemma (in reflection) Ex_reflection_0:
   5.189 +     "Reflects(Cl,P0,Q0) 
   5.190 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a), 
   5.191 +                   \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>), 
   5.192 +                   \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))" 
   5.193 +apply (simp add: Reflects_def) 
   5.194 +apply (intro conjI Closed_Unbounded_Int)
   5.195 +  apply blast 
   5.196 + apply (rule reflection.Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify) 
   5.197 +apply (rule_tac Cl=Cl in  ClEx_iff, assumption+, blast) 
   5.198 +done
   5.199 +
   5.200 +lemma (in reflection) All_reflection_0:
   5.201 +     "Reflects(Cl,P0,Q0) 
   5.202 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x.~P0(x), a), 
   5.203 +                   \<lambda>x. \<forall>z. M(z) --> P0(<x,z>), 
   5.204 +                   \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))" 
   5.205 +apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not) 
   5.206 +apply (rule Not_reflection, drule Not_reflection, simp) 
   5.207 +apply (erule Ex_reflection_0)
   5.208 +done
   5.209 +
   5.210 +theorem (in reflection) Ex_reflection [intro]:
   5.211 +     "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
   5.212 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   5.213 +                   \<lambda>x. \<exists>z. M(z) \<and> P(x,z), 
   5.214 +                   \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
   5.215 +by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))" 
   5.216 +                               "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
   5.217 +
   5.218 +theorem (in reflection) All_reflection [intro]:
   5.219 +     "Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
   5.220 +      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   5.221 +                   \<lambda>x. \<forall>z. M(z) --> P(x,z), 
   5.222 +                   \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 
   5.223 +by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" 
   5.224 +                                "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
   5.225 +
   5.226 +text{*No point considering bounded quantifiers, where reflection is trivial.*}
   5.227 +
   5.228 +
   5.229 +subsection{*Simple Examples of Reflection*}
   5.230 +
   5.231 +text{*Example 1: reflecting a simple formula.  The reflecting class is first
   5.232 +given as the variable @{text ?Cl} and later retrieved from the final 
   5.233 +proof state.*}
   5.234 +lemma (in reflection) 
   5.235 +     "Reflects(?Cl,
   5.236 +               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
   5.237 +               \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
   5.238 +by fast
   5.239 +
   5.240 +text{*Problem here: there needs to be a conjunction (class intersection)
   5.241 +in the class of reflecting ordinals.  The @{term "Ord(a)"} is redundant,
   5.242 +though harmless.*}
   5.243 +lemma (in reflection) 
   5.244 +     "Reflects(\<lambda>a. Ord(a) \<and> ClEx(\<lambda>x. fst(x) \<in> snd(x), a),   
   5.245 +               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
   5.246 +               \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" 
   5.247 +by fast
   5.248 +
   5.249 +
   5.250 +text{*Example 2*}
   5.251 +lemma (in reflection) 
   5.252 +     "Reflects(?Cl,
   5.253 +               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   5.254 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   5.255 +by fast
   5.256 +
   5.257 +text{*Example 2'.  We give the reflecting class explicitly. *}
   5.258 +lemma (in reflection) 
   5.259 +  "Reflects
   5.260 +    (\<lambda>a. (Ord(a) \<and>
   5.261 +          ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) \<and>
   5.262 +          ClEx(\<lambda>x. \<forall>z. M(z) --> z \<subseteq> fst(x) --> z \<in> snd(x), a),
   5.263 +	    \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   5.264 +	    \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   5.265 +by fast
   5.266 +
   5.267 +text{*Example 2''.  We expand the subset relation.*}
   5.268 +lemma (in reflection) 
   5.269 +  "Reflects(?Cl,
   5.270 +        \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
   5.271 +        \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
   5.272 +by fast
   5.273 +
   5.274 +text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
   5.275 +lemma (in reflection) 
   5.276 +     "Reflects(?Cl,
   5.277 +               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   5.278 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   5.279 +apply (rule Ex_reflection) 
   5.280 +txt{*
   5.281 +@{goals[display,indent=0,margin=60]}
   5.282 +*}
   5.283 +apply (rule All_reflection) 
   5.284 +txt{*
   5.285 +@{goals[display,indent=0,margin=60]}
   5.286 +*}
   5.287 +apply (rule Triv_reflection) 
   5.288 +txt{*
   5.289 +@{goals[display,indent=0,margin=60]}
   5.290 +*}
   5.291 +done
   5.292 +
   5.293 +text{*Example 3.  Warning: the following examples make sense only
   5.294 +if @{term P} is quantifier-free, since it is not being relativized.*}
   5.295 +lemma (in reflection) 
   5.296 +     "Reflects(?Cl,
   5.297 +               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<in> y <-> z \<in> x \<and> P(z)), 
   5.298 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x \<and> P(z))"
   5.299 +by fast
   5.300 +
   5.301 +text{*Example 3'*}
   5.302 +lemma (in reflection) 
   5.303 +     "Reflects(?Cl,
   5.304 +               \<lambda>x. \<exists>y. M(y) \<and> y = Collect(x,P),
   5.305 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
   5.306 +by fast
   5.307 +
   5.308 +text{*Example 3''*}
   5.309 +lemma (in reflection) 
   5.310 +     "Reflects(?Cl,
   5.311 +               \<lambda>x. \<exists>y. M(y) \<and> y = Replace(x,P),
   5.312 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
   5.313 +by fast
   5.314 +
   5.315 +text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
   5.316 +to be relativized.*}
   5.317 +lemma (in reflection) 
   5.318 +     "Reflects(?Cl,
   5.319 +               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) \<and> f \<in> (\<Pi>X \<in> A. X)),
   5.320 +               \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
   5.321 +by fast
   5.322 +
   5.323 +end
   5.324 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Jun 19 11:48:01 2002 +0200
     6.3 @@ -0,0 +1,956 @@
     6.4 +header {*Relativization and Absoluteness*}
     6.5 +
     6.6 +theory Relative = Main:
     6.7 +
     6.8 +subsection{* Relativized versions of standard set-theoretic concepts *}
     6.9 +
    6.10 +constdefs
    6.11 +  empty :: "[i=>o,i] => o"
    6.12 +    "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
    6.13 +
    6.14 +  subset :: "[i=>o,i,i] => o"
    6.15 +    "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
    6.16 +
    6.17 +  upair :: "[i=>o,i,i,i] => o"
    6.18 +    "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
    6.19 +
    6.20 +  pair :: "[i=>o,i,i,i] => o"
    6.21 +    "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) & 
    6.22 +                          (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
    6.23 +
    6.24 +  successor :: "[i=>o,i,i] => o"
    6.25 +    "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
    6.26 +
    6.27 +  powerset :: "[i=>o,i,i] => o"
    6.28 +    "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
    6.29 +
    6.30 +  union :: "[i=>o,i,i,i] => o"
    6.31 +    "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
    6.32 +
    6.33 +  inter :: "[i=>o,i,i,i] => o"
    6.34 +    "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
    6.35 +
    6.36 +  setdiff :: "[i=>o,i,i,i] => o"
    6.37 +    "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
    6.38 +
    6.39 +  big_union :: "[i=>o,i,i] => o"
    6.40 +    "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
    6.41 +
    6.42 +  big_inter :: "[i=>o,i,i] => o"
    6.43 +    "big_inter(M,A,z) == 
    6.44 +             (A=0 --> z=0) &
    6.45 +	     (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
    6.46 +
    6.47 +  cartprod :: "[i=>o,i,i,i] => o"
    6.48 +    "cartprod(M,A,B,z) == 
    6.49 +	\<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
    6.50 +
    6.51 +  is_converse :: "[i=>o,i,i] => o"
    6.52 +    "is_converse(M,r,z) == 
    6.53 +	\<forall>x. M(x) --> 
    6.54 +            (x \<in> z <-> 
    6.55 +             (\<exists>w\<in>r. M(w) & 
    6.56 +              (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
    6.57 +
    6.58 +  pre_image :: "[i=>o,i,i,i] => o"
    6.59 +    "pre_image(M,r,A,z) == 
    6.60 +	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"
    6.61 +
    6.62 +  is_domain :: "[i=>o,i,i] => o"
    6.63 +    "is_domain(M,r,z) == 
    6.64 +	\<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"
    6.65 +
    6.66 +  image :: "[i=>o,i,i,i] => o"
    6.67 +    "image(M,r,A,z) == 
    6.68 +        \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"
    6.69 +
    6.70 +  is_range :: "[i=>o,i,i] => o"
    6.71 +    --{*the cleaner 
    6.72 +      @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}
    6.73 +      unfortunately needs an instance of separation in order to prove 
    6.74 +        @{term "M(converse(r))"}.*}
    6.75 +    "is_range(M,r,z) == 
    6.76 +	\<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
    6.77 +
    6.78 +  is_relation :: "[i=>o,i] => o"
    6.79 +    "is_relation(M,r) == 
    6.80 +        (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
    6.81 +
    6.82 +  is_function :: "[i=>o,i] => o"
    6.83 +    "is_function(M,r) == 
    6.84 +	(\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') --> 
    6.85 +                      pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> 
    6.86 +                      y=y')"
    6.87 +
    6.88 +  fun_apply :: "[i=>o,i,i,i] => o"
    6.89 +    "fun_apply(M,f,x,y) == 
    6.90 +	(\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"
    6.91 +
    6.92 +  typed_function :: "[i=>o,i,i,i] => o"
    6.93 +    "typed_function(M,A,B,r) == 
    6.94 +        is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
    6.95 +        (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
    6.96 +
    6.97 +  injection :: "[i=>o,i,i,i] => o"
    6.98 +    "injection(M,A,B,f) == 
    6.99 +	typed_function(M,A,B,f) &
   6.100 +        (\<forall>x x' y p p'. M(x) --> M(x') --> M(y) --> M(p) --> M(p') --> 
   6.101 +                      pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> 
   6.102 +                      x=x')"
   6.103 +
   6.104 +  surjection :: "[i=>o,i,i,i] => o"
   6.105 +    "surjection(M,A,B,f) == 
   6.106 +        typed_function(M,A,B,f) &
   6.107 +        (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"
   6.108 +
   6.109 +  bijection :: "[i=>o,i,i,i] => o"
   6.110 +    "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
   6.111 +
   6.112 +  restriction :: "[i=>o,i,i,i] => o"
   6.113 +    "restriction(M,r,A,z) == 
   6.114 +	\<forall>x. M(x) --> 
   6.115 +            (x \<in> z <-> 
   6.116 +             (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"
   6.117 +
   6.118 +  transitive_set :: "[i=>o,i] => o"
   6.119 +    "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"
   6.120 +
   6.121 +  ordinal :: "[i=>o,i] => o"
   6.122 +     --{*an ordinal is a transitive set of transitive sets*}
   6.123 +    "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"
   6.124 +
   6.125 +  limit_ordinal :: "[i=>o,i] => o"
   6.126 +    --{*a limit ordinal is a non-empty, successor-closed ordinal*}
   6.127 +    "limit_ordinal(M,a) == 
   6.128 +	ordinal(M,a) & ~ empty(M,a) & 
   6.129 +        (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"
   6.130 +
   6.131 +  successor_ordinal :: "[i=>o,i] => o"
   6.132 +    --{*a successor ordinal is any ordinal that is neither empty nor limit*}
   6.133 +    "successor_ordinal(M,a) == 
   6.134 +	ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
   6.135 +
   6.136 +  finite_ordinal :: "[i=>o,i] => o"
   6.137 +    --{*an ordinal is finite if neither it nor any of its elements are limit*}
   6.138 +    "finite_ordinal(M,a) == 
   6.139 +	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   6.140 +        (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
   6.141 +
   6.142 +  omega :: "[i=>o,i] => o"
   6.143 +    --{*omega is a limit ordinal none of whose elements are limit*}
   6.144 +    "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
   6.145 +
   6.146 +  number1 :: "[i=>o,i] => o"
   6.147 +    "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"
   6.148 +
   6.149 +  number2 :: "[i=>o,i] => o"
   6.150 +    "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"
   6.151 +
   6.152 +  number3 :: "[i=>o,i] => o"
   6.153 +    "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"
   6.154 +
   6.155 +
   6.156 +subsection {*The relativized ZF axioms*}
   6.157 +constdefs
   6.158 +
   6.159 +  extensionality :: "(i=>o) => o"
   6.160 +    "extensionality(M) == 
   6.161 +	\<forall>x y. M(x) --> M(y) --> (\<forall>z. M(z) --> (z \<in> x <-> z \<in> y)) --> x=y"
   6.162 +
   6.163 +  separation :: "[i=>o, i=>o] => o"
   6.164 +    --{*Big problem: the formula @{text P} should only involve parameters
   6.165 +        belonging to @{text M}.  Don't see how to enforce that.*}
   6.166 +    "separation(M,P) == 
   6.167 +	\<forall>z. M(z) --> (\<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x))))"
   6.168 +
   6.169 +  upair_ax :: "(i=>o) => o"
   6.170 +    "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"
   6.171 +
   6.172 +  Union_ax :: "(i=>o) => o"
   6.173 +    "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"
   6.174 +
   6.175 +  power_ax :: "(i=>o) => o"
   6.176 +    "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"
   6.177 +
   6.178 +  univalent :: "[i=>o, i, [i,i]=>o] => o"
   6.179 +    "univalent(M,A,P) == 
   6.180 +	(\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
   6.181 +
   6.182 +  replacement :: "[i=>o, [i,i]=>o] => o"
   6.183 +    "replacement(M,P) == 
   6.184 +      \<forall>A. M(A) --> univalent(M,A,P) -->
   6.185 +      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"
   6.186 +
   6.187 +  strong_replacement :: "[i=>o, [i,i]=>o] => o"
   6.188 +    "strong_replacement(M,P) == 
   6.189 +      \<forall>A. M(A) --> univalent(M,A,P) -->
   6.190 +      (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"
   6.191 +
   6.192 +  foundation_ax :: "(i=>o) => o"
   6.193 +    "foundation_ax(M) == 
   6.194 +	\<forall>x. M(x) --> (\<exists>y\<in>x. M(y))
   6.195 +                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"
   6.196 +
   6.197 +
   6.198 +subsection{*A trivial consistency proof for $V_\omega$ *}
   6.199 +
   6.200 +text{*We prove that $V_\omega$ 
   6.201 +      (or @{text univ} in Isabelle) satisfies some ZF axioms.
   6.202 +     Kunen, Theorem IV 3.13, page 123.*}
   6.203 +
   6.204 +lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
   6.205 +apply (insert Transset_univ [OF Transset_0])  
   6.206 +apply (simp add: Transset_def, blast) 
   6.207 +done
   6.208 +
   6.209 +lemma univ0_Ball_abs [simp]: 
   6.210 +     "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   6.211 +by (blast intro: univ0_downwards_mem) 
   6.212 +
   6.213 +lemma univ0_Bex_abs [simp]: 
   6.214 +     "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   6.215 +by (blast intro: univ0_downwards_mem) 
   6.216 +
   6.217 +text{*Congruence rule for separation: can assume the variable is in @{text M}*}
   6.218 +lemma [cong]:
   6.219 +     "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
   6.220 +by (simp add: separation_def) 
   6.221 +
   6.222 +text{*Congruence rules for replacement*}
   6.223 +lemma [cong]:
   6.224 +     "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   6.225 +      ==> univalent(M,A,P) <-> univalent(M,A',P')"
   6.226 +by (simp add: univalent_def) 
   6.227 +
   6.228 +lemma [cong]:
   6.229 +     "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] 
   6.230 +      ==> strong_replacement(M,P) <-> strong_replacement(M,P')" 
   6.231 +by (simp add: strong_replacement_def) 
   6.232 +
   6.233 +text{*The extensionality axiom*}
   6.234 +lemma "extensionality(\<lambda>x. x \<in> univ(0))"
   6.235 +apply (simp add: extensionality_def)
   6.236 +apply (blast intro: univ0_downwards_mem) 
   6.237 +done
   6.238 +
   6.239 +text{*The separation axiom requires some lemmas*}
   6.240 +lemma Collect_in_Vfrom:
   6.241 +     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
   6.242 +apply (drule Transset_Vfrom)
   6.243 +apply (rule subset_mem_Vfrom)
   6.244 +apply (unfold Transset_def, blast)
   6.245 +done
   6.246 +
   6.247 +lemma Collect_in_VLimit:
   6.248 +     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] 
   6.249 +      ==> Collect(X,P) \<in> Vfrom(A,i)"
   6.250 +apply (rule Limit_VfromE, assumption+)
   6.251 +apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
   6.252 +done
   6.253 +
   6.254 +lemma Collect_in_univ:
   6.255 +     "[| X \<in> univ(A);  Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
   6.256 +by (simp add: univ_def Collect_in_VLimit Limit_nat)
   6.257 +
   6.258 +lemma "separation(\<lambda>x. x \<in> univ(0), P)"
   6.259 +apply (simp add: separation_def)
   6.260 +apply (blast intro: Collect_in_univ Transset_0) 
   6.261 +done
   6.262 +
   6.263 +text{*Unordered pairing axiom*}
   6.264 +lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
   6.265 +apply (simp add: upair_ax_def upair_def)  
   6.266 +apply (blast intro: doubleton_in_univ) 
   6.267 +done
   6.268 +
   6.269 +text{*Union axiom*}
   6.270 +lemma "Union_ax(\<lambda>x. x \<in> univ(0))"  
   6.271 +apply (simp add: Union_ax_def big_union_def)  
   6.272 +apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem) 
   6.273 +done
   6.274 +
   6.275 +text{*Powerset axiom*}
   6.276 +
   6.277 +lemma Pow_in_univ:
   6.278 +     "[| X \<in> univ(A);  Transset(A) |] ==> Pow(X) \<in> univ(A)"
   6.279 +apply (simp add: univ_def Pow_in_VLimit Limit_nat)
   6.280 +done
   6.281 +
   6.282 +lemma "power_ax(\<lambda>x. x \<in> univ(0))"  
   6.283 +apply (simp add: power_ax_def powerset_def subset_def)  
   6.284 +apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem) 
   6.285 +done
   6.286 +
   6.287 +text{*Foundation axiom*}
   6.288 +lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"  
   6.289 +apply (simp add: foundation_ax_def, clarify)
   6.290 +apply (cut_tac A=x in foundation, blast) 
   6.291 +done
   6.292 +
   6.293 +lemma "replacement(\<lambda>x. x \<in> univ(0), P)"  
   6.294 +apply (simp add: replacement_def, clarify) 
   6.295 +oops
   6.296 +text{*no idea: maybe prove by induction on the rank of A?*}
   6.297 +
   6.298 +text{*Still missing: Replacement, Choice*}
   6.299 +
   6.300 +subsection{*lemmas needed to reduce some set constructions to instances
   6.301 +      of Separation*}
   6.302 +
   6.303 +lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
   6.304 +apply (rule equalityI, auto) 
   6.305 +apply (simp add: Pair_def, blast) 
   6.306 +done
   6.307 +
   6.308 +lemma vimage_iff_Collect:
   6.309 +     "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
   6.310 +apply (rule equalityI, auto) 
   6.311 +apply (simp add: Pair_def, blast) 
   6.312 +done
   6.313 +
   6.314 +text{*These two lemmas lets us prove @{text domain_closed} and 
   6.315 +      @{text range_closed} without new instances of separation*}
   6.316 +
   6.317 +lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
   6.318 +apply (rule equalityI, auto)
   6.319 +apply (rule vimageI, assumption)
   6.320 +apply (simp add: Pair_def, blast) 
   6.321 +done
   6.322 +
   6.323 +lemma range_eq_image: "range(r) = r `` Union(Union(r))"
   6.324 +apply (rule equalityI, auto)
   6.325 +apply (rule imageI, assumption)
   6.326 +apply (simp add: Pair_def, blast) 
   6.327 +done
   6.328 +
   6.329 +lemma replacementD:
   6.330 +    "[| replacement(M,P); M(A);  univalent(M,A,P) |]
   6.331 +     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"
   6.332 +by (simp add: replacement_def) 
   6.333 +
   6.334 +lemma strong_replacementD:
   6.335 +    "[| strong_replacement(M,P); M(A);  univalent(M,A,P) |]
   6.336 +     ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"
   6.337 +by (simp add: strong_replacement_def) 
   6.338 +
   6.339 +lemma separationD:
   6.340 +    "[| separation(M,P); M(z) |]
   6.341 +     ==> \<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x)))"
   6.342 +by (simp add: separation_def) 
   6.343 +
   6.344 +
   6.345 +text{*More constants, for order types*}
   6.346 +constdefs
   6.347 +
   6.348 +  order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   6.349 +    "order_isomorphism(M,A,r,B,s,f) == 
   6.350 +        bijection(M,A,B,f) & 
   6.351 +        (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>p fx fy q. 
   6.352 +            M(x) --> M(y) --> M(p) --> M(fx) --> M(fy) --> M(q) --> 
   6.353 +            pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> 
   6.354 +            pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))"
   6.355 +
   6.356 +
   6.357 +  pred_set :: "[i=>o,i,i,i,i] => o"
   6.358 +    "pred_set(M,A,x,r,B) == 
   6.359 +	\<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"
   6.360 +
   6.361 +  membership :: "[i=>o,i,i] => o" --{*membership relation*}
   6.362 +    "membership(M,A,r) == 
   6.363 +	\<forall>p. M(p) --> 
   6.364 +             (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"
   6.365 +
   6.366 +
   6.367 +subsection{*Absoluteness for a transitive class model*}
   6.368 +
   6.369 +text{*The class M is assumed to be transitive and to satisfy some
   6.370 +      relativized ZF axioms*}
   6.371 +locale M_axioms =
   6.372 +  fixes M
   6.373 +  assumes transM:           "[| y\<in>x; M(x) |] ==> M(y)"
   6.374 +      and nonempty [simp]:  "M(0)"
   6.375 +      and upair_ax:	    "upair_ax(M)"
   6.376 +      and Union_ax:	    "Union_ax(M)"
   6.377 +      and power_ax:         "power_ax(M)"
   6.378 +      and replacement:      "replacement(M,P)"
   6.379 +  and Inter_separation:
   6.380 +     "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
   6.381 +  and cartprod_separation:
   6.382 +     "[| M(A); M(B) |] 
   6.383 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
   6.384 +  and image_separation:
   6.385 +     "[| M(A); M(r) |] 
   6.386 +      ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"
   6.387 +  and vimage_separation:
   6.388 +     "[| M(A); M(r) |] 
   6.389 +      ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
   6.390 +  and converse_separation:
   6.391 +     "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) & 
   6.392 +				     pair(M,x,y,p) & pair(M,y,x,z)))"
   6.393 +  and restrict_separation:
   6.394 +     "M(A) 
   6.395 +      ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
   6.396 +  and comp_separation:
   6.397 +     "[| M(r); M(s) |]
   6.398 +      ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &
   6.399 +			   (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) & 
   6.400 +		  pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
   6.401 +  and pred_separation:
   6.402 +     "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
   6.403 +  and Memrel_separation:
   6.404 +     "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) \<and> x \<in> y)"
   6.405 +  and obase_separation:
   6.406 +     --{*part of the order type formalization*}
   6.407 +     "[| M(A); M(r) |] 
   6.408 +      ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & 
   6.409 +	     ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
   6.410 +	     order_isomorphism(M,par,r,x,mx,g))"
   6.411 +  and well_ord_iso_separation:
   6.412 +     "[| M(A); M(f); M(r) |] 
   6.413 +      ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) \<and> (\<exists>p. M(p) \<and> 
   6.414 +		     fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
   6.415 +  and obase_equals_separation:
   6.416 +     "[| M(A); M(r) |] 
   6.417 +      ==> separation
   6.418 +      (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &
   6.419 +	      ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &
   6.420 +	      membership(M,y,my) & pred_set(M,A,x,r,pxr) &
   6.421 +	      order_isomorphism(M,pxr,r,y,my,g)))))"
   6.422 +  and is_recfun_separation:
   6.423 +     --{*for well-founded recursion.  NEEDS RELATIVIZATION*}
   6.424 +     "[| M(A); M(f); M(g); M(a); M(b) |] 
   6.425 +     ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
   6.426 +  and omap_replacement:
   6.427 +     "[| M(A); M(r) |] 
   6.428 +      ==> strong_replacement(M,
   6.429 +             \<lambda>a z. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &
   6.430 +	     ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & 
   6.431 +	     pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
   6.432 +
   6.433 +lemma (in M_axioms) Ball_abs [simp]: 
   6.434 +     "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))" 
   6.435 +by (blast intro: transM) 
   6.436 +
   6.437 +lemma (in M_axioms) Bex_abs [simp]: 
   6.438 +     "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))" 
   6.439 +by (blast intro: transM) 
   6.440 +
   6.441 +lemma (in M_axioms) Ball_iff_equiv: 
   6.442 +     "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <-> 
   6.443 +               (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)" 
   6.444 +by (blast intro: transM)
   6.445 +
   6.446 +lemma (in M_axioms) empty_abs [simp]: 
   6.447 +     "M(z) ==> empty(M,z) <-> z=0"
   6.448 +apply (simp add: empty_def)
   6.449 +apply (blast intro: transM) 
   6.450 +done
   6.451 +
   6.452 +lemma (in M_axioms) subset_abs [simp]: 
   6.453 +     "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
   6.454 +apply (simp add: subset_def) 
   6.455 +apply (blast intro: transM) 
   6.456 +done
   6.457 +
   6.458 +lemma (in M_axioms) upair_abs [simp]: 
   6.459 +     "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
   6.460 +apply (simp add: upair_def) 
   6.461 +apply (blast intro: transM) 
   6.462 +done
   6.463 +
   6.464 +lemma (in M_axioms) upair_in_M_iff [iff]:
   6.465 +     "M({a,b}) <-> M(a) & M(b)"
   6.466 +apply (insert upair_ax, simp add: upair_ax_def) 
   6.467 +apply (blast intro: transM) 
   6.468 +done
   6.469 +
   6.470 +lemma (in M_axioms) singleton_in_M_iff [iff]:
   6.471 +     "M({a}) <-> M(a)"
   6.472 +by (insert upair_in_M_iff [of a a], simp) 
   6.473 +
   6.474 +lemma (in M_axioms) pair_abs [simp]: 
   6.475 +     "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
   6.476 +apply (simp add: pair_def ZF.Pair_def)
   6.477 +apply (blast intro: transM) 
   6.478 +done
   6.479 +
   6.480 +lemma (in M_axioms) pair_in_M_iff [iff]:
   6.481 +     "M(<a,b>) <-> M(a) & M(b)"
   6.482 +by (simp add: ZF.Pair_def)
   6.483 +
   6.484 +lemma (in M_axioms) pair_components_in_M:
   6.485 +     "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
   6.486 +apply (simp add: Pair_def)
   6.487 +apply (blast dest: transM) 
   6.488 +done
   6.489 +
   6.490 +lemma (in M_axioms) cartprod_abs [simp]: 
   6.491 +     "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
   6.492 +apply (simp add: cartprod_def)
   6.493 +apply (rule iffI) 
   6.494 +apply (blast intro!: equalityI intro: transM dest!: spec) 
   6.495 +apply (blast dest: transM) 
   6.496 +done
   6.497 +
   6.498 +lemma (in M_axioms) union_abs [simp]: 
   6.499 +     "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
   6.500 +apply (simp add: union_def) 
   6.501 +apply (blast intro: transM) 
   6.502 +done
   6.503 +
   6.504 +lemma (in M_axioms) inter_abs [simp]: 
   6.505 +     "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
   6.506 +apply (simp add: inter_def) 
   6.507 +apply (blast intro: transM) 
   6.508 +done
   6.509 +
   6.510 +lemma (in M_axioms) setdiff_abs [simp]: 
   6.511 +     "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
   6.512 +apply (simp add: setdiff_def) 
   6.513 +apply (blast intro: transM) 
   6.514 +done
   6.515 +
   6.516 +lemma (in M_axioms) Union_abs [simp]: 
   6.517 +     "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
   6.518 +apply (simp add: big_union_def) 
   6.519 +apply (blast intro!: equalityI dest: transM) 
   6.520 +done
   6.521 +
   6.522 +lemma (in M_axioms) Union_closed [intro]:
   6.523 +     "M(A) ==> M(Union(A))"
   6.524 +by (insert Union_ax, simp add: Union_ax_def) 
   6.525 +
   6.526 +lemma (in M_axioms) Un_closed [intro]:
   6.527 +     "[| M(A); M(B) |] ==> M(A Un B)"
   6.528 +by (simp only: Un_eq_Union, blast) 
   6.529 +
   6.530 +lemma (in M_axioms) cons_closed [intro]:
   6.531 +     "[| M(a); M(A) |] ==> M(cons(a,A))"
   6.532 +by (subst cons_eq [symmetric], blast) 
   6.533 +
   6.534 +lemma (in M_axioms) successor_abs [simp]: 
   6.535 +     "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"
   6.536 +by (simp add: successor_def, blast)  
   6.537 +
   6.538 +lemma (in M_axioms) succ_in_M_iff [iff]:
   6.539 +     "M(succ(a)) <-> M(a)"
   6.540 +apply (simp add: succ_def) 
   6.541 +apply (blast intro: transM) 
   6.542 +done
   6.543 +
   6.544 +lemma (in M_axioms) separation_closed [intro]:
   6.545 +     "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
   6.546 +apply (insert separation, simp add: separation_def) 
   6.547 +apply (drule spec [THEN mp], assumption, clarify) 
   6.548 +apply (subgoal_tac "y = Collect(A,P)", blast)
   6.549 +apply (blast dest: transM) 
   6.550 +done
   6.551 +
   6.552 +text{*Probably the premise and conclusion are equivalent*}
   6.553 +lemma (in M_axioms) strong_replacementI [rule_format]:
   6.554 +    "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
   6.555 +     ==> strong_replacement(M,P)"
   6.556 +apply (simp add: strong_replacement_def) 
   6.557 +apply (clarify ); 
   6.558 +apply (frule replacementD [OF replacement]) 
   6.559 +apply assumption
   6.560 +apply (clarify ); 
   6.561 +apply (drule_tac x=A in spec)
   6.562 +apply (clarify );  
   6.563 +apply (drule_tac z=Y in separationD) 
   6.564 +apply assumption; 
   6.565 +apply (clarify ); 
   6.566 +apply (blast dest: transM) 
   6.567 +done
   6.568 +
   6.569 +
   6.570 +(*The last premise expresses that P takes M to M*)
   6.571 +lemma (in M_axioms) strong_replacement_closed [intro]:
   6.572 +     "[| strong_replacement(M,P); M(A); univalent(M,A,P); 
   6.573 +       !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
   6.574 +apply (simp add: strong_replacement_def) 
   6.575 +apply (drule spec [THEN mp], auto) 
   6.576 +apply (subgoal_tac "Replace(A,P) = Y")
   6.577 + apply (simp add: ); 
   6.578 +apply (rule equality_iffI) 
   6.579 +apply (simp add: Replace_iff) 
   6.580 +apply safe;
   6.581 + apply (blast dest: transM) 
   6.582 +apply (frule transM, assumption) 
   6.583 + apply (simp add: univalent_def);
   6.584 + apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
   6.585 + apply (blast dest: transM) 
   6.586 +done
   6.587 +
   6.588 +(*The first premise can't simply be assumed as a schema.
   6.589 +  It is essential to take care when asserting instances of Replacement.
   6.590 +  Let K be a nonconstructible subset of nat and define
   6.591 +  f(x) = x if x:K and f(x)=0 otherwise.  Then RepFun(nat,f) = cons(0,K), a 
   6.592 +  nonconstructible set.  So we cannot assume that M(X) implies M(RepFun(X,f))
   6.593 +  even for f : M -> M.
   6.594 +*)
   6.595 +lemma (in M_axioms) RepFun_closed [intro]:
   6.596 +     "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
   6.597 +      ==> M(RepFun(A,f))"
   6.598 +apply (simp add: RepFun_def) 
   6.599 +apply (rule strong_replacement_closed) 
   6.600 +apply (auto dest: transM  simp add: univalent_def) 
   6.601 +done
   6.602 +
   6.603 +lemma (in M_axioms) converse_abs [simp]: 
   6.604 +     "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
   6.605 +apply (simp add: is_converse_def)
   6.606 +apply (rule iffI)
   6.607 + apply (rule equalityI) 
   6.608 +  apply (blast dest: transM) 
   6.609 + apply (clarify, frule transM, assumption, simp, blast) 
   6.610 +done
   6.611 +
   6.612 +lemma (in M_axioms) image_abs [simp]: 
   6.613 +     "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
   6.614 +apply (simp add: image_def)
   6.615 +apply (rule iffI) 
   6.616 + apply (blast intro!: equalityI dest: transM, blast) 
   6.617 +done
   6.618 +
   6.619 +text{*What about @{text Pow_abs}?  Powerset is NOT absolute!
   6.620 +      This result is one direction of absoluteness.*}
   6.621 +
   6.622 +lemma (in M_axioms) powerset_Pow: 
   6.623 +     "powerset(M, x, Pow(x))"
   6.624 +by (simp add: powerset_def)
   6.625 +
   6.626 +text{*But we can't prove that the powerset in @{text M} includes the
   6.627 +      real powerset.*}
   6.628 +lemma (in M_axioms) powerset_imp_subset_Pow: 
   6.629 +     "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
   6.630 +apply (simp add: powerset_def) 
   6.631 +apply (blast dest: transM) 
   6.632 +done
   6.633 +
   6.634 +lemma (in M_axioms) cartprod_iff_lemma:
   6.635 +     "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}); 
   6.636 +       powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
   6.637 +       ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
   6.638 +apply (simp add: powerset_def) 
   6.639 +apply (rule equalityI, clarify, simp) 
   6.640 + apply (frule transM, assumption, simp) 
   6.641 + apply blast 
   6.642 +apply clarify
   6.643 +apply (frule transM, assumption, force) 
   6.644 +done
   6.645 +
   6.646 +lemma (in M_axioms) cartprod_iff:
   6.647 +     "[| M(A); M(B); M(C) |] 
   6.648 +      ==> cartprod(M,A,B,C) <-> 
   6.649 +          (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
   6.650 +                   C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
   6.651 +apply (simp add: Pair_def cartprod_def, safe)
   6.652 +defer 1 
   6.653 +  apply (simp add: powerset_def) 
   6.654 + apply blast 
   6.655 +txt{*Final, difficult case: the left-to-right direction of the theorem.*}
   6.656 +apply (insert power_ax, simp add: power_ax_def) 
   6.657 +apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   6.658 +apply (erule impE, blast, clarify) 
   6.659 +apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   6.660 +apply (blast intro: cartprod_iff_lemma) 
   6.661 +done
   6.662 +
   6.663 +lemma (in M_axioms) cartprod_closed_lemma:
   6.664 +     "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"
   6.665 +apply (simp del: cartprod_abs add: cartprod_iff)
   6.666 +apply (insert power_ax, simp add: power_ax_def) 
   6.667 +apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   6.668 +apply (erule impE, blast, clarify) 
   6.669 +apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec) 
   6.670 +apply (erule impE, blast, clarify)
   6.671 +apply (intro exI conjI) 
   6.672 +prefer 6 apply (rule refl) 
   6.673 +prefer 4 apply assumption
   6.674 +prefer 4 apply assumption
   6.675 +apply (insert cartprod_separation [of A B], simp, blast+)
   6.676 +done
   6.677 +
   6.678 +
   6.679 +text{*All the lemmas above are necessary because Powerset is not absolute.
   6.680 +      I should have used Replacement instead!*}
   6.681 +lemma (in M_axioms) cartprod_closed [intro]: 
   6.682 +     "[| M(A); M(B) |] ==> M(A*B)"
   6.683 +by (frule cartprod_closed_lemma, assumption, force)
   6.684 +
   6.685 +lemma (in M_axioms) image_closed [intro]: 
   6.686 +     "[| M(A); M(r) |] ==> M(r``A)"
   6.687 +apply (simp add: image_iff_Collect)
   6.688 +apply (insert image_separation [of A r], simp, blast) 
   6.689 +done
   6.690 +
   6.691 +lemma (in M_axioms) vimage_abs [simp]: 
   6.692 +     "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
   6.693 +apply (simp add: pre_image_def)
   6.694 +apply (rule iffI) 
   6.695 + apply (blast intro!: equalityI dest: transM, blast) 
   6.696 +done
   6.697 +
   6.698 +lemma (in M_axioms) vimage_closed [intro]: 
   6.699 +     "[| M(A); M(r) |] ==> M(r-``A)"
   6.700 +apply (simp add: vimage_iff_Collect)
   6.701 +apply (insert vimage_separation [of A r], simp, blast) 
   6.702 +done
   6.703 +
   6.704 +lemma (in M_axioms) domain_abs [simp]: 
   6.705 +     "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
   6.706 +apply (simp add: is_domain_def) 
   6.707 +apply (blast intro!: equalityI dest: transM) 
   6.708 +done
   6.709 +
   6.710 +lemma (in M_axioms) domain_closed [intro]: 
   6.711 +     "M(r) ==> M(domain(r))"
   6.712 +apply (simp add: domain_eq_vimage)
   6.713 +apply (blast intro: vimage_closed) 
   6.714 +done
   6.715 +
   6.716 +lemma (in M_axioms) range_abs [simp]: 
   6.717 +     "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
   6.718 +apply (simp add: is_range_def)
   6.719 +apply (blast intro!: equalityI dest: transM)
   6.720 +done
   6.721 +
   6.722 +lemma (in M_axioms) range_closed [intro]: 
   6.723 +     "M(r) ==> M(range(r))"
   6.724 +apply (simp add: range_eq_image)
   6.725 +apply (blast intro: image_closed) 
   6.726 +done
   6.727 +
   6.728 +lemma (in M_axioms) M_converse_iff:
   6.729 +     "M(r) ==> 
   6.730 +      converse(r) = 
   6.731 +      {z \<in> range(r) * domain(r). 
   6.732 +        \<exists>p\<in>r. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> p = \<langle>x,y\<rangle> \<and> z = \<langle>y,x\<rangle>)}"
   6.733 +by (blast dest: transM)
   6.734 +
   6.735 +lemma (in M_axioms) converse_closed [intro]: 
   6.736 +     "M(r) ==> M(converse(r))"
   6.737 +apply (simp add: M_converse_iff)
   6.738 +apply (insert converse_separation [of r], simp) 
   6.739 +apply (blast intro: image_closed) 
   6.740 +done
   6.741 +
   6.742 +lemma (in M_axioms) relation_abs [simp]: 
   6.743 +     "M(r) ==> is_relation(M,r) <-> relation(r)"
   6.744 +apply (simp add: is_relation_def relation_def) 
   6.745 +apply (blast dest!: bspec dest: pair_components_in_M)+
   6.746 +done
   6.747 +
   6.748 +lemma (in M_axioms) function_abs [simp]: 
   6.749 +     "M(r) ==> is_function(M,r) <-> function(r)"
   6.750 +apply (simp add: is_function_def function_def, safe) 
   6.751 +   apply (frule transM, assumption) 
   6.752 +  apply (blast dest: pair_components_in_M)+
   6.753 +done
   6.754 +
   6.755 +lemma (in M_axioms) apply_closed [intro]: 
   6.756 +     "[|M(f); M(a)|] ==> M(f`a)"
   6.757 +apply (simp add: apply_def) 
   6.758 +apply (blast intro: elim:); 
   6.759 +done
   6.760 +
   6.761 +lemma (in M_axioms) apply_abs: 
   6.762 +     "[| function(f); M(f); M(y) |] 
   6.763 +      ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
   6.764 +apply (simp add: fun_apply_def)
   6.765 +apply (blast intro: function_apply_equality function_apply_Pair) 
   6.766 +done
   6.767 +
   6.768 +lemma (in M_axioms) typed_apply_abs: 
   6.769 +     "[| f \<in> A -> B; M(f); M(y) |] 
   6.770 +      ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
   6.771 +by (simp add: apply_abs fun_is_function domain_of_fun) 
   6.772 +
   6.773 +lemma (in M_axioms) typed_function_abs [simp]: 
   6.774 +     "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
   6.775 +apply (auto simp add: typed_function_def relation_def Pi_iff) 
   6.776 +apply (blast dest: pair_components_in_M)+
   6.777 +done
   6.778 +
   6.779 +lemma (in M_axioms) injection_abs [simp]: 
   6.780 +     "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
   6.781 +apply (simp add: injection_def apply_iff inj_def apply_closed)
   6.782 +apply (blast dest: transM [of _ A]); 
   6.783 +done
   6.784 +
   6.785 +lemma (in M_axioms) surjection_abs [simp]: 
   6.786 +     "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
   6.787 +by (simp add: typed_apply_abs surjection_def surj_def)
   6.788 +
   6.789 +lemma (in M_axioms) bijection_abs [simp]: 
   6.790 +     "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
   6.791 +by (simp add: bijection_def bij_def)
   6.792 +
   6.793 +text{*no longer needed*}
   6.794 +lemma (in M_axioms) restriction_is_function: 
   6.795 +     "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] 
   6.796 +      ==> function(z)"
   6.797 +apply (rotate_tac 1)
   6.798 +apply (simp add: restriction_def Ball_iff_equiv) 
   6.799 +apply (unfold function_def, blast) 
   6.800 +done
   6.801 +
   6.802 +lemma (in M_axioms) restriction_abs [simp]: 
   6.803 +     "[| M(f); M(A); M(z) |] 
   6.804 +      ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
   6.805 +apply (simp add: Ball_iff_equiv restriction_def restrict_def)
   6.806 +apply (blast intro!: equalityI dest: transM) 
   6.807 +done
   6.808 +
   6.809 +
   6.810 +lemma (in M_axioms) M_restrict_iff:
   6.811 +     "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
   6.812 +by (simp add: restrict_def, blast dest: transM)
   6.813 +
   6.814 +lemma (in M_axioms) restrict_closed [intro]: 
   6.815 +     "[| M(A); M(r) |] ==> M(restrict(r,A))"
   6.816 +apply (simp add: M_restrict_iff)
   6.817 +apply (insert restrict_separation [of A], simp, blast) 
   6.818 +done
   6.819 +
   6.820 +
   6.821 +lemma (in M_axioms) M_comp_iff:
   6.822 +     "[| M(r); M(s) |] 
   6.823 +      ==> r O s = 
   6.824 +          {xz \<in> domain(s) * range(r).  
   6.825 +            \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and> 
   6.826 +                xz = \<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle> \<in> s \<and> \<langle>y,z\<rangle> \<in> r))}"
   6.827 +apply (simp add: comp_def)
   6.828 +apply (rule equalityI) 
   6.829 + apply (clarify ); 
   6.830 + apply (simp add: ); 
   6.831 + apply  (blast dest:  transM)+
   6.832 +done
   6.833 +
   6.834 +lemma (in M_axioms) comp_closed [intro]: 
   6.835 +     "[| M(r); M(s) |] ==> M(r O s)"
   6.836 +apply (simp add: M_comp_iff)
   6.837 +apply (insert comp_separation [of r s], simp, blast) 
   6.838 +done
   6.839 +
   6.840 +lemma (in M_axioms) nat_into_M [intro]:
   6.841 +     "n \<in> nat ==> M(n)"
   6.842 +by (induct n rule: nat_induct, simp_all)
   6.843 +
   6.844 +lemma (in M_axioms) Inl_in_M_iff [iff]:
   6.845 +     "M(Inl(a)) <-> M(a)"
   6.846 +by (simp add: Inl_def) 
   6.847 +
   6.848 +lemma (in M_axioms) Inr_in_M_iff [iff]:
   6.849 +     "M(Inr(a)) <-> M(a)"
   6.850 +by (simp add: Inr_def) 
   6.851 +
   6.852 +lemma (in M_axioms) Inter_abs [simp]: 
   6.853 +     "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
   6.854 +apply (simp add: big_inter_def Inter_def) 
   6.855 +apply (blast intro!: equalityI dest: transM) 
   6.856 +done
   6.857 +
   6.858 +lemma (in M_axioms) Inter_closed [intro]:
   6.859 +     "M(A) ==> M(Inter(A))"
   6.860 +by (insert Inter_separation, simp add: Inter_def, blast)
   6.861 +
   6.862 +lemma (in M_axioms) Int_closed [intro]:
   6.863 +     "[| M(A); M(B) |] ==> M(A Int B)"
   6.864 +apply (subgoal_tac "M({A,B})")
   6.865 +apply (frule Inter_closed, force+); 
   6.866 +done
   6.867 +
   6.868 +subsection{*Absoluteness for ordinals*}
   6.869 +text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
   6.870 +
   6.871 +lemma (in M_axioms) lt_closed:
   6.872 +     "[| j<i; M(i) |] ==> M(j)" 
   6.873 +by (blast dest: ltD intro: transM) 
   6.874 +
   6.875 +lemma (in M_axioms) transitive_set_abs [simp]: 
   6.876 +     "M(a) ==> transitive_set(M,a) <-> Transset(a)"
   6.877 +by (simp add: transitive_set_def Transset_def)
   6.878 +
   6.879 +lemma (in M_axioms) ordinal_abs [simp]: 
   6.880 +     "M(a) ==> ordinal(M,a) <-> Ord(a)"
   6.881 +by (simp add: ordinal_def Ord_def)
   6.882 +
   6.883 +lemma (in M_axioms) limit_ordinal_abs [simp]: 
   6.884 +     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
   6.885 +apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
   6.886 +apply (simp add: lt_def, blast) 
   6.887 +done
   6.888 +
   6.889 +lemma (in M_axioms) successor_ordinal_abs [simp]: 
   6.890 +     "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
   6.891 +apply (simp add: successor_ordinal_def, safe)
   6.892 +apply (drule Ord_cases_disj, auto) 
   6.893 +done
   6.894 +
   6.895 +lemma finite_Ord_is_nat:
   6.896 +      "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
   6.897 +by (induct a rule: trans_induct3, simp_all)
   6.898 +
   6.899 +lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
   6.900 +by (induct a rule: nat_induct, auto)
   6.901 +
   6.902 +lemma (in M_axioms) finite_ordinal_abs [simp]: 
   6.903 +     "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
   6.904 +apply (simp add: finite_ordinal_def)
   6.905 +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord 
   6.906 +             dest: Ord_trans naturals_not_limit)
   6.907 +done
   6.908 +
   6.909 +lemma Limit_non_Limit_implies_nat: "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
   6.910 +apply (rule le_anti_sym) 
   6.911 +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)  
   6.912 + apply (simp add: lt_def)  
   6.913 + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) 
   6.914 +apply (erule nat_le_Limit)
   6.915 +done
   6.916 +
   6.917 +lemma (in M_axioms) omega_abs [simp]: 
   6.918 +     "M(a) ==> omega(M,a) <-> a = nat"
   6.919 +apply (simp add: omega_def) 
   6.920 +apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
   6.921 +done
   6.922 +
   6.923 +lemma (in M_axioms) number1_abs [simp]: 
   6.924 +     "M(a) ==> number1(M,a) <-> a = 1"
   6.925 +by (simp add: number1_def) 
   6.926 +
   6.927 +lemma (in M_axioms) number1_abs [simp]: 
   6.928 +     "M(a) ==> number2(M,a) <-> a = succ(1)"
   6.929 +by (simp add: number2_def) 
   6.930 +
   6.931 +lemma (in M_axioms) number3_abs [simp]: 
   6.932 +     "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
   6.933 +by (simp add: number3_def) 
   6.934 +
   6.935 +text{*Kunen continued to 20...*}
   6.936 +
   6.937 +(*Could not get this to work.  The \<lambda>x\<in>nat is essential because everything 
   6.938 +  but the recursion variable must stay unchanged.  But then the recursion
   6.939 +  equations only hold for x\<in>nat (or in some other set) and not for the 
   6.940 +  whole of the class M.
   6.941 +  consts
   6.942 +    natnumber_aux :: "[i=>o,i] => i"
   6.943 +
   6.944 +  primrec
   6.945 +      "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
   6.946 +      "natnumber_aux(M,succ(n)) = 
   6.947 +	   (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) 
   6.948 +		     then 1 else 0)"
   6.949 +
   6.950 +  constdefs
   6.951 +    natnumber :: "[i=>o,i,i] => o"
   6.952 +      "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   6.953 +
   6.954 +  lemma (in M_axioms) [simp]: 
   6.955 +       "natnumber(M,0,x) == x=0"
   6.956 +*)
   6.957 +
   6.958 +
   6.959 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Wed Jun 19 11:48:01 2002 +0200
     7.3 @@ -0,0 +1,210 @@
     7.4 +theory WF_absolute = WF_extras + WFrec:
     7.5 +
     7.6 +
     7.7 +subsection{*Transitive closure without fixedpoints*}
     7.8 +
     7.9 +(*Ordinal.thy: just after succ_le_iff?*)
    7.10 +lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
    7.11 +apply (insert succ_le_iff [of i j]) 
    7.12 +apply (simp add: lt_def) 
    7.13 +done
    7.14 +
    7.15 +constdefs
    7.16 +  rtrancl_alt :: "[i,i]=>i"
    7.17 +    "rtrancl_alt(A,r) == 
    7.18 +       {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
    7.19 +                 \<exists>x y. p = <x,y> &  f`0 = x & f`n = y &
    7.20 +                       (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
    7.21 +
    7.22 +lemma alt_rtrancl_lemma1 [rule_format]: 
    7.23 +    "n \<in> nat
    7.24 +     ==> \<forall>f \<in> succ(n) -> field(r). 
    7.25 +         (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
    7.26 +apply (induct_tac n) 
    7.27 +apply (simp_all add: apply_funtype rtrancl_refl, clarify) 
    7.28 +apply (rename_tac n f) 
    7.29 +apply (rule rtrancl_into_rtrancl) 
    7.30 + prefer 2 apply assumption
    7.31 +apply (drule_tac x="restrict(f,succ(n))" in bspec)
    7.32 + apply (blast intro: restrict_type2) 
    7.33 +apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    7.34 +done
    7.35 +
    7.36 +lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
    7.37 +apply (simp add: rtrancl_alt_def)
    7.38 +apply (blast intro: alt_rtrancl_lemma1 )  
    7.39 +done
    7.40 +
    7.41 +lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
    7.42 +apply (simp add: rtrancl_alt_def, clarify) 
    7.43 +apply (frule rtrancl_type [THEN subsetD], clarify) 
    7.44 +apply simp 
    7.45 +apply (erule rtrancl_induct) 
    7.46 + txt{*Base case, trivial*}
    7.47 + apply (rule_tac x=0 in bexI) 
    7.48 +  apply (rule_tac x="lam x:1. xa" in bexI) 
    7.49 +   apply simp_all 
    7.50 +txt{*Inductive step*}
    7.51 +apply clarify 
    7.52 +apply (rename_tac n f) 
    7.53 +apply (rule_tac x="succ(n)" in bexI) 
    7.54 + apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
    7.55 +  apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI) 
    7.56 +  apply (blast intro: mem_asym)  
    7.57 + apply typecheck 
    7.58 + apply auto 
    7.59 +done
    7.60 +
    7.61 +lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
    7.62 +by (blast del: subsetI
    7.63 +	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt) 
    7.64 +
    7.65 +
    7.66 +text{*Relativized to M: Every well-founded relation is a subset of some
    7.67 +inverse image of an ordinal.  Key step is the construction (in M) of a 
    7.68 +rank function.*}
    7.69 +
    7.70 +
    7.71 +(*NEEDS RELATIVIZATION*)
    7.72 +locale M_recursion = M_axioms +
    7.73 +  assumes wfrank_separation':
    7.74 +     "[| M(r); M(a); r \<subseteq> A*A |] ==>
    7.75 +	separation
    7.76 +	   (M, \<lambda>x. x \<in> A --> 
    7.77 +		~(\<exists>f. M(f) \<and> 
    7.78 +		      is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f)))"
    7.79 + and wfrank_strong_replacement':
    7.80 +     "[| M(r); M(a); r \<subseteq> A*A |] ==>
    7.81 +      strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
    7.82 +		  pair(M,x,y,z) & 
    7.83 +		  is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f) & 
    7.84 +		  y = (\<Union>y \<in> r-``{x}. succ(g`y)))"
    7.85 +
    7.86 +
    7.87 +constdefs (*????????????????NEEDED?*)
    7.88 + is_wfrank_fun :: "[i=>o,i,i,i] => o"
    7.89 +    "is_wfrank_fun(M,r,a,f) == 
    7.90 +       function(f) & domain(f) = r-``{a} & 
    7.91 +       (\<forall>x. M(x) --> <x,a> \<in> r --> f`x = (\<Union>y \<in> r-``{x}. succ(f`y)))"
    7.92 +
    7.93 +
    7.94 +
    7.95 +
    7.96 +lemma (in M_recursion) exists_wfrank:
    7.97 +    "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
    7.98 +     ==> \<exists>f. M(f) & is_recfun(r, a, %x g. (\<Union>y \<in> r-``{x}. succ(g`y)), f)"
    7.99 +apply (rule exists_is_recfun [of A r]) 
   7.100 +apply (erule wellfounded_imp_wellfounded_on) 
   7.101 +apply assumption; 
   7.102 +apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
   7.103 +apply (rule succI1) 
   7.104 +apply (blast intro: wfrank_separation') 
   7.105 +apply (blast intro: wfrank_strong_replacement') 
   7.106 +apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   7.107 +done
   7.108 +
   7.109 +lemma (in M_recursion) exists_wfrank_fun:
   7.110 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_wfrank_fun(M,i,succ(j),f)"
   7.111 +apply (rule exists_wfrank [THEN exE])
   7.112 +apply (erule Ord_succ, assumption, simp) 
   7.113 +apply (rename_tac f, clarify) 
   7.114 +apply (frule is_recfun_type)
   7.115 +apply (rule_tac x=f in exI) 
   7.116 +apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   7.117 +                 is_wfrank_fun_eq Ord_trans [OF _ succI1])
   7.118 +done
   7.119 +
   7.120 +lemma (in M_recursion) is_wfrank_fun_apply:
   7.121 +    "[| x < j; M(i); M(j); M(f); is_wfrank_fun(M,r,a,f) |] 
   7.122 +     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
   7.123 +apply (simp add: is_wfrank_fun_eq lt_Ord2) 
   7.124 +apply (frule lt_closed, simp) 
   7.125 +apply (subgoal_tac "x <= domain(f)")
   7.126 + apply (simp add: Ord_trans [OF _ succI1] image_function)
   7.127 + apply (blast intro: elim:); 
   7.128 +apply (blast intro: dest!: leI [THEN le_imp_subset] ) 
   7.129 +done
   7.130 +
   7.131 +lemma (in M_recursion) is_wfrank_fun_eq_wfrank [rule_format]:
   7.132 +    "[| is_wfrank_fun(M,i,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
   7.133 +     ==> j<J --> f`j = i++j"
   7.134 +apply (erule_tac i=j in trans_induct, clarify) 
   7.135 +apply (subgoal_tac "\<forall>k\<in>x. k<J")
   7.136 + apply (simp (no_asm_simp) add: is_wfrank_def wfrank_unfold is_wfrank_fun_apply)
   7.137 +apply (blast intro: lt_trans ltI lt_Ord) 
   7.138 +done
   7.139 +
   7.140 +lemma (in M_recursion) wfrank_abs_fun_apply_iff:
   7.141 +    "[| M(i); M(J); M(f); M(k); j<J; is_wfrank_fun(M,i,J,f) |] 
   7.142 +     ==> fun_apply(M,f,j,k) <-> f`j = k"
   7.143 +by (auto simp add: lt_def is_wfrank_fun_eq subsetD apply_abs) 
   7.144 +
   7.145 +lemma (in M_recursion) Ord_wfrank_abs:
   7.146 +    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
   7.147 +apply (simp add: is_wfrank_def wfrank_abs_fun_apply_iff is_wfrank_fun_eq_wfrank)
   7.148 +apply (frule exists_wfrank_fun [of j i], blast+)
   7.149 +done
   7.150 +
   7.151 +lemma (in M_recursion) wfrank_abs:
   7.152 +    "[| M(i); M(j); M(k) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
   7.153 +apply (case_tac "Ord(i) & Ord(j)")
   7.154 + apply (simp add: Ord_wfrank_abs)
   7.155 +apply (auto simp add: is_wfrank_def wfrank_eq_if_raw_wfrank)
   7.156 +done
   7.157 +
   7.158 +lemma (in M_recursion) wfrank_closed [intro]:
   7.159 +    "[| M(i); M(j) |] ==> M(i++j)"
   7.160 +apply (simp add: wfrank_eq_if_raw_wfrank, clarify) 
   7.161 +apply (simp add: raw_wfrank_eq_wfrank) 
   7.162 +apply (frule exists_wfrank_fun [of j i], auto)
   7.163 +apply (simp add: apply_closed is_wfrank_fun_eq_wfrank [symmetric]) 
   7.164 +done
   7.165 +
   7.166 +
   7.167 +
   7.168 +constdefs
   7.169 +  wfrank :: "[i,i]=>i"
   7.170 +    "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
   7.171 +
   7.172 +constdefs
   7.173 +  wftype :: "i=>i"
   7.174 +    "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
   7.175 +
   7.176 +lemma (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
   7.177 +by (subst wfrank_def [THEN def_wfrec], simp_all)
   7.178 +
   7.179 +lemma (in M_axioms) Ord_wfrank: "wellfounded(M,r) ==> Ord(wfrank(r,a))"
   7.180 +apply (rule_tac a="a" in wf_induct, assumption)
   7.181 +apply (subst wfrank, assumption)
   7.182 +apply (rule Ord_succ [THEN Ord_UN], blast) 
   7.183 +done
   7.184 +
   7.185 +lemma (in M_axioms) wfrank_lt: "[|wellfounded(M,r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
   7.186 +apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
   7.187 +apply (rule UN_I [THEN ltI])
   7.188 +apply (simp add: Ord_wfrank vimage_iff)+
   7.189 +done
   7.190 +
   7.191 +lemma (in M_axioms) Ord_wftype: "wellfounded(M,r) ==> Ord(wftype(r))"
   7.192 +by (simp add: wftype_def Ord_wfrank)
   7.193 +
   7.194 +lemma (in M_axioms) wftypeI: "\<lbrakk>wellfounded(M,r);  x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
   7.195 +apply (simp add: wftype_def) 
   7.196 +apply (blast intro: wfrank_lt [THEN ltD]) 
   7.197 +done
   7.198 +
   7.199 +
   7.200 +lemma (in M_axioms) wf_imp_subset_rvimage:
   7.201 +     "[|wellfounded(M,r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
   7.202 +apply (rule_tac x="wftype(r)" in exI) 
   7.203 +apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI) 
   7.204 +apply (simp add: Ord_wftype, clarify) 
   7.205 +apply (frule subsetD, assumption, clarify) 
   7.206 +apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
   7.207 +apply (blast intro: wftypeI  ) 
   7.208 +done
   7.209 +
   7.210 +
   7.211 +
   7.212 +
   7.213 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/Constructible/WFrec.thy	Wed Jun 19 11:48:01 2002 +0200
     8.3 @@ -0,0 +1,559 @@
     8.4 +theory WFrec = Wellorderings:
     8.5 +
     8.6 +
     8.7 +(*WF.thy??*)
     8.8 +
     8.9 +lemma is_recfunI:
    8.10 +     "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
    8.11 +by (simp add: is_recfun_def) 
    8.12 +
    8.13 +lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)"
    8.14 +apply (simp add: is_recfun_def) 
    8.15 +apply (erule ssubst)
    8.16 +apply (rule function_lam) 
    8.17 +done
    8.18 +
    8.19 +text{*Expresses @{text is_recfun} as a recursion equation*}
    8.20 +lemma is_recfun_iff_equation:
    8.21 +     "is_recfun(r,a,H,f) <->
    8.22 +	   f \<in> r -`` {a} \<rightarrow> range(f) &
    8.23 +	   (\<forall>x \<in> r-``{a}. f`x = H(x, restrict(f, r-``{x})))"  
    8.24 +apply (rule iffI) 
    8.25 + apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff, 
    8.26 +        clarify)  
    8.27 +apply (simp add: is_recfun_def) 
    8.28 +apply (rule fun_extension) 
    8.29 +  apply assumption
    8.30 + apply (fast intro: lam_type, simp) 
    8.31 +done
    8.32 +
    8.33 +lemma trans_on_Int_eq [simp]:
    8.34 +      "[| trans[A](r); <y,x> \<in> r;  r \<subseteq> A*A |] 
    8.35 +       ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
    8.36 +by (blast intro: trans_onD) 
    8.37 +
    8.38 +lemma trans_on_Int_eq2 [simp]:
    8.39 +      "[| trans[A](r); <y,x> \<in> r;  r \<subseteq> A*A |] 
    8.40 +       ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
    8.41 +by (blast intro: trans_onD) 
    8.42 +
    8.43 +
    8.44 +constdefs
    8.45 +   M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
    8.46 +     "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
    8.47 +
    8.48 +
    8.49 +text{*Stated using @{term "trans[A](r)"} rather than
    8.50 +      @{term "transitive_rel(M,A,r)"} because the latter rewrites to
    8.51 +      the former anyway, by @{text transitive_rel_abs}.
    8.52 +      As always, theorems should be expressed in simplified form.*}
    8.53 +lemma (in M_axioms) is_recfun_equal [rule_format]: 
    8.54 +    "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
    8.55 +       wellfounded_on(M,A,r);  trans[A](r); 
    8.56 +       M(A); M(f); M(g); M(a); M(b); 
    8.57 +       r \<subseteq> A*A;  x\<in>A |] 
    8.58 +     ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x"
    8.59 +apply (frule_tac f="f" in is_recfun_type) 
    8.60 +apply (frule_tac f="g" in is_recfun_type) 
    8.61 +apply (simp add: is_recfun_def)
    8.62 +apply (erule wellfounded_on_induct2, assumption+) 
    8.63 +apply (force intro: is_recfun_separation, clarify)
    8.64 +apply (erule ssubst)+
    8.65 +apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
    8.66 +apply (rename_tac x1)
    8.67 +apply (rule_tac t="%z. H(x1,z)" in subst_context) 
    8.68 +apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g")
    8.69 + apply (blast intro: trans_onD) 
    8.70 +apply (simp add: apply_iff) 
    8.71 +apply (blast intro: trans_onD sym) 
    8.72 +done
    8.73 +
    8.74 +lemma (in M_axioms) is_recfun_cut: 
    8.75 +    "[|is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  
    8.76 +       wellfounded_on(M,A,r); trans[A](r); 
    8.77 +       M(A); M(f); M(g); M(a); M(b); 
    8.78 +       r \<subseteq> A*A;  <b,a>\<in>r |]   
    8.79 +      ==> restrict(f, r-``{b}) = g"
    8.80 +apply (frule_tac f="f" in is_recfun_type) 
    8.81 +apply (rule fun_extension) 
    8.82 +apply (blast intro: trans_onD restrict_type2) 
    8.83 +apply (erule is_recfun_type, simp) 
    8.84 +apply (blast intro: is_recfun_equal trans_onD) 
    8.85 +done
    8.86 +
    8.87 +lemma (in M_axioms) is_recfun_functional:
    8.88 +     "[|is_recfun(r,a,H,f);  is_recfun(r,a,H,g);  
    8.89 +       wellfounded_on(M,A,r); trans[A](r); 
    8.90 +       M(A); M(f); M(g); M(a); 
    8.91 +       r \<subseteq> A*A |]   
    8.92 +      ==> f=g"
    8.93 +apply (rule fun_extension)
    8.94 +apply (erule is_recfun_type)+
    8.95 +apply (blast intro!: is_recfun_equal) 
    8.96 +done
    8.97 +
    8.98 +text{*Tells us that is_recfun can (in principle) be relativized.*}
    8.99 +lemma (in M_axioms) is_recfun_relativize:
   8.100 +     "[| M(r); M(a); M(f); 
   8.101 +       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==>
   8.102 +       is_recfun(r,a,H,f) <->
   8.103 +       (\<forall>z. z \<in> f <-> (\<exists>x y. M(x) & M(y) & z=<x,y> & <x,a> \<in> r & 
   8.104 +                              y = H(x, restrict(f, r-``{x}))))";
   8.105 +apply (simp add: is_recfun_def vimage_closed restrict_closed lam_def)
   8.106 +apply (safe intro!: equalityI) 
   8.107 +  apply (drule equalityD1 [THEN subsetD], assumption) 
   8.108 +  apply clarify 
   8.109 +  apply (rule_tac x=x in exI) 
   8.110 +  apply (blast dest: pair_components_in_M) 
   8.111 + apply (blast elim!: equalityE dest: pair_components_in_M)
   8.112 + apply simp  
   8.113 + apply blast
   8.114 + apply simp 
   8.115 +apply (subgoal_tac "function(f)")  
   8.116 + prefer 2
   8.117 + apply (simp add: function_def) 
   8.118 +apply (frule pair_components_in_M, assumption) 
   8.119 +  apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed) 
   8.120 +done
   8.121 +
   8.122 +(* ideas for further weaking the H-closure premise:
   8.123 +apply (drule spec [THEN spec]) 
   8.124 +apply (erule mp)
   8.125 +apply (intro conjI)
   8.126 +apply (blast dest!: pair_components_in_M)
   8.127 +apply (blast intro!: function_restrictI dest!: pair_components_in_M)
   8.128 +apply (blast intro!: function_restrictI dest!: pair_components_in_M)
   8.129 +apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) 
   8.130 +apply (simp add:  vimage_singleton_iff) 
   8.131 +apply (intro allI impI conjI)
   8.132 +apply (blast intro: transM dest!: pair_components_in_M)
   8.133 +prefer 4;apply blast 
   8.134 +*)
   8.135 +
   8.136 +lemma (in M_axioms) is_recfun_restrict:
   8.137 +     "[| wellfounded_on(M,A,r); trans[A](r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
   8.138 +       M(A); M(r); M(f); 
   8.139 +       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \<subseteq> A * A |]
   8.140 +       ==> is_recfun(r, y, H, restrict(f, r -`` {y}))"
   8.141 +apply (frule pair_components_in_M, assumption, clarify) 
   8.142 +apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed
   8.143 +     restrict_iff)
   8.144 +apply safe
   8.145 +  apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff]) 
   8.146 +  apply (frule_tac x=xa in pair_components_in_M, assumption)
   8.147 +  apply (frule_tac x=xa in apply_recfun, blast intro: trans_onD)  
   8.148 +  apply (simp add: is_recfun_type [THEN apply_iff])
   8.149 +  (*???COMBINE*) 
   8.150 +  apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed) 
   8.151 +apply (blast intro: apply_recfun dest: trans_onD)+
   8.152 +done
   8.153 + 
   8.154 +lemma (in M_axioms) restrict_Y_lemma:
   8.155 +     "[| wellfounded_on(M,A,r); trans[A](r); M(A); M(r); r \<subseteq> A \<times> A;
   8.156 +       \<forall>x g. M(x) \<and> M(g) & function(g) --> M(H(x,g));  M(Y);
   8.157 +       \<forall>b. M(b) -->
   8.158 +	   b \<in> Y <->
   8.159 +	   (\<exists>x\<in>r -`` {a1}.
   8.160 +	       \<exists>y. M(y) \<and>
   8.161 +		   (\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g)));
   8.162 +          \<langle>x,a1\<rangle> \<in> r; M(f); is_recfun(r,x,H,f) |]
   8.163 +       ==> restrict(Y, r -`` {x}) = f"
   8.164 +apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:Y <-> <y,z>:f") 
   8.165 +apply (simp (no_asm_simp) add: restrict_def) 
   8.166 +apply (thin_tac "All(?P)")+  --{*essential for efficiency*}
   8.167 +apply (frule is_recfun_type [THEN fun_is_rel], blast)
   8.168 +apply (frule pair_components_in_M, assumption, clarify) 
   8.169 +apply (rule iffI)
   8.170 + apply (frule_tac y="<y,z>" in transM, assumption )
   8.171 + apply (rotate_tac -1)   
   8.172 + apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
   8.173 +			   apply_recfun is_recfun_cut) 
   8.174 +txt{*Opposite inclusion: something in f, show in Y*}
   8.175 +apply (frule_tac y="<y,z>" in transM, assumption, simp) 
   8.176 +apply (rule_tac x=y in bexI)
   8.177 +prefer 2 apply (blast dest: trans_onD)
   8.178 +apply (rule_tac x=z in exI, simp) 
   8.179 +apply (rule_tac x="restrict(f, r -`` {y})" in exI) 
   8.180 +apply (simp add: vimage_closed restrict_closed is_recfun_restrict
   8.181 +                 apply_recfun is_recfun_type [THEN apply_iff]) 
   8.182 +done
   8.183 +
   8.184 +text{*Proof of the inductive step for @{text exists_is_recfun}, since
   8.185 +      we must prove two versions.*}
   8.186 +lemma (in M_axioms) exists_is_recfun_indstep:
   8.187 +    "[|a1 \<in> A;  \<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f)); 
   8.188 +       wellfounded_on(M,A,r); trans[A](r); 
   8.189 +       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.190 +                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   8.191 +       M(A); M(r); r \<subseteq> A * A;
   8.192 +       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g))|]   
   8.193 +      ==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
   8.194 +apply (frule_tac y=a1 in transM, assumption)
   8.195 +apply (drule_tac A="r-``{a1}" in strong_replacementD)
   8.196 +  apply blast
   8.197 + txt{*Discharge the "univalent" obligation of Replacement*}
   8.198 + apply (clarsimp simp add: univalent_def)
   8.199 + apply (blast dest!: is_recfun_functional)
   8.200 +txt{*Show that the constructed object satisfies @{text is_recfun}*} 
   8.201 +apply clarify 
   8.202 +apply (rule_tac x=Y in exI)  
   8.203 +apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed) 
   8.204 +(*Tried using is_recfun_iff2 here.  Much more simplification takes place
   8.205 +  because an assumption can kick in.  Not sure how to relate the new 
   8.206 +  proof state to the current one.*)
   8.207 +apply safe
   8.208 +txt{*Show that elements of @{term Y} are in the right relationship.*}
   8.209 +apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec)
   8.210 +apply (erule impE, blast intro: transM)
   8.211 +txt{*We have an element of  @{term Y}, so we have x, y, z*} 
   8.212 +apply (frule_tac y=z in transM, assumption, clarify)
   8.213 +apply (simp add: vimage_closed restrict_closed restrict_Y_lemma [of A r H]) 
   8.214 +txt{*one more case*}
   8.215 +apply (simp add: vimage_closed restrict_closed )
   8.216 +apply (rule_tac x=x in bexI) 
   8.217 +prefer 2 apply blast 
   8.218 +apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI) 
   8.219 +apply (simp add: vimage_closed restrict_closed )
   8.220 +apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) 
   8.221 +apply (rule_tac x=f in exI) 
   8.222 +apply (simp add: restrict_Y_lemma [of A r H]) 
   8.223 +done
   8.224 +
   8.225 +
   8.226 +text{*Relativized version, when we have the (currently weaker) premise
   8.227 +      @{term "wellfounded_on(M,A,r)"}*}
   8.228 +lemma (in M_axioms) wellfounded_exists_is_recfun:
   8.229 +    "[|wellfounded_on(M,A,r);  trans[A](r);  a\<in>A; 
   8.230 +       separation(M, \<lambda>x. x \<in> A --> ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f)));
   8.231 +       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.232 +                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   8.233 +       M(A);  M(r);  r \<subseteq> A*A;  
   8.234 +       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
   8.235 +      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
   8.236 +apply (rule wellfounded_on_induct2, assumption+, clarify)
   8.237 +apply (rule exists_is_recfun_indstep, assumption+)
   8.238 +done
   8.239 +
   8.240 +lemma (in M_axioms) wf_exists_is_recfun:
   8.241 +    "[|wf[A](r);  trans[A](r);  a\<in>A; 
   8.242 +       strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.243 +                   pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g)); 
   8.244 +       M(A);  M(r);  r \<subseteq> A*A;  
   8.245 +       \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]   
   8.246 +      ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
   8.247 +apply (rule wf_on_induct2, assumption+)
   8.248 +apply (frule wf_on_imp_relativized)  
   8.249 +apply (rule exists_is_recfun_indstep, assumption+)
   8.250 +done
   8.251 +
   8.252 +(*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
   8.253 +lemma (in M_axioms) M_is_the_recfun: 
   8.254 +    "[|is_recfun(r,a,H,f);  
   8.255 +       wellfounded_on(M,A,r); trans[A](r); 
   8.256 +       M(A); M(f); M(a); r \<subseteq> A*A |]   
   8.257 +     ==> M(M_the_recfun(M,r,a,H)) & 
   8.258 +         is_recfun(r, a, H, M_the_recfun(M,r,a,H))"
   8.259 +apply (unfold M_the_recfun_def)
   8.260 +apply (rule ex1I [THEN theI2], fast)
   8.261 +apply (blast intro: is_recfun_functional, blast) 
   8.262 +done
   8.263 +
   8.264 +constdefs
   8.265 +   M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
   8.266 +     "M_is_recfun(M,r,a,MH,f) == 
   8.267 +      \<forall>z. M(z) -->
   8.268 +          (z \<in> f <-> 
   8.269 +           (\<exists>x y xa sx r_sx f_r_sx. 
   8.270 +              M(x) & M(y) & M(xa) & M(sx) & M(r_sx) & M(f_r_sx) &
   8.271 +	      pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
   8.272 +              pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
   8.273 +              xa \<in> r & MH(M, x, f_r_sx, y)))"
   8.274 +
   8.275 +lemma (in M_axioms) is_recfun_iff_M:
   8.276 +     "[| M(r); M(a); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g));
   8.277 +       \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==>
   8.278 +       is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
   8.279 +apply (simp add: vimage_closed restrict_closed M_is_recfun_def is_recfun_relativize)
   8.280 +apply (rule all_cong, safe)
   8.281 + apply (thin_tac "\<forall>x. ?P(x)")+
   8.282 + apply (blast dest: transM)  (*or del: allE*)
   8.283 +done
   8.284 +
   8.285 +lemma M_is_recfun_cong [cong]:
   8.286 +     "[| r = r'; a = a'; f = f'; 
   8.287 +       !!x g y. [| M(x); M(g); M(y) |] ==> MH(M,x,g,y) <-> MH'(M,x,g,y) |]
   8.288 +      ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')"
   8.289 +by (simp add: M_is_recfun_def) 
   8.290 +
   8.291 +
   8.292 +constdefs
   8.293 + (*This expresses ordinal addition as a formula in the LAST.  It also 
   8.294 +   provides an abbreviation that can be used in the instance of strong
   8.295 +   replacement below.  Here j is used to define the relation, namely
   8.296 +   Memrel(succ(j)), while x determines the domain of f.*)
   8.297 + is_oadd_fun :: "[i=>o,i,i,i,i] => o"
   8.298 +    "is_oadd_fun(M,i,j,x,f) == 
   8.299 +       (\<forall>sj msj. M(sj) --> M(msj) --> 
   8.300 +                 successor(M,j,sj) --> membership(M,sj,msj) --> 
   8.301 +	         M_is_recfun(M, msj, x, 
   8.302 +		     %M x g y. \<exists>gx. M(gx) & image(M,g,x,gx) & union(M,i,gx,y),
   8.303 +		     f))"
   8.304 +
   8.305 + is_oadd :: "[i=>o,i,i,i] => o"
   8.306 +    "is_oadd(M,i,j,k) == 
   8.307 +        (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) |
   8.308 +        (~ ordinal(M,i) & ordinal(M,j) & k=j) |
   8.309 +        (ordinal(M,i) & ~ ordinal(M,j) & k=i) |
   8.310 +        (ordinal(M,i) & ordinal(M,j) & 
   8.311 +	 (\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
   8.312 +		    successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) & 
   8.313 +		    fun_apply(M,f,j,fj) & fj = k))"
   8.314 +
   8.315 + (*NEEDS RELATIVIZATION*)
   8.316 + omult_eqns :: "[i,i,i,i] => o"
   8.317 +    "omult_eqns(i,x,g,z) ==
   8.318 +            Ord(x) & 
   8.319 +	    (x=0 --> z=0) &
   8.320 +            (\<forall>j. x = succ(j) --> z = g`j ++ i) &
   8.321 +            (Limit(x) --> z = \<Union>(g``x))"
   8.322 +
   8.323 + is_omult_fun :: "[i=>o,i,i,i] => o"
   8.324 +    "is_omult_fun(M,i,j,f) == 
   8.325 +	    (\<exists>df. M(df) & is_function(M,f) & 
   8.326 +                  is_domain(M,f,df) & subset(M, j, df)) & 
   8.327 +            (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))"
   8.328 +
   8.329 + is_omult :: "[i=>o,i,i,i] => o"
   8.330 +    "is_omult(M,i,j,k) == 
   8.331 +	\<exists>f fj sj. M(f) & M(fj) & M(sj) & 
   8.332 +                  successor(M,j,sj) & is_omult_fun(M,i,sj,f) & 
   8.333 +                  fun_apply(M,f,j,fj) & fj = k"
   8.334 +
   8.335 +
   8.336 +locale M_recursion = M_axioms +
   8.337 +  assumes oadd_strong_replacement:
   8.338 +   "[| M(i); M(j) |] ==>
   8.339 +    strong_replacement(M, 
   8.340 +         \<lambda>x z. \<exists>y f fx. M(y) & M(f) & M(fx) & 
   8.341 +		         pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) & 
   8.342 +		         image(M,f,x,fx) & y = i Un fx)" 
   8.343 + and omult_strong_replacement':
   8.344 +   "[| M(i); M(j) |] ==>
   8.345 +    strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.346 +	     pair(M,x,y,z) & 
   8.347 +	     is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) & 
   8.348 +	     y = (THE z. omult_eqns(i, x, g, z)))" 
   8.349 +
   8.350 +
   8.351 +
   8.352 +text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
   8.353 +lemma (in M_recursion) is_oadd_fun_iff:
   8.354 +   "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
   8.355 +    ==> is_oadd_fun(M,i,j,a,f) <->
   8.356 +	f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
   8.357 +apply (frule lt_Ord) 
   8.358 +apply (simp add: is_oadd_fun_def Memrel_closed Un_closed 
   8.359 +             is_recfun_iff_M [of concl: _ _ "%x g. i Un g``x", THEN iff_sym]
   8.360 +             image_closed is_recfun_iff_equation  
   8.361 +             Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
   8.362 +apply (simp add: lt_def) 
   8.363 +apply (blast dest: transM) 
   8.364 +done
   8.365 +
   8.366 +
   8.367 +lemma (in M_recursion) oadd_strong_replacement':
   8.368 +    "[| M(i); M(j) |] ==>
   8.369 +     strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
   8.370 +		  pair(M,x,y,z) & 
   8.371 +		  is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) & 
   8.372 +		  y = i Un g``x)" 
   8.373 +apply (insert oadd_strong_replacement [of i j]) 
   8.374 +apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def
   8.375 +                 is_recfun_iff_M)  
   8.376 +done
   8.377 +
   8.378 +
   8.379 +lemma (in M_recursion) exists_oadd:
   8.380 +    "[| Ord(j);  M(i);  M(j) |]
   8.381 +     ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
   8.382 +apply (rule wf_exists_is_recfun) 
   8.383 +apply (rule wf_Memrel [THEN wf_imp_wf_on]) 
   8.384 +apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
   8.385 +apply (rule succI1) 
   8.386 +apply (blast intro: oadd_strong_replacement') 
   8.387 +apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   8.388 +done
   8.389 +
   8.390 +lemma (in M_recursion) exists_oadd_fun:
   8.391 +    "[| Ord(j);  M(i);  M(j) |] 
   8.392 +     ==> \<exists>f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)"
   8.393 +apply (rule exists_oadd [THEN exE])
   8.394 +apply (erule Ord_succ, assumption, simp) 
   8.395 +apply (rename_tac f, clarify) 
   8.396 +apply (frule is_recfun_type)
   8.397 +apply (rule_tac x=f in exI) 
   8.398 +apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   8.399 +                 is_oadd_fun_iff Ord_trans [OF _ succI1])
   8.400 +done
   8.401 +
   8.402 +lemma (in M_recursion) is_oadd_fun_apply:
   8.403 +    "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |] 
   8.404 +     ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
   8.405 +apply (simp add: is_oadd_fun_iff lt_Ord2, clarify) 
   8.406 +apply (frule lt_closed, simp)
   8.407 +apply (frule leI [THEN le_imp_subset])  
   8.408 +apply (simp add: image_fun, blast) 
   8.409 +done
   8.410 +
   8.411 +lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]:
   8.412 +    "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |] 
   8.413 +     ==> j<J --> f`j = i++j"
   8.414 +apply (erule_tac i=j in trans_induct, clarify) 
   8.415 +apply (subgoal_tac "\<forall>k\<in>x. k<J")
   8.416 + apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply)
   8.417 +apply (blast intro: lt_trans ltI lt_Ord) 
   8.418 +done
   8.419 +
   8.420 +lemma (in M_recursion) oadd_abs_fun_apply_iff:
   8.421 +    "[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |] 
   8.422 +     ==> fun_apply(M,f,j,k) <-> f`j = k"
   8.423 +by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs) 
   8.424 +
   8.425 +lemma (in M_recursion) Ord_oadd_abs:
   8.426 +    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
   8.427 +apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
   8.428 +apply (frule exists_oadd_fun [of j i], blast+)
   8.429 +done
   8.430 +
   8.431 +lemma (in M_recursion) oadd_abs:
   8.432 +    "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
   8.433 +apply (case_tac "Ord(i) & Ord(j)")
   8.434 + apply (simp add: Ord_oadd_abs)
   8.435 +apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
   8.436 +done
   8.437 +
   8.438 +lemma (in M_recursion) oadd_closed [intro]:
   8.439 +    "[| M(i); M(j) |] ==> M(i++j)"
   8.440 +apply (simp add: oadd_eq_if_raw_oadd, clarify) 
   8.441 +apply (simp add: raw_oadd_eq_oadd) 
   8.442 +apply (frule exists_oadd_fun [of j i], auto)
   8.443 +apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric]) 
   8.444 +done
   8.445 +
   8.446 +
   8.447 +text{*Ordinal Multiplication*}
   8.448 +
   8.449 +lemma omult_eqns_unique:
   8.450 +     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
   8.451 +apply (simp add: omult_eqns_def, clarify) 
   8.452 +apply (erule Ord_cases, simp_all) 
   8.453 +done
   8.454 +
   8.455 +lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0"
   8.456 +by (simp add: omult_eqns_def)
   8.457 +
   8.458 +lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0"
   8.459 +by (simp add: omult_eqns_0)
   8.460 +
   8.461 +lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i"
   8.462 +by (simp add: omult_eqns_def)
   8.463 +
   8.464 +lemma the_omult_eqns_succ:
   8.465 +     "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i"
   8.466 +by (simp add: omult_eqns_succ) 
   8.467 +
   8.468 +lemma omult_eqns_Limit:
   8.469 +     "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)"
   8.470 +apply (simp add: omult_eqns_def) 
   8.471 +apply (blast intro: Limit_is_Ord) 
   8.472 +done
   8.473 +
   8.474 +lemma the_omult_eqns_Limit:
   8.475 +     "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)"
   8.476 +by (simp add: omult_eqns_Limit)
   8.477 +
   8.478 +lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)"
   8.479 +by (simp add: omult_eqns_def)
   8.480 +
   8.481 +
   8.482 +lemma (in M_recursion) the_omult_eqns_closed:
   8.483 +    "[| M(i); M(x); M(g); function(g) |] 
   8.484 +     ==> M(THE z. omult_eqns(i, x, g, z))"
   8.485 +apply (case_tac "Ord(x)")
   8.486 + prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
   8.487 +apply (erule Ord_cases) 
   8.488 +  apply (simp add: omult_eqns_0)
   8.489 + apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
   8.490 +apply (simp add: omult_eqns_Limit) 
   8.491 +apply (simp add: Union_closed image_closed) 
   8.492 +done
   8.493 +
   8.494 +lemma (in M_recursion) exists_omult:
   8.495 +    "[| Ord(j);  M(i);  M(j) |]
   8.496 +     ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
   8.497 +apply (rule wf_exists_is_recfun) 
   8.498 +apply (rule wf_Memrel [THEN wf_imp_wf_on]) 
   8.499 +apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)  
   8.500 +apply (rule succI1) 
   8.501 +apply (blast intro: omult_strong_replacement') 
   8.502 +apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
   8.503 +apply (blast intro: the_omult_eqns_closed) 
   8.504 +done
   8.505 +
   8.506 +lemma (in M_recursion) exists_omult_fun:
   8.507 +    "[| Ord(j);  M(i);  M(j) |] ==> \<exists>f. M(f) & is_omult_fun(M,i,succ(j),f)"
   8.508 +apply (rule exists_omult [THEN exE])
   8.509 +apply (erule Ord_succ, assumption, simp) 
   8.510 +apply (rename_tac f, clarify) 
   8.511 +apply (frule is_recfun_type)
   8.512 +apply (rule_tac x=f in exI) 
   8.513 +apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
   8.514 +                 is_omult_fun_def Ord_trans [OF _ succI1])
   8.515 +apply (force dest: Ord_in_Ord' 
   8.516 +             simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
   8.517 +                       the_omult_eqns_Limit) 
   8.518 +done
   8.519 +
   8.520 +lemma (in M_recursion) is_omult_fun_apply_0:
   8.521 +    "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
   8.522 +by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
   8.523 +
   8.524 +lemma (in M_recursion) is_omult_fun_apply_succ:
   8.525 +    "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
   8.526 +by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast) 
   8.527 +
   8.528 +lemma (in M_recursion) is_omult_fun_apply_Limit:
   8.529 +    "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |] 
   8.530 +     ==> f ` x = (\<Union>y\<in>x. f`y)"
   8.531 +apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
   8.532 +apply (drule subset_trans [OF OrdmemD], assumption+)  
   8.533 +apply (simp add: ball_conj_distrib omult_Limit image_function)
   8.534 +done
   8.535 +
   8.536 +lemma (in M_recursion) is_omult_fun_eq_omult:
   8.537 +    "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |] 
   8.538 +     ==> j<J --> f`j = i**j"
   8.539 +apply (erule_tac i=j in trans_induct3)
   8.540 +apply (safe del: impCE)
   8.541 +  apply (simp add: is_omult_fun_apply_0) 
   8.542 + apply (subgoal_tac "x<J") 
   8.543 +  apply (simp add: is_omult_fun_apply_succ omult_succ)  
   8.544 + apply (blast intro: lt_trans) 
   8.545 +apply (subgoal_tac "\<forall>k\<in>x. k<J")
   8.546 + apply (simp add: is_omult_fun_apply_Limit omult_Limit) 
   8.547 +apply (blast intro: lt_trans ltI lt_Ord) 
   8.548 +done
   8.549 +
   8.550 +lemma (in M_recursion) omult_abs_fun_apply_iff:
   8.551 +    "[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |] 
   8.552 +     ==> fun_apply(M,f,j,k) <-> f`j = k"
   8.553 +by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs) 
   8.554 +
   8.555 +lemma (in M_recursion) omult_abs:
   8.556 +    "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
   8.557 +apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
   8.558 +apply (frule exists_omult_fun [of j i], blast+)
   8.559 +done
   8.560 +
   8.561 +end
   8.562 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Wed Jun 19 11:48:01 2002 +0200
     9.3 @@ -0,0 +1,626 @@
     9.4 +header {*Relativized Wellorderings*}
     9.5 +
     9.6 +theory Wellorderings = Relative:
     9.7 +
     9.8 +text{*We define functions analogous to @{term ordermap} @{term ordertype} 
     9.9 +      but without using recursion.  Instead, there is a direct appeal
    9.10 +      to Replacement.  This will be the basis for a version relativized
    9.11 +      to some class @{text M}.  The main result is Theorem I 7.6 in Kunen,
    9.12 +      page 17.*}
    9.13 +
    9.14 +
    9.15 +subsection{*Wellorderings*}
    9.16 +
    9.17 +constdefs
    9.18 +  irreflexive :: "[i=>o,i,i]=>o"
    9.19 +    "irreflexive(M,A,r) == \<forall>x\<in>A. M(x) --> <x,x> \<notin> r"
    9.20 +  
    9.21 +  transitive_rel :: "[i=>o,i,i]=>o"
    9.22 +    "transitive_rel(M,A,r) == 
    9.23 +	\<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> (\<forall>z\<in>A. M(z) --> 
    9.24 +                          <x,y>\<in>r --> <y,z>\<in>r --> <x,z>\<in>r))"
    9.25 +
    9.26 +  linear_rel :: "[i=>o,i,i]=>o"
    9.27 +    "linear_rel(M,A,r) == 
    9.28 +	\<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
    9.29 +
    9.30 +  wellfounded :: "[i=>o,i]=>o"
    9.31 +    --{*EVERY non-empty set has an @{text r}-minimal element*}
    9.32 +    "wellfounded(M,r) == 
    9.33 +	\<forall>x. M(x) --> ~ empty(M,x) 
    9.34 +                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
    9.35 +  wellfounded_on :: "[i=>o,i,i]=>o"
    9.36 +    --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
    9.37 +    "wellfounded_on(M,A,r) == 
    9.38 +	\<forall>x. M(x) --> ~ empty(M,x) --> subset(M,x,A)
    9.39 +                 --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
    9.40 +
    9.41 +  wellordered :: "[i=>o,i,i]=>o"
    9.42 +    --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
    9.43 +    "wellordered(M,A,r) == 
    9.44 +	transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
    9.45 +
    9.46 +
    9.47 +subsubsection {*Trivial absoluteness proofs*}
    9.48 +
    9.49 +lemma (in M_axioms) irreflexive_abs [simp]: 
    9.50 +     "M(A) ==> irreflexive(M,A,r) <-> irrefl(A,r)"
    9.51 +by (simp add: irreflexive_def irrefl_def)
    9.52 +
    9.53 +lemma (in M_axioms) transitive_rel_abs [simp]: 
    9.54 +     "M(A) ==> transitive_rel(M,A,r) <-> trans[A](r)"
    9.55 +by (simp add: transitive_rel_def trans_on_def)
    9.56 +
    9.57 +lemma (in M_axioms) linear_rel_abs [simp]: 
    9.58 +     "M(A) ==> linear_rel(M,A,r) <-> linear(A,r)"
    9.59 +by (simp add: linear_rel_def linear_def)
    9.60 +
    9.61 +lemma (in M_axioms) wellordered_is_trans_on: 
    9.62 +    "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
    9.63 +by (auto simp add: wellordered_def )
    9.64 +
    9.65 +lemma (in M_axioms) wellordered_is_linear: 
    9.66 +    "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
    9.67 +by (auto simp add: wellordered_def )
    9.68 +
    9.69 +lemma (in M_axioms) wellordered_is_wellfounded_on: 
    9.70 +    "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
    9.71 +by (auto simp add: wellordered_def )
    9.72 +
    9.73 +lemma (in M_axioms) wellfounded_imp_wellfounded_on: 
    9.74 +    "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
    9.75 +by (auto simp add: wellfounded_def wellfounded_on_def)
    9.76 +
    9.77 +
    9.78 +subsubsection {*Well-founded relations*}
    9.79 +
    9.80 +lemma  (in M_axioms) wellfounded_on_iff_wellfounded:
    9.81 +     "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
    9.82 +apply (simp add: wellfounded_on_def wellfounded_def, safe)
    9.83 + apply blast 
    9.84 +apply (drule_tac x=x in spec, blast) 
    9.85 +done
    9.86 +
    9.87 +lemma (in M_axioms) wellfounded_on_induct: 
    9.88 +     "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  
    9.89 +       separation(M, \<lambda>x. x\<in>A --> ~P(x));  
    9.90 +       \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |]
    9.91 +      ==> P(a)";
    9.92 +apply (simp (no_asm_use) add: wellfounded_on_def)
    9.93 +apply (drule_tac x="{z\<in>A. z\<in>A --> ~P(z)}" in spec)
    9.94 +apply (blast intro: transM) 
    9.95 +done
    9.96 +
    9.97 +text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
    9.98 +      hypothesis by removing the restriction to @{term A}.*}
    9.99 +lemma (in M_axioms) wellfounded_on_induct2: 
   9.100 +     "[| a\<in>A;  wellfounded_on(M,A,r);  M(A);  r \<subseteq> A*A;  
   9.101 +       separation(M, \<lambda>x. x\<in>A --> ~P(x));  
   9.102 +       \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
   9.103 +      ==> P(a)";
   9.104 +by (rule wellfounded_on_induct, assumption+, blast)
   9.105 +
   9.106 +
   9.107 +subsubsection {*Kunen's lemma IV 3.14, page 123*}
   9.108 +
   9.109 +lemma (in M_axioms) linear_imp_relativized: 
   9.110 +     "linear(A,r) ==> linear_rel(M,A,r)" 
   9.111 +by (simp add: linear_def linear_rel_def) 
   9.112 +
   9.113 +lemma (in M_axioms) trans_on_imp_relativized: 
   9.114 +     "trans[A](r) ==> transitive_rel(M,A,r)" 
   9.115 +by (unfold transitive_rel_def trans_on_def, blast) 
   9.116 +
   9.117 +lemma (in M_axioms) wf_on_imp_relativized: 
   9.118 +     "wf[A](r) ==> wellfounded_on(M,A,r)" 
   9.119 +apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify) 
   9.120 +apply (drule_tac x="x" in spec, blast) 
   9.121 +done
   9.122 +
   9.123 +lemma (in M_axioms) wf_imp_relativized: 
   9.124 +     "wf(r) ==> wellfounded(M,r)" 
   9.125 +apply (simp add: wellfounded_def wf_def, clarify) 
   9.126 +apply (drule_tac x="x" in spec, blast) 
   9.127 +done
   9.128 +
   9.129 +lemma (in M_axioms) well_ord_imp_relativized: 
   9.130 +     "well_ord(A,r) ==> wellordered(M,A,r)" 
   9.131 +by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
   9.132 +       linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
   9.133 +
   9.134 +
   9.135 +subsection{* Relativized versions of order-isomorphisms and order types *}
   9.136 +
   9.137 +lemma (in M_axioms) order_isomorphism_abs [simp]: 
   9.138 +     "[| M(A); M(B); M(f) |] 
   9.139 +      ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
   9.140 +by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed 
   9.141 +              order_isomorphism_def ord_iso_def)
   9.142 +
   9.143 +
   9.144 +lemma (in M_axioms) pred_set_abs [simp]: 
   9.145 +     "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
   9.146 +apply (simp add: pred_set_def Order.pred_def)
   9.147 +apply (blast dest: transM) 
   9.148 +done
   9.149 +
   9.150 +lemma (in M_axioms) pred_closed [intro]: 
   9.151 +     "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
   9.152 +apply (simp add: Order.pred_def) 
   9.153 +apply (insert pred_separation [of r x], simp, blast) 
   9.154 +done
   9.155 +
   9.156 +lemma (in M_axioms) membership_abs [simp]: 
   9.157 +     "[| M(r); M(A) |] ==> membership(M,A,r) <-> r = Memrel(A)"
   9.158 +apply (simp add: membership_def Memrel_def, safe)
   9.159 +  apply (rule equalityI) 
   9.160 +   apply clarify 
   9.161 +   apply (frule transM, assumption)
   9.162 +   apply blast
   9.163 +  apply clarify 
   9.164 +  apply (subgoal_tac "M(<xb,ya>)", blast) 
   9.165 +  apply (blast dest: transM) 
   9.166 + apply auto 
   9.167 +done
   9.168 +
   9.169 +lemma (in M_axioms) M_Memrel_iff:
   9.170 +     "M(A) ==> 
   9.171 +      Memrel(A) = {z \<in> A*A. \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> z = \<langle>x,y\<rangle> \<and> x \<in> y)}"
   9.172 +apply (simp add: Memrel_def) 
   9.173 +apply (blast dest: transM)
   9.174 +done 
   9.175 +
   9.176 +lemma (in M_axioms) Memrel_closed [intro]: 
   9.177 +     "M(A) ==> M(Memrel(A))"
   9.178 +apply (simp add: M_Memrel_iff) 
   9.179 +apply (insert Memrel_separation, simp, blast)
   9.180 +done
   9.181 +
   9.182 +
   9.183 +subsection {* Main results of Kunen, Chapter 1 section 6 *}
   9.184 +
   9.185 +text{*Subset properties-- proved outside the locale*}
   9.186 +
   9.187 +lemma linear_rel_subset: 
   9.188 +    "[| linear_rel(M,A,r);  B<=A |] ==> linear_rel(M,B,r)"
   9.189 +by (unfold linear_rel_def, blast)
   9.190 +
   9.191 +lemma transitive_rel_subset: 
   9.192 +    "[| transitive_rel(M,A,r);  B<=A |] ==> transitive_rel(M,B,r)"
   9.193 +by (unfold transitive_rel_def, blast)
   9.194 +
   9.195 +lemma wellfounded_on_subset: 
   9.196 +    "[| wellfounded_on(M,A,r);  B<=A |] ==> wellfounded_on(M,B,r)"
   9.197 +by (unfold wellfounded_on_def subset_def, blast)
   9.198 +
   9.199 +lemma wellordered_subset: 
   9.200 +    "[| wellordered(M,A,r);  B<=A |] ==> wellordered(M,B,r)"
   9.201 +apply (unfold wellordered_def)
   9.202 +apply (blast intro: linear_rel_subset transitive_rel_subset 
   9.203 +		    wellfounded_on_subset)
   9.204 +done
   9.205 +
   9.206 +text{*Inductive argument for Kunen's Lemma 6.1, etc.
   9.207 +      Simple proof from Halmos, page 72*}
   9.208 +lemma  (in M_axioms) wellordered_iso_subset_lemma: 
   9.209 +     "[| wellordered(M,A,r);  f \<in> ord_iso(A,r, A',r);  A'<= A;  y \<in> A;  
   9.210 +       M(A);  M(f);  M(r) |] ==> ~ <f`y, y> \<in> r"
   9.211 +apply (unfold wellordered_def ord_iso_def)
   9.212 +apply (elim conjE CollectE) 
   9.213 +apply (erule wellfounded_on_induct, assumption+)
   9.214 + apply (insert well_ord_iso_separation [of A f r])
   9.215 + apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify) 
   9.216 +apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
   9.217 +done
   9.218 +
   9.219 +
   9.220 +text{*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
   9.221 +      of a well-ordering*}
   9.222 +lemma (in M_axioms) wellordered_iso_predD:
   9.223 +     "[| wellordered(M,A,r);  f \<in> ord_iso(A, r, Order.pred(A,x,r), r);  
   9.224 +       M(A);  M(f);  M(r) |] ==> x \<notin> A"
   9.225 +apply (rule notI) 
   9.226 +apply (frule wellordered_iso_subset_lemma, assumption)
   9.227 +apply (auto elim: predE)  
   9.228 +(*Now we know  ~ (f`x < x) *)
   9.229 +apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
   9.230 +(*Now we also know f`x  \<in> pred(A,x,r);  contradiction! *)
   9.231 +apply (simp add: Order.pred_def)
   9.232 +done
   9.233 +
   9.234 +
   9.235 +lemma (in M_axioms) wellordered_iso_pred_eq_lemma:
   9.236 +     "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
   9.237 +       wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
   9.238 +apply (frule wellordered_is_trans_on, assumption)
   9.239 +apply (rule notI) 
   9.240 +apply (drule_tac x2=y and x=x and r2=r in 
   9.241 +         wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD]) 
   9.242 +apply (simp add: trans_pred_pred_eq) 
   9.243 +apply (blast intro: predI dest: transM)+
   9.244 +done
   9.245 +
   9.246 +
   9.247 +text{*Simple consequence of Lemma 6.1*}
   9.248 +lemma (in M_axioms) wellordered_iso_pred_eq:
   9.249 +     "[| wellordered(M,A,r);
   9.250 +       f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);   
   9.251 +       M(A);  M(f);  M(r);  a\<in>A;  c\<in>A |] ==> a=c"
   9.252 +apply (frule wellordered_is_trans_on, assumption)
   9.253 +apply (frule wellordered_is_linear, assumption)
   9.254 +apply (erule_tac x=a and y=c in linearE, auto) 
   9.255 +apply (drule ord_iso_sym)
   9.256 +(*two symmetric cases*)
   9.257 +apply (blast dest: wellordered_iso_pred_eq_lemma)+ 
   9.258 +done
   9.259 +
   9.260 +lemma (in M_axioms) wellfounded_on_asym:
   9.261 +     "[| wellfounded_on(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   9.262 +apply (simp add: wellfounded_on_def) 
   9.263 +apply (drule_tac x="{x,a}" in spec) 
   9.264 +apply (simp add: cons_closed) 
   9.265 +apply (blast dest: transM) 
   9.266 +done
   9.267 +
   9.268 +lemma (in M_axioms) wellordered_asym:
   9.269 +     "[| wellordered(M,A,r);  <a,x>\<in>r;  a\<in>A; x\<in>A;  M(A) |] ==> <x,a>\<notin>r"
   9.270 +by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
   9.271 +
   9.272 +
   9.273 +text{*Surely a shorter proof using lemmas in @{text Order}?
   9.274 +     Like well_ord_iso_preserving?*}
   9.275 +lemma (in M_axioms) ord_iso_pred_imp_lt:
   9.276 +     "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
   9.277 +       g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
   9.278 +       wellordered(M,A,r);  x \<in> A;  y \<in> A; M(A); M(r); M(f); M(g); M(j);
   9.279 +       Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
   9.280 +      ==> i < j"
   9.281 +apply (frule wellordered_is_trans_on, assumption)
   9.282 +apply (frule_tac y=y in transM, assumption) 
   9.283 +apply (rule_tac i=i and j=j in Ord_linear_lt, auto)  
   9.284 +txt{*case @{term "i=j"} yields a contradiction*}
   9.285 + apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in 
   9.286 +          wellordered_iso_predD [THEN notE]) 
   9.287 +   apply (blast intro: wellordered_subset [OF _ pred_subset]) 
   9.288 +  apply (simp add: trans_pred_pred_eq)
   9.289 +  apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
   9.290 + apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
   9.291 +txt{*case @{term "j<i"} also yields a contradiction*}
   9.292 +apply (frule restrict_ord_iso2, assumption+) 
   9.293 +apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
   9.294 +apply (frule apply_type, blast intro: ltD) 
   9.295 +  --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
   9.296 +apply (simp add: pred_iff) 
   9.297 +apply (subgoal_tac
   9.298 +       "\<exists>h. M(h) & h \<in> ord_iso(Order.pred(A,y,r), r, 
   9.299 +                               Order.pred(A, converse(f)`j, r), r)")
   9.300 + apply (clarify, frule wellordered_iso_pred_eq, assumption+)
   9.301 + apply (blast dest: wellordered_asym)  
   9.302 +apply (intro exI conjI) 
   9.303 + prefer 2 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
   9.304 +done
   9.305 +
   9.306 +
   9.307 +lemma ord_iso_converse1:
   9.308 +     "[| f: ord_iso(A,r,B,s);  <b, f`a>: s;  a:A;  b:B |] 
   9.309 +      ==> <converse(f) ` b, a> : r"
   9.310 +apply (frule ord_iso_converse, assumption+) 
   9.311 +apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype]) 
   9.312 +apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
   9.313 +done
   9.314 +
   9.315 +
   9.316 +subsection {* Order Types: A Direct Construction by Replacement*}
   9.317 +
   9.318 +text{*This follows Kunen's Theorem I 7.6, page 17.*}
   9.319 +
   9.320 +constdefs
   9.321 +  
   9.322 +  obase :: "[i=>o,i,i,i] => o"
   9.323 +       --{*the domain of @{text om}, eventually shown to equal @{text A}*}
   9.324 +   "obase(M,A,r,z) == 
   9.325 +	\<forall>a. M(a) --> 
   9.326 +         (a \<in> z <-> 
   9.327 +          (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
   9.328 +                               membership(M,x,mx) & pred_set(M,A,a,r,par) &  
   9.329 +                               order_isomorphism(M,par,r,x,mx,g))))"
   9.330 +
   9.331 +
   9.332 +  omap :: "[i=>o,i,i,i] => o"  
   9.333 +    --{*the function that maps wosets to order types*}
   9.334 +   "omap(M,A,r,f) == 
   9.335 +	\<forall>z. M(z) --> 
   9.336 +         (z \<in> f <-> 
   9.337 +          (\<exists>a\<in>A. M(a) & 
   9.338 +           (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) & 
   9.339 +                         pair(M,a,x,z) & membership(M,x,mx) & 
   9.340 +                         pred_set(M,A,a,r,par) &  
   9.341 +                         order_isomorphism(M,par,r,x,mx,g))))"
   9.342 +
   9.343 +
   9.344 +  otype :: "[i=>o,i,i,i] => o"  --{*the order types themselves*}
   9.345 +   "otype(M,A,r,i) == \<exists>f. M(f) & omap(M,A,r,f) & is_range(M,f,i)"
   9.346 +
   9.347 +
   9.348 +
   9.349 +lemma (in M_axioms) obase_iff:
   9.350 +     "[| M(A); M(r); M(z) |] 
   9.351 +      ==> obase(M,A,r,z) <-> 
   9.352 +          z = {a\<in>A. \<exists>x g. M(x) & M(g) & Ord(x) & 
   9.353 +                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
   9.354 +apply (simp add: obase_def Memrel_closed pred_closed)
   9.355 +apply (rule iffI) 
   9.356 + prefer 2 apply blast 
   9.357 +apply (rule equalityI) 
   9.358 + apply (clarify, frule transM, assumption, rotate_tac -1, simp) 
   9.359 +apply (clarify, frule transM, assumption, force)
   9.360 +done
   9.361 +
   9.362 +text{*Can also be proved with the premise @{term "M(z)"} instead of
   9.363 +      @{term "M(f)"}, but that version is less useful.*}
   9.364 +lemma (in M_axioms) omap_iff:
   9.365 +     "[| omap(M,A,r,f); M(A); M(r); M(f) |] 
   9.366 +      ==> z \<in> f <->
   9.367 +      (\<exists>a\<in>A. \<exists>x g. M(x) & M(g) & z = <a,x> & Ord(x) & 
   9.368 +                   g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
   9.369 +apply (rotate_tac 1) 
   9.370 +apply (simp add: omap_def Memrel_closed pred_closed) 
   9.371 +apply (rule iffI) 
   9.372 +apply (drule_tac x=z in spec, blast dest: transM)+ 
   9.373 +done
   9.374 +
   9.375 +lemma (in M_axioms) omap_unique:
   9.376 +     "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f" 
   9.377 +apply (rule equality_iffI) 
   9.378 +apply (simp add: omap_iff) 
   9.379 +done
   9.380 +
   9.381 +lemma (in M_axioms) omap_yields_Ord:
   9.382 +     "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |]  ==> Ord(x)"
   9.383 +apply (simp add: omap_def, blast) 
   9.384 +done
   9.385 +
   9.386 +lemma (in M_axioms) otype_iff:
   9.387 +     "[| otype(M,A,r,i); M(A); M(r); M(i) |] 
   9.388 +      ==> x \<in> i <-> 
   9.389 +          (\<exists>a\<in>A. \<exists>g. M(x) & M(g) & Ord(x) & 
   9.390 +                     g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
   9.391 +apply (simp add: otype_def, auto)
   9.392 +  apply (blast dest: transM)
   9.393 + apply (blast dest!: omap_iff intro: transM)
   9.394 +apply (rename_tac a g) 
   9.395 +apply (rule_tac a=a in rangeI) 
   9.396 +apply (frule transM, assumption)
   9.397 +apply (simp add: omap_iff, blast)
   9.398 +done
   9.399 +
   9.400 +lemma (in M_axioms) otype_eq_range:
   9.401 +     "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] ==> i = range(f)"
   9.402 +apply (auto simp add: otype_def omap_iff)
   9.403 +apply (blast dest: omap_unique) 
   9.404 +done
   9.405 +
   9.406 +
   9.407 +lemma (in M_axioms) Ord_otype:
   9.408 +     "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
   9.409 +apply (rotate_tac 1) 
   9.410 +apply (rule OrdI) 
   9.411 +prefer 2 
   9.412 +    apply (simp add: Ord_def otype_def omap_def) 
   9.413 +    apply clarify 
   9.414 +    apply (frule pair_components_in_M, assumption) 
   9.415 +    apply blast 
   9.416 +apply (auto simp add: Transset_def otype_iff) 
   9.417 + apply (blast intro: transM)
   9.418 +apply (rename_tac y a g)
   9.419 +apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun, 
   9.420 +			  THEN apply_funtype],  assumption)  
   9.421 +apply (rule_tac x="converse(g)`y" in bexI)
   9.422 + apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption) 
   9.423 +apply (safe elim!: predE) 
   9.424 +apply (intro conjI exI) 
   9.425 +prefer 3
   9.426 +  apply (blast intro: restrict_ord_iso ord_iso_sym ltI)
   9.427 + apply (blast intro: transM)
   9.428 + apply (blast intro: Ord_in_Ord)
   9.429 +done
   9.430 +
   9.431 +lemma (in M_axioms) domain_omap:
   9.432 +     "[| omap(M,A,r,f);  obase(M,A,r,B); M(A); M(r); M(B); M(f) |] 
   9.433 +      ==> domain(f) = B"
   9.434 +apply (rotate_tac 2) 
   9.435 +apply (simp add: domain_closed obase_iff) 
   9.436 +apply (rule equality_iffI) 
   9.437 +apply (simp add: domain_iff omap_iff, blast) 
   9.438 +done
   9.439 +
   9.440 +lemma (in M_axioms) omap_subset: 
   9.441 +     "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   9.442 +       M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
   9.443 +apply (rotate_tac 3, clarify) 
   9.444 +apply (simp add: omap_iff obase_iff) 
   9.445 +apply (force simp add: otype_iff) 
   9.446 +done
   9.447 +
   9.448 +lemma (in M_axioms) omap_funtype: 
   9.449 +     "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   9.450 +       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
   9.451 +apply (rotate_tac 3) 
   9.452 +apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff) 
   9.453 +apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans) 
   9.454 +done
   9.455 +
   9.456 +
   9.457 +lemma (in M_axioms) wellordered_omap_bij:
   9.458 +     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   9.459 +       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)"
   9.460 +apply (insert omap_funtype [of A r f B i]) 
   9.461 +apply (auto simp add: bij_def inj_def) 
   9.462 +prefer 2  apply (blast intro: fun_is_surj dest: otype_eq_range) 
   9.463 +apply (frule_tac a="w" in apply_Pair, assumption) 
   9.464 +apply (frule_tac a="x" in apply_Pair, assumption) 
   9.465 +apply (simp add: omap_iff) 
   9.466 +apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans) 
   9.467 +done
   9.468 +
   9.469 +
   9.470 +text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
   9.471 +lemma (in M_axioms) omap_ord_iso:
   9.472 +     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   9.473 +       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(B,r,i,Memrel(i))"
   9.474 +apply (rule ord_isoI)
   9.475 + apply (erule wellordered_omap_bij, assumption+) 
   9.476 +apply (insert omap_funtype [of A r f B i], simp) 
   9.477 +apply (frule_tac a="x" in apply_Pair, assumption) 
   9.478 +apply (frule_tac a="y" in apply_Pair, assumption) 
   9.479 +apply (auto simp add: omap_iff)
   9.480 + txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
   9.481 + apply (blast intro: ltD ord_iso_pred_imp_lt)
   9.482 + txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
   9.483 +apply (rename_tac x y g ga) 
   9.484 +apply (frule wellordered_is_linear, assumption, 
   9.485 +       erule_tac x=x and y=y in linearE, assumption+) 
   9.486 +txt{*the case @{term "x=y"} leads to immediate contradiction*} 
   9.487 +apply (blast elim: mem_irrefl) 
   9.488 +txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
   9.489 +apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym) 
   9.490 +done
   9.491 +
   9.492 +lemma (in M_axioms) Ord_omap_image_pred:
   9.493 +     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   9.494 +       M(A); M(r); M(f); M(B); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
   9.495 +apply (frule wellordered_is_trans_on, assumption)
   9.496 +apply (rule OrdI) 
   9.497 +	prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast) 
   9.498 +txt{*Hard part is to show that the image is a transitive set.*}
   9.499 +apply (rotate_tac 3)
   9.500 +apply (simp add: Transset_def, clarify) 
   9.501 +apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]])
   9.502 +apply (rename_tac c j, clarify)
   9.503 +apply (frule omap_funtype [of A r f B, THEN apply_funtype], assumption+)
   9.504 +apply (subgoal_tac "j : i") 
   9.505 +	prefer 2 apply (blast intro: Ord_trans Ord_otype)
   9.506 +apply (subgoal_tac "converse(f) ` j : B") 
   9.507 +	prefer 2 
   9.508 +	apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij, 
   9.509 +                                      THEN bij_is_fun, THEN apply_funtype])
   9.510 +apply (rule_tac x="converse(f) ` j" in bexI) 
   9.511 + apply (simp add: right_inverse_bij [OF wellordered_omap_bij]) 
   9.512 +apply (intro predI conjI)
   9.513 + apply (erule_tac b=c in trans_onD) 
   9.514 + apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]])
   9.515 +apply (auto simp add: obase_iff)
   9.516 +done
   9.517 +
   9.518 +lemma (in M_axioms) restrict_omap_ord_iso:
   9.519 +     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i); 
   9.520 +       D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |] 
   9.521 +      ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
   9.522 +apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]], 
   9.523 +       assumption+)
   9.524 +apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel]) 
   9.525 +apply (blast dest: subsetD [OF omap_subset]) 
   9.526 +apply (drule ord_iso_sym, simp) 
   9.527 +done
   9.528 +
   9.529 +lemma (in M_axioms) obase_equals: 
   9.530 +     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
   9.531 +       M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
   9.532 +apply (rotate_tac 4)
   9.533 +apply (rule equalityI, force simp add: obase_iff, clarify) 
   9.534 +apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp) 
   9.535 +apply (frule wellordered_is_wellfounded_on, assumption)
   9.536 +apply (erule wellfounded_on_induct, assumption+)
   9.537 + apply (insert obase_equals_separation, simp add: Memrel_closed pred_closed, clarify) 
   9.538 +apply (rename_tac b) 
   9.539 +apply (subgoal_tac "Order.pred(A,b,r) <= B") 
   9.540 + prefer 2 apply (force simp add: pred_iff obase_iff)  
   9.541 +apply (intro conjI exI) 
   9.542 +    prefer 4 apply (blast intro: restrict_omap_ord_iso) 
   9.543 +apply (blast intro: Ord_omap_image_pred)+
   9.544 +done
   9.545 +
   9.546 +
   9.547 +
   9.548 +text{*Main result: @{term om} gives the order-isomorphism 
   9.549 +      @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
   9.550 +theorem (in M_axioms) omap_ord_iso_otype:
   9.551 +     "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
   9.552 +       M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
   9.553 +apply (frule omap_ord_iso, assumption+) 
   9.554 +apply (frule obase_equals, assumption+, blast) 
   9.555 +done
   9.556 +
   9.557 +lemma (in M_axioms) obase_exists:
   9.558 +     "[| M(A); M(r) |] ==> \<exists>z. M(z) & obase(M,A,r,z)"
   9.559 +apply (simp add: obase_def) 
   9.560 +apply (insert obase_separation [of A r])
   9.561 +apply (simp add: separation_def)  
   9.562 +done
   9.563 +
   9.564 +lemma (in M_axioms) omap_exists:
   9.565 +     "[| M(A); M(r) |] ==> \<exists>z. M(z) & omap(M,A,r,z)"
   9.566 +apply (insert obase_exists [of A r]) 
   9.567 +apply (simp add: omap_def) 
   9.568 +apply (insert omap_replacement [of A r])
   9.569 +apply (simp add: strong_replacement_def, clarify) 
   9.570 +apply (drule_tac x=z in spec, clarify) 
   9.571 +apply (simp add: Memrel_closed pred_closed obase_iff)
   9.572 +apply (erule impE) 
   9.573 + apply (clarsimp simp add: univalent_def)
   9.574 + apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)  
   9.575 +apply (rule_tac x=Y in exI) 
   9.576 +apply (simp add: Memrel_closed pred_closed obase_iff, blast)   
   9.577 +done
   9.578 +
   9.579 +lemma (in M_axioms) otype_exists:
   9.580 +     "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"
   9.581 +apply (insert omap_exists [of A r]) 
   9.582 +apply (simp add: otype_def, clarify) 
   9.583 +apply (rule_tac x="range(z)" in exI) 
   9.584 +apply blast 
   9.585 +done
   9.586 +
   9.587 +theorem (in M_axioms) omap_ord_iso_otype:
   9.588 +     "[| wellordered(M,A,r); M(A); M(r) |]
   9.589 +      ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   9.590 +apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   9.591 +apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
   9.592 +apply (rule Ord_otype) 
   9.593 +    apply (force simp add: otype_def range_closed) 
   9.594 +   apply (simp_all add: wellordered_is_trans_on) 
   9.595 +done
   9.596 +
   9.597 +lemma (in M_axioms) ordertype_exists:
   9.598 +     "[| wellordered(M,A,r); M(A); M(r) |]
   9.599 +      ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
   9.600 +apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
   9.601 +apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype) 
   9.602 +apply (rule Ord_otype) 
   9.603 +    apply (force simp add: otype_def range_closed) 
   9.604 +   apply (simp_all add: wellordered_is_trans_on) 
   9.605 +done
   9.606 +
   9.607 +
   9.608 +lemma (in M_axioms) relativized_imp_well_ord: 
   9.609 +     "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)" 
   9.610 +apply (insert ordertype_exists [of A r], simp)
   9.611 +apply (blast intro: well_ord_ord_iso well_ord_Memrel )  
   9.612 +done
   9.613 +
   9.614 +subsection {*Kunen's theorem 5.4, poage 127*}
   9.615 +
   9.616 +text{*(a) The notion of Wellordering is absolute*}
   9.617 +theorem (in M_axioms) well_ord_abs [simp]: 
   9.618 +     "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)" 
   9.619 +by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)  
   9.620 +
   9.621 +
   9.622 +text{*(b) Order types are absolute*}
   9.623 +lemma (in M_axioms) 
   9.624 +     "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
   9.625 +       M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
   9.626 +by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
   9.627 +                 Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
   9.628 +
   9.629 +end