gcd abs lemmas
authornipkow
Fri Jun 26 10:46:33 2009 +0200 (2009-06-26)
changeset 318134df828bbc411
parent 31812 73dc3a98669c
child 31814 7c122634da81
gcd abs lemmas
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Thu Jun 25 20:26:17 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Jun 26 10:46:33 2009 +0200
     1.3 @@ -181,8 +181,17 @@
     1.4  lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
     1.5    by (simp add: gcd_int_def)
     1.6  
     1.7 +lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
     1.8 +by(simp add: gcd_int_def)
     1.9 +
    1.10  lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
    1.11 -  by (simp add: gcd_int_def)
    1.12 +by (simp add: gcd_int_def)
    1.13 +
    1.14 +lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
    1.15 +by (metis abs_idempotent int_gcd_abs)
    1.16 +
    1.17 +lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
    1.18 +by (metis abs_idempotent int_gcd_abs)
    1.19  
    1.20  lemma int_gcd_cases:
    1.21    fixes x :: int and y
    1.22 @@ -252,7 +261,7 @@
    1.23  by simp
    1.24  
    1.25  lemma int_gcd_idem: "gcd (x::int) x = abs x"
    1.26 -by (subst int_gcd_abs, auto simp add: gcd_int_def)
    1.27 +by (auto simp add: gcd_int_def)
    1.28  
    1.29  declare gcd_nat.simps [simp del]
    1.30  
    1.31 @@ -269,18 +278,10 @@
    1.32  done
    1.33  
    1.34  lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
    1.35 -  apply (subst int_gcd_abs)
    1.36 -  apply (rule dvd_trans)
    1.37 -  apply (rule nat_gcd_dvd1 [transferred])
    1.38 -  apply auto
    1.39 -done
    1.40 +by (metis gcd_int_def int_dvd_iff nat_gcd_dvd1)
    1.41  
    1.42  lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
    1.43 -  apply (subst int_gcd_abs)
    1.44 -  apply (rule dvd_trans)
    1.45 -  apply (rule nat_gcd_dvd2 [transferred])
    1.46 -  apply auto
    1.47 -done
    1.48 +by (metis gcd_int_def int_dvd_iff nat_gcd_dvd2)
    1.49  
    1.50  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
    1.51  by(metis nat_gcd_dvd1 dvd_trans)
    1.52 @@ -310,13 +311,11 @@
    1.53  by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
    1.54  
    1.55  lemma int_gcd_greatest:
    1.56 -  assumes "(k::int) dvd m" and "k dvd n"
    1.57 -  shows "k dvd gcd m n"
    1.58 -
    1.59 +  "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    1.60    apply (subst int_gcd_abs)
    1.61    apply (subst abs_dvd_iff [symmetric])
    1.62    apply (rule nat_gcd_greatest [transferred])
    1.63 -  using prems apply auto
    1.64 +  apply auto
    1.65  done
    1.66  
    1.67  lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
    1.68 @@ -412,7 +411,7 @@
    1.69  
    1.70  lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
    1.71    apply (subst (1 2) int_gcd_abs)
    1.72 -  apply (simp add: abs_mult)
    1.73 +  apply (subst (1 2) abs_mult)
    1.74    apply (rule nat_gcd_mult_distrib [transferred])
    1.75    apply auto
    1.76  done
    1.77 @@ -425,16 +424,14 @@
    1.78    done
    1.79  
    1.80  lemma int_coprime_dvd_mult:
    1.81 -  assumes "coprime (k::int) n" and "k dvd m * n"
    1.82 -  shows "k dvd m"
    1.83 -
    1.84 -  using prems
    1.85 -  apply (subst abs_dvd_iff [symmetric])
    1.86 -  apply (subst dvd_abs_iff [symmetric])
    1.87 -  apply (subst (asm) int_gcd_abs)
    1.88 -  apply (rule nat_coprime_dvd_mult [transferred])
    1.89 -  apply auto
    1.90 -  apply (subst abs_mult [symmetric], auto)
    1.91 +  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
    1.92 +apply (subst abs_dvd_iff [symmetric])
    1.93 +apply (subst dvd_abs_iff [symmetric])
    1.94 +apply (subst (asm) int_gcd_abs)
    1.95 +apply (rule nat_coprime_dvd_mult [transferred])
    1.96 +    prefer 4 apply assumption
    1.97 +   apply auto
    1.98 +apply (subst abs_mult [symmetric], auto)
    1.99  done
   1.100  
   1.101  lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
   1.102 @@ -455,14 +452,10 @@
   1.103  done
   1.104  
   1.105  lemma int_gcd_mult_cancel:
   1.106 -  assumes "coprime (k::int) n"
   1.107 -  shows "gcd (k * m) n = gcd m n"
   1.108 -
   1.109 -  using prems
   1.110 -  apply (subst (1 2) int_gcd_abs)
   1.111 -  apply (subst abs_mult)
   1.112 -  apply (rule nat_gcd_mult_cancel [transferred])
   1.113 -  apply (auto simp add: int_gcd_abs [symmetric])
   1.114 +  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
   1.115 +apply (subst (1 2) int_gcd_abs)
   1.116 +apply (subst abs_mult)
   1.117 +apply (rule nat_gcd_mult_cancel [transferred], auto)
   1.118  done
   1.119  
   1.120  text {* \medskip Addition laws *}
   1.121 @@ -573,7 +566,7 @@
   1.122  
   1.123  subsection {* Coprimality *}
   1.124  
   1.125 -lemma nat_div_gcd_coprime [intro]:
   1.126 +lemma nat_div_gcd_coprime:
   1.127    assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
   1.128    shows "coprime (a div gcd a b) (b div gcd a b)"
   1.129  proof -
   1.130 @@ -597,16 +590,16 @@
   1.131    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   1.132  qed
   1.133  
   1.134 -lemma int_div_gcd_coprime [intro]:
   1.135 +lemma int_div_gcd_coprime:
   1.136    assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
   1.137    shows "coprime (a div gcd a b) (b div gcd a b)"
   1.138 -
   1.139 -  apply (subst (1 2 3) int_gcd_abs)
   1.140 -  apply (subst (1 2) abs_div)
   1.141 -  apply auto
   1.142 -  prefer 3
   1.143 -  apply (rule nat_div_gcd_coprime [transferred])
   1.144 -  using nz apply (auto simp add: int_gcd_abs [symmetric])
   1.145 +apply (subst (1 2 3) int_gcd_abs)
   1.146 +apply (subst (1 2) abs_div)
   1.147 +  apply simp
   1.148 + apply simp
   1.149 +apply(subst (1 2) abs_gcd_int)
   1.150 +apply (rule nat_div_gcd_coprime [transferred])
   1.151 +using nz apply (auto simp add: int_gcd_abs [symmetric])
   1.152  done
   1.153  
   1.154  lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.155 @@ -771,7 +764,7 @@
   1.156    thus ?thesis by simp
   1.157    next assume "~(a = 0 & b = 0)"
   1.158    hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
   1.159 -    by auto
   1.160 +    by (auto simp:nat_div_gcd_coprime)
   1.161    hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
   1.162        ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
   1.163      apply (subst (1 2) mult_commute)