merged

--- a/src/HOL/GCD.thy	Sun Jun 21 21:37:24 2009 +0200
+++ b/src/HOL/GCD.thy	Mon Jun 22 08:00:46 2009 +0200
@@ -564,6 +564,41 @@
 
 (* to do: add the three variations of these, and for ints? *)
 
+lemma finite_divisors_nat:
+  assumes "(m::nat)~= 0" shows "finite{d. d dvd m}"
+proof-
+  have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
+  from finite_subset[OF _ this] show ?thesis using assms
+    by(bestsimp intro!:dvd_imp_le)
+qed
+
+lemma finite_divisors_int:
+  assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
+proof-
+  have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
+  hence "finite{d. abs d <= abs i}" by simp
+  from finite_subset[OF _ this] show ?thesis using assms
+    by(bestsimp intro!:dvd_imp_le_int)
+qed
+
+lemma gcd_is_Max_divisors_nat:
+  "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
+apply(rule Max_eqI[THEN sym])
+  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
+ apply simp
+ apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le nat_gcd_greatest_iff nat_gcd_pos)
+apply simp
+done
+
+lemma gcd_is_Max_divisors_int:
+  "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
+apply(rule Max_eqI[THEN sym])
+  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
+ apply simp
+ apply (metis int_gcd_greatest_iff int_gcd_pos zdvd_imp_le)
+apply simp
+done
+
 
 subsection {* Coprimality *}
 

--- a/src/HOL/IntDiv.thy	Sun Jun 21 21:37:24 2009 +0200
+++ b/src/HOL/IntDiv.thy	Mon Jun 22 08:00:46 2009 +0200
@@ -1064,6 +1064,16 @@
 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   by (rule dvd_mod_imp_dvd) (* TODO: remove *)
 
+lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
+apply(auto simp:abs_if)
+   apply(clarsimp simp:dvd_def mult_less_0_iff)
+  using mult_le_cancel_left_neg[of _ "-1::int"]
+  apply(clarsimp simp:dvd_def mult_less_0_iff)
+ apply(clarsimp simp:dvd_def mult_less_0_iff
+         minus_mult_right simp del: mult_minus_right)
+apply(clarsimp simp:dvd_def mult_less_0_iff)
+done
+
 lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
   apply (auto elim!: dvdE)
   apply (subgoal_tac "0 < n")