# Theory May

(*
* May's Theorem, following Sen.
* (C)opyright Peter Gammie, peteg42 at gmail.com, commenced October 2008.
*)

(*<*)
theory May

imports SCFs

begin
(*>*)

section‹May's Theorem›

text ‹May's Theorem \<^cite>‹"May:1952"› provides a characterisation of
majority voting in terms of four conditions that appear quite natural for
\emph{a priori} unbiased social choice scenarios. It can be seen as a
refinement of some earlier work by Arrow \<^cite>‹‹Chapter V.1› in "Arrow:1963"›.

The following is a mechanisation of Sen's generalisation
\<^cite>‹‹Chapter~5*› in "Sen:70a"›; originally Arrow and May consider only two
alternatives, whereas Sen's model maps profiles of full RPRs to a possibly
intransitive relation that does at least generate a choice set that
satisfies May's conditions.›

subsection‹May's Conditions›

text ‹The condition of \emph{anonymity} asserts that the individuals'
identities are not considered by the choice rule. Rather than talk about
permutations we just assert the result of the SCF is the same when the
profile is composed with an arbitrary bijection on the set of
individuals.›

definition anonymous :: "('a, 'i) SCF ⇒ 'a set ⇒ 'i set ⇒ bool" where
"anonymous scf A Is ≡
(∀P f x y. profile A Is P ∧ bij_betw f Is Is ∧ x ∈ A ∧ y ∈ A
⟶ (x ⇘(scf P)⇙≼ y) = (x ⇘(scf (P ∘ f))⇙≼ y))"

lemma anonymousI[intro]:
"(⋀P f x y. ⟦ profile A Is P; bij_betw f Is Is;
x ∈ A; y ∈ A ⟧ ⟹ (x ⇘(scf P)⇙≼ y) = (x ⇘(scf (P ∘ f))⇙≼ y))
⟹ anonymous scf A Is"
unfolding anonymous_def by simp

lemma anonymousD:
"⟦ anonymous scf A Is; profile A Is P; bij_betw f Is Is; x ∈ A; y ∈ A ⟧
⟹ (x ⇘(scf P)⇙≼ y) = (x ⇘(scf (P ∘ f))⇙≼ y)"
unfolding anonymous_def by simp

text ‹Similarly, an SCF is \emph{neutral} if it is insensitive to the
identity of the alternatives. This is Sen's characterisation
\<^cite>‹‹p72› in "Sen:70a"›.›

definition neutral :: "('a, 'i) SCF ⇒ 'a set ⇒ 'i set ⇒ bool" where
"neutral scf A Is ≡
(∀P P' x y z w. profile A Is P ∧ profile A Is P' ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A ∧ w ∈ A
∧ (∀i ∈ Is. x ⇘(P i)⇙≼ y ⟷ z ⇘(P' i)⇙≼ w) ∧ (∀i ∈ Is. y ⇘(P i)⇙≼ x ⟷ w ⇘(P' i)⇙≼ z)
⟶ ((x ⇘(scf P)⇙≼ y ⟷ z ⇘(scf P')⇙≼ w) ∧ (y ⇘(scf P)⇙≼ x ⟷ w ⇘(scf P')⇙≼ z)))"

lemma neutralI[intro]:
"(⋀P P' x y z w.
⟦ profile A Is P; profile A Is P'; {x,y,z,w} ⊆ A;
⋀i. i ∈ Is ⟹ x ⇘(P i)⇙≼ y ⟷ z ⇘(P' i)⇙≼ w;
⋀i. i ∈ Is ⟹ y ⇘(P i)⇙≼ x ⟷ w ⇘(P' i)⇙≼ z ⟧
⟹ ((x ⇘(scf P)⇙≼ y ⟷ z ⇘(scf P')⇙≼ w) ∧ (y ⇘(scf P)⇙≼ x ⟷ w ⇘(scf P')⇙≼ z)))
⟹ neutral scf A Is"
unfolding neutral_def by simp

lemma neutralD:
"⟦ neutral scf A Is;
profile A Is P; profile A Is P'; {x,y,z,w} ⊆ A;
⋀i. i ∈ Is ⟹ x ⇘(P i)⇙≼ y ⟷ z ⇘(P' i)⇙≼ w;
⋀i. i ∈ Is ⟹ y ⇘(P i)⇙≼ x ⟷ w ⇘(P' i)⇙≼ z ⟧
⟹ (x ⇘(scf P)⇙≼ y ⟷ z ⇘(scf P')⇙≼ w) ∧ (y ⇘(scf P)⇙≼ x ⟷ w ⇘(scf P')⇙≼ z)"
unfolding neutral_def by simp

text ‹Neutrality implies independence of irrelevant alternatives.›

lemma neutral_iia: "neutral scf A Is ⟹ iia scf A Is"
unfolding neutral_def by (rule, auto)

text ‹\emph{Positive responsiveness} is a bit like non-manipulability: if
one individual improves their opinion of $x$, then the result should shift
in favour of $x$.›

definition positively_responsive :: "('a, 'i) SCF ⇒ 'a set ⇒ 'i set ⇒ bool" where
"positively_responsive scf A Is ≡
(∀P P' x y. profile A Is P ∧ profile A Is P' ∧ x ∈ A ∧ y ∈ A
∧ (∀i ∈ Is. (x ⇘(P i)⇙≺ y ⟶ x ⇘(P' i)⇙≺ y) ∧ (x ⇘(P i)⇙≈ y ⟶ x ⇘(P' i)⇙≼ y))
∧ (∃k ∈ Is. (x ⇘(P k)⇙≈ y ∧ x ⇘(P' k)⇙≺ y) ∨ (y ⇘(P k)⇙≺ x ∧ x ⇘(P' k)⇙≼ y))
⟶ x ⇘(scf P)⇙≼ y ⟶ x ⇘(scf P')⇙≺ y)"

lemma positively_responsiveI[intro]:
assumes I: "⋀P P' x y.
⟦ profile A Is P; profile A Is P'; x ∈ A; y ∈ A;
⋀i. ⟦ i ∈ Is; x ⇘(P i)⇙≺ y ⟧ ⟹ x ⇘(P' i)⇙≺ y;
⋀i. ⟦ i ∈ Is; x ⇘(P i)⇙≈ y ⟧ ⟹ x ⇘(P' i)⇙≼ y;
∃k ∈ Is. (x ⇘(P k)⇙≈ y ∧ x ⇘(P' k)⇙≺ y) ∨ (y ⇘(P k)⇙≺ x ∧ x ⇘(P' k)⇙≼ y);
x ⇘(scf P)⇙≼ y ⟧
⟹ x ⇘(scf P')⇙≺ y"
shows "positively_responsive scf A Is"
unfolding positively_responsive_def
by (blast intro: I)

lemma positively_responsiveD:
"⟦ positively_responsive scf A Is;
profile A Is P; profile A Is P'; x ∈ A; y ∈ A;
⋀i. ⟦ i ∈ Is; x ⇘(P i)⇙≺ y ⟧ ⟹ x ⇘(P' i)⇙≺ y;
⋀i. ⟦ i ∈ Is; x ⇘(P i)⇙≈ y ⟧ ⟹ x ⇘(P' i)⇙≼ y;
∃k ∈ Is. (x ⇘(P k)⇙≈ y ∧ x ⇘(P' k)⇙≺ y) ∨ (y ⇘(P k)⇙≺ x ∧ x ⇘(P' k)⇙≼ y);
x ⇘(scf P)⇙≼ y ⟧
⟹ x ⇘(scf P')⇙≺ y"
unfolding positively_responsive_def
apply clarsimp
apply (erule allE[where x=P])
apply (erule allE[where x=P'])
apply (erule allE[where x=x])
apply (erule allE[where x=y])
by auto

subsection‹The Method of Majority Decision satisfies May's conditions›

text ‹The \emph{method of majority decision} (MMD) says that if the number
of individuals who strictly prefer $x$ to $y$ is larger than or equal to
those who strictly prefer the converse, then $x\ R\ y$. Note that this
definition only makes sense for a finite population.›

definition MMD :: "'i set ⇒ ('a, 'i) SCF" where
"MMD Is P ≡ { (x, y) . card { i ∈ Is. x ⇘(P i)⇙≺ y } ≥ card { i ∈ Is. y ⇘(P i)⇙≺ x } }"

text ‹The first part of May's Theorem establishes that the conditions are
consistent, by showing that they are satisfied by MMD.›

lemma MMD_l2r:
fixes A :: "'a set"
and Is :: "'i set"
assumes finiteIs: "finite Is"
shows "SCF (MMD Is) A Is universal_domain"
and "anonymous (MMD Is) A Is"
and "neutral (MMD Is) A Is"
and "positively_responsive (MMD Is) A Is"
proof -
show "SCF (MMD Is) A Is universal_domain"
proof
fix P show "complete A (MMD Is P)"
by (rule completeI, unfold MMD_def, simp, arith)
qed
show "anonymous (MMD Is) A Is"
proof
fix P
fix x y :: "'a"
fix f assume bijf: "bij_betw f Is Is"
show "(x ⇘(MMD Is P)⇙≼ y) = (x ⇘(MMD Is (P ∘ f))⇙≼ y)"
using card_compose_bij[OF bijf, where P="λi. x ⇘(P i)⇙≺ y"]
card_compose_bij[OF bijf, where P="λi. y ⇘(P i)⇙≺ x"]
unfolding MMD_def by simp
qed
next
show "neutral (MMD Is) A Is"
proof
fix P P'
fix x y z w assume xyzwA: "{x,y,z,w} ⊆ A"
assume xyzw: "⋀i. i ∈ Is ⟹ (x ⇘(P i)⇙≼ y) = (z ⇘(P' i)⇙≼ w)"
and yxwz: "⋀i. i ∈ Is ⟹ (y ⇘(P i)⇙≼ x) = (w ⇘(P' i)⇙≼ z)"
from xyzwA xyzw yxwz
have "{ i ∈ Is. x ⇘(P i)⇙≺ y } = { i ∈ Is. z ⇘(P' i)⇙≺ w }"
and "{ i ∈ Is. y ⇘(P i)⇙≺ x } = { i ∈ Is. w ⇘(P' i)⇙≺ z }"
unfolding strict_pref_def by auto
thus "(x ⇘(MMD Is P)⇙≼ y) = (z ⇘(MMD Is P')⇙≼ w) ∧
(y ⇘(MMD Is P)⇙≼ x) = (w ⇘(MMD Is P')⇙≼ z)"
unfolding MMD_def by simp
qed
next
show "positively_responsive (MMD Is) A Is"
proof
fix P P' assume profileP: "profile A Is P"
fix x y assume xyA: "x ∈ A" "y ∈ A"
assume xPy: "⋀i. ⟦i ∈ Is; x ⇘(P i)⇙≺ y⟧ ⟹ x ⇘(P' i)⇙≺ y"
and xIy: "⋀i. ⟦i ∈ Is; x ⇘(P i)⇙≈ y⟧ ⟹ x ⇘(P' i)⇙≼ y"
and k: "∃k∈Is. x ⇘(P k)⇙≈ y ∧ x ⇘(P' k)⇙≺ y ∨ y ⇘(P k)⇙≺ x ∧ x ⇘(P' k)⇙≼ y"
and xRSCFy: "x ⇘(MMD Is P)⇙≼ y"
from k obtain k
where kIs: "k ∈ Is"
and kcond: "(x ⇘(P k)⇙≈ y ∧ x ⇘(P' k)⇙≺ y) ∨ (y ⇘(P k)⇙≺ x ∧ x ⇘(P' k)⇙≼ y)"
by blast
let ?xPy = "{ i ∈ Is. x ⇘(P i)⇙≺ y }"
let ?xP'y = "{ i ∈ Is. x ⇘(P' i)⇙≺ y }"
let ?yPx = "{ i ∈ Is. y ⇘(P i)⇙≺ x }"
let ?yP'x = "{ i ∈ Is. y ⇘(P' i)⇙≺ x }"
from profileP xyA xPy xIy have yP'xyPx: "?yP'x ⊆ ?yPx"
unfolding strict_pref_def indifferent_pref_def
by (blast dest: rpr_complete)
with finiteIs have yP'xyPxC: "card ?yP'x ≤ card ?yPx"
by (blast intro: card_mono finite_subset)
from finiteIs xPy have xPyxP'yC: "card ?xPy ≤ card ?xP'y"
by (blast intro: card_mono finite_subset)
show "x ⇘(MMD Is P')⇙≺ y"
proof
from xRSCFy xPyxP'yC yP'xyPxC show "x ⇘(MMD Is P')⇙≼ y"
unfolding MMD_def by auto
next
{
assume xIky: "x ⇘(P k)⇙≈ y" and xP'ky: "x ⇘(P' k)⇙≺ y"
have "card ?xPy < card ?xP'y"
proof -
from xIky have knP: "k ∉ ?xPy"
unfolding indifferent_pref_def strict_pref_def by blast
from kIs xP'ky have kP': "k ∈ ?xP'y" by simp
from finiteIs xPy knP kP' show ?thesis
by (blast intro: psubset_card_mono finite_subset)
qed
with xRSCFy yP'xyPxC have "card ?yP'x < card ?xP'y"
unfolding MMD_def by auto
}
moreover
{
assume yPkx: "y ⇘(P k)⇙≺ x" and xR'ky: "x ⇘(P' k)⇙≼ y"
have "card ?yP'x < card ?yPx"
proof -
from kIs yPkx have kP: "k ∈ ?yPx" by simp
from kIs xR'ky have knP': "k ∉ ?yP'x"
unfolding strict_pref_def by blast
from yP'xyPx kP knP' have "?yP'x ⊂ ?yPx" by blast
with finiteIs show ?thesis
by (blast intro: psubset_card_mono finite_subset)
qed
with xRSCFy xPyxP'yC have "card ?yP'x < card ?xP'y"
unfolding MMD_def by auto
}
moreover note kcond
ultimately show "¬(y ⇘(MMD Is P')⇙≼ x)"
unfolding MMD_def by auto
qed
qed
qed

subsection‹Everything satisfying May's conditions is the Method of Majority Decision›

text‹Now show that MMD is the only SCF that satisfies these conditions.›

text ‹Firstly develop some theory about exchanging alternatives $x$ and
$y$ in profile $P$.›

definition swapAlts :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where
"swapAlts a b u ≡ if u = a then b else if u = b then a else u"

lemma swapAlts_in_set_iff: "{a, b} ⊆ A ⟹ swapAlts a b u ∈ A ⟷ u ∈ A"
unfolding swapAlts_def by (simp split: if_split)

definition swapAltsP :: "('a, 'i) Profile ⇒ 'a ⇒ 'a ⇒ ('a, 'i) Profile" where
"swapAltsP P a b ≡ (λi. { (u, v) . (swapAlts a b u, swapAlts a b v) ∈ P i })"

lemma swapAltsP_ab: "a ⇘(P i)⇙≼ b ⟷ b ⇘(swapAltsP P a b i)⇙≼ a" "b ⇘(P i)⇙≼ a ⟷ a ⇘(swapAltsP P a b i)⇙≼ b"
unfolding swapAltsP_def swapAlts_def by simp_all

lemma profile_swapAltsP:
assumes profileP: "profile A Is P"
and abA: "{a,b} ⊆ A"
shows "profile A Is (swapAltsP P a b)"
proof(rule profileI)
from profileP show "Is ≠ {}" by (rule profile_non_empty)
next
fix i assume iIs: "i ∈ Is"
show "rpr A (swapAltsP P a b i)"
proof(rule rprI)
show "refl_on A (swapAltsP P a b i)"
proof(rule refl_onI)
from profileP iIs abA show "swapAltsP P a b i ⊆ A × A"
unfolding swapAltsP_def by (blast dest: swapAlts_in_set_iff)
from profileP iIs abA show "⋀x. x ∈ A ⟹ x ⇘(swapAltsP P a b i)⇙≼ x"
unfolding swapAltsP_def swapAlts_def by auto
qed
next
from profileP iIs abA show "complete A (swapAltsP P a b i)"
unfolding swapAltsP_def
by - (rule completeI, simp, rule rpr_complete[where A=A],
auto iff: swapAlts_in_set_iff)
next
from profileP iIs show "trans (swapAltsP P a b i)"
unfolding swapAltsP_def by (blast dest: rpr_le_trans intro: transI)
qed
qed

lemma profile_bij_profile:
assumes profileP: "profile A Is P"
and bijf: "bij_betw f Is Is"
shows "profile A Is (P ∘ f)"
using bij_betw_onto[OF bijf] profileP
by - (rule, auto dest: profile_non_empty)

text‹The locale keeps the conditions in scope for the next few
lemmas. Note how weak the constraints on the sets of alternatives and
individuals are; clearly there needs to be at least two alternatives and two
individuals for conflict to occur, but it is pleasant that the proof
uniformly handles the degenerate cases.›

locale May =
fixes A :: "'a set"

fixes Is :: "'i set"
assumes finiteIs: "finite Is"

fixes scf :: "('a, 'i) SCF"
assumes SCF: "SCF scf A Is universal_domain"
and anonymous: "anonymous scf A Is"
and neutral: "neutral scf A Is"
and positively_responsive: "positively_responsive scf A Is"
begin

text‹Anonymity implies that, for any pair of alternatives, the social
choice rule can only depend on the number of individuals who express any
given preference between them. Note we also need @{term "iia"}, implied by
neutrality, to restrict attention to alternatives $x$ and $y$.›

lemma anonymous_card:
assumes profileP: "profile A Is P"
and profileP': "profile A Is P'"
and xyA: "hasw [x,y] A"
and xytally: "card { i ∈ Is. x ⇘(P i)⇙≺ y } = card { i ∈ Is. x ⇘(P' i)⇙≺ y }"
and yxtally: "card { i ∈ Is. y ⇘(P i)⇙≺ x } = card { i ∈ Is. y ⇘(P' i)⇙≺ x }"
shows "x ⇘(scf P)⇙≼ y ⟷ x ⇘(scf P')⇙≼ y"
proof -
let ?xPy = "{ i ∈ Is. x ⇘(P i)⇙≺ y }"
let ?xP'y = "{ i ∈ Is. x ⇘(P' i)⇙≺ y }"
let ?yPx = "{ i ∈ Is. y ⇘(P i)⇙≺ x }"
let ?yP'x = "{ i ∈ Is. y ⇘(P' i)⇙≺ x }"
have disjPxy: "(?xPy ∪ ?yPx) - ?xPy = ?yPx"
unfolding strict_pref_def by blast
have disjP'xy: "(?xP'y ∪ ?yP'x) - ?xP'y = ?yP'x"
unfolding strict_pref_def by blast
from finiteIs xytally
obtain f where bijf: "bij_betw f ?xPy ?xP'y"
by - (drule card_eq_bij, auto)
from finiteIs yxtally
obtain g where bijg: "bij_betw g ?yPx ?yP'x"
by - (drule card_eq_bij, auto)
from bijf bijg disjPxy disjP'xy
obtain h
where bijh: "bij_betw h (?xPy ∪ ?yPx) (?xP'y ∪ ?yP'x)"
and hf: "⋀j. j ∈ ?xPy ⟹ h j = f j"
and hg: "⋀j. j ∈ (?xPy ∪ ?yPx) - ?xPy ⟹ h j = g j"
using bij_combine[where f=f and g=g and A="?xPy" and B ="?xPy ∪ ?yPx" and C="?xP'y" and D="?xP'y ∪ ?yP'x"]
by auto
from bijh finiteIs
obtain h' where bijh': "bij_betw h' Is Is"
and hh': "⋀j. j ∈ (?xPy ∪ ?yPx) ⟹ h' j = h j"
and hrest: "⋀j. j ∈ Is - (?xPy ∪ ?yPx) ⟹ h' j ∈ Is - (?xP'y ∪ ?yP'x)"
by - (drule bij_complete, auto)
from neutral_iia[OF neutral]
have "x ⇘(scf (P' ∘ h'))⇙≼ y ⟷ x ⇘(scf P)⇙≼ y"
proof(rule iiaE)
from xyA show "{x, y} ⊆ A" by simp
next
fix i assume iIs: "i ∈ Is"
fix a b assume ab: "a ∈ {x, y}" "b ∈ {x, y}"
from profileP iIs have completePi: "complete A (P i)" by (auto dest: rprD)
from completePi xyA
show "(a ⇘(P i)⇙≼ b) ⟷ (a ⇘((P' ∘ h') i)⇙≼ b)"
proof(cases rule: complete_exh)
case xPy with profileP profileP' xyA iIs ab hh' hf bijf show ?thesis
unfolding strict_pref_def bij_betw_def by (simp, blast)
next
case yPx with profileP profileP' xyA iIs ab hh' hg bijg show ?thesis
unfolding strict_pref_def bij_betw_def by (simp, blast)
next
case xIy with profileP profileP' xyA iIs ab hrest[where j=i] show ?thesis
unfolding indifferent_pref_def strict_pref_def bij_betw_def
by (simp, blast dest: rpr_complete)
qed
qed (simp_all add: profileP profile_bij_profile[OF profileP' bijh'])
moreover
from anonymousD[OF anonymous profileP' bijh'] xyA
have "x ⇘(scf P')⇙≼ y ⟷ x ⇘(scf (P' ∘ h'))⇙≼ y" by simp
ultimately show ?thesis by simp
qed

text ‹Using the previous result and neutrality, it must be the case that
if the tallies are tied for alternatives $x$ and $y$ then the social choice
function is indifferent between those two alternatives.›

lemma anonymous_neutral_indifference:
assumes profileP: "profile A Is P"
and xyA: "hasw [x,y] A"
and tallyP: "card { i ∈ Is. x ⇘(P i)⇙≺ y } = card { i ∈ Is. y ⇘(P i)⇙≺ x }"
shows "x ⇘(scf P)⇙≈ y"
proof -
― ‹Neutrality insists the results for @{term "P"} are symmetrical to those for @{term "swapAltsP P"}.›
from xyA
have symPP': "(x ⇘(scf P)⇙≼ y ⟷ y ⇘(scf (swapAltsP P x y))⇙≼ x)
∧ (y ⇘(scf P)⇙≼ x ⟷ x ⇘(scf (swapAltsP P x y))⇙≼ y)"
by - (rule neutralD[OF neutral profileP profile_swapAltsP[OF profileP]],
simp_all, (rule swapAltsP_ab)+)
― ‹Anonymity and neutrality insist the results for @{term "P"} are identical to those for @{term "swapAltsP P"}.›
from xyA tallyP have "card {i ∈ Is. x ⇘(P i)⇙≺ y} = card { i ∈ Is. x ⇘(swapAltsP P x y i)⇙≺ y }"
and "card {i ∈ Is. y ⇘(P i)⇙≺ x} = card { i ∈ Is. y ⇘(swapAltsP P x y i)⇙≺ x }"
unfolding swapAltsP_def swapAlts_def strict_pref_def by simp_all
with profileP xyA have idPP': "x ⇘(scf P)⇙≼ y ⟷ x ⇘(scf (swapAltsP P x y))⇙≼ y"
and "y ⇘(scf P)⇙≼ x ⟷ y ⇘(scf (swapAltsP P x y))⇙≼ x"
by - (rule anonymous_card[OF profileP profile_swapAltsP], clarsimp+)+
from xyA SCF_completeD[OF SCF] profileP symPP' idPP' show "x ⇘(scf P)⇙≈ y" by (simp, blast)
qed

text‹Finally, if the tallies are not equal then the social choice function
must lean towards the one with the higher count due to positive
responsiveness.›

lemma positively_responsive_prefer_witness:
assumes profileP: "profile A Is P"
and xyA: "hasw [x,y] A"
and tallyP: "card { i ∈ Is. x ⇘(P i)⇙≺ y } > card { i ∈ Is. y ⇘(P i)⇙≺ x }"
obtains P' k
where "profile A Is P'"
and "⋀i. ⟦i ∈ Is; x ⇘(P' i)⇙≺ y⟧ ⟹ x ⇘(P i)⇙≺ y"
and "⋀i. ⟦i ∈ Is; x ⇘(P' i)⇙≈ y⟧ ⟹ x ⇘(P i)⇙≼ y"
and "k ∈ Is ∧ x ⇘(P' k)⇙≈ y ∧ x ⇘(P k)⇙≺ y"
and "card { i ∈ Is. x ⇘(P' i)⇙≺ y } = card { i ∈ Is. y ⇘(P' i)⇙≺ x }"
proof -
from tallyP obtain C
where tallyP': "card ({ i ∈ Is. x ⇘(P i)⇙≺ y } - C) = card { i ∈ Is. y ⇘(P i)⇙≺ x }"
and C: "C ≠ {}" "C ⊆ Is"
and CxPy: "C ⊆ { i ∈ Is. x ⇘(P i)⇙≺ y }"
by - (drule card_greater[OF finiteIs], auto)
― ‹Add $(b, a)$ and close under transitivity.›
let ?P' = "λi. if i ∈ C
then P i ∪ { (y, x) }
∪ { (y, u) |u. x ⇘(P i)⇙≼ u }
∪ { (u, x) |u. u ⇘(P i)⇙≼ y }
∪ { (v, u) |u v. x ⇘(P i)⇙≼ u ∧ v ⇘(P i)⇙≼ y }
else P i"
have "profile A Is ?P'"
proof
fix i assume iIs: "i ∈ Is"
show "rpr A (?P' i)"
proof
from profileP iIs show "complete A (?P' i)"
unfolding complete_def by (simp, blast dest: rpr_complete)
from profileP iIs xyA show "refl_on A (?P' i)"
by - (rule refl_onI, auto)
show "trans (?P' i)"
proof(cases "i ∈ C")
case False with profileP iIs show ?thesis
by (simp, blast dest: rpr_le_trans intro: transI)
next
case True with profileP iIs C CxPy xyA show ?thesis
unfolding strict_pref_def
by - (rule transI, simp, blast dest: rpr_le_trans rpr_complete)
qed
qed
next
from C show "Is ≠ {}" by blast
qed
moreover
have "⋀i. ⟦ i ∈ Is; x ⇘(?P' i)⇙≺ y ⟧ ⟹ x ⇘(P i)⇙≺ y"
unfolding strict_pref_def by (simp split: if_split_asm)
moreover
from profileP C xyA
have "⋀i. ⟦i ∈ Is; x ⇘(?P' i)⇙≈ y⟧ ⟹ x ⇘(P i)⇙≼ y"
unfolding indifferent_pref_def by (simp split: if_split_asm)
moreover
from C CxPy obtain k where kC: "k ∈ C" and xPky: "x ⇘(P k)⇙≺ y" by blast
hence "x ⇘(?P' k)⇙≈ y" by auto
with C kC xPky have "k ∈ Is ∧ x ⇘(?P' k)⇙≈ y ∧ x ⇘(P k)⇙≺ y" by blast
moreover
have "card { i ∈ Is. x ⇘(?P' i)⇙≺ y } = card { i ∈ Is. y ⇘(?P' i)⇙≺ x }"
proof -
have "{ i ∈ Is. x ⇘(?P' i)⇙≺ y } = { i ∈ Is. x ⇘(?P' i)⇙≺ y } - C"
proof -
from C have "⋀i. ⟦ i ∈ Is; x ⇘(?P' i)⇙≺ y ⟧ ⟹ i ∈ Is - C"
unfolding indifferent_pref_def strict_pref_def by auto
thus ?thesis by blast
qed
also have "… = { i ∈ Is. x ⇘(P i)⇙≺ y } - C" by auto
finally have "card { i ∈ Is. x ⇘(?P' i)⇙≺ y } = card ({ i ∈ Is. x ⇘(P i)⇙≺ y } - C)"
by simp
with tallyP' have "card { i ∈ Is. x ⇘(?P' i)⇙≺ y } = card { i ∈ Is. y ⇘(P i)⇙≺ x }"
by simp
also have "… = card { i ∈ Is. y ⇘(?P' i)⇙≺ x }" (is "card ?lhs = card ?rhs")
proof -
from profileP xyA have "⋀i. ⟦ i ∈ Is; y ⇘(?P' i)⇙≺ x ⟧ ⟹ y ⇘(P i)⇙≺ x"
unfolding strict_pref_def by (simp split: if_split_asm, blast dest: rpr_complete)
hence "?rhs ⊆ ?lhs" by blast
moreover
from profileP xyA have "⋀i. ⟦ i ∈ Is; y ⇘(P i)⇙≺ x ⟧ ⟹ y ⇘(?P' i)⇙≺ x"
unfolding strict_pref_def by simp
hence "?lhs ⊆ ?rhs" by blast
ultimately show ?thesis by simp
qed
finally show ?thesis .
qed
ultimately show thesis ..
qed

lemma positively_responsive_prefer:
assumes profileP: "profile A Is P"
and xyA: "hasw [x,y] A"
and tallyP: "card { i ∈ Is. x ⇘(P i)⇙≺ y } > card { i ∈ Is. y ⇘(P i)⇙≺ x }"
shows "x ⇘(scf P)⇙≺ y"
proof -
from assms obtain P' k
where profileP': "profile A Is P'"
and F: "⋀i. ⟦i ∈ Is; x ⇘(P' i)⇙≺ y⟧ ⟹ x ⇘(P i)⇙≺ y"
and G: "⋀i. ⟦i ∈ Is; x ⇘(P' i)⇙≈ y⟧ ⟹ x ⇘(P i)⇙≼ y"
and pivot: "k ∈ Is ∧ x ⇘(P' k)⇙≈ y ∧ x ⇘(P k)⇙≺ y"
and cardP': "card { i ∈ Is. x ⇘(P' i)⇙≺ y } = card { i ∈ Is. y ⇘(P' i)⇙≺ x }"
by - (drule positively_responsive_prefer_witness, auto)
from profileP' xyA cardP' have "x ⇘(scf P')⇙≈ y"
by - (rule anonymous_neutral_indifference, auto)
with xyA F G pivot show ?thesis
by - (rule positively_responsiveD[OF positively_responsive profileP' profileP], auto)
qed

lemma MMD_r2l:
assumes profileP: "profile A Is P"
and xyA: "hasw [x,y] A"
shows "x ⇘(scf P)⇙≼ y ⟷ x ⇘(MMD Is P)⇙≼ y"
proof(cases rule: linorder_cases)
assume "card { i ∈ Is. x ⇘(P i)⇙≺ y } = card { i ∈ Is. y ⇘(P i)⇙≺ x }"
with profileP xyA show ?thesis
using anonymous_neutral_indifference
unfolding indifferent_pref_def MMD_def by simp
next
assume "card { i ∈ Is. x ⇘(P i)⇙≺ y } > card { i ∈ Is. y ⇘(P i)⇙≺ x }"
with profileP xyA show ?thesis
using positively_responsive_prefer
unfolding strict_pref_def MMD_def by simp
next
assume "card { i ∈ Is. x ⇘(P i)⇙≺ y } < card { i ∈ Is. y ⇘(P i)⇙≺ x }"
with profileP xyA show ?thesis
using positively_responsive_prefer
unfolding strict_pref_def MMD_def by clarsimp
qed

end

text‹May's original paper \<^cite>‹"May:1952"› goes on to show that the
conditions are independent by exhibiting choice rules that differ from
@{term "MMD"} and satisfy the conditions remaining after any particular one
is removed. I leave this to future work.

May also wrote a later article \<^cite>‹"May:1953"› where he shows that the
conditions are completely independent, i.e. for every partition of the
conditions into two sets, there is a voting rule that satisfies one and not
the other.

There are many later papers that characterise MMD with different sets of
conditions.

›

subsection‹The Plurality Rule›

text‹Goodin and List \<^cite>‹"GoodinList:2006"› show that May's original
result can be generalised to characterise plurality voting. The following
shows that this result is a short step from Sen's much earlier
generalisation.

\emph{Plurality voting} is a choice function that returns the alternative
that receives the most votes, or the set of such alternatives in the case of
a tie. Profiles are restricted to those where each individual casts a vote
in favour of a single alternative.›

type_synonym ('a, 'i) SVProfile = "'i ⇒ 'a"

definition svprofile :: "'a set ⇒ 'i set ⇒ ('a, 'i) SVProfile ⇒ bool" where
"svprofile A Is F ≡ Is ≠ {} ∧ F  Is ⊆ A"

definition plurality_rule :: "'a set ⇒ 'i set ⇒ ('a, 'i) SVProfile ⇒ 'a set" where
"plurality_rule A Is F
≡ { x ∈ A . ∀y ∈ A. card { i ∈ Is . F i = x } ≥ card { i ∈ Is . F i = y } }"

text‹By translating single-vote profiles into RPRs in the obvious way, the
choice function arising from @{term "MMD"} coincides with traditional
plurality voting.›

definition MMD_plurality_rule :: "'a set ⇒ 'i set ⇒ ('a, 'i) Profile ⇒ 'a set" where
"MMD_plurality_rule A Is P ≡ choiceSet A (MMD Is P)"

definition single_vote_to_RPR :: "'a set ⇒ 'a ⇒ 'a RPR" where
"single_vote_to_RPR A a ≡ { (a, x) |x. x ∈ A } ∪ (A - {a}) × (A - {a})"

lemma single_vote_to_RPR_iff:
"⟦ a ∈ A; x ∈ A; a ≠ x ⟧ ⟹ (a ⇘(single_vote_to_RPR A b)⇙≺ x) ⟷ (b = a)"
unfolding single_vote_to_RPR_def strict_pref_def by auto

lemma plurality_rule_equiv:
"plurality_rule A Is F = MMD_plurality_rule A Is (single_vote_to_RPR A ∘ F)"
proof -
{
fix x y
have "⟦ x ∈ A; y ∈ A ⟧ ⟹
(card {i ∈ Is. F i = y} ≤ card {i ∈ Is. F i = x}) =
(card {i ∈ Is. y ⇘(single_vote_to_RPR A (F i))⇙≺ x}
≤ card {i ∈ Is. x ⇘(single_vote_to_RPR A (F i))⇙≺ y})"
by (cases "x=y", auto iff: single_vote_to_RPR_iff)
}
thus ?thesis
unfolding plurality_rule_def MMD_plurality_rule_def choiceSet_def MMD_def
by auto
qed

text‹Thus it is clear that Sen's generalisation of May's result applies to
this case as well.

Their paper goes on to show how strengthening the anonymity condition gives
rise to a characterisation of approval voting that strictly generalises
May's original theorem. As this requires some rearrangement of the proof I
leave it to future work.›

(*<*)
end
(*>*)
`