Theory Util

section ‹Utilties›

theory Util
  imports
    Main
    "HOL-Library.Sublist"
    "HOL-Library.Multiset"

begin

abbreviation swap_events where
  "swap_events i j t ≡ take i t @ [t ! j, t ! i] @ take (j - (i+1)) (drop (i+1) t) @ drop (j+1) t"

lemma swap_neighbors_2:
  shows
    "i+1 < length t ⟹ swap_events i (i+1) t = (t[i := t ! (i+1)])[i+1 := t ! i]"
proof (induct i arbitrary: t)
  case 0
  then show ?case 
    by (metis One_nat_def Suc_eq_plus1 add_lessD1 append.left_neutral append_Cons cancel_comm_monoid_add_class.diff_cancel drop_update_cancel length_list_update numeral_One take_0 take_Cons_numeral upd_conv_take_nth_drop zero_less_Suc)
next
  case (Suc n)
  let ?t = "tl t"
  have "t = hd t # ?t"
    by (metis Suc.prems hd_Cons_tl list.size(3) not_less_zero)
  moreover have "swap_events n (n+1) ?t = (?t[n := ?t ! (n+1)])[n+1 := ?t ! n]" 
    by (metis Suc.hyps Suc.prems Suc_eq_plus1 length_tl less_diff_conv)
  ultimately show ?case 
    by (metis Suc_eq_plus1 append_Cons diff_self_eq_0 drop_Suc_Cons list_update_code(3) nth_Cons_Suc take_Suc_Cons)
qed

lemma swap_identical_length:
  assumes
    "i < j" and
    "j < length t"
  shows
    "length t = length (swap_events i j t)"
proof -
  have "length (take i t @ [t ! j, t ! i] @ take (j - (i+1)) (drop (i+1) t))
      = length (take i t) + length [t ! j, t ! i] + length (take (j - (i+1)) (drop (i+1) t))"
    by simp
  then have "... = j+1" 
    using assms(1) assms(2) by auto
  then show ?thesis using assms(2) by auto
qed

lemma swap_identical_heads:
  assumes
    "i < j" and
    "j < length t"
  shows
    "take i t = take i (swap_events i j t)"
  using assms by auto

lemma swap_identical_tails:
  assumes
    "i < j" and
    "j < length t"
  shows
    "drop (j+1) t = drop (j+1) (swap_events i j t)"
proof -
  have "length (take i t @ [t ! j, t ! i] @ take (j - (i+1)) (drop (i+1) t))
      = length (take i t) + length [t ! j, t ! i] + length (take (j - (i+1)) (drop (i+1) t))"
    by simp
  then have "... = j+1" 
    using assms(1) assms(2) by auto
  then show ?thesis 
    by (metis ‹length (take i t @ [t ! j, t ! i] @ take (j - (i + 1)) (drop (i + 1) t)) = length (take i t) + length [t ! j, t ! i] + length (take (j - (i + 1)) (drop (i + 1) t))› append.assoc append_eq_conv_conj)
qed

lemma swap_neighbors:
  shows
    "i+1 < length l ⟹ (l[i := l ! (i+1)])[i+1 := l ! i] = take i l @ [l ! (i+1), l ! i] @ drop (i+2) l"
proof (induct i arbitrary: l)
  case 0
  then show ?case 
    by (metis One_nat_def add.left_neutral add_lessD1 append_Cons append_Nil drop_update_cancel length_list_update one_add_one plus_1_eq_Suc take0 take_Suc_Cons upd_conv_take_nth_drop zero_less_two)
