# Theory Arrow_Utility

Up to index of Isabelle/HOL/ArrowImpossibilityGS

theory Arrow_Utility
imports Complex_Main
(*  Author:     Tobias Nipkow, 2002  *)header "Arrow's Theorem for Utility Functions"theory Arrow_Utility imports Complex_Mainbegintext{* This theory formalizes the first proof due toGeanakoplos~\cite{Geanakoplos05}.  In contrast to the standard modelof preferences as linear orders, we model preferences as \emph{utilityfunctions} mapping each alternative to a real number. The type ofalternatives and voters is assumed to be finite. *}typedecl alttypedecl indiaxiomatization where  alt3: "∃a b c::alt. distinct[a,b,c]" and  finite_alt: "finite(UNIV:: alt set)" and  finite_indi: "finite(UNIV:: indi set)"lemma third_alt: "a ≠ b ==> ∃c::alt. distinct[a,b,c]"using alt3 by simp metislemma alt2: "∃b::alt. b ≠ a"using alt3 by simp metistype_synonym pref = "alt => real"type_synonym prof = "indi => pref"definition top :: "pref => alt => bool" (infixr "<·" 60) where"p <· b  ≡  ∀a. a ≠ b --> p a < p b"definition bot :: "alt => pref => bool" (infixr "·<" 60) where"b ·< p  ≡  ∀a. a ≠ b --> p b < p a"definition extreme :: "pref => alt => bool" where"extreme p b  ≡  b ·< p ∨ p <· b"abbreviation"Extreme P b == ∀i. extreme (P i) b"lemma [simp]: "r <= s ==> r < s+(1::real)"by arithlemma [simp]: "r < s ==> r < s+(1::real)"by arithlemma [simp]: "r <= s ==> ¬ s+(1::real) < r"by arithlemma [simp]: "(r < s-(1::real)) = (r+1 < s)"by arithlemma [simp]: "(s-(1::real) < r) = (s < r+1)"by arithlemma less_if_bot[simp]: "[| b ·< p; x ≠ b |] ==> p b < p x"by(simp add:bot_def)lemma [simp]: "[| p <· b; x ≠ b |] ==> p x < p b"by(simp add:top_def)lemma [simp]: assumes top: "p <· b" shows "¬ p b < p c"proof (cases)  assume "b = c" thus ?thesis by simpnext  assume "b ≠ c"  with top have "p c < p b" by (simp add:eq_sym_conv)  thus ?thesis by simpqedlemma not_less_if_bot[simp]:  assumes bot: "b ·< p" shows "¬ p c < p b"proof (cases)  assume "b = c" thus ?thesis by simpnext  assume "b ≠ c"  with bot have "p b < p c" by (simp add:eq_sym_conv)  thus ?thesis by simpqedlemma top_impl_not_bot[simp]: "p <· b ==> ¬ b ·< p"by(unfold bot_def, simp add:alt2)lemma [simp]: "extreme p b ==> (¬ p <· b) = (b ·< p)"apply(unfold extreme_def)apply(fastforce dest:top_impl_not_bot)donelemma [simp]: "extreme p b ==> (¬ b ·< p) = (p <· b)"apply(unfold extreme_def)apply(fastforce dest:top_impl_not_bot)donetext{* Auxiliary construction to hide details of preference model. *}definition mktop :: "pref => alt => pref" where"mktop p b ≡ p(b := Max(range p) + 1)"definition mkbot :: "pref => alt => pref" where"mkbot p b ≡ p(b := Min(range p) - 1)"definition between :: "pref => alt => alt => alt => pref" where"between p a b c ≡ p(b := (p a + p c)/2)"text{*To make things simpler:*}declare between_def[simp]lemma [simp]: "a ≠ b ==> mktop p b a = p a"by(simp add:mktop_def)lemma [simp]: "a ≠ b ==> mkbot p b a = p a"by(simp add:mkbot_def)lemma [simp]: "a ≠ b ==> p a < mktop p b b"by(simp add:mktop_def finite_alt)lemma [simp]: "a ≠ b ==> mkbot p b b < p a"by(simp add:mkbot_def finite_alt)lemma [simp]: "mktop p b <· b"by(simp add:mktop_def top_def finite_alt)lemma [simp]: "¬ b ·< mktop p b"by(simp add:mktop_def bot_def alt2 finite_alt)lemma [simp]: "a ≠ b ==> ¬ P p a < mkbot (P p) b b"proof (simp add:mkbot_def finite_alt)  have "¬ P p a + 1 < P p a" by simp  thus "EX x. ¬ P p a + 1 < P p x" ..qedtext{* The proof starts here. *}locale arrow =fixes F :: "prof => pref"assumes unanimity: "(!!i. P i a < P i b) ==> F P a < F P b"and IIA:"(!!i. (P i a < P i b) = (P' i a < P' i b)) ==> (F P a < F P b) = (F P' a < F P' b)"beginlemmas IIA' = IIA[THEN iffD1]definition dictates :: "indi => alt => alt => bool" ("_ dictates _ < _") where"(i dictates a < b)  ≡  ∀P. P i a < P i b --> F P a < F P b"definition dictates2 :: "indi => alt => alt => bool" ("_ dictates _,_") where"(i dictates a,b)  ≡  (i dictates a < b) ∧ (i dictates b < a)"definition dictatesx:: "indi => alt => bool" ("_ dictates'_except _") where"(i dictates_except c)  ≡  ∀a b. c ∉ {a,b} --> (i dictates a<b)"definition dictator :: "indi => bool" where"dictator i  ≡  ∀a b. (i dictates a<b)"definition pivotal :: "indi => alt => bool" where"pivotal i b ≡ ∃P. Extreme P b  ∧  b ·< P i  ∧  b ·< F P  ∧     F (P(i := mktop (P i) b)) <· b"lemma all_top[simp]: "∀i. P i <· b ==> F P <· b"by (unfold top_def) (simp add: unanimity)lemma not_extreme:  assumes nex: "¬ extreme p b"  shows "∃a c. distinct[a,b,c] ∧ ¬ p a < p b ∧ ¬ p b < p c"proof -  obtain a c where abc: "a ≠ b ∧ ¬ p a < p b" "b ≠ c ∧ ¬ p b < p c"    using nex by (unfold extreme_def top_def bot_def) fastforce  show ?thesis  proof (cases "a = c")    assume "a ≠ c" thus ?thesis using abc by simp blast  next    assume ac: "a = c"    obtain d where d: "distinct[a,b,d]" using abc third_alt by blast    show ?thesis    proof (cases "p b < p d")      case False thus ?thesis using abc d by blast    next      case True      hence db: "¬ p d < p b" by arith      from d have "distinct[d,b,c]" by(simp add:ac eq_sym_conv)      thus ?thesis using abc db by blast    qed  qedqedlemma extremal:  assumes extremes: "Extreme P b" shows "extreme (F P) b"proof (rule ccontr)  assume nec: "¬ extreme (F P) b"  hence "∃a c. distinct[a,b,c] ∧ ¬ F P a < F P b ∧ ¬ F P b < F P c"    by(rule not_extreme)  then obtain a c where d: "distinct[a,b,c]" and    ab: "¬ F P a < F P b" and bc: "¬ F P b < F P c" by blast  let ?P = "λi. if P i <· b then between (P i) a c b                else (P i)(c := P i a + 1)"  have "¬ F ?P a < F ?P b"    using extremes d by(simp add:IIA[of _ _ _ P] ab)  moreover have "¬ F ?P b < F ?P c"    using extremes d by(simp add:IIA[of _ _ _ P] bc eq_sym_conv)  moreover have "F ?P a < F ?P c" by(rule unanimity)(insert d, simp)  ultimately show False by arithqedlemma pivotal_ind: assumes fin: "finite D"  shows "!!P. [| D = {i. b ·< P i}; Extreme P b; b ·< F P |]  ==> ∃i. pivotal i b" (is "!!P. ?D D P ==> ?E P ==> ?B P ==> _")using finproof (induct)  case (empty P)  from empty(1,2) have "∀i. P i <· b" by simp  hence "F P <· b" by simp  hence False using empty by(blast dest:top_impl_not_bot)  thus ?case ..next  fix D i P  assume IH: "!!P. ?D D P ==> ?E P ==> ?B P ==> ∃i. pivotal i b"    and "?E P" and "?B P" and insert: "insert i D = {i. b ·< P i}" and "i ∉ D"  from insert have "b ·< P i" by blast  let ?P = "P(i := mktop (P i) b)"  show "∃i. pivotal i b"  proof (cases "F ?P <· b")    case True    have "pivotal i b"    proof -      from ?E P ?B P b ·< P i True      show ?thesis by(unfold pivotal_def, blast)    qed    thus ?thesis ..  next    case False    have "D = {i. b ·< ?P i}"      by (rule set_eqI) (simp add:i ∉ D, insert insert, blast)    moreover have "Extreme ?P b"      using ?E P by (simp add:extreme_def)    moreover have "b ·< F ?P"      using extremal[OF Extreme ?P b] False by(simp del:fun_upd_apply)    ultimately show ?thesis by(rule IH)  qedqedlemma pivotal_exists: "∃i. pivotal i b"proof -  let ?P = "(λ_ a. if a=b then 0 else 1)::prof"  have "Extreme ?P b" by(simp add:extreme_def bot_def)  moreover have "b ·< F ?P"    by(simp add:bot_def unanimity del: less_if_bot not_less_if_bot)  ultimately show "∃i. pivotal i b"    by (rule pivotal_ind[OF finite_subset[OF subset_UNIV finite_indi] refl])qedlemma pivotal_xdictates: assumes pivo: "pivotal i b"  shows "i dictates_except b"proof -  have "!!a c. [| a ≠ b; b ≠ c |] ==> i dictates a < c"  proof (unfold dictates_def, intro allI impI)    fix a c and P::prof    assume abc: "a ≠ b" "b ≠ c" and           ac: "P i a < P i c"    show "F P a < F P c"    proof -      obtain P1 P2 where        "Extreme P1 b" and "b ·< F P1" and "b ·< P1 i" and "F P2 <· b" and        [simp]: "P2 = P1(i := mktop (P1 i) b)"        using pivo by (unfold pivotal_def) fast      let ?P = "λj. if j=i then between (P j) a b c                    else if P1 j <· b then mktop (P j) b else mkbot (P j) b"      have eq: "(F P a < F P c) = (F ?P a < F ?P c)"        using abc by - (rule IIA, auto)      have "F ?P a < F ?P b"      proof (rule IIA')        fix j show "(P2 j a < P2 j b) = (?P j a < ?P j b)"          using Extreme P1 b by(simp add: ac)      next        show "F P2 a < F P2 b"          using F P2 <· b abc by(simp add: eq_sym_conv)      qed      also have "… < F ?P c"      proof (rule IIA')        fix j show "(P1 j b < P1 j c) = (?P j b < ?P j c)"          using Extreme P1 b b ·< P1 i by(simp add: ac)      next        show "F P1 b < F P1 c"          using b ·< F P1 abc by(simp add: eq_sym_conv)      qed      finally show ?thesis by(simp add:eq)    qed  qed  thus ?thesis  by(unfold dictatesx_def) fastqedlemma pivotal_is_dictator:  assumes pivo: "pivotal i b" and ab: "a ≠ b" and d: "j dictates a,b"  shows "i = j"proof (rule ccontr)  assume pd: "i ≠ j"  obtain P1 P2 where "Extreme P1 b" and "b ·< F P1" and "F P2 <· b" and    P2: "P2 = P1(i := mktop (P1 i) b)"    using pivo by (unfold pivotal_def) fast  have "~(P1 j a < P1 j b)" (is "~ ?ab")  proof    assume "?ab"    hence "F P1 a < F P1 b" using d by(simp add: dictates_def dictates2_def)    with b ·< F P1 show False by simp  qed  hence "P1 j b < P1 j a" using Extreme P1 b[THEN spec, of j] ab    unfolding extreme_def top_def bot_def by metis  hence "P2 j b < P2 j a" using pd by (simp add:P2)  hence "F P2 b < F P2 a" using d by(simp add: dictates_def dictates2_def)  with F P2 <· b show False by simpqedtheorem dictator: "∃i. dictator i"proof-  from pivotal_exists[of b] obtain i where pivo: "pivotal i b" ..  { fix a assume neq: "a ≠ b" have "i dictates a,b"    proof -      obtain c where dist: "distinct[a,b,c]"        using neq third_alt by blast      obtain j where "pivotal j c" using pivotal_exists by fast      hence "j dictates_except c" by(rule pivotal_xdictates)      hence b: "j dictates a,b"         using dist by(simp add:dictatesx_def dictates2_def eq_sym_conv)      with pivo neq have "i = j" by(rule pivotal_is_dictator)      thus ?thesis using b by simp    qed  }  with pivotal_xdictates[OF pivo] have "dictator i"    by(simp add: dictates_def dictatesx_def dictates2_def dictator_def)      (metis less_le)  thus ?thesis ..qedendend