Theory List2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

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)"
  by (simp add: remdups_fwd_acc_empty sup.absorb1)

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) 
     (simp_all add: map_eq_Cons_conv, metis append_Cons) 
  
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 "finite A"
  shows "finite {xs. set xs = A ∧ distinct xs}"
by(blast intro: rev_finite_subset[OF finite_subset_distinct[OF assms]])

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