# Theory Linorder_Relations

theory Linorder_Relations
imports Multiset_Permutations List_Index
```(*
File:    Linorder_Relations.thy
Author:  Manuel Eberl

Linear orderings represented as relations (i.e. set of pairs). Also contains
material connecting such orderings to lists, and insertion sort w.r.t. a
given ordering relation.
*)
section ‹Linear orderings as relations›
theory Linorder_Relations
imports
Complex_Main
"HOL-Library.Multiset_Permutations"
"List-Index.List_Index"
begin

subsection ‹Auxiliary facts›

(* TODO: Move *)
lemma distinct_count_atmost_1':
"distinct xs = (∀a. count (mset xs) a ≤ 1)"
proof -
{
fix x have "count (mset xs) x = (if x ∈ set xs then 1 else 0) ⟷ count (mset xs) x ≤ 1"
using count_eq_zero_iff[of "mset xs" x]
by (cases "count (mset xs) x") (auto simp del: count_mset_0_iff)
}
thus ?thesis unfolding distinct_count_atmost_1 by blast
qed

lemma distinct_mset_mono:
assumes "distinct ys" "mset xs ⊆# mset ys"
shows   "distinct xs"
unfolding distinct_count_atmost_1'
proof
fix x
from assms(2) have "count (mset xs) x ≤ count (mset ys) x"
by (rule mset_subset_eq_count)
also from assms(1) have "… ≤ 1" unfolding distinct_count_atmost_1' ..
finally show "count (mset xs) x ≤ 1" .
qed

lemma mset_eq_imp_distinct_iff:
assumes "mset xs = mset ys"
shows   "distinct xs ⟷ distinct ys"
using assms by (simp add: distinct_count_atmost_1')

lemma total_on_subset: "total_on B R ⟹ A ⊆ B ⟹ total_on A R"
by (auto simp: total_on_def)

subsection ‹Sortedness w.r.t. a relation›

inductive sorted_wrt :: "('a × 'a) set ⇒ 'a list ⇒ bool" for R where
"sorted_wrt R []"
| "sorted_wrt R xs ⟹ (⋀y. y ∈ set xs ⟹ (x,y) ∈ R) ⟹ sorted_wrt R (x # xs)"

lemma sorted_wrt_Nil [simp]: "sorted_wrt R []"
by (rule sorted_wrt.intros)

lemma sorted_wrt_Cons: "sorted_wrt R (x # xs) ⟷ (∀y∈set xs. (x,y) ∈ R) ∧ sorted_wrt R xs"
by (auto intro: sorted_wrt.intros elim: sorted_wrt.cases)

lemma sorted_wrt_singleton [simp]: "sorted_wrt R [x]"
by (intro sorted_wrt.intros) simp_all

lemma sorted_wrt_many:
assumes "trans R"
shows   "sorted_wrt R (x # y # xs) ⟷ (x,y) ∈ R ∧ sorted_wrt R (y # xs)"
by (force intro: sorted_wrt.intros transD[OF assms] elim: sorted_wrt.cases)

lemma sorted_wrt_imp_le_last:
assumes "sorted_wrt R xs" "xs ≠ []" "x ∈ set xs" "x ≠ last xs"
shows   "(x, last xs) ∈ R"
using assms by induction auto

lemma sorted_wrt_append:
assumes "sorted_wrt R xs" "sorted_wrt R ys"
"⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹ (x,y) ∈ R" "trans R"
shows   "sorted_wrt R (xs @ ys)"
using assms by (induction xs) (auto simp: sorted_wrt_Cons)

lemma sorted_wrt_snoc:
assumes "sorted_wrt R xs" "(last xs, y) ∈ R" "trans R"
shows   "sorted_wrt R (xs @ [y])"
using assms(1,2)
proof induction
case (2 xs x)
show ?case
proof (cases "xs = []")
case False
with 2 have "(z,y) ∈ R" if "z ∈ set xs" for z
using that by (cases "z = last xs")
(auto intro: assms transD[OF assms(3), OF sorted_wrt_imp_le_last[OF 2(1)]])
from False have *: "last xs ∈ set xs" by simp
moreover from 2 False have "(x,y) ∈ R" by (intro transD[OF assms(3) 2(2)[OF *]]) simp
ultimately show ?thesis using 2 False
by (auto intro!: sorted_wrt.intros)
qed (insert 2, auto intro: sorted_wrt.intros)
qed simp_all

lemma sorted_wrt_conv_nth:
"sorted_wrt R xs ⟷ (∀i j. i < j ∧ j < length xs ⟶ (xs!i, xs!j) ∈ R)"
by (induction xs) (auto simp: sorted_wrt_Cons nth_Cons set_conv_nth split: nat.splits)

subsection ‹Linear orderings›

definition linorder_on :: "'a set ⇒ ('a × 'a) set ⇒ bool"  where
"linorder_on A R ⟷ refl_on A R ∧ antisym R ∧ trans R ∧ total_on A R"

lemma linorder_on_cases:
assumes "linorder_on A R" "x ∈ A" "y ∈ A"
shows   "x = y ∨ ((x, y) ∈ R ∧ (y, x) ∉ R) ∨ ((y, x) ∈ R ∧ (x, y) ∉ R)"
using assms by (auto simp: linorder_on_def refl_on_def total_on_def antisym_def)

lemma sorted_wrt_linorder_imp_index_le:
assumes "linorder_on A R" "set xs ⊆ A" "sorted_wrt R xs"
"x ∈ set xs" "y ∈ set xs" "(x,y) ∈ R"
shows   "index xs x ≤ index xs y"
proof -
define i j where "i = index xs x" and "j = index xs y"
{
assume "j < i"
moreover from assms have "i < length xs" by (simp add: i_def)
ultimately have "(xs!j,xs!i) ∈ R" using assms by (auto simp: sorted_wrt_conv_nth)
with assms have "x = y" by (auto simp: linorder_on_def antisym_def i_def j_def)
}
hence "i ≤ j ∨ x = y" by linarith
thus ?thesis by (auto simp: i_def j_def)
qed

lemma sorted_wrt_linorder_index_le_imp:
assumes "linorder_on A R" "set xs ⊆ A" "sorted_wrt R xs"
"x ∈ set xs" "y ∈ set xs" "index xs x ≤ index xs y"
shows   "(x,y) ∈ R"
proof (cases "x = y")
case False
define i j where "i = index xs x" and "j = index xs y"
from False and assms have "i ≠ j" by (simp add: i_def j_def)
with ‹index xs x ≤ index xs y› have "i < j" by (simp add: i_def j_def)
moreover from assms have "j < length xs" by (simp add: j_def)
ultimately have "(xs ! i, xs ! j) ∈ R" using assms(3)
by (auto simp: sorted_wrt_conv_nth)
with assms show ?thesis by (simp_all add: i_def j_def)
qed (insert assms, auto simp: linorder_on_def refl_on_def)

lemma sorted_wrt_linorder_index_le_iff:
assumes "linorder_on A R" "set xs ⊆ A" "sorted_wrt R xs"
"x ∈ set xs" "y ∈ set xs"
shows   "index xs x ≤ index xs y ⟷ (x,y) ∈ R"
using sorted_wrt_linorder_index_le_imp[OF assms] sorted_wrt_linorder_imp_index_le[OF assms]
by blast

lemma sorted_wrt_linorder_index_less_iff:
assumes "linorder_on A R" "set xs ⊆ A" "sorted_wrt R xs"
"x ∈ set xs" "y ∈ set xs"
shows   "index xs x < index xs y ⟷ (y,x) ∉ R"
by (subst sorted_wrt_linorder_index_le_iff[OF assms(1-3) assms(5,4), symmetric]) auto

lemma sorted_wrt_distinct_linorder_nth:
assumes "linorder_on A R" "set xs ⊆ A" "sorted_wrt R xs" "distinct xs"
"i < length xs" "j < length xs"
shows   "(xs!i, xs!j) ∈ R ⟷ i ≤ j"
proof (cases i j rule: linorder_cases)
case less
with assms show ?thesis by (simp add: sorted_wrt_conv_nth)
next
case equal
from assms have "xs ! i ∈ set xs" "xs ! j ∈ set xs" by (auto simp: set_conv_nth)
with assms(2) have "xs ! i ∈ A" "xs ! j ∈ A" by blast+
with ‹linorder_on A R› and equal show ?thesis by (simp add: linorder_on_def refl_on_def)
next
case greater
with assms have "(xs!j, xs!i) ∈ R" by (auto simp add: sorted_wrt_conv_nth)
moreover from assms and greater have "xs ! i ≠ xs ! j" by (simp add: nth_eq_iff_index_eq)
ultimately show ?thesis using ‹linorder_on A R› greater
by (auto simp: linorder_on_def antisym_def)
qed

subsection ‹Converting a list into a linear ordering›

definition linorder_of_list :: "'a list ⇒ ('a × 'a) set" where
"linorder_of_list xs = {(a,b). a ∈ set xs ∧ b ∈ set xs ∧ index xs a ≤ index xs b}"

lemma linorder_linorder_of_list [intro, simp]:
assumes "distinct xs"
shows   "linorder_on (set xs) (linorder_of_list xs)"
unfolding linorder_on_def using assms
by (auto simp: refl_on_def antisym_def trans_def total_on_def linorder_of_list_def)

lemma sorted_wrt_linorder_of_list [intro, simp]:
"distinct xs ⟹ sorted_wrt (linorder_of_list xs) xs"
by (auto simp: sorted_wrt_conv_nth linorder_of_list_def index_nth_id)

subsection ‹Insertion sort›

primrec insert_wrt :: "('a × 'a) set ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"insert_wrt R x [] = [x]"
| "insert_wrt R x (y # ys) = (if (x, y) ∈ R then x # y # ys else y # insert_wrt R x ys)"

lemma set_insert_wrt [simp]: "set (insert_wrt R x xs) = insert x (set xs)"
by (induction xs) auto

lemma mset_insert_wrt [simp]: "mset (insert_wrt R x xs) = add_mset x (mset xs)"
by (induction xs) auto

lemma length_insert_wrt [simp]: "length (insert_wrt R x xs) = Suc (length xs)"
by (induction xs) simp_all

definition insort_wrt :: "('a × 'a) set ⇒ 'a list ⇒ 'a list" where
"insort_wrt R xs = foldr (insert_wrt R) xs []"

lemma set_insort_wrt [simp]: "set (insort_wrt R xs) = set xs"
by (induction xs) (simp_all add: insort_wrt_def)

lemma mset_insort_wrt [simp]: "mset (insort_wrt R xs) = mset xs"
by (induction xs) (simp_all add: insort_wrt_def)

lemma length_insort_wrt [simp]: "length (insort_wrt R xs) = length xs"
by (induction xs) (simp_all add: insort_wrt_def)

lemma sorted_wrt_insert_wrt [intro]:
"linorder_on A R ⟹ set (x # xs) ⊆ A ⟹
sorted_wrt R xs ⟹ sorted_wrt R (insert_wrt R x xs)"
proof (induction xs)
case (Cons y ys)
from Cons.prems have "(x,y) ∈ R ∨ (y,x) ∈ R"
by (cases "x = y") (auto simp: linorder_on_def refl_on_def total_on_def)
with Cons show ?case
by (auto simp: sorted_wrt_Cons intro: transD simp: linorder_on_def)
qed auto

lemma sorted_wrt_insort [intro]:
assumes "linorder_on A R" "set xs ⊆ A"
shows   "sorted_wrt R (insort_wrt R xs)"
proof -
from assms have "set (insort_wrt R xs) = set xs ∧ sorted_wrt R (insort_wrt R xs)"
by (induction xs) (auto simp: insort_wrt_def intro!: sorted_wrt_insert_wrt)
thus ?thesis ..
qed

lemma distinct_insort_wrt [simp]: "distinct (insort_wrt R xs) ⟷ distinct xs"

lemma sorted_wrt_linorder_unique:
assumes "linorder_on A R" "mset xs = mset ys" "sorted_wrt R xs" "sorted_wrt R ys"
shows   "xs = ys"
proof -
from ‹mset xs = mset ys› have "length xs = length ys" by (rule mset_eq_length)
from this and assms(2-) show ?thesis
proof (induction xs ys rule: list_induct2)
case (Cons x xs y ys)
have "set (x # xs) = set_mset (mset (x # xs))" by simp
also have "mset (x # xs) = mset (y # ys)" by fact
also have "set_mset … = set (y # ys)" by simp
finally have eq: "set (x # xs) = set (y # ys)" .

have "x = y"
proof (rule ccontr)
assume "x ≠ y"
with eq have "x ∈ set ys" "y ∈ set xs" by auto
with Cons.prems and assms(1) and eq have "(x, y) ∈ R" "(y, x) ∈ R"
by (auto simp: sorted_wrt_Cons)
with assms(1) have "x = y" by (auto simp: linorder_on_def antisym_def)
with ‹x ≠ y› show False by contradiction
qed
with Cons show ?case by (auto simp: sorted_wrt_Cons)
qed auto
qed

subsection ‹Obtaining a sorted list of a given set›

definition sorted_wrt_list_of_set where
"sorted_wrt_list_of_set R A =
(if finite A then (THE xs. set xs = A ∧ distinct xs ∧ sorted_wrt R xs) else [])"

lemma mset_remdups: "mset (remdups xs) = mset_set (set xs)"
proof (induction xs)
case (Cons x xs)
thus ?case by (cases "x ∈ set xs") (auto simp: insert_absorb)
qed auto

lemma sorted_wrt_list_set:
assumes "linorder_on A R" "set xs ⊆ A"
shows   "sorted_wrt_list_of_set R (set xs) = insort_wrt R (remdups xs)"
proof -
have "sorted_wrt_list_of_set R (set xs) =
(THE xsa. set xsa = set xs ∧ distinct xsa ∧ sorted_wrt R xsa)"
also have "… = insort_wrt R (remdups xs)"
proof (rule the_equality)
fix xsa assume xsa: "set xsa = set xs ∧ distinct xsa ∧ sorted_wrt R xsa"
from xsa have "mset xsa = mset_set (set xsa)" by (subst mset_set_set) simp_all
also from xsa have "set xsa = set xs" by simp
also have "mset_set … = mset (remdups xs)" by (simp add: mset_remdups)
finally show "xsa = insort_wrt R (remdups xs)" using xsa assms
by (intro sorted_wrt_linorder_unique[OF assms(1)])
(auto intro!: sorted_wrt_insort)
qed (insert assms, auto intro!: sorted_wrt_insort)
finally show ?thesis .
qed

lemma linorder_sorted_wrt_exists:
assumes "linorder_on A R" "finite B" "B ⊆ A"
shows   "∃xs. set xs = B ∧ distinct xs ∧ sorted_wrt R xs"
proof -
from ‹finite B› obtain xs where "set xs = B" "distinct xs"
using finite_distinct_list by blast
hence "set (insort_wrt R xs) = B" "distinct (insort_wrt R xs)" by simp_all
moreover have "sorted_wrt R (insort_wrt R xs)"
using assms ‹set xs = B› by (intro sorted_wrt_insort[OF assms(1)]) auto
ultimately show ?thesis by blast
qed

lemma linorder_sorted_wrt_list_of_set:
assumes "linorder_on A R" "finite B" "B ⊆ A"
shows   "set (sorted_wrt_list_of_set R B) = B" "distinct (sorted_wrt_list_of_set R B)"
"sorted_wrt R (sorted_wrt_list_of_set R B)"
proof -
have "∃!xs. set xs = B ∧ distinct xs ∧ sorted_wrt R xs"
proof (rule ex_ex1I)
show "∃xs. set xs = B ∧ distinct xs ∧ sorted_wrt R xs"
by (rule linorder_sorted_wrt_exists assms)+
next
fix xs ys assume "set xs = B ∧ distinct xs ∧ sorted_wrt R xs"
"set ys = B ∧ distinct ys ∧ sorted_wrt R ys"
thus "xs = ys"
by (intro sorted_wrt_linorder_unique[OF assms(1)]) (auto simp: set_eq_iff_mset_eq_distinct)
qed
from theI'[OF this] show  "set (sorted_wrt_list_of_set R B) = B"
"distinct (sorted_wrt_list_of_set R B)" "sorted_wrt R (sorted_wrt_list_of_set R B)"
by (simp_all add: sorted_wrt_list_of_set_def ‹finite B›)
qed

lemma sorted_wrt_list_of_set_eqI:
assumes "linorder_on B R" "A ⊆ B" "set xs = A" "distinct xs" "sorted_wrt R xs"
shows   "sorted_wrt_list_of_set R A = xs"
proof (rule sorted_wrt_linorder_unique)
show "linorder_on B R" by fact
let ?ys = "sorted_wrt_list_of_set R A"
have fin [simp]: "finite A" by (simp_all add: assms(3) [symmetric])
have *: "distinct ?ys" "set ?ys = A" "sorted_wrt R ?ys"
by (rule linorder_sorted_wrt_list_of_set[OF assms(1)] fin assms)+
from assms * show "mset ?ys = mset xs"
by (subst set_eq_iff_mset_eq_distinct [symmetric]) simp_all
show "sorted_wrt R ?ys" by fact
qed fact+

subsection ‹Rank of an element in an ordering›

text ‹
The `rank' of an element in a set w.r.t. an ordering is how many smaller elements exist.
This is particularly useful in linear orders, where there exists a unique \$n\$-th element
for every \$n\$.
›
definition linorder_rank where
"linorder_rank R A x = card {y∈A-{x}. (y,x) ∈ R}"

