diff --git a/thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy b/thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy --- a/thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy +++ b/thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy @@ -1,295 +1,293 @@ subsection \Exact Division of Multivariate Polynomials\ theory MPoly_Divide - imports + imports Hermite_Lindemann.More_Multivariate_Polynomial_HLW Polynomials.MPoly_Type_Class Poly_Connection begin lemma poly_lead_coeff_dvd_lead_coeff: assumes "p dvd (q :: 'a :: idom poly)" shows "Polynomial.lead_coeff p dvd Polynomial.lead_coeff q" using assms by (elim dvdE) (auto simp: Polynomial.lead_coeff_mult) text \ Since there is no particularly sensible algorithm for division with a remainder on multivariate polynomials, we define the following division operator that performs an exact division if possible and returns 0 otherwise. \ -no_notation MPoly_Type.div (infixl "div" 70) - instantiation mpoly :: ("comm_semiring_1") divide begin definition divide_mpoly :: "'a mpoly \ 'a mpoly \ 'a mpoly" where "divide_mpoly x y = (if y \ 0 \ y dvd x then THE z. x = y * z else 0)" instance .. end instance mpoly :: (idom) idom_divide by standard (auto simp: divide_mpoly_def) lemma (in transfer_mpoly_to_mpoly_poly) transfer_div [transfer_rule]: assumes [transfer_rule]: "R p' p" "R q' q" assumes "q dvd p" shows "R (p' div q') (p div q)" using assms by (smt (z3) div_by_0 dvd_imp_mult_div_cancel_left mpoly_to_mpoly_poly_0 mpoly_to_mpoly_poly_eq_iff mpoly_to_mpoly_poly_mult nonzero_mult_div_cancel_left transfer_mpoly_to_mpoly_poly.R_def) instantiation mpoly :: ("{normalization_semidom, idom}") normalization_semidom begin definition unit_factor_mpoly :: "'a mpoly \ 'a mpoly" where "unit_factor_mpoly p = Const (unit_factor (lead_coeff p))" definition normalize_mpoly :: "'a mpoly \ 'a mpoly" where "normalize_mpoly p = Rings.divide p (unit_factor p)" lemma unit_factor_mpoly_Const [simp]: "unit_factor (Const c) = Const (unit_factor c)" unfolding unit_factor_mpoly_def by simp lemma normalize_mpoly_Const [simp]: "normalize (Const c) = Const (normalize c)" proof (cases "c = 0") case False have "normalize (Const c) = Const c div Const (unit_factor c)" by (simp add: normalize_mpoly_def) also have "\ = Const (unit_factor c * normalize c) div Const (unit_factor c)" by simp also have "\ = Const (unit_factor c) * Const (normalize c) div Const (unit_factor c)" by (subst mpoly_Const_mult) auto also have "\ = Const (normalize c)" using \c \ 0\ by (subst nonzero_mult_div_cancel_left) auto finally show ?thesis . qed (auto simp: normalize_mpoly_def) instance proof show "unit_factor (0 :: 'a mpoly) = 0" by (simp add: unit_factor_mpoly_def) next show "unit_factor x = x" if "x dvd 1" for x :: "'a mpoly" using that by (auto elim!: mpoly_is_unitE simp: is_unit_unit_factor) next fix x :: "'a mpoly" assume "x \ 0" thus "unit_factor x dvd 1" by (auto simp: unit_factor_mpoly_def) next fix x y :: "'a mpoly" assume "x dvd 1" hence "x \ 0" by auto show "unit_factor (x * y) = x * unit_factor y" proof (cases "y = 0") case False have "Const (unit_factor (lead_coeff x * lead_coeff y)) = x * Const (unit_factor (lead_coeff y))" using \x dvd 1\ by (subst unit_factor_mult_unit_left) (auto elim!: mpoly_is_unitE simp: mpoly_Const_mult) thus ?thesis using \x \ 0\ False by (simp add: unit_factor_mpoly_def lead_coeff_mult) qed (auto simp: unit_factor_mpoly_def) next fix p :: "'a mpoly" let ?c = "Const (unit_factor (lead_coeff p))" show "unit_factor p * normalize p = p" proof (cases "p = 0") case False hence "?c dvd 1" by (intro is_unit_ConstI) auto also have "1 dvd p" by simp finally have "?c * (p div ?c) = p" by (rule dvd_imp_mult_div_cancel_left) thus ?thesis by (auto simp: unit_factor_mpoly_def normalize_mpoly_def) qed (auto simp: normalize_mpoly_def) next show "normalize (0 :: 'a mpoly) = 0" by (simp add: normalize_mpoly_def) qed end text \ The following is an exact division operator that can fail, i.e.\ if the divisor does not divide the dividend, it returns \<^const>\None\. \ definition divide_option :: "'a :: idom_divide \ 'a \ 'a option" (infixl "div?" 70) where "divide_option p q = (if q dvd p then Some (p div q) else None)" text \ We now show that exact division on the ring $R[X_1,\ldots, X_n]$ can be reduced to exact division on the ring $R[X_1,\ldots,X_n][X]$, i.e.\ we can go from \<^typ>\'a mpoly\ to a \<^typ>\'a mpoly poly\ where the coefficients have one variable less than the original multivariate polynomial. We basically simply use the isomorphism between these two rings. \ lemma divide_option_mpoly: fixes p q :: "'a :: idom_divide mpoly" shows "p div? q = (let V = vars p \ vars q in (if V = {} then let a = MPoly_Type.coeff p 0; b = MPoly_Type.coeff q 0; c = a div b in if b * c = a then Some (Const c) else None else let x = Max V; p' = mpoly_to_mpoly_poly x p; q' = mpoly_to_mpoly_poly x q in case p' div? q' of None \ None | Some r \ Some (poly r (Var x))))" (is "_ = ?rhs") proof - define x where "x = Max (vars p \ vars q)" define p' where "p' = mpoly_to_mpoly_poly x p" define q' where "q' = mpoly_to_mpoly_poly x q" interpret transfer_mpoly_to_mpoly_poly x . have [transfer_rule]: "R p' p" "R q' q" by (auto simp: p'_def q'_def R_def) show ?thesis proof (cases "vars p \ vars q = {}") case True define a where "a = MPoly_Type.coeff p 0" define b where "b = MPoly_Type.coeff q 0" have [simp]: "p = Const a" "q = Const b" using True by (auto elim!: vars_emptyE simp: a_def b_def mpoly_coeff_Const) show ?thesis apply (cases "b = 0") apply (auto simp: Let_def mpoly_coeff_Const mpoly_Const_mult divide_option_def elim!: dvdE) by (metis dvd_triv_left) next case False have "?rhs = (case p' div? q' of None \ None | Some r \ Some (poly r (Var x)))" using False unfolding Let_def apply (simp only: ) apply (subst if_False) apply (simp flip: x_def p'_def q'_def cong: option.case_cong) done also have "\ = (if q' dvd p' then Some (poly (p' div q') (Var x)) else None)" using False by (auto simp: divide_option_def) also have "\ = p div? q" unfolding divide_option_def proof (intro if_cong refl arg_cong[where f = Some]) show "(q' dvd p') = (q dvd p)" by transfer_prover next assume [transfer_rule]: "q dvd p" have "R (p' div q') (p div q)" by transfer_prover thus "poly (p' div q') (Var x) = p div q" by (simp add: R_def poly_mpoly_to_mpoly_poly) qed finally show ?thesis .. qed qed text \ Next, we show that exact division on the ring $R[X_1,\ldots,X_n][Y]$ can be reduced to exact division on the ring $R[X_1,\ldots,X_n]$. This is essentially just polynomial division. \ lemma divide_option_mpoly_poly: fixes p q :: "'a :: idom_divide mpoly poly" - shows "p div? q = + shows "p div? q = (if p = 0 then Some 0 else if q = 0 then None else let dp = Polynomial.degree p; dq = Polynomial.degree q in if dp < dq then None else case Polynomial.lead_coeff p div? Polynomial.lead_coeff q of None \ None | Some c \ ( case (p - Polynomial.monom c (dp - dq) * q) div? q of None \ None | Some r \ Some (Polynomial.monom c (dp - dq) + r)))" (is "_ = ?rhs") proof (cases "p = 0"; cases "q = 0") assume [simp]: "p \ 0" "q \ 0" define dp where "dp = Polynomial.degree p" define dq where "dq = Polynomial.degree q" define cp where "cp = Polynomial.lead_coeff p" define cq where "cq = Polynomial.lead_coeff q" define mon where "mon = Polynomial.monom (cp div cq) (dp - dq)" show ?thesis proof (cases "dp < dq") case True hence "\q dvd p" unfolding dp_def dq_def by (meson \p \ 0\ divides_degree leD) thus ?thesis using True by (simp add: divide_option_def dp_def dq_def) next case deg: False show ?thesis proof (cases "cq dvd cp") case False hence "\q dvd p" unfolding cq_def cp_def using poly_lead_coeff_dvd_lead_coeff by blast thus ?thesis using deg False by (simp add: dp_def dq_def Let_def divide_option_def cp_def cq_def) next case dvd1: True show ?thesis proof (cases "q dvd (p - mon * q)") case False hence "\q dvd p" by (meson dvd_diff dvd_triv_right) thus ?thesis using deg dvd1 False by (simp add: dp_def dq_def Let_def divide_option_def cp_def cq_def mon_def) next case dvd2: True hence "q dvd p" by (metis diff_eq_eq dvd_add dvd_triv_right) have "?rhs = Some (mon + (p - mon * q) div q)" using deg dvd1 dvd2 by (simp add: dp_def dq_def Let_def divide_option_def cp_def cq_def mon_def) also have "mon + (p - mon * q) div q = p div q" using dvd2 by (elim dvdE) (auto simp: algebra_simps) also have "Some \ = p div? q" using \q dvd p\ by (simp add: divide_option_def) finally show ?thesis .. qed qed qed qed (auto simp: divide_option_def) text \ These two equations now serve as two mutually recursive code equations that allow us to reduce exact division of multivariate polynomials to exact division of their coefficients. Termination of these code equations is not shown explicitly, but is obvious since one variable is eliminated in every step. \ definition divide_option_mpoly :: "'a :: idom_divide mpoly \ _" where "divide_option_mpoly = divide_option" definition divide_option_mpoly_poly :: "'a :: idom_divide mpoly poly \ _" where "divide_option_mpoly_poly = divide_option" lemmas divide_option_mpoly_code [code] = divide_option_mpoly [folded divide_option_mpoly_def divide_option_mpoly_poly_def] lemmas divide_option_mpoly_poly_code [code] = divide_option_mpoly_poly [folded divide_option_mpoly_def divide_option_mpoly_poly_def] lemma divide_mpoly_code [code]: fixes p q :: "'a :: idom_divide mpoly" shows "p div q = (case divide_option_mpoly p q of None \ 0 | Some r \ r)" by (auto simp: divide_option_mpoly_def divide_option_def divide_mpoly_def) end diff --git a/thys/Polynomials/MPoly_Type.thy b/thys/Polynomials/MPoly_Type.thy --- a/thys/Polynomials/MPoly_Type.thy +++ b/thys/Polynomials/MPoly_Type.thy @@ -1,539 +1,518 @@ (* Author: Andreas Lochbihler, ETH Zurich Author: Florian Haftmann, TU Muenchen *) section \An abstract type for multivariate polynomials\ theory MPoly_Type imports "HOL-Library.Poly_Mapping" begin subsection \Abstract type definition\ typedef (overloaded) 'a mpoly = "UNIV :: ((nat \\<^sub>0 nat) \\<^sub>0 'a::zero) set" morphisms mapping_of MPoly .. setup_lifting type_definition_mpoly (* these theorems are automatically generated by setup_lifting... *) thm mapping_of_inverse thm MPoly_inverse thm mapping_of_inject thm MPoly_inject thm mapping_of_induct thm MPoly_induct thm mapping_of_cases thm MPoly_cases subsection \Additive structure\ instantiation mpoly :: (zero) zero begin lift_definition zero_mpoly :: "'a mpoly" is "0 :: (nat \\<^sub>0 nat) \\<^sub>0 'a" . instance .. end instantiation mpoly :: (monoid_add) monoid_add begin lift_definition plus_mpoly :: "'a mpoly \ 'a mpoly \ 'a mpoly" is "Groups.plus :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . instance by intro_classes (transfer, simp add: fun_eq_iff add.assoc)+ end instance mpoly :: (comm_monoid_add) comm_monoid_add by intro_classes (transfer, simp add: fun_eq_iff ac_simps)+ instantiation mpoly :: (cancel_comm_monoid_add) cancel_comm_monoid_add begin lift_definition minus_mpoly :: "'a mpoly \ 'a mpoly \ 'a mpoly" is "Groups.minus :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . instance by intro_classes (transfer, simp add: fun_eq_iff diff_diff_add)+ end instantiation mpoly :: (ab_group_add) ab_group_add begin lift_definition uminus_mpoly :: "'a mpoly \ 'a mpoly" is "Groups.uminus :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . instance by intro_classes (transfer, simp add: fun_eq_iff add_uminus_conv_diff)+ end subsection \Multiplication by a coefficient\ (* ?do we need inc_power on abstract polynomials? *) lift_definition smult :: "'a::{times,zero} \ 'a mpoly \ 'a mpoly" is "\a. Poly_Mapping.map (Groups.times a) :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . (* left lemmas in subsection \Pseudo-division of polynomials\, because I couldn't disentangle them and the notion of monomials. *) subsection \Multiplicative structure\ instantiation mpoly :: (zero_neq_one) zero_neq_one begin lift_definition one_mpoly :: "'a mpoly" is "1 :: ((nat \\<^sub>0 nat) \\<^sub>0 'a)" . instance by intro_classes (transfer, simp) end instantiation mpoly :: (semiring_0) semiring_0 begin lift_definition times_mpoly :: "'a mpoly \ 'a mpoly \ 'a mpoly" is "Groups.times :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . instance by intro_classes (transfer, simp add: algebra_simps)+ end instance mpoly :: (comm_semiring_0) comm_semiring_0 by intro_classes (transfer, simp add: algebra_simps)+ instance mpoly :: (semiring_0_cancel) semiring_0_cancel .. instance mpoly :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. instance mpoly :: (semiring_1) semiring_1 by intro_classes (transfer, simp)+ instance mpoly :: (comm_semiring_1) comm_semiring_1 by intro_classes (transfer, simp)+ instance mpoly :: (semiring_1_cancel) semiring_1_cancel .. (*instance mpoly :: (comm_semiring_1_cancel) comm_semiring_1_cancel .. FIXME unclear whether this holds *) instance mpoly :: (ring) ring .. instance mpoly :: (comm_ring) comm_ring .. instance mpoly :: (ring_1) ring_1 .. instance mpoly :: (comm_ring_1) comm_ring_1 .. subsection \Monomials\ text \ Terminology is not unique here, so we use the notions as follows: A "monomial" and a "coefficient" together give a "term". These notions are significant in connection with "leading", "leading term", "leading coefficient" and "leading monomial", which all rely on a monomial order. \ lift_definition monom :: "(nat \\<^sub>0 nat) \ 'a::zero \ 'a mpoly" is "Poly_Mapping.single :: (nat \\<^sub>0 nat) \ _" . lemma mapping_of_monom [simp]: "mapping_of (monom m a) = Poly_Mapping.single m a" by(fact monom.rep_eq) lemma monom_zero [simp]: "monom 0 0 = 0" by transfer simp lemma monom_one [simp]: "monom 0 1 = 1" by transfer simp lemma monom_add: "monom m (a + b) = monom m a + monom m b" by transfer (simp add: single_add) lemma monom_uminus: "monom m (- a) = - monom m a" by transfer (simp add: single_uminus) lemma monom_diff: "monom m (a - b) = monom m a - monom m b" by transfer (simp add: single_diff) lemma monom_numeral [simp]: "monom 0 (numeral n) = numeral n" by (induct n) (simp_all only: numeral.simps numeral_add monom_zero monom_one monom_add) lemma monom_of_nat [simp]: "monom 0 (of_nat n) = of_nat n" by (induct n) (simp_all add: monom_add) lemma of_nat_monom: "of_nat = monom 0 \ of_nat" by (simp add: fun_eq_iff) lemma inj_monom [iff]: "inj (monom m)" proof (rule injI, transfer) fix a b :: 'a and m :: "nat \\<^sub>0 nat" assume "Poly_Mapping.single m a = Poly_Mapping.single m b" with injD [of "Poly_Mapping.single m" a b] show "a = b" by simp qed lemma mult_monom: "monom x a * monom y b = monom (x + y) (a * b)" by transfer' (simp add: Poly_Mapping.mult_single) instance mpoly :: (semiring_char_0) semiring_char_0 by intro_classes (auto simp add: of_nat_monom inj_of_nat intro: inj_compose) instance mpoly :: (ring_char_0) ring_char_0 .. lemma monom_of_int [simp]: "monom 0 (of_int k) = of_int k" apply (cases k) apply simp_all unfolding monom_diff monom_uminus apply simp done subsection \Constants and Indeterminates\ text \Embedding of indeterminates and constants in type-class polynomials, can be used as constructors.\ definition Var\<^sub>0 :: "'a \ ('a \\<^sub>0 nat) \\<^sub>0 'b::{one,zero}" where "Var\<^sub>0 n \ Poly_Mapping.single (Poly_Mapping.single n 1) 1" definition Const\<^sub>0 :: "'b \ ('a \\<^sub>0 nat) \\<^sub>0 'b::zero" where "Const\<^sub>0 c \ Poly_Mapping.single 0 c" lemma Const\<^sub>0_one: "Const\<^sub>0 1 = 1" by (simp add: Const\<^sub>0_def) lemma Const\<^sub>0_numeral: "Const\<^sub>0 (numeral x) = numeral x" by (auto intro!: poly_mapping_eqI simp: Const\<^sub>0_def lookup_numeral) lemma Const\<^sub>0_minus: "Const\<^sub>0 (- x) = - Const\<^sub>0 x" by (simp add: Const\<^sub>0_def single_uminus) lemma Const\<^sub>0_zero: "Const\<^sub>0 0 = 0" by (auto intro!: poly_mapping_eqI simp: Const\<^sub>0_def) lemma Var\<^sub>0_power: "Var\<^sub>0 v ^ n = Poly_Mapping.single (Poly_Mapping.single v n) 1" by (induction n) (auto simp: Var\<^sub>0_def mult_single single_add[symmetric]) lift_definition Var::"nat \ 'b::{one,zero} mpoly" is Var\<^sub>0 . lift_definition Const::"'b::zero \ 'b mpoly" is Const\<^sub>0 . subsection \Integral domains\ instance mpoly :: (ring_no_zero_divisors) ring_no_zero_divisors by intro_classes (transfer, simp) instance mpoly :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. instance mpoly :: (idom) idom .. subsection \Monom coefficient lookup\ definition coeff :: "'a::zero mpoly \ (nat \\<^sub>0 nat) \ 'a" where "coeff p = Poly_Mapping.lookup (mapping_of p)" subsection \Insertion morphism\ definition insertion_fun_natural :: "(nat \ 'a) \ ((nat \ nat) \ 'a) \ 'a::comm_semiring_1" where "insertion_fun_natural f p = (\m. p m * (\v. f v ^ m v))" definition insertion_fun :: "(nat \ 'a) \ ((nat \\<^sub>0 nat) \ 'a) \ 'a::comm_semiring_1" where "insertion_fun f p = (\m. p m * (\v. f v ^ Poly_Mapping.lookup m v))" text \N.b. have been unable to relate this to @{const insertion_fun_natural} using lifting!\ lift_definition insertion_aux :: "(nat \ 'a) \ ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ 'a::comm_semiring_1" is "insertion_fun" . lift_definition insertion :: "(nat \ 'a) \ 'a mpoly \ 'a::comm_semiring_1" is "insertion_aux" . lemma aux: "Poly_Mapping.lookup f = (\_. 0) \ f = 0" apply transfer apply simp done lemma insertion_trivial [simp]: "insertion (\_. 0) p = coeff p 0" proof - { fix f :: "(nat \\<^sub>0 nat) \\<^sub>0 'a" have "insertion_aux (\_. 0) f = Poly_Mapping.lookup f 0" apply (simp add: insertion_aux_def insertion_fun_def power_Sum_any [symmetric]) apply (simp add: zero_power_eq mult_when aux) done } then show ?thesis by (simp add: coeff_def insertion_def) qed lemma insertion_zero [simp]: "insertion f 0 = 0" by transfer (simp add: insertion_aux_def insertion_fun_def) lemma insertion_fun_add: fixes f p q shows "insertion_fun f (Poly_Mapping.lookup (p + q)) = insertion_fun f (Poly_Mapping.lookup p) + insertion_fun f (Poly_Mapping.lookup q)" unfolding insertion_fun_def apply (subst Sum_any.distrib [symmetric]) apply (simp_all add: plus_poly_mapping.rep_eq algebra_simps) apply (rule finite_mult_not_eq_zero_rightI) apply simp apply (rule finite_mult_not_eq_zero_rightI) apply simp done lemma insertion_add: "insertion f (p + q) = insertion f p + insertion f q" by transfer (simp add: insertion_aux_def insertion_fun_add) lemma insertion_one [simp]: "insertion f 1 = 1" by transfer (simp add: insertion_aux_def insertion_fun_def one_poly_mapping.rep_eq when_mult) lemma insertion_fun_mult: fixes f p q shows "insertion_fun f (Poly_Mapping.lookup (p * q)) = insertion_fun f (Poly_Mapping.lookup p) * insertion_fun f (Poly_Mapping.lookup q)" proof - { fix m :: "nat \\<^sub>0 nat" have "finite {v. Poly_Mapping.lookup m v \ 0}" by simp then have "finite {v. f v ^ Poly_Mapping.lookup m v \ 1}" by (rule rev_finite_subset) (auto intro: ccontr) } moreover define g where "g m = (\v. f v ^ Poly_Mapping.lookup m v)" for m ultimately have *: "\a b. g (a + b) = g a * g b" by (simp add: plus_poly_mapping.rep_eq power_add Prod_any.distrib) have bij: "bij (\(l, n, m). (m, l, n))" by (auto intro!: bijI injI simp add: image_def) let ?P = "{l. Poly_Mapping.lookup p l \ 0}" let ?Q = "{n. Poly_Mapping.lookup q n \ 0}" let ?PQ = "{l + n | l n. l \ Poly_Mapping.keys p \ n \ Poly_Mapping.keys q}" have "finite {l + n | l n. Poly_Mapping.lookup p l \ 0 \ Poly_Mapping.lookup q n \ 0}" by (rule finite_not_eq_zero_sumI) simp_all then have fin_PQ: "finite ?PQ" by (simp add: in_keys_iff) have "(\m. Poly_Mapping.lookup (p * q) m * g m) = (\m. (\l. Poly_Mapping.lookup p l * (\n. Poly_Mapping.lookup q n when m = l + n)) * g m)" by (simp add: times_poly_mapping.rep_eq prod_fun_def) also have "\ = (\m. (\l. (\n. g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)))" apply (subst Sum_any_left_distrib) apply (auto intro: finite_mult_not_eq_zero_rightI) apply (subst Sum_any_right_distrib) apply (auto intro: finite_mult_not_eq_zero_rightI) apply (subst Sum_any_left_distrib) apply (auto intro: finite_mult_not_eq_zero_leftI) apply (simp add: ac_simps mult_when) done also have "\ = (\m. (\(l, n). g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n))" apply (subst (2) Sum_any.cartesian_product [of "?P \ ?Q"]) apply (auto dest!: mult_not_zero) done also have "\ = (\(m, l, n). g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)" apply (subst Sum_any.cartesian_product [of "?PQ \ (?P \ ?Q)"]) apply (auto dest!: mult_not_zero simp add: fin_PQ) apply (auto simp: in_keys_iff) done also have "\ = (\(l, n, m). g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)" using bij by (rule Sum_any.reindex_cong [of "\(l, n, m). (m, l, n)"]) (simp add: fun_eq_iff) also have "\ = (\(l, n). \m. g m * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n) when m = l + n)" apply (subst Sum_any.cartesian_product2 [of "(?P \ ?Q) \ ?PQ"]) apply (auto dest!: mult_not_zero simp add: fin_PQ ) apply (auto simp: in_keys_iff) done also have "\ = (\(l, n). (g l * g n) * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n))" by (simp add: *) also have "\ = (\l. \n. (g l * g n) * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n))" apply (subst Sum_any.cartesian_product [of "?P \ ?Q"]) apply (auto dest!: mult_not_zero) done also have "\ = (\l. \n. (Poly_Mapping.lookup p l * g l) * (Poly_Mapping.lookup q n * g n))" by (simp add: ac_simps) also have "\ = (\m. Poly_Mapping.lookup p m * g m) * (\m. Poly_Mapping.lookup q m * g m)" by (rule Sum_any_product [symmetric]) (auto intro: finite_mult_not_eq_zero_rightI) finally show ?thesis by (simp add: insertion_fun_def g_def) qed lemma insertion_mult: "insertion f (p * q) = insertion f p * insertion f q" by transfer (simp add: insertion_aux_def insertion_fun_mult) subsection \Degree\ lift_definition degree :: "'a::zero mpoly \ nat \ nat" is "\p v. Max (insert 0 ((\m. Poly_Mapping.lookup m v) ` Poly_Mapping.keys p))" . lift_definition total_degree :: "'a::zero mpoly \ nat" is "\p. Max (insert 0 ((\m. sum (Poly_Mapping.lookup m) (Poly_Mapping.keys m)) ` Poly_Mapping.keys p))" . lemma degree_zero [simp]: "degree 0 v = 0" by transfer simp lemma total_degree_zero [simp]: "total_degree 0 = 0" by transfer simp (* value [code] "total_degree (0 :: int mpoly)" (***) *) lemma degree_one [simp]: "degree 1 v = 0" by transfer simp lemma total_degree_one [simp]: "total_degree 1 = 0" by transfer simp subsection \Pseudo-division of polynomials\ lemma smult_conv_mult: "smult s p = monom 0 s * p" by transfer (simp add: mult_map_scale_conv_mult) lemma smult_monom [simp]: fixes c :: "_ :: mult_zero" shows "smult c (monom x c') = monom x (c * c')" by transfer simp lemma smult_0 [simp]: fixes p :: "_ :: mult_zero mpoly" shows "smult 0 p = 0" by transfer(simp add: map_eq_zero_iff) lemma mult_smult_left: "smult s p * q = smult s (p * q)" by(simp add: smult_conv_mult mult.assoc) lift_definition sdiv :: "'a::euclidean_ring \ 'a mpoly \ 'a mpoly" is "\a. Poly_Mapping.map (\b. b div a) :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . text \ \qt{Polynomial division} is only possible on univariate polynomials \K[x]\ over a field \K\, all other kinds of polynomials only allow pseudo-division [1]p.40/41": \\x y :: 'a mpoly. y \ 0 \ \a q r. smult a x = q * y + r\ The introduction of pseudo-division below generalises @{file \~~/src/HOL/Computational_Algebra/Polynomial.thy\}. [1] Winkler, Polynomial Algorithms, 1996. The generalisation raises issues addressed by Wenda Li and commented below. Florian replied to the issues conjecturing, that the abstract mpoly needs not be aware of the issues, in case these are only concerned with executability. \ definition pseudo_divmod_rel :: "'a::euclidean_ring => 'a mpoly => 'a mpoly => 'a mpoly => 'a mpoly => bool" where "pseudo_divmod_rel a x y q r \ smult a x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ degree r < degree y)" (* the notion of degree resigns a main variable in multivariate polynomials; also, there are infinitely many tuples (a,q,r) such that a x = q y + r *) definition pdiv :: "'a::euclidean_ring mpoly \ 'a mpoly \ ('a \ 'a mpoly)" (infixl "pdiv" 70) where "x pdiv y = (THE (a, q). \r. pseudo_divmod_rel a x y q r)" definition pmod :: "'a::euclidean_ring mpoly \ 'a mpoly \ 'a mpoly" (infixl "pmod" 70) where "x pmod y = (THE r. \a q. pseudo_divmod_rel a x y q r)" definition pdivmod :: "'a::euclidean_ring mpoly \ 'a mpoly \ ('a \ 'a mpoly) \ 'a mpoly" where "pdivmod p q = (p pdiv q, p pmod q)" (* "_code" seems inappropriate, since "THE" in definitions pdiv and pmod is not unique, see comment to definition pseudo_divmod_rel; so this cannot be executable ... *) lemma pdiv_code: "p pdiv q = fst (pdivmod p q)" by (simp add: pdivmod_def) lemma pmod_code: "p pmod q = snd (pdivmod p q)" by (simp add: pdivmod_def) -(*TODO ERROR: Ambiguous input produces n parse trees ???...*) -definition div :: "'a::{euclidean_ring,field} mpoly \ 'a mpoly \ 'a mpoly" (infixl "div" 70) -where - "x div y = (THE q'. \a q r. (pseudo_divmod_rel a x y q r) \ (q' = smult (inverse a) q))" - -definition mod :: "'a::{euclidean_ring,field} mpoly \ 'a mpoly \ 'a mpoly" (infixl "mod" 70) -where - "x mod y = (THE r'. \a q r. (pseudo_divmod_rel a x y q r) \ (r' = smult (inverse a) r))" - -definition divmod :: "'a::{euclidean_ring,field} mpoly \ 'a mpoly \ 'a mpoly \ 'a mpoly" -where - "divmod p q = (p div q, p mod q)" - -lemma div_poly_code: - "p div q = fst (divmod p q)" - by (simp add: divmod_def) - -lemma mod_poly_code: - "p mod q = snd (divmod p q)" - by (simp add: divmod_def) - subsection \Primitive poly, etc\ lift_definition coeffs :: "'a :: zero mpoly \ 'a set" is "Poly_Mapping.range :: ((nat \\<^sub>0 nat) \\<^sub>0 'a) \ _" . lemma finite_coeffs [simp]: "finite (coeffs p)" by transfer simp text \[1]p.82 A "primitive'" polynomial has coefficients with GCD equal to 1. A polynomial is factored into "content" and "primitive part" for many different purposes.\ definition primitive :: "'a::{euclidean_ring,semiring_Gcd} mpoly \ bool" where "primitive p \ Gcd (coeffs p) = 1" definition content_primitive :: "'a::{euclidean_ring,GCD.Gcd} mpoly \ 'a \ 'a mpoly" where "content_primitive p = ( let d = Gcd (coeffs p) in (d, sdiv d p))" value "let p = M [1,2,3] (4::int) + M [2,0,4] 6 + M [2,0,5] 8 in content_primitive p" end diff --git a/thys/Virtual_Substitution/ExecutiblePolyProps.thy b/thys/Virtual_Substitution/ExecutiblePolyProps.thy --- a/thys/Virtual_Substitution/ExecutiblePolyProps.thy +++ b/thys/Virtual_Substitution/ExecutiblePolyProps.thy @@ -1,1084 +1,1081 @@ 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 \\ -no_notation MPoly_Type.div (infixl "div" 70) -no_notation MPoly_Type.mod (infixl "mod" 70) - 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\<^sub>0_def) lemma monomials_Const: "monomials (Const x) = (if x = 0 then {} else {0})" by transfer' (auto simp: Const\<^sub>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\<^sub>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\<^sub>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\<^sub>0_one one_mpoly_def) lemma mult_one_right : "(P::real mpoly) * Const 1 = P" by (simp add: Const.abs_eq Const\<^sub>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\<^sub>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\<^sub>0_def lookup_single) lemma coeff_Var: "MPoly_Type.coeff (Var p) m = (1 when m = monomial 1 p)" by transfer' (auto simp: Var\<^sub>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.. (\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.. ((\i = 0..i = 0..i = 0..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 \\<^sub>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.. 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..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 \\<^sub>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::nat). ((insertion f (\i\{0..i\{0..(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 add: ) 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" proof - obtain pp :: "nat \ nat \ 'a mpoly \ nat \\<^sub>0 nat" where "\x0 x1 x2. (\v3. v3 \ monomials x2 \ \ lookup v3 x1 < x0) = (pp x0 x1 x2 \ monomials x2 \ \ lookup (pp x0 x1 x2) x1 < x0)" by moura then have f1: "\m n na. (\ MPoly_Type.degree m n < na \ 0 < na \ (\p. p \ monomials m \ lookup p n < na)) \ (MPoly_Type.degree m n < na \ \ 0 < na \ pp na n m \ monomials m \ \ lookup (pp na n m) n < na)" by (metis (no_types) degree_less_iff) then have "0 < x \ (\p. p \ monomials a \ lookup p var < x)" using assms(1) by presburger then show ?thesis using f1 by (metis MPolyExtension.coeff_add add.left_neutral assms(2) coeff_eq_zero_iff) qed 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 \\<^sub>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 \\<^sub>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 \\<^sub>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 simp: ) 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.. 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