next
  case (Suc n)
  let ?l = "tl l"
  have "(l[Suc n := l ! (Suc n + 1)])[Suc n + 1 := l ! Suc n] = hd l # (?l[n := ?l ! (n+1)])[n+1 := ?l ! n]"
    by (metis Suc.prems add.commute add_less_same_cancel2 list.collapse list.size(3) list_update_code(3) not_add_less2 nth_Cons_Suc plus_1_eq_Suc)
  have "n + 1 < length ?l" using Suc.prems by auto
  then have "(?l[n := ?l ! (n+1)])[n+1 := ?l ! n] = take n ?l @ [?l ! (n+1), ?l ! n] @ drop (n+2) ?l"
    using Suc.hyps by simp
  then show ?case
    by (cases l) auto
qed

lemma swap_events_perm:
  assumes
    "i < j" and
    "j < length t"
  shows
    "mset (swap_events i j t) = mset t"
proof -
  have swap: "swap_events i j t
      = take i t @ [t ! j, t ! i] @ (take (j - (i+1)) (drop (i+1) t)) @ (drop (j+1) t)"
    by auto
  have reg: "t = take i t @ (take ((j+1) - i) (drop i t)) @ drop (j+1) t" 
    by (metis add_diff_inverse_nat add_lessD1 append.assoc append_take_drop_id assms(1) less_imp_add_positive less_not_refl take_add)
  have "mset (take i t) = mset (take i t)" by simp
  moreover have "mset (drop (j+1) t) = mset (drop (j+1) t)" by simp
  moreover have "mset ([t ! j, t ! i] @ (take (j - (i+1)) (drop (i+1) t))) = mset (take ((j+1) - i) (drop i t))"
  proof -
    let ?l = "take (j - (i+1)) (drop (i+1) t)"
    have "take ((j+1) - i) (drop i t) = t ! i # ?l @ [t ! j]"
    proof -
      have f1: "Suc (j - Suc i) = j - i"
        by (meson Suc_diff_Suc assms(1))
      have f2: "i < length t"
        using assms(1) assms(2) by linarith
      have f3: "j - (i + 1) + (i + 1) = j"
        using ‹i < j› by simp
      then have "drop (j - (i + 1)) (drop (i + 1) t) = drop j t"
        by (metis drop_drop)
      then show ?thesis
        using f3 f2 f1 by (metis (no_types) Cons_nth_drop_Suc Suc_diff_le Suc_eq_plus1 assms(1) assms(2) hd_drop_conv_nth length_drop less_diff_conv nat_less_le take_Suc_Cons take_hd_drop)
    qed
    then show ?thesis by fastforce
  qed
  ultimately show ?thesis using swap reg
    by simp (metis mset_append union_mset_add_mset_left union_mset_add_mset_right)
qed

lemma sum_eq_if_same_subterms:
  fixes
    i :: nat
  shows
    "∀k. i ≤ k ∧ k < j ⟶ f k = f' k ⟹ sum f {i..<j} = sum f' {i..<j}"
  by auto

lemma filter_neq_takeWhile:
  assumes
    "filter ((≠) a) l ≠ takeWhile ((≠) a) l"
  shows
    "∃i j. i < j ∧ j < length l ∧ l ! i = a ∧ l ! j ≠ a" (is ?P)
proof (rule ccontr)
  assume "~ ?P"
  then have asm: "∀i j. i < j ∧ j < length l ⟶ l ! i ≠ a ∨ l ! j = a" (is ?Q) by simp
  then have "filter ((≠) a) l = takeWhile ((≠) a) l"
  proof (cases "a : set l")
    case False
    then have "∀i. i < length l ⟶ l ! i ≠ a" by auto
    then show ?thesis 
      by (metis (mono_tags, lifting) False filter_True takeWhile_eq_all_conv)
  next
    case True
    then have ex_j: "∃j. j < length l ∧ l ! j = a" 
      by (simp add: in_set_conv_nth)
    let ?j = "Min {j. j < length l ∧ l ! j = a}"
    have fin_j: "finite {j. j < length l ∧ l ! j = a}" 
      using finite_nat_set_iff_bounded by blast
    moreover have "{j. j < length l ∧ l ! j = a} ≠ empty" using ex_j by blast
    ultimately have "?j < length l" 
      using Min_less_iff by blast
    have tail_all_a: "∀j. j < length l ∧ j ≥ ?j ⟶ l ! j = a"
    proof (rule allI, rule impI)
      fix j
      assume "j < length l ∧ j ≥ ?j"
      moreover have "⟦ ?Q; j < length l ∧ j ≥ ?j ⟧ ⟹ ∀k. k ≥ ?j ∧ k ≤ j ⟶ l ! j = a"
      proof (induct "j - ?j")
        case 0
        then have "j = ?j" using 0 by simp
        then show ?case 
          using Min_in ‹{j. j < length l ∧ l ! j = a} ≠ {}› fin_j by blast
      next
        case (Suc n)
        then have "∀k. k ≥ ?j ∧ k < j ⟶ l ! j = a" 
          by (metis (mono_tags, lifting) Min_in ‹{j. j < length l ∧ l ! j = a} ≠ {}› fin_j le_eq_less_or_eq mem_Collect_eq)
        then show ?case 
          using Suc.hyps(2) by auto
      qed
      ultimately show "l ! j = a" using asm by blast
    qed
    moreover have head_all_not_a: "∀i. i < ?j ⟶ l ! i ≠ a" using asm calculation 
      by (metis (mono_tags, lifting) Min_le ‹Min {j. j < length l ∧ l ! j = a} < length l› fin_j leD less_trans mem_Collect_eq)
    ultimately have "takeWhile ((≠) a) l = take ?j l"
    proof -
      have "length (takeWhile ((≠) a) l) = ?j" 
      proof -
        have "length (takeWhile ((≠) a) l) ≤ ?j" (is ?S)
        proof (rule ccontr)
          assume "¬ ?S"
          then have "l ! ?j ≠ a" 
            by (metis (mono_tags, lifting) not_le_imp_less nth_mem set_takeWhileD takeWhile_nth)
          then show False 
            using ‹Min {j. j < length l ∧ l ! j = a} < length l› tail_all_a by blast
        qed
        moreover have "length (takeWhile ((≠) a) l) ≥ ?j" (is ?T)
        proof (rule ccontr)
          assume "¬ ?T"
          then have "∃j. j < ?j ∧ l ! j = a" 
            by (metis (mono_tags, lifting) ‹Min {j. j < length l ∧ l ! j = a} < length l› calculation le_less_trans not_le_imp_less nth_length_takeWhile)
          then show False 
            using head_all_not_a by blast
        qed
        ultimately show ?thesis by simp
      qed
      moreover have "length (take ?j l) = ?j" 
        by (metis calculation takeWhile_eq_take)
      ultimately show ?thesis 
        by (metis takeWhile_eq_take)

    qed
    moreover have "filter ((≠) a) l = take ?j l"
    proof -
      have "filter ((≠) a) l = filter ((≠) a) (take ?j l) @ filter ((≠) a) (drop ?j l)" 
        by (metis append_take_drop_id filter_append)
      moreover have "filter ((≠) a) (take ?j l) = take ?j l" using head_all_not_a 
        by (metis ‹takeWhile ((≠) a) l = take (Min {j. j < length l ∧ l ! j = a}) l› filter_id_conv set_takeWhileD)
      moreover have "filter ((≠) a) (drop ?j l) = []"
      proof -
        have "∀j. j ≥ ?j ∧ j < length l ⟶ l ! j = drop ?j l ! (j - ?j)" 
          by simp
        then have "∀j. j < length l - ?j ⟶ drop ?j l ! j = a" using tail_all_a 
          by (metis (no_types, lifting) Groups.add_ac(2) ‹Min {j. j < length l ∧ l ! j = a} < length l› less_diff_conv less_imp_le_nat not_add_less2 not_le nth_drop)
        then show ?thesis
        proof -
          obtain aa :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a" where
            "∀x0 x1. (∃v2. v2 ∈ set x1 ∧ x0 v2) = (aa x0 x1 ∈ set x1 ∧ x0 (aa x0 x1))"
            by moura
          then have f1: "∀as p. aa p as ∈ set as ∧ p (aa p as) ∨ filter p as = []"
            by (metis (full_types) filter_False)
          obtain nn :: "'a list ⇒ 'a ⇒ nat" where
            f2: "∀x0 x1. (∃v2<length x0. x0 ! v2 = x1) = (nn x0 x1 < length x0 ∧ x0 ! nn x0 x1 = x1)"
            by moura
          { assume "drop (Min {n. n < length l ∧ l ! n = a}) l ! nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) = a"
            then have "filter ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l) = [] ∨ ¬ nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) < length (drop (Min {n. n < length l ∧ l ! n = a}) l) ∨ drop (Min {n. n < length l ∧ l ! n = a}) l ! nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) ≠ aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)"
              using f1 by (metis (full_types)) }
          moreover
          { assume "¬ nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) < length l - Min {n. n < length l ∧ l ! n = a}"
            then have "¬ nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) < length (drop (Min {n. n < length l ∧ l ! n = a}) l) ∨ drop (Min {n. n < length l ∧ l ! n = a}) l ! nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) ≠ aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)"
              by simp }
          ultimately have "filter ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l) = [] ∨ ¬ nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) < length (drop (Min {n. n < length l ∧ l ! n = a}) l) ∨ drop (Min {n. n < length l ∧ l ! n = a}) l ! nn (drop (Min {n. n < length l ∧ l ! n = a}) l) (aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)) ≠ aa ((≠) a) (drop (Min {n. n < length l ∧ l ! n = a}) l)"
            using ‹∀j<length l - Min {j. j < length l ∧ l ! j = a}. drop (Min {j. j < length l ∧ l ! j = a}) l ! j = a› by blast
          then show ?thesis
            using f2 f1 by (meson in_set_conv_nth)
        qed
      qed
      ultimately show ?thesis by simp
    qed
    ultimately show ?thesis by simp
  qed
  then show False using assms by simp
