Theory Delta_System_Relative

section‹The Delta System Lemma, Relativized\label{sec:dsl-rel}›

theory Delta_System_Relative

relativize functional "delta_system" "delta_system_rel" external

locale M_delta = M_cardinal_library_extra +
    "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))"

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 (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
  from AF. Finite(A) M(F)
  have "M(λAF. |A|⇗M)"
    using cardinal_rel_separation Finite_cardinal_rel_in_nat[OF _ transM[of _ F]]
      separation_imp_lam_closed[of _ "cardinal_rel(M)" ω]
    by simp
  text‹Since 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
  note F ≈⇗M⇖ ℵ⇘1⇙⇗M⇖› M(F)
  moreover from calculation
  text‹there 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
  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
  text‹Therefore, 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ω
  text‹So 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›
    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
    case (succ n)
    have "aG. Finite(a)"
      fix a
      assume "a  G"
      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
      show "Finite(a)"
        using Finite_cardinal_rel_iff' nat_into_Finite[of "succ(n)"]
        by fastforce
    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›
      obtain p where "{AG . p  A} ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" "M(p)" by blast
      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
          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)
      text‹Now 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)
      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)
        show "Finite(A - {p})"
          using Finite_cardinal_rel_iff' by simp
      text‹we 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⇖›
      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
          Diff_closed[OF transM[OF _ 1(2)]] by auto
      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
      have "AD.BD. A{p}  B{p}(A  {p})  (B  {p}) = r{p}"
        by blast
      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
      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
          have "A -{p}  {p}  G"
            by auto
        with D  {A-{p} . A{XG. pX}}
        show ?thesis
          by blast
      note M(?D)
      show "D[M]. D  G  delta_system(D)  D ≈⇗M⇖ ℵ⇘1⇙⇗M⇖" by auto
      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
      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)
      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 G "λx y. xy"] mem_F_bound6[of _ G]
            lam_replacement_minimum separation_in lam_replacement_fst lam_replacement_snd
          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] lepoll_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)
      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
      text‹For 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)
        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
        note |X|⇗M< ℵ⇘1⇙⇗M⇖› M(X)
        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]
            [of "{A  G . (X)  A  0}" G]
            uncountable_rel_iff_nat_lt_cardinal_rel[of G]
          by force
        have "AG. SX. A  S = 0" by auto
        with XG
        show "AG. SX. <S,A>Disjoint" unfolding Disjoint_def
          using subsetD by simp
      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
      text‹Hence, 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)
      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)
      text‹and 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
        assume "w  ℵ⇘1⇙⇗M⇖" "x  ℵ⇘1⇙⇗M⇖" "S ` w = S ` x"
        show "w = x" by blast
      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)
      note M(G)
      moreover from calculation
      have "range(S)  G"
        using inj_rel_is_fun range_fun_subset_codomain
        by (fastforce dest: transM)
      note M(S)
      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)
      text‹This finishes the successor case and hence the proof.›
  with G  F
  show ?thesis by blast

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
  show ?thesis using delta_system_Aleph_rel1[of S]
    by (auto dest:transM)

end ― ‹localeM_delta