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