author chaieb Mon, 14 Jul 2008 16:13:51 +0200 changeset 27568 9949dc7a24de parent 27567 e3fe9a327c63 child 27569 c8419e8a2d83
Theorem names as in IntPrimes.thy, also several theorems moved from there
 src/HOL/Library/GCD.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Library/GCD.thy	Mon Jul 14 16:13:42 2008 +0200
+++ b/src/HOL/Library/GCD.thy	Mon Jul 14 16:13:51 2008 +0200
@@ -39,11 +39,10 @@

subsection {* GCD on nat by Euclid's algorithm *}

-fun gcd  :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+fun
+  gcd  :: "nat => nat => nat"
+where
"gcd m n = (if n = 0 then m else gcd n (m mod n))"
-
-thm gcd.induct
-
lemma gcd_induct [case_names "0" rec]:
fixes m n :: nat
assumes "\<And>m. P m 0"
@@ -222,11 +221,7 @@
definition
lcm :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
-  lcm_prim_def: "lcm m n = m * n div gcd m n"
-
-lemma lcm_def:
-  "lcm m n = m * n div gcd m n"
-  unfolding lcm_prim_def by simp
+  lcm_def: "lcm m n = m * n div gcd m n"

lemma prod_gcd_lcm:
"m * n = gcd m n * lcm m n"
@@ -324,6 +319,14 @@
qed
qed

+lemma gcd_add1_eq: "gcd (m + k) k = gcd (m + k) m"
+  by (simp add: gcd_commute)
+
+lemma gcd_diff2: "m \<le> n ==> gcd n (n - m) = gcd n m"
+  apply (subgoal_tac "n = m + (n - m)")
+   apply (erule ssubst, rule gcd_add1_eq, simp)
+  done
+

subsection {* GCD and LCM on integers *}

@@ -331,10 +334,10 @@
zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
"zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"

-lemma zgcd_dvd1 [simp]: "zgcd i j dvd i"
+lemma zgcd_zdvd1 [iff,simp]: "zgcd i j dvd i"
by (simp add: zgcd_def int_dvd_iff)

-lemma zgcd_dvd2 [simp]: "zgcd i j dvd j"
+lemma zgcd_zdvd2 [iff,simp]: "zgcd i j dvd j"
by (simp add: zgcd_def int_dvd_iff)

lemma zgcd_pos: "zgcd i j \<ge> 0"
@@ -346,10 +349,10 @@
lemma zgcd_commute: "zgcd i j = zgcd j i"
unfolding zgcd_def by (simp add: gcd_commute)

-lemma zgcd_neg1 [simp]: "zgcd (- i) j = zgcd i j"
+lemma zgcd_zminus [simp]: "zgcd (- i) j = zgcd i j"
unfolding zgcd_def by simp

-lemma zgcd_neg2 [simp]: "zgcd i (- j) = zgcd i j"
+lemma zgcd_zminus2 [simp]: "zgcd i (- j) = zgcd i j"
unfolding zgcd_def by simp

lemma zrelprime_dvd_mult: "zgcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
@@ -399,8 +402,8 @@
let ?a' = "a div ?g"
let ?b' = "b div ?g"
let ?g' = "zgcd ?a' ?b'"
-  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
-  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_dvd1 zgcd_dvd2)
+  have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
+  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
@@ -415,8 +418,71 @@
with zgcd_pos show "?g' = 1" by simp
qed

-definition zlcm :: "int \<Rightarrow> int \<Rightarrow> int" where
-  "zlcm i j = int (lcm (nat (abs i)) (nat (abs j)))"
+    (* IntPrimes stuff *)
+
+lemma zgcd_0 [simp]: "zgcd m 0 = abs m"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_0_left [simp]: "zgcd 0 m = abs m"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_non_0: "0 < n ==> zgcd m n = zgcd n (m mod n)"
+  apply (frule_tac b = n and a = m in pos_mod_sign)
+  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
+  apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
+  apply (frule_tac a = m in pos_mod_bound)
+  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
+  done
+
+lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
+  apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
+  apply (auto simp add: linorder_neq_iff zgcd_non_0)
+  apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
+  done
+
+lemma zgcd_1 [simp]: "zgcd m 1 = 1"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_0_1_iff [simp]: "zgcd 0 m = 1 \<longleftrightarrow> \<bar>m\<bar> = 1"
+  by (simp add: zgcd_def abs_if)
+
+lemma zgcd_greatest_iff: "k dvd zgcd m n = (k dvd m \<and> k dvd n)"
+  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
+
+lemma zgcd_1_left [simp]: "zgcd 1 m = 1"
+  by (simp add: zgcd_def gcd_1_left)
+
+lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
+  by (simp add: zgcd_def gcd_assoc)
+
+lemma zgcd_left_commute: "zgcd k (zgcd m n) = zgcd m (zgcd k n)"
+  apply (rule zgcd_commute [THEN trans])
+  apply (rule zgcd_assoc [THEN trans])
+  apply (rule zgcd_commute [THEN arg_cong])
+  done
+
+lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute
+  -- {* addition is an AC-operator *}
+
+lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
+  by (simp del: minus_mult_right [symmetric]
+      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
+          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
+
+lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
+  by (simp add: abs_if zgcd_zmult_distrib2)
+
+lemma zgcd_self [simp]: "0 \<le> m ==> zgcd m m = m"
+  by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
+
+lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd k (k * n) = k"
+  by (cut_tac k = k and m = 1 and n = n in zgcd_zmult_distrib2, simp_all)
+
+lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n) k = k"
+  by (cut_tac k = k and m = n and n = 1 in zgcd_zmult_distrib2, simp_all)
+
+
+definition "zlcm i j = int (lcm(nat(abs i)) (nat(abs j)))"

lemma dvd_zlcm_self1[simp]: "i dvd zlcm i j"
@@ -452,10 +518,10 @@

lemma lcm_pos:
assumes mpos: "m > 0"
-  and npos: "n > 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"
+assume h:"m*n div gcd m n = 0"
from mpos npos have "gcd m n \<noteq> 0" using gcd_zero by simp
hence gcdp: "gcd m n > 0" by simp
with h
@@ -464,7 +530,7 @@
moreover
have "gcd m n dvd m" by simp
with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
- with npos have t1:"gcd m n*n \<le> m*n" by simp
+ with npos have t1:"gcd m n *n \<le> m*n" by simp
have "gcd m n \<le> gcd m n*n" using npos by simp
with t1 have "gcd m n \<le> m*n" by arith
ultimately show "False" by simp```