Theory Contracts
theory Contracts
imports
Choice_Functions
"HOL-Library.Dual_Ordered_Lattice"
"HOL-Library.Bourbaki_Witt_Fixpoint"
"HOL-Library.While_Combinator"
"HOL-Library.Product_Order"
begin
section‹ \<^citet>‹"HatfieldMilgrom:2005"›: Matching with contracts \label{sec:contracts} ›
text‹
We take the original paper on matching with contracts by
\<^citet>‹"HatfieldMilgrom:2005"› as our roadmap, which follows a similar
path to \<^citet>‹‹\S2.5› in "RothSotomayor:1990"›. We defer further motivation
to these texts. Our first move is to capture the scenarios described
in their {\S}I(A) (p916) in a locale.
›
locale Contracts =
fixes Xd :: "'x::finite ⇒ 'd::finite"
fixes Xh :: "'x ⇒ 'h::finite"
fixes Pd :: "'d ⇒ 'x rel"
fixes Ch :: "'h ⇒ 'x cfun"
assumes Pd_linear: "∀d. Linear_order (Pd d)"
assumes Pd_range: "∀d. Field (Pd d) ⊆ {x. Xd x = d}"
assumes Ch_range: "∀h. ∀X. Ch h X ⊆ {x∈X. Xh x = h}"
assumes Ch_singular: "∀h. ∀X. inj_on Xd (Ch h X)"
begin
text ‹
The set of contracts is modelled by the type @{typ "'x"}, a free type
variable that will later be interpreted by some non-empty
set. Similarly @{typ "'d"} and @{typ "'h"} track the names of doctors
and hospitals respectively. All of these are finite by virtue of
belonging to the ‹finite› type class.
We fix four constants:
\begin{itemize}
\item ‹Xd› (‹Xh›) projects the name of the
relevant doctor (hospital) from a contract;
\item ‹Pd› maps doctors to their linear preferences over
some subset of contracts that name them (assumptions @{thm [source]
Pd_linear} and @{thm [source] Pd_range}); and
\item ‹Ch› maps hospitals to their choice functions
(\S\ref{sec:cf}), which are similarly constrained to contracts that
name them (assumption @{thm [source] Ch_range}). Moreover their
choices must name each doctor at most once, i.e., ‹Xd›
must be injective on these (assumption @{thm [source]
"Ch_singular"}).
\end{itemize}
The reader familiar with the literature will note that we do not have
a null contract (also said to represent the @{emph ‹outside option›} of
unemployment), and instead use partiality of the doctors'
preferences. This provides two benefits: firstly, ‹Xh› is
a total function here, and secondly we achieve some economy of
description when instantiating this locale as ‹Pd› only
has to rank the relevant contracts.
We note in passing that neither the doctors' nor hospitals' choice
functions are required to be decisive, unlike the standard literature
on choice functions (\S\ref{sec:cf}).
In addition to the above, the following constitute the definitions
that must be trusted for the results we prove to be meaningful.
›
definition Cd :: "'d ⇒ 'x cfun" where
"Cd d ≡ set_option ∘ MaxR.MaxR_opt (Pd d)"
definition CD_on :: "'d set ⇒ 'x cfun" where
"CD_on ds X = (⋃d∈ds. Cd d X)"
abbreviation CD :: "'x set ⇒ 'x set" where
"CD ≡ CD_on UNIV"
definition CH :: "'x cfun" where
"CH X = (⋃h. Ch h X)"
text‹
The function @{const "Cd"} constructs a choice function from the
doctor's linear preferences (see \S\ref{sec:cf-linear}). Both @{const
"CD"} and @{const "CH"} simply aggregate opinions in the obvious
way. The functions @{const "CD_on"} is parameterized with a set of
doctors to support the proofs of \S\ref{sec:contracts-vacancy-chain}.
We also define ‹RD› (‹Rh›,
‹RH›) to be the subsets of a given set of contracts that
are rejected by the doctors (hospitals). (The abbreviation @{const
"Rf"} is defined in \S\ref{sec:cf-rf}.)
›
abbreviation (input) RD_on :: "'d set ⇒ 'x cfun" where
"RD_on ds ≡ Rf (CD_on ds)"
abbreviation (input) RD :: "'x cfun" where
"RD ≡ RD_on UNIV"
abbreviation (input) Rh :: "'h ⇒ 'x cfun" where
"Rh h ≡ Rf (Ch h)"
abbreviation (input) RH :: "'x cfun" where
"RH ≡ Rf CH"
text ‹
A @{emph ‹mechanism›} maps doctor and hospital preferences into a match
(here a set of contracts).
›
type_synonym (in -) ('d, 'h, 'x) mechanism = "('d ⇒ 'x rel) ⇒ ('h ⇒ 'x cfun) ⇒ 'd set ⇒ 'x set"
lemmas Pd_linear' = Pd_linear[rule_format]
lemmas Pd_range' = subsetD[OF Pd_range[rule_format], simplified, of x d] for x d
lemma Pd_refl:
assumes "x ∈ Field (Pd d)"
shows "(x, x) ∈ Pd d"
using assms Pd_linear' by (meson subset_refl underS_incl_iff)
lemma Pd_Xd:
assumes "(x, y) ∈ Pd d"
shows "Xd x = d ∧ Xd y = d"
using assms Pd_range contra_subsetD unfolding Field_def by blast
lemma Above_Pd_Xd:
assumes "x ∈ Above (Pd d) X"
shows "Xd x = d"
using assms by (blast dest: Above_Field Pd_range')
lemma AboveS_Pd_Xd:
assumes "x ∈ AboveS (Pd d) X"
shows "Xd x = d"
using assms by (blast dest: AboveS_Field Pd_range')
interpretation Cd: linear_cf "Pd d" "Cd d" for d
using Cd_def Pd_linear by unfold_locales simp_all
lemmas Cd_domain = Cd.domain
lemmas Cd_f_range = Cd.f_range
lemmas Cd_range = Cd.range
lemmas Cd_range' = Cd.range'
lemmas Rf_Cd_mono = Cd.Rf_mono_on[of UNIV, unfolded mono_on_mono]
lemmas Cd_Chernoff = Cd.Chernoff
lemmas Cd_path_independent = Cd.path_independent
lemmas Cd_iia = Cd.iia
lemmas Cd_irc = Cd.irc
lemmas Cd_lad = Cd.lad
lemmas Cd_mono = Cd.mono
lemmas Cd_greatest = Cd.greatest
lemmas Cd_preferred = Cd.preferred
lemmas Cd_singleton = Cd.singleton
lemmas Cd_union = Cd.union
lemmas Cd_idem = iia_f_idem[OF Cd.f_range[of UNIV d, folded Cd_def] Cd_iia[of UNIV], simplified] for d
lemma Cd_Xd:
shows "x ∈ Cd d X ⟹ Xd x = d"
using Pd_range Cd_range by fastforce
lemma Cd_inj_on_Xd:
shows "inj_on Xd (Cd d X)"
by (rule inj_onI) (clarsimp simp: Cd_Xd Cd_singleton)
lemma Cd_range_disjoint:
assumes "d ≠ d'"
shows "Cd d A ∩ Cd d' A = {}"
using assms Cd_range Pd_range by blast
lemma Cd_single:
assumes "x ∈ X"
assumes "inj_on Xd X"
assumes "x ∈ Field (Pd d)"
shows "x ∈ Cd d X"
using assms Pd_linear unfolding Cd_greatest greatest_def
by clarsimp (metis Pd_Xd inj_on_eq_iff subset_refl underS_incl_iff)
lemma Cd_Above:
shows "Cd d X = Above (Pd d) (X ∩ Field (Pd d)) ∩ X"
unfolding Cd_greatest greatest_Above Above_def by blast
definition maxR :: "'d ⇒ 'x ⇒ 'x ⇒ 'x" where
"maxR d x y = (if (x, y) ∈ Pd d then y else x)"
definition MaxR_f :: "'d ⇒ 'x ⇒ 'x option ⇒ 'x option" where
"MaxR_f d = (λx acc. if x ∈ Field (Pd d) then Some (case acc of None ⇒ x | Some y ⇒ maxR d x y) else acc)"
lemma MaxR_maxR:
shows "MaxR.maxR (Pd d) = maxR d"
by (simp add: fun_eq_iff maxR_def Cd.maxR_code)
lemma MaxR_MaxR_f:
shows "MaxR.MaxR_f (Pd d) = MaxR_f d"
by (simp add: fun_eq_iff Cd.MaxR_f_code MaxR_f_def MaxR_maxR cong: option.case_cong)
lemmas Cd_code[code] = Cd.code[unfolded MaxR_MaxR_f]
lemma Cd_simps[simp, nitpick_simp]:
shows "Cd d {} = {}"
"Cd d (insert x A) = (if x ∈ Field (Pd d) then if Cd d A = {} then {x} else {maxR d x y |y. y ∈ Cd d A} else Cd d A)"
unfolding Cd.simps MaxR_maxR by simp_all
lemma CD_on_def2:
shows "CD_on ds A = (⋃d∈ds. Cd d (A ∩ Field (Pd d)))"
using Cd_domain unfolding CD_on_def by blast
lemma CD_on_Xd:
assumes "x ∈ CD_on ds A"
shows "Xd x ∈ ds"
using assms Cd_Xd unfolding CD_on_def by blast
lemma mem_CD_on_Cd:
shows "x ∈ CD_on ds X ⟷ (x ∈ Cd (Xd x) X ∧ Xd x ∈ ds)"
unfolding CD_on_def using Cd_range Cd_Xd by blast
lemma CD_on_domain:
assumes "d ∈ ds"
shows "CD_on ds A ∩ Field (Pd d) = Cd d (A ∩ Field (Pd d))"
unfolding CD_on_def2 using assms Cd_range by (force dest: Pd_range')
lemma CD_on_range:
shows "CD_on ds A ⊆ A ∩ (⋃d∈ds. Field (Pd d))"
using Cd_range unfolding CD_on_def by blast
lemmas CD_on_range' = subsetD[OF CD_on_range]
lemma CD_on_f_range_on:
shows "f_range_on A (CD_on ds)"
by (rule f_range_onI) (meson CD_on_range Int_subset_iff)
lemma RD_on_mono:
shows "mono (RD_on ds)"
unfolding CD_on_def by (rule monoI) (auto dest: monoD[OF Rf_Cd_mono])
lemma CD_on_Chernoff:
shows "Chernoff (CD_on ds)"
using mono_on_mono RD_on_mono[of ds] Rf_mono_on_iia_on[of UNIV] Chernoff_on_iia_on by (simp add: fun_eq_iff) blast
lemma CD_on_irc:
shows "irc (CD_on ds)"
by (rule ircI) (fastforce simp: CD_on_def ircD[OF Cd_irc] simp del: Cd_simps cong: SUP_cong)
lemmas CD_on_consistency = irc_on_consistency_on[OF CD_on_irc, simplified]
lemma CD_on_path_independent:
shows "path_independent (λX. CD_on ds X)"
using CD_on_f_range_on CD_on_Chernoff CD_on_consistency by (blast intro: path_independent_onI2)
lemma CD_on_simps:
shows "CD_on ds {} = {}"
using CD_on_range by blast
lemmas CD_on_iia = RD_on_mono[unfolded Rf_mono_iia]
lemmas CD_on_idem = iia_f_idem[OF CD_on_f_range_on CD_on_iia, simplified]
lemma CD_on_inj_on_Xd:
shows "inj_on Xd (CD_on ds X)"
unfolding CD_on_def by (rule inj_onI) (clarsimp simp: Cd_Xd Cd_singleton)
lemma CD_on_card:
shows "card (CD_on ds X) = (∑d∈ds. card (Cd d X))"
unfolding CD_on_def by (simp add: card_UN_disjoint Cd_range_disjoint)
lemma CD_on_closed:
assumes "inj_on Xd X"
assumes "X ⊆ (⋃d∈ds. Field (Pd d))"
shows "CD_on ds X = X"
using assms Cd_domain Cd_single[OF _ assms(1)] unfolding CD_on_def2 by (force dest: Cd_range')
lemmas Ch_singular' = Ch_singular[rule_format]
lemmas Ch_range' = subsetD[OF Ch_range[rule_format], simplified, of x h X] for x h X
lemma Ch_simps:
shows "Ch h {} = {}"
using Ch_range by blast
lemma Ch_range_disjoint:
assumes "h ≠ h'"
shows "Ch h A ∩ Ch h' A = {}"
using assms Ch_range by blast
lemma Ch_f_range:
shows "f_range (Ch h)"
using Ch_range unfolding f_range_on_def by blast
lemma CH_card:
shows "card (CH X) = (∑h∈UNIV. card (Ch h X))"
unfolding CH_def by (simp add: card_UN_disjoint Ch_range_disjoint)
lemma CH_simps:
shows "CH {} = {}"
unfolding CH_def by (simp add: Ch_simps)
lemma CH_range:
shows "CH A ⊆ A"
unfolding CH_def using Ch_range by blast
lemmas CH_range' = subsetD[OF CH_range]
lemmas CH_f_range_on = f_range_onI[OF CH_range]
lemma mem_CH_Ch:
shows "x ∈ CH X ⟷ x ∈ Ch (Xh x) X"
unfolding CH_def using Ch_range by blast
lemma mem_Ch_CH:
assumes "x ∈ Ch h X"
shows "x ∈ CH X"
unfolding CH_def using assms Ch_range by blast
text‹
An @{emph ‹allocation›} is a set of contracts where each names a distinct
doctor. (Hospitals can contract multiple doctors.)
›
abbreviation (input) allocation :: "'x set ⇒ bool" where
"allocation ≡ inj_on Xd"
text‹
We often wish to extract a doctor's or a hospital's contract from an
@{const "allocation"}.
›
definition dX :: "'x set ⇒ 'd ⇒ 'x set" where
"dX X d = {x ∈ X. Xd x = d}"
definition hX :: "'x set ⇒ 'h ⇒ 'x set" where
"hX X h = {x ∈ X. Xh x = h}"
lemma dX_union:
shows "dX (X ∪ Y) d = dX X d ∪ dX Y d"
unfolding dX_def by auto
lemma dX_range:
shows "∀d. dX X d ⊆ {x. Xd x = d}"
unfolding dX_def by clarsimp
lemma dX_range':
assumes "x ∈ dX X d"
shows "x ∈ X ∧ Xd x = d"
using assms unfolding dX_def by simp
lemma dX_empty_or_singleton:
assumes "allocation X"
shows "∀d. dX X d = {} ∨ (∃x. dX X d = {x})"
unfolding dX_def using ‹allocation X› by (fastforce dest: inj_onD)
lemma dX_linear:
assumes "allocation X"
shows "Linear_order (dX X d × dX X d)"
using spec[OF dX_empty_or_singleton[OF ‹allocation X›], where x=d] by fastforce
lemma dX_singular:
assumes "allocation X"
assumes "x ∈ X"
assumes "d = Xd x"
shows "dX X d = {x}"
using assms unfolding dX_def by (fastforce dest: inj_onD)
lemma dX_Int_Field_Pd:
assumes "dX X d ⊆ Field (Pd d)"
shows "X ∩ Field (Pd d) = dX X d"
using assms unfolding dX_def by (fastforce dest: Pd_range')
lemma Cd_Above_dX:
assumes "dX X d ⊆ Field (Pd d)"
shows "Cd d X = Above (Pd d) (dX X d) ∩ X"
using assms unfolding Cd_greatest greatest_Above Above_def dX_def by (auto dest: Pd_range')
text‹
@{emph ‹Stability›} is the key property we look for in a match (here a
set of contracts), and consists of two parts.
Firstly, we ask that it be @{emph ‹individually rational›}, i.e., the
contracts in the match are actually acceptable to all
participants. Note that this implies the match is an @{const
"allocation"}.
›
definition individually_rational_on :: "'d set ⇒ 'x set ⇒ bool" where
"individually_rational_on ds X ⟷ CD_on ds X = X ∧ CH X = X"
abbreviation individually_rational :: "'x set ⇒ bool" where
"individually_rational ≡ individually_rational_on UNIV"
text‹
The second condition requires that there be no coalition of a hospital
and one or more doctors who prefer another set of contracts involving
them; the hospital strictly, the doctors weakly. Contrast this
definition with the classical one for stable marriages given in
\S\ref{sec:sotomayor}.
›
definition blocking_on :: "'d set ⇒ 'x set ⇒ 'h ⇒ 'x set ⇒ bool" where
"blocking_on ds X h X' ⟷ X' ≠ Ch h X ∧ X' = Ch h (X ∪ X') ∧ X' ⊆ CD_on ds (X ∪ X')"
definition stable_no_blocking_on :: "'d set ⇒ 'x set ⇒ bool" where
"stable_no_blocking_on ds X ⟷ (∀h X'. ¬blocking_on ds X h X')"
abbreviation stable_no_blocking :: "'x set ⇒ bool" where
"stable_no_blocking ≡ stable_no_blocking_on UNIV"
definition stable_on :: "'d set ⇒ 'x set ⇒ bool" where
"stable_on ds X ⟷ individually_rational_on ds X ∧ stable_no_blocking_on ds X"
abbreviation stable :: "'x set ⇒ bool" where
"stable ≡ stable_on UNIV"
lemma stable_onI:
assumes "individually_rational_on ds X"
assumes "stable_no_blocking_on ds X"
shows "stable_on ds X"
unfolding stable_on_def using assms by blast
lemma individually_rational_onI:
assumes "CD_on ds X = X"
assumes "CH X = X"
shows "individually_rational_on ds X"
unfolding individually_rational_on_def using assms by blast
lemma individually_rational_on_CD_on:
assumes "individually_rational_on ds X"
shows "CD_on ds X = X"
using assms unfolding individually_rational_on_def by blast
lemma individually_rational_on_Cd:
assumes "individually_rational_on ds X"
shows "Cd d X = dX X d"
using individually_rational_on_CD_on[OF assms]
by (auto simp: dX_def mem_CD_on_Cd dest: Cd_range' Cd_Xd)
lemma individually_rational_on_empty:
shows "individually_rational_on ds {}"
by (simp add: CD_on_simps CH_simps individually_rational_onI)
lemma blocking_onI:
assumes "X'' ≠ Ch h X"
assumes "X'' = Ch h (X ∪ X'')"
assumes "⋀x. x ∈ X'' ⟹ x ∈ CD_on ds (X ∪ X'')"
shows "blocking_on ds X h X''"
unfolding blocking_on_def using assms by blast
lemma blocking_on_imp_not_stable:
assumes "blocking_on ds X h X''"
shows "¬stable_on ds X"
unfolding stable_on_def stable_no_blocking_on_def using assms by blast
lemma blocking_on_allocation:
assumes "blocking_on ds X h X''"
shows "allocation X''"
using assms unfolding blocking_on_def by (metis Ch_singular')
lemma blocking_on_Field:
assumes "blocking_on ds X h X''"
shows "dX X'' d ⊆ Field (Pd d)"
using assms blocking_on_allocation[OF assms] unfolding blocking_on_def dX_def
by (force simp: Pd_range' dest: CD_on_range')
lemma blocking_on_CD_on:
assumes "blocking_on ds X h X''"
shows "X'' ⊆ CD_on ds (X ∪ X'')"
using assms unfolding blocking_on_def by blast
lemma blocking_on_CD_on':
assumes "blocking_on ds X h X''"
assumes "x ∈ X''"
shows "x ∈ CD_on ds (X ∪ X'')"
using assms unfolding blocking_on_def by blast
lemma blocking_on_Cd:
assumes "blocking_on ds X h X''"
shows "dX X'' d ⊆ Cd d (X ∪ X'')"
using assms unfolding blocking_on_def by (force dest: dX_range' simp: mem_CD_on_Cd)
lemma stable_no_blocking_onI:
assumes "⋀h X''. ⟦X'' = Ch h (X ∪ X''); X'' ≠ Ch h X; X'' ⊆ CD_on ds (X ∪ X'')⟧ ⟹ False"
shows "stable_no_blocking_on ds X"
unfolding stable_no_blocking_on_def blocking_on_def using assms by blast
lemma stable_no_blocking_onI2:
assumes "⋀h X''. blocking_on ds X h X'' ⟹ False"
shows "stable_no_blocking_on ds X"
unfolding stable_no_blocking_on_def using assms by blast
lemma "stable_no_blocking_on ds UNIV"
using stable_no_blocking_onI by fastforce
lemma
assumes "stable_on ds X"
shows stable_on_CD_on: "CD_on ds X = X"
and stable_on_Xd: "x ∈ X ⟹ Xd x ∈ ds"
and stable_on_range': "x ∈ X ⟹ x ∈ Field (Pd (Xd x))"
and stable_on_CH: "CH X = X"
and stable_on_no_blocking_on: "stable_no_blocking_on ds X"
using assms mem_CD_on_Cd Cd_range' Pd_range'
unfolding stable_on_def individually_rational_on_def by blast+
lemma stable_on_allocation:
assumes "stable_on ds X"
shows "allocation X"
using assms unfolding stable_on_def individually_rational_on_def by (metis CD_on_inj_on_Xd)
lemma stable_on_blocking_onD:
assumes "stable_on ds X"
shows "⟦X'' = Ch h (X ∪ X''); X'' ⊆ CD_on ds (X ∪ X'')⟧ ⟹ X'' = Ch h X"
using ‹stable_on ds X› unfolding stable_on_def individually_rational_on_def stable_no_blocking_on_def blocking_on_def by blast
lemma not_stable_on_cases[consumes 1, case_names not_individually_rational not_no_blocking]:
assumes "¬ stable_on ds X"
assumes "¬ individually_rational_on ds X ⟹ P"
assumes "¬ stable_no_blocking_on ds X ⟹ P"
shows "P"
using assms unfolding stable_on_def by blast
text‹›
end
subsection‹ Theorem~1: Existence of stable pairs ›
text‹
We proceed to define a function whose fixed points capture all stable
matches. \<^citet>‹‹I(B), p917› in "HatfieldMilgrom:2005"› provide the
following intuition:
\begin{quote}
The first theorem states that a set of contracts is stable if any
alternative contract would be rejected by some doctor or some hospital
from its suitably defined opportunity set. In the formulas below,
think of the doctors' opportunity set as @{term "XD"} and the
hospitals' opportunity set as @{term "XH"}. If @{term "X'"} is the
corresponding stable set, then @{term "XD"} must include, in addition
to @{term "X'"}, all contracts that would not be rejected by the
hospitals, and @{term "XH"} must similarly include @{term "X'"} and
all contracts that would not be rejected by the doctors. If @{term
"X'"} is stable, then every alternative contract is rejected by
somebody, so @{term "X = XH ∪ XD"} [where @{term "X"} is the
set of all contracts]. This logic is summarized in the first theorem.
\end{quote}
See also \<^citet>‹‹p6,\S4› in "Fleiner:2003"› and \<^citet>‹‹\S2› in "Fleiner:2002"›,
from whom we adopt the term @{emph ‹stable pair›}.
›
context Contracts
begin
definition stable_pair_on :: "'d set ⇒ 'x set × 'x set ⇒ bool" where
"stable_pair_on ds = (λ(XD, XH). XD = - RH XH ∧ XH = - RD_on ds XD)"
abbreviation stable_pair :: "'x set × 'x set ⇒ bool" where
"stable_pair ≡ stable_pair_on UNIV"
abbreviation match :: "'x set × 'x set ⇒ 'x set" where
"match X ≡ fst X ∩ snd X"
text ‹
\<^citet>‹‹Theorem~1› in "HatfieldMilgrom:2005"› state that every solution
@{term "(XD, XH)"} of @{const "stable_pair"} yields a stable match
@{term "XD ∩ XH"}, and conversely, i.e., every stable match is
the intersection of some stable pair. \<^citet>‹"AygunSonmez:2012-WP2"›
show that neither is the case without further restrictions on the
hospitals' choice functions @{term "Ch"}; we exhibit their
counterexample below.
Even so we can establish some properties in the present setting:
›
lemma stable_pair_on_CD_on:
assumes "stable_pair_on ds XD_XH"
shows "match XD_XH = CD_on ds (fst XD_XH)"
using %invisible assms CD_on_range unfolding stable_pair_on_def split_def fst_conv snd_conv
by blast
lemma stable_pair_on_CH:
assumes "stable_pair_on ds XD_XH"
shows "match XD_XH = CH (snd XD_XH)"
using %invisible assms CH_range unfolding stable_pair_on_def split_def fst_conv snd_conv
by blast
lemma stable_pair_on_CD_on_CH:
assumes "stable_pair_on ds XD_XH"
shows "CD_on ds (fst XD_XH) = CH (snd XD_XH)"
using %invisible assms stable_pair_on_CD_on stable_pair_on_CH by blast
lemma stable_pair_on_allocation:
assumes "stable_pair_on ds XD_XH"
shows "allocation (match XD_XH)"
unfolding %invisible stable_pair_on_CD_on[OF assms] by (rule CD_on_inj_on_Xd)
lemma stable_pair_onI:
assumes "fst XD_XH = - RH (snd XD_XH)"
assumes "snd XD_XH = - RD_on ds (fst XD_XH)"
shows "stable_pair_on ds XD_XH"
using assms unfolding stable_pair_on_def split_def by blast
lemma stable_pair_onE:
shows "⟦stable_pair_on ds XD_XH; ⟦- RH (snd XD_XH) = fst XD_XH; - RD_on ds (fst XD_XH) = snd XD_XH⟧ ⟹ P⟧ ⟹ P"
unfolding stable_pair_on_def split_def by blast
lemma stable_pair_on_Cd:
assumes "stable_pair_on ds XD_XH"
assumes "d ∈ ds"
shows "Cd d (fst XD_XH) = match XD_XH ∩ Field (Pd d)"
using stable_pair_on_CD_on[OF ‹stable_pair_on ds XD_XH›] CD_on_domain Cd_domain ‹d ∈ ds› by simp
lemma stable_pair_on_Cd_match:
assumes "stable_pair_on ds XD_XH"
assumes "d ∈ ds"
shows "Cd d (match XD_XH) = Cd d (fst XD_XH)"
using assms by (metis Cd_domain Cd_idem stable_pair_on_Cd)
lemma stable_pair_on_Xd:
assumes "stable_pair_on ds XD_XH"
assumes "x ∈ match XD_XH"
shows "Xd x ∈ ds"
using assms CD_on_Xd unfolding stable_pair_on_def split_def by blast
lemma stable_pair_on_match_Cd:
assumes "stable_pair_on ds XD_XH"
assumes "x ∈ match XD_XH"
shows "x ∈ Cd (Xd x) (match XD_XH)"
using assms by (metis (full_types) CD_on_def Cd_Xd UN_iff stable_pair_on_CD_on stable_pair_on_Cd_match)
text‹
We run out of steam on the following two lemmas, which are the
remaining requirements for stability.
›
lemma
assumes "stable_pair_on ds XD_XH"
shows "individually_rational_on ds (match XD_XH)"
oops
lemma
assumes "stable_pair_on ds XD_XH"
shows "stable_no_blocking (match XD_XH)"
oops
text‹
\<^citet>‹"HatfieldMilgrom:2005"› also claim that the converse holds:
›
lemma
assumes "stable_on ds X"
obtains XD_XH where "stable_pair_on ds XD_XH" and "X = match XD_XH"
oops
text‹
Again, the following counterexample shows that the @{const
substitutes} condition on @{term "Ch"} is too weak to guarantee
this. We show it holds under stronger assumptions in
\S\ref{sec:contracts-t1-converse}.
›
end
subsubsection‹ Theorem~1 does not hold \<^citep>‹"AygunSonmez:2012-WP2"› \label{sec:contracts-t1-counterexample} ›
text‹
The following counterexample, due to \<^citet>‹‹\S3:
Example~2› in "AygunSonmez:2012-WP2"›, comprehensively demonstrates that
\<^citet>‹‹Theorem~1› in "HatfieldMilgrom:2005"› does not hold.
We create three types: ‹D2› consists of two elements,
representing the doctors, and ‹H› is the type of the single
hospital. There are four contracts in the type ‹X4›.
›
datatype D2 = D1 | D2
datatype H1 = H