(*
Title: HOL/Computational_Algebra/Formal_Laurent_Series.thy
Author: Jeremy Sylvestre, University of Alberta (Augustana Campus)
*)
section \<open>A formalization of formal Laurent series\<close>
theory Formal_Laurent_Series
imports
Polynomial_FPS
begin
subsection \<open>The type of formal Laurent series\<close>
subsubsection \<open>Type definition\<close>
typedef (overloaded) 'a fls = "{f::int \ 'a::zero. \\<^sub>\ n::nat. f (- int n) = 0}"
morphisms fls_nth Abs_fls
proof
show "(\x. 0) \ {f::int \ 'a::zero. \\<^sub>\ n::nat. f (- int n) = 0}"
by simp
qed
setup_lifting type_definition_fls
unbundle fps_notation
notation fls_nth (infixl "$$" 75)
lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]
lemma expand_fls_eq: "f = g \ (\n. f $$ n = g $$ n)"
by (simp add: fls_nth_inject[symmetric] fun_eq_iff)
lemma nth_Abs_fls [simp]: "\\<^sub>\n. f (- int n) = 0 \ Abs_fls f $$ n = f n"
by (simp add: Abs_fls_inverse[OF CollectI])
lemmas nth_Abs_fls_finite_nonzero_neg_nth = nth_Abs_fls[OF iffD2, OF eventually_cofinite]
lemmas nth_Abs_fls_ex_nat_lower_bound = nth_Abs_fls[OF iffD2, OF MOST_nat]
lemmas nth_Abs_fls_nat_lower_bound = nth_Abs_fls_ex_nat_lower_bound[OF exI]
lemma nth_Abs_fls_ex_lower_bound:
assumes "\N. \n
shows "Abs_fls f $$ n = f n"
proof (intro nth_Abs_fls_ex_nat_lower_bound)
from assms obtain N::int where "\n
hence "\n > (if N < 0 then nat (-N) else 0). f (-int n) = 0" by auto
thus "\M. \n>M. f (- int n) = 0" by fast
qed
lemmas nth_Abs_fls_lower_bound = nth_Abs_fls_ex_lower_bound[OF exI]
lemmas MOST_fls_neg_nth_eq_0 [simp] = CollectD[OF fls_nth]
lemmas fls_finite_nonzero_neg_nth = iffD1[OF eventually_cofinite MOST_fls_neg_nth_eq_0]
lemma fls_nth_vanishes_below_natE:
fixes f :: "'a::zero fls"
obtains N :: nat
where "\n>N. f$$(-int n) = 0"
using iffD1[OF MOST_nat MOST_fls_neg_nth_eq_0]
by blast
lemma fls_nth_vanishes_belowE:
fixes f :: "'a::zero fls"
obtains N :: int
where "\n
proof-
obtain K :: nat where K: "\n>K. f$$(-int n) = 0" by (elim fls_nth_vanishes_below_natE)
have "\n < -int K. f$$n = 0"
proof clarify
fix n assume n: "n < -int K"
define m where "m \ nat (-n)"
with n have "m > K" by simp
moreover from n m_def have "f$$n = f $$ (-int m)" by simp
ultimately show "f $$ n = 0" using K by simp
qed
thus "(\N. \n thesis) \ thesis" by fast
qed
subsubsection \<open>Definition of basic zero, one, constant, X, and inverse X elements\<close>
instantiation fls :: (zero) zero
begin
lift_definition zero_fls :: "'a fls" is "\_. 0" by simp
instance ..
end
lemma fls_zero_nth [simp]: "0 $$ n = 0"
by (simp add: zero_fls_def)
lemma fls_zero_eqI: "(\n. f$$n = 0) \ f = 0"
by (fastforce intro: fls_eqI)
lemma fls_nonzeroI: "f$$n \ 0 \ f \ 0"
by auto
lemma fls_nonzero_nth: "f \ 0 \ (\ n. f $$ n \ 0)"
using fls_zero_eqI by fastforce
lemma fls_trivial_delta_eq_zero [simp]: "b = 0 \ Abs_fls (\n. if n=a then b else 0) = 0"
by (intro fls_zero_eqI) simp
lemma fls_delta_nth [simp]:
"Abs_fls (\n. if n=a then b else 0) $$ n = (if n=a then b else 0)"
using nth_Abs_fls_lower_bound[of a "\n. if n=a then b else 0"] by simp
instantiation fls :: ("{zero,one}") one
begin
lift_definition one_fls :: "'a fls" is "\k. if k = 0 then 1 else 0"
by (simp add: eventually_cofinite)
instance ..
end
lemma fls_one_nth [simp]:
"1 $$ n = (if n = 0 then 1 else 0)"
by (simp add: one_fls_def eventually_cofinite)
instance fls :: (zero_neq_one) zero_neq_one
proof (standard, standard)
assume "(0::'a fls) = (1::'a fls)"
hence "(0::'a fls) $$ 0 = (1::'a fls) $$ 0" by simp
thus False by simp
qed
definition fls_const :: "'a::zero \ 'a fls"
where "fls_const c \ Abs_fls (\n. if n = 0 then c else 0)"
lemma fls_const_nth [simp]: "fls_const c $$ n = (if n = 0 then c else 0)"
by (simp add: fls_const_def eventually_cofinite)
lemma fls_const_0 [simp]: "fls_const 0 = 0"
unfolding fls_const_def using fls_trivial_delta_eq_zero by fast
lemma fls_const_nonzero: "c \ 0 \ fls_const c \ 0"
using fls_nonzeroI[of "fls_const c" 0] by simp
lemma fls_const_1 [simp]: "fls_const 1 = 1"
unfolding fls_const_def one_fls_def ..
lift_definition fls_X :: "'a::{zero,one} fls"
is "\n. if n = 1 then 1 else 0"
by simp
lemma fls_X_nth [simp]:
"fls_X $$ n = (if n = 1 then 1 else 0)"
by (simp add: fls_X_def)
lemma fls_X_nonzero [simp]: "(fls_X :: 'a :: zero_neq_one fls) \ 0"
by (intro fls_nonzeroI) simp
lift_definition fls_X_inv :: "'a::{zero,one} fls"
is "\n. if n = -1 then 1 else 0"
by (simp add: eventually_cofinite)
lemma fls_X_inv_nth [simp]:
"fls_X_inv $$ n = (if n = -1 then 1 else 0)"
by (simp add: fls_X_inv_def eventually_cofinite)
lemma fls_X_inv_nonzero [simp]: "(fls_X_inv :: 'a :: zero_neq_one fls) \ 0"
by (intro fls_nonzeroI) simp
subsection \<open>Subdegrees\<close>
lemma unique_fls_subdegree:
assumes "f \ 0"
shows "\!n. f$$n \ 0 \ (\m. f$$m \ 0 \ n \ m)"
proof-
obtain N::nat where N: "\n>N. f$$(-int n) = 0" by (elim fls_nth_vanishes_below_natE)
define M where "M \ -int N"
have M: "\m. f$$m \ 0 \ M \ m"
proof-
fix m assume m: "f$$m \ 0"
show "M \ m"
proof (cases "m<0")
case True with m N M_def show ?thesis
using allE[OF N, of "nat (-m)" False] by force
qed (simp add: M_def)
qed
have "\ (\k::nat. f$$(M + int k) = 0)"
proof
assume above0: "\k::nat. f$$(M + int k) = 0"
have "f=0"
proof (rule fls_zero_eqI)
fix n show "f$$n = 0"
proof (cases "M \ n")
case True
define k where "k = nat (n - M)"
from True have "n = M + int k" by (simp add: k_def)
with above0 show ?thesis by simp
next
case False with M show ?thesis by auto
qed
qed
with assms show False by fast
qed
hence ex_k: "\k::nat. f$$(M + int k) \ 0" by fast
define k where "k \ (LEAST k::nat. f$$(M + int k) \ 0)"
define n where "n \ M + int k"
from k_def n_def have fn: "f$$n \ 0" using LeastI_ex[OF ex_k] by simp
moreover have "\m. f$$m \ 0 \ n \ m"
proof (clarify)
fix m assume m: "f$$m \ 0"
with M have "M \ m" by fast
define l where "l = nat (m - M)"
from \<open>M \<le> m\<close> have l: "m = M + int l" by (simp add: l_def)
with n_def m k_def l show "n \ m"
using Least_le[of "\k. f$$(M + int k) \ 0" l] by auto
qed
moreover have "\n'. f$$n' \ 0 \ (\m. f$$m \ 0 \ n' \ m) \ n' = n"
proof-
fix n' :: int
assume n': "f$$n' \<noteq> 0" "\<forall>m. f$$m \<noteq> 0 \<longrightarrow> n' \<le> m"
from n'(1) M have "M \ n'" by fast
define l where "l = nat (n' - M)"
from \<open>M \<le> n'\<close> have l: "n' = M + int l" by (simp add: l_def)
with n_def k_def n' fn show "n' = n"
using Least_le[of "\k. f$$(M + int k) \ 0" l] by force
qed
ultimately show ?thesis
using ex1I[of "\n. f$$n \ 0 \ (\m. f$$m \ 0 \ n \ m)" n] by blast
qed
definition fls_subdegree :: "('a::zero) fls \ int"
where "fls_subdegree f \ (if f = 0 then 0 else LEAST n::int. f$$n \ 0)"
lemma fls_zero_subdegree [simp]: "fls_subdegree 0 = 0"
by (simp add: fls_subdegree_def)
lemma nth_fls_subdegree_nonzero [simp]: "f \ 0 \ f $$ fls_subdegree f \ 0"
using Least1I[OF unique_fls_subdegree] by (simp add: fls_subdegree_def)
lemma nth_fls_subdegree_zero_iff: "(f $$ fls_subdegree f = 0) \ (f = 0)"
using nth_fls_subdegree_nonzero by auto
lemma fls_subdegree_leI: "f $$ n \ 0 \ fls_subdegree f \ n"
using Least1_le[OF unique_fls_subdegree]
by (auto simp: fls_subdegree_def)
lemma fls_subdegree_leI': "f $$ n \ 0 \ n \ m \ fls_subdegree f \ m"
using fls_subdegree_leI by fastforce
lemma fls_eq0_below_subdegree [simp]: "n < fls_subdegree f \ f $$ n = 0"
using fls_subdegree_leI by fastforce
lemma fls_subdegree_geI: "f \ 0 \ (\k. k < n \ f $$ k = 0) \ n \ fls_subdegree f"
using nth_fls_subdegree_nonzero by force
lemma fls_subdegree_ge0I: "(\k. k < 0 \ f $$ k = 0) \ 0 \ fls_subdegree f"
using fls_subdegree_geI[of f 0] by (cases "f=0") auto
lemma fls_subdegree_greaterI:
assumes "f \ 0" "\k. k \ n \ f $$ k = 0"
shows "n < fls_subdegree f"
using assms(1) assms(2)[of "fls_subdegree f"] nth_fls_subdegree_nonzero[of f]
by force
lemma fls_subdegree_eqI: "f $$ n \ 0 \ (\k. k < n \ f $$ k = 0) \ fls_subdegree f = n"
using fls_subdegree_leI fls_subdegree_geI[of f]
by fastforce
lemma fls_delta_subdegree [simp]:
"b \ 0 \ fls_subdegree (Abs_fls (\n. if n=a then b else 0)) = a"
by (intro fls_subdegree_eqI) simp_all
lemma fls_delta0_subdegree: "fls_subdegree (Abs_fls (\n. if n=0 then a else 0)) = 0"
by (cases "a=0") simp_all
lemma fls_one_subdegree [simp]: "fls_subdegree 1 = 0"
by (auto intro: fls_delta0_subdegree simp: one_fls_def)
lemma fls_const_subdegree [simp]: "fls_subdegree (fls_const c) = 0"
by (cases "c=0") (auto intro: fls_subdegree_eqI)
lemma fls_X_subdegree [simp]: "fls_subdegree (fls_X::'a::{zero_neq_one} fls) = 1"
by (intro fls_subdegree_eqI) simp_all
lemma fls_X_inv_subdegree [simp]: "fls_subdegree (fls_X_inv::'a::{zero_neq_one} fls) = -1"
by (intro fls_subdegree_eqI) simp_all
lemma fls_eq_above_subdegreeI:
assumes "N \ fls_subdegree f" "N \ fls_subdegree g" "\k\N. f $$ k = g $$ k"
shows "f = g"
proof (rule fls_eqI)
fix n from assms show "f $$ n = g $$ n" by (cases "n < N") auto
qed
subsection \<open>Shifting\<close>
subsubsection \<open>Shift definition\<close>
definition fls_shift :: "int \ ('a::zero) fls \ 'a fls"
where "fls_shift n f \ Abs_fls (\k. f $$ (k+n))"
\<comment> \<open>Since the index set is unbounded in both directions, we can shift in either direction.\<close>
lemma fls_shift_nth [simp]: "fls_shift m f $$ n = f $$ (n+m)"
unfolding fls_shift_def
proof (rule nth_Abs_fls_ex_lower_bound)
obtain K::int where K: "\n
hence "\n
thus "\N. \n
qed
lemma fls_shift_eq_iff: "(fls_shift m f = fls_shift m g) \ (f = g)"
proof (rule iffI, rule fls_eqI)
fix k
assume 1: "fls_shift m f = fls_shift m g"
have "f $$ k = fls_shift m g $$ (k - m)" by (simp add: 1[symmetric])
thus "f $$ k = g $$ k" by simp
qed (intro fls_eqI, simp)
lemma fls_shift_0 [simp]: "fls_shift 0 f = f"
by (intro fls_eqI) simp
lemma fls_shift_subdegree [simp]:
"f \ 0 \ fls_subdegree (fls_shift n f) = fls_subdegree f - n"
by (intro fls_subdegree_eqI) simp_all
lemma fls_shift_fls_shift [simp]: "fls_shift m (fls_shift k f) = fls_shift (k+m) f"
by (intro fls_eqI) (simp add: algebra_simps)
lemma fls_shift_fls_shift_reorder:
"fls_shift m (fls_shift k f) = fls_shift k (fls_shift m f)"
using fls_shift_fls_shift[of m k f] fls_shift_fls_shift[of k m f] by (simp add: add.commute)
lemma fls_shift_zero [simp]: "fls_shift m 0 = 0"
by (intro fls_zero_eqI) simp
lemma fls_shift_eq0_iff: "fls_shift m f = 0 \ f = 0"
using fls_shift_eq_iff[of m f 0] by simp
lemma fls_shift_nonneg_subdegree: "m \ fls_subdegree f \ fls_subdegree (fls_shift m f) \ 0"
by (cases "f=0") (auto intro: fls_subdegree_geI)
lemma fls_shift_delta:
"fls_shift m (Abs_fls (\n. if n=a then b else 0)) = Abs_fls (\n. if n=a-m then b else 0)"
by (intro fls_eqI) simp
lemma fls_shift_const:
"fls_shift m (fls_const c) = Abs_fls (\n. if n=-m then c else 0)"
by (intro fls_eqI) simp
lemma fls_shift_const_nth:
"fls_shift m (fls_const c) $$ n = (if n=-m then c else 0)"
by (simp add: fls_shift_const)
lemma fls_X_conv_shift_1: "fls_X = fls_shift (-1) 1"
by (intro fls_eqI) simp
lemma fls_X_shift_to_one [simp]: "fls_shift 1 fls_X = 1"
using fls_shift_fls_shift[of "-1" 1 1] by (simp add: fls_X_conv_shift_1)
lemma fls_X_inv_conv_shift_1: "fls_X_inv = fls_shift 1 1"
by (intro fls_eqI) simp
lemma fls_X_inv_shift_to_one [simp]: "fls_shift (-1) fls_X_inv = 1"
using fls_shift_fls_shift[of 1 "-1" 1] by (simp add: fls_X_inv_conv_shift_1)
lemma fls_X_fls_X_inv_conv:
"fls_X = fls_shift (-2) fls_X_inv" "fls_X_inv = fls_shift 2 fls_X"
by (simp_all add: fls_X_conv_shift_1 fls_X_inv_conv_shift_1)
subsubsection \<open>Base factor\<close>
text \<open>
Similarly to the @{const unit_factor} for formal power series, we can decompose a formal Laurent
series as a power of the implied variable times a series of subdegree 0.
(See lemma @{text "fls_base_factor_X_power_decompose"}.)
But we will call this something other @{const unit_factor}
because it will not satisfy assumption @{text "is_unit_unit_factor"} of
@{class semidom_divide_unit_factor}.
\<close>
definition fls_base_factor :: "('a::zero) fls \ 'a fls"
where fls_base_factor_def[simp]: "fls_base_factor f = fls_shift (fls_subdegree f) f"
lemma fls_base_factor_nth: "fls_base_factor f $$ n = f $$ (n + fls_subdegree f)"
by simp
lemma fls_base_factor_nonzero [simp]: "f \ 0 \ fls_base_factor f \ 0"
using fls_nonzeroI[of "fls_base_factor f" 0] by simp
lemma fls_base_factor_subdegree [simp]: "fls_subdegree (fls_base_factor f) = 0"
by (cases "f=0") auto
lemma fls_base_factor_base [simp]:
"fls_base_factor f $$ fls_subdegree (fls_base_factor f) = f $$ fls_subdegree f"
using fls_base_factor_subdegree[of f] by simp
lemma fls_conv_base_factor_shift_subdegree:
"f = fls_shift (-fls_subdegree f) (fls_base_factor f)"
by simp
lemma fls_base_factor_idem:
"fls_base_factor (fls_base_factor (f::'a::zero fls)) = fls_base_factor f"
using fls_base_factor_subdegree[of f] by simp
lemma fls_base_factor_zero: "fls_base_factor (0::'a::zero fls) = 0"
by simp
lemma fls_base_factor_zero_iff: "fls_base_factor (f::'a::zero fls) = 0 \ f = 0"
proof
have "fls_shift (-fls_subdegree f) (fls_shift (fls_subdegree f) f) = f" by simp
thus "fls_base_factor f = 0 \ f=0" by simp
qed simp
lemma fls_base_factor_nth_0: "f \ 0 \ fls_base_factor f $$ 0 \ 0"
by simp
lemma fls_base_factor_one: "fls_base_factor (1::'a::{zero,one} fls) = 1"
by simp
lemma fls_base_factor_const: "fls_base_factor (fls_const c) = fls_const c"
by simp
lemma fls_base_factor_delta:
"fls_base_factor (Abs_fls (\n. if n=a then c else 0)) = fls_const c"
by (cases "c=0") (auto intro: fls_eqI)
lemma fls_base_factor_X: "fls_base_factor (fls_X::'a::{zero_neq_one} fls) = 1"
by simp
lemma fls_base_factor_X_inv: "fls_base_factor (fls_X_inv::'a::{zero_neq_one} fls) = 1"
by simp
lemma fls_base_factor_shift [simp]: "fls_base_factor (fls_shift n f) = fls_base_factor f"
by (cases "f=0") simp_all
subsection \<open>Conversion between formal power and Laurent series\<close>
subsubsection \<open>Converting Laurent to power series\<close>
text \<open>
We can truncate a Laurent series at index 0 to create a power series, called the regular part.
\<close>
lift_definition fls_regpart :: "('a::zero) fls \ 'a fps"
is "\f. Abs_fps (\n. f (int n))"
.
lemma fls_regpart_nth [simp]: "fls_regpart f $ n = f $$ (int n)"
by (simp add: fls_regpart_def)
lemma fls_regpart_zero [simp]: "fls_regpart 0 = 0"
by (intro fps_ext) simp
lemma fls_regpart_one [simp]: "fls_regpart 1 = 1"
by (intro fps_ext) simp
lemma fls_regpart_Abs_fls:
"\\<^sub>\n. F (- int n) = 0 \ fls_regpart (Abs_fls F) = Abs_fps (\n. F (int n))"
by (intro fps_ext) auto
lemma fls_regpart_delta:
"fls_regpart (Abs_fls (\n. if n=a then b else 0)) =
(if a < 0 then 0 else Abs_fps (\<lambda>n. if n=nat a then b else 0))"
by (rule fps_ext, auto)
lemma fls_regpart_const [simp]: "fls_regpart (fls_const c) = fps_const c"
by (intro fps_ext) simp
lemma fls_regpart_fls_X [simp]: "fls_regpart fls_X = fps_X"
by (intro fps_ext) simp
lemma fls_regpart_fls_X_inv [simp]: "fls_regpart fls_X_inv = 0"
by (intro fps_ext) simp
lemma fls_regpart_eq0_imp_nonpos_subdegree:
assumes "fls_regpart f = 0"
shows "fls_subdegree f \ 0"
proof (cases "f=0")
case False
have "fls_subdegree f \ 0 \ f $$ fls_subdegree f = 0"
proof-
assume "fls_subdegree f \ 0"
hence "f $$ (fls_subdegree f) = (fls_regpart f) $ (nat (fls_subdegree f))" by simp
with assms show "f $$ (fls_subdegree f) = 0" by simp
qed
with False show ?thesis by fastforce
qed simp
lemma fls_subdegree_lt_fls_regpart_subdegree:
"fls_subdegree f \ int (subdegree (fls_regpart f))"
using fls_subdegree_leI nth_subdegree_nonzero[of "fls_regpart f"]
by (cases "(fls_regpart f) = 0")
(simp_all add: fls_regpart_eq0_imp_nonpos_subdegree)
lemma fls_regpart_subdegree_conv:
assumes "fls_subdegree f \ 0"
shows "subdegree (fls_regpart f) = nat (fls_subdegree f)"
\<comment>\<open>
This is the best we can do since if the subdegree is negative, we might still have the bad luck
that the term at index 0 is equal to 0.
\<close>
proof (cases "f=0")
case False with assms show ?thesis by (intro subdegreeI) simp_all
qed simp
lemma fls_eq_conv_fps_eqI:
assumes "0 \ fls_subdegree f" "0 \ fls_subdegree g" "fls_regpart f = fls_regpart g"
shows "f = g"
proof (rule fls_eq_above_subdegreeI, rule assms(1), rule assms(2), clarify)
fix k::int assume "0 \ k"
with assms(3) show "f $$ k = g $$ k"
using fls_regpart_nth[of f "nat k"] fls_regpart_nth[of g] by simp
qed
lemma fls_regpart_shift_conv_fps_shift:
"m \ 0 \ fls_regpart (fls_shift m f) = fps_shift (nat m) (fls_regpart f)"
by (intro fps_ext) simp_all
lemma fps_shift_fls_regpart_conv_fls_shift:
"fps_shift m (fls_regpart f) = fls_regpart (fls_shift m f)"
by (intro fps_ext) simp_all
lemma fps_unit_factor_fls_regpart:
"fls_subdegree f \ 0 \ unit_factor (fls_regpart f) = fls_regpart (fls_base_factor f)"
by (auto intro: fps_ext simp: fls_regpart_subdegree_conv)
text \<open>
The terms below the zeroth form a polynomial in the inverse of the implied variable,
called the principle part.
\<close>
lift_definition fls_prpart :: "('a::zero) fls \ 'a poly"
is "\f. Abs_poly (\n. if n = 0 then 0 else f (- int n))"
.
lemma fls_prpart_coeff [simp]: "coeff (fls_prpart f) n = (if n = 0 then 0 else f $$ (- int n))"
proof-
have "{x. (if x = 0 then 0 else f $$ - int x) \ 0} \ {x. f $$ - int x \ 0}"
by auto
hence "finite {x. (if x = 0 then 0 else f $$ - int x) \ 0}"
using fls_finite_nonzero_neg_nth[of f] by (simp add: rev_finite_subset)
hence "coeff (fls_prpart f) = (\n. if n = 0 then 0 else f $$ (- int n))"
using Abs_poly_inverse[OF CollectI, OF iffD2, OF eventually_cofinite]
by (simp add: fls_prpart_def)
thus ?thesis by simp
qed
lemma fls_prpart_eq0_iff: "(fls_prpart f = 0) \ (fls_subdegree f \ 0)"
proof
assume 1: "fls_prpart f = 0"
show "fls_subdegree f \ 0"
proof (intro fls_subdegree_ge0I)
fix k::int assume "k < 0"
with 1 show "f $$ k = 0" using fls_prpart_coeff[of f "nat (-k)"] by simp
qed
qed (intro poly_eqI, simp)
lemma fls_prpart0 [simp]: "fls_prpart 0 = 0"
by (simp add: fls_prpart_eq0_iff)
lemma fls_prpart_one [simp]: "fls_prpart 1 = 0"
by (simp add: fls_prpart_eq0_iff)
lemma fls_prpart_delta:
"fls_prpart (Abs_fls (\n. if n=a then b else 0)) =
(if a<0 then Poly (replicate (nat (-a)) 0 @ [b]) else 0)"
by (intro poly_eqI) (auto simp: nth_default_def nth_append)
lemma fls_prpart_const [simp]: "fls_prpart (fls_const c) = 0"
by (simp add: fls_prpart_eq0_iff)
lemma fls_prpart_X [simp]: "fls_prpart fls_X = 0"
by (intro poly_eqI) simp
lemma fls_prpart_X_inv: "fls_prpart fls_X_inv = [:0,1:]"
proof (intro poly_eqI)
fix n show "coeff (fls_prpart fls_X_inv) n = coeff [:0,1:] n"
proof (cases n)
case (Suc i) thus ?thesis by (cases i) simp_all
qed simp
qed
lemma degree_fls_prpart [simp]:
"degree (fls_prpart f) = nat (-fls_subdegree f)"
proof (cases "f=0")
case False show ?thesis unfolding degree_def
proof (intro Least_equality)
fix N assume N: "\i>N. coeff (fls_prpart f) i = 0"
have "\i < -int N. f $$ i = 0"
proof clarify
fix i assume i: "i < -int N"
hence "nat (-i) > N" by simp
with N i show "f $$ i = 0" using fls_prpart_coeff[of f "nat (-i)"] by auto
qed
with False have "fls_subdegree f \ -int N" using fls_subdegree_geI by auto
thus "nat (- fls_subdegree f) \ N" by simp
qed auto
qed simp
lemma fls_prpart_shift:
assumes "m \ 0"
shows "fls_prpart (fls_shift m f) = pCons 0 (poly_shift (Suc (nat (-m))) (fls_prpart f))"
proof (intro poly_eqI)
fix n
define LHS RHS
where "LHS \ fls_prpart (fls_shift m f)"
and "RHS \ pCons 0 (poly_shift (Suc (nat (-m))) (fls_prpart f))"
show "coeff LHS n = coeff RHS n"
proof (cases n)
case (Suc k)
from assms have 1: "-int (Suc k + nat (-m)) = -int (Suc k) + m" by simp
have "coeff RHS n = f $$ (-int (Suc k) + m)"
using arg_cong[OF 1, of "($$) f"] by (simp add: Suc RHS_def coeff_poly_shift)
with Suc show ?thesis by (simp add: LHS_def)
qed (simp add: LHS_def RHS_def)
qed
lemma fls_prpart_base_factor: "fls_prpart (fls_base_factor f) = 0"
using fls_base_factor_subdegree[of f] by (simp add: fls_prpart_eq0_iff)
text \<open>The essential data of a formal Laurant series resides from the subdegree up.\<close>
abbreviation fls_base_factor_to_fps :: "('a::zero) fls \ 'a fps"
where "fls_base_factor_to_fps f \ fls_regpart (fls_base_factor f)"
lemma fls_base_factor_to_fps_conv_fps_shift:
assumes "fls_subdegree f \ 0"
shows "fls_base_factor_to_fps f = fps_shift (nat (fls_subdegree f)) (fls_regpart f)"
by (simp add: assms fls_regpart_shift_conv_fps_shift)
lemma fls_base_factor_to_fps_nth:
"fls_base_factor_to_fps f $ n = f $$ (fls_subdegree f + int n)"
by (simp add: algebra_simps)
lemma fls_base_factor_to_fps_base: "f \ 0 \ fls_base_factor_to_fps f $ 0 \ 0"
by simp
lemma fls_base_factor_to_fps_nonzero: "f \ 0 \ fls_base_factor_to_fps f \ 0"
using fps_nonzeroI[of "fls_base_factor_to_fps f" 0] fls_base_factor_to_fps_base by simp
lemma fls_base_factor_to_fps_subdegree [simp]: "subdegree (fls_base_factor_to_fps f) = 0"
by (cases "f=0") auto
lemma fls_base_factor_to_fps_trivial:
"fls_subdegree f = 0 \ fls_base_factor_to_fps f = fls_regpart f"
by simp
lemma fls_base_factor_to_fps_zero: "fls_base_factor_to_fps 0 = 0"
by simp
lemma fls_base_factor_to_fps_one: "fls_base_factor_to_fps 1 = 1"
by simp
lemma fls_base_factor_to_fps_delta:
"fls_base_factor_to_fps (Abs_fls (\n. if n=a then c else 0)) = fps_const c"
using fls_base_factor_delta[of a c] by simp
lemma fls_base_factor_to_fps_const:
"fls_base_factor_to_fps (fls_const c) = fps_const c"
by simp
lemma fls_base_factor_to_fps_X:
"fls_base_factor_to_fps (fls_X::'a::{zero_neq_one} fls) = 1"
by simp
lemma fls_base_factor_to_fps_X_inv:
"fls_base_factor_to_fps (fls_X_inv::'a::{zero_neq_one} fls) = 1"
by simp
lemma fls_base_factor_to_fps_shift:
"fls_base_factor_to_fps (fls_shift m f) = fls_base_factor_to_fps f"
using fls_base_factor_shift[of m f] by simp
lemma fls_base_factor_to_fps_base_factor:
"fls_base_factor_to_fps (fls_base_factor f) = fls_base_factor_to_fps f"
using fls_base_factor_to_fps_shift by simp
lemma fps_unit_factor_fls_base_factor:
"unit_factor (fls_base_factor_to_fps f) = fls_base_factor_to_fps f"
using fls_base_factor_to_fps_subdegree[of f] by simp
subsubsection \<open>Converting power to Laurent series\<close>
text \<open>We can extend a power series by 0s below to create a Laurent series.\<close>
definition fps_to_fls :: "('a::zero) fps \ 'a fls"
where "fps_to_fls f \ Abs_fls (\k::int. if k<0 then 0 else f $ (nat k))"
lemma fps_to_fls_nth [simp]:
"(fps_to_fls f) $$ n = (if n < 0 then 0 else f$(nat n))"
using nth_Abs_fls_lower_bound[of 0 "(\k::int. if k<0 then 0 else f $ (nat k))"]
unfolding fps_to_fls_def
by simp
lemma fps_to_fls_eq_imp_fps_eq:
assumes "fps_to_fls f = fps_to_fls g"
shows "f = g"
proof (intro fps_ext)
fix n
have "f $ n = fps_to_fls g $$ int n" by (simp add: assms[symmetric])
thus "f $ n = g $ n" by simp
qed
lemma fps_zero_to_fls [simp]: "fps_to_fls 0 = 0"
by (intro fls_zero_eqI) simp
lemma fps_to_fls_nonzeroI: "f \ 0 \ fps_to_fls f \ 0"
using fps_to_fls_eq_imp_fps_eq[of f 0] by auto
lemma fps_one_to_fls [simp]: "fps_to_fls 1 = 1"
by (intro fls_eqI) simp
lemma fps_to_fls_Abs_fps:
"fps_to_fls (Abs_fps F) = Abs_fls (\n. if n<0 then 0 else F (nat n))"
using nth_Abs_fls_lower_bound[of 0 "(\n::int. if n<0 then 0 else F (nat n))"]
by (intro fls_eqI) simp
lemma fps_delta_to_fls:
"fps_to_fls (Abs_fps (\n. if n=a then b else 0)) = Abs_fls (\n. if n=int a then b else 0)"
using fls_eqI[of _ "Abs_fls (\n. if n=int a then b else 0)"] by force
lemma fps_const_to_fls [simp]: "fps_to_fls (fps_const c) = fls_const c"
by (intro fls_eqI) simp
lemma fps_X_to_fls [simp]: "fps_to_fls fps_X = fls_X"
by (fastforce intro: fls_eqI)
lemma fps_to_fls_eq_zero_iff: "(fps_to_fls f = 0) \ (f=0)"
using fps_to_fls_nonzeroI by auto
lemma fls_subdegree_fls_to_fps_gt0: "fls_subdegree (fps_to_fls f) \ 0"
proof (cases "f=0")
case False show ?thesis
proof (rule fls_subdegree_geI, rule fls_nonzeroI)
from False show "fps_to_fls f $$ int (subdegree f) \ 0"
by simp
qed simp
qed simp
lemma fls_subdegree_fls_to_fps: "fls_subdegree (fps_to_fls f) = int (subdegree f)"
proof (cases "f=0")
case False
have "subdegree f = nat (fls_subdegree (fps_to_fls f))"
proof (rule subdegreeI)
from False show "f $ (nat (fls_subdegree (fps_to_fls f))) \ 0"
using fls_subdegree_fls_to_fps_gt0[of f] nth_fls_subdegree_nonzero[of "fps_to_fls f"]
fps_to_fls_nonzeroI[of f]
by simp
next
fix k assume k: "k < nat (fls_subdegree (fps_to_fls f))"
thus "f $ k = 0"
using fls_eq0_below_subdegree[of "int k" "fps_to_fls f"] by simp
qed
thus ?thesis by (simp add: fls_subdegree_fls_to_fps_gt0)
qed simp
lemma fps_shift_to_fls [simp]:
"n \ subdegree f \ fps_to_fls (fps_shift n f) = fls_shift (int n) (fps_to_fls f)"
by (auto intro: fls_eqI simp: nat_add_distrib nth_less_subdegree_zero)
lemma fls_base_factor_fps_to_fls: "fls_base_factor (fps_to_fls f) = fps_to_fls (unit_factor f)"
using nth_less_subdegree_zero[of _ f]
by (auto intro: fls_eqI simp: fls_subdegree_fls_to_fps nat_add_distrib)
lemma fls_regpart_to_fls_trivial [simp]:
"fls_subdegree f \ 0 \ fps_to_fls (fls_regpart f) = f"
by (intro fls_eqI) simp
lemma fls_regpart_fps_trivial [simp]: "fls_regpart (fps_to_fls f) = f"
by (intro fps_ext) simp
lemma fps_to_fls_base_factor_to_fps:
"fps_to_fls (fls_base_factor_to_fps f) = fls_base_factor f"
by (intro fls_eqI) simp
lemma fls_conv_base_factor_to_fps_shift_subdegree:
"f = fls_shift (-fls_subdegree f) (fps_to_fls (fls_base_factor_to_fps f))"
using fps_to_fls_base_factor_to_fps[of f] fps_to_fls_base_factor_to_fps[of f] by simp
lemma fls_base_factor_to_fps_to_fls:
"fls_base_factor_to_fps (fps_to_fls f) = unit_factor f"
using fls_base_factor_fps_to_fls[of f] fls_regpart_fps_trivial[of "unit_factor f"]
by simp
abbreviation
"fls_regpart_as_fls f \ fps_to_fls (fls_regpart f)"
abbreviation
"fls_prpart_as_fls f \
fls_shift (-fls_subdegree f) (fps_to_fls (fps_of_poly (reflect_poly (fls_prpart f))))"
lemma fls_regpart_as_fls_nth:
"fls_regpart_as_fls f $$ n = (if n < 0 then 0 else f $$ n)"
by simp
lemma fls_regpart_idem:
"fls_regpart (fls_regpart_as_fls f) = fls_regpart f"
by simp
lemma fls_prpart_as_fls_nth:
"fls_prpart_as_fls f $$ n = (if n < 0 then f $$ n else 0)"
proof (cases "n < fls_subdegree f" "n < 0" rule: case_split[case_product case_split])
case False_True
hence "nat (-fls_subdegree f) - nat (n - fls_subdegree f) = nat (-n)" by auto
with False_True show ?thesis
using coeff_reflect_poly[of "fls_prpart f" "nat (n - fls_subdegree f)"] by auto
next
case False_False thus ?thesis
using coeff_reflect_poly[of "fls_prpart f" "nat (n - fls_subdegree f)"] by auto
qed simp_all
lemma fls_prpart_idem [simp]: "fls_prpart (fls_prpart_as_fls f) = fls_prpart f"
using fls_prpart_as_fls_nth[of f] by (intro poly_eqI) simp
lemma fls_regpart_prpart: "fls_regpart (fls_prpart_as_fls f) = 0"
using fls_prpart_as_fls_nth[of f] by (intro fps_ext) simp
lemma fls_prpart_regpart: "fls_prpart (fls_regpart_as_fls f) = 0"
by (intro poly_eqI) simp
subsection \<open>Algebraic structures\<close>
subsubsection \<open>Addition\<close>
instantiation fls :: (monoid_add) plus
begin
lift_definition plus_fls :: "'a fls \ 'a fls \ 'a fls" is "\f g n. f n + g n"
proof-
fix f f' :: "int \ 'a"
assume "\\<^sub>\n. f (- int n) = 0" "\\<^sub>\n. f' (- int n) = 0"
from this obtain N N' where "\n>N. f (-int n) = 0" "\n>N'. f' (-int n) = 0"
by (auto simp: MOST_nat)
hence "\n > max N N'. f (-int n) + f' (-int n) = 0" by auto
hence "\K. \n>K. f (-int n) + f' (-int n) = 0" by fast
thus "\\<^sub>\n. f (- int n) + f' (-int n) = 0" by (simp add: MOST_nat)
qed
instance ..
end
lemma fls_plus_nth [simp]: "(f + g) $$ n = f $$ n + g $$ n"
by transfer simp
lemma fls_plus_const: "fls_const x + fls_const y = fls_const (x+y)"
by (intro fls_eqI) simp
lemma fls_plus_subdegree:
"f + g \ 0 \ fls_subdegree (f + g) \ min (fls_subdegree f) (fls_subdegree g)"
by (auto intro: fls_subdegree_geI)
lemma fls_shift_plus [simp]:
"fls_shift m (f + g) = (fls_shift m f) + (fls_shift m g)"
by (intro fls_eqI) simp
lemma fls_regpart_plus [simp]: "fls_regpart (f + g) = fls_regpart f + fls_regpart g"
by (intro fps_ext) simp
lemma fls_prpart_plus [simp] : "fls_prpart (f + g) = fls_prpart f + fls_prpart g"
by (intro poly_eqI) simp
lemma fls_decompose_reg_pr_parts:
fixes f :: "'a :: monoid_add fls"
defines "R \ fls_regpart_as_fls f"
and "P \ fls_prpart_as_fls f"
shows "f = P + R"
and "f = R + P"
using fls_prpart_as_fls_nth[of f]
by (auto intro: fls_eqI simp add: assms)
lemma fps_to_fls_plus [simp]: "fps_to_fls (f + g) = fps_to_fls f + fps_to_fls g"
by (intro fls_eqI) simp
instance fls :: (monoid_add) monoid_add
proof
fix a b c :: "'a fls"
show "a + b + c = a + (b + c)" by transfer (simp add: add.assoc)
show "0 + a = a" by transfer simp
show "a + 0 = a" by transfer simp
qed
instance fls :: (comm_monoid_add) comm_monoid_add
by (standard, transfer, auto simp: add.commute)
subsubsection \<open>Subtraction and negatives\<close>
instantiation fls :: (group_add) minus
begin
lift_definition minus_fls :: "'a fls \ 'a fls \ 'a fls" is "\f g n. f n - g n"
proof-
fix f f' :: "int \ 'a"
assume "\\<^sub>\n. f (- int n) = 0" "\\<^sub>\n. f' (- int n) = 0"
from this obtain N N' where "\n>N. f (-int n) = 0" "\n>N'. f' (-int n) = 0"
by (auto simp: MOST_nat)
hence "\n > max N N'. f (-int n) - f' (-int n) = 0" by auto
hence "\K. \n>K. f (-int n) - f' (-int n) = 0" by fast
thus "\\<^sub>\n. f (- int n) - f' (-int n) = 0" by (simp add: MOST_nat)
qed
instance ..
end
lemma fls_minus_nth [simp]: "(f - g) $$ n = f $$ n - g $$ n"
by transfer simp
lemma fls_minus_const: "fls_const x - fls_const y = fls_const (x-y)"
by (intro fls_eqI) simp
lemma fls_subdegree_minus:
"f - g \ 0 \ fls_subdegree (f - g) \ min (fls_subdegree f) (fls_subdegree g)"
by (intro fls_subdegree_geI) simp_all
lemma fls_shift_minus [simp]: "fls_shift m (f - g) = (fls_shift m f) - (fls_shift m g)"
by (auto intro: fls_eqI)
lemma fls_regpart_minus [simp]: "fls_regpart (f - g) = fls_regpart f - fls_regpart g"
by (intro fps_ext) simp
lemma fls_prpart_minus [simp] : "fls_prpart (f - g) = fls_prpart f - fls_prpart g"
by (intro poly_eqI) simp
lemma fps_to_fls_minus [simp]: "fps_to_fls (f - g) = fps_to_fls f - fps_to_fls g"
by (intro fls_eqI) simp
instantiation fls :: (group_add) uminus
begin
lift_definition uminus_fls :: "'a fls \ 'a fls" is "\f n. - f n"
proof-
fix f :: "int \ 'a" assume "\\<^sub>\n. f (- int n) = 0"
from this obtain N where "\n>N. f (-int n) = 0"
by (auto simp: MOST_nat)
hence "\n>N. - f (-int n) = 0" by auto
hence "\K. \n>K. - f (-int n) = 0" by fast
thus "\\<^sub>\n. - f (- int n) = 0" by (simp add: MOST_nat)
qed
instance ..
end
lemma fls_uminus_nth [simp]: "(-f) $$ n = - (f $$ n)"
by transfer simp
lemma fls_const_uminus[simp]: "fls_const (-x) = -fls_const x"
by (intro fls_eqI) simp
lemma fls_shift_uminus [simp]: "fls_shift m (- f) = - (fls_shift m f)"
by (auto intro: fls_eqI)
lemma fls_regpart_uminus [simp]: "fls_regpart (- f) = - fls_regpart f"
by (intro fps_ext) simp
lemma fls_prpart_uminus [simp] : "fls_prpart (- f) = - fls_prpart f"
by (intro poly_eqI) simp
lemma fps_to_fls_uminus [simp]: "fps_to_fls (- f) = - fps_to_fls f"
by (intro fls_eqI) simp
instance fls :: (group_add) group_add
proof
fix a b :: "'a fls"
show "- a + a = 0" by transfer simp
show "a + - b = a - b" by transfer simp
qed
instance fls :: (ab_group_add) ab_group_add
proof
fix a b :: "'a fls"
show "- a + a = 0" by transfer simp
show "a - b = a + - b" by transfer simp
qed
lemma fls_uminus_subdegree [simp]: "fls_subdegree (-f) = fls_subdegree f"
by (cases "f=0") (auto intro: fls_subdegree_eqI)
lemma fls_subdegree_minus_sym: "fls_subdegree (g - f) = fls_subdegree (f - g)"
using fls_uminus_subdegree[of "g-f"] by (simp add: algebra_simps)
lemma fls_regpart_sub_prpart: "fls_regpart (f - fls_prpart_as_fls f) = fls_regpart f"
using fls_decompose_reg_pr_parts(2)[of f]
add_diff_cancel[of "fls_regpart_as_fls f" "fls_prpart_as_fls f"]
by simp
lemma fls_prpart_sub_regpart: "fls_prpart (f - fls_regpart_as_fls f) = fls_prpart f"
using fls_decompose_reg_pr_parts(1)[of f]
add_diff_cancel[of "fls_prpart_as_fls f" "fls_regpart_as_fls f"]
by simp
subsubsection \<open>Multiplication\<close>
instantiation fls :: ("{comm_monoid_add, times}") times
begin
definition fls_times_def:
"(*) = (\f g.
fls_shift
(- (fls_subdegree f + fls_subdegree g))
(fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))
)"
instance ..
end
lemma fls_times_nth_eq0: "n < fls_subdegree f + fls_subdegree g \ (f * g) $$ n = 0"
by (simp add: fls_times_def)
lemma fls_times_nth:
fixes f df g dg
defines "df \ fls_subdegree f" and "dg \ fls_subdegree g"
shows "(f * g) $$ n = (\i=df + dg..n. f $$ (i - dg) * g $$ (dg + n - i))"
and "(f * g) $$ n = (\i=df..n - dg. f $$ i * g $$ (n - i))"
and "(f * g) $$ n = (\i=dg..n - df. f $$ (df + i - dg) * g $$ (dg + n - df - i))"
and "(f * g) $$ n = (\i=0..n - (df + dg). f $$ (df + i) * g $$ (n - df - i))"
proof-
define dfg where "dfg \ df + dg"
show 4: "(f * g) $$ n = (\i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))"
proof (cases "n < dfg")
case False
from False assms have
"(f * g) $$ n =
(\<Sum>i = 0..nat (n - dfg). f $$ (df + int i) * g $$ (dg + int (nat (n - dfg) - i)))"
using fps_mult_nth[of "fls_base_factor_to_fps f" "fls_base_factor_to_fps g"]
fls_base_factor_to_fps_nth[of f]
fls_base_factor_to_fps_nth[of g]
by (simp add: dfg_def fls_times_def algebra_simps)
moreover from False have index:
"\i. i \ {0..nat (n - dfg)} \ dg + int (nat (n - dfg) - i) = n - df - int i"
by (auto simp: dfg_def)
ultimately have
"(f * g) $$ n = (\i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i))"
by simp
moreover have
"(\i=0..nat (n - dfg). f $$ (df + int i) * g $$ (n - df - int i)) =
(\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))"
proof (intro sum.reindex_cong)
show "inj_on nat {0..n - dfg}" by standard auto
show "{0..nat (n - dfg)} = nat ` {0..n - dfg}"
proof
show "{0..nat (n - dfg)} \ nat ` {0..n - dfg}"
proof
fix i assume "i \ {0..nat (n - dfg)}"
hence i: "i \ 0" "i \ nat (n - dfg)" by auto
with False have "int i \ 0" "int i \ n - dfg" by auto
hence "int i \ {0..n - dfg}" by simp
moreover from i(1) have "i = nat (int i)" by simp
ultimately show "i \ nat ` {0..n - dfg}" by fast
qed
qed (auto simp: False)
qed (simp add: False)
ultimately show "(f * g) $$ n = (\i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))"
by simp
qed (simp add: fls_times_nth_eq0 assms dfg_def)
have
"(\i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i)) =
(\<Sum>i=0..n - dfg. f $$ (df + i) * g $$ (n - df - i))"
proof (intro sum.reindex_cong)
define T where "T \ \i. i + dfg"
show "inj_on T {0..n - dfg}" by standard (simp add: T_def)
qed (simp_all add: dfg_def algebra_simps)
with 4 show 1: "(f * g) $$ n = (\i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i))"
by simp
have
"(\i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i)) = (\i=df..n - dg. f $$ i * g $$ (n - i))"
proof (intro sum.reindex_cong)
define T where "T \ \i. i + dg"
show "inj_on T {df..n - dg}" by standard (simp add: T_def)
qed (auto simp: dfg_def)
with 1 show "(f * g) $$ n = (\i=df..n - dg. f $$ i * g $$ (n - i))"
by simp
have
"(\i=dfg..n. f $$ (i - dg) * g $$ (dg + n - i)) =
(\<Sum>i=dg..n - df. f $$ (df + i - dg) * g $$ (dg + n - df - i))"
proof (intro sum.reindex_cong)
define T where "T \ \i. i + df"
show "inj_on T {dg..n - df}" by standard (simp add: T_def)
qed (simp_all add: dfg_def algebra_simps)
with 1 show "(f * g) $$ n = (\i=dg..n - df. f $$ (df + i - dg) * g $$ (dg + n - df - i))"
by simp
qed
lemma fls_times_base [simp]:
"(f * g) $$ (fls_subdegree f + fls_subdegree g) =
(f $$ fls_subdegree f) * (g $$ fls_subdegree g)"
by (simp add: fls_times_nth(1))
instance fls :: ("{comm_monoid_add, mult_zero}") mult_zero
proof
fix a :: "'a fls"
have
"(0::'a fls) * a =
fls_shift (fls_subdegree a) (fps_to_fls ( (0::'a fps)*(fls_base_factor_to_fps a) ))"
by (simp add: fls_times_def)
moreover have
"a * (0::'a fls) =
fls_shift (fls_subdegree a) (fps_to_fls ( (fls_base_factor_to_fps a)*(0::'a fps) ))"
by (simp add: fls_times_def)
ultimately show "0 * a = (0::'a fls)" "a * 0 = (0::'a fls)"
by auto
qed
lemma fls_mult_one:
fixes f :: "'a::{comm_monoid_add, mult_zero, monoid_mult} fls"
shows "1 * f = f"
and "f * 1 = f"
using fls_conv_base_factor_to_fps_shift_subdegree[of f]
by (simp_all add: fls_times_def fps_one_mult)
lemma fls_mult_const_nth [simp]:
fixes f :: "'a::{comm_monoid_add, mult_zero} fls"
shows "(fls_const x * f) $$ n = x * f$$n"
and "(f * fls_const x ) $$ n = f$$n * x"
proof-
show "(fls_const x * f) $$ n = x * f$$n"
proof (cases "n)
case False
hence "{fls_subdegree f..n} = insert (fls_subdegree f) {fls_subdegree f+1..n}" by auto
thus ?thesis by (simp add: fls_times_nth(1))
qed (simp add: fls_times_nth_eq0)
show "(f * fls_const x ) $$ n = f$$n * x"
proof (cases "n)
case False
hence "{fls_subdegree f..n} = insert n {fls_subdegree f..n-1}" by auto
thus ?thesis by (simp add: fls_times_nth(1))
qed (simp add: fls_times_nth_eq0)
qed
lemma fls_const_mult_const[simp]:
fixes x y :: "'a::{comm_monoid_add, mult_zero}"
shows "fls_const x * fls_const y = fls_const (x*y)"
by (intro fls_eqI) simp
lemma fls_mult_subdegree_ge:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "f*g \ 0"
shows "fls_subdegree (f*g) \ fls_subdegree f + fls_subdegree g"
by (auto intro: fls_subdegree_geI simp: assms fls_times_nth_eq0)
lemma fls_mult_subdegree_ge_0:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0"
shows "fls_subdegree (f*g) \ 0"
using assms fls_mult_subdegree_ge[of f g]
by fastforce
lemma fls_mult_nonzero_base_subdegree_eq:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "f $$ (fls_subdegree f) * g $$ (fls_subdegree g) \ 0"
shows "fls_subdegree (f*g) = fls_subdegree f + fls_subdegree g"
proof-
from assms have "fls_subdegree (f*g) \ fls_subdegree f + fls_subdegree g"
using fls_nonzeroI[of "f*g" "fls_subdegree f + fls_subdegree g"]
fls_mult_subdegree_ge[of f g]
by simp
moreover from assms have "fls_subdegree (f*g) \ fls_subdegree f + fls_subdegree g"
by (intro fls_subdegree_leI) simp
ultimately show ?thesis by simp
qed
lemma fls_subdegree_mult [simp]:
fixes f g :: "'a::semiring_no_zero_divisors fls"
assumes "f \ 0" "g \ 0"
shows "fls_subdegree (f * g) = fls_subdegree f + fls_subdegree g"
using assms
by (auto intro: fls_subdegree_eqI simp: fls_times_nth_eq0)
lemma fls_shifted_times_simps:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "f * (fls_shift n g) = fls_shift n (f*g)" "(fls_shift n f) * g = fls_shift n (f*g)"
proof-
show "f * (fls_shift n g) = fls_shift n (f*g)"
proof (cases "g=0")
case False
hence
"f * (fls_shift n g) =
fls_shift (- (fls_subdegree f + (fls_subdegree g - n)))
(fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))"
unfolding fls_times_def by (simp add: fls_base_factor_to_fps_shift)
thus "f * (fls_shift n g) = fls_shift n (f*g)"
by (simp add: algebra_simps fls_times_def)
qed auto
show "(fls_shift n f)*g = fls_shift n (f*g)"
proof (cases "f=0")
case False
hence
"(fls_shift n f)*g =
fls_shift (- ((fls_subdegree f - n) + fls_subdegree g))
(fps_to_fls (fls_base_factor_to_fps f * fls_base_factor_to_fps g))"
unfolding fls_times_def by (simp add: fls_base_factor_to_fps_shift)
thus "(fls_shift n f) * g = fls_shift n (f*g)"
by (simp add: algebra_simps fls_times_def)
qed auto
qed
lemma fls_shifted_times_transfer:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "fls_shift n f * g = f * fls_shift n g"
using fls_shifted_times_simps(1)[of f n g] fls_shifted_times_simps(2)[of n f g]
by simp
lemma fls_times_both_shifted_simp:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "(fls_shift m f) * (fls_shift n g) = fls_shift (m+n) (f*g)"
by (simp add: fls_shifted_times_simps)
lemma fls_base_factor_mult_base_factor:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows "fls_base_factor (f * fls_base_factor g) = fls_base_factor (f * g)"
and "fls_base_factor (fls_base_factor f * g) = fls_base_factor (f * g)"
using fls_base_factor_shift[of "fls_subdegree g" "f*g"]
fls_base_factor_shift[of "fls_subdegree f" "f*g"]
by (simp_all add: fls_shifted_times_simps)
lemma fls_base_factor_mult_both_base_factor:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
shows "fls_base_factor (fls_base_factor f * fls_base_factor g) = fls_base_factor (f * g)"
using fls_base_factor_mult_base_factor(1)[of "fls_base_factor f" g]
fls_base_factor_mult_base_factor(2)[of f g]
by simp
lemma fls_base_factor_mult:
fixes f g :: "'a::semiring_no_zero_divisors fls"
shows "fls_base_factor (f * g) = fls_base_factor f * fls_base_factor g"
by (cases "f\0 \ g\0")
(auto simp: fls_times_both_shifted_simp)
lemma fls_times_conv_base_factor_times:
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows
"f * g =
fls_shift (-(fls_subdegree f + fls_subdegree g)) (fls_base_factor f * fls_base_factor g)"
by (simp add: fls_times_both_shifted_simp)
lemma fls_times_base_factor_conv_shifted_times:
\<comment> \<open>Convenience form of lemma @{text "fls_times_both_shifted_simp"}.\<close>
fixes f g :: "'a::{comm_monoid_add, mult_zero} fls"
shows
"fls_base_factor f * fls_base_factor g = fls_shift (fls_subdegree f + fls_subdegree g) (f * g)"
by (simp add: fls_times_both_shifted_simp)
lemma fls_times_conv_regpart:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0"
shows "fls_regpart (f * g) = fls_regpart f * fls_regpart g"
proof-
from assms have 1:
"f * g =
fls_shift (- (fls_subdegree f + fls_subdegree g)) (
fps_to_fls (
fps_shift (nat (fls_subdegree f) + nat (fls_subdegree g)) (
fls_regpart f * fls_regpart g
)
)
)"
by (simp add:
fls_times_def fls_base_factor_to_fps_conv_fps_shift[symmetric]
fls_regpart_subdegree_conv fps_shift_mult_both[symmetric]
)
show ?thesis
proof (cases "fls_regpart f * fls_regpart g = 0")
case False
with assms have
"subdegree (fls_regpart f * fls_regpart g) \
nat (fls_subdegree f) + nat (fls_subdegree g)"
by (simp add: fps_mult_subdegree_ge fls_regpart_subdegree_conv[symmetric])
with 1 assms show ?thesis by simp
qed (simp add: 1)
qed
lemma fls_base_factor_to_fps_mult_conv_unit_factor:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
shows
"fls_base_factor_to_fps (f * g) =
unit_factor (fls_base_factor_to_fps f * fls_base_factor_to_fps g)"
using fls_base_factor_mult_both_base_factor[of f g]
fps_unit_factor_fls_regpart[of "fls_base_factor f * fls_base_factor g"]
fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g]
fls_mult_subdegree_ge_0[of "fls_base_factor f" "fls_base_factor g"]
fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"]
by simp
lemma fls_base_factor_to_fps_mult':
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "(f $$ fls_subdegree f) * (g $$ fls_subdegree g) \ 0"
shows "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g"
using assms fls_mult_nonzero_base_subdegree_eq[of f g]
fls_times_base_factor_conv_shifted_times[of f g]
fls_times_conv_regpart[of "fls_base_factor f" "fls_base_factor g"]
fls_base_factor_subdegree[of f] fls_base_factor_subdegree[of g]
by fastforce
lemma fls_base_factor_to_fps_mult:
fixes f g :: "'a::semiring_no_zero_divisors fls"
shows "fls_base_factor_to_fps (f * g) = fls_base_factor_to_fps f * fls_base_factor_to_fps g"
using fls_base_factor_to_fps_mult'[of f g]
by (cases "f=0 \ g=0") auto
lemma fls_times_conv_fps_times:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0"
shows "f * g = fps_to_fls (fls_regpart f * fls_regpart g)"
using assms fls_mult_subdegree_ge[of f g]
by (cases "f * g = 0") (simp_all add: fls_times_conv_regpart[symmetric])
lemma fps_times_conv_fls_times:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
shows "f * g = fls_regpart (fps_to_fls f * fps_to_fls g)"
using fls_subdegree_fls_to_fps_gt0 fls_times_conv_regpart[symmetric]
by fastforce
lemma fls_times_fps_to_fls:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fps"
shows "fps_to_fls (f * g) = fps_to_fls f * fps_to_fls g"
proof (intro fls_eq_conv_fps_eqI, rule fls_subdegree_fls_to_fps_gt0)
show "fls_subdegree (fps_to_fls f * fps_to_fls g) \ 0"
proof (cases "fps_to_fls f * fps_to_fls g = 0")
case False thus ?thesis
using fls_mult_subdegree_ge fls_subdegree_fls_to_fps_gt0[of f]
fls_subdegree_fls_to_fps_gt0[of g]
by fastforce
qed simp
qed (simp add: fps_times_conv_fls_times)
lemma fls_X_times_conv_shift:
fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
shows "fls_X * f = fls_shift (-1) f" "f * fls_X = fls_shift (-1) f"
by (simp_all add: fls_X_conv_shift_1 fls_mult_one fls_shifted_times_simps)
lemmas fls_X_times_comm = trans_sym[OF fls_X_times_conv_shift]
lemma fls_subdegree_mult_fls_X:
fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
assumes "f \ 0"
shows "fls_subdegree (fls_X * f) = fls_subdegree f + 1"
and "fls_subdegree (f * fls_X) = fls_subdegree f + 1"
by (auto simp: fls_X_times_conv_shift assms)
lemma fls_mult_fls_X_nonzero:
fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
assumes "f \ 0"
shows "fls_X * f \ 0"
and "f * fls_X \ 0"
by (auto simp: fls_X_times_conv_shift fls_shift_eq0_iff assms)
lemma fls_base_factor_mult_fls_X:
fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fls"
shows "fls_base_factor (fls_X * f) = fls_base_factor f"
and "fls_base_factor (f * fls_X) = fls_base_factor f"
using fls_base_factor_shift[of "-1" f]
by (auto simp: fls_X_times_conv_shift)
lemma fls_X_inv_times_conv_shift:
fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
shows "fls_X_inv * f = fls_shift 1 f" "f * fls_X_inv = fls_shift 1 f"
by (simp_all add: fls_X_inv_conv_shift_1 fls_mult_one fls_shifted_times_simps)
lemmas fls_X_inv_times_comm = trans_sym[OF fls_X_inv_times_conv_shift]
lemma fls_subdegree_mult_fls_X_inv:
fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
assumes "f \ 0"
shows "fls_subdegree (fls_X_inv * f) = fls_subdegree f - 1"
and "fls_subdegree (f * fls_X_inv) = fls_subdegree f - 1"
by (auto simp: fls_X_inv_times_conv_shift assms)
lemma fls_mult_fls_X_inv_nonzero:
fixes f :: "'a::{comm_monoid_add,mult_zero,monoid_mult} fls"
assumes "f \ 0"
shows "fls_X_inv * f \ 0"
and "f * fls_X_inv \ 0"
by (auto simp: fls_X_inv_times_conv_shift fls_shift_eq0_iff assms)
lemma fls_base_factor_mult_fls_X_inv:
fixes f :: "'a::{comm_monoid_add,monoid_mult,mult_zero} fls"
shows "fls_base_factor (fls_X_inv * f) = fls_base_factor f"
and "fls_base_factor (f * fls_X_inv) = fls_base_factor f"
using fls_base_factor_shift[of 1 f]
by (auto simp: fls_X_inv_times_conv_shift)
lemma fls_mult_assoc_subdegree_ge_0:
fixes f g h :: "'a::semiring_0 fls"
assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0" "fls_subdegree h \ 0"
shows "f * g * h = f * (g * h)"
using assms
by (simp add: fls_times_conv_fps_times fls_subdegree_fls_to_fps_gt0 mult.assoc)
lemma fls_mult_assoc_base_factor:
fixes a b c :: "'a::semiring_0 fls"
shows
"fls_base_factor a * fls_base_factor b * fls_base_factor c =
fls_base_factor a * (fls_base_factor b * fls_base_factor c)"
by (simp add: fls_mult_assoc_subdegree_ge_0 del: fls_base_factor_def)
lemma fls_mult_distrib_subdegree_ge_0:
fixes f g h :: "'a::semiring_0 fls"
assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0" "fls_subdegree h \ 0"
shows "(f + g) * h = f * h + g * h"
and "h * (f + g) = h * f + h * g"
proof-
have "fls_subdegree (f+g) \ 0"
proof (cases "f+g = 0")
case False
with assms(1,2) show ?thesis
using fls_plus_subdegree by fastforce
qed simp
with assms show "(f + g) * h = f * h + g * h" "h * (f + g) = h * f + h * g"
using distrib_right[of "fls_regpart f"] distrib_left[of "fls_regpart h"]
by (simp_all add: fls_times_conv_fps_times)
qed
lemma fls_mult_distrib_base_factor:
fixes a b c :: "'a::semiring_0 fls"
shows
"fls_base_factor a * (fls_base_factor b + fls_base_factor c) =
fls_base_factor a * fls_base_factor b + fls_base_factor a * fls_base_factor c"
by (simp add: fls_mult_distrib_subdegree_ge_0 del: fls_base_factor_def)
instance fls :: (semiring_0) semiring_0
proof
fix a b c :: "'a fls"
have
"a * b * c =
fls_shift (- (fls_subdegree a + fls_subdegree b + fls_subdegree c))
(fls_base_factor a * fls_base_factor b * fls_base_factor c)"
by (simp add: fls_times_both_shifted_simp)
moreover have
"a * (b * c) =
fls_shift (- (fls_subdegree a + fls_subdegree b + fls_subdegree c))
(fls_base_factor a * fls_base_factor b * fls_base_factor c)"
using fls_mult_assoc_base_factor[of a b c] by (simp add: fls_times_both_shifted_simp)
ultimately show "a * b * c = a * (b * c)" by simp
have ab:
"fls_subdegree (fls_shift (min (fls_subdegree a) (fls_subdegree b)) a) \ 0"
"fls_subdegree (fls_shift (min (fls_subdegree a) (fls_subdegree b)) b) \ 0"
by (simp_all add: fls_shift_nonneg_subdegree)
have
"(a + b) * c =
fls_shift (- (min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c)) (
(
fls_shift (min (fls_subdegree a) (fls_subdegree b)) a +
fls_shift (min (fls_subdegree a) (fls_subdegree b)) b
) * fls_base_factor c)"
using fls_times_both_shifted_simp[of
"-min (fls_subdegree a) (fls_subdegree b)"
"fls_shift (min (fls_subdegree a) (fls_subdegree b)) a +
fls_shift (min (fls_subdegree a) (fls_subdegree b)) b"
"-fls_subdegree c" "fls_base_factor c"
]
by simp
also have
"\ =
fls_shift (-(min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c))
(fls_shift (min (fls_subdegree a) (fls_subdegree b)) a * fls_base_factor c)
+
fls_shift (-(min (fls_subdegree a) (fls_subdegree b) + fls_subdegree c))
(fls_shift (min (fls_subdegree a) (fls_subdegree b)) b * fls_base_factor c)"
using ab
by (simp add: fls_mult_distrib_subdegree_ge_0(1) del: fls_base_factor_def)
finally show "(a + b) * c = a * c + b * c" by (simp add: fls_times_both_shifted_simp)
have bc:
"fls_subdegree (fls_shift (min (fls_subdegree b) (fls_subdegree c)) b) \ 0"
"fls_subdegree (fls_shift (min (fls_subdegree b) (fls_subdegree c)) c) \ 0"
by (simp_all add: fls_shift_nonneg_subdegree)
have
"a * (b + c) =
fls_shift (- (fls_subdegree a + min (fls_subdegree b) (fls_subdegree c))) (
fls_base_factor a * (
fls_shift (min (fls_subdegree b) (fls_subdegree c)) b +
fls_shift (min (fls_subdegree b) (fls_subdegree c)) c
)
)
"
using fls_times_both_shifted_simp[of
"-fls_subdegree a" "fls_base_factor a"
"-min (fls_subdegree b) (fls_subdegree c)"
"fls_shift (min (fls_subdegree b) (fls_subdegree c)) b +
fls_shift (min (fls_subdegree b) (fls_subdegree c)) c"
]
by simp
also have
"\ =
fls_shift (-(fls_subdegree a + min (fls_subdegree b) (fls_subdegree c)))
(fls_base_factor a * fls_shift (min (fls_subdegree b) (fls_subdegree c)) b)
+
fls_shift (-(fls_subdegree a + min (fls_subdegree b) (fls_subdegree c)))
(fls_base_factor a * fls_shift (min (fls_subdegree b) (fls_subdegree c)) c)
"
using bc
by (simp add: fls_mult_distrib_subdegree_ge_0(2) del: fls_base_factor_def)
finally show "a * (b + c) = a * b + a * c" by (simp add: fls_times_both_shifted_simp)
qed
lemma fls_mult_commute_subdegree_ge_0:
fixes f g :: "'a::comm_semiring_0 fls"
assumes "fls_subdegree f \ 0" "fls_subdegree g \ 0"
shows "f * g = g * f"
using assms
by (simp add: fls_times_conv_fps_times mult.commute)
lemma fls_mult_commute_base_factor:
fixes a b c :: "'a::comm_semiring_0 fls"
shows "fls_base_factor a * fls_base_factor b = fls_base_factor b * fls_base_factor a"
by (simp add: fls_mult_commute_subdegree_ge_0 del: fls_base_factor_def)
instance fls :: (comm_semiring_0) comm_semiring_0
proof
fix a b c :: "'a fls"
show "a * b = b * a"
using fls_times_conv_base_factor_times[of a b] fls_times_conv_base_factor_times[of b a]
fls_mult_commute_base_factor[of a b]
by (simp add: add.commute)
qed (simp add: distrib_right)
instance fls :: (semiring_1) semiring_1
by (standard, simp_all add: fls_mult_one)
lemma fls_of_nat: "(of_nat n :: 'a::semiring_1 fls) = fls_const (of_nat n)"
by (induct n) (auto intro: fls_eqI)
lemma fls_of_nat_nth: "of_nat n $$ k = (if k=0 then of_nat n else 0)"
by (simp add: fls_of_nat)
lemma fls_mult_of_nat_nth [simp]:
shows "(of_nat k * f) $$ n = of_nat k * f$$n"
and "(f * of_nat k ) $$ n = f$$n * of_nat k"
by (simp_all add: fls_of_nat)
lemma fls_subdegree_of_nat [simp]: "fls_subdegree (of_nat n) = 0"
by (simp add: fls_of_nat)
lemma fls_shift_of_nat_nth:
"fls_shift k (of_nat a) $$ n = (if n=-k then of_nat a else 0)"
by (simp add: fls_of_nat fls_shift_const_nth)
lemma fls_base_factor_of_nat [simp]:
"fls_base_factor (of_nat n :: 'a::semiring_1 fls) = (of_nat n :: 'a fls)"
by (simp add: fls_of_nat)
lemma fls_regpart_of_nat [simp]: "fls_regpart (of_nat n) = (of_nat n :: 'a::semiring_1 fps)"
by (simp add: fls_of_nat fps_of_nat)
lemma fls_prpart_of_nat [simp]: "fls_prpart (of_nat n) = 0"
by (simp add: fls_prpart_eq0_iff)
lemma fls_base_factor_to_fps_of_nat:
"fls_base_factor_to_fps (of_nat n) = (of_nat n :: 'a::semiring_1 fps)"
by simp
lemma fps_to_fls_of_nat:
"fps_to_fls (of_nat n) = (of_nat n :: 'a::semiring_1 fls)"
proof -
have "fps_to_fls (of_nat n) = fps_to_fls (fps_const (of_nat n))"
by (simp add: fps_of_nat)
thus ?thesis by (simp add: fls_of_nat)
qed
instance fls :: (comm_semiring_1) comm_semiring_1
by standard simp
instance fls :: (ring) ring ..
instance fls :: (comm_ring) comm_ring ..
instance fls :: (ring_1) ring_1 ..
lemma fls_of_int_nonneg: "(of_int (int n) :: 'a::ring_1 fls) = fls_const (of_int (int n))"
by (induct n) (auto intro: fls_eqI)
lemma fls_of_int: "(of_int i :: 'a::ring_1 fls) = fls_const (of_int i)"
proof (induct i)
case (neg i)
have "of_int (int (Suc i)) = fls_const (of_int (int (Suc i)) :: 'a)"
using fls_of_int_nonneg[of "Suc i"] by simp
hence "- of_int (int (Suc i)) = - fls_const (of_int (int (Suc i)) :: 'a)"
by simp
thus ?case by (simp add: fls_const_uminus[symmetric])
qed (rule fls_of_int_nonneg)
lemma fls_of_int_nth: "of_int n $$ k = (if k=0 then of_int n else 0)"
by (simp add: fls_of_int)
lemma fls_mult_of_int_nth [simp]:
shows "(of_int k * f) $$ n = of_int k * f$$n"
and "(f * of_int k ) $$ n = f$$n * of_int k"
by (simp_all add: fls_of_int)
lemma fls_subdegree_of_int [simp]: "fls_subdegree (of_int i) = 0"
by (simp add: fls_of_int)
lemma fls_shift_of_int_nth:
"fls_shift k (of_int i) $$ n = (if n=-k then of_int i else 0)"
by (simp add: fls_of_int_nth)
lemma fls_base_factor_of_int [simp]:
"fls_base_factor (of_int i :: 'a::ring_1 fls) = (of_int i :: 'a fls)"
by (simp add: fls_of_int)
lemma fls_regpart_of_int [simp]:
"fls_regpart (of_int i) = (of_int i :: 'a::ring_1 fps)"
by (simp add: fls_of_int fps_of_int)
lemma fls_prpart_of_int [simp]: "fls_prpart (of_int n) = 0"
by (simp add: fls_prpart_eq0_iff)
lemma fls_base_factor_to_fps_of_int:
"fls_base_factor_to_fps (of_int i) = (of_int i :: 'a::ring_1 fps)"
by simp
lemma fps_to_fls_of_int:
"fps_to_fls (of_int i) = (of_int i :: 'a::ring_1 fls)"
proof -
have "fps_to_fls (of_int i) = fps_to_fls (fps_const (of_int i))"
by (simp add: fps_of_int)
thus ?thesis by (simp add: fls_of_int)
qed
instance fls :: (comm_ring_1) comm_ring_1 ..
instance fls :: (semiring_no_zero_divisors) semiring_no_zero_divisors
proof
fix a b :: "'a fls"
assume "a \ 0" and "b \ 0"
hence "(a * b) $$ (fls_subdegree a + fls_subdegree b) \ 0" by simp
thus "a * b \ 0" using fls_nonzeroI by fast
qed
instance fls :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
instance fls :: (ring_no_zero_divisors) ring_no_zero_divisors ..
instance fls :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
instance fls :: (idom) idom ..
subsubsection \<open>Powers\<close>
lemma fls_pow_subdegree_ge:
"f^n \ 0 \ fls_subdegree (f^n) \ n * fls_subdegree f"
proof (induct n)
case (Suc n) thus ?case
using fls_mult_subdegree_ge[of f "f^n"] by (fastforce simp: algebra_simps)
qed simp
lemma fls_pow_nth_below_subdegree:
"k < n * fls_subdegree f \ (f^n) $$ k = 0"
using fls_pow_subdegree_ge[of f n] by (cases "f^n = 0") auto
lemma fls_pow_base [simp]:
"(f ^ n) $$ (n * fls_subdegree f) = (f $$ fls_subdegree f) ^ n"
proof (induct n)
case (Suc n)
show ?case
proof (cases "Suc n * fls_subdegree f < fls_subdegree f + fls_subdegree (f^n)")
case True with Suc show ?thesis
by (simp_all add: fls_times_nth_eq0 distrib_right)
next
case False
from False have
"{0..int n * fls_subdegree f - fls_subdegree (f ^ n)} =
insert 0 {1..int n * fls_subdegree f - fls_subdegree (f ^ n)}"
by (auto simp: algebra_simps)
with False Suc show ?thesis
by (simp add: algebra_simps fls_times_nth(4) fls_pow_nth_below_subdegree)
qed
qed simp
lemma fls_pow_subdegree_eqI:
"(f $$ fls_subdegree f) ^ n \ 0 \ fls_subdegree (f^n) = n * fls_subdegree f"
using fls_pow_nth_below_subdegree by (fastforce intro: fls_subdegree_eqI)
lemma fls_unit_base_subdegree_power:
"x * f $$ fls_subdegree f = 1 \ fls_subdegree (f ^ n) = n * fls_subdegree f"
"f $$ fls_subdegree f * y = 1 \ fls_subdegree (f ^ n) = n * fls_subdegree f"
proof-
show "x * f $$ fls_subdegree f = 1 \ fls_subdegree (f ^ n) = n * fls_subdegree f"
using left_right_inverse_power[of x "f $$ fls_subdegree f" n]
by (auto intro: fls_pow_subdegree_eqI)
show "f $$ fls_subdegree f * y = 1 \ fls_subdegree (f ^ n) = n * fls_subdegree f"
using left_right_inverse_power[of "f $$ fls_subdegree f" y n]
by (auto intro: fls_pow_subdegree_eqI)
qed
lemma fls_base_dvd1_subdegree_power:
"f $$ fls_subdegree f dvd 1 \ fls_subdegree (f ^ n) = n * fls_subdegree f"
using fls_unit_base_subdegree_power unfolding dvd_def by auto
lemma fls_pow_subdegree_ge0:
assumes "fls_subdegree f \ 0"
shows "fls_subdegree (f^n) \ 0"
proof (cases "f^n = 0")
case False
moreover from assms have "int n * fls_subdegree f \ 0" by simp
ultimately show ?thesis using fls_pow_subdegree_ge by fastforce
qed simp
lemma fls_subdegree_pow:
fixes f :: "'a::semiring_1_no_zero_divisors fls"
shows "fls_subdegree (f ^ n) = n * fls_subdegree f"
proof (cases "f=0")
case False thus ?thesis by (induct n) (simp_all add: algebra_simps)
qed (cases "n=0", auto simp: zero_power)
lemma fls_shifted_pow:
"(fls_shift m f) ^ n = fls_shift (n*m) (f ^ n)"
by (induct n) (simp_all add: fls_times_both_shifted_simp algebra_simps)
lemma fls_pow_conv_fps_pow:
assumes "fls_subdegree f \ 0"
shows "f ^ n = fps_to_fls ( (fls_regpart f) ^ n )"
proof (induct n)
case (Suc n) with assms show ?case
using fls_pow_subdegree_ge0[of f n]
by (simp add: fls_times_conv_fps_times)
qed simp
lemma fls_pow_conv_regpart:
"fls_subdegree f \ 0 \ fls_regpart (f ^ n) = (fls_regpart f) ^ n"
using fls_pow_subdegree_ge0[of f n] fls_pow_conv_fps_pow[of f n]
by (intro fps_to_fls_eq_imp_fps_eq) simp
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.49 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
