Theory Order_Predicates
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
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›
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