Theory Pointed_DC_Relative
section‹Relative DC›
theory Pointed_DC_Relative
imports
Cardinal_Library_Relative
begin
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}"
lemmas dc_witness_def = dc_witness_nat_def
relativize functional "dc_witness" "dc_witness_rel"
relationalize "dc_witness_rel" "is_dc_witness"
schematic_goal sats_is_dc_witness_fm_auto:
assumes "na < length(env)" "e < length(env)"
shows
" na ∈ ω ⟹
A ∈ ω ⟹
a ∈ ω ⟹
s ∈ ω ⟹
R ∈ ω ⟹
e ∈ ω ⟹
env ∈ list(Aa) ⟹
0 ∈ Aa ⟹
is_dc_witness(##Aa, nth(na, env), nth(A, env), nth(a, env), nth(s, env), nth(R, env), nth(e, env)) ⟷
Aa, env ⊨ ?fm(nat, A, a, s, R, e)"
unfolding is_dc_witness_def is_recursor_def
by (rule is_transrec_iff_sats | simp_all)
(rule iff_sats is_nat_case_iff_sats is_eclose_iff_sats sep_rules | simp add:assms)+
synthesize "is_dc_witness" from_schematic
manual_arity for "is_dc_witness_fm"
unfolding is_dc_witness_fm_def apply (subst arity_transrec_fm)
apply (simp add:arity) defer 3
apply (simp add:arity) defer
apply (subst arity_is_nat_case_fm)
apply (simp add:arity del:arity_transrec_fm) prefer 5
by (simp add:arity del:arity_transrec_fm)+
definition dcwit_body :: "[i,i,i,i,i] ⇒ o" where
"dcwit_body(A,a,g,R) ≡ λp. snd(p) = dc_witness(fst(p), A, a, g, R)"
relativize functional "dcwit_body" "dcwit_body_rel"
relationalize "dcwit_body_rel" "is_dcwit_body"
synthesize "is_dcwit_body" from_definition assuming "nonempty"
arity_theorem for "is_dcwit_body_fm"
context M_replacement
begin
lemma dc_witness_closed[intro,simp]:
assumes "M(n)" "M(A)" "M(a)" "M(s)" "M(R)" "n∈nat"
shows "M(dc_witness(n,A,a,s,R))"
using ‹n∈nat›
proof(induct)
case 0
with ‹M(a)›
show ?case
unfolding dc_witness_def by simp
next
case (succ x)
with assms
have "M(dc_witness(x,A,a,s,R))" (is "M(?b)")
by simp
moreover from this assms
have "M(({?b}×A)∩R)" (is "M(?X)") by auto
moreover
have "{x∈A. ⟨?b,x⟩∈R} = {snd(y) . y∈?X}" (is "_ = ?Y")
by(intro equalityI subsetI,force,auto)
moreover from calculation
have "M(?Y)"
using lam_replacement_snd lam_replacement_imp_strong_replacement RepFun_closed
snd_closed[OF transM]
by auto
ultimately
show ?case
using ‹M(s)› apply_closed
unfolding dc_witness_def by simp
qed
lemma dc_witness_rel_char:
assumes "M(A)"
shows "dc_witness_rel(M,n,A,a,s,R) = dc_witness(n,A,a,s,R)"
proof -
from assms
have "{x ∈ A . ⟨rec, x⟩ ∈ R} = {x ∈ A . M(x) ∧ ⟨rec, x⟩ ∈ R}" for rec
by (auto dest:transM)
then
show ?thesis
unfolding dc_witness_def dc_witness_rel_def by simp
qed
lemma (in M_basic) first_section_closed:
assumes
"M(A)" "M(a)" "M(R)"
shows "M({x ∈ A . ⟨a, x⟩ ∈ R})"
proof -
have "{x ∈ A . ⟨a, x⟩ ∈ R} = range({a} × range(R) ∩ R) ∩ A"
by (intro equalityI) auto
with assms
show ?thesis
by simp
qed
lemma witness_into_A [TC]:
assumes "a∈A"
"∀X[M]. X≠0 ∧ X⊆A ⟶ s`X∈A"
"∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0" "n∈nat"
"M(A)" "M(a)" "M(s)" "M(R)"
shows "dc_witness(n, A, a, s, R)∈A"
using ‹n∈nat›
proof(induct n)
case 0
then show ?case using ‹a∈A› by simp
next
case (succ x)
with succ assms(1,3-)
show ?case
using nat_into_M first_section_closed
by (simp, rule_tac rev_subsetD, rule_tac assms(2)[rule_format])
auto
qed
end
locale M_DC = M_trancl + M_replacement + M_eclose +
assumes
separation_is_dcwit_body:
"M(A) ⟹ M(a) ⟹ M(g) ⟹ M(R) ⟹ separation(M,is_dcwit_body(M, A, a, g, R))"
and
dcwit_replacement:"Ord(na) ⟹
M(na) ⟹
M(A) ⟹
M(a) ⟹
M(s) ⟹
M(R) ⟹
transrec_replacement
(M, λn f ntc.
is_nat_case
(M, a,
λm bmfm.
∃fm[M]. ∃cp[M].
is_apply(M, f, m, fm) ∧
is_Collect(M, A, λx. ∃fmx[M]. (M(x) ∧ fmx ∈ R) ∧ pair(M, fm, x, fmx), cp) ∧
is_apply(M, s, cp, bmfm),
n, ntc),na)"
begin
lemma is_dc_witness_iff:
assumes "Ord(na)" "M(na)" "M(A)" "M(a)" "M(s)" "M(R)" "M(res)"
shows "is_dc_witness(M, na, A, a, s, R, res) ⟷ res = dc_witness_rel(M, na, A, a, s, R)"
proof -
note assms
moreover from this
have "{x ∈ A . M(x) ∧ ⟨f, x⟩ ∈ R} = {x ∈ A . ⟨f, x⟩ ∈ R}" for f
by (auto dest:transM)
moreover from calculation
have "M(fm) ⟹ M({x ∈ A . M(x) ∧ ⟨fm, x⟩ ∈ R})" for fm
using first_section_closed by (auto dest:transM)
moreover from calculation
have "M(x) ⟹ M(z) ⟹ M(mesa) ⟹
(∃ya[M]. pair(M, x, ya, z) ∧
is_wfrec(M, λn f. is_nat_case(M, a, λm bmfm. ∃fm[M]. is_apply(M, f, m, fm) ∧
is_apply(M, s, {x ∈ A . ⟨fm, x⟩ ∈ R}, bmfm), n), mesa, x, ya))
⟷
(∃y[M]. pair(M, x, y, z) ∧
is_wfrec(M, λn f. is_nat_case(M, a,
λm bmfm.
∃fm[M]. ∃cp[M]. is_apply(M, f, m, fm) ∧
is_Collect(M, A, λx. M(x) ∧ ⟨fm, x⟩ ∈ R, cp) ∧ is_apply(M, s, cp, bmfm),n),
mesa, x, y))" for x z mesa by simp
moreover from calculation
show ?thesis
using assms dcwit_replacement[of na A a s R]
unfolding is_dc_witness_def dc_witness_rel_def
by (rule_tac recursor_abs) (auto dest:transM)
qed
lemma dcwit_body_abs:
"fst(x) ∈ ω ⟹ M(A) ⟹ M(a) ⟹ M(g) ⟹ M(R) ⟹ M(x) ⟹
is_dcwit_body(M,A,a,g,R,x) ⟷ dcwit_body(A,a,g,R,x)"
using pair_in_M_iff apply_closed transM[of _ A]
is_dc_witness_iff[of "fst(x)" "A" "a" "g" "R" "snd(x)"]
fst_snd_closed dc_witness_closed
unfolding dcwit_body_def is_dcwit_body_def
by (auto dest:transM simp:absolut dc_witness_rel_char del:bexI intro!:bexI)
lemma Lambda_dc_witness_closed:
assumes "g ∈ Pow⇗M⇖(A)-{0} → A" "a∈A" "∀y∈A. {x ∈ A . ⟨y, x⟩ ∈ R} ≠ 0"
"M(g)" "M(A)" "M(a)" "M(R)"
shows "M(λn∈nat. dc_witness(n,A,a,g,R))"
proof -
from assms
have "(λn∈nat. dc_witness(n,A,a,g,R)) = {p ∈ ω × A . is_dcwit_body(M,A,a,g,R,p)}"
using witness_into_A[of a A g R]
Pow_rel_char apply_type[of g "{x ∈ Pow(A) . M(x)}-{0}" "λ_.A"]
unfolding lam_def split_def
apply (intro equalityI subsetI)
apply (auto)
by (subst dcwit_body_abs, simp_all add:transM[of _ ω] dcwit_body_def,
subst (asm) dcwit_body_abs, auto dest:transM simp:dcwit_body_def)
with assms
show ?thesis
using separation_is_dcwit_body dc_witness_rel_char unfolding split_def by simp
qed
lemma witness_related:
assumes "a∈A"
"∀X[M]. X≠0 ∧ X⊆A ⟶ s`X∈X"
"∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0" "n∈nat"
"M(a)" "M(A)" "M(s)" "M(R)" "M(n)"
shows "⟨dc_witness(n, A, a, s, R),dc_witness(succ(n), A, a, s, R)⟩∈R"
proof -
note assms
moreover from this
have "(∀X[M]. X≠0 ∧ X⊆A ⟶ s`X∈A)" by auto
moreover from calculation
have "dc_witness(n, A, a, s, R)∈A" (is "?x ∈ A")
using witness_into_A[of _ _ s R n] by simp
moreover from assms
have "M({x ∈ A . ⟨dc_witness(n, A, a, s, R), x⟩ ∈ R})"
using first_section_closed[of A "dc_witness(n, A, a, s, R)"]
by simp
ultimately
show ?thesis by auto
qed
lemma witness_funtype:
assumes "a∈A"
"∀X[M]. X≠0 ∧ X⊆A ⟶ s`X ∈ A"
"∀y∈A. {x∈A. ⟨y,x⟩∈R} ≠ 0"
"M(A)" "M(a)" "M(s)" "M(R)"
shows "(λn∈nat. dc_witness(n, A, a, s, R)) ∈ nat → A" (is "?f ∈ _ → _")
proof -
have "?f ∈ nat → {dc_witness(n, A, a, s, R). n∈nat}" (is "_ ∈ _ → ?B")
using lam_funtype assms by simp
then
have "?B ⊆ A"
using witness_into_A assms by auto
with ‹?f ∈ _›
show ?thesis
using fun_weaken_type
by simp
qed
lemma witness_to_fun:
assumes "a∈A"
"∀X[M]. X≠0 ∧ X⊆A ⟶ s`X∈A"
"∀y∈A. {x∈A. ⟨y,x⟩∈R } ≠ 0"
"M(A)" "M(a)" "M(s)" "M(R)"
shows "∃f ∈ nat→A. ∀n∈nat. f`n =dc_witness(n,A,a,s,R)"
using assms bexI[of _ "λn∈nat. dc_witness(n,A,a,s,R)"] witness_funtype
by simp
end
locale M_library_DC = M_library + M_DC
begin
lemma AC_M_func:
assumes "⋀x. x ∈ A ⟹ (∃y. y ∈ x)" "M(A)"
shows "∃f ∈ A →⇗M⇖ ⋃(A). ∀x ∈ A. f`x ∈ x"
proof -
from ‹M(A)›
interpret mpiA:M_Pi_assumption_repl _ A "λx . x"
by unfold_locales (simp_all add:lam_replacement_identity)
from ‹M(A)›
interpret mpi2:M_Pi_assumption_repl _ "⋃A" "λx . x"
by unfold_locales (simp_all add:lam_replacement_identity)
from ‹M(A)›
interpret mpic_A:M_Pi_assumptions_choice _ A "λx. x"
apply unfold_locales
using lam_replacement_constant lam_replacement_identity
lam_replacement_identity[THEN lam_replacement_imp_strong_replacement]
lam_replacement_minimum[THEN [5] lam_replacement_hcomp2]
unfolding lam_replacement_def[symmetric]
by auto
from assms
show ?thesis
using apply_type mpiA.mem_Pi_rel_abs mpi2.mem_Pi_rel_abs function_space_rel_char
by (rule_tac mpic_A.AC_Pi_rel[THEN rexE], simp,rename_tac f,rule_tac x=f in bexI)
(auto, rule_tac C="λx. x" in Pi_type,auto)
qed
lemma non_empty_family: "[| 0 ∉ A; x ∈ A |] ==> ∃y. y ∈ x"
by (subgoal_tac "x ≠ 0", blast+)
lemma AC_M_func0: "0 ∉ A ⟹ M(A) ⟹ ∃f ∈ A →⇗M⇖ ⋃(A). ∀x ∈ A. f`x ∈ x"
by (rule AC_M_func) (simp_all add: non_empty_family)
lemma AC_M_func_Pow_rel:
assumes "M(C)"
shows "∃f ∈ (Pow⇗M⇖(C)-{0}) →⇗M⇖ C. ∀x ∈ Pow⇗M⇖(C)-{0}. f`x ∈ x"
proof -
have "0∉Pow⇗M⇖(C)-{0}" by simp
with assms
obtain f where "f ∈ (Pow⇗M⇖(C)-{0}) →⇗M⇖ ⋃(Pow⇗M⇖(C)-{0})" "∀x ∈ Pow⇗M⇖(C)-{0}. f`x ∈ x"
using AC_M_func0[OF ‹0∉_›] by auto
moreover
have "x⊆C" if "x ∈ Pow⇗M⇖(C) - {0}" for x
using that Pow_rel_char assms
by auto
moreover
have "⋃(Pow⇗M⇖(C) - {0}) ⊆ C"
using assms Pow_rel_char by auto
ultimately
show ?thesis
using assms function_space_rel_char
by (rule_tac bexI,auto,rule_tac Pi_weaken_type,simp_all)
qed
theorem pointed_DC:
assumes "∀x∈A. ∃y∈A. ⟨x,y⟩∈ R" "M(A)" "M(R)"
shows "∀a∈A. ∃f ∈ nat→⇗M⇖ A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈R)"
proof -
have 0:"∀y∈A. {x ∈ A . ⟨y, x⟩ ∈ R} ≠ 0"
using assms by auto
from ‹M(A)›
obtain g where 1: "g ∈ Pow⇗M⇖(A)-{0} → A" "∀X[M]. X ≠ 0 ∧ X ⊆ A ⟶ g ` X ∈ X"
"M(g)"
using AC_M_func_Pow_rel[of A] mem_Pow_rel_abs
function_space_rel_char[of "Pow⇗M⇖(A)-{0}" A] by auto
then
have 2:"∀X[M]. X ≠ 0 ∧ X ⊆ A ⟶ g ` X ∈ A" by auto
{
fix a
assume "a∈A"
let ?f ="λn∈nat. dc_witness(n,A,a,g,R)"
note ‹a∈A›
moreover from this
have f0: "?f`0 = a" by simp
moreover
note ‹a∈A› ‹M(g)› ‹M(A)› ‹M(R)›
moreover from calculation
have "⟨?f ` n, ?f ` succ(n)⟩ ∈ R" if "n∈nat" for n
using witness_related[OF ‹a∈A› _ 0, of g n] 1 that
by (auto dest:transM)
ultimately
have "∃f[M]. f∈nat → A ∧ f ` 0 = a ∧ (∀n∈nat. ⟨f ` n, f ` succ(n)⟩ ∈ R)"
using 0 1 ‹a∈_›
by (rule_tac x="(λn∈ω. dc_witness(n, A, a, g, R))" in rexI)
(simp_all, rule_tac witness_funtype,
auto intro!: Lambda_dc_witness_closed dest:transM)
}
with ‹M(A)›
show ?thesis using function_space_rel_char by auto
qed
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))}"
by (rule ballI, erule_tac x="x" in ballE, simp_all)
lemma infer_snd : "c∈ A×B ⟹ snd(c) = k ⟹ c=⟨fst(c),k⟩"
by auto
corollary DC_on_A_x_nat :
assumes "(∀x∈A×nat. ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R)" "a∈A" "M(A)" "M(R)"
shows "∃f ∈ nat→⇗M⇖A. f`0 = a ∧ (∀n ∈ nat. ⟨⟨f`n,n⟩,⟨f`succ(n),succ(n)⟩⟩∈R)" (is "∃x∈_.?P(x)")
proof -
let ?R'="{⟨a,b⟩∈R. snd(b) = succ(snd(a))}"
from assms(1)
have "∀x∈A×nat. ∃y∈A×nat. ⟨x,y⟩ ∈ ?R'"
using aux_DC_on_AxNat2 by simp
moreover
note ‹a∈_› ‹M(A)›
moreover from this
have "M(A × ω)" by simp
have "lam_replacement(M, λx. succ(snd(fst(x))))"
using lam_replacement_fst lam_replacement_snd lam_replacement_hcomp
lam_replacement_hcomp[of _ "λx. succ(snd(x))"]
lam_replacement_succ by simp
with ‹M(R)›
have "M(?R')"
using separation_eq lam_replacement_fst lam_replacement_snd
lam_replacement_succ lam_replacement_hcomp lam_replacement_identity
unfolding split_def by simp
ultimately
obtain f where
F:"f∈nat→⇗M⇖ A×ω" "f ` 0 = ⟨a,0⟩" "∀n∈nat. ⟨f ` n, f ` succ(n)⟩ ∈ ?R'"
using pointed_DC[of "A×nat" ?R'] by blast
with ‹M(A)›
have "M(f)" using function_space_rel_char by simp
then
have "M(λx∈nat. fst(f`x))" (is "M(?f)")
using lam_replacement_fst lam_replacement_hcomp
lam_replacement_constant lam_replacement_identity
lam_replacement_apply
by (rule_tac lam_replacement_imp_lam_closed, auto)
with F ‹M(A)›
have "?f∈nat→⇗M⇖ A" "?f ` 0 = a" using function_space_rel_char by auto
have 1:"n∈ nat ⟹ f`n= ⟨?f`n, n⟩" for n
proof(induct n set:nat)
case 0
then show ?case using F by simp
next
case (succ x)
with ‹M(A)›
have "⟨f`x, f`succ(x)⟩ ∈ ?R'" "f`x ∈ A×nat" "f`succ(x)∈A×nat"
using F function_space_rel_char[of ω "A×ω"] by auto
then
have "snd(f`succ(x)) = succ(snd(f`x))" by simp
with succ ‹f`x∈_›
show ?case using infer_snd[OF ‹f`succ(_)∈_›] by auto
qed
have "⟨⟨?f`n,n⟩,⟨?f`succ(n),succ(n)⟩⟩ ∈ R" if "n∈nat" for n
using that 1[of "succ(n)"] 1[OF ‹n∈_›] F(3) by simp
with ‹f`0=⟨a,0⟩›
show ?thesis
using rev_bexI[OF ‹?f∈_›] by simp
qed
lemma aux_sequence_DC :
assumes "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n"
"R={⟨⟨x,n⟩,⟨y,m⟩⟩ ∈ (A×nat)×(A×nat). ⟨x,y⟩∈S`m }"
shows "∀ x∈A×nat . ∃y∈A. ⟨x,⟨y,succ(snd(x))⟩⟩ ∈ R"
using assms Pair_fst_snd_eq by auto
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:
assumes "∀x∈A. ∀n∈nat. ∃y∈A. ⟨x,y⟩ ∈ S`n" "M(A)" "M(S)"
shows "∀a∈A. (∃f ∈ nat→⇗M⇖ A. f`0 = a ∧ (∀n ∈ nat. ⟨f`n,f`succ(n)⟩∈S`succ(n)))"
proof -
from ‹M(S)›
have "lam_replacement(M, λx. S ` snd(snd(x)))"
using lam_replacement_snd lam_replacement_hcomp
lam_replacement_hcomp[of _ "λx. S`snd(x)"] lam_replacement_apply by simp
with assms
have "M({x ∈ (A × ω) × A × ω . (λ⟨⟨x,n⟩,y,m⟩. ⟨x, y⟩ ∈ S ` m)(x)})"
using lam_replacement_fst lam_replacement_snd lam_replacement_apply[of S]
lam_replacement_product[of "λx. fst(fst(x))" "λx. fst(snd(x))",
THEN [2] separation_in, of "λx. S ` snd(snd(x))"]
lam_replacement_hcomp unfolding split_def by simp
with assms
show ?thesis
by (rule_tac ballI) (drule aux_sequence_DC2, drule DC_on_A_x_nat, auto)
qed
end
end