src/HOL/Library/GCD.thy
changeset 22367 6860f09242bf
parent 22027 e4a08629c4bd
child 23244 1630951f0512
     1.1 --- a/src/HOL/Library/GCD.thy	Tue Feb 27 00:32:52 2007 +0100
     1.2 +++ b/src/HOL/Library/GCD.thy	Tue Feb 27 00:33:49 2007 +0100
     1.3 @@ -180,10 +180,10 @@
     1.4  
     1.5  lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
     1.6  proof -
     1.7 -  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute) 
     1.8 +  have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute)
     1.9    also have "... = gcd (n + m, m)" by (simp add: add_commute)
    1.10    also have "... = gcd (n, m)" by simp
    1.11 -  also have  "... = gcd (m, n)" by (rule gcd_commute) 
    1.12 +  also have  "... = gcd (m, n)" by (rule gcd_commute)
    1.13    finally show ?thesis .
    1.14  qed
    1.15  
    1.16 @@ -195,110 +195,124 @@
    1.17  lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
    1.18    by (induct k) (simp_all add: add_assoc)
    1.19  
    1.20 -  (* Division by gcd yields rrelatively primes *)
    1.21  
    1.22 +text {*
    1.23 +  \medskip Division by gcd yields rrelatively primes.
    1.24 +*}
    1.25  
    1.26  lemma div_gcd_relprime:
    1.27 -  assumes nz:"a\<noteq>0 \<or> b\<noteq>0"
    1.28 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
    1.29    shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1"
    1.30 -proof-
    1.31 -  let ?g = "gcd (a,b)"
    1.32 +proof -
    1.33 +  let ?g = "gcd (a, b)"
    1.34    let ?a' = "a div ?g"
    1.35    let ?b' = "b div ?g"
    1.36    let ?g' = "gcd (?a', ?b')"
    1.37    have dvdg: "?g dvd a" "?g dvd b" by simp_all
    1.38    have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
    1.39 -  from dvdg dvdg' obtain ka kb ka' kb' where 
    1.40 -   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'" 
    1.41 +  from dvdg dvdg' obtain ka kb ka' kb' where
    1.42 +      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
    1.43      unfolding dvd_def by blast
    1.44 -  hence	"?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
    1.45 -  hence dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    1.46 -    by (auto simp add: dvd_mult_div_cancel[OF dvdg(1)] 
    1.47 -      dvd_mult_div_cancel[OF dvdg(2)] dvd_def)
    1.48 +  then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
    1.49 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
    1.50 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
    1.51 +      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
    1.52    have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
    1.53 -  hence gp: "?g > 0" by simp 
    1.54 -  from gcd_greatest[OF dvdgg'] have "?g * ?g' dvd ?g" .
    1.55 -  with dvd_mult_cancel1[OF gp] show "?g' = 1" by simp
    1.56 +  then have gp: "?g > 0" by simp
    1.57 +  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
    1.58 +  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
    1.59  qed
    1.60  
    1.61 -  (* gcd on integers *)
    1.62 -constdefs igcd:: "int \<Rightarrow> int \<Rightarrow> int"
    1.63 -  "igcd i j \<equiv> int (gcd (nat (abs i),nat (abs j)))"
    1.64 -lemma igcd_dvd1[simp]:"igcd i j dvd i"
    1.65 +
    1.66 +text {*
    1.67 +  \medskip Gcd on integers.
    1.68 +*}
    1.69 +
    1.70 +definition
    1.71 +  igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.72 +  "igcd i j = int (gcd (nat (abs i), nat (abs j)))"
    1.73 +
    1.74 +lemma igcd_dvd1 [simp]: "igcd i j dvd i"
    1.75    by (simp add: igcd_def int_dvd_iff)
    1.76  
    1.77 -lemma igcd_dvd2[simp]:"igcd i j dvd j"
    1.78 -by (simp add: igcd_def int_dvd_iff)
    1.79 +lemma igcd_dvd2 [simp]: "igcd i j dvd j"
    1.80 +  by (simp add: igcd_def int_dvd_iff)
    1.81  
    1.82  lemma igcd_pos: "igcd i j \<ge> 0"
    1.83 -by (simp add: igcd_def)
    1.84 -lemma igcd0[simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
    1.85 -by (simp add: igcd_def gcd_zero) arith
    1.86 +  by (simp add: igcd_def)
    1.87 +
    1.88 +lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
    1.89 +  by (simp add: igcd_def gcd_zero) arith
    1.90  
    1.91  lemma igcd_commute: "igcd i j = igcd j i"
    1.92    unfolding igcd_def by (simp add: gcd_commute)
    1.93 -lemma igcd_neg1[simp]: "igcd (- i) j = igcd i j"
    1.94 +
    1.95 +lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j"
    1.96    unfolding igcd_def by simp
    1.97 -lemma igcd_neg2[simp]: "igcd i (- j) = igcd i j"
    1.98 +
    1.99 +lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j"
   1.100    unfolding igcd_def by simp
   1.101 +
   1.102  lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
   1.103    unfolding igcd_def
   1.104 -proof-
   1.105 -  assume H: "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   1.106 -  hence g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
   1.107 -  from H(2) obtain h where h:"k*j = i*h" unfolding dvd_def by blast  
   1.108 +proof -
   1.109 +  assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   1.110 +  then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
   1.111 +  from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
   1.112    have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
   1.113 -    unfolding dvd_def 
   1.114 -    by (rule_tac x= "nat \<bar>h\<bar>" in exI,simp add: h nat_abs_mult_distrib[symmetric])
   1.115 -  from relprime_dvd_mult[OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'" 
   1.116 +    unfolding dvd_def
   1.117 +    by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
   1.118 +  from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
   1.119      unfolding dvd_def by blast
   1.120    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
   1.121 -  hence "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   1.122 +  then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   1.123    then show ?thesis
   1.124 -    apply (subst zdvd_abs1[symmetric])
   1.125 -    apply (subst zdvd_abs2[symmetric])
   1.126 +    apply (subst zdvd_abs1 [symmetric])
   1.127 +    apply (subst zdvd_abs2 [symmetric])
   1.128      apply (unfold dvd_def)
   1.129 -    apply (rule_tac x="int h'" in exI, simp)
   1.130 +    apply (rule_tac x = "int h'" in exI, simp)
   1.131      done
   1.132  qed
   1.133  
   1.134  lemma int_nat_abs: "int (nat (abs x)) = abs x"  by arith
   1.135 -lemma igcd_greatest: assumes km:"k dvd m" and kn:"k dvd n"  shows "k dvd igcd m n"
   1.136 -proof-
   1.137 +
   1.138 +lemma igcd_greatest:
   1.139 +  assumes "k dvd m" and "k dvd n"
   1.140 +  shows "k dvd igcd m n"
   1.141 +proof -
   1.142    let ?k' = "nat \<bar>k\<bar>"
   1.143    let ?m' = "nat \<bar>m\<bar>"
   1.144    let ?n' = "nat \<bar>n\<bar>"
   1.145 -  from km kn have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
   1.146 +  from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
   1.147      unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
   1.148 -  from gcd_greatest[OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
   1.149 +  from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
   1.150      unfolding igcd_def by (simp only: zdvd_int)
   1.151 -  hence "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
   1.152 -  thus "k dvd igcd m n" by (simp add: zdvd_abs1)
   1.153 +  then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
   1.154 +  then show "k dvd igcd m n" by (simp add: zdvd_abs1)
   1.155  qed
   1.156  
   1.157  lemma div_igcd_relprime:
   1.158 -  assumes nz:"a\<noteq>0 \<or> b\<noteq>0"
   1.159 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.160    shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
   1.161 -proof-
   1.162 +proof -
   1.163    from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by simp
   1.164 -  have th1: "(1::int) = int 1" by simp
   1.165    let ?g = "igcd a b"
   1.166    let ?a' = "a div ?g"
   1.167    let ?b' = "b div ?g"
   1.168    let ?g' = "igcd ?a' ?b'"
   1.169    have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
   1.170    have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2)
   1.171 -  from dvdg dvdg' obtain ka kb ka' kb' where 
   1.172 -   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'" 
   1.173 +  from dvdg dvdg' obtain ka kb ka' kb' where
   1.174 +   kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
   1.175      unfolding dvd_def by blast
   1.176 -  hence	"?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
   1.177 -  hence dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.178 -    by (auto simp add: zdvd_mult_div_cancel[OF dvdg(1)] 
   1.179 -      zdvd_mult_div_cancel[OF dvdg(2)] dvd_def)
   1.180 +  then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
   1.181 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.182 +    by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
   1.183 +      zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.184    have "?g \<noteq> 0" using nz by simp
   1.185 -  hence gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
   1.186 -  from igcd_greatest[OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.187 -  with zdvd_mult_cancel1[OF gp] have "\<bar>?g'\<bar> = 1" by simp 
   1.188 +  then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
   1.189 +  from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.190 +  with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
   1.191    with igcd_pos show "?g' = 1" by simp
   1.192  qed
   1.193