extended - convers now basic lcm properties also
authorhaftmann
Tue Jul 10 09:23:13 2007 +0200 (2007-07-10)
changeset 2368706884f7ffb18
parent 23686 9d5671f61b31
child 23688 7cd68def72b2
extended - convers now basic lcm properties also
src/HOL/Library/GCD.thy
     1.1 --- a/src/HOL/Library/GCD.thy	Tue Jul 10 09:23:12 2007 +0200
     1.2 +++ b/src/HOL/Library/GCD.thy	Tue Jul 10 09:23:13 2007 +0200
     1.3 @@ -11,43 +11,64 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -  See \cite{davenport92}.
     1.8 -  \bigskip
     1.9 +  See \cite{davenport92}. \bigskip
    1.10  *}
    1.11  
    1.12 -consts
    1.13 -  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
    1.14 -
    1.15 -recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
    1.16 -  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    1.17 +subsection {* Specification of GCD on nats *}
    1.18  
    1.19  definition
    1.20 -  is_gcd :: "nat => nat => nat => bool" where -- {* @{term gcd} as a relation *}
    1.21 -  "is_gcd p m n = (p dvd m \<and> p dvd n \<and>
    1.22 -    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p))"
    1.23 +  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    1.24 +  "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    1.25 +    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    1.26 +
    1.27 +text {* Uniqueness *}
    1.28 +
    1.29 +lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n"
    1.30 +  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
    1.31 +
    1.32 +text {* Connection to divides relation *}
    1.33  
    1.34 +lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
    1.35 +  by (auto simp add: is_gcd_def)
    1.36 +
    1.37 +text {* Commutativity *}
    1.38 +
    1.39 +lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
    1.40 +  by (auto simp add: is_gcd_def)
    1.41 +
    1.42 +
    1.43 +subsection {* GCD on nat by Euclid's algorithm *}
    1.44 +
    1.45 +fun
    1.46 +  gcd  :: "nat \<times> nat => nat"
    1.47 +where
    1.48 +  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    1.49  
    1.50  lemma gcd_induct:
    1.51 -  "(!!m. P m 0) ==>
    1.52 -    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
    1.53 -  ==> P (m::nat) (n::nat)"
    1.54 -  apply (induct m n rule: gcd.induct)
    1.55 -  apply (case_tac "n = 0")
    1.56 -   apply simp_all
    1.57 -  done
    1.58 -
    1.59 +  fixes m n :: nat
    1.60 +  assumes "\<And>m. P m 0"
    1.61 +    and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
    1.62 +  shows "P m n"
    1.63 +apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split])
    1.64 +apply (case_tac "n = 0")
    1.65 +apply simp_all
    1.66 +using assms apply simp_all
    1.67 +done
    1.68  
    1.69  lemma gcd_0 [simp]: "gcd (m, 0) = m"
    1.70    by simp
    1.71  
    1.72 -lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
    1.73 +lemma gcd_0_left [simp]: "gcd (0, m) = m"
    1.74 +  by simp
    1.75 +
    1.76 +lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd (m, n) = gcd (n, m mod n)"
    1.77 +  by simp
    1.78 +
    1.79 +lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
    1.80    by simp
    1.81  
    1.82  declare gcd.simps [simp del]
    1.83  
    1.84 -lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
    1.85 -  by (simp add: gcd_non_0)
    1.86 -
    1.87  text {*
    1.88    \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    1.89    conjunctions don't seem provable separately.
    1.90 @@ -66,45 +87,24 @@
    1.91    @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    1.92  *}
    1.93  
    1.94 -lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
    1.95 +lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)"
    1.96    by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
    1.97  
    1.98 -lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
    1.99 -  by (blast intro!: gcd_greatest intro: dvd_trans)
   1.100 -
   1.101 -lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
   1.102 -  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   1.103 -
   1.104 -
   1.105  text {*
   1.106    \medskip Function gcd yields the Greatest Common Divisor.
   1.107  *}
   1.108  
   1.109  lemma is_gcd: "is_gcd (gcd (m, n)) m n"
   1.110 -  apply (simp add: is_gcd_def gcd_greatest)
   1.111 -  done
   1.112 -
   1.113 -text {*
   1.114 -  \medskip Uniqueness of GCDs.
   1.115 -*}
   1.116 -
   1.117 -lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
   1.118 -  apply (simp add: is_gcd_def)
   1.119 -  apply (blast intro: dvd_anti_sym)
   1.120 -  done
   1.121 -
   1.122 -lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
   1.123 -  apply (auto simp add: is_gcd_def)
   1.124 -  done
   1.125 +  by (simp add: is_gcd_def gcd_greatest)
   1.126  
   1.127  
   1.128 -text {*
   1.129 -  \medskip Commutativity
   1.130 -*}
   1.131 +subsection {* Derived laws for GCD *}
   1.132  
   1.133 -lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   1.134 -  apply (auto simp add: is_gcd_def)
   1.135 -  done
   1.136 +lemma gcd_greatest_iff [iff]: "k dvd gcd (m, n) \<longleftrightarrow> k dvd m \<and> k dvd n"
   1.137 +  by (blast intro!: gcd_greatest intro: dvd_trans)
   1.138 +
   1.139 +lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   1.140 +  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   1.141  
   1.142  lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   1.143    apply (rule is_gcd_unique)
   1.144 @@ -120,14 +120,8 @@
   1.145    apply (blast intro: dvd_trans)
   1.146    done
   1.147  
   1.148 -lemma gcd_0_left [simp]: "gcd (0, m) = m"
   1.149 -  apply (simp add: gcd_commute [of 0])
   1.150 -  done
   1.151 -
   1.152  lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
   1.153 -  apply (simp add: gcd_commute [of "Suc 0"])
   1.154 -  done
   1.155 -
   1.156 +  by (simp add: gcd_commute)
   1.157  
   1.158  text {*
   1.159    \medskip Multiplication laws
   1.160 @@ -195,6 +189,8 @@
   1.161  lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   1.162    by (induct k) (simp_all add: add_assoc)
   1.163  
   1.164 +lemma gcd_dvd_prod: "gcd (m, n) dvd m * n"
   1.165 +  using mult_dvd_mono [of 1] by auto
   1.166  
   1.167  text {*
   1.168    \medskip Division by gcd yields rrelatively primes.
   1.169 @@ -223,10 +219,115 @@
   1.170    with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   1.171  qed
   1.172  
   1.173 +subsection {* LCM defined by GCD *}
   1.174  
   1.175 -text {*
   1.176 -  \medskip Gcd on integers.
   1.177 -*}
   1.178 +definition
   1.179 +  lcm :: "nat \<times> nat \<Rightarrow> nat"
   1.180 +where
   1.181 +  "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
   1.182 +
   1.183 +lemma lcm_def:
   1.184 +  "lcm (m, n) = m * n div gcd (m, n)"
   1.185 +  unfolding lcm_def by simp
   1.186 +
   1.187 +lemma prod_gcd_lcm:
   1.188 +  "m * n = gcd (m, n) * lcm (m, n)"
   1.189 +  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
   1.190 +
   1.191 +lemma lcm_0 [simp]: "lcm (m, 0) = 0"
   1.192 +  unfolding lcm_def by simp
   1.193 +
   1.194 +lemma lcm_1 [simp]: "lcm (m, 1) = m"
   1.195 +  unfolding lcm_def by simp
   1.196 +
   1.197 +lemma lcm_0_left [simp]: "lcm (0, n) = 0"
   1.198 +  unfolding lcm_def by simp
   1.199 +
   1.200 +lemma lcm_1_left [simp]: "lcm (1, m) = m"
   1.201 +  unfolding lcm_def by simp
   1.202 +
   1.203 +lemma dvd_pos:
   1.204 +  fixes n m :: nat
   1.205 +  assumes "n > 0" and "m dvd n"
   1.206 +  shows "m > 0"
   1.207 +using assms by (cases m) auto
   1.208 +
   1.209 +lemma lcm_lowest:
   1.210 +  assumes "m dvd k" and "n dvd k"
   1.211 +  shows "lcm (m, n) dvd k"
   1.212 +proof (cases k)
   1.213 +  case 0 then show ?thesis by auto
   1.214 +next
   1.215 +  case (Suc _) then have pos_k: "k > 0" by auto
   1.216 +  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
   1.217 +  with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp
   1.218 +  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
   1.219 +  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
   1.220 +  from pos_k k_m have pos_p: "p > 0" by auto
   1.221 +  from pos_k k_n have pos_q: "q > 0" by auto
   1.222 +  have "k * k * gcd (q, p) = k * gcd (k * q, k * p)"
   1.223 +    by (simp add: mult_ac gcd_mult_distrib2)
   1.224 +  also have "\<dots> = k * gcd (m * p * q, n * q * p)"
   1.225 +    by (simp add: k_m [symmetric] k_n [symmetric])
   1.226 +  also have "\<dots> = k * p * q * gcd (m, n)"
   1.227 +    by (simp add: mult_ac gcd_mult_distrib2)
   1.228 +  finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)"
   1.229 +    by (simp only: k_m [symmetric] k_n [symmetric])
   1.230 +  then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)"
   1.231 +    by (simp add: mult_ac)
   1.232 +  with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)"
   1.233 +    by simp
   1.234 +  with prod_gcd_lcm [of m n]
   1.235 +  have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)"
   1.236 +    by (simp add: mult_ac)
   1.237 +  with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp
   1.238 +  then show ?thesis using dvd_def by auto
   1.239 +qed
   1.240 +
   1.241 +lemma lcm_dvd1 [iff]:
   1.242 +  "m dvd lcm (m, n)"
   1.243 +proof (cases m)
   1.244 +  case 0 then show ?thesis by simp
   1.245 +next
   1.246 +  case (Suc _)
   1.247 +  then have mpos: "m > 0" by simp
   1.248 +  show ?thesis
   1.249 +  proof (cases n)
   1.250 +    case 0 then show ?thesis by simp
   1.251 +  next
   1.252 +    case (Suc _)
   1.253 +    then have npos: "n > 0" by simp
   1.254 +    have "gcd (m, n) dvd n" by simp
   1.255 +    then obtain k where "n = gcd (m, n) * k" using dvd_def by auto
   1.256 +    then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac)
   1.257 +    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
   1.258 +    finally show ?thesis by (simp add: lcm_def)
   1.259 +  qed
   1.260 +qed
   1.261 +
   1.262 +lemma lcm_dvd2 [iff]: 
   1.263 +  "n dvd lcm (m, n)"
   1.264 +proof (cases n)
   1.265 +  case 0 then show ?thesis by simp
   1.266 +next
   1.267 +  case (Suc _)
   1.268 +  then have npos: "n > 0" by simp
   1.269 +  show ?thesis
   1.270 +  proof (cases m)
   1.271 +    case 0 then show ?thesis by simp
   1.272 +  next
   1.273 +    case (Suc _)
   1.274 +    then have mpos: "m > 0" by simp
   1.275 +    have "gcd (m, n) dvd m" by simp
   1.276 +    then obtain k where "m = gcd (m, n) * k" using dvd_def by auto
   1.277 +    then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac)
   1.278 +    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
   1.279 +    finally show ?thesis by (simp add: lcm_def)
   1.280 +  qed
   1.281 +qed
   1.282 +
   1.283 +
   1.284 +subsection {* GCD and LCM on integers *}
   1.285  
   1.286  definition
   1.287    igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   1.288 @@ -316,37 +417,9 @@
   1.289    with igcd_pos show "?g' = 1" by simp
   1.290  qed
   1.291  
   1.292 -text{* LCM *}
   1.293 -
   1.294 -definition "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
   1.295 -
   1.296  definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
   1.297  
   1.298  (* ilcm_dvd12 are needed later *)
   1.299 -lemma lcm_dvd1: 
   1.300 -  assumes mpos: " m >0"
   1.301 -  and npos: "n>0"
   1.302 -  shows "m dvd (lcm(m,n))"
   1.303 -proof-
   1.304 -  have "gcd(m,n) dvd n" by simp
   1.305 -  then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
   1.306 -  then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
   1.307 -  also have "\<dots> = m*k" using mpos npos gcd_zero by simp
   1.308 -  finally show ?thesis by (simp add: lcm_def)
   1.309 -qed
   1.310 -
   1.311 -lemma lcm_dvd2: 
   1.312 -  assumes mpos: " m >0"
   1.313 -  and npos: "n>0"
   1.314 -  shows "n dvd (lcm(m,n))"
   1.315 -proof-
   1.316 -  have "gcd(m,n) dvd m" by simp
   1.317 -  then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
   1.318 -  then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
   1.319 -  also have "\<dots> = n*k" using mpos npos gcd_zero by simp
   1.320 -  finally show ?thesis by (simp add: lcm_def)
   1.321 -qed
   1.322 -
   1.323  lemma ilcm_dvd1: 
   1.324  assumes anz: "a \<noteq> 0" 
   1.325    and bnz: "b \<noteq> 0"
   1.326 @@ -360,7 +433,6 @@
   1.327    thus ?thesis by (simp add: ilcm_def dvd_int_iff)
   1.328  qed
   1.329  
   1.330 -
   1.331  lemma ilcm_dvd2: 
   1.332  assumes anz: "a \<noteq> 0" 
   1.333    and bnz: "b \<noteq> 0"
   1.334 @@ -389,7 +461,6 @@
   1.335    assumes mpos: "m > 0"
   1.336    and npos: "n>0"
   1.337    shows "lcm (m,n) > 0"
   1.338 -
   1.339  proof(rule ccontr, simp add: lcm_def gcd_zero)
   1.340  assume h:"m*n div gcd(m,n) = 0"
   1.341  from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
   1.342 @@ -419,5 +490,4 @@
   1.343    thus ?thesis by (simp add: ilcm_def)
   1.344  qed
   1.345  
   1.346 -
   1.347  end