Theory Randomised_Social_Choice.Order_Predicates

(*  
  Title:    Order_Predicates.thy
  Author:   Manuel Eberl, TU München

  Locales for order relations modelled as predicates (as opposed to sets of pairs).
*)
section ‹Order Relations as Binary Predicates›

theory Order_Predicates
imports 
  Main
  "HOL-Library.Disjoint_Sets"
  "HOL-Combinatorics.Permutations"
  "List-Index.List_Index"
begin

subsection ‹Basic Operations on Relations›

text ‹The type of binary relations›
type_synonym 'a relation = "'a ⇒ 'a ⇒ bool"

definition map_relation :: "('a ⇒ 'b) ⇒ 'b relation ⇒ 'a relation" where
  "map_relation f R = (λx y. R (f x) (f y))"

definition restrict_relation :: "'a set ⇒ 'a relation ⇒ 'a relation" where
  "restrict_relation A R = (λx y. x ∈ A ∧ y ∈ A ∧ R x y)"

lemma restrict_relation_restrict_relation [simp]:
  "restrict_relation A (restrict_relation B R) = restrict_relation (A ∩ B) R"
  by (intro ext) (auto simp add: restrict_relation_def)

lemma restrict_relation_empty [simp]: "restrict_relation {} R = (λ_ _. False)"
  by (simp add: restrict_relation_def)

lemma restrict_relation_UNIV [simp]: "restrict_relation UNIV R = R"
  by (simp add: restrict_relation_def)


subsection ‹Preorders›

text ‹Preorders are reflexive and transitive binary relations.›
locale preorder_on =
  fixes carrier :: "'a set"
  fixes le :: "'a relation"
  assumes not_outside: "le x y ⟹ x ∈ carrier" "le x y ⟹ y ∈ carrier"
  assumes refl: "x ∈ carrier ⟹ le x x"
  assumes trans: "le x y ⟹ le y z ⟹ le x z"
begin

lemma carrier_eq: "carrier = {x. le x x}"
  using not_outside refl by auto
  
lemma preorder_on_map:
  "preorder_on (f -` carrier) (map_relation f le)"
  by unfold_locales (auto dest: not_outside simp: map_relation_def refl elim: trans)
  
lemma preorder_on_restrict:
  "preorder_on (carrier ∩ A) (restrict_relation A le)"
  by unfold_locales (auto simp: restrict_relation_def refl intro: trans not_outside)

lemma preorder_on_restrict_subset:
  "A ⊆ carrier ⟹ preorder_on A (restrict_relation A le)"
  using preorder_on_restrict[of A] by (simp add: Int_absorb1)

lemma restrict_relation_carrier [simp]:
  "restrict_relation carrier le = le"
  using not_outside by (intro ext) (auto simp add: restrict_relation_def)

end
  

subsection ‹Total preorders›

text ‹Total preorders are preorders where any two elements are comparable.›
locale total_preorder_on = preorder_on +
  assumes total: "x ∈ carrier ⟹ y ∈ carrier ⟹ le x y ∨ le y x"
begin

lemma total': "¬le x y ⟹ x ∈ carrier ⟹ y ∈ carrier ⟹ le y x"
  using total[of x y] by blast

lemma total_preorder_on_map:
  "total_preorder_on (f -` carrier) (map_relation f le)"
proof -
  interpret R': preorder_on "f -` carrier" "map_relation f le"
    using preorder_on_map[of f] .
  show ?thesis by unfold_locales (simp add: map_relation_def total)
qed

lemma total_preorder_on_restrict:
  "total_preorder_on (carrier ∩ A) (restrict_relation A le)"
proof -
  interpret R': preorder_on "carrier ∩ A" "restrict_relation A le"
    by (rule preorder_on_restrict)
  from total show ?thesis
    by unfold_locales (auto simp: restrict_relation_def)
qed

lemma total_preorder_on_restrict_subset:
  "A ⊆ carrier ⟹ total_preorder_on A (restrict_relation A le)"
  using total_preorder_on_restrict[of A] by (simp add: Int_absorb1)

end


text ‹Some fancy notation for order relations›
abbreviation (input) weakly_preferred :: "'a ⇒ 'a relation ⇒ 'a ⇒ bool"
    (‹_ ≼[_] _› [51,10,51] 60) where
  "a ≼[R] b ≡ R a b"
  
definition strongly_preferred (‹_ ≺[_] _› [51,10,51] 60) where
  "a ≺[R] b ≡ (a ≼[R] b) ∧ ¬(b ≼[R] a)"

definition indifferent (‹_ ∼[_] _› [51,10,51] 60) where
  "a ∼[R] b ≡ (a ≼[R] b) ∧ (b ≼[R] a)"

abbreviation (input) weakly_not_preferred (‹_ ≽[_] _› [51,10,51] 60) where
  "a ≽[R] b ≡ b ≼[R] a"
  term "a ≽[R] b ⟷ b ≼[R] a"

abbreviation (input) strongly_not_preferred (‹_ ≻[_] _› [51,10,51] 60) where
  "a ≻[R] b ≡ b ≺[R] a"

context preorder_on
begin

lemma strict_trans: "a ≺[le] b ⟹ b ≺[le] c ⟹ a ≺[le] c"
  unfolding strongly_preferred_def by (blast intro: trans)

lemma weak_strict_trans: "a ≼[le] b ⟹ b ≺[le] c ⟹ a ≺[le] c"
  unfolding strongly_preferred_def by (blast intro: trans)

lemma strict_weak_trans: "a ≺[le] b ⟹ b ≼[le] c ⟹ a ≺[le] c"
  unfolding strongly_preferred_def by (blast intro: trans)

end
  
lemma (in total_preorder_on) not_weakly_preferred_iff:
  "a ∈ carrier ⟹ b ∈ carrier ⟹ ¬a ≼[le] b ⟷ b ≺[le] a"
  using total[of a b] by (auto simp: strongly_preferred_def)

lemma (in total_preorder_on) not_strongly_preferred_iff:
  "a ∈ carrier ⟹ b ∈ carrier ⟹ ¬a ≺[le] b ⟷ b ≼[le] a"
  using total[of a b] by (auto simp: strongly_preferred_def)



subsection ‹Orders›

locale order_on = preorder_on +
  assumes antisymmetric: "le x y ⟹ le y x ⟹ x = y"

locale linorder_on = order_on carrier le + total_preorder_on carrier le for carrier le


subsection ‹Maximal elements›

text ‹
  Maximal elements are elements in a preorder for which there exists no strictly greater element.
›

definition Max_wrt_among :: "'a relation ⇒ 'a set ⇒ 'a set" where
  "Max_wrt_among R A = {x∈A. R x x ∧ (∀y∈A. R x y ⟶ R y x)}"

