(* Title: ZF/AC/AC18_AC19.thy Author: Krzysztof Grabczewski The proof of AC1 \<Longrightarrow> AC18 \<Longrightarrow> AC19 \<Longrightarrow> AC1 theory AC18_AC19imports AC_Equivbegin definition "i \ i" where "uu(a) \ {c \ {0}. c \ a}" (* ********************************************************************** *) (* AC1 \<Longrightarrow> AC18 *) (* ********************************************************************** *) lemma PROD_subsets:"\f \ (\b \ {P(a). a \ A}. b); \a \ A. P(a)<=Q(a)\ \<Longrightarrow> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Prod>a \<in> A. Q(a))" by (rule lam_type, drule apply_type, auto)lemma lemma_AC18:"\\A. 0 \ A \ (\f. f \ (\X \ A. X)); A \ 0\ \<Longrightarrow> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> \<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))" apply (rule subsetI)apply (erule_tac x = "{{b \ B (a) . x \ X (a,b) }. a \ A}" in allE) apply (erule impE, fast)apply (erule exE)apply (rule UN_I)apply (fast elim!: PROD_subsets)apply (simp, fast elim!: not_emptyE dest: apply_type [OF _ RepFunI])done lemma AC1_AC18: "AC1 \ PROP AC18" unfolding AC1_defapply (rule AC18.intro)apply (fast elim!: lemma_AC18 apply_type intro!: equalityI INT_I UN_I)done (* ********************************************************************** *) (* AC18 \<Longrightarrow> AC19 *) (* ********************************************************************** *) theorem (in AC18) AC19unfolding AC19_defapply (intro allI impI)apply (rule AC18 [of _ "\x. x", THEN mp], blast) done (* ********************************************************************** *) (* AC19 \<Longrightarrow> AC1 *) (* ********************************************************************** *) lemma RepRep_conj: "\A \ 0; 0 \ A\ \ {uu(a). a \ A} \ 0 \ 0 \ {uu(a). a \ A}" apply (unfold uu_def, auto) apply (blast dest!: sym [THEN RepFun_eq_0_iff [THEN iffD1]])done lemma lemma1_1: "\c \ a; x = c \ {0}; x \ a\ \ x - {0} \ a" apply clarify apply (rule subst_elem, assumption)apply (fast elim: notE subst_elem)done lemma lemma1_2: "\f`(uu(a)) \ a; f \ (\B \ {uu(a). a \ A}. B); a \ A\ \<Longrightarrow> f`(uu(a))-{0} \<in> a" apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type)done lemma lemma1: "\f. f \ (\B \ {uu(a). a \ A}. B) \ \f. f \ (\B \ A. B)" apply (erule exE)apply (rule_tac x = "\a\A. if (f` (uu(a)) \ a, f` (uu(a)), f` (uu(a))-{0})" in exI)apply (rule lam_type) apply (simp add: lemma1_2)done lemma lemma2_1: "a\0 \ 0 \ (\b \ uu(a). b)" by (unfold uu_def, auto)lemma lemma2: "\A\0; 0\A\ \ (\x \ {uu(a). a \ A}. \b \ x. b) \ 0" apply (erule not_emptyE) apply (rule_tac a = 0 in not_emptyI)apply (fast intro!: lemma2_1)done lemma AC19_AC1: "AC19 \ AC1" apply (unfold AC19_def AC1_def, clarify)apply (case_tac "A=0" , force)apply (erule_tac x = "{uu (a) . a \ A}" in allE) apply (erule impE)apply (erule RepRep_conj, assumption)apply (rule lemma1)apply (drule lemma2, assumption, auto) done end quality 100%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
