--- 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)
--- 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)
--- 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
-
--- 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>