Theory Arrow_Order

(*  Author:     Tobias Nipkow, 2007  *)

section "Arrow's Theorem for Strict Linear Orders"

theory Arrow_Order imports Main "HOL-Library.FuncSet"
begin

text‹This theory formalizes the third proof due to
Geanakoplos~\<^cite>‹"Geanakoplos05"›.  Preferences are modeled as strict
linear orderings. The set of alternatives need not be finite.

Individuals are assumed to be finite but are not a priori identified with an
initial segment of the naturals. In retrospect this generality appears
gratuitous and complicates some of the low-level reasoning where we use a
bijection with such an initial segment.›

typedecl alt
typedecl indi

abbreviation "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 metis

lemma alt2: "∃b::alt. b ≠ a"
using alt3 by simp metis

type_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_def

lemma notin_Lin_iff: "L : Lin ⟹ x≠y ⟹ (x,y) ∉ L ⟷ (y,x) : L"
apply(auto simp add: slo_defs)
apply(metis trans_def)
done

lemma converse_in_Lin[simp]: "L¯ : Lin ⟷ L : Lin"
apply (simp add: slo_defs)
apply blast
done

lemma 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)
done

abbreviation
 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_def
apply(simp)
apply blast
done

lemma above_Lin: "x≠y ⟹ L : Lin ⟹ above L x y : Lin"
unfolding slo_defs above_def trans_def
apply(simp)
apply blast
done

declare [[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)
done

lemma const_Lin_Prof: "L:Lin ⟹ (%p. L) : Prof"
by(simp add:Prof_def Pi_def)

lemma complete_Lin: assumes "a≠b" shows "∃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)
qed

declare Let_def[simp]

theorem Arrow: assumes "F : SWF" and u: "unanimity F" and "IIA F"
shows "∃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"
    define Q where
      "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')" for i
    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 safe metis
    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] 2
      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 2
      by metis
    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 "∃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)"] 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 ..
qed

end