Theory Random_Serial_Dictatorship

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

  Definition and basic properties of Random Serial Dictatorship
*)

section ‹Random Serial Dictatorship›

theory Random_Serial_Dictatorship
imports
  Complex_Main
  Social_Decision_Schemes
  Random_Dictatorship
begin

text ‹
  Random Serial Dictatorship is an anonymous, neutral, strongly strategy-proof, 
  and ex-post efficient Social Decision Scheme that extends Random Dictatorship
  to the domain of weak preferences.
  
  We define RSD using a fold over a random permutation. Effectively, we choose a random
  order of the agents (in the form of a list) and then traverse that list from left to right,
  where each agent in turn removes all the alternatives that are not top-ranked among the 
  remaining ones.
›
definition random_serial_dictatorship :: 
    "'agent set ⇒ 'alt set ⇒ ('agent, 'alt) pref_profile ⇒ 'alt lottery" where
  "random_serial_dictatorship agents alts R = 
     fold_bind_random_permutation (λi alts. Max_wrt_among (R i) alts) pmf_of_set alts agents"

text ‹
  The following two facts correspond give an alternative recursive definition to
  the above definition, which uses random permutations and list folding.
›
lemma random_serial_dictatorship_empty [simp]:
  "random_serial_dictatorship {} alts R = pmf_of_set alts"
  by (simp add: random_serial_dictatorship_def)

lemma random_serial_dictatorship_nonempty:
  "finite agents ⟹ agents ≠ {} ⟹ 
    random_serial_dictatorship agents alts R =
      do {
        i ← pmf_of_set agents;
        random_serial_dictatorship (agents - {i}) (Max_wrt_among (R i) alts) R
      }"
  by (simp add: random_serial_dictatorship_def)
     
     
text ‹
  We define the RSD winners w.r.t. a given set of alternatives and a fixed permutation 
  (i.e. list) of agents. In contrast to the above definition, the RSD winners are 
  determined by traversing the list of agents from right to left.
    This may seem strange, but it makes induction much easier, since induction over @{term foldr}
  does not require generalisation over the set of alternatives and is therefore much 
  easier than over @{term foldl}. 
›
definition rsd_winners where
  "rsd_winners R alts agents = foldr (λi alts. Max_wrt_among (R i) alts) agents alts"

lemma rsd_winners_empty [simp]: "rsd_winners R alts [] = alts"
  by (simp add: rsd_winners_def)

lemma rsd_winners_Cons [simp]:
  "rsd_winners R alts (i # agents) = Max_wrt_among (R i) (rsd_winners R alts agents)"
  by (simp add: rsd_winners_def)

lemma rsd_winners_map [simp]: 
  "rsd_winners R alts (map f agents) = rsd_winners (R ∘ f) alts agents"
  by (simp add: rsd_winners_def foldr_map o_def)

  
text ‹
  There is now another alternative definition of RSD in terms of the
  RSD winners. This will mostly be used for induction.
