(* Author: Tobias Nipkow, with contributions from Dmitriy Traytel, Lukas Bulwahn, and Peter Lammich *) section ‹Index-based manipulation of lists› theory List_Index imports Main begin text ‹\noindent This theory collects functions for index-based manipulation of lists. › subsection ‹Finding an index› text ‹ This subsection defines three functions for finding the index of items in a list: \begin{description} \item[‹find_index P xs›] finds the index of the first element in ‹xs› that satisfies ‹P›. \item[‹index xs x›] finds the index of the first occurrence of ‹x› in ‹xs›. \item[‹last_index xs x›] finds the index of the last occurrence of ‹x› in ‹xs›. \end{description} All functions return @{term "length xs"} if ‹xs› does not contain a suitable element. The argument order of ‹find_index› follows the function of the same name in the Haskell standard library. For ‹index› (and ‹last_index›) the order is intentionally reversed: ‹index› maps lists to a mapping from elements to their indices, almost the inverse of function ‹nth›.› primrec find_index :: "('a ⇒ bool) ⇒ 'a list ⇒ nat" where "find_index _ [] = 0" | "find_index P (x#xs) = (if P x then 0 else find_index P xs + 1)" definition index :: "'a list ⇒ 'a ⇒ nat" where "index xs = (λa. find_index (λx. x=a) xs)" definition last_index :: "'a list ⇒ 'a ⇒ nat" where "last_index xs x = (let i = index (rev xs) x; n = size xs in if i = n then i else n - (i+1))" lemma find_index_append: "find_index P (xs @ ys) = (if ∃x∈set xs. P x then find_index P xs else size xs + find_index P ys)" by (induct xs) simp_all lemma find_index_le_size: "find_index P xs <= size xs" by(induct xs) simp_all lemma index_le_size: "index xs x <= size xs" by(simp add: index_def find_index_le_size) lemma last_index_le_size: "last_index xs x <= size xs" by(simp add: last_index_def Let_def index_le_size) lemma index_Nil[simp]: "index [] a = 0" by(simp add: index_def) lemma index_Cons[simp]: "index (x#xs) a = (if x=a then 0 else index xs a + 1)" by(simp add: index_def) lemma index_append: "index (xs @ ys) x = (if x : set xs then index xs x else size xs + index ys x)" by (induct xs) simp_all lemma index_conv_size_if_notin[simp]: "x ∉ set xs ⟹ index xs x = size xs" by (induct xs) auto lemma find_index_eq_size_conv: "size xs = n ⟹ (find_index P xs = n) = (∀x ∈ set xs. ~ P x)" by(induct xs arbitrary: n) auto lemma size_eq_find_index_conv: "size xs = n ⟹ (n = find_index P xs) = (∀x ∈ set xs. ~ P x)" by(metis find_index_eq_size_conv) lemma index_size_conv: "size xs = n ⟹ (index xs x = n) = (x ∉ set xs)" by(auto simp: index_def find_index_eq_size_conv) lemma size_index_conv: "size xs = n ⟹ (n = index xs x) = (x ∉ set xs)" by (metis index_size_conv) lemma last_index_size_conv: "size xs = n ⟹ (last_index xs x = n) = (x ∉ set xs)" apply(auto simp: last_index_def index_size_conv) apply(drule length_pos_if_in_set) apply arith done lemma size_last_index_conv: "size xs = n ⟹ (n = last_index xs x) = (x ∉ set xs)" by (metis last_index_size_conv) lemma find_index_less_size_conv: "(find_index P xs < size xs) = (∃x ∈ set xs. P x)" by (induct xs) auto lemma index_less_size_conv: "(index xs x < size xs) = (x ∈ set xs)" by(auto simp: index_def find_index_less_size_conv) lemma last_index_less_size_conv: "(last_index xs x < size xs) = (x : set xs)" by(simp add: last_index_def Let_def index_size_conv length_pos_if_in_set del:length_greater_0_conv) lemma index_less[simp]: "x : set xs ⟹ size xs <= n ⟹ index xs x < n" apply(induct xs) apply auto apply (metis index_less_size_conv less_eq_Suc_le less_trans_Suc) done lemma last_index_less[simp]: "x : set xs ⟹ size xs <= n ⟹ last_index xs x < n" by(simp add: last_index_less_size_conv[symmetric]) lemma last_index_Cons: "last_index (x#xs) y = (if x=y then if x ∈ set xs then last_index xs y + 1 else 0 else last_index xs y + 1)" using index_le_size[of "rev xs" y] apply(auto simp add: last_index_def index_append Let_def) apply(simp add: index_size_conv) done lemma last_index_append: "last_index (xs @ ys) x = (if x : set ys then size xs + last_index ys x else if x : set xs then last_index xs x else size xs + size ys)" by (induct xs) (simp_all add: last_index_Cons last_index_size_conv) lemma last_index_Snoc[simp]: "last_index (xs @ [x]) y = (if x=y then size xs else if y : set xs then last_index xs y else size xs + 1)" by(simp add: last_index_append last_index_Cons) lemma nth_find_index: "find_index P xs < size xs ⟹ P(xs ! find_index P xs)" by (induct xs) auto lemma nth_index[simp]: "x ∈ set xs ⟹ xs ! index xs x = x" by (induct xs) auto lemma nth_last_index[simp]: "x ∈ set xs ⟹ xs ! last_index xs x = x" by(simp add:last_index_def index_size_conv Let_def rev_nth[symmetric]) lemma index_rev: "⟦ distinct xs; x ∈ set xs ⟧ ⟹ index (rev xs) x = length xs - index xs x - 1" by (induct xs) (auto simp: index_append) lemma index_nth_id: "⟦ distinct xs; n < length xs ⟧ ⟹ index xs (xs ! n) = n" by (metis in_set_conv_nth index_less_size_conv nth_eq_iff_index_eq nth_index) lemma index_upt[simp]: "m ≤ i ⟹ i < n ⟹ index [m..<n] i = i-m" by (induction n) (auto simp add: index_append) lemma index_eq_index_conv[simp]: "x ∈ set xs ∨ y ∈ set xs ⟹ (index xs x = index xs y) = (x = y)" by (induct xs) auto lemma last_index_eq_index_conv[simp]: "x ∈ set xs ∨ y ∈ set xs ⟹ (last_index xs x = last_index xs y) = (x = y)" by (induct xs) (auto simp:last_index_Cons) lemma inj_on_index: "inj_on (index xs) (set xs)" by (simp add:inj_on_def) lemma inj_on_index2: "I ⊆ set xs ⟹ inj_on (index xs) I" by (rule inj_onI) auto lemma inj_on_last_index: "inj_on (last_index xs) (set xs)" by (simp add:inj_on_def) lemma find_index_conv_takeWhile: "find_index P xs = size(takeWhile (Not o P) xs)" by(induct xs) auto lemma index_conv_takeWhile: "index xs x = size(takeWhile (λy. x≠y) xs)" by(induct xs) auto lemma find_index_first: "i < find_index P xs ⟹ ¬P (xs!i)" unfolding find_index_conv_takeWhile by (metis comp_apply nth_mem set_takeWhileD takeWhile_nth) lemma index_first: "i<index xs x ⟹ x≠xs!i" using find_index_first unfolding index_def by blast lemma find_index_eqI: assumes "i≤length xs" assumes "∀j<i. ¬P (xs!j)" assumes "i<length xs ⟹ P (xs!i)" shows "find_index P xs = i" by (metis (mono_tags, lifting) antisym_conv2 assms find_index_eq_size_conv find_index_first find_index_less_size_conv linorder_neqE_nat nth_find_index) lemma find_index_eq_iff: "find_index P xs = i ⟷ (i≤length xs ∧ (∀j<i. ¬P (xs!j)) ∧ (i<length xs ⟶ P (xs!i)))" by (auto intro: find_index_eqI simp: nth_find_index find_index_le_size find_index_first) lemma index_eqI: assumes "i≤length xs" assumes "∀j<i. xs!j ≠ x" assumes "i<length xs ⟹ xs!i = x" shows "index xs x = i" unfolding index_def by (simp add: find_index_eqI assms) lemma index_eq_iff: "index xs x = i ⟷ (i≤length xs ∧ (∀j<i. xs!j ≠ x) ∧ (i<length xs ⟶ xs!i = x))" by (auto intro: index_eqI simp: index_le_size index_less_size_conv dest: index_first) lemma index_take: "index xs x >= i ⟹ x ∉ set(take i xs)" apply(subst (asm) index_conv_takeWhile) apply(subgoal_tac "set(take i xs) <= set(takeWhile ((≠) x) xs)") apply(blast dest: set_takeWhileD) apply(metis set_take_subset_set_take takeWhile_eq_take) done lemma last_index_drop: "last_index xs x < i ⟹ x ∉ set(drop i xs)" apply(subgoal_tac "set(drop i xs) = set(take (size xs - i) (rev xs))") apply(simp add: last_index_def index_take Let_def split:if_split_asm) apply (metis rev_drop set_rev) done lemma set_take_if_index: assumes "index xs x < i" and "i ≤ length xs" shows "x ∈ set (take i xs)" proof - have "index (take i xs @ drop i xs) x < i" using append_take_drop_id[of i xs] assms(1) by simp thus ?thesis using assms(2) by(simp add:index_append del:append_take_drop_id split: if_splits) qed lemma index_take_if_index: assumes "index xs x ≤ n" shows "index (take n xs) x = index xs x" proof cases assume "x : set(take n xs)" with assms show ?thesis by (metis append_take_drop_id index_append) next assume "x ∉ set(take n xs)" with assms show ?thesis by (metis order_le_less set_take_if_index le_cases length_take min_def size_index_conv take_all) qed lemma index_take_if_set: "x : set(take n xs) ⟹ index (take n xs) x = index xs x" by (metis index_take index_take_if_index linear) lemma index_last[simp]: "xs ≠ [] ⟹ distinct xs ⟹ index xs (last xs) = length xs - 1" by (induction xs) auto lemma index_update_if_diff2: "n < length xs ⟹ x ≠ xs!n ⟹ x ≠ y ⟹ index (xs[n := y]) x = index xs x" by(subst (2) id_take_nth_drop[of n xs]) (auto simp: upd_conv_take_nth_drop index_append min_def) lemma set_drop_if_index: "distinct xs ⟹ index xs x < i ⟹ x ∉ set(drop i xs)" by (metis in_set_dropD index_nth_id last_index_drop last_index_less_size_conv nth_last_index) lemma index_swap_if_distinct: assumes "distinct xs" "i < size xs" "j < size xs" shows "index (xs[i := xs!j, j := xs!i]) x = (if x = xs!i then j else if x = xs!j then i else index xs x)" proof- have "distinct(xs[i := xs!j, j := xs!i])" using assms by simp with assms show ?thesis apply (auto simp: simp del: distinct_swap) apply (metis index_nth_id list_update_same_conv) apply (metis (erased, opaque_lifting) index_nth_id length_list_update list_update_swap nth_list_update_eq) apply (metis index_nth_id length_list_update nth_list_update_eq) by (metis index_update_if_diff2 length_list_update nth_list_update) qed lemma bij_betw_index: "distinct xs ⟹ X = set xs ⟹ l = size xs ⟹ bij_betw (index xs) X {0..<l}" apply simp apply(rule bij_betw_imageI[OF inj_on_index]) by (auto simp: image_def) (metis index_nth_id nth_mem) lemma index_image: "distinct xs ⟹ set xs = X ⟹ index xs ` X = {0..<size xs}" by (simp add: bij_betw_imp_surj_on bij_betw_index) lemma index_map_inj_on: "⟦ inj_on f S; y ∈ S; set xs ⊆ S ⟧ ⟹ index (map f xs) (f y) = index xs y" by (induct xs) (auto simp: inj_on_eq_iff) lemma index_map_inj: "inj f ⟹ index (map f xs) (f y) = index xs y" by (simp add: index_map_inj_on[where S=UNIV]) subsection ‹Map with index› primrec map_index' :: "nat ⇒ (nat ⇒ 'a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where "map_index' n f [] = []" | "map_index' n f (x#xs) = f n x # map_index' (Suc n) f xs" lemma length_map_index'[simp]: "length (map_index' n f xs) = length xs" by (induct xs arbitrary: n) auto lemma map_index'_map_zip: "map_index' n f xs = map (case_prod f) (zip [n ..< n + length xs] xs)" proof (induct xs arbitrary: n) case (Cons x xs) hence "map_index' n f (x#xs) = f n x # map (case_prod f) (zip [Suc n ..< n + length (x # xs)] xs)" by simp also have "… = map (case_prod f) (zip (n # [Suc n ..< n + length (x # xs)]) (x # xs))" by simp also have "(n # [Suc n ..< n + length (x # xs)]) = [n ..< n + length (x # xs)]" by (induct xs) auto finally show ?case by simp qed simp abbreviation "map_index ≡ map_index' 0" lemmas map_index = map_index'_map_zip[of 0, simplified] lemma take_map_index: "take p (map_index f xs) = map_index f (take p xs)" unfolding map_index by (auto simp: min_def take_map take_zip) lemma drop_map_index: "drop p (map_index f xs) = map_index' p f (drop p xs)" unfolding map_index'_map_zip by (cases "p < length xs") (auto simp: drop_map drop_zip) lemma map_map_index[simp]: "map g (map_index f xs) = map_index (λn x. g (f n x)) xs" unfolding map_index by auto lemma map_index_map[simp]: "map_index f (map g xs) = map_index (λn x. f n (g x)) xs" unfolding map_index by (auto simp: map_zip_map2) lemma set_map_index[simp]: "x ∈ set (map_index f xs) = (∃i < length xs. f i (xs ! i) = x)" unfolding map_index by (auto simp: set_zip intro!: image_eqI[of _ "case_prod f"]) lemma set_map_index'[simp]: "x∈set (map_index' n f xs) ⟷ (∃i<length xs. f (n+i) (xs!i) = x) " unfolding map_index'_map_zip by (auto simp: set_zip intro!: image_eqI[of _ "case_prod f"]) lemma nth_map_index[simp]: "p < length xs ⟹ map_index f xs ! p = f p (xs ! p)" unfolding map_index by auto lemma map_index_cong: "∀p < length xs. f p (xs ! p) = g p (xs ! p) ⟹ map_index f xs = map_index g xs" unfolding map_index by (auto simp: set_zip) lemma map_index_id: "map_index (curry snd) xs = xs" unfolding map_index by auto lemma map_index_no_index[simp]: "map_index (λn x. f x) xs = map f xs" unfolding map_index by (induct xs rule: rev_induct) auto lemma map_index_congL: "∀p < length xs. f p (xs ! p) = xs ! p ⟹ map_index f xs = xs" by (rule trans[OF map_index_cong map_index_id]) auto lemma map_index'_is_NilD: "map_index' n f xs = [] ⟹ xs = []" by (induct xs) auto declare map_index'_is_NilD[of 0, dest!] lemma map_index'_is_ConsD: "map_index' n f xs = y # ys ⟹ ∃z zs. xs = z # zs ∧ f n z = y ∧ map_index' (n + 1) f zs = ys" by (induct xs arbitrary: n) auto lemma map_index'_eq_imp_length_eq: "map_index' n f xs = map_index' n g ys ⟹ length xs = length ys" proof (induct ys arbitrary: xs n) case (Cons y ys) thus ?case by (cases xs) auto qed (auto dest!: map_index'_is_NilD) lemmas map_index_eq_imp_length_eq = map_index'_eq_imp_length_eq[of 0] lemma map_index'_comp[simp]: "map_index' n f (map_index' n g xs) = map_index' n (λn. f n o g n) xs" by (induct xs arbitrary: n) auto lemma map_index'_append[simp]: "map_index' n f (a @ b) = map_index' n f a @ map_index' (n + length a) f b" by (induct a arbitrary: n) auto lemma map_index_append[simp]: "map_index f (a @ b) = map_index f a @ map_index' (length a) f b" using map_index'_append[where n=0] by (simp del: map_index'_append) subsection ‹Insert at position› primrec insert_nth :: "nat ⇒ 'a ⇒ 'a list ⇒ 'a list" where "insert_nth 0 x xs = x # xs" | "insert_nth (Suc n) x xs = (case xs of [] ⇒ [x] | y # ys ⇒ y # insert_nth n x ys)" lemma insert_nth_take_drop[simp]: "insert_nth n x xs = take n xs @ [x] @ drop n xs" proof (induct n arbitrary: xs) case Suc thus ?case by (cases xs) auto qed simp lemma length_insert_nth: "length (insert_nth n x xs) = Suc (length xs)" by (induct xs) auto lemma set_insert_nth: "set (insert_nth i x xs) = insert x (set xs)" by (simp add: set_append[symmetric]) lemma distinct_insert_nth: assumes "distinct xs" assumes "x ∉ set xs" shows "distinct (insert_nth i x xs)" using assms proof (induct xs arbitrary: i) case Nil then show ?case by (cases i) auto next case (Cons a xs) then show ?case by (cases i) (auto simp add: set_insert_nth simp del: insert_nth_take_drop) qed lemma nth_insert_nth_front: assumes "i < j" "j ≤ length xs" shows "insert_nth j x xs ! i = xs ! i" using assms by (simp add: nth_append) lemma nth_insert_nth_index_eq: assumes "i ≤ length xs" shows "insert_nth i x xs ! i = x" using assms by (simp add: nth_append) lemma nth_insert_nth_back: assumes "j < i" "i ≤ length xs" shows "insert_nth j x xs ! i = xs ! (i - 1)" using assms by (cases i) (auto simp add: nth_append min_def) lemma nth_insert_nth: assumes "i ≤ length xs" "j ≤ length xs" shows "insert_nth j x xs ! i = (if i = j then x else if i < j then xs ! i else xs ! (i - 1))" using assms by (simp add: nth_insert_nth_front nth_insert_nth_index_eq nth_insert_nth_back del: insert_nth_take_drop) lemma insert_nth_inverse: assumes "j ≤ length xs" "j' ≤ length xs'" assumes "x ∉ set xs" "x ∉ set xs'" assumes "insert_nth j x xs = insert_nth j' x xs'" shows "j = j'" proof - from assms(1,3) have "∀i≤length xs. insert_nth j x xs ! i = x ⟷ i = j" by (auto simp add: nth_insert_nth simp del: insert_nth_take_drop) moreover from assms(2,4) have "∀i≤length xs'. insert_nth j' x xs' ! i = x ⟷ i = j'" by (auto simp add: nth_insert_nth simp del: insert_nth_take_drop) ultimately show "j = j'" using assms(1,2,5) by (metis dual_order.trans nat_le_linear) qed text ‹Insert several elements at given (ascending) positions› lemma length_fold_insert_nth: "length (fold (λ(p, b). insert_nth p b) pxs xs) = length xs + length pxs" by (induct pxs arbitrary: xs) auto lemma invar_fold_insert_nth: "⟦∀x∈set pxs. p < fst x; p < length xs; xs ! p = b⟧ ⟹ fold (λ(x, y). insert_nth x y) pxs xs ! p = b" by (induct pxs arbitrary: xs) (auto simp: nth_append) lemma nth_fold_insert_nth: "⟦sorted (map fst pxs); distinct (map fst pxs); ∀(p, b) ∈ set pxs. p < length xs + length pxs; i < length pxs; pxs ! i = (p, b)⟧ ⟹ fold (λ(p, b). insert_nth p b) pxs xs ! p = b" proof (induct pxs arbitrary: xs i p b) case (Cons pb pxs) show ?case proof (cases i) case 0 with Cons.prems have "p < Suc (length xs)" proof (induct pxs rule: rev_induct) case (snoc pb' pxs) then obtain p' b' where "pb' = (p', b')" by auto with snoc.prems have "∀p ∈ fst ` set pxs. p < p'" "p' ≤ Suc (length xs + length pxs)" by (auto simp: image_iff sorted_wrt_append le_eq_less_or_eq) with snoc.prems show ?case by (intro snoc(1)) (auto simp: sorted_append) qed auto with 0 Cons.prems show ?thesis unfolding fold.simps o_apply by (intro invar_fold_insert_nth) (auto simp: image_iff le_eq_less_or_eq nth_append) next case (Suc n) with Cons.prems show ?thesis unfolding fold.simps by (auto intro!: Cons(1)) qed qed simp subsection ‹Remove at position› fun remove_nth :: "nat ⇒ 'a list ⇒ 'a list" where "remove_nth i [] = []" | "remove_nth 0 (x # xs) = xs" | "remove_nth (Suc i) (x # xs) = x # remove_nth i xs" lemma remove_nth_take_drop: "remove_nth i xs = take i xs @ drop (Suc i) xs" proof (induct xs arbitrary: i) case Nil then show ?case by simp next case (Cons a xs) then show ?case by (cases i) auto qed lemma remove_nth_insert_nth: assumes "i ≤ length xs" shows "remove_nth i (insert_nth i x xs) = xs" using assms proof (induct xs arbitrary: i) case Nil then show ?case by simp next case (Cons a xs) then show ?case by (cases i) auto qed lemma insert_nth_remove_nth: assumes "i < length xs" shows "insert_nth i (xs ! i) (remove_nth i xs) = xs" using assms proof (induct xs arbitrary: i) case Nil then show ?case by simp next case (Cons a xs) then show ?case by (cases i) auto qed lemma length_remove_nth: assumes "i < length xs" shows "length (remove_nth i xs) = length xs - 1" using assms unfolding remove_nth_take_drop by simp lemma set_remove_nth_subset: "set (remove_nth j xs) ⊆ set xs" proof (induct xs arbitrary: j) case Nil then show ?case by simp next case (Cons a xs) then show ?case by (cases j) auto qed lemma set_remove_nth: assumes "distinct xs" "j < length xs" shows "set (remove_nth j xs) = set xs - {xs ! j}" using assms proof (induct xs arbitrary: j) case Nil then show ?case by simp next case (Cons a xs) then show ?case by (cases j) auto qed lemma distinct_remove_nth: assumes "distinct xs" shows "distinct (remove_nth i xs)" using assms proof (induct xs arbitrary: i) case Nil then show ?case by simp next case (Cons a xs) then show ?case by (cases i) (auto simp add: set_remove_nth_subset rev_subsetD) qed end