qed

lemma util_exactly_one_element:
  assumes
    "m ∉ set l" and
    "l' = l @ [m]"
  shows
    "∃!j. j < length l' ∧ l' ! j = m" (is ?P)
proof -
  have "∀j. j < length l' - 1 ⟶ l' ! j ≠ m" 
    by (metis assms(1) assms(2) butlast_snoc length_butlast nth_append nth_mem)
  then have one_j: "∀j. j < length l' ∧ l' ! j = m ⟶ j = (length l' - 1)"
    by (metis (no_types, opaque_lifting) diff_Suc_1 lessE)
  show ?thesis
  proof (rule ccontr)
    assume "~ ?P"
    then obtain i j where "i ≠ j" "i < length l'" "j < length l'"
                          "l' ! i = m" "l' ! j = m"
      using assms by auto
    then show False using one_j by blast
  qed
qed

lemma exists_one_iff_filter_one:
  shows
    "(∃!j. j < length l ∧ l ! j = a) ⟷ length (filter ((=) a) l) = 1"
proof (rule iffI)
  assume "∃!j. j < length l ∧ l ! j = a"
  then obtain j where "j < length l" "l ! j = a"
    by blast
  moreover have "∀k. k ≠ j ∧ k < length l ⟶ l ! k ≠ a" 
    using ‹∃!j. j < length l ∧ l ! j = a› ‹j < length l› ‹l ! j = a› by blast
  moreover have "l = take j l @ [l ! j] @ drop (j+1) l" 
    by (metis Cons_eq_appendI Cons_nth_drop_Suc Suc_eq_plus1 append_self_conv2 append_take_drop_id calculation(1) calculation(2))
  moreover have "filter ((=) a) (take j l) = []"
  proof -
    have "∀k. k < length (take j l) ⟶ (take j l) ! k ≠ a" 
      using calculation(3) by auto
    then show ?thesis 
      by (metis (full_types) filter_False in_set_conv_nth)
  qed
  moreover have "filter ((=) a) (drop (j+1) l) = []"
  proof -
    have "∀k. k < length (drop (j+1) l) ⟶ (drop (j+1) l) ! k ≠ a" 
      using calculation(3) by auto
    then show ?thesis
      by (metis (full_types) filter_False in_set_conv_nth)
  qed
  ultimately show "length (filter ((=) a) l) = 1" 
    by (metis (mono_tags, lifting) One_nat_def Suc_eq_plus1 append_Cons append_self_conv2 filter.simps(2) filter_append list.size(3) list.size(4))
