# Theory Social_Choice_Functions

(*
Title:    Social_Choice_Functions.thy
Author:   Manuel Eberl, TU München

Definitions of Social Choice Functions, their properties, and related concepts
*)

section ‹Social Choice Functions›

theory Social_Choice_Functions
imports
"Randomised_Social_Choice.Preference_Profile_Cmd"
begin

subsection ‹Weighted majority graphs›

definition supporters :: "('agent, 'alt) pref_profile ⇒ 'alt ⇒ 'alt ⇒ 'agent set" where
supporters_auxdef: "supporters R x y = {i. x ≽[R i] y}"

definition weighted_majority :: "('agent, 'alt) pref_profile ⇒ 'alt ⇒ 'alt ⇒ int" where
"weighted_majority R x y = int (card (supporters R x y)) - int (card (supporters R y x))"

lemma weighted_majority_refl [simp]: "weighted_majority R x x = 0"

lemma weighted_majority_swap: "weighted_majority R x y = -weighted_majority R y x"

lemma eval_set_filter:
"Set.filter P {} = {}"
"P x ⟹ Set.filter P (insert x A) = insert x (Set.filter P A)"
"¬P x ⟹ Set.filter P (insert x A) = Set.filter P A"
unfolding Set.filter_def by auto

context election
begin

lemma supporters_def:
assumes "is_pref_profile R"
shows   "supporters R x y = {i∈agents. x ≽[R i] y}"
proof -
interpret pref_profile_wf agents alts R by fact
show ?thesis using not_outside unfolding supporters_auxdef by blast
qed

lemma supporters_nonagent1:
assumes "is_pref_profile R" "x ∉ alts"
shows   "supporters R x y = {}"
proof -
interpret pref_profile_wf agents alts R by fact
from assms show ?thesis by (auto simp: supporters_def dest: not_outside)
qed

lemma supporters_nonagent2:
assumes "is_pref_profile R" "y ∉ alts"
shows   "supporters R x y = {}"
proof -
interpret pref_profile_wf agents alts R by fact
from assms show ?thesis by (auto simp: supporters_def dest: not_outside)
qed

lemma weighted_majority_nonagent1:
assumes "is_pref_profile R" "x ∉ alts"
shows   "weighted_majority R x y = 0"
using assms by (simp add: weighted_majority_def supporters_nonagent1 supporters_nonagent2)

lemma weighted_majority_nonagent2:
assumes "is_pref_profile R" "y ∉ alts"
shows   "weighted_majority R x y = 0"
using assms by (simp add: weighted_majority_def supporters_nonagent1 supporters_nonagent2)

lemma weighted_majority_eq_iff:
assumes "is_pref_profile R1" "is_pref_profile R2"
shows   "weighted_majority R1 = weighted_majority R2 ⟷
(∀x∈alts. ∀y∈alts. weighted_majority R1 x y = weighted_majority R2 x y)"
proof (intro iffI ext)
fix x y :: 'alt
assume "∀x∈alts. ∀y∈alts. weighted_majority R1 x y = weighted_majority R2 x y"
with assms show "weighted_majority R1 x y = weighted_majority R2 x y"
by (cases "x ∈ alts"; cases "y ∈ alts")
(auto simp: fun_eq_iff weighted_majority_nonagent1 weighted_majority_nonagent2)
qed auto

end

subsection ‹Definition of Social Choice Functions›

locale social_choice_function = election agents alts
for agents :: "'agent set" and alts :: "'alt set" +
fixes scf :: "('agent, 'alt) pref_profile ⇒ 'alt set"
assumes scf_nonempty: "is_pref_profile R ⟹ scf R ≠ {}"
assumes scf_alts: "is_pref_profile R ⟹ scf R ⊆ alts"

subsection ‹Anonymity›

text ‹
An SCF is anonymous if permuting the agents in the input does not change the result.
›
locale anonymous_scf = social_choice_function agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
assumes anonymous: "π permutes agents ⟹ is_pref_profile R ⟹ scf (R ∘ π) = scf R"
begin

lemma anonymous':
assumes "anonymous_profile R1 = anonymous_profile R2"
assumes "is_pref_profile R1" "is_pref_profile R2"
shows   "scf R1 = scf R2"
proof -
from anonymous_profile_agent_permutation[OF assms finite_agents]
obtain π where "π permutes agents" "R1 = R2 ∘ π" by blast
with anonymous[of π R2] assms show ?thesis by simp
qed

lemma anonymity_prefs_from_table:
assumes "prefs_from_table_wf agents alts xs" "prefs_from_table_wf agents alts ys"
assumes "mset (map snd xs) = mset (map snd ys)"
shows   "scf (prefs_from_table xs) = scf (prefs_from_table ys)"
proof -
from prefs_from_table_agent_permutation[OF assms] guess π .
with anonymous[of π, of "prefs_from_table xs"] assms(1) show ?thesis
qed

context
begin
qualified lemma anonymity_prefs_from_table_aux:
assumes "R1 = prefs_from_table xs" "prefs_from_table_wf agents alts xs"
assumes "R2 = prefs_from_table ys" "prefs_from_table_wf agents alts ys"
assumes "mset (map snd xs) = mset (map snd ys)"
shows   "scf R1 = scf R2" unfolding assms(1,3)
by (rule anonymity_prefs_from_table) (simp_all add: assms del: mset_map)
end

end

subsection ‹Neutrality›

text ‹
An SCF is neutral if permuting the alternatives in the input does not change the
result, modulo the equivalent permutation in the output lottery.
›
locale neutral_scf = social_choice_function agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
assumes neutral: "σ permutes alts ⟹ is_pref_profile R ⟹
scf (permute_profile σ R) = σ  scf R"
begin

text ‹
Alternative formulation of neutrality that shows that our definition is
equivalent to that in the paper.
›
lemma neutral':
assumes "σ permutes alts"
assumes "is_pref_profile R"
assumes "a ∈ alts"
shows   "σ a ∈ scf (permute_profile σ R) ⟷ a ∈ scf R"
proof -
have *: "x = y" if "σ x = σ y" for x y
using permutes_inj[OF assms(1)] that by (auto dest: injD)
from assms show ?thesis by (auto simp: neutral dest!: *)
qed

