# Theory ListUtils

```theory ListUtils
imports Main "HOL-Library.Sublist"
begin

― ‹TODO assure translations
* 'sublist' --> 'subseq'
* list\_frag l l' --> sublist l' l (switch operands!)›

lemma len_ge_0:
fixes l
shows "length l ≥ 0"
by simp

lemma len_gt_pref_is_pref:
fixes l l1 l2
assumes "(length l2 > length l1)" "(prefix l1 l)" "(prefix l2 l)"
shows "(prefix l1 l2)"
using assms proof (induction l2 arbitrary: l1 l)
case Nil
then have "¬(length [] > length l1)"
by simp
then show ?case
using Nil
by blast
next
case (Cons a l2)
then show ?case proof(induction l1 arbitrary: l)
case Nil
then show ?case
using Nil_prefix
by blast
next
case (Cons b l1)
then show ?case proof(cases l)
case Nil
then have "¬(prefix (a # l2) l)"
by simp
then show ?thesis using Cons.prems(4)
by simp
next
case (Cons c l)
then have 1: "length l2 > length l1"
using Cons.prems(2)
by fastforce
then show ?thesis using Cons proof(cases l)
case Nil
then have "l1 = [c]" "l2 = [c]"
using Cons.prems(3, 4) local.Cons 1
by fastforce+
then show ?thesis
using 1
by auto
next
case (Cons d l')
{
thm len_ge_0
have "length l1 ≥ 0"
by simp
then have "length l2 > 0"
using 1
by force
then have "l2 ≠ []" using 1
by blast
}
then have "length (a # l1) ≤ length (b # l2)"
using 1 le_eq_less_or_eq
by simp
then show ?thesis
using Cons.prems(3, 4) prefix_length_prefix
by fastforce
qed
qed
qed
qed

fixes l1 l2 l3
assumes "l2 ≠ []"
shows "length (l1 @ l3) < length (l1 @ l2 @l3)"
using assms
by (induction l2) auto

lemma append_filter:
fixes f1 :: "'a ⇒ bool" and f2 as1 as2 and p :: "'a list"
assumes "(as1 @ as2 = filter f1 (map f2 p))"
shows "(∃p_1 p_2.
(p_1 @ p_2 = p)
∧ (as1 = filter f1 (map f2 p_1))
∧ (as2 = filter f1 (map f2 p_2))
)"
using assms
proof (induction p arbitrary: f1 f2 as1 as2)
case Nil
from Nil have 1: "as1 @ as2 = []"
by force
then have 2: "as1 = []" "as2 = []"
by blast+
let ?p1="[]"
let ?p2="[]"
from 1 2
have "?p1 @ ?p2 = []" "as1 = (filter f1 (map f2 ?p1))" "as2 = (filter f1 (map f2 ?p2))"
subgoal by blast
subgoal using 2(1) by simp
subgoal using 2(2) by simp
done
then show ?case
by fast
next
case cons: (Cons a p)
then show ?case
proof (cases "as1")
case Nil
from cons.prems Nil
have 1: "as2 = filter f1 (map f2 (a # p))"
by simp
let ?p1="[]"
let ?p2="a # p"
have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)"
subgoal by simp
subgoal using Nil by simp
subgoal using 1 by auto
done
then show ?thesis
by blast
next
case (Cons a' p')
then show ?thesis
proof (cases "¬f1 (f2 a)")
case True
hence "filter f1 (map f2 (a # p)) = filter f1 (map f2 p)"
by fastforce
hence "as1 @ as2 = filter f1 (map f2 p)"
using cons.prems
by argo
then obtain p1 p2 where a:
"p1 @ p2 = p" "as1 = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)"
using cons.IH
by meson
let ?p1="a # p1"
let ?p2="p2"
have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)"
subgoal using a(1) by fastforce
subgoal using True a(2) by auto
subgoal using a(3) by blast
done
then show ?thesis
by blast
next
case False
hence "filter f1 (map f2 (a # p)) = f2 a # filter f1 (map f2 p)"
by fastforce
then have 1: "a' = f2 a" "p' @ as2 = filter f1 (map f2 p)" "as1 = a' # p'"
using cons.prems Cons
by fastforce+
then obtain p1 p2 where 2:
"p1 @ p2 = p" "p' = filter f1 (map f2 p1)" "as2 = filter f1 (map f2 p2)"
using cons.IH
by meson
let ?p1="a # p1"
let ?p2="p2"
have "?p1 @ ?p2 = a # p" "as1 = filter f1 (map f2 ?p1)" "as2 = filter f1 (map f2 ?p2)"
subgoal using 2(1) by simp
subgoal using False 1(1, 3) 2(2) by force
subgoal using 2(3) by blast
done
then show ?thesis
by blast
qed
qed
qed

― ‹NOTE types of `f1` and `p` had to be fixed for `append\_eq\_as\_proj\_1`.›
lemma append_eq_as_proj_1:
fixes f1 :: "'a ⇒ bool" and f2 as1 as2 as3 and p :: "'a list"
assumes "(as1 @ as2 @ as3 = filter f1 (map f2  p))"
shows "(∃p_1 p_2 p_3.
(p_1 @ p_2 @ p_3 = p)
∧ (as1 = filter f1 (map f2 p_1))
∧ (as2 = filter f1 (map f2 p_2))
∧ (as3 = filter f1 (map f2 p_3))
)"
proof -
from assms
obtain p_1 p_2 where 1: "(p_1 @ p_2 = p)" "(as1 = filter f1 (map f2 p_1))"
"(as2 @ as3 = filter f1 (map f2 p_2))"
using append_filter[of as1 "(as2 @ as3)"]
by meson
moreover from 1
obtain p_a p_b where "(p_a @ p_b = p_2)" "(as2 = filter f1 (map f2 p_a))"
"(as3 = filter f1 (map f2 p_b))"
using append_filter[where p=p_2]
by meson
ultimately show ?thesis
by blast
qed

lemma filter_empty_every_not: "⋀P l. (filter (λx. P x) l = []) = list_all (λx. ¬P x) l"
proof -
fix P l
show "(filter (λx. P x) l = []) = list_all (λx. ¬P x) l"
apply(induction l)
apply(auto)
done
qed

lemma MEM_SPLIT:
fixes x l
assumes "¬ListMem x l"
shows "∀l1 l2. l ≠ l1 @ [x] @ l2"
proof -
{
assume C: "¬(∀l1 l2. l ≠ l1 @ [x] @ l2)"
then have "∃l1 l2. l = l1 @ [x] @ l2"
by blast
then obtain l1 l2 where 1: "l = l1 @ [x] @ l2"
by blast
from assms
have 2: "(∀xs. l ≠ x # xs) ∧ (∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)"
using ListMem_iff
by fastforce
then have False
proof (cases l1)
case Nil
let ?xs="l2"
from 1 Nil have "l = [x] @ ?xs"
by blast
then show ?thesis
using 2
by simp
next
case (Cons a list)
{
let ?y="a"
let ?xs="list @ [x] @ l2"
from 1 Cons have "l = ?y # ?xs"
by simp
moreover have "ListMem x ?xs"
ultimately have "∃xs. ∃y. l = y # xs ∧ ListMem x xs"
by blast
then have "¬(∀xs. (∀y. l ≠ y # xs) ∨ ¬ ListMem x xs)"
by presburger
}
then show ?thesis
using 2
by auto
qed
}
then show ?thesis
by blast
qed

lemma APPEND_EQ_APPEND_MID:
fixes l1 l2 m1 m2 e
shows
"(l1 @ [e] @ l2 = m1 @ m2)
⟷
(∃l. (m1 = l1 @ [e] @ l) ∧ (l2 = l @ m2)) ∨
(∃l. (l1 = m1 @ l) ∧ (m2 = l @ [e] @ l2))"
proof (induction "l1" arbitrary: m1)
case Nil
then show ?case
by (simp; metis Cons_eq_append_conv)+
next
case (Cons a l1)
then show ?case
by (cases m1; simp; blast)
qed

― ‹NOTE variable `P` was removed (redundant).›
lemma LIST_FRAG_DICHOTOMY:
fixes l la x lb
assumes "sublist l (la @ [x] @ lb)" "¬ListMem x l"
shows "sublist l la ∨ sublist l lb"
proof -
{
from assms(1)
obtain pfx sfx where 1: "pfx @ l @ sfx = la @ [x] @ lb"
unfolding sublist_def
by force
from assms(2)
have 2: "∀l1 l2. l ≠ l1 @ [x] @ l2"
using MEM_SPLIT[OF assms(2)]
by blast
from 1
consider (a) "(∃lc. pfx = la @ [x] @ lc ∧ lb = lc @ l @ sfx)"
| (b) "(∃lc. la = pfx @ lc ∧ l @ sfx = lc @ [x] @ lb)"
using APPEND_EQ_APPEND_MID[of la x lb pfx "l @ sfx"]
by presburger
then have "∃pfx' sfx. (pfx' @ l @ sfx = la) ∨ (pfx'@  l @ sfx = lb)"
proof (cases)
case a
― ‹NOTE `lc` is `l'` in original proof.›
then obtain lc where a: "pfx = la @ [x] @ lc" "lb = lc @ l @ sfx"
by blast
then show ?thesis
by blast
next
case b
then obtain lc where i: "la = pfx @ lc" "l @ sfx = lc @ [x] @ lb"
by blast
then show ?thesis
using 2
by (metis APPEND_EQ_APPEND_MID)
qed
}
then show ?thesis
unfolding sublist_def
by blast
qed