lemma linorder_rank_le:
assumes "finite A"
shows   "linorder_rank R A x ≤ card A"
unfolding linorder_rank_def using assms
by (rule card_mono) auto

lemma linorder_rank_less:
assumes "finite A" "x ∈ A"
shows   "linorder_rank R A x < card A"
proof -
have "linorder_rank R A x ≤ card (A - {x})"
unfolding linorder_rank_def using assms by (intro card_mono) auto
also from assms have "… < card A" by (intro psubset_card_mono) auto
finally show ?thesis .
qed

lemma linorder_rank_union:
assumes "finite A" "finite B" "A ∩ B = {}"
shows   "linorder_rank R (A ∪ B) x = linorder_rank R A x + linorder_rank R B x"
proof -
have "linorder_rank R (A ∪ B) x = card {y∈(A∪B)-{x}. (y,x) ∈ R}"
also have "{y∈(A∪B)-{x}. (y,x) ∈ R} = {y∈A-{x}. (y,x) ∈ R} ∪ {y∈B-{x}. (y,x) ∈ R}" by blast
also have "card … = linorder_rank R A x + linorder_rank R B x" unfolding linorder_rank_def
using assms by (intro card_Un_disjoint) auto
finally show ?thesis .
qed

lemma linorder_rank_empty [simp]: "linorder_rank R {} x = 0"