end

locale an_scf =
anonymous_scf agents alts scf + neutral_scf agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf
begin

lemma scf_anonymous_neutral:
assumes perm: "σ permutes alts" and wf: "is_pref_profile R1" "is_pref_profile R2"
assumes eq: "anonymous_profile R1 =
image_mset (map (λA. σ  A)) (anonymous_profile R2)"
shows   "scf R1 = σ  scf R2"
proof -
interpret R1: pref_profile_wf agents alts R1 by fact
interpret R2: pref_profile_wf agents alts R2 by fact
from perm have wf': "is_pref_profile (permute_profile σ R2)"
by (rule R2.wf_permute_alts)
from eq perm have "anonymous_profile R1 = anonymous_profile (permute_profile σ R2)"
from anonymous_profile_agent_permutation[OF this wf(1) wf']
obtain π where "π permutes agents" "permute_profile σ R2 ∘ π = R1" by auto
have "scf (permute_profile σ R2 ∘ π) = scf (permute_profile σ R2)"
by (rule anonymous) fact+
also have "… = σ  scf R2"
by (rule neutral) fact+
also have "permute_profile σ R2 ∘ π = R1" by fact
finally show ?thesis .
qed

lemma scf_anonymous_neutral':
assumes perm: "σ permutes alts" and wf: "is_pref_profile R1" "is_pref_profile R2"
assumes eq: "anonymous_profile R1 =
image_mset (map (λA. σ  A)) (anonymous_profile R2)"
shows   "σ x ∈ scf R1 ⟷ x ∈ scf R2"
proof -
have "scf R1 = σ  scf R2" by (intro scf_anonymous_neutral) fact+
also have "σ x ∈ … ⟷ x ∈ scf R2"
by (blast dest: injD[OF permutes_inj[OF perm]])
finally show ?thesis .
qed

lemma scf_automorphism:
assumes perm: "σ permutes alts" and wf: "is_pref_profile R"
assumes eq: "image_mset (map (λA. σ  A)) (anonymous_profile R) = anonymous_profile R"
shows   "σ  scf R = scf R"
using scf_anonymous_neutral[OF perm wf wf eq [symmetric]] ..

end

lemma an_scf_automorphism_aux:
assumes wf: "prefs_from_table_wf agents alts yss" "R ≡ prefs_from_table yss"
assumes an: "an_scf agents alts scf"
assumes eq: "mset (map ((map (λA. permutation_of_list xs  A)) ∘ snd) yss) = mset (map snd yss)"
assumes perm: "set (map fst xs) ⊆ alts" "set (map snd xs) = set (map fst xs)"
"distinct (map fst xs)"
and x: "x ∈ alts" "y = permutation_of_list xs x"
shows   "x ∈ scf R ⟷ y ∈ scf R"
proof -
note perm = list_permutesI[OF perm]
let ?σ = "permutation_of_list xs"
note perm' = permutation_of_list_permutes [OF perm]
from wf have wf': "pref_profile_wf agents alts R" by (simp add: pref_profile_from_tableI)
then interpret R: pref_profile_wf agents alts R .
from perm' interpret R': pref_profile_wf agents alts "permute_profile ?σ R"
from an interpret an_scf agents alts scf .

from eq wf have eq': "image_mset (map (λA. ?σ  A)) (anonymous_profile R) = anonymous_profile R"
by (simp add: anonymise_prefs_from_table mset_map multiset.map_comp)
have "x ∈ scf R ⟷ ?σ x ∈ ?σ  scf R"
by (blast dest: injD[OF permutes_inj[OF perm']])
also from eq' x wf' perm' have "?σ  scf R = scf R"
by (intro scf_automorphism)
finally show ?thesis using x by simp
qed

subsection ‹Weighted-majoritarian SCFs›

locale pairwise_scf = social_choice_function agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
assumes pairwise:
"is_pref_profile R1 ⟹ is_pref_profile R2 ⟹ weighted_majority R1 = weighted_majority R2 ⟹
scf R1 = scf R2"

subsection ‹Pareto efficiency›

locale pareto_efficient_scf = social_choice_function agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
assumes pareto_efficient:
"is_pref_profile R ⟹ scf R ∩ pareto_losers R = {}"
begin

lemma pareto_efficient':
assumes "is_pref_profile R" "y ≻[Pareto(R)] x"
shows   "x ∉ scf R"
using pareto_efficient[of R] assms
by (auto simp: pareto_losers_def)

lemma pareto_efficient'':
assumes "is_pref_profile R" "i ∈ agents"  "∀i∈agents. y ≽[R i] x" "¬y ≼[R i] x"
shows   "x ∉ scf R"
proof -
from assms(1) interpret pref_profile_wf agents alts R .
from assms(2-) show ?thesis
by (intro pareto_efficient'[OF assms(1), of _ y])
(auto simp: Pareto_iff strongly_preferred_def)
qed

end

subsection ‹Set extensions›

type_synonym 'alt set_extension = "'alt relation ⇒ 'alt set relation"

definition Kelly :: "'alt set_extension" where
"A ≽[Kelly(R)] B ⟷ (∀a∈A. ∀b∈B. a ≽[R] b)"

lemma Kelly_strict_iff: "A ≻[Kelly(R)] B ⟷ ((∀a∈A. ∀b∈B. R b a) ∧ ¬ (∀a∈B. ∀b∈A. R b a))"
unfolding strongly_preferred_def Kelly_def ..

lemmas Kelly_eval = Kelly_def Kelly_strict_iff

definition Fishb :: "'alt set_extension" where
"A ≽[Fishb(R)] B ⟷ (∀a∈A. ∀b∈B-A. a ≽[R] b) ∧ (∀a∈A-B. ∀b∈B. a ≽[R] b)"

lemma Fishb_strict_iff:
"A ≻[Fishb(R)] B ⟷
((∀a∈A. ∀b∈B - A. R b a) ∧ (∀a∈A - B. ∀b∈B. R b a)) ∧
¬ ((∀a∈B. ∀b∈A - B. R b a) ∧ (∀a∈B - A. ∀b∈A. R b a))"
unfolding strongly_preferred_def Fishb_def ..

lemmas Fishb_eval = Fishb_def Fishb_strict_iff

subsection ‹Strategyproofness›

locale strategyproof_scf =
social_choice_function agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
fixes set_ext :: "'alt set_extension"
assumes strategyproof:
"is_pref_profile R ⟹ total_preorder_on alts Ri' ⟹ i ∈ agents ⟹
¬ scf (R(i := Ri')) ≻[set_ext(R i)] scf R"

locale strategyproof_anonymous_scf =
anonymous_scf agents alts scf + strategyproof_scf agents alts scf set_ext
for agents :: "'agent set" and alts :: "'alt set" and scf and set_ext
begin

lemma strategyproof':
assumes "is_pref_profile R1" "is_pref_profile R2" "i ∈ agents" "j ∈ agents"
assumes "anonymous_profile R2 = anonymous_profile R1 -
{#weak_ranking (R1 i)#} + {#weak_ranking (R2 j)#}"
shows   "¬scf R2 ≻[set_ext (R1 i)] scf R1"
proof -
let ?R3 = "R1(i := R2 j)"
interpret R1: pref_profile_wf agents alts R1 by fact
interpret R2: pref_profile_wf agents alts R2 by fact
from ‹j ∈ agents› have "total_preorder_on alts (R2 j)" by simp
from strategyproof[OF assms(1) this ‹i ∈ agents›]
have "¬scf ?R3 ≻[set_ext (R1 i)] scf R1" .
also from assms have "scf ?R3 = scf R2"
by (intro anonymous') (simp_all add: R1.anonymous_profile_update)
finally show ?thesis .
qed

end

context preorder_on
begin

lemma strict_not_outside:
assumes "x ≺[le] y"
shows   "x ∈ carrier" "y ∈ carrier"
using assms not_outside[of x y] unfolding strongly_preferred_def by blast+

end

subsection ‹Lifting preferences›

text ‹
Preference profiles can be lifted to a setting with more agents and alternatives by padding
them with dummy agents and alternatives in such a way that every original agent prefers and
original alternative over any dummy alternative and is indifferent between the dummy alternatives.
Moreover, every dummy agent is completely indifferent.
›

definition lift_prefs ::
"'alt set ⇒ 'alt set ⇒ 'alt relation ⇒ 'alt relation" where
"lift_prefs alts alts' R = (λx y.
x ∈ alts' ∧ y ∈ alts' ∧ (x = y ∨ x ∉ alts ∨ (y ∈ alts ∧ R x y)))"

lemma lift_prefs_wf:
assumes "total_preorder_on alts R" "alts ⊆ alts'"
shows   "total_preorder_on alts' (lift_prefs alts alts' R)"
proof -
interpret R: total_preorder_on alts R by fact
show ?thesis
by standard (insert R.total, auto dest: R.trans simp: lift_prefs_def)
qed

definition lift_pref_profile ::
"'agent set ⇒ 'alt set ⇒ 'agent set ⇒ 'alt set ⇒
('agent, 'alt) pref_profile ⇒ ('agent, 'alt) pref_profile" where
"lift_pref_profile agents alts agents' alts' R = (λi x y.
x ∈ alts' ∧ y ∈ alts' ∧ i ∈ agents' ∧
(x = y ∨ x ∉ alts ∨ i ∉ agents ∨ (y ∈ alts ∧ R i x y)))"

lemma lift_pref_profile_conv_vector:
assumes "i ∈ agents" "i ∈ agents'"
shows   "lift_pref_profile agents alts agents' alts' R i = lift_prefs alts alts' (R i)"
using assms by (auto simp: lift_pref_profile_def lift_prefs_def)

lemma lift_pref_profile_wf:
assumes "pref_profile_wf agents alts R"
assumes "agents ⊆ agents'" "alts ⊆ alts'" "finite alts'"
defines "R' ≡ lift_pref_profile agents alts agents' alts' R"
shows   "pref_profile_wf agents' alts' R'"
proof -
from assms interpret R: pref_profile_wf agents alts by simp
have "finite_total_preorder_on alts' (R' i)"
if i: "i ∈ agents'" for i
proof (cases "i ∈ agents")
case True
then interpret finite_total_preorder_on alts "R i" by simp
from True assms show ?thesis
by unfold_locales (auto simp: lift_pref_profile_def dest: total intro: trans)
next
case False
with assms i show ?thesis
qed
moreover have "R' i = (λ_ _. False)" if "i ∉ agents'" for i
unfolding lift_pref_profile_def R'_def using that by simp
ultimately show ?thesis unfolding pref_profile_wf_def using assms by auto
qed

lemma lift_pref_profile_permute_agents:
assumes "π permutes agents" "agents ⊆ agents'"
shows   "lift_pref_profile agents alts agents' alts' (R ∘ π) =
lift_pref_profile agents alts agents' alts' R ∘ π"
using assms permutes_subset[OF assms]
by (auto simp add: lift_pref_profile_def o_def permutes_in_image)

lemma lift_pref_profile_permute_alts:
assumes "σ permutes alts" "alts ⊆ alts'"
shows   "lift_pref_profile agents alts agents' alts' (permute_profile σ R) =
permute_profile σ (lift_pref_profile agents alts agents' alts' R)"
proof -
from assms have inv: "inv σ permutes alts" by (intro permutes_inv)
from this assms(2) have "inv σ permutes alts'" by (rule permutes_subset)
with inv show ?thesis using assms permutes_inj[OF ‹inv σ permutes alts›]
by (fastforce simp add: lift_pref_profile_def permutes_in_image
permute_profile_def fun_eq_iff dest: injD)
qed

context
fixes agents alts R agents' alts' R'
assumes R_wf: "pref_profile_wf agents alts R"
assumes election: "agents ⊆ agents'" "alts ⊆ alts'" "alts ≠ {}" "agents ≠ {}" "finite alts'"
defines "R' ≡ lift_pref_profile agents alts agents' alts' R"
begin

interpretation R: pref_profile_wf agents alts R by fact
interpretation R': pref_profile_wf agents' alts' R'
using election R_wf by (simp add: R'_def lift_pref_profile_wf)

lemma lift_pref_profile_strict_iff:
"x ≺[lift_pref_profile agents alts agents' alts' R i] y ⟷
i ∈ agents ∧ ((y ∈ alts ∧ x ∈ alts' - alts) ∨ x ≺[R i] y)"
proof (cases "i ∈ agents")
case True
then interpret total_preorder_on alts "R i" by simp
show ?thesis using not_outside election
by (auto simp: lift_pref_profile_def strongly_preferred_def)

lemma preferred_alts_lift_pref_profile:
assumes i: "i ∈ agents'" and x: "x ∈ alts'"
shows   "preferred_alts (R' i) x =
(if i ∈ agents ∧ x ∈ alts then preferred_alts (R i) x else alts')"
proof (cases "i ∈ agents")
assume i: "i ∈ agents"
then interpret Ri: total_preorder_on alts "R i" by simp
show ?thesis
using i x election Ri.not_outside
by (auto simp: preferred_alts_def R'_def lift_pref_profile_def Ri.refl)
qed (auto simp: preferred_alts_def R'_def lift_pref_profile_def i x)

lemma lift_pref_profile_Pareto_iff:
"x ≼[Pareto(R')] y ⟷ x ∈ alts' ∧ y ∈ alts' ∧ (x ∉ alts ∨ x ≼[Pareto(R)] y)"
proof -
from R.nonempty_agents obtain i where i: "i ∈ agents" by blast
then interpret Ri: finite_total_preorder_on alts "R i" by simp
show ?thesis unfolding R'.Pareto_iff R.Pareto_iff unfolding R'_def lift_pref_profile_def
using election i by (auto simp: preorder_on.refl[OF R.in_dom]
simp del: R.nonempty_alts R.nonempty_agents  intro: Ri.not_outside)
qed

lemma lift_pref_profile_Pareto_strict_iff:
"x ≺[Pareto(R')] y ⟷ x ∈ alts' ∧ y ∈ alts' ∧ (x ∉ alts ∧ y ∈ alts ∨ x ≺[Pareto(R)] y)"
by (auto simp: strongly_preferred_def lift_pref_profile_Pareto_iff R.Pareto.not_outside)

lemma pareto_losers_lift_pref_profile:
shows   "pareto_losers R' = pareto_losers R ∪ (alts' - alts)"
proof -
have A: "x ∈ alts" "y ∈ alts" if "x ≺[Pareto(R)] y" for x y
using that R.Pareto.not_outside unfolding strongly_preferred_def by auto
have B: "x ∈ alts'" if "x ∈ alts" for x using election that by blast
from R.nonempty_alts obtain x where x: "x ∈ alts" by blast
thus ?thesis unfolding pareto_losers_def lift_pref_profile_Pareto_strict_iff [abs_def]
by (auto dest: A B)
qed

end

subsection ‹Lowering SCFs›

text ‹
Using the preference lifting, we can now \emph{lower} an SCF to a setting with fewer agents
and alternatives under mild conditions to the original SCF. This preserves many nice properties,
such as anonymity, neutrality, and strategyproofness.
›

locale scf_lowering =
pareto_efficient_scf agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
fixes agents' alts'
assumes agents'_subset: "agents' ⊆ agents" and alts'_subset: "alts' ⊆ alts"
and agents'_nonempty [simp]: "agents' ≠ {}" and alts'_nonempty [simp]: "alts' ≠ {}"
begin

lemma finite_agents' [simp]: "finite agents'"
using agents'_subset finite_agents by (rule finite_subset)

lemma finite_alts' [simp]: "finite alts'"
using alts'_subset finite_alts by (rule finite_subset)

abbreviation lift :: "('agent, 'alt) pref_profile ⇒ ('agent, 'alt) pref_profile" where
"lift ≡ lift_pref_profile agents' alts' agents alts"

definition lowered :: "('agent, 'alt) pref_profile ⇒ 'alt set" where
"lowered = scf ∘ lift"

lemma lift_wf [simp, intro]:
"pref_profile_wf agents' alts' R ⟹ is_pref_profile (lift R)"
using alts'_subset agents'_subset by (intro lift_pref_profile_wf) simp_all

sublocale lowered: election agents' alts'
by unfold_locales simp_all

lemma preferred_alts_lift:
"lowered.is_pref_profile R ⟹ i ∈ agents ⟹ x ∈ alts ⟹
preferred_alts (lift R i) x =
(if i ∈ agents' ∧ x ∈ alts' then preferred_alts (R i) x else alts)"
using alts'_subset agents'_subset
by (intro preferred_alts_lift_pref_profile) simp_all

lemma pareto_losers_lift:
"lowered.is_pref_profile R ⟹ pareto_losers (lift R) = pareto_losers R ∪ (alts - alts')"
using agents'_subset alts'_subset by (intro pareto_losers_lift_pref_profile) simp_all

sublocale lowered: social_choice_function agents' alts' lowered
proof
fix R assume R_wf: "pref_profile_wf agents' alts' R"
from R_wf have R'_wf: "pref_profile_wf agents alts (lift R)" by (rule lift_wf)
show "lowered R ⊆ alts'"
proof safe
fix x assume "x ∈ lowered R"
hence "x ∈ scf (lift R)" by (auto simp: o_def lowered_def)
moreover have "scf (lift R) ∩ pareto_losers (lift R) = {}"
by (intro pareto_efficient R'_wf)
ultimately show "x ∈ alts'" using scf_alts[of "lift R"]
by (auto simp: pareto_losers_lift R_wf R'_wf)
qed
show "lowered R ≠ {}"
using R'_wf by (auto simp: lowered_def scf_nonempty)
qed

sublocale lowered: pareto_efficient_scf agents' alts' lowered
proof
fix R assume R_wf: "pref_profile_wf agents' alts' R"
from R_wf have R'_wf: "pref_profile_wf agents alts (lift R)" by (rule lift_wf)
have "lowered R ∩ pareto_losers (lift R) = {}" unfolding lowered_def o_def
by (intro pareto_efficient R'_wf)
with R_wf show "lowered R ∩ pareto_losers R = {}"
by (auto simp: pareto_losers_lift)
qed

end

locale scf_lowering_anonymous =
anonymous_scf agents alts scf +
scf_lowering agents alts scf agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and scf agents' alts'
begin

sublocale lowered: anonymous_scf agents' alts' lowered
proof
fix π R
assume "π permutes agents'" and "lowered.is_pref_profile R"
thus "lowered (R ∘ π) = lowered R" using agents'_subset
by (auto simp: lowered_def lift_pref_profile_permute_agents anonymous permutes_subset)
qed

end

locale scf_lowering_neutral =
neutral_scf agents alts scf +
scf_lowering agents alts scf agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and scf agents' alts'
begin

sublocale lowered: neutral_scf agents' alts' lowered
proof
fix σ R
assume "σ permutes alts'" and "lowered.is_pref_profile R"
thus "lowered (permute_profile σ R) = σ  lowered R" using alts'_subset
by (auto simp: lowered_def lift_pref_profile_permute_alts neutral permutes_subset)
qed

end

text ‹
The following is a technical condition that we need from a set extensions in order for
strategyproofness to survive the lowering. The condition could probably be weakened a bit,
but it is good enough for our purposes the way it is.
›
locale liftable_set_extension =
fixes alts' alts :: "'alt set" and set_ext :: "'alt relation ⇒ 'alt set relation"
assumes set_ext_strong_lift:
"total_preorder_on alts' R ⟹ A ≠ {} ⟹ B ≠ {} ⟹ A ⊆ alts' ⟹ B ⊆ alts' ⟹
A ≺[set_ext R] B ⟹ A ≺[set_ext (lift_prefs alts' alts R)] B"

lemma liftable_set_extensionI_weak:
assumes "⋀R A B. total_preorder_on alts' R ⟹ A ≠ {} ⟹ B ≠ {} ⟹
A ⊆ alts' ⟹ B ⊆ alts' ⟹
A ≼[set_ext R] B ⟷ A ≼[set_ext (lift_prefs alts' alts R)] B"
shows   "liftable_set_extension alts' alts set_ext"
proof (standard, goal_cases)
case (1 R A B)
from assms[of R A B] and assms[of R B A] and 1 show ?case
by (auto simp: strongly_preferred_def)
qed

lemma Kelly_liftable:
assumes "alts' ⊆ alts"
shows   "liftable_set_extension alts' alts Kelly"
proof (rule liftable_set_extensionI_weak, goal_cases)
case (1 R A B)
interpret R: total_preorder_on alts' R by fact
from 1(2-5) show ?case using assms  R.refl
by (force simp: Kelly_def lift_prefs_def)
qed

lemma Fishburn_liftable:
assumes "alts' ⊆ alts"
shows   "liftable_set_extension alts' alts Fishb"
proof (rule liftable_set_extensionI_weak, goal_cases)
case (1 R A B)
interpret R: total_preorder_on alts' R by fact
have conj_cong: "P1 ∧ Q1 ⟷ P2 ∧ Q2" if "P1 ⟷ P2" "Q1 ⟷ Q2" for P1 P2 Q1 Q2
using that by blast
from 1(2-5) show ?case using assms
unfolding Fishb_def lift_prefs_def by (intro conj_cong ball_cong refl) auto
qed

locale scf_lowering_strategyproof =
strategyproof_scf agents alts scf set_ext +
liftable_set_extension alts' alts set_ext +
scf_lowering agents alts scf agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and scf agents' alts' set_ext
begin

sublocale lowered: strategyproof_scf agents' alts' lowered
proof
fix R Ri' i
assume R_wf: "lowered.is_pref_profile R" and Ri'_wf: "total_preorder_on alts' Ri'"
and i: "i ∈ agents'"
interpret R: pref_profile_wf agents' alts' R by fact
interpret Ri': total_preorder_on alts' Ri' by fact
from R_wf have R'_wf: "is_pref_profile (lift R)" by (rule lift_wf)

― ‹We lift the alternative preference for the agent @{term i} in @{term R} to
preferences in the lifted profile. ›
define Ri'' where "Ri'' = lift_prefs alts' alts Ri'"

have "¬scf (lift R) ≺[set_ext (lift R i)] scf ((lift R)(i := Ri''))"
using i agents'_subset alts'_subset unfolding Ri''_def
by (intro strategyproof R'_wf Ri'_wf lift_prefs_wf) auto
also have "(lift R)(i := Ri'') = lift (R(i := Ri'))" using i agents'_subset
by (auto simp: fun_eq_iff Ri''_def lift_pref_profile_def lift_prefs_def)
finally have not_less: "¬scf (lift R) ≺[set_ext (lift R i)] scf (lift (R(i := Ri')))" .

show "¬lowered R ≺[set_ext (R i)] lowered (R(i := Ri'))"
proof
assume "lowered R ≺[set_ext (R i)] lowered (R(i := Ri'))"
hence "lowered R ≺[set_ext (lift_prefs alts' alts (R i))] lowered (R(i := Ri'))"
by (intro set_ext_strong_lift R.prefs_wf'(1) i lowered.scf_nonempty lowered.scf_alts
R.wf_update R_wf Ri'_wf)
also have "lift_prefs alts' alts (R i) = lift R i"
using agents'_subset i by (subst lift_pref_profile_conv_vector) auto
finally show False using not_less unfolding lowered_def o_def by contradiction
qed
qed

end

end

# Theory Fishburn_Impossibility

(*
File:     Fishburn_Impossibility.thy
Author:   Manuel Eberl, TU München
Author:   Christian Saile, TU München

Incompatibility of Pareto Optimality and Fishburn-Strategy-Proofness
*)
section ‹Main impossibility result›

theory Fishburn_Impossibility
imports
Social_Choice_Functions
begin

subsection ‹Setting of the base case›

text ‹
Suppose we have an anonymous, Fishburn-strategyproof, and Pareto-efficient SCF
for three agents $A1$ to $A3$ and three alternatives $a$, $b$, and $c$. We will derive
›
locale fb_impossibility_3_3 =
strategyproof_anonymous_scf agents alts scf Fishb +
pareto_efficient_scf agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf A1 A2 A3 a b c +
assumes agents_eq: "agents = {A1, A2, A3}"
assumes alts_eq:    "alts = {a, b, c}"
assumes distinct_agents: "distinct [A1, A2, A3]"
assumes distinct_alts: "distinct [a, b, c]"
begin

text ‹
We first give some simple rules that will allow us to break down the strategyproofness
and support conditions more easily later.
›
lemma agents_neq [simp]: "A1 ≠ A2" "A2 ≠ A1" "A1 ≠ A3" "A3 ≠ A1" "A2 ≠ A3" "A3 ≠ A2"
using distinct_agents by auto

lemma alts_neq [simp]: "a ≠ b" "a ≠ c" "b ≠ c" "b ≠ a" "c ≠ a" "c ≠ b"
using distinct_alts by auto

lemma agent_in_agents [simp]: "A1 ∈ agents" "A2 ∈ agents" "A3 ∈ agents"

lemma alt_in_alts [simp]: "a ∈ alts" "b ∈ alts" "c ∈ alts"

lemma Bex_alts: "(∃x∈alts. P x) ⟷ P a ∨ P b ∨ P c"

lemma eval_pareto_loser_aux:
assumes "is_pref_profile R"
shows   "x ∈ pareto_losers R ⟷ (∃y∈{a,b,c}. x ≺[Pareto(R)] y)"
proof -
interpret pref_profile_wf agents alts R by fact
have *: "y ∈ {a,b,c}" if "x ≺[Pareto(R)] y" for y
using Pareto.strict_not_outside[of x y] that by (simp add: alts_eq)
show ?thesis by (auto simp: pareto_losers_def dest: *)
qed

lemma eval_Pareto:
assumes "is_pref_profile R"
shows   "x ≺[Pareto(R)] y ⟷ (∀i∈{A1,A2,A3}. x ≼[R i] y) ∧ (∃i∈{A1,A2,A3}. ¬x ≽[R i] y)"
proof -
interpret R: pref_profile_wf agents alts by fact
show ?thesis unfolding R.Pareto_strict_iff by (auto simp: strongly_preferred_def agents_eq)
qed

lemmas eval_pareto = eval_pareto_loser_aux eval_Pareto
lemma pareto_efficiency: "is_pref_profile R ⟹ x ∈ pareto_losers R ⟹ x ∉ scf R"
using pareto_efficient[of R] by blast

lemma Ball_scf:
assumes "is_pref_profile R"
shows   "(∀x∈scf R. P x) ⟷ (a ∉ scf R ∨ P a) ∧ (b ∉ scf R ∨ P b) ∧ (c ∉ scf R ∨ P c)"
using scf_alts[OF assms] unfolding alts_eq by blast

lemma Ball_scf_diff:
assumes "is_pref_profile R1" "is_pref_profile R2"
shows   "(∀x∈scf R1 - scf R2. P x) ⟷
(a ∈ scf R2 ∨ a ∉ scf R1 ∨ P a) ∧ (b ∈ scf R2 ∨ b ∉ scf R1 ∨ P b) ∧
(c ∈ scf R2 ∨ c ∉ scf R1 ∨ P c)"
using assms[THEN scf_alts] unfolding alts_eq by blast

lemma scf_nonempty':
assumes "is_pref_profile R"
shows   "∃x∈alts. x ∈ scf R"
using scf_nonempty[OF assms] scf_alts[OF assms] by blast

subsection ‹Definition of Preference Profiles and Fact Gathering›

text ‹
We now define the 21 preference profile that will lead to the impossibility result.
›
preference_profile
agents: agents
alts:   alts
where R1   = A1: [a, c], b    A2: [a, c], b     A3: b, c, a
and R2   = A1: c, [a, b]    A2: b, c, a       A3: c, b, a
and R3   = A1: [a, c], b    A2: b, c, a       A3: c, b, a
and R4   = A1: [a, c], b    A2:  a, b, c      A3: b, c, a
and R5   = A1: c, [a, b]    A2:  a, b, c      A3: b, c, a
and R6   = A1: b, [a, c]    A2: c, [a, b]     A3:  b, c, a
and R7   = A1: [a, c], b    A2: b, [a, c]     A3: b, c, a
and R8   = A1: [b, c], a    A2: a, [b, c]     A3: a, c, b
and R9   = A1: [b, c], a    A2: b, [a, c]     A3: a, b, c
and R10  = A1: c, [a, b]    A2: a, b, c       A3: c, b, a
and R11  = A1: [a, c], b    A2: a, b, c       A3: c, b, a
and R12  = A1: c, [a, b]    A2: b, a, c       A3: c, b, a
and R13  = A1: [a, c], b    A2: b, a, c       A3: c, b, a
and R14  = A1: a, [b, c]    A2: c, [a, b]     A3: a, c, b
and R15  = A1: [b, c], a    A2: a, [b, c]     A3: a, b, c
and R16  = A1: [a, b], c    A2: c, [a, b]     A3: a, b, c
and R17  = A1: a, [b, c]    A2: a, b, c       A3: b, c, a
and R18  = A1: [a, c], b    A2: b, [a, c]     A3: b, a, c
and R19  = A1: a, [b, c]    A2: c, [a, b]     A3: a, b, c
and R20  = A1: b, [a, c]    A2: a, b, c       A3: b, a, c
and R21  = A1: [b, c], a    A2: a, b, c       A3: b, c, a

lemmas R_wfs =
R1.wf R2.wf R3.wf R4.wf R5.wf R6.wf R7.wf R8.wf R9.wf R10.wf R11.wf R12.wf R13.wf R14.wf R15.wf
R16.wf R17.wf R18.wf R19.wf R20.wf R21.wf

lemmas R_evals =
R1.eval R2.eval R3.eval R4.eval R5.eval R6.eval R7.eval R8.eval R9.eval R10.eval R11.eval R12.eval  R13.eval
R14.eval R15.eval R16.eval R17.eval R18.eval R19.eval R20.eval R21.eval

lemmas nonemptiness = R_wfs [THEN scf_nonempty', unfolded Bex_alts]

text ‹
We show the support conditions from Pareto efficiency
›
lemma [simp]: "a ∉ scf R1" by (rule pareto_efficiency) (simp_all add: eval_pareto R1.eval)
lemma [simp]: "a ∉ scf R2" by (rule pareto_efficiency) (simp_all add: eval_pareto R2.eval)
lemma [simp]: "a ∉ scf R3" by (rule pareto_efficiency) (simp_all add: eval_pareto R3.eval)
lemma [simp]: "a ∉ scf R6" by (rule pareto_efficiency) (simp_all add: eval_pareto R6.eval)
lemma [simp]: "a ∉ scf R7" by (rule pareto_efficiency) (simp_all add: eval_pareto R7.eval)
lemma [simp]: "b ∉ scf R8" by (rule pareto_efficiency) (simp_all add: eval_pareto R8.eval)
lemma [simp]: "c ∉ scf R9" by (rule pareto_efficiency) (simp_all add: eval_pareto R9.eval)
lemma [simp]: "a ∉ scf R12" by (rule pareto_efficiency) (simp_all add: eval_pareto R12.eval)
lemma [simp]: "b ∉ scf R14" by (rule pareto_efficiency) (simp_all add: eval_pareto R14.eval)
lemma [simp]: "c ∉ scf R15" by (rule pareto_efficiency) (simp_all add: eval_pareto R15.eval)
lemma [simp]: "b ∉ scf R16" by (rule pareto_efficiency) (simp_all add: eval_pareto R16.eval)
lemma [simp]: "c ∉ scf R17" by (rule pareto_efficiency) (simp_all add: eval_pareto R17.eval)
lemma [simp]: "c ∉ scf R18" by (rule pareto_efficiency) (simp_all add: eval_pareto R18.eval)
lemma [simp]: "b ∉ scf R19" by (rule pareto_efficiency) (simp_all add: eval_pareto R19.eval)
lemma [simp]: "c ∉ scf R20" by (rule pareto_efficiency) (simp_all add: eval_pareto R20.eval)
lemma [simp]: "c ∉ scf R21" by (rule pareto_efficiency) (simp_all add: eval_pareto R21.eval)

text ‹
We derive the strategyproofness conditions:
›
lemma s41: "¬ scf R4 ≻[Fishb(R1 A2)] scf R1"
by (intro strategyproof'[where j = A2]) (simp_all add: R4.eval R1.eval)

lemma s32: "¬ scf R3 ≻[Fishb(R2 A1)] scf R2"
by (intro strategyproof'[where j = A1]) (simp_all add: R3.eval R2.eval)

lemma s122: "¬ scf R12 ≻[Fishb(R2 A2)] scf R2"
by (intro strategyproof'[where j = A2]) (simp_all add: R12.eval R2.eval)

lemma s133: "¬ scf R13 ≻[Fishb(R3 A2)] scf R3"
by (intro strategyproof'[where j = A2]) (simp_all add: R13.eval R3.eval)

lemma s102: "¬ scf R10 ≻[Fishb(R2 A2)] scf R2"
by (intro strategyproof'[where j = A2]) (simp_all add: R10.eval R2.eval)

lemma s13: "¬ scf R1 ≻[Fishb(R3 A3)] scf R3"
by (intro strategyproof'[where j = A2]) (simp_all add: R1.eval R3.eval)

lemma s54: "¬ scf R5 ≻[Fishb(R4 A1)] scf R4"
by (intro strategyproof'[where j = A1]) (simp_all add: R5.eval R4.eval)

lemma s174: "¬ scf R17 ≻[Fishb(R4 A1)] scf R4"
by (intro strategyproof'[where j = A1]) (simp_all add: R17.eval R4.eval)

lemma s74: "¬ scf R7 ≻[Fishb(R4 A2)] scf R4"
by (intro strategyproof'[where j = A2]) (simp_all add: R7.eval R4.eval)

lemma s114: "¬ scf R11 ≻[Fishb(R4 A3)] scf R4"
by (intro strategyproof'[where j = A3]) (simp_all add: R11.eval R4.eval)

lemma s45: "¬ scf R4 ≻[Fishb(R5 A1)] scf R5"
by (intro strategyproof'[where j = A1]) (simp_all add: R4.eval R5.eval)

lemma s65: "¬ scf R6 ≻[Fishb(R5 A2)] scf R5"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute R5.eval R6.eval)

lemma s105: "¬ scf R10 ≻[Fishb(R5 A3)] scf R5"
by (intro strategyproof'[where j = A3]) (simp_all add:  R10.eval R5.eval)

lemma s67: "¬ scf R6 ≻[Fishb(R7 A1)] scf R7"
by (intro strategyproof'[where j = A2]) (simp_all add: insert_commute  R6.eval R7.eval)

lemma s187: "¬ scf R18 ≻[Fishb(R7 A3)] scf R7"
by (intro strategyproof'[where j = A3]) (simp_all add: insert_commute R7.eval R18.eval)

lemma s219: "¬ scf R21 ≻[Fishb(R9 A2)] scf R9"
by (intro strategyproof'[where j = A3]) (simp_all add: insert_commute R9.eval R21.eval)

lemma s1011: "¬ scf R10 ≻[Fishb(R11 A1)] scf R11"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute R10.eval R11.eval)

lemma s1012: "¬ scf R10 ≻[Fishb(R12 A2)] scf R12"
by (intro strategyproof'[where j = A2]) (simp_all add: insert_commute R10.eval R12.eval)

lemma s1213: "¬ scf R12 ≻[Fishb(R13 A1)] scf R13"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute R12.eval R13.eval)

lemma s1113: "¬ scf R11 ≻[Fishb(R13 A2)] scf R13"
by (intro strategyproof'[where j = A2]) (simp_all add: insert_commute R11.eval R13.eval)

lemma s1813: "¬ scf R18 ≻[Fishb(R13 A3)] scf R13"
by (intro strategyproof'[where j = A2]) (simp_all add: insert_commute R18.eval R13.eval)

lemma s814: "¬ scf R8 ≻[Fishb(R14 A2)] scf R14"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute R8.eval R14.eval)

lemma s1914: "¬ scf R19 ≻[Fishb(R14 A3)] scf R14"
by (intro strategyproof'[where j = A3]) (simp_all add: insert_commute R19.eval R14.eval)

lemma s1715: "¬ scf R17 ≻[Fishb(R15 A1)] scf R15"
by (intro strategyproof'[where j = A3]) (simp_all add: insert_commute R17.eval R15.eval)

lemma s815: "¬ scf R8 ≻[Fishb(R15 A3)] scf R15"
by (intro strategyproof'[where j = A3]) (simp_all add: insert_commute R8.eval R15.eval)

lemma s516: "¬ scf R5 ≻[Fishb(R16 A1)] scf R16"
by (intro strategyproof'[where j = A3]) (simp_all add: insert_commute R5.eval R16.eval)

lemma s517: "¬ scf R5 ≻[Fishb(R17 A1)] scf R17"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute R5.eval R17.eval)

lemma s1619: "¬ scf R16 ≻[Fishb(R19 A1)] scf R19"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute  R16.eval R19.eval)

lemma s1820: "¬ scf R18 ≻[Fishb(R20 A2)] scf R20"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute  R18.eval R20.eval)

lemma s920: "¬ scf R9 ≻[Fishb(R20 A3)] scf R20"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute  R20.eval R9.eval)

lemma s521: "¬ scf R5 ≻[Fishb(R21 A1)] scf R21"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute  R21.eval R5.eval)

lemma s421: "¬ scf R4 ≻[Fishb(R21 A1)] scf R21"
by (intro strategyproof'[where j = A1]) (simp_all add: insert_commute  R21.eval R4.eval)

lemmas sp = s41 s32 s122 s102 s133 s13 s54 s174 s54 s74 s114 s45 s65 s105 s67
s187 s219 s1011 s1012 s1213 s1113 s1813 s814 s1914 s1715 s815 s516
s517 s1619 s1820 s920 s521 s421

text ‹
We now use the simplifier to break down the strategyproofness conditions into SAT formulae.
This takes a few seconds, so we use some low-level ML code to at least do the simplification
in parallel.
›
local_setup ‹fn lthy =>
let
val lthy' = lthy addsimps @{thms Fishb_strict_iff Ball_scf Ball_scf_diff R_evals}
val thms = Par_List.map (Simplifier.asm_full_simplify lthy') @{thms sp}
in
Local_Theory.notes [((@{binding sp'}, []), [(thms, [])])] lthy |> snd
end
›

text ‹
We show that the strategyproofness conditions, the non-emptiness conditions (i.\,e.\ every SCF
must return at least one winner), and the efficiency conditions are not satisfiable together,
which means that the SCF whose existence we assumed simply cannot exist.
›
theorem absurd: False
using sp' and nonemptiness [simplified] by satx

end

subsection ‹Lifting to more than 3 agents and alternatives›

text ‹
We now employ the standard lifting argument outlined before to lift this impossibility
from 3 agents and alternatives to any setting with at least 3 agents and alternatives.
›
locale fb_impossibility =
strategyproof_anonymous_scf agents alts scf Fishb +
pareto_efficient_scf agents alts scf
for agents :: "'agent set" and alts :: "'alt set" and scf +
assumes card_agents_ge: "card agents ≥ 3"
and card_alts_ge:   "card alts ≥ 3"
begin

(* TODO: Move? *)
lemma finite_list':
assumes "finite A"
obtains xs where "A = set xs" "distinct xs" "length xs = card A"
proof -
from assms obtain xs where "set xs = A" using finite_list by blast
thus ?thesis using distinct_card[of "remdups xs"]
by (intro that[of "remdups xs"]) simp_all
qed

lemma finite_list_subset:
assumes "finite A" "card A ≥ n"
obtains xs where "set xs ⊆ A" "distinct xs" "length xs = n"
proof -
obtain xs where "A = set xs" "distinct xs" "length xs = card A"
using finite_list'[OF assms(1)] by blast
with assms show ?thesis
by (intro that[of "take n xs"]) (simp_all add: set_take_subset)
qed

lemma card_ge_3E:
assumes "finite A" "card A ≥ 3"
obtains a b c where "distinct [a,b,c]" "{a,b,c} ⊆ A"
proof -
from finite_list_subset[OF assms] guess xs .
moreover then obtain a b c where "xs = [a, b, c]"
by (auto simp: eval_nat_numeral length_Suc_conv)
ultimately show ?thesis by (intro that[of a b c]) simp_all
qed

theorem absurd: False
proof -
from card_ge_3E[OF finite_agents card_agents_ge] guess A1 A2 A3 .
note agents = this
let ?agents' = "{A1, A2, A3}"
from card_ge_3E[OF finite_alts card_alts_ge] guess a b c .
note alts = this
let ?alts' = "{a, b, c}"

interpret scf_lowering_anonymous agents alts scf ?agents' ?alts'
by standard (use agents alts in auto)
interpret liftable_set_extension ?alts' alts Fishb
by (intro Fishburn_liftable alts)
interpret scf_lowering_strategyproof agents alts scf ?agents' ?alts' Fishb ..
interpret fb_impossibility_3_3 ?agents' ?alts' lowered A1 A2 A3 a b c
by standard (use agents alts in simp_all)
from absurd show False .
qed

end

end`