Theory GS

Up to index of Isabelle/HOL/ArrowImpossibilityGS

theory GS
imports Arrow_Order
`(*    Author:     Tobias Nipkow, 2008*)header "The Gibbard-Satterthwaite Theorem"theory GS imports Arrow_Orderbegintext{* The Gibbard-Satterthwaite theorem as a corollary to Arrow'stheorem. 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_defapply blastdonelemma 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" ..  qednext  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)  qedqeddefinition "swf(f) ≡ λP. {(a,b). a≠b ∧ f(Top {a,b} o P) = b}"locale GS =fixes fassumes not_manip: "¬ manipulable f"and onto: "f ` Prof = UNIV"beginlemma 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:fun_eq_iff 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(fastforce simp: f_inv_into_f)      qed    qed  }  from this[of N] N show "f P' = f P" by simpqedlemma 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:fun_eq_iff 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)qedlemma 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  qedqedlemma 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)donelemma 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(fastforce 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:fun_eq_iff 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 blastqedlemma 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 <⇘swf f P⇙ b) = (a <⇘swf f P'⇙ b)" by(simp add: swf_def)qedlemma 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 simpqedtheorem Gibbard_Satterthwaite:  "∃i. dict f i"by (metis Arrow SWF_swf una_swf IIA_swf dict_swf)endtheorem Gibbard_Satterthwaite:  "¬ manipulable f ==> ∀a.∃P∈Prof. a = f P ==> ∃i. dict f i"using GS.Gibbard_Satterthwaite[of f,unfolded GS_def]by blastend`