Theory Anonymous_PAPP_Lowering

(*
  File:     Anonymous_PAPP_Lowering.thy
  Author:   Manuel Eberl, University of Innsbruck 
*)
section ‹Lowering P-APP Rules to Smaller Settings›
theory Anonymous_PAPP_Lowering
  imports Anonymous_PAPP
begin

text ‹
  In this section, we prove a number of lemmas (corresponding to Lemma~1 in the paper) that allow
  us to take an anonymous P-APP rule with some additional properties (typically
  Cardinality-Strategyproofness and Weak Representation or Weak Proportional Representation) and 
  construct from it an anonymous P-APP rule for a different setting, i.e.\ different number of
  voters, parties, and/or result committee size.

  In the reverse direction, this also allows us to lift impossibility results from one setting 
  to another.
›

subsection ‹Preliminary Lemmas›

context card_stratproof_anon_papp
begin

text ‹
  The following lemma is obtained by applying Strategyproofness repeatedly. It shows that
  if we have ‹l› voters with identical approval lists, then this entire group of voters has no
  incentive to submit wrong preferences. That is, the outcome they obtain by submitting their 
  genuine approval lists is weakly preferred by them over all outcomes obtained where these ‹l›
  voters submit any other preferences (and the remaining $n - l$ voters submit the same preferences
  as before).

  This is stronger than regular Strategyproofness, where we only demand that no voter has an
  incentive to submit wrong preferences ∗‹unilaterally› (and everyone else keeps the same
  preferences). Here we know that the entire group of ‹l› voters has no incentive to submit
  wrong preferences in coordination with one another.
›
lemma proposition2:
  assumes "size B = l" "size A + l = n_voters"
  assumes "X ≠ {}" "X ⊆ parties" "{} ∉# A+B" "∀X'∈#A+B. X' ⊆ parties"
  shows   "r (replicate_mset l X + A) ≽[Comm(X)] r (B + A)"
  using assms
proof (induction l arbitrary: A B)
  case 0
  thus ?case
    by simp