lemma linorder_rank_singleton:
"linorder_rank R {y} x = (if x ≠ y ∧ (y,x) ∈ R then 1 else 0)"
proof -
have "linorder_rank R {y} x = card {z∈{y}-{x}. (z,x) ∈ R}" by (simp add: linorder_rank_def)
also have "{z∈{y}-{x}. (z,x) ∈ R} = (if x ≠ y ∧ (y,x) ∈ R then {y} else {})" by auto
also have "card … = (if x ≠ y ∧ (y,x) ∈ R then 1 else 0)" by simp
finally show ?thesis .
qed

lemma linorder_rank_insert:
assumes "finite A" "y ∉ A"
shows   "linorder_rank R (insert y A) x =
(if x ≠ y ∧ (y,x) ∈ R then 1 else 0) + linorder_rank R A x"
using linorder_rank_union[of "{y}" A R x] assms by (auto simp: linorder_rank_singleton)

lemma linorder_rank_mono:
assumes "linorder_on B R" "finite A" "A ⊆ B" "(x, y) ∈ R"
shows   "linorder_rank R A x ≤ linorder_rank R A y"
unfolding linorder_rank_def
proof (rule card_mono)
from assms have trans: "trans R" and antisym: "antisym R" by (simp_all add: linorder_on_def)
from assms antisym show "{y ∈ A - {x}. (y, x) ∈ R} ⊆ {ya ∈ A - {y}. (ya, y) ∈ R}"
by (auto intro: transD[OF trans] simp: antisym_def)
qed (insert assms, simp_all)

