header "The Gibbard-Satterthwaite Theorem"
theory GS imports Arrow_Order
begin
text{* The Gibbard-Satterthwaite theorem as a corollary to Arrow's
theorem. The proof follows Nisan~\cite{NisanRTV07}. *}
definition "manipulable f == ∃P∈Prof. ∃i. ∃L∈Lin. (f P, f(P(i:=L))) : P i"
definition "dict f i == ∀P∈Prof.∀a. a ≠ f P --> (a,f P) : P i"
definition
Top :: "alt set => pref => pref" where
"Top S L ≡ {(a,b). (a,b) ∈ L ∧ (a ∈ S ∧ b ∈ S ∨ a ∉ S ∧ b ∉ S)} ∪
{(a,b). a ∉ S ∧ b ∈ S}"
lemma Top_in_Lin: "L:Lin ==> Top S L : Lin"
apply(simp add:Top_def slo_defs Sigma_def)
unfolding trans_def
apply blast
done
lemma Top_in_Prof: "P:Prof ==> Top S o P : Prof"
by(simp add:Prof_def Pi_def Top_in_Lin)
lemma not_manipulable: "¬ manipulable f <->
(∀P∈Prof.∀i.∀L∈Lin. f P ≠ f(P(i:=L)) -->
(f(P(i := L)), f P) : P i ∧ (f P, f(P(i := L))) : L)" (is "?A = ?B")
proof
assume ?A
show ?B
proof(clarsimp)
fix P i L assume 0: "P ∈ Prof" "L ∈ Lin" "f P ≠ f (P(i := L))"
moreover hence 1: "P i: Lin" "P(i:=L): Prof" by(simp add:Prof_def Pi_def)+
ultimately have "(f (P(i := L)), f P) ∈ P i" (is ?L)
using `?A` unfolding manipulable_def by (metis notin_Lin_iff)
moreover have "(f P, f (P(i := L))) ∈ L" (is ?R)
using 0 1 fun_upd_upd[of P] fun_upd_triv[of P] fun_upd_same[of P]
using `?A` unfolding manipulable_def by (metis notin_Lin_iff)
ultimately show "?L ∧ ?R" ..
qed
next
assume ?B
show ?A
proof(clarsimp simp:manipulable_def)
fix P i L assume "P ∈ Prof" "L ∈ Lin" "(f P, f (P(i := L))) ∈ P i"
moreover hence "P i: Lin" by(simp add:Prof_def Pi_def)
ultimately show False
using `?B` by(metis Lin_irrefl)
qed
qed
definition "swf(f) ≡ λP. {(a,b). a≠b ∧ f(Top {a,b} o P) = b}"
locale GS =
fixes f
assumes not_manip: "¬ manipulable f"
and onto: "f ` Prof = UNIV"
begin
lemma nonmanip:
"P:Prof ==> L:Lin ==> f(P(i := L)) ≠ f P ==>
(f(P(i := L)), f P) : P i ∧ (f P, f(P(i := L))) : L"
using not_manip by(metis not_manipulable)
lemma mono:
assumes "P∈Prof" "P'∈Prof" "∀i a. (a, f P) : P i --> (a, f P) : P' i"
shows "f P' = f P"
proof-
obtain h :: "indi => nat" where
injh: "inj h" and surjh: "h ` I = {0..<N}"
by(metis ex_bij_betw_finite_nat[OF finite_indi] bij_betw_def)
let ?M = "%n i. if h i < n then P' i else P i"
have N: "!!i. h i < N" using surjh by auto
have MProf: "!!n. ?M n : Prof" and P'Lin: "!!i. P' i : Lin"
using `P:Prof` `P':Prof` by(simp add:Prof_def Pi_def)+
{ fix n have "n<=N ==> f(?M n) = f P"
proof(induct n)
case 0 show ?case by simp
next
case (Suc n)
let ?up = "(?M n)(inv h n := P' (inv h n))"
have 1: "?M(Suc n) = ?up" using surjh Suc(2)
by(simp (no_asm_simp) add:expand_fun_eq f_inv_into_f)
(metis injh inv_f_f less_antisym)
show ?case
proof(rule ccontr)
assume "¬ ?case"
with `?M(Suc n) = ?up` Suc have 0: "f ?up ≠ f(?M n)" by simp
from nonmanip[OF MProf P'Lin 0] assms(3) show False
using N surjh Suc Lin_irrefl[OF P'Lin]
by(fastsimp simp: f_inv_into_f)
qed
qed
}
from this[of N] N show "f P' = f P" by simp
qed
lemma una_Top: assumes "P:Prof" "S ≠ {}" shows "f(Top S o P) : S"
proof -
obtain h :: "indi => nat" where
injh: "inj h" and surjh: "h ` I = {0..<N}"
by(metis ex_bij_betw_finite_nat[OF finite_indi] bij_betw_def)
from assms obtain a where "a:S" by blast
from onto obtain Pa where "Pa:Prof" "f Pa = a"
by(metis inv_into_into UNIV_I f_inv_into_f)
let ?M = "%n i. if h i < n then Top S (P i) else Pa i"
have N: "!!i. h i < N" using surjh by auto
have MProf: "!!n. ?M n : Prof" using `P:Prof` `Pa:Prof`
by(simp add:Prof_def Pi_def Top_in_Lin mktop_Lin)
{ fix n have "n<=N ==> f(?M n) : S"
proof(induct n)
case 0 thus ?case using `f Pa = a` `a:S` by simp
next
case (Suc n)
show ?case
proof cases
assume "f(?M n) = f(?M(Suc n))"
thus ?case using Suc by simp
next
let ?up = "(?M n)(inv h n := Top S (P(inv h n)))"
assume "f(?M n) ≠ f(?M(Suc n))"
also have eq: "?M(Suc n) = ?up" using surjh Suc
by(simp (no_asm_simp) add:expand_fun_eq f_inv_into_f)
(metis injh inv_f_eq less_antisym)
finally have n: "f(?M n) ≠ f(?up)" .
with nonmanip[OF MProf Top_in_Lin n[symmetric]] Suc eq `P:Prof`
show ?case by (simp add:Top_def Prof_def Pi_def)
qed
qed
}
from this[of N] N show ?thesis by(simp add:comp_def)
qed
lemma SWF_swf: "swf f : SWF"
proof (rule Pi_I)
fix P assume "P: Prof"
show "swf f P : Lin"
proof(unfold Lin_def strict_linear_order_on_def, auto)
show "total(swf f P)"
proof(simp add: total_on_def, intro allI impI)
fix a b :: alt assume "a≠b"
thus "(a,b) ∈ swf f P ∨ (b,a) ∈ swf f P"
unfolding swf_def using una_Top[of P "{a,b}"] `P:Prof`
by simp(metis insert_commute)
qed
show "irrefl(swf f P)" by(simp add: irrefl_def swf_def)
show "trans(swf f P)"
proof (clarsimp simp:trans_def swf_def insert_commute)
fix a b c assume "a≠b" "b≠c" "f(Top{a,b} o P) = b" "f(Top{b,c} o P) = c"
hence "a≠c" by(auto simp: insert_commute)
note 3 = Top_in_Prof[OF `P:Prof`, of "{a,b,c}"]
{ assume "f (Top {a, b, c} o P) = a"
hence "f(Top{a,b} o P) = a"
using mono[OF 3 Top_in_Prof[OF `P:Prof`], of "{a,b}"]
by(auto simp:Top_def)
with `f(Top{a,b} o P) = b` `a≠b` have False by simp
} moreover
{ assume "f (Top {a, b, c} o P) = b"
hence "f(Top{b,c} o P) = b"
using mono[OF 3 Top_in_Prof[OF `P:Prof`], of "{b,c}"]
by(auto simp:Top_def)
with `f(Top{b,c} o P) = c` `b≠c` have False by simp
}
ultimately have "f (Top {a, b, c} o P) = c"
using una_Top[OF `P:Prof`, of "{a,b,c}", simplified] by blast
hence "f(Top{a,c} o P) = c" (is ?R)
using mono[OF 3 Top_in_Prof[OF `P:Prof`], of "{a,c}"]
by (auto simp:Top_def)
thus "a≠c ∧ ?R" using `a≠c` by blast
qed
qed
qed
lemma Top_top: "L:Lin ==> (!!a. a≠b ==> (a,b) : L) ==> Top {b} L = L"
apply(auto simp:Top_def slo_defs)
apply (metis trans_def)
apply (metis trans_def)
done
lemma una_swf: "unanimity(swf f)"
proof(clarsimp simp:swf_def unanimity_def)
fix P a b
assume "P:Prof" and abP: "∀i. (a, b) ∈ P i"
hence "a ≠ b" by(fastsimp simp:Prof_def Pi_def slo_defs)
let ?abP = "Top {a,b} o P"
have "?abP : Prof" using `P:Prof` by(simp add:Prof_def Pi_def Top_in_Lin)
have top: "!!i c. b≠c ==> (c,b) : Top {a,b} (P i)"
using abP by(auto simp:Top_def)
have "Top {b} o ?abP = ?abP" using `P:Prof`
by (simp add:expand_fun_eq top Top_top Prof_def Pi_def Top_in_Lin)
moreover have "f(Top {b} o ?abP) = b"
by (metis una_Top[OF `?abP : Prof`] empty_not_insert singletonE)
ultimately have "f ?abP = b" by simp
thus "a≠b ∧ f ?abP = b" using `a≠b` by blast
qed
lemma IIA_swf: "IIA(swf f)"
proof(clarsimp simp: IIA_def)
fix P P' a b
assume "P:Prof" "P':Prof" and iff: "∀i. ((a,b) ∈ P i) = ((a,b) ∈ P' i)"
hence [simp]: "!!i x. (x,x) ~: P i ∧ (x,x) ~: P' i"
by(simp add:Prof_def Pi_def slo_defs)
have iff': "a≠b --> (∀i. ((b,a) ∈ P i) = ((b,a) ∈ P' i))"
using iff `P:Prof` `P':Prof` unfolding Prof_def Pi_def
by simp (metis iff notin_Lin_iff)
let ?abP = "Top {a,b} o P" let ?abP' = "Top {a,b} o P'"
have "∀i c. (c, f ?abP) : ?abP i --> (c, f ?abP) : ?abP' i"
using una_Top[of P "{a,b}", OF `P:Prof`] iff iff' by(auto simp add:Top_def)
then have "f (Top {a,b} o P) = f (Top {a,b} o P')"
using Top_in_Prof[OF `P:Prof`] Top_in_Prof[OF `P':Prof`]
mono[of "Top {a, b} o P"] by metis
thus "(a <\<^bsub>swf f P\<^esub> b) = (a <\<^bsub>swf f P'\<^esub> b)" by(simp add: swf_def)
qed
lemma dict_swf: assumes "dictator (swf f) i" shows "dict f i"
proof (auto simp:dict_def)
fix P a assume "P:Prof" "a≠f P"
have "f (Top {a,f P} o P) = f P"
using mono[OF `P:Prof` Top_in_Prof[OF `P:Prof`,of "{a,f P}"]]
by (auto simp:Top_def)
moreover have "P i = {(a,b). a≠b ∧ f(Top {a,b} o P) = b}"
using assms `P:Prof` by(simp add:dictator_def swf_def)
ultimately show "(a,f P) : P i" using `a≠f P` by simp
qed
theorem Gibbard_Satterthwaite:
"∃i. dict f i"
by (metis Arrow SWF_swf una_swf IIA_swf dict_swf)
end
theorem Gibbard_Satterthwaite:
"¬ manipulable f ==> ∀a.∃P∈Prof. a = f P ==> ∃i. dict f i"
using GS.Gibbard_Satterthwaite[of f,unfolded GS_def]
by blast
end