# Theory Linorder_Relations

(*
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-Combinatorics.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"
by (simp add: distinct_count_atmost_1)

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)"
by (simp add: sorted_wrt_list_of_set_def)
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}"
by (simp add: linorder_rank_def)
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"
by (simp add: linorder_rank_def)

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


# Theory Comparison_Sort_Lower_Bound

(*
File:     Comparison_Sort_Lower_Bound.thy
Author:   Manuel Eberl <eberlm@in.tum.de>

Proof of the lower-bound on worst-case comparisons in a comparison-based sorting algorithm.
*)
section ‹Lower bound on costs of comparison-based sorting›
theory Comparison_Sort_Lower_Bound
imports
Complex_Main
Linorder_Relations
Stirling_Formula.Stirling_Formula
"Landau_Symbols.Landau_More"
begin

subsection ‹Abstract description of sorting algorithms›

text ‹
We have chosen to model a sorting algorithm in the following way: A sorting algorithm takes a
list with distinct elements and a linear ordering on these elements, and it returns a list
with the same elements that is sorted w.\,r.\,t.\ the given ordering.

The use of an explicit ordering means that the algorithm must look at the ordering, i.\,e.\
it has to use pair-wise comparison of elements, since all the information that is relevant
for producing the correct sorting is in the ordering; the elements themselves are irrelevant.

Furthermore, we record the number of comparisons that the algorithm makes by not giving it the
relation explicitly, but in the form of a comparison oracle that may be queried.

A sorting algorithm (or sorter') for a fixed input list (but for arbitrary orderings) can then
be written as a recursive datatype that is either the result (the sorted list) or a comparison
query consisting of two elements and a continuation that maps the result of the comparison
to the remaining computation.
›

datatype 'a sorter = Return "'a list" | Query 'a 'a "bool ⇒ 'a sorter"

text ‹
Cormen~\emph{et\ al.}~\cite{cormen}\ use a similar decision tree' model where an sorting
algorithm for lists of fixed size $n$ is modelled as a binary tree where each node is a
comparison of two elements. They also demand that every leaf in the tree be reachable in
order to avoid dead' subtrees (if the algorithm makes redundant comparisons, there may be
branches that can never be taken). Then, the worst-case number of comparisons made is simply
the height of the tree.

We chose a subtly different model that does not have this restriction on the algorithm but
instead uses a more semantic way of counting the worst-case number of comparisons: We simply
use the maximum number of comparisons that occurs for any of the (finitely many) inputs.

We therefore first define a function that counts the number of queries for a specific
ordering and then a function that counts the number of queries in the worst case (ranging
over a given set of allowed orderings; typically, this will be the set of all linear orders
on the list).
›
primrec count_queries :: "('a × 'a) set ⇒ 'a sorter ⇒ nat" where
"count_queries _ (Return _)    = 0"
| "count_queries R (Query a b f) = Suc (count_queries R (f ((a, b) ∈ R)))"

definition count_wc_queries :: "('a × 'a) set set ⇒ 'a sorter ⇒ nat" where
"count_wc_queries Rs sorter = (if Rs = {} then 0 else Max ((λR. count_queries R sorter)  Rs))"

lemma count_wc_queries_empty [simp]: "count_wc_queries {} sorter = 0"
by (simp add: count_wc_queries_def)

lemma count_wc_queries_aux:
assumes "⋀R. R ∈ Rs ⟹ sorter = sorter' R" "Rs ⊆ Rs'" "finite Rs'"
shows   "count_wc_queries Rs sorter ≤ Max ((λR. count_queries R (sorter' R))  Rs')"
proof (cases "Rs = {}")
case False
hence "count_wc_queries Rs sorter = Max ((λR. count_queries R sorter)  Rs)"
by (simp add: count_wc_queries_def)
also have "(λR. count_queries R sorter)  Rs = (λR. count_queries R (sorter' R))  Rs"
by (intro image_cong refl) (simp_all add: assms)
also have "Max … ≤ Max ((λR. count_queries R (sorter' R))  Rs')" using False
by (intro Max_mono assms image_mono finite_imageI) auto
finally show ?thesis .
qed simp_all

primrec eval_sorter :: "('a × 'a) set ⇒ 'a sorter ⇒ 'a list" where
"eval_sorter _ (Return ys)   = ys"
| "eval_sorter R (Query a b f) = eval_sorter R (f ((a,b) ∈ R))"

