(* Author: Andreas Lochbihler, ETH Zürich Author: Florian Haftmann, TU Muenchen *) section ‹Less common functions on lists› theory More_List imports Main begin definition strip_while :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where "strip_while P = rev ∘ dropWhile P ∘ rev" lemma strip_while_rev [simp]: "strip_while P (rev xs) = rev (dropWhile P xs)" by (simp add: strip_while_def) lemma strip_while_Nil [simp]: "strip_while P [] = []" by (simp add: strip_while_def) lemma strip_while_append [simp]: "¬ P x ⟹ strip_while P (xs @ [x]) = xs @ [x]" by (simp add: strip_while_def) lemma strip_while_append_rec [simp]: "P x ⟹ strip_while P (xs @ [x]) = strip_while P xs" by (simp add: strip_while_def) lemma strip_while_Cons [simp]: "¬ P x ⟹ strip_while P (x # xs) = x # strip_while P xs" by (induct xs rule: rev_induct) (simp_all add: strip_while_def) lemma strip_while_eq_Nil [simp]: "strip_while P xs = [] ⟷ (∀x∈set xs. P x)" by (simp add: strip_while_def) lemma strip_while_eq_Cons_rec: "strip_while P (x # xs) = x # strip_while P xs ⟷ ¬ (P x ∧ (∀x∈set xs. P x))" by (induct xs rule: rev_induct) (simp_all add: strip_while_def) lemma split_strip_while_append: fixes xs :: "'a list" obtains ys zs :: "'a list" where "strip_while P xs = ys" and "∀x∈set zs. P x" and "xs = ys @ zs" proof (rule that) show "strip_while P xs = strip_while P xs" .. show "∀x∈set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric]) have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))" by (simp add: strip_while_def) then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))" by (simp only: rev_is_rev_conv) qed lemma strip_while_snoc [simp]: "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])" by (simp add: strip_while_def) lemma strip_while_map: "strip_while P (map f xs) = map f (strip_while (P ∘ f) xs)" by (simp add: strip_while_def rev_map dropWhile_map) lemma strip_while_dropWhile_commute: "strip_while P (dropWhile Q xs) = dropWhile Q (strip_while P xs)" proof (induct xs) case Nil then show ?case by simp next case (Cons x xs) show ?case proof (cases "∀y∈set xs. P y") case True with dropWhile_append2 [of "rev xs"] show ?thesis by (auto simp add: strip_while_def dest: set_dropWhileD) next case False then obtain y where "y ∈ set xs" and "¬ P y" by blast with Cons dropWhile_append3 [of P y "rev xs"] show ?thesis by (simp add: strip_while_def) qed qed lemma dropWhile_strip_while_commute: "dropWhile P (strip_while Q xs) = strip_while Q (dropWhile P xs)" by (simp add: strip_while_dropWhile_commute) definition no_leading :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where "no_leading P xs ⟷ (xs ≠ [] ⟶ ¬ P (hd xs))" lemma no_leading_Nil [simp, intro!]: "no_leading P []" by (simp add: no_leading_def) lemma no_leading_Cons [simp, intro!]: "no_leading P (x # xs) ⟷ ¬ P x" by (simp add: no_leading_def) lemma no_leading_append [simp]: "no_leading P (xs @ ys) ⟷ no_leading P xs ∧ (xs = [] ⟶ no_leading P ys)" by (induct xs) simp_all lemma no_leading_dropWhile [simp]: "no_leading P (dropWhile P xs)" by (induct xs) simp_all lemma dropWhile_eq_obtain_leading: assumes "dropWhile P xs = ys" obtains zs where "xs = zs @ ys" and "⋀z. z ∈ set zs ⟹ P z" and "no_leading P ys" proof - from assms have "∃zs. xs = zs @ ys ∧ (∀z ∈ set zs. P z) ∧ no_leading P ys" proof (induct xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs ys) show ?case proof (cases "P x") case True with Cons.hyps [of ys] Cons.prems have "∃zs. xs = zs @ ys ∧ (∀a∈set zs. P a) ∧ no_leading P ys" by simp then obtain zs where "xs = zs @ ys" and "⋀z. z ∈ set zs ⟹ P z" and *: "no_leading P ys" by blast with True have "x # xs = (x # zs) @ ys" and "⋀z. z ∈ set (x # zs) ⟹ P z" by auto with * show ?thesis by blast next case False with Cons show ?thesis by (cases ys) simp_all qed qed with that show thesis by blast qed lemma dropWhile_idem_iff: "dropWhile P xs = xs ⟷ no_leading P xs" by (cases xs) (auto elim: dropWhile_eq_obtain_leading) abbreviation no_trailing :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where "no_trailing P xs ≡ no_leading P (rev xs)" lemma no_trailing_unfold: "no_trailing P xs ⟷ (xs ≠ [] ⟶ ¬ P (last xs))" by (induct xs) simp_all lemma no_trailing_Nil [simp, intro!]: "no_trailing P []" by simp lemma no_trailing_Cons [simp]: "no_trailing P (x # xs) ⟷ no_trailing P xs ∧ (xs = [] ⟶ ¬ P x)" by simp lemma no_trailing_append: "no_trailing P (xs @ ys) ⟷ no_trailing P ys ∧ (ys = [] ⟶ no_trailing P xs)" by (induct xs) simp_all lemma no_trailing_append_Cons [simp]: "no_trailing P (xs @ y # ys) ⟷ no_trailing P (y # ys)" by simp lemma no_trailing_strip_while [simp]: "no_trailing P (strip_while P xs)" by (induct xs rule: rev_induct) simp_all lemma strip_while_idem [simp]: "no_trailing P xs ⟹ strip_while P xs = xs" by (cases xs rule: rev_cases) simp_all lemma strip_while_eq_obtain_trailing: assumes "strip_while P xs = ys" obtains zs where "xs = ys @ zs" and "⋀z. z ∈ set zs ⟹ P z" and "no_trailing P ys" proof - from assms have "rev (rev (dropWhile P (rev xs))) = rev ys" by (simp add: strip_while_def) then have "dropWhile P (rev xs) = rev ys" by simp then obtain zs where A: "rev xs = zs @ rev ys" and B: "⋀z. z ∈ set zs ⟹ P z" and C: "no_trailing P ys" using dropWhile_eq_obtain_leading by blast from A have "rev (rev xs) = rev (zs @ rev ys)" by simp then have "xs = ys @ rev zs" by simp moreover from B have "⋀z. z ∈ set (rev zs) ⟹ P z" by simp ultimately show thesis using that C by blast qed lemma strip_while_idem_iff: "strip_while P xs = xs ⟷ no_trailing P xs" proof - define ys where "ys = rev xs" moreover have "strip_while P (rev ys) = rev ys ⟷ no_trailing P (rev ys)" by (simp add: dropWhile_idem_iff) ultimately show ?thesis by simp qed lemma no_trailing_map: "no_trailing P (map f xs) ⟷ no_trailing (P ∘ f) xs" by (simp add: last_map no_trailing_unfold) lemma no_trailing_drop [simp]: "no_trailing P (drop n xs)" if "no_trailing P xs" proof - from that have "no_trailing P (take n xs @ drop n xs)" by simp then show ?thesis by (simp only: no_trailing_append) qed lemma no_trailing_upt [simp]: "no_trailing P [n..<m] ⟷ (n < m ⟶ ¬ P (m - 1))" by (auto simp add: no_trailing_unfold) definition nth_default :: "'a ⇒ 'a list ⇒ nat ⇒ 'a" where "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)" lemma nth_default_nth: "n < length xs ⟹ nth_default dflt xs n = xs ! n" by (simp add: nth_default_def) lemma nth_default_beyond: "length xs ≤ n ⟹ nth_default dflt xs n = dflt" by (simp add: nth_default_def) lemma nth_default_Nil [simp]: "nth_default dflt [] n = dflt" by (simp add: nth_default_def) lemma nth_default_Cons: "nth_default dflt (x # xs) n = (case n of 0 ⇒ x | Suc n' ⇒ nth_default dflt xs n')" by (simp add: nth_default_def split: nat.split) lemma nth_default_Cons_0 [simp]: "nth_default dflt (x # xs) 0 = x" by (simp add: nth_default_Cons) lemma nth_default_Cons_Suc [simp]: "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n" by (simp add: nth_default_Cons) lemma nth_default_replicate_dflt [simp]: "nth_default dflt (replicate n dflt) m = dflt" by (simp add: nth_default_def) lemma nth_default_append: "nth_default dflt (xs @ ys) n = (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))" by (auto simp add: nth_default_def nth_append) lemma nth_default_append_trailing [simp]: "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs" by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def) lemma nth_default_snoc_default [simp]: "nth_default dflt (xs @ [dflt]) = nth_default dflt xs" by (auto simp add: nth_default_def fun_eq_iff nth_append) lemma nth_default_eq_dflt_iff: "nth_default dflt xs k = dflt ⟷ (k < length xs ⟶ xs ! k = dflt)" by (simp add: nth_default_def) lemma in_enumerate_iff_nth_default_eq: "x ≠ dflt ⟹ (n, x) ∈ set (enumerate 0 xs) ⟷ nth_default dflt xs n = x" by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip) lemma last_conv_nth_default: assumes "xs ≠ []" shows "last xs = nth_default dflt xs (length xs - 1)" using assms by (simp add: nth_default_def last_conv_nth) lemma nth_default_map_eq: "f dflt' = dflt ⟹ nth_default dflt (map f xs) n = f (nth_default dflt' xs n)" by (simp add: nth_default_def) lemma finite_nth_default_neq_default [simp]: "finite {k. nth_default dflt xs k ≠ dflt}" by (simp add: nth_default_def) lemma sorted_list_of_set_nth_default: "sorted_list_of_set {k. nth_default dflt xs k ≠ dflt} = map fst (filter (λ(_, x). x ≠ dflt) (enumerate 0 xs))" by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI) lemma map_nth_default: "map (nth_default x xs) [0..<length xs] = xs" proof - have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]" by (rule map_cong) (simp_all add: nth_default_nth) show ?thesis by (simp add: * map_nth) qed lemma range_nth_default [simp]: "range (nth_default dflt xs) = insert dflt (set xs)" by (auto simp add: nth_default_def [abs_def] in_set_conv_nth) lemma nth_strip_while: assumes "n < length (strip_while P xs)" shows "strip_while P xs ! n = xs ! n" proof - have "length (dropWhile P (rev xs)) + length (takeWhile P (rev xs)) = length xs" by (subst add.commute) (simp add: arg_cong [where f=length, OF takeWhile_dropWhile_id, unfolded length_append]) then show ?thesis using assms by (simp add: strip_while_def rev_nth dropWhile_nth) qed lemma length_strip_while_le: "length (strip_while P xs) ≤ length xs" unfolding strip_while_def o_def length_rev by (subst (2) length_rev[symmetric]) (simp add: strip_while_def length_dropWhile_le del: length_rev) lemma nth_default_strip_while_dflt [simp]: "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs" by (induct xs rule: rev_induct) auto lemma nth_default_eq_iff: "nth_default dflt xs = nth_default dflt ys ⟷ strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P ⟷ ?Q") proof let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys" assume ?P then have eq: "nth_default dflt ?xs = nth_default dflt ?ys" by simp have len: "length ?xs = length ?ys" proof (rule ccontr) assume len: "length ?xs ≠ length ?ys" { fix xs ys :: "'a list" let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys" assume eq: "nth_default dflt ?xs = nth_default dflt ?ys" assume len: "length ?xs < length ?ys" then have "length ?ys > 0" by arith then have "?ys ≠ []" by simp with last_conv_nth_default [of ?ys dflt] have "last ?ys = nth_default dflt ?ys (length ?ys - 1)" by auto moreover from ‹?ys ≠ []› no_trailing_strip_while [of "HOL.eq dflt" ys] have "last ?ys ≠ dflt" by (simp add: no_trailing_unfold) ultimately have "nth_default dflt ?xs (length ?ys - 1) ≠ dflt" using eq by simp moreover from len have "length ?ys - 1 ≥ length ?xs" by simp ultimately have False by (simp only: nth_default_beyond) simp } from this [of xs ys] this [of ys xs] len eq show False by (auto simp only: linorder_class.neq_iff) qed then show ?Q proof (rule nth_equalityI [rule_format]) fix n assume n: "n < length ?xs" with len have "n < length ?ys" by simp with n have xs: "nth_default dflt ?xs n = ?xs ! n" and ys: "nth_default dflt ?ys n = ?ys ! n" by (simp_all only: nth_default_nth) with eq show "?xs ! n = ?ys ! n" by simp qed next assume ?Q then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)" by simp then show ?P by simp qed end