# HG changeset patch
# User nipkow
# Date 1246005993 -7200
# Node ID 4df828bbc41144a18e4e62a1e575a2bd09903105
# Parent  73dc3a98669c6ba52ee964bc789d7ea8b62ca185
gcd abs lemmas

diff -r 73dc3a98669c -r 4df828bbc411 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Jun 25 20:26:17 2009 +0200
+++ b/src/HOL/GCD.thy	Fri Jun 26 10:46:33 2009 +0200
@@ -181,8 +181,17 @@
 lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
   by (simp add: gcd_int_def)
 
+lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
+by(simp add: gcd_int_def)
+
 lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
-  by (simp add: gcd_int_def)
+by (simp add: gcd_int_def)
+
+lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
+by (metis abs_idempotent int_gcd_abs)
+
+lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
+by (metis abs_idempotent int_gcd_abs)
 
 lemma int_gcd_cases:
   fixes x :: int and y
@@ -252,7 +261,7 @@
 by simp
 
 lemma int_gcd_idem: "gcd (x::int) x = abs x"
-by (subst int_gcd_abs, auto simp add: gcd_int_def)
+by (auto simp add: gcd_int_def)
 
 declare gcd_nat.simps [simp del]
 
@@ -269,18 +278,10 @@
 done
 
 lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
-  apply (subst int_gcd_abs)
-  apply (rule dvd_trans)
-  apply (rule nat_gcd_dvd1 [transferred])
-  apply auto
-done
+by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1)
 
 lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
-  apply (subst int_gcd_abs)
-  apply (rule dvd_trans)
-  apply (rule nat_gcd_dvd2 [transferred])
-  apply auto
-done
+by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2)
 
 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
 by(metis nat_gcd_dvd1 dvd_trans)
@@ -310,13 +311,11 @@
 by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
 
 lemma int_gcd_greatest:
-  assumes "(k::int) dvd m" and "k dvd n"
-  shows "k dvd gcd m n"
-
+  "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
   apply (subst int_gcd_abs)
   apply (subst abs_dvd_iff [symmetric])
   apply (rule nat_gcd_greatest [transferred])
-  using prems apply auto
+  apply auto
 done
 
 lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
@@ -412,7 +411,7 @@
 
 lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   apply (subst (1 2) int_gcd_abs)
-  apply (simp add: abs_mult)
+  apply (subst (1 2) abs_mult)
   apply (rule nat_gcd_mult_distrib [transferred])
   apply auto
 done
@@ -425,16 +424,14 @@
   done
 
 lemma int_coprime_dvd_mult:
-  assumes "coprime (k::int) n" and "k dvd m * n"
-  shows "k dvd m"
-
-  using prems
-  apply (subst abs_dvd_iff [symmetric])
-  apply (subst dvd_abs_iff [symmetric])
-  apply (subst (asm) int_gcd_abs)
-  apply (rule nat_coprime_dvd_mult [transferred])
-  apply auto
-  apply (subst abs_mult [symmetric], auto)
+  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
+apply (subst abs_dvd_iff [symmetric])
+apply (subst dvd_abs_iff [symmetric])
+apply (subst (asm) int_gcd_abs)
+apply (rule nat_coprime_dvd_mult [transferred])
+    prefer 4 apply assumption
+   apply auto
+apply (subst abs_mult [symmetric], auto)
 done
 
 lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
@@ -455,14 +452,10 @@
 done
 
 lemma int_gcd_mult_cancel:
-  assumes "coprime (k::int) n"
-  shows "gcd (k * m) n = gcd m n"
-
-  using prems
-  apply (subst (1 2) int_gcd_abs)
-  apply (subst abs_mult)
-  apply (rule nat_gcd_mult_cancel [transferred])
-  apply (auto simp add: int_gcd_abs [symmetric])
+  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
+apply (subst (1 2) int_gcd_abs)
+apply (subst abs_mult)
+apply (rule nat_gcd_mult_cancel [transferred], auto)
 done
 
 text {* \medskip Addition laws *}
@@ -573,7 +566,7 @@
 
 subsection {* Coprimality *}
 
-lemma nat_div_gcd_coprime [intro]:
+lemma nat_div_gcd_coprime:
   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   shows "coprime (a div gcd a b) (b div gcd a b)"
 proof -
@@ -597,16 +590,16 @@
   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
 qed
 
-lemma int_div_gcd_coprime [intro]:
+lemma int_div_gcd_coprime:
   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   shows "coprime (a div gcd a b) (b div gcd a b)"
-
-  apply (subst (1 2 3) int_gcd_abs)
-  apply (subst (1 2) abs_div)
-  apply auto
-  prefer 3
-  apply (rule nat_div_gcd_coprime [transferred])
-  using nz apply (auto simp add: int_gcd_abs [symmetric])
+apply (subst (1 2 3) int_gcd_abs)
+apply (subst (1 2) abs_div)
+  apply simp
+ apply simp
+apply(subst (1 2) abs_gcd_int)
+apply (rule nat_div_gcd_coprime [transferred])
+using nz apply (auto simp add: int_gcd_abs [symmetric])
 done
 
 lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
@@ -771,7 +764,7 @@
   thus ?thesis by simp
   next assume "~(a = 0 & b = 0)"
   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
-    by auto
+    by (auto simp:nat_div_gcd_coprime)
   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
     apply (subst (1 2) mult_commute)