text ‹
We now get an obvious bound on the maximum number of different results that a given sorter
can produce.
›
lemma card_range_eval_sorter:
assumes "finite Rs"
shows   "card ((λR. eval_sorter R e)  Rs) ≤ 2 ^ count_wc_queries Rs e"
using assms
proof (induction e arbitrary: Rs)
case (Return xs Rs)
have *: "(λR. eval_sorter R (Return xs))  Rs = (if Rs = {} then {} else {xs})" by auto
show ?case by (subst *) auto
next
case (Query a b f Rs)
have "f True ∈ range f" "f False ∈ range f" by simp_all
note IH = this [THEN Query.IH]
let ?Rs1 = "{R∈Rs. (a, b) ∈ R}" and ?Rs2 = "{R∈Rs. (a, b) ∉ R}"
let ?A = "(λR. eval_sorter R (f True))  ?Rs1" and ?B = "(λR. eval_sorter R (f False))  ?Rs2"
from Query.prems have fin: "finite ?Rs1" "finite ?Rs2" by simp_all

have *: "(λR. eval_sorter R (Query a b f))  Rs ⊆ ?A ∪ ?B"
proof (intro subsetI, elim imageE, goal_cases)
case (1 xs R)
thus ?case by (cases "(a,b) ∈ R") auto
qed

show ?case
proof (cases "Rs = {}")
case False
have "card ((λR. eval_sorter R (Query a b f))  Rs) ≤ card (?A ∪ ?B)"
by (intro card_mono finite_UnI finite_imageI fin *)
also have "… ≤ card ?A + card ?B" by (rule card_Un_le)
also have "… ≤ 2 ^ count_wc_queries ?Rs1 (f True) + 2 ^ count_wc_queries ?Rs2 (f False)"
by (intro add_mono IH fin)
also have "count_wc_queries ?Rs1 (f True) ≤ Max ((λR. count_queries R (f ((a,b)∈R)))  Rs)"
by (intro count_wc_queries_aux Query.prems) auto
also have "count_wc_queries ?Rs2 (f False) ≤ Max ((λR. count_queries R (f ((a,b)∈R)))  Rs)"
by (intro count_wc_queries_aux Query.prems) auto
also have "2 ^ … + 2 ^ … = (2 ^ Suc … :: nat)" by simp
also have "Suc (Max ((λR. count_queries R (f ((a,b)∈R)))  Rs)) =
Max (Suc  ((λR. count_queries R (f ((a,b)∈R)))  Rs))" using False
by (intro mono_Max_commute finite_imageI Query.prems) (auto simp: incseq_def)
also have "Suc  ((λR. count_queries R (f ((a,b)∈R)))  Rs) =
(λR. Suc (count_queries R (f ((a,b)∈R))))  Rs" by (simp add: image_image)
also have "Max … = count_wc_queries Rs (Query a b f)" using False
by (auto simp add: count_wc_queries_def)
finally show ?thesis by - simp_all
qed simp_all
qed

text ‹
The following predicate describes what constitutes a valid sorting result for a given
ordering and a given input list. Note that when the ordering is linear, the result is
actually unique.
›
definition is_sorting :: "('a × 'a) set ⇒ 'a list ⇒ 'a list ⇒ bool" where
"is_sorting R xs ys ⟷ (mset xs = mset ys) ∧ sorted_wrt R ys"

subsection ‹Lower bounds on number of comparisons›

text ‹
For a list of $n$ distinct elements, there are $n!$ linear orderings on $n$ elements,
each of which leads to a different result after sorting the original list.
Since a sorter can produce at most $2^k$ different results with $k$ comparisons, we get
the bound $2^k \geq n!$:
›
theorem
fixes sorter :: "'a sorter" and xs :: "'a list"
assumes distinct: "distinct xs"
assumes sorter: "⋀R. linorder_on (set xs) R ⟹ is_sorting R xs (eval_sorter R sorter)"
defines "Rs ≡ {R. linorder_on (set xs) R}"
shows   two_power_count_queries_ge: "fact (length xs) ≤ (2 ^ count_wc_queries Rs sorter :: nat)"
and   count_queries_ge:           "log 2 (fact (length xs)) ≤ real (count_wc_queries Rs sorter)"
proof -
have "Rs ⊆ Pow (set xs × set xs)" by (auto simp: Rs_def linorder_on_def refl_on_def)
hence fin: "finite Rs" by (rule finite_subset) simp_all
from assms have "fact (length xs) = card (permutations_of_set (set xs))"
by (simp add: distinct_card)
also have "permutations_of_set (set xs) ⊆ (λR. eval_sorter R sorter)  Rs"
proof (rule subsetI, goal_cases)
case (1 ys)
define R where "R = linorder_of_list ys"
define zs where "zs = eval_sorter R sorter"
from 1 and distinct have mset_ys: "mset ys = mset xs"
by (auto simp: set_eq_iff_mset_eq_distinct permutations_of_set_def)
from 1 have *: "linorder_on (set xs) R" unfolding R_def using linorder_linorder_of_list[of ys]
by (simp add: permutations_of_set_def)
from sorter[OF this] have "mset xs = mset zs" "sorted_wrt R zs"
by (simp_all add: is_sorting_def zs_def)
moreover from 1 have "sorted_wrt R ys" unfolding R_def
by (intro sorted_wrt_linorder_of_list) (simp_all add: permutations_of_set_def)
ultimately have "zs = ys"
by (intro sorted_wrt_linorder_unique[OF *]) (simp_all add: mset_ys)
moreover from * have "R ∈ Rs" by (simp add: Rs_def)
ultimately show ?case unfolding zs_def by blast
qed
hence "card (permutations_of_set (set xs)) ≤ card ((λR. eval_sorter R sorter)  Rs)"
by (intro card_mono finite_imageI fin)
also from fin have "… ≤ 2 ^ count_wc_queries Rs sorter" by (rule card_range_eval_sorter)
finally show *: "fact (length xs) ≤ (2 ^ count_wc_queries Rs sorter :: nat)" .

