Theory Degree_Bound
subsection ‹Maximal Degree during Reconstruction›
text ‹We define a function which computes an upper bound on the degree of
a factor for which we have to reconstruct the integer values of the coefficients.
This degree will determine how large the second parameter of the factor-bound will
be.
In essence, if the Berlekamp-factorization will produce $n$ factors with degrees
$d_1,\ldots,d_n$, then our bound will be the sum of the $\frac{n}2$ largest degrees.
The reason is that we will combine at most $\frac{n}2$ factors before reconstruction.
Soundness of the bound is proven, as well as a monotonicity property.›
theory Degree_Bound
imports Containers.Set_Impl
"HOL-Library.Multiset"
Polynomial_Interpolation.Missing_Polynomial
"Efficient-Mergesort.Efficient_Sort"
begin
definition max_factor_degree :: "nat list ⇒ nat" where
"max_factor_degree degs = (let
ds = sort degs
in sum_list (drop (length ds div 2) ds))"
definition degree_bound where "degree_bound vs = max_factor_degree (map degree vs)"
lemma insort_middle: "sort (xs @ x # ys) = insort x (sort (xs @ ys))"
by (metis append.assoc sort_append_Cons_swap sort_snoc)
lemma sum_list_insort[simp]:
"sum_list (insort (d :: 'a :: {comm_monoid_add,linorder}) xs) = d + sum_list xs"
proof (induct xs)
case (Cons x xs)
thus ?case by (cases "d ≤ x", auto simp: ac_simps)
qed simp
lemma half_largest_elements_mono: "sum_list (drop (length ds div 2) (sort ds))
≤ sum_list (drop (Suc (length ds) div 2) (insort (d :: nat) (sort ds)))"
proof -
define n where "n = length ds div 2"
define m where "m = Suc (length ds) div 2"
define xs where "xs = sort ds"
have xs: "sorted xs" unfolding xs_def by auto
have nm: "m ∈ {n, Suc n}" unfolding n_def m_def by auto
show ?thesis unfolding n_def[symmetric] m_def[symmetric] xs_def[symmetric]
using nm xs
proof (induct xs arbitrary: n m d)
case (Cons x xs n m d)
show ?case
proof (cases n)
case 0
with Cons(2) have m: "m = 0 ∨ m = 1" by auto
show ?thesis
proof (cases "d ≤ x")
case True
hence ins: "insort d (x # xs) = d # x # xs" by auto
show ?thesis unfolding ins 0 using True m by auto
next
case False
hence ins: "insort d (x # xs) = x # insort d xs" by auto
show ?thesis unfolding ins 0 using False m by auto
qed
next
case (Suc nn)
with Cons(2) obtain mm where m: "m = Suc mm" and mm: "mm ∈ {nn, Suc nn}" by auto
from Cons(3) have sort: "sorted xs" by (simp)
note IH = Cons(1)[OF mm]
show ?thesis
proof (cases "d ≤ x")
case True
with Cons(3) have ins: "insort d (x # xs) = d # insort x xs"
by (cases xs, auto)
show ?thesis unfolding ins Suc m using IH[OF sort] by auto
next
case False
hence ins: "insort d (x # xs) = x # insort d xs" by auto
show ?thesis unfolding ins Suc m using IH[OF sort] Cons(3) by auto
qed
qed
qed auto
qed
lemma max_factor_degree_mono:
"max_factor_degree (map degree (fold remove1 ws vs)) ≤ max_factor_degree (map degree vs)"
unfolding max_factor_degree_def Let_def length_sort length_map
proof (induct ws arbitrary: vs)
case (Cons w ws vs)
show ?case
proof (cases "w ∈ set vs")
case False
hence "remove1 w vs = vs" by (rule remove1_idem)
thus ?thesis using Cons[of vs] by auto
next
case True
then obtain bef aft where vs: "vs = bef @ w # aft" and rem1: "remove1 w vs = bef @ aft"
by (metis remove1.simps(2) remove1_append split_list_first)
let ?exp = "λ ws vs. sum_list (drop (length (fold remove1 ws vs) div 2)
(sort (map degree (fold remove1 ws vs))))"
let ?bnd = "λ vs. sum_list (drop (length vs div 2) (sort (map degree vs)))"
let ?bd = "λ vs. sum_list (drop (length vs div 2) (sort vs))"
define ba where "ba = bef @ aft"
define ds where "ds = map degree ba"
define d where "d = degree w"
have "?exp (w # ws) vs = ?exp ws (bef @ aft)" by (auto simp: rem1)
also have "… ≤ ?bnd ba" unfolding ba_def by (rule Cons)
also have "… = ?bd ds" unfolding ds_def by simp
also have "… ≤ sum_list (drop (Suc (length ds) div 2) (insort d (sort ds)))"
by (rule half_largest_elements_mono)
also have "… = ?bnd vs" unfolding vs ds_def d_def by (simp add: ba_def insort_middle)
finally show "?exp (w # ws) vs ≤ ?bnd vs" by simp
qed
qed auto
lemma mset_sub_decompose: "mset ds ⊆# mset bs + as ⟹ length ds < length bs ⟹ ∃ b1 b b2.
bs = b1 @ b # b2 ∧ mset ds ⊆# mset (b1 @ b2) + as"
proof (induct ds arbitrary: bs as)
case Nil
hence "bs = [] @ hd bs # tl bs" by auto
thus ?case by fastforce
next
case (Cons d ds bs as)
have "d ∈# mset (d # ds)" by auto
with Cons(2) have d: "d ∈# mset bs + as" by (rule mset_subset_eqD)
hence "d ∈ set bs ∨ d ∈# as" by auto
thus ?case
proof
assume "d ∈ set bs"
from this[unfolded in_set_conv_decomp] obtain b1 b2 where bs: "bs = b1 @ d # b2" by auto
from Cons(2) Cons(3)
have "mset ds ⊆# mset (b1 @ b2) + as" "length ds < length (b1 @ b2)" by (auto simp: ac_simps bs)
from Cons(1)[OF this] obtain b1' b b2' where split: "b1 @ b2 = b1' @ b # b2'"
and sub: "mset ds ⊆# mset (b1' @ b2') + as" by auto
from split[unfolded append_eq_append_conv2]
obtain us where "b1 = b1' @ us ∧ us @ b2 = b # b2' ∨ b1 @ us = b1' ∧ b2 = us @ b # b2'" ..
thus ?thesis
proof
assume "b1 @ us = b1' ∧ b2 = us @ b # b2'"
hence *: "b1 @ us = b1'" "b2 = us @ b # b2'" by auto
hence bs: "bs = (b1 @ d # us) @ b # b2'" unfolding bs by auto
show ?thesis
by (intro exI conjI, rule bs, insert * sub, auto simp: ac_simps)
next
assume "b1 = b1' @ us ∧ us @ b2 = b # b2'"
hence *: "b1 = b1' @ us" "us @ b2 = b # b2'" by auto
show ?thesis
proof (cases us)
case Nil
with * have *: "b1 = b1'" "b2 = b # b2'" by auto
hence bs: "bs = (b1' @ [d]) @ b # b2'" unfolding bs by simp
show ?thesis
by (intro exI conjI, rule bs, insert * sub, auto simp: ac_simps)
next
case (Cons u vs)
with * have *: "b1 = b1' @ b # vs" "vs @ b2 = b2'" by auto
hence bs: "bs = b1' @ b # (vs @ d # b2)" unfolding bs by auto
show ?thesis
by (intro exI conjI, rule bs, insert * sub, auto simp: ac_simps)
qed
qed
next
define as' where "as' = as - {#d#}"
assume "d ∈# as"
hence as': "as = {#d#} + as'" unfolding as'_def by auto
from Cons(2)[unfolded as'] Cons(3) have "mset ds ⊆# mset bs + as'" "length ds < length bs"
by (auto simp: ac_simps)
from Cons(1)[OF this] obtain b1 b b2 where bs: "bs = b1 @ b # b2" and
sub: "mset ds ⊆# mset (b1 @ b2) + as'" by auto
show ?thesis
by (intro exI conjI, rule bs, insert sub, auto simp: as' ac_simps)
qed
qed
lemma max_factor_degree_aux: fixes es :: "nat list"
assumes sub: "mset ds ⊆# mset es"
and len: "length ds + length ds ≤ length es" and sort: "sorted es"
shows "sum_list ds ≤ sum_list (drop (length es div 2) es)"
proof -
define bef where "bef = take (length es div 2) es"
define aft where "aft = drop (length es div 2) es"
have es: "es = bef @ aft" unfolding bef_def aft_def by auto
from len have len: "length ds ≤ length bef" "length ds ≤ length aft" unfolding bef_def aft_def
by auto
from sub have sub: "mset ds ⊆# mset bef + mset aft" unfolding es by auto
from sort have sort: "sorted (bef @ aft)" unfolding es .
show ?thesis unfolding aft_def[symmetric] using sub len sort
proof (induct ds arbitrary: bef aft)
case (Cons d ds bef aft)
have "d ∈# mset (d # ds)" by auto
with Cons(2) have "d ∈# mset bef + mset aft" by (rule mset_subset_eqD)
hence "d ∈ set bef ∨ d ∈ set aft" by auto
thus ?case
proof
assume "d ∈ set aft"
from this[unfolded in_set_conv_decomp] obtain a1 a2 where aft: "aft = a1 @ d # a2" by auto
from Cons(4) have len_a: "length ds ≤ length (a1 @ a2)" unfolding aft by auto
from Cons(2)[unfolded aft] Cons(3)
have "mset ds ⊆# mset bef + (mset (a1 @ a2))" "length ds < length bef" by auto
from mset_sub_decompose[OF this]
obtain b b1 b2
where bef: "bef = b1 @ b # b2" and sub: "mset ds ⊆# (mset (b1 @ b2) + mset (a1 @ a2))" by auto
from Cons(3) have len_b: "length ds ≤ length (b1 @ b2)" unfolding bef by auto
from Cons(5)[unfolded bef aft] have sort: "sorted ( (b1 @ b2) @ (a1 @ a2))"
unfolding sorted_append by auto
note IH = Cons(1)[OF sub len_b len_a sort]
show ?thesis using IH unfolding aft by simp
next
assume "d ∈ set bef"
from this[unfolded in_set_conv_decomp] obtain b1 b2 where bef: "bef = b1 @ d # b2" by auto
from Cons(3) have len_b: "length ds ≤ length (b1 @ b2)" unfolding bef by auto
from Cons(2)[unfolded bef] Cons(4)
have "mset ds ⊆# mset aft + (mset (b1 @ b2))" "length ds < length aft" by (auto simp: ac_simps)
from mset_sub_decompose[OF this]
obtain a a1 a2
where aft: "aft = a1 @ a # a2" and sub: "mset ds ⊆# (mset (b1 @ b2) + mset (a1 @ a2))"
by (auto simp: ac_simps)
from Cons(4) have len_a: "length ds ≤ length (a1 @ a2)" unfolding aft by auto
from Cons(5)[unfolded bef aft] have sort: "sorted ( (b1 @ b2) @ (a1 @ a2))" and ad: "d ≤ a"
unfolding sorted_append by auto
note IH = Cons(1)[OF sub len_b len_a sort]
show ?thesis using IH ad unfolding aft by simp
qed
qed auto
qed
lemma max_factor_degree: assumes sub: "mset ws ⊆# mset vs"
and len: "length ws + length ws ≤ length vs"
shows "degree (prod_list ws) ≤ max_factor_degree (map degree vs)"
proof -
define ds where "ds ≡ map degree ws"
define es where "es ≡ sort (map degree vs)"
from sub len have sub: "mset ds ⊆# mset es" and len: "length ds + length ds ≤ length es"
and es: "sorted es"
unfolding ds_def es_def
by (auto simp: image_mset_subseteq_mono)
have "degree (prod_list ws) ≤ sum_list (map degree ws)" by (rule degree_prod_list_le)
also have "… ≤ max_factor_degree (map degree vs)"
unfolding max_factor_degree_def Let_def ds_def[symmetric] es_def[symmetric]
using sub len es by (rule max_factor_degree_aux)
finally show ?thesis .
qed
lemma degree_bound: assumes sub: "mset ws ⊆# mset vs"
and len: "length ws + length ws ≤ length vs"
shows "degree (prod_list ws) ≤ degree_bound vs"
using max_factor_degree[OF sub len] unfolding degree_bound_def by auto
end