new lemmas
authornipkow
Sun Jun 21 23:04:37 2009 +0200 (2009-06-21)
changeset 31734a4a79836d07b
parent 31733 ec013c3ade5a
child 31745 c494ae8970e1
new lemmas
src/HOL/GCD.thy
src/HOL/IntDiv.thy
     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  
     2.1 --- a/src/HOL/IntDiv.thy	Sun Jun 21 15:47:41 2009 +0200
     2.2 +++ b/src/HOL/IntDiv.thy	Sun Jun 21 23:04:37 2009 +0200
     2.3 @@ -1064,6 +1064,16 @@
     2.4  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
     2.5    by (rule dvd_mod_imp_dvd) (* TODO: remove *)
     2.6  
     2.7 +lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
     2.8 +apply(auto simp:abs_if)
     2.9 +   apply(clarsimp simp:dvd_def mult_less_0_iff)
    2.10 +  using mult_le_cancel_left_neg[of _ "-1::int"]
    2.11 +  apply(clarsimp simp:dvd_def mult_less_0_iff)
    2.12 + apply(clarsimp simp:dvd_def mult_less_0_iff
    2.13 +         minus_mult_right simp del: mult_minus_right)
    2.14 +apply(clarsimp simp:dvd_def mult_less_0_iff)
    2.15 +done
    2.16 +
    2.17  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    2.18    apply (auto elim!: dvdE)
    2.19    apply (subgoal_tac "0 < n")