have "ln (fact (length xs)) = ln (real (fact (length xs)))" by simp
also have "… ≤ ln (real (2 ^ count_wc_queries Rs sorter))"
proof (subst ln_le_cancel_iff)
show "real (fact (length xs)) ≤ real (2 ^ count_wc_queries Rs sorter)"
by (subst of_nat_le_iff) (rule *)
qed simp_all
also have "… = real (count_wc_queries Rs sorter) * ln 2" by (simp add: ln_realpow)
finally have "real (count_wc_queries Rs sorter) ≥ ln (fact (length xs)) / ln 2"
by (simp add: field_simps)
also have "ln (fact (length xs)) / ln 2 = log 2 (fact (length xs))" by (simp add: log_def)
finally show **: "log 2 (fact (length xs)) ≤ real (count_wc_queries Rs sorter)" .
qed

(* TODO: Good example for automation. Also, move. *)
lemma ln_fact_bigo: "(λn. ln (fact n) - (ln (2 * pi * n) / 2 + n * ln n - n)) ∈ O(λn. 1 / n)"
and asymp_equiv_ln_fact [asymp_equiv_intros]: "(λn. ln (fact n)) ∼[at_top] (λn. n * ln n)"
proof -
include asymp_equiv_notation
define f where "f = (λn. ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)"
have "eventually (λn. ln (fact n) - f n ∈ {0..1/(12*real n)}) at_top"
using eventually_gt_at_top[of "1::nat"]
proof eventually_elim
case (elim n)
with ln_fact_bounds[of n] show ?case by (simp add: f_def)
qed
hence "eventually (λn. norm (ln (fact n) - f n) ≤ (1/12) * norm (1 / real n)) at_top"
using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp_all add: field_simps)
thus "(λn. ln (fact n) - f n) ∈ O(λn. 1 / real n)"
using bigoI[of "λn. ln (fact n) - f n" "1/12" "λn. 1 / real n"] by simp
also have "(λn. 1 / real n) ∈ o(f)" unfolding f_def by (intro smallo_real_nat_transfer) simp
finally have "(λn. f n + (ln (fact n) - f n)) ∼ f"
by (subst asymp_equiv_add_right) simp_all
hence "(λn. ln (fact n)) ∼ f" by simp
also have "f ∼ (λn. n * ln n + (ln (2*pi*n)/2 - n))" by (simp add: f_def algebra_simps)
also have "… ∼ (λn. n * ln n)" by (subst asymp_equiv_add_right) auto
finally show "(λn. ln (fact n)) ∼ (λn. n * ln n)" .
qed

text ‹
This leads to the following well-known Big-Omega bound on the number of comparisons
that a general sorting algorithm has to make:
›
corollary count_queries_bigomega:
fixes sorter :: "nat ⇒ nat sorter"
assumes sorter: "⋀n R. linorder_on {..<n} R ⟹
is_sorting R [0..<n] (eval_sorter R (sorter n))"
defines "Rs ≡ λn. {R. linorder_on {..<n} R}"
shows   "(λn. count_wc_queries (Rs n) (sorter n)) ∈ Ω(λn. n * ln n)"
proof -
have "(λn. n * ln n) ∈ Θ(λn. ln (fact n))"
by (subst bigtheta_sym) (intro asymp_equiv_imp_bigtheta asymp_equiv_intros)
also have "(λn. ln (fact n)) ∈ Θ(λn. log 2 (fact n))" by (simp add: log_def)
also have "(λn. log 2 (fact n)) ∈ O(λn. count_wc_queries (Rs n) (sorter n))"
proof (intro bigoI[where c = 1] always_eventually allI, goal_cases)
case (1 n)
have "norm (log 2 (fact n)) = log 2 (fact (length [0..<n]))" by simp
also from sorter[of n] have "… ≤ real (count_wc_queries (Rs n) (sorter n))"
using count_queries_ge[of "[0..<n]" "sorter n"] by (auto simp: Rs_def atLeast0LessThan)
also have "… = 1 * norm …" by simp
finally show ?case by simp
qed
finally show ?thesis by (simp add: bigomega_iff_bigo)
qed

end