Theory Simple_Algorithm

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

theory Simple_Algorithm
  imports
    Linear_Diophantine_Equations
    Minimize_Wrt
begin

(*TODO: move?*)
lemma concat_map_nth0: "xs ≠ [] ⟹ f (xs ! 0) ≠ [] ⟹ concat (map f xs) ! 0 = f (xs ! 0) ! 0"
  by (induct xs) (auto simp: nth_append)


subsection ‹Reverse-Lexicographic Enumeration of Potential Minimal Solutions›

fun rlex2 :: "(nat list × nat list) ⇒ (nat list × nat list) ⇒ bool"  (infix ‹<⇩r⇩l⇩e⇩x⇩2› 50)
  where
    "(xs, ys) <⇩r⇩l⇩e⇩x⇩2 (us, vs) ⟷ xs @ ys <⇩r⇩l⇩e⇩x us @ vs"

lemma rlex2_irrefl:
  "¬ x <⇩r⇩l⇩e⇩x⇩2 x"
  by (cases x) (auto simp: rlex_irrefl)

lemma rlex2_not_sym: "x <⇩r⇩l⇩e⇩x⇩2 y ⟹ ¬ y <⇩r⇩l⇩e⇩x⇩2 x"
  using rlex_not_sym by (cases x; cases y; simp)

lemma less_imp_rlex2: "¬ (case x of (x, y) ⇒ λ(u, v). ¬ x @ y <⇩v u @ v) y ⟹ x <⇩r⇩l⇩e⇩x⇩2 y"
  using less_imp_rlex by (cases x; cases y; auto)


text ‹Generate all lists (of natural numbers) of length ‹n› with elements bounded by ‹B›.›
fun gen :: "nat ⇒ nat ⇒ nat list list"
  where
    "gen B 0 = [[]]"
  | "gen B (Suc n) = [x#xs . xs ← gen B n, x ← [0 ..< B + 1]]"

definition "generate A B m n = tl [(x, y) . y ← gen B n, x ← gen A m]"

definition "check a b = filter (λ(x, y). a ∙ x = b ∙ y)"

definition "minimize = minimize_wrt (λ(x, y) (u, v). ¬ x @ y <⇩v u @ v)"

definition "solutions a b =
  (let A = Max (set b); B = Max (set a); m = length a; n = length b
  in minimize (check a b (generate A B m n)))"

lemma set_gen: "set (gen B n) = {xs. length xs = n ∧ (∀i<n. xs ! i ≤ B)}" (is "_ = ?A n")
proof (induct n)
  case [simp]: (Suc n)
  { fix xs assume "xs ∈ ?A (Suc n)"
    then have "xs ∈ set (gen B (Suc n))"
      by (cases xs) (force simp: All_less_Suc2)+ }
  then show ?case by (auto simp: less_Suc_eq_0_disj)
qed simp

abbreviation "gen2 A B m n ≡ [(x, y) . y ← gen B n, x ← gen A m]"

lemma sorted_wrt_gen:
  "sorted_wrt (<⇩r⇩l⇩e⇩x) (gen B n)"
by (induction n)
   (auto simp: rlex_Cons sorted_wrt_append sorted_wrt_map rlex_irrefl
    intro!: sorted_wrt_concat_map [where h = id, simplified])

lemma sorted_wrt_gen2: "sorted_wrt (<⇩r⇩l⇩e⇩x⇩2) (gen2 A B m n)"
  by (intro sorted_wrt_concat_map_map [where Q = "(<⇩r⇩l⇩e⇩x)"] sorted_wrt_gen)
    (auto simp: set_gen rlex_def intro:  lex_append_leftI lex_append_rightI)

lemma gen_ne [simp]: "gen B n ≠ []" by (induct n) auto

lemma gen2_ne: "gen2 A B m n ≠ []" by auto

lemma sorted_wrt_generate: "sorted_wrt (<⇩r⇩l⇩e⇩x⇩2) (generate A B m n)"
  by (auto simp: generate_def intro: sorted_wrt_tl sorted_wrt_gen2)

abbreviation "check_generate a b ≡ check a b (generate (Max (set b)) (Max (set a)) (length a) (length b))"

lemma sorted_wrt_check_generate: "sorted_wrt (<⇩r⇩l⇩e⇩x⇩2) (check_generate a b)"
  by (auto simp: check_def intro: sorted_wrt_filter sorted_wrt_generate)

lemma in_tl_gen2: "x ∈ set (tl (gen2 A B m n)) ⟹ x ∈ set (gen2 A B m n)"
  by (rule list.set_sel) simp

lemma gen_nth0 [simp]: "gen B n ! 0 = zeroes n"
  by (induct n) (auto simp: nth_append concat_map_nth0)

lemma gen2_nth0 [simp]:
  "gen2 A B m n ! 0 = (zeroes m, zeroes n)"
  by (auto simp: concat_map_nth0)

lemma set_gen2:
  "set (gen2 A B m n) = {(x, y). length x = m ∧ length y = n ∧ (∀i<m. x ! i ≤ A) ∧ (∀j<n. y ! j ≤ B)}"
  by (auto simp: set_gen)

lemma gen2_unique:
  assumes "i < j"
    and "j < length (gen2 A B m n)"
  shows "gen2 A B m n ! i ≠ gen2 A B m n ! j"
  using sorted_wrt_nth_less [OF sorted_wrt_gen2 assms]
  by (auto simp: rlex2_irrefl)

