(*
 * Social Choice Functions (SCFs).
 * (C)opyright Peter Gammie, peteg42 at gmail.com, commenced July 2006.
 * License: BSD
 *)

(*<*)
theory SCFs

imports RPRs

begin
(*>*)

(* **************************************** *)

subsection‹Choice Sets, Choice Functions›

text‹A \emph{choice set} is the subset of @{term "A"} where every element
  that subset is (weakly) preferred to every other element of @{term "A"}
  respect to a given RPR. A \emph{choice function} yields a non-empty
  set whenever @{term "A"} is non-empty.›

definition choiceSet :: "'a set → 'a RPR → 'a set" where
  "choiceSet A r ≡ { x ∈ A . ∀y ∈ A. x ⪯ y }"

definition choiceFn :: "'a set → 'a RPR → bool" where
  "choiceFn A r ≡ ∀A' ⊆ A. A' ≠ {} ⟶ choiceSet A' r ≠ {}"

lemma choiceSetI[intro]:
  "[ x ∈ A; ∧y. y ∈ A ==> x ⪯ y ] ==> x ∈ choiceSet A r"
  unfolding choiceSet_def by simp

lemma choiceFnI[intro]:
  "(∧A'. [ A' ⊆ A; A' ≠ {} ] ==> choiceSet A' r ≠ {}) ==> choiceFn A r"
  unfolding choiceFn_def by simp

text‹If a complete and reflexive relation is also \emph{quasi-transitive}
  will yield a choice function.›

definition quasi_trans :: "'a RPR → bool" where
  "quasi_trans r ≡ ∀x y z. x ≺ y ∧ y ≺ z ⟶ x ≺ z"

lemma quasi_transI[intro]:
  "(∧x y z. [ x ≺ y; y ≺ z ] ==> x ≺ z) ==> quasi_trans r"
  unfolding quasi_trans_def by blast

lemma quasi_transD: "[ x ≺ y; y ≺ z; quasi_trans r ] ==> x ≺ z"
  unfolding quasi_trans_def by blast

lemma trans_imp_quasi_trans: "trans r ==> quasi_trans r"
  by (rule quasi_transI, unfold strict_pref_def trans_def, blast)

lemma r_c_qt_imp_cf:
  assumes finiteA: "finite A"
      and c: "complete A r"
      and qt: "quasi_trans r"
      and r: "refl_on A r"
  shows "choiceFn A r"
