(* Author: René Thiemann Akihisa Yamada License: BSD *) subsection ‹Missing List› text ‹The provides some standard algorithms and lemmas on lists.› theory Missing_List imports Matrix.Utility "HOL-Library.Monad_Syntax" begin fun concat_lists :: "'a list list ⇒ 'a list list" where "concat_lists [] = [[]]" | "concat_lists (as # xs) = concat (map (λvec. map (λa. a # vec) as) (concat_lists xs))" lemma concat_lists_listset: "set (concat_lists xs) = listset (map set xs)" by (induct xs, auto simp: set_Cons_def) lemma sum_list_concat: "sum_list (concat ls) = sum_list (map sum_list ls)" by (induct ls, auto) (* TODO: move to src/HOL/List *) lemma listset: "listset xs = { ys. length ys = length xs ∧ (∀ i < length xs. ys ! i ∈ xs ! i)}" proof (induct xs) case (Cons x xs) let ?n = "length xs" from Cons have "?case = (set_Cons x {ys. length ys = ?n ∧ (∀i < ?n. ys ! i ∈ xs ! i)} = {ys. length ys = Suc ?n ∧ ys ! 0 ∈ x ∧ (∀i < ?n. ys ! Suc i ∈ xs ! i)})" (is "_ = (?L = ?R)") by (auto simp: all_Suc_conv) also have "?L = ?R" by (auto simp: set_Cons_def, case_tac xa, auto) finally show ?case by simp qed auto lemma set_concat_lists[simp]: "set (concat_lists xs) = {as. length as = length xs ∧ (∀i<length xs. as ! i ∈ set (xs ! i))}" unfolding concat_lists_listset listset by simp declare concat_lists.simps[simp del] fun find_map_filter :: "('a ⇒ 'b) ⇒ ('b ⇒ bool) ⇒ 'a list ⇒ 'b option" where "find_map_filter f p [] = None" | "find_map_filter f p (a # as) = (let b = f a in if p b then Some b else find_map_filter f p as)" lemma find_map_filter_Some: "find_map_filter f p as = Some b ⟹ p b ∧ b ∈ f ` set as" by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits) lemma find_map_filter_None: "find_map_filter f p as = None ⟹ ∀ b ∈ f ` set as. ¬ p b" by (induct f p as rule: find_map_filter.induct, auto simp: Let_def split: if_splits) lemma remdups_adj_sorted_distinct[simp]: "sorted xs ⟹ distinct (remdups_adj xs)" by (induct xs rule: remdups_adj.induct) (auto) lemma subseqs_length_simple: assumes "b ∈ set (subseqs xs)" shows "length b ≤ length xs" using assms by(induct xs arbitrary:b;auto simp:Let_def Suc_leD) lemma subseqs_length_simple_False: assumes "b ∈ set (subseqs xs)" " length xs < length b" shows False using assms subseqs_length_simple by fastforce lemma empty_subseqs[simp]: "[] ∈ set (subseqs xs)" by (induct xs, auto simp: Let_def) lemma full_list_subseqs: "{ys. ys ∈ set (subseqs xs) ∧ length ys = length xs} = {xs}" proof (induct xs) case (Cons x xs) have "?case = ({ys ∈ (#) x ` set (subseqs xs) ∪ set (subseqs xs). length ys = Suc (length xs)} = (#) x ` {xs})" (is "_ = (?l = ?r)") by (auto simp: Let_def) also have "?l = {ys ∈ (#) x ` set (subseqs xs). length ys = Suc (length xs)}" using length_subseqs[of xs] using subseqs_length_simple_False by force also have "… = (#) x ` {ys ∈ set (subseqs xs). length ys = length xs}" by auto also have "… = (#) x ` {xs}" unfolding Cons by auto finally show ?case by simp qed simp lemma nth_concat_split: assumes "i < length (concat xs)" shows "∃ j k. j < length xs ∧ k < length (xs ! j) ∧ concat xs ! i = xs ! j ! k" using assms proof (induct xs arbitrary: i) case (Cons x xs i) define I where "I = i - length x" show ?case proof (cases "i < length x") case True note l = this hence i: "concat (Cons x xs) ! i = x ! i" by (auto simp: nth_append) show ?thesis unfolding i by (rule exI[of _ 0], rule exI[of _ i], insert Cons l, auto) next case False note l = this from l Cons(2) have i: "i = length x + I" "I < length (concat xs)" unfolding I_def by auto hence iI: "concat (Cons x xs) ! i = concat xs ! I" by (auto simp: nth_append) from Cons(1)[OF i(2)] obtain j k where IH: "j < length xs ∧ k < length (xs ! j) ∧ concat xs ! I = xs ! j ! k" by auto show ?thesis unfolding iI by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH, auto) qed qed simp lemma nth_concat_diff: assumes "i1 < length (concat xs)" "i2 < length (concat xs)" "i1 ≠ i2" shows "∃ j1 k1 j2 k2. (j1,k1) ≠ (j2,k2) ∧ j1 < length xs ∧ j2 < length xs ∧ k1 < length (xs ! j1) ∧ k2 < length (xs ! j2) ∧ concat xs ! i1 = xs ! j1 ! k1 ∧ concat xs ! i2 = xs ! j2 ! k2" using assms proof (induct xs arbitrary: i1 i2) case (Cons x xs) define I1 where "I1 = i1 - length x" define I2 where "I2 = i2 - length x" show ?case proof (cases "i1 < length x") case True note l1 = this hence i1: "concat (Cons x xs) ! i1 = x ! i1" by (auto simp: nth_append) show ?thesis proof (cases "i2 < length x") case True note l2 = this hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append) show ?thesis unfolding i1 i2 by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ 0], rule exI[of _ i2], insert Cons(4) l1 l2, auto) next case False note l2 = this from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append) from nth_concat_split[OF i22(2)] obtain j2 k2 where *: "j2 < length xs ∧ k2 < length (xs ! j2) ∧ concat xs ! I2 = xs ! j2 ! k2" by auto show ?thesis unfolding i1 i2 by (rule exI[of _ 0], rule exI[of _ i1], rule exI[of _ "Suc j2"], rule exI[of _ k2], insert * l1, auto) qed next case False note l1 = this from l1 Cons(2) have i11: "i1 = length x + I1" "I1 < length (concat xs)" unfolding I1_def by auto hence i1: "concat (Cons x xs) ! i1 = concat xs ! I1" by (auto simp: nth_append) show ?thesis proof (cases "i2 < length x") case False note l2 = this from l2 Cons(3) have i22: "i2 = length x + I2" "I2 < length (concat xs)" unfolding I2_def by auto hence i2: "concat (Cons x xs) ! i2 = concat xs ! I2" by (auto simp: nth_append) from Cons(4) i11 i22 have diff: "I1 ≠ I2" by auto from Cons(1)[OF i11(2) i22(2) diff] obtain j1 k1 j2 k2 where IH: "(j1,k1) ≠ (j2,k2) ∧ j1 < length xs ∧ j2 < length xs ∧ k1 < length (xs ! j1) ∧ k2 < length (xs ! j2) ∧ concat xs ! I1 = xs ! j1 ! k1 ∧ concat xs ! I2 = xs ! j2 ! k2" by auto show ?thesis unfolding i1 i2 by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ "Suc j2"], rule exI[of _ k2], insert IH, auto) next case True note l2 = this hence i2: "concat (Cons x xs) ! i2 = x ! i2" by (auto simp: nth_append) from nth_concat_split[OF i11(2)] obtain j1 k1 where *: "j1 < length xs ∧ k1 < length (xs ! j1) ∧ concat xs ! I1 = xs ! j1 ! k1" by auto show ?thesis unfolding i1 i2 by (rule exI[of _ "Suc j1"], rule exI[of _ k1], rule exI[of _ 0], rule exI[of _ i2], insert * l2, auto) qed qed qed auto lemma list_all2_map_map: "(⋀ x. x ∈ set xs ⟹ R (f x) (g x)) ⟹ list_all2 R (map f xs) (map g xs)" by (induct xs, auto) subsection ‹Partitions› text ‹Check whether a list of sets forms a partition, i.e., whether the sets are pairwise disjoint.› definition is_partition :: "('a set) list ⇒ bool" where "is_partition cs ⟷ (∀j<length cs. ∀i<j. cs ! i ∩ cs ! j = {})" (* and an equivalent but more symmetric version *) definition is_partition_alt :: "('a set) list ⇒ bool" where "is_partition_alt cs ⟷ (∀ i j. i < length cs ∧ j < length cs ∧ i ≠ j ⟶ cs!i ∩ cs!j = {})" lemma is_partition_alt: "is_partition = is_partition_alt" proof (intro ext) fix cs :: "'a set list" { assume "is_partition_alt cs" hence "is_partition cs" unfolding is_partition_def is_partition_alt_def by auto } moreover { assume part: "is_partition cs" have "is_partition_alt cs" unfolding is_partition_alt_def proof (intro allI impI) fix i j assume "i < length cs ∧ j < length cs ∧ i ≠ j" with part show "cs ! i ∩ cs ! j = {}" unfolding is_partition_def by (cases "i < j", simp, cases "j < i", force, simp) qed } ultimately show "is_partition cs = is_partition_alt cs" by auto qed lemma is_partition_Nil: "is_partition [] = True" unfolding is_partition_def by auto lemma is_partition_Cons: "is_partition (x#xs) ⟷ is_partition xs ∧ x ∩ ⋃(set xs) = {}" (is "?l = ?r") proof assume ?l have one: "is_partition xs" proof (unfold is_partition_def, intro allI impI) fix j i assume "j < length xs" and "i < j" hence "Suc j < length(x#xs)" and "Suc i < Suc j" by auto from ‹?l›[unfolded is_partition_def,THEN spec,THEN mp,THEN spec,THEN mp,OF this] have "(x#xs)!(Suc i) ∩ (x#xs)!(Suc j) = {}" . thus "xs!i ∩ xs!j = {}" by simp qed have two: "x ∩ ⋃(set xs) = {}" proof (rule ccontr) assume "x ∩ ⋃(set xs) ≠ {}" then obtain y where "y ∈ x" and "y ∈ ⋃(set xs)" by auto then obtain z where "z ∈ set xs" and "y ∈ z" by auto then obtain i where "i < length xs" and "xs!i = z" using in_set_conv_nth[of z xs] by auto with ‹y ∈ z› have "y ∈ (x#xs)!Suc i" by auto moreover with ‹y ∈ x› have "y ∈ (x#xs)!0" by simp ultimately have "(x#xs)!0 ∩ (x#xs)!Suc i ≠ {}" by auto moreover from ‹i < length xs› have "Suc i < length(x#xs)" by simp ultimately show False using ‹?l›[unfolded is_partition_def] by best qed from one two show ?r .. next assume ?r show ?l proof (unfold is_partition_def, intro allI impI) fix j i assume j: "j < length (x # xs)" assume i: "i < j" from i obtain j' where j': "j = Suc j'" by (cases j, auto) with j have j'len: "j' < length xs" and j'elem: "(x # xs) ! j = xs ! j'" by auto show "(x # xs) ! i ∩ (x # xs) ! j = {}" proof (cases i) case 0 with j'elem have "(x # xs) ! i ∩ (x # xs) ! j = x ∩ xs ! j'" by auto also have "… ⊆ x ∩ ⋃(set xs)" using j'len by force finally show ?thesis using ‹?r› by auto next case (Suc i') with i j' have i'j': "i' < j'" by auto from Suc j' have "(x # xs) ! i ∩ (x # xs) ! j = xs ! i' ∩ xs ! j'" by auto with ‹?r› i'j' j'len show ?thesis unfolding is_partition_def by auto qed qed qed lemma is_partition_sublist: assumes "is_partition (us @ xs @ ys @ zs @ vs)" shows "is_partition (xs @ zs)" proof (rule ccontr) assume "¬ is_partition (xs @ zs)" then obtain i j where j:"j < length (xs @ zs)" and i:"i < j" and *:"(xs @ zs) ! i ∩ (xs @ zs) ! j ≠ {}" unfolding is_partition_def by blast then show False proof (cases "j < length xs") case True let ?m = "j + length us" let ?n = "i + length us" from True have "?m < length (us @ xs @ ys @ zs @ vs)" by auto moreover from i have "?n < ?m" by auto moreover have "(us @ xs @ ys @ zs @ vs) ! ?n ∩ (us @ xs @ ys @ zs @ vs) ! ?m ≠ {}" using i True * nth_append by (metis (no_types, lifting) add_diff_cancel_right' not_add_less2 order.strict_trans) ultimately show False using assms unfolding is_partition_def by auto next case False let ?m = "j + length us + length ys" from j have m:"?m < length (us @ xs @ ys @ zs @ vs)" by auto have mj:"(us @ (xs @ ys @ zs @ vs)) ! ?m = (xs @ zs) ! j" unfolding nth_append using False j by auto show False proof (cases "i < length xs") case True let ?n = "i + length us" from i have "?n < ?m" by auto moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i" by (simp add: True nth_append) ultimately show False using * m assms mj unfolding is_partition_def by blast next case False let ?n = "i + length us + length ys" from i have i:"?n < ?m" by auto moreover have "(us @ xs @ ys @ zs @ vs) ! ?n = (xs @ zs) ! i" unfolding nth_append using False i j less_diff_conv2 by auto ultimately show False using * m assms mj unfolding is_partition_def by blast qed qed qed lemma is_partition_inj_map: assumes "is_partition xs" and "inj_on f (⋃x ∈ set xs. x)" shows "is_partition (map ((`) f) xs)" proof (rule ccontr) assume "¬ is_partition (map ((`) f) xs)" then obtain i j where neq:"i ≠ j" and i:"i < length (map ((`) f) xs)" and j:"j < length (map ((`) f) xs)" and "map ((`) f) xs ! i ∩ map ((`) f) xs ! j ≠ {}" unfolding is_partition_alt is_partition_alt_def by auto then obtain x where "x ∈ map ((`) f) xs ! i" and "x ∈ map ((`) f) xs ! j" by auto then obtain y z where yi:"y ∈ xs ! i" and yx:"f y = x" and zj:"z ∈ xs ! j" and zx:"f z = x" using i j by auto show False proof (cases "y = z") case True with zj yi neq assms(1) i j show ?thesis by (auto simp: is_partition_alt is_partition_alt_def) next case False have "y ∈ (⋃x ∈ set xs. x)" using yi i by force moreover have "z ∈ (⋃x ∈ set xs. x)" using zj j by force ultimately show ?thesis using assms(2) inj_on_def[of f "(⋃x∈set xs. x)"] False zx yx by blast qed qed context begin private fun is_partition_impl :: "'a set list ⇒ 'a set option" where "is_partition_impl [] = Some {}" | "is_partition_impl (as # rest) = do { all ← is_partition_impl rest; if as ∩ all = {} then Some (all ∪ as) else None }" lemma is_partition_code[code]: "is_partition as = (is_partition_impl as ≠ None)" proof - note [simp] = is_partition_Cons is_partition_Nil have "⋀ bs. (is_partition as = (is_partition_impl as ≠ None)) ∧ (is_partition_impl as = Some bs ⟶ bs = ⋃ (set as))" proof (induct as) case (Cons as rest bs) show ?case proof (cases "is_partition rest") case False thus ?thesis using Cons by auto next case True with Cons obtain c where rest: "is_partition_impl rest = Some c" by (cases "is_partition_impl rest", auto) with Cons True show ?thesis by auto qed qed auto thus ?thesis by blast qed end lemma case_prod_partition: "case_prod f (partition p xs) = f (filter p xs) (filter (Not ∘ p) xs)" by simp lemmas map_id[simp] = list.map_id subsection ‹merging functions› definition fun_merge :: "('a ⇒ 'b)list ⇒ 'a set list ⇒ 'a ⇒ 'b" where "fun_merge fs as a ≡ (fs ! (LEAST i. i < length as ∧ a ∈ as ! i)) a" lemma fun_merge: assumes i: "i < length as" and a: "a ∈ as ! i" and ident: "⋀ i j a. i < length as ⟹ j < length as ⟹ a ∈ as ! i ⟹ a ∈ as ! j ⟹ (fs ! i) a = (fs ! j) a" shows "fun_merge fs as a = (fs ! i) a" proof - let ?p = "λ i. i < length as ∧ a ∈ as ! i" let ?l = "LEAST i. ?p i" have p: "?p ?l" by (rule LeastI, insert i a, auto) show ?thesis unfolding fun_merge_def by (rule ident[OF _ i _ a], insert p, auto) qed lemma fun_merge_part: assumes part: "is_partition as" and i: "i < length as" and a: "a ∈ as ! i" shows "fun_merge fs as a = (fs ! i) a" proof(rule fun_merge[OF i a]) fix i j a assume "i < length as" and "j < length as" and "a ∈ as ! i" and "a ∈ as ! j" hence "i = j" using part[unfolded is_partition_alt is_partition_alt_def] by (cases "i = j", auto) thus "(fs ! i) a = (fs ! j) a" by simp qed lemma map_nth_conv: "map f ss = map g ts ⟹ ∀i < length ss. f(ss!i) = g(ts!i)" proof (intro allI impI) fix i show "map f ss = map g ts ⟹ i < length ss ⟹ f(ss!i) = g(ts!i)" proof (induct ss arbitrary: i ts) case Nil thus ?case by (induct ts) auto next case (Cons s ss) thus ?case by (induct ts, simp, (cases i, auto)) qed qed lemma distinct_take_drop: assumes dist: "distinct vs" and len: "i < length vs" shows "distinct(take i vs @ drop (Suc i) vs)" (is "distinct(?xs@?ys)") proof - from id_take_nth_drop[OF len] have vs[symmetric]: "vs = ?xs @ vs!i # ?ys" . with dist have "distinct ?xs" and "distinct(vs!i#?ys)" and "set ?xs ∩ set(vs!i#?ys) = {}" using distinct_append[of ?xs "vs!i#?ys"] by auto hence "distinct ?ys" and "set ?xs ∩ set ?ys = {}" by auto with ‹distinct ?xs› show ?thesis using distinct_append[of ?xs ?ys] vs by simp qed lemma map_nth_eq_conv: assumes len: "length xs = length ys" shows "(map f xs = ys) = (∀i<length ys. f (xs ! i) = ys ! i)" (is "?l = ?r") proof - have "(map f xs = ys) = (map f xs = map id ys)" by auto also have "... = (∀ i < length ys. f (xs ! i) = id (ys ! i))" using map_nth_conv[of f xs id ys] nth_map_conv[OF len, of f id] unfolding len by blast finally show ?thesis by auto qed lemma map_upt_len_conv: "map (λ i . f (xs!i)) [0..<length xs] = map f xs" by (rule nth_equalityI, auto) lemma map_upt_add': "map f [a..<a+b] = map (λ i. f (a + i)) [0..<b]" by (induct b, auto) definition generate_lists :: "nat ⇒ 'a list ⇒ 'a list list" where "generate_lists n xs ≡ concat_lists (map (λ _. xs) [0 ..< n])" lemma set_generate_lists[simp]: "set (generate_lists n xs) = {as. length as = n ∧ set as ⊆ set xs}" proof - { fix as have "(length as = n ∧ (∀i<n. as ! i ∈ set xs)) = (length as = n ∧ set as ⊆ set xs)" proof - { assume "length as = n" hence n: "n = length as" by auto have "(∀i<n. as ! i ∈ set xs) = (set as ⊆ set xs)" unfolding n unfolding all_set_conv_all_nth[of as "λ x. x ∈ set xs", symmetric] by auto } thus ?thesis by auto qed } thus ?thesis unfolding generate_lists_def unfolding set_concat_lists by auto qed lemma nth_append_take: assumes "i ≤ length xs" shows "(take i xs @ y#ys)!i = y" proof - from assms have a: "length(take i xs) = i" by simp have "(take i xs @ y#ys)!(length(take i xs)) = y" by (rule nth_append_length) thus ?thesis unfolding a . qed lemma nth_append_take_is_nth_conv: assumes "i < j" and "j ≤ length xs" shows "(take j xs @ ys)!i = xs!i" proof - from assms have "i < length(take j xs)" by simp hence "(take j xs @ ys)!i = take j xs ! i" unfolding nth_append by simp thus ?thesis unfolding nth_take[OF assms(1)] . qed lemma nth_append_drop_is_nth_conv: assumes "j < i" and "j ≤ length xs" and "i ≤ length xs" shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i" proof - from ‹j < i› obtain n where ij: "Suc(j + n) = i" using less_imp_Suc_add by auto with assms have i: "i = length(take j xs) + Suc n" by auto have len: "Suc j + n ≤ length xs" using assms i by auto have "(take j xs @ y # drop (Suc j) xs)!i = (y # drop (Suc j) xs)!(i - length(take j xs))" unfolding nth_append i by auto also have "… = (y # drop (Suc j) xs)!(Suc n)" unfolding i by simp also have "… = (drop (Suc j) xs)!n" by simp finally show ?thesis using ij len by simp qed lemma nth_append_take_drop_is_nth_conv: assumes "i ≤ length xs" and "j ≤ length xs" and "i ≠ j" shows "(take j xs @ y # drop (Suc j) xs)!i = xs!i" proof - from assms have "i < j ∨ i > j" by auto thus ?thesis using assms by (auto simp: nth_append_take_is_nth_conv nth_append_drop_is_nth_conv) qed lemma take_drop_imp_nth: "⟦take i ss @ x # drop (Suc i) ss = ss⟧ ⟹ x = ss!i" proof (induct ss arbitrary: i) case (Cons s ss) from ‹take i (s#ss) @ x # drop (Suc i) (s#ss) = (s#ss)› show ?case proof (induct i) case (Suc i) from Cons have IH: "take i ss @ x # drop (Suc i) ss = ss ⟹ x = ss!i" by auto from Suc have "take i ss @ x # drop (Suc i) ss = ss" by auto with IH show ?case by auto qed auto qed auto lemma take_drop_update_first: assumes "j < length ds" and "length cs = length ds" shows "(take j ds @ drop j cs)[j := ds ! j] = take (Suc j) ds @ drop (Suc j) cs" using assms proof (induct j arbitrary: ds cs) case 0 then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) show ?case unfolding ds cs by auto next case (Suc j) then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto qed lemma take_drop_update_second: assumes "j < length ds" and "length cs = length ds" shows "(take j ds @ drop j cs)[j := cs ! j] = take j ds @ drop j cs" using assms proof (induct j arbitrary: ds cs) case 0 then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) show ?case unfolding ds cs by auto next case (Suc j) then obtain d dds c ccs where ds: "ds = d # dds" and cs: "cs = c # ccs" by (cases ds, simp, cases cs, auto) from Suc(1)[of dds ccs] Suc(2) Suc(3) show ?case unfolding ds cs by auto qed lemma nth_take_prefix: "length ys ≤ length xs ⟹ ∀i < length ys. xs!i = ys!i ⟹ take (length ys) xs = ys" proof (induct xs ys rule: list_induct2') case (4 x xs y ys) have "take (length ys) xs = ys" by (rule 4(1), insert 4(2-3), auto) moreover from 4(3) have "x = y" by auto ultimately show ?case by auto qed auto lemma take_upt_idx: assumes i: "i < length ls" shows "take i ls = [ ls ! j . j ← [0..<i]]" proof - have e: "0 + i ≤ i" by auto show ?thesis using take_upt[OF e] take_map map_nth by (metis (opaque_lifting, no_types) add.left_neutral i nat_less_le take_upt) qed fun distinct_eq :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where "distinct_eq _ [] = True" | "distinct_eq eq (x # xs) = ((∀ y ∈ set xs. ¬ (eq y x)) ∧ distinct_eq eq xs)" lemma distinct_eq_append: "distinct_eq eq (xs @ ys) = (distinct_eq eq xs ∧ distinct_eq eq ys ∧ (∀ x ∈ set xs. ∀ y ∈ set ys. ¬ (eq y x)))" by (induct xs, auto) lemma append_Cons_nth_left: assumes "i < length xs" shows "(xs @ u # ys) ! i = xs ! i" using assms nth_append[of xs _ i] by simp lemma append_Cons_nth_middle: assumes "i = length xs" shows "(xs @ y # zs) ! i = y" using assms by auto lemma append_Cons_nth_right: assumes "i > length xs" shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i" by (simp add: assms nth_append) lemma append_Cons_nth_not_middle: assumes "i ≠ length xs" shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i" by (metis assms list_update_length nth_list_update_neq) lemmas append_Cons_nth = append_Cons_nth_middle append_Cons_nth_not_middle lemma concat_all_nth: assumes "length xs = length ys" and "⋀i. i < length xs ⟹ length (xs ! i) = length (ys ! i)" and "⋀i j. i < length xs ⟹ j < length (xs ! i) ⟹ P (xs ! i ! j) (ys ! i ! j)" shows "∀k<length (concat xs). P (concat xs ! k) (concat ys ! k)" using assms proof (induct xs ys rule: list_induct2) case (Cons x xs y ys) from Cons(3)[of 0] have xy: "length x = length y" by simp from Cons(4)[of 0] xy have pxy: "⋀ j. j < length x ⟹ P (x ! j) (y ! j)" by auto { fix i assume i: "i < length xs" with Cons(3)[of "Suc i"] have len: "length (xs ! i) = length (ys ! i)" by simp from Cons(4)[of "Suc i"] i have "⋀ j. j < length (xs ! i) ⟹ P (xs ! i ! j) (ys ! i ! j)" by auto note len and this } from Cons(2)[OF this] have ind: "⋀ k. k < length (concat xs) ⟹ P (concat xs ! k) (concat ys ! k)" by auto show ?case unfolding concat.simps proof (intro allI impI) fix k assume k: "k < length (x @ concat xs)" show "P ((x @ concat xs) ! k) ((y @ concat ys) ! k)" proof (cases "k < length x") case True show ?thesis unfolding nth_append using True xy pxy[OF True] by simp next case False with k have "k - (length x) < length (concat xs)" by auto then obtain n where n: "k - length x = n" and nxs: "n < length (concat xs)" by auto show ?thesis unfolding nth_append n n[unfolded xy] using False xy ind[OF nxs] by auto qed qed qed auto lemma eq_length_concat_nth: assumes "length xs = length ys" and "⋀i. i < length xs ⟹ length (xs ! i) = length (ys ! i)" shows "length (concat xs) = length (concat ys)" using assms proof (induct xs ys rule: list_induct2) case (Cons x xs y ys) from Cons(3)[of 0] have xy: "length x = length y" by simp { fix i assume "i < length xs" with Cons(3)[of "Suc i"] have "length (xs ! i) = length (ys ! i)" by simp } from Cons(2)[OF this] have ind: "length (concat xs) = length (concat ys)" by simp show ?case using xy ind by auto qed auto primrec list_union :: "'a list ⇒ 'a list ⇒ 'a list" where "list_union [] ys = ys" | "list_union (x # xs) ys = (let zs = list_union xs ys in if x ∈ set zs then zs else x # zs)" lemma set_list_union[simp]: "set (list_union xs ys) = set xs ∪ set ys" proof (induct xs) case (Cons x xs) thus ?case by (cases "x ∈ set (list_union xs ys)") (auto) qed simp declare list_union.simps[simp del] (*Why was list_inter thrown out of List.thy?*) fun list_inter :: "'a list ⇒ 'a list ⇒ 'a list" where "list_inter [] bs = []" | "list_inter (a#as) bs = (if a ∈ set bs then a # list_inter as bs else list_inter as bs)" lemma set_list_inter[simp]: "set (list_inter xs ys) = set xs ∩ set ys" by (induct rule: list_inter.induct) simp_all declare list_inter.simps[simp del] primrec list_diff :: "'a list ⇒ 'a list ⇒ 'a list" where "list_diff [] ys = []" | "list_diff (x # xs) ys = (let zs = list_diff xs ys in if x ∈ set ys then zs else x # zs)" lemma set_list_diff[simp]: "set (list_diff xs ys) = set xs - set ys" proof (induct xs) case (Cons x xs) thus ?case by (cases "x ∈ set ys") (auto) qed simp declare list_diff.simps[simp del] lemma nth_drop_0: "0 < length ss ⟹ (ss!0)#drop (Suc 0) ss = ss" by (simp add: Cons_nth_drop_Suc) lemma set_foldr_remdups_set_map_conv[simp]: "set (foldr (λx xs. remdups (f x @ xs)) xs []) = ⋃(set (map (set ∘ f) xs))" by (induct xs) auto lemma subset_set_code[code_unfold]: "set xs ⊆ set ys ⟷ list_all (λx. x ∈ set ys) xs" unfolding list_all_iff by auto fun union_list_sorted where "union_list_sorted (x # xs) (y # ys) = (if x = y then x # union_list_sorted xs ys else if x < y then x # union_list_sorted xs (y # ys) else y # union_list_sorted (x # xs) ys)" | "union_list_sorted [] ys = ys" | "union_list_sorted xs [] = xs" lemma [simp]: "set (union_list_sorted xs ys) = set xs ∪ set ys" by (induct xs ys rule: union_list_sorted.induct, auto) fun subtract_list_sorted :: "('a :: linorder) list ⇒ 'a list ⇒ 'a list" where "subtract_list_sorted (x # xs) (y # ys) = (if x = y then subtract_list_sorted xs (y # ys) else if x < y then x # subtract_list_sorted xs (y # ys) else subtract_list_sorted (x # xs) ys)" | "subtract_list_sorted [] ys = []" | "subtract_list_sorted xs [] = xs" lemma set_subtract_list_sorted[simp]: "sorted xs ⟹ sorted ys ⟹ set (subtract_list_sorted xs ys) = set xs - set ys" proof (induct xs ys rule: subtract_list_sorted.induct) case (1 x xs y ys) have xxs: "sorted (x # xs)" by fact have yys: "sorted (y # ys)" by fact have xs: "sorted xs" using xxs by (simp) show ?case proof (cases "x = y") case True thus ?thesis using 1(1)[OF True xs yys] by auto next case False note neq = this note IH = 1(2-3)[OF this] show ?thesis by (cases "x < y", insert IH xxs yys False, auto) qed qed auto lemma subset_subtract_listed_sorted: "set (subtract_list_sorted xs ys) ⊆ set xs" by (induct xs ys rule: subtract_list_sorted.induct, auto) lemma set_subtract_list_distinct[simp]: "distinct xs ⟹ distinct (subtract_list_sorted xs ys)" by (induct xs ys rule: subtract_list_sorted.induct, insert subset_subtract_listed_sorted, auto) definition "remdups_sort xs = remdups_adj (sort xs)" lemma remdups_sort[simp]: "sorted (remdups_sort xs)" "set (remdups_sort xs) = set xs" "distinct (remdups_sort xs)" by (simp_all add: remdups_sort_def) text ‹maximum and minimum› lemma max_list_mono: assumes "⋀ x. x ∈ set xs - set ys ⟹ ∃ y. y ∈ set ys ∧ x ≤ y" shows "max_list xs ≤ max_list ys" using assms proof (induct xs) case (Cons x xs) have "x ≤ max_list ys" proof (cases "x ∈ set ys") case True from max_list[OF this] show ?thesis . next case False with Cons(2)[of x] obtain y where y: "y ∈ set ys" and xy: "x ≤ y" by auto from xy max_list[OF y] show ?thesis by arith qed moreover have "max_list xs ≤ max_list ys" by (rule Cons(1)[OF Cons(2)], auto) ultimately show ?case by auto qed auto fun min_list :: "('a :: linorder) list ⇒ 'a" where "min_list [x] = x" | "min_list (x # xs) = min x (min_list xs)" lemma min_list: "(x :: 'a :: linorder) ∈ set xs ⟹ min_list xs ≤ x" proof (induct xs) case oCons : (Cons y ys) show ?case proof (cases ys) case Nil thus ?thesis using oCons by auto next case (Cons z zs) hence "min_list (y # ys) = min y (min_list ys)" by auto then show ?thesis using min_le_iff_disj oCons.hyps oCons.prems by auto qed qed simp lemma min_list_Cons: assumes xy: "x ≤ y" and len: "length xs = length ys" and xsys: "min_list xs ≤ min_list ys" shows "min_list (x # xs) ≤ min_list (y # ys)" by (metis min_list.simps len length_greater_0_conv min.mono nth_drop_0 xsys xy) lemma min_list_nth: assumes "length xs = length ys" and "⋀i. i < length ys ⟹ xs ! i ≤ ys ! i" shows "min_list xs ≤ min_list ys" using assms proof (induct xs arbitrary: ys) case (Cons x xs zs) from Cons(2) obtain y ys where zs: "zs = y # ys" by (cases zs, auto) note Cons = Cons[unfolded zs] from Cons(2) have len: "length xs = length ys" by simp from Cons(3)[of 0] have xy: "x ≤ y" by simp { fix i assume "i < length xs" with Cons(3)[of "Suc i"] Cons(2) have "xs ! i ≤ ys ! i" by simp } from Cons(1)[OF len this] Cons(2) have ind: "min_list xs ≤ min_list ys" by simp show ?case unfolding zs by (rule min_list_Cons[OF xy len ind]) qed auto lemma min_list_ex: assumes "xs ≠ []" shows "∃x∈set xs. min_list xs = x" using assms proof (induct xs) case oCons : (Cons x xs) show ?case proof (cases xs) case (Cons y ys) hence id: "min_list (x # xs) = min x (min_list xs)" and nNil: "xs ≠ []" by auto show ?thesis proof (cases "x ≤ min_list xs") case True show ?thesis unfolding id by (rule bexI[of _ x], insert True, auto simp: min_def) next case False show ?thesis unfolding id min_def using oCons(1)[OF nNil] False by auto qed qed auto qed auto lemma min_list_subset: assumes subset: "set ys ⊆ set xs" and mem: "min_list xs ∈ set ys" shows "min_list xs = min_list ys" by (metis antisym empty_iff empty_set mem min_list min_list_ex subset subsetD) text‹Apply a permutation to a list.› primrec permut_aux :: "'a list ⇒ (nat ⇒ nat) ⇒ 'a list ⇒ 'a list" where "permut_aux [] _ _ = []" | "permut_aux (a # as) f bs = (bs ! f 0) # (permut_aux as (λn. f (Suc n)) bs)" definition permut :: "'a list ⇒ (nat ⇒ nat) ⇒ 'a list" where "permut as f = permut_aux as f as" declare permut_def[simp] lemma permut_aux_sound: assumes "i < length as" shows "permut_aux as f bs ! i = bs ! (f i)" using assms proof (induct as arbitrary: i f bs) case (Cons x xs) show ?case proof (cases i) case (Suc j) with Cons(2) have "j < length xs" by simp from Cons(1)[OF this] and Suc show ?thesis by simp qed simp qed simp lemma permut_sound: assumes "i < length as" shows "permut as f ! i = as ! (f i)" using assms and permut_aux_sound by simp lemma permut_aux_length: assumes "bij_betw f {..<length as} {..<length bs}" shows "length (permut_aux as f bs) = length as" by (induct as arbitrary: f bs, simp_all) lemma permut_length: assumes "bij_betw f {..< length as} {..< length as}" shows "length (permut as f) = length as" using permut_aux_length[OF assms] by simp declare permut_def[simp del] lemma foldl_assoc: fixes b :: "('a ⇒ 'a) ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a" (infixl "⋅" 55) assumes "⋀f g h. f ⋅ (g ⋅ h) = f ⋅ g ⋅ h" shows "foldl (⋅) (x ⋅ y) zs = x ⋅ foldl (⋅) y zs" using assms[symmetric] by (induct zs arbitrary: y) simp_all lemma foldr_assoc: assumes "⋀f g h. b (b f g) h = b f (b g h)" shows "foldr b xs (b y z) = b (foldr b xs y) z" using assms by (induct xs) simp_all lemma foldl_foldr_o_id: "foldl (∘) id fs = foldr (∘) fs id" proof (induct fs) case (Cons f fs) have "id ∘ f = f ∘ id" by simp with Cons [symmetric] show ?case by (simp only: foldl_Cons foldr_Cons o_apply [of _ _ id] foldl_assoc o_assoc) qed simp lemma foldr_o_o_id[simp]: "foldr ((∘) ∘ f) xs id a = foldr f xs a" by (induct xs) simp_all lemma Ex_list_of_length_P: assumes "∀i<n. ∃x. P x i" shows "∃xs. length xs = n ∧ (∀i<n. P (xs ! i) i)" proof - from assms have "∀ i. ∃ x. i < n ⟶ P x i" by simp from choice[OF this] obtain xs where xs: "⋀ i. i < n ⟹ P (xs i) i" by auto show ?thesis by (rule exI[of _ "map xs [0 ..< n]"], insert xs, auto) qed lemma ex_set_conv_ex_nth: "(∃x∈set xs. P x) = (∃i<length xs. P (xs ! i))" using in_set_conv_nth[of _ xs] by force lemma map_eq_set_zipD [dest]: assumes "map f xs = map f ys" and "(x, y) ∈ set (zip xs ys)" shows "f x = f y" using assms proof (induct xs arbitrary: ys) case (Cons x xs) then show ?case by (cases ys) auto qed simp fun span :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list × 'a list" where "span P (x # xs) = (if P x then let (ys, zs) = span P xs in (x # ys, zs) else ([], x # xs))" | "span _ [] = ([], [])" lemma span[simp]: "span P xs = (takeWhile P xs, dropWhile P xs)" by (induct xs, auto) declare span.simps[simp del] lemma parallel_list_update: assumes one_update: "⋀ xs i y. length xs = n ⟹ i < n ⟹ r (xs ! i) y ⟹ p xs ⟹ p (xs[i := y])" and init: "length xs = n" "p xs" and rel: "length ys = n" "⋀ i. i < n ⟹ r (xs ! i) (ys ! i)" shows "p ys" proof - note len = rel(1) init(1) { fix i assume "i ≤ n" hence "p (take i ys @ drop i xs)" proof (induct i) case 0 with init show ?case by simp next case (Suc i) hence IH: "p (take i ys @ drop i xs)" by simp from Suc have i: "i < n" by simp let ?xs = "(take i ys @ drop i xs)" have "length ?xs = n" using i len by simp from one_update[OF this i _ IH, of "ys ! i"] rel(2)[OF i] i len show ?case by (simp add: nth_append take_drop_update_first) qed } from this[of n] show ?thesis using len by auto qed lemma nth_concat_two_lists: "i < length (concat (xs :: 'a list list)) ⟹ length (ys :: 'b list list) = length xs ⟹ (⋀ i. i < length xs ⟹ length (ys ! i) = length (xs ! i)) ⟹ ∃ j k. j < length xs ∧ k < length (xs ! j) ∧ (concat xs) ! i = xs ! j ! k ∧ (concat ys) ! i = ys ! j ! k" proof (induct xs arbitrary: i ys) case (Cons x xs i yys) then obtain y ys where yys: "yys = y # ys" by (cases yys, auto) note Cons = Cons[unfolded yys] from Cons(4)[of 0] have [simp]: "length y = length x" by simp show ?case proof (cases "i < length x") case True show ?thesis unfolding yys by (rule exI[of _ 0], rule exI[of _ i], insert True Cons(2-4), auto simp: nth_append) next case False let ?i = "i - length x" from False Cons(2-3) have "?i < length (concat xs)" "length ys = length xs" by auto note IH = Cons(1)[OF this] { fix i assume "i < length xs" with Cons(4)[of "Suc i"] have "length (ys ! i) = length (xs ! i)" by simp } from IH[OF this] obtain j k where IH1: "j < length xs" "k < length (xs ! j)" "concat xs ! ?i = xs ! j ! k" "concat ys ! ?i = ys ! j ! k" by auto show ?thesis unfolding yys by (rule exI[of _ "Suc j"], rule exI[of _ k], insert IH1 False, auto simp: nth_append) qed qed simp text ‹Removing duplicates w.r.t. some function.› fun remdups_gen :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'a list" where "remdups_gen f [] = []" | "remdups_gen f (x # xs) = x # remdups_gen f [y <- xs. ¬ f x = f y]" lemma remdups_gen_subset: "set (remdups_gen f xs) ⊆ set xs" by (induct f xs rule: remdups_gen.induct, auto) lemma remdups_gen_elem_imp_elem: "x ∈ set (remdups_gen f xs) ⟹ x ∈ set xs" using remdups_gen_subset[of f xs] by blast lemma elem_imp_remdups_gen_elem: "x ∈ set xs ⟹ ∃ y ∈ set (remdups_gen f xs). f x = f y" proof (induct f xs rule: remdups_gen.induct) case (2 f z zs) show ?case proof (cases "f x = f z") case False with 2(2) have "x ∈ set [y←zs . f z ≠ f y]" by auto from 2(1)[OF this] show ?thesis by auto qed auto qed auto lemma take_nth_drop_concat: assumes "i < length xss" and "xss ! i = ys" and "j < length ys" and "ys ! j = z" shows "∃k < length (concat xss). take k (concat xss) = concat (take i xss) @ take j ys ∧ concat xss ! k = xss ! i ! j ∧ drop (Suc k) (concat xss) = drop (Suc j) ys @ concat (drop (Suc i) xss)" using assms(1, 2) proof (induct xss arbitrary: i rule: List.rev_induct) case (snoc xs xss) then show ?case using assms by (cases "i < length xss") (auto simp: nth_append) qed simp lemma concat_map_empty [simp]: "concat (map (λ_. []) xs) = []" by simp lemma map_upt_len_same_len_conv: assumes "length xs = length ys" shows "map (λi. f (xs ! i)) [0 ..< length ys] = map f xs" unfolding assms [symmetric] by (rule map_upt_len_conv) lemma concat_map_concat [simp]: "concat (map concat xs) = concat (concat xs)" by (induct xs) simp_all lemma concat_concat_map: "concat (concat (map f xs)) = concat (map (concat ∘ f) xs)" by (induct xs) simp_all lemma UN_upt_len_conv [simp]: "length xs = n ⟹ (⋃i ∈ {0 ..< n}. f (xs ! i)) = ⋃(set (map f xs))" by (force simp: in_set_conv_nth) lemma Ball_at_Least0LessThan_conv [simp]: "length xs = n ⟹ (∀i ∈ {0 ..< n}. P (xs ! i)) ⟷ (∀x ∈ set xs. P x)" by (metis atLeast0LessThan in_set_conv_nth lessThan_iff) lemma sum_list_replicate_length [simp]: "sum_list (replicate (length xs) (Suc 0)) = length xs" by (induct xs) simp_all lemma list_all2_in_set2: assumes "list_all2 P xs ys" and "y ∈ set ys" obtains x where "x ∈ set xs" and "P x y" using assms by (induct) auto lemma map_eq_conv': "map f xs = map g ys ⟷ length xs = length ys ∧ (∀i < length xs. f (xs ! i) = g (ys ! i))" using map_equality_iff map_equality_iff nth_map_conv by auto lemma list_3_cases[case_names Nil 1 2]: assumes "xs = [] ⟹ P" and "⋀x. xs = [x] ⟹ P" and "⋀x y ys. xs = x#y#ys ⟹ P" shows P using assms by (rule remdups_adj.cases) lemma list_4_cases[case_names Nil 1 2 3]: assumes "xs = [] ⟹ P" and "⋀x. xs = [x] ⟹ P" and "⋀x y. xs = [x,y] ⟹ P" and "⋀x y z zs. xs = x # y # z # zs ⟹ P" shows P using assms by (cases xs; cases "tl xs"; cases "tl (tl xs)", auto) lemma foldr_append2 [simp]: "foldr ((@) ∘ f) xs (ys @ zs) = foldr ((@) ∘ f) xs ys @ zs" by (induct xs) simp_all lemma foldr_append2_Nil [simp]: "foldr ((@) ∘ f) xs [] @ zs = foldr ((@) ∘ f) xs zs" unfolding foldr_append2 [symmetric] by simp lemma UNION_set_zip: "(⋃x ∈ set (zip [0..<length xs] (map f xs)). g x) = (⋃i < length xs. g (i, f (xs ! i)))" by (auto simp: set_conv_nth) lemma zip_fst: "p ∈ set (zip as bs) ⟹ fst p ∈ set as" by (metis in_set_zipE prod.collapse) lemma zip_snd: "p ∈ set (zip as bs) ⟹ snd p ∈ set bs" by (metis in_set_zipE prod.collapse) lemma zip_size_aux: "size_list (size o snd) (zip ts ls) ≤ (size_list size ls)" proof (induct ls arbitrary: ts) case (Cons l ls ts) thus ?case by (cases ts, auto) qed auto text‹We definie the function that remove the nth element of a list. It uses take and drop and the soundness is therefore not too hard to prove thanks to the already existing lemmas.› definition remove_nth :: "nat ⇒ 'a list ⇒ 'a list" where "remove_nth n xs ≡ (take n xs) @ (drop (Suc n) xs)" declare remove_nth_def[simp] lemma remove_nth_len: assumes i: "i < length xs" shows "length xs = Suc (length (remove_nth i xs))" proof - show ?thesis unfolding arg_cong[where f = "length", OF id_take_nth_drop[OF i]] unfolding remove_nth_def by simp qed lemma remove_nth_length : assumes n_bd: "n < length xs" shows "length (remove_nth n xs) = length xs - 1" using n_bd by force lemma remove_nth_id : "length xs ≤ n ⟹ remove_nth n xs = xs" by simp lemma remove_nth_sound_l : assumes p_ub: "p < n" shows "(remove_nth n xs) ! p = xs ! p" proof (cases "n < length xs") case True from length_take and True have ltk: "length (take n xs) = n" by simp { assume pltn: "p < n" from this and ltk have plttk: "p < length (take n xs)" by simp with nth_append[of "take n xs" _ p] have "((take n xs) @ (drop (Suc n) xs)) ! p = take n xs ! p" by auto with pltn and nth_take have "((take n xs) @ (drop (Suc n) xs)) ! p = xs ! p" by simp } from this and ltk and p_ub show ?thesis by simp next case False hence "length xs ≤ n" by arith with remove_nth_id show ?thesis by force qed lemma remove_nth_sound_r : assumes "n ≤ p" and "p < length xs" shows "(remove_nth n xs) ! p = xs ! (Suc p)" proof- from ‹n ≤ p› and ‹p < length xs› have n_ub: "n < length xs" by arith from length_take and n_ub have ltk: "length (take n xs) = n" by simp from ‹n ≤ p› and ltk and nth_append[of "take n xs" _ p] have Hrew: "((take n xs) @ (drop (Suc n) xs)) ! p = drop (Suc n) xs ! (p - n)" by auto from ‹n ≤ p› have idx: "Suc n + (p - n) = Suc p" by arith from ‹p < length xs› have Sp_ub: "Suc p ≤ length xs" by arith from idx and Sp_ub and nth_drop have Hrew': "drop (Suc n) xs ! (p - n) = xs ! (Suc p)" by simp from Hrew and Hrew' show ?thesis by simp qed lemma nth_remove_nth_conv: assumes "i < length (remove_nth n xs)" shows "remove_nth n xs ! i = xs ! (if i < n then i else Suc i)" using assms remove_nth_sound_l remove_nth_sound_r[of n i xs] by auto lemma remove_nth_P_compat : assumes aslbs: "length as = length bs" and Pab: "∀i. i < length as ⟶ P (as ! i) (bs ! i)" shows "∀i. i < length (remove_nth p as) ⟶ P (remove_nth p as ! i) (remove_nth p bs ! i)" proof (cases "p < length as") case True hence p_ub: "p < length as" by assumption with remove_nth_length have lr_ub: "length (remove_nth p as) = length as - 1" by auto { fix i assume i_ub: "i < length (remove_nth p as)" have "P (remove_nth p as ! i) (remove_nth p bs ! i)" proof (cases "i < p") case True from i_ub and lr_ub have i_ub2: "i < length as" by arith from i_ub2 and Pab have P: "P (as ! i) (bs ! i)" by blast from P and remove_nth_sound_l[OF True, of as] and remove_nth_sound_l[OF True, of bs] show ?thesis by simp next case False hence p_ub2: "p ≤ i" by arith from i_ub and lr_ub have Si_ub: "Suc i < length as" by arith with Pab have P: "P (as ! Suc i) (bs ! Suc i)" by blast from i_ub and lr_ub have i_uba: "i < length as" by arith from i_uba and aslbs have i_ubb: "i < length bs" by simp from P and p_ub and aslbs and remove_nth_sound_r[OF p_ub2 i_uba] and remove_nth_sound_r[OF p_ub2 i_ubb] show ?thesis by auto qed } thus ?thesis by simp next case False hence p_lba: "length as ≤ p" by arith with aslbs have p_lbb: "length bs ≤ p" by simp from remove_nth_id[OF p_lba] and remove_nth_id[OF p_lbb] and Pab show ?thesis by simp qed declare remove_nth_def[simp del] definition adjust_idx :: "nat ⇒ nat ⇒ nat" where "adjust_idx i j ≡ (if j < i then j else (Suc j))" definition adjust_idx_rev :: "nat ⇒ nat ⇒ nat" where "adjust_idx_rev i j ≡ (if j < i then j else j - Suc 0)" lemma adjust_idx_rev1: "adjust_idx_rev i (adjust_idx i j) = j" using adjust_idx_def adjust_idx_rev_def by auto lemma adjust_idx_rev2: assumes "j ≠ i" shows "adjust_idx i (adjust_idx_rev i j) = j" using adjust_idx_def adjust_idx_rev_def assms by auto lemma adjust_idx_i: "adjust_idx i j ≠ i" using adjust_idx_def lessI less_irrefl_nat by auto lemma adjust_idx_nth: assumes i: "i < length xs" shows "remove_nth i xs ! j = xs ! adjust_idx i j" (is "?l = ?r") proof - let ?j = "adjust_idx i j" from i have ltake: "length (take i xs) = i" by simp note nth_xs = arg_cong[where f = "λ xs. xs ! ?j", OF id_take_nth_drop[OF i], unfolded nth_append ltake] show ?thesis proof (cases "j < i") case True hence j: "?j = j" unfolding adjust_idx_def by simp show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake using True by simp next case False hence j: "?j = Suc j" unfolding adjust_idx_def by simp from i have lxs: "min (length xs) i = i" by simp show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append using False by (simp add: lxs) qed qed lemma adjust_idx_rev_nth: assumes i: "i < length xs" and ji: "j ≠ i" shows "remove_nth i xs ! adjust_idx_rev i j = xs ! j" (is "?l = ?r") by (simp add: adjust_idx_nth adjust_idx_rev2 i ji) lemma adjust_idx_length: assumes i: "i < length xs" and j: "j < length (remove_nth i xs)" shows "adjust_idx i j < length xs" using adjust_idx_def i j remove_nth_len by fastforce lemma adjust_idx_rev_length: assumes "i < length xs" and "j < length xs" and "j ≠ i" shows "adjust_idx_rev i j < length (remove_nth i xs)" by (metis adjust_idx_def adjust_idx_rev2 assms not_less_eq remove_nth_len) text‹If a binary relation holds on two couples of lists, then it holds on the concatenation of the two couples.› lemma P_as_bs_extend: assumes lab: "length as = length bs" and lcd: "length cs = length ds" and nsab: "∀i. i < length bs ⟶ P (as ! i) (bs ! i)" and nscd: "∀i. i < length ds ⟶ P (cs ! i) (ds ! i)" shows "∀i. i < length (bs @ ds) ⟶ P ((as @ cs) ! i) ((bs @ ds) ! i)" by (simp add: lab nsab nscd nth_append) text‹Extension of filter and partition to binary relations.› fun filter2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ ('a list × 'b list)" where "filter2 P [] _ = ([], [])" | "filter2 P _ [] = ([], [])" | "filter2 P (a # as) (b # bs) = (if P a b then (a # fst (filter2 P as bs), b # snd (filter2 P as bs)) else filter2 P as bs)" lemma filter2_length: "length (fst (filter2 P as bs)) ≡ length (snd (filter2 P as bs))" proof (induct as arbitrary: bs) case Nil show ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases bs) case Nil thus ?thesis by simp next case (Cons b bs) thus ?thesis proof