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