Theory Delta_System_Relative

sectionThe Delta System Lemma, Relativized\label{sec:dsl-rel}

theory Delta_System_Relative
  imports
    Cardinal_Library_Relative
begin

(* FIXME: The following code (definition and 3 lemmas) is extracted
   from Delta_System where it is unnecesarily under the context of AC *)
definition
  delta_system :: "i  o" where
  "delta_system(D)  r. AD. BD. A  B  A  B = r"

lemma delta_systemI[intro]:
  assumes "AD. BD. A  B  A  B = r"
  shows "delta_system(D)"
  using assms unfolding delta_system_def by simp

lemma delta_systemD[dest]:
  "delta_system(D)  r. AD. BD. A  B  A  B = r"
  unfolding delta_system_def by simp

lemma delta_system_root_eq_Inter:
  assumes "delta_system(D)"
  shows "AD. BD. A  B  A  B = D"
proof (clarify, intro equalityI, auto)
  fix A' B' x C
  assume hyp:"A'D" "B' D" "A'B'" "xA'" "xB'" "CD"
  with assms
  obtain r where delta:"AD. BD. A  B  A  B = r"
    by auto
  show "x  C"
  proof (cases "C=A'")
    case True
    with hyp and assms
    show ?thesis by simp
  next
    case False
    moreover
    note hyp
    moreover from calculation and delta
    have "r = C  A'" "A'  B' = r" "xr" by auto
    ultimately
    show ?thesis by simp
  qed
qed

relativize functional "delta_system" "delta_system_rel" external

locale M_delta = M_cardinal_library +
  assumes
    countable_lepoll_assms:
    "M(G)  M(A)  M(b)  M(f)  separation(M, λy. xA.
                          y = x, μ i. x  if_range_F_else_F(λx. {xa  G . x  xa}, b, f, i))"
begin

lemmas cardinal_replacement = lam_replacement_cardinal_rel[unfolded lam_replacement_def]

lemma disjoint_separation: "M(c)  separation(M, λ x. a. b. x=a,b  a  b = c)"
  using separation_pair separation_eq lam_replacement_constant lam_replacement_Int
  by simp

lemma insnd_ball: "M(G)  separation(M, λp. xG. x  snd(p)  fst(p)  x)"
  using separation_ball separation_iff' lam_replacement_fst lam_replacement_snd
  separation_in lam_replacement_hcomp
  by simp

lemma (in M_trans) mem_F_bound6:
  fixes F G
  defines "F  λ_ x. Collect(G, (∈)(x))"
  shows "xF(G,c)  c  (range(f)  G)"
  using apply_0 unfolding F_def
  by (cases "M(c)", auto simp:F_def)

lemma delta_system_Aleph_rel1:
  assumes "AF. Finite(A)" "F ≈⇗M⇖ ℵ⇘1⇙⇗M" "M(F)"
  shows "D[M]. D  F  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M"
