# HG changeset patch # User paulson # Date 1024480081 -7200 # Node ID 45be08fbdcff364d0ca753e7ff42be2b88b12369 # Parent 74d9144c452c607b3c4b9256255e5a58245762bb new theory of inner models diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Formula.thy --- /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) \ 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|] + ==> \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 "\z\A. x = f(z)") + prefer 2 apply (blast del: allE elim: equalityE, clarify) +apply (subgoal_tac "B = {f(u) . u \ A - {z}}") + apply (blast intro: Diff_sing_Finite) +apply (thin_tac "\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: + "(\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 \ 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 \ 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) ==> \k. i \k. ii" + "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 \ formula; q \ formula |] ==> Or(p,q) \ formula" +by (simp add: Or_def) + +lemma Implies_type [TC]: + "[| p \ formula; q \ formula |] ==> Implies(p,q) \ formula" +by (simp add: Implies_def) + +lemma Exists_type [TC]: "p \ formula ==> Exists(p) \ 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)) = + (\env \ list(A). bool_of_o (nth(x,env) \ nth(y,env)))" + + "satisfies(A,Equal(x,y)) = + (\env \ list(A). bool_of_o (nth(x,env) = nth(y,env)))" + + "satisfies(A,Neg(p)) = + (\env \ list(A). not(satisfies(A,p)`env))" + + "satisfies(A,And(p,q)) = + (\env \ list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))" + + "satisfies(A,Forall(p)) = + (\env \ list(A). bool_of_o (\x\A. satisfies(A,p) ` (Cons(x,env)) = 1))" + + +lemma "p \ formula ==> satisfies(A,p) \ 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 \ list(A) + ==> sats(A, Member(x,y), env) <-> nth(x,env) \ nth(y,env)" +by simp + +lemma [simp]: + "env \ list(A) + ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)" +by simp + +lemma sats_Neg_iff [simp]: + "env \ 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 \ 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 \ list(A) + ==> sats(A, Forall(p), env) <-> (\x\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 \ 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 \ 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 \ list(A) + ==> sats(A, Exists(p), env) <-> (\x\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 incr_var(x,lev) = x" +by (simp add: incr_var_def) + +lemma incr_var_le: "lev\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)) = + (\lev \ nat. Member (incr_var(x,lev), incr_var(y,lev)))" + + "incr_bv(Equal(x,y)) = + (\lev \ nat. Equal (incr_var(x,lev), incr_var(y,lev)))" + + "incr_bv(Neg(p)) = + (\lev \ nat. Neg(incr_bv(p)`lev))" + + "incr_bv(And(p,q)) = + (\lev \ nat. And (incr_bv(p)`lev, incr_bv(q)`lev))" + + "incr_bv(Forall(p)) = + (\lev \ nat. Forall (incr_bv(p) ` succ(lev)))" + + +constdefs incr_boundvars :: "i => i" + "incr_boundvars(p) == incr_bv(p)`0" + + +lemma [TC]: "x \ nat ==> incr_var(x,lev) \ nat" +by (simp add: incr_var_def) + +lemma incr_bv_type [TC]: "p \ formula ==> incr_bv(p) \ nat -> formula" +by (induct_tac p, simp_all) + +lemma incr_boundvars_type [TC]: "p \ formula ==> incr_boundvars(p) \ 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 \ formula; env \ list(A); x \ A |] + ==> \bvs \ 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 \ formula; env \ list(A); x \ 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 \ formula; n \ nat |] + ==> \bvs \ list(A). \env \ 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) \ succ(y)" + + "arity(Equal(x,y)) = succ(x) \ succ(y)" + + "arity(Neg(p)) = arity(p)" + + "arity(And(p,q)) = arity(p) \ arity(q)" + + "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))" + + +lemma arity_type [TC]: "p \ formula ==> arity(p) \ nat" +by (induct_tac p, simp_all) + +lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \ arity(q)" +by (simp add: Or_def) + +lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \ 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 \ formula; extra \ list(A) |] + ==> \env \ list(A). + arity(p) \ 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) \ succ(length(env)); p \ formula; x \ A; env \ list(A); + extra \ 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 \ nat; y \ nat; lev \ x |] + ==> succ(x) \ incr_var(y,lev) = succ(x \ 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 \ succ(x) = succ(x \ 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 \ formula + ==> \n \ 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 \ 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 \ formula; n \ 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 \ formula ==> incr_bv1(p) \ 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 \ formula; env \ list(A); x \ A; y \ 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 \ formula; n \ nat; x \ A |] + ==> \bvs \ list(A). \env \ 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 \ 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 \ formula; n \ 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 \ Pow(A). + \env \ list(A). \p \ formula. + arity(p) \ succ(length(env)) & + X = {x\A. sats(A, p, Cons(x,env))}}" + +lemma DPowI: + "[|X <= A; env \ list(A); p \ formula; + arity(p) \ succ(length(env))|] + ==> {x\A. sats(A, p, Cons(x,env))} \ DPow(A)" +by (simp add: DPow_def, blast) + +lemma DPowD: + "X \ DPow(A) + ==> X <= A & + (\env \ list(A). + \p \ formula. arity(p) \ succ(length(env)) & + X = {x\A. sats(A, p, Cons(x,env))})" +by (simp add: DPow_def) + +lemmas DPow_imp_subset = DPowD [THEN conjunct1] + +(*Lemma 1.2*) +lemma "[| p \ formula; env \ list(A); arity(p) \ succ(length(env)) |] + ==> {x\A. sats(A, p, Cons(x,env))} \ 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 \ 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 \ DPow(A) ==> (A-X) \ 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 \ DPow(A); Y \ DPow(A) |] ==> X Int Y \ 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 \ DPow(A); Y \ DPow(A) |] ==> X Un Y \ 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 \ A ==> {x} \ 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 \ A; X \ DPow(A) |] ==> cons(a,X) \ 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 \ Fin(A) ==> X \ 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. \y\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\x; A \ DPow(Lset(y))|] ==> A \ Lset(x)"; +by (subst Lset, blast) + +lemma LsetD: "A \ Lset(x) ==> \y\x. A \ DPow(Lset(y))"; +apply (insert Lset [of x]) +apply (blast intro: elim: equalityE) +done + +subsubsection{* Transitivity *} + +lemma elem_subset_in_DPow: "[|X \ A; X \ A|] ==> X \ 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(\(X)) = (\y\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) = (\y\i. Lset(y))" +by (simp add: Lset_Union [symmetric] Limit_Union_eq) + +lemma lt_LsetI: "[| a: Lset(j); j 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 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 \ 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 \ nat; y \ nat |] ==> subset_fm(x,y) \ formula" +by (simp add: subset_fm_def) + +lemma arity_subset_fm [simp]: + "[| x \ nat; y \ nat |] ==> arity(subset_fm(x,y)) = succ(x) \ succ(y)" +by (simp add: subset_fm_def succ_Un_distrib [symmetric]) + +lemma sats_subset_fm [simp]: + "[|x < length(env); y \ nat; env \ list(A); Transset(A)|] + ==> sats(A, subset_fm(x,y), env) <-> nth(x,env) \ 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 \ nat ==> transset_fm(x) \ formula" +by (simp add: transset_fm_def) + +lemma arity_transset_fm [simp]: + "x \ 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 \ 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 \ nat ==> ordinal_fm(x) \ formula" +by (simp add: ordinal_fm_def) + +lemma arity_ordinal_fm [simp]: + "x \ 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 \ 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 \ A. Ord(x)} \ 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\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) \ DPow(Lset(x)) \ 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 \ Lset(i)" +by (subst Ords_of_Lset_eq [symmetric], assumption, fast) + +lemma Ord_in_Lset: "Ord(i) ==> i \ 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 \ Lset(j) ==> Union(X) \ 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 "\y. y \ X \ x \ 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) |] ==> : 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) |] ==> : 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 \ 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) == \i. Ord(i) & x \ Lset(i)" + + lrank :: "i=>i" --{*Kunen's definition VI, 1.7*} + "lrank(x) == \i. x \ Lset(succ(i))" + +lemma L_I: "[|x \ Lset(i); Ord(i)|] ==> L(x)" +by (simp add: L_def, blast) + +lemma L_D: "L(x) ==> \i. Ord(i) & x \ 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 \ 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 \ 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="\i. x \ Lset(succ(i))" in LeastI, assumption) +apply (blast intro!: le_imp_subset Lset_mono [THEN subsetD]) +done + +lemma Lset_succ_lrank_iff [simp]: "x \ 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) \ 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 \ 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 \ X |] ==> y \ (\y\Pow(X). Lset(succ(lrank(y))))" +by (auto intro: L_I iff: Lset_succ_lrank_iff) + +lemma LPow_in_Lset: + "[|X \ Lset(i); Ord(i)|] ==> \j. Ord(j) & {y \ Pow(X). L(y)} \ Lset(j)" +apply (rule_tac x="succ(\y \ 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 \ 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 \ Pow(X). L(y)})" +by (blast intro: L_I dest: L_D LPow_in_Lset) + +end diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/L_axioms.thy --- /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\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 \ 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 \ Lset(i); univalent(L,X,Q); Ord(i)|] + ==> \j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \ Lset(j)" +apply (rule_tac x="\y \ 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)|] + ==> \Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \ 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, \x. \y\A. L(y) --> x\y)" + and cartprod_separation: + "[| L(A); L(B) |] + ==> separation(M, \z. \x\A. \y\B. L(x) & L(y) & pair(M,x,y,z))" + and image_separation: + "[| L(A); L(r) |] + ==> separation(M, \y. \p\r. L(p) & (\x\A. L(x) & pair(M,x,y,p)))" + and vimage_separation: + "[| L(A); L(r) |] + ==> separation(M, \x. \p\r. L(p) & (\y\A. L(x) & pair(M,x,y,p)))" + and converse_separation: + "L(r) ==> separation(M, \z. \p\r. L(p) & (\x y. L(x) & L(y) & + pair(M,x,y,p) & pair(M,y,x,z)))" + and restrict_separation: + "L(A) + ==> separation(M, \z. \x\A. L(x) & (\y. L(y) & pair(M,x,y,z)))" + and comp_separation: + "[| L(r); L(s) |] + ==> separation(M, \xz. \x y z. L(x) & L(y) & L(z) & + (\xy\s. \yz\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, \y. \p\r. L(p) & pair(M,y,x,p))" + and Memrel_separation: + "separation(M, \z. \x y. L(x) & L(y) & pair(M,x,y,z) \ x \ y)" + and obase_separation: + --{*part of the order type formalization*} + "[| L(A); L(r) |] + ==> separation(M, \a. \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, \x. x\A --> (\y. L(y) \ (\p. L(p) \ + fun_apply(M,f,x,y) \ pair(M,y,x,p) \ p \ r)))" + and obase_equals_separation: + "[| L(A); L(r) |] + ==> separation + (M, \x. x\A --> ~(\y. L(y) & (\g. L(g) & + ordinal(M,y) & (\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, \x. x \ A --> \x,a\ \ r \ \x,b\ \ r \ f`x \ g`x)" + and omap_replacement: + "[| L(A); L(r) |] + ==> strong_replacement(M, + \a z. \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 diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Normal.thy --- /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) == \I. I \ 0 --> (\i\I. Ord(i) \ P(i)) --> P(\(I))" + + Unbounded :: "(i=>o) => o" + "Unbounded(P) == \i. Ord(i) --> (\j. i P(j))" + + Closed_Unbounded :: "(i=>o) => o" + "Closed_Unbounded(P) == Closed(P) \ Unbounded(P)" + + +subsubsection{*Simple facts about c.u. classes*} + +lemma ClosedI: + "[| !!I. [| I \ 0; \i\I. Ord(i) \ P(i) |] ==> P(\(I)) |] + ==> Closed(P)" +by (simp add: Closed_def) + +lemma ClosedD: + "[| Closed(P); I \ 0; !!i. i\I ==> Ord(i); !!i. i\I ==> P(i) |] + ==> P(\(I))" +by (simp add: Closed_def) + +lemma UnboundedD: + "[| Unbounded(P); Ord(i) |] ==> \j. i 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(\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\A ==> Closed(P(a))" + and unbounded: "a\A ==> Unbounded(P(a))" + and A_non0: "A\0" + defines "next_greater(a,x) == \y. x P(a,y)" + and "sup_greater(x) == \a\A. next_greater(a,x)" + + +text{*Trivial that the intersection is closed.*} +lemma (in cub_family) Closed_INT: "Closed(\x. \i\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\A |] ==> P(a, next_greater(a,x)) \ 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\A |] ==> P(a, next_greater(a,x))" +by (blast dest: next_greater_lemma) + +lemma (in cub_family) next_greater_gt: + "[| Ord(x); a\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\A ==> next_greater(a,x) \ 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\A |] + ==> sup_greater^\ (x) = + (\n\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\A |] ==> P(a, sup_greater^\ (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^\ (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(\x. \a\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(\x. \a\A. P(a,x))" +by (simp add: Closed_Unbounded_def Closed_INT Unbounded_INT) + + +theorem Closed_Unbounded_INT: + "(!!a. a\A ==> Closed_Unbounded(P(a))) + ==> Closed_Unbounded(\x. \a\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) \ Q(x) <-> (\i\2. (i=0 --> P(x)) \ (i=1 --> Q(x)))" +by auto + +theorem Closed_Unbounded_Int: + "[| Closed_Unbounded(P); Closed_Unbounded(Q) |] + ==> Closed_Unbounded(\x. P(x) \ 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) == \i j. i\j --> M(i) \ M(j)" + + mono_Ord :: "(i=>i) => o" + "mono_Ord(F) == \i j. i F(i) < F(j)" + + cont_Ord :: "(i=>i) => o" + "cont_Ord(F) == \l. Limit(l) --> F(l) = (\ii) => o" + "Normal(F) == mono_Ord(F) \ cont_Ord(F)" + + +subsubsection{*Immediate properties of the definitions*} + +lemma NormalI: + "[|!!i j. i F(i) < F(j); !!l. Limit(l) ==> F(l) = (\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 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) = (\i F(i) < F(j)" +by (simp add: Normal_def mono_Ord_def) + +lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\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 "(\y (\y mono_le_subset(F)" +apply (simp add: mono_le_subset_def, clarify) +apply (subgoal_tac "F(i)\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; \x\X. Ord(x) |] + ==> F(Union(X)) = (\y\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 "\X \ 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(\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\0; \x\X. Ord(x); Normal(F) |] ==> F(Union(X)) = (\y\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(\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\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\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^\ (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^\ (a)) = F^\ (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 \ F^\ (a)" +apply (unfold iterates_omega_def) +apply (rule UN_upper_le [of 0], simp_all) +done + +lemma Normal_imp_fp_Unbounded: "Normal(F) ==> Unbounded(\i. F(i) = i)" +apply (unfold Unbounded_def, clarify) +apply (rule_tac x="F^\ (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(\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), \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)) |] + ==> \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) \ 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, \x r. csucc(r))" + +syntax (xsymbols) + Aleph :: "i => i" ("\_" [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) ==> \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 + diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/ROOT.ML --- /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"; diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Reflection.thy --- /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: "(\x. P(x)) <-> (~ (\x. ~ P(x)))"; +by blast + +lemma ball_iff_not_bex_not: "(\x\A. P(x)) <-> (~ (\x\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 "\y\Mset(a). \z\Mset(a). P() <-> Q(a,)"}, 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 \ Mset(a); y \ Mset(a); Limit(a) |] + ==> \ Mset(a)" + defines "M(x) == \a. Ord(a) \ x \ Mset(a)" + and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) \ + (\a. Cl(a) --> (\x\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\Mset(a)"}*} + fixes ClEx --{*Reflecting ordinals for the formula @{term "\z. P"}*} + defines "F0(P,y) == \b. (\z. M(z) \ P()) --> + (\z\Mset(b). P())" + and "FF(P) == \a. \y\Mset(a). F0(P,y)" + and "ClEx(P) == \a. Limit(a) \ normalize(FF(P),a) = a" + +lemma (in reflection) Mset_mono: "i\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, \a x. P(x))" +by (simp add: Reflects_def) + +theorem (in reflection) Not_reflection [intro]: + "Reflects(Cl,P,Q) ==> Reflects(Cl, \x. ~P(x), \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(\a. Cl(a) \ C'(a), \x. P(x) \ P'(x), + \a x. Q(a,x) \ 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(\a. Cl(a) \ C'(a), \x. P(x) \ P'(x), + \a x. Q(a,x) \ 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(\a. Cl(a) \ C'(a), + \x. P(x) --> P'(x), + \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(\a. Cl(a) \ C'(a), + \x. P(x) <-> P'(x), + \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\Mset(a); Ord(a); M(z); P() |] ==> \z\Mset(F0(P,y)). P()" +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\Mset(a)"}, +while @{term FF} depends only upon @{term a}. *} +lemma (in reflection) FF_works: + "[| M(z); y\Mset(a); P(); Ord(a) |] ==> \z\Mset(FF(P,a)). P()" +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\Mset(a); P(); Ord(a) |] + ==> \z\Mset(normalize(FF(P),a)). P()" +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) |] ==> \x\Mset(a). P(x) <-> Q(a,x)" + +lemma (in ex_reflection) ClEx_downward: + "[| M(z); y\Mset(a); P(); Cl(a); ClEx(P,a) |] + ==> \z\Mset(a). Q(a,)" +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\Mset(a); y\Mset(a); Q(a,); Cl(a); ClEx(P,a) |] + ==> \z. M(z) \ P()" +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\Mset(a); Cl(a); ClEx(P,a) |] + ==> (\z. M(z) \ P()) <-> (\z\Mset(a). Q(a,))" +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\Mset(a); Cl(a); ClEx(P,a); + !!a. [| Cl(a); Ord(a) |] ==> \x\Mset(a). P(x) <-> Q(a,x) |] + ==> (\z. M(z) \ P()) <-> (\z\Mset(a). Q(a,))" +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) |] ==> \x\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(\a. Cl(a) \ ClEx(P0,a), + \x. \z. M(z) \ P0(), + \a x. \z\Mset(a). Q0(a,))" +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(\a. Cl(a) \ ClEx(\x.~P0(x), a), + \x. \z. M(z) --> P0(), + \a x. \z\Mset(a). Q0(a,))" +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, \x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))) + ==> Reflects(\a. Cl(a) \ ClEx(\x. P(fst(x),snd(x)), a), + \x. \z. M(z) \ P(x,z), + \a x. \z\Mset(a). Q(a,x,z))" +by (rule Ex_reflection_0 [of _ " \x. P(fst(x),snd(x))" + "\a x. Q(a,fst(x),snd(x))", simplified]) + +theorem (in reflection) All_reflection [intro]: + "Reflects(Cl, \x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))) + ==> Reflects(\a. Cl(a) \ ClEx(\x. ~P(fst(x),snd(x)), a), + \x. \z. M(z) --> P(x,z), + \a x. \z\Mset(a). Q(a,x,z))" +by (rule All_reflection_0 [of _ "\x. P(fst(x),snd(x))" + "\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, + \x. \y. M(y) \ x \ y, + \a x. \y\Mset(a). x \ 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(\a. Ord(a) \ ClEx(\x. fst(x) \ snd(x), a), + \x. \y. M(y) \ x \ y, + \a x. \y\Mset(a). x \ y)" +by fast + + +text{*Example 2*} +lemma (in reflection) + "Reflects(?Cl, + \x. \y. M(y) \ (\z. M(z) --> z \ x --> z \ y), + \a x. \y\Mset(a). \z\Mset(a). z \ x --> z \ y)" +by fast + +text{*Example 2'. We give the reflecting class explicitly. *} +lemma (in reflection) + "Reflects + (\a. (Ord(a) \ + ClEx(\x. ~ (snd(x) \ fst(fst(x)) --> snd(x) \ snd(fst(x))), a)) \ + ClEx(\x. \z. M(z) --> z \ fst(x) --> z \ snd(x), a), + \x. \y. M(y) \ (\z. M(z) --> z \ x --> z \ y), + \a x. \y\Mset(a). \z\Mset(a). z \ x --> z \ y)" +by fast + +text{*Example 2''. We expand the subset relation.*} +lemma (in reflection) + "Reflects(?Cl, + \x. \y. M(y) \ (\z. M(z) --> (\w. M(w) --> w\z --> w\x) --> z\y), + \a x. \y\Mset(a). \z\Mset(a). (\w\Mset(a). w\z --> w\x) --> z\y)" +by fast + +text{*Example 2'''. Single-step version, to reveal the reflecting class.*} +lemma (in reflection) + "Reflects(?Cl, + \x. \y. M(y) \ (\z. M(z) --> z \ x --> z \ y), + \a x. \y\Mset(a). \z\Mset(a). z \ x --> z \ 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, + \x. \y. M(y) \ (\z. M(z) --> z \ y <-> z \ x \ P(z)), + \a x. \y\Mset(a). \z\Mset(a). z \ y <-> z \ x \ P(z))" +by fast + +text{*Example 3'*} +lemma (in reflection) + "Reflects(?Cl, + \x. \y. M(y) \ y = Collect(x,P), + \a x. \y\Mset(a). y = Collect(x,P))"; +by fast + +text{*Example 3''*} +lemma (in reflection) + "Reflects(?Cl, + \x. \y. M(y) \ y = Replace(x,P), + \a x. \y\Mset(a). y = Replace(x,P))"; +by fast + +text{*Example 4: Axiom of Choice. Possibly wrong, since @{text \} needs +to be relativized.*} +lemma (in reflection) + "Reflects(?Cl, + \A. 0\A --> (\f. M(f) \ f \ (\X \ A. X)), + \a A. 0\A --> (\f\Mset(a). f \ (\X \ A. X)))" +by fast + +end + diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Relative.thy --- /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) == \x. M(x) --> x \ z" + + subset :: "[i=>o,i,i] => o" + "subset(M,A,B) == \x\A. M(x) --> x \ B" + + upair :: "[i=>o,i,i,i] => o" + "upair(M,a,b,z) == a \ z & b \ z & (\x\z. M(x) --> x = a | x = b)" + + pair :: "[i=>o,i,i,i] => o" + "pair(M,a,b,z) == \x. M(x) & upair(M,a,a,x) & + (\y. M(y) & upair(M,a,b,y) & upair(M,x,y,z))" + + successor :: "[i=>o,i,i] => o" + "successor(M,a,z) == \x. M(x) & upair(M,a,a,x) & union(M,x,a,z)" + + powerset :: "[i=>o,i,i] => o" + "powerset(M,A,z) == \x. M(x) --> (x \ z <-> subset(M,x,A))" + + union :: "[i=>o,i,i,i] => o" + "union(M,a,b,z) == \x. M(x) --> (x \ z <-> x \ a | x \ b)" + + inter :: "[i=>o,i,i,i] => o" + "inter(M,a,b,z) == \x. M(x) --> (x \ z <-> x \ a & x \ b)" + + setdiff :: "[i=>o,i,i,i] => o" + "setdiff(M,a,b,z) == \x. M(x) --> (x \ z <-> x \ a & x \ b)" + + big_union :: "[i=>o,i,i] => o" + "big_union(M,A,z) == \x. M(x) --> (x \ z <-> (\y\A. M(y) & x \ y))" + + big_inter :: "[i=>o,i,i] => o" + "big_inter(M,A,z) == + (A=0 --> z=0) & + (A\0 --> (\x. M(x) --> (x \ z <-> (\y\A. M(y) --> x \ y))))" + + cartprod :: "[i=>o,i,i,i] => o" + "cartprod(M,A,B,z) == + \u. M(u) --> (u \ z <-> (\x\A. M(x) & (\y\B. M(y) & pair(M,x,y,u))))" + + is_converse :: "[i=>o,i,i] => o" + "is_converse(M,r,z) == + \x. M(x) --> + (x \ z <-> + (\w\r. M(w) & + (\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) == + \x. M(x) --> (x \ z <-> (\w\r. M(w) & (\y\A. M(y) & pair(M,x,y,w))))" + + is_domain :: "[i=>o,i,i] => o" + "is_domain(M,r,z) == + \x. M(x) --> (x \ z <-> (\w\r. M(w) & (\y. M(y) & pair(M,x,y,w))))" + + image :: "[i=>o,i,i,i] => o" + "image(M,r,A,z) == + \y. M(y) --> (y \ z <-> (\w\r. M(w) & (\x\A. M(x) & pair(M,x,y,w))))" + + is_range :: "[i=>o,i,i] => o" + --{*the cleaner + @{term "\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) == + \y. M(y) --> (y \ z <-> (\w\r. M(w) & (\x. M(x) & pair(M,x,y,w))))" + + is_relation :: "[i=>o,i] => o" + "is_relation(M,r) == + (\z\r. M(z) --> (\x y. M(x) & M(y) & pair(M,x,y,z)))" + + is_function :: "[i=>o,i] => o" + "is_function(M,r) == + (\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\r --> p'\r --> + y=y')" + + fun_apply :: "[i=>o,i,i,i] => o" + "fun_apply(M,f,x,y) == + (\y'. M(y') --> ((\u\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) & + (\u\r. M(u) --> (\x y. M(x) & M(y) & pair(M,x,y,u) --> y\B))" + + injection :: "[i=>o,i,i,i] => o" + "injection(M,A,B,f) == + typed_function(M,A,B,f) & + (\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\f --> p'\f --> + x=x')" + + surjection :: "[i=>o,i,i,i] => o" + "surjection(M,A,B,f) == + typed_function(M,A,B,f) & + (\y\B. M(y) --> (\x\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) == + \x. M(x) --> + (x \ z <-> + (x \ r & (\u\A. M(u) & (\v. M(v) & pair(M,u,v,x)))))" + + transitive_set :: "[i=>o,i] => o" + "transitive_set(M,a) == \x\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) & (\x\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) & + (\x\a. M(x) --> (\y\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) & + (\x\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) & (\x\a. M(x) --> ~ limit_ordinal(M,x))" + + number1 :: "[i=>o,i] => o" + "number1(M,a) == (\x. M(x) & empty(M,x) & successor(M,x,a))" + + number2 :: "[i=>o,i] => o" + "number2(M,a) == (\x. M(x) & number1(M,x) & successor(M,x,a))" + + number3 :: "[i=>o,i] => o" + "number3(M,a) == (\x. M(x) & number2(M,x) & successor(M,x,a))" + + +subsection {*The relativized ZF axioms*} +constdefs + + extensionality :: "(i=>o) => o" + "extensionality(M) == + \x y. M(x) --> M(y) --> (\z. M(z) --> (z \ x <-> z \ 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) == + \z. M(z) --> (\y. M(y) & (\x. M(x) --> (x \ y <-> x \ z & P(x))))" + + upair_ax :: "(i=>o) => o" + "upair_ax(M) == \x y. M(x) --> M(y) --> (\z. M(z) & upair(M,x,y,z))" + + Union_ax :: "(i=>o) => o" + "Union_ax(M) == \x. M(x) --> (\z. M(z) & big_union(M,x,z))" + + power_ax :: "(i=>o) => o" + "power_ax(M) == \x. M(x) --> (\z. M(z) & powerset(M,x,z))" + + univalent :: "[i=>o, i, [i,i]=>o] => o" + "univalent(M,A,P) == + (\x\A. M(x) --> (\y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))" + + replacement :: "[i=>o, [i,i]=>o] => o" + "replacement(M,P) == + \A. M(A) --> univalent(M,A,P) --> + (\Y. M(Y) & (\b. M(b) --> ((\x\A. M(x) & P(x,b)) --> b \ Y)))" + + strong_replacement :: "[i=>o, [i,i]=>o] => o" + "strong_replacement(M,P) == + \A. M(A) --> univalent(M,A,P) --> + (\Y. M(Y) & (\b. M(b) --> (b \ Y <-> (\x\A. M(x) & P(x,b)))))" + + foundation_ax :: "(i=>o) => o" + "foundation_ax(M) == + \x. M(x) --> (\y\x. M(y)) + --> (\y\x. M(y) & ~(\z\x. M(z) & z \ 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 \ x; x \ univ(0) |] ==> y \ univ(0)" +apply (insert Transset_univ [OF Transset_0]) +apply (simp add: Transset_def, blast) +done + +lemma univ0_Ball_abs [simp]: + "A \ univ(0) ==> (\x\A. x \ univ(0) --> P(x)) <-> (\x\A. P(x))" +by (blast intro: univ0_downwards_mem) + +lemma univ0_Bex_abs [simp]: + "A \ univ(0) ==> (\x\A. x \ univ(0) & P(x)) <-> (\x\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\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(\x. x \ 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 \ Vfrom(A,j); Transset(A) |] ==> Collect(X,P) \ Vfrom(A, succ(j))" +apply (drule Transset_Vfrom) +apply (rule subset_mem_Vfrom) +apply (unfold Transset_def, blast) +done + +lemma Collect_in_VLimit: + "[| X \ Vfrom(A,i); Limit(i); Transset(A) |] + ==> Collect(X,P) \ Vfrom(A,i)" +apply (rule Limit_VfromE, assumption+) +apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom) +done + +lemma Collect_in_univ: + "[| X \ univ(A); Transset(A) |] ==> Collect(X,P) \ univ(A)" +by (simp add: univ_def Collect_in_VLimit Limit_nat) + +lemma "separation(\x. x \ univ(0), P)" +apply (simp add: separation_def) +apply (blast intro: Collect_in_univ Transset_0) +done + +text{*Unordered pairing axiom*} +lemma "upair_ax(\x. x \ univ(0))" +apply (simp add: upair_ax_def upair_def) +apply (blast intro: doubleton_in_univ) +done + +text{*Union axiom*} +lemma "Union_ax(\x. x \ 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 \ univ(A); Transset(A) |] ==> Pow(X) \ univ(A)" +apply (simp add: univ_def Pow_in_VLimit Limit_nat) +done + +lemma "power_ax(\x. x \ 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(\x. x \ univ(0))" +apply (simp add: foundation_ax_def, clarify) +apply (cut_tac A=x in foundation, blast) +done + +lemma "replacement(\x. x \ 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 \ Union(Union(r)). \p\r. \x\A. p=}" +apply (rule equalityI, auto) +apply (simp add: Pair_def, blast) +done + +lemma vimage_iff_Collect: + "r -`` A = {x \ Union(Union(r)). \p\r. \y\A. p=}" +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) |] + ==> \Y. M(Y) & (\b. M(b) --> ((\x\A. M(x) & P(x,b)) --> b \ Y))" +by (simp add: replacement_def) + +lemma strong_replacementD: + "[| strong_replacement(M,P); M(A); univalent(M,A,P) |] + ==> \Y. M(Y) & (\b. M(b) --> (b \ Y <-> (\x\A. M(x) & P(x,b))))" +by (simp add: strong_replacement_def) + +lemma separationD: + "[| separation(M,P); M(z) |] + ==> \y. M(y) & (\x. M(x) --> (x \ y <-> x \ 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) & + (\x\A. \y\A. \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\r <-> q\s))" + + + pred_set :: "[i=>o,i,i,i,i] => o" + "pred_set(M,A,x,r,B) == + \y. M(y) --> (y \ B <-> (\p\r. M(p) & y \ A & pair(M,y,x,p)))" + + membership :: "[i=>o,i,i] => o" --{*membership relation*} + "membership(M,A,r) == + \p. M(p) --> + (p \ r <-> (\x\A. \y\A. M(x) & M(y) & x\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\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, \x. \y\A. M(y) --> x\y)" + and cartprod_separation: + "[| M(A); M(B) |] + ==> separation(M, \z. \x\A. \y\B. M(x) & M(y) & pair(M,x,y,z))" + and image_separation: + "[| M(A); M(r) |] + ==> separation(M, \y. \p\r. M(p) & (\x\A. M(x) & pair(M,x,y,p)))" + and vimage_separation: + "[| M(A); M(r) |] + ==> separation(M, \x. \p\r. M(p) & (\y\A. M(x) & pair(M,x,y,p)))" + and converse_separation: + "M(r) ==> separation(M, \z. \p\r. M(p) & (\x y. M(x) & M(y) & + pair(M,x,y,p) & pair(M,y,x,z)))" + and restrict_separation: + "M(A) + ==> separation(M, \z. \x\A. M(x) & (\y. M(y) & pair(M,x,y,z)))" + and comp_separation: + "[| M(r); M(s) |] + ==> separation(M, \xz. \x y z. M(x) & M(y) & M(z) & + (\xy\s. \yz\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, \y. \p\r. M(p) & pair(M,y,x,p))" + and Memrel_separation: + "separation(M, \z. \x y. M(x) & M(y) & pair(M,x,y,z) \ x \ y)" + and obase_separation: + --{*part of the order type formalization*} + "[| M(A); M(r) |] + ==> separation(M, \a. \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, \x. x\A --> (\y. M(y) \ (\p. M(p) \ + fun_apply(M,f,x,y) \ pair(M,y,x,p) \ p \ r)))" + and obase_equals_separation: + "[| M(A); M(r) |] + ==> separation + (M, \x. x\A --> ~(\y. M(y) & (\g. M(g) & + ordinal(M,y) & (\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, \x. x \ A --> \x,a\ \ r \ \x,b\ \ r \ f`x \ g`x)" + and omap_replacement: + "[| M(A); M(r) |] + ==> strong_replacement(M, + \a z. \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) ==> (\x\A. M(x) --> P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_axioms) Bex_abs [simp]: + "M(A) ==> (\x\A. M(x) & P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_axioms) Ball_iff_equiv: + "M(A) ==> (\x. M(x) --> (x\A <-> P(x))) <-> + (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\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 \ 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=" +apply (simp add: pair_def ZF.Pair_def) +apply (blast intro: transM) +done + +lemma (in M_axioms) pair_in_M_iff [iff]: + "M() <-> M(a) & M(b)" +by (simp add: ZF.Pair_def) + +lemma (in M_axioms) pair_components_in_M: + "[| \ 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]: + "[| \A. M(A) --> separation(M, %u. \x\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, \x y. y = f(x)); M(A); \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); \u. M(u) --> u \ C <-> (\x\A. \y\B. u = {{x}, {x,y}}); + powerset(M, A \ B, p1); powerset(M, p1, p2); M(p2) |] + ==> C = {u \ p2 . \x\A. \y\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) <-> + (\p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) & + C = {z \ p2. \x\A. \y\B. z = })" +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="\x. M(x) --> Ex(?Q(x))" in spec) +apply (erule impE, blast, clarify) +apply (drule_tac x=z and P="\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) |] ==> \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="\x. M(x) --> Ex(?Q(x))" in spec) +apply (erule impE, blast, clarify) +apply (drule_tac x=z and P="\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 \ range(r) * domain(r). + \p\r. \x. M(x) \ (\y. M(y) \ p = \x,y\ \ z = \y,x\)}" +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 \ 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 \ A -> B; M(f); M(y) |] + ==> fun_apply(M,f,x,y) <-> x \ 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 \ 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 \ 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 \ 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 \ 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 \ r . \x\A. \y. M(y) & z = \x, y\}" +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 \ domain(s) * range(r). + \x. M(x) \ (\y. M(y) \ (\z. M(z) \ + xz = \x,z\ \ \x,y\ \ s \ \y,z\ \ 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 \ 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 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) & (\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); \x\a. ~ Limit(x) |] ==> a \ nat" +by (induct a rule: trans_induct3, simp_all) + +lemma naturals_not_limit: "a \ 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 \ 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); \x\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 \x\nat is essential because everything + but the recursion variable must stay unchanged. But then the recursion + equations only hold for x\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) = (\x\nat. if empty(M,x) then 1 else 0)" + "natnumber_aux(M,succ(n)) = + (\x\nat. if (\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 diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/WF_absolute.thy --- /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) \ succ(j) <-> i\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 \ A*A. \n\nat. \f \ succ(n) -> A. + \x y. p = & f`0 = x & f`n = y & + (\i\n. \ r)}" + +lemma alt_rtrancl_lemma1 [rule_format]: + "n \ nat + ==> \f \ succ(n) -> field(r). + (\i\n. \f`i, f ` succ(i)\ \ r) --> \f`0, f`n\ \ 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 \ A*A |] ==> + separation + (M, \x. x \ A --> + ~(\f. M(f) \ + is_recfun(r, x, %x f. \y \ r-``{x}. succ(f`y), f)))" + and wfrank_strong_replacement': + "[| M(r); M(a); r \ A*A |] ==> + strong_replacement(M, \x z. \y g. M(y) & M(g) & + pair(M,x,y,z) & + is_recfun(r, x, %x f. \y \ r-``{x}. succ(f`y), f) & + y = (\y \ 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} & + (\x. M(x) --> \ r --> f`x = (\y \ r-``{x}. succ(f`y)))" + + + + +lemma (in M_recursion) exists_wfrank: + "[| wellfounded(M,r); r \ A*A; a\A; M(r); M(A) |] + ==> \f. M(f) & is_recfun(r, a, %x g. (\y \ 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) |] ==> \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 (\k\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 f`j = i++j" +apply (erule_tac i=j in trans_induct, clarify) +apply (subgoal_tac "\k\x. k 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. \y \ r-``{x}. succ(f`y))" + +constdefs + wftype :: "i=>i" + "wftype(r) == \y \ range(r). succ(wfrank(r,y))" + +lemma (in M_axioms) wfrank: "wellfounded(M,r) ==> wfrank(r,a) = (\y \ 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); \ 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: "\wellfounded(M,r); x \ field(r)\ \ wfrank(r,x) \ 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 \ A*A|] ==> \i f. Ord(i) & r <= rvimage(A, f, Memrel(i))" +apply (rule_tac x="wftype(r)" in exI) +apply (rule_tac x="\x\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 diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/WFrec.thy --- /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 \ r -`` {a} \ range(f) & + (\x \ 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); \ r; r \ A*A |] + ==> r -`` {y} \ r -`` {x} = r -`` {y}" +by (blast intro: trans_onD) + +lemma trans_on_Int_eq2 [simp]: + "[| trans[A](r); \ r; r \ A*A |] + ==> r -`` {x} \ 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 \ A*A; x\A |] + ==> \ r --> \ 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. :f <-> :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 \ A*A; \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 \ 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); + \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] ==> + is_recfun(r,a,H,f) <-> + (\z. z \ f <-> (\x y. M(x) & M(y) & z= & \ 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); \y,x\ \ r; + M(A); M(r); M(f); + \x g. M(x) & M(g) & function(g) --> M(H(x,g)); r \ 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 \ A \ A; + \x g. M(x) \ M(g) & function(g) --> M(H(x,g)); M(Y); + \b. M(b) --> + b \ Y <-> + (\x\r -`` {a1}. + \y. M(y) \ + (\g. M(g) \ b = \x,y\ \ is_recfun(r,x,H,g) \ y = H(x,g))); + \x,a1\ \ r; M(f); is_recfun(r,x,H,f) |] + ==> restrict(Y, r -`` {x}) = f" +apply (subgoal_tac "ALL y : r-``{x}. ALL z. :Y <-> :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="" 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="" 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 \ A; \y. \y, a1\ \ r --> (\f. M(f) & is_recfun(r, y, H, f)); + wellfounded_on(M,A,r); trans[A](r); + strong_replacement(M, \x z. \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 \ A * A; + \x g. M(x) & M(g) & function(g) --> M(H(x,g))|] + ==> \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\A; + separation(M, \x. x \ A --> ~ (\f. M(f) \ is_recfun(r, x, H, f))); + strong_replacement(M, \x z. \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 \ A*A; + \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] + ==> \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\A; + strong_replacement(M, \x z. \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 \ A*A; + \x g. M(x) & M(g) & function(g) --> M(H(x,g)) |] + ==> \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 \ 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) == + \z. M(z) --> + (z \ f <-> + (\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 \ r & MH(M, x, f_r_sx, y)))" + +lemma (in M_axioms) is_recfun_iff_M: + "[| M(r); M(a); M(f); \x g. M(x) & M(g) & function(g) --> M(H(x,g)); + \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 "\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) == + (\sj msj. M(sj) --> M(msj) --> + successor(M,j,sj) --> membership(M,sj,msj) --> + M_is_recfun(M, msj, x, + %M x g y. \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) & + (\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) & + (\j. x = succ(j) --> z = g`j ++ i) & + (Limit(x) --> z = \(g``x))" + + is_omult_fun :: "[i=>o,i,i,i] => o" + "is_omult_fun(M,i,j,f) == + (\df. M(df) & is_function(M,f) & + is_domain(M,f,df) & subset(M, j, df)) & + (\x\j. omult_eqns(i,x,f,f`x))" + + is_omult :: "[i=>o,i,i,i] => o" + "is_omult(M,i,j,k) == + \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, + \x z. \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, \x z. \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\j; M(i); M(j); M(a); M(f) |] + ==> is_oadd_fun(M,i,j,a,f) <-> + f \ a \ range(f) & (\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, \x z. \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) |] + ==> \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) |] + ==> \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 (\k\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 f`j = i++j" +apply (erule_tac i=j in trans_induct, clarify) +apply (subgoal_tac "\k\x. k 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 = \(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)) = \(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) |] + ==> \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) |] ==> \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 = (\y\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 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 "xk\x. k 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 + diff -r 74d9144c452c -r 45be08fbdcff src/ZF/Constructible/Wellorderings.thy --- /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) == \x\A. M(x) --> \ r" + + transitive_rel :: "[i=>o,i,i]=>o" + "transitive_rel(M,A,r) == + \x\A. M(x) --> (\y\A. M(y) --> (\z\A. M(z) --> + \r --> \r --> \r))" + + linear_rel :: "[i=>o,i,i]=>o" + "linear_rel(M,A,r) == + \x\A. M(x) --> (\y\A. M(y) --> \r | x=y | \r)" + + wellfounded :: "[i=>o,i]=>o" + --{*EVERY non-empty set has an @{text r}-minimal element*} + "wellfounded(M,r) == + \x. M(x) --> ~ empty(M,x) + --> (\y\x. M(y) & ~(\z\x. M(z) & \ 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) == + \x. M(x) --> ~ empty(M,x) --> subset(M,x,A) + --> (\y\x. M(y) & ~(\z\x. M(z) & \ 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 \ 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\A; wellfounded_on(M,A,r); M(A); + separation(M, \x. x\A --> ~P(x)); + \x\A. M(x) & (\y\A. \ r --> P(y)) --> P(x) |] + ==> P(a)"; +apply (simp (no_asm_use) add: wellfounded_on_def) +apply (drule_tac x="{z\A. z\A --> ~P(z)}" in spec) +apply (blast intro: transM) +done + +text{*The assumption @{term "r \ A*A"} justifies strengthening the induction + hypothesis by removing the restriction to @{term A}.*} +lemma (in M_axioms) wellfounded_on_induct2: + "[| a\A; wellfounded_on(M,A,r); M(A); r \ A*A; + separation(M, \x. x\A --> ~P(x)); + \x\A. M(x) & (\y. \ 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 \ 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()", blast) + apply (blast dest: transM) + apply auto +done + +lemma (in M_axioms) M_Memrel_iff: + "M(A) ==> + Memrel(A) = {z \ A*A. \x. M(x) \ (\y. M(y) \ z = \x,y\ \ x \ 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 \ ord_iso(A,r, A',r); A'<= A; y \ A; + M(A); M(f); M(r) |] ==> ~ \ 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 \ ord_iso(A, r, Order.pred(A,x,r), r); + M(A); M(f); M(r) |] ==> x \ 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 \ pred(A,x,r); contradiction! *) +apply (simp add: Order.pred_def) +done + + +lemma (in M_axioms) wellordered_iso_pred_eq_lemma: + "[| f \ \Order.pred(A,y,r), r\ \ \Order.pred(A,x,r), r\; + wellordered(M,A,r); x\A; y\A; M(A); M(f); M(r) |] ==> \ 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 \ ord_iso(Order.pred(A,a,r), r, Order.pred(A,c,r), r); + M(A); M(f); M(r); a\A; c\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); \r; a\A; x\A; M(A) |] ==> \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); \r; a\A; x\A; M(A) |] ==> \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 \ ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); + g \ ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); + wellordered(M,A,r); x \ A; y \ A; M(A); M(r); M(f); M(g); M(j); + Ord(i); Ord(j); \x,y\ \ 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 Order.pred(A,x,r)"}*} +apply (simp add: pred_iff) +apply (subgoal_tac + "\h. M(h) & h \ 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); : s; a:A; b:B |] + ==> : 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) == + \a. M(a) --> + (a \ z <-> + (a\A & (\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) == + \z. M(z) --> + (z \ f <-> + (\a\A. M(a) & + (\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) == \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\A. \x g. M(x) & M(g) & Ord(x) & + g \ 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 \ f <-> + (\a\A. \x g. M(x) & M(g) & z = & Ord(x) & + g \ 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); \a,x\ \ 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 \ i <-> + (\a\A. \g. M(x) & M(g) & Ord(x) & + g \ 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 \ 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 \ 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 \ 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 \ 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 "\x,y\ \ r"}*} + apply (blast intro: ltD ord_iso_pred_imp_lt) + txt{*direction 2: proving @{term "\x,y\ \ 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 "\y,x\ \ 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 \ 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 \ B; M(A); M(r); M(f); M(B); M(i) |] + ==> restrict(f,D) \ (\D,r\ \ \f``D, Memrel(f``D)\)" +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 "\A,r\ \ \i, Memrel(i)\"} *} +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 \ 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) |] ==> \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) |] ==> \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) |] ==> \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) |] + ==> \f. M(f) & (\i. M(i) & Ord(i) & f \ 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) |] + ==> \f. M(f) & (\i. M(i) & Ord(i) & f \ 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 \ 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