Theory Strategic

(*<*)
theory Strategic
imports
  COP
begin

(*>*)
section‹ Strategic results \label{sec:strategic} ›

text (in ContractsWithSubstitutes) ‹

We proceed to establish a series of strategic results for the COP (see
\S\ref{sec:contracts-cop} and \S\ref{sec:cop}), making use of the
invariants we developed for it. These results also apply to the
matching-with-contracts setting of \S\ref{sec:contracts}, and where
possible we specialize our lemmas to it.

›


subsectioncitet"HatfieldMilgrom:2005": Theorems~10 and~11: Truthful revelation as a Dominant Strategy \label{sec:strategic-contracts} ›

text (in ContractsWithSubstitutes) ‹

Theorems~10 and 11 demonstrate that doctors cannot obtain better
results for themselves in the doctor-optimal match (i.e., @{term "cop ds"}, equal to @{term "match (gfp_F ds)"} by @{thm [source]
"Theorem_15_match"} assuming hospital preferences satisfy @{const
"substitutes"}) by misreporting their preferences. (See
citet‹\S4.2› in "RothSotomayor:1990" for a discussion about the
impossibility of a mechanism being strategy-proof for all agents.)

citet‹{\S}III(B)› in "HatfieldMilgrom:2005" provide the
following intuition:
\begin{quote}

We will show the positive incentive result for the doctor-offering
algorithm in two steps which highlight the different roles of the two
preference assumptions. First, we show that the @{const "substitutes"}
condition, by itself, guarantees that doctors cannot benefit by
exaggerating the ranking of an unattainable contract. More precisely,
if there exists a preferences list for a doctor @{term "d"} such that
@{term "d"} obtains contract @{term "x"} by submitting this list, then
@{term "d"} can also obtain @{term "x"} by submitting a preference
list that includes only contract @{term "x"} [Theorem~10]. Second, we
will show that adding the law of aggregate demand guarantees that a
doctor does at least as well as reporting truthfully as by reporting
any singleton [Theorem~11]. Together, these are the dominant strategy
result.

\end{quote}

We prove Theorem~10 via a lemma that states that the contracts above
@{term "x  X"} for some stable match @{term "X"} with respect to
manipulated preferences @{term "Pd (Xd x)"} do not improve the outcome
for doctor @{term "Xd x"} with respect to their true preferences
@{term "Pd' (Xd x)"} in the doctor-optimal match for @{term "Pd'"}.

This is weaker than citet‹Lemma~1› in "HatfieldKojima:2009" (see
\S\ref{sec:strategic-hk2010-lemma1}) as we do not guarantee that the
allocation does not change. By the bossiness result of
\S\ref{sec:bossiness}, such manipulations can change the outcomes of
the other doctors; this lemma establishes that only weak improvements
are possible.

›

context ContractsWithUnilateralSubstitutesAndIRC
begin

context
  fixes d' :: "'b"
  fixes Pd' :: "'b  'a rel"
  assumes Pd'_d'_linear: "Linear_order (Pd' d')"
  assumes Pd'_d'_range: "Field (Pd' d')  {y. Xd y = d'}"
  assumes Pd': "d. dd'  Pd' d = Pd d"
begin

(*<*)

lemma PdXXX_linear:
  shows "Linear_order (Pd' d)"
using Pd_linear Pd'_d'_linear Pd' by (cases "d = d'") simp_all

lemma PdXXX_range:
  shows "Field (Pd' d)  {x. Xd x = d}"
using Pd_range Pd'_d'_range Pd' by (cases "d = d'") simp_all

lemmas PdXXX_range' = subsetD[OF PdXXX_range, simplified, of x] for x

(*>*)

interpretation PdXXX: ContractsWithUnilateralSubstitutesAndIRC Xd Xh Pd' Ch
using %invisible PdXXX_linear PdXXX_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc
by unfold_locales blast+

theorem Pd_above_irrelevant:
  assumes d'_Field: "dX X d'  Field (Pd' d')"
  assumes d'_Above: "Above (Pd' d') (dX X d')  Above (Pd d') (dX X d')"
  assumes "x  X"
  assumes "stable_on ds X"
  shows "y  PdXXX.cop ds. (x, y)  Pd' (Xd x)"