lemma LIST_FRAG_DICHOTOMY_2:
fixes l la x lb P
assumes "sublist l (la @ [x] @ lb) " "¬P x" "list_all P l"
shows "sublist l la ∨ sublist l lb"
proof -
{
assume "¬P x" "list_all P l"
then have "¬ListMem x l"
proof (induction l arbitrary: x P)
case Nil
then show ?case
using ListMem_iff
by force
next
case (Cons a l)
{
have "list_all P l"
using Cons.prems(2)
by simp
then have "¬ListMem x l"
using Cons.prems(1) Cons.IH
by blast
}
moreover {
have "P a"
using Cons.prems(2)
by simp
then  have "a ≠ x"
using Cons.prems(1)
by meson
}
ultimately show ?case
using Cons.prems(1, 2) ListMem_iff list.pred_set
by metis
qed
}
then have "¬ListMem x l"
using assms(2, 3)
by fast
then show ?thesis
using assms(1) LIST_FRAG_DICHOTOMY
by metis
qed

lemma frag_len_filter_le:
fixes P l' l
assumes "sublist l' l"
shows "length (filter P l') ≤ length (filter P l)"
proof -
obtain ps ss where "l = ps @ l' @ ss"
using assms sublist_def
by blast
then have 1:
"length (filter P l) = length (filter P ps) + length (filter P l') + length (filter P ss)"
by force
then have "length (filter P ps) ≥ 0" "length (filter P ss) ≥ 0"
by blast+
then show ?thesis
using 1
by linarith
qed

end```