--- a/NEWS Sat Nov 11 18:33:35 2017 +0000
+++ b/NEWS Sat Nov 11 18:41:08 2017 +0000
@@ -89,7 +89,10 @@
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.
-* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
+* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
+
+* Predicate coprime is now a real definition, not a mere
+abbreviation. INCOMPATIBILITY.
*** System ***
--- a/src/Doc/Corec/Corec.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/Doc/Corec/Corec.thy Sat Nov 11 18:41:08 2017 +0000
@@ -334,9 +334,9 @@
primes m (n + 1))"
apply (relation "measure (\<lambda>(m, n).
if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
- apply (auto simp: mod_Suc intro: Suc_lessI)
- apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
- by (metis diff_less_mono2 lessI mod_less_divisor)
+ apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
+ apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
+ done
text \<open>
\noindent
--- a/src/HOL/Algebra/Multiplicative_Group.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Sat Nov 11 18:41:08 2017 +0000
@@ -139,7 +139,7 @@
(* Deviates from the definition given in the library in number theory *)
definition phi' :: "nat => nat"
- where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
+ where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
notation (latex output)
phi' ("\<phi> _")
@@ -148,8 +148,8 @@
assumes "m > 0"
shows "phi' m > 0"
proof -
- have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
- hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
+ have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp
+ hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)
thus ?thesis unfolding phi'_def by simp
qed
@@ -232,7 +232,7 @@
by (simp add: gcd_mult_distrib_nat q ac_simps)
hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
hence "a * n div d \<in> ?F"
- using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
+ using ge_1 le_n by (fastforce simp add: `d dvd n`)
} thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
{ fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
@@ -256,7 +256,7 @@
proof
fix m assume m: "m \<in> ?R"
thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
- by (simp add: dvd_mult_div_cancel)
+ by simp
qed
qed fastforce
finally show ?thesis by force
@@ -329,7 +329,7 @@
lemma ord_min:
assumes "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
proof -
- def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
+ define Ord where "Ord = {d \<in> {1..order G}. a (^) d = \<one>}"
have fin: "finite Ord" by (auto simp: Ord_def)
have in_ord: "ord a \<in> Ord"
using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
@@ -411,7 +411,7 @@
show "?R \<subseteq> ?L" by blast
{ fix y assume "y \<in> ?L"
then obtain x::nat where x:"y = a(^)x" by auto
- def r \<equiv> "x mod ord a"
+ define r where "r = x mod ord a"
then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
@@ -427,7 +427,7 @@
assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
shows "ord a dvd k"
proof -
- def r \<equiv> "k mod ord a"
+ define r where "r = k mod ord a"
then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
@@ -486,15 +486,16 @@
proof -
have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
- thus ?thesis by (simp add: gcd.commute)
+ thus ?thesis by (simp add: ac_simps)
qed
have dvd_d:"(ord a div gcd n (ord a)) dvd d"
proof -
have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
by (metis dvd_triv_right mult.commute)
hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
- by (simp add: mult.commute)
- thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
+ by (simp add: mult.commute)
+ then show ?thesis
+ using cp by (simp add: coprime_dvd_mult_left_iff)
qed
have "d > 0" using d_elem by simp
hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
@@ -744,7 +745,8 @@
shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
proof
assume A: ?L then show ?R
- using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
+ using assms ord_ge_1 [OF assms]
+ by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1)
next
assume ?R then show ?L
using ord_pow_dvd_ord_elem[OF assms, of k] by auto
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Sat Nov 11 18:41:08 2017 +0000
@@ -13,12 +13,6 @@
subsection \<open>Irreducible and prime elements\<close>
-(* TODO: Move ? *)
-lemma (in semiring_gcd) prod_coprime' [rule_format]:
- "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
- using prod_coprime[of A f a] by (simp add: gcd.commute)
-
-
context comm_semiring_1
begin
@@ -583,7 +577,7 @@
end
-subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
+subsection \<open>In a semiring with GCD, each irreducible element is a prime element\<close>
context semiring_gcd
begin
@@ -620,23 +614,26 @@
using assms by (simp add: prime_elem_imp_coprime)
lemma prime_elem_imp_power_coprime:
- "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
- by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
+ "prime_elem p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
+ by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps)
lemma prime_imp_power_coprime:
- "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
- by (simp add: prime_elem_imp_power_coprime)
+ "prime p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
+ by (rule prime_elem_imp_power_coprime) simp_all
lemma prime_elem_divprod_pow:
assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
shows "p^n dvd a \<or> p^n dvd b"
using assms
proof -
- from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
- by (auto simp: coprime prime_elem_def)
- with p have "coprime (p^n) a \<or> coprime (p^n) b"
- by (auto intro: prime_elem_imp_coprime coprime_exp_left)
- with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
+ from p have "\<not> is_unit p"
+ by simp
+ with ab p have "\<not> p dvd a \<or> \<not> p dvd b"
+ using not_coprimeI by blast
+ with p have "coprime (p ^ n) a \<or> coprime (p ^ n) b"
+ by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps)
+ with pab show ?thesis
+ by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff)
qed
lemma primes_coprime:
@@ -1524,6 +1521,27 @@
with assms[of P] assms[of Q] PQ show "P = Q" by simp
qed
+lemma divides_primepow:
+ assumes "prime p" and "a dvd p ^ n"
+ obtains m where "m \<le> n" and "normalize a = p ^ m"
+proof -
+ from assms have "a \<noteq> 0"
+ by auto
+ with assms
+ have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
+ by (simp add: prod_mset_prime_factorization)
+ then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
+ by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
+ with assms have "prime_factorization a \<subseteq># replicate_mset n p"
+ by (simp add: prime_factorization_prime_power)
+ then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
+ by (rule msubseteq_replicate_msetE)
+ then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
+ by simp
+ with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
+ by (simp add: prod_mset_prime_factorization)
+ with \<open>m \<le> n\<close> show thesis ..
+qed
subsection \<open>GCD and LCM computation with unique factorizations\<close>
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy Sat Nov 11 18:41:08 2017 +0000
@@ -16,6 +16,15 @@
"normalize_quot =
(\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))"
+lemma normalize_quot_zero [simp]:
+ "normalize_quot (a, 0) = (0, 1)"
+ by (simp add: normalize_quot_def)
+
+lemma normalize_quot_proj [simp]:
+ "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
+ "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
+ using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff')
+
definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where
"normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}"
@@ -61,8 +70,8 @@
lemma coprime_normalize_quot:
"coprime (fst (normalize_quot x)) (snd (normalize_quot x))"
- by (simp add: normalize_quot_def case_prod_unfold Let_def
- div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime)
+ by (simp add: normalize_quot_def case_prod_unfold div_mult_unit2)
+ (metis coprime_mult_self_right_iff div_gcd_coprime unit_div_mult_self unit_factor_is_unit)
lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts"
by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold)
@@ -203,15 +212,26 @@
and "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))"
shows "normalize_quot (a * c, b * d) = (e * g, f * h)"
proof (rule normalize_quotI)
+ from assms have "gcd a b = 1" "gcd c d = 1"
+ by simp_all
from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
- from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms]
- from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms]
- from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all)
+ with assms have "normalize b = b" "normalize d = d"
+ by (auto intro: normalize_unit_factor_eqI)
+ from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
+ note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
+ from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
+ note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
+ from k l show "a * c * (f * h) = b * d * (e * g)"
+ by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1"
by simp_all
from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot)
- with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts"
- by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq')
+ with k l assms(1,2) \<open>b \<noteq> 0\<close> \<open>d \<noteq> 0\<close> \<open>unit_factor b = 1\<close> \<open>unit_factor d = 1\<close>
+ \<open>normalize b = b\<close> \<open>normalize d = d\<close>
+ show "(e * g, f * h) \<in> normalized_fracts"
+ by (simp add: normalized_fracts_def unit_factor_mult e_def f_def g_def h_def
+ coprime_normalize_quot dvd_unit_factor_div unit_factor_gcd)
+ (metis coprime_mult_left_iff coprime_mult_right_iff)
qed (insert assms(3,4), auto)
lemma normalize_quot_mult:
@@ -230,8 +250,8 @@
(let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
(e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
in (e*g, f*h))"
- by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric]
- coprime_normalize_quot normalize_quot_mult [symmetric])
+ by transfer
+ (simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime)
lemma normalize_quot_0 [simp]:
"normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)"
@@ -254,7 +274,9 @@
by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
- using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute)
+ using assms(1,2) d
+ by (auto simp: normalized_fracts_def ac_simps)
+ (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
qed fact+
lemma quot_of_fract_inverse:
@@ -274,12 +296,19 @@
shows "normalize_quot (x div u, y) = (x' div u, y')"
proof (cases "y = 0")
case False
- from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
- from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
- with False d \<open>is_unit u\<close> show ?thesis
- by (intro normalize_quotI)
- (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
- gcd_div_unit1)
+ define v where "v = 1 div u"
+ with \<open>is_unit u\<close> have "is_unit v" and u: "\<And>a. a div u = a * v"
+ by simp_all
+ from \<open>is_unit v\<close> have "coprime v = top"
+ by (simp add: fun_eq_iff is_unit_left_imp_coprime)
+ from normalize_quotE[OF False, of x] guess d .
+ note d = this[folded assms(2,3)]
+ from assms have "coprime x' y'" "unit_factor y' = 1"
+ by (simp_all add: coprime_normalize_quot)
+ with d \<open>coprime v = top\<close> have "normalize_quot (x * v, y) = (x' * v, y')"
+ by (auto simp: normalized_fracts_def intro: normalize_quotI)
+ then show ?thesis
+ by (simp add: u)
qed (simp_all add: assms)
lemma normalize_quot_div_unit_right:
@@ -291,10 +320,8 @@
case False
from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
- with False d \<open>is_unit u\<close> show ?thesis
- by (intro normalize_quotI)
- (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
- gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric])
+ with d \<open>is_unit u\<close> show ?thesis
+ by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
qed (simp_all add: assms)
lemma normalize_quot_normalize_left:
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Sat Nov 11 18:41:08 2017 +0000
@@ -111,9 +111,10 @@
ultimately show "n dvd multiplicity p a"
by (auto simp: not_dvd_imp_multiplicity_0)
qed
- from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
- from A[of b a] assms show "is_nth_power n b"
- by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
+ from A [of a b] assms show "is_nth_power n a"
+ by (cases "n = 0") simp_all
+ from A [of b a] assms show "is_nth_power n b"
+ by (cases "n = 0") (simp_all add: ac_simps)
qed
lemma is_nth_power_mult_coprime_nat_iff:
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Sat Nov 11 18:41:08 2017 +0000
@@ -171,7 +171,7 @@
hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
- by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
+ by (simp_all add: a_def b_def coprime_quot_of_fract [of c] ac_simps
normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
ultimately show ?thesis by (intro that[of a b])
qed
@@ -513,9 +513,12 @@
from fract_poly_smult_eqE[OF this] guess a b . note ab = this
hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
- hence "normalize b = gcd a b" by simp
- also from ab(3) have "\<dots> = 1" .
- finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
+ then have "normalize b = gcd a b"
+ by simp
+ with \<open>coprime a b\<close> have "normalize b = 1"
+ by simp
+ then have "a = 1" "is_unit b"
+ by (simp_all add: a normalize_1_iff)
note eq
also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
@@ -676,7 +679,8 @@
from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
with assms content_e have "a = normalize b" by (simp add: ab(4))
- with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
+ with ab have ab': "a = 1" "is_unit b"
+ by (simp_all add: normalize_1_iff)
with ab ab' have "c' = to_fract b" by auto
from this and \<open>is_unit b\<close> show ?thesis by (rule that)
qed
--- a/src/HOL/Computational_Algebra/Primes.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Primes.thy Sat Nov 11 18:41:08 2017 +0000
@@ -245,9 +245,9 @@
using prime_power_cancel [OF assms] assms by auto
lemma prime_power_canonical:
- fixes m::nat
+ fixes m :: nat
assumes "prime p" "m > 0"
- shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
+ shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k"
using \<open>m > 0\<close>
proof (induction m rule: less_induct)
case (less m)
@@ -381,9 +381,9 @@
(* TODO: Generalise? *)
lemma prime_power_mult_nat:
- fixes p::nat
+ fixes p :: nat
assumes p: "prime p" and xy: "x * y = p ^ k"
- shows "\<exists>i j. x = p ^i \<and> y = p^ j"
+ shows "\<exists>i j. x = p ^ i \<and> y = p^ j"
using xy
proof(induct k arbitrary: x y)
case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
@@ -429,25 +429,10 @@
qed
lemma divides_primepow_nat:
- fixes p::nat
+ fixes p :: nat
assumes p: "prime p"
- shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
-proof
- assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
- unfolding dvd_def apply (auto simp add: mult.commute) by blast
- from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
- from e ij have "p^(i + j) = p^k" by (simp add: power_add)
- hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
- hence "i \<le> k" by arith
- with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
-next
- {fix i assume H: "i \<le> k" "d = p^i"
- then obtain j where j: "k = i + j"
- by (metis le_add_diff_inverse)
- hence "p^k = p^j*d" using H(2) by (simp add: power_add)
- hence "d dvd p^k" unfolding dvd_def by auto}
- thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
-qed
+ shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)"
+ using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
subsection \<open>Chinese Remainder Theorem Variants\<close>
@@ -481,8 +466,8 @@
from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
- then have d12: "d1 = 1" "d2 =1"
- by (metis ab coprime_nat)+
+ then have d12: "d1 = 1" "d2 = 1"
+ using ab coprime_common_divisor_nat [of a b] by blast+
let ?x = "v * a * x1 + u * b * x2"
let ?q1 = "v * x1 + u * y2"
let ?q2 = "v * y1 + u * x2"
@@ -497,14 +482,14 @@
lemma coprime_bezout_strong:
fixes a::nat assumes "coprime a b" "b \<noteq> 1"
shows "\<exists>x y. a * x = b * y + 1"
-by (metis assms bezout_nat gcd_nat.left_neutral)
+ by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left)
lemma bezout_prime:
assumes p: "prime p" and pa: "\<not> p dvd a"
shows "\<exists>x y. a*x = Suc (p*y)"
proof -
have ap: "coprime a p"
- by (metis gcd.commute p pa prime_imp_coprime)
+ using coprime_commute p pa prime_imp_coprime by auto
moreover from p have "p \<noteq> 1" by auto
ultimately have "\<exists>x y. a * x = p * y + 1"
by (rule coprime_bezout_strong)
--- a/src/HOL/Computational_Algebra/Squarefree.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Squarefree.thy Sat Nov 11 18:41:08 2017 +0000
@@ -116,13 +116,16 @@
show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
proof
fix p assume p: "p \<in> prime_factors (a * b)"
- {
+ with nz have "prime p"
+ by (simp add: prime_factors_dvd)
+ have "\<not> (p dvd a \<and> p dvd b)"
+ proof
assume "p dvd a \<and> p dvd b"
- hence "p dvd gcd a b" by simp
- also have "gcd a b = 1" by fact
- finally have False using nz using p by (auto simp: prime_factors_dvd)
- }
- hence "\<not>(p dvd a \<and> p dvd b)" by blast
+ with \<open>coprime a b\<close> have "is_unit p"
+ by (auto intro: coprime_common_divisor)
+ with \<open>prime p\<close> show False
+ by simp
+ qed
moreover from p have "p dvd a \<or> p dvd b" using nz
by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
@@ -138,7 +141,7 @@
shows "squarefree (prod f A)"
using assms
by (induction A rule: infinite_finite_induct)
- (auto intro!: squarefree_mult_coprime prod_coprime')
+ (auto intro!: squarefree_mult_coprime prod_coprime_right)
lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
by (cases m) (auto dest: squarefree_multD)
--- a/src/HOL/Corec_Examples/Paper_Examples.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy Sat Nov 11 18:41:08 2017 +0000
@@ -96,9 +96,9 @@
where "primes m n =
(if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
-apply (auto simp: mod_Suc intro: Suc_lessI )
-apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
-by (metis diff_less_mono2 lessI mod_less_divisor)
+ apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
+ apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
+ done
corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Sat Nov 11 18:41:08 2017 +0000
@@ -51,7 +51,8 @@
from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
- from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
+ from div_gcd_coprime[OF stupid] have gp1: "?g' = 1"
+ by simp
from ab consider "b < 0" | "b > 0" by arith
then show ?thesis
proof cases
@@ -198,6 +199,8 @@
from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
by (simp_all add: x y isnormNum_def add: gcd.commute)
+ then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
+ by (simp_all add: coprime_iff_gcd_eq_1)
from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
apply -
apply algebra
@@ -205,11 +208,11 @@
apply simp
apply algebra
done
- from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
- coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
- have eq1: "b = b'" using pos by arith
- with eq have "a = a'" using pos by simp
- with eq1 show ?thesis by (simp add: x y)
+ then have eq1: "b = b'"
+ using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
+ by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
+ with eq have "a = a'" using pos by simp
+ with \<open>b = b'\<close> show ?thesis by (simp add: x y)
qed
show ?lhs if ?rhs
using that by simp
--- a/src/HOL/Euclidean_Division.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy Sat Nov 11 18:41:08 2017 +0000
@@ -125,6 +125,15 @@
"a mod b = 0" if "is_unit b"
using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
+lemma coprime_mod_left_iff [simp]:
+ "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
+ by (rule; rule coprimeI)
+ (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
+
+lemma coprime_mod_right_iff [simp]:
+ "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0"
+ using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)
+
end
class euclidean_ring = idom_modulo + euclidean_semiring
@@ -533,6 +542,10 @@
with that show thesis .
qed
+lemma invertible_coprime:
+ "coprime a c" if "a * b mod c = 1"
+ by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)
+
end
@@ -772,6 +785,18 @@
end
+lemma coprime_Suc_0_left [simp]:
+ "coprime (Suc 0) n"
+ using coprime_1_left [of n] by simp
+
+lemma coprime_Suc_0_right [simp]:
+ "coprime n (Suc 0)"
+ using coprime_1_right [of n] by simp
+
+lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+ for a b :: nat
+ by (drule coprime_common_divisor [of _ _ x]) simp_all
+
instantiation nat :: unique_euclidean_semiring
begin
@@ -1422,6 +1447,64 @@
end
+lemma coprime_int_iff [simp]:
+ "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ show ?Q
+ proof (rule coprimeI)
+ fix q
+ assume "q dvd m" "q dvd n"
+ then have "int q dvd int m" "int q dvd int n"
+ by (simp_all add: zdvd_int)
+ with \<open>?P\<close> have "is_unit (int q)"
+ by (rule coprime_common_divisor)
+ then show "is_unit q"
+ by simp
+ qed
+next
+ assume ?Q
+ show ?P
+ proof (rule coprimeI)
+ fix k
+ assume "k dvd int m" "k dvd int n"
+ then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
+ by (simp_all add: zdvd_int)
+ with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
+ by (rule coprime_common_divisor)
+ then show "is_unit k"
+ by simp
+ qed
+qed
+
+lemma coprime_abs_left_iff [simp]:
+ "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int
+ using coprime_normalize_left_iff [of k l] by simp
+
+lemma coprime_abs_right_iff [simp]:
+ "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int
+ using coprime_abs_left_iff [of l k] by (simp add: ac_simps)
+
+lemma coprime_nat_abs_left_iff [simp]:
+ "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)"
+proof -
+ define m where "m = nat \<bar>k\<bar>"
+ then have "\<bar>k\<bar> = int m"
+ by simp
+ moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)"
+ by simp
+ ultimately show ?thesis
+ by simp
+qed
+
+lemma coprime_nat_abs_right_iff [simp]:
+ "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k"
+ using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)
+
+lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
+ for a b :: int
+ by (drule coprime_common_divisor [of _ _ x]) simp_all
+
instantiation int :: idom_modulo
begin
--- a/src/HOL/GCD.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/GCD.thy Sat Nov 11 18:41:08 2017 +0000
@@ -142,12 +142,6 @@
class gcd = zero + one + dvd +
fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-begin
-
-abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- where "coprime x y \<equiv> gcd x y = 1"
-
-end
class Gcd = gcd +
fixes Gcd :: "'a set \<Rightarrow> 'a"
@@ -243,7 +237,8 @@
by simp
qed
-lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+lemma is_unit_gcd_iff [simp]:
+ "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
sublocale gcd: abel_semigroup gcd
@@ -279,7 +274,7 @@
show "gcd (normalize a) b = gcd a b" for a b
using gcd_dvd1 [of "normalize a" b]
by (auto intro: associated_eqI)
- show "coprime 1 a" for a
+ show "gcd 1 a = 1" for a
by (rule associated_eqI) simp_all
qed simp_all
@@ -292,12 +287,6 @@
lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
by (fact gcd.right_idem)
-lemma coprime_1_left: "coprime 1 a"
- by (fact gcd.bottom_left_bottom)
-
-lemma coprime_1_right: "coprime a 1"
- by (fact gcd.bottom_right_bottom)
-
lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
proof (cases "c = 0")
case True
@@ -634,70 +623,6 @@
by (rule dvd_trans)
qed
-lemma coprime_dvd_mult:
- assumes "coprime a b" and "a dvd c * b"
- shows "a dvd c"
-proof (cases "c = 0")
- case True
- then show ?thesis by simp
-next
- case False
- then have unit: "is_unit (unit_factor c)"
- by simp
- from \<open>coprime a b\<close> mult_gcd_left [of c a b]
- have "gcd (c * a) (c * b) * unit_factor c = c"
- by (simp add: ac_simps)
- moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
- by (simp add: dvd_mult_unit_iff unit)
- ultimately show ?thesis
- by simp
-qed
-
-lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
- by (auto intro: coprime_dvd_mult)
-
-lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
- apply (rule associated_eqI)
- apply (rule gcd_greatest)
- apply (rule_tac b = c in coprime_dvd_mult)
- apply (simp add: gcd.assoc)
- apply (simp_all add: ac_simps)
- done
-
-lemma coprime_crossproduct:
- fixes a b c d :: 'a
- assumes "coprime a d" and "coprime b c"
- shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
- normalize a = normalize b \<and> normalize c = normalize d"
- (is "?lhs \<longleftrightarrow> ?rhs")
-proof
- assume ?rhs
- then show ?lhs by simp
-next
- assume ?lhs
- from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
- by (auto intro: dvdI dest: sym)
- with \<open>coprime a d\<close> have "a dvd b"
- by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
- from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
- by (auto intro: dvdI dest: sym)
- with \<open>coprime b c\<close> have "b dvd a"
- by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
- from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
- by (auto intro: dvdI dest: sym simp add: mult.commute)
- with \<open>coprime b c\<close> have "c dvd d"
- by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
- from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
- by (auto intro: dvdI dest: sym simp add: mult.commute)
- with \<open>coprime a d\<close> have "d dvd c"
- by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
- from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
- by (rule associatedI)
- moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
- by (rule associatedI)
- ultimately show ?rhs ..
-qed
-
lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
@@ -707,285 +632,6 @@
lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
-lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
- by (rule sym, rule gcdI) simp_all
-
-lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
- by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
-
-lemma div_gcd_coprime:
- assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
- shows "coprime (a div gcd a b) (b div gcd a b)"
-proof -
- let ?g = "gcd a b"
- let ?a' = "a div ?g"
- let ?b' = "b div ?g"
- let ?g' = "gcd ?a' ?b'"
- have dvdg: "?g dvd a" "?g dvd b"
- by simp_all
- have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
- by simp_all
- 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
- from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
- by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
- then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
- by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
- have "?g \<noteq> 0"
- using nz by simp
- moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
- ultimately show ?thesis
- using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
-qed
-
-lemma divides_mult:
- assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
- shows "a * b dvd c"
-proof -
- from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
- with \<open>a dvd c\<close> have "a dvd b' * b"
- by (simp add: ac_simps)
- with \<open>coprime a b\<close> have "a dvd b'"
- by (simp add: coprime_dvd_mult_iff)
- then obtain a' where "b' = a * a'" ..
- with \<open>c = b * b'\<close> have "c = (a * b) * a'"
- by (simp add: ac_simps)
- then show ?thesis ..
-qed
-
-lemma coprime_lmult:
- assumes dab: "gcd d (a * b) = 1"
- shows "gcd d a = 1"
-proof (rule coprimeI)
- fix l
- assume "l dvd d" and "l dvd a"
- then have "l dvd a * b"
- by simp
- with \<open>l dvd d\<close> and dab show "l dvd 1"
- by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_rmult:
- assumes dab: "gcd d (a * b) = 1"
- shows "gcd d b = 1"
-proof (rule coprimeI)
- fix l
- assume "l dvd d" and "l dvd b"
- then have "l dvd a * b"
- by simp
- with \<open>l dvd d\<close> and dab show "l dvd 1"
- by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_mult:
- assumes "coprime d a"
- and "coprime d b"
- shows "coprime d (a * b)"
- apply (subst gcd.commute)
- using assms(1) apply (subst gcd_mult_cancel)
- apply (subst gcd.commute)
- apply assumption
- apply (subst gcd.commute)
- apply (rule assms(2))
- done
-
-lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
- using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
- by blast
-
-lemma coprime_mul_eq':
- "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
- using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
-
-lemma gcd_coprime:
- assumes c: "gcd a b \<noteq> 0"
- and a: "a = a' * gcd a b"
- and b: "b = b' * gcd a b"
- shows "gcd a' b' = 1"
-proof -
- from c have "a \<noteq> 0 \<or> b \<noteq> 0"
- by simp
- with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
- also from assms have "a div gcd a b = a'"
- using dvd_div_eq_mult local.gcd_dvd1 by blast
- also from assms have "b div gcd a b = b'"
- using dvd_div_eq_mult local.gcd_dvd1 by blast
- finally show ?thesis .
-qed
-
-lemma coprime_power:
- assumes "0 < n"
- shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
- using assms
-proof (induct n)
- case 0
- then show ?case by simp
-next
- case (Suc n)
- then show ?case
- by (cases n) (simp_all add: coprime_mul_eq)
-qed
-
-lemma gcd_coprime_exists:
- assumes "gcd a b \<noteq> 0"
- shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
- apply (rule_tac x = "a div gcd a b" in exI)
- apply (rule_tac x = "b div gcd a b" in exI)
- using assms
- apply (auto intro: div_gcd_coprime)
- done
-
-lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
- by (induct n) (simp_all add: coprime_mult)
-
-lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
- by (induct n) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_exp2:
- assumes "coprime a b"
- shows "coprime (a ^ n) (b ^ m)"
-proof (rule coprime_exp_left)
- from assms show "coprime a (b ^ m)"
- by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
-qed
-
-lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
-proof (cases "a = 0 \<and> b = 0")
- case True
- then show ?thesis
- by (cases n) simp_all
-next
- case False
- then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
- using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
- then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
- by simp
- also note gcd_mult_distrib
- also have "unit_factor (gcd a b ^ n) = 1"
- using False by (auto simp add: unit_factor_power unit_factor_gcd)
- also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
- apply (subst ac_simps)
- apply (subst div_power)
- apply simp
- apply (rule dvd_div_mult_self)
- apply (rule dvd_power_same)
- apply simp
- done
- also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
- apply (subst ac_simps)
- apply (subst div_power)
- apply simp
- apply (rule dvd_div_mult_self)
- apply (rule dvd_power_same)
- apply simp
- done
- finally show ?thesis by simp
-qed
-
-lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
- apply (subgoal_tac "a dvd gcd a b")
- apply simp
- apply (erule (1) gcd_greatest)
- done
-
-lemma division_decomp:
- assumes "a dvd b * c"
- shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
-proof (cases "gcd a b = 0")
- case True
- then have "a = 0 \<and> b = 0"
- by simp
- then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
- by simp
- then show ?thesis by blast
-next
- case False
- let ?d = "gcd a b"
- from gcd_coprime_exists [OF False]
- obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
- by blast
- from ab'(1) have "a' dvd a"
- unfolding dvd_def by blast
- with assms have "a' dvd b * c"
- using dvd_trans [of a' a "b * c"] by simp
- from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
- by simp
- then have "?d * a' dvd ?d * (b' * c)"
- by (simp add: mult_ac)
- with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
- by simp
- with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
- by (subst (asm) ac_simps) blast
- with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
- by (simp add: mult_ac)
- then show ?thesis by blast
-qed
-
-lemma pow_divs_pow:
- assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
- shows "a dvd b"
-proof (cases "gcd a b = 0")
- case True
- then show ?thesis by simp
-next
- case False
- let ?d = "gcd a b"
- from n obtain m where m: "n = Suc m"
- by (cases n) simp_all
- from False have zn: "?d ^ n \<noteq> 0"
- by (rule power_not_zero)
- from gcd_coprime_exists [OF False]
- obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
- by blast
- from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
- by (simp add: ab'(1,2)[symmetric])
- then have "?d^n * a'^n dvd ?d^n * b'^n"
- by (simp only: power_mult_distrib ac_simps)
- with zn have "a'^n dvd b'^n"
- by simp
- then have "a' dvd b'^n"
- using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
- then have "a' dvd b'^m * b'"
- by (simp add: m ac_simps)
- with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
- have "a' dvd b'" by (subst (asm) ac_simps) blast
- then have "a' * ?d dvd b' * ?d"
- by (rule mult_dvd_mono) simp
- with ab'(1,2) show ?thesis
- by simp
-qed
-
-lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
- by (auto intro: pow_divs_pow dvd_power_same)
-
-lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
- by (subst add_commute) simp
-
-lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
- by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
-
-lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
- by (induct xs) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_divisors:
- assumes "d dvd a" "e dvd b" "gcd a b = 1"
- shows "gcd d e = 1"
-proof -
- from assms obtain k l where "a = d * k" "b = e * l"
- unfolding dvd_def by blast
- with assms have "gcd (d * k) (e * l) = 1"
- by simp
- then have "gcd (d * k) e = 1"
- by (rule coprime_lmult)
- also have "gcd (d * k) e = gcd e (d * k)"
- by (simp add: ac_simps)
- finally have "gcd e d = 1"
- by (rule coprime_lmult)
- then show ?thesis
- by (simp add: ac_simps)
-qed
-
lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
by (simp add: lcm_gcd)
@@ -1006,9 +652,6 @@
"a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
-lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
- by (subst lcm_gcd) simp
-
lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
apply (cases "a = 0")
apply simp
@@ -1058,7 +701,7 @@
qed
lemma dvd_productE:
- assumes "p dvd (a * b)"
+ assumes "p dvd a * b"
obtains x y where "p = x * y" "x dvd a" "y dvd b"
proof (cases "a = 0")
case True
@@ -1076,32 +719,11 @@
ultimately show ?thesis by (rule that)
qed
-lemma coprime_crossproduct':
- fixes a b c d
- assumes "b \<noteq> 0"
- assumes unit_factors: "unit_factor b = unit_factor d"
- assumes coprime: "coprime a b" "coprime c d"
- shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
- assume eq: "a * d = b * c"
- hence "normalize a * normalize d = normalize c * normalize b"
- by (simp only: normalize_mult [symmetric] mult_ac)
- with coprime have "normalize b = normalize d"
- by (subst (asm) coprime_crossproduct) simp_all
- from this and unit_factors show "b = d"
- by (rule normalize_unit_factor_eqI)
- from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
- with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-
end
class ring_gcd = comm_ring_1 + semiring_gcd
begin
-lemma coprime_minus_one: "coprime (n - 1) n"
- using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
-
lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
@@ -1471,36 +1093,6 @@
lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
by simp
-lemma Lcm_coprime:
- assumes "finite A"
- and "A \<noteq> {}"
- and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
- shows "Lcm A = normalize (\<Prod>A)"
- using assms
-proof (induct rule: finite_ne_induct)
- case singleton
- then show ?case by simp
-next
- case (insert a A)
- have "Lcm (insert a A) = lcm a (Lcm A)"
- by simp
- also from insert have "Lcm A = normalize (\<Prod>A)"
- by blast
- also have "lcm a \<dots> = lcm a (\<Prod>A)"
- by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
- also from insert have "gcd a (\<Prod>A) = 1"
- by (subst gcd.commute, intro prod_coprime) auto
- with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
- by (simp add: lcm_coprime)
- finally show ?case .
-qed
-
-lemma Lcm_coprime':
- "card A \<noteq> 0 \<Longrightarrow>
- (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
- Lcm A = normalize (\<Prod>A)"
- by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
-
lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
by (auto intro!: Gcd_eq_1_I)
@@ -1677,6 +1269,465 @@
end
+
+subsection \<open>Coprimality\<close>
+
+context semiring_gcd
+begin
+
+lemma coprime_imp_gcd_eq_1 [simp]:
+ "gcd a b = 1" if "coprime a b"
+proof -
+ define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
+ then have "a = t * r" and "b = t * s"
+ by simp_all
+ with that have "coprime (t * r) (t * s)"
+ by simp
+ then show ?thesis
+ by (simp add: t_def)
+qed
+
+lemma gcd_eq_1_imp_coprime:
+ "coprime a b" if "gcd a b = 1"
+proof (rule coprimeI)
+ fix c
+ assume "c dvd a" and "c dvd b"
+ then have "c dvd gcd a b"
+ by (rule gcd_greatest)
+ with that show "is_unit c"
+ by simp
+qed
+
+lemma coprime_iff_gcd_eq_1 [presburger, code]:
+ "coprime a b \<longleftrightarrow> gcd a b = 1"
+ by rule (simp_all add: gcd_eq_1_imp_coprime)
+
+lemma is_unit_gcd [simp]:
+ "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+ by (simp add: coprime_iff_gcd_eq_1)
+
+lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
+ by (simp add: gcd_eq_1_imp_coprime ac_simps)
+
+lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
+ using coprime_add_one_left [of a] by (simp add: ac_simps)
+
+lemma coprime_mult_left_iff [simp]:
+ "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c"
+proof
+ assume "coprime (a * b) c"
+ with coprime_common_divisor [of "a * b" c]
+ have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
+ using that by blast
+ have "coprime a c"
+ by (rule coprimeI, rule *) simp_all
+ moreover have "coprime b c"
+ by (rule coprimeI, rule *) simp_all
+ ultimately show "coprime a c \<and> coprime b c" ..
+next
+ assume "coprime a c \<and> coprime b c"
+ then have "coprime a c" "coprime b c"
+ by simp_all
+ show "coprime (a * b) c"
+ proof (rule coprimeI)
+ fix d
+ assume "d dvd a * b"
+ then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
+ by (rule dvd_productE)
+ assume "d dvd c"
+ with d have "r * s dvd c"
+ by simp
+ then have "r dvd c" "s dvd c"
+ by (auto intro: dvd_mult_left dvd_mult_right)
+ from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close>
+ have "is_unit r"
+ by (rule coprime_common_divisor)
+ moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close>
+ have "is_unit s"
+ by (rule coprime_common_divisor)
+ ultimately show "is_unit d"
+ by (simp add: d is_unit_mult_iff)
+ qed
+qed
+
+lemma coprime_mult_right_iff [simp]:
+ "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b"
+ using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)
+
+lemma coprime_power_left_iff [simp]:
+ "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0"
+proof (cases "n = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ then have "n > 0"
+ by simp
+ then show ?thesis
+ by (induction n rule: nat_induct_non_zero) simp_all
+qed
+
+lemma coprime_power_right_iff [simp]:
+ "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0"
+ using coprime_power_left_iff [of b n a] by (simp add: ac_simps)
+
+lemma prod_coprime_left:
+ "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a"
+ using that by (induct A rule: infinite_finite_induct) simp_all
+
+lemma prod_coprime_right:
+ "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)"
+ using that prod_coprime_left [of A f a] by (simp add: ac_simps)
+
+lemma prod_list_coprime_left:
+ "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a"
+ using that by (induct xs) simp_all
+
+lemma prod_list_coprime_right:
+ "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x"
+ using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)
+
+lemma coprime_dvd_mult_left_iff:
+ "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c"
+proof
+ assume "a dvd b"
+ then show "a dvd b * c"
+ by simp
+next
+ assume "a dvd b * c"
+ show "a dvd b"
+ proof (cases "b = 0")
+ case True
+ then show ?thesis
+ by simp
+ next
+ case False
+ then have unit: "is_unit (unit_factor b)"
+ by simp
+ from \<open>coprime a c\<close> mult_gcd_left [of b a c]
+ have "gcd (b * a) (b * c) * unit_factor b = b"
+ by (simp add: ac_simps)
+ moreover from \<open>a dvd b * c\<close>
+ have "a dvd gcd (b * a) (b * c) * unit_factor b"
+ by (simp add: dvd_mult_unit_iff unit)
+ ultimately show ?thesis
+ by simp
+ qed
+qed
+
+lemma coprime_dvd_mult_right_iff:
+ "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c"
+ using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)
+
+lemma divides_mult:
+ "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
+proof -
+ from \<open>b dvd c\<close> obtain b' where "c = b * b'" ..
+ with \<open>a dvd c\<close> have "a dvd b' * b"
+ by (simp add: ac_simps)
+ with \<open>coprime a b\<close> have "a dvd b'"
+ by (simp add: coprime_dvd_mult_left_iff)
+ then obtain a' where "b' = a * a'" ..
+ with \<open>c = b * b'\<close> have "c = (a * b) * a'"
+ by (simp add: ac_simps)
+ then show ?thesis ..
+qed
+
+lemma div_gcd_coprime:
+ assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+ shows "coprime (a div gcd a b) (b div gcd a b)"
+proof -
+ let ?g = "gcd a b"
+ let ?a' = "a div ?g"
+ let ?b' = "b div ?g"
+ let ?g' = "gcd ?a' ?b'"
+ have dvdg: "?g dvd a" "?g dvd b"
+ by simp_all
+ have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
+ by simp_all
+ 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
+ from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+ by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
+ then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
+ by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+ have "?g \<noteq> 0"
+ using assms by simp
+ moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+ ultimately show ?thesis
+ using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
+ by simp (simp only: coprime_iff_gcd_eq_1)
+qed
+
+lemma gcd_coprime:
+ assumes c: "gcd a b \<noteq> 0"
+ and a: "a = a' * gcd a b"
+ and b: "b = b' * gcd a b"
+ shows "coprime a' b'"
+proof -
+ from c have "a \<noteq> 0 \<or> b \<noteq> 0"
+ by simp
+ with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
+ also from assms have "a div gcd a b = a'"
+ using dvd_div_eq_mult local.gcd_dvd1 by blast
+ also from assms have "b div gcd a b = b'"
+ using dvd_div_eq_mult local.gcd_dvd1 by blast
+ finally show ?thesis .
+qed
+
+lemma gcd_coprime_exists:
+ assumes "gcd a b \<noteq> 0"
+ shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
+ apply (rule_tac x = "a div gcd a b" in exI)
+ apply (rule_tac x = "b div gcd a b" in exI)
+ using assms
+ apply (auto intro: div_gcd_coprime)
+ done
+
+lemma pow_divides_pow_iff [simp]:
+ "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
+proof (cases "gcd a b = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ show ?thesis
+ proof
+ let ?d = "gcd a b"
+ from \<open>n > 0\<close> obtain m where m: "n = Suc m"
+ by (cases n) simp_all
+ from False have zn: "?d ^ n \<noteq> 0"
+ by (rule power_not_zero)
+ from gcd_coprime_exists [OF False]
+ obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
+ by blast
+ assume "a ^ n dvd b ^ n"
+ then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
+ by (simp add: ab'(1,2)[symmetric])
+ then have "?d^n * a'^n dvd ?d^n * b'^n"
+ by (simp only: power_mult_distrib ac_simps)
+ with zn have "a' ^ n dvd b' ^ n"
+ by simp
+ then have "a' dvd b' ^ n"
+ using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
+ then have "a' dvd b' ^ m * b'"
+ by (simp add: m ac_simps)
+ moreover have "coprime a' (b' ^ n)"
+ using \<open>coprime a' b'\<close> by simp
+ then have "a' dvd b'"
+ using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast
+ then have "a' * ?d dvd b' * ?d"
+ by (rule mult_dvd_mono) simp
+ with ab'(1,2) show "a dvd b"
+ by simp
+ next
+ assume "a dvd b"
+ with \<open>n > 0\<close> show "a ^ n dvd b ^ n"
+ by (induction rule: nat_induct_non_zero)
+ (simp_all add: mult_dvd_mono)
+ qed
+qed
+
+lemma coprime_crossproduct:
+ fixes a b c d :: 'a
+ assumes "coprime a d" and "coprime b c"
+ shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
+ normalize a = normalize b \<and> normalize c = normalize d"
+ (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+ assume ?rhs
+ then show ?lhs by simp
+next
+ assume ?lhs
+ from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
+ by (auto intro: dvdI dest: sym)
+ with \<open>coprime a d\<close> have "a dvd b"
+ by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
+ from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
+ by (auto intro: dvdI dest: sym)
+ with \<open>coprime b c\<close> have "b dvd a"
+ by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
+ from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
+ by (auto intro: dvdI dest: sym simp add: mult.commute)
+ with \<open>coprime b c\<close> have "c dvd d"
+ by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
+ from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
+ by (auto intro: dvdI dest: sym simp add: mult.commute)
+ with \<open>coprime a d\<close> have "d dvd c"
+ by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
+ from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
+ by (rule associatedI)
+ moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
+ by (rule associatedI)
+ ultimately show ?rhs ..
+qed
+
+lemma coprime_crossproduct':
+ fixes a b c d
+ assumes "b \<noteq> 0"
+ assumes unit_factors: "unit_factor b = unit_factor d"
+ assumes coprime: "coprime a b" "coprime c d"
+ shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+ assume eq: "a * d = b * c"
+ hence "normalize a * normalize d = normalize c * normalize b"
+ by (simp only: normalize_mult [symmetric] mult_ac)
+ with coprime have "normalize b = normalize d"
+ by (subst (asm) coprime_crossproduct) simp_all
+ from this and unit_factors show "b = d"
+ by (rule normalize_unit_factor_eqI)
+ from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+ with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
+lemma gcd_mult_left_left_cancel:
+ "gcd (c * a) b = gcd a b" if "coprime b c"
+proof -
+ have "coprime (gcd b (a * c)) c"
+ by (rule coprimeI) (auto intro: that coprime_common_divisor)
+ then have "gcd b (a * c) dvd a"
+ using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
+ by simp
+ then show ?thesis
+ by (auto intro: associated_eqI simp add: ac_simps)
+qed
+
+lemma gcd_mult_left_right_cancel:
+ "gcd (a * c) b = gcd a b" if "coprime b c"
+ using that gcd_mult_left_left_cancel [of b c a]
+ by (simp add: ac_simps)
+
+lemma gcd_mult_right_left_cancel:
+ "gcd a (c * b) = gcd a b" if "coprime a c"
+ using that gcd_mult_left_left_cancel [of a c b]
+ by (simp add: ac_simps)
+
+lemma gcd_mult_right_right_cancel:
+ "gcd a (b * c) = gcd a b" if "coprime a c"
+ using that gcd_mult_right_left_cancel [of a c b]
+ by (simp add: ac_simps)
+
+lemma gcd_exp [simp]:
+ "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
+ case True
+ then show ?thesis
+ by (cases n) simp_all
+next
+ case False
+ then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
+ by (auto intro: div_gcd_coprime)
+ then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+ by simp
+ then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+ by simp
+ then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
+ by simp
+ also note gcd_mult_distrib
+ also have "unit_factor (gcd a b ^ n) = 1"
+ using False by (auto simp add: unit_factor_power unit_factor_gcd)
+ also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
+ by (simp add: ac_simps div_power dvd_power_same)
+ also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
+ by (simp add: ac_simps div_power dvd_power_same)
+ finally show ?thesis by simp
+qed
+
+lemma division_decomp:
+ assumes "a dvd b * c"
+ shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
+proof (cases "gcd a b = 0")
+ case True
+ then have "a = 0 \<and> b = 0"
+ by simp
+ then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
+ by simp
+ then show ?thesis by blast
+next
+ case False
+ let ?d = "gcd a b"
+ from gcd_coprime_exists [OF False]
+ obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
+ by blast
+ from ab'(1) have "a' dvd a" ..
+ with assms have "a' dvd b * c"
+ using dvd_trans [of a' a "b * c"] by simp
+ from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
+ by simp
+ then have "?d * a' dvd ?d * (b' * c)"
+ by (simp add: mult_ac)
+ with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
+ by simp
+ then have "a' dvd c"
+ using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff)
+ with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
+ by (simp add: ac_simps)
+ then show ?thesis by blast
+qed
+
+lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)"
+ by (subst lcm_gcd) simp
+
+end
+
+context ring_gcd
+begin
+
+lemma coprime_minus_left_iff [simp]:
+ "coprime (- a) b \<longleftrightarrow> coprime a b"
+ by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+
+lemma coprime_minus_right_iff [simp]:
+ "coprime a (- b) \<longleftrightarrow> coprime a b"
+ using coprime_minus_left_iff [of b a] by (simp add: ac_simps)
+
+lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
+ using coprime_add_one_right [of "a - 1"] by simp
+
+lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
+ using coprime_diff_one_left [of a] by (simp add: ac_simps)
+
+end
+
+context semiring_Gcd
+begin
+
+lemma Lcm_coprime:
+ assumes "finite A"
+ and "A \<noteq> {}"
+ and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b"
+ shows "Lcm A = normalize (\<Prod>A)"
+ using assms
+proof (induct rule: finite_ne_induct)
+ case singleton
+ then show ?case by simp
+next
+ case (insert a A)
+ have "Lcm (insert a A) = lcm a (Lcm A)"
+ by simp
+ also from insert have "Lcm A = normalize (\<Prod>A)"
+ by blast
+ also have "lcm a \<dots> = lcm a (\<Prod>A)"
+ by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
+ also from insert have "coprime a (\<Prod>A)"
+ by (subst coprime_commute, intro prod_coprime_left) auto
+ with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
+ by (simp add: lcm_coprime)
+ finally show ?case .
+qed
+
+lemma Lcm_coprime':
+ "card A \<noteq> 0 \<Longrightarrow>
+ (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow>
+ Lcm A = normalize (\<Prod>A)"
+ by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
+
+end
+
+
subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
instantiation nat :: gcd
@@ -1716,9 +1767,6 @@
apply simp_all
done
-
-text \<open>Specific to \<open>int\<close>.\<close>
-
lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
by (simp add: gcd_int_def)
@@ -1949,19 +1997,6 @@
for k m n :: int
by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
-lemma coprime_crossproduct_nat:
- fixes a b c d :: nat
- assumes "coprime a d" and "coprime b c"
- shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
- using assms coprime_crossproduct [of a d b c] by simp
-
-lemma coprime_crossproduct_int:
- fixes a b c d :: int
- assumes "coprime a d" and "coprime b c"
- shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
- using assms coprime_crossproduct [of a d b c] by simp
-
-
text \<open>\medskip Addition laws.\<close>
(* TODO: add the other variations? *)
@@ -2064,53 +2099,33 @@
for k l :: int
by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
-
-subsection \<open>Coprimality\<close>
-
-lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
- for a b :: nat
- using coprime [of a b] by simp
-
-lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
- for a b :: nat
- using coprime_nat by simp
-
-lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
- for a b :: int
- using gcd_unique_int [of 1 a b]
- apply clarsimp
- apply (erule subst)
- apply (rule iffI)
- apply force
- using abs_dvd_iff abs_ge_zero apply blast
- done
-
-lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
- for a b n :: nat
- using pow_divs_eq[of n] by simp
-
-lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
- using coprime_plus_one[of n] by simp
-
-lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
- for n :: nat
- using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
-
-lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
- for a b :: nat
- by (metis gcd_greatest_iff nat_dvd_1_iff_1)
-
-lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
- for a b :: int
- using gcd_greatest_iff [of x a b] by auto
-
-lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
- for m x y :: nat
- by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
-
-lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
- for m x y :: int
- by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
+lemma coprime_Suc_left_nat [simp]:
+ "coprime (Suc n) n"
+ using coprime_add_one_left [of n] by simp
+
+lemma coprime_Suc_right_nat [simp]:
+ "coprime n (Suc n)"
+ using coprime_Suc_left_nat [of n] by (simp add: ac_simps)
+
+lemma coprime_diff_one_left_nat [simp]:
+ "coprime (n - 1) n" if "n > 0" for n :: nat
+ using that coprime_Suc_right_nat [of "n - 1"] by simp
+
+lemma coprime_diff_one_right_nat [simp]:
+ "coprime n (n - 1)" if "n > 0" for n :: nat
+ using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps)
+
+lemma coprime_crossproduct_nat:
+ fixes a b c d :: nat
+ assumes "coprime a d" and "coprime b c"
+ shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
+ using assms coprime_crossproduct [of a d b c] by simp
+
+lemma coprime_crossproduct_int:
+ fixes a b c d :: int
+ assumes "coprime a d" and "coprime b c"
+ shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
+ using assms coprime_crossproduct [of a d b c] by simp
subsection \<open>Bezout's theorem\<close>
@@ -2742,14 +2757,6 @@
for i m n :: int
by (fact dvd_lcmI2)
-lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
- for a b :: nat
- by (fact coprime_exp2)
-
-lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
- for a b :: int
- by (fact coprime_exp2)
-
lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
--- a/src/HOL/Isar_Examples/Fibonacci.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Sat Nov 11 18:41:08 2017 +0000
@@ -21,10 +21,6 @@
text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
-
-declare One_nat_def [simp]
-
-
subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat"
@@ -65,12 +61,13 @@
finally show "?P (n + 2)" .
qed
-lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1"
+lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
(is "?P n")
proof (induct n rule: fib_induct)
show "?P 0" by simp
show "?P 1" by simp
fix n
+ assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
by simp
also have "\<dots> = fib (n + 2) + fib (n + 1)"
@@ -79,8 +76,10 @@
by (rule gcd_add2)
also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
by (simp add: gcd.commute)
- also assume "\<dots> = 1"
- finally show "?P (n + 2)" .
+ also have "\<dots> = 1"
+ using P by simp
+ finally show "?P (n + 2)"
+ by (simp add: coprime_iff_gcd_eq_1)
qed
lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
@@ -106,7 +105,8 @@
also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
by (simp add: gcd_mult_add)
also have "\<dots> = gcd (fib n) (fib (k + 1))"
- by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
+ using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
+ by (simp add: ac_simps)
also have "\<dots> = gcd (fib m) (fib n)"
using Suc by (simp add: gcd.commute)
finally show ?thesis .
--- a/src/HOL/Library/Multiset.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Library/Multiset.thy Sat Nov 11 18:41:08 2017 +0000
@@ -2155,6 +2155,42 @@
"image_mset f (replicate_mset n a) = replicate_mset n (f a)"
by (induct n) simp_all
+lemma replicate_mset_msubseteq_iff:
+ "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
+ by (cases m)
+ (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
+
+lemma msubseteq_replicate_msetE:
+ assumes "A \<subseteq># replicate_mset n a"
+ obtains m where "m \<le> n" and "A = replicate_mset m a"
+proof (cases "n = 0")
+ case True
+ with assms that show thesis
+ by simp
+next
+ case False
+ from assms have "set_mset A \<subseteq> set_mset (replicate_mset n a)"
+ by (rule set_mset_mono)
+ with False have "set_mset A \<subseteq> {a}"
+ by simp
+ then have "\<exists>m. A = replicate_mset m a"
+ proof (induction A)
+ case empty
+ then show ?case
+ by simp
+ next
+ case (add b A)
+ then obtain m where "A = replicate_mset m a"
+ by auto
+ with add.prems show ?case
+ by (auto intro: exI [of _ "Suc m"])
+ qed
+ then obtain m where A: "A = replicate_mset m a" ..
+ with assms have "m \<le> n"
+ by (auto simp add: replicate_mset_msubseteq_iff)
+ then show thesis using A ..
+qed
+
subsection \<open>Big operators\<close>
--- a/src/HOL/Map.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Map.thy Sat Nov 11 18:41:08 2017 +0000
@@ -782,6 +782,20 @@
with * \<open>x = (k, v)\<close> show ?case by simp
qed
+lemma eq_key_imp_eq_value:
+ "v1 = v2"
+ if "distinct (map fst xs)" "(k, v1) \<in> set xs" "(k, v2) \<in> set xs"
+proof -
+ from that have "inj_on fst (set xs)"
+ by (simp add: distinct_map)
+ moreover have "fst (k, v1) = fst (k, v2)"
+ by simp
+ ultimately have "(k, v1) = (k, v2)"
+ by (rule inj_onD) (fact that)+
+ then show ?thesis
+ by simp
+qed
+
lemma map_of_inject_set:
assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
--- a/src/HOL/Nitpick.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Nitpick.thy Sat Nov 11 18:41:08 2017 +0000
@@ -137,7 +137,7 @@
by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
definition Frac :: "int \<times> int \<Rightarrow> bool" where
- "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> gcd a b = 1"
+ "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> coprime a b"
consts
Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
--- a/src/HOL/Number_Theory/Cong.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Cong.thy Sat Nov 11 18:41:08 2017 +0000
@@ -229,7 +229,8 @@
lemma cong_mult_rcancel_int:
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
if "coprime k m" for a k m :: int
- by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
+ using that by (simp add: cong_altdef_int)
+ (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib')
lemma cong_mult_rcancel_nat:
"[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
@@ -242,7 +243,7 @@
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
by (simp add: abs_mult nat_times_as_int)
also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
- by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
+ by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
by (simp add: cong_altdef_nat')
finally show ?thesis .
@@ -320,11 +321,11 @@
lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
for a b :: nat
- by (auto simp add: cong_gcd_eq_nat)
+ by (auto simp add: cong_gcd_eq_nat coprime_iff_gcd_eq_1)
lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
for a b :: int
- by (auto simp add: cong_gcd_eq_int)
+ by (auto simp add: cong_gcd_eq_int coprime_iff_gcd_eq_1)
lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
for a b :: nat
@@ -490,36 +491,24 @@
qed
lemma cong_solve_coprime_nat:
- fixes a :: nat
- assumes "coprime a n"
- shows "\<exists>x. [a * x = 1] (mod n)"
-proof (cases "a = 0")
- case True
- with assms show ?thesis
- by (simp add: cong_0_1_nat')
-next
- case False
- with assms show ?thesis
- by (metis cong_solve_nat)
-qed
+ "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
+ using that cong_solve_nat [of a n] by (cases "a = 0") simp_all
-lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
- apply (cases "a = 0")
- apply auto
- apply (cases "n \<ge> 0")
- apply auto
- apply (metis cong_solve_int)
- done
+lemma cong_solve_coprime_int:
+ "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
+ using that cong_solve_int [of a n] by (cases "a = 0")
+ (auto simp add: zabs_def split: if_splits)
lemma coprime_iff_invertible_nat:
- "m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))"
- by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0)
+ "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))"
+ by (auto intro: cong_solve_coprime_nat)
+ (use cong_imp_coprime_nat cong_sym coprime_Suc_0_left coprime_mult_left_iff in blast)
-lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
+lemma coprime_iff_invertible_int:
+ "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
for m :: int
- apply (auto intro: cong_solve_coprime_int)
- using cong_gcd_eq_int coprime_mul_eq' apply fastforce
- done
+ by (auto intro: cong_solve_coprime_int)
+ (meson cong_imp_coprime_int cong_sym coprime_1_left coprime_mult_left_iff)
lemma coprime_iff_invertible'_nat:
"m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
@@ -554,16 +543,16 @@
and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
using that apply (induct A rule: infinite_finite_induct)
apply auto
- apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
+ apply (metis coprime_cong_mult_nat prod_coprime_right)
done
-lemma cong_cong_prod_coprime_int [rule_format]:
+lemma cong_cong_prod_coprime_int:
"[x = y] (mod (\<Prod>i\<in>A. m i))" if
"(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
"(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
using that apply (induct A rule: infinite_finite_induct)
- apply auto
- apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
+ apply auto
+ apply (metis coprime_cong_mult_int prod_coprime_right)
done
lemma binary_chinese_remainder_aux_nat:
@@ -574,7 +563,7 @@
from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
- by (subst gcd.commute)
+ by (simp add: ac_simps)
from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
@@ -593,7 +582,7 @@
from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
by auto
from a have b: "coprime m2 m1"
- by (subst gcd.commute)
+ by (simp add: ac_simps)
from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
by auto
have "[m1 * x1 = 0] (mod m1)"
@@ -730,8 +719,8 @@
fix i
assume "i \<in> A"
with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
- by (intro prod_coprime) auto
- then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
+ by (intro prod_coprime_left) auto
+ then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)"
by (elim cong_solve_coprime_nat)
then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
by auto
@@ -789,8 +778,8 @@
if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
using that apply (induct A rule: infinite_finite_induct)
- apply auto
- apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
+ apply auto
+ apply (metis coprime_cong_mult_nat prod_coprime_right)
done
lemma chinese_remainder_unique_nat:
--- a/src/HOL/Number_Theory/Euler_Criterion.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy Sat Nov 11 18:41:08 2017 +0000
@@ -65,7 +65,7 @@
proof -
have "~ p dvd x" using assms zdvd_not_zless S1_def by auto
hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x]
- by (simp add: gcd.commute)
+ by (simp add: ac_simps)
then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
moreover define y where "y = y' * a mod p"
ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
--- a/src/HOL/Number_Theory/Fib.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Fib.thy Sat Nov 11 18:41:08 2017 +0000
@@ -87,17 +87,34 @@
lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
apply (induct n rule: fib.induct)
- apply auto
- apply (metis gcd_add1 add.commute)
+ apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
+ apply (simp add: add.assoc [symmetric])
done
-lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
- apply (simp add: gcd.commute [of "fib m"])
- apply (cases m)
- apply (auto simp add: fib_add)
- apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
- gcd_add_mult gcd_mult_cancel gcd.commute)
- done
+lemma gcd_fib_add:
+ "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
+proof (cases m)
+ case 0
+ then show ?thesis
+ by simp
+next
+ case (Suc q)
+ from coprime_fib_Suc_nat [of q]
+ have "coprime (fib (Suc q)) (fib q)"
+ by (simp add: ac_simps)
+ have "gcd (fib q) (fib (Suc q)) = Suc 0"
+ using coprime_fib_Suc_nat [of q] by simp
+ then have *: "gcd (fib n * fib q) (fib n * fib (Suc q)) = fib n"
+ by (simp add: gcd_mult_distrib_nat [symmetric])
+ moreover have "gcd (fib (Suc q)) (fib n * fib q + fib (Suc n) * fib (Suc q)) =
+ gcd (fib (Suc q)) (fib n * fib q)"
+ using gcd_add_mult [of "fib (Suc q)"] by (simp add: ac_simps)
+ moreover have "gcd (fib (Suc q)) (fib n * fib (Suc q)) = fib (Suc q)"
+ by simp
+ ultimately show ?thesis
+ using Suc \<open>coprime (fib (Suc q)) (fib q)\<close>
+ by (auto simp add: fib_add algebra_simps gcd_mult_right_right_cancel)
+qed
lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
--- a/src/HOL/Number_Theory/Gauss.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy Sat Nov 11 18:41:08 2017 +0000
@@ -115,8 +115,9 @@
proof -
from p_a_relprime have "\<not> p dvd a"
by (simp add: cong_altdef_int)
- with p_prime have "coprime a (int p)"
- by (subst gcd.commute, intro prime_imp_coprime) auto
+ with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
+ have "coprime a (int p)"
+ by (simp_all add: zdvd_int ac_simps)
with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -149,8 +150,9 @@
using cong_def by blast
from p_a_relprime have "\<not>p dvd a"
by (simp add: cong_altdef_int)
- with p_prime have "coprime a (int p)"
- by (subst gcd.commute, intro prime_imp_coprime) auto
+ with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
+ have "coprime a (int p)"
+ by (simp_all add: zdvd_int ac_simps)
with a' cong_mult_rcancel_int [of a "int p" x y]
have "[x = y] (mod p)" by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -219,13 +221,16 @@
by (auto simp add: D_def C_def B_def A_def)
lemma all_A_relprime:
- assumes "x \<in> A"
- shows "gcd x p = 1"
- using p_prime A_ncong_p [OF assms]
- by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
-
-lemma A_prod_relprime: "gcd (prod id A) p = 1"
- by (metis id_def all_A_relprime prod_coprime)
+ "coprime x p" if "x \<in> A"
+proof -
+ from A_ncong_p [OF that] have "\<not> int p dvd x"
+ by (simp add: cong_altdef_int)
+ with p_prime show ?thesis
+ by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer)
+qed
+
+lemma A_prod_relprime: "coprime (prod id A) p"
+ by (auto intro: prod_coprime_left all_A_relprime)
subsection \<open>Relationships Between Gauss Sets\<close>
--- a/src/HOL/Number_Theory/Pocklington.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Pocklington.thy Sat Nov 11 18:41:08 2017 +0000
@@ -11,18 +11,11 @@
subsection \<open>Lemmas about previously defined terms\<close>
lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
- unfolding prime_nat_iff
-proof safe
- fix m
- assume p: "p > 0" "p \<noteq> 1"
- and m: "m dvd p" "m \<noteq> p"
- and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
- from p m have "m \<noteq> 0" by (intro notI) auto
- moreover from p m have "m < p" by (auto dest: dvd_imp_le)
- ultimately have "coprime p m"
- using * by blast
- with m show "m = 1" by simp
-qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
+ apply (auto simp add: prime_nat_iff)
+ apply (rule coprimeI)
+ apply (auto dest: nat_dvd_not_less simp add: ac_simps)
+ apply (metis One_nat_def dvd_1_iff_1 dvd_pos_nat gcd_nat.order_iff is_unit_gcd linorder_neqE_nat nat_dvd_not_less)
+ done
lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
proof -
@@ -46,7 +39,7 @@
from bezout_add_strong_nat [OF this]
obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
from dxy(1,2) have d1: "d = 1"
- by (metis assms coprime_nat)
+ using assms coprime_common_divisor [of a n d] by simp
with dxy(3) have "a * x * b = (n * y + 1) * b"
by simp
then have "a * (x * b) = n * (y * b) + b"
@@ -94,9 +87,9 @@
shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
proof -
from pa have ap: "coprime a p"
- by (metis gcd.commute)
- have px: "coprime x p"
- by (metis gcd.commute p prime_nat_iff'' x0 xp)
+ by (simp add: ac_simps)
+ from x0 xp p have px: "coprime x p"
+ by (auto simp add: prime_nat_iff'' ac_simps)
obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
have "y \<noteq> 0"
@@ -104,8 +97,8 @@
assume "y = 0"
with y(2) have "p dvd a"
using cong_dvd_iff by auto
- then show False
- by (metis gcd_nat.absorb1 not_prime_1 p pa)
+ with not_prime_1 p pa show False
+ by (auto simp add: gcd_nat.order_iff)
qed
with y show ?thesis
by blast
@@ -128,9 +121,9 @@
obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
by blast
from ma nb x have "coprime x a" "coprime x b"
- by (metis cong_gcd_eq_nat)+
+ using cong_imp_coprime_nat cong_sym by blast+
then have "coprime x (a*b)"
- by (metis coprime_mul_eq)
+ by simp
with x show ?thesis
by blast
qed
@@ -164,7 +157,8 @@
from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
by simp
qed
- then show ?thesis by blast
+ then show ?thesis
+ by (auto intro: coprimeI)
qed
qed
@@ -216,8 +210,8 @@
from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
by simp
from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
- have an: "coprime a n" "coprime (a^(n - 1)) n"
- by (auto simp add: coprime_exp gcd.commute)
+ have an: "coprime a n" "coprime (a ^ (n - 1)) n"
+ using \<open>n \<ge> 2\<close> by simp_all
have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
proof -
from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
@@ -229,7 +223,7 @@
let ?y = "a^ ((n - 1) div m * m)"
note mdeq = div_mult_mod_eq[of "(n - 1)" m]
have yn: "coprime ?y n"
- by (metis an(1) coprime_exp gcd.commute)
+ using an(1) by (cases "(n - Suc 0) div m * m = 0") auto
have "?y mod n = (a^m)^((n - 1) div m) mod n"
by (simp add: algebra_simps power_mult)
also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
@@ -359,9 +353,11 @@
next
case (Suc d')
then have d0: "d \<noteq> 0" by simp
- from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
+ from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1"
+ by (auto elim: not_coprimeE)
from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
- by (metis prem d0 gcd.commute lucas_coprime_lemma)
+ using prem d0 lucas_coprime_lemma
+ by (auto elim: not_coprimeE simp add: ac_simps)
then have "a ^ d + n * q1 - n * q2 = 1" by simp
with dvd_diff_nat [OF dvd_add [OF divides_rexp]] dvd_mult2 Suc p have "p dvd 1"
by metis
@@ -398,8 +394,10 @@
qed
qed
-lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
- by (metis euler_theorem gcd.commute ord_divides that)
+lemma order_divides_totient:
+ "ord n a dvd totient n" if "coprime n a"
+ using that euler_theorem [of a n]
+ by (simp add: ord_divides [symmetric] ac_simps)
lemma order_divides_expdiff:
fixes n::nat and a::nat assumes na: "coprime n a"
@@ -412,11 +410,11 @@
from na ed have "\<exists>c. d = e + c" by presburger
then obtain c where c: "d = e + c" ..
from na have an: "coprime a n"
- by (metis gcd.commute)
- have aen: "coprime (a^e) n"
- by (metis coprime_exp gcd.commute na)
- have acn: "coprime (a^c) n"
- by (metis coprime_exp gcd.commute na)
+ by (simp add: ac_simps)
+ then have aen: "coprime (a ^ e) n"
+ by (cases "e > 0") simp_all
+ from an have acn: "coprime (a ^ c) n"
+ by (cases "c > 0") simp_all
from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
by simp
also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
@@ -620,8 +618,9 @@
by (metis cong_to_1_nat exps)
from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
using P0 by simp
- with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
- with p01 pn pd0 coprime_common_divisor_nat show False
+ with caP have "coprime (a ^ (ord p (a ^ r) * t * r) - 1) n"
+ by simp
+ with p01 pn pd0 coprime_common_divisor [of _ n p] show False
by auto
qed
with d have o: "ord p (a^r) = q" by simp
@@ -632,12 +631,14 @@
assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
from n have "n \<noteq> 0" by simp
- then have False using d dp pn
- by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
+ then have False using d dp pn an
+ by auto (metis One_nat_def Suc_lessI
+ \<open>1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)\<close> \<open>a ^ (q * r) = p * l * k + 1\<close> add_diff_cancel_left' dvd_diff_nat dvd_power dvd_triv_left gcd_nat.trans nat_dvd_not_less nqr zero_less_diff zero_less_one)
}
- then have cpa: "coprime p a" by auto
- have arp: "coprime (a^r) p"
- by (metis coprime_exp cpa gcd.commute)
+ then have cpa: "coprime p a"
+ by (auto intro: coprimeI)
+ then have arp: "coprime (a ^ r) p"
+ by (cases "r > 0") (simp_all add: ac_simps)
from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
by simp
then obtain d where d:"p - 1 = q * d"
--- a/src/HOL/Number_Theory/Residues.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Residues.thy Sat Nov 11 18:41:08 2017 +0000
@@ -106,13 +106,9 @@
lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
using m_gt_one
- unfolding Units_def R_def residue_ring_def
- apply auto
- apply (subgoal_tac "x \<noteq> 0")
- apply auto
- apply (metis invertible_coprime_int)
+ apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
apply (subst (asm) coprime_iff_invertible'_int)
- apply (auto simp add: cong_def mult.commute)
+ apply (auto simp add: cong_def)
done
lemma res_neg_eq: "\<ominus> x = (- x) mod m"
@@ -220,6 +216,22 @@
context residues_prime
begin
+lemma p_coprime_left:
+ "coprime p a \<longleftrightarrow> \<not> p dvd a"
+ using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
+
+lemma p_coprime_right:
+ "coprime a p \<longleftrightarrow> \<not> p dvd a"
+ using p_coprime_left [of a] by (simp add: ac_simps)
+
+lemma p_coprime_left_int:
+ "coprime (int p) a \<longleftrightarrow> \<not> int p dvd a"
+ using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
+
+lemma p_coprime_right_int:
+ "coprime a (int p) \<longleftrightarrow> \<not> int p dvd a"
+ using p_coprime_left_int [of a] by (simp add: ac_simps)
+
lemma is_field: "field R"
proof -
have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
@@ -231,9 +243,7 @@
lemma res_prime_units_eq: "Units R = {1..p - 1}"
apply (subst res_units_eq)
- apply auto
- apply (subst gcd.commute)
- apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
+ apply (auto simp add: p_coprime_right_int zdvd_not_zless)
done
end
@@ -246,26 +256,27 @@
subsection \<open>Euler's theorem\<close>
-lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
+lemma (in residues) totatives_eq:
+ "totatives (nat m) = nat ` Units R"
proof -
+ from m_gt_one have "\<bar>m\<bar> > 1"
+ by simp
+ then have "totatives (nat \<bar>m\<bar>) = nat ` abs ` Units R"
+ by (auto simp add: totatives_def res_units_eq image_iff le_less)
+ (use m_gt_one zless_nat_eq_int_zless in force)
+ moreover have "\<bar>m\<bar> = m" "abs ` Units R = Units R"
+ using m_gt_one by (auto simp add: res_units_eq image_iff)
+ ultimately show ?thesis
+ by simp
+qed
+
+lemma (in residues) totient_eq:
+ "totient (nat m) = card (Units R)"
+proof -
have *: "inj_on nat (Units R)"
by (rule inj_onI) (auto simp add: res_units_eq)
- define m' where "m' = nat m"
- from m_gt_one have "m = int m'" "m' > 1"
- by (simp_all add: m'_def)
- then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
- unfolding res_units_eq
- by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
- then have "Units R = int ` totatives m'"
- by blast
- then have "totatives m' = nat ` Units R"
- by (simp add: image_image)
- then have "card (totatives (nat m)) = card (nat ` Units R)"
- by (simp add: m'_def)
- also have "\<dots> = card (Units R)"
- using * card_image [of nat "Units R"] by auto
- finally show ?thesis
- by (simp add: totient_def)
+ then show ?thesis
+ by (simp add: totient_def totatives_eq card_image)
qed
lemma (in residues_prime) totient_eq: "totient p = p - 1"
--- a/src/HOL/Number_Theory/Totient.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Totient.thy Sat Nov 11 18:41:08 2017 +0000
@@ -15,7 +15,7 @@
definition totatives :: "nat \<Rightarrow> nat set" where
"totatives n = {k \<in> {0<..n}. coprime k n}"
-
+
lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
by (simp add: totatives_def)
@@ -60,7 +60,7 @@
lemma minus_one_in_totatives:
assumes "n \<ge> 2"
shows "n - 1 \<in> totatives n"
- using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff)
+ using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
lemma totatives_prime_power_Suc:
assumes "prime p"
@@ -72,7 +72,8 @@
fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
hence "coprime k (p ^ Suc n)"
- using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute)
+ using prime_imp_coprime [OF assms, of k]
+ by (cases "n > 0") (auto simp add: ac_simps)
with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
qed (auto simp: totatives_def)
@@ -101,14 +102,15 @@
proof safe
fix x assume "x \<in> totatives (m1 * m2)"
with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
- by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
+ using coprime_common_divisor [of x m1 m1] coprime_common_divisor [of x m2 m2]
+ by (auto simp add: in_totatives_iff mod_greater_zero_iff_not_dvd)
next
fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
from x ab assms(3) have "x \<in> totatives (m1 * m2)"
- by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
+ by (auto intro: ccontr simp add: in_totatives_iff)
with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
qed
qed
@@ -125,21 +127,18 @@
show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
proof (intro equalityI subsetI, goal_cases)
case (1 k)
- thus ?case using assms
- by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d]
- gcd_mult_right gcd.commute)
+ then show ?case using assms
+ by (auto elim: dvdE simp add: in_totatives_iff ac_simps gcd_mult_right)
next
case (2 k)
hence "d dvd k" by auto
then obtain l where k: "k = l * d" by (elim dvdE) auto
- from 2 and assms show ?case unfolding k
- by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d]
- gcd_mult_right elim!: dvdE)
+ from 2 assms show ?case
+ using gcd_mult_right [of _ d l]
+ by (auto intro: gcd_eq_1_imp_coprime elim!: dvdE simp add: k image_iff in_totatives_iff ac_simps)
qed
qed
-
-
definition totient :: "nat \<Rightarrow> nat" where
"totient n = card (totatives n)"
@@ -272,7 +271,8 @@
proof -
from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
- from that and nz have "\<not>coprime x p" by auto
+ from that and nz have "\<not>coprime x p"
+ by (auto elim: dvdE)
hence "x \<notin> totatives p" by (simp add: totatives_def)
also note *
finally show False using that and le by auto
@@ -299,7 +299,8 @@
by simp_all
lemma totient_6 [simp]: "totient 6 = 2"
- using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat)
+ using totient_mult_coprime [of 2 3] coprime_add_one_right [of 2]
+ by simp
lemma totient_even:
assumes "n > 2"
@@ -314,11 +315,14 @@
have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
then obtain m where m: "n = p ^ k * m" by (elim dvdE)
with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
- from k_def m_pos p have "\<not>p dvd m"
+ from k_def m_pos p have "\<not> p dvd m"
by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib
prime_elem_multiplicity_eq_zero_iff)
- hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)])
- thus ?thesis using p k_pos \<open>odd p\<close>
+ with \<open>prime p\<close> have "coprime p m"
+ by (rule prime_imp_coprime)
+ with \<open>k > 0\<close> have "coprime (p ^ k) m"
+ by simp
+ then show ?thesis using p k_pos \<open>odd p\<close>
by (auto simp add: m totient_mult_coprime totient_prime_power)
next
case False
@@ -341,7 +345,7 @@
proof (induction A rule: infinite_finite_induct)
case (insert x A)
have *: "coprime (prod f A) (f x)"
- proof (rule prod_coprime)
+ proof (rule prod_coprime_left)
fix y
assume "y \<in> A"
with \<open>x \<notin> A\<close> have "y \<noteq> x"
@@ -388,10 +392,12 @@
proof (rule totient_prod_coprime)
show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
proof (rule pairwiseI, clarify)
- fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n"
+ fix p q assume *: "p \<in># prime_factorization n" "q \<in># prime_factorization n"
"p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
- thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
- by (intro coprime_exp2 primes_coprime[of p q]) auto
+ then have "multiplicity p n > 0" "multiplicity q n > 0"
+ by (simp_all add: prime_factors_multiplicity)
+ with * primes_coprime [of p q] show "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
+ by auto
qed
next
show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
@@ -475,20 +481,22 @@
by (subst totient_gcd [symmetric]) simp
lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
- using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff)
+ by (fact of_nat_eq_1_iff)
(* TODO Move *)
-lemma gcd_2_odd:
+lemma odd_imp_coprime_nat:
assumes "odd (n::nat)"
- shows "gcd n 2 = 1"
+ shows "coprime n 2"
proof -
from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
- have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat)
- thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all
+ have "coprime (Suc (2 * k)) (2 * k)"
+ by (fact coprime_Suc_left_nat)
+ then show ?thesis using n
+ by simp
qed
lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
- by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd)
+ by (simp add: totient_mult ac_simps odd_imp_coprime_nat)
lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
proof (induction m arbitrary: n)
--- a/src/HOL/Parity.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Parity.thy Sat Nov 11 18:41:08 2017 +0000
@@ -318,6 +318,38 @@
using mult_div_mod_eq [of 2 a]
by (simp add: even_iff_mod_2_eq_zero)
+lemma coprime_left_2_iff_odd [simp]:
+ "coprime 2 a \<longleftrightarrow> odd a"
+proof
+ assume "odd a"
+ show "coprime 2 a"
+ proof (rule coprimeI)
+ fix b
+ assume "b dvd 2" "b dvd a"
+ then have "b dvd a mod 2"
+ by (auto intro: dvd_mod)
+ with \<open>odd a\<close> show "is_unit b"
+ by (simp add: mod_2_eq_odd)
+ qed
+next
+ assume "coprime 2 a"
+ show "odd a"
+ proof (rule notI)
+ assume "even a"
+ then obtain b where "a = 2 * b" ..
+ with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
+ by simp
+ moreover have "\<not> coprime 2 (2 * b)"
+ by (rule not_coprimeI [of 2]) simp_all
+ ultimately show False
+ by blast
+ qed
+qed
+
+lemma coprime_right_2_iff_odd [simp]:
+ "coprime a 2 \<longleftrightarrow> odd a"
+ using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
+
end
class ring_parity = ring + semiring_parity
--- a/src/HOL/Rat.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Rat.thy Sat Nov 11 18:41:08 2017 +0000
@@ -999,7 +999,7 @@
proof (cases p)
case (Fract a b)
then show ?thesis
- by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
+ by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract ac_simps)
qed
lemma rat_divide_code [code abstract]:
@@ -1008,9 +1008,10 @@
in normalize (a * d, c * b))"
by (cases p, cases q) (simp add: quotient_of_Fract)
-lemma rat_abs_code [code abstract]: "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
+lemma rat_abs_code [code abstract]:
+ "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
by (cases p) (simp add: quotient_of_Fract)
-
+
lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
proof (cases p)
case (Fract a b)
--- a/src/HOL/Real.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Real.thy Sat Nov 11 18:41:08 2017 +0000
@@ -1245,7 +1245,7 @@
lemma Rats_abs_nat_div_natE:
assumes "x \<in> \<rat>"
- obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
+ obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "coprime m n"
proof -
from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n"
by (auto simp add: Rats_eq_int_div_nat)
@@ -1281,6 +1281,8 @@
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
with gcd show ?thesis by auto
qed
+ then have "coprime ?k ?l"
+ by (simp only: coprime_iff_gcd_eq_1)
ultimately show ?thesis ..
qed
@@ -1415,8 +1417,6 @@
for m :: nat
by (metis not_le real_of_nat_less_numeral_iff)
-declare of_int_floor_le [simp] (* FIXME duplicate!? *)
-
lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
by (metis floor_of_int)
@@ -1424,7 +1424,7 @@
by linarith
lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
- by linarith
+ by (fact floor_unique)
lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
by linarith
--- a/src/HOL/Rings.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Rings.thy Sat Nov 11 18:41:08 2017 +0000
@@ -1161,6 +1161,108 @@
"is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
+
+text \<open>Coprimality\<close>
+
+definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)"
+
+lemma coprimeI:
+ assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c"
+ shows "coprime a b"
+ using assms by (auto simp: coprime_def)
+
+lemma not_coprimeI:
+ assumes "c dvd a" and "c dvd b" and "\<not> is_unit c"
+ shows "\<not> coprime a b"
+ using assms by (auto simp: coprime_def)
+
+lemma coprime_common_divisor:
+ "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
+ using that by (auto simp: coprime_def)
+
+lemma not_coprimeE:
+ assumes "\<not> coprime a b"
+ obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c"
+ using assms by (auto simp: coprime_def)
+
+lemma coprime_imp_coprime:
+ "coprime a b" if "coprime c d"
+ and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c"
+ and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d"
+proof (rule coprimeI)
+ fix e
+ assume "e dvd a" and "e dvd b"
+ with that have "e dvd c" and "e dvd d"
+ by (auto intro: dvd_trans)
+ with \<open>coprime c d\<close> show "is_unit e"
+ by (rule coprime_common_divisor)
+qed
+
+lemma coprime_divisors:
+ "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
+using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
+ fix e
+ assume "e dvd a" then show "e dvd c"
+ using \<open>a dvd c\<close> by (rule dvd_trans)
+ assume "e dvd b" then show "e dvd d"
+ using \<open>b dvd d\<close> by (rule dvd_trans)
+qed
+
+lemma coprime_self [simp]:
+ "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
+proof
+ assume ?P
+ then show ?Q
+ by (rule coprime_common_divisor) simp_all
+next
+ assume ?Q
+ show ?P
+ by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
+qed
+
+lemma coprime_commute [ac_simps]:
+ "coprime b a \<longleftrightarrow> coprime a b"
+ unfolding coprime_def by auto
+
+lemma is_unit_left_imp_coprime:
+ "coprime a b" if "is_unit a"
+proof (rule coprimeI)
+ fix c
+ assume "c dvd a"
+ with that show "is_unit c"
+ by (auto intro: dvd_unit_imp_unit)
+qed
+
+lemma is_unit_right_imp_coprime:
+ "coprime a b" if "is_unit b"
+ using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)
+
+lemma coprime_1_left [simp]:
+ "coprime 1 a"
+ by (rule coprimeI)
+
+lemma coprime_1_right [simp]:
+ "coprime a 1"
+ by (rule coprimeI)
+
+lemma coprime_0_left_iff [simp]:
+ "coprime 0 a \<longleftrightarrow> is_unit a"
+ by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])
+
+lemma coprime_0_right_iff [simp]:
+ "coprime a 0 \<longleftrightarrow> is_unit a"
+ using coprime_0_left_iff [of a] by (simp add: ac_simps)
+
+lemma coprime_mult_self_left_iff [simp]:
+ "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b"
+ by (auto intro: coprime_common_divisor)
+ (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+
+
+lemma coprime_mult_self_right_iff [simp]:
+ "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
+ using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
+
end
class unit_factor =
@@ -1430,6 +1532,14 @@
shows "is_unit a \<longleftrightarrow> a = 1"
using assms by (cases "a = 0") (auto dest: is_unit_normalize)
+lemma coprime_normalize_left_iff [simp]:
+ "coprime (normalize a) b \<longleftrightarrow> coprime a b"
+ by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+
+lemma coprime_normalize_right_iff [simp]:
+ "coprime a (normalize b) \<longleftrightarrow> coprime a b"
+ using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)
+
text \<open>
We avoid an explicit definition of associated elements but prefer explicit
normalisation instead. In theory we could define an abbreviation like @{prop
@@ -2435,8 +2545,8 @@
subclass ordered_ring_abs
by standard (auto simp: abs_if not_less mult_less_0_iff)
-lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
- by (simp add: abs_if)
+lemma abs_mult_self: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
+ by (fact abs_mult_self_eq)
lemma abs_mult_less:
assumes ac: "\<bar>a\<bar> < c"
--- a/src/HOL/Set.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Set.thy Sat Nov 11 18:41:08 2017 +0000
@@ -1874,6 +1874,11 @@
lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
by (auto simp: pairwise_def)
+lemma pairwise_imageI:
+ "pairwise P (f ` A)"
+ if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)"
+ using that by (auto intro: pairwiseI)
+
lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
by (force simp: pairwise_def)