next
  assume asm: "length (filter ((=) a) l) = 1"
  then have "filter ((=) a) l = [a]"
  proof -
    let ?xs = "filter ((=) a) l"
    have "length ?xs = 1"
      using asm by blast
    then show ?thesis 
      by (metis (full_types) Cons_eq_filterD One_nat_def length_0_conv length_Suc_conv)
  qed
  then have "∃j. j < length l ∧ l ! j = a" 
    by (metis (full_types) filter_False in_set_conv_nth list.discI)
  then obtain j where j: "j < length l" "l ! j = a" by blast
  moreover have "∀k. k < length l ∧ k ≠ j ⟶ l ! k ≠ a"
  proof (rule allI, rule impI)
    fix k
    assume assm: "k < length l ∧ k ≠ j"
    then have ‹k < length l› ..
    show "l ! k ≠ a"
    proof (rule ccontr)
      assume lka: "¬ l ! k ≠ a"
      then have ‹l ! k = a›
        by simp
      show False
      proof (cases "k < j")
        let ?xs = "take (k+1) l"
        let ?ys = "drop (k+1) l"
        case True
        then have "length (filter ((=) a) ?xs) > 0"
          using ‹k < length l› ‹l ! k = a› by (auto simp add: filter_empty_conv in_set_conv_nth)
        moreover have "length (filter ((=) a) ?ys) > 0"
        proof -
          have "?ys ! (j - (k+1)) = l ! j" 
            using True assm by auto
          moreover have "j - (k+1) < length ?ys" 
            using True ‹j < length l› by auto
          ultimately show ?thesis 
            by (metis (full_types) ‹l ! j = a› filter_empty_conv length_greater_0_conv nth_mem)
        qed
        moreover have "?xs @ ?ys = l" 
          using append_take_drop_id by blast
        ultimately have "length (filter ((=) a) l) > 1" 
          by (metis (no_types, lifting) One_nat_def Suc_eq_plus1 asm filter_append length_append less_add_eq_less less_one nat_neq_iff)
        then show False using asm by simp
      next
        let ?xs = "take (j+1) l"
        let ?ys = "drop (j+1) l"
        case False
        then have "length (filter ((=) a) ?xs) > 0" 
          using ‹k < length l› ‹l ! j = a› by (auto simp add: filter_empty_conv in_set_conv_nth)
        moreover have "length (filter ((=) a) ?ys) > 0"
        proof -
          have "?ys ! (k - (j+1)) = l ! k" 
            using False assm by auto
          moreover have "k - (j+1) < length ?ys" 
            using False assm by auto
          ultimately show ?thesis 
            by (metis (full_types) filter_empty_conv length_greater_0_conv lka nth_mem)
        qed
        moreover have "?xs @ ?ys = l" 
          using append_take_drop_id by blast
        ultimately have "length (filter ((=) a) l) > 1" 
          by (metis (no_types, lifting) One_nat_def Suc_eq_plus1 asm filter_append length_append less_add_eq_less less_one nat_neq_iff)
        then show False using asm by simp
      qed
    qed
  qed
  ultimately show "∃!j. j < length l ∧ l ! j = a" by blast
qed

end