# 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`{xA. dc_witness(n,A,a,s,R),xR}"

lemmas dc_witness_def = dc_witness_nat_def

relativize functional "dc_witness" "dc_witness_rel"
relationalize "dc_witness_rel" "is_dc_witness"
(* definition
is_dc_witness_fm where
"is_dc_witness_fm(na, A, a, s, R, e) ≡ is_transrec_fm
(is_nat_case_fm
(a +ω 8, (⋅∃⋅⋅4`2 is 0⋅ ∧ (⋅∃⋅⋅s +ω 12`0 is 2⋅ ∧ Collect_fm(A +ω 12, ⋅(⋅∃⋅0 = 0⋅⋅) ∧ (⋅∃⋅⋅0 ∈ R +ω 14⋅ ∧ pair_fm(3, 1, 0) ⋅⋅)⋅, 0) ⋅⋅)⋅⋅), 2,
0), na, e)"
*)
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 (subst arity_is_nat_case_fm)
apply (simp add:arity del:arity_transrec_fm) prefer 5

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)" "nnat"
shows "M(dc_witness(n,A,a,s,R))"
using nnat
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 "{xA. ?b,xR} = {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 "aA"
"X[M]. X0  XA  s`XA"
"yA. {xA. y,xR }  0" "nnat"
"M(A)" "M(a)" "M(s)" "M(R)"
shows "dc_witness(n, A, a, s, R)A"
using nnat
proof(induct n)
case 0
then show ?case using aA 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 ― ‹localeM_replacement

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" "aA" "yA. {x  A . y, x  R}  0"
"M(g)" "M(A)" "M(a)" "M(R)"
shows "M(λnnat. dc_witness(n,A,a,g,R))"
proof -
from assms
have "(λnnat. 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) (* slow *)
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)
(* by (intro equalityI subsetI, auto) (* Extremely slow *)
(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 "aA"
"X[M]. X0  XA  s`XX"
"yA. {xA. y,xR }  0" "nnat"
"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]. X0  XA  s`XA)" 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 "aA"
"X[M]. X0  XA  s`X  A"
"yA. {xA. y,xR}  0"
"M(A)" "M(a)" "M(s)" "M(R)"
shows "(λnnat. dc_witness(n, A, a, s, R))  nat  A" (is "?f  _  _")
proof -
have "?f  nat  {dc_witness(n, A, a, s, R). nnat}" (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 "aA"
"X[M]. X0  XA  s`XA"
"yA. {xA. y,xR }  0"
"M(A)" "M(a)" "M(s)" "M(R)"
shows "f  natA. nnat. f`n =dc_witness(n,A,a,s,R)"
using assms bexI[of _ "λnnat. dc_witness(n,A,a,s,R)"] witness_funtype
by simp

end ― ‹localeM_DC

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"
from M(A)
interpret mpi2:M_Pi_assumption_repl _ "A" "λx . x"
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}) →⇗MC. x  Pow⇗M⇖(C)-{0}. f`x  x"
proof -
have "0Pow⇗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 "xC" 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 "xA. yA. x,y R" "M(A)" "M(R)"
shows "aA. f  nat→⇗MA. f`0 = a  (n  nat. f`n,f`succ(n)R)"
proof -
have 0:"yA. {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 "aA"
let ?f ="λnnat. dc_witness(n,A,a,g,R)"
note aA
moreover from this
have f0: "?f`0 = a" by simp
moreover
note aA M(g) M(A) M(R)
moreover from calculation
have "?f ` n, ?f ` succ(n)  R" if "nnat" for n
using witness_related[OF aA _ 0, of g n] 1 that
by (auto dest:transM)
ultimately
have "f[M]. fnat  A  f ` 0 = a  (nnat. 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 : "xA×nat. yA. x,y,succ(snd(x))  R
xA×nat. yA×nat. x,y  {a,bR. 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 "(xA×nat. yA. x,y,succ(snd(x))  R)" "aA" "M(A)" "M(R)"
shows "f  nat→⇗MA. f`0 = a  (n  nat. f`n,n,f`succ(n),succ(n)R)" (is "x_.?P(x)")
proof -
let ?R'="{a,bR. snd(b) = succ(snd(a))}"
from assms(1)
have "xA×nat. yA×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:"fnat→⇗MA×ω" "f ` 0 = a,0"  "nnat. 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(λxnat. 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 "?fnat→⇗MA" "?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 "nnat" 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 "xA. nnat. yA. x,y  S`n"
"R={x,n,y,m  (A×nat)×(A×nat). x,yS`m }"
shows " xA×nat . yA. x,y,succ(snd(x))  R"
using assms Pair_fst_snd_eq by auto

lemma aux_sequence_DC2 : "xA. nnat. yA. x,y  S`n
xA×nat. yA. x,y,succ(snd(x))  {x,n,y,m(A×nat)×(A×nat). x,yS`m }"
by auto

lemma sequence_DC:
assumes "xA. nnat. yA. x,y  S`n" "M(A)" "M(S)"
shows "aA. (f  nat→⇗MA. 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 ― ‹localeM_library_DC

end