Theory SDS_Lowering
section ‹Lowering Social Decision Schemes›
theory SDS_Lowering
imports Social_Decision_Schemes
begin
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_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
by unfold_locales (simp_all add: lift_pref_profile_def)
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
lemma lotteries_on_subset: "A ⊆ B ⟹ p ∈ lotteries_on A ⟹ p ∈ lotteries_on B"
unfolding lotteries_on_def by blast
lemma lottery_prob_carrier: "p ∈ lotteries_on A ⟹ measure_pmf.prob p A = 1"
by (auto simp: measure_pmf.prob_eq_1 lotteries_on_def AE_measure_pmf_iff)
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)
qed (simp_all add: 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
context
begin
private lemma lift_SD_iff_agent:
assumes "p ∈ lotteries_on alts" "q ∈ lotteries_on alts" and i: "i ∈ agents"
shows "p ≼[SD(R' i)] q ⟷ p ≼[SD(R i)] q"
proof -
from i interpret Ri: preorder_on alts "R i" by simp
from i election have i': "i ∈ agents'" by blast
then interpret R'i: preorder_on alts' "R' i" by simp
from assms election have "p ∈ lotteries_on alts'" "q ∈ lotteries_on alts'"
by (auto intro: lotteries_on_subset)
with assms election i' show ?thesis
by (auto simp: Ri.SD_preorder R'i.SD_preorder
preferred_alts_lift_pref_profile lottery_prob_carrier)
qed
private lemma lift_SD_iff_nonagent:
assumes "p ∈ lotteries_on alts" "q ∈ lotteries_on alts" and i: "i ∈ agents' - agents"
shows "p ≼[SD(R' i)] q"
proof -
from i election have i': "i ∈ agents'" by blast
then interpret R'i: preorder_on alts' "R' i" by simp
from assms election have "p ∈ lotteries_on alts'" "q ∈ lotteries_on alts'"
by (auto intro: lotteries_on_subset)
with assms election i' show ?thesis
by (auto simp: R'i.SD_preorder preferred_alts_lift_pref_profile lottery_prob_carrier)
qed
lemmas lift_SD_iff = lift_SD_iff_agent lift_SD_iff_nonagent
lemma lift_SD_iff':
"p ∈ lotteries_on alts ⟹ q ∈ lotteries_on alts ⟹ i ∈ agents' ⟹
p ≼[SD(R' i)] q ⟷ i ∉ agents ∨ p ≼[SD(R i)] q"
by (cases "i ∈ agents") (simp_all add: lift_SD_iff)
end
lemma lift_SD_strict_iff:
assumes "p ∈ lotteries_on alts" "q ∈ lotteries_on alts" and i: "i ∈ agents"
shows "p ≺[SD(R' i)] q ⟷ p ≺[SD(R i)] q"
using assms by (simp add: strongly_preferred_def lift_SD_iff)
lemma lift_Pareto_SD_iff:
assumes "p ∈ lotteries_on alts" "q ∈ lotteries_on alts"
shows "p ≼[Pareto(SD ∘ R')] q ⟷ p ≼[Pareto(SD ∘ R)] q"
using assms election by (auto simp: R.SD.Pareto_iff R'.SD.Pareto_iff lift_SD_iff')
lemma lift_Pareto_SD_strict_iff:
assumes "p ∈ lotteries_on alts" "q ∈ lotteries_on alts"
shows "p ≺[Pareto(SD ∘ R')] q ⟷ p ≺[Pareto(SD ∘ R)] q"
using assms by (simp add: strongly_preferred_def lift_Pareto_SD_iff)
lemma lift_SD_efficient_iff:
assumes p: "p ∈ lotteries_on alts"
shows "SD_efficient R' p ⟷ SD_efficient R p"
proof
assume eff: "SD_efficient R' p"
have "¬(q ≻[Pareto(SD ∘ R)] p)" if q: "q ∈ lotteries_on alts" for q
proof -
from q election have q': "q ∈ lotteries_on alts'" by (blast intro: lotteries_on_subset)
with eff have "¬(q ≻[Pareto(SD ∘ R')] p)" by (simp add: R'.SD_efficient_def)
with p q show ?thesis by (simp add: lift_Pareto_SD_strict_iff)
qed
thus "SD_efficient R p" by (simp add: R.SD_efficient_def)
next
assume eff: "SD_efficient R p"
have "¬(q ≻[Pareto(SD ∘ R')] p)" if q: "q ∈ lotteries_on alts'" for q
proof
assume less: "q ≻[Pareto(SD ∘ R')] p"
from R'.SD_efficient_lottery_exists[OF q]
obtain q' where q': "q' ∈ lotteries_on alts'" "Pareto (SD ∘ R') q q'" "SD_efficient R' q'" .
have "x ∉ set_pmf q'" if x: "x ∈ alts' - alts" for x
proof -
from x have "x ∈ pareto_losers R'" by (simp add: pareto_losers_lift_pref_profile)
with R'.SD_efficient_no_pareto_loser[OF q'(3,1)] show "x ∉ set_pmf q'" by blast
qed
with q' have "q' ∈ lotteries_on alts" by (auto simp: lotteries_on_def)
moreover from q' less have "q' ≻[Pareto(SD ∘ R')] p"
by (auto intro: R'.SD.Pareto.strict_weak_trans)
with ‹q' ∈ lotteries_on alts› p have "q' ≻[Pareto(SD ∘ R)] p"
by (subst (asm) lift_Pareto_SD_strict_iff)
ultimately have "¬SD_efficient R p" by (auto simp: R.SD_efficient_def)
with eff show False by contradiction
qed
thus "SD_efficient R' p" by (simp add: R'.SD_efficient_def)
qed
end
locale sds_lowering =
ex_post_efficient_sds agents alts sds
for agents :: "'agent set" and alts :: "'alt set" and sds +
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 lottery" where
"lowered = sds ∘ 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
lemma lowered_lotteries: "lowered.lotteries ⊆ lotteries"
unfolding lotteries_on_def using alts'_subset by blast
sublocale lowered: social_decision_scheme 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 ∈ lowered.lotteries" unfolding lotteries_on_def
proof safe
fix x assume "x ∈ set_pmf (lowered R)"
hence x: "x ∈ set_pmf (sds (lift R))" by (simp add: lowered_def)
with ex_post_efficient[OF R'_wf]
have "x ∉ pareto_losers (lift R)" by blast
with pareto_losers_lift[OF R_wf]
have "x ∉ alts - alts'" by blast
moreover from x have "x ∈ alts" using sds_wf[OF R'_wf]
by (auto simp: lotteries_on_def)
ultimately show "x ∈ alts'" by simp
qed
qed
sublocale ex_post_efficient_sds agents' alts' lowered
proof
fix R assume R_wf: "lowered.is_pref_profile R"
hence "is_pref_profile (lift R)" by simp
have "set_pmf (lowered R) ∩ pareto_losers (lift R) = {}"
unfolding lowered_def o_def by (intro ex_post_efficient lift_wf R_wf)
also have "pareto_losers (lift R) = pareto_losers R ∪ (alts - alts')"
by (intro pareto_losers_lift R_wf)
finally show "set_pmf (lowered R) ∩ pareto_losers R = {}" by blast
qed
lemma lowered_in_lotteries [simp]: "lowered.is_pref_profile R ⟹ lowered R ∈ lotteries"
using lowered.sds_wf[of R] lowered_lotteries by blast
end
locale sds_lowering_anonymous =
anonymous_sds agents alts sds +
sds_lowering agents alts sds agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and sds agents' alts'
begin
sublocale lowered: anonymous_sds agents' alts' lowered
proof
fix π R assume perm: "π permutes agents'" and R_wf: "lowered.is_pref_profile R"
from perm have "lift (R ∘ π) = lift R ∘ π"
using agents'_subset by (rule lift_pref_profile_permute_agents)
hence "sds (lift (R ∘ π)) = sds (lift R ∘ π)" by simp
also from perm R_wf have "π permutes agents" "is_pref_profile (lift R)"
using agents'_subset by (auto dest: permutes_subset)
from anonymous[OF this] have "sds (lift R ∘ π) = sds (lift R)"
by (simp add: lowered_def)
finally show "lowered (R ∘ π) = lowered R" unfolding lowered_def o_def .
qed
end
locale sds_lowering_neutral =
neutral_sds agents alts sds +
sds_lowering agents alts sds agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and sds agents' alts'
begin
sublocale lowered: neutral_sds agents' alts' lowered
proof
fix σ R assume perm: "σ permutes alts'" and R_wf: "lowered.is_pref_profile R"
from perm alts'_subset
have "lift (permute_profile σ R) = permute_profile σ (lift R)"
by (rule lift_pref_profile_permute_alts)
hence "sds (lift (permute_profile σ R)) = sds (permute_profile σ (lift R))" by simp
also from R_wf perm have "is_pref_profile (lift R)" by simp
with perm alts'_subset
have "sds (permute_profile σ (lift R)) = map_pmf σ (sds (lift R))"
by (intro neutral) (auto intro: permutes_subset)
finally show "lowered (permute_profile σ R) = map_pmf σ (lowered R)"
by (simp add: lowered_def o_def)
qed
end
locale sds_lowering_sd_efficient =
sd_efficient_sds agents alts sds +
sds_lowering agents alts sds agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and sds agents' alts'
begin
sublocale sd_efficient_sds agents' alts' lowered
proof
fix R assume R_wf: "lowered.is_pref_profile R"
interpret R: pref_profile_wf agents' alts' R by fact
from R_wf agents'_subset alts'_subset show "SD_efficient R (lowered R)"
unfolding lowered_def o_def
by (subst lift_SD_efficient_iff [symmetric])
(insert SD_efficient R_wf lowered.sds_wf[OF R_wf], auto simp: lowered_def)
qed
end
locale sds_lowering_strategyproof =
strategyproof_sds agents alts sds +
sds_lowering agents alts sds agents' alts'
for agents :: "'agent set" and alts :: "'alt set" and sds agents' alts'
begin
sublocale strategyproof_sds agents' alts' lowered
proof (unfold_locales, safe)
fix R i Ri'
assume R_wf: "lowered.is_pref_profile R" and i: "i ∈ agents'"
assume Ri': "total_preorder_on alts' Ri'"
assume manipulable: "lowered.manipulable_profile R i Ri'"
from i agents'_subset have i': "i ∈ agents" by blast
interpret R: pref_profile_wf agents' alts' R by fact
from R_wf interpret liftR: pref_profile_wf agents alts "lift R" by simp
define lift_Ri'
where "lift_Ri' x y ⟷ x ∈ alts ∧ y ∈ alts ∧ (x = y ∨ x ∉ alts' ∨ (y ∈ alts' ∧ Ri' x y))"
for x y
define S where "S = (lift R)(i := lift_Ri')"
from Ri' interpret Ri': total_preorder_on alts' Ri' .
have wf_lift_Ri': "total_preorder_on alts lift_Ri'" using Ri'.total
by unfold_locales (auto simp: lift_Ri'_def intro: Ri'.trans)
from agents'_subset i have S_altdef: "S = lift (R(i := Ri'))"
by (auto simp: fun_eq_iff lift_pref_profile_def lift_Ri'_def S_def)
have "lowered (R(i := Ri')) ∈ lowered.lotteries"
by (intro lowered.sds_wf R.wf_update i Ri')
hence sds_S_wf: "sds S ∈ lowered.lotteries" by (simp add: S_altdef lowered_def)
from manipulable have "lowered R ≺[SD (R i)] sds (lift (R(i := Ri')))"
unfolding lowered.manipulable_profile_def by (simp add: lowered_def)
also note S_altdef [symmetric]
finally have "lowered R ≺[SD (lift R i)] sds S"
using R_wf i lowered.sds_wf[OF R_wf] sds_S_wf
by (subst lift_SD_strict_iff) (simp_all add: agents'_subset alts'_subset)
hence "manipulable_profile (lift R) i lift_Ri'"
by (simp add: manipulable_profile_def lowered_def S_def)
with strategyproof[OF lift_wf[OF R_wf] i' wf_lift_Ri'] show False by contradiction
qed
end
locale sds_lowering_anonymous_neutral_sdeff_stratproof =
sds_lowering_anonymous + sds_lowering_neutral +
sds_lowering_sd_efficient + sds_lowering_strategyproof
end