Theory Simplex.Simplex_Auxiliary

(* Authors: F. Maric, M. Spasic *)
section ‹Auxiliary Results›
theory Simplex_Auxiliary
  imports 
    "HOL-Library.Mapping"
begin

(* -------------------------------------------------------------------------- *)
(* MoreList *)
(* -------------------------------------------------------------------------- *)
lemma map_reindex:
  assumes "∀ i < length l. g (l ! i) = f i"
  shows "map f [0..<length l] = map g l"
  using assms
  by (induct l rule: rev_induct) (auto simp add: nth_append split: if_splits)

lemma map_parametrize_idx: 
  "map f l = map (λi. f (l ! i)) [0..<length l]"
  by (induct l rule: rev_induct) (auto simp add: nth_append)

lemma last_tl:
  assumes "length l > 1"
  shows "last (tl l) = last l"
  using assms
  by (induct l) auto

lemma hd_tl:
  assumes "length l > 1"
  shows "hd (tl l) = l ! 1"
  using assms
  by (induct l) (auto simp add: hd_conv_nth)

lemma butlast_empty_conv_length:
  shows "(butlast l = []) = (length l ≤ 1)"
  by (induct l) (auto split: if_splits)

lemma butlast_nth:
  assumes "n + 1 < length l"
  shows "butlast l ! n = l ! n"
  using assms
  by (induct l rule: rev_induct) (auto simp add: nth_append)

lemma last_take_conv_nth:
  assumes "0 < n" "n ≤ length l"
  shows "last (take n l) = l ! (n - 1)"
  using assms
  by (cases "l = []") (auto simp add: last_conv_nth min_def)

lemma tl_nth:
  assumes "l ≠ []" 
  shows "tl l ! n = l ! (n + 1)"
  using assms
  by (induct l) auto

lemma interval_3split:
  assumes "i < n"
  shows "[0..<n] = [0..<i] @ [i] @ [i+1..<n]"
proof-
  have "[0..<n] = [0..<i + 1] @ [i + 1..<n]"
    using upt_add_eq_append[of 0 "i + 1" "n - i - 1"]
    using ‹i < n›
    by (auto simp del: upt_Suc)
  then show ?thesis
    by simp
qed

abbreviation "list_min l ≡ foldl min (hd l) (tl l)"
lemma list_min_Min[simp]: "l ≠ [] ⟹ list_min l = Min (set l)"
proof (induct l rule: rev_induct)
  case (snoc a l')
  then show ?case
    by (cases "l' = []") (auto simp add: ac_simps)
qed simp

(* Minimal element of a list satisfying the given property *)

definition min_satisfying :: "(('a::linorder) ⇒ bool) ⇒ 'a list ⇒ 'a option" where
  "min_satisfying P l ≡
    let xs = filter P l in
    if xs = [] then None else Some (list_min xs)"

lemma min_satisfying_None:
  "min_satisfying P l = None ⟶ 
    (∀ x ∈ set l. ¬ P x)"
  unfolding min_satisfying_def Let_def
  by (simp add: filter_empty_conv)

lemma min_satisfying_Some: 
  "min_satisfying P l = Some x ⟶ 
      x ∈ set l ∧ P x ∧ (∀ x' ∈ set l. x' < x ⟶ ¬ P x')"
proof (safe)
  let ?xs = "filter P l"
  assume "min_satisfying P l = Some x"
  then have "set ?xs ≠ {}" "x = Min (set ?xs)"
    unfolding min_satisfying_def Let_def
    by (auto split: if_splits simp add: filter_empty_conv)
  then show "x ∈ set l" "P x" 
    using Min_in[of "set ?xs"]
    by simp_all
  fix x'
  assume "x' ∈ set l" "P x'" "x' < x"
  have "x' ∉ set ?xs"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then have "x' ≥ x"
      using ‹x = Min (set ?xs)›
      by simp
    then show False
      using ‹x' < x›
      by simp
  qed
  then show "False"
    using ‹x' ∈ set l› ‹P x'›
    by simp
qed

(* -------------------------------------------------------------------------- *)
(* MoreNat *)
(* -------------------------------------------------------------------------- *)

lemma min_element:
  fixes k :: nat
  assumes "∃ (m::nat). P m"
  shows "∃ mm. P mm ∧ (∀ m'. m' < mm ⟶ ¬ P m')"
proof-
  from assms obtain m where "P m"
    by auto
  show ?thesis
  proof (cases "∀m'<m. ¬ P m'")
    case True
    then show ?thesis 
      using ‹P m›
      by auto
  next
    case False
    then show ?thesis
    proof (induct m)
      case 0
      then show ?case
        by auto
    next
      case (Suc m')
      then show ?case
        by (cases "¬ (∀m'a<m'. ¬ P m'a)") auto
    qed
  qed
qed

(* -------------------------------------------------------------------------- *)
(* MoreFun *)
(* -------------------------------------------------------------------------- *)

lemma finite_fun_args:
  assumes "finite A" "∀ a ∈ A. finite (B a)"
  shows "finite {f. (∀ a. if a ∈ A then f a ∈ B a else f a = f0 a)}" (is "finite (?F A)")
  using assms
proof (induct) 
  case empty
  have "?F {} = {λ x. f0 x}"
    by auto
  then show ?case
    by auto
next
  case (insert a A')
  then have "finite (?F A')"
    by auto
  let ?f = "λ f. {f'. (∀ a'. if a = a' then f' a ∈ B a else f' a' = f a')}"
  have "∀ f ∈ ?F A'. finite (?f f)"
  proof
    fix f
    assume "f ∈ ?F A'"
    then have "?f f = (λ b. f (a := b)) ` B a"
      by (force split: if_splits)
    then show "finite (?f f)"
      using ‹∀a∈insert a A'. finite (B a)›
      by auto
  qed
  then have "finite (⋃ (?f ` (?F A')))"
    using ‹finite (?F A')›
    by auto
  moreover
  have "?F (insert a A') = ⋃ (?f ` (?F A'))"
  proof
    show "?F (insert a A') ⊆ ⋃ (?f ` (?F A'))"
    proof
      fix f
      assume "f ∈ ?F (insert a A')"
      then have "f ∈ ?f (f (a := f0 a))" "f (a := f0 a) ∈ ?F A'"
        using ‹a ∉ A'›
        by auto
      then show "f ∈ ⋃ (?f ` (?F A'))"
        by blast
    qed
  next
    show "⋃ (?f ` (?F A')) ⊆ ?F (insert a A')"
    proof
      fix f
      assume "f ∈ ⋃ (?f ` (?F A'))"
      then obtain f0 where "f0 ∈ ?F A'" "f ∈ ?f f0"
        by auto
      then show "f ∈ ?F (insert a A')"
        using ‹a ∉ A'›
        by (force split: if_splits)
    qed
  qed
  ultimately
  show ?case
    by simp
qed

(* -------------------------------------------------------------------------- *)
(* MoreMapping *)
(* -------------------------------------------------------------------------- *)

lemma foldl_mapping_update:
  assumes "X ∈ set l" "distinct (map f l)"
  shows "Mapping.lookup (foldl (λm a. Mapping.update (f a) (g a) m) i l) (f X) = Some (g X)"
  using assms
proof(induct l rule:rev_induct)
  case Nil
  then show ?case
    by simp
next
  case (snoc h t)
  show ?case
  proof (cases "f h = f X")
    case True
    then show ?thesis using snoc by (auto simp: lookup_update)
  next
    case False
    show ?thesis by (simp add: lookup_update' False, rule snoc, insert False snoc, auto)
  qed
qed

end