lemma zeroes_ni_tl_gen2:
  "(zeroes m, zeroes n) ∉ set (tl (gen2 A B m n))"
proof -
  have "gen2 A B m n ! 0 = (zeroes m, zeroes n)" by (auto simp: generate_def)
  with gen2_unique[of 0 _ A m B n] show ?thesis
    by (metis (no_types, lifting) Suc_eq_plus1 in_set_conv_nth length_tl less_diff_conv nth_tl zero_less_Suc)
qed

lemma set_generate:
  "set (generate A B m n) = {(x, y). (x, y) ≠ (zeroes m, zeroes n) ∧ (x, y) ∈ set (gen2 A B m n)}"
proof
  show "set (generate A B m n)
    ⊆ {(x, y).(x, y) ≠ (zeroes m, zeroes n) ∧ (x, y) ∈ set (gen2 A B m n)}"
    using in_tl_gen2 and mem_Collect_eq and zeroes_ni_tl_gen2 by (auto simp: generate_def)
next
  have "(zeroes m, zeroes n) = hd (gen2 A B m n)"
    by (simp add: hd_conv_nth)
  moreover have "set (gen2 A B m n) = set (generate A B m n) ∪ {(zeroes m, zeroes n)}"
    by (metis Un_empty_right generate_def Un_insert_right gen2_ne calculation list.exhaust_sel list.simps(15))
  ultimately show " {(x, y). (x, y) ≠ (zeroes m, zeroes n) ∧ (x, y) ∈ set (gen2 A B m n)}
    ⊆ set (generate A B m n)"
    by blast
qed

lemma set_check_generate:
  "set (check_generate a b) = {(x, y).
    (x, y) ≠ (zeroes (length a), zeroes (length b)) ∧
    length x = length a ∧ length y = length b ∧ a ∙ x = b ∙ y ∧
    (∀i<length a. x ! i ≤ Max (set b)) ∧ (∀j<length b. y ! j ≤ Max (set a))}"
  unfolding check_def and set_filter and set_generate and set_gen2 by auto

lemma set_minimize_check_generate:
  "set (minimize (check_generate a b)) =
    {(x, y)∈set (check_generate a b). ¬ (∃(u, v)∈set (check_generate a b). u @ v <⇩v x @ y)}"
  unfolding minimize_def
  by (subst set_minimize_wrt [OF _ sorted_wrt_check_generate]) (auto dest: rlex_not_sym less_imp_rlex)

lemma set_solutions_iff:
  "set (solutions a b) =
    {(x, y) ∈ set (check_generate a b). ¬ (∃(u, v)∈set (check_generate a b). u @ v <⇩v x @ y)}"
  by (auto simp: solutions_def set_minimize_check_generate)


subsubsection ‹Completeness: every minimal solution is generated by ‹solutions››

lemma (in hlde) solutions_complete:
  "Minimal_Solutions ⊆ set (solutions a b)"
proof (rule subrelI)
  let ?A = "Max (set b)" and ?B = "Max (set a)"
  fix x y assume min: "(x, y) ∈ Minimal_Solutions"
  then have "(x, y) ∈ set (check a b (generate ?A ?B m n))"
    by (auto simp: Minimal_Solutions_alt_def set_check_generate less_eq_def in_Solutions_iff)
  moreover have "∀(u, v) ∈ set (check a b (generate ?A ?B m n)). ¬ u @ v <⇩v x @ y"
    using min and no0
    by (auto simp: check_def set_generate neq_0_iff' set_gen nonzero_iff dest!: Minimal_Solutions_min)
  ultimately show "(x, y) ∈ set (solutions a b)" by (auto simp: set_solutions_iff)
qed


subsubsection ‹Correctness: ‹solutions› generates only minimal solutions.›

lemma (in hlde) solutions_sound:
  "set (solutions a b) ⊆ Minimal_Solutions"
proof (rule subrelI)
  fix x y assume sol: "(x, y) ∈ set (solutions a b)"
  show "(x, y) ∈ Minimal_Solutions"
  proof (rule Minimal_SolutionsI')
    show *: "(x, y) ∈ Solutions"
      using sol by (auto simp: set_solutions_iff in_Solutions_iff check_def set_generate set_gen)
    show "nonzero x"
      using sol and nonzero_iff and replicate_eqI and nonzero_Solutions_iff [OF *]
      by (fastforce simp: solutions_def minimize_def check_def set_generate set_gen dest!: minimize_wrtD)
    show "¬ (∃(u, v)∈Minimal_Solutions. u @ v <⇩v x @ y)"
    proof
      have min_cg: "(x, y) ∈ set (minimize (check_generate a b))"
        using sol by (auto simp: solutions_def)
      note * = in_minimize_wrt_False [OF _ sorted_wrt_check_generate min_cg [unfolded minimize_def]]

      assume "∃(u, v)∈Minimal_Solutions. u @ v <⇩v x @ y"
      then obtain u and v where "(u, v) ∈ Minimal_Solutions" and less: "u @ v <⇩v x @ y" by blast
      then have "(u, v) ∈ set (solutions a b)" by (auto intro: solutions_complete [THEN subsetD])
      then have "(u, v) ∈ set (check_generate a b)"
        by (auto simp: solutions_def minimize_def dest: minimize_wrtD)
      from * [OF _ _ _ this] and less show False
        using less_imp_rlex and rlex_not_sym by force
    qed
  qed
qed

lemma (in hlde) set_solutions [simp]: "set (solutions a b) = Minimal_Solutions"
  using solutions_sound and solutions_complete by blast

end