# Theory List2

theory List2
imports Omega_Words_Fun List_Index
```(*
Author:      Salomon Sickert
*)

section ‹Auxiliary List Facts›

theory List2
imports Main "HOL-Library.Omega_Words_Fun" "List-Index.List_Index"
begin

subsection ‹remdups\_fwd›
― ‹Remove duplicates of a list in a forward moving direction›

fun remdups_fwd_acc
where
"remdups_fwd_acc Acc [] = []"
| "remdups_fwd_acc Acc (x#xs) = (if x ∈ Acc then [] else [x]) @ remdups_fwd_acc (insert x Acc) xs"

lemma remdups_fwd_acc_append[simp]:
"remdups_fwd_acc Acc (xs@ys) = (remdups_fwd_acc Acc xs) @ (remdups_fwd_acc (Acc ∪ set xs) ys)"
by (induction xs arbitrary: Acc) simp+

lemma remdups_fwd_acc_set[simp]:
"set (remdups_fwd_acc Acc xs) = set xs - Acc"
by (induction xs arbitrary: Acc) force+

lemma remdups_fwd_acc_distinct:
"distinct (remdups_fwd_acc Acc xs)"
by (induction xs arbitrary: Acc rule: rev_induct) simp+

lemma remdups_fwd_acc_empty:
"set xs ⊆ Acc ⟷ remdups_fwd_acc Acc xs = []"
by (metis remdups_fwd_acc_set set_empty Diff_eq_empty_iff Diff_eq_empty_iff)

lemma remdups_fwd_acc_drop:
"set ys ⊆ Acc ∪ set xs ⟹ remdups_fwd_acc Acc (xs @ ys @ zs) = remdups_fwd_acc Acc (xs @ zs)"

lemma remdups_fwd_acc_filter:
"remdups_fwd_acc Acc (filter P xs) = filter P (remdups_fwd_acc Acc xs)"
by (induction xs rule: rev_induct) simp+

fun remdups_fwd
where
"remdups_fwd xs = remdups_fwd_acc {} xs "

lemma remdups_fwd_eq:
"remdups_fwd xs = (rev o remdups o rev) xs"
by (induction xs rule: rev_induct) simp+

lemma remdups_fwd_set[simp]:
"set (remdups_fwd xs) = set xs"
by simp

lemma remdups_fwd_distinct:
"distinct (remdups_fwd xs)"
using remdups_fwd_acc_distinct by simp

lemma remdups_fwd_filter:
"remdups_fwd (filter P xs) = filter P (remdups_fwd xs)"
using remdups_fwd_acc_filter by simp

subsection ‹Split Lemmas›

lemma map_splitE:
assumes "map f xs = ys @ zs"
obtains us vs where "xs = us @ vs" and "map f us = ys" and "map f vs = zs"
by (insert assms; induction ys arbitrary: xs)

lemma filter_split':
"filter P xs = ys @ zs ⟹ ∃us vs. xs = us @ vs ∧ filter P us = ys ∧ filter P vs = zs"
proof (induction ys arbitrary: zs xs rule: rev_induct)
case (snoc y ys)
obtain us vs where "xs = us @ vs" and "filter P us = ys" and "filter P vs = y # zs"
using snoc(1)[OF snoc(2)[unfolded append_assoc]] by auto
moreover
then obtain vs' vs'' where "vs = vs' @ y # vs''" and "y ∉ set vs'" and "(∀u∈set vs'. ¬ P u)" and "filter P vs'' = zs" and "P y"
unfolding filter_eq_Cons_iff by blast
ultimately
have "xs = (us @ vs' @ [y]) @ vs''" and "filter P (us @ vs' @ [y]) = ys @ [y]" and "filter P (vs'') = zs"
unfolding filter_append by auto
thus ?case
by blast
qed fastforce

lemma filter_splitE:
assumes "filter P xs = ys @ zs"
obtains us vs where "xs = us @ vs" and "filter P us = ys" and "filter P vs = zs"
using filter_split'[OF assms] by blast

lemma filter_map_splitE:
assumes "filter P (map f xs) = ys @ zs"
obtains us vs where "xs = us @ vs" and "filter P (map f us) = ys" and "filter P (map f vs) = zs"
using assms by (fastforce elim: filter_splitE map_splitE)

lemma filter_map_split_iff:
"filter P (map f xs) = ys @ zs ⟷ (∃us vs. xs = us @ vs ∧ filter P (map f us) = ys ∧ filter P (map f vs) = zs)"
by (fastforce elim: filter_map_splitE)

lemma list_empty_prefix:
"xs @ y # zs = y # us ⟹ y ∉ set xs ⟹ xs = []"
by (metis hd_append2 list.sel(1) list.set_sel(1))

lemma remdups_fwd_split:
"remdups_fwd_acc Acc xs = ys @ zs ⟹ ∃us vs. xs = us @ vs ∧ remdups_fwd_acc Acc us = ys ∧ remdups_fwd_acc (Acc ∪ set ys) vs = zs"
proof (induction ys arbitrary: zs rule: rev_induct)
case (snoc y ys)
then obtain us vs where "xs = us @ vs"
and "remdups_fwd_acc Acc us = ys"
and "remdups_fwd_acc (Acc ∪ set ys) vs = y # zs"
by fastforce
moreover
hence "y ∈ set vs" and "y ∉ Acc ∪ set ys"
using remdups_fwd_acc_set[of "Acc ∪ set ys" vs] by auto
moreover
then obtain vs' vs'' where "vs = vs' @ y # vs''" and "y ∉ set vs'"
using split_list_first by metis
moreover
hence "remdups_fwd_acc (Acc ∪ set ys) vs' = []"
using ‹remdups_fwd_acc (Acc ∪ set ys) vs = y # zs› ‹y ∉ Acc ∪ set ys›
by (force intro: list_empty_prefix)
ultimately
have "xs = (us @ vs' @ [y]) @ vs''"
and "remdups_fwd_acc Acc (us @ vs' @ [y]) = ys @ [y]"
and "remdups_fwd_acc (Acc ∪ set (ys @ [y])) vs'' = zs"
by (auto simp add: remdups_fwd_acc_empty sup.absorb1)
thus ?case
by blast
qed force

lemma remdups_fwd_split_exact:
assumes "remdups_fwd_acc Acc xs = ys @ x # zs"
shows "∃us vs. xs = us @ x # vs ∧ x ∉ Acc ∧ x ∉ set ys ∧ remdups_fwd_acc Acc us = ys ∧ remdups_fwd_acc (Acc ∪ set ys ∪ {x}) vs = zs"
proof -
obtain us vs where "xs = us @ vs" and "remdups_fwd_acc Acc us = ys" and "remdups_fwd_acc (Acc ∪ set ys) vs = x # zs"
using assms by (blast dest: remdups_fwd_split)
moreover
hence "x ∈ set vs" and "x ∉ Acc ∪ set ys"
using remdups_fwd_acc_set[of "Acc ∪ set ys"] by (fastforce, metis (no_types) Diff_iff list.set_intros(1))
moreover
then obtain vs' vs'' where "vs = vs' @ x # vs''" and "x ∉ set vs'"
by (blast dest: split_list_first)
moreover
hence "set vs' ⊆ Acc ∪ set ys"
using ‹remdups_fwd_acc (Acc ∪ set ys) vs = x # zs› ‹x ∉ Acc ∪ set ys›
unfolding remdups_fwd_acc_empty by (fastforce intro: list_empty_prefix)
moreover
hence "remdups_fwd_acc (Acc ∪ set ys) vs' = []"
using remdups_fwd_acc_empty by blast
ultimately
have "xs = (us @ vs') @ x # vs''"
and "remdups_fwd_acc Acc (us @ vs') = ys"
and "remdups_fwd_acc (Acc ∪ set ys ∪ {x}) vs'' = zs"
by (fastforce dest: sup.absorb1)+
thus ?thesis
using ‹x ∉ Acc ∪ set ys› by blast
qed

lemma remdups_fwd_split_exactE:
assumes "remdups_fwd_acc Acc xs = ys @ x # zs"
obtains us vs where "xs = us @ x # vs" and "x ∉ set us" and "remdups_fwd_acc Acc us = ys" and "remdups_fwd_acc (Acc ∪ set ys ∪ {x}) vs = zs"
using remdups_fwd_split_exact[OF assms] by auto

lemma remdups_fwd_split_exact_iff:
"remdups_fwd_acc Acc xs = ys @ x # zs ⟷
(∃us vs. xs = us @ x # vs ∧ x ∉ Acc ∧ x ∉ set us ∧ remdups_fwd_acc Acc us = ys ∧ remdups_fwd_acc (Acc ∪ set ys ∪ {x}) vs = zs)"
using remdups_fwd_split_exact by fastforce

lemma sorted_pre:
"(⋀x y xs ys. zs = xs @ [x, y] @ ys ⟹ x ≤ y) ⟹ sorted zs"
apply (induction zs)
apply simp
by (metis append_Nil append_Cons list.exhaust sorted1 sorted2)

lemma sorted_list:
assumes "x ∈ set xs" and "y ∈ set xs"
assumes "sorted (map f xs)" and "f x < f y"
shows "∃xs' xs'' xs'''. xs = xs' @ x # xs'' @ y # xs'''"
proof -
obtain ys zs where "xs = ys @ y # zs" and "y ∉ set ys"
using assms by (blast dest: split_list_first)
moreover
hence "sorted (map f (y # zs))"
using ‹sorted (map f xs)› by (simp add: sorted_append)
hence "∀x∈set (map f (y # zs)). f y ≤ x"
by force
hence "∀x∈set (y # zs). f y ≤ f x"
by auto
have "x ∈ set ys"
apply (rule ccontr)
using ‹f x < f y› ‹x ∈ set xs› ‹∀x∈set (y # zs). f y ≤ f x› unfolding ‹xs = ys @ y # zs› set_append by auto
then obtain ys' zs' where "ys = ys' @ x # zs'"
using assms by (blast dest: split_list_first)
ultimately
show ?thesis
by auto
qed

lemma takeWhile_foo:
"x ∉ set ys ⟹ ys = takeWhile (λy. y ≠ x) (ys @ x # zs)"
by (metis (mono_tags, lifting) append_Nil2 takeWhile.simps(2) takeWhile_append2)

lemma takeWhile_split:
"x ∈ set xs ⟹ y ∈ set (takeWhile (λy. y ≠ x) xs) ⟹ ∃xs' xs'' xs'''. xs = xs' @ y # xs'' @ x # xs'''"
using split_list_first by (metis append_Cons append_assoc takeWhile_foo)

lemma takeWhile_distinct:
"distinct (xs' @ x # xs'') ⟹ y ∈ set (takeWhile (λy. y ≠ x) (xs' @ x # xs'')) ⟷ y ∈ set xs'"
by (induction xs') simp+

lemma finite_lists_length_eqE:
assumes "finite A"
shows "finite {xs. set xs = A ∧ length xs = n}"
proof -
have "{xs. set xs = A ∧ length xs = n} ⊆ {xs. set xs ⊆ A ∧ length xs = n}"
by blast
thus ?thesis
using finite_lists_length_eq[OF assms(1), of n] using finite_subset by auto
qed

lemma finite_set2:
assumes "card A = n" and "finite A"
shows "finite {xs. set xs = A ∧ distinct xs}"
proof -
have "{xs. set xs = A ∧ distinct xs} ⊆ {xs. set xs = A ∧ length xs = n}"
using assms(1) distinct_card by fastforce
thus ?thesis
by (metis (no_types, lifting) finite_lists_length_eqE[OF ‹finite A›, of n] finite_subset)
qed

lemma set_list:
assumes "finite (set ` XS)"
assumes "⋀xs. xs ∈ XS ⟹ distinct xs"
shows "finite XS"
proof -
have "XS ⊆ {xs | xs. set xs ∈ set ` XS ∧ distinct xs}"
using assms by auto
moreover
have 1: "{xs |xs. set xs ∈ set ` XS ∧ distinct xs} = ⋃{{xs | xs. set xs = A ∧ distinct xs} | A. A ∈ set ` XS}"
by auto
have "finite {xs |xs. set xs ∈ set ` XS ∧ distinct xs}"
using finite_set2[OF _ finite_set] distinct_card  assms(1) unfolding 1 by fastforce
ultimately
show ?thesis
using finite_subset by blast
qed

