# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1504016654 -7200
# Node ID e5d82cf3c3877ee2b2cea5fb368f62cfe3ed20f5
# Parent  b8a6f933722988c43514ef396211c2ee5b90e507
Some small lemmas about polynomials and FPSs

diff -r b8a6f9337229 -r e5d82cf3c387 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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>
 
diff -r b8a6f9337229 -r e5d82cf3c387 src/HOL/Computational_Algebra/Polynomial.thy
--- 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)
diff -r b8a6f9337229 -r e5d82cf3c387 src/HOL/List.thy
--- 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: