Theory Sort_Descending
theory Sort_Descending
imports Main
begin
section‹sorting descending›
context linorder
begin
fun sorted_descending :: "'a list ⇒ bool" where
"sorted_descending [] ⟷ True" |
"sorted_descending (a#as) ⟷ (∀x ∈ set as. a ≥ x) ∧ sorted_descending as"
definition sort_descending_key :: "('b ⇒ 'a) ⇒ 'b list ⇒ 'b list" where
"sort_descending_key f xs ≡ rev (sort_key f xs)"
end
lemma sorted_descending_Cons: "sorted_descending (x#xs) ⟷ sorted_descending xs ∧ (∀y∈set xs. y ≤ x)"
by(induction xs) auto
lemma sorted_descending_tail: "sorted_descending (xs@[x]) ⟷ sorted_descending xs ∧ (∀y∈set xs. x ≤ y)"
by(induction xs) auto
lemma sorted_descending_append: "sorted_descending (xs @ ys) =
(sorted_descending xs ∧ sorted_descending ys ∧ (∀x∈set xs. ∀y∈set ys. x ≥ y))"
by(induction xs) auto
lemma sorted_descending: "sorted_descending (rev xs) ⟷ sorted xs"
apply(induction xs)
apply(simp)
apply(auto simp add: sorted_descending_tail)
done
lemma sorted_descending_alt: "sorted_descending xs ⟷ sorted (rev xs)"
using sorted_descending[of "rev xs"] unfolding rev_rev_ident .
lemma sort_descending: "sorted_descending (sort_descending_key (λx. x) xs)"
by(simp add: sort_descending_key_def sorted_descending)
lemma sort_descending_key_distinct: "distinct xs ⟹ distinct (sort_descending_key f xs)"
by(simp add: sort_descending_key_def)
lemma sorted_descending_sort_descending_key: "sorted_descending (map f (sort_descending_key f xs))"
apply(simp add: sort_descending_key_def)
using sorted_descending by (metis rev_map sorted_sort_key)
lemma sorted_descending_split: "sorted_descending (map f l) ⟹
∃m n. l = m @ n ∧ (∀e ∈ set m. f (hd l) = f e) ∧ (∀e ∈ set n. f e < f (hd l))"
proof(induction l)
case Nil thus ?case by simp
next
case (Cons a as)
from Cons(2) have IHm: "sorted_descending (map f as)" by simp
note mIH = Cons(1)[OF this]
thus ?case (is ?kees)
proof(cases as)
case Nil
show ?kees unfolding Nil by force
next
case (Cons aa ass)
show ?kees
proof(cases "f a = f aa")
case True
from mIH obtain m n where mn: "as = m @ n" "(∀e∈set m. f a = f e)" "(∀e∈set n. f e < f a)"
using True local.Cons by auto
have "a # as = a # m @ n" using mn(1) by simp
moreover have "∀e∈set (a # m). f (hd (a # m)) = f e" unfolding list.sel(1) using True mn(2) using Cons by auto
ultimately show "∃m n. a # as = m @ n ∧ (∀e∈set m. f (hd (a # as)) = f e) ∧
(∀e∈set n. f e < f (hd (a # as)))" using mn(3) by (metis append.simps(2) list.sel(1))
next
case False
from Cons.prems have "∀y∈set (map f as). y < f a"
unfolding list.map(2)
unfolding sorted_descending_Cons
unfolding set_map
unfolding local.Cons
using False
by auto
then have "∀e∈set as. f e < f a" by simp
moreover have "a # as = [a] @ as ∧ (∀e∈set [a]. f (hd [a]) = f e)" by simp
ultimately show ?kees by (metis list.sel(1))
qed
qed
qed
lemma sort_descending_set_inv[simp]: "set (sort_descending_key k t) = set t"
by (simp add: sort_descending_key_def)
end