# HG changeset patch
# User haftmann
# Date 1435237302 -7200
# Node ID 7ed2cde6806d32b8c7f1da73da93759a9ef7fdec
# Parent  f2f1f6860959670b3dd6400e3d11add54b8962e7
more theorems

diff -r f2f1f6860959 -r 7ed2cde6806d src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Jun 25 15:01:41 2015 +0200
+++ b/src/HOL/Fields.thy	Thu Jun 25 15:01:42 2015 +0200
@@ -139,9 +139,6 @@
 lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
 by (simp add: divide_inverse)
 
-lemma divide_zero_left [simp]: "0 / a = 0"
-by (simp add: divide_inverse)
-
 lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a"
 by (simp add: divide_inverse)
 
diff -r f2f1f6860959 -r 7ed2cde6806d src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Jun 25 15:01:41 2015 +0200
+++ b/src/HOL/Int.thy	Thu Jun 25 15:01:42 2015 +0200
@@ -859,6 +859,23 @@
                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
 done
 
+lemma int_in_range_abs [simp]:
+  "int n \<in> range abs"
+proof (rule range_eqI)
+  show "int n = \<bar>int n\<bar>"
+    by simp
+qed
+
+lemma range_abs_Nats [simp]:
+  "range abs = (\<nat> :: int set)"
+proof -
+  have "\<bar>k\<bar> \<in> \<nat>" for k :: int
+    by (cases k) simp_all
+  moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
+    using that by induct simp
+  ultimately show ?thesis by blast
+qed  
+
 lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
 apply (rule sym)
 apply (simp add: nat_eq_iff)
diff -r f2f1f6860959 -r 7ed2cde6806d src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Jun 25 15:01:41 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Thu Jun 25 15:01:42 2015 +0200
@@ -244,6 +244,17 @@
     using \<open>p = pCons a q\<close> by simp
 qed
 
+lemma degree_eq_zeroE:
+  fixes p :: "'a::zero poly"
+  assumes "degree p = 0"
+  obtains a where "p = pCons a 0"
+proof -
+  obtain a q where p: "p = pCons a q" by (cases p)
+  with assms have "q = 0" by (cases "q = 0") simp_all
+  with p have "p = pCons a 0" by simp
+  with that show thesis .
+qed
+
 
 subsection \<open>List-style syntax for polynomials\<close>
 
@@ -297,7 +308,7 @@
   }
   note * = this
   show ?thesis
-    by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc)
+    by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
 qed
 
 lemma not_0_cCons_eq [simp]:
@@ -876,6 +887,10 @@
   unfolding one_poly_def
   by (simp add: coeff_pCons split: nat.split)
 
+lemma monom_eq_1 [simp]:
+  "monom 1 0 = 1"
+  by (simp add: monom_0 one_poly_def)
+  
 lemma degree_1 [simp]: "degree 1 = 0"
   unfolding one_poly_def
   by (rule degree_pCons_0)
@@ -973,6 +988,18 @@
 apply (simp add: coeff_mult_degree_sum)
 done
 
+lemma degree_mult_right_le:
+  fixes p q :: "'a::idom poly"
+  assumes "q \<noteq> 0"
+  shows "degree p \<le> degree (p * q)"
+  using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
+
+lemma coeff_degree_mult:
+  fixes p q :: "'a::idom poly"
+  shows "coeff (p * q) (degree (p * q)) =
+    coeff q (degree q) * coeff p (degree p)"
+  by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum)
+
 lemma dvd_imp_degree_le:
   fixes p q :: "'a::idom poly"
   shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
@@ -1436,6 +1463,48 @@
 
 end
 
+lemma is_unit_monom_0:
+  fixes a :: "'a::field"
+  assumes "a \<noteq> 0"
+  shows "is_unit (monom a 0)"
+proof
+  from assms show "1 = monom a 0 * monom (1 / a) 0"
+    by (simp add: mult_monom)
+qed
+
+lemma is_unit_triv:
+  fixes a :: "'a::field"
+  assumes "a \<noteq> 0"
+  shows "is_unit [:a:]"
+  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
+
+lemma is_unit_iff_degree:
+  assumes "p \<noteq> 0"
+  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q
+  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
+  with assms show ?P by (simp add: is_unit_triv)
+next
+  assume ?P
+  then obtain q where "q \<noteq> 0" "p * q = 1" ..
+  then have "degree (p * q) = degree 1"
+    by simp
+  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
+    by (simp add: degree_mult_eq)
+  then show ?Q by simp
+qed
+
+lemma is_unit_pCons_iff:
+  "is_unit (pCons a p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0" (is "?P \<longleftrightarrow> ?Q")
+  by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
+
+lemma is_unit_monom_trival:
+  fixes p :: "'a::field poly"
+  assumes "is_unit p"
+  shows "monom (coeff p (degree p)) 0 = p"
+  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
+
 lemma degree_mod_less:
   "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   using pdivmod_rel [of x y]
@@ -1833,4 +1902,3 @@
 no_notation cCons (infixr "##" 65)
 
 end
-
diff -r f2f1f6860959 -r 7ed2cde6806d src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Thu Jun 25 15:01:41 2015 +0200
+++ b/src/HOL/Rings.thy	Thu Jun 25 15:01:42 2015 +0200
@@ -619,6 +619,16 @@
   shows "a div a = 1"
   using assms nonzero_mult_divide_cancel_left [of a 1] by simp
 
+lemma divide_zero_left [simp]:
+  "0 div a = 0"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False then have "a * 0 div a = 0"
+    by (rule nonzero_mult_divide_cancel_left)
+  then show ?thesis by simp
+qed 
+
 end
 
 class idom_divide = idom + semidom_divide
@@ -651,6 +661,16 @@
   shows "b div c * a = (b * a) div c"
   using assms div_mult_swap [of c b a] by (simp add: ac_simps)
 
+lemma dvd_div_mult2_eq:
+  assumes "b * c dvd a"
+  shows "a div (b * c) = a div b div c"
+using assms proof
+  fix k
+  assume "a = b * c * k"
+  then show ?thesis
+    by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
+qed
+
 
 text \<open>Units: invertible elements in a ring\<close>
 
@@ -803,6 +823,17 @@
   with assms show ?thesis by simp
 qed
 
+lemma is_unit_div_mult2_eq:
+  assumes "is_unit b" and "is_unit c"
+  shows "a div (b * c) = a div b div c"
+proof -
+  from assms have "is_unit (b * c)" by (simp add: unit_prod)
+  then have "b * c dvd a"
+    by (rule unit_imp_dvd)
+  then show ?thesis
+    by (rule dvd_div_mult2_eq)
+qed
+
 
 text \<open>Associated elements in a ring --- an equivalence relation induced
   by the quasi-order divisibility.\<close>