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.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.16 @@ -195,110 +195,124 @@
1.17  lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
1.20 -  (* Division by gcd yields rrelatively primes *)
1.22 +text {*
1.23 +  \medskip Division by gcd yields rrelatively primes.
1.24 +*}
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.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.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.82  lemma igcd_pos: "igcd i j \<ge> 0"
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.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.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.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.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.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