# HG changeset patch
# User haftmann
# Date 1494514073 -7200
# Node ID 2653f1cd8775ea4bcb2fde75c3555f61d60e2d95
# Parent  356c2b488cf30bc872a2b5615e14b59b74e04d78
more lemmas

diff -r 356c2b488cf3 -r 2653f1cd8775 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri May 12 16:32:53 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Thu May 11 16:47:53 2017 +0200
@@ -425,6 +425,19 @@
 lemma [code abstract]: "coeffs (pCons a p) = a ## coeffs p"
   by (fact coeffs_pCons_eq_cCons)
 
+lemma set_coeffs_subset_singleton_0_iff [simp]:
+  "set (coeffs p) \<subseteq> {0} \<longleftrightarrow> p = 0"
+  by (auto simp add: coeffs_def intro: classical)
+
+lemma set_coeffs_not_only_0 [simp]:
+  "set (coeffs p) \<noteq> {0}"
+  by (auto simp add: set_eq_subset)
+
+lemma forall_coeffs_conv:
+  "(\<forall>n. P (coeff p n)) \<longleftrightarrow> (\<forall>c \<in> set (coeffs p). P c)" if "P 0"
+  using that by (auto simp add: coeffs_def)
+    (metis atLeastLessThan_iff coeff_eq_0 not_less_iff_gr_or_eq zero_le)
+
 instantiation poly :: ("{zero, equal}") equal
 begin
 
diff -r 356c2b488cf3 -r 2653f1cd8775 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri May 12 16:32:53 2017 +0200
+++ b/src/HOL/GCD.thy	Thu May 11 16:47:53 2017 +0200
@@ -1644,6 +1644,34 @@
   qed
 qed
 
+lemma unit_factor_Gcd_fin:
+  "unit_factor (Gcd\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Gcd\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
+  by (rule normalize_idem_imp_unit_factor_eq) simp
+
+lemma unit_factor_Lcm_fin:
+  "unit_factor (Lcm\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Lcm\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
+  by (rule normalize_idem_imp_unit_factor_eq) simp
+
+lemma is_unit_Gcd_fin_iff [simp]:
+  "is_unit (Gcd\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A = 1"
+  by (rule normalize_idem_imp_is_unit_iff) simp
+
+lemma is_unit_Lcm_fin_iff [simp]:
+  "is_unit (Lcm\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Lcm\<^sub>f\<^sub>i\<^sub>n A = 1"
+  by (rule normalize_idem_imp_is_unit_iff) simp
+ 
+lemma Gcd_fin_0_iff:
+  "Gcd\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> A \<subseteq> {0} \<and> finite A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
+lemma Lcm_fin_0_iff:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A"
+  using that by (induct A) (auto simp add: lcm_eq_0_iff)
+
+lemma Lcm_fin_1_iff:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
 end
 
 context semiring_Gcd
diff -r 356c2b488cf3 -r 2653f1cd8775 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri May 12 16:32:53 2017 +0200
+++ b/src/HOL/Rings.thy	Thu May 11 16:47:53 2017 +0200
@@ -1405,6 +1405,24 @@
   then show ?thesis by simp
 qed
 
+lemma normalize_idem_imp_unit_factor_eq:
+  assumes "normalize a = a"
+  shows "unit_factor a = of_bool (a \<noteq> 0)"
+proof (cases "a = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then show ?thesis
+    using assms unit_factor_normalize [of a] by simp
+qed
+
+lemma normalize_idem_imp_is_unit_iff:
+  assumes "normalize a = a"
+  shows "is_unit a \<longleftrightarrow> a = 1"
+  using assms by (cases "a = 0") (auto dest: is_unit_normalize)
+
 text \<open>
   We avoid an explicit definition of associated elements but prefer explicit
   normalisation instead. In theory we could define an abbreviation like @{prop