# Theory Missing_List

(* 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 (hide_lams, 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" proof - from assms have "i - length xs > 0" by auto then obtain j where j: "i - length xs = Suc j" by (cases "i - length xs", auto) thus ?thesis by (simp add: nth_append) qed lemma append_Cons_nth_not_middle: assumes "i ≠ length xs" shows "(xs @ u # ys) ! i = (xs @ z # ys) ! i" proof (cases "i < length xs") case True thus ?thesis by (simp add: append_Cons_nth_left) next case False with assms have "i > length xs" by arith thus ?thesis by (rule append_Cons_nth_right) qed 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 (induct ss) auto 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 id: "min_list (y # ys) = min y (min_list ys)" by auto show ?thesis proof (cases "x = y") case True show ?thesis unfolding id True by auto next case False have "min y (min_list ys) ≤ min_list ys" by auto also have "... ≤ x" using oCons False by auto finally show ?thesis unfolding id . qed 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)" proof (cases xs) case Nil with len have ys: "ys = []" by simp with xy Nil show ?thesis by simp next case (Cons x' xs') with len obtain y' ys' where ys: "ys = y' # ys'" by (cases ys, auto) from Cons have one: "min_list (x # xs) = min x (min_list xs)" by auto from ys have two: "min_list (y # ys) = min y (min_list ys)" by auto show ?thesis unfolding one two using xy xsys unfolding min_def by auto qed 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" proof - from subset mem have "xs ≠ []" by auto from min_list_ex[OF this] obtain x where x: "x ∈ set xs" and mx: "min_list xs = x" by auto from min_list[OF mem] have two: "min_list ys ≤ min_list xs" by auto from mem have "ys ≠ []" by auto from min_list_ex[OF this] obtain y where y: "y ∈ set ys" and my: "min_list ys = y" by auto from y subset have "y ∈ set xs" by auto from min_list[OF this] have one: "min_list xs ≤ y" by auto from one two show ?thesis unfolding mx my by auto qed 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))" by (auto dest: map_eq_imp_length_eq map_nth_conv simp: nth_map_conv) 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 (cases xs; cases "tl xs", auto) 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 (cases p, rule set_zip_leftD, simp) lemma zip_snd: "p ∈ set (zip as bs) ⟹ snd p ∈ set bs" by (cases p, rule set_zip_rightD, simp) 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" proof- from length_take have ll:"n < length xs ⟶ length (take n xs) = n" by auto from length_drop have lr: "length (drop (Suc n) xs) = length xs - (Suc n)" by simp from ll and lr and length_append and n_bd show ?thesis by auto qed lemma remove_nth_id : "length xs ≤ n ⟹ remove_nth n xs = xs" using take_all drop_all append_Nil2 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" unfolding adjust_idx_def adjust_idx_rev_def by (cases "i < j", auto) lemma adjust_idx_rev2: assumes "j ≠ i" shows "adjust_idx i (adjust_idx_rev i j) = j" unfolding adjust_idx_def adjust_idx_rev_def using assms by (cases "i < j", auto) lemma adjust_idx_i: "adjust_idx i j ≠ i" unfolding adjust_idx_def by (cases "j < i", 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") proof - let ?j = "adjust_idx_rev 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_rev_def by simp show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake using True by simp next case False with ji have ji: "j > i" by auto hence j: "?j = j - Suc 0" unfolding adjust_idx_rev_def by simp show ?thesis unfolding nth_xs unfolding j remove_nth_def nth_append ltake using ji by auto qed qed 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 j unfolding remove_nth_len[OF i] adjust_idx_def by (cases "j < i", auto) 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)" using assms by (cases "j < i") (simp_all add: adjust_idx_rev_def remove_nth_len[OF assms(1)]) 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)" proof- { fix i assume i_bd: "i < length (bs @ ds)" have "P ((as @ cs) ! i) ((bs @ ds) ! i)" proof (cases "i < length as") case True with nth_append and nsab and lab show ?thesis by metis next case False with lab and lcd and i_bd and length_append[of bs ds] have "(i - length as) < length cs" by arith with False and nth_append[of _ _ i] and lab and lcd and nscd[rule_format] show ?thesis by metis qed } thus ?thesis by clarify qed 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 (cases "P a b") case True with Cons and IH show ?thesis by simp next case False with Cons and IH show ?thesis by simp qed qed qed lemma filter2_sound: "∀i. i < length (fst (filter2 P as bs)) ⟶ P (fst (filter2 P as bs) ! i) (snd (filter2 P as bs) ! i)" proof (induct as arbitrary: bs) case Nil thus ?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 (cases "P a b") case False with Cons and IH show ?thesis by simp next case True { fix i assume i_bd: "i < length (fst (filter2 P (a # as) (b # bs)))" have "P (fst (filter2 P (a # as) (b # bs)) ! i) (snd (filter2 P (a # as) (b # bs)) ! i)" proof (cases i) case 0 with True show ?thesis by simp next case (Suc j) with i_bd and True have "j < length (fst (filter2 P as bs))" by auto with Suc and IH and True show ?thesis by simp qed } with Cons show ?thesis by simp qed qed qed definition partition2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ ('a list × 'b list) × ('a list × 'b list)" where "partition2 P as bs ≡ ((filter2 P as bs) , (filter2 (λa b. ¬ (P a b)) as bs))" lemma partition2_sound_P: "∀i. i < length (fst (fst (partition2 P as bs))) ⟶ P (fst (fst (partition2 P as bs)) ! i) (snd (fst (partition2 P as bs)) ! i)" proof- from filter2_sound show ?thesis unfolding partition2_def by simp qed lemma partition2_sound_nP: "∀i. i < length (fst (snd (partition2 P as bs))) ⟶ ¬ P (fst (snd (partition2 P as bs)) ! i) (snd (snd (partition2 P as bs)) ! i)" proof- from filter2_sound show ?thesis unfolding partition2_def by simp qed text‹Membership decision function that actually returns the value of the index where the value can be found.› fun mem_idx :: "'a ⇒ 'a list ⇒ nat Option.option" where "mem_idx _ [] = None" | "mem_idx x (a # as) = (if x = a then Some 0 else map_option Suc (mem_idx x as))" lemma mem_idx_sound_output: assumes "mem_idx x as = Some i" shows "i < length as ∧ as ! i = x" using assms proof (induct as arbitrary: i) case Nil thus ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases "x = a") case True with IH(2) show ?thesis by simp next case False note neq_x_a = this show ?thesis proof (cases "mem_idx x as") case None with IH(2) and neq_x_a show ?thesis by simp next case (Some j) with IH(2) and neq_x_a have "i = Suc j" by simp with IH(1) and Some show ?thesis by simp qed qed qed lemma mem_idx_sound_output2: assumes "mem_idx x as = Some i" shows "∀j. j < i ⟶ as ! j ≠ x" using assms proof (induct as arbitrary: i) case Nil thus ?case by simp next case (Cons a as) note IH = this thus ?case proof (cases "x = a") case True with IH show ?thesis by simp next case False note neq_x_a = this show ?thesis proof (cases "mem_idx x as") case None with IH(2) and neq_x_a show ?thesis by simp next case (Some j) with IH(2) and neq_x_a have eq_i_Sj: "i = Suc j" by simp { fix k assume k_bd: "k < i" have "(a # as) ! k ≠ x" proof (cases k) case 0 with neq_x_a show ?thesis by simp next case (Suc l) with k_bd and eq_i_Sj have l_bd: "l < j" by arith with IH(1) and Some have "as ! l ≠ x" by simp with Suc show ?thesis by simp qed } thus ?thesis by simp qed qed qed lemma mem_idx_sound: "(x ∈ set as) = (∃i. mem_idx x as = Some i)" proof (induct as) case Nil thus ?case by simp next case (Cons a as) note IH = this show ?case proof (cases "x = a") case True thus ?thesis by simp next case False { assume "x ∈ set (a # as)" with False have "x ∈ set as" by simp with IH obtain i where Some_i: "mem_idx x as = Some i" by auto with False have "mem_idx x (a # as) = Some (Suc i)" by simp hence "∃i. mem_idx x (a # as) = Some i" by simp } moreover { assume "∃i. mem_idx x (a # as) = Some i" then obtain i where Some_i: "mem_idx x (a # as) = Some i" by fast have "x ∈ set as" proof (cases i) case 0 with mem_idx_sound_output[OF Some_i] and False show ?thesis by simp next case (Suc j) with Some_i and False have "mem_idx x as = Some j" by simp hence "∃i. mem_idx x as = Some i" by simp with IH show ?thesis by simp qed hence "x ∈ set (a # as)" by simp } ultimately show ?thesis by fast qed qed lemma mem_idx_sound2: "(x ∉ set as) = (mem_idx x as = None)" unfolding mem_idx_sound by auto lemma sum_list_replicate_mono: assumes "w1 ≤ (w2 :: nat)" shows "sum_list (replicate n w1) ≤ sum_list (replicate n w2)" proof (induct n) case (Suc n) thus ?case using ‹w1 ≤ w2› by auto qed simp lemma all_gt_0_sum_list_map: assumes *: "⋀x. f x > (0::nat)" and x: "x ∈ set xs" and len: "1 < length xs" shows "f x < (∑x←xs. f x)" using x len proof (induct xs) case (Cons y xs) show ?case proof (cases "y = x") case True with *[of "hd xs"] Cons(3) show ?thesis by (cases xs, auto) next case False with Cons(2) have x: "x ∈ set xs" by auto then obtain z zs where xs: "xs = z # zs" by (cases xs, auto) show ?thesis proof (cases "length zs") case 0 with x xs *[of y] show ?thesis by auto next case (Suc n) with xs have "1 < length xs" by auto from Cons(1)[OF x this] show ?thesis by simp qed qed qed simp lemma finite_distinct: "finite { xs . distinct xs ∧ set xs = X}" (is "finite (?S X)") proof (cases "finite X") case False with finite_set have id: "?S X = {}" by auto show ?thesis unfolding id by auto next case True show ?thesis proof (induct rule: finite_induct[OF True]) case (2 x X) let ?L = "{0..< card (insert x X)} × ?S X" from 2(3) have fin: "finite ?L" by auto let ?f = "λ (i,xs). take i xs @ x # drop i xs" show ?case proof (rule finite_surj[OF fin, of _ ?f], rule) fix xs assume "xs ∈ ?S (insert x X)" hence dis: "distinct xs" and set: "set xs = insert x X" by auto from distinct_card[OF dis] have len: "length xs = card (set xs)" by auto from set[unfolded set_conv_nth] obtain i where x: "x = xs ! i" and i: "i < length xs" by auto from i have min: "min (length xs) i = i" by simp let ?ys = "take i xs @ drop (Suc i) xs" from id_take_nth_drop[OF i] have xsi: "xs = take i xs @ xs ! i # drop (Suc i) xs" . also have "... = ?f (i,?ys)" unfolding split by (simp add: min x) finally have xs: "xs = ?f (i,?ys)" . show "xs ∈ ?f ` ?L" proof (rule image_eqI, rule xs, rule SigmaI) show "i ∈ {0..<card (insert x X)}" using i[unfolded len] set[symmetric] by simp next from dis xsi have disxsi: "distinct (take i xs @ xs ! i # drop (Suc i) xs)" by simp note disxsi = disxsi[unfolded distinct_append x[symmetric]] have xys: "x ∉ set ?ys" using disxsi by auto from distinct_take_drop[OF dis i] have disys: "distinct ?ys" . have "insert x (set ?ys) = set xs" unfolding arg_cong[OF xsi, of set] x by simp hence "insert x (set ?ys) = insert x X" unfolding set by simp from this[unfolded insert_eq_iff[OF xys 2(2)]] show "?ys ∈ ?S X" using disys by auto qed qed qed simp qed lemma finite_distinct_subset: assumes "finite X" shows "finite { xs . distinct xs ∧ set xs ⊆ X}" (is "finite (?S X)") proof - let ?X = "{ { xs. distinct xs ∧ set xs = Y} | Y. Y ⊆ X}" have id: "?S X = ⋃ ?X" by blast show ?thesis unfolding id proof (rule finite_Union) show "finite ?X" using assms by auto next fix M assume "M ∈ ?X" with finite_distinct show "finite M" by auto qed qed lemma map_of_filter: assumes "P x" shows "map_of [(x',y) ← ys. P x'] x = map_of ys x" proof (induct ys) case (Cons xy ys) obtain x' y where xy: "xy = (x',y)" by force show ?case by (cases "x' = x", insert assms xy Cons, auto) qed simp lemma set_subset_insertI: "set xs ⊆ set (List.insert x xs)" by auto lemma set_removeAll_subset: "set (removeAll x xs) ⊆ set xs" by auto lemma map_of_append_Some: "map_of xs y = Some z ⟹ map_of (xs @ ys) y = Some z" by (induction xs) auto lemma map_of_append_None: "map_of xs y = None ⟹ map_of (xs @ ys) y = map_of ys y" by (induction xs) auto end

# Theory Missing_Multiset

(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Preliminaries› subsection ‹Missing Multiset› text ‹This theory provides some definitions and lemmas on multisets which we did not find in the Isabelle distribution.› theory Missing_Multiset imports "HOL-Library.Multiset" Missing_List begin lemma remove_nth_soundness: assumes "n < length as" shows "mset (remove_nth n as) = mset as - {#(as!n)#}" using assms proof (induct as arbitrary: n) case (Cons a as) note [simp] = remove_nth_def show ?case proof (cases n) case (Suc n) with Cons have n_bd: "n < length as" by auto with Cons have "mset (remove_nth n as) = mset as - {#as ! n#}" by auto hence G: "mset (remove_nth (Suc n) (a # as)) = mset as - {#as ! n#} + {#a#}" by simp thus ?thesis proof (cases "a = as!n") case True with G and Suc and insert_DiffM2[symmetric] and insert_DiffM2[of _ "{#as ! n#}"] and nth_mem_mset[of n as] and n_bd show ?thesis by auto next case False from G and Suc and diff_union_swap[OF this[symmetric], symmetric] show ?thesis by simp qed qed auto qed auto lemma multiset_subset_insert: "{ps. ps ⊆# add_mset x xs} = {ps. ps ⊆# xs} ∪ add_mset x ` {ps. ps ⊆# xs}" (is "?l = ?r") proof - { fix ps have "(ps ∈ ?l) = (ps ⊆# xs + {# x #})" by auto also have "… = (ps ∈ ?r)" proof (cases "x ∈# ps") case True then obtain qs where ps: "ps = qs + {#x#}" by (metis insert_DiffM2) show ?thesis unfolding ps mset_subset_eq_mono_add_right_cancel by (auto dest: mset_subset_eq_insertD) next case False hence id: "(ps ⊆# xs + {#x#}) = (ps ⊆# xs)" by (simp add: subset_mset.inf.absorb_iff2 inter_add_left1) show ?thesis unfolding id using False by auto qed finally have "(ps ∈ ?l) = (ps ∈ ?r)" . } thus ?thesis by auto qed lemma multiset_of_subseqs: "mset ` set (subseqs xs) = { ps. ps ⊆# mset xs}" proof (induct xs) case (Cons x xs) show ?case (is "?l = ?r") proof - have id: "?r = {ps. ps ⊆# mset xs} ∪ (add_mset x) ` {ps. ps ⊆# mset xs}" by (simp add: multiset_subset_insert) show ?thesis unfolding id Cons[symmetric] by (auto simp add: Let_def) (metis UnCI image_iff mset.simps(2)) qed qed simp lemma remove1_mset: "w ∈ set vs ⟹ mset (remove1 w vs) + {#w#} = mset vs" by (induct vs) auto lemma fold_remove1_mset: "mset ws ⊆# mset vs ⟹ mset (fold remove1 ws vs) + mset ws = mset vs" proof (induct ws arbitrary: vs) case (Cons w ws vs) from Cons(2) have "w ∈ set vs" using set_mset_mono by force from remove1_mset[OF this] have vs: "mset vs = mset (remove1 w vs) + {#w#}" by simp from Cons(2)[unfolded vs] have "mset ws ⊆# mset (remove1 w vs)" by auto from Cons(1)[OF this,symmetric] show ?case unfolding vs by (simp add: ac_simps) qed simp lemma subseqs_sub_mset: "ws ∈ set (subseqs vs) ⟹ mset ws ⊆# mset vs" proof (induct vs arbitrary: ws) case (Cons v vs Ws) note mem = Cons(2) note IH = Cons(1) show ?case proof (cases Ws) case (Cons w ws) show ?thesis proof (cases "v = w") case True from mem Cons have "ws ∈ set (subseqs vs)" by (auto simp: Let_def Cons_in_subseqsD[of _ ws vs]) from IH[OF this] show ?thesis unfolding Cons True by simp next case False with mem Cons have "Ws ∈ set (subseqs vs)" by (auto simp: Let_def Cons_in_subseqsD[of _ ws vs]) note IH = mset_subset_eq_count[OF IH[OF this]] with IH[of v] show ?thesis by (intro mset_subset_eqI, auto, linarith) qed qed simp qed simp lemma filter_mset_inequality: "filter_mset f xs ≠ xs ⟹ ∃ x ∈# xs. ¬ f x" by (induct xs, auto) end

# Theory Precomputation

subsection Precomputation text ‹This theory contains precomputation functions, which take another function $f$ and a finite set of inputs, and provide the same function $f$ as output, except that now all values $f\ i$ are precomputed if $i$ is contained in the set of finite inputs.› theory Precomputation imports Containers.RBT_Set2 "HOL-Library.RBT_Mapping" begin lemma lookup_tabulate: "x ∈ set xs ⟹ Mapping.lookup (Mapping.tabulate xs f) x = Some (f x)" by (transfer, simp add: map_of_map_Pair_key) lemma lookup_tabulate2: "Mapping.lookup (Mapping.tabulate xs f) x = Some y ⟹ y = f x" by transfer (metis map_of_map_Pair_key option.distinct(1) option.sel) definition memo_int :: "int ⇒ int ⇒ (int ⇒ 'a) ⇒ (int ⇒ 'a)" where "memo_int low up f ≡ let m = Mapping.tabulate [low .. up] f in (λ x. if x ≥ low ∧ x ≤ up then the (Mapping.lookup m x) else f x)" lemma memo_int[simp]: "memo_int low up f = f" proof (intro ext) fix x show "memo_int low up f x = f x" proof (cases "x ≥ low ∧ x ≤ up") case False thus ?thesis unfolding memo_int_def by auto next case True from True have x: "x ∈ set [low .. up]" by auto with True lookup_tabulate[OF this, of f] show ?thesis unfolding memo_int_def by auto qed qed definition memo_nat :: "nat ⇒ nat ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)" where "memo_nat low up f ≡ let m = Mapping.tabulate [low ..< up] f in (λ x. if x ≥ low ∧ x < up then the (Mapping.lookup m x) else f x)" lemma memo_nat[simp]: "memo_nat low up f = f" proof (intro ext) fix x show "memo_nat low up f x = f x" proof (cases "x ≥ low ∧ x < up") case False thus ?thesis unfolding memo_nat_def by auto next case True from True have x: "x ∈ set [low ..< up]" by auto with True lookup_tabulate[OF this, of f] show ?thesis unfolding memo_nat_def by auto qed qed definition memo :: "'a list ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)" where "memo xs f ≡ let m = Mapping.tabulate xs f in (λ x. case Mapping.lookup m x of None ⇒ f x | Some y ⇒ y)" lemma memo[simp]: "memo xs f = f" proof (intro ext) fix x show "memo xs f x = f x" proof (cases "Mapping.lookup (Mapping.tabulate xs f) x") case None thus ?thesis unfolding memo_def by auto next case (Some y) with lookup_tabulate2[OF this] show ?thesis unfolding memo_def by auto qed qed end

# Theory Order_Polynomial

(* Author: René Thiemann Akihisa Yamada License: BSD *) subsection ‹Order of Polynomial Roots› text ‹We extend the collection of results on the order of roots of polynomials. Moreover, we provide code-equations to compute the order for a given root and polynomial.› theory Order_Polynomial imports Polynomial_Interpolation.Missing_Polynomial begin lemma order_linear[simp]: "order a [:- a, 1:] = Suc 0" unfolding order_def proof (rule Least_equality, intro notI) assume "[:- a, 1:] ^ Suc (Suc 0) dvd [:- a, 1:]" from dvd_imp_degree_le[OF this] show False by auto next fix n assume *: "¬ [:- a, 1:] ^ Suc n dvd [:- a, 1:]" thus "Suc 0 ≤ n" by (cases n, auto) qed declare order_power_n_n[simp] lemma linear_power_nonzero: "[: a, 1 :] ^ n ≠ 0" proof assume "[: a, 1 :]^n = 0" with arg_cong[OF this, of degree, unfolded degree_linear_power] show False by auto qed lemma order_linear_power': "order a ([: b, 1:]^Suc n) = (if b = -a then Suc n else 0)" proof (cases "b = -a") case True thus ?thesis unfolding True order_power_n_n by simp next case False let ?p = "[: b, 1:]^Suc n" from linear_power_nonzero have "?p ≠ 0" . have p: "?p = (∏a← replicate (Suc n) b. [:a, 1:])" by auto { assume "order a ?p ≠ 0" then obtain m where ord: "order a ?p = Suc m" by (cases "order a ?p", auto) from order[OF ‹?p ≠ 0›, of a, unfolded ord] have dvd: "[:- a, 1:] ^ Suc m dvd ?p" by auto from poly_linear_exp_linear_factors[OF dvd[unfolded p]] False have False by auto } hence "order a ?p = 0" by auto with False show ?thesis by simp qed lemma order_linear_power: "order a ([: b, 1:]^n) = (if b = -a then n else 0)" proof (cases n) case (Suc m) show ?thesis unfolding Suc order_linear_power' by simp qed simp lemma order_linear': "order a [: b, 1:] = (if b = -a then 1 else 0)" using order_linear_power'[of a b 0] by simp lemma degree_div_less: assumes p: "(p::'a::field poly) ≠ 0" and dvd: "r dvd p" and deg: "degree r ≠ 0" shows "degree (p div r) < degree p" proof - from dvd obtain q where prq: "p = r * q" unfolding dvd_def by auto have "degree p = degree r + degree q" unfolding prq by (rule degree_mult_eq, insert p prq, auto) with deg have deg: "degree q < degree p" by auto from prq have "q = p div r" using deg p by auto with deg show ?thesis by auto qed lemma order_sum_degree: assumes "p ≠ 0" shows "sum (λ a. order a p) { a. poly p a = 0 } ≤ degree p" proof - define n where "n = degree p" have "degree p ≤ n" unfolding n_def by auto thus ?thesis using ‹p ≠ 0› proof (induct n arbitrary: p) case (0 p) define a where "a = coeff p 0" from 0 have "degree p = 0" by auto hence p: "p = [: a :]" unfolding a_def by (metis degree_0_id) with 0 have "a ≠ 0" by auto thus ?case unfolding p by auto next case (Suc m p) note order = order[OF ‹p ≠ 0›] show ?case proof (cases "∃ a. poly p a = 0") case True then obtain a where root: "poly p a = 0" by auto with order_root[of p a] Suc obtain n where orda: "order a p = Suc n" by (cases "order a p", auto) let ?a = "[: -a, 1 :] ^ Suc n" from order_decomp[OF ‹p ≠ 0›, of a, unfolded orda] obtain q where p: "p = ?a * q" and ndvd: "¬ [:- a, 1:] dvd q" by auto from ‹p ≠ 0›[unfolded p] have nz: "?a ≠ 0" "q ≠ 0" by auto hence deg: "degree p = degree ?a + degree q" unfolding p by (subst degree_mult_eq, auto) have ord: "⋀ a. order a p = order a ?a + order a q" unfolding p by (subst order_mult, insert nz, auto) have roots: "{ a. poly p a = 0 } = insert a ({ a. poly q a = 0} - {a})" using root unfolding p poly_mult by auto have fin: "finite {a. poly q a = 0}" by (rule poly_roots_finite[OF ‹q ≠ 0›]) have "Suc n = order a p" using orda by simp also have "… = Suc n + order a q" unfolding ord order_linear_power' by simp finally have "order a q = 0" by auto with order_root[of q a] ‹q ≠ 0› have qa: "poly q a ≠ 0" by auto have "(∑a∈{a. poly q a = 0} - {a}. order a p) = (∑a∈{a. poly q a = 0} - {a}. order a q)" proof (rule sum.cong[OF refl]) fix b assume "b ∈ {a. poly q a = 0} - {a}" hence "b ≠ a" by auto hence "order b ?a = 0" unfolding order_linear_power' by simp thus "order b p = order b q" unfolding ord by simp qed also have "… = (∑a∈{a. poly q a = 0}. order a q)" using qa by auto also have "… ≤ degree q" by (rule Suc(1)[OF _ ‹q ≠ 0›], insert deg[unfolded degree_linear_power] Suc(2), auto) finally have "(∑a∈{a. poly q a = 0} - {a}. order a p) ≤ degree q" . thus ?thesis unfolding roots deg using fin by (subst sum.insert, simp_all only: degree_linear_power, auto simp: orda) qed auto qed qed lemma order_code[code]: "order (a::'a::idom_divide) p = (if p = 0 then Code.abort (STR ''order of polynomial 0 undefined'') (λ _. order a p) else if poly p a ≠ 0 then 0 else Suc (order a (p div [: -a, 1 :])))" proof (cases "p = 0") case False note p = this note order = order[OF p] show ?thesis proof (cases "poly p a = 0") case True with order_root[of p a] p obtain n where ord: "order a p = Suc n" by (cases "order a p", auto) from this(1) have "[: -a, 1 :] dvd p" using True poly_eq_0_iff_dvd by blast then obtain q where p: "p = [: -a, 1 :] * q" unfolding dvd_def by auto have ord: "order a p = order a [: -a, 1 :] + order a q" using p False order_mult[of "[: -a, 1 :]" q] by auto have q: "p div [: -a, 1 :] = q" using False p by (metis mult_zero_left nonzero_mult_div_cancel_left) show ?thesis unfolding ord q using False True by auto next case False with order_root[of p a] p show ?thesis by auto qed qed auto end

# Theory Explicit_Roots

(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Explicit Formulas for Roots› text ‹We provide algorithms which use the explicit formulas to compute the roots of polynomials of degree up to 2. We also define the formula for polynomials of degree 3, but did not (yet) prove anything about it.› theory Explicit_Roots imports Polynomial_Interpolation.Missing_Polynomial Sqrt_Babylonian.Sqrt_Babylonian begin lemma roots0: assumes p: "p ≠ 0" and p0: "degree p = 0" shows "{x. poly p x = 0} = {}" using degree0_coeffs[OF p0] p by auto definition roots1 :: "'a :: field poly ⇒ 'a" where "roots1 p = (- coeff p 0 / coeff p 1)" lemma roots1: fixes p :: "'a :: field poly" assumes p1: "degree p = 1" shows "{x. poly p x = 0} = {roots1 p}" using degree1_coeffs[OF p1] unfolding roots1_def by (auto simp: add_eq_0_iff nonzero_neg_divide_eq_eq2) lemma roots2: fixes p :: "'a :: field_char_0 poly" assumes p2: "p = [: c, b, a :]" and a: "a ≠ 0" shows "{x. poly p x = 0} = { - ( b / (2 * a)) + e | e. e^2 = ( b / (2 * a))^2 - c/a}" (is "?l = ?r") proof - define b2a where "b2a = b / (2 * a)" { fix x have "(x ∈ ?l) = (x * x * a + x * b + c = 0)" unfolding p2 by (simp add: field_simps) also have "… = ((x * x + 2 * x * b2a) + c/a = 0)" using a by (auto simp: b2a_def field_simps) also have "x * x + 2 * x * b2a = (x * x + 2 * x * b2a + b2a^2) - b2a^2" by simp also have "… = (x + b2a) ^ 2 - b2a ^ 2" by (simp add: field_simps power2_eq_square) also have "(… + c / a = 0) = ((x + b2a) ^ 2 = b2a^2 - c/a)" by algebra also have "… = (x ∈ ?r)" unfolding b2a_def[symmetric] by (auto simp: field_simps) finally have "(x ∈ ?l) = (x ∈ ?r)" . } thus ?thesis by auto qed definition croots2 :: "complex poly ⇒ complex list" where "croots2 p = (let a = coeff p 2; b = coeff p 1; c = coeff p 0; b2a = b / (2 * a); bac = b2a^2 - c/a; e = csqrt bac in remdups [- b2a + e, - b2a - e])" definition complex_rat :: "complex ⇒ bool" where "complex_rat x = (Re x ∈ ℚ ∧ Im x ∈ ℚ)" lemma croots2: assumes "degree p = 2" shows "{x. poly p x = 0} = set (croots2 p)" proof - from degree2_coeffs[OF assms] obtain a b c where p: "p = [:c, b, a:]" and a: "a ≠ 0" by auto note main = roots2[OF p a] have 2: "2 = Suc (Suc 0)" by simp have coeff: "coeff p 2 = a" "coeff p 1 = b" "coeff p 0 = c" unfolding p by (auto simp: 2) let ?b2a = "b / (2 * a)" define b2a where "b2a = ?b2a" let ?bac = "b2a^2 - c/a" define bac where "bac = ?bac" have roots: "set (croots2 p) = {- b2a + csqrt bac, - b2a - csqrt bac}" unfolding croots2_def Let_def coeff b2a_def[symmetric] bac_def[symmetric] by (auto split: if_splits) show ?thesis unfolding roots main b2a_def[symmetric] bac_def[symmetric] using power2_eq_iff by fastforce qed definition rroots2 :: "real poly ⇒ real list" where "rroots2 p = (let a = coeff p 2; b = coeff p 1; c = coeff p 0; b2a = b / (2 * a); bac = b2a^2 - c/a in if bac = 0 then [- b2a] else if bac < 0 then [] else let e = sqrt bac in [- b2a + e, - b2a - e])" definition rat_roots2 :: "rat poly ⇒ rat list" where "rat_roots2 p = (let a = coeff p 2; b = coeff p 1; c = coeff p 0; b2a = b / (2 * a); bac = b2a^2 - c/a in map (λ e. - b2a + e) (sqrt_rat bac))" lemma rroots2: assumes "degree p = 2" shows "{x. poly p x = 0} = set (rroots2 p)" proof - from degree2_coeffs[OF assms] obtain a b c where p: "p = [:c, b, a:]" and a: "a ≠ 0" by auto note main = roots2[OF p a] have 2: "2 = Suc (Suc 0)" by simp have coeff: "coeff p 2 = a" "coeff p 1 = b" "coeff p 0 = c" unfolding p by (auto simp: 2) let ?b2a = "b / (2 * a)" define b2a where "b2a = ?b2a" let ?bac = "b2a^2 - c/a" define bac where "bac = ?bac" have roots: "set (rroots2 p) = (if bac < 0 then {} else {- b2a + sqrt bac, - b2a - sqrt bac})" unfolding rroots2_def Let_def coeff b2a_def[symmetric] bac_def[symmetric] by (auto split: if_splits) show ?thesis unfolding roots main b2a_def[symmetric] bac_def[symmetric] by auto qed lemma rat_roots2: assumes "degree p = 2" shows "{x. poly p x = 0} = set (rat_roots2 p)" proof - from degree2_coeffs[OF assms] obtain a b c where p: "p = [:c, b, a:]" and a: "a ≠ 0" by auto note main = roots2[OF p a] have 2: "2 = Suc (Suc 0)" by simp have coeff: "coeff p 2 = a" "coeff p 1 = b" "coeff p 0 = c" unfolding p by (auto simp: 2) let ?b2a = "b / (2 * a)" define b2a where "b2a = ?b2a" let ?bac = "b2a^2 - c/a" define bac where "bac = ?bac" have roots: "(rat_roots2 p) = (map (λ e. -b2a + e) (sqrt_rat bac))" unfolding rat_roots2_def Let_def coeff b2a_def[symmetric] bac_def[symmetric] by auto show ?thesis unfolding roots main b2a_def[symmetric] bac_def[symmetric] by (auto simp: power2_eq_square) qed text ‹Determinining roots of complex polynomials of degree up to 2.› definition croots :: "complex poly ⇒ complex list" where "croots p = (if p = 0 ∨ degree p > 2 then [] else (if degree p = 0 then [] else if degree p = 1 then [roots1 p] else croots2 p))" lemma croots: assumes "p ≠ 0" "degree p ≤ 2" shows "set (croots p) = {x. poly p x = 0}" using assms unfolding croots_def using roots0[of p] roots1[of p] croots2[of p] by (auto split: if_splits) text ‹Determinining roots of real polynomials of degree up to 2.› definition rroots :: "real poly ⇒ real list" where "rroots p = (if p = 0 ∨ degree p > 2 then [] else (if degree p = 0 then [] else if degree p = 1 then [roots1 p] else rroots2 p))" lemma rroots: assumes "p ≠ 0" "degree p ≤ 2" shows "set (rroots p) = {x. poly p x = 0}" using assms unfolding rroots_def using roots0[of p] roots1[of p] rroots2[of p] by (auto split: if_splits) text ‹Although there is a closed form for cubic roots, which is specified below, we did not yet integrate it into the @{const croots} and @{const rroots} algorithms. One obstracle is that for complex numbers, the cubic root is not even defined. Therefore, we also did not proof soundness of the croots3 algorithm.› context fixes croot :: "nat ⇒ complex ⇒ complex" begin definition croots3 :: "complex poly ⇒ complex × complex × complex × complex" where "croots3 p = (let a = coeff p 3; b = coeff p 2; c = coeff p 1; d = coeff p 0; Δ⇩_{0}= b^2 - 3 * a * c; Δ⇩_{1}= 2 * b^3 - 9 * a * b * c + 27 * a^2 * d; C = croot 3 ((Δ⇩_{1}+ csqrt ( Δ⇩_{1}^2 - 4 * Δ⇩_{0}^3)) / 2); u⇩_{1}= 1; u⇩_{2}= (-1 + 𝗂 * csqrt 3) / 2; u⇩_{3}= (-1 - 𝗂 * csqrt 3) / 2; x⇩_{k}= (λ u. (-1 / (3 * a)) * (b + u * C + Δ⇩_{0}/ (u * C))) in (x⇩_{k}u⇩_{1}, x⇩_{k}u⇩_{2}, x⇩_{k}u⇩_{3}, a))" end end

# Theory Dvd_Int_Poly

(* Author: Sebastiaan Joosten René Thiemann License: BSD *) section ‹Division of Polynomials over Integers› text ‹This theory contains an algorithm to efficiently compute divisibility of two integer polynomials.› theory Dvd_Int_Poly imports Polynomial_Interpolation.Ring_Hom_Poly Polynomial_Interpolation.Divmod_Int Polynomial_Interpolation.Is_Rat_To_Rat begin definition div_int_poly_step :: "int poly ⇒ int ⇒ (int poly × int poly) option ⇒ (int poly × int poly) option" where "div_int_poly_step q = (λa sro. case sro of Some (s, r) ⇒ let ar = pCons a r; (b,m) = divmod_int (coeff ar (degree q)) (coeff q (degree q)) in if m = 0 then Some (pCons b s, ar - smult b q) else None | None ⇒ None)" declare div_int_poly_step_def[code_unfold] definition div_mod_int_poly :: "int poly ⇒ int poly ⇒ (int poly × int poly) option" where "div_mod_int_poly p q = (if q = 0 then None else (let n = degree q; qn = coeff q n in fold_coeffs (div_int_poly_step q) p (Some (0, 0))))" definition div_int_poly :: "int poly ⇒ int poly ⇒ int poly option" where "div_int_poly p q = (case div_mod_int_poly p q of None ⇒ None | Some (d,m) ⇒ if m = 0 then Some d else None)" definition div_rat_poly_step :: "'a::field poly ⇒ 'a ⇒ 'a poly × 'a poly ⇒ 'a poly × 'a poly" where "div_rat_poly_step q = (λa (s, r). let b = coeff (pCons a r) (degree q) / coeff q (degree q) in (pCons b s, pCons a r - smult b q))" lemma foldr_cong_plus: (* a more elaborate version of foldr_cong. Using f'=id, g'=id and s = set lst would give foldr_cong exactly. *) assumes f_is_g : "⋀ a b c. b ∈ s ⟹ f' a = f b (f' c) ⟹ g' a = g b (g' c)" (* main assumption *) and f'_inj : "⋀ a b. f' a = f' b ⟹ a = b" and f_bit_sur : "⋀ a b c. f' a = f b c ⟹ ∃ c'. c = f' c'" (* should be provable by cases c *) and lst_in_s : "set lst ⊆ s" (* formulated like this to make induction easier *) shows "f' a = foldr f lst (f' b) ⟹ g' a = foldr g lst (g' b)" using lst_in_s proof (induct lst arbitrary: a) case (Cons x xs) have prems: "f' a = (f x ∘ foldr f xs) (f' b)" using Cons.prems unfolding foldr_Cons by auto hence "∃ c'. f' c' = foldr f xs (f' b)" using f_bit_sur by fastforce then obtain c' where c'_def: "f' c' = foldr f xs (f' b)" by blast hence "f' a = f x (f' c')" using prems by simp hence "g' a = g x (g' c')" using f_is_g Cons.prems(2) by simp also have "g' c' = foldr g xs (g' b)" using Cons.hyps[of c'] c'_def Cons.prems(2) by auto finally have "g' a = (g x ∘ foldr g xs) (g' b)" by simp thus ?case using foldr_Cons by simp qed (insert f'_inj, auto) abbreviation (input) rp :: "int poly ⇒ rat poly" where "rp ≡ map_poly rat_of_int" (* fully transitive proof, right to left also holds without the precondition: int_step_then_rat_poly_step Left to right holds if q≠0: rat_poly_step_then_int_step *) lemma rat_int_poly_step_agree : assumes "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0" shows "(rp a1,rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b (rp c1,rp c2) ⟷ Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))" proof - have coeffs: "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0" using assms by auto let ?ri = "rat_of_int" let ?withDiv1 = "pCons (?ri (coeff (pCons b c2) (degree q) div coeff q (degree q))) (rp c1)" let ?withSls1 = "pCons (coeff (pCons (?ri b) (rp c2)) (degree q) / coeff (rp q) (degree q)) (rp c1)" let ?ident1 = "?withDiv1 = ?withSls1" let ?withDiv2 = "rp (pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q)" let ?withSls2 = "pCons (?ri b) (rp c2) - smult (coeff (pCons (?ri b) (rp c2)) (degree q) / coeff (rp q) (degree q)) (rp q)" let ?ident2 = "?withDiv2 = ?withSls2" note simps = div_int_poly_step_def option.simps Let_def prod.simps have id1:"?ri (coeff (pCons b c2) (degree q) div coeff q (degree q)) = ?ri (coeff (pCons b c2) (degree q)) / ?ri (coeff q (degree q))" using coeffs by auto have id2:"?ident1" unfolding id1 by (simp, fold of_int_hom.coeff_map_poly_hom of_int_hom.map_poly_pCons_hom, simp) hence id3:"?ident2" using id2 by (auto simp: hom_distribs) have c1:"((rp (pCons (coeff (pCons b c2) (degree q) div coeff q (degree q)) c1) ,rp (pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q)) = div_rat_poly_step (rp q) (?ri b) (rp c1,rp c2)) ⟷ (?ident1 ∧ ?ident2)" unfolding div_rat_poly_step_def simps by (simp add: hom_distribs) have "((rp a1, rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b (rp c1, rp c2)) ⟷ (rp a1 = ?withSls1 ∧ rp a2 = ?withSls2)" unfolding div_rat_poly_step_def simps by simp also have "… ⟷ ((a1 = pCons (coeff (pCons b c2) (degree q) div coeff q (degree q)) c1) ∧ (a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q))" by (fold id2 id3 of_int_hom.map_poly_pCons_hom, unfold of_int_poly_hom.eq_iff, auto) also have c0:"… ⟷ Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))" unfolding divmod_int_def div_int_poly_step_def option.simps Let_def prod.simps using coeffs by (auto split: option.splits prod.splits if_splits) finally show ?thesis . qed lemma int_step_then_rat_poly_step : assumes Some:"Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))" shows "(rp a1,rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b (rp c1,rp c2)" proof - note simps = div_int_poly_step_def option.simps Let_def divmod_int_def prod.simps from Some[unfolded simps] have mod0: "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0" by (auto split: option.splits prod.splits if_splits) thus ?thesis using assms rat_int_poly_step_agree by auto qed lemma is_int_rat_division : assumes "y ≠ 0" shows "is_int_rat (rat_of_int x / rat_of_int y) ⟷ x mod y = 0" proof assume "is_int_rat (rat_of_int x / rat_of_int y)" then obtain v where v_def:"rat_of_int v = rat_of_int x / rat_of_int y" using int_of_rat(2) is_int_rat by fastforce hence "v = ⌊rat_of_int x / rat_of_int y⌋" by linarith hence "v * y = x - x mod y" using div_is_floor_divide_rat mod_div_equality_int by simp hence "rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)" by (fold hom_distribs, unfold of_int_hom.eq_iff) hence "(rat_of_int x / rat_of_int y) * rat_of_int y = rat_of_int x - rat_of_int (x mod y)" using v_def by simp hence "rat_of_int x = rat_of_int x - rat_of_int (x mod y)" by (simp add: assms) thus "x mod y = 0" by simp qed (force) lemma pCons_of_rp_contains_ints : assumes "rp a = pCons b c" shows "is_int_rat b" proof - have "⋀ b n. rp a = b ⟹ is_int_rat (coeff b n)" by auto hence "rp a = pCons b c ⟹ is_int_rat (coeff (pCons b c) 0)". thus ?thesis using assms by auto qed lemma rat_step_then_int_poly_step : assumes "q ≠ 0" and "(rp a1,rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b2 (rp c1,rp c2)" shows "Some (a1,a2) = div_int_poly_step q b2 (Some (c1,c2))" proof - let ?mustbeint = "rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (coeff q (degree q))" let ?mustbeint2 = "coeff (pCons (rat_of_int b2) (rp c2)) (degree (rp q)) / coeff (rp q) (degree (rp q))" have mustbeint : "?mustbeint = ?mustbeint2" by (fold hom_distribs of_int_hom.coeff_map_poly_hom, simp) note simps = div_int_poly_step_def option.simps Let_def divmod_int_def prod.simps from assms leading_coeff_neq_0[of q] have q0:"coeff q (degree q) ≠ 0" by simp have "rp a1 = pCons ?mustbeint2 (rp c1)" using assms(2) unfolding div_rat_poly_step_def by (simp add:div_int_poly_step_def Let_def) hence "is_int_rat ?mustbeint2" unfolding div_rat_poly_step_def using pCons_of_rp_contains_ints by simp hence "is_int_rat ?mustbeint" unfolding mustbeint by simp hence "coeff (pCons b2 c2) (degree q) mod coeff q (degree q) = 0" using is_int_rat_division q0 by simp thus ?thesis using rat_int_poly_step_agree assms by simp qed lemma div_int_poly_step_surjective : "Some a = div_int_poly_step q b c ⟹ ∃ c'. c = Some c'" unfolding div_int_poly_step_def by(cases c, simp_all) lemma div_mod_int_poly_then_pdivmod: assumes "div_mod_int_poly p q = Some (r,m)" shows "(rp p div rp q, rp p mod rp q) = (rp r, rp m)" and "q ≠ 0" proof - let ?rpp = "(λ (a,b). (rp a,rp b))" let ?p = "rp p" let ?q = "rp q" let ?r = "rp r" let ?m = "rp m" let ?div_rat_step = "div_rat_poly_step ?q" let ?div_int_step = "div_int_poly_step q" from assms show q0 : "q ≠ 0" using div_mod_int_poly_def by auto hence "div_mod_int_poly p q = Some (r,m) ⟷ Some (r,m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))" unfolding div_mod_int_poly_def fold_coeffs_def by (auto split: option.splits prod.splits if_splits) hence innerRes: "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0, 0))" using assms by simp { fix oldRes res :: "int poly × int poly" fix lst :: "int list" have "Some res = foldr ?div_int_step lst (Some oldRes) ⟹ ?rpp res = foldr (?div_rat_step ∘ rat_of_int) lst (?rpp oldRes)" using foldr_cong_plus[of "set lst" Some ?div_int_step ?rpp "?div_rat_step ∘ rat_of_int" lst res oldRes] int_step_then_rat_poly_step div_int_poly_step_surjective by auto hence "Some res = foldr ?div_int_step lst (Some oldRes) ⟹ ?rpp res = foldr ?div_rat_step (map rat_of_int lst) (?rpp oldRes)" using foldr_map[of ?div_rat_step rat_of_int lst] by simp } hence equal_foldr : "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0)) ⟹ ?rpp (r,m) = foldr (?div_rat_step) (map rat_of_int (coeffs p)) (?rpp (0,0))". have "(map rat_of_int (coeffs p) = coeffs ?p)" by simp hence "(?r,?m) = (foldr (?div_rat_step) (coeffs ?p) (0,0))" using equal_foldr innerRes by simp thus "(?p div ?q, ?p mod ?q) = (?r,?m)" using fold_coeffs_def [of "?div_rat_step" ?p] q0 div_mod_fold_coeffs [of ?p ?q] unfolding div_rat_poly_step_def by auto qed lemma div_rat_poly_step_sur: assumes "(case a of (a, b) ⇒ (rp a, rp b)) = (div_rat_poly_step (rp q) ∘ rat_of_int) x pair" shows "∃c'. pair = (case c' of (a, b) ⇒ (rp a, rp b))" proof - obtain b1 b2 where pair: "pair = (b1, b2)" by (cases pair) simp define p12 where "p12 = coeff (pCons (rat_of_int x) b2) (degree (rp q)) / coeff (rp q) (degree (rp q))" obtain a1 a2 where "a = (a1, a2)" by (cases a) simp with assms pair have "(rp a1, rp a2) = div_rat_poly_step (rp q) (rat_of_int x) (b1, b2)" by simp then have a1: "rp a1 = pCons p12 b1" and "rp a2 = pCons (rat_of_int x) b2 - smult p12 (rp q)" by (auto split: prod.splits simp add: Let_def div_rat_poly_step_def p12_def) then obtain p21 p22 where "rp p21 = pCons p22 b2" apply (simp add: field_simps) apply (metis coeff_pCons_0 of_int_hom.map_poly_hom_add of_int_hom.map_poly_hom_smult of_int_hom.coeff_map_poly_hom) done moreover obtain p21' p21q where "p21 = pCons p21' p21q" by (rule pCons_cases) ultimately obtain p2 where "b2 = rp p2 " by (auto simp: hom_distribs) moreover obtain a1' a1q where "a1 = pCons a1' a1q" by (rule pCons_cases) with a1 obtain p1 where "b1 = rp p1" by (auto simp: hom_distribs) ultimately have "pair = (rp p1, rp p2)" using pair by simp then show ?thesis by auto qed lemma pdivmod_then_div_mod_int_poly: assumes q0: "q ≠ 0" and "(rp p div rp q, rp p mod rp q) = (rp r, rp m)" shows "div_mod_int_poly p q = Some (r,m)" proof - let ?rpp = "(λ (a,b). (rp a,rp b))" (* rp pair *) let ?p = "rp p" let ?q = "rp q" let ?r = "rp r" let ?m = "rp m" let ?div_rat_step = "div_rat_poly_step ?q" let ?div_int_step = "div_int_poly_step q" { fix oldRes res :: "int poly × int poly" fix lst :: "int list" have inj: "(⋀a b. (case a of (a, b) ⇒ (rp a, rp b)) = (case b of (a, b) ⇒ (rp a, rp b)) ⟹ a = b)" by auto have "(⋀a b c. b ∈ set lst ⟹ (case a of (a, b) ⇒ (map_poly rat_of_int a, map_poly rat_of_int b)) = (div_rat_poly_step (map_poly rat_of_int q) ∘ rat_of_int) b (case c of (a, b) ⇒ (map_poly rat_of_int a, map_poly rat_of_int b)) ⟹ Some a = div_int_poly_step q b (Some c))" using rat_step_then_int_poly_step[OF q0] by auto hence "?rpp res = foldr (?div_rat_step ∘ rat_of_int) lst (?rpp oldRes) ⟹ Some res = foldr ?div_int_step lst (Some oldRes)" using foldr_cong_plus[of "set lst" ?rpp "?div_rat_step ∘ rat_of_int" Some ?div_int_step lst res oldRes] div_rat_poly_step_sur inj by simp hence "?rpp res = foldr ?div_rat_step (map rat_of_int lst) (?rpp oldRes) ⟹ Some res = foldr ?div_int_step lst (Some oldRes)" using foldr_map[of ?div_rat_step rat_of_int lst] by auto } hence equal_foldr : "?rpp (r,m) = foldr (?div_rat_step) (map rat_of_int (coeffs p)) (?rpp (0,0)) ⟹ Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))" by simp have "(?r,?m) = (foldr (?div_rat_step) (coeffs ?p) (0,0))" using fold_coeffs_def[of "?div_rat_step" ?p] assms div_mod_fold_coeffs [of ?p ?q] unfolding div_rat_poly_step_def by auto hence "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))" using equal_foldr by simp thus ?thesis using q0 unfolding div_mod_int_poly_def by (simp add: fold_coeffs_def) qed lemma div_int_then_rqp: assumes "div_int_poly p q = Some r" shows "r * q = p" and "q ≠ 0" proof - let ?rpp = "(λ (a,b). (rp a,rp b))" (* rp pair *) let ?p = "rp p" let ?q = "rp q" let ?r = "rp r" have "Some (r,0) = div_mod_int_poly p q" using assms unfolding div_int_poly_def by (auto split: option.splits prod.splits if_splits) with div_mod_int_poly_then_pdivmod[of p q r 0] have "?p div ?q = ?r ∧ ?p mod ?q = 0" by simp with div_mult_mod_eq[of ?p ?q] have "?p = ?r * ?q" by auto also have "… = rp (r * q)" by (simp add: hom_distribs) finally have "?p = rp (r * q)". thus "r * q = p" by simp show "q ≠ 0" using assms unfolding div_int_poly_def div_mod_int_poly_def by (auto split: option.splits prod.splits if_splits) qed lemma rqp_then_div_int: assumes "r * q = p" and q0:"q ≠ 0" shows "div_int_poly p q = Some r" proof - let ?rpp = "(λ (a,b). (rp a,rp b))" (* rp pair *) let ?p = "rp p" let ?q = "rp q" let ?r = "rp r" have "?p = ?r * ?q" using assms(1) by (auto simp: hom_distribs) hence "?p div ?q = ?r" and "?p mod ?q = 0" using q0 by simp_all hence "(rp p div rp q, rp p mod rp q) = (rp r, 0)" by (auto split: prod.splits) hence "(rp p div rp q, rp p mod rp q) = (rp r, rp 0)" by simp hence "Some (r,0) = div_mod_int_poly p q" using pdivmod_then_div_mod_int_poly[OF q0,of p r 0] by simp thus ?thesis unfolding div_mod_int_poly_def div_int_poly_def using q0 by (metis (mono_tags, lifting) option.simps(5) split_conv) qed lemma div_int_poly: "(div_int_poly p q = Some r) ⟷ (q ≠ 0 ∧ p = r * q)" using div_int_then_rqp rqp_then_div_int by blast definition dvd_int_poly :: "int poly ⇒ int poly ⇒ bool" where "dvd_int_poly q p = (if q = 0 then p = 0 else div_int_poly p q ≠ None)" lemma dvd_int_poly[simp]: "dvd_int_poly q p = (q dvd p)" unfolding dvd_def dvd_int_poly_def using div_int_poly[of p q] by (cases "q = 0", auto) definition dvd_int_poly_non_0 :: "int poly ⇒ int poly ⇒ bool" where "dvd_int_poly_non_0 q p = (div_int_poly p q ≠ None)" lemma dvd_int_poly_non_0[simp]: "q ≠ 0 ⟹ dvd_int_poly_non_0 q p = (q dvd p)" unfolding dvd_def dvd_int_poly_non_0_def using div_int_poly[of p q] by auto lemma [code_unfold]: "p dvd q ⟷ dvd_int_poly p q" by simp hide_const rp end

# Theory Missing_Polynomial_Factorial

section ‹More on Polynomials› text ‹This theory contains several results on content, gcd, primitive part, etc.. Moreover, there is a slightly improved code-equation for computing the gcd.› theory Missing_Polynomial_Factorial imports "HOL-Computational_Algebra.Polynomial_Factorial" Polynomial_Interpolation.Missing_Polynomial begin text ‹Improved code equation for @{const gcd_poly_code} which avoids computing the content twice.› lemma gcd_poly_code_code[code]: "gcd_poly_code p q = (if p = 0 then normalize q else if q = 0 then normalize p else let c1 = content p; c2 = content q; p' = map_poly (λ x. x div c1) p; q' = map_poly (λ x. x div c2) q in smult (gcd c1 c2) (gcd_poly_code_aux p' q'))" unfolding gcd_poly_code_def Let_def primitive_part_def by simp lemma gcd_smult: fixes f g :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly" defines cf: "cf ≡ content f" and cg: "cg ≡ content g" shows "gcd (smult a f) g = (if a = 0 ∨ f = 0 then normalize g else smult (gcd a (cg div (gcd cf cg))) (gcd f g))" proof (cases "a = 0 ∨ f = 0") case False let ?c = "content" let ?pp = primitive_part let ?ua = "unit_factor a" let ?na = "normalize a" define H where "H = gcd (?c f) (?c g)" have "H dvd ?c f" unfolding H_def by auto then obtain F where fh: "?c f = H * F" unfolding dvd_def by blast from False have cf0: "?c f ≠ 0" by auto hence H: "H ≠ 0" unfolding H_def by auto from arg_cong[OF fh, of "λ f. f div H"] H have F: "F = ?c f div H" by auto have "H dvd ?c g" unfolding H_def by auto then obtain G where gh: "?c g = H * G" unfolding dvd_def by blast from arg_cong[OF gh, of "λ f. f div H"] H have G: "G = ?c g div H" by auto have "coprime F G" using H unfolding F G H_def using cf0 div_gcd_coprime by blast have "is_unit ?ua" using False by simp then have ua: "is_unit [: ?ua :]" by (simp add: is_unit_const_poly_iff) have "gcd (smult a f) g = smult (gcd (?na * ?c f) (?c g)) (gcd (smult ?ua (?pp f)) (?pp g))" unfolding gcd_poly_decompose[of "smult a f"] content_smult primitive_part_smult by simp also have "smult ?ua (?pp f) = ?pp f * [: ?ua :]" by simp also have "gcd … (?pp g) = gcd (?pp f) (?pp g)" unfolding gcd_mult_unit1[OF ua] .. also have "gcd (?na * ?c f) (?c g) = gcd ((?na * F) * H) (G * H)" unfolding fh gh by (simp add: ac_simps) also have "… = gcd (?na * F) G * normalize H" unfolding gcd_mult_right gcd.commute[of G] by (simp add: normalize_mult) also have "normalize H = H" by (metis H_def normalize_gcd) finally have "gcd (smult a f) g = smult (gcd (?na * F) G) (smult H (gcd (?pp f) (?pp g)))" by simp also have "smult H (gcd (?pp f) (?pp g)) = gcd f g" unfolding H_def by (rule gcd_poly_decompose[symmetric]) also have "gcd (?na * F) G = gcd (F * ?na) G" by (simp add: ac_simps) also have "… = gcd ?na G" using ‹coprime F G› by (simp add: gcd_mult_right_left_cancel ac_simps) finally show ?thesis unfolding G H_def cg cf using False by simp next case True hence "gcd (smult a f) g = normalize g" by (cases "a = 0", auto) thus ?thesis using True by simp qed lemma gcd_smult_ex: assumes "a ≠ 0" shows "∃ b. gcd (smult a f) g = smult b (gcd f g) ∧ b ≠ 0" proof (cases "f = 0") case True thus ?thesis by (intro exI[of _ 1], auto) next case False hence id: "(a = 0 ∨ f = 0) = False" using assms by auto show ?thesis unfolding gcd_smult id if_False by (intro exI conjI, rule refl, insert assms, auto) qed lemma primitive_part_idemp[simp]: fixes f :: "'a :: {semiring_gcd,normalization_semidom_multiplicative} poly" shows "primitive_part (primitive_part f) = primitive_part f" by (metis content_primitive_part[of f] primitive_part_eq_0_iff primitive_part_prim) lemma content_gcd_primitive: "f ≠ 0 ⟹ content (gcd (primitive_part f) g) = 1" "f ≠ 0 ⟹ content (gcd (primitive_part f) (primitive_part g)) = 1" by (metis (no_types, lifting) content_dvd_contentI content_primitive_part gcd_dvd1 is_unit_content_iff)+ lemma content_gcd_content: "content (gcd f g) = gcd (content f) (content g)" (is "?l = ?r") proof - let ?c = "content" have "?l = normalize (gcd (?c f) (?c g)) * ?c (gcd (primitive_part f) (primitive_part g))" unfolding gcd_poly_decompose[of f g] content_smult .. also have "… = gcd (?c f) (?c g) * ?c (gcd (primitive_part f) (primitive_part g))" by simp also have "… = ?r" using content_gcd_primitive[of f g] by (metis (no_types, lifting) content_dvd_contentI content_eq_zero_iff content_primitive_part gcd_dvd2 gcd_eq_0_iff is_unit_content_iff mult_cancel_left1) finally show ?thesis . qed lemma gcd_primitive_part: "gcd (primitive_part f) (primitive_part g) = normalize (primitive_part (gcd f g))" proof(cases "f = 0") case True show ?thesis unfolding gcd_poly_decompose[of f g] gcd_0_left primitive_part_0 True by (simp add: associatedI primitive_part_dvd_primitive_partI) next case False have "normalize 1 = normalize (unit_factor (gcd (content f) (content g)))" by (simp add: False) then show ?thesis unfolding gcd_poly_decompose[of f g] by (metis (no_types) Polynomial.normalize_smult content_gcd_primitive(1)[OF False] content_times_primitive_part normalize_gcd primitive_part_smult) qed lemma primitive_part_gcd: "primitive_part (gcd f g) = unit_factor (gcd f g) * gcd (primitive_part f) (primitive_part g)" unfolding gcd_primitive_part by (metis (no_types, lifting) content_times_primitive_part gcd.normalize_idem mult_cancel_left2 mult_smult_left normalize_eq_0_iff normalize_mult_unit_factor primitive_part_eq_0_iff smult_content_normalize_primitive_part unit_factor_mult_normalize) lemma primitive_part_normalize: fixes f :: "'a :: {semiring_gcd,idom_divide,normalization_semidom_multiplicative} poly" shows "primitive_part (normalize f) = normalize (primitive_part f)" proof (cases "f = 0") case True thus ?thesis by simp next case False have "normalize (content (normalize (primitive_part f))) = 1" using content_primitive_part[OF False] content_dvd content_const content_dvd_contentI dvd_normalize_iff is_unit_content_iff by (metis (no_types)) then have "content (normalize (primitive_part f)) = 1" by fastforce then have "content (normalize f) = 1 * content f" by (metis (no_types) content_smult mult.commute normalize_content smult_content_normalize_primitive_part) then have "content f = content (normalize f)" by simp then show ?thesis unfolding smult_content_normalize_primitive_part[of f,symmetric] by (metis (no_types) False content_times_primitive_part mult.commute mult_cancel_left mult_smult_right smult_content_normalize_primitive_part) qed lemma length_coeffs_primitive_part[simp]: "length (coeffs (primitive_part f)) = length (coeffs f)" proof (cases "f = 0") case False hence "length (coeffs f) ≠ 0" "length (coeffs (primitive_part f)) ≠ 0" by auto thus ?thesis using degree_primitive_part[of f, unfolded degree_eq_length_coeffs] by linarith qed simp lemma degree_unit_factor[simp]: "degree (unit_factor f) = 0" by (simp add: monom_0 unit_factor_poly_def) lemma degree_normalize[simp]: "degree (normalize f) = degree f" proof (cases "f = 0") case False have "degree f = degree (unit_factor f * normalize f)" by simp also have "… = degree (unit_factor f) + degree (normalize f)" by (rule degree_mult_eq, insert False, auto) finally show ?thesis by simp qed simp lemma content_iff: "x dvd content p ⟷ (∀ c ∈ set (coeffs p). x dvd c)" by (simp add: content_def dvd_gcd_list_iff) lemma is_unit_field_poly[simp]: "(p::'a::field poly) dvd 1 ⟷ p ≠ 0 ∧ degree p = 0" proof(intro iffI conjI, unfold conj_imp_eq_imp_imp) assume "is_unit p" then obtain q where *: "p * q = 1" by (elim dvdE, auto) from * show p0: "p ≠ 0" by auto from * have q0: "q ≠ 0" by auto from * degree_mult_eq[OF p0 q0] show "degree p = 0" by auto next assume "degree p = 0" from degree0_coeffs[OF this] obtain c where c: "p = [:c:]" by auto assume "p ≠ 0" with c have "c ≠ 0" by auto with c have "1 = p * [:1/c:]" by auto from dvdI[OF this] show "is_unit p". qed definition primitive where "primitive f ⟷ (∀x. (∀y ∈ set (coeffs f). x dvd y) ⟶ x dvd 1)" lemma primitiveI: assumes "(⋀x. (⋀y. y ∈ set (coeffs f) ⟹ x dvd y) ⟹ x dvd 1)" shows "primitive f" by (insert assms, auto simp: primitive_def) lemma primitiveD: assumes "primitive f" shows "(⋀y. y ∈ set (coeffs f) ⟹ x dvd y) ⟹ x dvd 1" by (insert assms, auto simp: primitive_def) lemma not_primitiveE: assumes "¬ primitive f" and "⋀x. (⋀y. y ∈ set (coeffs f) ⟹ x dvd y) ⟹ ¬ x dvd 1 ⟹ thesis" shows thesis by (insert assms, auto simp: primitive_def) lemma primitive_iff_content_eq_1[simp]: fixes f :: "'a :: semiring_gcd poly" shows "primitive f ⟷ content f = 1" proof(intro iffI primitiveI) fix x assume "(⋀y. y ∈ set (coeffs f) ⟹ x dvd y)" from gcd_list_greatest[of "coeffs f", OF this] have "x dvd content f" by (simp add: content_def) also assume "content f = 1" finally show "x dvd 1". next assume "primitive f" from primitiveD[OF this list_gcd[of _ "coeffs f"], folded content_def] show "content f = 1" by simp qed lemma primitive_prod_list: fixes fs :: "'a :: {factorial_semiring,semiring_Gcd,normalization_semidom_multiplicative} poly list" assumes "primitive (prod_list fs)" and "f ∈ set fs" shows "primitive f" proof (insert assms, induct fs arbitrary: f) case (Cons f' fs) from Cons.prems have "is_unit (content f' * content (prod_list fs))" by (auto simp: content_mult) from this[unfolded is_unit_mult_iff] have "content f' = 1" and "content (prod_list fs) = 1" by auto moreover from Cons.prems have "f = f' ∨ f ∈ set fs" by auto ultimately show ?case using Cons.hyps[of f] by auto qed auto lemma irreducible_imp_primitive: fixes f :: "'a :: {idom,semiring_gcd} poly" assumes irr: "irreducible f" and deg: "degree f ≠ 0" shows "primitive f" proof (rule ccontr) assume not: "¬ ?thesis" then have "¬ [:content f:] dvd 1" by simp moreover have "f = [:content f:] * primitive_part f" by simp note Factorial_Ring.irreducibleD[OF irr this] ultimately have "primitive_part f dvd 1" by auto from this[unfolded poly_dvd_1] have "degree f = 0" by auto with deg show False by auto qed lemma irreducible_primitive_connect: fixes f :: "'a :: {idom,semiring_gcd} poly" assumes cf: "primitive f" shows "irreducible⇩_{d}f ⟷ irreducible f" (is "?l ⟷ ?r") proof assume l: ?l show ?r proof(rule ccontr, elim not_irreducibleE) from l have deg: "degree f > 0" by (auto dest: irreducible⇩_{d}D) from cf have f0: "f ≠ 0" by auto then show "f = 0 ⟹ False" by auto show "f dvd 1 ⟹ False" using deg by (auto simp:poly_dvd_1) fix a b assume fab: "f = a * b" and a1: "¬ a dvd 1" and b1: "¬ b dvd 1" then have af: "a dvd f" and bf: "b dvd f" by auto with f0 have a0: "a ≠ 0" and b0: "b ≠ 0" by auto from irreducible⇩_{d}D(2)[OF l, of a] af dvd_imp_degree_le[OF af f0] have "degree a = 0 ∨ degree a = degree f" by (metis degree_smult_le irreducible⇩_{d}_dvd_smult l le_antisym Nat.neq0_conv) then show False proof(elim disjE) assume "degree a = 0" then obtain c where ac: "a = [:c:]" by (auto dest: degree0_coeffs) from fab[unfolded ac] have "c dvd content f" by (simp add: content_iff coeffs_smult) with cf have "c dvd 1" by simp then have "a dvd 1" by (auto simp: ac) with a1 show False by auto next assume dega: "degree a = degree f" with f0 degree_mult_eq[OF a0 b0] fab have "degree b = 0" by (auto simp: ac_simps) then obtain c where bc: "b = [:c:]" by (auto dest: degree0_coeffs) from fab[unfolded bc] have "c dvd content f" by (simp add: content_iff coeffs_smult) with cf have "c dvd 1" by simp then have "b dvd 1" by (auto simp: bc) with b1 show False by auto qed qed next assume r: ?r show ?l proof(intro irreducible⇩_{d}I) show "degree f > 0" proof (rule ccontr) assume "¬degree f > 0" then obtain f0 where f: "f = [:f0:]" by (auto dest: degree0_coeffs) from cf[unfolded this] have "normalize f0 = 1" by auto then have "f0 dvd 1" by (unfold normalize_1_iff) with r[unfolded f irreducible_const_poly_iff] show False by auto qed next fix g h assume deg_g: "degree g > 0" and deg_gf: "degree g < degree f" and fgh: "f = g * h" with r have "g dvd 1 ∨ h dvd 1" by auto with deg_g have "degree h = 0" by (auto simp: poly_dvd_1) with deg_gf[unfolded fgh] degree_mult_eq[of g h] show False by (cases "g = 0 ∨ h = 0", auto) qed qed lemma deg_not_zero_imp_not_unit: fixes f:: "'a::{idom_divide,semidom_divide_unit_factor} poly" assumes deg_f: "degree f > 0" shows "¬ is_unit f" proof - have "degree (normalize f) > 0" using deg_f degree_normalize by auto hence "normalize f ≠ 1" by fastforce thus "¬ is_unit f" using normalize_1_iff by auto qed lemma content_pCons[simp]: "content (pCons a p) = gcd a (content p)" proof(induct p arbitrary: a) case 0 show ?case by simp next case (pCons c p) then show ?case by (cases "p = 0", auto simp: content_def cCons_def) qed lemma content_field_poly: fixes f :: "'a :: {field,semiring_gcd} poly" shows "content f = (if f = 0 then 0 else 1)" by(induct f, auto simp: dvd_field_iff is_unit_normalize) end

# Theory Gauss_Lemma

(* Author: René Thiemann Akihisa Yamada License: BSD *) (*TODO: Rename! *) section ‹Gauss Lemma› text ‹We formalized Gauss Lemma, that the content of a product of two polynomials $p$ and $q$ is the product of the contents of $p$ and $q$. As a corollary we provide an algorithm to convert a rational factor of an integer polynomial into an integer factor. In contrast to the theory on unique factorization domains -- where Gauss Lemma is also proven in a more generic setting -- we are here in an executable setting and do not use the unspecified $some-gcd$ function. Moreover, there is a slight difference in the definition of content: in this theory it is only defined for integer-polynomials, whereas in the UFD theory, the content is defined for polynomials in the fraction field.› theory Gauss_Lemma imports "HOL-Computational_Algebra.Primes" "HOL-Computational_Algebra.Field_as_Ring" Polynomial_Interpolation.Ring_Hom_Poly Missing_Polynomial_Factorial begin lemma primitive_part_alt_def: "primitive_part p = sdiv_poly p (content p)" by (simp add: primitive_part_def sdiv_poly_def) definition common_denom :: "rat list ⇒ int × int list" where "common_denom xs ≡ let nds = map quotient_of xs; denom = list_lcm (map snd nds); ints = map (λ (n,d). n * denom div d) nds in (denom, ints)" definition rat_to_int_poly :: "rat poly ⇒ int × int poly" where "rat_to_int_poly p ≡ let ais = coeffs p; d = fst (common_denom ais) in (d, map_poly (λ x. case quotient_of x of (p,q) ⇒ p * d div q) p)" definition rat_to_normalized_int_poly :: "rat poly ⇒ rat × int poly" where "rat_to_normalized_int_poly p ≡ if p = 0 then (1,0) else case rat_to_int_poly p of (s,q) ⇒ (of_int (content q) / of_int s, primitive_part q)" lemma rat_to_normalized_int_poly_code[code]: "rat_to_normalized_int_poly p = (if p = 0 then (1,0) else case rat_to_int_poly p of (s,q) ⇒ let c = content q in (of_int c / of_int s, sdiv_poly q c))" unfolding Let_def rat_to_normalized_int_poly_def primitive_part_alt_def .. lemma common_denom: assumes cd: "common_denom xs = (dd,ys)" shows "xs = map (λ i. of_int i / of_int dd) ys" "dd > 0" "⋀x. x ∈ set xs ⟹ rat_of_int (case quotient_of x of (n, x) ⇒ n * dd div x) / rat_of_int dd = x" proof - let ?nds = "map quotient_of xs" define nds where "nds = ?nds" let ?denom = "list_lcm (map snd nds)" let ?ints = "map (λ (n,d). n * dd div d) nds" from cd[unfolded common_denom_def Let_def] have dd: "dd = ?denom" and ys: "ys = ?ints" unfolding nds_def by auto show dd0: "dd > 0" unfolding dd by (intro list_lcm_pos(3), auto simp: nds_def quotient_of_nonzero) { fix x assume x: "x ∈ set xs" obtain p q where quot: "quotient_of x = (p,q)" by force from x have "(p,q) ∈ set nds" unfolding nds_def using quot by force hence "q ∈ set (map snd nds)" by force from list_lcm[OF this] have q: "q dvd dd" unfolding dd . show "rat_of_int (case quotient_of x of (n, x) ⇒ n * dd div x) / rat_of_int dd = x" unfolding quot split unfolding quotient_of_div[OF quot] proof - have f1: "q * (dd div q) = dd" using dvd_mult_div_cancel q by blast have "rat_of_int (dd div q) ≠ 0" using dd0 dvd_mult_div_cancel q by fastforce thus "rat_of_int (p * dd div q) / rat_of_int dd = rat_of_int p / rat_of_int q" using f1 by (metis (no_types) div_mult_swap mult_divide_mult_cancel_right of_int_mult q) qed } note main = this show "xs = map (λ i. of_int i / of_int dd) ys" unfolding ys map_map o_def nds_def by (rule sym, rule map_idI, rule main) qed lemma rat_to_int_poly: assumes "rat_to_int_poly p = (d,q)" shows "p = smult (inverse (of_int d)) (map_poly of_int q)" "d > 0" proof - let ?f = "λ x. case quotient_of x of (pa, x) ⇒ pa * d div x" define f where "f = ?f" from assms[unfolded rat_to_int_poly_def Let_def] obtain xs where cd: "common_denom (coeffs p) = (d,xs)" and q: "q = map_poly f p" unfolding f_def by (cases "common_denom (coeffs p)", auto) from common_denom[OF cd] have d: "d > 0" and id: "⋀ x. x ∈ set (coeffs p) ⟹ rat_of_int (f x) / rat_of_int d = x" unfolding f_def by auto have f0: "f 0 = 0" unfolding f_def by auto have id: "rat_of_int (f (coeff p n)) / rat_of_int d = coeff p n" for n using id[of "coeff p n"] f0 range_coeff by (cases "coeff p n = 0", auto) show "d > 0" by fact show "p = smult (inverse (of_int d)) (map_poly of_int q)" unfolding q smult_as_map_poly using id f0 by (intro poly_eqI, auto simp: field_simps coeff_map_poly) qed lemma content_ge_0_int: "content p ≥ (0 :: int)" unfolding content_def by (cases "coeffs p", auto) lemma abs_content_int[simp]: fixes p :: "int poly" shows "abs (content p) = content p" using content_ge_0_int[of p] by auto lemma content_smult_int: fixes p :: "int poly" shows "content (smult a p) = abs a * content p" by simp lemma normalize_non_0_smult: "∃ a. (a :: 'a :: semiring_gcd) ≠ 0 ∧ smult a (primitive_part p) = p" by (cases "p = 0", rule exI[of _ 1], simp, rule exI[of _ "content p"], auto) lemma rat_to_normalized_int_poly: assumes "rat_to_normalized_int_poly p = (d,q)" shows "p = smult d (map_poly of_int q)" "d > 0" "p ≠ 0 ⟹ content q = 1" "degree q = degree p" proof - have "p = smult d (map_poly of_int q) ∧ d > 0 ∧ (p ≠ 0 ⟶ content q = 1)" proof (cases "p = 0") case True thus ?thesis using assms unfolding rat_to_normalized_int_poly_def by (auto simp: eval_poly_def) next case False hence p0: "p ≠ 0" by auto obtain s r where id: "rat_to_int_poly p = (s,r)" by force let ?cr = "rat_of_int (content r)" let ?s = "rat_of_int s" let ?q = "map_poly rat_of_int q" from rat_to_int_poly[OF id] have p: "p = smult (inverse ?s) (map_poly of_int r)" and s: "s > 0" by auto let ?q = "map_poly rat_of_int q" from p0 assms[unfolded rat_to_normalized_int_poly_def id split] have d: "d = ?cr / ?s" and q: "q = primitive_part r" by auto from content_times_primitive_part[of r, folded q] have qr: "smult (content r) q = r" . have "smult d ?q = smult (?cr / ?s) ?q" unfolding d by simp also have "?cr / ?s = ?cr * inverse ?s" by (rule divide_inverse) also have "… = inverse ?s * ?cr" by simp also have "smult (inverse ?s * ?cr) ?q = smult (inverse ?s) (smult ?cr ?q)" by simp also have "smult ?cr ?q = map_poly of_int (smult (content r) q)" by (simp add: hom_distribs) also have "… = map_poly of_int r" unfolding qr .. finally have pq: "p = smult d ?q" unfolding p by simp from p p0 have r0: "r ≠ 0" by auto from content_eq_zero_iff[of r] content_ge_0_int[of r] r0 have cr: "?cr > 0" by linarith with s have d0: "d > 0" unfolding d by auto from content_primitive_part[OF r0] have cq: "content q = 1" unfolding q . from pq d0 cq show ?thesis by auto qed thus p: "p = smult d (map_poly of_int q)" and d: "d > 0" and "p ≠ 0 ⟹ content q = 1" by auto show "degree q = degree p" unfolding p smult_as_map_poly by (rule sym, subst map_poly_map_poly, force+, rule degree_map_poly, insert d, auto) qed lemma content_dvd_1: "content g = 1" if "content f = (1 :: 'a :: semiring_gcd)" "g dvd f" proof - from ‹g dvd f› have "content g dvd content f" by (rule content_dvd_contentI) with ‹content f = 1› show ?thesis by simp qed lemma dvd_smult_int: fixes c :: int assumes c: "c ≠ 0" and dvd: "q dvd (smult c p)" shows "primitive_part q dvd p" proof (cases "p = 0") case True thus ?thesis by auto next case False note p0 = this let ?cp = "smult c p" from p0 c have cp0: "?cp ≠ 0" by auto from dvd obtain r where prod: "?cp = q * r" unfolding dvd_def by auto from prod cp0 have q0: "q ≠ 0" and r0: "r ≠ 0" by auto let ?c = "content :: int poly ⇒ int" let ?n = "primitive_part :: int poly ⇒ int poly" let ?pn = "λ p. smult (?c p) (?n p)" have cq: "(?c q = 0) = False" using content_eq_zero_iff q0 by auto from prod have id1: "?cp = ?pn q * ?pn r" unfolding content_times_primitive_part by simp from arg_cong[OF this, of content, unfolded content_smult_int content_mult content_primitive_part[OF r0] content_primitive_part[OF q0], symmetric] p0[folded content_eq_zero_iff] c have "abs c dvd ?c q * ?c r" unfolding dvd_def by auto hence "c dvd ?c q * ?c r" by auto then obtain d where id: "?c q * ?c r = c * d" unfolding dvd_def by auto have "?cp = ?pn q * ?pn r" by fact also have "… = smult (c * d) (?n q * ?n r)" unfolding id [symmetric] by (metis content_mult content_times_primitive_part primitive_part_mult) finally have id: "?cp = smult c (?n q * smult d (?n r))" by (simp add: mult.commute) interpret map_poly_inj_zero_hom "(*) c" using c by (unfold_locales, auto) have "p = ?n q * smult d (?n r)" using id[unfolded smult_as_map_poly[of c]] by auto thus dvd: "?n q dvd p" unfolding dvd_def by blast qed lemma irreducible⇩_{d}_primitive_part: fixes p :: "int poly" (* can be relaxed but primitive_part_mult has bad type constraint *) shows "irreducible⇩_{d}(primitive_part p) ⟷ irreducible⇩_{d}p" (is "?l ⟷ ?r") proof (rule iffI, rule irreducible⇩_{d}I) assume l: ?l show "degree p > 0" using l by auto have dpp: "degree (primitive_part p) = degree p" by simp fix q r assume deg: "degree q < degree p" "degree r < degree p" and "p = q * r" then have pp: "primitive_part p = primitive_part q * primitive_part r" by (simp add: primitive_part_mult) have "¬ irreducible⇩_{d}(primitive_part p)" apply (intro reducible⇩_{d}I, rule exI[of _ "primitive_part q"], rule exI[of _ "primitive_part r"], unfold dpp) using deg pp by auto with l show False by auto next show "?r ⟹ ?l" by (metis irreducible⇩_{d}_smultI normalize_non_0_smult) qed lemma irreducible⇩_{d}_smult_int: fixes c :: int assumes c: "c ≠ 0" shows "irreducible⇩_{d}(smult c p) = irreducible⇩_{d}p" (is "?l = ?r") using irreducible⇩_{d}_primitive_part[of "smult c p", unfolded primitive_part_smult] c apply (cases "c < 0", simp) apply (metis add.inverse_inverse add.inverse_neutral c irreducible⇩_{d}_smultI normalize_non_0_smult smult_1_left smult_minus_left) apply (simp add: irreducible⇩_{d}_primitive_part) done lemma irreducible⇩_{d}_as_irreducible: fixes p :: "int poly" shows "irreducible⇩_{d}p ⟷ irreducible (primitive_part p)" using irreducible_primitive_connect[of "primitive_part p"] by (cases "p = 0", auto simp: irreducible⇩_{d}_primitive_part) lemma rat_to_int_factor_content_1: fixes p :: "int poly" assumes cp: "content p = 1" and pgh: "map_poly rat_of_int p = g * h" and g: "rat_to_normalized_int_poly g = (r,rg)" and h: "rat_to_normalized_int_poly h = (s,sh)" and p: "p ≠ 0" shows "p = rg * sh" proof - let ?r = "rat_of_int" let ?rp = "map_poly ?r" from p have rp0: "?rp p ≠ 0" by simp with pgh have g0: "g ≠ 0" and h0: "h ≠ 0" by auto from rat_to_normalized_int_poly[OF g] g0 have r: "r > 0" "r ≠ 0" and g: "g = smult r (?rp rg)" and crg: "content rg = 1" by auto from rat_to_normalized_int_poly[OF h] h0 have s: "s > 0" "s ≠ 0" and h: "h = smult s (?rp sh)" and csh: "content sh = 1" by auto let ?irs = "inverse (r * s)" from r s have irs0: "?irs ≠ 0" by (auto simp: field_simps) have "?rp (rg * sh) = ?rp rg * ?rp sh" by (simp add: hom_distribs) also have "… = smult ?irs (?rp p)" unfolding pgh g h using r s by (simp add: field_simps) finally have id: "?rp (rg * sh) = smult ?irs (?rp p)" by auto have rsZ: "?irs ∈ ℤ" proof (rule ccontr) assume not: "¬ ?irs ∈ ℤ" obtain n d where irs': "quotient_of ?irs = (n,d)" by force from quotient_of_denom_pos[OF irs'] have "d > 0" . from not quotient_of_div[OF irs'] have "d ≠ 1" "d ≠ 0" and irs: "?irs = ?r n / ?r d" by auto with irs0 have n0: "n ≠ 0" by auto from ‹d > 0› ‹d ≠ 1› have "d ≥ 2" and "¬ d dvd 1" by auto with content_iff[of d p, unfolded cp] obtain c where c: "c ∈ set (coeffs p)" and dc: "¬ d dvd c" by auto from c range_coeff[of p] obtain i where "c = coeff p i" by auto from arg_cong[OF id, of "λ p. coeff p i", unfolded coeff_smult of_int_hom.coeff_map_poly_hom this[symmetric] irs] have "?r n / ?r d * ?r c ∈ ℤ" by (metis Ints_of_int) also have "?r n / ?r d * ?r c = ?r (n * c) / ?r d" by simp finally have inZ: "?r (n * c) / ?r d ∈ ℤ" . have cop: "coprime n d" by (rule quotient_of_coprime[OF irs']) (* now there comes tedious reasoning that `coprime n d` `¬ d dvd c` ` nc / d ∈ ℤ` yields a contradiction *) define prod where "prod = ?r (n * c) / ?r d" obtain n' d' where quot: "quotient_of prod = (n',d')" by force have qr: "⋀ x. quotient_of (?r x) = (x, 1)" using Rat.of_int_def quotient_of_int by auto from quotient_of_denom_pos[OF quot] have "d' > 0" . with quotient_of_div[OF quot] inZ[folded prod_def] have "d' = 1" by (metis Ints_cases Rat.of_int_def old.prod.inject quot quotient_of_int) with quotient_of_div[OF quot] have "prod = ?r n'" by auto from arg_cong[OF this, of quotient_of, unfolded prod_def rat_divide_code qr Let_def split] have "Rat.normalize (n * c, d) = (n',1)" by simp from normalize_crossproduct[OF ‹d ≠ 0›, of 1 "n * c" n', unfolded this] have id: "n * c = n' * d" by auto from quotient_of_coprime[OF irs'] have "coprime n d" . with id have "d dvd c" by (metis coprime_commute coprime_dvd_mult_right_iff dvd_triv_right) with dc show False .. qed then obtain irs where irs: "?irs = ?r irs" unfolding Ints_def by blast from id[unfolded irs, folded hom_distribs, unfolded of_int_poly_hom.eq_iff] have p: "rg * sh = smult irs p" by auto have "content (rg * sh) = 1" unfolding content_mult crg csh by auto from this[unfolded p content_smult_int cp] have "abs irs = 1" by simp hence "abs ?irs = 1" using irs by auto with r s have "?irs = 1" by auto with irs have "irs = 1" by auto with p show p: "p = rg * sh" by auto qed lemma rat_to_int_factor_explicit: fixes p :: "int poly" assumes pgh: "map_poly rat_of_int p = g * h" and g: "rat_to_normalized_int_poly g = (r,rg)" shows "∃ r. p = rg * smult (content p) r" proof - show ?thesis proof (cases "p = 0") case True show ?thesis unfolding True by (rule exI[of _ 0], auto simp: degree_monom_eq) next case False hence p: "p ≠ 0" by auto let ?r = "rat_of_int" let ?rp = "map_poly ?r" define q where "q = primitive_part p" from content_times_primitive_part[of p, folded q_def] content_eq_zero_iff[of p] p obtain a where a: "a ≠ 0" and pq: "p = smult a q" and acp: "content p = a" by metis from a pq p have ra: "?r a ≠ 0" and q0: "q ≠ 0" by auto from content_primitive_part[OF p, folded q_def] have cq: "content q = 1" by auto obtain s sh where h: "rat_to_normalized_int_poly (smult (inverse (?r a)) h) = (s,sh)" by force from arg_cong[OF pgh[unfolded pq], of "smult (inverse (?r a))"] ra have "?rp q = g * smult (inverse (?r a)) h" by (auto simp: hom_distribs) from rat_to_int_factor_content_1[OF cq this g h q0] have qrs: "q = rg * sh" . show ?thesis unfolding acp unfolding pq qrs by (rule exI[of _ sh], auto) qed qed lemma rat_to_int_factor: fixes p :: "int poly" assumes pgh: "map_poly rat_of_int p = g * h" shows "∃ g' h'. p = g' * h' ∧ degree g' = degree g ∧ degree h' = degree h" proof(cases "p = 0") case True with pgh have "g = 0 ∨ h = 0" by auto then show ?thesis by (metis True degree_0 mult_hom.hom_zero mult_zero_left rat_to_normalized_int_poly(4) surj_pair) next case False obtain r rg where ri: "rat_to_normalized_int_poly (smult (1 / of_int (content p)) g) = (r,rg)" by force obtain q qh where ri2: "rat_to_normalized_int_poly h = (q,qh)" by force show ?thesis proof (intro exI conjI) have "of_int_poly (primitive_part p) = smult (1 / of_int (content p)) (g * h)" apply (auto simp: primitive_part_def pgh[symmetric] smult_map_poly map_poly_map_poly o_def intro!: map_poly_cong) by (metis (no_types, lifting) content_dvd_coeffs div_by_0 dvd_mult_div_cancel floor_of_int nonzero_mult_div_cancel_left of_int_hom.hom_zero of_int_mult) also have "… = smult (1 / of_int (content p)) g * h" by simp finally have "of_int_poly (primitive_part p) = …". note main = rat_to_int_factor_content_1[OF _ this ri ri2, simplified, OF False] show "p = smult (content p) rg * qh" by (simp add: main[symmetric]) from ri2 show "degree qh = degree h" by (fact rat_to_normalized_int_poly) from rat_to_normalized_int_poly(4)[OF ri] False show "degree (smult (content p) rg) = degree g" by auto qed qed lemma rat_to_int_factor_normalized_int_poly: fixes p :: "rat poly" assumes pgh: "p = g * h" and p: "rat_to_normalized_int_poly p = (i,ip)" shows "∃ g' h'. ip = g' * h' ∧ degree g' = degree g" proof - from rat_to_normalized_int_poly[OF p] have p: "p = smult i (map_poly rat_of_int ip)" and i: "i ≠ 0" by auto from arg_cong[OF p, of "smult (inverse i)", unfolded pgh] i have "map_poly rat_of_int ip = g * smult (inverse i) h" by auto from rat_to_int_factor[OF this] show ?thesis by auto qed (* TODO: move *) lemma irreducible_smult [simp]: fixes c :: "'a :: field" shows "irreducible (smult c p) ⟷ irreducible p ∧ c ≠ 0" using irreducible_mult_unit_left[of "[:c:]", simplified] by force text ‹A polynomial with integer coefficients is irreducible over the rationals, if it is irreducible over the integers.› theorem irreducible⇩_{d}_int_rat: fixes p :: "int poly" assumes p: "irreducible⇩_{d}p" shows "irreducible⇩_{d}(map_poly rat_of_int p)" proof (rule irreducible⇩_{d}I) from irreducible⇩_{d}D[OF p] have p: "degree p ≠ 0" and irr: "⋀ q r. degree q < degree p ⟹ degree r < degree p ⟹ p ≠ q * r" by auto let ?r = "rat_of_int" let ?rp = "map_poly ?r" from p show rp: "degree (?rp p) > 0" by auto from p have p0: "p ≠ 0" by auto fix g h :: "rat poly" assume deg: "degree g > 0" "degree g < degree (?rp p)" "degree h > 0" "degree h < degree (?rp p)" and pgh: "?rp p = g * h" from rat_to_int_factor[OF pgh] obtain g' h' where p: "p = g' * h'" and dg: "degree g' = degree g" "degree h' = degree h" by auto from irr[of g' h'] deg[unfolded dg] show False using degree_mult_eq[of g' h'] by (auto simp: p dg) qed corollary irreducible⇩_{d}_rat_to_normalized_int_poly: assumes rp: "rat_to_normalized_int_poly rp = (a, ip)" and ip: "irreducible⇩_{d}ip" shows "irreducible⇩_{d}rp" proof - from rat_to_normalized_int_poly[OF rp] have rp: "rp = smult a (map_poly rat_of_int ip)" and a: "a ≠ 0" by auto with irreducible⇩_{d}_int_rat[OF ip] show ?thesis by auto qed lemma dvd_content_dvd: assumes dvd: "content f dvd content g" "primitive_part f dvd primitive_part g" shows "f dvd g" proof - let ?cf = "content f" let ?nf = "primitive_part f" let ?cg = "content g" let ?ng = "primitive_part g" have "f dvd g = (smult ?cf ?nf dvd smult ?cg ?ng)" unfolding content_times_primitive_part by auto from dvd(1) obtain ch where cg: "?cg = ?cf * ch" unfolding dvd_def by auto from dvd(2) obtain nh where ng: "?ng = ?nf * nh" unfolding dvd_def by auto have "f dvd g = (smult ?cf ?nf dvd smult ?cg ?ng)" unfolding content_times_primitive_part[of f] content_times_primitive_part[of g] by auto also have "… = (smult ?cf ?nf dvd smult ?cf ?nf * smult ch nh)" unfolding cg ng by (metis mult.commute mult_smult_right smult_smult) also have "…" by (rule dvd_triv_left) finally show ?thesis . qed lemma sdiv_poly_smult: "c ≠ 0 ⟹ sdiv_poly (smult c f) c = f" by (intro poly_eqI, unfold coeff_sdiv_poly coeff_smult, auto) lemma primitive_part_smult_int: fixes f :: "int poly" shows "primitive_part (smult d f) = smult (sgn d) (primitive_part f)" proof (cases "d = 0 ∨ f = 0") case False obtain cf where cf: "content f = cf" by auto with False have 0: "d ≠ 0" "f ≠ 0" "cf ≠ 0" by auto show ?thesis proof (rule poly_eqI, unfold primitive_part_alt_def coeff_sdiv_poly content_smult_int coeff_smult cf) fix n consider (pos) "d > 0" | (neg) "d < 0" using 0(1) by linarith thus "d * coeff f n div (¦d¦ * cf) = sgn d * (coeff f n div cf)" proof cases case neg hence "?thesis = (d * coeff f n div - (d * cf) = - (coeff f n div cf))" by auto also have "d * coeff f n div - (d * cf) = - (d * coeff f n div (d * cf))" by (subst dvd_div_neg, insert 0(1), auto simp: cf[symmetric]) also have "d * coeff f n div (d * cf) = coeff f n div cf" using 0(1) by auto finally show ?thesis by simp qed auto qed qed auto lemma gcd_smult_left: assumes "c ≠ 0" shows "gcd (smult c f) g = gcd f (g :: 'b :: {field_gcd} poly)" proof - from assms have "normalize c = 1" by (meson dvd_field_iff is_unit_normalize) then show ?thesis by (metis (no_types) Polynomial.normalize_smult gcd.commute gcd.left_commute gcd_left_idem gcd_self smult_1_left) qed lemma gcd_smult_right: "c ≠ 0 ⟹ gcd f (smult c g) = gcd f (g :: 'b :: {field_gcd} poly)" using gcd_smult_left[of c g f] by (simp add: gcd.commute) lemma gcd_rat_to_gcd_int: "gcd (of_int_poly f :: rat poly) (of_int_poly g) = smult (inverse (of_int (lead_coeff (gcd f g)))) (of_int_poly (gcd f g))" proof (cases "f = 0 ∧ g = 0") case True thus ?thesis by simp next case False let ?r = rat_of_int let ?rp = "map_poly ?r" from False have gcd0: "gcd f g ≠ 0" by auto hence lc0: "lead_coeff (gcd f g) ≠ 0" by auto hence inv: "inverse (?r (lead_coeff (gcd f g))) ≠ 0" by auto show ?thesis proof (rule sym, rule gcdI, goal_cases) case 1 have "gcd f g dvd f" by auto then obtain h where f: "f = gcd f g * h" unfolding dvd_def by auto show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF f, of ?rp], simp add: hom_distribs) next case 2 have "gcd f g dvd g" by auto then obtain h where g: "g = gcd f g * h" unfolding dvd_def by auto show ?case by (rule smult_dvd[OF _ inv], insert arg_cong[OF g, of ?rp],