lemma linorder_rank_strict_mono:
assumes "linorder_on B R" "finite A" "A ⊆ B" "y ∈ A" "(y, x) ∈ R" "x ≠ y"
shows   "linorder_rank R A y < linorder_rank R A x"
proof -
from assms(1) have trans: "trans R" by (simp add: linorder_on_def)
from assms have *: "(x, y) ∉ R" by (auto simp: linorder_on_def antisym_def)
from this and ‹(y,x) ∈ R› have "{z∈A-{y}. (z, y) ∈ R} ⊆ {z∈A-{x}. (z,x) ∈ R}"
by (auto intro: transD[OF trans])
moreover from * and assms have "y ∉ {z∈A-{y}. (z, y) ∈ R}" "y ∈ {z∈A-{x}. (z, x) ∈ R}"
by auto
ultimately have "{z∈A-{y}. (z, y) ∈ R} ⊂ {z∈A-{x}. (z,x) ∈ R}" by blast
thus ?thesis using assms unfolding linorder_rank_def by (intro psubset_card_mono) auto
qed

lemma linorder_rank_le_iff:
assumes "linorder_on B R" "finite A" "A ⊆ B" "x ∈ A" "y ∈ A"
shows   "linorder_rank R A x ≤ linorder_rank R A y ⟷ (x, y) ∈ R"
proof (cases "x = y")
case True
with assms show ?thesis by (auto simp: linorder_on_def refl_on_def)
next
case False
from assms(1) have trans: "trans R" by (simp_all add: linorder_on_def)
from assms have "x ∈ B" "y ∈ B" by auto
with ‹linorder_on B R› and False have "((x,y) ∈ R ∧ (y,x) ∉ R) ∨ ((y,x) ∈ R ∧ (x,y) ∉ R)"
by (fastforce simp: linorder_on_def antisym_def total_on_def)
thus ?thesis
proof
assume "(x,y) ∈ R ∧ (y,x) ∉ R"
with assms show ?thesis by (auto intro!: linorder_rank_mono)
next
assume *: "(y,x) ∈ R ∧ (x,y) ∉ R"
with linorder_rank_strict_mono[OF assms(1-3), of y x] assms False
show ?thesis by auto
qed
qed

