# 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) \ {0} \ p = 0" + by (auto simp add: coeffs_def intro: classical) + +lemma set_coeffs_not_only_0 [simp]: + "set (coeffs p) \ {0}" + by (auto simp add: set_eq_subset) + +lemma forall_coeffs_conv: + "(\n. P (coeff p n)) \ (\c \ 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 \ 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 \ 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) \ 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) \ 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 \ A \ {0} \ 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 \ 0 \ 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 \ (\a\A. is_unit a) \ 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 \ 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 \ a = 1" + using assms by (cases "a = 0") (auto dest: is_unit_normalize) + text \ We avoid an explicit definition of associated elements but prefer explicit normalisation instead. In theory we could define an abbreviation like @{prop