Theory Sorted_Wrt

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
License: LGPL
*)

theory Sorted_Wrt
  imports Main
begin

lemma sorted_wrt_filter:
  "sorted_wrt P xs ⟹ sorted_wrt P (filter Q xs)"
  by (induct xs) (auto)

lemma sorted_wrt_map_mono:
  assumes "sorted_wrt Q xs"
    and "⋀x y. Q x y ⟹ P (f x) (f y)"
  shows "sorted_wrt P (map f xs)"
  using assms by (induct xs) (auto)

lemma sorted_wrt_concat_map_map:
  assumes "sorted_wrt Q xs"
    and "sorted_wrt Q ys"
    and "⋀a x y. Q x y ⟹ P (f x a) (f y a)"
    and "⋀x y u v. x ∈ set xs ⟹ y ∈ set xs ⟹ Q u v ⟹ P (f x u) (f y v)"
  shows "sorted_wrt P [f x y . y ← ys, x ← xs]"
  using assms by (induct ys)
    (auto simp: sorted_wrt_append intro: sorted_wrt_map_mono [of Q])

lemma sorted_wrt_concat_map:
  assumes "sorted_wrt P (map h xs)"
    and "⋀x. x ∈ set xs ⟹ sorted_wrt P (map h (f x))"
    and "⋀x y u v. P (h x) (h y) ⟹ x ∈ set xs ⟹ y ∈ set xs ⟹ u ∈ set (f x) ⟹ v ∈ set (f y) ⟹ P (h u) (h v)"
  shows "sorted_wrt P (concat (map (map h ∘ f) xs))"
  using assms by (induct xs) (auto simp: sorted_wrt_append)

lemma sorted_wrt_map_distr:
  assumes "sorted_wrt (λx y. P x y) (map f xs)"
  shows "sorted_wrt (λx y. P (f x) (f y)) xs"
  using assms
  by (induct xs) (auto)

lemma sorted_wrt_tl:
  "xs ≠ [] ⟹ sorted_wrt P xs ⟹ sorted_wrt P (tl xs)"
  by (cases xs) (auto)

end