proof
  fix B assume B: "B ⊆ A" "B ≠ {}"
  with finite_subset finiteA have finiteB: "finite B" by auto
  from finiteB B show "choiceSet B r ≠ {}"
  proof(induct rule: finite_subset_induct')
    case empty with B show ?case by auto
  next
    case (insert a B)
    hence finiteB: "finite B"
        and aA: "a ∈ A"
        and AB: "B ⊆ A"
        and aB: "a ∉ B"
        and cF: "B ≠ {} ==> choiceSet B r ≠ {}" by - blast
    show ?case
    proof(cases "B = {}")
      case True with aA r show ?thesis
        unfolding choiceSet_def by blast
    next
      case False
      with cF obtain b where bCF: "b ∈ choiceSet B r" by blast
      from AB aA bCF complete_refl_on[OF c r]
      have "a ≺ b ∨ b ⪯ a" unfolding choiceSet_def strict_pref_def by blast
      thus ?thesis
      proof
        assume ab: "b ⪯ a"
        with bCF show ?thesis unfolding choiceSet_def by auto
      next
        assume ab: "a ≺ b"
        have "a ∈ choiceSet (insert a B) r"
        proof(rule ccontr)
          assume aCF: "a ∉ choiceSet (insert a B) r"
          from aB have "∧b. b ∈ B ==> a ≠ b" by auto
          with aCF aA AB c r obtain b' where B: "b' ∈ B" "b' ≺ a"
            unfolding choiceSet_def complete_def strict_pref_def by blast
          with ab qt have "b' ≺ b" by (blast dest: quasi_transD)
          with bCF B show False unfolding choiceSet_def strict_pref_def by blast
        qed
        thus ?thesis by auto
      qed
    qed
  qed
qed

lemma rpr_choiceFn: "[ finite A; rpr A r ] ==> choiceFn A r"
  unfolding rpr_def by (blast dest: trans_imp_quasi_trans r_c_qt_imp_cf)

(* **************************************** *)

subsection‹Social Choice Functions (SCFs)›

text ‹A \emph{social choice function} (SCF), also called a
 emph{collective choice rule} by Sen cite‹‹p28› in "Sen:70a"›, is a function that
  aggregates society's opinions, expressed as a profile, into a
  relation.›

type_synonym ('a, 'i) SCF = "('a, 'i) Profile → 'a RPR"

text ‹The least we require of an SCF is that it be \emph{complete} and
  function of the profile. The latter condition is usually implied by
  conditions, such as @{term "iia"}.›

definition
  SCF :: "('a, 'i) SCF → 'a set → 'i set → ('a set → 'i set → ('a, 'i) Profile → bool) → bool"
where
  "SCF scf A Is Pcond ≡ (∀P. Pcond A Is P ⟶ (complete A (scf P)))"

lemma SCFI[intro]:
  assumes c: "∧P. Pcond A Is P ==> complete A (scf P)"
  shows "SCF scf A Is Pcond"
  unfolding SCF_def using assms by blast

lemma SCF_completeD[dest]: "[ SCF scf A Is Pcond; Pcond A Is P ] ==> complete A (scf P)"
  unfolding SCF_def by blast

(* **************************************** *)

subsection‹Social Welfare Functions (SWFs)›

text ‹A \emph{Social Welfare Function} (SWF) is an SCF that expresses the
 's opinion as a single RPR.

  some situations it might make sense to restrict the allowable
 .›

definition
  SWF :: "('a, 'i) SCF → 'a set → 'i set → ('a set → 'i set → ('a, 'i) Profile → bool) → bool"
where
  "SWF swf A Is Pcond ≡ (∀P. Pcond A Is P ⟶ rpr A (swf P))"

lemma SWF_rpr[dest]: "[ SWF swf A Is Pcond; Pcond A Is P ] ==> rpr A (swf P)"
  unfolding SWF_def by simp

(* **************************************** *)

subsection‹General Properties of an SCF›

text‹An SCF has a \emph{universal domain} if it works for all profiles.›

definition universal_domain :: "'a set → 'i set → ('a, 'i) Profile → bool" where
  "universal_domain A Is P ≡ profile A Is P"

declare universal_domain_def[simp]

text‹An SCF is \emph{weakly Pareto-optimal} if, whenever everyone strictly
  @{term "x"} to @{term "y"}, the SCF does too.›

definition
  weak_pareto :: "('a, 'i) SCF → 'a set → 'i set → ('a set → 'i set → ('a, 'i) Profile → bool) → bool"
where
  "weak_pareto scf A Is Pcond ≡
     (∀P x y. Pcond A Is P ∧ x ∈ A ∧ y ∈ A ∧ (∀i ∈ Is. x _{P i)}≺ y) ⟶ x _{scf P)}≺ y)"

lemma weak_paretoI[intro]:
  "(∧P x y. [Pcond A Is P; x ∈ A; y ∈ A; ∧i. i∈Is ==> x _{P i)}≺ y] ==> x _{scf P)}≺ y)
  ==> weak_pareto scf A Is Pcond"
  unfolding weak_pareto_def by simp

lemma weak_paretoD:
  "[ weak_pareto scf A Is Pcond; Pcond A Is P; x ∈ A; y ∈ A;
     (∧i. i ∈ Is ==> x _{P i)}≺ y) ] ==> x _{scf P)}≺ y"
  unfolding weak_pareto_def by simp

