src/HOL/GCD.thy
changeset 65811 2653f1cd8775
parent 65555 85ed070017b7
child 66796 ea9b2e5ca9fc
     1.1 --- a/src/HOL/GCD.thy	Fri May 12 16:32:53 2017 +0200
     1.2 +++ b/src/HOL/GCD.thy	Thu May 11 16:47:53 2017 +0200
     1.3 @@ -1644,6 +1644,34 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma unit_factor_Gcd_fin:
     1.8 +  "unit_factor (Gcd\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Gcd\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
     1.9 +  by (rule normalize_idem_imp_unit_factor_eq) simp
    1.10 +
    1.11 +lemma unit_factor_Lcm_fin:
    1.12 +  "unit_factor (Lcm\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Lcm\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)"
    1.13 +  by (rule normalize_idem_imp_unit_factor_eq) simp
    1.14 +
    1.15 +lemma is_unit_Gcd_fin_iff [simp]:
    1.16 +  "is_unit (Gcd\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A = 1"
    1.17 +  by (rule normalize_idem_imp_is_unit_iff) simp
    1.18 +
    1.19 +lemma is_unit_Lcm_fin_iff [simp]:
    1.20 +  "is_unit (Lcm\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Lcm\<^sub>f\<^sub>i\<^sub>n A = 1"
    1.21 +  by (rule normalize_idem_imp_is_unit_iff) simp
    1.22 + 
    1.23 +lemma Gcd_fin_0_iff:
    1.24 +  "Gcd\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> A \<subseteq> {0} \<and> finite A"
    1.25 +  by (induct A rule: infinite_finite_induct) simp_all
    1.26 +
    1.27 +lemma Lcm_fin_0_iff:
    1.28 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A"
    1.29 +  using that by (induct A) (auto simp add: lcm_eq_0_iff)
    1.30 +
    1.31 +lemma Lcm_fin_1_iff:
    1.32 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A"
    1.33 +  by (induct A rule: infinite_finite_induct) simp_all
    1.34 +
    1.35  end
    1.36  
    1.37  context semiring_Gcd