# HG changeset patch
# User haftmann
# Date 1483604647 -3600
# Node ID 3df00fb1ce0ba9ea8990c14072106131e0f66076
# Parent  3074080f4f12be96256b24b1181b1672b2d28b3e
more lemmas;
tuned headings

diff -r 3074080f4f12 -r 3df00fb1ce0b src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Jan 05 17:10:13 2017 +0000
+++ b/src/HOL/Library/Polynomial.thy	Thu Jan 05 09:24:07 2017 +0100
@@ -1169,7 +1169,7 @@
   by (intro poly_eqI) (simp_all add: coeff_map_poly)
 
 
-subsection \<open>Conversions from natural numbers\<close>
+subsection \<open>Conversions from @{typ nat} and @{typ int} numbers\<close>
 
 lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
 proof (induction n)
@@ -1185,11 +1185,17 @@
 lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
   by (simp add: of_nat_poly)
 
-lemma degree_numeral [simp]: "degree (numeral n) = 0"
-  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+lemma of_int_poly: "of_int n = [:of_int n :: 'a :: comm_ring_1:]"
+  by (simp only: of_int_of_nat of_nat_poly) simp
+
+lemma degree_of_int [simp]: "degree (of_int n) = 0"
+  by (simp add: of_int_poly)
 
 lemma numeral_poly: "numeral n = [:numeral n:]"
   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+    
+lemma degree_numeral [simp]: "degree (numeral n) = 0"
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
 
 
 subsection \<open>Lemmas about divisibility\<close>
@@ -3746,7 +3752,6 @@
   The equivalence is obvious since any rational polynomial can be multiplied with the 
   LCM of its coefficients, yielding an integer polynomial with the same roots.
 \<close>
-subsection \<open>Algebraic numbers\<close>
 
 definition algebraic :: "'a :: field_char_0 \<Rightarrow> bool" where
   "algebraic x \<longleftrightarrow> (\<exists>p. (\<forall>i. coeff p i \<in> \<int>) \<and> p \<noteq> 0 \<and> poly p x = 0)"