# Theory Arrow_Order

Up to index of Isabelle/HOL/ArrowImpossibilityGS

theory Arrow_Order
imports FuncSet Zorn
`(*  Author:     Tobias Nipkow, 2007  *)header "Arrow's Theorem for Strict Linear Orders"theory Arrow_Order imports Main "~~/src/HOL/Library/FuncSet" "~~/src/HOL/Library/Zorn"begintext{* This theory formalizes the third proof due toGeanakoplos~\cite{Geanakoplos05}.  Preferences are modeled as strictlinear orderings. The set of alternatives need not be finite.Individuals are assumed to be finite but are not a priory identified with aninitial segment of the naturals. In retrospect this generality appearsgratuitous and complicates some of the low-level reasoning where we use abijection with such an initial segment.  *}typedecl alttypedecl indiabbreviation "I == (UNIV::indi set)"axiomatization where  alt3: "∃a b c::alt. distinct[a,b,c]" and  finite_indi: "finite I"abbreviation "N == card I"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 * alt)set"definition "Lin == {L::pref. strict_linear_order L}"lemmas slo_defs = Lin_def strict_linear_order_on_def total_on_def irrefl_deflemma notin_Lin_iff: "L : Lin ==> x≠y ==> (x,y) ∉ L <-> (y,x) : L"apply(auto simp add: slo_defs)apply(metis trans_def)donelemma converse_in_Lin[simp]: "L¯ : Lin <-> L : Lin"apply (simp add: slo_defs)apply blastdonelemma Lin_irrefl: "L:Lin ==> (a,b):L ==> (b,a):L ==> False"by(simp add:slo_defs)(metis trans_def)corollary linear_alt: "∃L::pref. L : Lin"using well_order_on[where 'a = "alt", of UNIV]apply (auto simp:well_order_on_def Lin_def)apply (metis strict_linear_order_on_diff_Id)doneabbreviation rem :: "pref => alt => pref" where"rem L a ≡ {(x,y). (x,y) ∈ L ∧ x≠a ∧ y≠a}"definition mktop :: "pref => alt => pref" where"mktop L b ≡ rem L b ∪ {(x,b)|x. x≠b}"definition mkbot :: "pref => alt => pref" where"mkbot L b ≡ rem L b ∪ {(b,y)|y. y≠b}"definition below :: "pref => alt => alt => pref" where"below L a b ≡ rem L a ∪  {(a,b)} ∪ {(x,a)|x. (x,b) : L ∧ x≠a} ∪ {(a,y)|y. (b,y) : L ∧ y≠a}"definition above :: "pref => alt => alt => pref" where"above L a b ≡ rem L b ∪  {(a,b)} ∪ {(x,b)|x. (x,a) : L ∧ x≠b} ∪ {(b,y)|y. (a,y) : L ∧ y≠b}"lemma in_mktop: "(x,y) ∈ mktop L z <-> x≠z ∧ (if y=z then x≠y else (x,y) ∈ L)"by(auto simp:mktop_def)lemma in_mkbot: "(x,y) ∈ mkbot L z <-> y≠z ∧ (if x=z then x≠y else (x,y) ∈ L)"by(auto simp:mkbot_def)lemma in_above: "a≠b ==> L:Lin ==>  (x,y) : above L a b <-> x≠y ∧  (if x=b then (a,y) : L else   if y=b then x=a | (x,a) : L else (x,y) : L)"by(auto simp:above_def slo_defs)lemma in_below: "a≠b ==> L:Lin ==>  (x,y) : below L a b <-> x≠y ∧  (if y=a then (x,b) : L else   if x=a then y=b | (b,y) : L else (x,y) : L)"by(auto simp:below_def slo_defs)declare [[simp_depth_limit = 2]]lemma mktop_Lin: "L : Lin ==> mktop L x : Lin"by(auto simp add:slo_defs mktop_def trans_def)lemma mkbot_Lin: "L : Lin ==> mkbot L x : Lin"by(auto simp add:slo_defs trans_def mkbot_def)lemma below_Lin: "x≠y ==> L : Lin ==> below L x y : Lin"unfolding slo_defs below_def trans_defapply(simp)apply blastdonelemma above_Lin: "x≠y ==> L : Lin ==> above L x y : Lin"unfolding slo_defs above_def trans_defapply(simp)apply blastdonedeclare [[simp_depth_limit = 50]]abbreviation lessLin :: "alt => pref => alt => bool" ("(_ <⇘_⇙ _)" [51, 51] 50)where "a <⇘L⇙ b == (a,b) : L"definition "Prof = I -> Lin"abbreviation "SWF == Prof -> Lin"definition "unanimity F == ∀P∈Prof.∀a b. (∀i. a <⇘P i⇙ b) -->  a <⇘F P⇙ b"definition "IIA F == ∀P∈Prof.∀P'∈Prof.∀a b.   (∀i. a <⇘P i⇙ b <-> a <⇘P' i⇙ b) --> (a <⇘F P⇙ b <-> a <⇘F P'⇙ b)"definition "dictator F i == ∀P∈Prof. F P = P i"lemma dictatorI: "F : SWF ==>  ∀P∈Prof. ∀a b. a ≠ b --> (a,b) : P i --> (a,b) : F P ==> dictator F i"apply(simp add:dictator_def Prof_def Pi_def Lin_def strict_linear_order_on_def)apply safe apply(erule_tac x=P in allE) apply(erule_tac x=P in allE) apply(simp add:total_on_def irrefl_def) apply (metis trans_def)apply (metis irrefl_def)donelemma const_Lin_Prof: "L:Lin ==> (%p. L) : Prof"by(simp add:Prof_def Pi_def)lemma complete_Lin: assumes "a≠b" shows "EX L:Lin. (a,b) : L"proof -  from linear_alt obtain R where "R:Lin" by auto  thus ?thesis by (metis assms in_mkbot mkbot_Lin)qeddeclare Let_def[simp]theorem Arrow: assumes "F : SWF" and u: "unanimity F" and "IIA F"shows "EX i. dictator F i"proof -  { fix a b a' b' and P P'    assume d1: "a≠b" "a'≠b'" and d2: "a≠b'" "b≠a'" and      "P : Prof" "P' : Prof" and 1: "∀i. (a,b) : P i <-> (a',b') : P' i"    assume "(a,b) : F P"    def Q ≡ "%i. let L = (if a=a' then P i else below (P i) a' a)                  in if b=b' then L else above L b b'"    have "Q : Prof" using `P : Prof`      by(simp add:Q_def Prof_def Pi_def above_Lin below_Lin)    hence "F Q : Lin" using `F : SWF` by(simp add:Pi_def)    have "∀i. (a,b) : P i <-> (a,b) : Q i" using d1 d2 `P : Prof`      by(simp add:in_above in_below Q_def Prof_def Pi_def below_Lin)    hence "(a,b) : F Q" using `(a,b) : F P` `IIA F` `P:Prof` `Q : Prof`      unfolding IIA_def by blast    moreover    { assume "a≠a'"      hence "!!i. (a',a) : Q i" using d1 d2 `P : Prof`        by(simp add:in_above in_below Q_def Prof_def Pi_def below_Lin)      hence "(a',a) : F Q" using u `Q : Prof` by(simp add:unanimity_def)    } moreover    { assume "b≠b'"      hence "!!i. (b,b') : Q i" using d1 d2 `P : Prof`        by(simp add:in_above in_below Q_def Prof_def Pi_def below_Lin)      hence "(b,b') : F Q" using u `Q : Prof` by(simp add:unanimity_def)    }    ultimately have "(a',b') : F Q" using `F Q : Lin`      unfolding slo_defs trans_def by blast    moreover    have "∀i. (a',b') : Q i <-> (a',b') : P' i" using d1 d2 `P : Prof` 1      by(simp add:Q_def in_below in_above Prof_def Pi_def below_Lin) blast    ultimately have "(a',b') : F P'"      using `IIA F` `P' : Prof` `Q : Prof` unfolding IIA_def by blast  } note 1 = this  { fix a b a' b' and P P'    assume "a≠b" "a'≠b'" "a≠b'" "b≠a'" "P : Prof" "P' : Prof"           "∀i. (a,b) : P i <-> (a',b') : P' i"    hence "(a,b) : F P <-> (a',b') : F P'" using 1 by blast  } note 2 = this  { fix a b P P'    assume "a≠b" "P : Prof" "P' : Prof" and      iff: "∀i. (a,b) : P i <-> (b,a) : P' i"    from `a≠b` obtain c where dist: "distinct[a,b,c]" using third_alt by metis    let ?Q = "%p. below (P p) c b"    let ?R = "%p. below (?Q p) b a"    let ?S = "%p. below (?R p) a c"    have "?Q : Prof" using `P : Prof` dist      by(auto simp add:Prof_def Pi_def below_Lin)    hence "?R : Prof" using dist by(auto simp add:Prof_def Pi_def below_Lin)    hence "?S : Prof" using dist by(auto simp add:Prof_def Pi_def below_Lin)    have "∀i. (a,b) : P i <-> (a,c) : ?Q i" using `P : Prof` dist      by(auto simp add:in_below Prof_def Pi_def)    hence ab: "(a,b) : F P <-> (a,c) : F ?Q"      using 2 `P : Prof` `?Q : Prof` dist[simplified] by (blast)    have "∀i. (a,c) : ?Q i <-> (b,c) : ?R i" using `P : Prof` dist      by(auto simp add:in_below Prof_def Pi_def below_Lin)    hence ac: "(a,c) : F ?Q <-> (b,c) : F ?R"      using 2 `?Q : Prof` `?R : Prof` dist[simplified] by (blast)    have "∀i. (b,c) : ?R i <-> (b,a) : ?S i" using `P : Prof` dist      by(auto simp add:in_below Prof_def Pi_def below_Lin)    hence bc: "(b,c) : F ?R <-> (b,a) : F ?S"      using `?R : Prof` `?S : Prof` dist[simplified]      apply - apply(rule 2) by fast+    have "∀i. (b,a) : ?S i <-> (a,b) : P i" using `P : Prof` dist      by(auto simp add:in_below Prof_def Pi_def below_Lin)    hence "∀i. (b,a) : ?S i <-> (b,a) : P' i" using iff by blast    hence ba: "(b,a) : F ?S <-> (b,a) : F P'"      using `IIA F` `P' : Prof` `?S : Prof` unfolding IIA_def by fast    from ab ac bc ba have "(a,b) : F P <-> (b,a) : F P'" by simp  } note 3 = this  { fix a b c P P'    assume A: "a≠b" "b≠c" "a≠c" "P : Prof" "P' : Prof" and      iff: "∀i. (a,b) : P i <-> (b,c) : P' i"    hence "∀i. (b,a) : (converse o P)i <-> (b,c) : P' i" by simp    moreover have cP: "converse o P : Prof"      using `P:Prof` by(simp add:Prof_def Pi_def)    ultimately have "(b,a) : F(converse o P) <-> (b,c) : F P'" using A      apply - apply(rule 2) by fast+    moreover have "(a,b) : F P <-> (b,a) : F(converse o P)"      by (rule 3[OF `a≠b` `P:Prof` cP]) simp    ultimately have "(a,b) : F P <-> (b,c) : F P'" by blast  } note 4 = this  { fix a b a' b' :: alt and P P'    assume A: "a≠b" "a'≠b'" "P : Prof" "P' : Prof"      "∀i. (a,b) : P i <-> (a',b') : P' i"    have "(a,b) : F P <-> (a',b') : F P'"    proof-      { assume "a≠b' & b≠a'" hence ?thesis using 2 A by blast }      moreover      { assume "a=b' & b≠a'" hence ?thesis using 4 A by blast }      moreover      { assume "a≠b' & b=a'" hence ?thesis using 4 A by blast }      moreover      { assume "a=b' & b=a'" hence ?thesis using 3 A by blast }      ultimately show ?thesis by blast    qed  } note pairwise_neutrality = this  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)  obtain a b :: alt where "a ≠ b" using alt3 by auto  obtain Lab where "(a,b) : Lab" "Lab:Lin" using `a≠b` by (metis complete_Lin)  hence "(b,a) ∉ Lab" by(simp add:slo_defs trans_def) metis  obtain Lba where "(b,a) : Lba" "Lba:Lin" using `a≠b` by (metis complete_Lin)  hence "(a,b) ∉ Lba" by(simp add:slo_defs trans_def) metis  let ?Pi = "%n. %i. if h i < n then Lab else Lba"  have PiProf: "!!n. ?Pi n : Prof" using `Lab:Lin` `Lba:Lin`    unfolding Prof_def Pi_def by simp  have "EX n<N. (∀m≤n. (b,a) : F(?Pi m)) & (a,b) : F(?Pi(n+1))"  proof -    have 0: "!!n. F(?Pi n) : Lin" using `F : SWF` PiProf by(simp add:Pi_def)    have "F(%i. Lba):Lin" using `F:SWF` `Lba:Lin` by(simp add:Prof_def Pi_def)    hence 1: "(a,b) ∉ F(?Pi 0)" using u `(a,b) ∉ Lba` `Lba:Lin` `Lba:Lin` `a≠b`      by(simp add:unanimity_def notin_Lin_iff const_Lin_Prof)    have "?Pi N = (%p. Lab)" using surjh [THEN equalityD1]      by(auto simp: subset_eq)    moreover    have "F(%i. Lab):Lin" using `F:SWF` `Lab:Lin` by(simp add:Prof_def Pi_def)    ultimately have 2: "(a,b) ∈ F(?Pi N)" using u `(a,b) : Lab` `Lab:Lin`      by(simp add:unanimity_def const_Lin_Prof)    with ex_least_nat_less[of "%n. (a,b) : F(?Pi n)",OF 1 2]      notin_Lin_iff[OF 0 `a≠b`]    show ?thesis by simp  qed  then obtain n where n: "n<N" "∀m≤n. (b,a) : F(?Pi m)" "(a,b) : F(?Pi(n+1))"    by blast  have "dictator F (inv h n)"  proof (rule dictatorI [OF `F : SWF`], auto)    fix P c d assume "P ∈ Prof" "c≠d" "(c,d) ∈ P(inv h n)"    then obtain e where dist: "distinct[c,d,e]" using third_alt by metis    let ?W = "%i. if h i < n then mktop (P i) e else                  if h i = n then above (P i) c e else mkbot (P i) e"    have "?W : Prof" using `P : Prof` dist      by(simp add:Pi_def Prof_def mkbot_Lin mktop_Lin above_Lin)    have "∀i. (c,d) : P i <-> (c,d) : ?W i" using dist `P : Prof`      by(auto simp: in_above in_mkbot in_mktop Prof_def Pi_def)    hence PW: "(c,d) : F P <-> (c,d) : F ?W"      using `IIA F`[unfolded IIA_def] `P:Prof` `?W:Prof` by fast    have "∀i. (c,e) : ?W i <-> (a,b) : ?Pi (n+1) i" using dist `P : Prof`      by (auto simp: `(a,b):Lab` `(a,b)∉Lba`        in_mkbot in_mktop in_above Prof_def Pi_def)    hence "(c,e) : F ?W <-> (a,b) : F(?Pi(n+1))"      using pairwise_neutrality[of c e a b ?W "?Pi(n+1)"]        `a≠b` dist `?W : Prof` PiProf by simp    hence "(c,e) : F ?W" using n(3) by blast    have "∀i. (e,d) : ?W i <-> (b,a) : ?Pi n i"      using dist `P : Prof` `(c,d) ∈ P(inv h n)` `inj h`      by(auto simp: `(b,a):Lba` `(b,a)∉Lab`        in_mkbot in_mktop in_above Prof_def Pi_def)    hence "(e,d) : F ?W <-> (b,a) : F(?Pi n)"      using pairwise_neutrality[of e d b a ?W "?Pi n"]        `a≠b` dist `?W : Prof` PiProf by simp blast    hence "(e,d) : F ?W" using n(2) by auto    with `(c,e) : F ?W` `?W : Prof` `F:SWF`    have "(c,d) ∈ F ?W" unfolding Pi_def slo_defs trans_def by blast    thus "(c,d) ∈ F P" using PW by blast  qed  thus ?thesis ..qedend`