lemma linorder_rank_eq_iff:
assumes "linorder_on B R" "finite A" "A ⊆ B" "x ∈ A" "y ∈ A"
shows   "linorder_rank R A x = linorder_rank R A y ⟷ x = y"
proof
assume "linorder_rank R A x = linorder_rank R A y"
with linorder_rank_le_iff[OF assms(1-5)] linorder_rank_le_iff[OF assms(1-3) assms(5,4)]
have "(x, y) ∈ R" "(y, x) ∈ R" by simp_all
with assms show "x = y" by (auto simp: linorder_on_def antisym_def)
qed simp_all

lemma linorder_rank_set_sorted_wrt:
assumes "linorder_on B R" "set xs ⊆ B" "sorted_wrt R xs" "x ∈ set xs" "distinct xs"
shows   "linorder_rank R (set xs) x = index xs x"
proof -
define j where "j = index xs x"
from assms have j: "j < length xs" by (simp add: j_def)
have *: "x = y ∨ ((x, y) ∈ R ∧ (y, x) ∉ R) ∨ ((y, x) ∈ R ∧ (x, y) ∉ R)" if "y ∈ set xs" for y
using linorder_on_cases[OF assms(1), of x y] assms that by auto
from assms have "{y∈set xs-{x}. (y, x) ∈ R} = {y∈set xs-{x}. index xs y < index xs x}"
by (auto simp: sorted_wrt_linorder_index_less_iff[OF assms(1-3)] dest: *)
also have "… = {y∈set xs. index xs y < j}" by (auto simp: j_def)
also have "… = (λi. xs ! i) ` {i. i < j}"
proof safe
fix y assume "y ∈ set xs" "index xs y < j"
moreover from this and j have "y = xs ! index xs y" by simp
ultimately show "y ∈ (!) xs ` {i. i < j}" by blast
qed (insert assms j, auto simp: index_nth_id)
also from assms and j have "card … = card {i. i < j}"
by (intro card_image) (auto simp: inj_on_def nth_eq_iff_index_eq)
also have "… = j" by simp
finally show ?thesis by (simp only: j_def linorder_rank_def)
qed

