(* 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" 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