Theory Minimize_Wrt

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

section ‹Minimization›

theory Minimize_Wrt
  imports Sorted_Wrt
begin

fun minimize_wrt
  where
    "minimize_wrt P [] = []"
  | "minimize_wrt P (x # xs) = x # filter (P x) (minimize_wrt P xs)"

lemma minimize_wrt_subset: "set (minimize_wrt P xs) ⊆ set xs"
  by (induct xs) auto

lemmas minimize_wrtD = minimize_wrt_subset [THEN subsetD]

lemma sorted_wrt_minimize_wrt:
  "sorted_wrt P (minimize_wrt P xs)"
  by (induct xs) (auto simp: sorted_wrt_filter)

lemma sorted_wrt_imp_sorted_wrt_minimize_wrt:
  "sorted_wrt Q xs ⟹ sorted_wrt Q (minimize_wrt P xs)"
  by (induct xs) (auto simp: sorted_wrt_filter dest: minimize_wrtD)

lemma in_minimize_wrt_False:
  assumes "⋀x y. Q x y ⟹ ¬ Q y x"
    and "sorted_wrt Q xs"
    and "x ∈ set (minimize_wrt P xs)"
    and "¬ P y x" and "Q y x" and "y ∈ set xs" and "y ≠ x"
  shows False
  using assms by (induct xs) (auto dest: minimize_wrtD)

lemma in_minimize_wrtI:
  assumes "x ∈ set xs"
    and "∀y∈set xs. P y x"
  shows "x ∈ set (minimize_wrt P xs)"
  using assms by (induct xs) auto

lemma minimize_wrt_eq:
  assumes "distinct xs" and "⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ P x y ⟷ Q x y ∨ x = y"
  shows "minimize_wrt P xs = minimize_wrt Q xs"
  using assms by (induct xs) (auto, metis contra_subsetD filter_cong minimize_wrt_subset)

lemma minimize_wrt_ni:
  assumes "x ∈ set xs"
    and "x ∉ set (minimize_wrt Q xs)"
  shows "∃y ∈ set xs. (¬ Q y x) ∧ x ≠ y"
  using assms by (induct xs) (auto)

lemma in_minimize_wrtD:
  assumes "⋀x y. Q x y ⟹ ¬ Q y x"
    and "sorted_wrt Q xs"
    and "x ∈ set (minimize_wrt P xs)"
    and "⋀x y. ¬ P x y ⟹ Q x y"
    and "⋀x. P x x"
  shows "x ∈ set xs ∧ (∀y∈set xs. P y x)"
  using in_minimize_wrt_False [OF assms(1-3)] and minimize_wrt_subset [of P xs] and assms(3-5)
  by blast

lemma in_minimize_wrt_iff:
  assumes "⋀x y. Q x y ⟹ ¬ Q y x"
    and "sorted_wrt Q xs"
    and "⋀x y. ¬ P x y ⟹ Q x y"
    and "⋀x. P x x"
  shows "x ∈ set (minimize_wrt P xs) ⟷ x ∈ set xs ∧ (∀y∈set xs. P y x)"
  using assms and in_minimize_wrtD [of Q xs x P, OF assms(1,2) _ assms(3,4)]
  by (blast intro: in_minimize_wrtI)

lemma set_minimize_wrt:
  assumes "⋀x y. Q x y ⟹ ¬ Q y x"
    and "sorted_wrt Q xs"
    and "⋀x y. ¬ P x y ⟹ Q x y"
    and "⋀x. P x x"
  shows "set (minimize_wrt P xs) = {x ∈ set xs. ∀y∈set xs. P y x}"
  by (auto simp: in_minimize_wrt_iff [OF assms])

lemma minimize_wrt_append:
  assumes "∀x∈set xs. ∀y∈set (xs @ ys). P y x"
  shows "minimize_wrt P (xs @ ys) = xs @ filter (λy. ∀x∈set xs. P x y) (minimize_wrt P ys)"
  using assms by (induct xs) (auto intro: filter_cong)

end