proof -
  have "M(G)  M(p)  M({AG . p  A})" for G p
  proof -
    assume "M(G)" "M(p)"
    have "{AG . p  A} = G  (Memrel({p}  G) `` {p})"
      unfolding Memrel_def by auto
    with M(G) M(p)
    show ?thesis by simp
  qed
  from M(F)
  have "M(λAF. |A|⇗M)"
    using cardinal_replacement
    by (rule_tac lam_closed) (auto dest:transM)
  textSince all members are finite,
  with AF. Finite(A) M(F)
  have "(λAF. |A|⇗M) : F →⇗Mω" (is "?cards : _")
    by (simp add:mem_function_space_rel_abs, rule_tac lam_type)
      (force dest:transM)
  moreover from this
  have a:"?cards -`` {n} = { AF . |A|⇗M= n }" for n
    using vimage_lam by auto
  moreover
  note F ≈⇗M⇖ ℵ⇘1⇙⇗M M(F)
  moreover from calculation
  textthere are uncountably many have the same cardinal:
  obtain n where "nω" "|?cards -`` {n}|⇗M= ℵ⇘1⇙⇗M"
    using eqpoll_rel_Aleph_rel1_cardinal_rel_vimage[of F ?cards] by auto
  moreover
  define G where "G  ?cards -`` {n}"
  moreover from calculation and M(?cards)
  have "M(G)" by blast
  moreover from calculation
  have "G  F" by auto
  ultimately
  textTherefore, without loss of generality, we can assume that all
  elements of the family have cardinality termnω.
  have "AG  |A|⇗M= n" and "G ≈⇗M⇖ ℵ⇘1⇙⇗M" and "M(G)" for A
    using cardinal_rel_Card_rel_eqpoll_rel_iff by auto
  with nω
  textSo we prove the result by induction on this termn and
  generalizing termG, since the argument requires changing the
  family in order to apply the inductive hypothesis.
  have "D[M]. D  G  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M"
  proof (induct arbitrary:G)
    case 0 ― ‹This case is impossible
    then
    have "G  {0}"
      using cardinal_rel_0_iff_0 by (blast dest:transM)
    with G ≈⇗M⇖ ℵ⇘1⇙⇗M M(G)
    show ?case
      using nat_lt_Aleph_rel1 subset_imp_le_cardinal_rel[of G "{0}"]
        lt_trans2 cardinal_rel_Card_rel_eqpoll_rel_iff by auto
  next
    case (succ n)
    have "aG. Finite(a)"
    proof
      fix a
      assume "a  G"
      moreover
      note M(G) nω
      moreover from calculation
      have "M(a)" by (auto dest: transM)
      moreover from succ and aG
      have "|a|⇗M= succ(n)" by simp
      ultimately
      show "Finite(a)"
        using Finite_cardinal_rel_iff' nat_into_Finite[of "succ(n)"]
        by fastforce
    qed
    show "D[M]. D  G  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M"
    proof (cases "p[M]. {AG . p  A} ≈⇗M⇖ ℵ⇘1⇙⇗M")
      case True ― ‹the positive case, uncountably many sets with a
                    common element
      then
      obtain p where "{AG . p  A} ≈⇗M⇖ ℵ⇘1⇙⇗M" "M(p)" by blast
      moreover
      note 1=M(G) M(G)  M(p)  M({AG . p  A}) singleton_closed[OF M(p)]
      moreover from this
      have "M({x - {p} . x  {x  G . p  x}})"
        using RepFun_closed[OF lam_replacement_Diff'[THEN
              lam_replacement_imp_strong_replacement]]
          Diff_closed[OF transM[OF _ 1(2)]] by auto
      moreover from 1
      have "M(converse(λx{x  G . p  x}. x - {p}))" (is "M(converse(?h))")
        using converse_closed[of ?h] lam_closed[OF diff_Pair_replacement]
          Diff_closed[OF transM[OF _ 1(2)]]
        by auto
      moreover from calculation
      have "{A-{p} . A{XG. pX}} ≈⇗M⇖ ℵ⇘1⇙⇗M" (is "?F ≈⇗M_")
        using Diff_bij_rel[of "{AG . p  A}" "{p}", THEN
          comp_bij_rel[OF bij_rel_converse_bij_rel, where C="ℵ⇘1⇙⇗M",
            THEN bij_rel_imp_eqpoll_rel, of _ _ ?F]]
        unfolding eqpoll_rel_def
        by (auto simp del:mem_bij_abs)
      textNow using the hypothesis of the successor case,
      moreover from A. AG  |A|⇗M=succ(n) aG. Finite(a)
        and this M(G)
      have "pA  AG  |A - {p}|⇗M= n" for A
        using Finite_imp_succ_cardinal_rel_Diff[of _ p] by (force dest: transM)
      moreover
      have "a?F. Finite(a)"
      proof (clarsimp)
        fix A
        assume "pA" "AG"
        with A. p  A  A  G  |A - {p}|⇗M= n and nω M(G)
        have "Finite(|A - {p}|⇗M)"
          using nat_into_Finite by simp
        moreover from pA AG M(G)
        have "M(A - {p})" by (auto dest: transM)
        ultimately
        show "Finite(A - {p})"
          using Finite_cardinal_rel_iff' by simp
      qed
      moreover
      textwe may apply the inductive hypothesis to the new family term?F:
      note (A. A  ?F  |A|⇗M= n)  ?F ≈⇗M⇖ ℵ⇘1⇙⇗M M(?F) 
             D[M]. D  ?F  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M
      moreover
      note 1=M(G) M(G)  M(p)  M({AG . p  A}) singleton_closed[OF M(p)]
      moreover from this
      have "M({x - {p} . x  {x  G . p  x}})"
        using RepFun_closed[OF lam_replacement_Diff'[THEN
              lam_replacement_imp_strong_replacement]]
          Diff_closed[OF transM[OF _ 1(2)]] by auto
      ultimately
      obtain D where "D{A-{p} . A{XG. pX}}" "delta_system(D)" "D ≈⇗M⇖ ℵ⇘1⇙⇗M" "M(D)"
        by auto
      moreover from this
      obtain r where "AD. BD. A  B  A  B = r"
        by fastforce
      then
      have "AD.BD. A{p}  B{p}(A  {p})  (B  {p}) = r{p}"
        by blast
      ultimately
      have "delta_system({B  {p} . BD})" (is "delta_system(?D)")
        by fastforce
      moreover from M(D) M(p)
      have "M(?D)"
        using RepFun_closed un_Pair_replacement transM[of _ D] by auto
      moreover from D ≈⇗M⇖ ℵ⇘1⇙⇗M M(D)
      have "Infinite(D)" "|D|⇗M= ℵ⇘1⇙⇗M"
        using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1[THEN iffD2,
            THEN uncountable_rel_imp_Infinite, of D]
          cardinal_rel_eqpoll_rel_iff[of D "ℵ⇘1⇙⇗M"] M(D) D ≈⇗M⇖ ℵ⇘1⇙⇗M
        by auto
      moreover from this M(?D) M(D) M(p)
      have "?D ≈⇗M⇖ ℵ⇘1⇙⇗M"
        using cardinal_rel_map_Un[of D "{p}"] naturals_lt_nat
          cardinal_rel_eqpoll_rel_iff[THEN iffD1] by simp
      moreover
      note D  {A-{p} . A{XG. pX}}
      have "?D  G"
      proof -
        {
          fix A
          assume "AG" "pA"
          moreover from this
          have "A = A - {p}  {p}"
            by blast
          ultimately
          have "A -{p}  {p}  G"
            by auto
        }
        with D  {A-{p} . A{XG. pX}}
        show ?thesis
          by blast
      qed
      moreover
      note M(?D)
      ultimately
      show "D[M]. D  G  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M" by auto
    next
      case False
      note ¬ (p[M]. {A  G . p  A} ≈⇗M⇖ ℵ⇘1⇙⇗M) ― ‹the other case
        M(G) p. M(G)  M(p)  M({AG . p  A})
      moreover from G ≈⇗M⇖ ℵ⇘1⇙⇗M and this
      have "M(p)  {A  G . p  A} ≲⇗M⇖ ℵ⇘1⇙⇗M" (is "_  ?G(p) ≲⇗M_") for p
        by (auto intro!:lepoll_rel_eq_trans[OF subset_imp_lepoll_rel] dest:transM)
      moreover from calculation
      have "M(p)  ?G(p) ≺⇗M⇖ ℵ⇘1⇙⇗M" for p
        using M(G)  M(p)  M({AG . p  A})
        unfolding lesspoll_rel_def by simp
      moreover from calculation
      have "M(p)  ?G(p) ≲⇗Mω" for p
        using lesspoll_rel_Aleph_rel_succ[of 0] Aleph_rel_zero by auto
      moreover
      have "{A  G . S  A  0} = (pS. ?G(p))" for S
        by auto
      moreover from calculation
      have "M(S)  i  S  M({x  G . i  x})" for i S
        by (auto dest: transM)
      moreover
      have "M(S)  countable_rel(M,S)  countable_rel(M,{A  G . S  A  0})" for S
      proof -
        from M(G)
        interpret M_replacement_lepoll M "λ_ x. Collect(G, (∈)(x))"
          using countable_lepoll_assms lam_replacement_inj_rel separation_in_rev
            lam_replacement_Collect[OF _ _ insnd_ball] mem_F_bound6[of _ G]
          by unfold_locales
            (auto dest:transM intro:lam_Least_assumption_general[of _  _ _ _ Union])
        fix S
        assume "M(S)"
        with M(G) i. M(S)  i  S  M({x  G . i  x})
        interpret M_cardinal_UN_lepoll _ ?G S
          using lepoll_assumptions
          by unfold_locales (auto dest:transM)
        assume "countable_rel(M,S)"
        with M(S) calculation(6) calculation(7,8)[of S]
        show "countable_rel(M,{A  G . S  A  0})"
          using InfCard_rel_nat Card_rel_nat
            le_Card_rel_iff[THEN iffD2, THEN [3] leqpoll_rel_imp_cardinal_rel_UN_le,
              THEN [4] le_Card_rel_iff[THEN iffD1], of ω] j.UN_closed
          unfolding countable_rel_def by (auto dest: transM)
      qed
      define Disjoint where "Disjoint = {<A,B>  G×G . B  A = 0}"
      have "Disjoint = {x  G×G .  a b. x=<a,b>  ab=0}"
        unfolding Disjoint_def by force
      with M(G)
      have "M(Disjoint)"
        using disjoint_separation by simp
      textFor every countable\_rel subfamily of termG there is another some
      element disjoint from all of them:
      have "AG. SX. <S,A>Disjoint" if "|X|⇗M< ℵ⇘1⇙⇗M" "X  G" "M(X)" for X
      proof -
        note nω M(G)
        moreover from this and A. AG  |A|⇗M= succ(n)
        have "|A|⇗M= succ(n)" "M(A)" if "AG" for A
          using that Finite_cardinal_rel_eq_cardinal[of A] Finite_cardinal_rel_iff'[of A]
            nat_into_Finite transM[of A G] by (auto dest:transM)
        ultimately
        have "AG  Finite(A)" for A
          using cardinal_rel_Card_rel_eqpoll_rel_iff[of "succ(n)" A]
            Finite_cardinal_rel_eq_cardinal[of A] nat_into_Card_rel[of "succ(n)"]
            nat_into_M[of n] unfolding Finite_def eqpoll_rel_def by (auto)
        with XG M(X)
        have "AX  countable_rel(M,A)" for A
          using Finite_imp_countable_rel by (auto dest: transM)
        moreover from M(X)
        have "M(X)" by simp
        moreover
        note |X|⇗M< ℵ⇘1⇙⇗M M(X)
        ultimately
        have "countable_rel(M,X)"
          using Card_rel_nat[THEN cardinal_rel_lt_csucc_rel_iff, of X]
            countable_rel_union_countable_rel[of X]
            countable_rel_iff_cardinal_rel_le_nat[of X] Aleph_rel_succ
            Aleph_rel_zero by simp
        with M(X) M(_)  countable_rel(M,_)  countable_rel(M,{A  G . _   A  0})
        have "countable_rel(M,{A  G . (X)  A  0})" by simp
        with G ≈⇗M⇖ ℵ⇘1⇙⇗M M(G)
        obtain B where "BG" "B  {A  G . (X)  A  0}"
          using nat_lt_Aleph_rel1 cardinal_rel_Card_rel_eqpoll_rel_iff[of "ℵ⇘1⇙⇗M" G]
            uncountable_rel_not_subset_countable_rel
            [of "{A  G . (X)  A  0}" G]
            uncountable_rel_iff_nat_lt_cardinal_rel[of G]
          by force
        then
        have "AG. SX. A  S = 0" by auto
        with XG
        show "AG. SX. <S,A>Disjoint" unfolding Disjoint_def
          using subsetD by simp
        qed
      moreover from G ≈⇗M⇖ ℵ⇘1⇙⇗M M(G)
      obtain b where "bG"
        using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1
          uncountable_rel_not_empty by blast
      ultimately
      textHence, the hypotheses to perform a bounded-cardinal selection
      are satisfied,
      obtain S where "S:ℵ⇘1⇙⇗M⇖→⇗MG" "αℵ⇘1⇙⇗M βℵ⇘1⇙⇗M α<β  <S`α, S`β> Disjoint"
        for α β
        using bounded_cardinal_rel_selection[of "ℵ⇘1⇙⇗M" G Disjoint] M(Disjoint)
        by force
      moreover from this nω M(G)
      have inM:"M(S)" "M(n)" "x. x  ℵ⇘1⇙⇗M S ` x  G" "x. x  ℵ⇘1⇙⇗M M(x)"
        using function_space_rel_char by (auto dest: transM)
      ultimately
      have "α  ℵ⇘1⇙⇗M β  ℵ⇘1⇙⇗M αβ  S`α  S`β = 0" for α β
        unfolding Disjoint_def
        using lt_neq_symmetry[of "ℵ⇘1⇙⇗M" "λα β. S`α  S`β = 0"] Card_rel_is_Ord
        by auto (blast)
      textand a symmetry argument shows that obtained termS is
      an injective  term‹ℵ⇘1⇙⇗M⇖›-sequence of disjoint elements of termG.
      moreover from this and A. AG  |A|⇗M= succ(n) inM
        S : ℵ⇘1⇙⇗M⇖ →⇗MG M(G)
      have "S  inj_rel(M,ℵ⇘1⇙⇗M, G)"
        using def_inj_rel[OF Aleph_rel_closed M(G), of 1]
      proof (clarsimp)
        fix w x
        from inM
        have "a  ℵ⇘1⇙⇗M b  ℵ⇘1⇙⇗M a  b  S ` a  S ` b" for a b
          using A. AG  |A|⇗M= succ(n)[THEN [4] cardinal_rel_succ_not_0[THEN [4]
                Int_eq_zero_imp_not_eq[OF calculation, of "ℵ⇘1⇙⇗M" "λx. x"],
                of "λ_.n"], OF _ _ _ _ apply_closed] by auto
        moreover
        assume "w  ℵ⇘1⇙⇗M" "x  ℵ⇘1⇙⇗M" "S ` w = S ` x"
        ultimately
        show "w = x" by blast
      qed
      moreover from this M(G)
      have "range(S) ≈⇗M⇖ ℵ⇘1⇙⇗M"
        using inj_rel_bij_rel_range eqpoll_rel_sym unfolding eqpoll_rel_def
        by (blast dest: transM)
      moreover
      note M(G)
      moreover from calculation
      have "range(S)  G"
        using inj_rel_is_fun range_fun_subset_codomain
        by (fastforce dest: transM)
      moreover
      note M(S)
      ultimately
      show "D[M]. D  G  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M"
        using inj_rel_is_fun ZF_Library.range_eq_image[of S "ℵ⇘1⇙⇗M" G]
          image_function[OF fun_is_function, OF inj_rel_is_fun, of S "ℵ⇘1⇙⇗M" G]
          domain_of_fun[OF inj_rel_is_fun, of S "ℵ⇘1⇙⇗M" G] apply_replacement[of S]
        by (rule_tac x="S``ℵ⇘1⇙⇗M" in rexI) (auto dest:transM intro!:RepFun_closed)
      textThis finishes the successor case and hence the proof.
    qed
  qed
  with G  F
  show ?thesis by blast
qed

lemma delta_system_uncountable_rel:
  assumes "AF. Finite(A)" "uncountable_rel(M,F)" "M(F)"
  shows "D[M]. D  F  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M"
proof -
  from assms
  obtain S where "S  F" "S ≈⇗M⇖ ℵ⇘1⇙⇗M" "M(S)"
    using uncountable_rel_iff_subset_eqpoll_rel_Aleph_rel1[of F] by auto
  moreover from AF. Finite(A) and this
  have "AS. Finite(A)" by auto
  ultimately
  show ?thesis using delta_system_Aleph_rel1[of S]
    by (auto dest:transM)
qed

end ― ‹localeM_delta

end