# Theory ExecutiblePolyProps

```text "Executable Polynomial Properties"
theory ExecutiblePolyProps
imports
Polynomials.MPoly_Type_Univariate
MPolyExtension
begin

text ‹(Univariate) Polynomial hiding›

lifting_update poly.lifting
lifting_forget poly.lifting

text ‹›

subsection "Lemmas with Monomial and Monomials"

lemma of_nat_monomial: "of_nat p = monomial p 0"
by (auto simp: poly_mapping_eq_iff lookup_of_nat fun_eq_iff lookup_single)

lemma of_nat_times_monomial: "of_nat p * monomial c i = monomial (p*c) i"
by (auto simp: poly_mapping_eq_iff prod_fun_def fun_eq_iff of_nat_monomial
lookup_single mult_single)

lemma monomial_adds_nat_iff: "monomial p i adds c ⟷ lookup c i ≥ p" for p::"nat"
apply (auto simp: adds_def lookup_add)
by (metis add.left_commute nat_le_iff_add remove_key_sum single_add)

lemma update_minus_monomial: "Poly_Mapping.update k i (m - monomial i k) = Poly_Mapping.update k i m"
by (auto simp: poly_mapping_eq_iff lookup_update update.rep_eq fun_eq_iff lookup_minus
lookup_single)

lemma monomials_Var: "monomials (Var x::'a::zero_neq_one mpoly) = {Poly_Mapping.single x 1}"
by transfer (auto simp: Var⇩0_def)

lemma monomials_Const: "monomials (Const x) = (if x = 0 then {} else {0})"
by transfer' (auto simp: Const⇩0_def)

lemma coeff_eq_zero_iff: "MPoly_Type.coeff c p = 0 ⟷ p ∉ monomials c"
by transfer (simp add: not_in_keys_iff_lookup_eq_zero)

lemma monomials_1[simp]: "monomials 1 = {0}"
by transfer auto

lemma monomials_and_monoms:
shows "(k ∈ monomials m) = (∃ (a::nat). a ≠ 0 ∧ (monomials (MPoly_Type.monom k a)) ⊆ monomials m)"
proof -
show ?thesis using monomials_monom by auto
qed

lemma mult_monomials_dir_one:
shows "monomials (p*q) ⊆ {a+b | a b . a ∈ monomials p ∧ b ∈ monomials q}"
using monomials_and_monoms mult_monom
by (simp add: keys_mult monomials.rep_eq times_mpoly.rep_eq)

lemma monom_eq_zero_iff[simp]: "MPoly_Type.monom a b = 0 ⟷ b = 0"
by (metis MPolyExtension.coeff_monom MPolyExtension.monom_zero)

lemma update_eq_plus_monomial:
"v ≥ lookup m k ⟹ Poly_Mapping.update k v m = m + monomial (v - lookup m k) k"
for v n::nat
by transfer auto

lemma coeff_monom_mult':
"MPoly_Type.coeff ((MPoly_Type.monom m' a) * q) (m'm)  = a * MPoly_Type.coeff q (m'm - m')"
if *: "m'm = m' + (m'm - m')"
by (subst *) (rule More_MPoly_Type.coeff_monom_mult)

lemma monomials_zero[simp]: "monomials 0 = {}"
by transfer auto

lemma in_monomials_iff: "x ∈ monomials m ⟷ MPoly_Type.coeff m x ≠ 0"
using coeff_eq_zero_iff[of m x] by auto

lemma monomials_monom_mult: "monomials (MPoly_Type.monom mon a * q) = (if a = 0 then {} else (+) mon ` monomials q)"
for q::"'a::semiring_no_zero_divisors mpoly"
apply auto
subgoal by transfer' (auto elim!: in_keys_timesE)
subgoal by (simp add: in_monomials_iff More_MPoly_Type.coeff_monom_mult)
done

subsection "Simplification Lemmas for Const 0 and Const 1"
lemma add_zero : "P + Const 0 = P"
proof -
have h:"P + 0 = P" using add_0_right by auto
show ?thesis unfolding Const_def using h by (simp add: Const⇩0_zero zero_mpoly.abs_eq)
qed

(* example *)
lemma add_zero_example : "((Var 0)^2 - (Const 1)) + Const 0 = ((Var 0)^2 - (Const 1))"
proof -
show ?thesis by (simp add : add_zero)
qed

lemma mult_zero_left : "Const 0 * P = Const 0"
proof -
have h:"0*P = 0" by simp
show ?thesis unfolding Const_def using h by (simp add: Const⇩0_zero zero_mpoly_def)
qed

lemma mult_zero_right : "P * Const 0 = Const 0"
by (metis mult_zero_left mult_zero_right)

lemma mult_one_left : "Const 1 * (P :: real mpoly) = P"
by (simp add: Const.abs_eq Const⇩0_one one_mpoly_def)

lemma mult_one_right : "(P::real mpoly) * Const 1 = P"
by (simp add: Const.abs_eq Const⇩0_one one_mpoly_def)

subsection "Coefficient Lemmas"
lemma coeff_zero[simp]: "MPoly_Type.coeff 0 x = 0"
by transfer auto

lemma coeff_sum: "MPoly_Type.coeff (sum f S) x = sum (λi. MPoly_Type.coeff (f i) x) S"
apply (induction S rule: infinite_finite_induct)
apply (auto)
by (metis More_MPoly_Type.coeff_add)

lemma coeff_mult_Var: "MPoly_Type.coeff (x * Var i ^ p) c = (MPoly_Type.coeff x (c - monomial p i) when lookup c i ≥ p)"
by transfer'
(auto simp: Var⇩0_def pprod.monomial_power lookup_times_monomial_right
of_nat_times_monomial monomial_adds_nat_iff)

lemma lookup_update_self[simp]: "Poly_Mapping.update i (lookup m i) m = m"
by (auto simp: lookup_update intro!: poly_mapping_eqI)

lemma coeff_Const: "MPoly_Type.coeff (Const p) m = (p when m = 0)"
by transfer' (auto simp: Const⇩0_def lookup_single)

lemma coeff_Var: "MPoly_Type.coeff (Var p) m = (1 when m = monomial 1 p)"
by transfer' (auto simp: Var⇩0_def lookup_single when_def)

subsection "Miscellaneous"
lemma update_0_0[simp]: "Poly_Mapping.update x 0 0 = 0"
by (metis lookup_update_self lookup_zero)

lemma mpoly_eq_iff: "p = q ⟷ (∀m. MPoly_Type.coeff p m = MPoly_Type.coeff q m)"
by transfer (auto simp: poly_mapping_eqI)

lemma power_both_sides :
assumes Ah : "(A::real) ≥0"
assumes Bh : "(B::real) ≥0"
shows "(A≤B) = (A^2≤B^2)"
using Ah Bh by (meson power2_le_imp_le power_mono)

lemma in_list_induct_helper:
assumes "set(xs)⊆X"
assumes  "P []"
assumes "(⋀x. x∈X ⟹ ( ⋀xs. P xs ⟹ P (x # xs)))"
shows "P xs" using assms(1)
proof(induction xs)
case Nil
then show ?case using assms by auto
next
case (Cons a xs)
then show ?case using assms(3) by auto
qed

