# Theory Virtual_Substitution.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"

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

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

lemma coeff_eq_zero_iff:

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]:
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]:
by transfer auto

lemma in_monomials_iff:
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::
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: Const0_zero zero_mpoly.abs_eq)
qed

(* example *)
lemma add_zero_example : "((Var 0)^2 - (Const 1)) + Const 0 = ((Var 0)^2 - (Const 1))"
proof -
qed

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

lemma mult_zero_right :
by (metis mult_zero_left mult_zero_right)

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

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

subsection "Coefficient Lemmas"
lemma coeff_zero[simp]:
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)

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: Var0_def pprod.monomial_power lookup_times_monomial_right

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: Const0_def lookup_single)

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

subsection "Miscellaneous"
lemma update_0_0[simp]:
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 "(AB) = (A^2B^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. xX  ( 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. xset(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 : "a0  x  keys m  x  vars(MPoly_Type.monom m a)"

lemma notInKeys_notInVars : "x  keys m  x  vars(MPoly_Type.monom m a)"

lemma lookupNotIn : "x  keys m  lookup m x = 0"

subsection "Degree Lemmas"

lemma degree_le_iff: "MPoly_Type.degree p x  k  (mmonomials p. lookup m x  k)"
by transfer simp

lemma degree_less_iff: "MPoly_Type.degree p x < k  (k>0  (mmonomials 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  (mmonomials 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  (mmonomials 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 (mmonomials p. lookup m x = 0)
else (mmonomials p. lookup m x = k)  (mmonomials 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"

lemma degree_one : "MPoly_Type.degree (Var x :: real mpoly) x = 1"

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 )

lemma isolate_zero[simp]:
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 :
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 :
by (auto simp add: mpoly_eq_iff coeff_isolate_variable_sparse coeff_Var coeff_eq_zero_iff)
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
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"

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")
next
case (sum p1 p2 m a)
then show ?case
qed

lemma degree0isovarspar :
assumes deg0 : "MPoly_Type.degree (p::real mpoly) x = 0"
shows
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"
have h2 :
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)
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

lemma not_in_isovarspar : "isolate_variable_sparse (p::real mpoly) var x = (q::real mpoly)  var(vars q)"
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 ::
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 "pkeys (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))"

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

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)
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 :
"xkeys (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
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 ::
assume a1: "xkeys (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. xkeys (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)
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 (in. g(i))) = (in. 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"

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 : "xvars(p::real mpoly)  xvars(q::real mpoly)
insertion f (p-q) = insertion f p - insertion f q"

lemma insertion_sub : "insertion f (A-B :: real mpoly) = insertion f A - insertion f B"

lemma insertion_four : "insertion ((nth_default 0) xs) 4 = 4"

"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

"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
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))"
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))"
then show ?thesis using not_contains_insertion
by blast
qed
lemma insertion_zero : "insertion f (Const 0 ::real mpoly) = 0"

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"
assumes h1 : "MPoly_Type.degree a var  x"
assumes h2 : "MPoly_Type.degree b var  x"
shows "MPoly_Type.degree (a+b) var  x"

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

lemma varNotIn_degree :
assumes "var  vars p"
shows "MPoly_Type.degree p var = 0"
proof-
have "mmonomials 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: "mmonomials p. lookup m var  MPoly_Type.degree p var" using degree_eq_iff
by (metis zero_le)
have hq: "mmonomials 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: "(mmonomials (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
qed

lemma degree_exists_monom:
assumes "p0"
shows  "mmonomials p. lookup m var = MPoly_Type.degree p var"
proof(cases "MPoly_Type.degree p var =0")
case True
have h1: "mmonomials 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 "p0"
shows  "¬ ( mmonomials p. lookup m var > MPoly_Type.degree p var)"
proof -
show ?thesis using degree_less_iff by blast
qed

lemma degree_monom:
by (auto simp: degree_eq_iff)

lemma degree_plus_disjoint:

if "m  monomials p"
for p::
using that
apply (subst degree_eq_iff)
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:: is
"λ(mp::'a mpoly) (v::nat) (p::nat). isolate_variable_sparse mp v p"
― ‹note constextract_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:

apply transfer'
apply transfer'
apply (auto simp: fun_eq_iff)
proof -
fix mpa :: "'a mpoly" and va :: nat and m ::
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:
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 ::
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:
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
subgoal
apply transfer'
apply transfer'
by (auto simp: fun_eq_iff intro!: sum.neutral)
done
qed

lemma isolate_variable_sparse_degree_eq_zero_iff:
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"
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:
apply auto
apply (rule antisym)
subgoal
apply (rule Polynomial.le_degree)
apply auto
apply transfer'
subgoal apply (rule Polynomial.degree_le)
apply (auto simp: elim!: degree_eq_zeroE)
apply transfer'
done

lemma compute_mpoly_to_nested_poly[code]:

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

for q::
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: 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)
done

lemma isolate_variable_sparse_mult:
"isolate_variable_sparse (p * q) v n = (in. isolate_variable_sparse p v i * isolate_variable_sparse q v (n - i))"
for p q::
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 : "varvars (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:

for p q::
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::
assumes "p  0"
assumes "q  0"
shows
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

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:
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: "(mmonomials p. lookup m var = n)  (mmonomials p. lookup m var  n)"
using degree_eq_iff assms(1)
by (metis degree_ge_iff h1 order_refl)
have h3: "(mmonomials (p + q). lookup m var = n)"
using h2
have h4: "(mmonomials (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)]

(* 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
shows
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 : "mmonomials p. lookup m x = n+1"
using n_def degree_eq_iff assms
have h1a :
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"
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
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"]
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
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
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:
using sum_over_zero[where mp="p",where x="var"]
by auto
have h1b:
using 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
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 +