(* 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 "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