# 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

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
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]"
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"
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"
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
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"
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
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"
show "l ! k ≠ a"
proof (rule ccontr)
assume lka: "¬ l ! k ≠ a"
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"
by (metis (full_types, opaque_lifting) add.commute assm discrete filter_empty_conv length_greater_0_conv length_take less_add_one lka min.absorb2 nth_mem nth_take)
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"
by (metis (full_types, opaque_lifting) add.commute j discrete filter_empty_conv length_greater_0_conv length_take less_add_one min.absorb2 nth_mem nth_take)
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
```