--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Formula.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,1006 @@
+header {* First-Order Formulas and the Definition of the Class L *}
+
+theory Formula = Main:
+
+
+(*??for Bool.thy**)
+constdefs bool_of_o :: "o=>i"
+ "bool_of_o(P) == (if P then 1 else 0)"
+
+lemma [simp]: "bool_of_o(True) = 1"
+by (simp add: bool_of_o_def)
+
+lemma [simp]: "bool_of_o(False) = 0"
+by (simp add: bool_of_o_def)
+
+lemma [simp,TC]: "bool_of_o(P) \<in> bool"
+by (simp add: bool_of_o_def)
+
+lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+by (simp add: bool_of_o_def)
+
+lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+by (simp add: bool_of_o_def)
+
+(*????????????????Cardinal.ML*)
+lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
+by (blast intro: Finite_cons subset_Finite)
+
+lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
+by (simp add: succ_def)
+
+declare Finite_0 [simp]
+
+lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
+by (erule Finite_induct, simp_all)
+
+lemma Finite_RepFun_lemma [rule_format]:
+ "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|]
+ ==> \<forall>A. x = RepFun(A,f) --> Finite(A)"
+apply (erule Finite_induct)
+ apply clarify
+ apply (case_tac "A=0", simp)
+ apply (blast del: allE, clarify)
+apply (subgoal_tac "\<exists>z\<in>A. x = f(z)")
+ prefer 2 apply (blast del: allE elim: equalityE, clarify)
+apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
+ apply (blast intro: Diff_sing_Finite)
+apply (thin_tac "\<forall>A. ?P(A) --> Finite(A)")
+apply (rule equalityI)
+ apply (blast intro: elim: equalityE)
+apply (blast intro: elim: equalityCE)
+done
+
+text{*I don't know why, but if the premise is expressed using meta-connectives
+then the simplifier cannot prove it automatically in conditional rewriting.*}
+lemma Finite_RepFun_iff:
+ "(\<forall>x y. f(x)=f(y) --> x=y) ==> Finite(RepFun(A,f)) <-> Finite(A)"
+by (blast intro: Finite_RepFun Finite_RepFun_lemma [of _ f])
+
+lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
+apply (erule Finite_induct)
+apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
+done
+
+lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
+apply (subgoal_tac "Finite({{x} . x \<in> A})")
+ apply (simp add: Finite_RepFun_iff )
+apply (blast intro: subset_Finite)
+done
+
+lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) <-> Finite(A)"
+by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
+
+lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
+apply (erule nat_induct)
+ apply (simp add: Vfrom_0)
+apply (simp add: Vset_succ)
+done
+
+(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)
+text{*Every ordinal is exceeded by some limit ordinal.*}
+lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
+apply (rule_tac x="i ++ nat" in exI)
+apply (blast intro: oadd_LimitI oadd_lt_self Limit_nat [THEN Limit_has_0])
+done
+
+lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
+apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
+apply (simp add: Un_least_lt_iff)
+done
+
+
+
+(*Internalized formulas of FOL. De Bruijn representation.
+ Unbound variables get their denotations from an environment.*)
+
+consts formula :: i
+datatype
+ "formula" = Member ("x: nat", "y: nat")
+ | Equal ("x: nat", "y: nat")
+ | Neg ("p: formula")
+ | And ("p: formula", "q: formula")
+ | Forall ("p: formula")
+
+declare formula.intros [TC]
+
+constdefs Or :: "[i,i]=>i"
+ "Or(p,q) == Neg(And(Neg(p),Neg(q)))"
+
+constdefs Implies :: "[i,i]=>i"
+ "Implies(p,q) == Neg(And(p,Neg(q)))"
+
+constdefs Exists :: "i=>i"
+ "Exists(p) == Neg(Forall(Neg(p)))";
+
+lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
+by (simp add: Or_def)
+
+lemma Implies_type [TC]:
+ "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
+by (simp add: Implies_def)
+
+lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
+by (simp add: Exists_def)
+
+
+consts satisfies :: "[i,i]=>i"
+primrec (*explicit lambda is required because the environment varies*)
+ "satisfies(A,Member(x,y)) =
+ (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env)))"
+
+ "satisfies(A,Equal(x,y)) =
+ (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
+
+ "satisfies(A,Neg(p)) =
+ (\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"
+
+ "satisfies(A,And(p,q)) =
+ (\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"
+
+ "satisfies(A,Forall(p)) =
+ (\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
+
+
+lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
+by (induct_tac p, simp_all)
+
+syntax sats :: "[i,i,i] => o"
+translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
+
+lemma [simp]:
+ "env \<in> list(A)
+ ==> sats(A, Member(x,y), env) <-> nth(x,env) \<in> nth(y,env)"
+by simp
+
+lemma [simp]:
+ "env \<in> list(A)
+ ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
+by simp
+
+lemma sats_Neg_iff [simp]:
+ "env \<in> list(A)
+ ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
+by (simp add: Bool.not_def cond_def)
+
+lemma sats_And_iff [simp]:
+ "env \<in> list(A)
+ ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
+by (simp add: Bool.and_def cond_def)
+
+lemma sats_Forall_iff [simp]:
+ "env \<in> list(A)
+ ==> sats(A, Forall(p), env) <-> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
+by simp
+
+declare satisfies.simps [simp del];
+
+(**** DIVIDING LINE BETWEEN PRIMITIVE AND DERIVED CONNECTIVES ****)
+
+lemma sats_Or_iff [simp]:
+ "env \<in> list(A)
+ ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
+by (simp add: Or_def)
+
+lemma sats_Implies_iff [simp]:
+ "env \<in> list(A)
+ ==> (sats(A, Implies(p,q), env)) <-> (sats(A,p,env) --> sats(A,q,env))"
+apply (simp add: Implies_def, blast)
+done
+
+lemma sats_Exists_iff [simp]:
+ "env \<in> list(A)
+ ==> sats(A, Exists(p), env) <-> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
+by (simp add: Exists_def)
+
+
+
+
+(*pretty but unnecessary
+constdefs sat :: "[i,i] => o"
+ "sat(A,p) == satisfies(A,p)`[] = 1"
+
+syntax "_sat" :: "[i,i] => o" (infixl "|=" 50)
+translations "A |= p" == "sat(A,p)"
+
+lemma [simp]: "(A |= Neg(p)) <-> ~ (A |= p)"
+by (simp add: sat_def)
+
+lemma [simp]: "(A |= And(p,q)) <-> A|=p & A|=q"
+by (simp add: sat_def)
+*)
+
+
+constdefs incr_var :: "[i,i]=>i"
+ "incr_var(x,lev) == if x<lev then x else succ(x)"
+
+lemma incr_var_lt: "x<lev ==> incr_var(x,lev) = x"
+by (simp add: incr_var_def)
+
+lemma incr_var_le: "lev\<le>x ==> incr_var(x,lev) = succ(x)"
+apply (simp add: incr_var_def)
+apply (blast dest: lt_trans1)
+done
+
+consts incr_bv :: "i=>i"
+primrec
+ "incr_bv(Member(x,y)) =
+ (\<lambda>lev \<in> nat. Member (incr_var(x,lev), incr_var(y,lev)))"
+
+ "incr_bv(Equal(x,y)) =
+ (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
+
+ "incr_bv(Neg(p)) =
+ (\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"
+
+ "incr_bv(And(p,q)) =
+ (\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"
+
+ "incr_bv(Forall(p)) =
+ (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
+
+
+constdefs incr_boundvars :: "i => i"
+ "incr_boundvars(p) == incr_bv(p)`0"
+
+
+lemma [TC]: "x \<in> nat ==> incr_var(x,lev) \<in> nat"
+by (simp add: incr_var_def)
+
+lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
+by (induct_tac p, simp_all)
+
+lemma incr_boundvars_type [TC]: "p \<in> formula ==> incr_boundvars(p) \<in> formula"
+by (simp add: incr_boundvars_def)
+
+(*Obviously DPow is closed under complements and finite intersections and
+unions. Needs an inductive lemma to allow two lists of parameters to
+be combined.*)
+
+lemma sats_incr_bv_iff [rule_format]:
+ "[| p \<in> formula; env \<in> list(A); x \<in> A |]
+ ==> \<forall>bvs \<in> list(A).
+ sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) <->
+ sats(A, p, bvs@env)"
+apply (induct_tac p)
+apply (simp_all add: incr_var_def nth_append succ_lt_iff length_type)
+apply (auto simp add: diff_succ not_lt_iff_le)
+done
+
+(*UNUSED*)
+lemma sats_incr_boundvars_iff:
+ "[| p \<in> formula; env \<in> list(A); x \<in> A |]
+ ==> sats(A, incr_boundvars(p), Cons(x,env)) <-> sats(A, p, env)"
+apply (insert sats_incr_bv_iff [of p env A x Nil])
+apply (simp add: incr_boundvars_def)
+done
+
+(*UNUSED
+lemma formula_add_params [rule_format]:
+ "[| p \<in> formula; n \<in> nat |]
+ ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
+ length(bvs) = n -->
+ sats(A, iterates(incr_boundvars,n,p), bvs@env) <-> sats(A, p, env)"
+apply (induct_tac n, simp, clarify)
+apply (erule list.cases)
+apply (auto simp add: sats_incr_boundvars_iff)
+done
+*)
+
+consts arity :: "i=>i"
+primrec
+ "arity(Member(x,y)) = succ(x) \<union> succ(y)"
+
+ "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
+
+ "arity(Neg(p)) = arity(p)"
+
+ "arity(And(p,q)) = arity(p) \<union> arity(q)"
+
+ "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"
+
+
+lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
+by (induct_tac p, simp_all)
+
+lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Or_def)
+
+lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
+by (simp add: Implies_def)
+
+lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
+by (simp add: Exists_def)
+
+
+lemma arity_sats_iff [rule_format]:
+ "[| p \<in> formula; extra \<in> list(A) |]
+ ==> \<forall>env \<in> list(A).
+ arity(p) \<le> length(env) -->
+ sats(A, p, env @ extra) <-> sats(A, p, env)"
+apply (induct_tac p)
+apply (simp_all add: nth_append Un_least_lt_iff arity_type
+ split: split_nat_case3, auto)
+done
+
+lemma arity_sats1_iff:
+ "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
+ extra \<in> list(A) |]
+ ==> sats(A, p, Cons(x, env @ extra)) <-> sats(A, p, Cons(x, env))"
+apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
+apply simp
+done
+
+(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
+lemma incr_var_lemma:
+ "[| x \<in> nat; y \<in> nat; lev \<le> x |]
+ ==> succ(x) \<union> incr_var(y,lev) = succ(x \<union> y)"
+apply (simp add: incr_var_def Ord_Un_if, auto)
+ apply (blast intro: leI)
+ apply (simp add: not_lt_iff_le)
+ apply (blast intro: le_anti_sym)
+apply (blast dest: lt_trans2)
+done
+
+lemma incr_And_lemma:
+ "y < x ==> y \<union> succ(x) = succ(x \<union> y)"
+apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)
+apply (blast dest: lt_asym)
+done
+
+lemma arity_incr_bv_lemma [rule_format]:
+ "p \<in> formula
+ ==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =
+ (if n < arity(p) then succ(arity(p)) else arity(p))"
+apply (induct_tac p)
+apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
+ succ_Un_distrib [symmetric] incr_var_lt incr_var_le
+ Un_commute incr_var_lemma arity_type
+ split: split_nat_case3)
+(*left with the And case*)
+apply safe
+ apply (blast intro: incr_And_lemma lt_trans1)
+apply (subst incr_And_lemma)
+ apply (blast intro: lt_trans1)
+apply (simp add: Un_commute)
+done
+
+lemma arity_incr_boundvars_eq:
+ "p \<in> formula
+ ==> arity(incr_boundvars(p)) =
+ (if 0 < arity(p) then succ(arity(p)) else arity(p))"
+apply (insert arity_incr_bv_lemma [of p 0])
+apply (simp add: incr_boundvars_def)
+done
+
+lemma arity_iterates_incr_boundvars_eq:
+ "[| p \<in> formula; n \<in> nat |]
+ ==> arity(incr_boundvars^n(p)) =
+ (if 0 < arity(p) then n #+ arity(p) else arity(p))"
+apply (induct_tac n)
+apply (simp_all add: arity_incr_boundvars_eq not_lt_iff_le)
+done
+
+
+(**** TRYING INCR_BV1 AGAIN ****)
+
+constdefs incr_bv1 :: "i => i"
+ "incr_bv1(p) == incr_bv(p)`1"
+
+
+lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
+by (simp add: incr_bv1_def)
+
+(*For renaming all but the bound variable at level 0*)
+lemma sats_incr_bv1_iff [rule_format]:
+ "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
+ ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) <->
+ sats(A, p, Cons(x,env))"
+apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
+apply (simp add: incr_bv1_def)
+done
+
+lemma formula_add_params1 [rule_format]:
+ "[| p \<in> formula; n \<in> nat; x \<in> A |]
+ ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
+ length(bvs) = n -->
+ sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) <->
+ sats(A, p, Cons(x,env))"
+apply (induct_tac n, simp, clarify)
+apply (erule list.cases)
+apply (simp_all add: sats_incr_bv1_iff)
+done
+
+
+lemma arity_incr_bv1_eq:
+ "p \<in> formula
+ ==> arity(incr_bv1(p)) =
+ (if 1 < arity(p) then succ(arity(p)) else arity(p))"
+apply (insert arity_incr_bv_lemma [of p 1])
+apply (simp add: incr_bv1_def)
+done
+
+lemma arity_iterates_incr_bv1_eq:
+ "[| p \<in> formula; n \<in> nat |]
+ ==> arity(incr_bv1^n(p)) =
+ (if 1 < arity(p) then n #+ arity(p) else arity(p))"
+apply (induct_tac n)
+apply (simp_all add: arity_incr_bv1_eq )
+apply (simp add: not_lt_iff_le)
+apply (blast intro: le_trans add_le_self2 arity_type)
+done
+
+
+(*Definable powerset operation: Kunen's definition 1.1, page 165.*)
+constdefs DPow :: "i => i"
+ "DPow(A) == {X \<in> Pow(A).
+ \<exists>env \<in> list(A). \<exists>p \<in> formula.
+ arity(p) \<le> succ(length(env)) &
+ X = {x\<in>A. sats(A, p, Cons(x,env))}}"
+
+lemma DPowI:
+ "[|X <= A; env \<in> list(A); p \<in> formula;
+ arity(p) \<le> succ(length(env))|]
+ ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
+by (simp add: DPow_def, blast)
+
+lemma DPowD:
+ "X \<in> DPow(A)
+ ==> X <= A &
+ (\<exists>env \<in> list(A).
+ \<exists>p \<in> formula. arity(p) \<le> succ(length(env)) &
+ X = {x\<in>A. sats(A, p, Cons(x,env))})"
+by (simp add: DPow_def)
+
+lemmas DPow_imp_subset = DPowD [THEN conjunct1]
+
+(*Lemma 1.2*)
+lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |]
+ ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
+by (blast intro: DPowI)
+
+lemma DPow_subset_Pow: "DPow(A) <= Pow(A)"
+by (simp add: DPow_def, blast)
+
+lemma empty_in_DPow: "0 \<in> DPow(A)"
+apply (simp add: DPow_def)
+apply (rule_tac x="Nil" in bexI)
+ apply (rule_tac x="Neg(Equal(0,0))" in bexI)
+ apply (auto simp add: Un_least_lt_iff)
+done
+
+lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
+apply (simp add: DPow_def, clarify, auto)
+apply (rule bexI)
+ apply (rule_tac x="Neg(p)" in bexI)
+ apply auto
+done
+
+lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Int Y \<in> DPow(A)"
+apply (simp add: DPow_def, auto)
+apply (rename_tac envp p envq q)
+apply (rule_tac x="envp@envq" in bexI)
+ apply (rule_tac x="And(p, iterates(incr_bv1,length(envp),q))" in bexI)
+ apply typecheck
+apply (rule conjI)
+(*finally check the arity!*)
+ apply (simp add: arity_iterates_incr_bv1_eq length_app Un_least_lt_iff)
+ apply (force intro: add_le_self le_trans)
+apply (simp add: arity_sats1_iff formula_add_params1, blast)
+done
+
+lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X Un Y \<in> DPow(A)"
+apply (subgoal_tac "X Un Y = A - ((A-X) Int (A-Y))")
+apply (simp add: Int_in_DPow Compl_in_DPow)
+apply (simp add: DPow_def, blast)
+done
+
+lemma singleton_in_DPow: "x \<in> A ==> {x} \<in> DPow(A)"
+apply (simp add: DPow_def)
+apply (rule_tac x="Cons(x,Nil)" in bexI)
+ apply (rule_tac x="Equal(0,1)" in bexI)
+ apply typecheck
+apply (force simp add: succ_Un_distrib [symmetric])
+done
+
+lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
+apply (rule cons_eq [THEN subst])
+apply (blast intro: singleton_in_DPow Un_in_DPow)
+done
+
+(*Part of Lemma 1.3*)
+lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
+apply (erule Fin.induct)
+ apply (rule empty_in_DPow)
+apply (blast intro: cons_in_DPow)
+done
+
+(*DPow is not monotonic. For example, let A be some non-constructible set
+ of natural numbers, and let B be nat. Then A<=B and obviously A : DPow(A)
+ but A ~: DPow(B).*)
+lemma DPow_mono: "A : DPow(B) ==> DPow(A) <= DPow(B)"
+apply (simp add: DPow_def, auto)
+(*must use the formula defining A in B to relativize the new formula...*)
+oops
+
+lemma DPow_0: "DPow(0) = {0}"
+by (blast intro: empty_in_DPow dest: DPow_imp_subset)
+
+lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) <= DPow(A)"
+by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
+
+lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
+apply (rule equalityI)
+apply (rule DPow_subset_Pow)
+apply (erule Finite_Pow_subset_Pow)
+done
+
+(*This may be true but the proof looks difficult, requiring relativization
+lemma DPow_insert: "DPow (cons(a,A)) = DPow(A) Un {cons(a,X) . X: DPow(A)}"
+apply (rule equalityI, safe)
+oops
+*)
+
+subsection{* Constant Lset: Levels of the Constructible Universe *}
+
+constdefs Lset :: "i=>i"
+ "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
+
+text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
+lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
+by (subst Lset_def [THEN def_transrec], simp)
+
+lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
+by (subst Lset, blast)
+
+lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
+apply (insert Lset [of x])
+apply (blast intro: elim: equalityE)
+done
+
+subsubsection{* Transitivity *}
+
+lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)"
+apply (simp add: Transset_def DPow_def)
+apply (rule_tac x="[X]" in bexI)
+ apply (rule_tac x="Member(0,1)" in bexI)
+ apply (auto simp add: Un_least_lt_iff)
+done
+
+lemma Transset_subset_DPow: "Transset(A) ==> A <= DPow(A)"
+apply clarify
+apply (simp add: Transset_def)
+apply (blast intro: elem_subset_in_DPow)
+done
+
+lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
+apply (simp add: Transset_def)
+apply (blast intro: elem_subset_in_DPow dest: DPowD)
+done
+
+text{*Kunen's VI, 1.6 (a)*}
+lemma Transset_Lset: "Transset(Lset(i))"
+apply (rule_tac a=i in eps_induct)
+apply (subst Lset)
+apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
+done
+
+subsubsection{* Monotonicity *}
+
+text{*Kunen's VI, 1.6 (b)*}
+lemma Lset_mono [rule_format]:
+ "ALL j. i<=j --> Lset(i) <= Lset(j)"
+apply (rule_tac a=i in eps_induct)
+apply (rule impI [THEN allI])
+apply (subst Lset)
+apply (subst Lset, blast)
+done
+
+text{*This version lets us remove the premise @{term "Ord(i)"} sometimes.*}
+lemma Lset_mono_mem [rule_format]:
+ "ALL j. i:j --> Lset(i) <= Lset(j)"
+apply (rule_tac a=i in eps_induct)
+apply (rule impI [THEN allI])
+apply (subst Lset, auto)
+apply (rule rev_bexI, assumption)
+apply (blast intro: elem_subset_in_DPow dest: LsetD DPowD)
+done
+
+subsubsection{* 0, successor and limit equations fof Lset *}
+
+lemma Lset_0 [simp]: "Lset(0) = 0"
+by (subst Lset, blast)
+
+lemma Lset_succ_subset1: "DPow(Lset(i)) <= Lset(succ(i))"
+by (subst Lset, rule succI1 [THEN RepFunI, THEN Union_upper])
+
+lemma Lset_succ_subset2: "Lset(succ(i)) <= DPow(Lset(i))"
+apply (subst Lset, rule UN_least)
+apply (erule succE)
+ apply blast
+apply clarify
+apply (rule elem_subset_in_DPow)
+ apply (subst Lset)
+ apply blast
+apply (blast intro: dest: DPowD Lset_mono_mem)
+done
+
+lemma Lset_succ: "Lset(succ(i)) = DPow(Lset(i))"
+by (intro equalityI Lset_succ_subset1 Lset_succ_subset2)
+
+lemma Lset_Union [simp]: "Lset(\<Union>(X)) = (\<Union>y\<in>X. Lset(y))"
+apply (subst Lset)
+apply (rule equalityI)
+ txt{*first inclusion*}
+ apply (rule UN_least)
+ apply (erule UnionE)
+ apply (rule subset_trans)
+ apply (erule_tac [2] UN_upper, subst Lset, erule UN_upper)
+txt{*opposite inclusion*}
+apply (rule UN_least)
+apply (subst Lset, blast)
+done
+
+subsubsection{* Lset applied to Limit ordinals *}
+
+lemma Limit_Lset_eq:
+ "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
+by (simp add: Lset_Union [symmetric] Limit_Union_eq)
+
+lemma lt_LsetI: "[| a: Lset(j); j<i |] ==> a : Lset(i)"
+by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
+
+lemma Limit_LsetE:
+ "[| a: Lset(i); ~R ==> Limit(i);
+ !!x. [| x<i; a: Lset(x) |] ==> R
+ |] ==> R"
+apply (rule classical)
+apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
+ prefer 2 apply assumption
+ apply blast
+apply (blast intro: ltI Limit_is_Ord)
+done
+
+subsubsection{* Basic closure properties *}
+
+lemma zero_in_Lset: "y:x ==> 0 : Lset(x)"
+by (subst Lset, blast intro: empty_in_DPow)
+
+lemma notin_Lset: "x \<notin> Lset(x)"
+apply (rule_tac a=x in eps_induct)
+apply (subst Lset)
+apply (blast dest: DPowD)
+done
+
+
+
+text{*Kunen's VI, 1.9 (b)*}
+
+constdefs subset_fm :: "[i,i]=>i"
+ "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
+
+lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
+by (simp add: subset_fm_def)
+
+lemma arity_subset_fm [simp]:
+ "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
+by (simp add: subset_fm_def succ_Un_distrib [symmetric])
+
+lemma sats_subset_fm [simp]:
+ "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
+ ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \<subseteq> nth(y,env)"
+apply (frule lt_nat_in_nat, erule length_type)
+apply (simp add: subset_fm_def Transset_def)
+apply (blast intro: nth_type )
+done
+
+constdefs transset_fm :: "i=>i"
+ "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
+
+lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
+by (simp add: transset_fm_def)
+
+lemma arity_transset_fm [simp]:
+ "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
+by (simp add: transset_fm_def succ_Un_distrib [symmetric])
+
+lemma sats_transset_fm [simp]:
+ "[|x < length(env); env \<in> list(A); Transset(A)|]
+ ==> sats(A, transset_fm(x), env) <-> Transset(nth(x,env))"
+apply (frule lt_nat_in_nat, erule length_type)
+apply (simp add: transset_fm_def Transset_def)
+apply (blast intro: nth_type )
+done
+
+constdefs ordinal_fm :: "i=>i"
+ "ordinal_fm(x) ==
+ And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
+
+lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
+by (simp add: ordinal_fm_def)
+
+lemma arity_ordinal_fm [simp]:
+ "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
+by (simp add: ordinal_fm_def succ_Un_distrib [symmetric])
+
+lemma sats_ordinal_fm [simp]:
+ "[|x < length(env); env \<in> list(A); Transset(A)|]
+ ==> sats(A, ordinal_fm(x), env) <-> Ord(nth(x,env))"
+apply (frule lt_nat_in_nat, erule length_type)
+apply (simp add: ordinal_fm_def Ord_def Transset_def)
+apply (blast intro: nth_type )
+done
+
+text{*The subset consisting of the ordinals is definable.*}
+lemma Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
+apply (simp add: DPow_def Collect_subset)
+apply (rule_tac x="Nil" in bexI)
+ apply (rule_tac x="ordinal_fm(0)" in bexI)
+apply (simp_all add: sats_ordinal_fm)
+done
+
+lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
+apply (erule trans_induct3)
+ apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
+txt{*The successor case remains.*}
+apply (rule equalityI)
+txt{*First inclusion*}
+ apply clarify
+ apply (erule Ord_linear_lt, assumption)
+ apply (blast dest: DPow_imp_subset ltD notE [OF notin_Lset])
+ apply blast
+ apply (blast dest: ltD)
+txt{*Opposite inclusion, @{term "succ(x) \<subseteq> DPow(Lset(x)) \<inter> ON"}*}
+apply auto
+txt{*Key case: *}
+ apply (erule subst, rule Ords_in_DPow [OF Transset_Lset])
+ apply (blast intro: elem_subset_in_DPow dest: OrdmemD elim: equalityE)
+apply (blast intro: Ord_in_Ord)
+done
+
+
+lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
+by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
+
+lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
+apply (simp add: Lset_succ)
+apply (subst Ords_of_Lset_eq [symmetric], assumption,
+ rule Ords_in_DPow [OF Transset_Lset])
+done
+
+subsubsection{* Unions *}
+
+lemma Union_in_Lset:
+ "X \<in> Lset(j) ==> Union(X) \<in> Lset(succ(j))"
+apply (insert Transset_Lset)
+apply (rule LsetI [OF succI1])
+apply (simp add: Transset_def DPow_def)
+apply (intro conjI, blast)
+txt{*Now to create the formula @{term "\<exists>y. y \<in> X \<and> x \<in> y"} *}
+apply (rule_tac x="Cons(X,Nil)" in bexI)
+ apply (rule_tac x="Exists(And(Member(0,2), Member(1,0)))" in bexI)
+ apply typecheck
+apply (simp add: succ_Un_distrib [symmetric], blast)
+done
+
+lemma Union_in_LLimit:
+ "[| X: Lset(i); Limit(i) |] ==> Union(X) : Lset(i)"
+apply (rule Limit_LsetE, assumption+)
+apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset)
+done
+
+subsubsection{* Finite sets and ordered pairs *}
+
+lemma singleton_in_Lset: "a: Lset(i) ==> {a} : Lset(succ(i))"
+by (simp add: Lset_succ singleton_in_DPow)
+
+lemma doubleton_in_Lset:
+ "[| a: Lset(i); b: Lset(i) |] ==> {a,b} : Lset(succ(i))"
+by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
+
+lemma Pair_in_Lset:
+ "[| a: Lset(i); b: Lset(i); Ord(i) |] ==> <a,b> : Lset(succ(succ(i)))"
+apply (unfold Pair_def)
+apply (blast intro: doubleton_in_Lset)
+done
+
+lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
+
+lemma singleton_in_LLimit:
+ "[| a: Lset(i); Limit(i) |] ==> {a} : Lset(i)"
+apply (erule Limit_LsetE, assumption)
+apply (erule singleton_in_Lset [THEN lt_LsetI])
+apply (blast intro: Limit_has_succ)
+done
+
+lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
+lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
+
+text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
+lemma doubleton_in_LLimit:
+ "[| a: Lset(i); b: Lset(i); Limit(i) |] ==> {a,b} : Lset(i)"
+apply (erule Limit_LsetE, assumption)
+apply (erule Limit_LsetE, assumption)
+apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
+ Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
+done
+
+lemma Pair_in_LLimit:
+ "[| a: Lset(i); b: Lset(i); Limit(i) |] ==> <a,b> : Lset(i)"
+txt{*Infer that a, b occur at ordinals x,xa < i.*}
+apply (erule Limit_LsetE, assumption)
+apply (erule Limit_LsetE, assumption)
+txt{*Infer that succ(succ(x Un xa)) < i *}
+apply (blast intro: lt_Ord lt_LsetI [OF Pair_in_Lset]
+ Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
+done
+
+lemma product_LLimit: "Limit(i) ==> Lset(i) * Lset(i) <= Lset(i)"
+by (blast intro: Pair_in_LLimit)
+
+lemmas Sigma_subset_LLimit = subset_trans [OF Sigma_mono product_LLimit]
+
+lemma nat_subset_LLimit: "Limit(i) ==> nat \<subseteq> Lset(i)"
+by (blast dest: Ord_subset_Lset nat_le_Limit le_imp_subset Limit_is_Ord)
+
+lemma nat_into_LLimit: "[| n: nat; Limit(i) |] ==> n : Lset(i)"
+by (blast intro: nat_subset_LLimit [THEN subsetD])
+
+
+subsubsection{* Closure under disjoint union *}
+
+lemmas zero_in_LLimit = Limit_has_0 [THEN ltD, THEN zero_in_Lset, standard]
+
+lemma one_in_LLimit: "Limit(i) ==> 1 : Lset(i)"
+by (blast intro: nat_into_LLimit)
+
+lemma Inl_in_LLimit:
+ "[| a: Lset(i); Limit(i) |] ==> Inl(a) : Lset(i)"
+apply (unfold Inl_def)
+apply (blast intro: zero_in_LLimit Pair_in_LLimit)
+done
+
+lemma Inr_in_LLimit:
+ "[| b: Lset(i); Limit(i) |] ==> Inr(b) : Lset(i)"
+apply (unfold Inr_def)
+apply (blast intro: one_in_LLimit Pair_in_LLimit)
+done
+
+lemma sum_LLimit: "Limit(i) ==> Lset(i) + Lset(i) <= Lset(i)"
+by (blast intro!: Inl_in_LLimit Inr_in_LLimit)
+
+lemmas sum_subset_LLimit = subset_trans [OF sum_mono sum_LLimit]
+
+
+text{*The constructible universe and its rank function*}
+constdefs
+ L :: "i=>o" --{*Kunen's definition VI, 1.5, page 167*}
+ "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
+
+ lrank :: "i=>i" --{*Kunen's definition VI, 1.7*}
+ "lrank(x) == \<mu>i. x \<in> Lset(succ(i))"
+
+lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
+by (simp add: L_def, blast)
+
+lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
+by (simp add: L_def)
+
+lemma Ord_lrank [simp]: "Ord(lrank(a))"
+by (simp add: lrank_def)
+
+lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) --> lrank(x) < i"
+apply (erule trans_induct3)
+ apply simp
+ apply (simp only: lrank_def)
+ apply (blast intro: Least_le)
+apply (simp_all add: Limit_Lset_eq)
+apply (blast intro: ltI Limit_is_Ord lt_trans)
+done
+
+text{*Kunen's VI, 1.8, and the proof is much less trivial than the text
+would suggest. For a start it need the previous lemma, proved by induction.*}
+lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) <-> L(x) & lrank(x) < i"
+apply (simp add: L_def, auto)
+ apply (blast intro: Lset_lrank_lt)
+ apply (unfold lrank_def)
+apply (drule succI1 [THEN Lset_mono_mem, THEN subsetD])
+apply (drule_tac P="\<lambda>i. x \<in> Lset(succ(i))" in LeastI, assumption)
+apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
+done
+
+lemma Lset_succ_lrank_iff [simp]: "x \<in> Lset(succ(lrank(x))) <-> L(x)"
+by (simp add: Lset_iff_lrank_lt)
+
+text{*Kunen's VI, 1.9 (a)*}
+lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
+apply (unfold lrank_def)
+apply (rule Least_equality)
+ apply (erule Ord_in_Lset)
+ apply assumption
+apply (insert notin_Lset [of i])
+apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD])
+done
+
+text{*This is lrank(lrank(a)) = lrank(a) *}
+declare Ord_lrank [THEN lrank_of_Ord, simp]
+
+text{*Kunen's VI, 1.10 *}
+lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
+apply (simp add: Lset_succ DPow_def)
+apply (rule_tac x="Nil" in bexI)
+ apply (rule_tac x="Equal(0,0)" in bexI)
+apply auto
+done
+
+lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
+apply (unfold lrank_def)
+apply (rule Least_equality)
+ apply (rule Lset_in_Lset_succ)
+ apply assumption
+apply clarify
+apply (subgoal_tac "Lset(succ(ia)) <= Lset(i)")
+ apply (blast dest: mem_irrefl)
+apply (blast intro!: le_imp_subset Lset_mono)
+done
+
+text{*Kunen's VI, 1.11 *}
+lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) <= Vset(i)";
+apply (erule trans_induct)
+apply (subst Lset)
+apply (subst Vset)
+apply (rule UN_mono [OF subset_refl])
+apply (rule subset_trans [OF DPow_subset_Pow])
+apply (rule Pow_mono, blast)
+done
+
+text{*Kunen's VI, 1.12 *}
+lemma Lset_subset_Vset: "i \<in> nat ==> Lset(i) = Vset(i)";
+apply (erule nat_induct)
+ apply (simp add: Vfrom_0)
+apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
+done
+
+subsection{*For L to satisfy the ZF axioms*}
+
+lemma Union_in_L: "L(X) ==> L(Union(X))"
+apply (simp add: L_def, clarify)
+apply (drule Ord_imp_greater_Limit)
+apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord)
+done
+
+lemma doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
+apply (simp add: L_def, clarify)
+apply (drule Ord2_imp_greater_Limit, assumption)
+apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
+done
+
+subsubsection{*For L to satisfy Powerset *}
+
+lemma LPow_env_typing:
+ "[| y : Lset(i); Ord(i); y \<subseteq> X |] ==> y \<in> (\<Union>y\<in>Pow(X). Lset(succ(lrank(y))))"
+by (auto intro: L_I iff: Lset_succ_lrank_iff)
+
+lemma LPow_in_Lset:
+ "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
+apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
+apply simp
+apply (rule LsetI [OF succI1])
+apply (simp add: DPow_def)
+apply (intro conjI, clarify)
+apply (rule_tac a="x" in UN_I, simp+)
+txt{*Now to create the formula @{term "y \<subseteq> X"} *}
+apply (rule_tac x="Cons(X,Nil)" in bexI)
+ apply (rule_tac x="subset_fm(0,1)" in bexI)
+ apply typecheck
+apply (rule conjI)
+apply (simp add: succ_Un_distrib [symmetric])
+apply (rule equality_iffI)
+apply (simp add: Transset_UN [OF Transset_Lset] list.Cons [OF LPow_env_typing])
+apply (auto intro: L_I iff: Lset_succ_lrank_iff)
+done
+
+lemma LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
+by (blast intro: L_I dest: L_D LPow_in_Lset)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/L_axioms.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,129 @@
+header {* The class L satisfies the axioms of ZF*}
+
+theory L_axioms = Formula + Relative:
+
+
+text {* The class L satisfies the premises of locale @{text M_axioms} *}
+
+lemma transL: "[| y\<in>x; L(x) |] ==> L(y)"
+apply (insert Transset_Lset)
+apply (simp add: Transset_def L_def, blast)
+done
+
+lemma nonempty: "L(0)"
+apply (simp add: L_def)
+apply (blast intro: zero_in_Lset)
+done
+
+lemma upair_ax: "upair_ax(L)"
+apply (simp add: upair_ax_def upair_def, clarify)
+apply (rule_tac x="{x,y}" in exI)
+apply (simp add: doubleton_in_L)
+done
+
+lemma Union_ax: "Union_ax(L)"
+apply (simp add: Union_ax_def big_union_def, clarify)
+apply (rule_tac x="Union(x)" in exI)
+apply (simp add: Union_in_L, auto)
+apply (blast intro: transL)
+done
+
+lemma power_ax: "power_ax(L)"
+apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
+apply (rule_tac x="{y \<in> Pow(x). L(y)}" in exI)
+apply (simp add: LPow_in_L, auto)
+apply (blast intro: transL)
+done
+
+subsubsection{*For L to satisfy Replacement *}
+
+(*Can't move these to Formula unless the definition of univalent is moved
+there too!*)
+
+lemma LReplace_in_Lset:
+ "[|X \<in> Lset(i); univalent(L,X,Q); Ord(i)|]
+ ==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"
+apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"
+ in exI)
+apply simp
+apply clarify
+apply (rule_tac a="x" in UN_I)
+ apply (simp_all add: Replace_iff univalent_def)
+apply (blast dest: transL L_I)
+done
+
+lemma LReplace_in_L:
+ "[|L(X); univalent(L,X,Q)|]
+ ==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"
+apply (drule L_D, clarify)
+apply (drule LReplace_in_Lset, assumption+)
+apply (blast intro: L_I Lset_in_Lset_succ)
+done
+
+lemma replacement: "replacement(L,P)"
+apply (simp add: replacement_def, clarify)
+apply (frule LReplace_in_L, assumption+)
+apply clarify
+apply (rule_tac x=Y in exI)
+apply (simp add: Replace_iff univalent_def, blast)
+done
+
+end
+
+(*
+
+ and Inter_separation:
+ "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
+ and cartprod_separation:
+ "[| L(A); L(B) |]
+ ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
+ and image_separation:
+ "[| L(A); L(r) |]
+ ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
+ and vimage_separation:
+ "[| L(A); L(r) |]
+ ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
+ and converse_separation:
+ "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) &
+ pair(M,x,y,p) & pair(M,y,x,z)))"
+ and restrict_separation:
+ "L(A)
+ ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
+ and comp_separation:
+ "[| L(r); L(s) |]
+ ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
+ (\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) &
+ pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+ and pred_separation:
+ "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
+ and Memrel_separation:
+ "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
+ and obase_separation:
+ --{*part of the order type formalization*}
+ "[| L(A); L(r) |]
+ ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
+ ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
+ order_isomorphism(M,par,r,x,mx,g))"
+ and well_ord_iso_separation:
+ "[| L(A); L(f); L(r) |]
+ ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and>
+ fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+ and obase_equals_separation:
+ "[| L(A); L(r) |]
+ ==> separation
+ (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
+ ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
+ membership(M,y,my) & pred_set(M,A,x,r,pxr) &
+ order_isomorphism(M,pxr,r,y,my,g)))))"
+ and is_recfun_separation:
+ --{*for well-founded recursion. NEEDS RELATIVIZATION*}
+ "[| L(A); L(f); L(g); L(a); L(b) |]
+ ==> 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)"
+ and omap_replacement:
+ "[| L(A); L(r) |]
+ ==> strong_replacement(M,
+ \<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
+ ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
+ pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
+
+*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Normal.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,457 @@
+header {*Closed Unbounded Classes and Normal Functions*}
+
+theory Normal = Main:
+
+text{*
+One source is the book
+
+Frank R. Drake.
+\emph{Set Theory: An Introduction to Large Cardinals}.
+North-Holland, 1974.
+*}
+
+
+subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
+
+constdefs
+ Closed :: "(i=>o) => o"
+ "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
+
+ Unbounded :: "(i=>o) => o"
+ "Unbounded(P) == \<forall>i. Ord(i) --> (\<exists>j. i<j \<and> P(j))"
+
+ Closed_Unbounded :: "(i=>o) => o"
+ "Closed_Unbounded(P) == Closed(P) \<and> Unbounded(P)"
+
+
+subsubsection{*Simple facts about c.u. classes*}
+
+lemma ClosedI:
+ "[| !!I. [| I \<noteq> 0; \<forall>i\<in>I. Ord(i) \<and> P(i) |] ==> P(\<Union>(I)) |]
+ ==> Closed(P)"
+by (simp add: Closed_def)
+
+lemma ClosedD:
+ "[| Closed(P); I \<noteq> 0; !!i. i\<in>I ==> Ord(i); !!i. i\<in>I ==> P(i) |]
+ ==> P(\<Union>(I))"
+by (simp add: Closed_def)
+
+lemma UnboundedD:
+ "[| Unbounded(P); Ord(i) |] ==> \<exists>j. i<j \<and> P(j)"
+by (simp add: Unbounded_def)
+
+lemma Closed_Unbounded_imp_Unbounded: "Closed_Unbounded(C) ==> Unbounded(C)"
+by (simp add: Closed_Unbounded_def)
+
+
+text{*The universal class, V, is closed and unbounded.
+ A bit odd, since C. U. concerns only ordinals, but it's used below!*}
+theorem Closed_Unbounded_V [simp]: "Closed_Unbounded(\<lambda>x. True)"
+by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
+
+text{*The class of ordinals, @{term Ord}, is closed and unbounded.*}
+theorem Closed_Unbounded_Ord [simp]: "Closed_Unbounded(Ord)"
+by (unfold Closed_Unbounded_def Closed_def Unbounded_def, blast)
+
+text{*The class of limit ordinals, @{term Limit}, is closed and unbounded.*}
+theorem Closed_Unbounded_Limit [simp]: "Closed_Unbounded(Limit)"
+apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Limit_Union,
+ clarify)
+apply (rule_tac x="i++nat" in exI)
+apply (blast intro: oadd_lt_self oadd_LimitI Limit_nat Limit_has_0)
+done
+
+text{*The class of cardinals, @{term Card}, is closed and unbounded.*}
+theorem Closed_Unbounded_Card [simp]: "Closed_Unbounded(Card)"
+apply (simp add: Closed_Unbounded_def Closed_def Unbounded_def Card_Union)
+apply (blast intro: lt_csucc Card_csucc)
+done
+
+
+subsubsection{*The intersection of any set-indexed family of c.u. classes is
+ c.u.*}
+
+text{*The constructions below come from Kunen, \emph{Set Theory}, page 78.*}
+locale cub_family =
+ fixes P and A
+ fixes next_greater -- "the next ordinal satisfying class @{term A}"
+ fixes sup_greater -- "sup of those ordinals over all @{term A}"
+ assumes closed: "a\<in>A ==> Closed(P(a))"
+ and unbounded: "a\<in>A ==> Unbounded(P(a))"
+ and A_non0: "A\<noteq>0"
+ defines "next_greater(a,x) == \<mu>y. x<y \<and> P(a,y)"
+ and "sup_greater(x) == \<Union>a\<in>A. next_greater(a,x)"
+
+
+text{*Trivial that the intersection is closed.*}
+lemma (in cub_family) Closed_INT: "Closed(\<lambda>x. \<forall>i\<in>A. P(i,x))"
+by (blast intro: ClosedI ClosedD [OF closed])
+
+text{*All remaining effort goes to show that the intersection is unbounded.*}
+
+lemma (in cub_family) Ord_sup_greater:
+ "Ord(sup_greater(x))"
+by (simp add: sup_greater_def next_greater_def)
+
+lemma (in cub_family) Ord_next_greater:
+ "Ord(next_greater(a,x))"
+by (simp add: next_greater_def Ord_Least)
+
+text{*@{term next_greater} works as expected: it returns a larger value
+and one that belongs to class @{term "P(a)"}. *}
+lemma (in cub_family) next_greater_lemma:
+ "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x)) \<and> x < next_greater(a,x)"
+apply (simp add: next_greater_def)
+apply (rule exE [OF UnboundedD [OF unbounded]])
+ apply assumption+
+apply (blast intro: LeastI2 lt_Ord2)
+done
+
+lemma (in cub_family) next_greater_in_P:
+ "[| Ord(x); a\<in>A |] ==> P(a, next_greater(a,x))"
+by (blast dest: next_greater_lemma)
+
+lemma (in cub_family) next_greater_gt:
+ "[| Ord(x); a\<in>A |] ==> x < next_greater(a,x)"
+by (blast dest: next_greater_lemma)
+
+lemma (in cub_family) sup_greater_gt:
+ "Ord(x) ==> x < sup_greater(x)"
+apply (simp add: sup_greater_def)
+apply (insert A_non0)
+apply (blast intro: UN_upper_lt next_greater_gt Ord_next_greater)
+done
+
+lemma (in cub_family) next_greater_le_sup_greater:
+ "a\<in>A ==> next_greater(a,x) \<le> sup_greater(x)"
+apply (simp add: sup_greater_def)
+apply (blast intro: UN_upper_le Ord_next_greater)
+done
+
+lemma (in cub_family) omega_sup_greater_eq_UN:
+ "[| Ord(x); a\<in>A |]
+ ==> sup_greater^\<omega> (x) =
+ (\<Union>n\<in>nat. next_greater(a, sup_greater^n (x)))"
+apply (simp add: iterates_omega_def)
+apply (rule le_anti_sym)
+apply (rule le_implies_UN_le_UN)
+apply (blast intro: leI next_greater_gt Ord_iterates Ord_sup_greater)
+txt{*Opposite bound:
+@{subgoals[display,indent=0,margin=65]}
+*}
+apply (rule UN_least_le)
+apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+apply (rule_tac a="succ(n)" in UN_upper_le)
+apply (simp_all add: next_greater_le_sup_greater)
+apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+done
+
+lemma (in cub_family) P_omega_sup_greater:
+ "[| Ord(x); a\<in>A |] ==> P(a, sup_greater^\<omega> (x))"
+apply (simp add: omega_sup_greater_eq_UN)
+apply (rule ClosedD [OF closed])
+apply (blast intro: ltD, auto)
+apply (blast intro: Ord_iterates Ord_next_greater Ord_sup_greater)
+apply (blast intro: next_greater_in_P Ord_iterates Ord_sup_greater)
+done
+
+lemma (in cub_family) omega_sup_greater_gt:
+ "Ord(x) ==> x < sup_greater^\<omega> (x)"
+apply (simp add: iterates_omega_def)
+apply (rule UN_upper_lt [of 1], simp_all)
+ apply (blast intro: sup_greater_gt)
+apply (blast intro: Ord_UN Ord_iterates Ord_sup_greater)
+done
+
+lemma (in cub_family) Unbounded_INT: "Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
+apply (unfold Unbounded_def)
+apply (blast intro!: omega_sup_greater_gt P_omega_sup_greater)
+done
+
+lemma (in cub_family) Closed_Unbounded_INT:
+ "Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a,x))"
+by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT)
+
+
+theorem Closed_Unbounded_INT:
+ "(!!a. a\<in>A ==> Closed_Unbounded(P(a)))
+ ==> Closed_Unbounded(\<lambda>x. \<forall>a\<in>A. P(a, x))"
+apply (case_tac "A=0", simp)
+apply (rule cub_family.Closed_Unbounded_INT)
+apply (simp_all add: Closed_Unbounded_def)
+done
+
+lemma Int_iff_INT2:
+ "P(x) \<and> Q(x) <-> (\<forall>i\<in>2. (i=0 --> P(x)) \<and> (i=1 --> Q(x)))"
+by auto
+
+theorem Closed_Unbounded_Int:
+ "[| Closed_Unbounded(P); Closed_Unbounded(Q) |]
+ ==> Closed_Unbounded(\<lambda>x. P(x) \<and> Q(x))"
+apply (simp only: Int_iff_INT2)
+apply (rule Closed_Unbounded_INT, auto)
+done
+
+
+subsection {*Normal Functions*}
+
+constdefs
+ mono_le_subset :: "(i=>i) => o"
+ "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
+
+ mono_Ord :: "(i=>i) => o"
+ "mono_Ord(F) == \<forall>i j. i<j --> F(i) < F(j)"
+
+ cont_Ord :: "(i=>i) => o"
+ "cont_Ord(F) == \<forall>l. Limit(l) --> F(l) = (\<Union>i<l. F(i))"
+
+ Normal :: "(i=>i) => o"
+ "Normal(F) == mono_Ord(F) \<and> cont_Ord(F)"
+
+
+subsubsection{*Immediate properties of the definitions*}
+
+lemma NormalI:
+ "[|!!i j. i<j ==> F(i) < F(j); !!l. Limit(l) ==> F(l) = (\<Union>i<l. F(i))|]
+ ==> Normal(F)"
+by (simp add: Normal_def mono_Ord_def cont_Ord_def)
+
+lemma mono_Ord_imp_Ord: "[| Ord(i); mono_Ord(F) |] ==> Ord(F(i))"
+apply (simp add: mono_Ord_def)
+apply (blast intro: lt_Ord)
+done
+
+lemma mono_Ord_imp_mono: "[| i<j; mono_Ord(F) |] ==> F(i) < F(j)"
+by (simp add: mono_Ord_def)
+
+lemma Normal_imp_Ord [simp]: "[| Normal(F); Ord(i) |] ==> Ord(F(i))"
+by (simp add: Normal_def mono_Ord_imp_Ord)
+
+lemma Normal_imp_cont: "[| Normal(F); Limit(l) |] ==> F(l) = (\<Union>i<l. F(i))"
+by (simp add: Normal_def cont_Ord_def)
+
+lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
+by (simp add: Normal_def mono_Ord_def)
+
+lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
+apply (induct i rule: trans_induct3_rule)
+ apply (simp add: subset_imp_le)
+ apply (subgoal_tac "F(x) < F(succ(x))")
+ apply (force intro: lt_trans1)
+ apply (simp add: Normal_def mono_Ord_def)
+apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")
+ apply (simp add: Normal_imp_cont Limit_OUN_eq)
+apply (blast intro: ltD le_implies_OUN_le_OUN)
+done
+
+
+subsubsection{*The class of fixedpoints is closed and unbounded*}
+
+text{*The proof is from Drake, pages 113--114.*}
+
+lemma mono_Ord_imp_le_subset: "mono_Ord(F) ==> mono_le_subset(F)"
+apply (simp add: mono_le_subset_def, clarify)
+apply (subgoal_tac "F(i)\<le>F(j)", blast dest: le_imp_subset)
+apply (simp add: le_iff)
+apply (blast intro: lt_Ord2 mono_Ord_imp_Ord mono_Ord_imp_mono)
+done
+
+text{*The following equation is taken for granted in any set theory text.*}
+lemma cont_Ord_Union:
+ "[| cont_Ord(F); mono_le_subset(F); X=0 --> F(0)=0; \<forall>x\<in>X. Ord(x) |]
+ ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
+apply (frule Ord_set_cases)
+apply (erule disjE, force)
+apply (thin_tac "X=0 --> ?Q", auto)
+ txt{*The trival case of @{term "\<Union>X \<in> X"}*}
+ apply (rule equalityI, blast intro: Ord_Union_eq_succD)
+ apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff)
+ apply (blast elim: equalityE)
+txt{*The limit case, @{term "Limit(\<Union>X)"}:
+@{subgoals[display,indent=0,margin=65]}
+*}
+apply (simp add: OUN_Union_eq cont_Ord_def)
+apply (rule equalityI)
+txt{*First inclusion:*}
+ apply (rule UN_least [OF OUN_least])
+ apply (simp add: mono_le_subset_def, blast intro: leI)
+txt{*Second inclusion:*}
+apply (rule UN_least)
+apply (frule Union_upper_le, blast, blast intro: Ord_Union)
+apply (erule leE, drule ltD, elim UnionE)
+ apply (simp add: OUnion_def)
+ apply blast+
+done
+
+lemma Normal_Union:
+ "[| X\<noteq>0; \<forall>x\<in>X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\<Union>y\<in>X. F(y))"
+apply (simp add: Normal_def)
+apply (blast intro: mono_Ord_imp_le_subset cont_Ord_Union)
+done
+
+lemma Normal_imp_fp_Closed: "Normal(F) ==> Closed(\<lambda>i. F(i) = i)"
+apply (simp add: Closed_def ball_conj_distrib, clarify)
+apply (frule Ord_set_cases)
+apply (auto simp add: Normal_Union)
+done
+
+
+lemma iterates_Normal_increasing:
+ "[| n\<in>nat; x < F(x); Normal(F) |]
+ ==> F^n (x) < F^(succ(n)) (x)"
+apply (induct n rule: nat_induct)
+apply (simp_all add: Normal_imp_mono)
+done
+
+lemma Ord_iterates_Normal:
+ "[| n\<in>nat; Normal(F); Ord(x) |] ==> Ord(F^n (x))"
+by (simp add: Ord_iterates)
+
+text{*THIS RESULT IS UNUSED*}
+lemma iterates_omega_Limit:
+ "[| Normal(F); x < F(x) |] ==> Limit(F^\<omega> (x))"
+apply (frule lt_Ord)
+apply (simp add: iterates_omega_def)
+apply (rule increasing_LimitI)
+ --"this lemma is @{thm increasing_LimitI [no_vars]}"
+ apply (blast intro: UN_upper_lt [of "1"] Normal_imp_Ord
+ Ord_UN Ord_iterates lt_imp_0_lt
+ iterates_Normal_increasing)
+apply clarify
+apply (rule bexI)
+ apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal])
+apply (rule UN_I, erule nat_succI)
+apply (blast intro: iterates_Normal_increasing Ord_iterates_Normal
+ ltD [OF lt_trans1, OF succ_leI, OF ltI])
+done
+
+lemma iterates_omega_fixedpoint:
+ "[| Normal(F); Ord(a) |] ==> F(F^\<omega> (a)) = F^\<omega> (a)"
+apply (frule Normal_increasing, assumption)
+apply (erule leE)
+ apply (simp_all add: iterates_omega_triv [OF sym]) (*for subgoal 2*)
+apply (simp add: iterates_omega_def Normal_Union)
+apply (rule equalityI, force simp add: nat_succI)
+txt{*Opposite inclusion:
+@{subgoals[display,indent=0,margin=65]}
+*}
+apply clarify
+apply (rule UN_I, assumption)
+apply (frule iterates_Normal_increasing, assumption, assumption, simp)
+apply (blast intro: Ord_trans ltD Ord_iterates_Normal Normal_imp_Ord [of F])
+done
+
+lemma iterates_omega_increasing:
+ "[| Normal(F); Ord(a) |] ==> a \<le> F^\<omega> (a)"
+apply (unfold iterates_omega_def)
+apply (rule UN_upper_le [of 0], simp_all)
+done
+
+lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\<lambda>i. F(i) = i)"
+apply (unfold Unbounded_def, clarify)
+apply (rule_tac x="F^\<omega> (succ(i))" in exI)
+apply (simp add: iterates_omega_fixedpoint)
+apply (blast intro: lt_trans2 [OF _ iterates_omega_increasing])
+done
+
+
+theorem Normal_imp_fp_Closed_Unbounded:
+ "Normal(F) ==> Closed_Unbounded(\<lambda>i. F(i) = i)"
+by (simp add: Closed_Unbounded_def Normal_imp_fp_Closed
+ Normal_imp_fp_Unbounded)
+
+
+subsubsection{*Function @{text normalize}*}
+
+text{*Function @{text normalize} maps a function @{text F} to a
+ normal function that bounds it above. The result is normal if and
+ only if @{text F} is continuous: succ is not bounded above by any
+ normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
+*}
+constdefs
+ normalize :: "[i=>i, i] => i"
+ "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
+
+
+lemma Ord_normalize [simp, intro]:
+ "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
+apply (induct a rule: trans_induct3_rule)
+apply (simp_all add: ltD def_transrec2 [OF normalize_def])
+done
+
+lemma normalize_lemma [rule_format]:
+ "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |]
+ ==> \<forall>a. a < b --> normalize(F, a) < normalize(F, b)"
+apply (erule trans_induct3)
+ apply (simp_all add: le_iff def_transrec2 [OF normalize_def])
+ apply clarify
+apply (rule Un_upper2_lt)
+ apply auto
+ apply (drule spec, drule mp, assumption)
+ apply (erule leI)
+apply (drule Limit_has_succ, assumption)
+apply (blast intro!: Ord_normalize intro: OUN_upper_lt ltD lt_Ord)
+done
+
+lemma normalize_increasing:
+ "[| a < b; !!x. Ord(x) ==> Ord(F(x)) |]
+ ==> normalize(F, a) < normalize(F, b)"
+by (blast intro!: normalize_lemma intro: lt_Ord2)
+
+theorem Normal_normalize:
+ "(!!x. Ord(x) ==> Ord(F(x))) ==> Normal(normalize(F))"
+apply (rule NormalI)
+apply (blast intro!: normalize_increasing)
+apply (simp add: def_transrec2 [OF normalize_def])
+done
+
+theorem le_normalize:
+ "[| Ord(a); cont_Ord(F); !!x. Ord(x) ==> Ord(F(x)) |]
+ ==> F(a) \<le> normalize(F,a)"
+apply (erule trans_induct3)
+apply (simp_all add: def_transrec2 [OF normalize_def])
+apply (simp add: Un_upper1_le)
+apply (simp add: cont_Ord_def)
+apply (blast intro: ltD le_implies_OUN_le_OUN)
+done
+
+
+subsection {*The Alephs*}
+text {*This is the well-known transfinite enumeration of the cardinal
+numbers.*}
+
+constdefs
+ Aleph :: "i => i"
+ "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
+
+syntax (xsymbols)
+ Aleph :: "i => i" ("\<aleph>_" [90] 90)
+
+lemma Card_Aleph [simp, intro]:
+ "Ord(a) ==> Card(Aleph(a))"
+apply (erule trans_induct3)
+apply (simp_all add: Card_csucc Card_nat Card_is_Ord
+ def_transrec2 [OF Aleph_def])
+done
+
+lemma Aleph_lemma [rule_format]:
+ "Ord(b) ==> \<forall>a. a < b --> Aleph(a) < Aleph(b)"
+apply (erule trans_induct3)
+apply (simp_all add: le_iff def_transrec2 [OF Aleph_def])
+apply (blast intro: lt_trans lt_csucc Card_is_Ord, clarify)
+apply (drule Limit_has_succ, assumption)
+apply (blast intro: Card_is_Ord Card_Aleph OUN_upper_lt ltD lt_Ord)
+done
+
+lemma Aleph_increasing:
+ "a < b ==> Aleph(a) < Aleph(b)"
+by (blast intro!: Aleph_lemma intro: lt_Ord2)
+
+theorem Normal_Aleph: "Normal(Aleph)"
+apply (rule NormalI)
+apply (blast intro!: Aleph_increasing)
+apply (simp add: def_transrec2 [OF Aleph_def])
+done
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/ROOT.ML Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,4 @@
+use_thy "Reflection";
+use_thy "WFrec";
+use_thy "WF_extras";
+use_thy "L_axioms";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Reflection.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,321 @@
+header {* The Reflection Theorem*}
+
+theory Reflection = Normal:
+
+lemma all_iff_not_ex_not: "(\<forall>x. P(x)) <-> (~ (\<exists>x. ~ P(x)))";
+by blast
+
+lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) <-> (~ (\<exists>x\<in>A. ~ P(x)))";
+by blast
+
+text{*From the notes of A. S. Kechris, page 6, and from
+ Andrzej Mostowski, \emph{Constructible Sets with Applications},
+ North-Holland, 1969, page 23.*}
+
+
+subsection{*Basic Definitions*}
+
+text{*First part: the cumulative hierarchy defining the class @{text M}.
+To avoid handling multiple arguments, we assume that @{text "Mset(l)"} is
+closed under ordered pairing provided @{text l} is limit. Possibly this
+could be avoided: the induction hypothesis @{term Cl_reflects}
+(in locale @{text ex_reflection}) could be weakened to
+@{term "\<forall>y\<in>Mset(a). \<forall>z\<in>Mset(a). P(<y,z>) <-> Q(a,<y,z>)"}, removing most
+uses of @{term Pair_in_Mset}. But there isn't much point in doing so, since
+ultimately the @{text ex_reflection} proof is packaged up using the
+predicate @{text Reflects}.
+*}
+locale reflection =
+ fixes Mset and M and Reflects
+ assumes Mset_mono_le : "mono_le_subset(Mset)"
+ and Mset_cont : "cont_Ord(Mset)"
+ and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |]
+ ==> <x,y> \<in> Mset(a)"
+ defines "M(x) == \<exists>a. Ord(a) \<and> x \<in> Mset(a)"
+ and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) \<and>
+ (\<forall>a. Cl(a) --> (\<forall>x\<in>Mset(a). P(x) <-> Q(a,x)))"
+ fixes F0 --{*ordinal for a specific value @{term y}*}
+ fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
+ fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
+ defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) \<and> P(<y,z>)) -->
+ (\<exists>z\<in>Mset(b). P(<y,z>))"
+ and "FF(P) == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
+ and "ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(FF(P),a) = a"
+
+lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) <= Mset(j)"
+apply (insert Mset_mono_le)
+apply (simp add: mono_le_subset_def leI)
+done
+
+subsection{*Easy Cases of the Reflection Theorem*}
+
+theorem (in reflection) Triv_reflection [intro]:
+ "Reflects(Ord, P, \<lambda>a x. P(x))"
+by (simp add: Reflects_def)
+
+theorem (in reflection) Not_reflection [intro]:
+ "Reflects(Cl,P,Q) ==> Reflects(Cl, \<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x))"
+by (simp add: Reflects_def);
+
+theorem (in reflection) And_reflection [intro]:
+ "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
+ ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x),
+ \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+theorem (in reflection) Or_reflection [intro]:
+ "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
+ ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x),
+ \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+theorem (in reflection) Imp_reflection [intro]:
+ "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
+ ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a),
+ \<lambda>x. P(x) --> P'(x),
+ \<lambda>a x. Q(a,x) --> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+theorem (in reflection) Iff_reflection [intro]:
+ "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |]
+ ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a),
+ \<lambda>x. P(x) <-> P'(x),
+ \<lambda>a x. Q(a,x) <-> Q'(a,x))"
+by (simp add: Reflects_def Closed_Unbounded_Int, blast)
+
+subsection{*Reflection for Existential Quantifiers*}
+
+lemma (in reflection) F0_works:
+ "[| y\<in>Mset(a); Ord(a); M(z); P(<y,z>) |] ==> \<exists>z\<in>Mset(F0(P,y)). P(<y,z>)"
+apply (unfold F0_def M_def, clarify)
+apply (rule LeastI2)
+ apply (blast intro: Mset_mono [THEN subsetD])
+ apply (blast intro: lt_Ord2, blast)
+done
+
+lemma (in reflection) Ord_F0 [intro,simp]: "Ord(F0(P,y))"
+by (simp add: F0_def)
+
+lemma (in reflection) Ord_FF [intro,simp]: "Ord(FF(P,y))"
+by (simp add: FF_def)
+
+lemma (in reflection) cont_Ord_FF: "cont_Ord(FF(P))"
+apply (insert Mset_cont)
+apply (simp add: cont_Ord_def FF_def, blast)
+done
+
+text{*Recall that @{term F0} depends upon @{term "y\<in>Mset(a)"},
+while @{term FF} depends only upon @{term a}. *}
+lemma (in reflection) FF_works:
+ "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |] ==> \<exists>z\<in>Mset(FF(P,a)). P(<y,z>)"
+apply (simp add: FF_def)
+apply (simp_all add: cont_Ord_Union [of concl: Mset]
+ Mset_cont Mset_mono_le not_emptyI Ord_F0)
+apply (blast intro: F0_works)
+done
+
+lemma (in reflection) FFN_works:
+ "[| M(z); y\<in>Mset(a); P(<y,z>); Ord(a) |]
+ ==> \<exists>z\<in>Mset(normalize(FF(P),a)). P(<y,z>)"
+apply (drule FF_works [of concl: P], assumption+)
+apply (blast intro: cont_Ord_FF le_normalize [THEN Mset_mono, THEN subsetD])
+done
+
+
+text{*Locale for the induction hypothesis*}
+
+locale ex_reflection = reflection +
+ fixes P --"the original formula"
+ fixes Q --"the reflected formula"
+ fixes Cl --"the class of reflecting ordinals"
+ assumes Cl_reflects: "[| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x)"
+
+lemma (in ex_reflection) ClEx_downward:
+ "[| M(z); y\<in>Mset(a); P(<y,z>); Cl(a); ClEx(P,a) |]
+ ==> \<exists>z\<in>Mset(a). Q(a,<y,z>)"
+apply (simp add: ClEx_def, clarify)
+apply (frule Limit_is_Ord)
+apply (frule FFN_works [of concl: P], assumption+)
+apply (drule Cl_reflects, assumption+)
+apply (auto simp add: Limit_is_Ord Pair_in_Mset)
+done
+
+lemma (in ex_reflection) ClEx_upward:
+ "[| z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |]
+ ==> \<exists>z. M(z) \<and> P(<y,z>)"
+apply (simp add: ClEx_def M_def)
+apply (blast dest: Cl_reflects
+ intro: Limit_is_Ord Pair_in_Mset)
+done
+
+text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
+lemma (in ex_reflection) ZF_ClEx_iff:
+ "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |]
+ ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+by (blast intro: dest: ClEx_downward ClEx_upward)
+
+text{*...and it is closed and unbounded*}
+lemma (in ex_reflection) ZF_Closed_Unbounded_ClEx:
+ "Closed_Unbounded(ClEx(P))"
+apply (simp add: ClEx_def)
+apply (fast intro: Closed_Unbounded_Int Normal_imp_fp_Closed_Unbounded
+ Closed_Unbounded_Limit Normal_normalize)
+done
+
+text{*The same two theorems, exported to locale @{text reflection}.*}
+
+text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
+lemma (in reflection) ClEx_iff:
+ "[| y\<in>Mset(a); Cl(a); ClEx(P,a);
+ !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |]
+ ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
+apply (unfold ClEx_def FF_def F0_def M_def)
+apply (rule Reflection.ZF_ClEx_iff [of Mset Cl],
+ simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
+done
+
+lemma (in reflection) Closed_Unbounded_ClEx:
+ "(!!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x))
+ ==> Closed_Unbounded(ClEx(P))"
+apply (unfold ClEx_def FF_def F0_def M_def)
+apply (rule Reflection.ZF_Closed_Unbounded_ClEx,
+ simp_all add: Mset_mono_le Mset_cont Pair_in_Mset)
+done
+
+lemma (in reflection) Ex_reflection_0:
+ "Reflects(Cl,P0,Q0)
+ ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a),
+ \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>),
+ \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))"
+apply (simp add: Reflects_def)
+apply (intro conjI Closed_Unbounded_Int)
+ apply blast
+ apply (rule reflection.Closed_Unbounded_ClEx [of Cl P0 Q0], blast, clarify)
+apply (rule_tac Cl=Cl in ClEx_iff, assumption+, blast)
+done
+
+lemma (in reflection) All_reflection_0:
+ "Reflects(Cl,P0,Q0)
+ ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x.~P0(x), a),
+ \<lambda>x. \<forall>z. M(z) --> P0(<x,z>),
+ \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))"
+apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not)
+apply (rule Not_reflection, drule Not_reflection, simp)
+apply (erule Ex_reflection_0)
+done
+
+theorem (in reflection) Ex_reflection [intro]:
+ "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
+ ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a),
+ \<lambda>x. \<exists>z. M(z) \<and> P(x,z),
+ \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
+by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))"
+ "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
+
+theorem (in reflection) All_reflection [intro]:
+ "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
+ ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a),
+ \<lambda>x. \<forall>z. M(z) --> P(x,z),
+ \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))"
+by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))"
+ "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
+
+text{*No point considering bounded quantifiers, where reflection is trivial.*}
+
+
+subsection{*Simple Examples of Reflection*}
+
+text{*Example 1: reflecting a simple formula. The reflecting class is first
+given as the variable @{text ?Cl} and later retrieved from the final
+proof state.*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> x \<in> y,
+ \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
+by fast
+
+text{*Problem here: there needs to be a conjunction (class intersection)
+in the class of reflecting ordinals. The @{term "Ord(a)"} is redundant,
+though harmless.*}
+lemma (in reflection)
+ "Reflects(\<lambda>a. Ord(a) \<and> ClEx(\<lambda>x. fst(x) \<in> snd(x), a),
+ \<lambda>x. \<exists>y. M(y) \<and> x \<in> y,
+ \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
+by fast
+
+
+text{*Example 2*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
+ \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
+by fast
+
+text{*Example 2'. We give the reflecting class explicitly. *}
+lemma (in reflection)
+ "Reflects
+ (\<lambda>a. (Ord(a) \<and>
+ ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) \<and>
+ ClEx(\<lambda>x. \<forall>z. M(z) --> z \<subseteq> fst(x) --> z \<in> snd(x), a),
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
+ \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
+by fast
+
+text{*Example 2''. We expand the subset relation.*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
+ \<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)"
+by fast
+
+text{*Example 2'''. Single-step version, to reveal the reflecting class.*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y),
+ \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)"
+apply (rule Ex_reflection)
+txt{*
+@{goals[display,indent=0,margin=60]}
+*}
+apply (rule All_reflection)
+txt{*
+@{goals[display,indent=0,margin=60]}
+*}
+apply (rule Triv_reflection)
+txt{*
+@{goals[display,indent=0,margin=60]}
+*}
+done
+
+text{*Example 3. Warning: the following examples make sense only
+if @{term P} is quantifier-free, since it is not being relativized.*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<in> y <-> z \<in> x \<and> P(z)),
+ \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x \<and> P(z))"
+by fast
+
+text{*Example 3'*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> y = Collect(x,P),
+ \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
+by fast
+
+text{*Example 3''*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>x. \<exists>y. M(y) \<and> y = Replace(x,P),
+ \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
+by fast
+
+text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \<Pi>} needs
+to be relativized.*}
+lemma (in reflection)
+ "Reflects(?Cl,
+ \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) \<and> f \<in> (\<Pi>X \<in> A. X)),
+ \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
+by fast
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Relative.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,956 @@
+header {*Relativization and Absoluteness*}
+
+theory Relative = Main:
+
+subsection{* Relativized versions of standard set-theoretic concepts *}
+
+constdefs
+ empty :: "[i=>o,i] => o"
+ "empty(M,z) == \<forall>x. M(x) --> x \<notin> z"
+
+ subset :: "[i=>o,i,i] => o"
+ "subset(M,A,B) == \<forall>x\<in>A. M(x) --> x \<in> B"
+
+ upair :: "[i=>o,i,i,i] => o"
+ "upair(M,a,b,z) == a \<in> z & b \<in> z & (\<forall>x\<in>z. M(x) --> x = a | x = b)"
+
+ pair :: "[i=>o,i,i,i] => o"
+ "pair(M,a,b,z) == \<exists>x. M(x) & upair(M,a,a,x) &
+ (\<exists>y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))"
+
+ successor :: "[i=>o,i,i] => o"
+ "successor(M,a,z) == \<exists>x. M(x) & upair(M,a,a,x) & union(M,x,a,z)"
+
+ powerset :: "[i=>o,i,i] => o"
+ "powerset(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> subset(M,x,A))"
+
+ union :: "[i=>o,i,i,i] => o"
+ "union(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a | x \<in> b)"
+
+ inter :: "[i=>o,i,i,i] => o"
+ "inter(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<in> b)"
+
+ setdiff :: "[i=>o,i,i,i] => o"
+ "setdiff(M,a,b,z) == \<forall>x. M(x) --> (x \<in> z <-> x \<in> a & x \<notin> b)"
+
+ big_union :: "[i=>o,i,i] => o"
+ "big_union(M,A,z) == \<forall>x. M(x) --> (x \<in> z <-> (\<exists>y\<in>A. M(y) & x \<in> y))"
+
+ big_inter :: "[i=>o,i,i] => o"
+ "big_inter(M,A,z) ==
+ (A=0 --> z=0) &
+ (A\<noteq>0 --> (\<forall>x. M(x) --> (x \<in> z <-> (\<forall>y\<in>A. M(y) --> x \<in> y))))"
+
+ cartprod :: "[i=>o,i,i,i] => o"
+ "cartprod(M,A,B,z) ==
+ \<forall>u. M(u) --> (u \<in> z <-> (\<exists>x\<in>A. M(x) & (\<exists>y\<in>B. M(y) & pair(M,x,y,u))))"
+
+ is_converse :: "[i=>o,i,i] => o"
+ "is_converse(M,r,z) ==
+ \<forall>x. M(x) -->
+ (x \<in> z <->
+ (\<exists>w\<in>r. M(w) &
+ (\<exists>u v. M(u) & M(v) & pair(M,u,v,w) & pair(M,v,u,x))))"
+
+ pre_image :: "[i=>o,i,i,i] => o"
+ "pre_image(M,r,A,z) ==
+ \<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y\<in>A. M(y) & pair(M,x,y,w))))"
+
+ is_domain :: "[i=>o,i,i] => o"
+ "is_domain(M,r,z) ==
+ \<forall>x. M(x) --> (x \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>y. M(y) & pair(M,x,y,w))))"
+
+ image :: "[i=>o,i,i,i] => o"
+ "image(M,r,A,z) ==
+ \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x\<in>A. M(x) & pair(M,x,y,w))))"
+
+ is_range :: "[i=>o,i,i] => o"
+ --{*the cleaner
+ @{term "\<exists>r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"}
+ unfortunately needs an instance of separation in order to prove
+ @{term "M(converse(r))"}.*}
+ "is_range(M,r,z) ==
+ \<forall>y. M(y) --> (y \<in> z <-> (\<exists>w\<in>r. M(w) & (\<exists>x. M(x) & pair(M,x,y,w))))"
+
+ is_relation :: "[i=>o,i] => o"
+ "is_relation(M,r) ==
+ (\<forall>z\<in>r. M(z) --> (\<exists>x y. M(x) & M(y) & pair(M,x,y,z)))"
+
+ is_function :: "[i=>o,i] => o"
+ "is_function(M,r) ==
+ (\<forall>x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') -->
+ pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r -->
+ y=y')"
+
+ fun_apply :: "[i=>o,i,i,i] => o"
+ "fun_apply(M,f,x,y) ==
+ (\<forall>y'. M(y') --> ((\<exists>u\<in>f. M(u) & pair(M,x,y',u)) <-> y=y'))"
+
+ typed_function :: "[i=>o,i,i,i] => o"
+ "typed_function(M,A,B,r) ==
+ is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
+ (\<forall>u\<in>r. M(u) --> (\<forall>x y. M(x) & M(y) & pair(M,x,y,u) --> y\<in>B))"
+
+ injection :: "[i=>o,i,i,i] => o"
+ "injection(M,A,B,f) ==
+ typed_function(M,A,B,f) &
+ (\<forall>x x' y p p'. M(x) --> M(x') --> M(y) --> M(p) --> M(p') -->
+ pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f -->
+ x=x')"
+
+ surjection :: "[i=>o,i,i,i] => o"
+ "surjection(M,A,B,f) ==
+ typed_function(M,A,B,f) &
+ (\<forall>y\<in>B. M(y) --> (\<exists>x\<in>A. M(x) & fun_apply(M,f,x,y)))"
+
+ bijection :: "[i=>o,i,i,i] => o"
+ "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)"
+
+ restriction :: "[i=>o,i,i,i] => o"
+ "restriction(M,r,A,z) ==
+ \<forall>x. M(x) -->
+ (x \<in> z <->
+ (x \<in> r & (\<exists>u\<in>A. M(u) & (\<exists>v. M(v) & pair(M,u,v,x)))))"
+
+ transitive_set :: "[i=>o,i] => o"
+ "transitive_set(M,a) == \<forall>x\<in>a. M(x) --> subset(M,x,a)"
+
+ ordinal :: "[i=>o,i] => o"
+ --{*an ordinal is a transitive set of transitive sets*}
+ "ordinal(M,a) == transitive_set(M,a) & (\<forall>x\<in>a. M(x) --> transitive_set(M,x))"
+
+ limit_ordinal :: "[i=>o,i] => o"
+ --{*a limit ordinal is a non-empty, successor-closed ordinal*}
+ "limit_ordinal(M,a) ==
+ ordinal(M,a) & ~ empty(M,a) &
+ (\<forall>x\<in>a. M(x) --> (\<exists>y\<in>a. M(y) & successor(M,x,y)))"
+
+ successor_ordinal :: "[i=>o,i] => o"
+ --{*a successor ordinal is any ordinal that is neither empty nor limit*}
+ "successor_ordinal(M,a) ==
+ ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)"
+
+ finite_ordinal :: "[i=>o,i] => o"
+ --{*an ordinal is finite if neither it nor any of its elements are limit*}
+ "finite_ordinal(M,a) ==
+ ordinal(M,a) & ~ limit_ordinal(M,a) &
+ (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
+
+ omega :: "[i=>o,i] => o"
+ --{*omega is a limit ordinal none of whose elements are limit*}
+ "omega(M,a) == limit_ordinal(M,a) & (\<forall>x\<in>a. M(x) --> ~ limit_ordinal(M,x))"
+
+ number1 :: "[i=>o,i] => o"
+ "number1(M,a) == (\<exists>x. M(x) & empty(M,x) & successor(M,x,a))"
+
+ number2 :: "[i=>o,i] => o"
+ "number2(M,a) == (\<exists>x. M(x) & number1(M,x) & successor(M,x,a))"
+
+ number3 :: "[i=>o,i] => o"
+ "number3(M,a) == (\<exists>x. M(x) & number2(M,x) & successor(M,x,a))"
+
+
+subsection {*The relativized ZF axioms*}
+constdefs
+
+ extensionality :: "(i=>o) => o"
+ "extensionality(M) ==
+ \<forall>x y. M(x) --> M(y) --> (\<forall>z. M(z) --> (z \<in> x <-> z \<in> y)) --> x=y"
+
+ separation :: "[i=>o, i=>o] => o"
+ --{*Big problem: the formula @{text P} should only involve parameters
+ belonging to @{text M}. Don't see how to enforce that.*}
+ "separation(M,P) ==
+ \<forall>z. M(z) --> (\<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x))))"
+
+ upair_ax :: "(i=>o) => o"
+ "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z. M(z) & upair(M,x,y,z))"
+
+ Union_ax :: "(i=>o) => o"
+ "Union_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & big_union(M,x,z))"
+
+ power_ax :: "(i=>o) => o"
+ "power_ax(M) == \<forall>x. M(x) --> (\<exists>z. M(z) & powerset(M,x,z))"
+
+ univalent :: "[i=>o, i, [i,i]=>o] => o"
+ "univalent(M,A,P) ==
+ (\<forall>x\<in>A. M(x) --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
+
+ replacement :: "[i=>o, [i,i]=>o] => o"
+ "replacement(M,P) ==
+ \<forall>A. M(A) --> univalent(M,A,P) -->
+ (\<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y)))"
+
+ strong_replacement :: "[i=>o, [i,i]=>o] => o"
+ "strong_replacement(M,P) ==
+ \<forall>A. M(A) --> univalent(M,A,P) -->
+ (\<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b)))))"
+
+ foundation_ax :: "(i=>o) => o"
+ "foundation_ax(M) ==
+ \<forall>x. M(x) --> (\<exists>y\<in>x. M(y))
+ --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & z \<in> y))"
+
+
+subsection{*A trivial consistency proof for $V_\omega$ *}
+
+text{*We prove that $V_\omega$
+ (or @{text univ} in Isabelle) satisfies some ZF axioms.
+ Kunen, Theorem IV 3.13, page 123.*}
+
+lemma univ0_downwards_mem: "[| y \<in> x; x \<in> univ(0) |] ==> y \<in> univ(0)"
+apply (insert Transset_univ [OF Transset_0])
+apply (simp add: Transset_def, blast)
+done
+
+lemma univ0_Ball_abs [simp]:
+ "A \<in> univ(0) ==> (\<forall>x\<in>A. x \<in> univ(0) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
+by (blast intro: univ0_downwards_mem)
+
+lemma univ0_Bex_abs [simp]:
+ "A \<in> univ(0) ==> (\<exists>x\<in>A. x \<in> univ(0) & P(x)) <-> (\<exists>x\<in>A. P(x))"
+by (blast intro: univ0_downwards_mem)
+
+text{*Congruence rule for separation: can assume the variable is in @{text M}*}
+lemma [cong]:
+ "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M,P) <-> separation(M,P')"
+by (simp add: separation_def)
+
+text{*Congruence rules for replacement*}
+lemma [cong]:
+ "[| A=A'; !!x y. [| x\<in>A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
+ ==> univalent(M,A,P) <-> univalent(M,A',P')"
+by (simp add: univalent_def)
+
+lemma [cong]:
+ "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |]
+ ==> strong_replacement(M,P) <-> strong_replacement(M,P')"
+by (simp add: strong_replacement_def)
+
+text{*The extensionality axiom*}
+lemma "extensionality(\<lambda>x. x \<in> univ(0))"
+apply (simp add: extensionality_def)
+apply (blast intro: univ0_downwards_mem)
+done
+
+text{*The separation axiom requires some lemmas*}
+lemma Collect_in_Vfrom:
+ "[| X \<in> Vfrom(A,j); Transset(A) |] ==> Collect(X,P) \<in> Vfrom(A, succ(j))"
+apply (drule Transset_Vfrom)
+apply (rule subset_mem_Vfrom)
+apply (unfold Transset_def, blast)
+done
+
+lemma Collect_in_VLimit:
+ "[| X \<in> Vfrom(A,i); Limit(i); Transset(A) |]
+ ==> Collect(X,P) \<in> Vfrom(A,i)"
+apply (rule Limit_VfromE, assumption+)
+apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom)
+done
+
+lemma Collect_in_univ:
+ "[| X \<in> univ(A); Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
+by (simp add: univ_def Collect_in_VLimit Limit_nat)
+
+lemma "separation(\<lambda>x. x \<in> univ(0), P)"
+apply (simp add: separation_def)
+apply (blast intro: Collect_in_univ Transset_0)
+done
+
+text{*Unordered pairing axiom*}
+lemma "upair_ax(\<lambda>x. x \<in> univ(0))"
+apply (simp add: upair_ax_def upair_def)
+apply (blast intro: doubleton_in_univ)
+done
+
+text{*Union axiom*}
+lemma "Union_ax(\<lambda>x. x \<in> univ(0))"
+apply (simp add: Union_ax_def big_union_def)
+apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem)
+done
+
+text{*Powerset axiom*}
+
+lemma Pow_in_univ:
+ "[| X \<in> univ(A); Transset(A) |] ==> Pow(X) \<in> univ(A)"
+apply (simp add: univ_def Pow_in_VLimit Limit_nat)
+done
+
+lemma "power_ax(\<lambda>x. x \<in> univ(0))"
+apply (simp add: power_ax_def powerset_def subset_def)
+apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem)
+done
+
+text{*Foundation axiom*}
+lemma "foundation_ax(\<lambda>x. x \<in> univ(0))"
+apply (simp add: foundation_ax_def, clarify)
+apply (cut_tac A=x in foundation, blast)
+done
+
+lemma "replacement(\<lambda>x. x \<in> univ(0), P)"
+apply (simp add: replacement_def, clarify)
+oops
+text{*no idea: maybe prove by induction on the rank of A?*}
+
+text{*Still missing: Replacement, Choice*}
+
+subsection{*lemmas needed to reduce some set constructions to instances
+ of Separation*}
+
+lemma image_iff_Collect: "r `` A = {y \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>x\<in>A. p=<x,y>}"
+apply (rule equalityI, auto)
+apply (simp add: Pair_def, blast)
+done
+
+lemma vimage_iff_Collect:
+ "r -`` A = {x \<in> Union(Union(r)). \<exists>p\<in>r. \<exists>y\<in>A. p=<x,y>}"
+apply (rule equalityI, auto)
+apply (simp add: Pair_def, blast)
+done
+
+text{*These two lemmas lets us prove @{text domain_closed} and
+ @{text range_closed} without new instances of separation*}
+
+lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))"
+apply (rule equalityI, auto)
+apply (rule vimageI, assumption)
+apply (simp add: Pair_def, blast)
+done
+
+lemma range_eq_image: "range(r) = r `` Union(Union(r))"
+apply (rule equalityI, auto)
+apply (rule imageI, assumption)
+apply (simp add: Pair_def, blast)
+done
+
+lemma replacementD:
+ "[| replacement(M,P); M(A); univalent(M,A,P) |]
+ ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> ((\<exists>x\<in>A. M(x) & P(x,b)) --> b \<in> Y))"
+by (simp add: replacement_def)
+
+lemma strong_replacementD:
+ "[| strong_replacement(M,P); M(A); univalent(M,A,P) |]
+ ==> \<exists>Y. M(Y) & (\<forall>b. M(b) --> (b \<in> Y <-> (\<exists>x\<in>A. M(x) & P(x,b))))"
+by (simp add: strong_replacement_def)
+
+lemma separationD:
+ "[| separation(M,P); M(z) |]
+ ==> \<exists>y. M(y) & (\<forall>x. M(x) --> (x \<in> y <-> x \<in> z & P(x)))"
+by (simp add: separation_def)
+
+
+text{*More constants, for order types*}
+constdefs
+
+ order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
+ "order_isomorphism(M,A,r,B,s,f) ==
+ bijection(M,A,B,f) &
+ (\<forall>x\<in>A. \<forall>y\<in>A. \<forall>p fx fy q.
+ M(x) --> M(y) --> M(p) --> M(fx) --> M(fy) --> M(q) -->
+ pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) -->
+ pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))"
+
+
+ pred_set :: "[i=>o,i,i,i,i] => o"
+ "pred_set(M,A,x,r,B) ==
+ \<forall>y. M(y) --> (y \<in> B <-> (\<exists>p\<in>r. M(p) & y \<in> A & pair(M,y,x,p)))"
+
+ membership :: "[i=>o,i,i] => o" --{*membership relation*}
+ "membership(M,A,r) ==
+ \<forall>p. M(p) -->
+ (p \<in> r <-> (\<exists>x\<in>A. \<exists>y\<in>A. M(x) & M(y) & x\<in>y & pair(M,x,y,p)))"
+
+
+subsection{*Absoluteness for a transitive class model*}
+
+text{*The class M is assumed to be transitive and to satisfy some
+ relativized ZF axioms*}
+locale M_axioms =
+ fixes M
+ assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
+ and nonempty [simp]: "M(0)"
+ and upair_ax: "upair_ax(M)"
+ and Union_ax: "Union_ax(M)"
+ and power_ax: "power_ax(M)"
+ and replacement: "replacement(M,P)"
+ and Inter_separation:
+ "M(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. M(y) --> x\<in>y)"
+ and cartprod_separation:
+ "[| M(A); M(B) |]
+ ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. M(x) & M(y) & pair(M,x,y,z))"
+ and image_separation:
+ "[| M(A); M(r) |]
+ ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & (\<exists>x\<in>A. M(x) & pair(M,x,y,p)))"
+ and vimage_separation:
+ "[| M(A); M(r) |]
+ ==> separation(M, \<lambda>x. \<exists>p\<in>r. M(p) & (\<exists>y\<in>A. M(x) & pair(M,x,y,p)))"
+ and converse_separation:
+ "M(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. M(p) & (\<exists>x y. M(x) & M(y) &
+ pair(M,x,y,p) & pair(M,y,x,z)))"
+ and restrict_separation:
+ "M(A)
+ ==> separation(M, \<lambda>z. \<exists>x\<in>A. M(x) & (\<exists>y. M(y) & pair(M,x,y,z)))"
+ and comp_separation:
+ "[| M(r); M(s) |]
+ ==> separation(M, \<lambda>xz. \<exists>x y z. M(x) & M(y) & M(z) &
+ (\<exists>xy\<in>s. \<exists>yz\<in>r. M(xy) & M(yz) &
+ pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+ and pred_separation:
+ "[| M(r); M(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. M(p) & pair(M,y,x,p))"
+ and Memrel_separation:
+ "separation(M, \<lambda>z. \<exists>x y. M(x) & M(y) & pair(M,x,y,z) \<and> x \<in> y)"
+ and obase_separation:
+ --{*part of the order type formalization*}
+ "[| M(A); M(r) |]
+ ==> separation(M, \<lambda>a. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &
+ ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
+ order_isomorphism(M,par,r,x,mx,g))"
+ and well_ord_iso_separation:
+ "[| M(A); M(f); M(r) |]
+ ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. M(y) \<and> (\<exists>p. M(p) \<and>
+ fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+ and obase_equals_separation:
+ "[| M(A); M(r) |]
+ ==> separation
+ (M, \<lambda>x. x\<in>A --> ~(\<exists>y. M(y) & (\<exists>g. M(g) &
+ ordinal(M,y) & (\<exists>my pxr. M(my) & M(pxr) &
+ membership(M,y,my) & pred_set(M,A,x,r,pxr) &
+ order_isomorphism(M,pxr,r,y,my,g)))))"
+ and is_recfun_separation:
+ --{*for well-founded recursion. NEEDS RELATIVIZATION*}
+ "[| M(A); M(f); M(g); M(a); M(b) |]
+ ==> 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)"
+ and omap_replacement:
+ "[| M(A); M(r) |]
+ ==> strong_replacement(M,
+ \<lambda>a z. \<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) &
+ ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
+ pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
+
+lemma (in M_axioms) Ball_abs [simp]:
+ "M(A) ==> (\<forall>x\<in>A. M(x) --> P(x)) <-> (\<forall>x\<in>A. P(x))"
+by (blast intro: transM)
+
+lemma (in M_axioms) Bex_abs [simp]:
+ "M(A) ==> (\<exists>x\<in>A. M(x) & P(x)) <-> (\<exists>x\<in>A. P(x))"
+by (blast intro: transM)
+
+lemma (in M_axioms) Ball_iff_equiv:
+ "M(A) ==> (\<forall>x. M(x) --> (x\<in>A <-> P(x))) <->
+ (\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) --> M(x) --> x\<in>A)"
+by (blast intro: transM)
+
+lemma (in M_axioms) empty_abs [simp]:
+ "M(z) ==> empty(M,z) <-> z=0"
+apply (simp add: empty_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) subset_abs [simp]:
+ "M(A) ==> subset(M,A,B) <-> A \<subseteq> B"
+apply (simp add: subset_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) upair_abs [simp]:
+ "M(z) ==> upair(M,a,b,z) <-> z={a,b}"
+apply (simp add: upair_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) upair_in_M_iff [iff]:
+ "M({a,b}) <-> M(a) & M(b)"
+apply (insert upair_ax, simp add: upair_ax_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) singleton_in_M_iff [iff]:
+ "M({a}) <-> M(a)"
+by (insert upair_in_M_iff [of a a], simp)
+
+lemma (in M_axioms) pair_abs [simp]:
+ "M(z) ==> pair(M,a,b,z) <-> z=<a,b>"
+apply (simp add: pair_def ZF.Pair_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) pair_in_M_iff [iff]:
+ "M(<a,b>) <-> M(a) & M(b)"
+by (simp add: ZF.Pair_def)
+
+lemma (in M_axioms) pair_components_in_M:
+ "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
+apply (simp add: Pair_def)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) cartprod_abs [simp]:
+ "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B"
+apply (simp add: cartprod_def)
+apply (rule iffI)
+apply (blast intro!: equalityI intro: transM dest!: spec)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) union_abs [simp]:
+ "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b"
+apply (simp add: union_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) inter_abs [simp]:
+ "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b"
+apply (simp add: inter_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) setdiff_abs [simp]:
+ "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b"
+apply (simp add: setdiff_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) Union_abs [simp]:
+ "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)"
+apply (simp add: big_union_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
+lemma (in M_axioms) Union_closed [intro]:
+ "M(A) ==> M(Union(A))"
+by (insert Union_ax, simp add: Union_ax_def)
+
+lemma (in M_axioms) Un_closed [intro]:
+ "[| M(A); M(B) |] ==> M(A Un B)"
+by (simp only: Un_eq_Union, blast)
+
+lemma (in M_axioms) cons_closed [intro]:
+ "[| M(a); M(A) |] ==> M(cons(a,A))"
+by (subst cons_eq [symmetric], blast)
+
+lemma (in M_axioms) successor_abs [simp]:
+ "[| M(a); M(z) |] ==> successor(M,a,z) <-> z=succ(a)"
+by (simp add: successor_def, blast)
+
+lemma (in M_axioms) succ_in_M_iff [iff]:
+ "M(succ(a)) <-> M(a)"
+apply (simp add: succ_def)
+apply (blast intro: transM)
+done
+
+lemma (in M_axioms) separation_closed [intro]:
+ "[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
+apply (insert separation, simp add: separation_def)
+apply (drule spec [THEN mp], assumption, clarify)
+apply (subgoal_tac "y = Collect(A,P)", blast)
+apply (blast dest: transM)
+done
+
+text{*Probably the premise and conclusion are equivalent*}
+lemma (in M_axioms) strong_replacementI [rule_format]:
+ "[| \<forall>A. M(A) --> separation(M, %u. \<exists>x\<in>A. P(x,u)) |]
+ ==> strong_replacement(M,P)"
+apply (simp add: strong_replacement_def)
+apply (clarify );
+apply (frule replacementD [OF replacement])
+apply assumption
+apply (clarify );
+apply (drule_tac x=A in spec)
+apply (clarify );
+apply (drule_tac z=Y in separationD)
+apply assumption;
+apply (clarify );
+apply (blast dest: transM)
+done
+
+
+(*The last premise expresses that P takes M to M*)
+lemma (in M_axioms) strong_replacement_closed [intro]:
+ "[| strong_replacement(M,P); M(A); univalent(M,A,P);
+ !!x y. [| P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))"
+apply (simp add: strong_replacement_def)
+apply (drule spec [THEN mp], auto)
+apply (subgoal_tac "Replace(A,P) = Y")
+ apply (simp add: );
+apply (rule equality_iffI)
+apply (simp add: Replace_iff)
+apply safe;
+ apply (blast dest: transM)
+apply (frule transM, assumption)
+ apply (simp add: univalent_def);
+ apply (drule spec [THEN mp, THEN iffD1], assumption, assumption)
+ apply (blast dest: transM)
+done
+
+(*The first premise can't simply be assumed as a schema.
+ It is essential to take care when asserting instances of Replacement.
+ Let K be a nonconstructible subset of nat and define
+ f(x) = x if x:K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a
+ nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f))
+ even for f : M -> M.
+*)
+lemma (in M_axioms) RepFun_closed [intro]:
+ "[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x. M(x) --> M(f(x)) |]
+ ==> M(RepFun(A,f))"
+apply (simp add: RepFun_def)
+apply (rule strong_replacement_closed)
+apply (auto dest: transM simp add: univalent_def)
+done
+
+lemma (in M_axioms) converse_abs [simp]:
+ "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)"
+apply (simp add: is_converse_def)
+apply (rule iffI)
+ apply (rule equalityI)
+ apply (blast dest: transM)
+ apply (clarify, frule transM, assumption, simp, blast)
+done
+
+lemma (in M_axioms) image_abs [simp]:
+ "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A"
+apply (simp add: image_def)
+apply (rule iffI)
+ apply (blast intro!: equalityI dest: transM, blast)
+done
+
+text{*What about @{text Pow_abs}? Powerset is NOT absolute!
+ This result is one direction of absoluteness.*}
+
+lemma (in M_axioms) powerset_Pow:
+ "powerset(M, x, Pow(x))"
+by (simp add: powerset_def)
+
+text{*But we can't prove that the powerset in @{text M} includes the
+ real powerset.*}
+lemma (in M_axioms) powerset_imp_subset_Pow:
+ "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)"
+apply (simp add: powerset_def)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) cartprod_iff_lemma:
+ "[| M(C); \<forall>u. M(u) --> u \<in> C <-> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
+ powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
+ ==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
+apply (simp add: powerset_def)
+apply (rule equalityI, clarify, simp)
+ apply (frule transM, assumption, simp)
+ apply blast
+apply clarify
+apply (frule transM, assumption, force)
+done
+
+lemma (in M_axioms) cartprod_iff:
+ "[| M(A); M(B); M(C) |]
+ ==> cartprod(M,A,B,C) <->
+ (\<exists>p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) &
+ C = {z \<in> p2. \<exists>x\<in>A. \<exists>y\<in>B. z = <x,y>})"
+apply (simp add: Pair_def cartprod_def, safe)
+defer 1
+ apply (simp add: powerset_def)
+ apply blast
+txt{*Final, difficult case: the left-to-right direction of the theorem.*}
+apply (insert power_ax, simp add: power_ax_def)
+apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)
+apply (erule impE, blast, clarify)
+apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)
+apply (blast intro: cartprod_iff_lemma)
+done
+
+lemma (in M_axioms) cartprod_closed_lemma:
+ "[| M(A); M(B) |] ==> \<exists>C. M(C) & cartprod(M,A,B,C)"
+apply (simp del: cartprod_abs add: cartprod_iff)
+apply (insert power_ax, simp add: power_ax_def)
+apply (frule_tac x="A Un B" and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)
+apply (erule impE, blast, clarify)
+apply (drule_tac x=z and P="\<lambda>x. M(x) --> Ex(?Q(x))" in spec)
+apply (erule impE, blast, clarify)
+apply (intro exI conjI)
+prefer 6 apply (rule refl)
+prefer 4 apply assumption
+prefer 4 apply assumption
+apply (insert cartprod_separation [of A B], simp, blast+)
+done
+
+
+text{*All the lemmas above are necessary because Powerset is not absolute.
+ I should have used Replacement instead!*}
+lemma (in M_axioms) cartprod_closed [intro]:
+ "[| M(A); M(B) |] ==> M(A*B)"
+by (frule cartprod_closed_lemma, assumption, force)
+
+lemma (in M_axioms) image_closed [intro]:
+ "[| M(A); M(r) |] ==> M(r``A)"
+apply (simp add: image_iff_Collect)
+apply (insert image_separation [of A r], simp, blast)
+done
+
+lemma (in M_axioms) vimage_abs [simp]:
+ "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A"
+apply (simp add: pre_image_def)
+apply (rule iffI)
+ apply (blast intro!: equalityI dest: transM, blast)
+done
+
+lemma (in M_axioms) vimage_closed [intro]:
+ "[| M(A); M(r) |] ==> M(r-``A)"
+apply (simp add: vimage_iff_Collect)
+apply (insert vimage_separation [of A r], simp, blast)
+done
+
+lemma (in M_axioms) domain_abs [simp]:
+ "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)"
+apply (simp add: is_domain_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
+lemma (in M_axioms) domain_closed [intro]:
+ "M(r) ==> M(domain(r))"
+apply (simp add: domain_eq_vimage)
+apply (blast intro: vimage_closed)
+done
+
+lemma (in M_axioms) range_abs [simp]:
+ "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)"
+apply (simp add: is_range_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
+lemma (in M_axioms) range_closed [intro]:
+ "M(r) ==> M(range(r))"
+apply (simp add: range_eq_image)
+apply (blast intro: image_closed)
+done
+
+lemma (in M_axioms) M_converse_iff:
+ "M(r) ==>
+ converse(r) =
+ {z \<in> range(r) * domain(r).
+ \<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>)}"
+by (blast dest: transM)
+
+lemma (in M_axioms) converse_closed [intro]:
+ "M(r) ==> M(converse(r))"
+apply (simp add: M_converse_iff)
+apply (insert converse_separation [of r], simp)
+apply (blast intro: image_closed)
+done
+
+lemma (in M_axioms) relation_abs [simp]:
+ "M(r) ==> is_relation(M,r) <-> relation(r)"
+apply (simp add: is_relation_def relation_def)
+apply (blast dest!: bspec dest: pair_components_in_M)+
+done
+
+lemma (in M_axioms) function_abs [simp]:
+ "M(r) ==> is_function(M,r) <-> function(r)"
+apply (simp add: is_function_def function_def, safe)
+ apply (frule transM, assumption)
+ apply (blast dest: pair_components_in_M)+
+done
+
+lemma (in M_axioms) apply_closed [intro]:
+ "[|M(f); M(a)|] ==> M(f`a)"
+apply (simp add: apply_def)
+apply (blast intro: elim:);
+done
+
+lemma (in M_axioms) apply_abs:
+ "[| function(f); M(f); M(y) |]
+ ==> fun_apply(M,f,x,y) <-> x \<in> domain(f) & f`x = y"
+apply (simp add: fun_apply_def)
+apply (blast intro: function_apply_equality function_apply_Pair)
+done
+
+lemma (in M_axioms) typed_apply_abs:
+ "[| f \<in> A -> B; M(f); M(y) |]
+ ==> fun_apply(M,f,x,y) <-> x \<in> A & f`x = y"
+by (simp add: apply_abs fun_is_function domain_of_fun)
+
+lemma (in M_axioms) typed_function_abs [simp]:
+ "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \<in> A -> B"
+apply (auto simp add: typed_function_def relation_def Pi_iff)
+apply (blast dest: pair_components_in_M)+
+done
+
+lemma (in M_axioms) injection_abs [simp]:
+ "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \<in> inj(A,B)"
+apply (simp add: injection_def apply_iff inj_def apply_closed)
+apply (blast dest: transM [of _ A]);
+done
+
+lemma (in M_axioms) surjection_abs [simp]:
+ "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \<in> surj(A,B)"
+by (simp add: typed_apply_abs surjection_def surj_def)
+
+lemma (in M_axioms) bijection_abs [simp]:
+ "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \<in> bij(A,B)"
+by (simp add: bijection_def bij_def)
+
+text{*no longer needed*}
+lemma (in M_axioms) restriction_is_function:
+ "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |]
+ ==> function(z)"
+apply (rotate_tac 1)
+apply (simp add: restriction_def Ball_iff_equiv)
+apply (unfold function_def, blast)
+done
+
+lemma (in M_axioms) restriction_abs [simp]:
+ "[| M(f); M(A); M(z) |]
+ ==> restriction(M,f,A,z) <-> z = restrict(f,A)"
+apply (simp add: Ball_iff_equiv restriction_def restrict_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
+
+lemma (in M_axioms) M_restrict_iff:
+ "M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y. M(y) & z = \<langle>x, y\<rangle>}"
+by (simp add: restrict_def, blast dest: transM)
+
+lemma (in M_axioms) restrict_closed [intro]:
+ "[| M(A); M(r) |] ==> M(restrict(r,A))"
+apply (simp add: M_restrict_iff)
+apply (insert restrict_separation [of A], simp, blast)
+done
+
+
+lemma (in M_axioms) M_comp_iff:
+ "[| M(r); M(s) |]
+ ==> r O s =
+ {xz \<in> domain(s) * range(r).
+ \<exists>x. M(x) \<and> (\<exists>y. M(y) \<and> (\<exists>z. M(z) \<and>
+ xz = \<langle>x,z\<rangle> \<and> \<langle>x,y\<rangle> \<in> s \<and> \<langle>y,z\<rangle> \<in> r))}"
+apply (simp add: comp_def)
+apply (rule equalityI)
+ apply (clarify );
+ apply (simp add: );
+ apply (blast dest: transM)+
+done
+
+lemma (in M_axioms) comp_closed [intro]:
+ "[| M(r); M(s) |] ==> M(r O s)"
+apply (simp add: M_comp_iff)
+apply (insert comp_separation [of r s], simp, blast)
+done
+
+lemma (in M_axioms) nat_into_M [intro]:
+ "n \<in> nat ==> M(n)"
+by (induct n rule: nat_induct, simp_all)
+
+lemma (in M_axioms) Inl_in_M_iff [iff]:
+ "M(Inl(a)) <-> M(a)"
+by (simp add: Inl_def)
+
+lemma (in M_axioms) Inr_in_M_iff [iff]:
+ "M(Inr(a)) <-> M(a)"
+by (simp add: Inr_def)
+
+lemma (in M_axioms) Inter_abs [simp]:
+ "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)"
+apply (simp add: big_inter_def Inter_def)
+apply (blast intro!: equalityI dest: transM)
+done
+
+lemma (in M_axioms) Inter_closed [intro]:
+ "M(A) ==> M(Inter(A))"
+by (insert Inter_separation, simp add: Inter_def, blast)
+
+lemma (in M_axioms) Int_closed [intro]:
+ "[| M(A); M(B) |] ==> M(A Int B)"
+apply (subgoal_tac "M({A,B})")
+apply (frule Inter_closed, force+);
+done
+
+subsection{*Absoluteness for ordinals*}
+text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*}
+
+lemma (in M_axioms) lt_closed:
+ "[| j<i; M(i) |] ==> M(j)"
+by (blast dest: ltD intro: transM)
+
+lemma (in M_axioms) transitive_set_abs [simp]:
+ "M(a) ==> transitive_set(M,a) <-> Transset(a)"
+by (simp add: transitive_set_def Transset_def)
+
+lemma (in M_axioms) ordinal_abs [simp]:
+ "M(a) ==> ordinal(M,a) <-> Ord(a)"
+by (simp add: ordinal_def Ord_def)
+
+lemma (in M_axioms) limit_ordinal_abs [simp]:
+ "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
+apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def)
+apply (simp add: lt_def, blast)
+done
+
+lemma (in M_axioms) successor_ordinal_abs [simp]:
+ "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\<exists>b. M(b) & a = succ(b))"
+apply (simp add: successor_ordinal_def, safe)
+apply (drule Ord_cases_disj, auto)
+done
+
+lemma finite_Ord_is_nat:
+ "[| Ord(a); ~ Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a \<in> nat"
+by (induct a rule: trans_induct3, simp_all)
+
+lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
+by (induct a rule: nat_induct, auto)
+
+lemma (in M_axioms) finite_ordinal_abs [simp]:
+ "M(a) ==> finite_ordinal(M,a) <-> a \<in> nat"
+apply (simp add: finite_ordinal_def)
+apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord
+ dest: Ord_trans naturals_not_limit)
+done
+
+lemma Limit_non_Limit_implies_nat: "[| Limit(a); \<forall>x\<in>a. ~ Limit(x) |] ==> a = nat"
+apply (rule le_anti_sym)
+apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord)
+ apply (simp add: lt_def)
+ apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat)
+apply (erule nat_le_Limit)
+done
+
+lemma (in M_axioms) omega_abs [simp]:
+ "M(a) ==> omega(M,a) <-> a = nat"
+apply (simp add: omega_def)
+apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit)
+done
+
+lemma (in M_axioms) number1_abs [simp]:
+ "M(a) ==> number1(M,a) <-> a = 1"
+by (simp add: number1_def)
+
+lemma (in M_axioms) number1_abs [simp]:
+ "M(a) ==> number2(M,a) <-> a = succ(1)"
+by (simp add: number2_def)
+
+lemma (in M_axioms) number3_abs [simp]:
+ "M(a) ==> number3(M,a) <-> a = succ(succ(1))"
+by (simp add: number3_def)
+
+text{*Kunen continued to 20...*}
+
+(*Could not get this to work. The \<lambda>x\<in>nat is essential because everything
+ but the recursion variable must stay unchanged. But then the recursion
+ equations only hold for x\<in>nat (or in some other set) and not for the
+ whole of the class M.
+ consts
+ natnumber_aux :: "[i=>o,i] => i"
+
+ primrec
+ "natnumber_aux(M,0) = (\<lambda>x\<in>nat. if empty(M,x) then 1 else 0)"
+ "natnumber_aux(M,succ(n)) =
+ (\<lambda>x\<in>nat. if (\<exists>y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x))
+ then 1 else 0)"
+
+ constdefs
+ natnumber :: "[i=>o,i,i] => o"
+ "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
+
+ lemma (in M_axioms) [simp]:
+ "natnumber(M,0,x) == x=0"
+*)
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/WF_absolute.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,210 @@
+theory WF_absolute = WF_extras + WFrec:
+
+
+subsection{*Transitive closure without fixedpoints*}
+
+(*Ordinal.thy: just after succ_le_iff?*)
+lemma Ord_succ_mem_iff: "Ord(j) ==> succ(i) \<in> succ(j) <-> i\<in>j"
+apply (insert succ_le_iff [of i j])
+apply (simp add: lt_def)
+done
+
+constdefs
+ rtrancl_alt :: "[i,i]=>i"
+ "rtrancl_alt(A,r) ==
+ {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
+ \<exists>x y. p = <x,y> & f`0 = x & f`n = y &
+ (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)}"
+
+lemma alt_rtrancl_lemma1 [rule_format]:
+ "n \<in> nat
+ ==> \<forall>f \<in> succ(n) -> field(r).
+ (\<forall>i\<in>n. \<langle>f`i, f ` succ(i)\<rangle> \<in> r) --> \<langle>f`0, f`n\<rangle> \<in> r^*"
+apply (induct_tac n)
+apply (simp_all add: apply_funtype rtrancl_refl, clarify)
+apply (rename_tac n f)
+apply (rule rtrancl_into_rtrancl)
+ prefer 2 apply assumption
+apply (drule_tac x="restrict(f,succ(n))" in bspec)
+ apply (blast intro: restrict_type2)
+apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
+done
+
+lemma rtrancl_alt_subset_rtrancl: "rtrancl_alt(field(r),r) <= r^*"
+apply (simp add: rtrancl_alt_def)
+apply (blast intro: alt_rtrancl_lemma1 )
+done
+
+lemma rtrancl_subset_rtrancl_alt: "r^* <= rtrancl_alt(field(r),r)"
+apply (simp add: rtrancl_alt_def, clarify)
+apply (frule rtrancl_type [THEN subsetD], clarify)
+apply simp
+apply (erule rtrancl_induct)
+ txt{*Base case, trivial*}
+ apply (rule_tac x=0 in bexI)
+ apply (rule_tac x="lam x:1. xa" in bexI)
+ apply simp_all
+txt{*Inductive step*}
+apply clarify
+apply (rename_tac n f)
+apply (rule_tac x="succ(n)" in bexI)
+ apply (rule_tac x="lam i:succ(succ(n)). if i=succ(n) then z else f`i" in bexI)
+ apply (simp add: Ord_succ_mem_iff nat_0_le [THEN ltD] leI [THEN ltD] ltI)
+ apply (blast intro: mem_asym)
+ apply typecheck
+ apply auto
+done
+
+lemma rtrancl_alt_eq_rtrancl: "rtrancl_alt(field(r),r) = r^*"
+by (blast del: subsetI
+ intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
+
+
+text{*Relativized to M: Every well-founded relation is a subset of some
+inverse image of an ordinal. Key step is the construction (in M) of a
+rank function.*}
+
+
+(*NEEDS RELATIVIZATION*)
+locale M_recursion = M_axioms +
+ assumes wfrank_separation':
+ "[| M(r); M(a); r \<subseteq> A*A |] ==>
+ separation
+ (M, \<lambda>x. x \<in> A -->
+ ~(\<exists>f. M(f) \<and>
+ is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f)))"
+ and wfrank_strong_replacement':
+ "[| M(r); M(a); r \<subseteq> A*A |] ==>
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) &
+ is_recfun(r, x, %x f. \<Union>y \<in> r-``{x}. succ(f`y), f) &
+ y = (\<Union>y \<in> r-``{x}. succ(g`y)))"
+
+
+constdefs (*????????????????NEEDED?*)
+ is_wfrank_fun :: "[i=>o,i,i,i] => o"
+ "is_wfrank_fun(M,r,a,f) ==
+ function(f) & domain(f) = r-``{a} &
+ (\<forall>x. M(x) --> <x,a> \<in> r --> f`x = (\<Union>y \<in> r-``{x}. succ(f`y)))"
+
+
+
+
+lemma (in M_recursion) exists_wfrank:
+ "[| wellfounded(M,r); r \<subseteq> A*A; a\<in>A; M(r); M(A) |]
+ ==> \<exists>f. M(f) & is_recfun(r, a, %x g. (\<Union>y \<in> r-``{x}. succ(g`y)), f)"
+apply (rule exists_is_recfun [of A r])
+apply (erule wellfounded_imp_wellfounded_on)
+apply assumption;
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)
+apply (rule succI1)
+apply (blast intro: wfrank_separation')
+apply (blast intro: wfrank_strong_replacement')
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+done
+
+lemma (in M_recursion) exists_wfrank_fun:
+ "[| Ord(j); M(i); M(j) |] ==> \<exists>f. M(f) & is_wfrank_fun(M,i,succ(j),f)"
+apply (rule exists_wfrank [THEN exE])
+apply (erule Ord_succ, assumption, simp)
+apply (rename_tac f, clarify)
+apply (frule is_recfun_type)
+apply (rule_tac x=f in exI)
+apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+ is_wfrank_fun_eq Ord_trans [OF _ succI1])
+done
+
+lemma (in M_recursion) is_wfrank_fun_apply:
+ "[| x < j; M(i); M(j); M(f); is_wfrank_fun(M,r,a,f) |]
+ ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
+apply (simp add: is_wfrank_fun_eq lt_Ord2)
+apply (frule lt_closed, simp)
+apply (subgoal_tac "x <= domain(f)")
+ apply (simp add: Ord_trans [OF _ succI1] image_function)
+ apply (blast intro: elim:);
+apply (blast intro: dest!: leI [THEN le_imp_subset] )
+done
+
+lemma (in M_recursion) is_wfrank_fun_eq_wfrank [rule_format]:
+ "[| is_wfrank_fun(M,i,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |]
+ ==> j<J --> f`j = i++j"
+apply (erule_tac i=j in trans_induct, clarify)
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp (no_asm_simp) add: is_wfrank_def wfrank_unfold is_wfrank_fun_apply)
+apply (blast intro: lt_trans ltI lt_Ord)
+done
+
+lemma (in M_recursion) wfrank_abs_fun_apply_iff:
+ "[| M(i); M(J); M(f); M(k); j<J; is_wfrank_fun(M,i,J,f) |]
+ ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (auto simp add: lt_def is_wfrank_fun_eq subsetD apply_abs)
+
+lemma (in M_recursion) Ord_wfrank_abs:
+ "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
+apply (simp add: is_wfrank_def wfrank_abs_fun_apply_iff is_wfrank_fun_eq_wfrank)
+apply (frule exists_wfrank_fun [of j i], blast+)
+done
+
+lemma (in M_recursion) wfrank_abs:
+ "[| M(i); M(j); M(k) |] ==> is_wfrank(M,r,a,k) <-> k = i++j"
+apply (case_tac "Ord(i) & Ord(j)")
+ apply (simp add: Ord_wfrank_abs)
+apply (auto simp add: is_wfrank_def wfrank_eq_if_raw_wfrank)
+done
+
+lemma (in M_recursion) wfrank_closed [intro]:
+ "[| M(i); M(j) |] ==> M(i++j)"
+apply (simp add: wfrank_eq_if_raw_wfrank, clarify)
+apply (simp add: raw_wfrank_eq_wfrank)
+apply (frule exists_wfrank_fun [of j i], auto)
+apply (simp add: apply_closed is_wfrank_fun_eq_wfrank [symmetric])
+done
+
+
+
+constdefs
+ wfrank :: "[i,i]=>i"
+ "wfrank(r,a) == wfrec(r, a, %x f. \<Union>y \<in> r-``{x}. succ(f`y))"
+
+constdefs
+ wftype :: "i=>i"
+ "wftype(r) == \<Union>y \<in> range(r). succ(wfrank(r,y))"
+
+lemma (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\<Union>y \<in> r-``{a}. succ(wfrank(r,y)))"
+by (subst wfrank_def [THEN def_wfrec], simp_all)
+
+lemma (in M_axioms) Ord_wfrank: "wellfounded(M,r) ==> Ord(wfrank(r,a))"
+apply (rule_tac a="a" in wf_induct, assumption)
+apply (subst wfrank, assumption)
+apply (rule Ord_succ [THEN Ord_UN], blast)
+done
+
+lemma (in M_axioms) wfrank_lt: "[|wellfounded(M,r); <a,b> \<in> r|] ==> wfrank(r,a) < wfrank(r,b)"
+apply (rule_tac a1 = "b" in wfrank [THEN ssubst], assumption)
+apply (rule UN_I [THEN ltI])
+apply (simp add: Ord_wfrank vimage_iff)+
+done
+
+lemma (in M_axioms) Ord_wftype: "wellfounded(M,r) ==> Ord(wftype(r))"
+by (simp add: wftype_def Ord_wfrank)
+
+lemma (in M_axioms) wftypeI: "\<lbrakk>wellfounded(M,r); x \<in> field(r)\<rbrakk> \<Longrightarrow> wfrank(r,x) \<in> wftype(r)"
+apply (simp add: wftype_def)
+apply (blast intro: wfrank_lt [THEN ltD])
+done
+
+
+lemma (in M_axioms) wf_imp_subset_rvimage:
+ "[|wellfounded(M,r); r \<subseteq> A*A|] ==> \<exists>i f. Ord(i) & r <= rvimage(A, f, Memrel(i))"
+apply (rule_tac x="wftype(r)" in exI)
+apply (rule_tac x="\<lambda>x\<in>A. wfrank(r,x)" in exI)
+apply (simp add: Ord_wftype, clarify)
+apply (frule subsetD, assumption, clarify)
+apply (simp add: rvimage_iff wfrank_lt [THEN ltD])
+apply (blast intro: wftypeI )
+done
+
+
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/WFrec.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,559 @@
+theory WFrec = Wellorderings:
+
+
+(*WF.thy??*)
+
+lemma is_recfunI:
+ "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
+by (simp add: is_recfun_def)
+
+lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)"
+apply (simp add: is_recfun_def)
+apply (erule ssubst)
+apply (rule function_lam)
+done
+
+text{*Expresses @{text is_recfun} as a recursion equation*}
+lemma is_recfun_iff_equation:
+ "is_recfun(r,a,H,f) <->
+ f \<in> r -`` {a} \<rightarrow> range(f) &
+ (\<forall>x \<in> r-``{a}. f`x = H(x, restrict(f, r-``{x})))"
+apply (rule iffI)
+ apply (simp add: is_recfun_type apply_recfun Ball_def vimage_singleton_iff,
+ clarify)
+apply (simp add: is_recfun_def)
+apply (rule fun_extension)
+ apply assumption
+ apply (fast intro: lam_type, simp)
+done
+
+lemma trans_on_Int_eq [simp]:
+ "[| trans[A](r); <y,x> \<in> r; r \<subseteq> A*A |]
+ ==> r -`` {y} \<inter> r -`` {x} = r -`` {y}"
+by (blast intro: trans_onD)
+
+lemma trans_on_Int_eq2 [simp]:
+ "[| trans[A](r); <y,x> \<in> r; r \<subseteq> A*A |]
+ ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
+by (blast intro: trans_onD)
+
+
+constdefs
+ M_the_recfun :: "[i=>o, i, i, [i,i]=>i] => i"
+ "M_the_recfun(M,r,a,H) == (THE f. M(f) & is_recfun(r,a,H,f))"
+
+
+text{*Stated using @{term "trans[A](r)"} rather than
+ @{term "transitive_rel(M,A,r)"} because the latter rewrites to
+ the former anyway, by @{text transitive_rel_abs}.
+ As always, theorems should be expressed in simplified form.*}
+lemma (in M_axioms) is_recfun_equal [rule_format]:
+ "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g);
+ wellfounded_on(M,A,r); trans[A](r);
+ M(A); M(f); M(g); M(a); M(b);
+ r \<subseteq> A*A; x\<in>A |]
+ ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x"
+apply (frule_tac f="f" in is_recfun_type)
+apply (frule_tac f="g" in is_recfun_type)
+apply (simp add: is_recfun_def)
+apply (erule wellfounded_on_induct2, assumption+)
+apply (force intro: is_recfun_separation, clarify)
+apply (erule ssubst)+
+apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
+apply (rename_tac x1)
+apply (rule_tac t="%z. H(x1,z)" in subst_context)
+apply (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g")
+ apply (blast intro: trans_onD)
+apply (simp add: apply_iff)
+apply (blast intro: trans_onD sym)
+done
+
+lemma (in M_axioms) is_recfun_cut:
+ "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g);
+ wellfounded_on(M,A,r); trans[A](r);
+ M(A); M(f); M(g); M(a); M(b);
+ r \<subseteq> A*A; <b,a>\<in>r |]
+ ==> restrict(f, r-``{b}) = g"
+apply (frule_tac f="f" in is_recfun_type)
+apply (rule fun_extension)
+apply (blast intro: trans_onD restrict_type2)
+apply (erule is_recfun_type, simp)
+apply (blast intro: is_recfun_equal trans_onD)
+done
+
+lemma (in M_axioms) is_recfun_functional:
+ "[|is_recfun(r,a,H,f); is_recfun(r,a,H,g);
+ wellfounded_on(M,A,r); trans[A](r);
+ M(A); M(f); M(g); M(a);
+ r \<subseteq> A*A |]
+ ==> f=g"
+apply (rule fun_extension)
+apply (erule is_recfun_type)+
+apply (blast intro!: is_recfun_equal)
+done
+
+text{*Tells us that is_recfun can (in principle) be relativized.*}
+lemma (in M_axioms) is_recfun_relativize:
+ "[| M(r); M(a); M(f);
+ \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==>
+ is_recfun(r,a,H,f) <->
+ (\<forall>z. z \<in> f <-> (\<exists>x y. M(x) & M(y) & z=<x,y> & <x,a> \<in> r &
+ y = H(x, restrict(f, r-``{x}))))";
+apply (simp add: is_recfun_def vimage_closed restrict_closed lam_def)
+apply (safe intro!: equalityI)
+ apply (drule equalityD1 [THEN subsetD], assumption)
+ apply clarify
+ apply (rule_tac x=x in exI)
+ apply (blast dest: pair_components_in_M)
+ apply (blast elim!: equalityE dest: pair_components_in_M)
+ apply simp
+ apply blast
+ apply simp
+apply (subgoal_tac "function(f)")
+ prefer 2
+ apply (simp add: function_def)
+apply (frule pair_components_in_M, assumption)
+ apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed)
+done
+
+(* ideas for further weaking the H-closure premise:
+apply (drule spec [THEN spec])
+apply (erule mp)
+apply (intro conjI)
+apply (blast dest!: pair_components_in_M)
+apply (blast intro!: function_restrictI dest!: pair_components_in_M)
+apply (blast intro!: function_restrictI dest!: pair_components_in_M)
+apply (simp only: subset_iff domain_iff restrict_iff vimage_iff)
+apply (simp add: vimage_singleton_iff)
+apply (intro allI impI conjI)
+apply (blast intro: transM dest!: pair_components_in_M)
+prefer 4;apply blast
+*)
+
+lemma (in M_axioms) is_recfun_restrict:
+ "[| wellfounded_on(M,A,r); trans[A](r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r;
+ M(A); M(r); M(f);
+ \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \<subseteq> A * A |]
+ ==> is_recfun(r, y, H, restrict(f, r -`` {y}))"
+apply (frule pair_components_in_M, assumption, clarify)
+apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed
+ restrict_iff)
+apply safe
+ apply (simp_all add: vimage_singleton_iff is_recfun_type [THEN apply_iff])
+ apply (frule_tac x=xa in pair_components_in_M, assumption)
+ apply (frule_tac x=xa in apply_recfun, blast intro: trans_onD)
+ apply (simp add: is_recfun_type [THEN apply_iff])
+ (*???COMBINE*)
+ apply (simp add: is_recfun_imp_function function_restrictI restrict_closed vimage_closed)
+apply (blast intro: apply_recfun dest: trans_onD)+
+done
+
+lemma (in M_axioms) restrict_Y_lemma:
+ "[| wellfounded_on(M,A,r); trans[A](r); M(A); M(r); r \<subseteq> A \<times> A;
+ \<forall>x g. M(x) \<and> M(g) & function(g) --> M(H(x,g)); M(Y);
+ \<forall>b. M(b) -->
+ b \<in> Y <->
+ (\<exists>x\<in>r -`` {a1}.
+ \<exists>y. M(y) \<and>
+ (\<exists>g. M(g) \<and> b = \<langle>x,y\<rangle> \<and> is_recfun(r,x,H,g) \<and> y = H(x,g)));
+ \<langle>x,a1\<rangle> \<in> r; M(f); is_recfun(r,x,H,f) |]
+ ==> restrict(Y, r -`` {x}) = f"
+apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:Y <-> <y,z>:f")
+apply (simp (no_asm_simp) add: restrict_def)
+apply (thin_tac "All(?P)")+ --{*essential for efficiency*}
+apply (frule is_recfun_type [THEN fun_is_rel], blast)
+apply (frule pair_components_in_M, assumption, clarify)
+apply (rule iffI)
+ apply (frule_tac y="<y,z>" in transM, assumption )
+ apply (rotate_tac -1)
+ apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
+ apply_recfun is_recfun_cut)
+txt{*Opposite inclusion: something in f, show in Y*}
+apply (frule_tac y="<y,z>" in transM, assumption, simp)
+apply (rule_tac x=y in bexI)
+prefer 2 apply (blast dest: trans_onD)
+apply (rule_tac x=z in exI, simp)
+apply (rule_tac x="restrict(f, r -`` {y})" in exI)
+apply (simp add: vimage_closed restrict_closed is_recfun_restrict
+ apply_recfun is_recfun_type [THEN apply_iff])
+done
+
+text{*Proof of the inductive step for @{text exists_is_recfun}, since
+ we must prove two versions.*}
+lemma (in M_axioms) exists_is_recfun_indstep:
+ "[|a1 \<in> A; \<forall>y. \<langle>y, a1\<rangle> \<in> r --> (\<exists>f. M(f) & is_recfun(r, y, H, f));
+ wellfounded_on(M,A,r); trans[A](r);
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
+ M(A); M(r); r \<subseteq> A * A;
+ \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g))|]
+ ==> \<exists>f. M(f) & is_recfun(r,a1,H,f)"
+apply (frule_tac y=a1 in transM, assumption)
+apply (drule_tac A="r-``{a1}" in strong_replacementD)
+ apply blast
+ txt{*Discharge the "univalent" obligation of Replacement*}
+ apply (clarsimp simp add: univalent_def)
+ apply (blast dest!: is_recfun_functional)
+txt{*Show that the constructed object satisfies @{text is_recfun}*}
+apply clarify
+apply (rule_tac x=Y in exI)
+apply (simp (no_asm_simp) add: is_recfun_relativize vimage_closed restrict_closed)
+(*Tried using is_recfun_iff2 here. Much more simplification takes place
+ because an assumption can kick in. Not sure how to relate the new
+ proof state to the current one.*)
+apply safe
+txt{*Show that elements of @{term Y} are in the right relationship.*}
+apply (frule_tac x=z and P="%b. M(b) --> ?Q(b)" in spec)
+apply (erule impE, blast intro: transM)
+txt{*We have an element of @{term Y}, so we have x, y, z*}
+apply (frule_tac y=z in transM, assumption, clarify)
+apply (simp add: vimage_closed restrict_closed restrict_Y_lemma [of A r H])
+txt{*one more case*}
+apply (simp add: vimage_closed restrict_closed )
+apply (rule_tac x=x in bexI)
+prefer 2 apply blast
+apply (rule_tac x="H(x, restrict(Y, r -`` {x}))" in exI)
+apply (simp add: vimage_closed restrict_closed )
+apply (drule_tac x1=x in spec [THEN mp], assumption, clarify)
+apply (rule_tac x=f in exI)
+apply (simp add: restrict_Y_lemma [of A r H])
+done
+
+
+text{*Relativized version, when we have the (currently weaker) premise
+ @{term "wellfounded_on(M,A,r)"}*}
+lemma (in M_axioms) wellfounded_exists_is_recfun:
+ "[|wellfounded_on(M,A,r); trans[A](r); a\<in>A;
+ separation(M, \<lambda>x. x \<in> A --> ~ (\<exists>f. M(f) \<and> is_recfun(r, x, H, f)));
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
+ M(A); M(r); r \<subseteq> A*A;
+ \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+ ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
+apply (rule wellfounded_on_induct2, assumption+, clarify)
+apply (rule exists_is_recfun_indstep, assumption+)
+done
+
+lemma (in M_axioms) wf_exists_is_recfun:
+ "[|wf[A](r); trans[A](r); a\<in>A;
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) & is_recfun(r,x,H,g) & y = H(x,g));
+ M(A); M(r); r \<subseteq> A*A;
+ \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g)) |]
+ ==> \<exists>f. M(f) & is_recfun(r,a,H,f)"
+apply (rule wf_on_induct2, assumption+)
+apply (frule wf_on_imp_relativized)
+apply (rule exists_is_recfun_indstep, assumption+)
+done
+
+(*If some f satisfies is_recfun(r,a,H,-) then so does M_the_recfun(M,r,a,H) *)
+lemma (in M_axioms) M_is_the_recfun:
+ "[|is_recfun(r,a,H,f);
+ wellfounded_on(M,A,r); trans[A](r);
+ M(A); M(f); M(a); r \<subseteq> A*A |]
+ ==> M(M_the_recfun(M,r,a,H)) &
+ is_recfun(r, a, H, M_the_recfun(M,r,a,H))"
+apply (unfold M_the_recfun_def)
+apply (rule ex1I [THEN theI2], fast)
+apply (blast intro: is_recfun_functional, blast)
+done
+
+constdefs
+ M_is_recfun :: "[i=>o, i, i, [i=>o,i,i,i]=>o, i] => o"
+ "M_is_recfun(M,r,a,MH,f) ==
+ \<forall>z. M(z) -->
+ (z \<in> f <->
+ (\<exists>x y xa sx r_sx f_r_sx.
+ M(x) & M(y) & M(xa) & M(sx) & M(r_sx) & M(f_r_sx) &
+ pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) &
+ pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) &
+ xa \<in> r & MH(M, x, f_r_sx, y)))"
+
+lemma (in M_axioms) is_recfun_iff_M:
+ "[| M(r); M(a); M(f); \<forall>x g. M(x) & M(g) & function(g) --> M(H(x,g));
+ \<forall>x g y. M(x) --> M(g) --> M(y) --> MH(M,x,g,y) <-> y = H(x,g) |] ==>
+ is_recfun(r,a,H,f) <-> M_is_recfun(M,r,a,MH,f)"
+apply (simp add: vimage_closed restrict_closed M_is_recfun_def is_recfun_relativize)
+apply (rule all_cong, safe)
+ apply (thin_tac "\<forall>x. ?P(x)")+
+ apply (blast dest: transM) (*or del: allE*)
+done
+
+lemma M_is_recfun_cong [cong]:
+ "[| r = r'; a = a'; f = f';
+ !!x g y. [| M(x); M(g); M(y) |] ==> MH(M,x,g,y) <-> MH'(M,x,g,y) |]
+ ==> M_is_recfun(M,r,a,MH,f) <-> M_is_recfun(M,r',a',MH',f')"
+by (simp add: M_is_recfun_def)
+
+
+constdefs
+ (*This expresses ordinal addition as a formula in the LAST. It also
+ provides an abbreviation that can be used in the instance of strong
+ replacement below. Here j is used to define the relation, namely
+ Memrel(succ(j)), while x determines the domain of f.*)
+ is_oadd_fun :: "[i=>o,i,i,i,i] => o"
+ "is_oadd_fun(M,i,j,x,f) ==
+ (\<forall>sj msj. M(sj) --> M(msj) -->
+ successor(M,j,sj) --> membership(M,sj,msj) -->
+ M_is_recfun(M, msj, x,
+ %M x g y. \<exists>gx. M(gx) & image(M,g,x,gx) & union(M,i,gx,y),
+ f))"
+
+ is_oadd :: "[i=>o,i,i,i] => o"
+ "is_oadd(M,i,j,k) ==
+ (~ ordinal(M,i) & ~ ordinal(M,j) & k=0) |
+ (~ ordinal(M,i) & ordinal(M,j) & k=j) |
+ (ordinal(M,i) & ~ ordinal(M,j) & k=i) |
+ (ordinal(M,i) & ordinal(M,j) &
+ (\<exists>f fj sj. M(f) & M(fj) & M(sj) &
+ successor(M,j,sj) & is_oadd_fun(M,i,sj,sj,f) &
+ fun_apply(M,f,j,fj) & fj = k))"
+
+ (*NEEDS RELATIVIZATION*)
+ omult_eqns :: "[i,i,i,i] => o"
+ "omult_eqns(i,x,g,z) ==
+ Ord(x) &
+ (x=0 --> z=0) &
+ (\<forall>j. x = succ(j) --> z = g`j ++ i) &
+ (Limit(x) --> z = \<Union>(g``x))"
+
+ is_omult_fun :: "[i=>o,i,i,i] => o"
+ "is_omult_fun(M,i,j,f) ==
+ (\<exists>df. M(df) & is_function(M,f) &
+ is_domain(M,f,df) & subset(M, j, df)) &
+ (\<forall>x\<in>j. omult_eqns(i,x,f,f`x))"
+
+ is_omult :: "[i=>o,i,i,i] => o"
+ "is_omult(M,i,j,k) ==
+ \<exists>f fj sj. M(f) & M(fj) & M(sj) &
+ successor(M,j,sj) & is_omult_fun(M,i,sj,f) &
+ fun_apply(M,f,j,fj) & fj = k"
+
+
+locale M_recursion = M_axioms +
+ assumes oadd_strong_replacement:
+ "[| M(i); M(j) |] ==>
+ strong_replacement(M,
+ \<lambda>x z. \<exists>y f fx. M(y) & M(f) & M(fx) &
+ pair(M,x,y,z) & is_oadd_fun(M,i,j,x,f) &
+ image(M,f,x,fx) & y = i Un fx)"
+ and omult_strong_replacement':
+ "[| M(i); M(j) |] ==>
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) &
+ is_recfun(Memrel(succ(j)),x,%x g. THE z. omult_eqns(i,x,g,z),g) &
+ y = (THE z. omult_eqns(i, x, g, z)))"
+
+
+
+text{*is_oadd_fun: Relating the pure "language of set theory" to Isabelle/ZF*}
+lemma (in M_recursion) is_oadd_fun_iff:
+ "[| a\<le>j; M(i); M(j); M(a); M(f) |]
+ ==> is_oadd_fun(M,i,j,a,f) <->
+ f \<in> a \<rightarrow> range(f) & (\<forall>x. M(x) --> x < a --> f`x = i Un f``x)"
+apply (frule lt_Ord)
+apply (simp add: is_oadd_fun_def Memrel_closed Un_closed
+ is_recfun_iff_M [of concl: _ _ "%x g. i Un g``x", THEN iff_sym]
+ image_closed is_recfun_iff_equation
+ Ball_def lt_trans [OF ltI, of _ a] lt_Memrel)
+apply (simp add: lt_def)
+apply (blast dest: transM)
+done
+
+
+lemma (in M_recursion) oadd_strong_replacement':
+ "[| M(i); M(j) |] ==>
+ strong_replacement(M, \<lambda>x z. \<exists>y g. M(y) & M(g) &
+ pair(M,x,y,z) &
+ is_recfun(Memrel(succ(j)),x,%x g. i Un g``x,g) &
+ y = i Un g``x)"
+apply (insert oadd_strong_replacement [of i j])
+apply (simp add: Memrel_closed Un_closed image_closed is_oadd_fun_def
+ is_recfun_iff_M)
+done
+
+
+lemma (in M_recursion) exists_oadd:
+ "[| Ord(j); M(i); M(j) |]
+ ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. i Un g``x, f)"
+apply (rule wf_exists_is_recfun)
+apply (rule wf_Memrel [THEN wf_imp_wf_on])
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)
+apply (rule succI1)
+apply (blast intro: oadd_strong_replacement')
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+done
+
+lemma (in M_recursion) exists_oadd_fun:
+ "[| Ord(j); M(i); M(j) |]
+ ==> \<exists>f. M(f) & is_oadd_fun(M,i,succ(j),succ(j),f)"
+apply (rule exists_oadd [THEN exE])
+apply (erule Ord_succ, assumption, simp)
+apply (rename_tac f, clarify)
+apply (frule is_recfun_type)
+apply (rule_tac x=f in exI)
+apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+ is_oadd_fun_iff Ord_trans [OF _ succI1])
+done
+
+lemma (in M_recursion) is_oadd_fun_apply:
+ "[| x < j; M(i); M(j); M(f); is_oadd_fun(M,i,j,j,f) |]
+ ==> f`x = i Un (\<Union>k\<in>x. {f ` k})"
+apply (simp add: is_oadd_fun_iff lt_Ord2, clarify)
+apply (frule lt_closed, simp)
+apply (frule leI [THEN le_imp_subset])
+apply (simp add: image_fun, blast)
+done
+
+lemma (in M_recursion) is_oadd_fun_iff_oadd [rule_format]:
+ "[| is_oadd_fun(M,i,J,J,f); M(i); M(J); M(f); Ord(i); Ord(j) |]
+ ==> j<J --> f`j = i++j"
+apply (erule_tac i=j in trans_induct, clarify)
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp (no_asm_simp) add: is_oadd_def oadd_unfold is_oadd_fun_apply)
+apply (blast intro: lt_trans ltI lt_Ord)
+done
+
+lemma (in M_recursion) oadd_abs_fun_apply_iff:
+ "[| M(i); M(J); M(f); M(k); j<J; is_oadd_fun(M,i,J,J,f) |]
+ ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (force simp add: lt_def is_oadd_fun_iff subsetD typed_apply_abs)
+
+lemma (in M_recursion) Ord_oadd_abs:
+ "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
+apply (simp add: is_oadd_def oadd_abs_fun_apply_iff is_oadd_fun_iff_oadd)
+apply (frule exists_oadd_fun [of j i], blast+)
+done
+
+lemma (in M_recursion) oadd_abs:
+ "[| M(i); M(j); M(k) |] ==> is_oadd(M,i,j,k) <-> k = i++j"
+apply (case_tac "Ord(i) & Ord(j)")
+ apply (simp add: Ord_oadd_abs)
+apply (auto simp add: is_oadd_def oadd_eq_if_raw_oadd)
+done
+
+lemma (in M_recursion) oadd_closed [intro]:
+ "[| M(i); M(j) |] ==> M(i++j)"
+apply (simp add: oadd_eq_if_raw_oadd, clarify)
+apply (simp add: raw_oadd_eq_oadd)
+apply (frule exists_oadd_fun [of j i], auto)
+apply (simp add: apply_closed is_oadd_fun_iff_oadd [symmetric])
+done
+
+
+text{*Ordinal Multiplication*}
+
+lemma omult_eqns_unique:
+ "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
+apply (simp add: omult_eqns_def, clarify)
+apply (erule Ord_cases, simp_all)
+done
+
+lemma omult_eqns_0: "omult_eqns(i,0,g,z) <-> z=0"
+by (simp add: omult_eqns_def)
+
+lemma the_omult_eqns_0: "(THE z. omult_eqns(i,0,g,z)) = 0"
+by (simp add: omult_eqns_0)
+
+lemma omult_eqns_succ: "omult_eqns(i,succ(j),g,z) <-> Ord(j) & z = g`j ++ i"
+by (simp add: omult_eqns_def)
+
+lemma the_omult_eqns_succ:
+ "Ord(j) ==> (THE z. omult_eqns(i,succ(j),g,z)) = g`j ++ i"
+by (simp add: omult_eqns_succ)
+
+lemma omult_eqns_Limit:
+ "Limit(x) ==> omult_eqns(i,x,g,z) <-> z = \<Union>(g``x)"
+apply (simp add: omult_eqns_def)
+apply (blast intro: Limit_is_Ord)
+done
+
+lemma the_omult_eqns_Limit:
+ "Limit(x) ==> (THE z. omult_eqns(i,x,g,z)) = \<Union>(g``x)"
+by (simp add: omult_eqns_Limit)
+
+lemma omult_eqns_Not: "~ Ord(x) ==> ~ omult_eqns(i,x,g,z)"
+by (simp add: omult_eqns_def)
+
+
+lemma (in M_recursion) the_omult_eqns_closed:
+ "[| M(i); M(x); M(g); function(g) |]
+ ==> M(THE z. omult_eqns(i, x, g, z))"
+apply (case_tac "Ord(x)")
+ prefer 2 apply (simp add: omult_eqns_Not) --{*trivial, non-Ord case*}
+apply (erule Ord_cases)
+ apply (simp add: omult_eqns_0)
+ apply (simp add: omult_eqns_succ apply_closed oadd_closed)
+apply (simp add: omult_eqns_Limit)
+apply (simp add: Union_closed image_closed)
+done
+
+lemma (in M_recursion) exists_omult:
+ "[| Ord(j); M(i); M(j) |]
+ ==> \<exists>f. M(f) & is_recfun(Memrel(succ(j)), j, %x g. THE z. omult_eqns(i,x,g,z), f)"
+apply (rule wf_exists_is_recfun)
+apply (rule wf_Memrel [THEN wf_imp_wf_on])
+apply (rule trans_Memrel [THEN trans_imp_trans_on], simp)
+apply (rule succI1)
+apply (blast intro: omult_strong_replacement')
+apply (simp_all add: Memrel_type Memrel_closed Un_closed image_closed)
+apply (blast intro: the_omult_eqns_closed)
+done
+
+lemma (in M_recursion) exists_omult_fun:
+ "[| Ord(j); M(i); M(j) |] ==> \<exists>f. M(f) & is_omult_fun(M,i,succ(j),f)"
+apply (rule exists_omult [THEN exE])
+apply (erule Ord_succ, assumption, simp)
+apply (rename_tac f, clarify)
+apply (frule is_recfun_type)
+apply (rule_tac x=f in exI)
+apply (simp add: fun_is_function domain_of_fun lt_Memrel apply_recfun lt_def
+ is_omult_fun_def Ord_trans [OF _ succI1])
+apply (force dest: Ord_in_Ord'
+ simp add: omult_eqns_def the_omult_eqns_0 the_omult_eqns_succ
+ the_omult_eqns_Limit)
+done
+
+lemma (in M_recursion) is_omult_fun_apply_0:
+ "[| 0 < j; is_omult_fun(M,i,j,f) |] ==> f`0 = 0"
+by (simp add: is_omult_fun_def omult_eqns_def lt_def ball_conj_distrib)
+
+lemma (in M_recursion) is_omult_fun_apply_succ:
+ "[| succ(x) < j; is_omult_fun(M,i,j,f) |] ==> f`succ(x) = f`x ++ i"
+by (simp add: is_omult_fun_def omult_eqns_def lt_def, blast)
+
+lemma (in M_recursion) is_omult_fun_apply_Limit:
+ "[| x < j; Limit(x); M(j); M(f); is_omult_fun(M,i,j,f) |]
+ ==> f ` x = (\<Union>y\<in>x. f`y)"
+apply (simp add: is_omult_fun_def omult_eqns_def domain_closed lt_def, clarify)
+apply (drule subset_trans [OF OrdmemD], assumption+)
+apply (simp add: ball_conj_distrib omult_Limit image_function)
+done
+
+lemma (in M_recursion) is_omult_fun_eq_omult:
+ "[| is_omult_fun(M,i,J,f); M(J); M(f); Ord(i); Ord(j) |]
+ ==> j<J --> f`j = i**j"
+apply (erule_tac i=j in trans_induct3)
+apply (safe del: impCE)
+ apply (simp add: is_omult_fun_apply_0)
+ apply (subgoal_tac "x<J")
+ apply (simp add: is_omult_fun_apply_succ omult_succ)
+ apply (blast intro: lt_trans)
+apply (subgoal_tac "\<forall>k\<in>x. k<J")
+ apply (simp add: is_omult_fun_apply_Limit omult_Limit)
+apply (blast intro: lt_trans ltI lt_Ord)
+done
+
+lemma (in M_recursion) omult_abs_fun_apply_iff:
+ "[| M(i); M(J); M(f); M(k); j<J; is_omult_fun(M,i,J,f) |]
+ ==> fun_apply(M,f,j,k) <-> f`j = k"
+by (auto simp add: lt_def is_omult_fun_def subsetD apply_abs)
+
+lemma (in M_recursion) omult_abs:
+ "[| M(i); M(j); M(k); Ord(i); Ord(j) |] ==> is_omult(M,i,j,k) <-> k = i**j"
+apply (simp add: is_omult_def omult_abs_fun_apply_iff is_omult_fun_eq_omult)
+apply (frule exists_omult_fun [of j i], blast+)
+done
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/Wellorderings.thy Wed Jun 19 11:48:01 2002 +0200
@@ -0,0 +1,626 @@
+header {*Relativized Wellorderings*}
+
+theory Wellorderings = Relative:
+
+text{*We define functions analogous to @{term ordermap} @{term ordertype}
+ but without using recursion. Instead, there is a direct appeal
+ to Replacement. This will be the basis for a version relativized
+ to some class @{text M}. The main result is Theorem I 7.6 in Kunen,
+ page 17.*}
+
+
+subsection{*Wellorderings*}
+
+constdefs
+ irreflexive :: "[i=>o,i,i]=>o"
+ "irreflexive(M,A,r) == \<forall>x\<in>A. M(x) --> <x,x> \<notin> r"
+
+ transitive_rel :: "[i=>o,i,i]=>o"
+ "transitive_rel(M,A,r) ==
+ \<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> (\<forall>z\<in>A. M(z) -->
+ <x,y>\<in>r --> <y,z>\<in>r --> <x,z>\<in>r))"
+
+ linear_rel :: "[i=>o,i,i]=>o"
+ "linear_rel(M,A,r) ==
+ \<forall>x\<in>A. M(x) --> (\<forall>y\<in>A. M(y) --> <x,y>\<in>r | x=y | <y,x>\<in>r)"
+
+ wellfounded :: "[i=>o,i]=>o"
+ --{*EVERY non-empty set has an @{text r}-minimal element*}
+ "wellfounded(M,r) ==
+ \<forall>x. M(x) --> ~ empty(M,x)
+ --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
+ wellfounded_on :: "[i=>o,i,i]=>o"
+ --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*}
+ "wellfounded_on(M,A,r) ==
+ \<forall>x. M(x) --> ~ empty(M,x) --> subset(M,x,A)
+ --> (\<exists>y\<in>x. M(y) & ~(\<exists>z\<in>x. M(z) & <z,y> \<in> r))"
+
+ wellordered :: "[i=>o,i,i]=>o"
+ --{*every non-empty subset of @{text A} has an @{text r}-minimal element*}
+ "wellordered(M,A,r) ==
+ transitive_rel(M,A,r) & linear_rel(M,A,r) & wellfounded_on(M,A,r)"
+
+
+subsubsection {*Trivial absoluteness proofs*}
+
+lemma (in M_axioms) irreflexive_abs [simp]:
+ "M(A) ==> irreflexive(M,A,r) <-> irrefl(A,r)"
+by (simp add: irreflexive_def irrefl_def)
+
+lemma (in M_axioms) transitive_rel_abs [simp]:
+ "M(A) ==> transitive_rel(M,A,r) <-> trans[A](r)"
+by (simp add: transitive_rel_def trans_on_def)
+
+lemma (in M_axioms) linear_rel_abs [simp]:
+ "M(A) ==> linear_rel(M,A,r) <-> linear(A,r)"
+by (simp add: linear_rel_def linear_def)
+
+lemma (in M_axioms) wellordered_is_trans_on:
+ "[| wellordered(M,A,r); M(A) |] ==> trans[A](r)"
+by (auto simp add: wellordered_def )
+
+lemma (in M_axioms) wellordered_is_linear:
+ "[| wellordered(M,A,r); M(A) |] ==> linear(A,r)"
+by (auto simp add: wellordered_def )
+
+lemma (in M_axioms) wellordered_is_wellfounded_on:
+ "[| wellordered(M,A,r); M(A) |] ==> wellfounded_on(M,A,r)"
+by (auto simp add: wellordered_def )
+
+lemma (in M_axioms) wellfounded_imp_wellfounded_on:
+ "[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
+by (auto simp add: wellfounded_def wellfounded_on_def)
+
+
+subsubsection {*Well-founded relations*}
+
+lemma (in M_axioms) wellfounded_on_iff_wellfounded:
+ "wellfounded_on(M,A,r) <-> wellfounded(M, r \<inter> A*A)"
+apply (simp add: wellfounded_on_def wellfounded_def, safe)
+ apply blast
+apply (drule_tac x=x in spec, blast)
+done
+
+lemma (in M_axioms) wellfounded_on_induct:
+ "[| a\<in>A; wellfounded_on(M,A,r); M(A);
+ separation(M, \<lambda>x. x\<in>A --> ~P(x));
+ \<forall>x\<in>A. M(x) & (\<forall>y\<in>A. <y,x> \<in> r --> P(y)) --> P(x) |]
+ ==> P(a)";
+apply (simp (no_asm_use) add: wellfounded_on_def)
+apply (drule_tac x="{z\<in>A. z\<in>A --> ~P(z)}" in spec)
+apply (blast intro: transM)
+done
+
+text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
+ hypothesis by removing the restriction to @{term A}.*}
+lemma (in M_axioms) wellfounded_on_induct2:
+ "[| a\<in>A; wellfounded_on(M,A,r); M(A); r \<subseteq> A*A;
+ separation(M, \<lambda>x. x\<in>A --> ~P(x));
+ \<forall>x\<in>A. M(x) & (\<forall>y. <y,x> \<in> r --> P(y)) --> P(x) |]
+ ==> P(a)";
+by (rule wellfounded_on_induct, assumption+, blast)
+
+
+subsubsection {*Kunen's lemma IV 3.14, page 123*}
+
+lemma (in M_axioms) linear_imp_relativized:
+ "linear(A,r) ==> linear_rel(M,A,r)"
+by (simp add: linear_def linear_rel_def)
+
+lemma (in M_axioms) trans_on_imp_relativized:
+ "trans[A](r) ==> transitive_rel(M,A,r)"
+by (unfold transitive_rel_def trans_on_def, blast)
+
+lemma (in M_axioms) wf_on_imp_relativized:
+ "wf[A](r) ==> wellfounded_on(M,A,r)"
+apply (simp add: wellfounded_on_def wf_def wf_on_def, clarify)
+apply (drule_tac x="x" in spec, blast)
+done
+
+lemma (in M_axioms) wf_imp_relativized:
+ "wf(r) ==> wellfounded(M,r)"
+apply (simp add: wellfounded_def wf_def, clarify)
+apply (drule_tac x="x" in spec, blast)
+done
+
+lemma (in M_axioms) well_ord_imp_relativized:
+ "well_ord(A,r) ==> wellordered(M,A,r)"
+by (simp add: wellordered_def well_ord_def tot_ord_def part_ord_def
+ linear_imp_relativized trans_on_imp_relativized wf_on_imp_relativized)
+
+
+subsection{* Relativized versions of order-isomorphisms and order types *}
+
+lemma (in M_axioms) order_isomorphism_abs [simp]:
+ "[| M(A); M(B); M(f) |]
+ ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
+by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed
+ order_isomorphism_def ord_iso_def)
+
+
+lemma (in M_axioms) pred_set_abs [simp]:
+ "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
+apply (simp add: pred_set_def Order.pred_def)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) pred_closed [intro]:
+ "[| M(A); M(r); M(x) |] ==> M(Order.pred(A,x,r))"
+apply (simp add: Order.pred_def)
+apply (insert pred_separation [of r x], simp, blast)
+done
+
+lemma (in M_axioms) membership_abs [simp]:
+ "[| M(r); M(A) |] ==> membership(M,A,r) <-> r = Memrel(A)"
+apply (simp add: membership_def Memrel_def, safe)
+ apply (rule equalityI)
+ apply clarify
+ apply (frule transM, assumption)
+ apply blast
+ apply clarify
+ apply (subgoal_tac "M(<xb,ya>)", blast)
+ apply (blast dest: transM)
+ apply auto
+done
+
+lemma (in M_axioms) M_Memrel_iff:
+ "M(A) ==>
+ 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)}"
+apply (simp add: Memrel_def)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) Memrel_closed [intro]:
+ "M(A) ==> M(Memrel(A))"
+apply (simp add: M_Memrel_iff)
+apply (insert Memrel_separation, simp, blast)
+done
+
+
+subsection {* Main results of Kunen, Chapter 1 section 6 *}
+
+text{*Subset properties-- proved outside the locale*}
+
+lemma linear_rel_subset:
+ "[| linear_rel(M,A,r); B<=A |] ==> linear_rel(M,B,r)"
+by (unfold linear_rel_def, blast)
+
+lemma transitive_rel_subset:
+ "[| transitive_rel(M,A,r); B<=A |] ==> transitive_rel(M,B,r)"
+by (unfold transitive_rel_def, blast)
+
+lemma wellfounded_on_subset:
+ "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)"
+by (unfold wellfounded_on_def subset_def, blast)
+
+lemma wellordered_subset:
+ "[| wellordered(M,A,r); B<=A |] ==> wellordered(M,B,r)"
+apply (unfold wellordered_def)
+apply (blast intro: linear_rel_subset transitive_rel_subset
+ wellfounded_on_subset)
+done
+
+text{*Inductive argument for Kunen's Lemma 6.1, etc.
+ Simple proof from Halmos, page 72*}
+lemma (in M_axioms) wellordered_iso_subset_lemma:
+ "[| wellordered(M,A,r); f \<in> ord_iso(A,r, A',r); A'<= A; y \<in> A;
+ M(A); M(f); M(r) |] ==> ~ <f`y, y> \<in> r"
+apply (unfold wellordered_def ord_iso_def)
+apply (elim conjE CollectE)
+apply (erule wellfounded_on_induct, assumption+)
+ apply (insert well_ord_iso_separation [of A f r])
+ apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify)
+apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
+done
+
+
+text{*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
+ of a well-ordering*}
+lemma (in M_axioms) wellordered_iso_predD:
+ "[| wellordered(M,A,r); f \<in> ord_iso(A, r, Order.pred(A,x,r), r);
+ M(A); M(f); M(r) |] ==> x \<notin> A"
+apply (rule notI)
+apply (frule wellordered_iso_subset_lemma, assumption)
+apply (auto elim: predE)
+(*Now we know ~ (f`x < x) *)
+apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+(*Now we also know f`x \<in> pred(A,x,r); contradiction! *)
+apply (simp add: Order.pred_def)
+done
+
+
+lemma (in M_axioms) wellordered_iso_pred_eq_lemma:
+ "[| f \<in> \<langle>Order.pred(A,y,r), r\<rangle> \<cong> \<langle>Order.pred(A,x,r), r\<rangle>;
+ wellordered(M,A,r); x\<in>A; y\<in>A; M(A); M(f); M(r) |] ==> <x,y> \<notin> r"
+apply (frule wellordered_is_trans_on, assumption)
+apply (rule notI)
+apply (drule_tac x2=y and x=x and r2=r in
+ wellordered_subset [OF _ pred_subset, THEN wellordered_iso_predD])
+apply (simp add: trans_pred_pred_eq)
+apply (blast intro: predI dest: transM)+
+done
+
+
+text{*Simple consequence of Lemma 6.1*}
+lemma (in M_axioms) wellordered_iso_pred_eq:
+ "[| wellordered(M,A,r);
+ f \<in> ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r);
+ M(A); M(f); M(r); a\<in>A; c\<in>A |] ==> a=c"
+apply (frule wellordered_is_trans_on, assumption)
+apply (frule wellordered_is_linear, assumption)
+apply (erule_tac x=a and y=c in linearE, auto)
+apply (drule ord_iso_sym)
+(*two symmetric cases*)
+apply (blast dest: wellordered_iso_pred_eq_lemma)+
+done
+
+lemma (in M_axioms) wellfounded_on_asym:
+ "[| wellfounded_on(M,A,r); <a,x>\<in>r; a\<in>A; x\<in>A; M(A) |] ==> <x,a>\<notin>r"
+apply (simp add: wellfounded_on_def)
+apply (drule_tac x="{x,a}" in spec)
+apply (simp add: cons_closed)
+apply (blast dest: transM)
+done
+
+lemma (in M_axioms) wellordered_asym:
+ "[| wellordered(M,A,r); <a,x>\<in>r; a\<in>A; x\<in>A; M(A) |] ==> <x,a>\<notin>r"
+by (simp add: wellordered_def, blast dest: wellfounded_on_asym)
+
+
+text{*Surely a shorter proof using lemmas in @{text Order}?
+ Like well_ord_iso_preserving?*}
+lemma (in M_axioms) ord_iso_pred_imp_lt:
+ "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
+ g \<in> ord_iso(Order.pred(A,y,r), r, j, Memrel(j));
+ wellordered(M,A,r); x \<in> A; y \<in> A; M(A); M(r); M(f); M(g); M(j);
+ Ord(i); Ord(j); \<langle>x,y\<rangle> \<in> r |]
+ ==> i < j"
+apply (frule wellordered_is_trans_on, assumption)
+apply (frule_tac y=y in transM, assumption)
+apply (rule_tac i=i and j=j in Ord_linear_lt, auto)
+txt{*case @{term "i=j"} yields a contradiction*}
+ apply (rule_tac x1=x and A1="Order.pred(A,y,r)" in
+ wellordered_iso_predD [THEN notE])
+ apply (blast intro: wellordered_subset [OF _ pred_subset])
+ apply (simp add: trans_pred_pred_eq)
+ apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
+ apply (simp_all add: pred_iff pred_closed converse_closed comp_closed)
+txt{*case @{term "j<i"} also yields a contradiction*}
+apply (frule restrict_ord_iso2, assumption+)
+apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun])
+apply (frule apply_type, blast intro: ltD)
+ --{*thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}*}
+apply (simp add: pred_iff)
+apply (subgoal_tac
+ "\<exists>h. M(h) & h \<in> ord_iso(Order.pred(A,y,r), r,
+ Order.pred(A, converse(f)`j, r), r)")
+ apply (clarify, frule wellordered_iso_pred_eq, assumption+)
+ apply (blast dest: wellordered_asym)
+apply (intro exI conjI)
+ prefer 2 apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)+
+done
+
+
+lemma ord_iso_converse1:
+ "[| f: ord_iso(A,r,B,s); <b, f`a>: s; a:A; b:B |]
+ ==> <converse(f) ` b, a> : r"
+apply (frule ord_iso_converse, assumption+)
+apply (blast intro: ord_iso_is_bij [THEN bij_is_fun, THEN apply_funtype])
+apply (simp add: left_inverse_bij [OF ord_iso_is_bij])
+done
+
+
+subsection {* Order Types: A Direct Construction by Replacement*}
+
+text{*This follows Kunen's Theorem I 7.6, page 17.*}
+
+constdefs
+
+ obase :: "[i=>o,i,i,i] => o"
+ --{*the domain of @{text om}, eventually shown to equal @{text A}*}
+ "obase(M,A,r,z) ==
+ \<forall>a. M(a) -->
+ (a \<in> z <->
+ (a\<in>A & (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) &
+ membership(M,x,mx) & pred_set(M,A,a,r,par) &
+ order_isomorphism(M,par,r,x,mx,g))))"
+
+
+ omap :: "[i=>o,i,i,i] => o"
+ --{*the function that maps wosets to order types*}
+ "omap(M,A,r,f) ==
+ \<forall>z. M(z) -->
+ (z \<in> f <->
+ (\<exists>a\<in>A. M(a) &
+ (\<exists>x g mx par. M(x) & M(g) & M(mx) & M(par) & ordinal(M,x) &
+ pair(M,a,x,z) & membership(M,x,mx) &
+ pred_set(M,A,a,r,par) &
+ order_isomorphism(M,par,r,x,mx,g))))"
+
+
+ otype :: "[i=>o,i,i,i] => o" --{*the order types themselves*}
+ "otype(M,A,r,i) == \<exists>f. M(f) & omap(M,A,r,f) & is_range(M,f,i)"
+
+
+
+lemma (in M_axioms) obase_iff:
+ "[| M(A); M(r); M(z) |]
+ ==> obase(M,A,r,z) <->
+ z = {a\<in>A. \<exists>x g. M(x) & M(g) & Ord(x) &
+ g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
+apply (simp add: obase_def Memrel_closed pred_closed)
+apply (rule iffI)
+ prefer 2 apply blast
+apply (rule equalityI)
+ apply (clarify, frule transM, assumption, rotate_tac -1, simp)
+apply (clarify, frule transM, assumption, force)
+done
+
+text{*Can also be proved with the premise @{term "M(z)"} instead of
+ @{term "M(f)"}, but that version is less useful.*}
+lemma (in M_axioms) omap_iff:
+ "[| omap(M,A,r,f); M(A); M(r); M(f) |]
+ ==> z \<in> f <->
+ (\<exists>a\<in>A. \<exists>x g. M(x) & M(g) & z = <a,x> & Ord(x) &
+ g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
+apply (rotate_tac 1)
+apply (simp add: omap_def Memrel_closed pred_closed)
+apply (rule iffI)
+apply (drule_tac x=z in spec, blast dest: transM)+
+done
+
+lemma (in M_axioms) omap_unique:
+ "[| omap(M,A,r,f); omap(M,A,r,f'); M(A); M(r); M(f); M(f') |] ==> f' = f"
+apply (rule equality_iffI)
+apply (simp add: omap_iff)
+done
+
+lemma (in M_axioms) omap_yields_Ord:
+ "[| omap(M,A,r,f); \<langle>a,x\<rangle> \<in> f; M(a); M(x) |] ==> Ord(x)"
+apply (simp add: omap_def, blast)
+done
+
+lemma (in M_axioms) otype_iff:
+ "[| otype(M,A,r,i); M(A); M(r); M(i) |]
+ ==> x \<in> i <->
+ (\<exists>a\<in>A. \<exists>g. M(x) & M(g) & Ord(x) &
+ g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
+apply (simp add: otype_def, auto)
+ apply (blast dest: transM)
+ apply (blast dest!: omap_iff intro: transM)
+apply (rename_tac a g)
+apply (rule_tac a=a in rangeI)
+apply (frule transM, assumption)
+apply (simp add: omap_iff, blast)
+done
+
+lemma (in M_axioms) otype_eq_range:
+ "[| omap(M,A,r,f); otype(M,A,r,i); M(A); M(r); M(f); M(i) |] ==> i = range(f)"
+apply (auto simp add: otype_def omap_iff)
+apply (blast dest: omap_unique)
+done
+
+
+lemma (in M_axioms) Ord_otype:
+ "[| otype(M,A,r,i); trans[A](r); M(A); M(r); M(i) |] ==> Ord(i)"
+apply (rotate_tac 1)
+apply (rule OrdI)
+prefer 2
+ apply (simp add: Ord_def otype_def omap_def)
+ apply clarify
+ apply (frule pair_components_in_M, assumption)
+ apply blast
+apply (auto simp add: Transset_def otype_iff)
+ apply (blast intro: transM)
+apply (rename_tac y a g)
+apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun,
+ THEN apply_funtype], assumption)
+apply (rule_tac x="converse(g)`y" in bexI)
+ apply (frule_tac a="converse(g) ` y" in ord_iso_restrict_pred, assumption)
+apply (safe elim!: predE)
+apply (intro conjI exI)
+prefer 3
+ apply (blast intro: restrict_ord_iso ord_iso_sym ltI)
+ apply (blast intro: transM)
+ apply (blast intro: Ord_in_Ord)
+done
+
+lemma (in M_axioms) domain_omap:
+ "[| omap(M,A,r,f); obase(M,A,r,B); M(A); M(r); M(B); M(f) |]
+ ==> domain(f) = B"
+apply (rotate_tac 2)
+apply (simp add: domain_closed obase_iff)
+apply (rule equality_iffI)
+apply (simp add: domain_iff omap_iff, blast)
+done
+
+lemma (in M_axioms) omap_subset:
+ "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i) |] ==> f \<subseteq> B * i"
+apply (rotate_tac 3, clarify)
+apply (simp add: omap_iff obase_iff)
+apply (force simp add: otype_iff)
+done
+
+lemma (in M_axioms) omap_funtype:
+ "[| omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> B -> i"
+apply (rotate_tac 3)
+apply (simp add: domain_omap omap_subset Pi_iff function_def omap_iff)
+apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
+done
+
+
+lemma (in M_axioms) wellordered_omap_bij:
+ "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> bij(B,i)"
+apply (insert omap_funtype [of A r f B i])
+apply (auto simp add: bij_def inj_def)
+prefer 2 apply (blast intro: fun_is_surj dest: otype_eq_range)
+apply (frule_tac a="w" in apply_Pair, assumption)
+apply (frule_tac a="x" in apply_Pair, assumption)
+apply (simp add: omap_iff)
+apply (blast intro: wellordered_iso_pred_eq ord_iso_sym ord_iso_trans)
+done
+
+
+text{*This is not the final result: we must show @{term "oB(A,r) = A"}*}
+lemma (in M_axioms) omap_ord_iso:
+ "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(B,r,i,Memrel(i))"
+apply (rule ord_isoI)
+ apply (erule wellordered_omap_bij, assumption+)
+apply (insert omap_funtype [of A r f B i], simp)
+apply (frule_tac a="x" in apply_Pair, assumption)
+apply (frule_tac a="y" in apply_Pair, assumption)
+apply (auto simp add: omap_iff)
+ txt{*direction 1: assuming @{term "\<langle>x,y\<rangle> \<in> r"}*}
+ apply (blast intro: ltD ord_iso_pred_imp_lt)
+ txt{*direction 2: proving @{term "\<langle>x,y\<rangle> \<in> r"} using linearity of @{term r}*}
+apply (rename_tac x y g ga)
+apply (frule wellordered_is_linear, assumption,
+ erule_tac x=x and y=y in linearE, assumption+)
+txt{*the case @{term "x=y"} leads to immediate contradiction*}
+apply (blast elim: mem_irrefl)
+txt{*the case @{term "\<langle>y,x\<rangle> \<in> r"}: handle like the opposite direction*}
+apply (blast dest: ord_iso_pred_imp_lt ltD elim: mem_asym)
+done
+
+lemma (in M_axioms) Ord_omap_image_pred:
+ "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i); b \<in> A |] ==> Ord(f `` Order.pred(A,b,r))"
+apply (frule wellordered_is_trans_on, assumption)
+apply (rule OrdI)
+ prefer 2 apply (simp add: image_iff omap_iff Ord_def, blast)
+txt{*Hard part is to show that the image is a transitive set.*}
+apply (rotate_tac 3)
+apply (simp add: Transset_def, clarify)
+apply (simp add: image_iff pred_iff apply_iff [OF omap_funtype [of A r f B i]])
+apply (rename_tac c j, clarify)
+apply (frule omap_funtype [of A r f B, THEN apply_funtype], assumption+)
+apply (subgoal_tac "j : i")
+ prefer 2 apply (blast intro: Ord_trans Ord_otype)
+apply (subgoal_tac "converse(f) ` j : B")
+ prefer 2
+ apply (blast dest: wellordered_omap_bij [THEN bij_converse_bij,
+ THEN bij_is_fun, THEN apply_funtype])
+apply (rule_tac x="converse(f) ` j" in bexI)
+ apply (simp add: right_inverse_bij [OF wellordered_omap_bij])
+apply (intro predI conjI)
+ apply (erule_tac b=c in trans_onD)
+ apply (rule ord_iso_converse1 [OF omap_ord_iso [of A r f B i]])
+apply (auto simp add: obase_iff)
+done
+
+lemma (in M_axioms) restrict_omap_ord_iso:
+ "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ D \<subseteq> B; M(A); M(r); M(f); M(B); M(i) |]
+ ==> restrict(f,D) \<in> (\<langle>D,r\<rangle> \<cong> \<langle>f``D, Memrel(f``D)\<rangle>)"
+apply (frule ord_iso_restrict_image [OF omap_ord_iso [of A r f B i]],
+ assumption+)
+apply (drule ord_iso_sym [THEN subset_ord_iso_Memrel])
+apply (blast dest: subsetD [OF omap_subset])
+apply (drule ord_iso_sym, simp)
+done
+
+lemma (in M_axioms) obase_equals:
+ "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i) |] ==> B = A"
+apply (rotate_tac 4)
+apply (rule equalityI, force simp add: obase_iff, clarify)
+apply (subst obase_iff [of A r B, THEN iffD1], assumption+, simp)
+apply (frule wellordered_is_wellfounded_on, assumption)
+apply (erule wellfounded_on_induct, assumption+)
+ apply (insert obase_equals_separation, simp add: Memrel_closed pred_closed, clarify)
+apply (rename_tac b)
+apply (subgoal_tac "Order.pred(A,b,r) <= B")
+ prefer 2 apply (force simp add: pred_iff obase_iff)
+apply (intro conjI exI)
+ prefer 4 apply (blast intro: restrict_omap_ord_iso)
+apply (blast intro: Ord_omap_image_pred)+
+done
+
+
+
+text{*Main result: @{term om} gives the order-isomorphism
+ @{term "\<langle>A,r\<rangle> \<cong> \<langle>i, Memrel(i)\<rangle>"} *}
+theorem (in M_axioms) omap_ord_iso_otype:
+ "[| wellordered(M,A,r); omap(M,A,r,f); obase(M,A,r,B); otype(M,A,r,i);
+ M(A); M(r); M(f); M(B); M(i) |] ==> f \<in> ord_iso(A, r, i, Memrel(i))"
+apply (frule omap_ord_iso, assumption+)
+apply (frule obase_equals, assumption+, blast)
+done
+
+lemma (in M_axioms) obase_exists:
+ "[| M(A); M(r) |] ==> \<exists>z. M(z) & obase(M,A,r,z)"
+apply (simp add: obase_def)
+apply (insert obase_separation [of A r])
+apply (simp add: separation_def)
+done
+
+lemma (in M_axioms) omap_exists:
+ "[| M(A); M(r) |] ==> \<exists>z. M(z) & omap(M,A,r,z)"
+apply (insert obase_exists [of A r])
+apply (simp add: omap_def)
+apply (insert omap_replacement [of A r])
+apply (simp add: strong_replacement_def, clarify)
+apply (drule_tac x=z in spec, clarify)
+apply (simp add: Memrel_closed pred_closed obase_iff)
+apply (erule impE)
+ apply (clarsimp simp add: univalent_def)
+ apply (blast intro: Ord_iso_implies_eq ord_iso_sym ord_iso_trans, clarify)
+apply (rule_tac x=Y in exI)
+apply (simp add: Memrel_closed pred_closed obase_iff, blast)
+done
+
+lemma (in M_axioms) otype_exists:
+ "[| wellordered(M,A,r); M(A); M(r) |] ==> \<exists>i. M(i) & otype(M,A,r,i)"
+apply (insert omap_exists [of A r])
+apply (simp add: otype_def, clarify)
+apply (rule_tac x="range(z)" in exI)
+apply blast
+done
+
+theorem (in M_axioms) omap_ord_iso_otype:
+ "[| wellordered(M,A,r); M(A); M(r) |]
+ ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
+apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
+apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
+apply (rule Ord_otype)
+ apply (force simp add: otype_def range_closed)
+ apply (simp_all add: wellordered_is_trans_on)
+done
+
+lemma (in M_axioms) ordertype_exists:
+ "[| wellordered(M,A,r); M(A); M(r) |]
+ ==> \<exists>f. M(f) & (\<exists>i. M(i) & Ord(i) & f \<in> ord_iso(A, r, i, Memrel(i)))"
+apply (insert obase_exists [of A r] omap_exists [of A r] otype_exists [of A r], simp, clarify)
+apply (subgoal_tac "Ord(i)", blast intro: omap_ord_iso_otype)
+apply (rule Ord_otype)
+ apply (force simp add: otype_def range_closed)
+ apply (simp_all add: wellordered_is_trans_on)
+done
+
+
+lemma (in M_axioms) relativized_imp_well_ord:
+ "[| wellordered(M,A,r); M(A); M(r) |] ==> well_ord(A,r)"
+apply (insert ordertype_exists [of A r], simp)
+apply (blast intro: well_ord_ord_iso well_ord_Memrel )
+done
+
+subsection {*Kunen's theorem 5.4, poage 127*}
+
+text{*(a) The notion of Wellordering is absolute*}
+theorem (in M_axioms) well_ord_abs [simp]:
+ "[| M(A); M(r) |] ==> wellordered(M,A,r) <-> well_ord(A,r)"
+by (blast intro: well_ord_imp_relativized relativized_imp_well_ord)
+
+
+text{*(b) Order types are absolute*}
+lemma (in M_axioms)
+ "[| wellordered(M,A,r); f \<in> ord_iso(A, r, i, Memrel(i));
+ M(A); M(r); M(f); M(i); Ord(i) |] ==> i = ordertype(A,r)"
+by (blast intro: Ord_ordertype relativized_imp_well_ord ordertype_ord_iso
+ Ord_iso_implies_eq ord_iso_sym ord_iso_trans)
+
+end