lemma Max_wrt_among_cong:
  assumes "restrict_relation A R = restrict_relation A R'"
  shows   "Max_wrt_among R A = Max_wrt_among R' A"
proof -
  from assms have "R x y ⟷ R' x y" if "x ∈ A" "y ∈ A" for x y
    using that by (auto simp: restrict_relation_def fun_eq_iff)
  thus ?thesis unfolding Max_wrt_among_def by blast
qed

definition Max_wrt :: "'a relation ⇒ 'a set" where
  "Max_wrt R = Max_wrt_among R UNIV"
  
lemma Max_wrt_altdef: "Max_wrt R = {x. R x x ∧ (∀y. R x y ⟶ R y x)}"
  unfolding Max_wrt_def Max_wrt_among_def by simp

context preorder_on
begin

lemma Max_wrt_among_preorder:
  "Max_wrt_among le A = {x∈carrier ∩ A. ∀y∈carrier ∩ A. le x y ⟶ le y x}"
  unfolding Max_wrt_among_def using not_outside refl by blast

lemma Max_wrt_preorder:
  "Max_wrt le = {x∈carrier. ∀y∈carrier. le x y ⟶ le y x}"
  unfolding Max_wrt_altdef using not_outside refl by blast

lemma Max_wrt_among_subset:
  "Max_wrt_among le A ⊆ carrier" "Max_wrt_among le A ⊆ A"
  unfolding Max_wrt_among_preorder by auto
  
lemma Max_wrt_subset:
  "Max_wrt le ⊆ carrier"
  unfolding Max_wrt_preorder by auto

lemma Max_wrt_among_nonempty:
  assumes "B ∩ carrier ≠ {}" "finite (B ∩ carrier)"
  shows   "Max_wrt_among le B ≠ {}"
proof -
  define A where "A = B ∩ carrier"
  have "A ⊆ carrier" by (simp add: A_def)
  from assms(2,1)[folded A_def] this have "{x∈A. (∀y∈A. le x y ⟶ le y x)} ≠ {}"
  proof (induction A rule: finite_ne_induct)
    case (singleton x)
    thus ?case by (auto simp: refl)
  next
    case (insert x A)
    then obtain y where y: "y ∈ A" "⋀z. z ∈ A ⟹ le y z ⟹ le z y" by blast
    thus ?case using insert.prems
      by (cases "le y x") (blast intro: trans)+
  qed
  thus ?thesis by (simp add: A_def Max_wrt_among_preorder Int_commute)
qed
  
lemma Max_wrt_nonempty:
  "carrier ≠ {} ⟹ finite carrier ⟹ Max_wrt le ≠ {}"
  using Max_wrt_among_nonempty[of UNIV] by (simp add: Max_wrt_def)

lemma Max_wrt_among_map_relation_vimage:
  "f -` Max_wrt_among le A ⊆ Max_wrt_among (map_relation f le) (f -` A)"
  by (auto simp: Max_wrt_among_def map_relation_def)

lemma Max_wrt_map_relation_vimage:
  "f -` Max_wrt le ⊆ Max_wrt (map_relation f le)"
  by (auto simp: Max_wrt_altdef map_relation_def)

lemma image_subset_vimage_the_inv_into: 
  assumes "inj_on f A" "B ⊆ A"
  shows   "f ` B ⊆ the_inv_into A f -` B"
  using assms by (auto simp: the_inv_into_f_f)

