# HG changeset patch
# User nipkow
# Date 1247402881 -7200
# Node ID 8f37cf60b8852a6f5f1b8dd1885db667860d250e
# Parent  f88e4f4948327f2caddb64be33c5c8c62da52731
more gcd/lcm lemmas

diff -r f88e4f494832 -r 8f37cf60b885 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Jul 12 11:36:09 2009 +0200
+++ b/src/HOL/GCD.thy	Sun Jul 12 14:48:01 2009 +0200
@@ -545,7 +545,7 @@
     by(bestsimp intro!:dvd_imp_le)
 qed
 
-lemma finite_divisors_int:
+lemma finite_divisors_int[simp]:
   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)
@@ -554,10 +554,25 @@
     by(bestsimp intro!:dvd_imp_le_int)
 qed
 
+lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
+apply(rule antisym)
+ apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
+apply simp
+done
+
+lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
+apply(rule antisym)
+ apply(rule Max_le_iff[THEN iffD2])
+   apply simp
+  apply fastsimp
+ apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
+apply simp
+done
+
 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 (metis finite_Collect_conjI finite_divisors_nat)
  apply simp
  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
 apply simp
@@ -566,7 +581,7 @@
 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 (metis finite_Collect_conjI finite_divisors_int)
  apply simp
  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
 apply simp
@@ -1476,6 +1491,21 @@
 proof qed (auto simp add: lcm_ac_int)
 
 
+(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
+
+lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
+
+lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
+
+lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
+by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
+
+lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
+by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
+
+
 subsection {* Primes *}
 
 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)