Theory COP

(*<*)
theory COP
imports
  Contracts
begin

(*>*)
section‹ \<^citet>‹"HatfieldKojima:2010"›: Substitutes and stability for matching with contracts \label{sec:cop} ›

text‹

\<^citet>‹"HatfieldKojima:2010"› set about weakening @{const "substitutes"}
and therefore making the @{emph ‹cumulative offer processes›} (COPs,
\S\ref{sec:contracts-cop}) applicable to more matching problems. In
doing so they lose the lattice structure of the stable matches, which
necessitates redeveloping the results of \S\ref{sec:contracts}.

In contrast to the COP of \S\ref{sec:contracts-cop},
\<^citet>‹"HatfieldKojima:2010"› develop and analyze a @{emph
‹single-offer›} variant, where only one doctor (who has
no held contract) proposes per round. The order of doctors making
offers is not specified. We persist with the simultaneous-offer COP as
it is deterministic. See \<^citet>‹"HirataKasuya:2014"› for equivalence
arguments.

We begin with some observations due to
\citeauthor{AygunSonmez:2012-WP}. Firstly, as for the
matching-with-contracts setting of \S\ref{sec:contracts},
\<^citet>‹"AygunSonmez:2012-WP"› demonstrate that these results depend on
hospital preferences satisfying @{const "irc"}. We do not formalize
their examples. Secondly, an alternative to hospitals having choice
functions (as we have up to now) is for the hospitals to have
preference orders over sets, which is suggested by both
\<^citet>‹"HatfieldMilgrom:2005"› (weakly) and \<^citet>‹"HatfieldKojima:2010"›.
\<^citet>‹‹\S2› in "AygunSonmez:2012-WP"› argue that this approach is
under-specified and propose to define ‹Ch› as choosing
amongst maximal elements of some non-strict preference order (i.e.,
including indifference). They then claim that this is equivalent to
taking ‹Ch› as primitive, and so we continue down that
path.

›


subsection‹ Theorem~1: the COP yields a stable match under @{emph ‹bilateral substitutes›} ›

text‹

The weakest replacement condition suggested by
\<^citet>‹‹\S1› in "HatfieldKojima:2010"› for the @{const "substitutes"}
condition on hospital choice functions is termed @{emph ‹bilateral
substitutes›}:
\begin{quote}

Contracts are @{emph ‹bilateral substitutes›} for a hospital if there are
no two contracts ‹x› and ‹z› and a set of
contracts ‹Y› with other doctors than those associated
with ‹x› and ‹z› such that the hospital that
regards ‹Y› as available wants to sign ‹z›
if and only if ‹x› becomes available. In other words,
contracts are bilateral substitutes when any hospital, presented with
an offer from a doctor he does not currently employ, never wishes to
also hire another doctor he does not currently employ at a contract he
previously rejected.

\end{quote}

Note that this constraint is specific to this matching-with-contracts
setting, unlike those of \S\ref{sec:cf}.

›

context Contracts
begin

definition bilateral_substitutes_on :: "'x set ⇒ 'x cfun ⇒ bool" where
  "bilateral_substitutes_on A f
     ⟷ ¬(∃B⊆A. ∃a b. {a, b} ⊆ A ∧ Xd a ∉ Xd ` B ∧ Xd b ∉ Xd ` B
                     ∧ b ∉ f (B ∪ {b}) ∧ b ∈ f (B ∪ {a, b}))"

abbreviation bilateral_substitutes :: "'x cfun ⇒ bool" where
  "bilateral_substitutes ≡ bilateral_substitutes_on UNIV"

lemma bilateral_substitutes_on_def2:
  "bilateral_substitutes_on A f
     ⟷ (∀B⊆A. ∀a∈A. ∀b∈A. Xd a ∉ Xd ` B ∧ Xd b ∉ Xd ` B ∧ b ∉ f (B ∪ {b}) ⟶ b ∉ f (B ∪ {a, b}))"
(*<*)
(is "?lhs ⟷ ?rhs")
proof %invisible (rule iffI, clarsimp)
  fix B a b
  assume lhs: ?lhs and XXX: "B ⊆ A" "a ∈ A" "b ∈ A" "Xd a ∉ Xd ` B" "Xd b ∉ Xd ` B" "b ∉ f (insert b B)" "b ∈ f (insert a (insert b B))"
  show False
  proof(cases "a ∈ B")
    case True with XXX show ?thesis by (simp add: insert_absorb)
  next
    case False with lhs XXX show ?thesis
      unfolding bilateral_substitutes_on_def
      by (cases "b ∈ B") (auto simp: insert_commute insert_absorb)
  qed
qed (fastforce simp: bilateral_substitutes_on_def)

