Theory Pointed_DC_Relative

sectionRelative 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 (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)" "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 separation_eq_dc_witness:
"M(A) 
    M(a) 
    M(g) 
    M(R)   separation(M,λp. fst(p)ω  snd(p) = dc_witness(fst(p), A, a, g, R))"
  using separation_is_dcwit_body dcwit_body_abs unfolding is_dcwit_body_def
  oops

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

(* Should port the whole AC theory, including the absolute version
  of the following theorem *)
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_assumptions _ A "λx. x"
    using Pi_replacement Pi_separation lam_replacement_identity
      lam_replacement_Sigfun[THEN lam_replacement_imp_strong_replacement]
    by unfold_locales (simp_all add:transM[of _ A])
  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 M(A)
  interpret mpi2:M_Pi_assumptions2 _ A "λ_. A" "λx. x"
    using Pi_replacement Pi_separation lam_replacement_constant
      lam_replacement_Sigfun[THEN lam_replacement_imp_strong_replacement,
        of  "λ_. A"] Pi_replacement1[of _  "A"] transM[of _  "A"]
    by unfold_locales auto
  from assms
  show ?thesis
    using mpi2.Pi_rel_type 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, rule_tac x=x 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_iff_lam_closed[THEN iffD1, rule_format])
      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_Pair[THEN [5] lam_replacement_hcomp2,
        of "λx. fst(fst(x))" "λx. fst(snd(x))", THEN [2] separation_in,
        of "λx. S ` snd(snd(x))"] lam_replacement_apply[of S]
      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