proof(rule PdXXX.Theorem_5[OF ccontr x  X])
  assume "¬PdXXX.stable_on ds X"
  then show False
  proof(cases rule: PdXXX.not_stable_on_cases)
    case not_individually_rational
    from Pd' stable_on ds X d'_Field have "x  PdXXX.Cd (Xd x) X" if "x  X" for x
      using that unfolding dX_def by (force simp: stable_on_range' stable_on_allocation PdXXX.Cd_single)
    with stable_on ds X not_individually_rational show False
      unfolding PdXXX.individually_rational_on_def
      by (auto simp: PdXXX.mem_CD_on_Cd stable_on_Xd dest: stable_on_CH PdXXX.CD_on_range')
  next
    case not_no_blocking
    then obtain h X'' where "PdXXX.blocking_on ds X h X''"
      unfolding PdXXX.stable_no_blocking_on_def by blast
    have "blocking_on ds X h X''"
    proof(rule blocking_onI)
      fix x assume "x  X''"
      note Pbos = PdXXX.blocking_on_Field[OF PdXXX.blocking_on ds X h X'']
                  PdXXX.blocking_on_allocation[OF PdXXX.blocking_on ds X h X'']
                  PdXXX.blocking_on_CD_on'[OF PdXXX.blocking_on ds X h X'' x  X'']
      show "x  CD_on ds (X  X'')"
      proof(cases "Xd x = d'")
        case True
        from Pd_linear' d'_Field d'_Above x  X'' Xd x = d' Pbos
        have "dX X'' (Xd x)  Field (Pd (Xd x))"
          by (force simp: PdXXX.mem_CD_on_Cd PdXXX.Cd_Above PdXXX.dX_Int_Field_Pd Above_union
                          Int_Un_distrib2 dX_singular intro: Above_Field)
        moreover from stable_on ds X have "dX X (Xd x)  Field (Pd (Xd x))"
          by (force dest: dX_range' stable_on_range')
        moreover note Pd_linear' Pd_range PdXXX_range d'_Field d'_Above x  X'' Xd x = d' Pbos
        ultimately show ?thesis
          by (clarsimp simp: PdXXX.mem_CD_on_Cd PdXXX.Cd_Above_dX mem_CD_on_Cd Cd_Above_dX
                             Above_union dX_union Int_Un_distrib2)
             (fastforce simp: dX_singular intro: Above_Linear_singleton)
      next
        case False
        with x  PdXXX.CD_on ds (X  X'') show ?thesis
          by (clarsimp simp: Pd' PdXXX.mem_CD_on_Cd mem_CD_on_Cd PdXXX.Cd_greatest Cd_greatest)
      qed
    qed (use PdXXX.blocking_on ds X h X'' in simp_all add: PdXXX.blocking_on_def)
    with stable_on ds X show False by (simp add: blocking_on_imp_not_stable)
  qed
qed

end

end

text‹

We now specialize this lemma to Theorem~10 by defining a preference
order for the doctors where distinguished doctors @{term "ds"} submit
single preferences for the contracts they receive in the
doctor-optimal match.

The function @{thm "override_on_def"} denotes function update at
several points.

›

context Contracts
begin

definition Pd_singletons_for_ds :: "'x set  'd set  'd  'x rel" where
  "Pd_singletons_for_ds X ds  override_on Pd (λd. dX X d × dX X d) ds"

(*<*)

lemma Pd_singletons_for_ds_range:
  shows "Field (Pd_singletons_for_ds X ds d)  {x. Xd x = d}"
using Pd_range dX_range unfolding Pd_singletons_for_ds_def
by (clarsimp simp: Field_def override_on_def) blast

lemma Pd_singletons_for_ds_linear:
  assumes "allocation X"
  shows "Linear_order (Pd_singletons_for_ds X ds d)"
unfolding Pd_singletons_for_ds_def using Pd_linear dX_linear[OF assms] by (simp add: override_on_def)

lemma Pd_singletons_for_ds_simps:
  shows "d  ds  Pd_singletons_for_ds X ds d = dX X d × dX X d"
    and "d  ds  Pd_singletons_for_ds X ds d = Pd d"
unfolding Pd_singletons_for_ds_def by simp_all

(*>*)

end

text‹

We interpret our @{const "ContractsWithUnilateralSubstitutesAndIRC"}
locale with respect to this updated preference order, which gives us
the stable match and properties of it.

›

context ContractsWithUnilateralSubstitutesAndIRC
begin

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

interpretation
  Singleton_for_d: ContractsWithUnilateralSubstitutesAndIRC Xd Xh "Pd_singletons_for_ds X {d}" Ch for d
using %invisible Pd_singletons_for_ds_linear Pd_singletons_for_ds_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc
                 stable_on_allocation[OF stable_on ds X]
by unfold_locales blast+

text‹

Our version of citet‹Theorem~10› in "HatfieldMilgrom:2005" (for the COP)
states that if a doctor submits a preference order containing just
@{term "x"}, where @{term "x"} is their contract in some stable match
@{term "X"}, then that doctor receives exactly @{term "x"} in the
doctor-optimal match and all other doctors do at least as well.

›

theorem Theorem_10_fp_cop_F:
  assumes "x  X"
  shows "y  Singleton_for_d.cop d ds. (x, y)  Pd_singletons_for_ds X {d} (Xd x)"
proof(rule Pd_above_irrelevant[where ds=ds and d'=d and X=X])
  from stable_on_allocation stable_on ds X
  show "Above (Pd_singletons_for_ds X {d} d) (Singleton_for_d.dX X d)  Above (Pd d) (Singleton_for_d.dX X d)"
    by (clarsimp simp: Above_def Pd_singletons_for_ds_simps dX_def) (metis inj_on_eq_iff stable_on_range' Pd_refl)
qed (use stable_on_allocation stable_on ds X Pd_singletons_for_ds_linear Pd_singletons_for_ds_range assms
     in simp_all, simp_all add: Pd_singletons_for_ds_simps dX_def)

end

end

text (in ContractsWithSubstitutesAndIRC) ‹

We can recover the original Theorem~10 by specializing this result to
@{const "gfp_F"}.

›

context ContractsWithSubstitutesAndIRC
begin

interpretation
  Singleton_for_d: ContractsWithSubstitutesAndIRC Xd Xh "Pd_singletons_for_ds (match (gfp_F ds)) {d}" Ch
for ds d
using %invisible Pd_singletons_for_ds_linear Pd_singletons_for_ds_range Ch_range Ch_singular Ch_substitutes Ch_irc gfp_F_stable_on
                 stable_on_allocation[OF gfp_F_stable_on[of ds]]
by unfold_locales blast+

theorem Theorem_10:
  assumes "x  match (gfp_F ds)"
  shows "y  match (Singleton_for_d.gfp_F ds d ds). (x, y)  Pd_singletons_for_ds (match (gfp_F ds)) {d} (Xd x)"
using Theorem_10_fp_cop_F Singleton_for_d.Theorem_15_match Theorem_15_match gfp_F_stable_on assms by simp

corollary Theorem_10_d:
  assumes "x  match (gfp_F ds)"
  shows "x  match (Singleton_for_d.gfp_F ds (Xd x) ds)"
using gfp_F_stable_on[of ds] Theorem_10[OF assms(1), of "Xd x"] assms
by (clarsimp simp: Pd_singletons_for_ds_simps dX_def inj_on_eq_iff dest!: stable_on_allocation)

end

text (in ContractsWithSubstitutes) ‹

The second theorem citep‹Theorem~11› in "HatfieldMilgrom:2005" depends on
both Theorem~10 and the rural hospitals theorem
(\S\ref{sec:contracts-rh}, \S\ref{sec:cop-rh}). It shows that,
assuming everything else is fixed, if doctor @{term "d'"} obtains
contract @{term "x"} with (manipulated) preferences @{term "Pd d'"} in
the doctor-optimal match, then they will obtain a contract at least as
good by submitting their true preferences @{term "Pd' d'"} (with
respect to these true preferences).

›

locale TruePrefs = Contracts +
  fixes x :: "'a"
  fixes X :: "'a set"
  fixes ds :: "'b set"
  fixes Pd' :: "'b  'a rel"
  assumes x: "x  X"
  assumes X: "stable_on ds X"
  assumes Pd'_d'_x: "x  Field (Pd' (Xd x))"
  assumes Pd'_d'_linear: "Linear_order (Pd' (Xd x))"
  assumes Pd'_d'_range: "Field (Pd' (Xd x))  {y. Xd y = Xd x}"
  assumes Pd': "d. dXd x  Pd' d = Pd d"

(*<*)

begin

lemma Pd'_linear:
  shows "Linear_order (Pd' d)"
using Pd_linear Pd'_d'_linear Pd' by (cases "d = Xd x") simp_all

lemma Pd'_range:
  shows "Field (Pd' d)  {x. Xd x = d}"
using Pd_range Pd'_d'_range Pd' by (cases "d = Xd x") simp_all

definition Pd'_tax :: "'b  'a rel" where
  "Pd'_tax = (Pd'(Xd x := Restr (Pd' (Xd x)) (above (Pd' (Xd x)) x)))"

lemma Pd'_tax_linear:
  shows "Linear_order (Pd'_tax d)"
using Pd'_linear Pd'_d'_linear Linear_order_Restr unfolding Pd'_tax_def by auto

lemma Pd'_tax_Pd':
  shows "Pd'_tax d  Pd' d"
unfolding Pd'_tax_def by simp

lemma Pd'_tax_range:
  shows "Field (Pd'_tax d)  {x. Xd x = d}"
using Pd'_range Pd'_tax_Pd' by (meson mono_Field subset_trans)

lemma Pd'_tax_x:
  shows "x  Field (Pd'_tax (Xd x))"
using Pd'_d'_x Pd'_d'_linear unfolding Pd'_tax_def above_def order_on_defs
by (fastforce intro: FieldI2 dest: refl_onD)

lemma Pd'_Above:
  assumes "Y  above (Pd' (Xd x)) x"
  assumes "Y  {}"
  shows "Above (Pd' d) Y  Above (Pd'_tax d) Y"
using Pd'_d'_linear assms unfolding Above_def Pd'_tax_def above_def order_on_defs
by (auto simp: Refl_Field_Restr subset_eq elim: transE)

end

(*>*)

locale ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs =
  ContractsWithUnilateralSubstitutesAndIRCAndLAD + TruePrefs
begin

interpretation TruePref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd' Ch
using %invisible Pd'_linear Pd'_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad
by unfold_locales blast+

interpretation TruePref_tax: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd'_tax Ch
using %invisible Pd'_tax_linear Pd'_tax_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad
by unfold_locales blast+

interpretation
  Singleton_for_d: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd_singletons_for_ds X {Xd x}" Ch
using %invisible Pd_singletons_for_ds_linear Pd_singletons_for_ds_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad X stable_on_allocation[OF X]
by unfold_locales blast+

(*<*)

lemma Xd_x_ds:
  shows "Xd x  ds"
using %invisible X stable_on_Xd x by blast

lemma TruePref_tax_Cd_not_x:
  assumes "d  Xd x"
  shows "TruePref_tax.Cd d = Singleton_for_d.Cd d"
using assms spec[OF Pd', of d] stable_on_allocation[OF X]
unfolding TruePref_tax.Cd_def Singleton_for_d.Cd_def by (simp add: Pd'_tax_def Pd_singletons_for_ds_simps)

(*>*)

lemma Theorem_11_Pd'_tax:
  shows "yTruePref_tax.cop ds. (x, y)  Pd'_tax (Xd x)"
proof(rule ccontr)
  let ?Z = "TruePref_tax.cop ds"
  assume "¬?thesis" then have "Xd x  Xd ` ?Z"
    using Pd'_range Pd'_linear[of "Xd x"] Pd'_d'_x unfolding order_on_defs
    by - (clarsimp, drule (1) bspec,
          fastforce simp: Pd'_tax_def above_def Refl_Field_Restr dest: refl_onD
                   dest!: CH_range' TruePref_tax.fp_cop_F_range_inv')
  show False
  proof(cases "Singleton_for_d.stable_on ds ?Z")
    case True
    moreover
    from Theorem_10_fp_cop_F[OF X x, of "Xd x"] X
    have "x  CH (Singleton_for_d.fp_cop_F ds)"
      by (force simp: Pd_singletons_for_ds_simps dX_def dest: inj_onD stable_on_allocation)
    with Singleton_for_d.fp_cop_F_allocation
    have "Singleton_for_d.Cd (Xd x) (Singleton_for_d.cop ds) = {x}"
      by (meson Singleton_for_d.Cd_single Singleton_for_d.Cd_singleton Singleton_for_d.fp_cop_F_range_inv'
                TruePref_tax.CH_range')
    with Singleton_for_d.Theorem_1[of ds]
    have "x  Y" if "Singleton_for_d.stable_on ds Y" for Y
      using Singleton_for_d.Theorem_6_fp_cop_F(1)[where ds="ds" and X="Y" and d="Xd x"] that Xd_x_ds x
            card_Suc_eq[where A="Singleton_for_d.Cd (Xd x) Y" and k=0] stable_on_allocation[OF X]
      by (fastforce simp: Singleton_for_d.Cd_singleton[symmetric] Pd_singletons_for_ds_simps dX_def
                    dest: Singleton_for_d.Cd_range' inj_onD)
    moreover note Xd x  Xd ` ?Z
    ultimately show False by blast
  next
    case False note ¬Singleton_for_d.stable_on ds ?Z
    then show False
    proof(cases rule: Singleton_for_d.not_stable_on_cases)
      case not_individually_rational
      with TruePref_tax.Theorem_1[of ds] Xd x  Xd ` ?Z
      show False
        unfolding TruePref_tax.stable_on_def Singleton_for_d.individually_rational_on_def
                  TruePref_tax.individually_rational_on_def Singleton_for_d.CD_on_def
        by (auto dest: Singleton_for_d.Cd_range')
           (metis TruePref_tax.mem_CD_on_Cd TruePref_tax_Cd_not_x image_eqI)
    next
      case not_no_blocking
      then obtain h X'' where "Singleton_for_d.blocking_on ds ?Z h X''"
        unfolding Singleton_for_d.stable_no_blocking_on_def by blast
      have "TruePref_tax.blocking_on ds ?Z h X''"
      proof(rule TruePref_tax.blocking_onI)
        fix y assume "y  X''"
        with Singleton_for_d.blocking_on ds ?Z h X'' have YYY: "y  Singleton_for_d.CD_on ds (?Z  X'')"
          unfolding Singleton_for_d.blocking_on_def by blast
        show "y  TruePref_tax.CD_on ds (?Z  X'')"
        proof(cases "Xd y = Xd x")
          case True
          with inj_on_eq_iff[OF stable_on_allocation x] X YYY have "y = x"
            by (fastforce simp: Singleton_for_d.mem_CD_on_Cd Pd_singletons_for_ds_simps dX_def
                          dest: Singleton_for_d.Cd_range')
          with X Xd_x_ds TruePref_tax.Theorem_1[of ds] Xd x  Xd ` ?Z y  X''
          show ?thesis
            using Singleton_for_d.blocking_on_allocation[OF Singleton_for_d.blocking_on ds ?Z h X'']
            by (clarsimp simp: TruePref_tax.mem_CD_on_Cd TruePref_tax.Cd_greatest greatest_def Pd'_tax_x)
               (metis TruePref_tax.Pd_range' image_eqI inj_on_contraD TruePref_tax.Pd_refl)
        next
          case False with YYY show ?thesis
            by (simp add: Singleton_for_d.mem_CD_on_Cd TruePref_tax.mem_CD_on_Cd TruePref_tax_Cd_not_x)
        qed
      qed (use Singleton_for_d.blocking_on ds ?Z h X'' in simp_all add: Singleton_for_d.blocking_on_def)
      with TruePref_tax.Theorem_1[of ds] show False by (simp add: TruePref_tax.blocking_on_imp_not_stable)
    qed
  qed
qed

theorem Theorem_11_fp_cop_F:
  shows "yTruePref.cop ds. (x, y)  Pd' (Xd x)"
proof -
  from Theorem_11_Pd'_tax
  obtain y where y: "y  CH (TruePref_tax.fp_cop_F ds)"
            and xy: "(x, y)  Pd'_tax (Xd x)" ..
  from TruePref_tax.stable_on_range'[OF TruePref_tax.Theorem_1]
  have "dX (CH (TruePref_tax.fp_cop_F ds)) (Xd x)  Field (Pd' (Xd x))"
    by (clarsimp simp: dX_def) (metis (no_types, opaque_lifting) Pd'_tax_Pd' contra_subsetD mono_Field)
  moreover
  from TruePref_tax.fp_cop_F_allocation[of ds] Pd'_tax_Pd' y xy
  have "Above (Pd' (Xd x)) (dX (CH (TruePref_tax.fp_cop_F ds)) (Xd x))
      Above (Pd'_tax (Xd x)) (dX (CH (TruePref_tax.fp_cop_F ds)) (Xd x))"
    by - (rule Pd'_Above; fastforce simp: dX_singular above_def dest: TruePref_tax.Pd_Xd)
  moreover note Pd'_linear Pd'_range TruePref_tax.Theorem_1[of ds] y
  ultimately have z: "zCH (TruePref.fp_cop_F ds). (y, z)  Pd' (Xd y)"
    by - (rule TruePref_tax.Pd_above_irrelevant[where d'="Xd x" and X="CH (TruePref_tax.fp_cop_F ds)"];
          simp add: Pd'_tax_def)
  from Pd'_linear xy z show ?thesis
    unfolding Pd'_tax_def order_on_defs by clarsimp (metis TruePref.Pd_Xd transE)
qed

end

locale ContractsWithSubstitutesAndLADAndTruePrefs =
  ContractsWithSubstitutesAndLAD + TruePrefs

sublocale ContractsWithSubstitutesAndLADAndTruePrefs
        < ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs
by %invisible unfold_locales

context ContractsWithSubstitutesAndLADAndTruePrefs
begin

interpretation TruePref: ContractsWithSubstitutesAndLAD Xd Xh Pd' Ch
using %invisible Pd'_linear Pd'_range Ch_range Ch_singular Ch_substitutes Ch_irc Ch_lad
by unfold_locales blast+

theorem Theorem_11:
  shows "ymatch (TruePref.gfp_F ds). (x, y)  Pd' (Xd x)"
using Theorem_11_fp_cop_F TruePref.Theorem_15_match by simp

end

text‹

Note that this theorem depends on the hypotheses introduced by the
@{const "TruePrefs"} locale, and only applies to doctor @{term "Xd
x"}. The following sections show more general and syntactically
self-contained results.

We omit citet‹Theorem~12› in "HatfieldMilgrom:2005", which demonstrates
the almost-necessity of LAD for truth revelation to be the dominant
strategy for doctors.

›


subsectioncitet"HatfieldKojima:2009" and "HatfieldKojima:2010": The doctor-optimal match is group strategy-proof \label{sec:strategic-gsp} ›

text citet‹Theorem~7› in "HatfieldKojima:2010" assert that the COP is group
strategy-proof, which we define below. We begin by focusing on a
single agent citep"HatfieldKojima:2009": \begin{quote}

A mechanism @{term "φ"} is @{emph ‹strategy-proof›} if, for any
preference profile @{term "Pd"}, there is no doctor @{term "d"} and
preferences @{term "Pd'"} such that @{term "d"} strictly prefers
@{term "yd"} to @{term "xd"} according to @{term "Pd
d"}, where @{term "xd"} and @{term "yd"} are the
(possibly null) contracts for @{term "d"} in @{term "φ Pd"} and
φ Pd(d := Pd')›, respectively.

\end{quote}

The syntax @{thm "fun_upd_def"} denotes function update at a point.

We make this definition in the Contracts› locale to
avail ourselves of some types and the Xd› and
Xh› constants. We also restrict hospital preferences to
those that guarantee our earlier strategic results.  As @{term
"gfp_F"} requires these to satisfy the stronger @{const "substitutes"}
constraint for stable matches to exist, we now deal purely with the
COP.

›

context Contracts
begin

abbreviation (input) mechanism_domain :: "('d  'x rel)  ('h  'x cfun)  bool" where
  "mechanism_domain  ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh"

definition strategy_proof :: "'d set  ('d, 'h, 'x) mechanism  bool" where
  "strategy_proof ds φ 
    (Pd Ch. mechanism_domain Pd Ch 
     ¬(dds. Pd'. mechanism_domain (Pd(d:=Pd')) Ch
        (yφ (Pd(d:=Pd')) Ch ds. y  AboveS (Pd d) (dX (φ Pd Ch ds) d))))"

(*<*)

lemma strategy_proofI:
  assumes "Pd Pd' Ch d y.  mechanism_domain Pd Ch; mechanism_domain (Pd(d:=Pd')) Ch; d  ds;
                             y  φ (Pd(d := Pd')) Ch ds; y  Field (Pd d);
                             xdX (φ Pd Ch ds) d. x  y  (x, y)  Pd d   False"
  shows "strategy_proof ds φ"
unfolding strategy_proof_def AboveS_def using assms by blast

(*>*)
text‹›

theorem fp_cop_F_strategy_proof:
  shows "strategy_proof ds Contracts.cop" (is "strategy_proof _ ")
proof %invisible (rule strategy_proofI)
  fix Pd Pd' Ch d y
  assume A: "mechanism_domain Pd Ch" and B: "mechanism_domain (Pd(d:=Pd')) Ch"
     and y: "y   (Pd(d := Pd')) Ch ds" "y  Field (Pd d)" "xdX ( Pd Ch ds) d. x  y  (x, y)  Pd d"
  from A interpret TruePref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch .
  from B interpret ManiPref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd(d := Pd')" Ch .
  from B y interpret ManiPref: ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs Xd Xh "Pd(d := Pd')" Ch y " (Pd(d := Pd')) Ch ds" ds Pd
    by unfold_locales (simp_all add: FieldI2 TruePref.Pd_Xd TruePref.Pd_linear TruePref.Pd_range' subsetI ManiPref.Theorem_1)
  from ManiPref.Theorem_11_fp_cop_F obtain z where "z  TruePref.cop ds" "(y, z)  Pd (Xd y)" ..
  with TruePref.Pd_linear TruePref.stable_on_allocation[OF TruePref.Theorem_1[of ds]] TruePref.Pd_Xd TruePref.Pd_range' y
  show False
    unfolding order_on_defs antisym_def dX_def by (metis (mono_tags, lifting) mem_Collect_eq)
qed

end

text‹

The adaptation to groups is straightforward
citep"HatfieldKojima:2009" and "HatfieldKojima:2010":
\begin{quote}

A mechanism @{term "φ"} is @{emph ‹group strategy-proof›} if, for
any preference profile @{term "Pd"}, there is no group of doctors
@{term "ds'  ds"} and a preference profile @{term "Pd'"}
such that every @{term "d  ds'"} strictly prefers @{term
"yd"} to @{term "xd"} according to @{term "Pd d"}, where
@{term "xd"} and @{term "yd"} are the (possibly null)
contracts for @{term "d"} in @{term "φ Pd"} and φ
Pd(d1 := Pd' d1, …, dn := Pd' dn)›,
respectively.

\end{quote}

This definition requires all doctors in the coalition to strictly
prefer the outcome with manipulated preferences, as
\citeauthor{Kojima:2010}'s bossiness results (see
\S\ref{sec:bossiness}) show that a doctor may influence other doctors'
allocations without affecting their own. See
citet‹\S3› in "HatfieldKojima:2009" for discussion, and also
citet‹Chapter~4› in "RothSotomayor:1990"; in particular their \S4.3.1
discusses the robustness of these results and exogenous transfers.

›

context Contracts
begin

definition group_strategy_proof :: "'d set  ('d, 'h, 'x) mechanism  bool" where
  "group_strategy_proof ds φ 
    (Pd Ch. mechanism_domain Pd Ch 
     ¬(ds'ds. ds'  {}  (Pd'. mechanism_domain (override_on Pd Pd' ds') Ch
        (dds'. yφ (override_on Pd Pd' ds') Ch ds. y  AboveS (Pd d) (dX (φ Pd Ch ds) d)))))"

(*<*)

lemma group_strategy_proofI:
  assumes "Pd Pd' Ch ds'.  mechanism_domain Pd Ch; mechanism_domain (override_on Pd Pd' ds') Ch; ds'  ds; ds'  {};
                             dds'. yφ (override_on Pd Pd' ds') Ch ds. y  AboveS (Pd d) (dX (φ Pd Ch ds) d)   False"
  shows "group_strategy_proof ds φ"
unfolding group_strategy_proof_def using assms by blast

lemmas group_strategy_proofD = iffD1[OF group_strategy_proof_def, simplified, unfolded disj_imp, simplified, rule_format]

(*>*)

lemma group_strategy_proof_strategy_proof:
  assumes "group_strategy_proof ds φ"
  shows "strategy_proof ds φ"
proof %invisible (rule strategy_proofI)
  fix Pd Pd' Ch d y
  assume "mechanism_domain Pd Ch" "mechanism_domain (Pd(d := Pd')) Ch" "d  ds"
         "y  φ (Pd(d := Pd')) Ch ds" "y  Field (Pd d)" "xdX (φ Pd Ch ds) d. x  y  (x, y)  Pd d"
  with assms show False
    unfolding group_strategy_proof_def
    by (clarsimp dest!: spec[where x=Pd] spec[where x=Ch])
       (fastforce simp: override_on_insert AboveS_def dest!: spec[where x="{d}"])
qed

end

text‹

\label{sec:strategic-hk2010-lemma1}

Perhaps surprisingly, citet‹Lemma~1, for a single
doctor› in "HatfieldKojima:2010" assert that shuffling any contract above
the doctor-optimal one to the top of a doctor's preference order
preserves exactly the doctor-optimal match, which on the face of it
seems to contradict the bossiness result of \S\ref{sec:bossiness}: by
the earlier strategy-proofness results, this cannot affect the outcome
for that particular doctor, but by bossiness it may affect others.
The key observation is that this manipulation preserves blocking
coalitions in the presence of @{const "lad"}.

This result is central to showing the group-strategy-proofness of the
COP.

›

context Contracts
begin

definition shuffle_to_top :: "'x set  'd  'x rel" where
  "shuffle_to_top Y = (λd. Pd d - dX Y d × UNIV  (Domain (Pd d)  dX Y d) × dX Y d)"

definition Pd_shuffle_to_top :: "'d set  'x set  'd  'x rel" where
  "Pd_shuffle_to_top ds' Y = override_on Pd (shuffle_to_top Y) ds'"

(*<*)

lemma shuffle_to_top_Field:
  assumes "allocation Y"
  shows "Field (shuffle_to_top Y d) = Field (Pd d)  dX Y d"
unfolding shuffle_to_top_def Field_def using dX_empty_or_singleton[OF assms]
by (auto simp: Domain.simps; meson FieldI2 equalityE Pd_refl)

lemma shuffle_to_top_Total:
  assumes "allocation Y"
  shows "Total (shuffle_to_top Y d)"
using Pd_linear'[of d] dX_empty_or_singleton[OF assms]
unfolding order_on_defs total_on_def shuffle_to_top_Field[OF assms]
by (auto simp: shuffle_to_top_def Domain.simps dest: refl_onD)

lemma shuffle_to_top_linear:
  assumes "allocation Y"
  shows "Linear_order (shuffle_to_top Y d)"
using Pd_linear'[of d] dX_empty_or_singleton[OF assms] shuffle_to_top_Total[OF assms]
unfolding shuffle_to_top_def order_on_defs
by (auto simp: Field_def intro!: antisymI refl_onI transI dest: refl_onD antisymD elim: transE)

lemma shuffle_to_top_range:
  shows "Field (shuffle_to_top Y d)  {x. Xd x = d}"
unfolding shuffle_to_top_def using Pd_range dX_range by (force simp: Field_def)

lemma shuffle_to_top_range':
  assumes "(x, y)  shuffle_to_top Y d"
  shows "x  Field (Pd d)  dX Y d  y  Field (Pd d)  dX Y d"
using assms unfolding shuffle_to_top_def by (auto intro: FieldI1 FieldI2)

lemma Pd_shuffle_to_top_linear:
  assumes "allocation Y"
  shows "Linear_order (Pd_shuffle_to_top ds' Y d)"
unfolding Pd_shuffle_to_top_def using Pd_linear shuffle_to_top_linear[OF assms] by (cases "d  ds'") simp_all

lemma Pd_shuffle_to_top_range:
  shows "Field (Pd_shuffle_to_top ds' Y d)  {x. Xd x = d}"
unfolding Pd_shuffle_to_top_def using Pd_range shuffle_to_top_range by (cases "d  ds'") simp_all

lemma Pd_shuffle_to_top_simps:
  shows "Pd_shuffle_to_top (insert d ds') Y = (Pd_shuffle_to_top ds' Y)(d := shuffle_to_top Y d)"
    and "d  ds'  Pd_shuffle_to_top ds' Y d = shuffle_to_top Y d"
    and "d  ds'  Pd_shuffle_to_top ds' Y d = Pd d"
unfolding Pd_shuffle_to_top_def by (simp_all add: override_on_insert)

lemma Pd_shuffle_to_top_Field:
  assumes "allocation Y"
  shows "Field (Pd_shuffle_to_top ds' Y d) = Field (Pd d)  (if d  ds' then dX Y d else {})"
by (simp add: Pd_shuffle_to_top_simps shuffle_to_top_Field[OF assms])

lemma Above_shuffle_to_top:
  assumes "x  Above (shuffle_to_top Y (Xd x)) X"
  assumes "y  Y"
  assumes "allocation Y"
  assumes "y  X"
  shows "x = y"
using assms unfolding Above_def shuffle_to_top_def
by (fastforce simp: dX_singular dest: Pd_Xd dX_range' Pd_range' inj_onD)

(*>*)

end

context ContractsWithUnilateralSubstitutesAndIRCAndLAD
begin

lemma Lemma_1:
  assumes "allocation Y"
  assumes III: "dds''. yY. y  AboveS (Pd d) (dX (cop ds) d)"
  shows "cop ds = Contracts.cop (Pd_shuffle_to_top ds'' Y) Ch ds"
using finite[of ds''] subset_refl
proof(induct ds'' rule: finite_subset_induct')
  case empty show ?case by (simp add: Pd_shuffle_to_top_simps)
next
  case (insert d ds')
  from insert
  interpret Pds': ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd_shuffle_to_top ds' Y" Ch
    using %invisible Pd_shuffle_to_top_linear[OF allocation Y] Pd_shuffle_to_top_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad
    by unfold_locales simp_all
  let ?Z = "CH (Pds'.fp_cop_F ds)"
  note IH = cop ds = ?Z
  let ?Pd_shuffle_to_top = "Pd_shuffle_to_top (insert d ds') Y"
  from insert interpret Pdds': ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh ?Pd_shuffle_to_top Ch
    using %invisible Pd_shuffle_to_top_linear[OF allocation Y] Pd_shuffle_to_top_range Ch_range Ch_singular Ch_unilateral_substitutes Ch_irc Ch_lad
    by unfold_locales (simp_all add: Pd_shuffle_to_top_simps(1)[symmetric])
  ― ‹\citet[Lemma~1, for a single doctor]{HatfieldKojima:2010}›
  have XXX: "?Z = CH (Pdds'.fp_cop_F ds)"
  proof(rule Pdds'.doctor_optimal_match_unique[OF Pdds'.doctor_optimal_matchI Pdds'.fp_cop_F_doctor_optimal_match])
    show "Pdds'.stable_on ds ?Z"
    proof(rule Pdds'.stable_onI)
      show "Pdds'.individually_rational_on ds ?Z"
      proof(rule Pdds'.individually_rational_onI)
        show "Pdds'.CD_on ds ?Z = ?Z" (is "?lhs = ?rhs")
        proof(rule set_elem_equalityI)
          fix x assume "x  ?rhs"
          with allocation Y IH Pds'.Theorem_1[of ds] d  ds' show "x  ?lhs"
            by (clarsimp simp: Pds'.stable_on_Xd Pdds'.mem_CD_on_Cd Pdds'.Cd_greatest greatest_def
                               Pd_shuffle_to_top_Field[OF allocation Y],
                simp add: Pd_shuffle_to_top_simps shuffle_to_top_def dX_def Set.Ball_def,
                metis stable_on_range'[OF Theorem_1[of ds]] inj_on_contraD[OF Pds'.fp_cop_F_allocation[of ds]]
                      fp_cop_F_worst[of _ ds] Pd_range' Pds'.CH_range')
        qed (meson IntE Pdds'.CD_on_range')
        show "CH ?Z = ?Z" by (simp add: CH_irc_idem)
      qed
      show "Pdds'.stable_no_blocking_on ds ?Z"
      proof(rule Pdds'.stable_no_blocking_onI2)
        fix h X'' assume Pbo: "Pdds'.blocking_on ds ?Z h X''"
        have "Pds'.blocking_on ds ?Z h X''"
        proof(rule Pds'.blocking_onI)
          fix x assume "x  X''"
          note Pbos = Pdds'.blocking_on_allocation[OF Pdds'.blocking_on ds ?Z h X'']
                      Pdds'.blocking_on_CD_on'[OF Pdds'.blocking_on ds ?Z h X'' x  X'']
                      Pdds'.blocking_on_Cd[OF Pdds'.blocking_on ds ?Z h X'', where d="Xd x"]
          show "x  Pds'.CD_on ds (?Z  X'')"
          proof(cases "Xd x = d")
            case True
            from allocation Y III d  ds'' Xd x = d
            have "dX Y (Xd x)  Field (Pd (Xd x))"
                by clarsimp (metis AboveS_Pd_Xd AboveS_Field dX_range' inj_on_eq_iff)
            moreover with allocation Y d  ds'
                          Pdds'.blocking_on_Field[OF Pdds'.blocking_on ds ?Z h X'', where d=d] Xd x = d
            have "dX X'' (Xd x)  Field (Pd (Xd x))"
              by (force simp: Pd_shuffle_to_top_simps shuffle_to_top_Field)
            moreover note allocation Y bspec[OF III[unfolded IH] d  ds''] d  ds' x  X'' Xd x = d
                          Pds'.stable_on_allocation[OF Pds'.Theorem_1] Pbos
            ultimately show ?thesis
              by (clarsimp simp: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_Above Pdds'.Cd_Above
                                 Int_Un_distrib2 Pd_shuffle_to_top_Field)
                 (clarsimp simp: Pd_shuffle_to_top_simps dX_singular dX_Int_Field_Pd;
                  fastforce simp: Above_def AboveS_def Pd_refl shuffle_to_top_def dX_def intro: FieldI1 dest: Pd_range' iff: inj_on_eq_iff)
         next
            case False
            from Pbos Xd x  d
            show ?thesis
              by (simp add: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_greatest Pdds'.Cd_greatest)
                 (simp add: Pd_shuffle_to_top_simps)
          qed
        qed (use Pdds'.blocking_on ds ?Z h X'' in simp_all add: Pdds'.blocking_on_def)
        with Pds'.Theorem_1[of ds] show False by (simp add: Pds'.blocking_on_imp_not_stable)
      qed
    qed
  next
    fix W w assume "Pdds'.stable_on ds W" "w  W"
      from III d  ds'' IH
      obtain y where Y: "y  Y" "y  AboveS (Pd d) (dX (Pds'.cop ds) d)" "Xd y = d"
        by (metis AboveS_Pd_Xd)
      show "zPds'.cop ds. (w, z)  Pd_shuffle_to_top (insert d ds') Y (Xd w)"
      proof(cases "y  W")
        case True note y  W
        from d  ds' Pdds'.stable_on ds W Y y  W
        interpret Pdds': ContractsWithUnilateralSubstitutesAndIRCAndLADAndTruePrefs
                           Xd Xh "Pd_shuffle_to_top (insert d ds') Y" Ch y W ds "Pd_shuffle_to_top ds' Y"
          using %invisible Pds'.Pd_linear Pds'.Pd_range Pd_shuffle_to_top_simps Pd_range' unfolding AboveS_def
          by unfold_locales auto
        from d  ds' Y Pdds'.Theorem_11_fp_cop_F have False
          using Pds'.stable_on_allocation[OF Pds'.Theorem_1[of ds]] Pd_linear Pd_range'
          unfolding order_on_defs antisym_def AboveS_def dX_def
          by (clarsimp simp: Pd_shuffle_to_top_simps) (blast dest: Pd_Xd)
        then show ?thesis ..
      next
        case False note y  W
        show ?thesis
        proof (cases "Pds'.stable_on ds W")
          case True note Pds'.stable_on ds W
          with allocation Y d  ds' Y w  W y  W show ?thesis
            using Pds'.Theorem_5[OF Pds'.stable_on ds W w  W]
            by (auto 0 2 simp: Pd_shuffle_to_top_simps shuffle_to_top_def dX_def AboveS_def dest: Pd_range' inj_onD)
        next
          case False note ¬Pds'.stable_on ds W
          then show ?thesis
          proof(cases rule: Pds'.not_stable_on_cases)
            case not_individually_rational
            note Psos = Pdds'.stable_on_allocation[OF Pdds'.stable_on ds W]
                        Pdds'.stable_on_CH[OF Pdds'.stable_on ds W]
                        Pdds'.stable_on_Xd[OF Pdds'.stable_on ds W]
            have "x  Pds'.Cd (Xd x) W" if "x  W" for x
            proof(cases "Xd x = d")
              case True
              with allocation Y allocation W Y(1,3) y  W
                   Pdds'.stable_on_range'[OF Pdds'.stable_on ds W x  W] x  W
              show ?thesis by (force simp: Pd_shuffle_to_top_Field dest: dX_range' inj_onD intro: Pds'.Cd_single)
            next
              case False
              with allocation Y allocation W Pdds'.stable_on_range'[OF Pdds'.stable_on ds W x  W] x  W
              show ?thesis by (auto simp: Pd_shuffle_to_top_Field intro!: Pds'.Cd_single)
            qed
            with not_individually_rational Pdds'.CH W = W Psos(3) show ?thesis
              unfolding Pds'.individually_rational_on_def by (auto simp: Pds'.mem_CD_on_Cd dest: Pds'.Cd_range')
        next
          case not_no_blocking
          then obtain h X'' where Pbo: "Pds'.blocking_on ds W h X''"
            unfolding Pds'.stable_no_blocking_on_def by blast
          have "Pdds'.blocking_on ds W h X''"
          proof(rule Pdds'.blocking_onI)
            fix x assume "x  X''"
            note Pbos = Pds'.blocking_on_allocation[OF Pds'.blocking_on ds W h X'']
                        Pds'.blocking_on_CD_on'[OF Pds'.blocking_on ds W h X'' x  X'']
                        Pds'.blocking_on_Field[OF Pds'.blocking_on ds W h X'', where d=d]
            show "x  Pdds'.CD_on ds (W  X'')"
            proof(cases "Xd x = d")
              case True
              from allocation Y III d  ds''  Xd x = d
              have "dX Y (Xd x)  Field (Pd (Xd x))"
                by clarsimp (metis AboveS_Pd_Xd AboveS_Field dX_range' inj_on_eq_iff)
              moreover with d  ds' Xd x = d Pbos
              have "dX X'' (Xd x)  Field (Pd (Xd x))"
                by (clarsimp simp: Pd_shuffle_to_top_simps)
              moreover note allocation Y d  ds' y  W Xd y = d x  X'' Pbos
              ultimately show ?thesis
                by (clarsimp simp: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_Above Pdds'.Cd_Above
                                   Int_Un_distrib2)
                   (clarsimp simp: Pd_shuffle_to_top_simps shuffle_to_top_Field dX_singular dX_Int_Field_Pd Un_absorb2,
                    force simp: y  Y shuffle_to_top_def dX_def Above_def dest: inj_onD intro: FieldI1)
            next
              case False
              from Pbos Xd x  d show ?thesis
                by (simp add: Pdds'.mem_CD_on_Cd Pds'.mem_CD_on_Cd Pds'.Cd_greatest Pdds'.Cd_greatest)
                   (simp add: Pd_shuffle_to_top_simps)
            qed
          qed (use Pds'.blocking_on ds W h X'' in simp_all add: Pds'.blocking_on_def)
          with Pdds'.stable_on ds W have False by (simp add: Pdds'.blocking_on_imp_not_stable)
          then show ?thesis ..
        qed
      qed
    qed
  qed
  from ?Z = CH (Pdds'.fp_cop_F ds) IH show "cop ds = Pdds'.cop ds" by simp
qed

text‹

The top-level theorem states that the COP is group strategy proof. To
account for the quantification over preferences, we directly use the
raw constants from the @{const "Contracts"} locale.

›

theorem fp_cop_F_group_strategy_proof:
  shows "group_strategy_proof ds Contracts.cop"
        (is "group_strategy_proof _ ")
proof(rule group_strategy_proofI)
  fix Pd Pds' Ch ds'
  assume XXX: "mechanism_domain Pd Ch" "mechanism_domain (override_on Pd Pds' ds') Ch"
     and YYY: "ds'  ds" "ds'  {}"
     and ZZZ: "dds'. y (override_on Pd Pds' ds') Ch ds. y  AboveS (Pd d) (dX ( Pd Ch ds) d)"
  from XXX(1) interpret TruePref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh Pd Ch .
  from XXX(2) interpret
    ManiPref: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "override_on Pd Pds' ds'" Ch .
  let ?Y = "ManiPref.cop ds"
  let ?Z = "TruePref.cop ds"
  let ?Pd_shuffle_to_top = "TruePref.Pd_shuffle_to_top ds' ?Y"
  interpret ManiPref': ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh ?Pd_shuffle_to_top Ch
    using TruePref.Ch_unilateral_substitutes TruePref.Ch_irc TruePref.Ch_lad TruePref.Ch_range TruePref.Ch_singular
          TruePref.Pd_shuffle_to_top_linear ManiPref.stable_on_allocation[OF ManiPref.Theorem_1[of ds]]
          TruePref.Pd_shuffle_to_top_range ManiPref.dX_range
    by unfold_locales simp_all
  let ?Y' = "ManiPref'.cop ds"
  have "ManiPref'.stable_on ds ?Y"
  proof(rule ManiPref'.stable_onI)
    show "ManiPref'.individually_rational_on ds ?Y"
    proof(rule ManiPref'.individually_rational_onI)
      show "ManiPref'.CD_on ds ?Y = ?Y" (is "?lhs = ?rhs")
      proof(rule set_elem_equalityI)
        fix x assume "x  ?rhs"
        then have "Xd x  ds  (Xd x  ds'  x  Field (Pd (Xd x)))"
          by (metis ManiPref.fp_cop_F_range_inv' TruePref.CH_range' override_on_apply_notin)
        with ManiPref.Theorem_1[of ds] x  ?rhs show "x  ?lhs"
          by (fastforce dest: ManiPref.stable_on_allocation
                    simp: ManiPref'.Cd_single ManiPref'.mem_CD_on_Cd TruePref.Pd_shuffle_to_top_Field dX_def)
      qed (meson IntE ManiPref'.CD_on_range')
      show "ManiPref'.CH ?Y = ?Y" by (simp add: ManiPref'.CH_irc_idem)
    qed
    show "ManiPref'.stable_no_blocking_on ds ?Y"
    proof(rule ManiPref'.stable_no_blocking_onI2)
      fix h X'' assume "ManiPref'.blocking_on ds ?Y h X''"
      have "ManiPref.blocking_on ds ?Y h X''"
      proof(rule ManiPref.blocking_onI)
        fix x assume "x  X''"
        note Pbos = ManiPref'.blocking_on_Field[OF ManiPref'.blocking_on ds ?Y h X'', where d="Xd x"]
                    ManiPref'.blocking_on_allocation[OF ManiPref'.blocking_on ds ?Y h X'']
                    ManiPref'.blocking_on_CD_on'[OF ManiPref'.blocking_on ds ?Y h X'' x  X'']
                    ManiPref'.blocking_on_Cd[OF ManiPref'.blocking_on ds ?Y h X'', where d="Xd x"]
        show "x  ManiPref.CD_on ds (?Y  X'')"
        proof(cases "Xd x  ds'")
          case True
          from ManiPref.fp_cop_F_allocation[of ds] x  X'' Xd x  ds' Pbos bspec[OF ZZZ Xd x  ds']
          have "dX X'' (Xd x)  Field (Pds' (Xd x))"
            by (clarsimp simp: dX_singular ManiPref'.mem_CD_on_Cd ManiPref'.Cd_Above TruePref.Pd_shuffle_to_top_Field)
               (fastforce simp: TruePref.Pd_shuffle_to_top_simps dX_singular dest: TruePref.AboveS_Pd_Xd
                          dest: ManiPref.fp_cop_F_range_inv' ManiPref.CH_range' TruePref.Above_shuffle_to_top)
          moreover from ManiPref.stable_on_range'[OF ManiPref.Theorem_1] Xd x  ds'
          have "dX ?Y (Xd x)  Field (Pds' (Xd x))"
            by (metis dX_range' override_on_apply_in subsetI)
          moreover note bspec[OF ZZZ Xd x  ds'] x  X'' Xd x  ds' Pbos
          ultimately show ?thesis
            using ManiPref.Pd_linear'[of "Xd x"] ManiPref.fp_cop_F_allocation[of ds]
                  ManiPref'.fp_cop_F_allocation[of ds]
            by (clarsimp simp: ManiPref'.mem_CD_on_Cd ManiPref'.Cd_Above_dX ManiPref.mem_CD_on_Cd
                               ManiPref.Cd_Above_dX dX_union dX_singular
                               TruePref.Pd_shuffle_to_top_Field TruePref.AboveS_Pd_Xd)
               (force simp: TruePref.Pd_shuffle_to_top_simps insert_absorb elim: Above_Linear_singleton
                     dest!: TruePref.Above_shuffle_to_top)
        next
          case False
          with Pbos show ?thesis
            by (fastforce simp: ManiPref'.mem_CD_on_Cd ManiPref'.Cd_greatest ManiPref.mem_CD_on_Cd
                                ManiPref.Cd_greatest TruePref.Pd_shuffle_to_top_simps)
        qed
      qed (use ManiPref'.blocking_on ds ?Y h X'' in simp_all add: ManiPref'.blocking_on_def)
      with ManiPref.Theorem_1[of ds] show False by (simp add: ManiPref.blocking_on_imp_not_stable)
    qed
  qed
  with ManiPref'.stable_on_allocation have "{x  ?Y. Xd x  ds'}  {x  ?Y'. Xd x  ds'}"
    by (force dest: ManiPref'.Theorem_5[of ds]
              simp: TruePref.Pd_shuffle_to_top_simps TruePref.shuffle_to_top_def dX_def dest: inj_onD)
  moreover
  from ManiPref.stable_on_allocation[OF ManiPref.Theorem_1] ZZZ
  have "?Z = ?Y'" by (rule TruePref.Lemma_1)
  moreover note YYY ZZZ
  ultimately show False
    unfolding AboveS_def dX_def by (fastforce simp: ex_in_conv[symmetric] dest: TruePref.Pd_range')
qed

end

text (in ContractsWithSubstitutes) ‹

Again, this result does not directly apply to @{term "gfp_F"} due to
the mechanism domain hypothesis.

Finally, citet‹Corollary~2› in "HatfieldKojima:2010" (respectively,
citet‹Corollary~1› in "HatfieldKojima:2009") assert that the COP (@{const
"gfp_F"}) is ``weakly Pareto optimal'', i.e., that there is no @{const
"individually_rational"} allocation that every doctor strictly prefers
to the doctor-optimal match.

›

context ContractsWithUnilateralSubstitutesAndIRCAndLAD
begin

theorem Corollary_2:
  assumes "ds  {}"
  shows "¬(Y. individually_rational_on ds Y
         (dds. yY. y  AboveS (Pd d) (dX (cop ds) d)))"
proof(unfold individually_rational_on_def, safe)
  fix Y assume "CD_on ds Y = Y" "CH Y = Y"
           and Z: "dds. yY. y  AboveS (Pd d) (dX (cop ds) d)"
  from CD_on ds Y = Y have "allocation Y" by (metis CD_on_inj_on_Xd)
  from CD_on ds Y = Y
  interpret Y: ContractsWithUnilateralSubstitutesAndIRCAndLAD Xd Xh "Pd_singletons_for_ds Y ds" Ch
    using Ch_unilateral_substitutes Ch_irc Ch_lad Ch_range Ch_singular Pd_singletons_for_ds_range
          Pd_singletons_for_ds_linear[OF CD_on_inj_on_Xd]
    by unfold_locales (simp_all, metis)
  from Y.fp_cop_F_doctor_optimal_match Y.doctor_optimal_matchI
  have "CH (Y.fp_cop_F ds) = Y"
  proof(rule Y.doctor_optimal_match_unique)
    show "Y.stable_on ds Y"
    proof(rule Y.stable_onI)
      show "Y.individually_rational_on ds Y"
      proof(rule Y.individually_rational_onI)
        from CD_on ds Y = Y CD_on_Xd[where A=Y and ds=ds] show "Y.CD_on ds Y = Y"
          unfolding Y.CD_on_def CD_on_def
          by (force simp: Y.Cd_greatest Cd_greatest greatest_def Pd_singletons_for_ds_simps dX_def)
        from CH Y = Y show "Y.CH Y = Y" .
      qed
      show "Y.stable_no_blocking_on ds Y"
        by (rule Y.stable_no_blocking_onI,
            drule subset_trans[OF _ Y.CD_on_range],
            clarsimp simp: Pd_singletons_for_ds_def dX_def Un_absorb1 subset_eq sup_commute)
    qed
  next
    fix x X assume "x  X" "Y.stable_on ds X"
    with Y.Theorem_5[of ds X x] Pd_singletons_for_ds_linear[OF allocation Y]
    show "yY. (x, y)  Pd_singletons_for_ds Y ds (Xd x)"
      by (fastforce simp: Pd_singletons_for_ds_simps Y.stable_on_Xd dX_def)
  qed
  from Z CH (Y.fp_cop_F ds) = Y show False
    using group_strategy_proofD[OF
      fp_cop_F_group_strategy_proof
      ContractsWithUnilateralSubstitutesAndIRCAndLAD_axioms subset_refl
      ds  {}
      Y.ContractsWithUnilateralSubstitutesAndIRCAndLAD_axioms[unfolded Pd_singletons_for_ds_def]]
    unfolding Pd_singletons_for_ds_def by force
qed

end

textcitet‹\S4.4› in "RothSotomayor:1990" discuss how the non-proposing agents
can strategise to improve their outcomes in one-to-one matches.

›
(*<*)

end
(*>*)