lemma Max_wrt_among_map_relation_bij_subset:
  assumes "bij (f :: 'a ⇒ 'b)"
  shows   "f ` Max_wrt_among le A ⊆ 
             Max_wrt_among (map_relation (inv f) le) (f ` A)"
  using assms Max_wrt_among_map_relation_vimage[of "inv f" A]
  by (simp add: bij_imp_bij_inv inv_inv_eq bij_vimage_eq_inv_image)
  
lemma Max_wrt_among_map_relation_bij:
  assumes "bij f"
  shows   "f ` Max_wrt_among le A = Max_wrt_among (map_relation (inv f) le) (f ` A)"
proof (intro equalityI Max_wrt_among_map_relation_bij_subset assms)
  interpret R: preorder_on "f ` carrier" "map_relation (inv f) le"
    using preorder_on_map[of "inv f"] assms 
      by (simp add: bij_imp_bij_inv bij_vimage_eq_inv_image inv_inv_eq)
  show "Max_wrt_among (map_relation (inv f) le) (f ` A) ⊆ f ` Max_wrt_among le A"
    unfolding Max_wrt_among_preorder R.Max_wrt_among_preorder 
    using assms bij_is_inj[OF assms]
    by (auto simp: map_relation_def inv_f_f image_Int [symmetric])
qed

lemma Max_wrt_map_relation_bij:
  "bij f ⟹ f ` Max_wrt le = Max_wrt (map_relation (inv f) le)"
proof -
  assume bij: "bij f"
  interpret R: preorder_on "f ` carrier" "map_relation (inv f) le"
    using preorder_on_map[of "inv f"] bij
      by (simp add: bij_imp_bij_inv bij_vimage_eq_inv_image inv_inv_eq)
  from bij show ?thesis
    unfolding R.Max_wrt_preorder Max_wrt_preorder
    by (auto simp: map_relation_def inv_f_f bij_is_inj)
qed

lemma Max_wrt_among_mono:
  "le x y ⟹ x ∈ Max_wrt_among le A ⟹ y ∈ A ⟹ y ∈ Max_wrt_among le A"
  using not_outside by (auto simp: Max_wrt_among_preorder intro: trans)

lemma Max_wrt_mono:
  "le x y ⟹ x ∈ Max_wrt le ⟹ y ∈ Max_wrt le"
  unfolding Max_wrt_def using Max_wrt_among_mono[of x y UNIV] by blast

end


context total_preorder_on
begin

lemma Max_wrt_among_total_preorder:
  "Max_wrt_among le A = {x∈carrier ∩ A. ∀y∈carrier ∩ A. le y x}"
  unfolding Max_wrt_among_preorder using total by blast

lemma Max_wrt_total_preorder:
  "Max_wrt le = {x∈carrier. ∀y∈carrier. le y x}"
  unfolding Max_wrt_preorder using total by blast

lemma decompose_Max:
  assumes A: "A ⊆ carrier"
  defines "M ≡ Max_wrt_among le A"
  shows   "restrict_relation A le = (λx y. x ∈ A ∧ y ∈ M ∨ (y ∉ M ∧ restrict_relation (A - M) le x y))"
  using A by (intro ext) (auto simp: M_def Max_wrt_among_total_preorder 
                            restrict_relation_def Int_absorb1 intro: trans)

end


subsection ‹Weak rankings›

inductive of_weak_ranking :: "'alt set list ⇒ 'alt relation" where
  "i ≤ j ⟹ i < length xs ⟹ j < length xs ⟹ x ∈ xs ! i ⟹ y ∈ xs ! j ⟹ 
     x ≽[of_weak_ranking xs] y"

lemma of_weak_ranking_Nil [simp]: "of_weak_ranking [] = (λ_ _. False)"
  by (intro ext) (simp add: of_weak_ranking.simps)

lemma of_weak_ranking_Nil' [code]: "of_weak_ranking [] x y = False"
  by simp
  
lemma of_weak_ranking_Cons [code]:
  "x ≽[of_weak_ranking (z#zs)] y ⟷ x ∈ z ∧ y ∈ ⋃(set (z#zs)) ∨ x ≽[of_weak_ranking zs] y" 
      (is "?lhs ⟷ ?rhs")
proof 
  assume ?lhs
  then obtain i j 
    where ij: "i < length (z#zs)" "j < length (z#zs)" "i ≤ j" "x ∈ (z#zs) ! i" "y ∈ (z#zs) ! j"
    by (blast elim: of_weak_ranking.cases)
  thus ?rhs by (cases i; cases j) (force intro: of_weak_ranking.intros)+
next
  assume ?rhs
  thus ?lhs
  proof (elim disjE conjE)
    assume "x ∈ z" "y ∈ ⋃(set (z # zs))"
    then obtain j where "j < length (z # zs)" "y ∈ (z # zs) ! j" 
      by (subst (asm) set_conv_nth) auto
    with ‹x ∈ z› show "of_weak_ranking (z # zs) y x" 
      by (intro of_weak_ranking.intros[of 0 j]) auto
  next
    assume "of_weak_ranking zs y x"
    then obtain i j where "i < length zs" "j < length zs" "i ≤ j" "x ∈ zs ! i" "y ∈ zs ! j"
      by (blast elim: of_weak_ranking.cases)
    thus "of_weak_ranking (z # zs) y x"
      by (intro of_weak_ranking.intros[of "Suc i" "Suc j"]) auto
  qed
qed

lemma of_weak_ranking_indifference:
  assumes "A ∈ set xs" "x ∈ A" "y ∈ A"
  shows   "x ≼[of_weak_ranking xs] y"
  using assms by (induction xs) (auto simp: of_weak_ranking_Cons)


lemma of_weak_ranking_map:
  "map_relation f (of_weak_ranking xs) = of_weak_ranking (map ((-`) f) xs)"
  by (intro ext, induction xs)
     (simp_all add: map_relation_def of_weak_ranking_Cons)

lemma of_weak_ranking_permute':
  assumes "f permutes (⋃(set xs))"
  shows   "map_relation f (of_weak_ranking xs) = of_weak_ranking (map ((`) (inv f)) xs)"
proof -
  have "map_relation f (of_weak_ranking xs) = of_weak_ranking (map ((-`) f) xs)"
    by (rule of_weak_ranking_map)
  also from assms have "map ((-`) f) xs = map ((`) (inv f)) xs"
    by (intro map_cong refl) (simp_all add: bij_vimage_eq_inv_image permutes_bij)
  finally show ?thesis .
qed 

lemma of_weak_ranking_permute:
  assumes "f permutes (⋃(set xs))"
  shows   "of_weak_ranking (map ((`) f) xs) = map_relation (inv f) (of_weak_ranking xs)"
  using of_weak_ranking_permute'[OF permutes_inv[OF assms]] assms
  by (simp add: inv_inv_eq permutes_bij)

definition is_weak_ranking where
  "is_weak_ranking xs ⟷ ({} ∉ set xs) ∧
     (∀i j. i < length xs ∧ j < length xs ∧ i ≠ j ⟶ xs ! i ∩ xs ! j = {})"

definition is_finite_weak_ranking where
  "is_finite_weak_ranking xs ⟷ is_weak_ranking xs ∧ (∀x∈set xs. finite x)"

definition weak_ranking :: "'alt relation ⇒ 'alt set list" where
  "weak_ranking R = (SOME xs. is_weak_ranking xs ∧ R = of_weak_ranking xs)"

lemma is_weak_rankingI [intro?]:
  assumes "{} ∉ set xs" "⋀i j. i < length xs ⟹ j < length xs ⟹ i ≠ j ⟹ xs ! i ∩ xs ! j = {}"
  shows   "is_weak_ranking xs"
  using assms by (auto simp add: is_weak_ranking_def)

lemma is_weak_ranking_nonempty: "is_weak_ranking xs ⟹ {} ∉ set xs"
  by (simp add: is_weak_ranking_def) 
     
lemma is_weak_rankingD:
  assumes "is_weak_ranking xs" "i < length xs" "j < length xs" "i ≠ j"
  shows   "xs ! i ∩ xs ! j = {}"
  using assms by (simp add: is_weak_ranking_def)
  
lemma is_weak_ranking_iff:
  "is_weak_ranking xs ⟷ distinct xs ∧ disjoint (set xs) ∧ {} ∉ set xs"
proof safe
  assume wf: "is_weak_ranking xs"
  from wf show "disjoint (set xs)"
    by (auto simp: disjoint_def is_weak_ranking_def set_conv_nth)
  show "distinct xs"
  proof (subst distinct_conv_nth, safe)
    fix i j assume ij: "i < length xs" "j < length xs" "i ≠ j" "xs ! i = xs ! j"
    then have "xs ! i ∩ xs ! j = {}" by (intro is_weak_rankingD wf)
    with ij have "xs ! i = {}" by simp
    with ij have "{} ∈ set xs" by (auto simp: set_conv_nth)
    moreover from wf ij have "{} ∉ set xs" by (intro is_weak_ranking_nonempty wf)
    ultimately show False by contradiction
 qed
next
  assume A: "distinct xs" "disjoint (set xs)" "{} ∉ set xs"
  thus "is_weak_ranking xs"
    by (intro is_weak_rankingI) (auto simp: disjoint_def distinct_conv_nth)
qed (simp_all add: is_weak_ranking_nonempty)

lemma is_weak_ranking_rev [simp]: "is_weak_ranking (rev xs) ⟷ is_weak_ranking xs"
  by (simp add: is_weak_ranking_iff)

lemma is_weak_ranking_map_inj:
  assumes "is_weak_ranking xs" "inj_on f (⋃(set xs))"
  shows   "is_weak_ranking (map ((`) f) xs)"
  using assms by (auto simp: is_weak_ranking_iff distinct_map inj_on_image disjoint_image)

lemma of_weak_ranking_rev [simp]:
  "of_weak_ranking (rev xs) (x::'a) y ⟷ of_weak_ranking xs y x"
proof -
  have "of_weak_ranking (rev xs) y x" if "of_weak_ranking xs x y" for xs and x y :: 'a
  proof -
    from that obtain i j where "i < length xs" "j < length xs" "x ∈ xs ! i" "y ∈ xs ! j" "i ≥ j"
      by (elim of_weak_ranking.cases) simp_all
    thus ?thesis
      by (intro of_weak_ranking.intros[of "length xs - i - 1" "length xs - j - 1"] diff_le_mono2)
         (auto simp: diff_le_mono2 rev_nth)
  qed
  from this[of xs y x] this[of "rev xs" x y] show ?thesis by (intro iffI) simp_all
qed


lemma is_weak_ranking_Nil [simp, code]: "is_weak_ranking []"
  by (auto simp: is_weak_ranking_def)

lemma is_finite_weak_ranking_Nil [simp, code]: "is_finite_weak_ranking []"
  by (auto simp: is_finite_weak_ranking_def)

lemma is_weak_ranking_Cons_empty [simp]:
  "¬is_weak_ranking ({} # xs)" by (simp add: is_weak_ranking_def)

lemma is_finite_weak_ranking_Cons_empty [simp]:
  "¬is_finite_weak_ranking ({} # xs)" by (simp add: is_finite_weak_ranking_def)
  
lemma is_weak_ranking_singleton [simp]:
  "is_weak_ranking [x] ⟷ x ≠ {}" 
  by (auto simp add: is_weak_ranking_def)

lemma is_finite_weak_ranking_singleton [simp]:
  "is_finite_weak_ranking [x] ⟷ x ≠ {} ∧ finite x" 
  by (auto simp add: is_finite_weak_ranking_def)
  
lemma is_weak_ranking_append:
  "is_weak_ranking (xs @ ys) ⟷ 
      is_weak_ranking xs ∧ is_weak_ranking ys ∧
      (set xs ∩ set ys = {} ∧ ⋃(set xs) ∩ ⋃(set ys) = {})"
  by (simp only: is_weak_ranking_iff)
     (auto dest: disjointD disjoint_unionD1 disjoint_unionD2 intro: disjoint_union)

lemma is_weak_ranking_Cons [code]:
  "is_weak_ranking (x # xs) ⟷ 
      x ≠ {} ∧ is_weak_ranking xs ∧ x ∩ ⋃(set xs) = {}"
  using is_weak_ranking_append[of "[x]" xs] by auto

lemma is_finite_weak_ranking_Cons [code]:
  "is_finite_weak_ranking (x # xs) ⟷ 
      x ≠ {} ∧ finite x ∧ is_finite_weak_ranking xs ∧ x ∩ ⋃(set xs) = {}"
  by (auto simp add: is_finite_weak_ranking_def is_weak_ranking_Cons)

primrec is_weak_ranking_aux where
  "is_weak_ranking_aux A [] ⟷ True"
| "is_weak_ranking_aux A (x#xs) ⟷ x ≠ {} ∧
       A ∩ x = {} ∧ is_weak_ranking_aux (A ∪ x) xs"


lemma is_weak_ranking_aux:
  "is_weak_ranking_aux A xs ⟷ A ∩ ⋃(set xs) = {} ∧ is_weak_ranking xs"
  by (induction xs arbitrary: A) (auto simp: is_weak_ranking_Cons)

lemma is_weak_ranking_code [code]:
  "is_weak_ranking xs ⟷ is_weak_ranking_aux {} xs"
  by (subst is_weak_ranking_aux) auto

lemma of_weak_ranking_altdef:
  assumes "is_weak_ranking xs" "x ∈ ⋃(set xs)" "y ∈ ⋃(set xs)"
  shows   "of_weak_ranking xs x y ⟷ 
             find_index ((∈) x) xs ≥ find_index ((∈) y) xs"
proof -
 from assms 
    have A: "find_index ((∈) x) xs < length xs" "find_index ((∈) y) xs < length xs"
    by (simp_all add: find_index_less_size_conv)
 from this[THEN nth_find_index] 
    have B: "x ∈ xs ! find_index ((∈) x) xs" "y ∈ xs ! find_index ((∈) y) xs" .
  show ?thesis
  proof
    assume "of_weak_ranking xs x y"
    then obtain i j where ij: "j ≤ i" "i < length xs" "j < length xs" "x ∈ xs ! i" "y ∈ xs !j"
      by (cases rule: of_weak_ranking.cases) simp_all
    with A B have "i = find_index ((∈) x) xs" "j = find_index ((∈) y) xs"
      using assms(1) unfolding is_weak_ranking_def by blast+
    with ij show "find_index ((∈) x) xs ≥ find_index ((∈) y) xs" by simp
  next
    assume "find_index ((∈) x) xs ≥ find_index ((∈) y) xs"
    from this A(2,1) B(2,1) show "of_weak_ranking xs x y"
      by (rule of_weak_ranking.intros)
  qed
qed

  
lemma total_preorder_of_weak_ranking:
  assumes "⋃(set xs) = A"
  assumes "is_weak_ranking xs"
  shows   "total_preorder_on A (of_weak_ranking xs)"
proof
  fix x y assume "x ≼[of_weak_ranking xs] y"
  with assms show "x ∈ A" "y ∈ A"
    by (auto elim!: of_weak_ranking.cases)
next
  fix x assume "x ∈ A"
  with assms(1) obtain i where "i < length xs" "x ∈ xs ! i"
    by (auto simp: set_conv_nth)
  thus "x ≼[of_weak_ranking xs] x" by (auto intro: of_weak_ranking.intros)
next
  fix x y assume "x ∈ A" "y ∈ A"
  with assms(1) obtain i j where ij: "i < length xs" "j < length xs" "x ∈ xs ! i" "y ∈ xs ! j"
    by (auto simp: set_conv_nth)
  consider "i ≤ j" | "j ≤ i" by force
  thus "x ≼[of_weak_ranking xs] y ∨ y ≼[of_weak_ranking xs] x"
    by cases (insert ij, (blast intro: of_weak_ranking.intros)+)
next
  fix x y z
  assume A: "x ≼[of_weak_ranking xs] y" and B: "y ≼[of_weak_ranking xs] z"
  from A obtain i j 
    where ij: "i ≥ j" "i < length xs" "j < length xs" "x ∈ xs ! i" "y ∈ xs ! j"
    by (auto elim!: of_weak_ranking.cases)
  moreover from B obtain j' k 
    where j'k: "j' ≥ k" "j' < length xs" "k < length xs" "y ∈ xs ! j'" "z ∈ xs ! k"
    by (auto elim!: of_weak_ranking.cases)
  moreover from ij j'k is_weak_rankingD[OF assms(2), of j j'] 
    have "j = j'" by blast
  ultimately show "x ≼[of_weak_ranking xs] z" by (auto intro: of_weak_ranking.intros[of k i])
qed

lemma restrict_relation_of_weak_ranking_Cons:
  assumes "is_weak_ranking (A # As)"
  shows   "restrict_relation (⋃(set As)) (of_weak_ranking (A # As)) = of_weak_ranking As"
proof -
  from assms interpret R: total_preorder_on "⋃(set As)" "of_weak_ranking As"
    by (intro total_preorder_of_weak_ranking)
       (simp_all add: is_weak_ranking_Cons)
  from assms show ?thesis using R.not_outside
    by (intro ext) (auto simp: restrict_relation_def of_weak_ranking_Cons
                     is_weak_ranking_Cons)
qed




lemmas of_weak_ranking_wf = 
  total_preorder_of_weak_ranking is_weak_ranking_code insert_commute


(* Test *)
lemma "total_preorder_on {1,2,3,4::nat} (of_weak_ranking [{1,3},{2},{4}])"
  by (simp add: of_weak_ranking_wf)


context
  fixes x :: "'alt set" and xs :: "'alt set list"
  assumes wf: "is_weak_ranking (x#xs)"
begin

interpretation R: total_preorder_on "⋃(set (x#xs))" "of_weak_ranking (x#xs)"
  by (intro total_preorder_of_weak_ranking) (simp_all add: wf)

lemma of_weak_ranking_imp_in_set:
  assumes "of_weak_ranking xs a b"
  shows   "a ∈ ⋃(set xs)" "b ∈ ⋃(set xs)"
  using assms by (fastforce elim!: of_weak_ranking.cases)+

lemma of_weak_ranking_Cons':
  assumes "a ∈ ⋃(set (x#xs))" "b ∈ ⋃(set (x#xs))"
  shows   "of_weak_ranking (x#xs) a b ⟷ b ∈ x ∨ (a ∉ x ∧ of_weak_ranking xs a b)"
proof
  assume "of_weak_ranking (x # xs) a b"
  with wf of_weak_ranking_imp_in_set[of a b] 
    show "(b ∈ x ∨  a ∉ x ∧ of_weak_ranking xs a b)"
    by (auto simp: is_weak_ranking_Cons of_weak_ranking_Cons)
next
  assume "b ∈ x ∨ a ∉ x ∧ of_weak_ranking xs a b"
  with assms show "of_weak_ranking (x#xs) a b"
    by (fastforce simp: of_weak_ranking_Cons)
qed

lemma Max_wrt_among_of_weak_ranking_Cons1:
  assumes "x ∩ A = {}"
  shows   "Max_wrt_among (of_weak_ranking (x#xs)) A = Max_wrt_among (of_weak_ranking xs) A"
proof -
  from wf interpret R': total_preorder_on "⋃(set xs)" "of_weak_ranking xs"
    by (intro total_preorder_of_weak_ranking) (simp_all add: is_weak_ranking_Cons)
  from assms show ?thesis
    by (auto simp: R.Max_wrt_among_total_preorder
          R'.Max_wrt_among_total_preorder of_weak_ranking_Cons)
qed

lemma Max_wrt_among_of_weak_ranking_Cons2:
  assumes "x ∩ A ≠ {}"
  shows   "Max_wrt_among (of_weak_ranking (x#xs)) A = x ∩ A"
proof -
  from wf interpret R': total_preorder_on "⋃(set xs)" "of_weak_ranking xs"
    by (intro total_preorder_of_weak_ranking) (simp_all add: is_weak_ranking_Cons)
  from assms obtain a where "a ∈ x ∩ A" by blast
  with wf R'.not_outside(1)[of a] show ?thesis
    by (auto simp: R.Max_wrt_among_total_preorder is_weak_ranking_Cons
          R'.Max_wrt_among_total_preorder of_weak_ranking_Cons)
qed

lemma Max_wrt_among_of_weak_ranking_Cons:
  "Max_wrt_among (of_weak_ranking (x#xs)) A =
     (if x ∩ A = {} then Max_wrt_among (of_weak_ranking xs) A else x ∩ A)"
  using Max_wrt_among_of_weak_ranking_Cons1 Max_wrt_among_of_weak_ranking_Cons2 by simp

lemma Max_wrt_of_weak_ranking_Cons:
  "Max_wrt (of_weak_ranking (x#xs)) = x"
  using wf by (simp add: is_weak_ranking_Cons Max_wrt_def Max_wrt_among_of_weak_ranking_Cons)

end

lemma Max_wrt_of_weak_ranking:
  assumes "is_weak_ranking xs"
  shows   "Max_wrt (of_weak_ranking xs) = (if xs = [] then {} else hd xs)"
proof (cases xs)
  case Nil
  hence "of_weak_ranking xs = (λ_ _. False)" by (intro ext) simp_all
  with Nil show ?thesis by (simp add: Max_wrt_def Max_wrt_among_def)
next
  case (Cons x xs')
  with assms show ?thesis by (simp add: Max_wrt_of_weak_ranking_Cons)
qed


locale finite_total_preorder_on = total_preorder_on +
  assumes finite_carrier [intro]: "finite carrier"
begin

lemma finite_total_preorder_on_map:
  assumes "finite (f -` carrier)"
  shows   "finite_total_preorder_on (f -` carrier) (map_relation f le)"
proof -
  interpret R': total_preorder_on "f -` carrier" "map_relation f le"
    using total_preorder_on_map[of f] .
  from assms show ?thesis by unfold_locales simp
qed

function weak_ranking_aux :: "'a set ⇒ 'a set list" where
  "weak_ranking_aux {} = []"
| "A ≠ {} ⟹ A ⊆ carrier ⟹ weak_ranking_aux A =
     Max_wrt_among le A # weak_ranking_aux (A - Max_wrt_among le A)"
| "¬(A ⊆ carrier) ⟹ weak_ranking_aux A = undefined"
by blast simp_all
termination proof (relation "Wellfounded.measure card")
  fix A
  let ?B = "Max_wrt_among le A"
  assume A: "A ≠ {}" "A ⊆ carrier"
  moreover from A(2) have "finite A" by (rule finite_subset) blast
  moreover from A have "?B ≠ {}" "?B ⊆ A"
    by (intro Max_wrt_among_nonempty Max_wrt_among_subset; force)+
  ultimately have "card (A - ?B) < card A"
    by (intro psubset_card_mono) auto
  thus "(A - ?B, A) ∈ measure card" by simp
qed simp_all

lemma weak_ranking_aux_Union:
  "A ⊆ carrier ⟹ ⋃(set (weak_ranking_aux A)) = A"
proof (induction A rule: weak_ranking_aux.induct [case_names empty nonempty])
  case (nonempty A)
  with Max_wrt_among_subset[of A] show ?case by auto
qed simp_all

lemma weak_ranking_aux_wf:
  "A ⊆ carrier ⟹ is_weak_ranking (weak_ranking_aux A)"
proof (induction A rule: weak_ranking_aux.induct [case_names empty nonempty])
  case (nonempty A)
  have "is_weak_ranking (Max_wrt_among le A # weak_ranking_aux (A - Max_wrt_among le A))"
    unfolding is_weak_ranking_Cons
  proof (intro conjI)
    from nonempty.prems nonempty.hyps show "Max_wrt_among le A ≠ {}"
      by (intro Max_wrt_among_nonempty) auto
  next
    from nonempty.prems show "is_weak_ranking (weak_ranking_aux (A - Max_wrt_among le A))"
      by (intro nonempty.IH) blast
  next
    from nonempty.prems nonempty.hyps have "Max_wrt_among le A ≠ {}"
      by (intro Max_wrt_among_nonempty) auto
    moreover from nonempty.prems 
      have "⋃(set (weak_ranking_aux (A - Max_wrt_among le A))) = A - Max_wrt_among le A"
      by (intro weak_ranking_aux_Union) auto
    ultimately show "Max_wrt_among le A ∩ ⋃(set (weak_ranking_aux (A - Max_wrt_among le A))) = {}"
      by blast+
  qed
  with nonempty.prems nonempty.hyps show ?case by simp
qed simp_all    

lemma of_weak_ranking_weak_ranking_aux':
  assumes "A ⊆ carrier" "x ∈ A" "y ∈ A"
  shows   "of_weak_ranking (weak_ranking_aux A) x y ⟷ restrict_relation A le x y"
using assms
proof (induction A rule: weak_ranking_aux.induct [case_names empty nonempty])
  case (nonempty A)
  define M where "M = Max_wrt_among le A"
  from nonempty.prems nonempty.hyps have M: "M ⊆ A" unfolding M_def
    by (intro Max_wrt_among_subset)
  from nonempty.prems have in_MD: "le x y" if "x ∈ A" "y ∈ M" for x y
    using that unfolding M_def Max_wrt_among_total_preorder
    by (auto simp: Int_absorb1)
  from nonempty.prems have in_MI: "x ∈ M" if "y ∈ M" "x ∈ A"  "le y x" for x y
    using that unfolding M_def Max_wrt_among_total_preorder
    by (auto simp: Int_absorb1 intro: trans)

  from nonempty.prems nonempty.hyps
    have IH: "of_weak_ranking (weak_ranking_aux (A - M)) x y = 
                restrict_relation (A - M) le x y" if "x ∉ M" "y ∉ M"
       using that unfolding M_def by (intro nonempty.IH) auto
  from nonempty.prems 
    interpret R': total_preorder_on "A - M" "of_weak_ranking (weak_ranking_aux (A - M))"
    by (intro total_preorder_of_weak_ranking weak_ranking_aux_wf weak_ranking_aux_Union) auto
  
  from nonempty.prems nonempty.hyps M weak_ranking_aux_Union[of A] R'.not_outside[of x y] 
    show ?case
    by (cases "x ∈ M"; cases "y ∈ M")
       (auto simp: restrict_relation_def of_weak_ranking_Cons IH M_def [symmetric]
             intro: in_MD dest: in_MI)
qed simp_all

lemma of_weak_ranking_weak_ranking_aux:
  "of_weak_ranking (weak_ranking_aux carrier) = le"
proof (intro ext)
  fix x y
  have "is_weak_ranking (weak_ranking_aux carrier)" by (rule weak_ranking_aux_wf) simp
  then interpret R: total_preorder_on carrier "of_weak_ranking (weak_ranking_aux carrier)"
    by (intro total_preorder_of_weak_ranking weak_ranking_aux_wf weak_ranking_aux_Union)
       (simp_all add: weak_ranking_aux_Union)

  show "of_weak_ranking (weak_ranking_aux carrier) x y = le x y"
  proof (cases "x ∈ carrier ∧ y ∈ carrier")
    case True
    thus ?thesis
      using of_weak_ranking_weak_ranking_aux'[of carrier x y]  by simp
  next
    case False
    with R.not_outside have "of_weak_ranking (weak_ranking_aux carrier) x y = False"
      by auto
    also from not_outside False have "… = le x y" by auto
    finally show ?thesis .
  qed
qed

lemma weak_ranking_aux_unique':
  assumes "⋃(set As) ⊆ carrier" "is_weak_ranking As"
          "of_weak_ranking As = restrict_relation (⋃(set As)) le"
  shows   "As = weak_ranking_aux (⋃(set As))"
using assms
proof (induction As)
  case (Cons A As)
  have "restrict_relation (⋃(set As)) (of_weak_ranking (A # As)) = of_weak_ranking As"
    by (intro restrict_relation_of_weak_ranking_Cons Cons.prems)
  also have eq1: "of_weak_ranking (A # As) = restrict_relation (⋃(set (A # As))) le" by fact
  finally have eq: "of_weak_ranking As = restrict_relation (⋃(set As)) le"
    by (simp add: Int_absorb2)
  with Cons.prems have eq2: "weak_ranking_aux (⋃(set As)) = As"
    by (intro sym [OF Cons.IH]) (auto simp: is_weak_ranking_Cons)

  from eq1 have 
    "Max_wrt_among le (⋃(set (A # As))) = 
       Max_wrt_among (of_weak_ranking (A#As)) (⋃(set (A#As)))"
    by (intro Max_wrt_among_cong) simp_all
  also from Cons.prems have "… = A"
    by (subst Max_wrt_among_of_weak_ranking_Cons2)
       (simp_all add: is_weak_ranking_Cons)
  finally have Max: "Max_wrt_among le (⋃(set (A # As))) = A" .

  moreover from Cons.prems have "A ≠ {}" by (simp add: is_weak_ranking_Cons)
  ultimately have "weak_ranking_aux (⋃(set (A # As))) = A # weak_ranking_aux (A ∪ ⋃(set As) - A)" 
    using Cons.prems by simp
  also from Cons.prems have "A ∪ ⋃(set As) - A = ⋃(set As)"
    by (auto simp: is_weak_ranking_Cons)
  also from eq2 have "weak_ranking_aux … = As" .
  finally show ?case ..
qed simp_all

lemma weak_ranking_aux_unique:
  assumes "is_weak_ranking As" "of_weak_ranking As = le"
  shows   "As = weak_ranking_aux carrier"
proof -
  interpret R: total_preorder_on "⋃(set As)" "of_weak_ranking As"
    by (intro total_preorder_of_weak_ranking assms) simp_all
  from assms have "x ∈ ⋃(set As) ⟷ x ∈ carrier" for x
    using R.not_outside not_outside R.refl[of x] refl[of x]
    by blast
  hence eq: "⋃(set As) = carrier" by blast
  from assms eq have "As = weak_ranking_aux (⋃(set As))"
    by (intro weak_ranking_aux_unique') simp_all
  with eq show ?thesis by simp
qed

lemma weak_ranking_total_preorder:
  "is_weak_ranking (weak_ranking le)" "of_weak_ranking (weak_ranking le) = le"
proof -
  from weak_ranking_aux_wf[of carrier] of_weak_ranking_weak_ranking_aux
    have "∃x. is_weak_ranking x ∧ le = of_weak_ranking x" by auto
  hence "is_weak_ranking (weak_ranking le) ∧ le = of_weak_ranking (weak_ranking le)"
    unfolding weak_ranking_def by (rule someI_ex)
  thus "is_weak_ranking (weak_ranking le)" "of_weak_ranking (weak_ranking le) = le"
    by simp_all
qed

lemma weak_ranking_altdef:
  "weak_ranking le = weak_ranking_aux carrier"
  by (intro weak_ranking_aux_unique weak_ranking_total_preorder)

lemma weak_ranking_Union: "⋃(set (weak_ranking le)) = carrier"
  by (simp add: weak_ranking_altdef weak_ranking_aux_Union)

lemma weak_ranking_unique:
  assumes "is_weak_ranking As" "of_weak_ranking As = le"
  shows   "As = weak_ranking le"
  using assms unfolding weak_ranking_altdef by (rule weak_ranking_aux_unique)

lemma weak_ranking_permute:
  assumes "f permutes carrier"
  shows   "weak_ranking (map_relation (inv f) le) = map ((`) f) (weak_ranking le)"
proof -
  from assms have "inv f -` carrier = carrier"
    by (simp add: permutes_vimage permutes_inv)
  then interpret R: finite_total_preorder_on "inv f -` carrier" "map_relation (inv f) le"
    by (intro finite_total_preorder_on_map) (simp_all add: finite_carrier)
  from assms have "is_weak_ranking (map ((`) f) (weak_ranking le))"
    by (intro is_weak_ranking_map_inj) 
       (simp_all add: weak_ranking_total_preorder permutes_inj_on)
  with assms show ?thesis
    by (intro sym[OF R.weak_ranking_unique])
       (simp_all add: of_weak_ranking_permute weak_ranking_Union weak_ranking_total_preorder)
qed

lemma weak_ranking_index_unique:
  assumes "is_weak_ranking xs" "i < length xs" "j < length xs" "x ∈ xs ! i" "x ∈ xs ! j"
  shows   "i = j"
  using assms unfolding is_weak_ranking_def by auto

lemma weak_ranking_index_unique':
  assumes "is_weak_ranking xs" "i < length xs" "x ∈ xs ! i"
  shows   "i = find_index ((∈) x) xs"
  using assms find_index_less_size_conv nth_mem
  by (intro weak_ranking_index_unique[OF assms(1,2) _ assms(3)]
        nth_find_index[of "(∈) x"]) blast+

lemma weak_ranking_eqclass1:
  assumes "A ∈ set (weak_ranking le)" "x ∈ A" "y ∈ A"
  shows   "le x y"
proof -
  from assms obtain i where "weak_ranking le ! i = A" "i < length (weak_ranking le)" 
    by (auto simp: set_conv_nth)
  with assms have "of_weak_ranking (weak_ranking le) x y"
    by (intro of_weak_ranking.intros[of i i]) auto
  thus ?thesis by (simp add: weak_ranking_total_preorder)
qed

lemma weak_ranking_eqclass2:
  assumes A: "A ∈ set (weak_ranking le)" "x ∈ A" and le: "le x y" "le y x"
  shows   "y ∈ A"
proof -
  define xs where "xs = weak_ranking le"
  have wf: "is_weak_ranking xs" by (simp add: xs_def weak_ranking_total_preorder)
  let ?le' = "of_weak_ranking xs"
  from le have le': "?le' x y" "?le' y x" by (simp_all add: weak_ranking_total_preorder xs_def)
  from le'(1) obtain i j
    where ij: "j ≤ i" "i < length xs" "j < length xs" "x ∈ xs ! i" "y ∈ xs ! j"
    by (cases rule: of_weak_ranking.cases)
  from le'(2) obtain i' j'
    where i'j': "j' ≤ i'" "i' < length xs" "j' < length xs" "x ∈ xs ! j'" "y ∈ xs ! i'"
    by (cases rule: of_weak_ranking.cases)
  from ij i'j' have eq: "i = j'" "j = i'"
    by (intro weak_ranking_index_unique[OF wf]; simp)+
  moreover from A obtain k where k: "k < length xs" "A = xs ! k" 
    by (auto simp: xs_def set_conv_nth)
  ultimately have "k = i" using ij i'j' A
    by (intro weak_ranking_index_unique[OF wf, of _ _ x]) auto
  with ij i'j' k eq show ?thesis by (auto simp: xs_def)
qed

lemma hd_weak_ranking:
  assumes "x ∈ hd (weak_ranking le)" "y ∈ carrier"
  shows   "le y x"
proof -
  from weak_ranking_Union assms obtain i
    where "i < length (weak_ranking le)" "y ∈ weak_ranking le ! i"
    by (auto simp: set_conv_nth)
  moreover from assms(2) weak_ranking_Union have "weak_ranking le ≠ []" by auto
  ultimately have "of_weak_ranking (weak_ranking le) y x" using assms(1)
    by (intro of_weak_ranking.intros[of 0 i]) (auto simp: hd_conv_nth)
  thus ?thesis by (simp add: weak_ranking_total_preorder)
qed

lemma last_weak_ranking:
  assumes "x ∈ last (weak_ranking le)" "y ∈ carrier"
  shows   "le x y"
proof -
  from weak_ranking_Union assms obtain i
    where "i < length (weak_ranking le)" "y ∈ weak_ranking le ! i"
    by (auto simp: set_conv_nth)
  moreover from assms(2) weak_ranking_Union have "weak_ranking le ≠ []" by auto
  ultimately have "of_weak_ranking (weak_ranking le) x y" using assms(1)
    by (intro of_weak_ranking.intros[of i "length (weak_ranking le) - 1"])
       (auto simp: last_conv_nth)
  thus ?thesis by (simp add: weak_ranking_total_preorder)
qed

text ‹
  The index in weak ranking of a given alternative. An element with index 0 is 
  first-ranked; larger indices correspond to less-preferred alternatives.
›
definition weak_ranking_index :: "'a ⇒ nat" where
  "weak_ranking_index x = find_index (λA. x ∈ A) (weak_ranking le)"

lemma nth_weak_ranking_index:
  assumes "x ∈ carrier"
  shows   "weak_ranking_index x < length (weak_ranking le)" 
          "x ∈ weak_ranking le ! weak_ranking_index x"
proof -
  from assms weak_ranking_Union show "weak_ranking_index x < length (weak_ranking le)"
     unfolding weak_ranking_index_def by (auto simp add: find_index_less_size_conv)
  thus "x ∈ weak_ranking le ! weak_ranking_index x" unfolding weak_ranking_index_def
    by (rule nth_find_index)
qed

lemma ranking_index_eqI:
  "i < length (weak_ranking le) ⟹ x ∈ weak_ranking le ! i ⟹ weak_ranking_index x = i"
  using weak_ranking_index_unique'[of "weak_ranking le" i x]
  by (simp add: weak_ranking_index_def weak_ranking_total_preorder)

lemma ranking_index_le_iff [simp]:
  assumes "x ∈ carrier" "y ∈ carrier"
  shows   "weak_ranking_index x ≥ weak_ranking_index y ⟷ le x y"
proof -
  have "le x y ⟷ of_weak_ranking (weak_ranking le) x y"
    by (simp add: weak_ranking_total_preorder)
  also have "… ⟷ weak_ranking_index x ≥ weak_ranking_index y"
  proof
    assume "weak_ranking_index x ≥ weak_ranking_index y"
    thus "of_weak_ranking (weak_ranking le) x y"
      by (rule of_weak_ranking.intros) (simp_all add: nth_weak_ranking_index assms)
  next
    assume "of_weak_ranking (weak_ranking le) x y"
    then obtain i j where 
      "i ≤ j" "i < length (weak_ranking le)" "j < length (weak_ranking le)"
      "x ∈ weak_ranking le ! j" "y ∈ weak_ranking le ! i"
      by (elim of_weak_ranking.cases) blast
    with ranking_index_eqI[of i] ranking_index_eqI[of j]
      show "weak_ranking_index x ≥ weak_ranking_index y" by simp
  qed
  finally show ?thesis ..
qed

end

lemma weak_ranking_False [simp]: "weak_ranking (λ_ _. False) = []"
proof -
  interpret finite_total_preorder_on "{}" "λ_ _. False"
    by unfold_locales simp_all
  have "[] = weak_ranking (λ_ _. False)" by (rule weak_ranking_unique) simp_all
  thus ?thesis ..
qed

lemmas of_weak_ranking_weak_ranking = 
  finite_total_preorder_on.weak_ranking_total_preorder(2)

lemma finite_total_preorder_on_iff:
  "finite_total_preorder_on A R ⟷ total_preorder_on A R ∧ finite A"
  by (simp add: finite_total_preorder_on_def finite_total_preorder_on_axioms_def)

lemma finite_total_preorder_of_weak_ranking:
  assumes "⋃(set xs) = A" "is_finite_weak_ranking xs"
  shows   "finite_total_preorder_on A (of_weak_ranking xs)"
proof -
  from assms(2) have "is_weak_ranking xs" by (simp add: is_finite_weak_ranking_def)
  from assms(1) and this interpret total_preorder_on A "of_weak_ranking xs"
    by (rule total_preorder_of_weak_ranking)
  from assms(2) show ?thesis
    by unfold_locales (simp add: assms(1)[symmetric] is_finite_weak_ranking_def)
qed  

lemma weak_ranking_of_weak_ranking:
  assumes "is_finite_weak_ranking xs"
  shows   "weak_ranking (of_weak_ranking xs) = xs"
proof -
  from assms interpret finite_total_preorder_on "⋃(set xs)" "of_weak_ranking xs"
    by (intro finite_total_preorder_of_weak_ranking) simp_all
  from assms show ?thesis
    by (intro sym[OF weak_ranking_unique]) (simp_all add: is_finite_weak_ranking_def)
qed


lemma weak_ranking_eqD:
  assumes "finite_total_preorder_on alts R1"
  assumes "finite_total_preorder_on alts R2"
  assumes "weak_ranking R1 = weak_ranking R2"
  shows   "R1 = R2"
proof -
  from assms have "of_weak_ranking (weak_ranking R1) = of_weak_ranking (weak_ranking R2)" by simp
  with assms(1,2) show ?thesis by (simp add: of_weak_ranking_weak_ranking)
qed

lemma weak_ranking_eq_iff:
  assumes "finite_total_preorder_on alts R1"
  assumes "finite_total_preorder_on alts R2"
  shows   "weak_ranking R1 = weak_ranking R2 ⟷ R1 = R2"
  using assms weak_ranking_eqD by auto


definition preferred_alts :: "'alt relation ⇒ 'alt ⇒ 'alt set" where
  "preferred_alts R x = {y. y ≽[R] x}"

lemma (in preorder_on) preferred_alts_refl [simp]: "x ∈ carrier ⟹ x ∈ preferred_alts le x"
  by (simp add: preferred_alts_def refl)  

lemma (in preorder_on) preferred_alts_altdef:
  "preferred_alts le x = {y∈carrier. y ≽[le] x}"
  by (auto simp: preferred_alts_def intro: not_outside)
  
lemma (in preorder_on) preferred_alts_subset: "preferred_alts le x ⊆ carrier"
  unfolding preferred_alts_def using not_outside by blast


subsection ‹Rankings›

(* TODO: Extend theory on rankings. Can probably mostly be based on
   existing theory on weak rankings. *)

definition ranking :: "'a relation ⇒ 'a list" where
  "ranking R = map the_elem (weak_ranking R)"

locale finite_linorder_on = linorder_on +
  assumes finite_carrier [intro]: "finite carrier"
begin

sublocale finite_total_preorder_on carrier le
  by unfold_locales (fact finite_carrier)

lemma singleton_weak_ranking:
  assumes "A ∈ set (weak_ranking le)"
  shows   "is_singleton A"
proof (rule is_singletonI')
  from assms show "A ≠ {}"
    using weak_ranking_total_preorder(1) is_weak_ranking_iff by auto
next
  fix x y assume "x ∈ A" "y ∈ A"
  with assms 
    have "x ≼[of_weak_ranking (weak_ranking le)] y" "y ≼[of_weak_ranking (weak_ranking le)] x"
    by (auto intro!: of_weak_ranking_indifference)
  with weak_ranking_total_preorder(2) 
    show "x = y" by (intro antisymmetric) simp_all
qed

lemma weak_ranking_ranking: "weak_ranking le = map (λx. {x}) (ranking le)"
  unfolding ranking_def map_map o_def
proof (rule sym, rule map_idI)
  fix A assume "A ∈ set (weak_ranking le)"
  hence "is_singleton A" by (rule singleton_weak_ranking)
  thus "{the_elem A} = A" by (auto elim: is_singletonE)
qed

end

end