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.
›
subsection‹ \<^citet>‹"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. d≠d' ⟶ 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. d≠Xd 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 "∃y∈TruePref_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 "∃y∈TruePref.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: "∃z∈CH (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 "∃y∈match (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.
›
subsection‹ \<^citet>‹"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 "y⇩d"} to @{term "x⇩d"} according to @{term "Pd
d"}, where @{term "x⇩d"} and @{term "y⇩d"} 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 ⟶
¬(∃d∈ds. ∃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);
∀x∈dX (φ 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)" "∀x∈dX (?φ 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
"y⇩d"} to @{term "x⇩d"} according to @{term "Pd d"}, where
@{term "x⇩d"} and @{term "y⇩d"} are the (possibly null)
contracts for @{term "d"} in @{term "φ Pd"} and ‹φ
Pd(d⇩1 := Pd' d⇩1, …, d⇩n := Pd' d⇩n)›,
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
∧ (∀d∈ds'. ∃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' ≠ {};
∀d∈ds'. ∃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)" "∀x∈dX (φ 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: "∀d∈ds''. ∃y∈Y. 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])
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 "∃z∈Pds'.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: "∀d∈ds'. ∃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
∧ (∀d∈ds. ∃y∈Y. 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: "∀d∈ds. ∃y∈Y. 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 "∃y∈Y. (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
text‹
\<^citet>‹‹\S4.4› in "RothSotomayor:1990"› discuss how the non-proposing agents
can strategise to improve their outcomes in one-to-one matches.
›
end