lemmas bilateral_substitutes_onI = iffD2[OF bilateral_substitutes_on_def2, rule_format]
lemmas bilateral_substitutes_onD = iffD1[OF bilateral_substitutes_on_def2, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

lemmas bilateral_substitutes_def = bilateral_substitutes_on_def2[where A=UNIV, simplified]
lemmas bilateral_substitutesI = iffD2[OF bilateral_substitutes_def, rule_format]
lemmas bilateral_substitutesD = iffD1[OF bilateral_substitutes_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

(*>*)
text‹›

lemma substitutes_on_bilateral_substitutes_on:
  assumes "substitutes_on A f"
  shows "bilateral_substitutes_on A f"
using %invisible assms by (auto intro!: bilateral_substitutes_onI dest: substitutes_onD[rotated -1])

text‹

\<^citet>‹‹\S4, Definition~5› in "AygunSonmez:2012-WP"› give the following
equivalent definition:

›

lemma bilateral_substitutes_on_def3:
  "bilateral_substitutes_on A f
     ⟷ (∀B⊆A. ∀a∈A. ∀b∈A. b ∉ f (B ∪ {b}) ∧ b ∈ f (B ∪ {a, b}) ⟶ Xd a ∈ Xd ` B ∨ Xd b ∈ Xd ` B)"
unfolding %invisible bilateral_substitutes_on_def2 by blast

end

text‹

As before, we define a series of locales that capture the relevant
hypotheses about hospital choice functions.

›

locale ContractsWithBilateralSubstitutes = Contracts +
  assumes Ch_bilateral_substitutes: "∀h. bilateral_substitutes (Ch h)"

sublocale ContractsWithSubstitutes < ContractsWithBilateralSubstitutes
using %invisible Ch_substitutes by unfold_locales (blast intro: substitutes_on_bilateral_substitutes_on)

locale ContractsWithBilateralSubstitutesAndIRC =
  ContractsWithBilateralSubstitutes + ContractsWithIRC

sublocale ContractsWithSubstitutesAndIRC < ContractsWithBilateralSubstitutesAndIRC
by %invisible unfold_locales

context ContractsWithBilateralSubstitutesAndIRC
begin

text‹

The key difficulty in showing the stability of the result of the COP
under this condition \<^citep>‹‹Theorem~1› in "HatfieldKojima:2010"› is in
proving that it ensures we get an @{const "allocation"}; the remainder
of the proof of \S\ref{sec:contracts-cop} (for a single hospital,
where this property is trivial) goes through unchanged. We avail
ourselves of \<^citet>‹‹Lemma› in "HirataKasuya:2014"›, which they say is a
restatement of the proof of
\<^citet>‹‹Theorem~1› in "HatfieldKojima:2010"›. See also
\<^citet>‹‹Appendix~A› in "AygunSonmez:2012-WP"›.

›

lemma bilateral_substitutes_lemma:
  assumes "Xd x ∉ Xd ` Ch h X"
  assumes "d ∉ Xd ` Ch h X"
  assumes "d ≠ Xd x"
  shows "d ∉ Xd ` Ch h (insert x X)"
proof(rule notI)
  assume "d ∈ Xd ` Ch h (insert x X)"
  then obtain x' where x': "x' ∈ Ch h (insert x X)" "Xd x' = d" by blast
  with Ch_irc ‹d ∉ Xd ` Ch h X›
  have "x ∈ Ch h (insert x X)" unfolding irc_def by blast
  let ?X' = "{y ∈ X. Xd y ∉ {Xd x, d}}"
  from Ch_range ‹Xd x ∉ Xd ` Ch h X› ‹d ∉ Xd ` Ch h X› ‹d ≠ Xd x› x'
  have "Ch h (insert x' ?X') = Ch h X"
    using consistencyD[OF Ch_consistency[where h=h], where B="X" and C="insert x' ?X'"]
    by (fastforce iff: image_iff) (* slow *)
  moreover from Ch_range Ch_singular ‹d ∉ Xd ` Ch h X› x' ‹x ∈ Ch h (insert x X)›
  have "Ch h (insert x (insert x' ?X')) = Ch h (insert x X)"
    using consistencyD[OF Ch_consistency[where h=h], where B="insert x X" and C="insert x (insert x' ?X')"]
    by (clarsimp simp: insert_commute) (blast dest: inj_onD)
  moreover note ‹d ∉ Xd ` Ch h X› x'
  ultimately show False
    using bilateral_substitutesD[OF spec[OF Ch_bilateral_substitutes, of h], where a=x and b=x' and B="?X'"] by fastforce
qed

text ‹

Our proof essentially adds the inductive details these earlier efforts
skipped over. It is somewhat complicated by our use of the
simultaneous-offer COP.

›

lemma bilateral_substitutes_lemma_union:
  assumes "Xd ` Ch h X ∩ Xd ` Y = {}"
  assumes "d ∉ Xd ` Ch h X"
  assumes "d ∉ Xd ` Y"
  assumes "allocation Y"
  shows "d ∉ Xd ` Ch h (X ∪ Y)"
using %invisible finite[of Y] assms by (induct arbitrary: d) (simp_all add: bilateral_substitutes_lemma)

lemma cop_F_CH_CD_on_disjoint:
  assumes "cop_F_closed_inv ds fp"
  assumes "cop_F_range_inv ds fp"
  shows "Xd ` CH fp ∩ Xd ` (CD_on ds (- RH fp) - fp) = {}"
using %invisible assms CH_range unfolding cop_F_range_inv_def cop_F_closed_inv_def above_def
by (fastforce simp: set_eq_iff mem_CD_on_Cd Cd_greatest greatest_def)

text‹

Our key lemma shows that we effectively have @{const "substitutes"}
for rejected contracts, provided the relevant doctor does not have a
contract held with the relevant hospital. Note the similarity to
Theorem~4 (\S\ref{sec:cop-theorem-4}).

›

lemma cop_F_RH_mono:
  assumes "cop_F_closed_inv ds fp"
  assumes "cop_F_range_inv ds fp"
  assumes "Xd x ∉ Xd ` Ch (Xh x) fp"
  assumes "x ∈ RH fp"
  shows "x ∈ RH (cop_F ds fp)"
proof(safe)
  from ‹x ∈ RH fp› show "x ∈ cop_F ds fp" using cop_F_increasing by blast
next
  assume "x ∈ CH (cop_F ds fp)"
  from Ch_singular ‹x ∈ CH (cop_F ds fp)› ‹x ∈ RH fp›
  have "Ch (Xh x) (cop_F ds fp) = Ch (Xh x) (fp ∪ (CD_on ds (-RH fp) - fp - {z. Xd z = Xd x}))"
    unfolding cop_F_def
    by - (rule consistencyD[OF Ch_consistency], auto simp: mem_CH_Ch dest: Ch_range' inj_onD)
  with cop_F_CH_CD_on_disjoint[OF ‹cop_F_closed_inv ds fp› ‹cop_F_range_inv ds fp›]
  have "Xd x ∉ Xd ` Ch (Xh x) (cop_F ds fp)"
    by simp (rule bilateral_substitutes_lemma_union[OF _ ‹Xd x ∉ Xd ` Ch (Xh x) fp›],
             auto simp: CH_def CD_on_inj_on_Xd inj_on_diff)
  with ‹x ∈ CH (cop_F ds fp)› show False by (simp add: mem_CH_Ch)
qed

lemma cop_F_allocation_inv:
  "valid ds (λds fp. cop_F_range_inv ds fp ∧ cop_F_closed_inv ds fp) (λds fp. allocation (CH fp))"
proof(induct rule: validI)
  case base show ?case by (simp add: CH_simps)
next
  case (step fp)
  then have "allocation (CH fp)"
        and "cop_F_closed_inv ds fp"
        and "cop_F_range_inv ds fp" by blast+
  note cop_F_CH_CD_on_disjoint = cop_F_CH_CD_on_disjoint[OF ‹cop_F_closed_inv ds fp› ‹cop_F_range_inv ds fp›]
  note cop_F_RH_mono = cop_F_RH_mono[OF ‹cop_F_closed_inv ds fp› ‹cop_F_range_inv ds fp›]
  show ?case
  proof(rule inj_onI)
    fix x y
    assume "x ∈ CH (cop_F ds fp)" and "y ∈ CH (cop_F ds fp)" and "Xd x = Xd y"
    show "x = y"
    proof(cases "Xh y = Xh x")
      case True with Ch_singular ‹x ∈ CH (cop_F ds fp)› ‹y ∈ CH (cop_F ds fp)› ‹Xd x = Xd y›
      show ?thesis by (fastforce simp: mem_CH_Ch dest: inj_onD)
    next
      case False note ‹Xh y ≠ Xh x›
      from ‹x ∈ CH (cop_F ds fp)› show ?thesis
      proof(cases x rule: CH_cop_F_cases)
        case CH note ‹x ∈ CH fp›
        from ‹y ∈ CH (cop_F ds fp)› show ?thesis
        proof(cases y rule: CH_cop_F_cases)
          case CH note ‹y ∈ CH fp›
          with ‹allocation (CH fp)› ‹Xd x = Xd y› ‹x ∈ CH fp›
          show ?thesis by (blast dest: inj_onD)
        next
          case RH_fp note ‹y ∈ RH fp›
          from ‹allocation (CH fp)› ‹Xd x = Xd y› ‹Xh y ≠ Xh x› ‹x ∈ CH fp› have "Xd y ∉ Xd ` Ch (Xh y) fp"
            by clarsimp (metis Ch_CH_irc_idem Ch_range' inj_on_contraD)
          with ‹y ∈ CH (cop_F ds fp)› ‹y ∈ RH fp› cop_F_RH_mono show ?thesis by blast
        next
          case CD_on note y' = ‹y ∈ CD_on ds (- RH fp) - fp›
          with cop_F_CH_CD_on_disjoint ‹Xd x = Xd y› ‹x ∈ CH fp› show ?thesis by blast
        qed
      next
        case RH_fp note ‹x ∈ RH fp›
        from ‹y ∈ CH (cop_F ds fp)› show ?thesis
        proof(cases y rule: CH_cop_F_cases)
          case CH note ‹y ∈ CH fp›
          from ‹allocation (CH fp)› ‹Xd x = Xd y› ‹Xh y ≠ Xh x› ‹y ∈ CH fp› have "Xd x ∉ Xd ` Ch (Xh x) fp"
            by clarsimp (metis Ch_CH_irc_idem Ch_range' inj_on_contraD)
          with ‹x ∈ CH (cop_F ds fp)› ‹x ∈ RH fp› cop_F_RH_mono show ?thesis by blast
        next
          case RH_fp note ‹y ∈ RH fp›
          show ?thesis
          proof(cases "Xd x ∈ Xd ` Ch (Xh x) fp")
            case True
            with ‹allocation (CH fp)› ‹Xd x = Xd y› ‹Xh y ≠ Xh x› have "Xd y ∉ Xd ` Ch (Xh y) fp"
              by clarsimp (metis Ch_range' inj_onD mem_CH_Ch)
            with ‹y ∈ CH (cop_F ds fp)› ‹y ∈ RH fp› cop_F_RH_mono show ?thesis by blast
          next
            case False note ‹Xd x ∉ Xd ` Ch (Xh x) fp›
            with ‹x ∈ CH (cop_F ds fp)› ‹x ∈ RH fp› cop_F_RH_mono show ?thesis by blast
          qed
        next
          case CD_on note ‹y ∈ CD_on ds (- RH fp) - fp›
          from cop_F_CH_CD_on_disjoint ‹Xd x = Xd y› ‹y ∈ CD_on ds (- RH fp) - fp›
          have "Xd x ∉ Xd ` Ch (Xh x) fp" by (auto simp: CH_def dest: Ch_range')
          with ‹x ∈ CH (cop_F ds fp)› ‹x ∈ RH fp› cop_F_RH_mono show ?thesis by blast
        qed
      next
        case CD_on note ‹x ∈ CD_on ds (- RH fp) - fp›
        from ‹y ∈ CH (cop_F ds fp)› show ?thesis
        proof(cases y rule: CH_cop_F_cases)
          case CH note ‹y ∈ CH fp›
          with cop_F_CH_CD_on_disjoint ‹Xd x = Xd y› ‹x ∈ CD_on ds (- RH fp) - fp› show ?thesis by blast
        next
          case RH_fp note ‹y ∈ RH fp›
          from cop_F_CH_CD_on_disjoint ‹Xd x = Xd y› ‹x ∈ CD_on ds (- RH fp) - fp›
          have "Xd y ∉ Xd ` Ch (Xh y) fp" unfolding CH_def by clarsimp (blast dest: Ch_range')
          with ‹y ∈ CH (cop_F ds fp)› ‹y ∈ RH fp› cop_F_RH_mono show ?thesis by blast
        next
          case CD_on note ‹y ∈ CD_on ds (- RH fp) - fp›
          with ‹Xd x = Xd y› ‹x ∈ CD_on ds (- RH fp) - fp› show ?thesis
            by (meson CD_on_inj_on_Xd DiffD1 inj_on_eq_iff)
        qed
      qed
    qed
  qed
qed

lemma fp_cop_F_allocation:
  shows "allocation (cop ds)"
proof %invisible -
  have "invariant ds (λds fp. cop_F_range_inv ds fp ∧ cop_F_closed_inv ds fp ∧ allocation (CH fp))"
    using cop_F_range_inv cop_F_closed_inv cop_F_allocation_inv
    by - (rule valid_conj | blast | rule valid_pre)+
  then show ?thesis by (blast dest: invariantD)
qed

theorem Theorem_1:
  shows "stable_on ds (cop ds)"
proof %invisible (rule stable_onI)
  show "individually_rational_on ds (cop ds)"
  proof(rule individually_rational_onI)
    from fp_cop_F_allocation show "CD_on ds (cop ds) = cop ds"
      by (rule CD_on_closed) (blast dest: fp_cop_F_range_inv' CH_range')
    show "CH (cop ds) = cop ds" by (simp add: CH_irc_idem)
  qed
  show "stable_no_blocking_on ds (cop ds)" by (rule cop_stable_no_blocking_on)
qed

end

text (in ContractsWithBilateralSubstitutesAndIRC) ‹

\<^citet>‹‹\S3.1› in "HatfieldKojima:2010"› provide an example that shows that
the traditional optimality and strategic results do not hold under
@{const "bilateral_substitutes"}, which motivates looking for a
stronger condition that remains weaker than @{const "substitutes"}.

Their example involves two doctors, two hospitals, and five contracts.

›

datatype X5 = Xd1 | Xd1' | Xd2 | Xd2' | Xd2''

primrec X5d :: "X5 ⇒ D2" where
  "X5d Xd1 = D1"
| "X5d Xd1' = D1"
| "X5d Xd2 = D2"
| "X5d Xd2' = D2"
| "X5d Xd2'' = D2"

primrec X5h :: "X5 ⇒ H2" where
  "X5h Xd1 = H1"
| "X5h Xd1' = H1"
| "X5h Xd2 = H1"
| "X5h Xd2' = H2"
| "X5h Xd2'' = H1"

primrec PX5d :: "D2 ⇒ X5 rel" where
  "PX5d D1 = linord_of_list [Xd1, Xd1']"
| "PX5d D2 = linord_of_list [Xd2, Xd2', Xd2'']"

primrec CX5h :: "H2 ⇒ X5 cfun" where
  "CX5h H1 A =
     (if {Xd1', Xd2} ⊆ A then {Xd1', Xd2} else
      if {Xd2''} ⊆ A then {Xd2''} else
      if {Xd1} ⊆ A then {Xd1} else
      if {Xd1'} ⊆ A then {Xd1'} else
      if {Xd2} ⊆ A then {Xd2} else {})"
| "CX5h H2 A = { x . x ∈ A ∧ x = Xd2' }"

(*<*)

lemma X5_UNIV:
  shows "UNIV = set [Xd1, Xd1', Xd2, Xd2', Xd2'']"
using X5.exhaust by auto

lemmas X5_pow = subset_subseqs[OF subset_trans[OF subset_UNIV Set.equalityD1[OF X5_UNIV]]]

instance X5 :: finite
by standard (simp add: X5_UNIV)

lemma X5_ALL:
  shows "(∀X''. P X'') ⟷ (∀X''∈set ` set (subseqs [Xd1, Xd1', Xd2, Xd2', Xd2'']). P X'')"
using X5_pow by blast

lemma PX5d_linear:
  shows "Linear_order (PX5d d)"
by (cases d) (simp_all add: linord_of_list_Linear_order)

lemma PX5d_range:
  shows "Field (PX5d d) ⊆ {x. X5d x = d}"
by (cases d) simp_all

lemma CX5h_range:
  shows "CX5h h X ⊆ {x ∈ X. X5h x = h}"
by (cases h) auto

lemma CX5h_singular:
  shows "inj_on X5d (CX5h h X)"
by (cases h) (auto intro: inj_onI)

(*>*)
text‹›

interpretation BSI: Contracts X5d X5h PX5d CX5h
using %invisible PX5d_linear PX5d_range CX5h_range CX5h_singular by unfold_locales blast+

lemma CX5h_bilateral_substitutes:
  shows "BSI.bilateral_substitutes (CX5h h)"
unfolding BSI.bilateral_substitutes_def by (cases h) (auto simp: X5_ALL)

lemma CX5h_irc:
  shows "irc (CX5h h)"
unfolding irc_def by (cases h) (auto simp: X5_ALL)

interpretation BSI: ContractsWithBilateralSubstitutesAndIRC X5d X5h PX5d CX5h
using %invisible CX5h_bilateral_substitutes CX5h_irc by unfold_locales blast+

text‹

There are two stable matches in this model.

›
(*<*)

lemma Xd1_Xd2'_stable:
  shows "BSI.stable {Xd1, Xd2'}"
proof(rule BSI.stable_onI)
  note image_cong_simp [cong del] note INF_cong_simp [cong] note SUP_cong_simp [cong]
  show "BSI.individually_rational {Xd1, Xd2'}"
    unfolding BSI.individually_rational_on_def BSI.CD_on_def BSI.CH_def
    by (auto simp: insert_commute D2_UNION H2_UNION)
  show "BSI.stable_no_blocking {Xd1, Xd2'}"
    unfolding BSI.stable_no_blocking_on_def
    by (auto simp: X5_ALL BSI.blocking_on_def BSI.mem_CD_on_Cd BSI.maxR_def linord_of_list_linord_of_listP)
qed

lemma Xd1'_Xd2_stable:
  shows "BSI.stable {Xd1', Xd2}"
proof(rule BSI.stable_onI)
  note image_cong_simp [cong del] note INF_cong_simp [cong] note SUP_cong_simp [cong]
  show "BSI.individually_rational {Xd1', Xd2}"
    unfolding BSI.individually_rational_on_def BSI.CD_on_def BSI.CH_def
    by (auto simp: insert_commute D2_UNION H2_UNION)
  show "BSI.stable_no_blocking {Xd1', Xd2}"
    unfolding BSI.stable_no_blocking_on_def
    by (auto simp: X5_ALL BSI.blocking_on_def BSI.mem_CD_on_Cd BSI.maxR_def linord_of_list_linord_of_listP)
qed

(*>*)
text‹›

lemma BSI_stable:
  shows "BSI.stable X ⟷ X = {Xd1, Xd2'} ∨ X = {Xd1', Xd2}"
(*<*)
(is "?lhs = ?rhs")
proof(rule iffI)
  assume ?lhs then show ?rhs
    using X5_pow[where X=X] BSI.stable_on_allocation[OF ‹?lhs›]
    apply clarsimp
    apply (elim disjE; simp add: insert_eq_iff)
    apply (simp_all only: BSI.stable_on_def BSI.individually_rational_on_def BSI.stable_no_blocking_on_def BSI.blocking_on_def BSI.CH_def)
    apply (auto 0 1 simp: D2_UNION H2_UNION X5_ALL BSI.mem_CD_on_Cd BSI.maxR_def linord_of_list_linord_of_listP)
    done
next
  assume ?rhs then show ?lhs
    using Xd1'_Xd2_stable Xd1_Xd2'_stable by blast
qed

(*>*)
text (in Contracts) ‹

Therefore there is no doctor-optimal match under these preferences:

›

lemma
  "¬(∃ (Y::X5 set). BSI.doctor_optimal_match UNIV Y)"
unfolding BSI.doctor_optimal_match_def BSI_stable
apply clarsimp
apply (cut_tac X=Y in X5_pow)
apply clarsimp
apply (elim disjE; simp add: insert_eq_iff; simp add: X5_ALL linord_of_list_linord_of_listP)
done


subsection‹ Theorem~3: @{emph ‹pareto separability›} relates @{emph ‹unilateral substitutes›} and @{emph ‹substitutes›} ›

text‹

\<^citet>‹‹\S4› in "HatfieldKojima:2010"› proceed to define @{emph ‹unilateral
substitutes›}:
\begin{quote}

[P]references satisfy @{emph ‹unilateral substitutes›} if whenever a
hospital rejects the contract @{term "z"} when that is the only
contract with @{term "Xd z"} available, it still rejects the contract
@{term "z"} when the choice set expands.

\end{quote}

›

context Contracts
begin

definition unilateral_substitutes_on :: "'x set ⇒ 'x cfun ⇒ bool" where
  "unilateral_substitutes_on A f
     ⟷ ¬(∃B⊆A. ∃a b. {a, b} ⊆ A ∧ Xd b ∉ Xd ` B ∧ b ∉ f (B ∪ {b}) ∧ b ∈ f (B ∪ {a, b}))"

abbreviation unilateral_substitutes :: "'x cfun ⇒ bool" where
  "unilateral_substitutes ≡ unilateral_substitutes_on UNIV"

lemma unilateral_substitutes_on_def2:
  "unilateral_substitutes_on A f
     ⟷ (∀B⊆A. ∀a∈A. ∀b∈A. Xd b ∉ Xd ` B ∧ b ∉ f (B ∪ {b}) ⟶ b ∉ f (B ∪ {a, b}))"
(*<*)
(is "?lhs ⟷ ?rhs")
proof %invisible (rule iffI, clarsimp)
  fix B a b
  assume lhs: ?lhs and XXX: "B ⊆ A" "a ∈ A" "b ∈ A" "Xd b ∉ Xd ` B" "b ∉ f (insert b B)" "b ∈ f (insert a (insert b B))"
  show False
  proof(cases "a ∈ B")
    case True with XXX show ?thesis by (simp add: insert_absorb)
  next
    case False with lhs XXX show ?thesis
      unfolding unilateral_substitutes_on_def
      by (cases "b ∈ B") (auto simp: insert_commute insert_absorb)
  qed
qed (fastforce simp: unilateral_substitutes_on_def)

lemmas %invisible unilateral_substitutes_onI = iffD2[OF unilateral_substitutes_on_def2, rule_format, simplified, unfolded conj_imp_eq_imp_imp]
lemmas %invisible unilateral_substitutes_onD = iffD1[OF unilateral_substitutes_on_def2, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

lemmas %invisible unilateral_substitutes_def = unilateral_substitutes_on_def2[where A=UNIV, simplified]
lemmas %invisible unilateral_substitutesI = iffD2[OF unilateral_substitutes_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]
lemmas %invisible unilateral_substitutesD = iffD1[OF unilateral_substitutes_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

(*>*)
text‹

\<^citet>‹‹\S4, Definition~6› in "AygunSonmez:2012-WP"› give the following equivalent definition:

›

lemma unilateral_substitutes_on_def3:
  "unilateral_substitutes_on A f
     ⟷ (∀B⊆A. ∀a∈A. ∀b∈A. b ∉ f (B ∪ {b}) ∧ b ∈ f (B ∪ {a, b}) ⟶ Xd b ∈ Xd ` B)"
(*<*)
unfolding %invisible unilateral_substitutes_on_def2 by blast

lemmas %invisible unilateral_substitutes_def3 = unilateral_substitutes_on_def3[where A=UNIV, simplified]
lemmas %invisible unilateral_substitutesD3 = iffD1[OF unilateral_substitutes_def3, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

(*>*)
text‹›

lemma substitutes_on_unilateral_substitutes_on:
  assumes "substitutes_on A f"
  shows "unilateral_substitutes_on A f"
using %invisible assms by (auto intro!: unilateral_substitutes_onI dest: substitutes_onD)

lemma unilateral_substitutes_on_bilateral_substitutes_on:
  assumes "unilateral_substitutes_on A f"
  shows "bilateral_substitutes_on A f"
using %invisible assms by (auto intro!: bilateral_substitutes_onI dest: unilateral_substitutes_onD[rotated -1])

text‹

The following defines locales for the @{const
"unilateral_substitutes"} hypothesis, and inserts these between those
for @{const "substitutes"} and @{const "bilateral_substitutes"}.

›

end

locale ContractsWithUnilateralSubstitutes = Contracts +
  assumes Ch_unilateral_substitutes: "∀h. unilateral_substitutes (Ch h)"

sublocale ContractsWithUnilateralSubstitutes < ContractsWithBilateralSubstitutes
using %invisible Ch_unilateral_substitutes by unfold_locales (blast intro: unilateral_substitutes_on_bilateral_substitutes_on)

sublocale ContractsWithSubstitutes < ContractsWithUnilateralSubstitutes
using %invisible Ch_substitutes by unfold_locales (blast intro: substitutes_on_unilateral_substitutes_on)

locale ContractsWithUnilateralSubstitutesAndIRC =
  ContractsWithUnilateralSubstitutes + ContractsWithIRC

sublocale ContractsWithUnilateralSubstitutesAndIRC < ContractsWithBilateralSubstitutesAndIRC
by %invisible unfold_locales

sublocale ContractsWithSubstitutesAndIRC < ContractsWithUnilateralSubstitutesAndIRC
by %invisible unfold_locales

text (in Contracts) ‹

\<^citet>‹‹Theorem~3› in "HatfieldKojima:2010"› relate @{const
"unilateral_substitutes"} to @{const "substitutes"} using @{emph
‹Pareto separability›}:
\begin{quote}

Preferences are @{emph ‹Pareto separable›} for a hospital if the
hospital's choice between ‹x› and ‹x'›, two
[distinct] contracts with the same doctor, does not depend on what
other contracts the hospital has access to.

\end{quote}
This result also depends on @{const "irc"}.

›

context Contracts
begin

definition pareto_separable_on :: "'x set ⇒ bool" where
  "pareto_separable_on A
     ⟷ (∀B⊆A. ∀C⊆A. ∀a b. {a, b} ⊆ A ∧ a ≠ b ∧ Xd a = Xd b ∧ Xh a = Xh b
                     ∧ a ∈ Ch (Xh b) (B ∪ {a, b}) ⟶ b ∉ Ch (Xh b) (C ∪ {a, b}))"

abbreviation pareto_separable :: "bool" where
  "pareto_separable ≡ pareto_separable_on UNIV"

lemmas %invisible pareto_separable_def = pareto_separable_on_def[where A=UNIV, simplified]

lemmas %invisible pareto_separable_onI = iffD2[OF pareto_separable_on_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]
lemmas %invisible pareto_separable_onD = iffD1[OF pareto_separable_on_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

lemma substitutes_on_pareto_separable_on:
  assumes "∀h. substitutes_on A (Ch h)"
  shows "pareto_separable_on A"
proof(rule pareto_separable_onI)
  fix B C a b
  assume XXX: "B ⊆ A" "C ⊆ A" "a ∈ A" "b ∈ A" "a ≠ b" "Xd a = Xd b" "Xh a = Xh b" "a ∈ Ch (Xh b) (insert a (insert b B))"
  note Ch_iiaD = iia_onD[OF iffD1[OF substitutes_iia spec[OF ‹∀h. substitutes_on A (Ch h)›]], rotated -1, simplified]
  from XXX have "a ∈ Ch (Xh b) {a, b}" by (fast elim: Ch_iiaD)
  with XXX have "b ∉ Ch (Xh b) {a, b}" by (meson Ch_singular inj_on_eq_iff)
  with XXX have "b ∉ Ch (Xh b) (C ∪ {a, b})" by (blast dest: Ch_iiaD)
  with XXX show "b ∉ Ch (Xh b) (insert a (insert b C))" by simp
qed

lemma unilateral_substitutes_on_pareto_separable_on_substitutes_on:
  assumes "∀h. unilateral_substitutes_on A (Ch h)"
  assumes "∀h. irc_on A (Ch h)"
  assumes "pareto_separable_on A"
  shows "substitutes_on A (Ch h)"
proof(rule substitutes_onI)
  fix B a b
  assume XXX: "B ⊆ A" "a ∈ A" "b ∈ A" "b ∉ Ch h (insert b B)"
  show "b ∉ Ch h (insert a (insert b B))"
  proof(cases "Xd b ∈ Xd ` B")
    case True show ?thesis
    proof(cases "Xd b ∈ Xd ` Ch h (insert b B)")
      case True
      then obtain x where "x ∈ Ch h (insert b B)" "Xd x = Xd b" by force
      moreover with XXX have "x ∈ B" "x ≠ b" using Ch_range by blast+
      moreover note ‹pareto_separable_on A› XXX
      ultimately show ?thesis
        using pareto_separable_onD[where A=A and B="B - {x}" and a=x and b=b and C="insert a (B - {x})"] Ch_range
        by (cases "Xh b = h") (auto simp: insert_commute insert_absorb)
    next
      case False
      let ?B' = "{x ∈ B . Xd x ≠ Xd b}"
      from False have "b ∉ Ch h (insert b B)" by blast
      with ‹∀h. irc_on A (Ch h)› XXX False have "b ∉ Ch h (insert b ?B')"
        using consistency_onD[OF irc_on_consistency_on[where f="Ch h"], where B="insert b B" and C="insert b ?B'"] Ch_range
        by (fastforce iff: image_iff)
      with ‹∀h. unilateral_substitutes_on A (Ch h)› XXX False have "b ∉ Ch h (insert a (insert b ?B'))"
        using unilateral_substitutes_onD[where f="Ch h" and B="?B'"]
        by (fastforce iff: image_iff)
      with ‹∀h. irc_on A (Ch h)› XXX False show ?thesis
        using consistency_onD[OF irc_on_consistency_on[where f="Ch h"],
                              where A=A and B="insert a (insert b B)" and C="insert a (insert b ?B')"]
              Ch_range'[of _ h "insert a (insert b B)"] Ch_singular
        by simp (blast dest: inj_on_contraD)
    qed
  next
    case False
    with ‹∀h. unilateral_substitutes_on A (Ch h)› XXX show ?thesis by (blast dest: unilateral_substitutes_onD)
  qed
qed

theorem Theorem_3:
  assumes "∀h. irc_on A (Ch h)"
  shows "(∀h. substitutes_on A (Ch h)) ⟷ (∀h. unilateral_substitutes_on A (Ch h) ∧ pareto_separable_on A)"
using %invisible assms
      unilateral_substitutes_on_pareto_separable_on_substitutes_on substitutes_on_pareto_separable_on
      substitutes_on_unilateral_substitutes_on
by blast

end


subsubsection‹ \<^citet>‹"AfacanTurhan:2015"›: @{emph ‹doctor separability›} relates bi- and unilateral substitutes ›

context Contracts
begin

text ‹

\<^citet>‹‹Theorem~1› in "AfacanTurhan:2015"› relate @{const
"bilateral_substitutes"} and @{const "unilateral_substitutes"} using
@{emph ‹doctor separability›}:
\begin{quote}

@{emph ‹[Doctor separability (DS)]›} says that if a doctor is not chosen
from a set of contracts in the sense that no contract of him is
selected, then that doctor should still not be chosen unless a
contract of a new doctor (that is, doctor having no contract in the
given set of contracts) becomes available. For practical purposes, we
can consider DS as capturing contracts where certain groups of doctors
are substitutes. [footnote: If ‹Xd x ∉ Xd ` Ch h (Y
∪ {x, z})›, then doctor ‹Xd x› is not
chosen. And under DS, he continues not to be chosen unless a new
doctor comes. Hence, we can interpret it as the doctors in the given
set of contracts are substitutes.]

\end{quote}

›

definition doctor_separable_on :: "'x set ⇒ 'x cfun ⇒ bool" where
  "doctor_separable_on A f
     ⟷ (∀B⊆A. ∀a b c. {a, b, c} ⊆ A ∧ Xd a ≠ Xd b ∧ Xd b = Xd c ∧ Xd a ∉ Xd ` f (B ∪ {a, b})
         ⟶ Xd a ∉ Xd ` f (B ∪ {a, b, c}))"

abbreviation doctor_separable :: "'x cfun ⇒ bool" where
  "doctor_separable ≡ doctor_separable_on UNIV"

(*<*)

lemmas doctor_separable_def = doctor_separable_on_def[where A=UNIV, simplified]

lemmas doctor_separable_onI = iffD2[OF doctor_separable_on_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]
lemmas doctor_separable_onD = iffD1[OF doctor_separable_on_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp, rotated -1]

(*>*)

lemma unilateral_substitutes_on_doctor_separable_on:
  assumes "unilateral_substitutes_on A f"
  assumes "irc_on A f"
  assumes "∀B⊆A. allocation (f B)"
  assumes "f_range_on A f"
  shows "doctor_separable_on A f"
proof(rule doctor_separable_onI)
  fix B a b c
  assume XXX: "B ⊆ A" "a ∈ A" "b ∈ A" "c ∈ A" "Xd a ≠ Xd b" "Xd b = Xd c" "Xd a ∉ Xd ` f (insert a (insert b B))"
  have "a ∉ f (insert a (insert b (insert c B)))"
  proof(rule notI)
    assume a: "a ∈ f (insert a (insert b (insert c B)))"
    let ?C = "{x ∈ B . Xd x ≠ Xd a ∨ x = a}"
    from ‹irc_on A f› ‹f_range_on A f› XXX(1-3,7)
    have "f (insert a (insert b B)) = f (insert a (insert b ?C))"
      by - (rule consistency_onD[OF irc_on_consistency_on[where A=A and f=f]];
            fastforce dest: f_range_onD[where A=A and f=f and B="insert a (insert b B)"] simp: rev_image_eqI)
    with ‹unilateral_substitutes_on A f› XXX
    have abcC: "a ∉ f (insert a (insert b (insert c ?C)))"
      using unilateral_substitutes_onD[where A=A and f=f and a=c and b=a and B="insert b ?C - {a}"]
      by (force simp: insert_commute)
    from ‹irc_on A f› ‹∀B⊆A. allocation (f B)› ‹f_range_on A f› XXX(1-4) a
    have "f (insert a (insert b (insert c B))) = f (insert a (insert b (insert c ?C)))"
      by - (rule consistency_onD[OF irc_on_consistency_on[where A=A and f=f]], (auto)[4],
            clarsimp, rule conjI, blast dest!: f_range_onD'[where A=A], metis inj_on_contraD insert_subset)
    with a abcC show False by simp
  qed
  moreover
  have "a' ∉ f (insert a (insert b (insert c B)))" if a': "a' ∈ B" "Xd a' = Xd a" for a'
  proof(rule notI)
    assume a'X: "a' ∈ f (insert a (insert b (insert c B)))"
    let ?B = "insert a B - {a'}"
    from XXX a'
    have XXX_7': "Xd a ∉ Xd ` f (insert a' (insert b ?B))"
      by clarsimp (metis imageI insert_Diff_single insert_absorb insert_commute)
    let ?C = "{x ∈ ?B . Xd x ≠ Xd a ∨ x = a'}"
    from ‹irc_on A f› ‹f_range_on A f› XXX(1-3) a' XXX_7'
    have "f (insert a' (insert b ?B)) = f (insert a' (insert b ?C))"
      by - (rule consistency_onD[OF irc_on_consistency_on[where A=A and f=f]];
            fastforce dest: f_range_onD[where A=A and f=f and B="insert a' (insert b ?B)"] simp: rev_image_eqI)
    with ‹unilateral_substitutes_on A f› XXX(1-6) XXX_7' a'
    have abcC: "a' ∉ f (insert a' (insert b (insert c ?C)))"
      using unilateral_substitutes_onD[where A=A and f=f and a=c and b=a' and B="insert b ?C - {a'}"]
      by (force simp: insert_commute rev_image_eqI)
    have "f (insert a' (insert b (insert c ?B))) = f (insert a' (insert b (insert c ?C)))"
    proof(rule consistency_onD[OF irc_on_consistency_on[where A=A and f=f]])
      from a' have "insert a' (insert b (insert c ?B)) = insert a (insert b (insert c B))" by blast
      with ‹∀B⊆A. allocation (f B)› ‹f_range_on A f› XXX(1-4) a' a'X
      show "f (insert a' (insert b (insert c ?B))) ⊆ insert a' (insert b (insert c {x ∈ ?B. Xd x ≠ Xd a ∨ x = a'}))"
        by clarsimp (rule conjI, blast dest!: f_range_onD'[where A=A], metis inj_on_contraD insert_subset)
    qed (use ‹irc_on A f› XXX(1-4) a' in auto)
    with a' a'X abcC show False by simp (metis insert_Diff insert_Diff_single insert_commute)
  qed
  moreover note ‹f_range_on A f› XXX
  ultimately show "Xd a ∉ Xd ` f (insert a (insert b (insert c B)))"
    by (fastforce dest: f_range_onD[where B="insert a (insert b (insert c B))"])
qed

lemma bilateral_substitutes_on_doctor_separable_on_unilateral_substitutes_on:
  assumes "bilateral_substitutes_on A f"
  assumes "doctor_separable_on A f"
  assumes "f_range_on A f"
  shows "unilateral_substitutes_on A f"
proof(rule unilateral_substitutes_onI)
  fix B a b
  assume XXX: "B ⊆ A" "a ∈ A" "b ∈ A" "Xd b ∉ Xd ` B" "b ∉ f (insert b B)"
  show "b ∉ f (insert a (insert b B))"
  proof(cases "Xd a ∈ Xd ` B")
    case True
    then obtain C c where Cc: "B = insert c C" "c ∉ C" "Xd c = Xd a" by (metis Set.set_insert image_iff)
    from ‹b ∉ f (insert b B)› Cc have "b ∉ f (insert b (insert c C))" by simp
    with ‹f_range_on A f› XXX Cc have "Xd b ∉ Xd ` f (insert b (insert c C))"
      by clarsimp (metis f_range_onD' image_eqI insertE insert_subset)
    with ‹doctor_separable_on A f› XXX Cc show ?thesis
      by (auto simp: insert_commute dest: doctor_separable_onD)
  qed (use ‹bilateral_substitutes_on A f› XXX in ‹simp add: bilateral_substitutes_onD›)
qed

theorem unilateral_substitutes_on_doctor_separable_on_bilateral_substitutes_on:
  assumes "irc_on A f"
  assumes "∀B⊆A. allocation (f B)" ― ‹A rephrasing of @{thm [source] "Ch_singular"}.›
  assumes "f_range_on A f"
  shows "unilateral_substitutes_on A f ⟷ bilateral_substitutes_on A f ∧ doctor_separable_on A f"
using %invisible assms
      unilateral_substitutes_on_bilateral_substitutes_on
      unilateral_substitutes_on_doctor_separable_on
      bilateral_substitutes_on_doctor_separable_on_unilateral_substitutes_on
by metis

text‹

\<^citet>‹‹Remark~2› in "AfacanTurhan:2015"› observe the independence of the
@{const "doctor_separable"}, @{const "pareto_separable"} and @{const
"bilateral_substitutes"} conditions.

›

end


subsection‹ Theorems~4 and 5: Doctor optimality ›

context ContractsWithUnilateralSubstitutesAndIRC
begin

text ‹

We return to analyzing the COP following
\<^citet>‹"HatfieldKojima:2010"›. The next goal is to establish a
doctor-optimality result for it in the spirit of
\S\ref{sec:contracts-optimality}.

We first show that, with hospital choice functions satisfying @{const
"unilateral_substitutes"}, we effectively have the @{const
"substitutes"} condition for all contracts that have been rejected. In
other words, hospitals never renegotiate with doctors.

The proof is by induction over the finite set @{term "Y"}.

›

lemma
  assumes "Xd x ∉ Xd ` Ch h X"
  assumes "x ∈ X"
  shows no_renegotiation_union: "x ∉ Ch h (X ∪ Y)"
    and "x ∉ Ch h (insert x ((X ∪ Y) - {z. Xd z = Xd x}))"
using %invisible finite[of Y]
proof induct
  case empty
  { case 1 from ‹Xd x ∉ Xd ` Ch h X› show ?case by clarsimp }
  { case 2 from assms show ?case
      by - (clarsimp, drule subsetD[OF equalityD2[OF consistencyD[OF Ch_consistency[of h], where B=X]], rotated -1], auto simp: image_iff dest: Ch_range') }
next
  case (insert y Y)
  { case 1 show ?case
    proof(cases "y ∈ Ch h (insert y (X ∪ Y))")
      case True note ‹y ∈ Ch h (insert y (X ∪ Y))›
      show ?thesis
      proof(cases "Xd y = Xd x")
        case True with ‹x ∈ X› ‹x ∉ Ch h (X ∪ Y)› ‹y ∈ Ch h (insert y (X ∪ Y))› show ?thesis
          by clarsimp (metis Ch_singular Un_iff inj_onD insert_absorb)
      next
        case False note xy = ‹Xd y ≠ Xd x›
        show ?thesis
        proof(rule notI)
          assume "x ∈ Ch h (X ∪ insert y Y)"
          with ‹x ∈ X› have "x ∈ Ch h (insert y (insert x ((X ∪ Y) - {z. Xd z = Xd x})))"
            by - (rule subsetD[OF equalityD1[OF consistencyD[OF Ch_consistency[of h]]], rotated -1],
                  assumption, clarsimp+, metis Ch_range' Ch_singular Un_iff inj_onD insertE)
          with ‹x ∉ Ch h (insert x (X ∪ Y - {z. Xd z = Xd x}))› show False
            by (force dest: unilateral_substitutesD3[OF spec[OF Ch_unilateral_substitutes, of h], rotated])
        qed
      qed
    next
      case False with ‹x ∉ Ch h (X ∪ Y)› show ?thesis
        using Ch_irc unfolding irc_def by simp
    qed }
  { case 2 from insert(4) show ?case
      by (auto simp: insert_commute insert_Diff_if split: if_splits
               dest: unilateral_substitutesD3[OF spec[OF Ch_unilateral_substitutes, of h], where a=y]) }
qed

text‹

To discharge the first antecedent of this lemma, we need an invariant
for the COP that asserts that, for each doctor @{term "d"}, there is a
subset of the contracts currently offered by @{term "d"} that was
previously uniformly rejected by the COP, for each contract that is
rejected at the current step. To support a later theorem (see
\S\ref{sec:cop-worst}) we require these subsets to be upwards-closed
with respect to the doctor's preferences.

›

definition
  cop_F_rejected_inv :: "'b set ⇒ 'a set ⇒ bool"
where
  "cop_F_rejected_inv ds fp ⟷ (∀x∈RH fp. ∃fp'⊆fp. x ∈ fp' ∧ above (Pd (Xd x)) x ⊆ fp' ∧ Xd x ∉ Xd ` CH fp')"

(*<*)

lemmas cop_F_rejected_invI = iffD2[OF cop_F_rejected_inv_def, rule_format, simplified, unfolded conj_imp_eq_imp_imp]

(*>*)

lemma cop_F_rejected_inv:
  shows "valid ds (λds fp. cop_F_range_inv ds fp ∧ cop_F_closed_inv ds fp ∧ allocation (CH fp)) cop_F_rejected_inv"
proof %invisible (induct rule: validI)
  case base show ?case unfolding cop_F_rejected_inv_def by simp
next
  case (step fp)
  then have "cop_F_closed_inv ds fp"
        and "cop_F_range_inv ds fp"
        and "allocation (CH fp)"
        and "cop_F_rejected_inv ds fp" by blast+
  show ?case
  proof(rule cop_F_rejected_invI)
    fix x assume x: "x ∈ cop_F ds fp" "x ∉ CH (cop_F ds fp)"
    show "∃fp'⊆cop_F ds fp. x ∈ fp' ∧ above (Pd (Xd x)) x ⊆ fp' ∧ Xd x ∉ Xd ` CH fp'"
    proof(cases "Xd x ∈ Xd ` CH (cop_F ds fp)")
      case True
      with ‹x ∉ CH (cop_F ds fp)› obtain y
        where y: "Xd y = Xd x" "y ∈ CH (cop_F ds fp)" "x ≠ y" by (metis imageE)
      from ‹x ∈ cop_F ds fp› show ?thesis
      proof(cases x rule: cop_F_cases)
        case fp note ‹x ∈ fp›
        from ‹y ∈ CH (cop_F ds fp)›
        show ?thesis
        proof(cases y rule: CH_cop_F_cases)
          case CH note ‹y ∈ CH fp›
          with ‹allocation (CH fp)› y(1,3) have "x ∉ CH fp" by (metis inj_on_eq_iff)
          with ‹cop_F_rejected_inv ds fp› ‹x ∈ fp› show ?thesis
            unfolding cop_F_rejected_inv_def by (metis Diff_iff Un_upper1 cop_F_def subset_refl subset_trans)
        next
          case RH_fp note ‹y ∈ RH fp›
          with ‹cop_F_rejected_inv ds fp›
          obtain fp' where "fp' ⊆ fp ∧ y ∈ fp' ∧ above (Pd (Xd y)) y ⊆ fp' ∧ Xd y ∉ Xd ` CH fp'"
            unfolding cop_F_rejected_inv_def by (fastforce simp: mem_CH_Ch)
          with ‹y ∈ CH (cop_F ds fp)› show ?thesis
            using no_renegotiation_union[where x=y and X="fp'" and Y="cop_F ds fp"] cop_F_increasing
            by (clarsimp simp: mem_Ch_CH image_iff) (metis Un_absorb1 mem_CH_Ch subset_trans)
        next
          case CD_on note ‹y ∈ CD_on ds (- RH fp) - fp›
          with cop_F_increasing ‹cop_F_closed_inv ds fp› cop_F_CH_CD_on_disjoint[OF ‹cop_F_closed_inv ds fp› ‹cop_F_range_inv ds fp›] ‹x ∈ fp› y(1) show ?thesis
            unfolding cop_F_closed_inv_def by - (rule exI[where x=fp]; clarsimp; blast)
        qed
      next
        case CD_on
        { fix z assume z: "z ∈ CH (cop_F ds fp)" "Xd z = Xd x"
          from ‹allocation (CH fp)› x(2) z have "z ≠ x" by blast
          from z(1) have False
          proof(cases z rule: CH_cop_F_cases)
            case CH
            with ‹cop_F_range_inv ds fp› ‹cop_F_closed_inv ds fp› ‹x ∈ CD_on ds (- RH fp) - fp› z(2) ‹z ≠ x›
            show False
              using cop_F_CH_CD_on_disjoint by blast
          next
            case RH_fp note ‹z ∈ RH fp›
            with ‹cop_F_rejected_inv ds fp›
            obtain fp' where "fp' ⊆ fp ∧ z ∈ fp' ∧ above (Pd (Xd z)) z ⊆ fp' ∧ Xd z ∉ Xd ` CH fp'"
              unfolding cop_F_rejected_inv_def by (fastforce simp: mem_CH_Ch)
            with ‹z ∈ CH (cop_F ds fp)› show ?thesis
              using no_renegotiation_union[where x=z and X="fp'" and Y="cop_F ds fp"] cop_F_increasing
              by (clarsimp simp: mem_Ch_CH image_iff) (metis Un_absorb1 mem_CH_Ch subset_trans)
          next
            case CD_on note ‹z ∈ CD_on ds (- RH fp) - fp›
            with z(2) ‹x ∈ CD_on ds (- RH fp) - fp› ‹z ≠ x› show False
              by (meson CD_on_inj_on_Xd DiffD1 inj_onD)
          qed }
        with True have False by clarsimp blast
        then show ?thesis ..
      qed
    next
      case False note ‹Xd x ∉ Xd ` CH (cop_F ds fp)›
      with cop_F_closed_inv ‹cop_F_closed_inv ds fp› ‹x ∈ cop_F ds fp›
      show ?thesis by (metis cop_F_closed_inv_def subsetI valid_def)
    qed
  qed
qed

lemma fp_cop_F_rejected_inv:
  shows "cop_F_rejected_inv ds (fp_cop_F ds)"
proof %invisible -
  have "invariant ds (λds fp. cop_F_range_inv ds fp ∧ cop_F_closed_inv ds fp ∧ allocation (CH fp) ∧ cop_F_rejected_inv ds fp)"
    using cop_F_range_inv cop_F_closed_inv cop_F_allocation_inv cop_F_rejected_inv
    by - (rule valid_conj | blast | rule valid_pre)+
  then show ?thesis by (blast dest: invariantD)
qed

text‹

\label{sec:cop-theorem-4}

\<^citet>‹‹Theorem~4› in "HatfieldKojima:2010"› assert that we effectively
recover @{const "substitutes"} for the contracts relevant to the
COP. We cannot adopt their phrasing as it talks about the execution
traces of the COP, and not just its final state. Instead we present
the result we use, which relates two consecutive states in an
execution trace of the COP:

›

theorem Theorem_4:
  assumes "cop_F_rejected_inv ds fp"
  assumes "x ∈ RH fp"
  shows "x ∈ RH (cop_F ds fp)"
using %invisible bspec[OF assms[unfolded cop_F_rejected_inv_def]] cop_F_increasing[of fp ds]
      no_renegotiation_union[where x=x and h="Xh x" and Y="cop_F ds fp"]
by (auto simp: mem_CH_Ch image_iff Ch_CH_irc_idem) (metis le_iff_sup mem_Ch_CH sup.coboundedI1)

text‹

\label{sec:cop-worst}

Another way to interpret @{const "cop_F_rejected_inv"} is to observe
that the doctor-optimal match contains the least preferred of the
contracts that the doctors have offered.

›

corollary fp_cop_F_worst:
  assumes "x ∈ cop ds"
  assumes "y ∈ fp_cop_F ds"
  assumes "Xd y = Xd x"
  shows "(x, y) ∈ Pd (Xd x)"
proof %invisible (rule ccontr)
  assume "(x, y) ∉ Pd (Xd x)"
  with assms have "(y, x) ∈ Pd (Xd x) ∧ x ≠ y"
    by (metis CH_range' Pd_linear eq_iff fp_cop_F_range_inv' order_on_defs(3) total_on_def underS_incl_iff)
  with assms have "y ∉ (cop ds)"
    using fp_cop_F_allocation by (blast dest: inj_onD)
  with fp_cop_F_rejected_inv[of ds] ‹y ∈ fp_cop_F ds›
  obtain fp' where "fp' ⊆ fp_cop_F ds ∧ y ∈ fp' ∧ above (Pd (Xd y)) y ⊆ fp' ∧ Xd y ∉ Xd ` CH fp'"
    unfolding cop_F_rejected_inv_def by fastforce
  with ‹(y, x) ∈ Pd (Xd x) ∧ x ≠ y› assms show False
    using no_renegotiation_union[where x=x and h="Xh x" and X=fp' and Y="fp_cop_F ds"]
    unfolding above_def
    by (clarsimp simp: mem_CH_Ch image_iff) (metis contra_subsetD le_iff_sup mem_Ch_CH mem_Collect_eq)
qed

text‹

The doctor optimality result, Theorem~5, hinges on showing that no
contract in any stable match is ever rejected.

›

definition
  theorem_5_inv :: "'b set ⇒ 'a set ⇒ bool"
where
  "theorem_5_inv ds fp ⟷ RH fp ∩ ⋃{X. stable_on ds X} = {}"

(*<*)

lemma theorem_5_invI:
  assumes "⋀z X. ⟦z ∈ RH fp; z ∈ X; stable_on ds X⟧ ⟹ False"
  shows "theorem_5_inv ds fp"
unfolding theorem_5_inv_def using assms by blast

(*>*)

lemma theorem_5_inv:
  shows "valid ds (λds fp. cop_F_range_inv ds fp ∧ cop_F_closed_inv ds fp
                     ∧ allocation (CH fp) ∧ cop_F_rejected_inv ds fp) theorem_5_inv"
proof(induct rule: validI)
  case base show ?case unfolding theorem_5_inv_def by simp
next
  case (step fp)
  then have "cop_F_range_inv ds fp"
        and "cop_F_closed_inv ds fp"
        and "allocation (CH fp)"
        and "cop_F_rejected_inv ds fp"
        and "theorem_5_inv ds fp" by blast+
  show ?case
  proof(rule theorem_5_invI)
    fix z X assume z: "z ∈ RH (cop_F ds fp)" and "z ∈ X" and "stable_on ds X"
    from ‹theorem_5_inv ds fp› ‹z ∈ X› ‹stable_on ds X›
    have z': "z ∉ RH fp" unfolding theorem_5_inv_def by blast
    define Y where "Y ≡ Ch (Xh z) (cop_F ds fp)"
    from z have YYY: "z ∉ Ch (Xh z) (insert z Y)"
      using consistencyD[OF Ch_consistency]
      by (simp add: mem_CH_Ch Y_def)
         (metis Ch_f_range f_range_on_def insert_subset subset_insertI top_greatest)
    have yRx: "(x, y) ∈ Pd (Xd y)" if "x ∈ X" and "y ∈ Y" and "Xd y = Xd x" for x y
    proof(rule ccontr)
      assume "(x, y) ∉ Pd (Xd y)"
      with Pd_linear ‹cop_F_range_inv ds fp› ‹stable_on ds X› that
      have BBB: "(y, x) ∈ Pd (Xd y) ∧ x ≠ y"
        unfolding Y_def cop_F_def cop_F_range_inv_def order_on_defs total_on_def
        by (clarsimp simp: mem_CD_on_Cd dest!: Ch_range') (metis Cd_range' Int_iff refl_onD stable_on_range')
      from ‹stable_on ds X› ‹cop_F_closed_inv ds fp› ‹theorem_5_inv ds fp› BBB that have "x ∈ fp ∧ y ∈ fp"
        unfolding cop_F_def cop_F_closed_inv_def theorem_5_inv_def above_def Y_def
        by (fastforce simp: mem_CD_on_Cd dest: Ch_range' Cd_preferred)
      with ‹stable_on ds X› ‹theorem_5_inv ds fp› ‹x ∈ X› have "x ∈ Ch (Xh x) fp"
        unfolding theorem_5_inv_def by (force simp: mem_CH_Ch)
      with ‹allocation (CH fp)› ‹Xd y = Xd x› BBB have "y ∉ Ch (Xh z) fp"
        by (metis Ch_range' inj_onD mem_CH_Ch)
      with ‹y ∈ Y› ‹x ∈ fp ∧ y ∈ fp› show False
        unfolding Y_def using Theorem_4[OF ‹cop_F_rejected_inv ds fp›, where x=y]
        by (metis Ch_range' Diff_iff mem_CH_Ch)
    qed
    have "Xd z ∉ Xd ` Y"
    proof(safe)
      fix w assume w: "Xd z = Xd w" "w ∈ Y"
      show False
      proof(cases "z ∈ fp")
        case True note ‹z ∈ fp›
        show False
        proof(cases "w ∈ fp")
          case True note ‹w ∈ fp›
          from ‹Xd z = Xd w› ‹w ∈ Y› z' ‹z ∈ fp› have "w ∉ CH fp"
            by (metis Ch_irc_idem DiffI YYY Y_def ‹allocation (CH fp)› inj_on_eq_iff insert_absorb)
          with Theorem_4[OF ‹cop_F_rejected_inv ds fp›, where x=w] ‹w ∈ Y› ‹w ∈ fp› show False
            unfolding Y_def CH_def by simp
        next
          case False note ‹w ∉ fp›
          with ‹w ∈ Y› have "w ∉ Ch (Xh z) fp ∧ w ∈ cop_F ds fp ∧ Xh w = Xh z"
            unfolding Y_def by (blast dest: Ch_range')
          with ‹cop_F_closed_inv ds fp› ‹cop_F_range_inv ds fp› ‹z ∉ RH fp› ‹w ∉ fp› ‹z ∈ fp› ‹Xd z = Xd w›
          show False
            unfolding cop_F_closed_inv_def cop_F_range_inv_def above_def
            by (fastforce simp: cop_F_def mem_CD_on_Cd Cd_greatest greatest_def)
        qed
      next
        case False note ‹z ∉ fp›
        from ‹cop_F_range_inv ds fp› ‹cop_F_closed_inv ds fp› z ‹z ∉ fp› have "Xd z ∉ Xd ` Ch (Xh z) fp"
          unfolding cop_F_range_inv_def cop_F_closed_inv_def above_def
          by (clarsimp simp: mem_CD_on_Cd Cd_greatest greatest_def dest!: mem_Ch_CH elim!: cop_F_cases)
             (blast dest: CH_range')
        with w ‹z ∈ RH (cop_F ds fp)› ‹z ∉ fp› show False
          by (clarsimp simp: Y_def cop_F_def mem_CH_Ch)
             (metis CD_on_inj_on_Xd Ch_range' Un_iff inj_onD no_renegotiation_union)
      qed
    qed
    show False
    proof(cases "z ∈ Ch (Xh z) (X ∪ Y)")
      case True note ‹z ∈ Ch (Xh z) (X ∪ Y)›
      with ‹z ∈ X› have "Xd z ∈ Xd ` Ch (Xh z) (insert z Y)"
        using no_renegotiation_union[where X="insert z Y" and Y="X - {z}" and x=z and h="Xh z"]
        by clarsimp (metis Un_insert_right insert_Diff Un_commute)
      with ‹Xd z ∉ Xd ` Y› ‹z ∉ Ch (Xh z) (insert z Y)› show False by (blast dest: Ch_range')
    next
      case False note ‹z ∉ Ch (Xh z) (X ∪ Y)›
      have "¬stable_on ds X"
      proof(rule blocking_on_imp_not_stable[OF blocking_onI])
        from False ‹z ∈ X› ‹stable_on ds X›
        show "Ch (Xh z) (X ∪ Y) ≠ Ch (Xh z) X"
          using mem_CH_Ch stable_on_CH by blast
        show "Ch (Xh z) (X ∪ Y) = Ch (Xh z) (X ∪ Ch (Xh z) (X ∪ Y))"
          using Ch_range' by (blast intro!: consistencyD[OF Ch_consistency])
      next
        fix x assume "x ∈ Ch (Xh z) (X ∪ Y)"
        with Ch_singular'[of "Xh z" "X ∪ Ch (Xh z) (cop_F ds fp)"]
             invariant_cop_FD[OF cop_F_range_inv ‹cop_F_range_inv ds fp›]
             stable_on_allocation[OF ‹stable_on ds X›] stable_on_Xd[OF ‹stable_on ds X›]
             stable_on_range'[OF ‹stable_on ds X›]
        show "x ∈ CD_on ds (X ∪ Ch (Xh z) (X ∪ Y))"
          unfolding cop_F_range_inv_def
          by (clarsimp simp: mem_CD_on_Cd Cd_greatest greatest_def)
             (metis Ch_range' IntE Pd_range' Pd_refl Un_iff Y_def inj_onD yRx)
      qed
      with ‹stable_on ds X› show False by blast
    qed
  qed
qed

lemma fp_cop_F_theorem_5_inv:
  shows "theorem_5_inv ds (fp_cop_F ds)"
proof %invisible -
  have "invariant ds (λds fp. cop_F_range_inv ds fp ∧ cop_F_closed_inv ds fp ∧ allocation (CH fp) ∧ cop_F_rejected_inv ds fp ∧ theorem_5_inv ds fp)"
    using cop_F_range_inv cop_F_closed_inv cop_F_allocation_inv cop_F_rejected_inv theorem_5_inv
    by - (rule valid_conj | blast | rule valid_pre)+
  then show ?thesis by (blast dest: invariantD)
qed

theorem Theorem_5:
  assumes "stable_on ds X"
  assumes "x ∈ X"
  shows "∃y ∈ cop ds. (x, y) ∈ Pd (Xd x)"
proof -
  from fp_cop_F_theorem_5_inv assms
  have x: "x ∉ RH (fp_cop_F ds)"
    unfolding theorem_5_inv_def by blast
  show ?thesis
  proof(cases "Xd x ∈ Xd ` cop ds")
    case True
    then obtain z where z: "z ∈ cop ds" "Xd z = Xd x" by auto
    show ?thesis
    proof(cases "(x, z) ∈ Pd (Xd x)")
      case True with z show ?thesis by blast
    next
      case False
      with Pd_linear'[where d="Xd x"] fp_cop_F_range_inv'[of z ds] assms z
      have "(z, x) ∈ Pd (Xd x)"
        unfolding order_on_defs total_on_def by (metis CH_range' refl_onD stable_on_range')
      with fp_cop_F_closed_inv'[of z ds x] x z have "x ∈ fp_cop_F ds"
        unfolding above_def by (force simp: mem_CH_Ch dest: Ch_range')
      with fp_cop_F_allocation x z have "z = x" by (fastforce dest: inj_onD)
      with Pd_linear assms z show ?thesis
        by (meson equalityD2 stable_on_range' underS_incl_iff)
    qed
  next
    case False note ‹Xd x ∉ Xd ` cop ds›
    with assms x show ?thesis
      by (metis DiffI Diff_eq_empty_iff fp_cop_F_all emptyE imageI stable_on_Xd stable_on_range')
  qed
qed

theorem fp_cop_F_doctor_optimal_match:
  shows "doctor_optimal_match ds (cop ds)"
by %invisible (rule doctor_optimal_matchI[OF Theorem_1 Theorem_5]) auto

end

text‹

\label{sec:cop-opposition-of-interests}

The next lemma demonstrates the @{emph ‹opposition of interests›} of
doctors and hospitals: if all doctors weakly prefer one stable match
to another, then the hospitals weakly prefer the converse.

As we do not have linear preferences for hospitals, we use revealed
preference and hence assume @{const "irc"} holds of hospital choice
functions. Our definition of the doctor-preferred ordering @{term
"dpref"} follows the Isabelle/HOL convention of putting the larger
(more preferred) element on the right, and takes care with
unemployment.

›

context Contracts
begin

definition dpref :: "'x set ⇒ 'x set ⇒ bool" where
  "dpref X Y = (∀x∈X. ∃y∈Y. (x, y) ∈ Pd (Xd x))"

lemmas %invisible dprefI = iffD2[OF dpref_def, rule_format]

end

context ContractsWithIRC
begin

theorem Lemma_1:
  assumes "stable_on ds Y"
  assumes "stable_on ds Z"
  assumes "dpref Z Y"
  assumes "x ∈ Ch h Z"
  shows "x ∈ Ch h (Y ∪ Z)"
proof(rule ccontr)
  assume "x ∉ Ch h (Y ∪ Z)"
  from ‹x ∈ Ch h Z› ‹x ∉ Ch h (Y ∪ Z)›
  have "Ch h (Y ∪ Z) ≠ Ch h Z" by blast
  moreover
  have "Ch h (Y ∪ Z) = Ch h (Z ∪ Ch h (Y ∪ Z))"
   by (rule consistency_onD[OF Ch_consistency]; auto dest: Ch_range')
  moreover
  have "y ∈ CD_on ds (Z ∪ Ch h (Y ∪ Z))" if "y ∈ Ch h (Y ∪ Z)" for y
  proof -
    from ‹stable_on ds Y› ‹stable_on ds Z› that
    have "Xd y ∈ ds ∧ y ∈ Field (Pd (Xd y))"
      using stable_on_Xd stable_on_range' Ch_range' by (meson Un_iff)
    with Pd_linear'[of "Xd y"] Ch_singular ‹stable_on ds Y› ‹stable_on ds Z› ‹dpref Z Y› that show ?thesis
      unfolding dpref_def
      by (clarsimp simp: mem_CD_on_Cd Cd_greatest greatest_def)
         (metis Ch_range' Pd_Xd Un_iff eq_iff inj_on_contraD stable_on_allocation underS_incl_iff)
  qed
  ultimately show False by (blast dest: stable_on_blocking_onD[OF ‹stable_on ds Z›])
qed

end

text (in Contracts) ‹

\<^citet>‹‹Corollary~1 (of Theorem~5 and Lemma~1)› in "HatfieldKojima:2010"›:
@{const "unilateral_substitutes"} implies there is a hospital-pessimal
match, which is indeed the doctor-optimal one.

›

context ContractsWithUnilateralSubstitutesAndIRC
begin

theorem Corollary_1:
  assumes "stable_on ds Z"
  shows "dpref Z (cop ds)"
    and "x ∈ Z ⟹ x ∈ Ch (Xh x) (cop ds ∪ Z)"
proof -
  show "dpref Z (cop ds)"
    by (rule dprefI[OF Theorem_5[OF ‹stable_on ds Z›]])
  fix x assume "x ∈ Z" with assms show "x ∈ Ch (Xh x) (cop ds ∪ Z)"
    using Lemma_1[OF Theorem_1 assms ‹dpref Z (cop ds)›] stable_on_CH
    by (fastforce simp: mem_CH_Ch)
qed

text‹

\<^citet>‹‹p1717› in "HatfieldKojima:2010"› show that there is not always a
hospital-optimal/doctor-pessimal match when hospital preferences
satisfy @{const "unilateral_substitutes"}, in contrast to the
situation under @{const "substitutes"} (see
\S\ref{sec:contracts-optimality}). This reflects the loss of the
lattice structure.

›

end


subsection‹ Theorem~6: A ``rural hospitals'' theorem \label{sec:cop-rh} ›

text (in Contracts) ‹

\<^citet>‹‹Theorem~6› in "HatfieldKojima:2010"› demonstrates a ``rural
hospitals'' theorem for the COP assuming hospital choice functions
satisfy @{const "unilateral_substitutes"} and @{const "lad"}, as for
\S\ref{sec:contracts-rh}. However \<^citet>‹‹\S4,
Example~1› in "AygunSonmez:2012-WP"› observe that @{thm [source]
"lad_on_substitutes_on_irc_on"} does not hold with @{const
"bilateral_substitutes"} instead of @{const "substitutes"}, and their
Example~3 similarly for @{const "unilateral_substitutes"}. Moreover
@{const "fp_cop_F"} can yield an unstable allocation with just these
two hypotheses. Ergo we need to assume @{const "irc"} even when we
have @{const "lad"}, unlike before (see \S\ref{sec:contracts-rh}).

This theorem is the foundation for all later strategic results.

›

locale ContractsWithUnilateralSubstitutesAndIRCAndLAD = ContractsWithUnilateralSubstitutesAndIRC + ContractsWithLAD

sublocale ContractsWithSubstitutesAndLAD < ContractsWithUnilateralSubstitutesAndIRCAndLAD
using %invisible Ch_lad by unfold_locales

context ContractsWithUnilateralSubstitutesAndIRCAndLAD
begin

context
  fixes ds :: "'b set"
  fixes X :: "'a set"
  assumes "stable_on ds X"
begin

text‹

The proofs of these first two lemmas are provided by
\<^citet>‹‹Theorem~6› in "HatfieldKojima:2010"›. We treat unemployment in the
definition of the function @{term "A"} as we did in
\S\ref{sec:contracts-t1-converse}.

›

lemma RHT_Cd_card:
  assumes "d ∈ ds"
  shows "card (Cd d X) ≤ card (Cd d (cop ds))"
proof %invisible (cases "d ∈ Xd ` X")
  case True
  then obtain x where "x ∈ X" "Xd x = d" by blast
  with ‹stable_on ds X› have "Cd d X = {x}"
    using Cd_singleton mem_CD_on_Cd stable_on_CD_on by blast
  moreover
  from Theorem_5[OF ‹stable_on ds X› ‹x ∈ X›] obtain y where "Cd d (cop ds) = {y}"
    using Cd_single Cd_singleton FieldI2 ‹Xd x = d› fp_cop_F_allocation by metis
  ultimately show ?thesis by simp
next
  case False
  then have "Cd d X = {}"
    using Cd_Xd Cd_range' by blast
  then show ?thesis by simp
qed

lemma RHT_Ch_card:
  shows "card (Ch h (fp_cop_F ds)) ≤ card (Ch h X)"
proof -
  define A where "A ≡ λX. {y |y. Xd y ∈ ds ∧ y ∈ Field (Pd (Xd y)) ∧ (∀x ∈ X. Xd x = Xd y ⟶ (x, y) ∈ Pd (Xd x))}"
  have "A (cop ds) = fp_cop_F ds" (is "?lhs = ?rhs")
  proof(rule set_elem_equalityI)
    fix x assume "x ∈ ?lhs"
    show "x ∈ ?rhs"
    proof(cases "Xd x ∈ Xd ` cop ds")
      case True with ‹x ∈ ?lhs› show ?thesis
        unfolding A_def by clarsimp (metis CH_range' above_def fp_cop_F_closed_inv' mem_Collect_eq)
    next
      case False with ‹x ∈ ?lhs› fp_cop_F_all show ?thesis
        unfolding A_def by blast
    qed
  next
    fix x assume "x ∈ ?rhs"
    with fp_cop_F_worst show "x ∈ ?lhs"
      unfolding A_def using fp_cop_F_range_inv'[OF ‹x ∈ ?rhs›] by fastforce
  qed
  moreover
  have "CH (A X) = X"
  proof(rule ccontr)
    assume "CH (A X) ≠ X"
    then have "CH (A X) ≠ CH X" using ‹stable_on ds X› stable_on_CH by blast
    then obtain h where XXX: "Ch h (A X) ≠ Ch h X" using mem_CH_Ch by blast
    have "¬stable_on ds X"
    proof(rule blocking_on_imp_not_stable[OF blocking_onI])
      show "Ch h (A X) ≠ Ch h X" by fact
      from Pd_linear ‹stable_on ds X› show "Ch h (A X) = Ch h (X ∪ Ch h (A X))"
        unfolding A_def
        by - (rule consistencyD[OF Ch_consistency],
              auto 10 0 dest: Ch_range' stable_on_Xd stable_on_range' stable_on_allocation inj_onD underS_incl_iff)
    next
      fix x assume "x ∈ Ch h (A X)"
      with Ch_singular Pd_linear show "x ∈ CD_on ds (X ∪ Ch h (A X))"
        unfolding A_def
        by (auto 9 3 simp: mem_CD_on_Cd Cd_greatest greatest_def
                     dest: Ch_range' Pd_range' Cd_Xd Cd_single inj_onD underS_incl_iff
                    intro: FieldI1)
    qed
    with ‹stable_on ds X› show False by blast
  qed
  moreover
  from Pd_linear Theorem_5[OF ‹stable_on ds X›] ‹stable_on ds X› have "A (cop ds) ⊆ A X"
    unfolding A_def order_on_defs by (fastforce dest: Pd_Xd elim: transE)
  then have "card (Ch h (A (cop ds))) ≤ card (Ch h (A X))"
    by (fastforce intro: ladD[OF spec[OF Ch_lad]])
  ultimately show ?thesis by (metis (no_types, lifting) Ch_CH_irc_idem)
qed

text‹

The top-level proof is the same as in \S\ref{sec:contracts-rh}.

›

lemma Theorem_6_fp_cop_F:
  shows "d ∈ ds ⟹ card (Cd d X) = card (Cd d (cop ds))"
    and "card (Ch h X) = card (Ch h (fp_cop_F ds))"
proof -
  let ?Sum_Cd_COP = "∑d∈ds. card (Cd d (cop ds))"
  let ?Sum_Ch_COP = "∑h∈UNIV. card (Ch h (fp_cop_F ds))"
  let ?Sum_Cd_X = "∑d∈ds. card (Cd d X)"
  let ?Sum_Ch_X = "∑h∈UNIV. card (Ch h X)"

  have "?Sum_Cd_COP = ?Sum_Ch_COP"
    using Theorem_1 stable_on_CD_on CD_on_card[symmetric] CH_card[symmetric] by simp
  also have "… ≤ ?Sum_Ch_X"
    using RHT_Ch_card by (simp add: sum_mono)
  also have "… = ?Sum_Cd_X"
    using CD_on_card[symmetric] CH_card[symmetric]
    using ‹stable_on ds X› stable_on_CD_on stable_on_CH by auto
  finally have "?Sum_Cd_X = ?Sum_Cd_COP"
    using RHT_Cd_card by (simp add: eq_iff sum_mono)
  with RHT_Cd_card show "d ∈ ds ⟹ card (Cd d X) = card (Cd d (cop ds))"
    by (fastforce elim: sum_mono_inv)

  have "?Sum_Ch_X = ?Sum_Cd_X"
    using ‹stable_on ds X› stable_on_CD_on stable_on_CH CD_on_card[symmetric] CH_card[symmetric] by simp
  also have "… ≤ ?Sum_Cd_COP"
    using RHT_Cd_card by (simp add: sum_mono)
  also have "… = ?Sum_Ch_COP"
    using CD_on_card[symmetric] CH_card[symmetric]
    using Theorem_1 stable_on_CD_on stable_on_CH by auto
  finally have "?Sum_Ch_COP = ?Sum_Ch_X"
    using RHT_Ch_card by (simp add: eq_iff sum_mono)
  with RHT_Ch_card show "card (Ch h X) = card (Ch h (fp_cop_F ds))"
    by (fastforce elim: sym[OF sum_mono_inv])
qed

end

theorem Theorem_6:
  assumes "stable_on ds X"
  assumes "stable_on ds Y"
  shows "d ∈ ds ⟹ card (Cd d X) = card (Cd d Y)"
    and "card (Ch h X) = card (Ch h Y)"
using %invisible Theorem_6_fp_cop_F assms by simp_all

end


subsection‹ Concluding remarks ›

text‹

We next discuss a kind of interference between doctors termed
@{emph ‹bossiness›} in \S\ref{sec:bossiness}. This has some implications
for the strategic issues we discuss in \S\ref{sec:strategic}.

›
(*<*)

end
(*>*)