# Theory Missing_List

(*
Author:      René Thiemann
*)
subsection ‹Missing List›

text ‹The provides some standard algorithms and lemmas on lists.›
theory Missing_List
imports
Matrix.Utility
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)

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
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)

"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)"

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)"

assumes "j ≠ i" shows "adjust_idx i (adjust_idx_rev i j) = j"

unfolding adjust_idx_def by (cases "j < i", auto)

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

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

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)

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
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
*)
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)
by (auto dest: mset_subset_eq_insertD)
next
case False
hence id: "(ps ⊆# xs + {#x#}) = (ps ⊆# xs)"
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}"
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)"

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
*)
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
*)
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

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

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
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 (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 :]"
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]
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
next
case False
have "normalize 1 = normalize (unit_factor (gcd (content f) (content g)))"
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"

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)"

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⇩dD)
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⇩dD(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⇩dI)
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
*)
(*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)"

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⇩dI)
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⇩dI, 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)
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
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
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⇩dI)
from irreducible⇩dD[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],`