Theory Marriage.Marriage

(* Authors: Dongchen Jiang and Tobias Nipkow *)

theory Marriage
imports Main 
begin

theorem marriage_necessary:
  fixes A :: "'a  'b set" and I :: "'a set"
  assumes "finite I" and " iI. finite (A i)"
  and "R. (iI. R i  A i)  inj_on R I" (is "R. ?R R A & ?inj R A")
  shows "JI. card J  card ((A ` J))"
proof clarify
  fix J
  assume "J  I"
  show "card J  card ((A ` J))"
  proof-
    from assms(3) obtain R where "?R R A" and "?inj R A" by auto
    have "inj_on R J" by(rule subset_inj_on[OF ?inj R A JI])
    moreover have "(R ` J)  ((A ` J))" using JI ?R R A by auto
    moreover have "finite ((A ` J))" using JI assms
      by (metis finite_UN_I finite_subset subsetD)
    ultimately show ?thesis by (rule card_inj_on_le)
  qed
qed

text‹The proof by Halmos and Vaughan:›
theorem marriage_HV:
  fixes A :: "'a  'b set" and I :: "'a set"
  assumes "finite I" and " iI. finite (A i)"
  and "JI. card J  card ((A ` J))" (is "?M A I")
  shows "R. (iI. R i  A i)  inj_on R I"
       (is "?SDR A I" is "R. ?R R A I & ?inj R A I")
proof-
  { fix I
    have "finite I  iI. finite (A i)  ?M A I  ?SDR A I"
    proof(induct arbitrary: A rule: finite_psubset_induct)
      case (psubset I)
      show ?case
      proof (cases)
        assume "I={}" then show ?thesis by simp
      next 
        assume "I  {}"
        have "iI. A i  {}"
        proof (rule ccontr)
          assume  "¬ (iI. A i{})"
          then obtain i where "iI" "A i = {}" by blast
          hence "{i} I" by auto
          from mp[OF spec[OF psubset.prems(2)] this] A i={}
          show False by simp
        qed
        show ?thesis
        proof cases
          assume case1: "KI. K{}  card ((A ` K))  card K + 1"
          show ?thesis
          proof-
            from I{} obtain n where "nI" by auto
            with iI. A i  {} have "A n  {}" by auto
            then obtain x where "x  A n" by auto
            let ?A' = "λi. A i - {x}" let ?I' = "I - {n}"
            from nI have "?I'  I"
              by (metis DiffD2 Diff_subset insertI1 psubset_eq)
            have fin': "i?I'. finite (?A' i)" using psubset.prems(1) by auto
            have "?M ?A' ?I'"
            proof clarify
              fix J
              assume "J  ?I'"
              hence "J  I" by (metis I - {n}  I subset_psubset_trans)
              show "card J  card (iJ. A i - {x})"
              proof cases
                assume "J = {}" thus ?thesis by auto
              next
                assume "J  {}"
                hence "card J + 1  card((A ` J))" using case1 JI by blast
                moreover
                have "card((A ` J)) - 1  card (iJ. A i - {x})" (is "?l  ?r")
                proof-
                  have "finite J" using J  I psubset(1)
                    by (metis psubset_imp_subset finite_subset)
                  hence 1: "finite((A ` J))"
                    using iI. finite(A i) JI by force
                  have "?l = card((A ` J)) - card{x}" by simp
                  also have "  card((A ` J) - {x})" using 1
                    by (metis diff_card_le_card_Diff finite.intros)
                  also have "(A ` J) - {x} = (iJ. A i - {x})" by blast
                  finally show ?thesis .
                qed
                ultimately show ?thesis by arith
              qed
            qed
            from psubset(2)[OF ?I'I fin' ?M ?A' ?I']
            obtain R' where "?R R' ?A' ?I'" "?inj R' ?A' ?I'" by auto
            let ?Rx = "R'(n := x)"
            have "?R ?Rx A I" using xA n ?R R' ?A' ?I' by force
            have "i?I'. ?Rx i  x" using ?R R' ?A' ?I' by auto
            hence "?inj ?Rx A I" using ?inj R' ?A' ?I'
              by(auto simp: inj_on_def)
            with ?R ?Rx A I show ?thesis by auto
          qed
        next
          assume "¬ (KI. K{}  card ((A ` K))  card K + 1)"
          then obtain K where
            "KI" "K{}" and c1: "¬(card ((A ` K))  card K + 1)" by auto
          with psubset.prems(2) have "card ((A ` K))  card K" by auto
          with c1 have case2: "card ((A ` K))= card K" by auto
          from KI finite I have "finite K" by (auto intro:finite_subset)
          from psubset.prems KI
          have "iK. finite (A i)" "JK. card J  card((A ` J))" by auto
          from psubset(2)[OF KI this]
          obtain R1 where "?R R1 A K" "?inj R1 A K" by auto
          let ?AK = "λi. A i - (A ` K)" let ?IK = "I - K"
          from K{} KI have "?IKI" by auto
          have "i?IK. finite (?AK i)" using psubset.prems(1) by auto
          have "?M ?AK ?IK"
          proof clarify
            fix J assume "J  ?IK"
            with finite I have "finite J" by(auto intro: finite_subset)
            show "card J  card ( (?AK ` J))"
            proof-
              from J?IK have "J  K = {}" by auto
              have "card J = card(JK) - card K"
                using finite J finite K JK={}
                by (auto simp: card_Un_disjoint)
              also have "card(JK)  card((A ` (JK)))"
              proof -
                from J?IK KI have "J  K  I" by auto
                with psubset.prems(2) show ?thesis by blast
              qed
              also have " - card K = card( (?AK ` J)  (A ` K)) - card K"
              proof-
                have "(A ` (JK)) =  (?AK ` J)  (A ` K)"
                  using J?IK by auto
                thus ?thesis by simp
              qed
              also have " = card ( (?AK ` J)) + card((A ` K)) - card K"
              proof-
                have "finite ( (?AK ` J))" using finite J J?IK psubset(3)
                  by(blast intro: finite_UN_I finite_Diff)
                moreover have "finite ((A ` K))"
                  using finite K iK. finite (A i) by auto
                moreover have " (?AK ` J)  (A ` K) = {}" by auto
                ultimately show ?thesis
                  by (simp add: card_Un_disjoint del:Un_Diff_cancel2)
              qed
              also have " = card ( (?AK ` J))" using case2 by simp
              finally show ?thesis by simp
            qed
          qed
          from psubset(2)[OF ?IKI i?IK. finite (?AK i) J?IK. card J  card (iJ. A i -  (A ` K))]
          obtain R2 where "?R R2 ?AK ?IK" "?inj R2 ?AK ?IK" by auto
          let ?R12 = "λi. if iK then R1 i else R2 i"
          have "iI. ?R12 i  A i" using ?R R1 A K?R R2 ?AK ?IK by auto
          moreover have "iI. jI. ij?R12 i  ?R12 j"
          proof clarify
            fix i j assume "iI" "jI" "ij" "?R12 i = ?R12 j"
            show False
            proof-
              { assume "iK  jK  iKjK"
                with ?inj R1 A K ?inj R2 ?AK ?IK ?R12 i=?R12 j ij iI jI
                have ?thesis by (fastforce simp: inj_on_def)
              } moreover
              { assume "iK  jK  iK  jK"
                with ?R R1 A K ?R R2 ?AK ?IK ?R12 i=?R12 j jI iI
                have ?thesis by auto (metis Diff_iff)
              } ultimately show ?thesis by blast
            qed
          qed
          ultimately show ?thesis unfolding inj_on_def by fast
        qed
      qed
    qed
  }
  with assms ?M A I show ?thesis by auto
qed


text‹The proof by Rado:›
theorem marriage_Rado:
  fixes A :: "'a  'b set" and I :: "'a set"
  assumes "finite I" and " iI. finite (A i)"
  and "JI. card J  card ((A ` J))" (is "?M A")
  shows "R. (iI. R i  A i)  inj_on R I"
       (is "?SDR A" is "R. ?R R A & ?inj R A")
proof-
  { have "iI. finite (A i)  ?M A  ?SDR A"
    proof(induct n == "iI. card(A i) - 1" arbitrary: A)
      case 0
      have "iI.a. A(i) = {a}"
      proof (rule ccontr)
        assume  "¬ (iI.a. A i = {a})"
        then obtain i where i: "i:I" "a. A i  {a}" by blast
        hence "{i} I" by auto
        from "0"(1-2) mp[OF spec[OF "0.prems"(2)] {i}I] finite I i
        show False by (auto simp: card_le_Suc_iff)
      qed
      then obtain R where R: "iI. A i = {R i}" by metis
      then have "iI. R i  A i" by blast
      moreover have "inj_on R I"
      proof (auto simp: inj_on_def)
        fix x y assume "x  I" "y  I" "R x = R y"
        with R spec[OF "0.prems"(2), of "{x,y}"] show "x=y"
          by (simp add:le_Suc_eq card_insert_if split: if_splits)
      qed
      ultimately show ?case by blast
    next
      case (Suc n)
      from Suc.hyps(2)[symmetric, THEN sum_SucD]
      obtain i where i: "i:I" "2  card(A i)" by auto
      then obtain x1 x2 where "x1 : A i" "x2 : A i" "x1  x2"
        using Suc(3) by (fastforce simp: card_le_Suc_iff eval_nat_numeral)
      let "?Ai x" = "A i - {x}" let "?A x" = "A(i:=?Ai x)"
      let "?U J" = "(A ` J)" let "?Ui J x" = "?U J  ?Ai x"
      have n1: "n = (jI. card (?A x1 j) - 1)"
        using Suc.hyps(2) Suc.prems(1) i finite I x1:A i
        by (auto simp: sum.remove card_Diff_singleton)
      have n2: "n = (jI. card (?A x2 j) - 1)"
        using Suc.hyps(2) Suc.prems(1) i finite I x2:A i
        by (auto simp: sum.remove card_Diff_singleton)
      have finx1: "jI. finite (?A x1 j)" by (simp add: Suc(3))
      have finx2: "jI. finite (?A x2 j)" by (simp add: Suc(3))
      { fix x assume "¬ ?M (A(i:= ?Ai x))"
        with Suc.prems(2) obtain J
          where J: "J  I" "card J > card(((A(i:= ?Ai x) ` J)))"
          by (auto simp add:not_less_eq_eq Suc_le_eq)
        note fJi = finite_Diff[OF finite_subset[OF JI finite I], of "{i}"]
        have fU: "finite(?U (J-{i}))" using JI
          by (metis Diff_iff Suc(3) finite_UN[OF fJi] subsetD)
        have "i  J" using J Suc.prems(2)
          by (simp_all add: UNION_fun_upd not_le[symmetric] del: fun_upd_apply split: if_splits)
        hence "card(J-{i})  card(?Ui (J-{i}) x)"
          using fJi J by(simp add: UNION_fun_upd del: fun_upd_apply)
        hence "JI. i  J  card(J)  card(?Ui J x)  finite(?U J)"
          by (metis DiffD2 J(1) fU i  J insertI1 subset_insertI2 subset_insert_iff)
      } note lem = this
      have "?M (?A x1)  ?M (?A x2)" ― ‹Rado's Lemma›
      proof(rule ccontr)
        assume "¬ (?M (?A x1)  ?M (?A x2))"
        with lem obtain J1 J2 where
          J1: "J1I" "iJ1" "card J1  card(?Ui J1 x1)" "finite(?U J1)" and
          J2: "J2I" "iJ2" "card J2  card(?Ui J2 x2)" "finite(?U J2)"
          by metis
        note fin1 = finite_subset[OF J1I assms(1)]
        note fin2 = finite_subset[OF J2I assms(1)]
        have finUi1: "finite(?Ui J1 x1)" using Suc(3) by(blast intro: J1(4) i(1))
        have finUi2: "finite(?Ui J2 x2)" using Suc(3) by(blast intro: J2(4) i(1))
        have "card J1 + card J2 + 1 = card(J1  J2) + 1 + card(J1  J2)"
          by simp (metis card_Un_Int fin1 fin2)
        also have "card(J1  J2) + 1 = card(insert i (J1  J2))"
          using iJ1 iJ2 fin1 fin2 by simp
        also have "  card ( (A ` insert i (J1  J2)))" (is "_  card ?M")
          by (metis J1(1) J2(1) Suc(4) Un_least i(1) insert_subset)
        also have "?M = ?Ui J1 x1  ?Ui J2 x2" using x1x2 by auto
        also have "card(J1  J2)  card((A ` (J1  J2)))"
          by (metis J2(1) Suc(4) le_infI2)
        also have "  card(?U J1  ?U J2)" by(blast intro: card_mono J1(4))
        also have "  card(?Ui J1 x1  ?Ui J2 x2)"
          using Suc(3) iI by(blast intro: card_mono J1(4))
        finally show False using J1(3) J2(3)
          by(auto simp add: card_Un_Int[symmetric, OF finUi1 finUi2])
      qed
      thus ?case using Suc.hyps(1)[OF n1 finx1] Suc.hyps(1)[OF n2 finx2]
        by (metis DiffD1 fun_upd_def)
    qed
  } with assms ?M A show ?thesis by auto
qed

end