src/HOL/GCD.thy
 changeset 31734 a4a79836d07b parent 31730 d74830dc3e4a child 31766 f767c5b1702e
```     1.1 --- a/src/HOL/GCD.thy	Sun Jun 21 15:47:41 2009 +0200
1.2 +++ b/src/HOL/GCD.thy	Sun Jun 21 23:04:37 2009 +0200
1.3 @@ -564,6 +564,41 @@
1.4
1.5  (* to do: add the three variations of these, and for ints? *)
1.6
1.7 +lemma finite_divisors_nat:
1.8 +  assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
1.9 +proof-
1.10 +  have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
1.11 +  from finite_subset[OF _ this] show ?thesis using assms
1.12 +    by(bestsimp intro!:dvd_imp_le)
1.13 +qed
1.14 +
1.15 +lemma finite_divisors_int:
1.16 +  assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
1.17 +proof-
1.18 +  have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
1.19 +  hence "finite{d. abs d <= abs i}" by simp
1.20 +  from finite_subset[OF _ this] show ?thesis using assms
1.21 +    by(bestsimp intro!:dvd_imp_le_int)
1.22 +qed
1.23 +
1.24 +lemma gcd_is_Max_divisors_nat:
1.25 +  "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
1.26 +apply(rule Max_eqI[THEN sym])
1.27 +  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
1.28 + apply simp
1.29 + apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos)
1.30 +apply simp
1.31 +done
1.32 +
1.33 +lemma gcd_is_Max_divisors_int:
1.34 +  "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
1.35 +apply(rule Max_eqI[THEN sym])
1.36 +  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
1.37 + apply simp
1.38 + apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le)
1.39 +apply simp
1.40 +done
1.41 +
1.42
1.43  subsection {* Coprimality *}
1.44
```