Theory HOL-Data_Structures.Sorted_Less

(* Author: Tobias Nipkow *)

section ‹Lists Sorted wrt $<$›

theory Sorted_Less
imports Less_False
begin

hide_const sorted

text ‹Is a list sorted without duplicates, i.e., wrt ‹<›?.›

abbreviation sorted :: "'a::linorder list ⇒ bool" where
"sorted ≡ sorted_wrt (<)"

lemmas sorted_wrt_Cons = sorted_wrt.simps(2)

text ‹The definition of \<^const>‹sorted_wrt› relates each element to all the elements after it.
This causes a blowup of the formulas. Thus we simplify matters by only comparing adjacent elements.›

declare
  sorted_wrt.simps(2)[simp del]
  sorted_wrt1[simp] sorted_wrt2[OF transp_on_less, simp]

lemma sorted_cons: "sorted (x#xs) ⟹ sorted xs"
by(simp add: sorted_wrt_Cons)

lemma sorted_cons': "ASSUMPTION (sorted (x#xs)) ⟹ sorted xs"
by(rule ASSUMPTION_D [THEN sorted_cons])

lemma sorted_snoc: "sorted (xs @ [y]) ⟹ sorted xs"
by(simp add: sorted_wrt_append)

lemma sorted_snoc': "ASSUMPTION (sorted (xs @ [y])) ⟹ sorted xs"
by(rule ASSUMPTION_D [THEN sorted_snoc])

lemma sorted_mid_iff:
  "sorted(xs @ y # ys) = (sorted(xs @ [y]) ∧ sorted(y # ys))"
by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)

lemma sorted_mid_iff2:
  "sorted(x # xs @ y # ys) =
  (sorted(x # xs) ∧ x < y ∧ sorted(xs @ [y]) ∧ sorted(y # ys))"
by(fastforce simp add: sorted_wrt_Cons sorted_wrt_append)

lemma sorted_mid_iff': "NO_MATCH [] ys ⟹
  sorted(xs @ y # ys) = (sorted(xs @ [y]) ∧ sorted(y # ys))"
by(rule sorted_mid_iff)

lemmas sorted_lems = sorted_mid_iff' sorted_mid_iff2 sorted_cons' sorted_snoc'

text‹Splay trees need two additional \<^const>‹sorted› lemmas:›

lemma sorted_snoc_le:
  "ASSUMPTION(sorted(xs @ [x])) ⟹ x ≤ y ⟹ sorted (xs @ [y])"
by (auto simp add: sorted_wrt_append ASSUMPTION_def)

lemma sorted_Cons_le:
  "ASSUMPTION(sorted(x # xs)) ⟹ y ≤ x ⟹ sorted (y # xs)"
by (auto simp add: sorted_wrt_Cons ASSUMPTION_def)

end