Quelle  Marriage.thy

(* 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 "∀ i∈I. finite (A i)"
  and "∃R. (∀i∈I. R i ∈ A i) ∧ inj_on R I" (is "∃R. ?R R A & ?inj R A")
  shows "∀J⊆I. 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 inj_on_subset[OF ‹?inj R A› ‹J⊆I›])
    moreover have "(R ` J) ⊆ (∪(A ` J))" using ‹J⊆I› ‹?R R A› by auto
    moreover have "finite (∪(A ` J))" using ‹J⊆I› 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 "∀ i∈I. finite (A i)"
  and "∀J⊆I. card J ≤ card (∪(A ` J))" (is "?M A I")
  shows "∃R. (∀i∈I. 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 ==> ∀i∈I. 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 "∀i∈I. A i ≠ {}"
        proof (rule ccontr)
          assume  "¬ (∀i∈I. A i≠{})"
          then obtain i where "i∈I" "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: "∀K⊂I. K≠{} ⟶ card (∪(A ` K)) ≥ card K + 1"
          show ?thesis
          proof-
            from ‹I≠{}› obtain n where "n∈I" by auto
            with ‹∀i∈I. 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 ‹n∈I› 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 (∪i∈J. A i - {x})"
              proof cases
                assume "J = {}" thus ?thesis by auto
              next
                assume "J ≠ {}"
                hence "card J + 1 ≤ card(∪(A ` J))" using case1 ‹J⊂I› by blast
                moreover
                have "card(∪(A ` J)) - 1 ≤ card (∪i∈J. 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 ‹∀i∈I. finite(A i)› ‹J⊂I› 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} = (∪i∈J. 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 ‹x∈A 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 "¬ (∀K⊂I. K≠{} ⟶ card (∪(A ` K)) ≥ card K + 1)"
          then obtain K where
            "K⊂I" "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 ‹K⊂I› ‹finite I› have "finite K" by (auto intro:finite_subset)
          from psubset.prems ‹K⊂I›
          have "∀i∈K. finite (A i)" "∀J⊆K. card J ≤ card(∪(A ` J))" by auto
          from psubset(2)[OF ‹K⊂I› 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≠{}› ‹K⊂I› have "?IK⊂I" 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(J∪K) - card K"
                using ‹finite J› ‹finite K› ‹J∩K={}›
                by (auto simp: card_Un_disjoint)
              also have "card(J∪K) ≤ card(∪(A ` (J∪K)))"
              proof -
                from ‹J⊆?IK› ‹K⊂I› 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 ` (J∪K)) = ∪ (?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› ‹∀i∈K. 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 ‹?IK⊂I› ‹∀i∈?IK. finite (?AK i)› ‹∀J⊆?IK. card J ≤ card (∪i∈J. A i - ∪ (A ` K))›]
          obtain R2 where "?R R2 ?AK ?IK" "?inj R2 ?AK ?IK" by auto
          let ?R12 = "λi. if i∈K then R1 i else R2 i"
          have "∀i∈I. ?R12 i ∈ A i" using ‹?R R1 A K›\<open>?R R2 ?AK ?IK› by auto
          moreover have "∀i∈I. ∀j∈I. i≠j⟶?R12 i ≠ ?R12 j"
          proof clarify
            fix i j assume "i∈I" "j∈I" "i≠j" "?R12 i = ?R12 j"
            show False
            proof-
              { assume "i∈K ∧ j∈K ∨ i∉K∧j∉K"
                with ‹?inj R1 A K› ‹?inj R2 ?AK ?IK› ‹?R12 i=?R12 j› ‹i≠j› ‹i∈I› ‹j∈I›
                have ?thesis by (fastforce simp: inj_on_def)
              } moreover
              { assume "i\<in>K \<and> j\<notin>K \<or> i\<notin>K \<and> j\<in>K"
                with \<open>?R R1 A K\<close> \<open>?R R2 ?AK ?IK\<close> \<open>?R12 i=?R12 j\<close> \<open>j\<in>I\<close> \<open>i\<in>I\<close>
                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 \<open>?M A I\<close> show ?thesis by auto
qed


text\<open>The proof by Rado:\<close>
theorem marriage_Rado:
  fixes A :: "'a \<Rightarrow> 'b set" and I :: "'a set"
  assumes "finite I" and "\<forall> i\<in>I. finite (A i)"
  and "\<forall>J\<subseteq>I. card J \<le> card (\<Union>(A ` J))" (is "?M A")
  shows "\<exists>R. (\<forall>i\<in>I. R i \<in> A i) \<and> inj_on R I"
       (is "?SDR A" is "\<exists>R. ?R R A & ?inj R A")
proof-
  { have "\<forall>i\<in>I. finite (A i) \<Longrightarrow> ?M A \<Longrightarrow> ?SDR A"
    proof(induct n == "\<Sum>i\<in>I. card(A i) - 1" arbitrary: A)
      case 0
      have "\<forall>i\<in>I.\<exists>a. A(i) = {a}"
      proof (rule ccontr)
        assume  "\<not> (\<forall>i\<in>I.\<exists>a. A i = {a})"
        then obtain i where i: "i:I" "\<forall>a. A i \<noteq> {a}" by blast
        hence "{i}\<subseteq> I" by auto
        from "0"(1-2) mp[OF spec[OF "0.prems"(2)] \<open>{i}\<subseteq>I\<close>] \<open>finite I\<close> i
        show False by (auto simp: card_le_Suc_iff)
      qed
      then obtain R where R: "\<forall>i\<in>I. A i = {R i}" by metis
      then have "\<forall>i\<in>I. R i \<in> A i" by blast
      moreover have "inj_on R I"
      proof (auto simp: inj_on_def)
        fix x y assume "x \<in> I" "y \<in> 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 \<le> card(A i)" by auto
      then obtain x1 x2 where "x1 : A i" "x2 : A i" "x1 \<noteq> 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" = "\<Union>(A ` J)" let "?Ui J x" = "?U J \<union> ?Ai x"
      have n1: "n = (\<Sum>j\<in>I. card (?A x1 j) - 1)"
        using Suc.hyps(2) Suc.prems(1) i \<open>finite I\<close> \<open>x1:A i\<close>
        by (auto simp: sum.remove card_Diff_singleton)
      have n2: "n = (\<Sum>j\<in>I. card (?A x2 j) - 1)"
        using Suc.hyps(2) Suc.prems(1) i \<open>finite I\<close> \<open>x2:A i\<close>
        by (auto simp: sum.remove card_Diff_singleton)
      have finx1: "\<forall>j\<in>I. finite (?A x1 j)" by (simp add: Suc(3))
      have finx2: "\<forall>j\<in>I. finite (?A x2 j)" by (simp add: Suc(3))
      { fix x assume "\<not> ?M (A(i:= ?Ai x))"
        with Suc.prems(2) obtain J
          where J: "J \<subseteq> I" "card J > card(\<Union>((A(i:= ?Ai x) ` J)))"
          by (auto simp add:not_less_eq_eq Suc_le_eq)
        note fJi = finite_Diff[OF finite_subset[OF \<open>J\<subseteq>I\<close> \<open>finite I\<close>], of "{i}"]
        have fU: "finite(?U (J-{i}))" using \<open>J\<subseteq>I\<close>
          by (metis Diff_iff Suc(3) finite_UN[OF fJi] subsetD)
        have "i \<in> 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}) \<ge> card(?Ui (J-{i}) x)"
          using fJi J by(simp add: UNION_fun_upd del: fun_upd_apply)
        hence "\<exists>J\<subseteq>I. i \<notin> J \<and> card(J) \<ge> card(?Ui J x) \<and> finite(?U J)"
          by (metis DiffD2 J(1) fU \<open>i \<in> J\<close> insertI1 subset_insertI2 subset_insert_iff)
      } note lem = this
      have "?M (?A x1) \<or> ?M (?A x2)" \<comment> \<open>Rado's Lemma\<close>
      proof(rule ccontr)
        assume "\<not> (?M (?A x1) \<or> ?M (?A x2))"
        with lem obtain J1 J2 where
          J1: "J1\<subseteq>I" "i\<notin>J1" "card J1 \<ge> card(?Ui J1 x1)" "finite(?U J1)" and
          J2: "J2\<subseteq>I" "i\<notin>J2" "card J2 \<ge> card(?Ui J2 x2)" "finite(?U J2)"
          by metis
        note fin1 = finite_subset[OF \<open>J1\<subseteq>I\<close> assms(1)]
        note fin2 = finite_subset[OF \<open>J2\<subseteq>I\<close> 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 \<union> J2) + 1 + card(J1 \<inter> J2)"
          by simp (metis card_Un_Int fin1 fin2)
        also have "card(J1 \<union> J2) + 1 = card(insert i (J1 \<union> J2))"
          using \<open>i\<notin>J1\<close> \<open>i\<notin>J2\<close> fin1 fin2 by simp
        also have "\<dots> \<le> card (\<Union> (A ` insert i (J1 \<union> J2)))" (is "_ \<le> card ?M")
          by (metis J1(1) J2(1) Suc(4) Un_least i(1) insert_subset)
        also have "?M = ?Ui J1 x1 \<union> ?Ui J2 x2" using \<open>x1\<noteq>x2\<close> by auto
        also have "card(J1 \<inter> J2) \<le> card(\<Union>(A ` (J1 \<inter> J2)))"
          by (metis J2(1) Suc(4) le_infI2)
        also have "\<dots> \<le> card(?U J1 \<inter> ?U J2)" by(blast intro: card_mono J1(4))
        also have "\<dots> \<le> card(?Ui J1 x1 \<inter> ?Ui J2 x2)"
          using Suc(3) \<open>i\<in>I\<close> 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 \<open>?M A\<close> show ?thesis by auto
qed

end