next
  case (Suc l A B)
  from Suc.prems have "set_mset B ≠ {}"
    by auto
  then obtain Y where Y: "Y ∈# B"
    by blast
  define B' where "B' = B - {#Y#}"
  define A' where "A' = A + {#Y#}"
  have [simp]: "size B' = l"
    using Suc.prems Y by (simp add: B'_def size_Diff_singleton)
  have [simp]: "size A' = n_voters - l"
    using Suc.prems Y by (simp add: A'_def)

  have "r (B' + A') ≼[Comm(X)] r (replicate_mset l X + A')"
    by (rule Suc.IH) (use Suc.prems Y in ‹auto simp: A'_def B'_def size_Diff_singleton›)
  also have "B' + A' = B + A"
    using Y by (simp add: B'_def A'_def)
  also have "r (replicate_mset l X + A') ≼[Comm(X)] r (replicate_mset (Suc l) X + A)"
  proof (rule not_manipulable'')
    show "replicate_mset (Suc l) X + A + {#Y#} = replicate_mset l X + A' + {#X#}"
      by (simp add: A'_def)
  next
    show "is_pref_profile (replicate_mset (Suc l) X + A)"
     using Suc.prems by unfold_locales (auto split: if_splits)
  next
    show "is_pref_profile (replicate_mset l X + A')"
      using Suc.prems Y by unfold_locales (auto split: if_splits simp: A'_def)
  qed
  finally show ?case .
qed

end


context card_stratproof_weak_rep_anon_papp
begin

text ‹
  In a setting with Weak Representation and Cardinality-Strategyproofness, Proposition 2 allows
  us to strengthen Weak Representation in the following way: Suppose we at least 
  $l \lfloor n/k\rfloor$ voters with the same approval list ‹X›, and ‹X› consists of at least ‹l›
  parties. Then at least ‹l› of the members of the result committee are in ‹X›.
›
lemma proposition3:
  assumes "is_pref_profile A" "X ⊆ parties" "card X ≥ l"
  assumes "committee_size > 0"
  assumes "count A X ≥ l * ⌈n_voters / committee_size⌉"
  shows   "size {# x∈# r A. x ∈ X #} ≥ l"
  using assms
proof (induction l arbitrary: A X rule: less_induct)
  case (less l A X)
  interpret A: anon_papp_profile n_voters parties committee_size A
    by fact
  consider "l = 0" | "l = 1" | "l > 1"
    by force
  thus ?case
  proof cases
    assume "l = 0"
    thus ?thesis by simp
  next
    assume [simp]: "l = 1"
    define n where "n = count A X"
    with less.prems have "X ≠ {}"
      by auto
    then obtain x where x: "x ∈ X"
      by blast
    have "n ≤ size A"
      unfolding n_def by (rule count_le_size)
    hence "n ≤ n_voters"
      by (simp add: A.size_A)

    have "count A X > 0"
      by (rule Nat.gr0I) (use n_voters_pos less.prems in ‹auto simp: field_simps›)
    hence "X ∈# A"
      by force
    have [simp]: "replicate_mset n X ⊆# A"
      by (simp add: n_def flip: count_le_replicate_mset_subset_eq)

    define A'' where "A'' = A - replicate_mset n X"
    define A' where "A' = A'' + replicate_mset n {x}"
    interpret A': anon_papp_profile n_voters parties committee_size A'
      using A.A_nonempty A.A_subset A.size_A x ‹X ∈# A›
      by unfold_locales
         (fastforce simp: A'_def A''_def size_Diff_submset subset_mset.add_increasing2 
                    split: if_splits dest!: in_diffD)+

    have "x ∈# r A'"
    proof (rule weak_representation)
      show "is_pref_profile A'"
        by (fact A'.anon_papp_profile_axioms)
    next
      have "n_voters ≤ committee_size * n"
        using less.prems by (simp add: n_def ceiling_le_iff field_simps flip: of_nat_mult)
      also have "n ≤ count A' {x}"
        by (simp add: A'_def)
      finally show "n_voters ≤ committee_size * count A' {x}"
        by simp
    qed
    hence "1 ≤ count (r A') x"
      by simp
    also have "… = size {# y ∈# r A'. y = x #}"
      by simp
    also have "… ≤ size {# y ∈# r A'. y ∈ X #}"
      by (intro size_mset_mono multiset_filter_mono') (use x in auto)

    also have "r A' ≼[Comm(X)] r A"
    proof -
      have "r (replicate_mset n {x} + A'') ≼[Comm(X)] r (replicate_mset n X + A'')"
      proof (rule proposition2)
        show "{} ∉# A'' + replicate_mset n {x}"
          using A'.A_nonempty by (auto simp: A'_def)
        show "∀X'∈#A'' + replicate_mset n {x}. X' ⊆ parties"
          using A'.A_subset x by (auto simp: A'_def dest: in_diffD)
        show "size A'' + n = n_voters"
          using ‹n ≤ n_voters› by (auto simp: A''_def size_Diff_submset A.size_A)
      qed (use less.prems in auto)
      also have "replicate_mset n X + A'' = A"
        by (simp add: A''_def n_def flip: count_le_replicate_mset_subset_eq)
      finally show ?thesis
        by (simp add: A'_def add_ac)
    qed
    hence "size {# y ∈# r A'. y ∈ X #} ≤ size {# y ∈# r A. y ∈ X #}"
      by (simp add: committee_preference_def)

    finally show ?thesis
      by simp

  next
    assume l: "l > 1"
    
    define n where "n = count A X"
    have "n ≤ size A"
      unfolding n_def by (rule count_le_size)
    hence "n ≤ n_voters"
      by (simp add: A.size_A)

    define m where "m = nat (ceiling (n_voters / committee_size))"
    have "n_voters / committee_size ≤ m"
      unfolding m_def by linarith
    hence m: "n_voters ≤ committee_size * m"
      using ‹committee_size > 0› by (simp add: field_simps flip: of_nat_mult)
    have "real n_voters / real committee_size > 0"
      using n_voters_pos less.prems by auto
    hence m': "⌈real n_voters / real committee_size⌉ = int m"
      by (simp add: m_def)
    have "1 * m ≤ l * m"
      using l by (intro mult_right_mono) auto
    also have "l * m ≤ n"
      using less.prems by (simp add: m' n_def flip: of_nat_mult)
    finally have "m ≤ n"
      by simp

    with less.prems l have "X ≠ {}"
      by auto
    then obtain x where x: "x ∈ X"
      by blast
    have "card (X - {x}) > 0"
      using less.prems x l by simp
    hence "X - {x} ≠ {}"
      by force

    have "count A X > 0"
      by (rule Nat.gr0I) (use n_voters_pos less.prems l in ‹auto simp: field_simps mult_le_0_iff›)
    hence "X ∈# A"
      by force
    have [simp]: "replicate_mset n X ⊆# A"
      by (simp add: n_def flip: count_le_replicate_mset_subset_eq)

    define A'' where "A'' = A - replicate_mset n X"
    define A' where "A' = A'' + replicate_mset m {x} + replicate_mset (n - m) (X - {x})"
    interpret A': anon_papp_profile n_voters parties committee_size A'
    proof
      show "Y ⊆ parties" if "Y ∈# A'" for Y
        using that A.A_subset x ‹X ∈# A›
        by (fastforce simp: A'_def A''_def dest!: in_diffD split: if_splits)
    next
      show "{} ∉# A'"
        using A.A_nonempty x ‹X ∈# A› ‹X - {x} ≠ {}›
        by (auto simp: A'_def A''_def dest!: in_diffD split: if_splits)
    next
      show "size A' = n_voters"
        using ‹m ≤ n›
        by (auto simp: A'_def A''_def A.size_A subset_mset.add_increasing2 size_Diff_submset)
    qed

    have "x ∈# r A'"
    proof (rule weak_representation)
      show "is_pref_profile A'"
        by (fact A'.anon_papp_profile_axioms)
    next
      have "n_voters ≤ committee_size * m"
        by (fact m)
      also have "m ≤ count A' {x}"
        by (simp add: A'_def)
      finally show "n_voters ≤ committee_size * count A' {x}"
        by simp
    qed
    hence "1 ≤ count (r A') x"
      by simp
    also have "… = size {# y ∈# r A'. y = x #}"
      by simp
    finally have 1: "size {#y ∈# r A'. y = x#} ≥ 1" .

    have 2: "size {# y ∈# r A'. y ∈ X - {x} #} ≥ l - 1"
    proof (rule less.IH)
      have "int (l - 1) * ⌈real n_voters / real committee_size⌉ = int ((l - 1) * m)"
        by (auto simp add: m' not_less)
      also have "(l - 1) * m = l * m - m"
        by (simp add: algebra_simps)
      also have "l * m ≤ n"
        using less.prems by (simp add: m' n_def flip: of_nat_mult)
      hence "l * m - m ≤ n - m"
        by (meson diff_le_mono)
      also have "n - m ≤ count A' (X - {x})"
        by (simp add: A'_def A''_def)
      finally show "int (l - 1) * ⌈real n_voters / real committee_size⌉ ≤ int (count A' (X - {x}))"
        by simp
    qed (use l A'.anon_papp_profile_axioms x less.prems in ‹auto›)

    have "1 + (l - 1) ≤ size {#y ∈# r A'. y = x#} + size {#y ∈# r A'. y ∈ X - {x}#}"
      by (intro add_mono 1 2)
    also have "… = size ({#y ∈# r A'. y = x#} + {#y ∈# r A'. y ∈ X - {x}#})"
      by simp
    also have "{#y ∈# r A'. y = x#} + {#y ∈# r A'. y ∈ X - {x}#} =
               {#y ∈# r A'. y = x ∨ y ∈ X - {x}#}"
      by (rule filter_mset_disjunction [symmetric]) auto
    also have "(λy. y = x ∨ y ∈ X - {x}) = (λy. y ∈ X)"
      using x by auto
    also have "1 + (l - 1) = l"
      using l by simp

    also have "r A' ≼[Comm(X)] r A"
    proof -
      have "r (replicate_mset m {x} + replicate_mset (n - m) (X - {x}) + A'') ≼[Comm(X)] 
            r (replicate_mset n X + A'')"
      proof (rule proposition2)
        show " {} ∉# A'' + (replicate_mset m {x} + replicate_mset (n - m) (X - {x}))"
          using A'.A_nonempty by (auto simp: A'_def)
        show "∀X'∈# A'' + (replicate_mset m {x} + replicate_mset (n - m) (X - {x})). X' ⊆ parties"
          using A'.A_subset x by (auto simp: A'_def dest: in_diffD)
        show "size A'' + n = n_voters"
          using ‹n ≤ n_voters› by (auto simp: A''_def size_Diff_submset A.size_A)
      qed (use less.prems l ‹m ≤ n› in auto)
      also have "replicate_mset n X + A'' = A"
        by (simp add: A''_def n_def flip: count_le_replicate_mset_subset_eq)
      finally show ?thesis
        by (simp add: A'_def add_ac)
    qed
    hence "size {# y ∈# r A'. y ∈ X #} ≤ size {# y ∈# r A. y ∈ X #}"
      by (simp add: committee_preference_def)

    finally show ?thesis
      by simp
  qed
qed

end


subsection ‹Dividing the number of voters›

text ‹
  If we have a PAPP rule that satisfies weak representation and cardinality strategyproofness,
  for $ln$ voters, we can turn it into one for ‹n› voters.
  This is done by simply cloning each voter ‹l› times.

  Consequently, if we have an impossibility result for $n$ voters, it also holds for any
  integer multiple of ‹n›.
›
locale divide_voters_card_stratproof_weak_rep_anon_papp =
  card_stratproof_weak_rep_anon_papp "l * n_voters" parties committee_size r
  for l n_voters parties committee_size r
begin

definition lift_profile :: "'a set multiset ⇒ 'a set multiset" where
  "lift_profile A = (∑X∈#A. replicate_mset l X)"

sublocale lowered: anon_papp_election n_voters parties
  by standard (use n_voters_pos in auto)

lemma l_pos: "l > 0"
  using n_voters_pos by auto

lemma empty_in_lift_profile_iff [simp]: "{} ∈# lift_profile A ⟷ {} ∈# A"
  using l_pos by (auto simp: lift_profile_def)

lemma set_mset_lift_profile [simp]: "set_mset (lift_profile A) = set_mset A"
  using l_pos by (auto simp: lift_profile_def)

lemma size_lift_profile: "size (lift_profile A) = l * size A"
  by (simp add: size_mset_sum_mset lift_profile_def image_mset.compositionality o_def)

lemma count_lift_profile [simp]: "count (lift_profile A) x = l * count A x"
  unfolding lift_profile_def by (induction A) auto

lemma is_pref_profile_lift_profile [intro]:
  assumes "lowered.is_pref_profile A"
  shows   "is_pref_profile (lift_profile A)"
proof -
  interpret anon_papp_profile n_voters parties committee_size A
    by fact
  show ?thesis
    using A_nonempty A_subset size_A
    by unfold_locales
       (auto simp: lift_profile_def size_mset_sum_mset image_mset.compositionality o_def)
qed

sublocale lowered: anon_papp n_voters parties committee_size "r ∘ lift_profile"
proof
  fix A assume "lowered.is_pref_profile A"
  hence "is_pref_profile (lift_profile A)"
    by blast
  hence "is_committee (r (lift_profile A))"
    using rule_wf by blast
  thus "lowered.is_committee ((r ∘ lift_profile) A)"
    by simp
qed

sublocale lowered: weak_rep_anon_papp n_voters parties committee_size "r ∘ lift_profile"
proof
  fix A x
  assume A: "lowered.is_pref_profile A" and x: "n_voters ≤ committee_size * count A {x}"
  from A have A': "is_pref_profile (lift_profile A)"
    by blast
  from x have "l * n_voters ≤ l * (committee_size * count A {x})"
    by (rule mult_left_mono) auto
  also have "… = committee_size * count (lift_profile A) {x}"
    by simp
  finally have "x ∈# r (lift_profile A)"
    by (intro weak_representation A')
  thus "x ∈# (r ∘ lift_profile) A"
    by simp
qed

sublocale lowered: card_stratproof_anon_papp n_voters parties committee_size "r ∘ lift_profile"
proof
  fix A X Y
  show "¬lowered.card_manipulable A X Y"
    unfolding lowered.card_manipulable_def
  proof (rule notI, elim conjE)
    assume A: "lowered.is_pref_profile A" and XY: "X ∈# A" "Y ≠ {}" "Y ⊆ parties"
    assume *: "(r ∘ lift_profile) A ≺[lowered.committee_preference X] 
               (r ∘ lift_profile) (A - {#X#} + {#Y#})"
    interpret anon_papp_profile n_voters parties committee_size A
      by fact
    have X: "X ≠ {}" "X ⊆ parties"
      using XY A_nonempty A_subset by auto

    define A' where "A' = A - {#X#}"
    have A': "A = A' + {#X#}"
      using XY by (simp add: A'_def)

    have "r (lift_profile A) ≺[committee_preference X]
          r (lift_profile (A - {#X#} + {#Y#}))"
      using * by simp
    also have "r (lift_profile (A - {#X#} + {#Y#})) ≼[committee_preference X]
               r (lift_profile A - {#X#} + {#Y#})"
    proof -
      have "r (replicate_mset (l - 1) Y + (lift_profile A' + {#Y#})) ≼[committee_preference X]
            r (replicate_mset (l - 1) X + (lift_profile A' + {#Y#}))"
      proof (rule proposition2)
        show "size (lift_profile A' + {#Y#}) + (l - 1) = l * n_voters"
          using XY l_pos n_voters_pos
          by (simp add: A'_def size_lift_profile size_Diff_singleton 
                        algebra_simps Suc_diff_le size_A)
      next
        show "{} ∉# lift_profile A' + {#Y#} + replicate_mset (l - 1) Y"
          using XY A_nonempty by (auto simp: A'_def dest: in_diffD)
      next
        show "∀X'∈#lift_profile A' + {#Y#} + replicate_mset (l - 1) Y. X' ⊆ parties"
          using XY A_subset by (auto simp: A'_def dest: in_diffD)
      qed (use X in auto)
      thus ?thesis
        by (simp add: A' replicate_mset_rec l_pos lift_profile_def)
    qed
    finally have "card_manipulable (lift_profile A) X Y"
      unfolding card_manipulable_def using XY A by auto
    with not_manipulable show False
      by blast
  qed
qed

sublocale lowered: card_stratproof_weak_rep_anon_papp n_voters parties committee_size "r ∘ lift_profile"
  ..

end


locale divide_voters_card_stratproof_weak_prop_rep_anon_papp =
  card_stratproof_weak_prop_rep_anon_papp "l * n_voters" parties committee_size r
  for l n_voters parties committee_size r
begin

sublocale divide_voters_card_stratproof_weak_rep_anon_papp ..

sublocale lowered: card_stratproof_weak_prop_rep_anon_papp
  n_voters parties committee_size "r ∘ lift_profile"
proof
  fix A x l'
  assume A: "lowered.is_pref_profile A" and x: "l' * n_voters ≤ committee_size * count A {x}"
  from A have A': "is_pref_profile (lift_profile A)"
    by blast
  from x have "l * (l' * n_voters) ≤ l * (committee_size * count A {x})"
    by (rule mult_left_mono) auto
  also have "… = committee_size * count (lift_profile A) {x}"
    by simp
  also have "l * (l' * n_voters) = l' * (l * n_voters)"
    by (simp add: algebra_simps)
  finally have "count (r (lift_profile A)) x ≥ l'"
    by (intro weak_proportional_representation A')
  thus "count ((r ∘ lift_profile) A) x ≥ l'"
    by simp
qed

end



subsection ‹Decreasing the number of parties›

text ‹
  If we have a PAPP rule that satisfies weak representation and cardinality strategyproofness,
  for $m$ parties, we can turn it into one for $m-1$ parties. This is done by simply
  duplicating one particular party (say ‹x›) in the preference profile, i.e.\ whenever
  ‹x› is part of an approval list, we add a clone of ‹x› (say ‹y›) as well. Should ‹y› then end up
  in the committee, we simply replace it with ‹x›.

  Consequently, if we have an impossibility result for $k$ parties, it also holds for
  $\geq m$ parties.
›
locale remove_alt_card_stratproof_weak_rep_anon_papp =
  card_stratproof_weak_rep_anon_papp n_voters parties committee_size r
  for n_voters and parties :: "'a set" and committee_size r +
  fixes x y :: 'a
  assumes xy: "x ∈ parties" "y ∈ parties" "x ≠ y"
begin

definition lift_applist :: "'a set ⇒ 'a set" where
  "lift_applist X = (if x ∈ X then insert y X else X)"

definition lift_profile :: "'a set multiset ⇒ 'a set multiset" where
  "lift_profile A = image_mset lift_applist A"

definition lower_result where "lower_result C = image_mset (λz. if z = y then x else z) C"

definition lowered where "lowered = lower_result ∘ r ∘ lift_profile"


lemma lift_profile_empty [simp]: "lift_profile {#} = {#}"
  by (simp add: lift_profile_def)

lemma lift_profile_add_mset [simp]:
  "lift_profile (add_mset X A) = add_mset (lift_applist X) (lift_profile A)"
  by (simp add: lift_profile_def)

lemma empty_in_lift_profile_iff [simp]: "{} ∈# lift_profile A ⟷ {} ∈# A"
  by (auto simp: lift_applist_def lift_profile_def)

lemma size_lift_profile [simp]: "size (lift_profile A) = size A"
  by (simp add: lift_profile_def)

lemma lift_applist_eq_self_iff [simp]: "lift_applist X = X ⟷ x ∉ X ∨ y ∈ X"
  by (auto simp: lift_applist_def)

lemma lift_applist_eq_self_iff' [simp]: "lift_applist (X - {y}) = X ⟷ (x ∈ X ⟷ y ∈ X)"
  by (cases "y ∈ X") (auto simp: lift_applist_def xy)

lemma in_lift_applist_iff: "z ∈ lift_applist X ⟷ z ∈ X ∨ (z = y ∧ x ∈ X)"
  by (auto simp: lift_applist_def)

lemma count_lift_profile:
  assumes "∀Y∈#A. y ∉ Y"
  shows   "count (lift_profile A) X = (if x ∈ X ⟷ y ∈ X then count A (X - {y}) else 0)"
  using assms xy by (induction A) (auto simp: lift_applist_def)

lemma y_notin_lower_result [simp]: "y ∉# lower_result C"
  using xy by (auto simp: lower_result_def)

lemma lower_result_subset: "set_mset (lower_result C) ⊆ insert x (set_mset C - {y})"
  using xy by (auto simp: lower_result_def)

lemma lower_result_subset': "set_mset C ⊆ parties ⟹ set_mset (lower_result C) ⊆ parties"
  using xy by (auto simp: lower_result_def)

lemma size_lower_result [simp]: "size (lower_result C) = size C"
  by (simp add: lower_result_def)

lemma count_lower_result:
  "count (lower_result C) z =
     (if z = y then 0
      else if z = x then count C x + count C y
      else count C z)"
  using xy by (induction C) (auto simp: lower_result_def)

lemma in_lower_result_iff:
  "z ∈# lower_result C ⟷ z ≠ y ∧ (z ∈# C ∨ (z = x ∧ y ∈# C))"
  unfolding lower_result_def using xy by (induction C) auto


sublocale lowered: anon_papp_election n_voters "parties - {y}"
  by standard (use n_voters_pos xy in auto)

lemma is_pref_profile_lift_profile [intro]:
  assumes "lowered.is_pref_profile A"
  shows   "is_pref_profile (lift_profile A)"
proof -
  interpret anon_papp_profile n_voters "parties - {y}" committee_size A
    by fact
  show ?thesis
    using A_nonempty A_subset size_A
    by unfold_locales
       (auto simp: lift_profile_def lift_applist_def xy 
                   size_mset_sum_mset image_mset.compositionality o_def)
qed

sublocale lowered: anon_papp n_voters "parties - {y}" committee_size lowered
proof
  fix A assume "lowered.is_pref_profile A"
  hence "is_pref_profile (lift_profile A)"
    by blast
  hence "is_committee (r (lift_profile A))"
    using rule_wf by blast
  thus "lowered.is_committee (lowered A)"
    unfolding lowered.is_committee_def is_committee_def lowered_def
    using lower_result_subset'[of "r (lift_profile A)"] by auto
qed

sublocale lowered: weak_rep_anon_papp n_voters "parties - {y}" committee_size lowered
proof
  fix A z
  assume A: "lowered.is_pref_profile A" and z: "n_voters ≤ committee_size * count A {z}"
  interpret A: anon_papp_profile n_voters "parties - {y}" committee_size A
    by fact
  have "committee_size > 0"
    using z n_voters_pos by (intro Nat.gr0I) auto

  from A have A': "is_pref_profile (lift_profile A)"
    by blast
  have "count A {z} > 0"
    using z n_voters_pos by (intro Nat.gr0I) auto
  hence "{z} ∈# A"
    by simp
  hence z': "z ∈ parties - {y}"
    using A.A_subset z by auto

  define C where "C = r (lift_profile A)"

  show "z ∈# lowered A"
  proof (cases "z = x")
    case False
    have "n_voters ≤ committee_size * count A {z}"
      by fact
    also have "count A {z} ≤ count (lift_profile A) {z}"
      using A.A_subset z' False by (subst count_lift_profile) auto
    hence "committee_size * count A {z} ≤ committee_size * count (lift_profile A) {z}"
      by (intro mult_left_mono) auto
    finally have "z ∈# r (lift_profile A)"
      by (intro weak_representation A')
    thus "z ∈# lowered A"
      using False z' by (simp add: lowered_def in_lower_result_iff)
  next
    case [simp]: True
    have "1 ≤ size {#z ∈# C. z ∈ {x, y}#}"
      unfolding C_def
    proof (rule proposition3)
      have [simp]: "{x, y} - {y} = {x}"
        using xy by auto
      hence "n_voters ≤ committee_size * count (lift_profile A) {x, y}"
        using xy A.A_subset z by (subst count_lift_profile) auto
      thus "int 1 * ⌈real n_voters / real committee_size⌉ ≤ int (count (lift_profile A) {x, y})"
        using ‹committee_size > 0›
        by (auto simp: ceiling_le_iff field_simps simp flip: of_nat_mult)
    qed (use A' xy ‹committee_size > 0› in auto)
    also have "… = count C x + count C y"
      using xy by (induction C) auto
    also have "… = count (lowered A) x"
      using xy by (simp add: lowered_def count_lower_result C_def)
    finally show "z ∈# lowered A"
      by simp
  qed
qed

lemma filter_lower_result_eq:
  "y ∉ X ⟹ {#x ∈# lower_result C. x ∈ X#} = lower_result {#x ∈# C. x ∈ lift_applist X#}"
  by (induction C) (auto simp: lower_result_def lift_applist_def)

sublocale lowered: card_stratproof_anon_papp n_voters "parties - {y}" committee_size lowered
proof
  fix A X Y
  show "¬lowered.card_manipulable A X Y"
    unfolding lowered.card_manipulable_def
  proof (rule notI, elim conjE)
    assume A: "lowered.is_pref_profile A" and XY: "X ∈# A" "Y ≠ {}" "Y ⊆ parties - {y}"
    assume *: "lowered A ≺[lowered.committee_preference X] lowered (A - {#X#} + {#Y#})"
    interpret anon_papp_profile n_voters "parties - {y}" committee_size A
      by fact
    have X: "X ≠ {}" "X ⊆ parties - {y}"
      using XY A_nonempty A_subset by auto
    define A' where "A' = A - {#X#}"
    have A': "A = A' + {#X#}"
      using XY by (simp add: A'_def)

    from * have "size {#x ∈# lower_result (r (lift_profile A' + {#lift_applist X#})). x ∈ X#} <
                 size {#x ∈# lower_result (r (lift_profile A' + {#lift_applist Y#})). x ∈ X#}"
      by (simp add: lowered_def A' lowered.strong_committee_preference_iff)
    also have "{#x ∈# lower_result (r (lift_profile A' + {#lift_applist X#})). x ∈ X#} =
               lower_result {#x ∈# r (lift_profile A' + {#lift_applist X#}). x ∈ lift_applist X#}"
      using X by (subst filter_lower_result_eq) auto
    also have "{#x ∈# lower_result (r (lift_profile A' + {#lift_applist Y#})). x ∈ X#} =
               lower_result {#x ∈# r (lift_profile A' + {#lift_applist Y#}). x ∈ lift_applist X#}"
      using X by (subst filter_lower_result_eq) auto
    finally have "size {#x ∈# r (lift_profile A' + {#lift_applist X#}). x ∈ lift_applist X#} <
                  size {#x ∈# r (lift_profile A' + {#lift_applist Y#}). x ∈ lift_applist X#}"
      by simp
    hence "r (lift_profile A' + {#lift_applist X#}) ≺[committee_preference (lift_applist X)]
           r (lift_profile A' + {#lift_applist Y#})"
      by (simp add: strong_committee_preference_iff)
    moreover have "¬r (lift_profile A' + {#lift_applist X#}) ≺[committee_preference (lift_applist X)]
                    r (lift_profile A' + {#lift_applist Y#})"
    proof (rule not_manipulable' [where Y = "lift_applist Y"])
      have "is_pref_profile (lift_profile A)"
        using A by blast
      thus "is_pref_profile (lift_profile A' + {#lift_applist X#})"
        using A by (simp add: A')
    next
      have "is_pref_profile (lift_profile (A - {#X#} + {#Y#}))"
        using A  XY lowered.is_pref_profile_replace by blast
      thus "is_pref_profile (lift_profile A' + {#lift_applist Y#})"
        by (simp add: A')
    qed auto
    ultimately show False
      by contradiction
  qed
qed

sublocale lowered: card_stratproof_weak_rep_anon_papp n_voters "parties - {y}" committee_size lowered
  ..

end


text ‹
  The following lemma is now simply an iterated application of the above. This allows us to
  restrict a P-APP rule to any non-empty subset of parties.
›
lemma card_stratproof_weak_rep_anon_papp_restrict_parties:
  assumes "card_stratproof_weak_rep_anon_papp n parties k r" "parties' ⊆ parties" "parties' ≠ {}"
  shows   "∃r. card_stratproof_weak_rep_anon_papp n parties' k r"
proof -
  have "finite parties"
  proof -
    interpret card_stratproof_weak_rep_anon_papp n parties k r
      by fact
    show ?thesis
      by (rule finite_parties)
  qed
  thus ?thesis
    using assms
  proof (induction parties arbitrary: r rule: finite_psubset_induct)
    case (psubset parties r)
    show ?thesis
    proof (cases "parties = parties'")
      case True
      thus ?thesis
        using psubset.prems by auto
    next
      case False
      obtain x where x: "x ∈ parties'"
        using psubset.prems by blast
      from False and psubset.prems have "parties - parties' ≠ {}"
        by auto
      then obtain y where y: "y ∈ parties - parties'"
        by blast

      interpret card_stratproof_weak_rep_anon_papp n parties k r
        by fact
      interpret remove_alt_card_stratproof_weak_rep_anon_papp n parties k r x y
        by standard (use x y psubset.prems in auto)
      show ?thesis
      proof (rule psubset.IH)
        show "parties - {y} ⊂ parties" and "parties' ⊆ parties - {y}" "parties' ≠ {}"
          using x y psubset.prems by auto
      next
        show "card_stratproof_weak_rep_anon_papp n (parties - {y}) k lowered"
          using lowered.card_stratproof_weak_rep_anon_papp_axioms .
      qed
    qed
  qed
qed



subsection ‹Decreasing the committee size›

text ‹
  If we have a PAPP rule that satisfies weak representation and cardinality strategyproofness,
  for $l(k+1)$ voters, $m+1$ parties, and a committee size of $k+1$, we can turn it into
  one for $lk$ voters, $m$ parties, and a committee size of $k$.

  This is done by again cloning a party ‹x› into a new party ‹y› and additionally
  adding ‹l› new voters whose preferences are ‹{x, y}›. We again replace any ‹y› occuring in the
  output committee with ‹x›. Weak representation then ensures that ‹x› occurs in the output
  at least once, and we then simply remove one ‹x› from the committee to obtain an output
  committee of size ‹k - 1›.

  Consequently, if we have an impossibility result for a committee size of $m$, we can
  extend it to a larger committee size, but at the cost of introducing a new party
  and new voters, and with a restriction on the number of voters.
›
(* n / k = l *)
locale decrease_committee_card_stratproof_weak_rep_anon_papp =
  card_stratproof_weak_rep_anon_papp "l * (k + 1)" "insert y parties" "k + 1" r
  for l k y and parties :: "'a set" and r +
  fixes x :: 'a
  assumes xy: "x ∈ parties" "y ∉ parties"
  assumes k: "k > 0"
begin

definition lift_applist :: "'a set ⇒ 'a set" where
  "lift_applist X = (if x ∈ X then insert y X else X)"

definition lift_profile :: "'a set multiset ⇒ 'a set multiset" where
  "lift_profile A = image_mset lift_applist A + replicate_mset l {x, y}"

definition lower_result
  where "lower_result C = image_mset (λz. if z = y then x else z) C - {#x#}"

definition lowered where "lowered = lower_result ∘ r ∘ lift_profile"


lemma l: "l > 0"
  using n_voters_pos by auto

lemma x_neq_y [simp]: "x ≠ y" "y ≠ x"
  using xy by auto

lemma lift_profile_empty [simp]: "lift_profile {#} = replicate_mset l {x, y}"
  by (simp add: lift_profile_def)

lemma lift_profile_add_mset [simp]:
  "lift_profile (add_mset X A) = add_mset (lift_applist X) (lift_profile A)"
  by (simp add: lift_profile_def)

lemma empty_in_lift_profile_iff [simp]: "{} ∈# lift_profile A ⟷ {} ∈# A"
  by (auto simp: lift_applist_def lift_profile_def)

lemma size_lift_profile [simp]: "size (lift_profile A) = size A + l"
  by (simp add: lift_profile_def)

lemma lift_applist_eq_self_iff [simp]: "lift_applist X = X ⟷ x ∉ X ∨ y ∈ X"
  by (auto simp: lift_applist_def)

lemma lift_applist_eq_self_iff' [simp]: "lift_applist (X - {y}) = X ⟷ (x ∈ X ⟷ y ∈ X)"
  by (cases "y ∈ X") (auto simp: lift_applist_def xy)

lemma in_lift_applist_iff: "z ∈ lift_applist X ⟷ z ∈ X ∨ (z = y ∧ x ∈ X)"
  by (auto simp: lift_applist_def)

lemma count_lift_profile:
  assumes "∀Y∈#A. y ∉ Y"
  shows   "count (lift_profile A) X =
             (if x ∈ X ⟷ y ∈ X then count A (X - {y}) else 0) +
             (if X = {x, y} then l else 0)"
  using assms xy by (induction A) (auto simp: lift_applist_def)



lemma y_notin_lower_result [simp]: "y ∉# lower_result C"
  using xy by (auto simp: lower_result_def dest: in_diffD)

lemma lower_result_subset: "set_mset (lower_result C) ⊆ insert x (set_mset C - {y})"
  using xy by (auto simp: lower_result_def dest: in_diffD)

lemma lower_result_subset': "set_mset C ⊆ insert y parties ⟹ set_mset (lower_result C) ⊆ parties"
  by (rule order.trans[OF lower_result_subset]) (use xy in auto)

lemma size_lower_result [simp]:
  assumes "x ∈# C ∨ y ∈# C"
  shows   "size (lower_result C) = size C - 1"
  using assms by (auto simp: lower_result_def size_Diff_singleton)

lemma size_lower_result': "size (lower_result C) = size C - (if x ∈# C ∨ y ∈# C then 1 else 0)"
proof -
  define f where "f = (λC. image_mset (λz. if z = y then x else z) C)"
  have "size (lower_result C) = size (f C - {#x#})"
    by (simp add: lower_result_def f_def)
  also have "… = size (f C) - (if x ∈# f C then 1 else 0)"
    by (simp add: diff_single_trivial size_Diff_singleton)
  finally show ?thesis
    by (auto simp: f_def)
qed

lemma count_lower_result:
  "count (lower_result C) z =
     (if z = y then 0
      else if z = x then count C x + count C y - 1
      else count C z)" (is "_ = ?rhs")
proof -
  define f where "f = (λC. image_mset (λz. if z = y then x else z) C)"
  have "count (lower_result C) z = count (f C - {#x#}) z"
    by (simp add: lower_result_def f_def)
  also have "… = count (f C) z - (if z = x then 1 else 0)"
    by auto
  also have "count (f C) z = (if z = y then 0 else if z = x then count C x + count C y else count C z)"
    using xy by (induction C)  (auto simp: f_def)
  also have "… - (if z = x then 1 else 0) = ?rhs"
    by auto
  finally show ?thesis .
qed

lemma in_lower_resultD:
  "z ∈# lower_result C ⟹ z = x ∨ z ∈# C"
  using xy by (auto simp: lower_result_def dest!: in_diffD)

lemma in_lower_result_iff:
  "z ∈# lower_result C ⟷ z ≠ y ∧ (if z = x then count C x + count C y > 1 else z ∈# C)"
  (is "_ = ?rhs")
proof -
  have "z ∈# lower_result C ⟷ count (lower_result C) z > 0"
    by auto
  also have "… ⟷ ?rhs"
    by (subst count_lower_result) auto
  finally show ?thesis .
qed

lemma filter_lower_result_eq:
  assumes "y ∉ X"
  shows   "{#z ∈# lower_result C. z ∈ X#} = lower_result {#z ∈# C. z ∈ lift_applist X#}"
proof -
  define f where "f = (λC. {#if z = y then x else z. z ∈# C#})"
  have "lower_result {#z ∈# C. z ∈ lift_applist X#} = f {#z ∈# C. z ∈ lift_applist X#} - {#x#}"
    by (simp add: f_def lower_result_def)
  also have "f {#z ∈# C. z ∈ lift_applist X#} = {#z ∈# f C. z ∈ X#}"
    using assms by (induction C) (auto simp: f_def lift_applist_def)
  also have "… - {#x#} = {#z ∈# f C - {#x#}. z ∈ X#}"
    by (subst filter_diff_mset') auto
  also have "f C - {#x#} = lower_result C"
    by (simp add: f_def lower_result_def)
  finally show ?thesis ..
qed


sublocale lowered: anon_papp_election "l * k" parties k
  by standard (use n_voters_pos xy finite_parties k in auto)

lemma is_pref_profile_lift_profile [intro]:
  assumes "lowered.is_pref_profile A"
  shows   "is_pref_profile (lift_profile A)"
proof -
  interpret A: anon_papp_profile "l * k" parties k A
    by fact
  show ?thesis
    using A.A_nonempty A.A_subset A.size_A l
    by unfold_locales
       (auto simp: lift_profile_def lift_applist_def xy 
                   size_mset_sum_mset image_mset.compositionality o_def)
qed

lemma is_committee_lower_result:
  assumes "is_committee C" "x ∈# C ∨ y ∈# C"
  shows   "lowered.is_committee (lower_result C)"
  using assms unfolding is_committee_def lowered.is_committee_def
  using lower_result_subset'[of C] by auto

lemma x_or_y_in_r_lift_profile:
  assumes "lowered.is_pref_profile A"
  shows   "x ∈# r (lift_profile A) ∨ y ∈# r (lift_profile A)"
proof -
  interpret A: anon_papp_profile "l * k" parties k A
    by fact
  have "size {#z ∈# r (lift_profile A). z ∈ {x, y}#} ≥ 1"
  proof (rule proposition3)
    have "real (l * (k + 1)) / real (k + 1) = real l"
      by (simp add: field_simps)
    also have "int 1 * ⌈…⌉ = int l"
      by simp
    also have "l ≤ count (lift_profile A) {x, y}"
      using xy A.A_subset by (subst count_lift_profile) auto
    finally show "int 1 * ⌈real (l * (k + 1)) / real (k + 1)⌉ ≤ int (count (lift_profile A) {x, y})"
      by simp
  next
    show "is_pref_profile (lift_profile A)"
      by (intro is_pref_profile_lift_profile) fact
  qed (use xy in auto)
  hence "{#z ∈# r (lift_profile A). z ∈ {x, y}#} ≠ {#}"
    by force
  thus ?thesis
    by auto
qed

sublocale lowered: anon_papp "l * k" parties k lowered
proof
  fix A assume A: "lowered.is_pref_profile A"
  hence "is_pref_profile (lift_profile A)"
    by blast
  hence "is_committee (r (lift_profile A))"
    using rule_wf by blast
  thus "lowered.is_committee (lowered A)"
    unfolding lowered_def o_def using x_or_y_in_r_lift_profile[of A] A
    by (intro is_committee_lower_result) auto
qed

sublocale lowered: weak_rep_anon_papp "l * k" parties k lowered
proof
  fix A z
  assume A: "lowered.is_pref_profile A" and z: "l * k ≤ k * count A {z}"
  interpret A: anon_papp_profile "l * k" "parties" k A
    by fact

  from A have A': "is_pref_profile (lift_profile A)"
    by blast
  have "count A {z} > 0"
    using z k n_voters_pos by (intro Nat.gr0I) auto
  hence "{z} ∈# A"
    by simp
  hence z': "z ∈ parties"
    using A.A_subset z by auto
  hence [simp]: "y ≠ z" "z ≠ y"
    using xy by auto

  define C where "C = r (lift_profile A)"

  show "z ∈# lowered A"
  proof (cases "z = x")
    case False
    have "l ≤ count A {z}"
      using z k by (simp add: algebra_simps)
    hence "l * (k + 1) ≤ (k + 1) * count A {z}"
      by (subst mult.commute, intro mult_right_mono) auto
    also have "count A {z} = count (lift_profile A) {z}"
      using False A.A_subset xy by (subst count_lift_profile) auto
    finally have "z ∈# r (lift_profile A)"
      by (intro weak_representation A')
    thus "z ∈# lowered A"
      using False by (auto simp: lowered_def in_lower_result_iff)
  next
    case [simp]: True
    from xy have [simp]: "{x, y} - {y} = {x}"
      by auto

    have "size {#z ∈# C. z ∈ {x, y}#} ≥ 2"
      unfolding C_def
    proof (rule proposition3)
      have "real (l * (k + 1)) / real (k + 1) = l"
        unfolding of_nat_mult using k by (simp add: divide_simps)
      also have "int 2 * ⌈…⌉ = int (2 * l)"
        by simp
      also have "… ≤ count (lift_profile A) {x, y}"
        using z k xy A.A_subset by (subst count_lift_profile) auto
      finally show "int 2 * ⌈real (l * (k + 1)) / real (k + 1)⌉ ≤ …" .
    qed (use A' xy in auto)
    also have "size {#z ∈# C. z ∈ {x, y}#} = count C x + count C y"
      by (induction C) auto
    finally have "x ∈# lower_result C"
      by (subst in_lower_result_iff) auto
    thus "z ∈# lowered A"
      by (simp add: lowered_def C_def)
  qed
qed

sublocale lowered: card_stratproof_anon_papp "l * k" parties k lowered
proof
  fix A X Y
  show "¬lowered.card_manipulable A X Y"
    unfolding lowered.card_manipulable_def
  proof (rule notI, elim conjE)
    assume A: "lowered.is_pref_profile A" and XY: "X ∈# A" "Y ≠ {}" "Y ⊆ parties"
    assume *: "lowered A ≺[lowered.committee_preference X] lowered (A - {#X#} + {#Y#})"
    interpret anon_papp_profile "l * k" "parties" k A
      by fact
    have X: "X ≠ {}" "X ⊆ parties"
      using XY A_nonempty A_subset by auto
    define A' where "A' = A - {#X#}"
    have A': "A = A' + {#X#}"
      using XY by (simp add: A'_def)
    from xy X XY have [simp]: "y ∉ X" "y ∉ Y"
      by auto

    define Al1 where "Al1 = lift_profile A"
    define Al2 where "Al2 = lift_profile (A' + {#Y#})"
    have A'_plus_Y: "lowered.is_pref_profile (A' + {#Y#})"
      unfolding A'_def using A XY lowered.is_pref_profile_replace by blast
    have Al1: "is_pref_profile Al1"
      unfolding Al1_def using A by blast
    have Al2: "is_pref_profile Al2"
      unfolding Al2_def unfolding A'_def using A XY lowered.is_pref_profile_replace by blast

    have size_aux: "size (lower_result {#x ∈# r (lift_profile A). x ∈ lift_applist X#}) =
                    size {#x ∈# r (lift_profile A). x ∈ lift_applist X#} - (if x ∈ X then 1 else 0)"
      if A: "lowered.is_pref_profile A" for A
      using x_or_y_in_r_lift_profile[OF A] 
      by (subst size_lower_result') (auto simp: lift_applist_def)

    from * have "size {#x ∈# lower_result (r Al1). x ∈ X#} <
                 size {#x ∈# lower_result (r Al2). x ∈ X#}"
      by (simp add: Al1_def Al2_def lowered_def A' lowered.strong_committee_preference_iff)
    also have "{#x ∈# lower_result (r Al1). x ∈ X#} = lower_result {#x ∈# r Al1. x ∈ lift_applist X#}"
      using X xy by (subst filter_lower_result_eq) auto
    also have "{#x ∈# lower_result (r Al2). x ∈ X#} = lower_result {#x ∈# r Al2. x ∈ lift_applist X#}"
      using X xy by (subst filter_lower_result_eq) auto
    also have "size (lower_result {#x ∈# r Al1. x ∈ lift_applist X#}) =
               size {#x ∈# r Al1. x ∈ lift_applist X#} - (if x ∈ X then 1 else 0)"
      unfolding Al1_def by (rule size_aux) fact
    also have "size (lower_result {#x ∈# r Al2. x ∈ lift_applist X#}) =
               size {#x ∈# r Al2. x ∈ lift_applist X#} - (if x ∈ X then 1 else 0)"
      unfolding Al2_def by (rule size_aux) fact
    finally have "size {#x ∈# r Al1. x ∈ lift_applist X#} < size {#x ∈# r Al2. x ∈ lift_applist X#}"
      by auto
    hence "r Al1 ≺[committee_preference (lift_applist X)] r Al2"
      by (simp add: strong_committee_preference_iff)

    moreover have "¬r Al1 ≺[committee_preference (lift_applist X)] r Al2"
      by (rule not_manipulable' [where Y = "lift_applist Y"])
         (use Al1 Al2 in ‹auto simp: Al1_def Al2_def A'›)

    ultimately show False
      by contradiction
  qed
qed

sublocale lowered: card_stratproof_weak_rep_anon_papp "l * k" parties k lowered
  ..

end


text ‹
  For Weak ∗‹Proportional› Representation, the lowering argument to decrease the committee size
  is somewhat easier since it does not involve adding a new party; instead, we simply
  add ‹l› new voters whose preferences are ‹{x}›.
›
locale decrease_committee_card_stratproof_weak_prop_rep_anon_papp =
  card_stratproof_weak_prop_rep_anon_papp "l * (k + 1)" parties "k + 1" r
  for l k and parties :: "'a set" and r +
  fixes x :: 'a
  assumes x: "x ∈ parties"
  assumes k: "k > 0"
begin

definition lift_profile :: "'a set multiset ⇒ 'a set multiset" where
  "lift_profile A = A + replicate_mset l {x}"

definition lower_result
  where "lower_result C = C - {#x#}"

definition lowered where "lowered = lower_result ∘ r ∘ lift_profile"


lemma l: "l > 0"
  using n_voters_pos by auto

lemma lift_profile_empty [simp]: "lift_profile {#} = replicate_mset l {x}"
  by (simp add: lift_profile_def)

lemma lift_profile_add_mset [simp]:
  "lift_profile (add_mset X A) = add_mset X (lift_profile A)"
  by (simp add: lift_profile_def)

lemma empty_in_lift_profile_iff [simp]: "{} ∈# lift_profile A ⟷ {} ∈# A"
  by (auto simp: lift_profile_def)

lemma size_lift_profile [simp]: "size (lift_profile A) = size A + l"
  by (simp add: lift_profile_def)

lemma count_lift_profile:
  "count (lift_profile A) X = count A X + (if X = {x} then l else 0)"
  by (auto simp: lift_profile_def)


lemma size_lower_result [simp]:
  assumes "x ∈# C"
  shows   "size (lower_result C) = size C - 1"
  using assms by (auto simp: lower_result_def size_Diff_singleton)

lemma size_lower_result': "size (lower_result C) = size C - (if x ∈# C then 1 else 0)"
  by (induction C) (auto simp: lower_result_def size_Diff_singleton)

lemma count_lower_result:
  "count (lower_result C) z = count C z - (if z = x then 1 else 0)"
  by (auto simp: lower_result_def)

lemma in_lower_resultD:
  "z ∈# lower_result C ⟹ z ∈# C"
  by (auto simp: lower_result_def dest!: in_diffD)

lemma in_lower_result_iff:
  "z ∈# lower_result C ⟷ (if z = x then count C x > 1 else z ∈# C)"
  (is "_ = ?rhs")
proof -
  have "z ∈# lower_result C ⟷ count (lower_result C) z > 0"
    by auto
  also have "… ⟷ ?rhs"
    by (subst count_lower_result) auto
  finally show ?thesis .
qed


sublocale lowered: anon_papp_election "l * k" parties k
  by standard (use n_voters_pos finite_parties k in auto)

lemma is_pref_profile_lift_profile [intro]:
  assumes "lowered.is_pref_profile A"
  shows   "is_pref_profile (lift_profile A)"
proof -
  interpret A: anon_papp_profile "l * k" parties k A
    by fact
  show ?thesis
    using A.A_nonempty A.A_subset A.size_A l
    by unfold_locales
       (auto simp: lift_profile_def x size_mset_sum_mset image_mset.compositionality o_def)
qed

lemma is_committee_lower_result:
  assumes "is_committee C" "x ∈# C"
  shows   "lowered.is_committee (lower_result C)"
  using assms unfolding is_committee_def lowered.is_committee_def
  by (auto simp: lower_result_def size_Diff_singleton dest: in_diffD)

lemma x_in_r_lift_profile:
  assumes "lowered.is_pref_profile A"
  shows   "x ∈# r (lift_profile A)"
proof (rule weak_representation)
  show "is_pref_profile (lift_profile A)"
    using assms by blast
next
  have "(k + 1) * l ≤ (k + 1) * count (lift_profile A) {x}"
    by (intro mult_left_mono) (auto simp: count_lift_profile)
  thus "l * (k + 1) ≤ (k + 1) * count (lift_profile A) {x}"
    by (simp add: algebra_simps)
qed

sublocale lowered: anon_papp "l * k" parties k lowered
proof
  fix A assume A: "lowered.is_pref_profile A"
  hence "is_pref_profile (lift_profile A)"
    by blast
  hence "is_committee (r (lift_profile A))"
    using rule_wf by blast
  thus "lowered.is_committee (lowered A)"
    unfolding lowered_def o_def using x_in_r_lift_profile[of A] A
    by (intro is_committee_lower_result) auto
qed

sublocale lowered: weak_prop_rep_anon_papp "l * k" parties k lowered
proof
  fix A z l'
  assume A: "lowered.is_pref_profile A" and z: "l' * (l * k) ≤ k * count A {z}"
  interpret A: anon_papp_profile "l * k" "parties" k A
    by fact

  show "count (lowered A) z ≥ l'"
  proof (cases "l' > 0")
    case False
    thus ?thesis by auto
  next
    case l: True

    from A have A': "is_pref_profile (lift_profile A)"
      by blast
    have "count A {z} > 0"
      using z k n_voters_pos l by (intro Nat.gr0I) auto
    hence "{z} ∈# A"
      by simp
    hence z': "z ∈ parties"
      using A.A_subset z by auto
  
    define C where "C = r (lift_profile A)"
  
    show "count (lowered A) z ≥ l'"
    proof (cases "z = x")
      case False
      have "l' * l ≤ count A {z}"
        using z k by (simp add: algebra_simps)
      hence "l' * l * (k + 1) ≤ (k + 1) * count A {z}"
        by (subst mult.commute, intro mult_right_mono) auto
      also have "count A {z} = count (lift_profile A) {z}"
        using False A.A_subset by (subst count_lift_profile) auto
      finally have "count (r (lift_profile A)) z ≥ l'"
        by (intro weak_proportional_representation A') (auto simp: algebra_simps)
      thus "l' ≤ count (lowered A) z"
        using False by (simp add: lowered_def lower_result_def)
    next
      case [simp]: True
      have "l' * l ≤ count A {x}"
        using z k by (simp add: algebra_simps)
      hence "l' * l * (k + 1) ≤ (k + 1) * count A {x}"
        by (subst mult.commute, intro mult_right_mono) auto
      also have "… + (k + 1) * l = (k + 1) * count (lift_profile A) {x}"
        by (simp add: count_lift_profile algebra_simps)
      finally have "(l' + 1) * (l * (k + 1)) ≤ (k + 1) * count (lift_profile A) {x}"
        by (simp add: algebra_simps)
      hence "count (r (lift_profile A)) x ≥ l' + 1"
        by (intro weak_proportional_representation A')
      thus "l' ≤ count (lowered A) z"
        by (simp add: lowered_def lower_result_def)
    qed
  qed
qed

sublocale lowered: card_stratproof_anon_papp "l * k" parties k lowered
proof
  fix A X Y
  show "¬lowered.card_manipulable A X Y"
    unfolding lowered.card_manipulable_def
  proof (rule notI, elim conjE)
    assume A: "lowered.is_pref_profile A" and XY: "X ∈# A" "Y ≠ {}" "Y ⊆ parties"
    assume *: "lowered A ≺[lowered.committee_preference X] lowered (A - {#X#} + {#Y#})"
    interpret anon_papp_profile "l * k" "parties" k A
      by fact
    have X: "X ≠ {}" "X ⊆ parties"
      using XY A_nonempty A_subset by auto
    define A' where "A' = A - {#X#}"
    have A': "A = A' + {#X#}"
      using XY by (simp add: A'_def)

    define Al1 where "Al1 = lift_profile A"
    define Al2 where "Al2 = lift_profile (A' + {#Y#})"
    have A'_plus_Y: "lowered.is_pref_profile (A' + {#Y#})"
      unfolding A'_def using A XY lowered.is_pref_profile_replace by blast
    have Al1: "is_pref_profile Al1"
      unfolding Al1_def using A by blast
    have Al2: "is_pref_profile Al2"
      unfolding Al2_def unfolding A'_def using A XY lowered.is_pref_profile_replace by blast

    have size_aux: "size (lower_result {#x ∈# r (lift_profile A). x ∈ X#}) =
                    size {#x ∈# r (lift_profile A). x ∈ X#} - (if x ∈ X then 1 else 0)"
      if A: "lowered.is_pref_profile A" for A
      using x_in_r_lift_profile[OF A]  by (subst size_lower_result') auto

    from * have "size {#x ∈# lower_result (r Al1). x ∈ X#} <
                 size {#x ∈# lower_result (r Al2). x ∈ X#}"
      by (simp add: Al1_def Al2_def lowered_def A' lowered.strong_committee_preference_iff)
    also have "{#x ∈# lower_result (r Al1). x ∈ X#} = lower_result {#x ∈# r Al1. x ∈ X#}"
      using X x unfolding lower_result_def by (subst filter_diff_mset') auto
    also have "{#x ∈# lower_result (r Al2). x ∈ X#} = lower_result {#x ∈# r Al2. x ∈ X#}"
      using X x unfolding lower_result_def by (subst filter_diff_mset') auto
    also have "size (lower_result {#x ∈# r Al1. x ∈ X#}) =
               size {#x ∈# r Al1. x ∈ X#} - (if x ∈ X then 1 else 0)"
      unfolding Al1_def by (rule size_aux) fact
    also have "size (lower_result {#x ∈# r Al2. x ∈ X#}) =
               size {#x ∈# r Al2. x ∈ X#} - (if x ∈ X then 1 else 0)"
      unfolding Al2_def by (rule size_aux) fact
    finally have "size {#x ∈# r Al1. x ∈ X#} < size {#x ∈# r Al2. x ∈ X#}"
      by auto
    hence "r Al1 ≺[committee_preference X] r Al2"
      by (simp add: strong_committee_preference_iff)

    moreover have "¬r Al1 ≺[committee_preference X] r Al2"
      by (rule not_manipulable' [where Y = "Y"])
         (use Al1 Al2 in ‹auto simp: Al1_def Al2_def A'›)

    ultimately show False
      by contradiction
  qed
qed

sublocale lowered: card_stratproof_weak_prop_rep_anon_papp "l * k" parties k lowered
  ..

end

end