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 "(uset 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 "xset (map f (y # zs)). f y  x"
    by force
  hence "xset (y # zs). f y  f x"
    by auto
  have "x  set ys"
    apply (rule ccontr)
    using f x < f y x  set xs xset (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