theorem in_list_induct [case_names Nil Cons]:
assumes  "P []"
assumes "(⋀x. x∈set(xs) ⟹ ( ⋀xs. P xs ⟹ P (x # xs)))"
shows "P xs"
using in_list_induct_helper[of xs "set(xs)" P] using assms by auto

subsubsection "Keys and vars"

lemma inKeys_inVars : "a≠0 ⟹ x ∈ keys m ⟹ x ∈ vars(MPoly_Type.monom m a)"
by(simp add: vars_def)

lemma notInKeys_notInVars : "x ∉ keys m ⟹ x ∉ vars(MPoly_Type.monom m a)"
by(simp add: vars_def)

lemma lookupNotIn : "x ∉ keys m ⟹ lookup m x = 0"
by (simp add: in_keys_iff)

subsection "Degree Lemmas"

lemma degree_le_iff: "MPoly_Type.degree p x ≤ k ⟷ (∀m∈monomials p. lookup m x ≤ k)"
by transfer simp

lemma degree_less_iff: "MPoly_Type.degree p x < k ⟷ (k>0 ∧ (∀m∈monomials p. lookup m x < k))"
by (transfer fixing: k) (cases "k = 0"; simp)

lemma degree_ge_iff: "k > 0 ⟹ MPoly_Type.degree p x ≥ k ⟷ (∃m∈monomials p. lookup m x ≥ k)"
using Max_ge_iff by (meson degree_less_iff not_less)

lemma degree_greater_iff: "MPoly_Type.degree p x > k ⟷ (∃m∈monomials p. lookup m x > k)"
by transfer' (auto simp: Max_gr_iff)

lemma degree_eq_iff:
"MPoly_Type.degree p x = k ⟷ (if k = 0
then (∀m∈monomials p. lookup m x = 0)
else (∃m∈monomials p. lookup m x = k) ∧ (∀m∈monomials p. lookup m x ≤ k))"
by (subst eq_iff) (force simp: degree_le_iff degree_ge_iff intro!: antisym)

declare poly_mapping.lookup_inject[simp del]

lemma lookup_eq_and_update_lemma: "lookup m var = deg ∧ Poly_Mapping.update var 0 m = x ⟷
m = Poly_Mapping.update var deg x ∧ lookup x var = 0"
unfolding poly_mapping_eq_iff
by (force simp: update.rep_eq fun_eq_iff)

lemma degree_const : "MPoly_Type.degree (Const (z::real)) (x::nat) = 0"
by (simp add: degree_eq_iff monomials_Const)

lemma degree_one : "MPoly_Type.degree (Var x :: real mpoly) x = 1"
by(simp add: degree_eq_iff monomials_Var)

subsection "Lemmas on treating a multivariate polynomial as univariate "
lemma coeff_isolate_variable_sparse:
"MPoly_Type.coeff (isolate_variable_sparse p var deg) x =
(if lookup x var = 0
then MPoly_Type.coeff p (Poly_Mapping.update var deg x)
else 0)"
apply (transfer fixing: x var deg p)
unfolding lookup_sum
unfolding lookup_single
apply (auto simp: when_def)
apply (subst sum.inter_filter[symmetric])
subgoal by simp
subgoal by (simp add: lookup_eq_and_update_lemma Collect_conv_if)
by (auto intro!: sum.neutral simp add: lookup_update)

lemma isovarspar_sum:
"isolate_variable_sparse (p+q) var deg =
isolate_variable_sparse (p) var deg
+ isolate_variable_sparse (q) var deg"
apply (auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse )
apply (metis More_MPoly_Type.coeff_add coeff_isolate_variable_sparse)
by (metis More_MPoly_Type.coeff_add add.comm_neutral coeff_isolate_variable_sparse less_numeral_extra(3))

lemma isolate_zero[simp]: "isolate_variable_sparse 0 var n = 0"
by transfer' (auto simp: mpoly_eq_iff)

lemma coeff_isolate_variable_sparse_minus_monomial:
"MPoly_Type.coeff (isolate_variable_sparse mp var i) (m - monomial i var) =
(if lookup m var ≤ i then MPoly_Type.coeff mp (Poly_Mapping.update var i m) else 0)"
by (simp add: coeff_isolate_variable_sparse lookup_minus update_minus_monomial)

lemma sum_over_zero: "(mp::real mpoly) = (∑i::nat ≤MPoly_Type.degree mp x. isolate_variable_sparse mp x i * Var x^i)"
by (auto simp add: mpoly_eq_iff coeff_sum coeff_mult_Var if_if_eq_conj not_le
coeff_isolate_variable_sparse_minus_monomial when_def lookup_update degree_less_iff
simp flip: eq_iff
intro!: coeff_not_in_monomials)

lemma const_lookup_zero : "isolate_variable_sparse (Const p ::real mpoly) (x::nat) (0::nat) = Const p"
by (auto simp: mpoly_eq_iff coeff_isolate_variable_sparse coeff_Const when_def)
(metis lookup_update_self)

lemma const_lookup_suc : "isolate_variable_sparse (Const p :: real mpoly) x (Suc i) = 0"
apply(auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse coeff_Const when_def)
by (metis lookup_update lookup_zero nat.distinct(1))

lemma isovar_greater_degree : "∀i > MPoly_Type.degree p var. isolate_variable_sparse p var i = 0"
apply(auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse degree_less_iff)
by (metis coeff_not_in_monomials less_irrefl_nat lookup_update)

lemma isolate_var_0 : "isolate_variable_sparse (Var x::real mpoly) x 0 = 0"
apply(auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse coeff_Var when_def)
by (metis gr0I lookup_single_eq lookup_update_self n_not_Suc_n)

lemma isolate_var_one : "isolate_variable_sparse (Var x :: real mpoly) x 1 = 1"
by (auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse coeff_Var coeff_eq_zero_iff)
(smt More_MPoly_Type.coeff_monom One_nat_def add_diff_cancel_left' lookup_eq_and_update_lemma
lookup_single_eq lookup_update_self monom_one plus_1_eq_Suc single_diff single_zero update_minus_monomial)

lemma isovarspase_monom :
assumes notInKeys : "x ∉ keys m"
assumes notZero : "a ≠ 0"
shows "isolate_variable_sparse (MPoly_Type.monom m a) x 0 = (MPoly_Type.monom m a :: real mpoly)"
using assms
by (auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse coeff_eq_zero_iff in_keys_iff)
(metis lookup_update_self)

lemma isolate_variable_spase_zero : "lookup m x = 0 ⟹
insertion (nth L) ((MPoly_Type.monom m a)::real mpoly) = 0 ⟹
a ≠ 0 ⟹ insertion (nth L) (isolate_variable_sparse (MPoly_Type.monom m a) x 0) = 0"
by (simp add: isovarspase_monom lookup_eq_zero_in_keys_contradict notInKeys_notInVars)

