# HG changeset patch
# User haftmann
# Date 1184052193 -7200
# Node ID 06884f7ffb18bb6725e15ab8338462113b3c1f83
# Parent  9d5671f61b3154b89cc277389af4b505569595f9
extended - convers now basic lcm properties also

diff -r 9d5671f61b31 -r 06884f7ffb18 src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Tue Jul 10 09:23:12 2007 +0200
+++ b/src/HOL/Library/GCD.thy	Tue Jul 10 09:23:13 2007 +0200
@@ -11,43 +11,64 @@
 begin
 
 text {*
-  See \cite{davenport92}.
-  \bigskip
+  See \cite{davenport92}. \bigskip
 *}
 
-consts
-  gcd  :: "nat \<times> nat => nat"  -- {* Euclid's algorithm *}
-
-recdef gcd  "measure ((\<lambda>(m, n). n) :: nat \<times> nat => nat)"
-  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
+subsection {* Specification of GCD on nats *}
 
 definition
-  is_gcd :: "nat => nat => nat => bool" where -- {* @{term gcd} as a relation *}
-  "is_gcd p m n = (p dvd m \<and> p dvd n \<and>
-    (\<forall>d. d dvd m \<and> d dvd n --> d dvd p))"
+  is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
+  "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
+
+text {* Uniqueness *}
+
+lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n"
+  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
+
+text {* Connection to divides relation *}
 
+lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
+  by (auto simp add: is_gcd_def)
+
+text {* Commutativity *}
+
+lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
+  by (auto simp add: is_gcd_def)
+
+
+subsection {* GCD on nat by Euclid's algorithm *}
+
+fun
+  gcd  :: "nat \<times> nat => nat"
+where
+  "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
 
 lemma gcd_induct:
-  "(!!m. P m 0) ==>
-    (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
-  ==> P (m::nat) (n::nat)"
-  apply (induct m n rule: gcd.induct)
-  apply (case_tac "n = 0")
-   apply simp_all
-  done
-
+  fixes m n :: nat
+  assumes "\<And>m. P m 0"
+    and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
+  shows "P m n"
+apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split])
+apply (case_tac "n = 0")
+apply simp_all
+using assms apply simp_all
+done
 
 lemma gcd_0 [simp]: "gcd (m, 0) = m"
   by simp
 
-lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
+lemma gcd_0_left [simp]: "gcd (0, m) = m"
+  by simp
+
+lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd (m, n) = gcd (n, m mod n)"
+  by simp
+
+lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
   by simp
 
 declare gcd.simps [simp del]
 
-lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
-  by (simp add: gcd_non_0)
-
 text {*
   \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
   conjunctions don't seem provable separately.
@@ -66,45 +87,24 @@
   @{term n} then @{term k} divides @{term "gcd (m, n)"}.
 *}
 
-lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
+lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)"
   by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
 
-lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
-  by (blast intro!: gcd_greatest intro: dvd_trans)
-
-lemma gcd_zero: "(gcd (m, n) = 0) = (m = 0 \<and> n = 0)"
-  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
-
-
 text {*
   \medskip Function gcd yields the Greatest Common Divisor.
 *}
 
 lemma is_gcd: "is_gcd (gcd (m, n)) m n"
-  apply (simp add: is_gcd_def gcd_greatest)
-  done
-
-text {*
-  \medskip Uniqueness of GCDs.
-*}
-
-lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
-  apply (simp add: is_gcd_def)
-  apply (blast intro: dvd_anti_sym)
-  done
-
-lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
-  apply (auto simp add: is_gcd_def)
-  done
+  by (simp add: is_gcd_def gcd_greatest)
 
 
-text {*
-  \medskip Commutativity
-*}
+subsection {* Derived laws for GCD *}
 
-lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
-  apply (auto simp add: is_gcd_def)
-  done
+lemma gcd_greatest_iff [iff]: "k dvd gcd (m, n) \<longleftrightarrow> k dvd m \<and> k dvd n"
+  by (blast intro!: gcd_greatest intro: dvd_trans)
+
+lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
+  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
 
 lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   apply (rule is_gcd_unique)
@@ -120,14 +120,8 @@
   apply (blast intro: dvd_trans)
   done
 
-lemma gcd_0_left [simp]: "gcd (0, m) = m"
-  apply (simp add: gcd_commute [of 0])
-  done
-
 lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
