Theory AC7_AC9
theory AC7_AC9
imports AC_Equiv
begin
lemma Sigma_fun_space_not0: "⟦0∉A; B ∈ A⟧ ⟹ (nat->⋃(A)) * B ≠ 0"
by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])
lemma inj_lemma:
"C ∈ A ⟹ (λg ∈ (nat->⋃(A))*C.
(λn ∈ nat. if(n=0, snd(g), fst(g)`(n #- 1))))
∈ inj((nat->⋃(A))*C, (nat->⋃(A)) ) "
unfolding inj_def
apply (rule CollectI)
apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto)
apply (rule fun_extension, assumption+)
apply (drule lam_eqE [OF _ nat_succI], assumption, simp)
apply (drule lam_eqE [OF _ nat_0I], simp)
done
lemma Sigma_fun_space_eqpoll:
"⟦C ∈ A; 0∉A⟧ ⟹ (nat->⋃(A)) * C ≈ (nat->⋃(A))"
apply (rule eqpollI)
apply (simp add: lepoll_def)
apply (fast intro!: inj_lemma)
apply (fast elim!: prod_lepoll_self not_sym [THEN not_emptyE] subst_elem
elim: swap)
done
lemma AC6_AC7: "AC6 ⟹ AC7"
by (unfold AC6_def AC7_def, blast)
lemma lemma1_1: "y ∈ (∏B ∈ A. Y*B) ⟹ (λB ∈ A. snd(y`B)) ∈ (∏B ∈ A. B)"
by (fast intro!: lam_type snd_type apply_type)
lemma lemma1_2:
"y ∈ (∏B ∈ {Y*C. C ∈ A}. B) ⟹ (λB ∈ A. y`(Y*B)) ∈ (∏B ∈ A. Y*B)"
apply (fast intro!: lam_type apply_type)
done
lemma AC7_AC6_lemma1:
"(∏B ∈ {(nat->⋃(A))*C. C ∈ A}. B) ≠ 0 ⟹ (∏B ∈ A. B) ≠ 0"
by (fast intro!: equals0I lemma1_1 lemma1_2)
lemma AC7_AC6_lemma2: "0 ∉ A ⟹ 0 ∉ {(nat -> ⋃(A)) * C. C ∈ A}"
by (blast dest: Sigma_fun_space_not0)
lemma AC7_AC6: "AC7 ⟹ AC6"
unfolding AC6_def AC7_def
apply (rule allI)
apply (rule impI)
apply (case_tac "A=0", simp)
apply (rule AC7_AC6_lemma1)
apply (erule allE)
apply (blast del: notI
intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans
Sigma_fun_space_eqpoll)
done
lemma AC1_AC8_lemma1:
"∀B ∈ A. ∃B1 B2. B=⟨B1,B2⟩ ∧ B1 ≈ B2
⟹ 0 ∉ { bij(fst(B),snd(B)). B ∈ A }"
apply (unfold eqpoll_def, auto)
done
lemma AC1_AC8_lemma2:
"⟦f ∈ (∏X ∈ RepFun(A,p). X); D ∈ A⟧ ⟹ (λx ∈ A. f`p(x))`D ∈ p(D)"
apply (simp, fast elim!: apply_type)
done
lemma AC1_AC8: "AC1 ⟹ AC8"
unfolding AC1_def AC8_def
apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2)
done
lemma AC8_AC9_lemma:
"∀B1 ∈ A. ∀B2 ∈ A. B1 ≈ B2
⟹ ∀B ∈ A*A. ∃B1 B2. B=⟨B1,B2⟩ ∧ B1 ≈ B2"
by fast
lemma AC8_AC9: "AC8 ⟹ AC9"
unfolding AC8_def AC9_def
apply (intro allI impI)
apply (erule allE)
apply (erule impE, erule AC8_AC9_lemma, force)
done
lemma snd_lepoll_SigmaI: "b ∈ B ⟹ X ≲ B × X"
by (blast intro: lepoll_trans prod_lepoll_self eqpoll_imp_lepoll
prod_commute_eqpoll)
lemma nat_lepoll_lemma:
"⟦0 ∉ A; B ∈ A⟧ ⟹ nat ≲ ((nat → ⋃(A)) × B) × nat"
by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)
lemma AC9_AC1_lemma1:
"⟦0∉A; A≠0;
C = {((nat->⋃(A))*B)*nat. B ∈ A} ∪
{cons(0,((nat->⋃(A))*B)*nat). B ∈ A};
B1 ∈ C; B2 ∈ C⟧
⟹ B1 ≈ B2"
by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
nat_cons_eqpoll [THEN eqpoll_trans]
prod_eqpoll_cong [OF _ eqpoll_refl]
intro: eqpoll_trans eqpoll_sym )
lemma AC9_AC1_lemma2:
"∀B1 ∈ {(F*B)*N. B ∈ A} ∪ {cons(0,(F*B)*N). B ∈ A}.
∀B2 ∈ {(F*B)*N. B ∈ A} ∪ {cons(0,(F*B)*N). B ∈ A}.
f`⟨B1,B2⟩ ∈ bij(B1, B2)
⟹ (λB ∈ A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) ∈ (∏X ∈ A. X)"
apply (intro lam_type snd_type fst_type)
apply (rule apply_type [OF _ consI1])
apply (fast intro!: fun_weaken_type bij_is_fun)
done
lemma AC9_AC1: "AC9 ⟹ AC1"
unfolding AC1_def AC9_def
apply (intro allI impI)
apply (erule allE)
apply (case_tac "A≠0")
apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force)
done
end