(* Title: ZF/AC/AC16_lemmas.thy
Author: Krzysztof Grabczewski
Lemmas used in the proofs concerning AC16
*)
theory AC16_lemmas
imports AC_Equiv Hartog Cardinal_aux
begin
lemma cons_Diff_eq: "a\A ==> cons(a,A)-{a}=A"
by fast
lemma nat_1_lepoll_iff: "1\X \ (\x. x \ X)"
apply (unfold lepoll_def)
apply (rule iffI)
apply (fast intro: inj_is_fun [THEN apply_type])
apply (erule exE)
apply (rule_tac x = "\a \ 1. x" in exI)
apply (fast intro!: lam_injective)
done
lemma eqpoll_1_iff_singleton: "X\1 \ (\x. X={x})"
apply (rule iffI)
apply (erule eqpollE)
apply (drule nat_1_lepoll_iff [THEN iffD1])
apply (fast intro!: lepoll_1_is_sing)
apply (fast intro!: singleton_eqpoll_1)
done
lemma cons_eqpoll_succ: "[| x\n; y\x |] ==> cons(y,x)\succ(n)"
apply (unfold succ_def)
apply (fast elim!: cons_eqpoll_cong mem_irrefl)
done
lemma subsets_eqpoll_1_eq: "{Y \ Pow(X). Y\1} = {{x}. x \ X}"
apply (rule equalityI)
apply (rule subsetI)
apply (erule CollectE)
apply (drule eqpoll_1_iff_singleton [THEN iffD1])
apply (fast intro!: RepFunI)
apply (rule subsetI)
apply (erule RepFunE)
apply (rule CollectI, fast)
apply (fast intro!: singleton_eqpoll_1)
done
lemma eqpoll_RepFun_sing: "X\{{x}. x \ X}"
apply (unfold eqpoll_def bij_def)
apply (rule_tac x = "\x \ X. {x}" in exI)
apply (rule IntI)
apply (unfold inj_def surj_def, simp)
apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1], simp)
apply (fast intro!: lam_type)
done
lemma subsets_eqpoll_1_eqpoll: "{Y \ Pow(X). Y\1}\X"
apply (rule subsets_eqpoll_1_eq [THEN ssubst])
apply (rule eqpoll_RepFun_sing [THEN eqpoll_sym])
done
lemma InfCard_Least_in:
"[| InfCard(x); y \ x; y \ succ(z) |] ==> (\ i. i \ y) \ y"
apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll,
THEN succ_lepoll_imp_not_empty, THEN not_emptyE])
apply (fast intro: LeastI
dest!: InfCard_is_Card [THEN Card_is_Ord]
elim: Ord_in_Ord)
done
lemma subsets_lepoll_lemma1:
"[| InfCard(x); n \ nat |]
==> {y \<in> Pow(x). y\<approx>succ(succ(n))} \<lesssim> x*{y \<in> Pow(x). y\<approx>succ(n)}"
apply (unfold lepoll_def)
apply (rule_tac x = "\y \ {y \ Pow(x) . y\succ (succ (n))}.
<\<mu> i. i \<in> y, y-{\<mu> i. i \<in> y}>" in exI)
apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective)
apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in)
apply (simp, blast intro: InfCard_Least_in)
done
lemma set_of_Ord_succ_Union: "(\y \ z. Ord(y)) ==> z \ succ(\(z))"
apply (rule subsetI)
apply (case_tac "\y \ z. y \ x", blast )
apply (simp, erule bexE)
apply (rule_tac i=y and j=x in Ord_linear_le)
apply (blast dest: le_imp_subset elim: leE ltE)+
done
lemma subset_not_mem: "j \ i ==> i \ j"
by (fast elim!: mem_irrefl)
lemma succ_Union_not_mem:
"(!!y. y \ z ==> Ord(y)) ==> succ(\(z)) \ z"
apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
done
lemma Union_cons_eq_succ_Union:
"\(cons(succ(\(z)),z)) = succ(\(z))"
by fast
lemma Un_Ord_disj: "[| Ord(i); Ord(j) |] ==> i \ j = i | i \ j = j"
by (fast dest!: le_imp_subset elim: Ord_linear_le)
lemma Union_eq_Un: "x \ X ==> \(X) = x \ \(X-{x})"
by fast
lemma Union_in_lemma [rule_format]:
"n \ nat ==> \z. (\y \ z. Ord(y)) & z\n & z\0 \ \(z) \ z"
apply (induct_tac "n")
apply (fast dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
apply (intro allI impI)
apply (erule natE)
apply (fast dest!: eqpoll_1_iff_singleton [THEN iffD1]
intro!: Union_singleton, clarify)
apply (elim not_emptyE)
apply (erule_tac x = "z-{xb}" in allE)
apply (erule impE)
apply (fast elim!: Diff_sing_eqpoll
Diff_sing_eqpoll [THEN eqpoll_succ_imp_not_empty])
apply (subgoal_tac "xb \ \(z - {xb}) \ z")
apply (simp add: Union_eq_Un [symmetric])
apply (frule bspec, assumption)
apply (drule bspec)
apply (erule Diff_subset [THEN subsetD])
apply (drule Un_Ord_disj, assumption, auto)
done
lemma Union_in: "[| \x \ z. Ord(x); z\n; z\0; n \ nat |] ==> \(z) \ z"
by (blast intro: Union_in_lemma)
lemma succ_Union_in_x:
"[| InfCard(x); z \ Pow(x); z\n; n \ nat |] ==> succ(\(z)) \ x"
apply (rule Limit_has_succ [THEN ltE])
prefer 3 apply assumption
apply (erule InfCard_is_Limit)
apply (case_tac "z=0")
apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0])
apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]], assumption)
apply (blast intro: Union_in
InfCard_is_Card [THEN Card_is_Ord, THEN Ord_in_Ord])+
done
lemma succ_lepoll_succ_succ:
"[| InfCard(x); n \ nat |]
==> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
apply (unfold lepoll_def)
apply (rule_tac x = "\z \ {y\Pow(x). y\succ(n)}. cons(succ(\(z)), z)"
in exI)
apply (rule_tac d = "%z. z-{\(z) }" in lam_injective)
apply (blast intro!: succ_Union_in_x succ_Union_not_mem
intro: cons_eqpoll_succ Ord_in_Ord
dest!: InfCard_is_Card [THEN Card_is_Ord])
apply (simp only: Union_cons_eq_succ_Union)
apply (rule cons_Diff_eq)
apply (fast dest!: InfCard_is_Card [THEN Card_is_Ord]
elim: Ord_in_Ord
intro!: succ_Union_not_mem)
done
lemma subsets_eqpoll_X:
"[| InfCard(X); n \ nat |] ==> {Y \ Pow(X). Y\succ(n)} \ X"
apply (induct_tac "n")
apply (rule subsets_eqpoll_1_eqpoll)
apply (rule eqpollI)
apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+)
apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll])
apply (erule eqpoll_refl [THEN prod_eqpoll_cong])
apply (erule InfCard_square_eqpoll)
apply (fast elim: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
intro!: succ_lepoll_succ_succ)
done
lemma image_vimage_eq:
"[| f \ surj(A,B); y \ B |] ==> f``(converse(f)``y) = y"
apply (unfold surj_def)
apply (fast dest: apply_equality2 elim: apply_iff [THEN iffD2])
done
lemma vimage_image_eq: "[| f \ inj(A,B); y \ A |] ==> converse(f)``(f``y) = y"
by (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
lemma subsets_eqpoll:
"A\B ==> {Y \ Pow(A). Y\n}\{Y \ Pow(B). Y\n}"
apply (unfold eqpoll_def)
apply (erule exE)
apply (rule_tac x = "\X \ {Y \ Pow (A) . \f. f \ bij (Y, n) }. f``X" in exI)
apply (rule_tac d = "%Z. converse (f) ``Z" in lam_bijective)
apply (fast intro!: bij_is_inj [THEN restrict_bij, THEN bij_converse_bij,
THEN comp_bij]
elim!: bij_is_fun [THEN fun_is_rel, THEN image_subset])
apply (blast intro!: bij_is_inj [THEN restrict_bij]
comp_bij bij_converse_bij
bij_is_fun [THEN fun_is_rel, THEN image_subset])
apply (fast elim!: bij_is_inj [THEN vimage_image_eq])
apply (fast elim!: bij_is_surj [THEN image_vimage_eq])
done
lemma WO2_imp_ex_Card: "WO2 ==> \a. Card(a) & X\a"
apply (unfold WO2_def)
apply (drule spec [of _ X])
apply (blast intro: Card_cardinal eqpoll_trans
well_ord_Memrel [THEN well_ord_cardinal_eqpoll, THEN eqpoll_sym])
done
lemma lepoll_infinite: "[| X\Y; ~Finite(X) |] ==> ~Finite(Y)"
by (blast intro: lepoll_Finite)
lemma infinite_Card_is_InfCard: "[| ~Finite(X); Card(X) |] ==> InfCard(X)"
apply (unfold InfCard_def)
apply (fast elim!: Card_is_Ord [THEN nat_le_infinite_Ord])
done
lemma WO2_infinite_subsets_eqpoll_X: "[| WO2; n \ nat; ~Finite(X) |]
==> {Y \<in> Pow(X). Y\<approx>succ(n)}\<approx>X"
apply (drule WO2_imp_ex_Card)
apply (elim allE exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (drule infinite_Card_is_InfCard, assumption)
apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans)
done
lemma well_ord_imp_ex_Card: "well_ord(X,R) ==> \a. Card(a) & X\a"
by (fast elim!: well_ord_cardinal_eqpoll [THEN eqpoll_sym]
intro!: Card_cardinal)
lemma well_ord_infinite_subsets_eqpoll_X:
"[| well_ord(X,R); n \ nat; ~Finite(X) |] ==> {Y \ Pow(X). Y\succ(n)}\X"
apply (drule well_ord_imp_ex_Card)
apply (elim allE exE conjE)
apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
apply (drule infinite_Card_is_InfCard, assumption)
apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans)
done
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
