more lemmas
authorhaftmann
Thu May 11 16:47:53 2017 +0200 (2017-05-11)
changeset 658112653f1cd8775
parent 65810 356c2b488cf3
child 65812 04ba6d530c87
more lemmas
src/HOL/Computational_Algebra/Polynomial.thy
src/HOL/GCD.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri May 12 16:32:53 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Thu May 11 16:47:53 2017 +0200
     1.3 @@ -425,6 +425,19 @@
     1.4  lemma [code abstract]: "coeffs (pCons a p) = a ## coeffs p"
     1.5    by (fact coeffs_pCons_eq_cCons)
     1.6  
     1.7 +lemma set_coeffs_subset_singleton_0_iff [simp]:
     1.8 +  "set (coeffs p) \<subseteq> {0} \<longleftrightarrow> p = 0"
     1.9 +  by (auto simp add: coeffs_def intro: classical)
    1.10 +
    1.11 +lemma set_coeffs_not_only_0 [simp]:
    1.12 +  "set (coeffs p) \<noteq> {0}"
    1.13 +  by (auto simp add: set_eq_subset)
    1.14 +
    1.15 +lemma forall_coeffs_conv:
    1.16 +  "(\<forall>n. P (coeff p n)) \<longleftrightarrow> (\<forall>c \<in> set (coeffs p). P c)" if "P 0"
    1.17 +  using that by (auto simp add: coeffs_def)
    1.18 +    (metis atLeastLessThan_iff coeff_eq_0 not_less_iff_gr_or_eq zero_le)
    1.19 +
    1.20  instantiation poly :: ("{zero, equal}") equal
    1.21  begin
    1.22  
     2.1 --- a/src/HOL/GCD.thy	Fri May 12 16:32:53 2017 +0200
     2.2 +++ b/src/HOL/GCD.thy	Thu May 11 16:47:53 2017 +0200
     2.3 @@ -1644,6 +1644,34 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +lemma unit_factor_Gcd_fin:
     2.8 +  "unit_factor (Gcd\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Gcd\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
     2.9 +  by (rule normalize_idem_imp_unit_factor_eq) simp
    2.10 +
    2.11 +lemma unit_factor_Lcm_fin:
    2.12 +  "unit_factor (Lcm\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Lcm\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
    2.13 +  by (rule normalize_idem_imp_unit_factor_eq) simp
    2.14 +
    2.15 +lemma is_unit_Gcd_fin_iff [simp]:
    2.16 +  "is_unit (Gcd\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A = 1"
    2.17 +  by (rule normalize_idem_imp_is_unit_iff) simp
    2.18 +
    2.19 +lemma is_unit_Lcm_fin_iff [simp]:
    2.20 +  "is_unit (Lcm\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Lcm\<^sub>f\<^sub>i\<^sub>n A = 1"
    2.21 +  by (rule normalize_idem_imp_is_unit_iff) simp
    2.22 + 
    2.23 +lemma Gcd_fin_0_iff:
    2.24 +  "Gcd\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> A \<subseteq> {0} \<and> finite A"
    2.25 +  by (induct A rule: infinite_finite_induct) simp_all
    2.26 +
    2.27 +lemma Lcm_fin_0_iff:
    2.28 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A"
    2.29 +  using that by (induct A) (auto simp add: lcm_eq_0_iff)
    2.30 +
    2.31 +lemma Lcm_fin_1_iff:
    2.32 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A"
    2.33 +  by (induct A rule: infinite_finite_induct) simp_all
    2.34 +
    2.35  end
    2.36  
    2.37  context semiring_Gcd
     3.1 --- a/src/HOL/Rings.thy	Fri May 12 16:32:53 2017 +0200
     3.2 +++ b/src/HOL/Rings.thy	Thu May 11 16:47:53 2017 +0200
     3.3 @@ -1405,6 +1405,24 @@
     3.4    then show ?thesis by simp
     3.5  qed
     3.6  
     3.7 +lemma normalize_idem_imp_unit_factor_eq:
     3.8 +  assumes "normalize a = a"
     3.9 +  shows "unit_factor a = of_bool (a \<noteq> 0)"
    3.10 +proof (cases "a = 0")
    3.11 +  case True
    3.12 +  then show ?thesis
    3.13 +    by simp
    3.14 +next
    3.15 +  case False
    3.16 +  then show ?thesis
    3.17 +    using assms unit_factor_normalize [of a] by simp
    3.18 +qed
    3.19 +
    3.20 +lemma normalize_idem_imp_is_unit_iff:
    3.21 +  assumes "normalize a = a"
    3.22 +  shows "is_unit a \<longleftrightarrow> a = 1"
    3.23 +  using assms by (cases "a = 0") (auto dest: is_unit_normalize)
    3.24 +
    3.25  text \<open>
    3.26    We avoid an explicit definition of associated elements but prefer explicit
    3.27    normalisation instead. In theory we could define an abbreviation like @{prop