lemma set_foldl_append:
"set (foldl (@) i xs) = set i ∪ ⋃{set x | x. x ∈ set xs}"
by (induction xs arbitrary: i) auto

subsection ‹Short-circuited Version of @{const foldl}›

fun foldl_break :: "('b ⇒ 'a ⇒ 'b) ⇒ ('b ⇒ bool) ⇒ 'b ⇒ 'a list ⇒ 'b"
where
"foldl_break f s a [] = a"
| "foldl_break f s a (x # xs) = (if s a then a else foldl_break f s (f a x) xs)"

lemma foldl_break_append:
"foldl_break f s a (xs @ ys) = (if s (foldl_break f s a xs) then foldl_break f s a xs else (foldl_break f s (foldl_break f s a xs) ys))"
by (induction xs arbitrary: a) (cases ys, auto)

subsection ‹Suffixes›

― ‹Non empty suffixes of finite words - specialised!›

fun suffixes
where
"suffixes [] = []"
| "suffixes (x#xs) = (suffixes xs) @ [x#xs]"

lemma suffixes_append:
"suffixes (xs @ ys) = (suffixes ys) @ (map (λzs. zs @ ys) (suffixes xs))"
by (induction xs) simp_all

lemma suffixes_alt_def:
"suffixes xs = rev (prefix (length xs) (λi. drop i xs))"
proof (induction xs rule: rev_induct)
case (snoc x xs)
show ?case
by (simp add: subsequence_def suffixes_append snoc rev_map)
qed simp

end
```