text‹

  SCF satisfies \emph{independence of irrelevant alternatives} if, for two
  profiles @{term "P"} and @{term "P'"} where for all individuals
 {term "i"}, alternatives @{term "x"} and @{term "y"} drawn from set @{term
 S"} have the same order in @{term "P i"} and @{term "P' i"}, then
  @{term "x"} and @{term "y"} have the same order in @{term "scf
 "} and @{term "scf P'"}.

 ›

definition iia :: "('a, 'i) SCF → 'a set → 'i set → bool" where
  "iia scf S Is ≡
    (∀P P' x y. profile S Is P ∧ profile S Is P'
      ∧ x ∈ S ∧ y ∈ S
      ∧ (∀i ∈ Is. ((x _{P i)}⪯ y) ⟷ (x _{P' i)}⪯ y)) ∧ ((y _{P i)}⪯ x) ⟷ (y _{P' i)}⪯ x)))
         ⟶ ((x _{scf P)}⪯ y) ⟷ (x _{scf P')}⪯ y)))"

lemma iiaI[intro]:
  "(∧P P' x y.
    [ profile S Is P; profile S Is P';
      x ∈ S; y ∈ S;
      ∧i. i ∈ Is ==> ((x _{P i)}⪯ y) ⟷ (x _{P' i)}⪯ y)) ∧ ((y _{P i)}⪯ x) ⟷ (y _{P' i)}⪯ x))
    ] ==> ((x _{swf P)}⪯ y) ⟷ (x _{swf P')}⪯ y)))
  ==> iia swf S Is"
  unfolding iia_def by simp

lemma iiaE:
  "[ iia swf S Is;
     {x,y} ⊆ S;
     a ∈ {x, y}; b ∈ {x, y};
     ∧i a b. [ a ∈ {x, y}; b ∈ {x, y}; i ∈ Is ] ==> (a _{P' i)}⪯ b) ⟷ (a _{P i)}⪯ b);
     profile S Is P; profile S Is P' ]
  ==> (a _{swf P)}⪯ b) ⟷ (a _{swf P')}⪯ b)"
  unfolding iia_def by (simp, blast)

(* **************************************** *)

subsection‹Decisiveness and Semi-decisiveness›

text‹This notion is the key to Arrow's Theorem, and hinges on the use of
  preference cite‹‹p42› in "Sen:70a"›.›

text‹A coalition @{term "C"} of agents is \emph{semi-decisive} for @{term
 x"} over @{term "y"} if, whenever the coalition prefers @{term "x"} to
 {term "y"} and all other agents prefer the converse, the coalition
 .›

definition semidecisive :: "('a, 'i) SCF → 'a set → 'i set → 'i set → 'a → 'a → bool" where
  "semidecisive scf A Is C x y ≡
    C ⊆ Is ∧ (∀P. profile A Is P ∧ (∀i ∈ C. x _{P i)}≺ y) ∧ (∀i ∈ Is - C. y _{P i)}≺ x)
      ⟶ x _{scf P)}≺ y)"

lemma semidecisiveI[intro]:
  "[ C ⊆ Is;
    ∧P. [ profile A Is P; ∧i. i ∈ C ==> x _{P i)}≺ y; ∧i. i ∈ Is - C ==> y _{P i)}≺ x ]
     ==> x _{scf P)}≺ y ] ==> semidecisive scf A Is C x y"
  unfolding semidecisive_def by simp

lemma semidecisive_coalitionD[dest]: "semidecisive scf A Is C x y ==> C ⊆ Is"
  unfolding semidecisive_def by simp

lemma sd_refl: "[ C ⊆ Is; C ≠ {} ] ==> semidecisive scf A Is C x x"
  unfolding semidecisive_def strict_pref_def by blast

text‹A coalition @{term "C"} is \emph{decisive} for @{term "x"} over
 {term "y"} if, whenever the coalition prefers @{term "x"} to @{term "y"},
  coalition prevails.›

definition decisive :: "('a, 'i) SCF → 'a set → 'i set → 'i set → 'a → 'a → bool" where
  "decisive scf A Is C x y ≡
    C ⊆ Is ∧ (∀P. profile A Is P ∧ (∀i ∈ C. x _{P i)}≺ y) ⟶ x _{scf P)}≺ y)"

lemma decisiveI[intro]:
  "[ C ⊆ Is; ∧P. [ profile A Is P; ∧i. i ∈ C ==> x _{P i)}≺ y ] ==> x _{scf P)}≺ y ]
    ==> decisive scf A Is C x y"
  unfolding decisive_def by simp

lemma d_imp_sd: "decisive scf A Is C x y ==> semidecisive scf A Is C x y"
  unfolding decisive_def by (rule semidecisiveI, blast+)

lemma decisive_coalitionD[dest]: "decisive scf A Is C x y ==> C ⊆ Is"
  unfolding decisive_def by simp

text ‹Anyone is trivially decisive for @{term "x"} against @{term "x"}.›

lemma d_refl: "[ C ⊆ Is; C ≠ {} ] ==> decisive scf A Is C x x"
  unfolding decisive_def strict_pref_def by simp

text‹Agent @{term "j"} is a \emph{dictator} if her preferences always
 . This is the same as saying that she is decisive for all @{term "x"}
  @{term "y"}.›

definition dictator :: "('a, 'i) SCF → 'a set → 'i set → 'i → bool" where
  "dictator scf A Is j ≡ j ∈ Is ∧ (∀x ∈ A. ∀y ∈ A. decisive scf A Is {j} x y)"

lemma dictatorI[intro]:
  "[ j ∈ Is; ∧x y. [ x ∈ A; y ∈ A ] ==> decisive scf A Is {j} x y ] ==> dictator scf A Is j"
  unfolding dictator_def by simp

lemma dictator_individual[dest]: "dictator scf A Is j ==> j ∈ Is"
  unfolding dictator_def by simp

(*<*)
end
(*>*)