--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Aug 29 17:01:11 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Aug 29 16:24:14 2017 +0200
@@ -1386,6 +1386,22 @@
lemmas fps_numeral_simps =
fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
+lemma subdegree_div:
+ assumes "q dvd p"
+ shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p - subdegree q"
+proof (cases "p = 0")
+ case False
+ from assms have "p = p div q * q" by simp
+ also from assms False have "subdegree \<dots> = subdegree (p div q) + subdegree q"
+ by (intro subdegree_mult) (auto simp: dvd_div_eq_0_iff)
+ finally show ?thesis by simp
+qed simp_all
+
+lemma subdegree_div_unit:
+ assumes "q $ 0 \<noteq> 0"
+ shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p"
+ using assms by (subst subdegree_div) simp_all
+
subsection \<open>Formal power series form a Euclidean ring\<close>
--- a/src/HOL/Computational_Algebra/Polynomial.thy Tue Aug 29 17:01:11 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Tue Aug 29 16:24:14 2017 +0200
@@ -1388,6 +1388,9 @@
for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
by (auto simp: degree_mult_eq)
+lemma degree_power_eq: "p \<noteq> 0 \<Longrightarrow> degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
+ by (induction n) (simp_all add: degree_mult_eq)
+
lemma degree_mult_right_le:
fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
assumes "q \<noteq> 0"
@@ -2454,9 +2457,6 @@
qed
qed
-lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
- by (induct n arbitrary: f) auto
-
lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
unfolding pderiv_coeffs_def
proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
@@ -2539,6 +2539,10 @@
apply (simp add: algebra_simps)
done
+lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
+ by (induction p rule: pCons_induct)
+ (auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
+
lemma pderiv_prod: "pderiv (prod f (as)) = (\<Sum>a\<in>as. prod f (as - {a}) * pderiv (f a))"
proof (induct as rule: infinite_finite_induct)
case (insert a as)
--- a/src/HOL/List.thy Tue Aug 29 17:01:11 2017 +0200
+++ b/src/HOL/List.thy Tue Aug 29 16:24:14 2017 +0200
@@ -3108,7 +3108,10 @@
done
lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
+ by (induct n) simp_all
+
+lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
+ by (induct n arbitrary: f) auto
lemma nth_take_lemma: