equal
deleted
inserted
replaced
64 apply (blast dest!: sym [THEN RepFun_eq_0_iff [THEN iffD1]]) |
64 apply (blast dest!: sym [THEN RepFun_eq_0_iff [THEN iffD1]]) |
65 done |
65 done |
66 |
66 |
67 lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a" |
67 lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a" |
68 apply clarify |
68 apply clarify |
69 apply (rule subst_elem , (assumption)) |
69 apply (rule subst_elem, assumption) |
70 apply (fast elim: notE subst_elem) |
70 apply (fast elim: notE subst_elem) |
71 done |
71 done |
72 |
72 |
73 lemma lemma1_2: |
73 lemma lemma1_2: |
74 "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B); a \<in> A |] |
74 "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi>B \<in> {uu(a). a \<in> A}. B); a \<in> A |] |
96 lemma AC19_AC1: "AC19 ==> AC1" |
96 lemma AC19_AC1: "AC19 ==> AC1" |
97 apply (unfold AC19_def AC1_def, clarify) |
97 apply (unfold AC19_def AC1_def, clarify) |
98 apply (case_tac "A=0", force) |
98 apply (case_tac "A=0", force) |
99 apply (erule_tac x = "{uu (a) . a \<in> A}" in allE) |
99 apply (erule_tac x = "{uu (a) . a \<in> A}" in allE) |
100 apply (erule impE) |
100 apply (erule impE) |
101 apply (erule RepRep_conj , (assumption)) |
101 apply (erule RepRep_conj, assumption) |
102 apply (rule lemma1) |
102 apply (rule lemma1) |
103 apply (drule lemma2 , (assumption)) |
103 apply (drule lemma2, assumption, auto) |
104 apply auto |
|
105 done |
104 done |
106 |
105 |
107 end |
106 end |