lemma isovarsparNotIn : "x ∉ vars (p::real mpoly) ⟹ isolate_variable_sparse p x 0 = p"
proof(induction p rule: mpoly_induct)
case (monom m a)
then show ?case
apply(cases "a=0")
by (simp_all add: isovarspase_monom vars_monom_keys)
next
case (sum p1 p2 m a)
then show ?case
by (simp add: monomials.rep_eq vars_add_monom isovarspar_sum)
qed

lemma degree0isovarspar :
assumes deg0 : "MPoly_Type.degree (p::real mpoly) x = 0"
shows "isolate_variable_sparse p x 0 = p"
proof -
have h1 : "p = (∑i::nat ≤MPoly_Type.degree p x. isolate_variable_sparse p x i * Var x ^ i)"
using sum_over_zero by auto
have h2a : "∀f. (∑i::nat ≤0. f i) = f 0"
apply(simp add: sum_def)
by (metis add.right_neutral comm_monoid_add_class.sum_def finite.emptyI insert_absorb insert_not_empty sum.empty sum.insert)
have h2 : "p = isolate_variable_sparse p x 0 * Var x ^ 0"
using deg0 h1 h2a by auto
show ?thesis using h2
by auto
qed

subsection "Summation Lemmas"

lemma summation_normalized :
assumes nonzero : "(B ::real) ≠0"
shows "(∑i = 0..<((n::nat)+1). (f i :: real) * B ^ (n - i)) = (∑i = 0..<(n+1). (f i) / (B ^ i)) * (B^n)"
proof -
have h1a : "∀x::real. ((∑i = 0..<(n+1). (f i) / (B ^ i)) * x = (∑i = 0..<(n+1). ((f i) / (B ^ i)) * x))"
apply(induction n )
apply(auto)
by (simp add: distrib_right)
have h1 : "(∑i = 0..<(n+1). (f i) / (B ^ i)) * (B^n) = (∑i = 0..<(n+1). ((f i) / (B ^ i)) * (B^n))"
using h1a by auto
have h2 : "(∑i = 0..<(n+1). ((f i) / (B ^ i)) * (B^n)) = (∑i = 0..<(n+1). (f i) * ((B^n) / (B ^ i)))"
by auto
have h3 : "(∑i = 0..<(n+1). (f i) * ((B^n) / (B ^ i))) = (∑i = 0..<(n+1). (f i) * B ^ (n - i))"
using add.right_neutral nonzero power_diff by fastforce
show ?thesis using h1 h2 h3 by auto
qed

lemma normalize_summation :
assumes nonzero : "(B::real)≠0"
shows "(∑i = 0..<n+1. f i * B ^ (n - i))= 0
⟷
(∑i = 0..<(n::nat)+1. (f i::real) / (B ^ i)) = 0"
proof -
have pow_zero : "∀i. B^(i :: nat)≠0" using nonzero by(auto)
have single_division_zero : "∀X. B*(X::real)=0 ⟷ X=0" using nonzero by(auto)
have h1: "(∑i = 0..<n+1. (f i) / (B ^ i)) = 0 ⟷ ((∑i = 0..<n+1. (f i) / (B ^ i)))*B^n = 0"
using nonzero single_division_zero by(auto)
have h2: "((∑i = 0..<n+1. (f i) / (B ^ i))*(B^n)) = ((∑i = 0..<n+1. (f i) * (B ^ (n- i))))"
using summation_normalized nonzero by auto
show ?thesis using h1 h2 by auto
qed

lemma normalize_summation_less :
assumes nonzero : "(B::real)≠0"
shows "(∑i = 0..<(n+1). (f i) * B ^ (n - i)) * B ^ (n mod 2) < 0
⟷
(∑i = 0..<((n::nat)+1). (f i::real) / (B ^ i)) < 0"
proof -
have h1 : "(∑i = 0..<(n+1). (f i) * B ^ (n - i)) * B ^ (n mod 2) < 0
⟷  (∑i = 0..<(n+1). (f i) / (B ^ i)) * (B^n) * B ^ (n mod 2) < 0"
using summation_normalized nonzero by auto
have h2a : "n mod 2 = 0 ∨ n mod 2 = 1" by auto
have h2b : "n mod 2 = 1 ⟹ odd n" by auto
have h2c : "(B^n) * B ^ (n mod 2) > 0"
using h2a h2b apply auto
using nonzero apply presburger
by (metis even_Suc mult.commute nonzero power_Suc zero_less_power_eq)
have h2 : "∀x. ((x * (B^n) * B ^ (n mod 2) < 0) = (x<0))"
using h2c using mult.assoc by (metis mult_less_0_iff not_square_less_zero)
show ?thesis using h1 h2 by auto
qed

subsection "Additional Lemmas with Vars"

lemma not_in_isovarspar : "isolate_variable_sparse (p::real mpoly) var x = (q::real mpoly) ⟹ var∉(vars q)"
apply(simp add: isolate_variable_sparse_def vars_def)
proof -
assume a1: "MPoly (∑m | m ∈ monomials p ∧ lookup m var = x. monomial (MPoly_Type.coeff p m) (Poly_Mapping.update var 0 m)) = q"
{ fix pp :: "nat ⇒⇩0 nat"
have "isolate_variable_sparse p var x = q"
using a1 isolate_variable_sparse.abs_eq by blast
then have "var ∉ keys pp ∨ pp ∉ keys (mapping_of q)"
by (metis (no_types) coeff_def coeff_isolate_variable_sparse in_keys_iff) }
then show "∀p∈keys (mapping_of q). var ∉ keys p"
by meson
qed

lemma not_in_add : "var∉(vars (p::real mpoly)) ⟹ var∉(vars (q::real mpoly)) ⟹ var∉(vars (p+q))"
by (meson UnE in_mono vars_add)

lemma not_in_mult : "var∉(vars (p::real mpoly)) ⟹ var∉(vars (q::real mpoly)) ⟹ var∉(vars (p*q))"
by (meson UnE in_mono vars_mult)

