This instance will be upgraded to Heptapod 0.31.0 (final) on 2022-05-24 at 14:00 UTC+2 (a few minutes of down time)

Commit 97fc7f95 authored by immler's avatar immler
Browse files

renaming and moving theories about polynomials

parent 370db8240e5a
......@@ -3,7 +3,7 @@
section \<open>Polynomials representing the Deep Network Model\<close>
theory DL_Deep_Model_Poly
imports DL_Deep_Model PP_More_MPoly Jordan_Normal_Form.Determinant
imports DL_Deep_Model Polynomials.More_MPoly_Type Jordan_Normal_Form.Determinant
begin
definition "polyfun N f = (\<exists>p. vars p \<subseteq> N \<and> (\<forall>x. insertion x p = f x))"
......@@ -68,7 +68,7 @@ lemma polyfun_single:
assumes "i\<in>N"
shows "polyfun N (\<lambda>x. x i)"
proof -
have "\<forall>f. insertion f (monom (PP_Poly_Mapping.single i 1) 1) = f i" using insertion_single by simp
have "\<forall>f. insertion f (monom (Poly_Mapping.single i 1) 1) = f i" using insertion_single by simp
then show ?thesis unfolding polyfun_def
using vars_monom_single[of i 1 1] One_nat_def assms singletonD subset_eq
by blast
......
......@@ -3,7 +3,10 @@
section \<open>Lebesgue Measure of Polynomial Zero Sets\<close>
theory Lebesgue_Zero_Set
imports PP_MPoly PP_More_MPoly Lebesgue_Functional PP_Univariate
imports
Polynomials.More_MPoly_Type
Lebesgue_Functional
Polynomials.MPoly_Type_Univariate
begin
lemma measurable_insertion [measurable]:
......@@ -14,11 +17,11 @@ using assms proof (induction p rule:mpoly_induct)
then show ?case
proof (cases "a = 0")
case True
show ?thesis unfolding insertion_single `a = 0` PP_MPoly.monom.abs_eq single_zero
show ?thesis unfolding insertion_single `a = 0` MPoly_Type.monom.abs_eq single_zero
zero_mpoly.abs_eq[symmetric] insertion_zero by measurable
next
case False
have "PP_Poly_Mapping.keys m \<subseteq> {..<n}" using monom by (simp add: False vars_monom_keys)
have "Poly_Mapping.keys m \<subseteq> {..<n}" using monom by (simp add: False vars_monom_keys)
then show ?thesis using `a\<noteq>0`
proof (induction m arbitrary:a rule:poly_mapping_induct)
case (single x i a)
......@@ -33,10 +36,10 @@ using assms proof (induction p rule:mpoly_induct)
qed
next
case (sum m1 m2 x i)
then have "PP_Poly_Mapping.keys m1 \<inter> PP_Poly_Mapping.keys m2 = {}" by simp
then have "PP_Poly_Mapping.keys m1 \<union> PP_Poly_Mapping.keys m2 = PP_Poly_Mapping.keys (m1 + m2)" using keys_add by metis
then have 1:"PP_Poly_Mapping.keys m1 \<subseteq> {..<n}" and 2:"PP_Poly_Mapping.keys m2 \<subseteq> {..<n}" using sum.prems by auto
show ?case unfolding PP_MPoly.mult_monom[of m1 a m2 1,simplified,symmetric]
then have "Poly_Mapping.keys m1 \<inter> Poly_Mapping.keys m2 = {}" by simp
then have "Poly_Mapping.keys m1 \<union> Poly_Mapping.keys m2 = Poly_Mapping.keys (m1 + m2)" using keys_add by metis
then have 1:"Poly_Mapping.keys m1 \<subseteq> {..<n}" and 2:"Poly_Mapping.keys m2 \<subseteq> {..<n}" using sum.prems by auto
show ?case unfolding MPoly_Type.mult_monom[of m1 a m2 1,simplified,symmetric]
insertion_mult using sum.IH(1)[OF 1 `a\<noteq>0`] sum.IH(2)[OF 2, of 1, simplified] by measurable
qed
qed
......@@ -57,19 +60,19 @@ assumes "p \<noteq> 0" "vars p \<subseteq> {..<n}"
shows "{f\<in>space (lborel_f n). insertion f p = 0} \<in> null_sets (lborel_f n)"
using assms proof (induction n arbitrary:p)
case 0
then have "vars p = {}" by simp then have "\<And>f. insertion f p = PP_MPoly.coeff p 0"
then have "vars p = {}" by simp then have "\<And>f. insertion f p = MPoly_Type.coeff p 0"
unfolding insertion_trivial[symmetric] using insertion_irrelevant_vars by blast
have "\<And>m. m\<noteq>0 \<Longrightarrow> PP_MPoly.coeff p m = 0"
have "\<And>m. m\<noteq>0 \<Longrightarrow> MPoly_Type.coeff p m = 0"
proof (rule ccontr)
fix m::"nat \<Rightarrow>\<^sub>0 nat" assume "m\<noteq>0" "PP_MPoly.coeff p m \<noteq> 0"
then obtain v where "PP_Poly_Mapping.lookup m v \<noteq> 0" using aux by auto
then have "v\<in>vars p" unfolding PP_More_MPoly.vars_def using `PP_MPoly.coeff p m \<noteq> 0`
fix m::"nat \<Rightarrow>\<^sub>0 nat" assume "m\<noteq>0" "MPoly_Type.coeff p m \<noteq> 0"
then obtain v where "Poly_Mapping.lookup m v \<noteq> 0" using aux by auto
then have "v\<in>vars p" unfolding More_MPoly_Type.vars_def using `MPoly_Type.coeff p m \<noteq> 0`
by (meson UN_I coeff_keys lookup_not_eq_zero_eq_in_keys)
then show False using `vars p = {}` by auto
qed
then have "PP_MPoly.coeff p 0 \<noteq> 0" using `p \<noteq> 0`
then have "MPoly_Type.coeff p 0 \<noteq> 0" using `p \<noteq> 0`
by (metis coeff_all_0)
then have "{f. insertion f p = 0} = {}" using `\<And>f. insertion f p = PP_MPoly.coeff p 0` by auto
then have "{f. insertion f p = 0} = {}" using `\<And>f. insertion f p = MPoly_Type.coeff p 0` by auto
then show ?case by auto
next
case (Suc n p)
......@@ -77,7 +80,7 @@ next
text \<open>Show that N is finite:\<close>
then have "extract_var p n \<noteq> 0" using reduce_nested_mpoly_0
by (metis reduce_nested_mpoly_extract_var)
let ?q = "\<lambda>j. PP_MPoly.coeff (extract_var p n) j"
let ?q = "\<lambda>j. MPoly_Type.coeff (extract_var p n) j"
obtain j where "?q j \<noteq> 0" using `extract_var p n \<noteq> 0`
by (metis coeff_all_0)
then have "finite {x. insertion (\<lambda>_. x) (?q j) = 0}"
......@@ -92,13 +95,13 @@ text \<open>Show that N is finite:\<close>
proof
fix x assume "x\<in>N"
then have "p_fix1 x = 0" using N_def by auto
then have "\<And>m. PP_MPoly.coeff (p_fix1 x) m = 0" by (metis PP_More_MPoly.coeff_monom monom_zero when_def)
then have "\<And>m. MPoly_Type.coeff (p_fix1 x) m = 0" by (metis More_MPoly_Type.coeff_monom monom_zero when_def)
have "\<And>j. insertion (\<lambda>_. x) (?q j) = 0"
using `\<And>m. PP_MPoly.coeff (p_fix1 x) m = 0`[unfolded p_fix1_def coeff_replace_coeff[of "insertion (\<lambda>_. x)", OF insertion_zero]]
using `\<And>m. MPoly_Type.coeff (p_fix1 x) m = 0`[unfolded p_fix1_def coeff_replace_coeff[of "insertion (\<lambda>_. x)", OF insertion_zero]]
by metis
then show "x \<in> {x. \<forall>j. insertion (\<lambda>_. x) (PP_MPoly.coeff (extract_var p n) j) = 0}" by blast
then show "x \<in> {x. \<forall>j. insertion (\<lambda>_. x) (MPoly_Type.coeff (extract_var p n) j) = 0}" by blast
qed
then have "finite N" by (simp add: \<open>finite {x. \<forall>j. insertion (\<lambda>_. x) (PP_MPoly.coeff (extract_var p n) j) = 0}\<close> finite_subset)
then have "finite N" by (simp add: \<open>finite {x. \<forall>j. insertion (\<lambda>_. x) (MPoly_Type.coeff (extract_var p n) j) = 0}\<close> finite_subset)
text \<open>Use the IH:\<close>
......
......@@ -41,6 +41,8 @@ session "Deep_Learning_Lib" (AFP) = "HOL-Probability" +
session "Deep_Learning" (AFP) = "Deep_Learning_Lib" +
options [timeout = 600]
sessions
Polynomials
theories
DL_Fundamental_Theorem_Network_Capacity
document_files
......
......@@ -3,12 +3,14 @@
section \<open>Computing Gr\"obner Bases\<close>
theory Computations
imports Groebner_Bases Polynomials.Poly_Lists "HOL-Library.AList"
imports
Groebner_Bases
Polynomials.MPoly_Type_Class_FMap
begin
text \<open>We now compute concrete Gr\"obner bases w.r.t. both the purely lexicographic and the
degree-lexicographic term order, making use of the implementation of multivariate polynomials in
@{theory "Poly_Lists"}.\<close>
@{theory "MPoly_Type_Class_FMap"}.\<close>
subsection \<open>Lexicographic Order\<close>
......@@ -310,6 +312,6 @@ lemma
]"
by eval
hide_const (open) Poly_Lists.X Poly_Lists.Y Poly_Lists.Z
hide_const (open) MPoly_Type_Class_FMap.X MPoly_Type_Class_FMap.Y MPoly_Type_Class_FMap.Z
end (* theory *)
......@@ -3,7 +3,7 @@
section \<open>Gr\"obner Bases\<close>
theory Groebner_Bases
imports Polynomials.Abstract_Poly Confluence
imports Polynomials.MPoly_Type_Class Confluence
begin
text \<open>This theory provides the main results about Gr\"obner bases of multivariate polynomials.
......@@ -304,7 +304,7 @@ proof -
hence c: "lookup (tail p) (t + lp f) = lookup p (t + lp f)" using lookup_tail[of p] by simp
show ?thesis
proof (intro red_setI[OF \<open>f \<in> F\<close>])
show "red_single p (q + PP_Poly_Mapping.single (lp p) (lc p)) f t" unfolding red_single_def
show "red_single p (q + Poly_Mapping.single (lp p) (lc p)) f t" unfolding red_single_def
proof (intro conjI, fact)
from ct c show "lookup p (t + lp f) \<noteq> 0" by simp
next
......
......@@ -4,8 +4,7 @@ session Groebner_Bases (AFP) = Polynomials +
options [timeout = 600]
theories [document = false]
"Abstract-Rewriting.Abstract_Rewriting"
Polynomials.Abstract_Poly
Polynomials.Poly_Lists
Polynomials.MPoly_Type_Class_FMap
theories
Computations
document_files
......
......@@ -4,8 +4,8 @@
section \<open>An abstract type for multivariate polynomials\<close>
theory PP_MPoly
imports PP_Poly_Mapping
theory MPoly_Type
imports Poly_Mapping
begin
subsection \<open>Abstract type definition\<close>
......@@ -78,7 +78,7 @@ subsection \<open>Multiplication by a coefficient\<close>
(* ?do we need inc_power on abstract polynomials? *)
lift_definition smult :: "'a::{times,zero} \<Rightarrow> 'a mpoly \<Rightarrow> 'a mpoly"
is "\<lambda>a. PP_Poly_Mapping.map (Groups.times a) :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _" .
is "\<lambda>a. Poly_Mapping.map (Groups.times a) :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _" .
(* left lemmas in subsection \<open>Pseudo-division of polynomials\<close>,
because I couldn't disentangle them and the notion of monomials. *)
......@@ -152,10 +152,10 @@ text \<open>
\<close>
lift_definition monom :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> 'a::zero \<Rightarrow> 'a mpoly"
is "PP_Poly_Mapping.single :: (nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> _" .
is "Poly_Mapping.single :: (nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> _" .
lemma mapping_of_monom [simp]:
"mapping_of (monom m a) = PP_Poly_Mapping.single m a"
"mapping_of (monom m a) = Poly_Mapping.single m a"
by(fact monom.rep_eq)
lemma monom_zero [simp]:
......@@ -194,14 +194,13 @@ lemma inj_monom [iff]:
"inj (monom m)"
proof (rule injI, transfer)
fix a b :: 'a and m :: "nat \<Rightarrow>\<^sub>0 nat"
assume "PP_Poly_Mapping.single m a = PP_Poly_Mapping.single m b"
with injD [of "PP_Poly_Mapping.single m" a b]
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: PP_Poly_Mapping.mult_single)
\<comment> \<open>FIXME: why does transfer need so much backtracking until it finds the right goal?\<close>
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_comp)
......@@ -234,7 +233,7 @@ subsection \<open>Monom coefficient lookup\<close>
definition coeff :: "'a::zero mpoly \<Rightarrow> (nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> 'a"
where
"coeff p = PP_Poly_Mapping.lookup (mapping_of p)"
"coeff p = Poly_Mapping.lookup (mapping_of p)"
subsection \<open>Insertion morphism\<close>
......@@ -245,7 +244,7 @@ where
definition insertion_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> 'a) \<Rightarrow> 'a::comm_semiring_1"
where
"insertion_fun f p = (\<Sum>m. p m * (\<Prod>v. f v ^ PP_Poly_Mapping.lookup m v))"
"insertion_fun f p = (\<Sum>m. p m * (\<Prod>v. f v ^ Poly_Mapping.lookup m v))"
text \<open>N.b. have been unable to relate this to @{const insertion_fun_natural} using lifting!\<close>
......@@ -256,14 +255,14 @@ lift_definition insertion :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a mpoly \<Ri
is "insertion_aux" .
lemma aux:
"PP_Poly_Mapping.lookup f = (\<lambda>_. 0) \<longleftrightarrow> f = 0"
"Poly_Mapping.lookup f = (\<lambda>_. 0) \<longleftrightarrow> f = 0"
apply transfer apply simp done
lemma insertion_trivial [simp]:
"insertion (\<lambda>_. 0) p = coeff p 0"
proof -
{ fix f :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a"
have "insertion_aux (\<lambda>_. 0) f = PP_Poly_Mapping.lookup f 0"
have "insertion_aux (\<lambda>_. 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
......@@ -277,9 +276,9 @@ lemma insertion_zero [simp]:
lemma insertion_fun_add:
fixes f p q
shows "insertion_fun f (PP_Poly_Mapping.lookup (p + q)) =
insertion_fun f (PP_Poly_Mapping.lookup p) +
insertion_fun f (PP_Poly_Mapping.lookup 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)
......@@ -299,32 +298,32 @@ lemma insertion_one [simp]:
lemma insertion_fun_mult:
fixes f p q
shows "insertion_fun f (PP_Poly_Mapping.lookup (p * q)) =
insertion_fun f (PP_Poly_Mapping.lookup p) *
insertion_fun f (PP_Poly_Mapping.lookup 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 \<Rightarrow>\<^sub>0 nat"
have "finite {v. PP_Poly_Mapping.lookup m v \<noteq> 0}"
have "finite {v. Poly_Mapping.lookup m v \<noteq> 0}"
by simp
then have "finite {v. f v ^ PP_Poly_Mapping.lookup m v \<noteq> 1}"
then have "finite {v. f v ^ Poly_Mapping.lookup m v \<noteq> 1}"
by (rule rev_finite_subset) (auto intro: ccontr)
}
moreover define g where "g m = (\<Prod>v. f v ^ PP_Poly_Mapping.lookup m v)" for m
moreover define g where "g m = (\<Prod>v. f v ^ Poly_Mapping.lookup m v)" for m
ultimately have *: "\<And>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 (\<lambda>(l, n, m). (m, l, n))"
by (auto intro!: bijI injI simp add: image_def)
let ?P = "{l. PP_Poly_Mapping.lookup p l \<noteq> 0}"
let ?Q = "{n. PP_Poly_Mapping.lookup q n \<noteq> 0}"
let ?PQ = "{l + n | l n. l \<in> PP_Poly_Mapping.keys p \<and> n \<in> PP_Poly_Mapping.keys q}"
have "finite {l + n | l n. PP_Poly_Mapping.lookup p l \<noteq> 0 \<and> PP_Poly_Mapping.lookup q n \<noteq> 0}"
let ?P = "{l. Poly_Mapping.lookup p l \<noteq> 0}"
let ?Q = "{n. Poly_Mapping.lookup q n \<noteq> 0}"
let ?PQ = "{l + n | l n. l \<in> Poly_Mapping.keys p \<and> n \<in> Poly_Mapping.keys q}"
have "finite {l + n | l n. Poly_Mapping.lookup p l \<noteq> 0 \<and> Poly_Mapping.lookup q n \<noteq> 0}"
by (rule finite_not_eq_zero_sumI) simp_all
then have fin_PQ: "finite ?PQ"
by simp
have "(\<Sum>m. PP_Poly_Mapping.lookup (p * q) m * g m) =
(\<Sum>m. (\<Sum>l. PP_Poly_Mapping.lookup p l * (\<Sum>n. PP_Poly_Mapping.lookup q n when m = l + n)) * g m)"
have "(\<Sum>m. Poly_Mapping.lookup (p * q) m * g m) =
(\<Sum>m. (\<Sum>l. Poly_Mapping.lookup p l * (\<Sum>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 "\<dots> = (\<Sum>m. (\<Sum>l. (\<Sum>n. g m * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n) when m = l + n)))"
also have "\<dots> = (\<Sum>m. (\<Sum>l. (\<Sum>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)
......@@ -333,33 +332,33 @@ proof -
apply (auto intro: finite_mult_not_eq_zero_leftI)
apply (simp add: ac_simps mult_when)
done
also have "\<dots> = (\<Sum>m. (\<Sum>(l, n). g m * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n) when m = l + n))"
also have "\<dots> = (\<Sum>m. (\<Sum>(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 \<times> ?Q"])
apply (auto dest!: mult_not_zero)
done
also have "\<dots> = (\<Sum>(m, l, n). g m * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n) when m = l + n)"
also have "\<dots> = (\<Sum>(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 \<times> (?P \<times> ?Q)"])
apply (auto dest!: mult_not_zero simp add: fin_PQ)
apply auto
done
also have "\<dots> = (\<Sum>(l, n, m). g m * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n) when m = l + n)"
also have "\<dots> = (\<Sum>(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 "\<lambda>(l, n, m). (m, l, n)"]) (simp add: fun_eq_iff)
also have "\<dots> = (\<Sum>(l, n). \<Sum>m. g m * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n) when m = l + n)"
also have "\<dots> = (\<Sum>(l, n). \<Sum>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 \<times> ?Q) \<times> ?PQ"])
apply (auto dest!: mult_not_zero simp add: fin_PQ )
apply auto
done
also have "\<dots> = (\<Sum>(l, n). (g l * g n) * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n))"
also have "\<dots> = (\<Sum>(l, n). (g l * g n) * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n))"
by (simp add: *)
also have "\<dots> = (\<Sum>l. \<Sum>n. (g l * g n) * (PP_Poly_Mapping.lookup p l * PP_Poly_Mapping.lookup q n))"
also have "\<dots> = (\<Sum>l. \<Sum>n. (g l * g n) * (Poly_Mapping.lookup p l * Poly_Mapping.lookup q n))"
apply (subst Sum_any.cartesian_product [of "?P \<times> ?Q"])
apply (auto dest!: mult_not_zero)
done
also have "\<dots> = (\<Sum>l. \<Sum>n. (PP_Poly_Mapping.lookup p l * g l) * (PP_Poly_Mapping.lookup q n * g n))"
also have "\<dots> = (\<Sum>l. \<Sum>n. (Poly_Mapping.lookup p l * g l) * (Poly_Mapping.lookup q n * g n))"
by (simp add: ac_simps)
also have "\<dots> =
(\<Sum>m. PP_Poly_Mapping.lookup p m * g m) *
(\<Sum>m. PP_Poly_Mapping.lookup q m * g m)"
(\<Sum>m. Poly_Mapping.lookup p m * g m) *
(\<Sum>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
......@@ -372,11 +371,11 @@ lemma insertion_mult:
subsection \<open>Degree\<close>
lift_definition degree :: "'a::zero mpoly \<Rightarrow> nat \<Rightarrow> nat"
is "\<lambda>p v. Max (insert 0 ((\<lambda>m. PP_Poly_Mapping.lookup m v) ` PP_Poly_Mapping.keys p))" .
is "\<lambda>p v. Max (insert 0 ((\<lambda>m. Poly_Mapping.lookup m v) ` Poly_Mapping.keys p))" .
lift_definition total_degree :: "'a::zero mpoly \<Rightarrow> nat"
is "\<lambda>p. Max (insert 0 ((\<lambda>m. sum (PP_Poly_Mapping.lookup m) (PP_Poly_Mapping.keys m)) ` PP_Poly_Mapping.keys p))" .
is "\<lambda>p. Max (insert 0 ((\<lambda>m. sum (Poly_Mapping.lookup m) (Poly_Mapping.keys m)) ` Poly_Mapping.keys p))" .
lemma degree_zero [simp]:
"degree 0 v = 0"
......@@ -416,7 +415,7 @@ 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 \<Rightarrow> 'a mpoly \<Rightarrow> 'a mpoly"
is "\<lambda>a. PP_Poly_Mapping.map (\<lambda>b. b div a) :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _"
is "\<lambda>a. Poly_Mapping.map (\<lambda>b. b div a) :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _"
.
text \<open>
\qt{Polynomial division} is only possible on univariate polynomials @{text "K[x]"}
......@@ -486,7 +485,7 @@ lemma mod_poly_code:
subsection \<open>Primitive poly, etc\<close>
lift_definition coeffs :: "'a :: zero mpoly \<Rightarrow> 'a set"
is "PP_Poly_Mapping.range :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _" .
is "Poly_Mapping.range :: ((nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) \<Rightarrow> _" .
lemma finite_coeffs [simp]: "finite (coeffs p)"
by transfer simp
......
......@@ -2,7 +2,7 @@
section \<open>Type-Class-Multivariate Polynomials\<close>
theory Abstract_Poly
theory MPoly_Type_Class
imports
Power_Products
begin
......@@ -18,7 +18,7 @@ lemma coeff_monom:
"coeff (monom s c) t = (if t = s then c else 0)"
by (auto simp: coeff_monom)
abbreviation "monomial \<equiv> (\<lambda>c t. PP_Poly_Mapping.single t c)"
abbreviation "monomial \<equiv> (\<lambda>c t. Poly_Mapping.single t c)"
subsection \<open>Multiplication by Monomials (in type class)\<close>
......@@ -457,7 +457,7 @@ next
define c where "c = lookup p t"
define q where "q = except p {t}"
have *: "p = monomial c t + q"
by (rule poly_mapping_eqI, simp add: lookup_add lookup_single PP_Poly_Mapping.when_def, intro conjI impI,
by (rule poly_mapping_eqI, simp add: lookup_add lookup_single Poly_Mapping.when_def, intro conjI impI,
simp add: q_def lookup_except c_def, simp add: q_def lookup_except_eq_idI)
show ?case
proof (simp only: *, rule assms(2))
......@@ -1231,7 +1231,7 @@ definition lp::"('a \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> 'a" where
"lp p \<equiv> (if p = 0 then 0 else ordered_powerprod_lin.Max (keys p))"
definition lc::"('a \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> 'b" where
"lc p \<equiv> PP_Poly_Mapping.lookup p (lp p)"
"lc p \<equiv> Poly_Mapping.lookup p (lp p)"
definition tail::"('a \<Rightarrow>\<^sub>0 'b::zero) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b)" where
"tail p \<equiv> lower p (lp p)"
......
......@@ -2,9 +2,9 @@
section \<open>Executable Representation of Polynomial Mappings as Association Lists\<close>
theory Poly_Lists
theory MPoly_Type_Class_FMap
imports
Abstract_Poly
MPoly_Type_Class
Poly_Mapping_Finite_Map
begin
......@@ -301,7 +301,7 @@ end
lemmas [simp] = compute_zero_pp[symmetric]
lemma compute_monom_mult_poly_mapping[code]:
"monom_mult c t (Pm_fmap xs) = Pm_fmap (if c = 0 then fmempty else shift_map_keys t ((*) c) xs)"
"monom_mult c t (Pm_fmap xs) = Pm_fmap (if c = 0 then fmempty else shift_map_keys t (( * ) c) xs)"
proof (cases "c = 0")
case True
hence "monom_mult c t (Pm_fmap xs) = 0" using monom_mult_left0 by simp
......
(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
theory PP_Univariate
imports PP_MPoly PP_More_MPoly "HOL-Computational_Algebra.Polynomial"
theory MPoly_Type_Univariate
imports
More_MPoly_Type
"HOL-Computational_Algebra.Polynomial"
begin
text \<open>This file connects univariate MPolys to the theory of univariate polynomials from
@{file "~~/src/HOL/Computational_Algebra/Polynomial.thy"}.\<close>
definition poly_to_mpoly::"nat \<Rightarrow> 'a::comm_monoid_add poly \<Rightarrow> 'a mpoly"
where "poly_to_mpoly v p = MPoly (Abs_poly_mapping (\<lambda>m. (coeff p (PP_Poly_Mapping.lookup m v)) when PP_Poly_Mapping.keys m \<subseteq> {v}))"
where "poly_to_mpoly v p = MPoly (Abs_poly_mapping (\<lambda>m. (coeff p (Poly_Mapping.lookup m v)) when Poly_Mapping.keys m \<subseteq> {v}))"
lemma poly_to_mpoly_finite: "finite {m::nat \<Rightarrow>\<^sub>0 nat. (coeff p (PP_Poly_Mapping.lookup m v) when PP_Poly_Mapping.keys m \<subseteq> {v}) \<noteq> 0}" (is "finite ?M")
lemma poly_to_mpoly_finite: "finite {m::nat \<Rightarrow>\<^sub>0 nat. (coeff p (Poly_Mapping.lookup m v) when Poly_Mapping.keys m \<subseteq> {v}) \<noteq> 0}" (is "finite ?M")
proof -
have "?M \<subseteq> PP_Poly_Mapping.single v ` {x. Polynomial.coeff p x \<noteq> 0}"
have "?M \<subseteq> Poly_Mapping.single v ` {x. Polynomial.coeff p x \<noteq> 0}"
proof
fix m assume "m \<in> ?M"
then have "\<And>v'. v'\<noteq>v \<Longrightarrow> PP_Poly_Mapping.lookup m v' = 0" by fastforce
then have "m = PP_Poly_Mapping.single v (PP_Poly_Mapping.lookup m v)"
using PP_Poly_Mapping.poly_mapping_eqI by (metis (full_types) lookup_single_eq lookup_single_not_eq)
then show "m \<in> (PP_Poly_Mapping.single v) ` {x. Polynomial.coeff p x \<noteq> 0}" using \<open>m \<in> ?M\<close> by auto
then have "\<And>v'. v'\<noteq>v \<Longrightarrow> Poly_Mapping.lookup m v' = 0" by fastforce
then have "m = Poly_Mapping.single v (Poly_Mapping.lookup m v)"
using Poly_Mapping.poly_mapping_eqI by (metis (full_types) lookup_single_eq lookup_single_not_eq)
then show "m \<in> (Poly_Mapping.single v) ` {x. Polynomial.coeff p x \<noteq> 0}" using \<open>m \<in> ?M\<close> by auto
qed
then show ?thesis using finite_surj[OF MOST_coeff_eq_0[unfolded eventually_cofinite]] by blast
qed
lemma coeff_poly_to_mpoly: "PP_MPoly.coeff (poly_to_mpoly v p) (PP_Poly_Mapping.single v k) = Polynomial.coeff p k"
lemma coeff_poly_to_mpoly: "MPoly_Type.coeff (poly_to_mpoly v p) (Poly_Mapping.single v k) = Polynomial.coeff p k"
unfolding poly_to_mpoly_def coeff_def MPoly_inverse[OF Set.UNIV_I] lookup_Abs_poly_mapping[OF poly_to_mpoly_finite]
using empty_subsetI keys_single lookup_single order_refl when_simps(1) by simp
definition mpoly_to_poly::"nat \<Rightarrow> 'a::comm_monoid_add mpoly \<Rightarrow> 'a poly"
where "mpoly_to_poly v p = Abs_poly (\<lambda>k. PP_MPoly.coeff p (PP_Poly_Mapping.single v k))"
where "mpoly_to_poly v p = Abs_poly (\<lambda>k. MPoly_Type.coeff p (Poly_Mapping.single v k))"
lemma coeff_mpoly_to_poly[simp]: "Polynomial.coeff (mpoly_to_poly v p) k = PP_MPoly.coeff p (PP_Poly_Mapping.single v k)"
lemma coeff_mpoly_to_poly[simp]: "Polynomial.coeff (mpoly_to_poly v p) k = MPoly_Type.coeff p (Poly_Mapping.single v k)"
proof -
have 0:"PP_Poly_Mapping.single v ` {x. PP_Poly_Mapping.lookup (mapping_of p) (PP_Poly_Mapping.single v x) \<noteq> 0}
\<subseteq> {k. PP_Poly_Mapping.lookup (mapping_of p) k \<noteq> 0}"
have 0:"Poly_Mapping.single v ` {x. Poly_Mapping.lookup (mapping_of p) (Poly_Mapping.single v x) \<noteq> 0}
\<subseteq> {k. Poly_Mapping.lookup (mapping_of p) k \<noteq> 0}"
by auto
have "\<forall>\<^sub>\<infinity> k. PP_MPoly.coeff p (PP_Poly_Mapping.single v k) = 0" unfolding coeff_def eventually_cofinite
using finite_imageD[OF finite_subset[OF 0 PP_Poly_Mapping.finite_lookup]] inj_single by (metis inj_eq inj_onI)
have "\<forall>\<^sub>\<infinity> k. MPoly_Type.coeff p (Poly_Mapping.single v k) = 0" unfolding coeff_def eventually_cofinite
using finite_imageD[OF finite_subset[OF 0 Poly_Mapping.finite_lookup]] inj_single by (metis inj_eq inj_onI)
then show ?thesis
unfolding mpoly_to_poly_def by (simp add: Abs_poly_inverse)
qed
......@@ -45,22 +47,22 @@ lemma mpoly_to_poly_inverse:
assumes "vars p \<subseteq> {v}"
shows "poly_to_mpoly v (mpoly_to_poly v p) = p"
proof -
define f where "f = (\<lambda>m. Polynomial.coeff (mpoly_to_poly v p) (PP_Poly_Mapping.lookup m v) when PP_Poly_Mapping.keys m \<subseteq> {v})"
define f where "f = (\<lambda>m. Polynomial.coeff (mpoly_to_poly v p) (Poly_Mapping.lookup m v) when Poly_Mapping.keys m \<subseteq> {v})"
have "finite {m. f m \<noteq> 0}" unfolding f_def using poly_to_mpoly_finite by blast
have "Abs_poly_mapping f = mapping_of p"
proof (rule "PP_Poly_Mapping.poly_mapping_eqI")
proof (rule "Poly_Mapping.poly_mapping_eqI")
fix m
show "PP_Poly_Mapping.lookup (Abs_poly_mapping f) m = PP_Poly_Mapping.lookup (mapping_of p) m"
proof (cases "PP_Poly_Mapping.keys m \<subseteq> {v}")
assume "PP_Poly_Mapping.keys m \<subseteq> {v}"
then show ?thesis unfolding "PP_Poly_Mapping.lookup_Abs_poly_mapping"[OF `finite {m. f m \<noteq> 0}`] unfolding f_def
show "Poly_Mapping.lookup (Abs_poly_mapping f) m = Poly_Mapping.lookup (mapping_of p) m"
proof (cases "Poly_Mapping.keys m \<subseteq> {v}")
assume "Poly_Mapping.keys m \<subseteq> {v}"
then show ?thesis unfolding "Poly_Mapping.lookup_Abs_poly_mapping"[OF `finite {m. f m \<noteq> 0}`] unfolding f_def
unfolding coeff_mpoly_to_poly coeff_def using when_simps(1) apply simp
using keys_single lookup_not_eq_zero_eq_in_keys lookup_single_eq
lookup_single_not_eq poly_mapping_eqI subset_singletonD
by (metis (no_types, lifting) aux lookup_eq_zero_in_keys_contradict)
next
assume "\<not>PP_Poly_Mapping.keys m \<subseteq> {v}"
then show ?thesis unfolding "PP_Poly_Mapping.lookup_Abs_poly_mapping"[OF `finite {m. f m \<noteq> 0}`] unfolding f_def
assume "\<not>Poly_Mapping.keys m \<subseteq> {v}"
then show ?thesis unfolding "Poly_Mapping.lookup_Abs_poly_mapping"[OF `finite {m. f m \<noteq> 0}`] unfolding f_def
using `vars p \<subseteq> {v}` unfolding vars_def by (metis (no_types, lifting) UN_I lookup_not_eq_zero_eq_in_keys subsetCE subsetI when_def)
qed
qed
......@@ -73,14 +75,14 @@ lemma poly_to_mpoly_inverse: "mpoly_to_poly v (poly_to_mpoly v p) = p"
lemma poly_to_mpoly0: "poly_to_mpoly v 0 = 0"
proof -
have "\<And>m. (Polynomial.coeff 0 (PP_Poly_Mapping.lookup m v) when PP_Poly_Mapping.keys m \<subseteq> {v}) = 0" by simp
have "Abs_poly_mapping (\<lambda>m. Polynomial.coeff 0 (PP_Poly_Mapping.lookup m v) when PP_Poly_Mapping.keys m \<subseteq> {v}) = 0"
apply (rule PP_Poly_Mapping.poly_mapping_eqI) unfolding lookup_Abs_poly_mapping[OF poly_to_mpoly_finite] by auto
have "\<And>m. (Polynomial.coeff 0 (Poly_Mapping.lookup m v) when Poly_Mapping.keys m \<subseteq> {v}) = 0" by simp
have "Abs_poly_mapping (\<lambda>m. Polynomial.coeff 0 (Poly_Mapping.lookup m v) when Poly_Mapping.keys m \<subseteq> {v}) = 0"
apply (rule Poly_Mapping.poly_mapping_eqI) unfolding lookup_Abs_poly_mapping[OF poly_to_mpoly_finite] by auto
then show ?thesis using poly_to_mpoly_def zero_mpoly.abs_eq by (metis (no_types))
qed
lemma mpoly_to_poly_add: "mpoly_to_poly v (p1 + p2) = mpoly_to_poly v p1 + mpoly_to_poly v p2"
unfolding Polynomial.plus_poly.abs_eq PP_More_MPoly.coeff_add coeff_mpoly_to_poly
unfolding Polynomial.plus_poly.abs_eq More_MPoly_Type.coeff_add coeff_mpoly_to_poly
using mpoly_to_poly_def by auto
lemma poly_eq_insertion:
......@@ -92,20 +94,20 @@ using assms proof (induction p rule:mpoly_induct)
proof (cases "a=0")
case True
then show ?thesis
by (metis PP_MPoly.monom.abs_eq insertion_zero monom_zero poly_0 poly_to_mpoly0 poly_to_mpoly_inverse single_zero)
by (metis MPoly_Type.monom.abs_eq insertion_zero monom_zero poly_0 poly_to_mpoly0 poly_to_mpoly_inverse single_zero)
next
case False
then have "PP_Poly_Mapping.keys m \<subseteq> {v}" using monom unfolding vars_def PP_MPoly.mapping_of_monom keys_single by simp
then have "\<And>v'. v'\<noteq>v \<Longrightarrow> PP_Poly_Mapping.lookup m v' = 0" unfolding vars_def by auto
then have "m = PP_Poly_Mapping.single v (PP_Poly_Mapping.lookup m v)"
then have "Poly_Mapping.keys m \<subseteq> {v}" using monom unfolding vars_def MPoly_Type.mapping_of_monom keys_single by simp
then have "\<And>v'. v'\<noteq>v \<Longrightarrow> Poly_Mapping.lookup m v' = 0" unfolding vars_def by auto
then have "m = Poly_Mapping.single v (Poly_Mapping.lookup m v)"
by (metis lookup_single_eq lookup_single_not_eq poly_mapping_eqI)
then have 0:"insertion (\<lambda>v. x) (PP_MPoly.monom m a) = a * x ^ (PP_Poly_Mapping.lookup m v)"
then have 0:"insertion (\<lambda>v. x) (MPoly_Type.monom m a) = a * x ^ (Poly_Mapping.lookup m v)"
using insertion_single by metis
have "\<And>k. PP_Poly_Mapping.single v k = m \<longleftrightarrow> PP_Poly_Mapping.lookup m v = k"
using \<open>m = PP_Poly_Mapping.single v (PP_Poly_Mapping.lookup m v)\<close> by auto
then have "monom a (PP_Poly_Mapping.lookup m v) = (Abs_poly (\<lambda>k. if PP_Poly_Mapping.single v k = m then a else 0))"
have "\<And>k. Poly_Mapping.single v k = m \<longleftrightarrow> Poly_Mapping.lookup m v = k"
using \<open>m = Poly_Mapping.single v (Poly_Mapping.lookup m v)\<close> by auto
then have "monom a (Poly_Mapping.lookup m v) = (Abs_poly (\<lambda>k. if Poly_Mapping.single v k = m then a else 0))"
by (simp add: Polynomial.monom.abs_eq)
then show ?thesis unfolding mpoly_to_poly_def PP_More_MPoly.coeff_monom 0 when_def by (metis poly_monom)
then show ?thesis unfolding mpoly_to_poly_def More_MPoly_Type.coeff_monom 0 when_def by (metis poly_monom)
qed
next
case (sum p1 p2 m a)
......
......@@ -4,7 +4,7 @@
section \<open>Less common functions on lists\<close>
theory PP_More_List2
theory More_List2
imports
Main
begin
......
(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
theory PP_More_MPoly
imports PP_MPoly
theory More_MPoly_Type
imports MPoly_Type
begin
abbreviation "lookup == PP_Poly_Mapping.lookup"
abbreviation "keys == PP_Poly_Mapping.keys"
abbreviation "lookup == Poly_Mapping.lookup"
abbreviation "keys == Poly_Mapping.keys"
section "MPpoly Mapping extenion"
......@@ -38,25 +38,25 @@ next
qed
lemma remove_key_sum: "remove_key k f + PP_Poly_Mapping.single k (lookup f k) = f"
lemma remove_key_sum: "remove_key k f + Poly_Mapping.single k (lookup f k) = f"
proof -
{
fix k'
have rem:"(lookup f k' when k' \<noteq> k) = lookup (remove_key k f) k'"
using when_def by (simp add: remove_key_lookup)
have sin:"(lookup f k when k'=k) = lookup (PP_Poly_Mapping.single k (lookup f k)) k'"
have sin:"(lookup f k when k'=k) = lookup (Poly_Mapping.single k (lookup f k)) k'"
by (simp add: lookup_single_not_eq when_def)
have "lookup f k' = (lookup f k' when k' \<noteq> k) + ((lookup f k) when k'=k)"
unfolding when_def by fastforce
with rem sin have "lookup f k' = lookup ((remove_key k f) + PP_Poly_Mapping.single k (lookup f k)) k'"
with rem sin have "lookup f k' = lookup ((remove_key k f) + Poly_Mapping.single k (lookup f k)) k'"
using lookup_add by metis
}
then show ?thesis by (metis poly_mapping_eqI)
qed
lemma remove_key_single[simp]: "remove_key v (PP_Poly_Mapping.single v n) = 0"