›
lemma random_serial_dictatorship_altdef:
  assumes "finite agents"
  shows   "random_serial_dictatorship agents alts R =
             do {
               agents' ← pmf_of_set (permutations_of_set agents);
               pmf_of_set (rsd_winners R alts agents')
             }"
   by (simp add: random_serial_dictatorship_def 
         fold_bind_random_permutation_foldr assms rsd_winners_def)
   
text ‹
  The following lemma shows that folding from left to right yields the same
  distribution. This is probably the most commonly used definition in the literature,
  along with the recursive one.
›
lemma random_serial_dictatorship_foldl:
  assumes "finite agents"
  shows   "random_serial_dictatorship agents alts R =
             do {
               agents' ← pmf_of_set (permutations_of_set agents);
               pmf_of_set (foldl (λalts i. Max_wrt_among (R i) alts) alts agents')
             }"
   by (simp add: random_serial_dictatorship_def fold_bind_random_permutation_foldl assms)


   
subsection ‹Auxiliary facts about RSD›


subsubsection ‹Pareto-equivalence classes›

text ‹
  First of all, we introduce the auxiliary notion of a Pareto-equivalence class.
  A non-empty set of alternatives is a Pareto equivalence class if all agents are 
  indifferent between all alternatives in it, and if some alternative @{term "x::'alt"} 
  is contained in the set, any other alternative @{term "y::'alt"} is contained in it
  if and only if, to all agents, @{term y} is at least as good as @{term x}.
    The importance of this notion lies in the fact that the set of RSD winners is always
  a Pareto-equivalence class, which we will later use to show ex-post efficiency and
  strategy-proofness.
›

definition RSD_pareto_eqclass where
  "RSD_pareto_eqclass agents alts R A ⟷
     A ≠ {} ∧ A ⊆ alts ∧ (∀x∈A. ∀y∈alts. y ∈ A ⟷ (∀i∈agents. R i x y))"

lemma RSD_pareto_eqclassI:
  assumes "A ≠ {}" "A ⊆ alts" "⋀x y. x ∈ A ⟹ y ∈ alts ⟹ y ∈ A ⟷ (∀i∈agents. R i x y)"
  shows   "RSD_pareto_eqclass agents alts R A"
  using assms unfolding RSD_pareto_eqclass_def by simp_all

lemma RSD_pareto_eqclassD:
  assumes "RSD_pareto_eqclass agents alts R A"
  shows   "A ≠ {}" "A ⊆ alts" "⋀x y. x ∈ A ⟹ y ∈ alts ⟹ y ∈ A ⟷ (∀i∈agents. R i x y)"
  using assms unfolding RSD_pareto_eqclass_def by simp_all

lemma RSD_pareto_eqclass_indiff_set:
  assumes "RSD_pareto_eqclass agents alts R A" "i ∈ agents" "x ∈ A" "y ∈ A"
  shows   "R i x y"
  using assms unfolding RSD_pareto_eqclass_def by blast

lemma RSD_pareto_eqclass_empty [simp, intro!]:
  "alts ≠ {} ⟹ RSD_pareto_eqclass {} alts R alts"
  by (auto intro!: RSD_pareto_eqclassI)

lemma (in pref_profile_wf) RSD_pareto_eqclass_insert:
  assumes "RSD_pareto_eqclass agents' alts R A" "finite alts"
          "i ∈ agents" "agents' ⊆ agents"
  shows   "RSD_pareto_eqclass (insert i agents') alts R (Max_wrt_among (R i) A)"
proof -
  from assms interpret total_preorder_on alts "R i" by simp
  show ?thesis
  proof (intro RSD_pareto_eqclassI Max_wrt_among_nonempty Max_wrt_among_subset, goal_cases)
    case (3 x y)
    with RSD_pareto_eqclassD[OF assms(1)] 
      show ?case unfolding Max_wrt_among_total_preorder 
      by (blast intro: trans)
  qed (insert RSD_pareto_eqclassD[OF assms(1)] assms(2), 
       simp_all add: Int_absorb1 Int_absorb2 finite_subset)[2]
qed


subsubsection ‹Facts about RSD winners›

context pref_profile_wf
begin

text ‹
  Any RSD winner is a valid alternative.  
›
lemma rsd_winners_subset:
  assumes "set agents' ⊆ agents" 
  shows   "rsd_winners R alts' agents' ⊆ alts'"
proof -
  {
    fix i assume "i ∈ agents"
    then interpret total_preorder_on alts "R i" by simp
    have "Max_wrt_among (R i) A ⊆ A" for A
      using Max_wrt_among_subset by blast
  } note A = this

  from ‹set agents' ⊆ agents› show "rsd_winners R alts' agents' ⊆ alts'"
    using A by (induction agents') auto
qed

text ‹
  There is always at least one RSD winner.  
›
lemma rsd_winners_nonempty:
  assumes finite: "finite alts"  and "alts' ≠ {}"  "set agents' ⊆ agents" "alts' ⊆ alts" 
  shows   "rsd_winners R alts' agents' ≠ {}"
proof -
  {
    fix i assume "i ∈ agents"
    then interpret total_preorder_on alts "R i" by simp
    have "Max_wrt_among (R i) A ≠ {}" if "A ⊆ alts" "A ≠ {}" for A
      using that assms by (intro Max_wrt_among_nonempty) (auto simp: Int_absorb)
  } note B = this

  with ‹set agents' ⊆ agents› ‹alts' ⊆ alts› ‹alts' ≠ {}› 
    show "rsd_winners R alts' agents' ≠ {}"
  proof (induction agents')
    case (Cons i agents')
    with B[of i "rsd_winners R alts' agents'"] rsd_winners_subset[of agents' alts'] finite wf
      show ?case by auto
  qed simp
qed

text ‹
  Obviously, the set of RSD winners is always finite.
›
lemma rsd_winners_finite: 
  assumes "set agents' ⊆ agents" "finite alts" "alts' ⊆ alts"
  shows   "finite (rsd_winners R alts' agents')"
  by (rule finite_subset[OF subset_trans[OF rsd_winners_subset]]) fact+

lemmas rsd_winners_wf = 
  rsd_winners_subset rsd_winners_nonempty rsd_winners_finite


text ‹
  The set of RSD winners is a Pareto-equivalence class.
›
lemma RSD_pareto_eqclass_rsd_winners_aux:
  assumes finite: "finite alts" and "alts ≠ {}" and "set agents' ⊆ agents"
  shows   "RSD_pareto_eqclass (set agents') alts R (rsd_winners R alts agents')"
  using ‹set agents' ⊆ agents›
proof (induction agents')
  case (Cons i agents')
  from Cons.prems show ?case
    by (simp only: set_simps rsd_winners_Cons,
        intro RSD_pareto_eqclass_insert[OF Cons.IH finite]) simp_all
qed (insert assms, simp_all)

lemma RSD_pareto_eqclass_rsd_winners:
  assumes finite: "finite alts" and "alts ≠ {}" and "set agents' = agents"
  shows   "RSD_pareto_eqclass agents alts R (rsd_winners R alts agents')"
  using RSD_pareto_eqclass_rsd_winners_aux[of agents'] assms by simp


text ‹
  For the proof of strategy-proofness, we need to define indifference sets
  and lift preference relations to sets in a specific way.
›
context
begin

text ‹
  An indifference set for a given preference relation is a non-empty set of alternatives 
  such that the agent is indifferent over all of them.
›
private definition indiff_set where
  "indiff_set S A ⟷ A ≠ {} ∧ (∀x∈A. ∀y∈A. S x y)"
  
private lemma indiff_set_mono: "indiff_set S A ⟹ B ⊆ A ⟹ B ≠ {} ⟹ indiff_set S B"
  unfolding indiff_set_def by blast

  
text ‹
  Given an arbitrary set of alternatives @{term A} and an indifference set @{term B},
  we say that @{term B} is set-preferred over @{term A} w.r.t. the preference 
  relation @{term R} if all (or, equivalently, any) of the alternatives in @{term B} 
  are preferred over all alternatives in @{term A}.
›
private definition RSD_set_rel where
  "RSD_set_rel S A B ⟷ indiff_set S B ∧ (∀x∈A. ∀y∈B. S x y)" 

text ‹
  The most-preferred alternatives (w.r.t. @{term R}) among any non-empty set of alternatives 
  form an indifference set w.r.t. @{term R}.
›
private lemma indiff_set_Max_wrt_among:
  assumes "finite carrier" "A ⊆ carrier" "A ≠ {}" "total_preorder_on carrier S" 
  shows   "indiff_set S (Max_wrt_among S A)"
  unfolding indiff_set_def
proof
  from assms(4) interpret total_preorder_on carrier S .
  from assms(1-3) 
    show "Max_wrt_among S A ≠ {}" by (intro Max_wrt_among_nonempty) auto
  from assms(1-3) show "∀x∈Max_wrt_among S A. ∀y∈Max_wrt_among S A. S x y"
    by (auto simp: indiff_set_def Max_wrt_among_total_preorder)
qed


text ‹
  We now consider the set of RSD winners in the setting of a preference profile @{term R}
  and a manipulated profile @{term "R(i := Ri')"}.
    This theorem shows that the set of RSD winners in the outcome is either the same
  in both cases or the outcome for the truthful profile is an indifference set that is
  set-preferred over the outcome for the manipulated profile.
›
lemma rsd_winners_manipulation_aux:
  assumes wf: "total_preorder_on alts Ri'"
      and i: "i ∈ agents" and "set agents' ⊆ agents" "finite agents" 
      and finite: "finite alts" and "alts ≠ {}"
  defines [simp]: "w' ≡ rsd_winners (R(i := Ri')) alts" and [simp]: "w ≡ rsd_winners R alts"
  shows   "w' agents' = w agents' ∨ RSD_set_rel (R i) (w' agents') (w agents')"
using ‹set agents' ⊆ agents›
proof (induction agents')
  case (Cons j agents')
  from wf i interpret Ri: total_preorder_on alts "R i" by simp
  from wf Cons.prems interpret Rj: total_preorder_on alts "R j" by simp
  from wf interpret Ri': total_preorder_on alts "Ri'" .
  from wf assms Cons.prems 
    have indiff_set: "indiff_set (R i) (Max_wrt_among (R i) (rsd_winners R alts agents'))"
    by (intro indiff_set_Max_wrt_among[OF finite] rsd_winners_wf) simp_all
        
  show ?case
  proof (cases "j = i")
    assume j [simp]: "j = i"
    from indiff_set Cons have "RSD_set_rel (R i) (w' (j # agents')) (w (j # agents'))"
      unfolding RSD_set_rel_def
      by (auto simp: Ri.Max_wrt_among_total_preorder Ri'.Max_wrt_among_total_preorder)
    thus ?case ..
  next
    assume j [simp]: "j ≠ i"
    from Cons have "w' agents' = w agents' ∨ RSD_set_rel (R i) (w' agents') (w agents')" by simp
    thus ?case
    proof
      assume rel: "RSD_set_rel (R i) (w' agents') (w agents')"
      hence indiff_set: "indiff_set (R i) (w agents')" by (simp add: RSD_set_rel_def)
      moreover from Cons.prems finite ‹alts ≠ {}› 
        have "w agents' ⊆ alts" "w agents' ≠ {}" unfolding w_def
        by (intro rsd_winners_wf; simp)+
      with finite have "Max_wrt_among (R j) (w agents') ≠ {}"
        by (intro Rj.Max_wrt_among_nonempty) auto
      ultimately have "indiff_set (R i) (w (j # agents'))"
        by (intro indiff_set_mono[OF indiff_set] Rj.Max_wrt_among_subset)
           (simp_all add: Rj.Max_wrt_among_subset)
      moreover from rel have "∀x∈w' (j # agents'). ∀y∈w (j # agents'). R i x y"
        by (auto simp: RSD_set_rel_def Rj.Max_wrt_among_total_preorder)
      ultimately have "RSD_set_rel (R i) (w' (j # agents')) (w (j # agents'))"
        unfolding RSD_set_rel_def ..
      thus ?case ..
    qed simp_all
  qed
qed simp_all


text ‹
  The following variant of the previous theorem is slightly easier to use.
  We eliminate the case where the two outcomes are the same by observing that
  the original outcome is then also set-preferred to the manipulated one.
    In essence, this means that no matter what manipulation is done, the 
  original outcome is always set-preferred to the manipulated one.
›
lemma rsd_winners_manipulation:
  assumes wf: "total_preorder_on alts Ri'"
      and i: "i ∈ agents" and "set agents' = agents" "finite agents" 
      and finite: "finite alts" and "alts ≠ {}"
  defines [simp]: "w' ≡ rsd_winners (R(i := Ri')) alts" and [simp]: "w ≡ rsd_winners R alts"
  shows   "∀x∈w' agents'. ∀y∈w agents'. x ≼[R i] y"
proof -
  have "w' agents' = w agents' ∨ RSD_set_rel (R i) (w' agents') (w agents')"
    using rsd_winners_manipulation_aux[OF assms(1-2) _ assms(4-6)] assms(3) by simp
  thus ?thesis
  proof
    assume eq: "w' agents' = w agents'"
    from assms have "RSD_pareto_eqclass (set agents') alts R (w agents')" unfolding w_def
      by (intro RSD_pareto_eqclass_rsd_winners_aux) simp_all
    from RSD_pareto_eqclass_indiff_set[OF this, of i] i eq assms(3) show ?thesis by auto
  qed (auto simp: RSD_set_rel_def)
qed

end


text ‹
  The lottery that RSD yields is well-defined.
›
lemma random_serial_dictatorship_support:
  assumes "finite agents" "finite alts" "agents' ⊆ agents" "alts' ≠ {}" "alts' ⊆ alts"
  shows   "set_pmf (random_serial_dictatorship agents' alts' R) ⊆ alts'"
proof -
  from assms have [simp]: "finite agents'" by (auto intro: finite_subset)
  have A: "set_pmf (pmf_of_set (rsd_winners R alts' agents'')) ⊆ alts'"
    if "agents'' ∈ permutations_of_set agents'" for agents''
    using that assms rsd_winners_wf[where alts' = alts' and agents' = agents'']
    by (auto simp: permutations_of_set_def)
  from assms show ?thesis
    by (auto dest!: A simp add: random_serial_dictatorship_altdef)
qed

text ‹
  Permutation of alternatives commutes with RSD winners.
›
lemma rsd_winners_permute_profile:
  assumes perm: "σ permutes alts" and "set agents' ⊆ agents" 
  shows   "rsd_winners (permute_profile σ R) alts agents' = σ ` rsd_winners R alts agents'"
  using ‹set agents' ⊆ agents›
proof (induction agents')
  case Nil
  from perm show ?case by (simp add: permutes_image)
next
  case (Cons i agents')
  from wf Cons interpret total_preorder_on alts "R i" by simp
  from perm Cons show ?case
    by (simp add: permute_profile_map_relation Max_wrt_among_map_relation_bij permutes_bij)
qed

lemma random_serial_dictatorship_singleton:
  assumes "finite agents" "finite alts" "agents' ⊆ agents" "x ∈ alts"
  shows   "random_serial_dictatorship agents' {x} R = return_pmf x" (is "?d = _")
proof -
  from assms have "set_pmf ?d ⊆ {x}" 
    by (intro random_serial_dictatorship_support) simp_all
  thus ?thesis by (simp add: set_pmf_subset_singleton)
qed

end


subsection ‹Proofs of properties›

text ‹
  With all the facts that we have proven about the RSD winners, the hard work is
  mostly done. We can now simply fix some arbitrary order of the agents, apply the 
  theorems about the RSD winners, and show the properties we want to show without 
  doing much reasoning about probabilities.
›

context election
begin     

abbreviation "RSD ≡ random_serial_dictatorship agents alts"

subsubsection ‹Well-definedness›

sublocale RSD: social_decision_scheme agents alts RSD
  using pref_profile_wf.random_serial_dictatorship_support[of agents alts]
  by unfold_locales (simp_all add: lotteries_on_def)


subsubsection ‹RD extension›

lemma RSD_extends_RD:
  assumes wf: "is_pref_profile R" and unique: "has_unique_favorites R"
  shows   "RSD R = RD R"
proof -
  from wf interpret pref_profile_wf agents alts R .
  from unique interpret pref_profile_unique_favorites by unfold_locales
  have "RSD R = pmf_of_set agents ⤜ 
                  (λi. random_serial_dictatorship (agents - {i}) (favorites R i) R)"
    by (simp add: random_serial_dictatorship_nonempty favorites_altdef Max_wrt_def)
  also from assms have "… = pmf_of_set agents ⤜ (λi. return_pmf (favorite R i))"
    by (intro bind_pmf_cong refl, subst random_serial_dictatorship_singleton [symmetric])
       (auto simp: unique_favorites favorite_in_alts)
  also from assms have "… = RD R"
    by (simp add: random_dictatorship_unique_favorites map_pmf_def)
  finally show ?thesis .
qed
  

subsubsection ‹Anonymity›

text ‹
  Anonymity is a direct consequence of the fact that we randomise over all
  permutations in a uniform way.
›

sublocale RSD: anonymous_sds agents alts RSD
proof
  fix π R assume perm: "π permutes agents" and wf: "is_pref_profile R"
  let ?f = "λagents'. pmf_of_set (rsd_winners R alts agents')"
  from perm wf have "RSD (R ∘ π) = map_pmf (map π) (pmf_of_set (permutations_of_set agents)) ⤜ ?f"
    by (simp add: random_serial_dictatorship_altdef bind_map_pmf)
  also from perm have "… = RSD R"
    by (simp add: map_pmf_of_set_inj permutes_inj_on inj_on_mapI
                  permutations_of_set_image_permutes random_serial_dictatorship_altdef)
  finally show "RSD (R ∘ π) = RSD R" .
qed


subsubsection ‹Neutrality›

text ‹
  Neutrality follows from the fact that the RSD winners of a permuted profile 
  are simply the image of the original RSD winners under the permutation.
›

sublocale RSD: neutral_sds agents alts RSD
proof
  fix σ R assume perm: "σ permutes alts" and wf: "is_pref_profile R"
  from wf interpret pref_profile_wf agents alts R .
  from perm show "RSD (permute_profile σ R) = map_pmf σ (RSD R)"
    by (auto intro!: bind_pmf_cong dest!: permutations_of_setD(1) 
             simp: random_serial_dictatorship_altdef rsd_winners_permute_profile
                   map_bind_pmf map_pmf_of_set_inj permutes_inj_on rsd_winners_wf)
qed


subsubsection ‹Ex-post efficiency›

text ‹
  Ex-post efficiency follows from the fact that the set of RSD winners 
  is a Pareto-equivalence class.
›

sublocale RSD: ex_post_efficient_sds agents alts RSD
proof
  fix R assume wf: "is_pref_profile R"
  then interpret pref_profile_wf agents alts R .
  {
    fix x assume x: "x ∈ set_pmf (RSD R)" "x ∈ pareto_losers R"
    from x(2) obtain y where [simp]: "y ∈ alts" and pareto: "y ≻[Pareto(R)] x" 
      by (cases rule: pareto_losersE)
    from x have [simp]: "x ∈ alts" using pareto_loser_in_alts by simp

    from x(1) obtain agents' where agents': "set agents' = agents" and 
        "x ∈ set_pmf (pmf_of_set (rsd_winners R alts agents'))"
      by (auto simp: random_serial_dictatorship_altdef dest: permutations_of_setD)
    with wf have x': "x ∈ rsd_winners R alts agents'"
      using rsd_winners_wf[where alts' = alts and agents' = agents']
      by (subst (asm) set_pmf_of_set) (auto simp: permutations_of_setD)

    from wf agents' 
      have "RSD_pareto_eqclass agents alts R (rsd_winners R alts agents')"
      by (intro RSD_pareto_eqclass_rsd_winners) simp_all
    hence winner_iff: "y ∈ rsd_winners R alts agents' ⟷ (∀i∈agents. x ≼[R i] y)"
      if "x ∈ rsd_winners R alts agents'" "y ∈ alts" for x y
      using that unfolding RSD_pareto_eqclass_def by blast
    from x' pareto winner_iff[of x y] winner_iff[of y x] have False
      by (force simp: strongly_preferred_def Pareto_iff)
  }
  thus "set_pmf (RSD R) ∩ pareto_losers R = {}" by blast
qed


subsubsection ‹Strong strategy-proofness›

text ‹
  Strong strategy-proofness is slightly more difficult to show. We have already shown
  that the set of RSD winners for the truthful profile is always set-preferred (by the
  manipulating agent) to the RSD winners for the manipulated profile.
    This can now be used to show strategy-proofness: We recall that the set of RSD 
  winners is always an indifference class. Therefore, given any fixed alternative @{term "x::'alt"}
  and considering a fixed order of the agents, either all of the RSD winners in the original
  profile are at least as good as @{term "x::'alt"} or none of them are, and, since the original 
  RSD winners are set-preferred to the manipulated ones, none of the RSD winners in the
  manipulated case are at least as good than @{term "x::'alt"} either in that case.
    This means that for a fixed order of agents, either the probability that the original  
  outcome is at least as good as @{term "x::'alt"} is 1 or the probability that the manipulated
  outcome is at least as good as @{term "x::'alt"} is 0.
    Therefore, the original lottery is clearly SD-preferred to the manipulated one.
›

sublocale RSD: strongly_strategyproof_sds agents alts RSD
proof (unfold_locales, rule)
  fix R i Ri' x
  assume wf: "is_pref_profile R" and i [simp]: "i ∈ agents" and x: "x ∈ alts" and
         wf': "total_preorder_on alts Ri'"
  interpret R: pref_profile_wf agents alts R by fact
  define R' where "R' = R (i := Ri')"
  from wf wf' have "is_pref_profile R'" by (simp add: R'_def R.wf_update)
  then interpret R': pref_profile_wf agents alts R' .
  note wf = wf wf'
  let ?A = "preferred_alts (R i) x"
  from wf interpret Ri: total_preorder_on alts "R i" by simp

  {
    fix agents' assume agents': "agents' ∈ permutations_of_set agents"
    from agents' have [simp]: "set agents' = agents"
      by (simp add: permutations_of_set_def)
      
    let ?W = "rsd_winners R alts agents'" and ?W' = "rsd_winners R' alts agents'"
    have indiff_set: "RSD_pareto_eqclass agents alts R ?W"
      by (rule R.RSD_pareto_eqclass_rsd_winners; simp add: wf)+
    from R.rsd_winners_wf R'.rsd_winners_wf
      have winners: "?W ⊆ alts" "?W ≠ {}" "finite ?W" "?W' ⊆ alts" "?W' ≠ {}" "finite ?W'"
      by simp_all
    
    from ‹?W ≠ {}› obtain y where y: "y ∈ ?W" by blast
    with winners have [simp]: "y ∈ alts" by blast
    from wf' i have mono: "∀x∈?W'. ∀y∈?W. R i x y" unfolding R'_def
      by (intro R.rsd_winners_manipulation) simp_all
    
    have "lottery_prob (pmf_of_set ?W) ?A ≥ lottery_prob (pmf_of_set ?W') ?A"
    proof (cases "y ≽[R i] x")
      case True
      with y RSD_pareto_eqclass_indiff_set[OF indiff_set(1), of i]  winners
        have "?W ⊆ preferred_alts (R i) x"
        by (auto intro: Ri.trans simp: preferred_alts_def)
      with winners show ?thesis
        by (subst (2) measure_pmf_of_set) (simp_all add: Int_absorb2)
    next
      case False
      with y mono have "?W' ∩ preferred_alts (R i) x = {}" 
        by (auto intro: Ri.trans simp: preferred_alts_def)
      with winners show ?thesis
        by (subst (1) measure_pmf_of_set)
           (simp_all add: Int_absorb2 one_ereal_def measure_nonneg)
    qed
    hence "emeasure (measure_pmf (pmf_of_set ?W)) ?A ≥ emeasure (measure_pmf (pmf_of_set ?W')) ?A"
      by (simp add: measure_pmf.emeasure_eq_measure)
  }
  hence "emeasure (measure_pmf (RSD R)) ?A ≥ emeasure (measure_pmf (RSD R')) ?A"
    by (auto simp: random_serial_dictatorship_altdef AE_measure_pmf_iff
             intro!: nn_integral_mono_AE)
  thus "lottery_prob (RSD R) ?A ≥ lottery_prob (RSD R') ?A" 
    by (simp add: measure_pmf.emeasure_eq_measure)
qed

end

end