lemma not_in_neg : "var∉(vars(p::real mpoly)) ⟷ var∉(vars(-p))"
proof -
have h: "var ∉ (vars (-1::real mpoly))" by (metis add_diff_cancel_right' add_neg_numeral_special(8) isolate_var_one isolate_zero isovarsparNotIn isovarspar_sum not_in_isovarspar)
show ?thesis using not_in_mult using h by fastforce
qed

lemma not_in_sub : "var∉(vars (p::real mpoly)) ⟹ var∉(vars (q::real mpoly)) ⟹ var∉(vars (p-q))"
using not_in_add not_in_neg by fastforce

lemma not_in_pow : "var∉(vars(p::real mpoly)) ⟹ var∉(vars(p^i))"
proof (induction i)
case 0
then show ?case using isolate_var_one not_in_isovarspar
by (metis power_0)
next
case (Suc i)
then show ?case using not_in_mult by simp
qed

lemma not_in_sum_var: "(∀i. var∉(vars(f(i)::real mpoly))) ⟹ var∉(vars(∑i∈{0..<(n::nat)}.f(i)))"
proof (induction n)
case 0
then show ?case using isolate_zero not_in_isovarspar by fastforce
next
case (Suc n)
have h1: "(sum f {0..<Suc n}) = (sum f {0..< n}) + (f n)" using sum.atLeast0_lessThan_Suc by blast
have h2: "var ∉ vars (f n)" by (simp add: Suc.prems)
then show ?case using h1 vars_add by (simp add: Suc.IH Suc.prems not_in_add)
qed

lemma not_in_sum : "(∀i. var∉(vars(f(i)::real mpoly))) ⟹ ∀(n::nat). var∉(vars(∑i∈{0..<n}.f(i)))"
using not_in_sum_var by blast

lemma not_contains_insertion_helper :
"∀x∈keys (mapping_of p). var ∉ keys x ⟹
(⋀k f. (k ∉ keys f) = (lookup f k = 0)) ⟹
lookup (mapping_of p) a = 0 ∨
(∏aa. (if aa < length L then L[var := y] ! aa else 0) ^ lookup a aa) =
(∏aa. (if aa < length L then L[var := x] ! aa else 0) ^ lookup a aa)"
apply(cases "lookup (mapping_of p) a = 0")
apply auto
apply(rule Prod_any.cong)
apply auto
using lookupNotIn nth_list_update_neq power_0 by smt

lemma not_contains_insertion :
assumes notIn : "var ∉ vars (p:: real mpoly)"
assumes exists : "insertion (nth_default 0 (list_update L var x)) p = val"
shows "insertion (nth_default 0 (list_update L var y)) p = val"
using notIn exists
apply(simp add: insertion_def insertion_aux_def insertion_fun_def)
unfolding vars_def nth_default_def
using not_in_keys_iff_lookup_eq_zero
apply auto
apply(rule Sum_any.cong)
apply simp
using not_contains_insertion_helper[of p var _ L y x]
proof -
fix a :: "nat ⇒⇩0 nat"
assume a1: "∀x∈keys (mapping_of p). var ∉ keys x"
assume "⋀k f. ((k::'a) ∉ keys f) = (lookup f k = 0)"
then show "lookup (mapping_of p) a = 0 ∨ (∏n. (if n < length L then L[var := y] ! n else 0) ^ lookup a n) = (∏n. (if n < length L then L[var := x] ! n else 0) ^ lookup a n)"
using a1 ‹⋀a. ⟦∀x∈keys (mapping_of p). var ∉ keys x; ⋀k f. (k ∉ keys f) = (lookup f k = 0)⟧ ⟹ lookup (mapping_of p) a = 0 ∨ (∏aa. (if aa < length L then L[var := y] ! aa else 0) ^ lookup a aa) = (∏aa. (if aa < length L then L[var := x] ! aa else 0) ^ lookup a aa)› by blast
qed

subsection "Insertion Lemmas"
lemma insertion_sum_var : "((insertion f (∑i∈{0..<(n::nat)}.g(i))) = (∑i∈{0..<n}. insertion f (g i)))"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case by (simp add: insertion_add)
qed

(* changed to explicitly typecast n as a nat *)
lemma insertion_sum : "∀(n::nat). ((insertion f (∑i∈{0..<n}.g(i))) = (∑i∈{0..<n}. insertion f (g i)))"
using insertion_sum_var by blast

lemma insertion_sum' : "⋀(n::nat). ((insertion f (∑i≤n. g(i))) = (∑i≤n. insertion f (g i)))"
by (metis (no_types, lifting) fun_sum_commute insertion_add insertion_zero sum.cong)

lemma insertion_pow : "insertion f (p^i) = (insertion f p)^i"
proof (induction i)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case by (simp add: insertion_mult)
qed

lemma insertion_neg : "insertion f (-p) = -insertion f p"
by (metis add.inverse_inverse insertionNegative)

lemma insertion_var :
"length L > var ⟹ insertion (nth_default 0 (list_update L var x)) (Var var) = x"
by (auto simp: monomials_Var coeff_Var insertion_code nth_default_def)

lemma insertion_var_zero : "insertion (nth_default 0 (x#xs)) (Var 0) = x" using insertion_var
by fastforce

lemma notIn_insertion_sub : "x∉vars(p::real mpoly) ⟹ x∉vars(q::real mpoly)
⟹ insertion f (p-q) = insertion f p - insertion f q"
by (metis ab_group_add_class.ab_diff_conv_add_uminus insertion_add insertion_neg)

lemma insertion_sub : "insertion f (A-B :: real mpoly) = insertion f A - insertion f B"
using insertion_neg insertion_add
by (metis uminus_add_conv_diff)

lemma insertion_four : "insertion ((nth_default 0) xs) 4 = 4"
by (metis (no_types, lifting) insertion_add insertion_one numeral_plus_numeral one_add_one semiring_norm(2) semiring_norm(6))

lemma insertion_add_ind_basecase:
"insertion (nth (list_update L var x)) ((∑i::nat ≤ 0. isolate_variable_sparse p var i * (Var var)^i))
= (∑i = 0..<(0+1).  insertion (nth (list_update L var x)) (isolate_variable_sparse p var i * (Var var)^i))"
proof -
have h1: "((∑i::nat ≤ 0. isolate_variable_sparse p var i * (Var var)^i))
= (isolate_variable_sparse p var 0 * (Var var)^0)"
by auto
show ?thesis using h1
by auto
qed

lemma insertion_add_ind:
"insertion (nth_default 0 (list_update L var x)) ((∑i::nat ≤ d. isolate_variable_sparse p var i * (Var var)^i))
= (∑i = 0..<(d+1).  insertion (nth_default 0 (list_update L var x)) (isolate_variable_sparse p var i * (Var var)^i))"
proof (induction d)
case 0
then show ?case using insertion_add_ind_basecase nth_default_def
by auto
next
case (Suc n)
then show ?case using insertion_add apply auto
by (simp add: insertion_add)
qed

lemma sum_over_degree_insertion :
assumes lLength : "length L > var"
assumes deg : "MPoly_Type.degree (p::real mpoly) var = d"
shows "(∑i = 0..<(d+1). insertion (nth_default 0 (list_update L var x)) (isolate_variable_sparse p var i) * (x^i))
= insertion (nth_default 0 (list_update L var x)) p"
proof -
have h1: "(p::real mpoly) = (∑i::nat ≤(MPoly_Type.degree p var). isolate_variable_sparse p var i * (Var var)^i)" using sum_over_zero by auto
have h2: "insertion (nth_default 0 (list_update L var x)) p =
insertion (nth_default 0 (list_update L var x)) ((∑i::nat ≤ d. isolate_variable_sparse p var i * (Var var)^i))" using h1 deg by auto
have h3:  "insertion (nth_default 0 (list_update L var x)) p = (∑i = 0..<(d+1).  insertion (nth_default 0 (list_update L var x)) (isolate_variable_sparse p var i * (Var var)^i))"
using h2 insertion_add_ind nth_default_def
by simp
show ?thesis using h3 insertion_var insertion_pow
by (metis (no_types, lifting) insertion_mult lLength sum.cong)
qed

lemma insertion_isovarspars_free :
"insertion (nth_default 0 (list_update L var x)) (isolate_variable_sparse (p::real mpoly) var (i::nat))
=insertion (nth_default 0 (list_update L var y)) (isolate_variable_sparse (p::real mpoly) var (i::nat))"
proof -
have h : "var ∉ vars(isolate_variable_sparse (p::real mpoly) var (i::nat))"
by (simp add: not_in_isovarspar)
then show ?thesis using not_contains_insertion
by blast
qed
lemma insertion_zero : "insertion f (Const 0 ::real mpoly) = 0"
by (metis add_cancel_right_right add_zero insertion_zero)

lemma insertion_one : "insertion f (Const 1 ::real mpoly) = 1"
by (metis insertion_one mult.right_neutral mult_one_left)

lemma insertion_const : "insertion f (Const c::real mpoly) = (c::real)"
by (auto simp: monomials_Const coeff_Const insertion_code)

subsection "Putting Things Together"
subsubsection "More Degree Lemmas"
lemma degree_add_leq :
assumes h1 : "MPoly_Type.degree a var ≤ x"
assumes h2 : "MPoly_Type.degree b var ≤ x"
shows "MPoly_Type.degree (a+b) var ≤ x"
using degree_eq_iff coeff_add coeff_not_in_monomials
by (smt (z3) More_MPoly_Type.coeff_add add.left_neutral coeff_eq_zero_iff degree_le_iff h1 h2)

lemma degree_add_less :
assumes h1 : "MPoly_Type.degree a var < x"
assumes h2 : "MPoly_Type.degree b var < x"
shows "MPoly_Type.degree (a+b) var < x"
by (metis degree_add_leq h1 h2 linorder_not_le nat_less_le)

lemma degree_sum : "(∀i∈{0..n::nat}. MPoly_Type.degree (f i :: real mpoly) var ≤ x) ⟹ (MPoly_Type.degree (∑x∈{0..n}. f x) var) ≤ x"
proof(induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case by(simp add: degree_add_leq)
qed

lemma degree_sum_less : "(∀i∈{0..n::nat}. MPoly_Type.degree (f i :: real mpoly) var < x) ⟹ (MPoly_Type.degree (∑x∈{0..n}. f x) var) < x"
proof(induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case by(simp add: degree_add_less)
qed

lemma varNotIn_degree :
assumes "var ∉ vars p"
shows "MPoly_Type.degree p var = 0"
proof-
have "∀m∈monomials p. lookup m var = 0"
using assms unfolding vars_def keys_def
using monomials.rep_eq by fastforce
then show ?thesis
using degree_less_iff by blast
qed

lemma degree_mult_leq :
assumes pnonzero: "(p::real mpoly)≠0"
assumes qnonzero: "(q::real mpoly)≠0"
shows "MPoly_Type.degree ((p::real mpoly) * (q::real mpoly)) var ≤ (MPoly_Type.degree p var) + (MPoly_Type.degree q var)"
proof(cases "MPoly_Type.degree (p*q) var =0")
case True
then show ?thesis by simp
next
case False
have hp: "∀m∈monomials p. lookup m var ≤ MPoly_Type.degree p var" using degree_eq_iff
by (metis zero_le)
have hq: "∀m∈monomials q. lookup m var ≤ MPoly_Type.degree q var" using degree_eq_iff
by (metis zero_le)
have hpq: "∀m∈{a+b | a b . a ∈ monomials p ∧ b ∈ monomials q}.
lookup m var ≤ (MPoly_Type.degree p var) + (MPoly_Type.degree q var)"
by (smt add_le_mono hp hq mem_Collect_eq plus_poly_mapping.rep_eq)
have h1: "(∀m∈monomials (p*q). lookup m var ≤ (MPoly_Type.degree p var) + (MPoly_Type.degree q var))"
using mult_monomials_dir_one hpq
by blast
then show ?thesis using h1 degree_eq_iff False
by (simp add: degree_le_iff)
qed

lemma degree_exists_monom:
assumes "p≠0"
shows  "∃m∈monomials p. lookup m var = MPoly_Type.degree p var"
proof(cases "MPoly_Type.degree p var =0")
case True
have h1: "∃m∈monomials p. lookup m var = 0" unfolding monomials_def
by (metis True assms(1) aux degree_eq_iff in_keys_iff mapping_of_inject monomials.rep_eq monomials_def zero_mpoly.rep_eq)
then show ?thesis using h1
using True by simp
next
case False
then show ?thesis using degree_eq_iff assms(1) apply(auto)
by (metis degree_eq_iff dual_order.strict_iff_order)
qed

lemma degree_not_exists_monom:
assumes "p≠0"
shows  "¬ (∃ m∈monomials p. lookup m var > MPoly_Type.degree p var)"
proof -
show ?thesis using degree_less_iff by blast
qed

lemma degree_monom: "MPoly_Type.degree (MPoly_Type.monom x y) v = (if y = 0 then 0 else lookup x v)"
by (auto simp: degree_eq_iff)

lemma degree_plus_disjoint:
"MPoly_Type.degree (p + MPoly_Type.monom m c) v = max (MPoly_Type.degree p v) (MPoly_Type.degree (MPoly_Type.monom m c) v)"
if "m ∉ monomials p"
for p::"real mpoly"
using that
apply (subst degree_eq_iff)
apply (auto simp: monomials_add_disjoint)
apply (auto simp: degree_eq_iff degree_monom)
apply (metis MPoly_Type.degree_zero degree_exists_monom less_numeral_extra(3))
using degree_le_iff apply blast
using degree_eq_iff
apply (metis max_def neq0_conv)
apply (metis degree_eq_iff max.coboundedI1 neq0_conv)
apply (metis MPoly_Type.degree_zero degree_exists_monom max_def zero_le)
using degree_le_iff max.cobounded1 by blast

subsubsection "More isolate\\_variable\\_sparse lemmas"

lemma isolate_variable_sparse_ne_zeroD:
"isolate_variable_sparse mp v x ≠ 0 ⟹ x ≤ MPoly_Type.degree mp v"
using isovar_greater_degree leI by blast

context includes poly.lifting begin
lift_definition mpoly_to_nested_poly::"'a::comm_monoid_add mpoly ⇒ nat ⇒ 'a mpoly Polynomial.poly" is
"λ(mp::'a mpoly) (v::nat) (p::nat). isolate_variable_sparse mp v p"
― ‹note \<^const>‹extract_var› nests the other way around›
unfolding MOST_iff_cofinite
proof -
fix mp::"'a mpoly" and v::nat
have "{p. isolate_variable_sparse mp v p ≠ 0} ⊆ {0..MPoly_Type.degree mp v}"
(is "?s ⊆ _")
by (auto dest!: isolate_variable_sparse_ne_zeroD)
also have "finite …" by simp
finally (finite_subset) show "finite ?s" .
qed

lemma degree_eq_0_mpoly_to_nested_polyI:
"mpoly_to_nested_poly mp v = 0 ⟹ MPoly_Type.degree mp v = 0"
apply transfer'
apply (simp add: degree_eq_iff)
apply transfer'
apply (auto simp: fun_eq_iff)
proof -
fix mpa :: "'a mpoly" and va :: nat and m :: "nat ⇒⇩0 nat"
assume a1: "∀x. (∑m | m ∈ monomials mpa ∧ lookup m va = x. monomial (MPoly_Type.coeff mpa m) (Poly_Mapping.update va 0 m)) = 0"
assume a2: "m ∈ monomials mpa"
have f3: "∀m p. lookup (mapping_of m) p ≠ (0::'a) ∨ p ∉ monomials m"
by (metis (full_types) coeff_def coeff_eq_zero_iff)
have f4: "∀n. mapping_of (isolate_variable_sparse mpa va n) = 0"
using a1 by (simp add: isolate_variable_sparse.rep_eq)
have "∀p n. lookup 0 (p::nat ⇒⇩0 nat) = (0::'a) ∨ (0::nat) = n"
by simp
then show "lookup m va = 0"
using f4 f3 a2 by (metis coeff_def coeff_isolate_variable_sparse lookup_eq_and_update_lemma)
qed

lemma coeff_eq_zero_mpoly_to_nested_polyD: "mpoly_to_nested_poly mp v = 0 ⟹ MPoly_Type.coeff mp 0 = 0"
apply transfer'
apply transfer'
by (metis (no_types) coeff_def coeff_isolate_variable_sparse isolate_variable_sparse.rep_eq lookup_zero update_0_0)

lemma mpoly_to_nested_poly_eq_zero_iff[simp]:
"mpoly_to_nested_poly mp v = 0 ⟷ mp = 0"
apply (auto simp: coeff_eq_zero_mpoly_to_nested_polyD degree_eq_0_mpoly_to_nested_polyI)
proof -
show "mpoly_to_nested_poly mp v = 0 ⟹ mp = 0"
apply (frule degree_eq_0_mpoly_to_nested_polyI)
apply (frule coeff_eq_zero_mpoly_to_nested_polyD)
apply (transfer' fixing: mp v)
apply (transfer' fixing: mp v)
apply (auto simp: fun_eq_iff mpoly_eq_iff intro!: sum.neutral)
proof -
fix m :: "nat ⇒⇩0 nat"
assume a1: "∀x. (∑m | m ∈ monomials mp ∧ lookup m v = x. monomial (MPoly_Type.coeff mp m) (Poly_Mapping.update v 0 m)) = 0"
assume a2: "MPoly_Type.degree mp v = 0"
have "∀n. isolate_variable_sparse mp v n = 0"
using a1 by (simp add: isolate_variable_sparse.abs_eq zero_mpoly.abs_eq)
then have f3: "∀p. MPoly_Type.coeff mp p = MPoly_Type.coeff 0 p ∨ lookup p v ≠ 0"
by (metis (no_types) coeff_isolate_variable_sparse lookup_update_self)
then show "MPoly_Type.coeff mp m = 0"
using a2 coeff_zero
by (metis coeff_not_in_monomials degree_eq_iff)
qed
show "mp = 0 ⟹ mpoly_to_nested_poly 0 v = 0"
subgoal
apply transfer'
apply transfer'
by (auto simp: fun_eq_iff intro!: sum.neutral)
done
qed

lemma isolate_variable_sparse_degree_eq_zero_iff: "isolate_variable_sparse p v (MPoly_Type.degree p v) = 0 ⟷ p = 0"
apply (transfer')
apply auto
proof -
fix pa :: "'a mpoly" and va :: nat
assume "(∑m | m ∈ monomials pa ∧ lookup m va = MPoly_Type.degree pa va. monomial (MPoly_Type.coeff pa m) (Poly_Mapping.update va 0 m)) = 0"
then have "mapping_of (isolate_variable_sparse pa va (MPoly_Type.degree pa va)) = 0"
by (simp add: isolate_variable_sparse.rep_eq)
then show "pa = 0"
by (metis (no_types) coeff_def coeff_eq_zero_iff coeff_isolate_variable_sparse degree_exists_monom lookup_eq_and_update_lemma lookup_zero)
qed

lemma degree_eq_univariate_degree: "MPoly_Type.degree p v =
(if p = 0 then 0 else Polynomial.degree (mpoly_to_nested_poly p v))"
apply auto
apply (rule antisym)
subgoal
apply (rule Polynomial.le_degree)
apply auto
apply transfer'
by (simp add: isolate_variable_sparse_degree_eq_zero_iff)
subgoal apply (rule Polynomial.degree_le)
apply (auto simp: elim!: degree_eq_zeroE)
apply transfer'
by (simp add: isovar_greater_degree)
done

lemma compute_mpoly_to_nested_poly[code]:
"coeffs (mpoly_to_nested_poly mp v) =
(if mp = 0 then []
else map (isolate_variable_sparse mp v) [0..<Suc(MPoly_Type.degree mp v)])"
unfolding coeffs_def unfolding mpoly_to_nested_poly_eq_zero_iff degree_eq_univariate_degree apply auto
subgoal by transfer' (rule refl)
by transfer' (rule refl)

end

lemma isolate_variable_sparse_monom: "isolate_variable_sparse (MPoly_Type.monom m a) v i =
(if a = 0 ∨ lookup m v ≠ i then 0 else MPoly_Type.monom (Poly_Mapping.update v 0 m) a)"
proof -
have *: "{x. x = m ∧ lookup x v = i} = (if lookup m v = i then {m} else {})"
by auto
show ?thesis
by (transfer' fixing: m a v i) (simp add:*)
qed

lemma isolate_variable_sparse_monom_mult:
"isolate_variable_sparse (MPoly_Type.monom m a * q) v n =
(if n ≥ lookup m v
then MPoly_Type.monom (Poly_Mapping.update v 0 m) a * isolate_variable_sparse q v (n - lookup m v)
else 0)"
for q::"'a::semiring_no_zero_divisors mpoly"
apply (auto simp: MPoly_Type.mult_monom)
subgoal
apply transfer'
subgoal for mon v i a q
apply (auto simp add: monomials_monom_mult sum_distrib_left)
apply (rule sum.reindex_bij_witness_not_neutral[where
j="λa. a - mon"
and i="λa. mon + a"
and S'="{}"
and T'="{}"
])
apply (auto simp: lookup_add)
apply (auto simp: poly_mapping_eq_iff fun_eq_iff single.rep_eq Poly_Mapping.mult_single)
apply (auto simp: when_def More_MPoly_Type.coeff_monom_mult)
by (auto simp: lookup_update lookup_add split: if_splits)
done
subgoal
apply transfer'
apply (auto intro!: sum.neutral simp: monomials_monom_mult )
apply (rule poly_mapping_eqI)
apply (auto simp: lookup_single when_def)
by (simp add: lookup_add)
done

lemma isolate_variable_sparse_mult:
"isolate_variable_sparse (p * q) v n = (∑i≤n. isolate_variable_sparse p v i * isolate_variable_sparse q v (n - i))"
for p q::"'a::semiring_no_zero_divisors mpoly"
proof (induction p rule: mpoly_induct)
case (monom m a)
then show ?case
by (cases "a = 0")
(auto simp add: mpoly_eq_iff coeff_sum coeff_mult if_conn if_distrib if_distribR
isolate_variable_sparse_monom isolate_variable_sparse_monom_mult
cong: if_cong)
next
case (sum p1 p2 m a)
then show ?case
by (simp add: distrib_right isovarspar_sum sum.distrib)
qed

subsubsection "More Miscellaneous"
lemma var_not_in_Const : "var∉vars (Const x :: real mpoly)"
unfolding vars_def keys_def
by (smt UN_iff coeff_def coeff_isolate_variable_sparse const_lookup_zero keys_def lookup_eq_zero_in_keys_contradict)

lemma mpoly_to_nested_poly_mult:
"mpoly_to_nested_poly (p * q) v = mpoly_to_nested_poly p v * mpoly_to_nested_poly q v"
for p q::"'a::{comm_semiring_0, semiring_no_zero_divisors} mpoly"
by (auto simp: poly_eq_iff coeff_mult mpoly_to_nested_poly.rep_eq isolate_variable_sparse_mult)

lemma get_if_const_insertion :
assumes "get_if_const (p::real mpoly) = Some r"
shows "insertion f p = r"
proof-
have "Set.is_empty (vars p)"
apply(cases "Set.is_empty (vars p)")
apply(simp) using assms by(simp)
then have "(MPoly_Type.coeff p 0) = r"
using assms by simp
then show ?thesis
by (metis Set.is_empty_def ‹Set.is_empty (vars p)› empty_iff insertion_irrelevant_vars insertion_trivial)
qed

subsubsection "Yet more Degree Lemmas"
lemma degree_mult:
fixes p q::"'a::{comm_semiring_0, ring_1_no_zero_divisors} mpoly"
assumes "p ≠ 0"
assumes "q ≠ 0"
shows "MPoly_Type.degree (p * q) v = MPoly_Type.degree p v + MPoly_Type.degree q v"
using assms
by (auto simp add: degree_eq_univariate_degree mpoly_to_nested_poly_mult Polynomial.degree_mult_eq)

lemma degree_eq:
assumes "(p::real mpoly) = (q:: real mpoly)"
shows "MPoly_Type.degree p x = MPoly_Type.degree q x"
by (simp add: assms)

lemma degree_var_i : "MPoly_Type.degree (((Var x)^i:: real mpoly)) x = i"
proof (induct i)
case 0
then show ?case using degree_const
by simp
next
case (Suc i)
have multh: "(Var x)^(Suc i) = ((Var x)^i::real mpoly) * (Var x:: real mpoly)"
using power_Suc2 by blast
have deg0h: "MPoly_Type.degree 0 x = 0"
by simp
have deg1h: "MPoly_Type.degree (Var x::real mpoly) x = 1"
using degree_one
by blast
have nonzeroh1: "(Var x:: real mpoly) ≠ 0"
using degree_eq deg0h deg1h by auto
have nonzeroh2: "((Var x)^i:: real mpoly) ≠ 0"
using degree_eq deg0h Suc.hyps
by (metis one_neq_zero power_0)
have sumh: "(MPoly_Type.degree (((Var x)^i:: real mpoly) * (Var x:: real mpoly)) x) = (MPoly_Type.degree ((Var x)^i::real mpoly) x) + (MPoly_Type.degree (Var x::real mpoly) x)"
using degree_mult[where p = "(Var x)^i::real mpoly", where q = "Var x::real mpoly"]  nonzeroh1 nonzeroh2
by blast
then show ?case using sumh deg1h
by (metis Suc.hyps Suc_eq_plus1 multh)
qed

lemma degree_less_sum:
assumes "MPoly_Type.degree (p::real mpoly) var = n"
assumes "MPoly_Type.degree (q::real mpoly) var = m"
assumes "m < n"
shows "MPoly_Type.degree (p + q) var = n"
proof -
have h1: "n > 0"
using assms(3) neq0_conv by blast
have h2: "(∃m∈monomials p. lookup m var = n) ∧ (∀m∈monomials p. lookup m var ≤ n)"
using degree_eq_iff assms(1)
by (metis degree_ge_iff h1 order_refl)
have h3: "(∃m∈monomials (p + q). lookup m var = n)"
using h2
by (metis MPolyExtension.coeff_add add.right_neutral assms(2) assms(3) coeff_eq_zero_iff degree_not_exists_monom)
have h4: "(∀m∈monomials (p + q). lookup m var ≤ n)"
using h2 assms(3) assms(2)
using degree_add_leq degree_le_iff dual_order.strict_iff_order by blast
show ?thesis using degree_eq_iff h3 h4
by (metis assms(3) gr_implies_not0)
qed

lemma degree_less_sum':
assumes "MPoly_Type.degree (p::real mpoly) var = n"
assumes "MPoly_Type.degree (q::real mpoly) var = m"
assumes "n < m"
shows "MPoly_Type.degree (p + q) var = m" using degree_less_sum[OF assms(2) assms(1) assms(3)]
by (simp add: add.commute)

(* Result on the degree of the derivative  *)

lemma nonzero_const_is_nonzero:
assumes "(k::real) ≠ 0"
shows "((Const k)::real mpoly) ≠ 0"
by (metis MPoly_Type.insertion_zero assms insertion_const)

lemma degree_derivative :
assumes "MPoly_Type.degree p x > 0"
shows "MPoly_Type.degree p x = MPoly_Type.degree (derivative x p) x + 1"
proof -
define f where "f i = (isolate_variable_sparse p x (i+1) * (Var x)^(i) * (Const (i+1)))" for i
define n where "n = MPoly_Type.degree p x-1"
have d : "∃m∈monomials p. lookup m x = n+1"
using n_def degree_eq_iff assms
by (metis add.commute less_not_refl2 less_one linordered_semidom_class.add_diff_inverse)
have h1a : "∀i. MPoly_Type.degree (isolate_variable_sparse p x i) x = 0"
by (simp add: not_in_isovarspar varNotIn_degree)
have h1b : "∀i::nat. MPoly_Type.degree ((Var x)^i:: real mpoly) x = i"
using degree_var_i by auto
have h1c1 : "∀i. (Var(x)^(i)::real mpoly)≠0"
by (metis MPoly_Type.degree_zero h1b power_0 zero_neq_one)
fix i
have h1c1var: "((Var x)^i:: real mpoly) ≠ 0" using h1c1 by blast
have h1c2 : "((Const ((i::nat) + 1))::real mpoly)≠0"
using nonzero_const_is_nonzero
by auto
have h1c3: "(isolate_variable_sparse p x (n + 1)) ≠ 0" using d
by (metis One_nat_def Suc_pred add.commute assms isolate_variable_sparse_degree_eq_zero_iff n_def not_gr_zero not_in_isovarspar plus_1_eq_Suc varNotIn_degree)
have h3: "(isolate_variable_sparse p x (i+1) = 0) ⟶ (MPoly_Type.degree (f i) x) = 0"
by (simp add: f_def)
have degh1: "(MPoly_Type.degree (((Const ((i::nat)+1))::real mpoly)*(Var x)^i) x) =
((MPoly_Type.degree ((Const (i+1))::real mpoly) x) + (MPoly_Type.degree ((Var x)^i:: real mpoly) x))"
using h1c2 h1c1var degree_mult[where p="((Const ((i::nat)+1))::real mpoly)", where q="((Var x)^i:: real mpoly)"]
by blast
then have degh2: "(MPoly_Type.degree (((Const ((i::nat)+1))::real mpoly)*(Var x)^i) x) = i"
using degree_var_i degree_const
by simp
have nonzerohyp: "(((Const ((i::nat)+1))::real mpoly)*(Var x)^i) ≠ 0"
proof (induct i)
case 0
then show ?case
by (simp add: nonzero_const_is_nonzero)
next
case (Suc i)
then show ?case using degree_eq degh2
by (metis Suc_eq_plus1 h1c1 mult_eq_0_iff nat.simps(3) nonzero_const_is_nonzero of_nat_eq_0_iff)
qed
have h4a1: "(isolate_variable_sparse p x (i+1) ≠ 0) ⟶ (MPoly_Type.degree (isolate_variable_sparse p x (i+1) * ((Var x)^(i) * (Const (i+1)))::real mpoly) x =
(MPoly_Type.degree (isolate_variable_sparse p x (i+1):: real mpoly) x) + (MPoly_Type.degree (((Const (i+1)) *  (Var x)^(i))::real mpoly) x))"
using nonzerohyp degree_mult[where p = "(isolate_variable_sparse p x (i+1))::real mpoly", where q = "((Const (i+1)) *  (Var x)^(i)):: real mpoly", where v = "x"]
by (simp add: mult.commute)
have h4: "(isolate_variable_sparse p x (i+1) ≠ 0) ⟶ (MPoly_Type.degree (f i) x) = i"
using h4a1 f_def degh2 h1a
by (metis (no_types, lifting) degh1 degree_const h1b mult.commute mult.left_commute of_nat_1 of_nat_add)
have h5: "(MPoly_Type.degree (f i) x) ≤ i" using h3 h4 by auto
have h6: "(MPoly_Type.degree (f n) x) = n" using h1c3 h4
by (smt One_nat_def add.right_neutral add_Suc_right degree_const degree_mult divisors_zero f_def h1a h1b h1c1 mult.commute nonzero_const_is_nonzero of_nat_1 of_nat_add of_nat_neq_0)
have h7a: "derivative x p = (∑i∈{0..MPoly_Type.degree p x-1}. isolate_variable_sparse p x (i+1) * (Var x)^i * (Const (i+1)))" using derivative_def by auto
have h7b: "(∑i∈{0..MPoly_Type.degree p x-1}. isolate_variable_sparse p x (i+1) * (Var x)^i * (Const (i+1))) = (∑i∈{0..MPoly_Type.degree p x-1}. (f i))" using f_def
by (metis Suc_eq_plus1 add.commute semiring_1_class.of_nat_simps(2))
have h7c: "derivative x p = (∑i∈{0..MPoly_Type.degree p x-1}. (f i))" using h7a h7b by auto
have h7: "derivative x p = (∑i∈{0..n}. (f i))" using n_def h7c
by blast
have h8: "n > 0 ⟶ ((MPoly_Type.degree (∑i∈{0..(n-1)}. (f i)) x) < n)"
proof (induct n)
case 0
then show ?case
by blast
next
case (Suc n)
then show ?case using h5 degree_less_sum
by (smt add_cancel_right_right atLeastAtMost_iff degree_const degree_mult degree_sum_less degree_var_i diff_Suc_1 f_def h1a le_imp_less_Suc mult.commute mult_eq_0_iff)
qed
have h9a: "n = 0 ⟶ MPoly_Type.degree (∑i∈{0..n}. (f i)) x = n" using h6
by auto
have h9b: "n > 0 ⟶ MPoly_Type.degree (∑i∈{0..n}. (f i)) x = n"
proof -
have h9bhyp: "n > 0 ⟶ (MPoly_Type.degree (∑i∈{0..n}. (f i)) x = MPoly_Type.degree ((∑i∈{0..(n-1)}. (f i)) + (f n)) x)"
by (metis Suc_diff_1 sum.atLeast0_atMost_Suc)
have h9bhyp2: "n > 0 ⟶ ((MPoly_Type.degree ((∑i∈{0..(n-1)}. (f i)) + (f n)) x) = n)"
using h6 h8 degree_less_sum
by (simp add: add.commute)
then show ?thesis using h9bhyp2 h9bhyp
by linarith
qed
have h9:  "MPoly_Type.degree (∑i∈{0..n}. (f i)) x = n" using h9a h9b
by blast
have h10: "MPoly_Type.degree (derivative x p) x = n" using h9 h7
by simp
show ?thesis using h10 n_def
using assms by linarith
qed

lemma express_poly :
assumes h : "MPoly_Type.degree (p::real mpoly) var = 1 ∨ MPoly_Type.degree p var = 2"
shows "p =
(isolate_variable_sparse p var 2)*(Var var)^2
+(isolate_variable_sparse p var 1)*(Var var)
+(isolate_variable_sparse p var 0)"
proof-
have h1a: "MPoly_Type.degree p var = 1 ⟶ p =
isolate_variable_sparse p var 0 +
isolate_variable_sparse p var 1 * Var var"
using sum_over_zero[where mp="p",where x="var"]
by auto
have h1b: "MPoly_Type.degree p var = 1 ⟶ isolate_variable_sparse p var 2 = 0"
using isovar_greater_degree
by (simp add: isovar_greater_degree)
have h1: "MPoly_Type.degree p var = 1 ⟶ p =
isolate_variable_sparse p var 0 +
isolate_variable_sparse p var 1 * Var var
+ isolate_variable_sparse p var 2 * (Var var)^2" using h1a h1b by auto
have h2a: "MPoly_Type.degree p var = 2 ⟶ p = (∑i::nat ≤ 2. isolate_variable_sparse p var i * Var var^i)"
using sum_over_zero[where mp="p", where x="var"] by auto
have h2b: "(∑i::nat ≤ 2. isolate_variable_sparse p var i * Var var^i) =
(∑i::nat ≤ 1. isolate_variable_sparse p var i * Var var^i) +
isolate_variable_sparse p var 2 * (Var var)^2" apply auto
by (simp add: numerals(2))
have h2:  "MPoly_Type.degree p var = 2 ⟶ p =
isolate_variable_sparse p var 0 +
isolate_variable_sparse p var 1 * Var var +
isolate_variable_sparse p var 2 * (Var var)^2"
using h2a h2b by auto
have h3: "isolate_variable_sparse p var 0 +
isolate_variable_sparse p var 1 * Var var +
isolate_variable_sparse p var 2 * (Var var)^2 =
isolate_variable_sparse p var 2 * (Var var)^2 +
isolate_variable_sparse p var 1 * Var var +
isolate_variable_sparse p var 0" by (simp add: add.commute)

show ?thesis using h h1 h2 h3 by presburger
qed

lemma degree_isovarspar : "MPoly_Type.degree (isolate_variable_sparse (p::real mpoly) x i) x = 0"
using not_in_isovarspar varNotIn_degree by blast

end
```