src/HOL/GCD.thy
changeset 31995 8f37cf60b885
parent 31992 f8aed98faae7
child 31996 1d93369079c4
     1.1 --- a/src/HOL/GCD.thy	Sun Jul 12 11:36:09 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Jul 12 14:48:01 2009 +0200
     1.3 @@ -545,7 +545,7 @@
     1.4      by(bestsimp intro!:dvd_imp_le)
     1.5  qed
     1.6  
     1.7 -lemma finite_divisors_int:
     1.8 +lemma finite_divisors_int[simp]:
     1.9    assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
    1.10  proof-
    1.11    have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
    1.12 @@ -554,10 +554,25 @@
    1.13      by(bestsimp intro!:dvd_imp_le_int)
    1.14  qed
    1.15  
    1.16 +lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
    1.17 +apply(rule antisym)
    1.18 + apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
    1.19 +apply simp
    1.20 +done
    1.21 +
    1.22 +lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
    1.23 +apply(rule antisym)
    1.24 + apply(rule Max_le_iff[THEN iffD2])
    1.25 +   apply simp
    1.26 +  apply fastsimp
    1.27 + apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
    1.28 +apply simp
    1.29 +done
    1.30 +
    1.31  lemma gcd_is_Max_divisors_nat:
    1.32    "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
    1.33  apply(rule Max_eqI[THEN sym])
    1.34 -  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_nat)
    1.35 +  apply (metis finite_Collect_conjI finite_divisors_nat)
    1.36   apply simp
    1.37   apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
    1.38  apply simp
    1.39 @@ -566,7 +581,7 @@
    1.40  lemma gcd_is_Max_divisors_int:
    1.41    "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
    1.42  apply(rule Max_eqI[THEN sym])
    1.43 -  apply (metis dvd.eq_iff finite_Collect_conjI finite_divisors_int)
    1.44 +  apply (metis finite_Collect_conjI finite_divisors_int)
    1.45   apply simp
    1.46   apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
    1.47  apply simp
    1.48 @@ -1476,6 +1491,21 @@
    1.49  proof qed (auto simp add: lcm_ac_int)
    1.50  
    1.51  
    1.52 +(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
    1.53 +
    1.54 +lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
    1.55 +by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
    1.56 +
    1.57 +lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
    1.58 +by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
    1.59 +
    1.60 +lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
    1.61 +by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
    1.62 +
    1.63 +lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
    1.64 +by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
    1.65 +
    1.66 +
    1.67  subsection {* Primes *}
    1.68  
    1.69  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)