author eberlm Tue, 29 Aug 2017 16:24:14 +0200 changeset 66551 e5d82cf3c387 parent 66550 b8a6f9337229 child 66552 4df6b0ae900d
Some small lemmas about polynomials and FPSs
```--- 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 @@
done

+lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
+  by (induction p rule: pCons_induct)
+
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:```