Theory May

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

(*<*)
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
(*>*)