-  apply (simp add: gcd_commute [of "Suc 0"])
-  done
-
+  by (simp add: gcd_commute)
 
 text {*
   \medskip Multiplication laws
@@ -195,6 +189,8 @@
 lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   by (induct k) (simp_all add: add_assoc)
 
+lemma gcd_dvd_prod: "gcd (m, n) dvd m * n"
+  using mult_dvd_mono [of 1] by auto
 
 text {*
   \medskip Division by gcd yields rrelatively primes.
@@ -223,10 +219,115 @@
   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
 qed
 
+subsection {* LCM defined by GCD *}
 
-text {*
-  \medskip Gcd on integers.
-*}
+definition
+  lcm :: "nat \<times> nat \<Rightarrow> nat"
+where
+  "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
+
+lemma lcm_def:
+  "lcm (m, n) = m * n div gcd (m, n)"
+  unfolding lcm_def by simp
+
+lemma prod_gcd_lcm:
+  "m * n = gcd (m, n) * lcm (m, n)"
+  unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
+
+lemma lcm_0 [simp]: "lcm (m, 0) = 0"
+  unfolding lcm_def by simp
+
+lemma lcm_1 [simp]: "lcm (m, 1) = m"
+  unfolding lcm_def by simp
+
+lemma lcm_0_left [simp]: "lcm (0, n) = 0"
+  unfolding lcm_def by simp
+
+lemma lcm_1_left [simp]: "lcm (1, m) = m"
+  unfolding lcm_def by simp
+
+lemma dvd_pos:
+  fixes n m :: nat
+  assumes "n > 0" and "m dvd n"
+  shows "m > 0"
+using assms by (cases m) auto
+
+lemma lcm_lowest:
+  assumes "m dvd k" and "n dvd k"
+  shows "lcm (m, n) dvd k"
+proof (cases k)
+  case 0 then show ?thesis by auto
+next
+  case (Suc _) then have pos_k: "k > 0" by auto
+  from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
+  with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp
+  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
+  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
+  from pos_k k_m have pos_p: "p > 0" by auto
+  from pos_k k_n have pos_q: "q > 0" by auto
+  have "k * k * gcd (q, p) = k * gcd (k * q, k * p)"
+    by (simp add: mult_ac gcd_mult_distrib2)
+  also have "\<dots> = k * gcd (m * p * q, n * q * p)"
+    by (simp add: k_m [symmetric] k_n [symmetric])
+  also have "\<dots> = k * p * q * gcd (m, n)"
+    by (simp add: mult_ac gcd_mult_distrib2)
+  finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)"
+    by (simp only: k_m [symmetric] k_n [symmetric])
+  then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)"
+    by (simp add: mult_ac)
+  with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)"
+    by simp
+  with prod_gcd_lcm [of m n]
+  have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)"
+    by (simp add: mult_ac)
+  with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp
+  then show ?thesis using dvd_def by auto
+qed
+
+lemma lcm_dvd1 [iff]:
+  "m dvd lcm (m, n)"
+proof (cases m)
+  case 0 then show ?thesis by simp
+next
+  case (Suc _)
+  then have mpos: "m > 0" by simp
+  show ?thesis
+  proof (cases n)
+    case 0 then show ?thesis by simp
+  next
+    case (Suc _)
+    then have npos: "n > 0" by simp
+    have "gcd (m, n) dvd n" by simp
+    then obtain k where "n = gcd (m, n) * k" using dvd_def by auto
+    then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac)
+    also have "\<dots> = m * k" using mpos npos gcd_zero by simp
+    finally show ?thesis by (simp add: lcm_def)
+  qed
+qed
+
+lemma lcm_dvd2 [iff]: 
+  "n dvd lcm (m, n)"
+proof (cases n)
+  case 0 then show ?thesis by simp
+next
+  case (Suc _)
+  then have npos: "n > 0" by simp
+  show ?thesis
+  proof (cases m)
+    case 0 then show ?thesis by simp
+  next
+    case (Suc _)
+    then have mpos: "m > 0" by simp
+    have "gcd (m, n) dvd m" by simp
+    then obtain k where "m = gcd (m, n) * k" using dvd_def by auto
+    then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac)
+    also have "\<dots> = n * k" using mpos npos gcd_zero by simp
+    finally show ?thesis by (simp add: lcm_def)
+  qed
+qed
+
+
+subsection {* GCD and LCM on integers *}
 
 definition
   igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
@@ -316,37 +417,9 @@
   with igcd_pos show "?g' = 1" by simp
 qed
 
-text{* LCM *}
-
-definition "lcm = (\<lambda>(m,n). m*n div gcd(m,n))"
-
 definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
 
 (* ilcm_dvd12 are needed later *)
-lemma lcm_dvd1: 
-  assumes mpos: " m >0"
-  and npos: "n>0"
-  shows "m dvd (lcm(m,n))"
-proof-
-  have "gcd(m,n) dvd n" by simp
-  then obtain "k" where "n = gcd(m,n) * k" using dvd_def by auto
-  then have "m*n div gcd(m,n) = m*(gcd(m,n)*k) div gcd(m,n)" by (simp add: mult_ac)
-  also have "\<dots> = m*k" using mpos npos gcd_zero by simp
-  finally show ?thesis by (simp add: lcm_def)
-qed
-
-lemma lcm_dvd2: 
-  assumes mpos: " m >0"
-  and npos: "n>0"
-  shows "n dvd (lcm(m,n))"
-proof-
-  have "gcd(m,n) dvd m" by simp
-  then obtain "k" where "m = gcd(m,n) * k" using dvd_def by auto
-  then have "m*n div gcd(m,n) = (gcd(m,n)*k)*n div gcd(m,n)" by (simp add: mult_ac)
-  also have "\<dots> = n*k" using mpos npos gcd_zero by simp
-  finally show ?thesis by (simp add: lcm_def)
-qed
-
 lemma ilcm_dvd1: 
 assumes anz: "a \<noteq> 0" 
   and bnz: "b \<noteq> 0"
@@ -360,7 +433,6 @@
   thus ?thesis by (simp add: ilcm_def dvd_int_iff)
 qed
 
-
 lemma ilcm_dvd2: 
 assumes anz: "a \<noteq> 0" 
   and bnz: "b \<noteq> 0"
@@ -389,7 +461,6 @@
   assumes mpos: "m > 0"
   and npos: "n>0"
   shows "lcm (m,n) > 0"
-
 proof(rule ccontr, simp add: lcm_def gcd_zero)
 assume h:"m*n div gcd(m,n) = 0"
 from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
@@ -419,5 +490,4 @@
   thus ?thesis by (simp add: ilcm_def)
 qed
 
-
 end