lemma bij_betw_linorder_rank:
assumes "linorder_on B R" "finite A" "A ⊆ B"
shows   "bij_betw (linorder_rank R A) A {..<card A}"
proof -
define xs where "xs = sorted_wrt_list_of_set R A"
note xs = linorder_sorted_wrt_list_of_set[OF assms, folded xs_def]
from ‹distinct xs› have len_xs: "length xs = card A"
by (subst ‹set xs = A› [symmetric]) (auto simp: distinct_card)
have rank: "linorder_rank R (set xs) x = index xs x" if "x ∈ A" for x
using linorder_rank_set_sorted_wrt[OF assms(1), of xs x] assms that xs by simp_all
from xs len_xs show ?thesis
by (intro bij_betw_byWitness[where f' = "λi. xs ! i"])
(auto simp: rank index_nth_id intro!: nth_mem)
qed

subsection ‹The bijection between linear orderings and lists›

theorem bij_betw_linorder_of_list:
assumes "finite A"
shows   "bij_betw linorder_of_list (permutations_of_set A) {R. linorder_on A R}"
proof (intro bij_betw_byWitness[where f' = "λR. sorted_wrt_list_of_set R A"] ballI subsetI,
goal_cases)
case (1 xs)
thus ?case by (intro sorted_wrt_list_of_set_eqI) (auto simp: permutations_of_set_def)
next
case (2 R)
hence R: "linorder_on A R" by simp
from R have in_R: "x ∈ A" "y ∈ A" if "(x,y) ∈ R" for x y using that
by (auto simp: linorder_on_def refl_on_def)
let ?xs = "sorted_wrt_list_of_set R A"
have xs: "distinct ?xs" "set ?xs = A" "sorted_wrt R ?xs"
by (rule linorder_sorted_wrt_list_of_set[OF R] assms order.refl)+
thus ?case using sorted_wrt_linorder_index_le_iff[OF R, of ?xs]
by (auto simp: linorder_of_list_def dest: in_R)
next
case (4 xs)
then obtain R where R: "linorder_on A R" and xs [simp]: "xs = sorted_wrt_list_of_set R A" by auto
let ?xs = "sorted_wrt_list_of_set R A"
have xs: "distinct ?xs" "set ?xs = A" "sorted_wrt R ?xs"
by (rule linorder_sorted_wrt_list_of_set[OF R] assms order.refl)+
thus ?case by auto
qed (auto simp: permutations_of_set_def)

corollary card_finite_linorders:
assumes "finite A"
shows   "card {R. linorder_on A R} = fact (card A)"
proof -
have "card {R. linorder_on A R} = card (permutations_of_set A)"
by (rule sym, rule bij_betw_same_card [OF bij_betw_linorder_of_list[OF assms]])
also from assms have "… = fact (card A)" by (rule card_permutations_of_set)
finally show ?thesis .
qed

end
```