section‹A pointed version of DC›
theory Pointed_DC imports ZF.AC
begin
txt‹This proof of DC is from Moschovakis "Notes on Set Theory"›
consts dc_witness :: "i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i"
primrec
wit0 : "dc_witness(0,A,a,s,R) = a"
witrec :"dc_witness(succ(n),A,a,s,R) = s`{x∈A. ⟨dc_witness(n,A,a,s,R),x⟩∈R }"
lemma witness_into_A [TC]: "a∈A ⟹ n∈nat ⟹
(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
dc_witness(n, A, a, s, R)∈A"
apply (induct_tac n ,simp+)
apply (drule_tac x="dc_witness(x, A, a, s, R)" in bspec, assumption)
apply (drule_tac x="{xa ∈ A . ⟨dc_witness(x, A, a, s, R), xa⟩ ∈ R}" in spec)
apply auto
done
lemma witness_related : "a∈A ⟹ n∈nat ⟹
(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
⟨dc_witness(n, A, a, s, R),dc_witness(succ(n), A, a, s, R)⟩∈R"
apply (frule_tac n="n" and s="s" and R="R" in witness_into_A, assumption+)
apply (drule_tac x="dc_witness(n, A, a, s, R)" in bspec, assumption)
apply (drule_tac x= "{x ∈ A . ⟨dc_witness(n, A, a, s, R), x⟩ ∈ R}" in spec)
apply (simp, blast)
done
lemma witness_funtype: "a∈A ⟹
(∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
(λn∈nat. dc_witness(n, A, a, s, R)) ∈ nat → A"
apply (rule_tac B="{dc_witness(n, A, a, s, R). n∈nat}" in fun_weaken_type)
apply (rule lam_funtype)
apply ( blast intro:witness_into_A)
done
lemma witness_to_fun: "a∈A ⟹ (∀X . X≠0 ∧ X⊆A ⟶ s`X∈X) ⟹
∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0 ⟹
∃f ∈ nat→A. ∀n∈nat. f`n =dc_witness(n,A,a,s,R)"
apply (rule_tac x="λn∈nat. dc_witness(n,A,a,s,R)" in bexI, simp)
apply (rule witness_funtype, simp+)
done
theorem pointed_DC : "(∀x∈A. ∃y∈A. ⟨x,y⟩∈ R) ⟹
∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈R))"
apply (rule)
apply (insert AC_func_Pow)
apply (drule allI)
apply (drule_tac x="A" in spec)
apply (drule_tac P="λf .∀x∈Pow(A) - {0}. f ` x ∈ x"
and A="Pow(A)-{0}→ A"
and Q=" ∃f∈nat→ A. f ` 0 = a ∧ (∀n∈nat. ⟨f ` n, f ` succ(n)⟩ ∈ R)" in bexE)
prefer 2 apply (assumption)
apply (rename_tac s)
apply (rule_tac x="λn∈nat. dc_witness(n,A,a,s,R)" in bexI)
prefer 2 apply (blast intro:witness_funtype)
apply (rule conjI, simp)
apply (rule ballI, rename_tac m)
apply (subst beta, simp)+
apply (rule witness_related, auto)
done
lemma aux_DC_on_AxNat2 : "∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R ⟹
∀x∈A×nat. ∃y∈A×nat. ⟨x,y⟩ ∈ {⟨a,b⟩∈R. snd(b) = succ(snd(a))}"
apply (rule ballI, erule_tac x="x" in ballE, simp_all)
done
lemma infer_snd : "c∈ A×B ⟹ snd(c) = k ⟹ c=⟨fst(c),k⟩"
by auto
corollary DC_on_A_x_nat :
"(∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R) ⟹
∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨⟨f`n,n⟩,⟨f`succ(n),succ(n)⟩⟩∈R))"
apply (frule aux_DC_on_AxNat2)
apply (drule_tac R="{⟨a,b⟩∈R. snd(b) = succ(snd(a))}" in pointed_DC)
apply (rule ballI)
apply (rotate_tac)
apply (drule_tac x="⟨a,0⟩" in bspec, simp)
apply (erule bexE, rename_tac g)
apply (rule_tac x="λx∈nat. fst(g`x)" and A="nat→A" in bexI, auto)
apply (subgoal_tac "∀n∈nat. g`n= ⟨fst(g ` n), n⟩")
prefer 2 apply (rule ballI, rename_tac m)
apply (induct_tac m, simp)
apply (rename_tac d, auto)
apply (frule_tac A="nat" and x="d" in bspec, simp)
apply (rule_tac A="A" and B="nat" in infer_snd, auto)
apply (rule_tac a="⟨fst(g ` d), d⟩" and b="g ` d" in ssubst, assumption)
apply (subst snd_conv, simp)
done
lemma aux_sequence_DC : "⋀R. ∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n ⟹
R={⟨⟨x,n⟩,⟨y,m⟩⟩∈(A×nat)×(A×nat). ⟨x,y⟩∈S`m } ⟹
∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R"
apply (rule ballI, rename_tac v)
apply (frule Pair_fst_snd_eq)
apply (erule_tac x="fst(v)" in ballE)
apply (drule_tac x="succ(snd(v))" in bspec, auto)
done
lemma aux_sequence_DC2 : "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n ⟹
∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ {⟨⟨x,n⟩,⟨y,m⟩⟩∈(A×nat)×(A×nat). ⟨x,y⟩∈S`m }"
by auto
lemma sequence_DC: "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n ⟹
∀a∈A. (∃f ∈ nat→A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈S`succ(n)))"
apply (drule aux_sequence_DC2)
apply (drule DC_on_A_x_nat, auto)
done
end