dedicated definition for coprimality
authorhaftmann
Sat Nov 11 18:41:08 2017 +0000 (17 months ago)
changeset 67051e7e54a0b9197
parent 67050 1e29e2666a15
child 67052 caf87d4b9b61
dedicated definition for coprimality
NEWS
src/Doc/Corec/Corec.thy
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Computational_Algebra/Factorial_Ring.thy
src/HOL/Computational_Algebra/Normalized_Fraction.thy
src/HOL/Computational_Algebra/Nth_Powers.thy
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/Computational_Algebra/Primes.thy
src/HOL/Computational_Algebra/Squarefree.thy
src/HOL/Corec_Examples/Paper_Examples.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Euclidean_Division.thy
src/HOL/GCD.thy
src/HOL/Isar_Examples/Fibonacci.thy
src/HOL/Library/Multiset.thy
src/HOL/Map.thy
src/HOL/Nitpick.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Euler_Criterion.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/Totient.thy
src/HOL/Parity.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/Set.thy
     1.1 --- a/NEWS	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/NEWS	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -89,7 +89,10 @@
     1.4  * Class linordered_semiring_1 covers zero_less_one also, ruling out
     1.5  pathologic instances. Minor INCOMPATIBILITY.
     1.6  
     1.7 -* Removed nat-int transfer machinery.  Rare INCOMPATIBILITY.
     1.8 +* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
     1.9 +
    1.10 +* Predicate coprime is now a real definition, not a mere
    1.11 +abbreviation. INCOMPATIBILITY.
    1.12  
    1.13  
    1.14  *** System ***
     2.1 --- a/src/Doc/Corec/Corec.thy	Sat Nov 11 18:33:35 2017 +0000
     2.2 +++ b/src/Doc/Corec/Corec.thy	Sat Nov 11 18:41:08 2017 +0000
     2.3 @@ -334,9 +334,9 @@
     2.4            primes m (n + 1))"
     2.5        apply (relation "measure (\<lambda>(m, n).
     2.6          if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
     2.7 -       apply (auto simp: mod_Suc intro: Suc_lessI)
     2.8 -       apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
     2.9 -      by (metis diff_less_mono2 lessI mod_less_divisor)
    2.10 +       apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
    2.11 +      apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
    2.12 +      done
    2.13  
    2.14  text \<open>
    2.15  \noindent
     3.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat Nov 11 18:33:35 2017 +0000
     3.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sat Nov 11 18:41:08 2017 +0000
     3.3 @@ -139,7 +139,7 @@
     3.4  
     3.5  (* Deviates from the definition given in the library in number theory *)
     3.6  definition phi' :: "nat => nat"
     3.7 -  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
     3.8 +  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
     3.9  
    3.10  notation (latex output)
    3.11    phi' ("\<phi> _")
    3.12 @@ -148,8 +148,8 @@
    3.13    assumes "m > 0"
    3.14    shows "phi' m > 0"
    3.15  proof -
    3.16 -  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
    3.17 -  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
    3.18 +  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp
    3.19 +  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)
    3.20    thus ?thesis unfolding phi'_def by simp
    3.21  qed
    3.22  
    3.23 @@ -232,7 +232,7 @@
    3.24            by (simp add: gcd_mult_distrib_nat q ac_simps)
    3.25          hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
    3.26          hence "a * n div d \<in> ?F"
    3.27 -          using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
    3.28 +          using ge_1 le_n by (fastforce simp add: `d dvd n`)
    3.29        } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
    3.30        { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
    3.31          hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
    3.32 @@ -256,7 +256,7 @@
    3.33      proof
    3.34        fix m assume m: "m \<in> ?R"
    3.35        thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
    3.36 -        by (simp add: dvd_mult_div_cancel)
    3.37 +        by simp
    3.38      qed
    3.39    qed fastforce
    3.40    finally show ?thesis by force
    3.41 @@ -329,7 +329,7 @@
    3.42  lemma ord_min:
    3.43    assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
    3.44  proof -
    3.45 -  def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
    3.46 +  define Ord where "Ord = {d \<in> {1..order G}. a (^) d = \<one>}"
    3.47    have fin: "finite Ord" by (auto simp: Ord_def)
    3.48    have in_ord: "ord a \<in> Ord"
    3.49      using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
    3.50 @@ -411,7 +411,7 @@
    3.51    show "?R \<subseteq> ?L" by blast
    3.52    { fix y assume "y \<in> ?L"
    3.53      then obtain x::nat where x:"y = a(^)x" by auto
    3.54 -    def r \<equiv> "x mod ord a"
    3.55 +    define r where "r = x mod ord a"
    3.56      then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
    3.57      hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
    3.58        using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
    3.59 @@ -427,7 +427,7 @@
    3.60    assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
    3.61    shows "ord a dvd k"
    3.62  proof -
    3.63 -  def r \<equiv> "k mod ord a"
    3.64 +  define r where "r = k mod ord a"
    3.65    then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
    3.66    hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
    3.67        using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
    3.68 @@ -486,15 +486,16 @@
    3.69      proof -
    3.70        have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
    3.71          using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
    3.72 -      thus ?thesis by (simp add: gcd.commute)
    3.73 +      thus ?thesis by (simp add: ac_simps)
    3.74      qed
    3.75      have dvd_d:"(ord a div gcd n (ord a)) dvd d"
    3.76      proof -
    3.77        have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
    3.78          by (metis dvd_triv_right mult.commute)
    3.79        hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
    3.80 -        by (simp add:  mult.commute)
    3.81 -      thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
    3.82 +        by (simp add: mult.commute)
    3.83 +      then show ?thesis
    3.84 +        using cp by (simp add: coprime_dvd_mult_left_iff)
    3.85      qed
    3.86      have "d > 0" using d_elem by simp
    3.87      hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
    3.88 @@ -744,7 +745,8 @@
    3.89    shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
    3.90  proof
    3.91    assume A: ?L then show ?R
    3.92 -    using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
    3.93 +    using assms ord_ge_1 [OF assms]
    3.94 +    by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1)
    3.95  next
    3.96    assume ?R then show ?L
    3.97      using ord_pow_dvd_ord_elem[OF assms, of k] by auto
     4.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Nov 11 18:33:35 2017 +0000
     4.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Nov 11 18:41:08 2017 +0000
     4.3 @@ -13,12 +13,6 @@
     4.4  
     4.5  subsection \<open>Irreducible and prime elements\<close>
     4.6  
     4.7 -(* TODO: Move ? *)
     4.8 -lemma (in semiring_gcd) prod_coprime' [rule_format]: 
     4.9 -    "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
    4.10 -  using prod_coprime[of A f a] by (simp add: gcd.commute)
    4.11 -
    4.12 -
    4.13  context comm_semiring_1
    4.14  begin
    4.15  
    4.16 @@ -583,7 +577,7 @@
    4.17  end
    4.18  
    4.19  
    4.20 -subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
    4.21 +subsection \<open>In a semiring with GCD, each irreducible element is a prime element\<close>
    4.22  
    4.23  context semiring_gcd
    4.24  begin
    4.25 @@ -620,23 +614,26 @@
    4.26    using assms by (simp add: prime_elem_imp_coprime)
    4.27  
    4.28  lemma prime_elem_imp_power_coprime:
    4.29 -  "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
    4.30 -  by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
    4.31 +  "prime_elem p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
    4.32 +  by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps)
    4.33  
    4.34  lemma prime_imp_power_coprime:
    4.35 -  "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
    4.36 -  by (simp add: prime_elem_imp_power_coprime)
    4.37 +  "prime p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
    4.38 +  by (rule prime_elem_imp_power_coprime) simp_all
    4.39  
    4.40  lemma prime_elem_divprod_pow:
    4.41    assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
    4.42    shows   "p^n dvd a \<or> p^n dvd b"
    4.43    using assms
    4.44  proof -
    4.45 -  from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
    4.46 -    by (auto simp: coprime prime_elem_def)
    4.47 -  with p have "coprime (p^n) a \<or> coprime (p^n) b"
    4.48 -    by (auto intro: prime_elem_imp_coprime coprime_exp_left)
    4.49 -  with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
    4.50 +  from p have "\<not> is_unit p"
    4.51 +    by simp
    4.52 +  with ab p have "\<not> p dvd a \<or> \<not> p dvd b"
    4.53 +    using not_coprimeI by blast
    4.54 +  with p have "coprime (p ^ n) a \<or> coprime (p ^ n) b"
    4.55 +    by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps)
    4.56 +  with pab show ?thesis
    4.57 +    by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff)
    4.58  qed
    4.59  
    4.60  lemma primes_coprime:
    4.61 @@ -1524,6 +1521,27 @@
    4.62      with assms[of P] assms[of Q] PQ show "P = Q" by simp
    4.63  qed
    4.64  
    4.65 +lemma divides_primepow:
    4.66 +  assumes "prime p" and "a dvd p ^ n"
    4.67 +  obtains m where "m \<le> n" and "normalize a = p ^ m"
    4.68 +proof -
    4.69 +  from assms have "a \<noteq> 0"
    4.70 +    by auto
    4.71 +  with assms
    4.72 +  have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
    4.73 +    by (simp add: prod_mset_prime_factorization)
    4.74 +  then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
    4.75 +    by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
    4.76 +  with assms have "prime_factorization a \<subseteq># replicate_mset n p"
    4.77 +    by (simp add: prime_factorization_prime_power)
    4.78 +  then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
    4.79 +    by (rule msubseteq_replicate_msetE)
    4.80 +  then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
    4.81 +    by simp
    4.82 +  with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
    4.83 +    by (simp add: prod_mset_prime_factorization)
    4.84 +  with \<open>m \<le> n\<close> show thesis ..
    4.85 +qed
    4.86  
    4.87  
    4.88  subsection \<open>GCD and LCM computation with unique factorizations\<close>
     5.1 --- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Sat Nov 11 18:33:35 2017 +0000
     5.2 +++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Sat Nov 11 18:41:08 2017 +0000
     5.3 @@ -16,6 +16,15 @@
     5.4    "normalize_quot = 
     5.5       (\<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))" 
     5.6  
     5.7 +lemma normalize_quot_zero [simp]:
     5.8 +  "normalize_quot (a, 0) = (0, 1)"
     5.9 +  by (simp add: normalize_quot_def)
    5.10 +
    5.11 +lemma normalize_quot_proj [simp]:
    5.12 +  "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
    5.13 +  "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
    5.14 +  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')
    5.15 +
    5.16  definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where
    5.17    "normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}"
    5.18    
    5.19 @@ -61,8 +70,8 @@
    5.20    
    5.21  lemma coprime_normalize_quot:
    5.22    "coprime (fst (normalize_quot x)) (snd (normalize_quot x))"
    5.23 -  by (simp add: normalize_quot_def case_prod_unfold Let_def
    5.24 -        div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime)
    5.25 +  by (simp add: normalize_quot_def case_prod_unfold div_mult_unit2)
    5.26 +    (metis coprime_mult_self_right_iff div_gcd_coprime unit_div_mult_self unit_factor_is_unit)
    5.27  
    5.28  lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts"
    5.29    by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold)
    5.30 @@ -203,15 +212,26 @@
    5.31       and  "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))"
    5.32    shows   "normalize_quot (a * c, b * d) = (e * g, f * h)"
    5.33  proof (rule normalize_quotI)
    5.34 +  from assms have "gcd a b = 1" "gcd c d = 1"
    5.35 +    by simp_all
    5.36    from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
    5.37 -  from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms]
    5.38 -  from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms]
    5.39 -  from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all)
    5.40 +  with assms have "normalize b = b" "normalize d = d"
    5.41 +    by (auto intro: normalize_unit_factor_eqI)
    5.42 +  from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
    5.43 +  note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
    5.44 +  from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
    5.45 +  note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
    5.46 +  from k l show "a * c * (f * h) = b * d * (e * g)"
    5.47 +    by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
    5.48    from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1"
    5.49      by simp_all
    5.50    from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot)
    5.51 -  with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts"
    5.52 -    by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq')
    5.53 +  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>
    5.54 +    \<open>normalize b = b\<close> \<open>normalize d = d\<close>
    5.55 +  show "(e * g, f * h) \<in> normalized_fracts"
    5.56 +    by (simp add: normalized_fracts_def unit_factor_mult e_def f_def g_def h_def
    5.57 +      coprime_normalize_quot dvd_unit_factor_div unit_factor_gcd)
    5.58 +      (metis coprime_mult_left_iff coprime_mult_right_iff)
    5.59  qed (insert assms(3,4), auto)
    5.60  
    5.61  lemma normalize_quot_mult:
    5.62 @@ -230,8 +250,8 @@
    5.63       (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
    5.64            (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
    5.65        in  (e*g, f*h))"
    5.66 -  by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric]
    5.67 -                 coprime_normalize_quot normalize_quot_mult [symmetric])
    5.68 +  by transfer
    5.69 +     (simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime)
    5.70    
    5.71  lemma normalize_quot_0 [simp]: 
    5.72      "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)"
    5.73 @@ -254,7 +274,9 @@
    5.74      by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
    5.75    have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
    5.76    thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
    5.77 -    using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute)
    5.78 +    using assms(1,2) d
    5.79 +    by (auto simp: normalized_fracts_def ac_simps)
    5.80 +      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
    5.81  qed fact+
    5.82    
    5.83  lemma quot_of_fract_inverse:
    5.84 @@ -274,12 +296,19 @@
    5.85    shows "normalize_quot (x div u, y) = (x' div u, y')"
    5.86  proof (cases "y = 0")
    5.87    case False
    5.88 -  from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
    5.89 -  from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
    5.90 -  with False d \<open>is_unit u\<close> show ?thesis
    5.91 -    by (intro normalize_quotI)
    5.92 -       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
    5.93 -          gcd_div_unit1)
    5.94 +  define v where "v = 1 div u"
    5.95 +  with \<open>is_unit u\<close> have "is_unit v" and u: "\<And>a. a div u = a * v"
    5.96 +    by simp_all
    5.97 +  from \<open>is_unit v\<close> have "coprime v = top"
    5.98 +    by (simp add: fun_eq_iff is_unit_left_imp_coprime)
    5.99 +  from normalize_quotE[OF False, of x] guess d .
   5.100 +  note d = this[folded assms(2,3)]
   5.101 +  from assms have "coprime x' y'" "unit_factor y' = 1"
   5.102 +    by (simp_all add: coprime_normalize_quot)
   5.103 +  with d \<open>coprime v = top\<close> have "normalize_quot (x * v, y) = (x' * v, y')"
   5.104 +    by (auto simp: normalized_fracts_def intro: normalize_quotI)
   5.105 +  then show ?thesis
   5.106 +    by (simp add: u)
   5.107  qed (simp_all add: assms)
   5.108  
   5.109  lemma normalize_quot_div_unit_right:
   5.110 @@ -291,10 +320,8 @@
   5.111    case False
   5.112    from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
   5.113    from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
   5.114 -  with False d \<open>is_unit u\<close> show ?thesis
   5.115 -    by (intro normalize_quotI)
   5.116 -       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
   5.117 -          gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric])
   5.118 +  with d \<open>is_unit u\<close> show ?thesis
   5.119 +    by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
   5.120  qed (simp_all add: assms)
   5.121  
   5.122  lemma normalize_quot_normalize_left:
     6.1 --- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Sat Nov 11 18:33:35 2017 +0000
     6.2 +++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Sat Nov 11 18:41:08 2017 +0000
     6.3 @@ -111,9 +111,10 @@
     6.4      ultimately show "n dvd multiplicity p a"
     6.5        by (auto simp: not_dvd_imp_multiplicity_0)
     6.6    qed
     6.7 -  from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
     6.8 -  from A[of b a] assms show "is_nth_power n b" 
     6.9 -    by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
    6.10 +  from A [of a b] assms show "is_nth_power n a"
    6.11 +    by (cases "n = 0") simp_all
    6.12 +  from A [of b a] assms show "is_nth_power n b"
    6.13 +    by (cases "n = 0") (simp_all add: ac_simps)
    6.14  qed
    6.15      
    6.16  lemma is_nth_power_mult_coprime_nat_iff:
     7.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 11 18:33:35 2017 +0000
     7.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 11 18:41:08 2017 +0000
     7.3 @@ -171,7 +171,7 @@
     7.4    hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
     7.5    hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
     7.6    moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
     7.7 -    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
     7.8 +    by (simp_all add: a_def b_def coprime_quot_of_fract [of c] ac_simps
     7.9            normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
    7.10    ultimately show ?thesis by (intro that[of a b])
    7.11  qed
    7.12 @@ -513,9 +513,12 @@
    7.13     from fract_poly_smult_eqE[OF this] guess a b . note ab = this
    7.14     hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
    7.15     with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
    7.16 -   hence "normalize b = gcd a b" by simp
    7.17 -   also from ab(3) have "\<dots> = 1" .
    7.18 -   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
    7.19 +   then have "normalize b = gcd a b"
    7.20 +     by simp
    7.21 +   with \<open>coprime a b\<close> have "normalize b = 1"
    7.22 +     by simp
    7.23 +   then have "a = 1" "is_unit b"
    7.24 +     by (simp_all add: a normalize_1_iff)
    7.25     
    7.26     note eq
    7.27     also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
    7.28 @@ -676,7 +679,8 @@
    7.29      from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
    7.30      from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
    7.31      with assms content_e have "a = normalize b" by (simp add: ab(4))
    7.32 -    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
    7.33 +    with ab have ab': "a = 1" "is_unit b"
    7.34 +      by (simp_all add: normalize_1_iff)
    7.35      with ab ab' have "c' = to_fract b" by auto
    7.36      from this and \<open>is_unit b\<close> show ?thesis by (rule that)
    7.37    qed
     8.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sat Nov 11 18:33:35 2017 +0000
     8.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sat Nov 11 18:41:08 2017 +0000
     8.3 @@ -245,9 +245,9 @@
     8.4    using prime_power_cancel [OF assms] assms by auto
     8.5  
     8.6  lemma prime_power_canonical:
     8.7 -  fixes m::nat
     8.8 +  fixes m :: nat
     8.9    assumes "prime p" "m > 0"
    8.10 -  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
    8.11 +  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k"
    8.12  using \<open>m > 0\<close>
    8.13  proof (induction m rule: less_induct)
    8.14    case (less m)
    8.15 @@ -381,9 +381,9 @@
    8.16  
    8.17  (* TODO: Generalise? *)
    8.18  lemma prime_power_mult_nat:
    8.19 -  fixes p::nat
    8.20 +  fixes p :: nat
    8.21    assumes p: "prime p" and xy: "x * y = p ^ k"
    8.22 -  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
    8.23 +  shows "\<exists>i j. x = p ^ i \<and> y = p^ j"
    8.24  using xy
    8.25  proof(induct k arbitrary: x y)
    8.26    case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
    8.27 @@ -429,25 +429,10 @@
    8.28  qed
    8.29  
    8.30  lemma divides_primepow_nat:
    8.31 -  fixes p::nat
    8.32 +  fixes p :: nat
    8.33    assumes p: "prime p"
    8.34 -  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
    8.35 -proof
    8.36 -  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
    8.37 -    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
    8.38 -  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
    8.39 -  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
    8.40 -  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
    8.41 -  hence "i \<le> k" by arith
    8.42 -  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
    8.43 -next
    8.44 -  {fix i assume H: "i \<le> k" "d = p^i"
    8.45 -    then obtain j where j: "k = i + j"
    8.46 -      by (metis le_add_diff_inverse)
    8.47 -    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
    8.48 -    hence "d dvd p^k" unfolding dvd_def by auto}
    8.49 -  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
    8.50 -qed
    8.51 +  shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)"
    8.52 +  using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
    8.53  
    8.54  
    8.55  subsection \<open>Chinese Remainder Theorem Variants\<close>
    8.56 @@ -481,8 +466,8 @@
    8.57    from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
    8.58    obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
    8.59      and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
    8.60 -  then have d12: "d1 = 1" "d2 =1"
    8.61 -    by (metis ab coprime_nat)+
    8.62 +  then have d12: "d1 = 1" "d2 = 1"
    8.63 +    using ab coprime_common_divisor_nat [of a b] by blast+
    8.64    let ?x = "v * a * x1 + u * b * x2"
    8.65    let ?q1 = "v * x1 + u * y2"
    8.66    let ?q2 = "v * y1 + u * x2"
    8.67 @@ -497,14 +482,14 @@
    8.68  lemma coprime_bezout_strong:
    8.69    fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
    8.70    shows "\<exists>x y. a * x = b * y + 1"
    8.71 -by (metis assms bezout_nat gcd_nat.left_neutral)
    8.72 +  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)
    8.73  
    8.74  lemma bezout_prime:
    8.75    assumes p: "prime p" and pa: "\<not> p dvd a"
    8.76    shows "\<exists>x y. a*x = Suc (p*y)"
    8.77  proof -
    8.78    have ap: "coprime a p"
    8.79 -    by (metis gcd.commute p pa prime_imp_coprime)
    8.80 +    using coprime_commute p pa prime_imp_coprime by auto
    8.81    moreover from p have "p \<noteq> 1" by auto
    8.82    ultimately have "\<exists>x y. a * x = p * y + 1"
    8.83      by (rule coprime_bezout_strong)
     9.1 --- a/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:33:35 2017 +0000
     9.2 +++ b/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:41:08 2017 +0000
     9.3 @@ -116,13 +116,16 @@
     9.4    show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
     9.5    proof
     9.6      fix p assume p: "p \<in> prime_factors (a * b)"
     9.7 -    {
     9.8 +    with nz have "prime p"
     9.9 +      by (simp add: prime_factors_dvd)
    9.10 +    have "\<not> (p dvd a \<and> p dvd b)"
    9.11 +    proof
    9.12        assume "p dvd a \<and> p dvd b"
    9.13 -      hence "p dvd gcd a b" by simp
    9.14 -      also have "gcd a b = 1" by fact
    9.15 -      finally have False using nz using p by (auto simp: prime_factors_dvd)
    9.16 -    }
    9.17 -    hence "\<not>(p dvd a \<and> p dvd b)" by blast
    9.18 +      with \<open>coprime a b\<close> have "is_unit p"
    9.19 +        by (auto intro: coprime_common_divisor)
    9.20 +      with \<open>prime p\<close> show False
    9.21 +        by simp
    9.22 +    qed
    9.23      moreover from p have "p dvd a \<or> p dvd b" using nz 
    9.24        by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
    9.25      ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
    9.26 @@ -138,7 +141,7 @@
    9.27    shows   "squarefree (prod f A)"
    9.28    using assms 
    9.29    by (induction A rule: infinite_finite_induct) 
    9.30 -     (auto intro!: squarefree_mult_coprime prod_coprime')
    9.31 +     (auto intro!: squarefree_mult_coprime prod_coprime_right)
    9.32  
    9.33  lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
    9.34    by (cases m) (auto dest: squarefree_multD)
    10.1 --- a/src/HOL/Corec_Examples/Paper_Examples.thy	Sat Nov 11 18:33:35 2017 +0000
    10.2 +++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Sat Nov 11 18:41:08 2017 +0000
    10.3 @@ -96,9 +96,9 @@
    10.4  where "primes m n =
    10.5    (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
    10.6  apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
    10.7 -apply (auto simp: mod_Suc intro: Suc_lessI )
    10.8 -apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
    10.9 -by (metis diff_less_mono2 lessI mod_less_divisor)
   10.10 +   apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
   10.11 +   apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
   10.12 +  done
   10.13  
   10.14  corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
   10.15  where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
    11.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:33:35 2017 +0000
    11.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:41:08 2017 +0000
    11.3 @@ -51,7 +51,8 @@
    11.4      from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
    11.5      have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
    11.6      from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
    11.7 -    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
    11.8 +    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1"
    11.9 +      by simp
   11.10      from ab consider "b < 0" | "b > 0" by arith
   11.11      then show ?thesis
   11.12      proof cases
   11.13 @@ -198,6 +199,8 @@
   11.14      from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
   11.15      have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
   11.16        by (simp_all add: x y isnormNum_def add: gcd.commute)
   11.17 +    then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
   11.18 +      by (simp_all add: coprime_iff_gcd_eq_1)
   11.19      from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
   11.20        apply -
   11.21        apply algebra
   11.22 @@ -205,11 +208,11 @@
   11.23        apply simp
   11.24        apply algebra
   11.25        done
   11.26 -    from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
   11.27 -        coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
   11.28 -      have eq1: "b = b'" using pos by arith
   11.29 -      with eq have "a = a'" using pos by simp
   11.30 -      with eq1 show ?thesis by (simp add: x y)
   11.31 +    then have eq1: "b = b'"
   11.32 +      using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
   11.33 +      by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
   11.34 +    with eq have "a = a'" using pos by simp
   11.35 +    with \<open>b = b'\<close> show ?thesis by (simp add: x y)
   11.36    qed
   11.37    show ?lhs if ?rhs
   11.38      using that by simp
    12.1 --- a/src/HOL/Euclidean_Division.thy	Sat Nov 11 18:33:35 2017 +0000
    12.2 +++ b/src/HOL/Euclidean_Division.thy	Sat Nov 11 18:41:08 2017 +0000
    12.3 @@ -125,6 +125,15 @@
    12.4    "a mod b = 0" if "is_unit b"
    12.5    using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
    12.6  
    12.7 +lemma coprime_mod_left_iff [simp]:
    12.8 +  "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
    12.9 +  by (rule; rule coprimeI)
   12.10 +    (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
   12.11 +
   12.12 +lemma coprime_mod_right_iff [simp]:
   12.13 +  "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0"
   12.14 +  using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)
   12.15 +
   12.16  end
   12.17  
   12.18  class euclidean_ring = idom_modulo + euclidean_semiring
   12.19 @@ -533,6 +542,10 @@
   12.20    with that show thesis .
   12.21  qed
   12.22  
   12.23 +lemma invertible_coprime:
   12.24 +  "coprime a c" if "a * b mod c = 1"
   12.25 +  by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)
   12.26 +
   12.27  end
   12.28  
   12.29    
   12.30 @@ -772,6 +785,18 @@
   12.31  
   12.32  end
   12.33  
   12.34 +lemma coprime_Suc_0_left [simp]:
   12.35 +  "coprime (Suc 0) n"
   12.36 +  using coprime_1_left [of n] by simp
   12.37 +
   12.38 +lemma coprime_Suc_0_right [simp]:
   12.39 +  "coprime n (Suc 0)"
   12.40 +  using coprime_1_right [of n] by simp
   12.41 +
   12.42 +lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   12.43 +  for a b :: nat
   12.44 +  by (drule coprime_common_divisor [of _ _ x]) simp_all
   12.45 +
   12.46  instantiation nat :: unique_euclidean_semiring
   12.47  begin
   12.48  
   12.49 @@ -1422,6 +1447,64 @@
   12.50  
   12.51  end
   12.52  
   12.53 +lemma coprime_int_iff [simp]:
   12.54 +  "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
   12.55 +proof
   12.56 +  assume ?P
   12.57 +  show ?Q
   12.58 +  proof (rule coprimeI)
   12.59 +    fix q
   12.60 +    assume "q dvd m" "q dvd n"
   12.61 +    then have "int q dvd int m" "int q dvd int n"
   12.62 +      by (simp_all add: zdvd_int)
   12.63 +    with \<open>?P\<close> have "is_unit (int q)"
   12.64 +      by (rule coprime_common_divisor)
   12.65 +    then show "is_unit q"
   12.66 +      by simp
   12.67 +  qed
   12.68 +next
   12.69 +  assume ?Q
   12.70 +  show ?P
   12.71 +  proof (rule coprimeI)
   12.72 +    fix k
   12.73 +    assume "k dvd int m" "k dvd int n"
   12.74 +    then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
   12.75 +      by (simp_all add: zdvd_int)
   12.76 +    with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
   12.77 +      by (rule coprime_common_divisor)
   12.78 +    then show "is_unit k"
   12.79 +      by simp
   12.80 +  qed
   12.81 +qed
   12.82 +
   12.83 +lemma coprime_abs_left_iff [simp]:
   12.84 +  "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int
   12.85 +  using coprime_normalize_left_iff [of k l] by simp
   12.86 +
   12.87 +lemma coprime_abs_right_iff [simp]:
   12.88 +  "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int
   12.89 +  using coprime_abs_left_iff [of l k] by (simp add: ac_simps)
   12.90 +
   12.91 +lemma coprime_nat_abs_left_iff [simp]:
   12.92 +  "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)"
   12.93 +proof -
   12.94 +  define m where "m = nat \<bar>k\<bar>"
   12.95 +  then have "\<bar>k\<bar> = int m"
   12.96 +    by simp
   12.97 +  moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)"
   12.98 +    by simp
   12.99 +  ultimately show ?thesis
  12.100 +    by simp
  12.101 +qed
  12.102 +
  12.103 +lemma coprime_nat_abs_right_iff [simp]:
  12.104 +  "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k"
  12.105 +  using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)
  12.106 +
  12.107 +lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  12.108 +  for a b :: int
  12.109 +  by (drule coprime_common_divisor [of _ _ x]) simp_all
  12.110 +
  12.111  instantiation int :: idom_modulo
  12.112  begin
  12.113  
    13.1 --- a/src/HOL/GCD.thy	Sat Nov 11 18:33:35 2017 +0000
    13.2 +++ b/src/HOL/GCD.thy	Sat Nov 11 18:41:08 2017 +0000
    13.3 @@ -142,12 +142,6 @@
    13.4  class gcd = zero + one + dvd +
    13.5    fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    13.6      and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    13.7 -begin
    13.8 -
    13.9 -abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   13.10 -  where "coprime x y \<equiv> gcd x y = 1"
   13.11 -
   13.12 -end
   13.13  
   13.14  class Gcd = gcd +
   13.15    fixes Gcd :: "'a set \<Rightarrow> 'a"
   13.16 @@ -243,7 +237,8 @@
   13.17      by simp
   13.18  qed
   13.19  
   13.20 -lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   13.21 +lemma is_unit_gcd_iff [simp]:
   13.22 +  "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
   13.23    by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
   13.24  
   13.25  sublocale gcd: abel_semigroup gcd
   13.26 @@ -279,7 +274,7 @@
   13.27    show "gcd (normalize a) b = gcd a b" for a b
   13.28      using gcd_dvd1 [of "normalize a" b]
   13.29      by (auto intro: associated_eqI)
   13.30 -  show "coprime 1 a" for a
   13.31 +  show "gcd 1 a = 1" for a
   13.32      by (rule associated_eqI) simp_all
   13.33  qed simp_all
   13.34  
   13.35 @@ -292,12 +287,6 @@
   13.36  lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   13.37    by (fact gcd.right_idem)
   13.38  
   13.39 -lemma coprime_1_left: "coprime 1 a"
   13.40 -  by (fact gcd.bottom_left_bottom)
   13.41 -
   13.42 -lemma coprime_1_right: "coprime a 1"
   13.43 -  by (fact gcd.bottom_right_bottom)
   13.44 -
   13.45  lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
   13.46  proof (cases "c = 0")
   13.47    case True
   13.48 @@ -634,70 +623,6 @@
   13.49      by (rule dvd_trans)
   13.50  qed
   13.51  
   13.52 -lemma coprime_dvd_mult:
   13.53 -  assumes "coprime a b" and "a dvd c * b"
   13.54 -  shows "a dvd c"
   13.55 -proof (cases "c = 0")
   13.56 -  case True
   13.57 -  then show ?thesis by simp
   13.58 -next
   13.59 -  case False
   13.60 -  then have unit: "is_unit (unit_factor c)"
   13.61 -    by simp
   13.62 -  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   13.63 -  have "gcd (c * a) (c * b) * unit_factor c = c"
   13.64 -    by (simp add: ac_simps)
   13.65 -  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   13.66 -    by (simp add: dvd_mult_unit_iff unit)
   13.67 -  ultimately show ?thesis
   13.68 -    by simp
   13.69 -qed
   13.70 -
   13.71 -lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
   13.72 -  by (auto intro: coprime_dvd_mult)
   13.73 -
   13.74 -lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   13.75 -  apply (rule associated_eqI)
   13.76 -     apply (rule gcd_greatest)
   13.77 -      apply (rule_tac b = c in coprime_dvd_mult)
   13.78 -       apply (simp add: gcd.assoc)
   13.79 -       apply (simp_all add: ac_simps)
   13.80 -  done
   13.81 -
   13.82 -lemma coprime_crossproduct:
   13.83 -  fixes a b c d :: 'a
   13.84 -  assumes "coprime a d" and "coprime b c"
   13.85 -  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
   13.86 -    normalize a = normalize b \<and> normalize c = normalize d"
   13.87 -    (is "?lhs \<longleftrightarrow> ?rhs")
   13.88 -proof
   13.89 -  assume ?rhs
   13.90 -  then show ?lhs by simp
   13.91 -next
   13.92 -  assume ?lhs
   13.93 -  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   13.94 -    by (auto intro: dvdI dest: sym)
   13.95 -  with \<open>coprime a d\<close> have "a dvd b"
   13.96 -    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   13.97 -  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   13.98 -    by (auto intro: dvdI dest: sym)
   13.99 -  with \<open>coprime b c\<close> have "b dvd a"
  13.100 -    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
  13.101 -  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
  13.102 -    by (auto intro: dvdI dest: sym simp add: mult.commute)
  13.103 -  with \<open>coprime b c\<close> have "c dvd d"
  13.104 -    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
  13.105 -  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
  13.106 -    by (auto intro: dvdI dest: sym simp add: mult.commute)
  13.107 -  with \<open>coprime a d\<close> have "d dvd c"
  13.108 -    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
  13.109 -  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
  13.110 -    by (rule associatedI)
  13.111 -  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
  13.112 -    by (rule associatedI)
  13.113 -  ultimately show ?rhs ..
  13.114 -qed
  13.115 -
  13.116  lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
  13.117    by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
  13.118  
  13.119 @@ -707,285 +632,6 @@
  13.120  lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
  13.121    by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
  13.122  
  13.123 -lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
  13.124 -  by (rule sym, rule gcdI) simp_all
  13.125 -
  13.126 -lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
  13.127 -  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
  13.128 -
  13.129 -lemma div_gcd_coprime:
  13.130 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  13.131 -  shows "coprime (a div gcd a b) (b div gcd a b)"
  13.132 -proof -
  13.133 -  let ?g = "gcd a b"
  13.134 -  let ?a' = "a div ?g"
  13.135 -  let ?b' = "b div ?g"
  13.136 -  let ?g' = "gcd ?a' ?b'"
  13.137 -  have dvdg: "?g dvd a" "?g dvd b"
  13.138 -    by simp_all
  13.139 -  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
  13.140 -    by simp_all
  13.141 -  from dvdg dvdg' obtain ka kb ka' kb' where
  13.142 -    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
  13.143 -    unfolding dvd_def by blast
  13.144 -  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
  13.145 -    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
  13.146 -  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  13.147 -    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  13.148 -  have "?g \<noteq> 0"
  13.149 -    using nz by simp
  13.150 -  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  13.151 -  ultimately show ?thesis
  13.152 -    using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
  13.153 -qed
  13.154 -
  13.155 -lemma divides_mult:
  13.156 -  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
  13.157 -  shows "a * b dvd c"
  13.158 -proof -
  13.159 -  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
  13.160 -  with \<open>a dvd c\<close> have "a dvd b' * b"
  13.161 -    by (simp add: ac_simps)
  13.162 -  with \<open>coprime a b\<close> have "a dvd b'"
  13.163 -    by (simp add: coprime_dvd_mult_iff)
  13.164 -  then obtain a' where "b' = a * a'" ..
  13.165 -  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
  13.166 -    by (simp add: ac_simps)
  13.167 -  then show ?thesis ..
  13.168 -qed
  13.169 -
  13.170 -lemma coprime_lmult:
  13.171 -  assumes dab: "gcd d (a * b) = 1"
  13.172 -  shows "gcd d a = 1"
  13.173 -proof (rule coprimeI)
  13.174 -  fix l
  13.175 -  assume "l dvd d" and "l dvd a"
  13.176 -  then have "l dvd a * b"
  13.177 -    by simp
  13.178 -  with \<open>l dvd d\<close> and dab show "l dvd 1"
  13.179 -    by (auto intro: gcd_greatest)
  13.180 -qed
  13.181 -
  13.182 -lemma coprime_rmult:
  13.183 -  assumes dab: "gcd d (a * b) = 1"
  13.184 -  shows "gcd d b = 1"
  13.185 -proof (rule coprimeI)
  13.186 -  fix l
  13.187 -  assume "l dvd d" and "l dvd b"
  13.188 -  then have "l dvd a * b"
  13.189 -    by simp
  13.190 -  with \<open>l dvd d\<close> and dab show "l dvd 1"
  13.191 -    by (auto intro: gcd_greatest)
  13.192 -qed
  13.193 -
  13.194 -lemma coprime_mult:
  13.195 -  assumes "coprime d a"
  13.196 -    and "coprime d b"
  13.197 -  shows "coprime d (a * b)"
  13.198 -  apply (subst gcd.commute)
  13.199 -  using assms(1) apply (subst gcd_mult_cancel)
  13.200 -   apply (subst gcd.commute)
  13.201 -   apply assumption
  13.202 -  apply (subst gcd.commute)
  13.203 -  apply (rule assms(2))
  13.204 -  done
  13.205 -
  13.206 -lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
  13.207 -  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
  13.208 -  by blast
  13.209 -
  13.210 -lemma coprime_mul_eq':
  13.211 -  "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
  13.212 -  using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
  13.213 -
  13.214 -lemma gcd_coprime:
  13.215 -  assumes c: "gcd a b \<noteq> 0"
  13.216 -    and a: "a = a' * gcd a b"
  13.217 -    and b: "b = b' * gcd a b"
  13.218 -  shows "gcd a' b' = 1"
  13.219 -proof -
  13.220 -  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
  13.221 -    by simp
  13.222 -  with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
  13.223 -  also from assms have "a div gcd a b = a'"
  13.224 -    using dvd_div_eq_mult local.gcd_dvd1 by blast
  13.225 -  also from assms have "b div gcd a b = b'"
  13.226 -    using dvd_div_eq_mult local.gcd_dvd1 by blast
  13.227 -  finally show ?thesis .
  13.228 -qed
  13.229 -
  13.230 -lemma coprime_power:
  13.231 -  assumes "0 < n"
  13.232 -  shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
  13.233 -  using assms
  13.234 -proof (induct n)
  13.235 -  case 0
  13.236 -  then show ?case by simp
  13.237 -next
  13.238 -  case (Suc n)
  13.239 -  then show ?case
  13.240 -    by (cases n) (simp_all add: coprime_mul_eq)
  13.241 -qed
  13.242 -
  13.243 -lemma gcd_coprime_exists:
  13.244 -  assumes "gcd a b \<noteq> 0"
  13.245 -  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
  13.246 -  apply (rule_tac x = "a div gcd a b" in exI)
  13.247 -  apply (rule_tac x = "b div gcd a b" in exI)
  13.248 -  using assms
  13.249 -  apply (auto intro: div_gcd_coprime)
  13.250 -  done
  13.251 -
  13.252 -lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
  13.253 -  by (induct n) (simp_all add: coprime_mult)
  13.254 -
  13.255 -lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
  13.256 -  by (induct n) (simp_all add: gcd_mult_cancel)
  13.257 -
  13.258 -lemma coprime_exp2:
  13.259 -  assumes "coprime a b"
  13.260 -  shows "coprime (a ^ n) (b ^ m)"
  13.261 -proof (rule coprime_exp_left)
  13.262 -  from assms show "coprime a (b ^ m)"
  13.263 -    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
  13.264 -qed
  13.265 -
  13.266 -lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
  13.267 -proof (cases "a = 0 \<and> b = 0")
  13.268 -  case True
  13.269 -  then show ?thesis
  13.270 -    by (cases n) simp_all
  13.271 -next
  13.272 -  case False
  13.273 -  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  13.274 -    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
  13.275 -  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
  13.276 -    by simp
  13.277 -  also note gcd_mult_distrib
  13.278 -  also have "unit_factor (gcd a b ^ n) = 1"
  13.279 -    using False by (auto simp add: unit_factor_power unit_factor_gcd)
  13.280 -  also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
  13.281 -    apply (subst ac_simps)
  13.282 -    apply (subst div_power)
  13.283 -     apply simp
  13.284 -    apply (rule dvd_div_mult_self)
  13.285 -    apply (rule dvd_power_same)
  13.286 -    apply simp
  13.287 -    done
  13.288 -  also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
  13.289 -    apply (subst ac_simps)
  13.290 -    apply (subst div_power)
  13.291 -     apply simp
  13.292 -    apply (rule dvd_div_mult_self)
  13.293 -    apply (rule dvd_power_same)
  13.294 -    apply simp
  13.295 -    done
  13.296 -  finally show ?thesis by simp
  13.297 -qed
  13.298 -
  13.299 -lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
  13.300 -  apply (subgoal_tac "a dvd gcd a b")
  13.301 -   apply simp
  13.302 -  apply (erule (1) gcd_greatest)
  13.303 -  done
  13.304 -
  13.305 -lemma division_decomp:
  13.306 -  assumes "a dvd b * c"
  13.307 -  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  13.308 -proof (cases "gcd a b = 0")
  13.309 -  case True
  13.310 -  then have "a = 0 \<and> b = 0"
  13.311 -    by simp
  13.312 -  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
  13.313 -    by simp
  13.314 -  then show ?thesis by blast
  13.315 -next
  13.316 -  case False
  13.317 -  let ?d = "gcd a b"
  13.318 -  from gcd_coprime_exists [OF False]
  13.319 -    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
  13.320 -    by blast
  13.321 -  from ab'(1) have "a' dvd a"
  13.322 -    unfolding dvd_def by blast
  13.323 -  with assms have "a' dvd b * c"
  13.324 -    using dvd_trans [of a' a "b * c"] by simp
  13.325 -  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
  13.326 -    by simp
  13.327 -  then have "?d * a' dvd ?d * (b' * c)"
  13.328 -    by (simp add: mult_ac)
  13.329 -  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
  13.330 -    by simp
  13.331 -  with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
  13.332 -    by (subst (asm) ac_simps) blast
  13.333 -  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
  13.334 -    by (simp add: mult_ac)
  13.335 -  then show ?thesis by blast
  13.336 -qed
  13.337 -
  13.338 -lemma pow_divs_pow:
  13.339 -  assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
  13.340 -  shows "a dvd b"
  13.341 -proof (cases "gcd a b = 0")
  13.342 -  case True
  13.343 -  then show ?thesis by simp
  13.344 -next
  13.345 -  case False
  13.346 -  let ?d = "gcd a b"
  13.347 -  from n obtain m where m: "n = Suc m"
  13.348 -    by (cases n) simp_all
  13.349 -  from False have zn: "?d ^ n \<noteq> 0"
  13.350 -    by (rule power_not_zero)
  13.351 -  from gcd_coprime_exists [OF False]
  13.352 -  obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
  13.353 -    by blast
  13.354 -  from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
  13.355 -    by (simp add: ab'(1,2)[symmetric])
  13.356 -  then have "?d^n * a'^n dvd ?d^n * b'^n"
  13.357 -    by (simp only: power_mult_distrib ac_simps)
  13.358 -  with zn have "a'^n dvd b'^n"
  13.359 -    by simp
  13.360 -  then have "a' dvd b'^n"
  13.361 -    using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
  13.362 -  then have "a' dvd b'^m * b'"
  13.363 -    by (simp add: m ac_simps)
  13.364 -  with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
  13.365 -  have "a' dvd b'" by (subst (asm) ac_simps) blast
  13.366 -  then have "a' * ?d dvd b' * ?d"
  13.367 -    by (rule mult_dvd_mono) simp
  13.368 -  with ab'(1,2) show ?thesis
  13.369 -    by simp
  13.370 -qed
  13.371 -
  13.372 -lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
  13.373 -  by (auto intro: pow_divs_pow dvd_power_same)
  13.374 -
  13.375 -lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
  13.376 -  by (subst add_commute) simp
  13.377 -
  13.378 -lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
  13.379 -  by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
  13.380 -
  13.381 -lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
  13.382 -  by (induct xs) (simp_all add: gcd_mult_cancel)
  13.383 -
  13.384 -lemma coprime_divisors:
  13.385 -  assumes "d dvd a" "e dvd b" "gcd a b = 1"
  13.386 -  shows "gcd d e = 1"
  13.387 -proof -
  13.388 -  from assms obtain k l where "a = d * k" "b = e * l"
  13.389 -    unfolding dvd_def by blast
  13.390 -  with assms have "gcd (d * k) (e * l) = 1"
  13.391 -    by simp
  13.392 -  then have "gcd (d * k) e = 1"
  13.393 -    by (rule coprime_lmult)
  13.394 -  also have "gcd (d * k) e = gcd e (d * k)"
  13.395 -    by (simp add: ac_simps)
  13.396 -  finally have "gcd e d = 1"
  13.397 -    by (rule coprime_lmult)
  13.398 -  then show ?thesis
  13.399 -    by (simp add: ac_simps)
  13.400 -qed
  13.401 -
  13.402  lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
  13.403    by (simp add: lcm_gcd)
  13.404  
  13.405 @@ -1006,9 +652,6 @@
  13.406    "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"
  13.407    by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
  13.408  
  13.409 -lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
  13.410 -  by (subst lcm_gcd) simp
  13.411 -
  13.412  lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
  13.413    apply (cases "a = 0")
  13.414     apply simp
  13.415 @@ -1058,7 +701,7 @@
  13.416  qed
  13.417  
  13.418  lemma dvd_productE:
  13.419 -  assumes "p dvd (a * b)"
  13.420 +  assumes "p dvd a * b"
  13.421    obtains x y where "p = x * y" "x dvd a" "y dvd b"
  13.422  proof (cases "a = 0")
  13.423    case True
  13.424 @@ -1076,32 +719,11 @@
  13.425    ultimately show ?thesis by (rule that)
  13.426  qed
  13.427  
  13.428 -lemma coprime_crossproduct':
  13.429 -  fixes a b c d
  13.430 -  assumes "b \<noteq> 0"
  13.431 -  assumes unit_factors: "unit_factor b = unit_factor d"
  13.432 -  assumes coprime: "coprime a b" "coprime c d"
  13.433 -  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
  13.434 -proof safe
  13.435 -  assume eq: "a * d = b * c"
  13.436 -  hence "normalize a * normalize d = normalize c * normalize b"
  13.437 -    by (simp only: normalize_mult [symmetric] mult_ac)
  13.438 -  with coprime have "normalize b = normalize d"
  13.439 -    by (subst (asm) coprime_crossproduct) simp_all
  13.440 -  from this and unit_factors show "b = d"
  13.441 -    by (rule normalize_unit_factor_eqI)
  13.442 -  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
  13.443 -  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
  13.444 -qed (simp_all add: mult_ac)
  13.445 -
  13.446  end
  13.447  
  13.448  class ring_gcd = comm_ring_1 + semiring_gcd
  13.449  begin
  13.450  
  13.451 -lemma coprime_minus_one: "coprime (n - 1) n"
  13.452 -  using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
  13.453 -
  13.454  lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
  13.455    by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
  13.456  
  13.457 @@ -1471,36 +1093,6 @@
  13.458  lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
  13.459    by simp
  13.460  
  13.461 -lemma Lcm_coprime:
  13.462 -  assumes "finite A"
  13.463 -    and "A \<noteq> {}"
  13.464 -    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
  13.465 -  shows "Lcm A = normalize (\<Prod>A)"
  13.466 -  using assms
  13.467 -proof (induct rule: finite_ne_induct)
  13.468 -  case singleton
  13.469 -  then show ?case by simp
  13.470 -next
  13.471 -  case (insert a A)
  13.472 -  have "Lcm (insert a A) = lcm a (Lcm A)"
  13.473 -    by simp
  13.474 -  also from insert have "Lcm A = normalize (\<Prod>A)"
  13.475 -    by blast
  13.476 -  also have "lcm a \<dots> = lcm a (\<Prod>A)"
  13.477 -    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
  13.478 -  also from insert have "gcd a (\<Prod>A) = 1"
  13.479 -    by (subst gcd.commute, intro prod_coprime) auto
  13.480 -  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
  13.481 -    by (simp add: lcm_coprime)
  13.482 -  finally show ?case .
  13.483 -qed
  13.484 -
  13.485 -lemma Lcm_coprime':
  13.486 -  "card A \<noteq> 0 \<Longrightarrow>
  13.487 -    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
  13.488 -    Lcm A = normalize (\<Prod>A)"
  13.489 -  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  13.490 -
  13.491  lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
  13.492    by (auto intro!: Gcd_eq_1_I)
  13.493  
  13.494 @@ -1677,6 +1269,465 @@
  13.495  
  13.496  end
  13.497  
  13.498 +
  13.499 +subsection \<open>Coprimality\<close>
  13.500 +
  13.501 +context semiring_gcd
  13.502 +begin
  13.503 +
  13.504 +lemma coprime_imp_gcd_eq_1 [simp]:
  13.505 +  "gcd a b = 1" if "coprime a b"
  13.506 +proof -
  13.507 +  define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
  13.508 +  then have "a = t * r" and "b = t * s"
  13.509 +    by simp_all
  13.510 +  with that have "coprime (t * r) (t * s)"
  13.511 +    by simp
  13.512 +  then show ?thesis
  13.513 +    by (simp add: t_def)
  13.514 +qed
  13.515 +
  13.516 +lemma gcd_eq_1_imp_coprime:
  13.517 +  "coprime a b" if "gcd a b = 1"
  13.518 +proof (rule coprimeI)
  13.519 +  fix c
  13.520 +  assume "c dvd a" and "c dvd b"
  13.521 +  then have "c dvd gcd a b"
  13.522 +    by (rule gcd_greatest)
  13.523 +  with that show "is_unit c"
  13.524 +    by simp
  13.525 +qed
  13.526 +
  13.527 +lemma coprime_iff_gcd_eq_1 [presburger, code]:
  13.528 +  "coprime a b \<longleftrightarrow> gcd a b = 1"
  13.529 +  by rule (simp_all add: gcd_eq_1_imp_coprime)
  13.530 +
  13.531 +lemma is_unit_gcd [simp]:
  13.532 +  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
  13.533 +  by (simp add: coprime_iff_gcd_eq_1)
  13.534 +
  13.535 +lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
  13.536 +  by (simp add: gcd_eq_1_imp_coprime ac_simps)
  13.537 +
  13.538 +lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
  13.539 +  using coprime_add_one_left [of a] by (simp add: ac_simps)
  13.540 +
  13.541 +lemma coprime_mult_left_iff [simp]:
  13.542 +  "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c"
  13.543 +proof
  13.544 +  assume "coprime (a * b) c"
  13.545 +  with coprime_common_divisor [of "a * b" c]
  13.546 +  have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
  13.547 +    using that by blast
  13.548 +  have "coprime a c"
  13.549 +    by (rule coprimeI, rule *) simp_all
  13.550 +  moreover have "coprime b c"
  13.551 +    by (rule coprimeI, rule *) simp_all
  13.552 +  ultimately show "coprime a c \<and> coprime b c" ..
  13.553 +next
  13.554 +  assume "coprime a c \<and> coprime b c"
  13.555 +  then have "coprime a c" "coprime b c"
  13.556 +    by simp_all
  13.557 +  show "coprime (a * b) c"
  13.558 +  proof (rule coprimeI)
  13.559 +    fix d
  13.560 +    assume "d dvd a * b"
  13.561 +    then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
  13.562 +      by (rule dvd_productE)
  13.563 +    assume "d dvd c"
  13.564 +    with d have "r * s dvd c"
  13.565 +      by simp
  13.566 +    then have "r dvd c" "s dvd c"
  13.567 +      by (auto intro: dvd_mult_left dvd_mult_right)
  13.568 +    from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close>
  13.569 +    have "is_unit r"
  13.570 +      by (rule coprime_common_divisor)
  13.571 +    moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close>
  13.572 +    have "is_unit s"
  13.573 +      by (rule coprime_common_divisor)
  13.574 +    ultimately show "is_unit d"
  13.575 +      by (simp add: d is_unit_mult_iff)
  13.576 +  qed
  13.577 +qed
  13.578 +
  13.579 +lemma coprime_mult_right_iff [simp]:
  13.580 +  "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b"
  13.581 +  using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)
  13.582 +
  13.583 +lemma coprime_power_left_iff [simp]:
  13.584 +  "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0"
  13.585 +proof (cases "n = 0")
  13.586 +  case True
  13.587 +  then show ?thesis
  13.588 +    by simp
  13.589 +next
  13.590 +  case False
  13.591 +  then have "n > 0"
  13.592 +    by simp
  13.593 +  then show ?thesis
  13.594 +    by (induction n rule: nat_induct_non_zero) simp_all
  13.595 +qed
  13.596 +
  13.597 +lemma coprime_power_right_iff [simp]:
  13.598 +  "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0"
  13.599 +  using coprime_power_left_iff [of b n a] by (simp add: ac_simps)
  13.600 +
  13.601 +lemma prod_coprime_left:
  13.602 +  "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a"
  13.603 +  using that by (induct A rule: infinite_finite_induct) simp_all
  13.604 +
  13.605 +lemma prod_coprime_right:
  13.606 +  "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)"
  13.607 +  using that prod_coprime_left [of A f a] by (simp add: ac_simps)
  13.608 +
  13.609 +lemma prod_list_coprime_left:
  13.610 +  "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a"
  13.611 +  using that by (induct xs) simp_all
  13.612 +
  13.613 +lemma prod_list_coprime_right:
  13.614 +  "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x"
  13.615 +  using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)
  13.616 +
  13.617 +lemma coprime_dvd_mult_left_iff:
  13.618 +  "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c"
  13.619 +proof
  13.620 +  assume "a dvd b"
  13.621 +  then show "a dvd b * c"
  13.622 +    by simp
  13.623 +next
  13.624 +  assume "a dvd b * c"
  13.625 +  show "a dvd b"
  13.626 +  proof (cases "b = 0")
  13.627 +    case True
  13.628 +    then show ?thesis
  13.629 +      by simp
  13.630 +  next
  13.631 +    case False
  13.632 +    then have unit: "is_unit (unit_factor b)"
  13.633 +      by simp
  13.634 +    from \<open>coprime a c\<close> mult_gcd_left [of b a c]
  13.635 +    have "gcd (b * a) (b * c) * unit_factor b = b"
  13.636 +      by (simp add: ac_simps)
  13.637 +    moreover from \<open>a dvd b * c\<close>
  13.638 +    have "a dvd gcd (b * a) (b * c) * unit_factor b"
  13.639 +      by (simp add: dvd_mult_unit_iff unit)
  13.640 +    ultimately show ?thesis
  13.641 +      by simp
  13.642 +  qed
  13.643 +qed
  13.644 +
  13.645 +lemma coprime_dvd_mult_right_iff:
  13.646 +  "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c"
  13.647 +  using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)
  13.648 +
  13.649 +lemma divides_mult:
  13.650 +  "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
  13.651 +proof -
  13.652 +  from \<open>b dvd c\<close> obtain b' where "c = b * b'" ..
  13.653 +  with \<open>a dvd c\<close> have "a dvd b' * b"
  13.654 +    by (simp add: ac_simps)
  13.655 +  with \<open>coprime a b\<close> have "a dvd b'"
  13.656 +    by (simp add: coprime_dvd_mult_left_iff)
  13.657 +  then obtain a' where "b' = a * a'" ..
  13.658 +  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
  13.659 +    by (simp add: ac_simps)
  13.660 +  then show ?thesis ..
  13.661 +qed
  13.662 +
  13.663 +lemma div_gcd_coprime:
  13.664 +  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
  13.665 +  shows "coprime (a div gcd a b) (b div gcd a b)"
  13.666 +proof -
  13.667 +  let ?g = "gcd a b"
  13.668 +  let ?a' = "a div ?g"
  13.669 +  let ?b' = "b div ?g"
  13.670 +  let ?g' = "gcd ?a' ?b'"
  13.671 +  have dvdg: "?g dvd a" "?g dvd b"
  13.672 +    by simp_all
  13.673 +  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
  13.674 +    by simp_all
  13.675 +  from dvdg dvdg' obtain ka kb ka' kb' where
  13.676 +    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
  13.677 +    unfolding dvd_def by blast
  13.678 +  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
  13.679 +    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
  13.680 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  13.681 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  13.682 +  have "?g \<noteq> 0"
  13.683 +    using assms by simp
  13.684 +  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  13.685 +  ultimately show ?thesis
  13.686 +    using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
  13.687 +    by simp (simp only: coprime_iff_gcd_eq_1)
  13.688 +qed
  13.689 +
  13.690 +lemma gcd_coprime:
  13.691 +  assumes c: "gcd a b \<noteq> 0"
  13.692 +    and a: "a = a' * gcd a b"
  13.693 +    and b: "b = b' * gcd a b"
  13.694 +  shows "coprime a' b'"
  13.695 +proof -
  13.696 +  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
  13.697 +    by simp
  13.698 +  with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
  13.699 +  also from assms have "a div gcd a b = a'"
  13.700 +    using dvd_div_eq_mult local.gcd_dvd1 by blast
  13.701 +  also from assms have "b div gcd a b = b'"
  13.702 +    using dvd_div_eq_mult local.gcd_dvd1 by blast
  13.703 +  finally show ?thesis .
  13.704 +qed
  13.705 +
  13.706 +lemma gcd_coprime_exists:
  13.707 +  assumes "gcd a b \<noteq> 0"
  13.708 +  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  13.709 +  apply (rule_tac x = "a div gcd a b" in exI)
  13.710 +  apply (rule_tac x = "b div gcd a b" in exI)
  13.711 +  using assms
  13.712 +  apply (auto intro: div_gcd_coprime)
  13.713 +  done
  13.714 +
  13.715 +lemma pow_divides_pow_iff [simp]:
  13.716 +  "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
  13.717 +proof (cases "gcd a b = 0")
  13.718 +  case True
  13.719 +  then show ?thesis
  13.720 +    by simp
  13.721 +next
  13.722 +  case False
  13.723 +  show ?thesis
  13.724 +  proof
  13.725 +    let ?d = "gcd a b"
  13.726 +    from \<open>n > 0\<close> obtain m where m: "n = Suc m"
  13.727 +      by (cases n) simp_all
  13.728 +    from False have zn: "?d ^ n \<noteq> 0"
  13.729 +      by (rule power_not_zero)
  13.730 +    from gcd_coprime_exists [OF False]
  13.731 +    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
  13.732 +      by blast
  13.733 +    assume "a ^ n dvd b ^ n"
  13.734 +    then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
  13.735 +      by (simp add: ab'(1,2)[symmetric])
  13.736 +    then have "?d^n * a'^n dvd ?d^n * b'^n"
  13.737 +      by (simp only: power_mult_distrib ac_simps)
  13.738 +    with zn have "a' ^ n dvd b' ^ n"
  13.739 +      by simp
  13.740 +    then have "a' dvd b' ^ n"
  13.741 +      using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
  13.742 +    then have "a' dvd b' ^ m * b'"
  13.743 +      by (simp add: m ac_simps)
  13.744 +    moreover have "coprime a' (b' ^ n)"
  13.745 +      using \<open>coprime a' b'\<close> by simp
  13.746 +    then have "a' dvd b'"
  13.747 +      using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast
  13.748 +    then have "a' * ?d dvd b' * ?d"
  13.749 +      by (rule mult_dvd_mono) simp
  13.750 +    with ab'(1,2) show "a dvd b"
  13.751 +      by simp
  13.752 +  next
  13.753 +    assume "a dvd b"
  13.754 +    with \<open>n > 0\<close> show "a ^ n dvd b ^ n"
  13.755 +      by (induction rule: nat_induct_non_zero)
  13.756 +        (simp_all add: mult_dvd_mono)
  13.757 +  qed
  13.758 +qed
  13.759 +
  13.760 +lemma coprime_crossproduct:
  13.761 +  fixes a b c d :: 'a
  13.762 +  assumes "coprime a d" and "coprime b c"
  13.763 +  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
  13.764 +    normalize a = normalize b \<and> normalize c = normalize d"
  13.765 +    (is "?lhs \<longleftrightarrow> ?rhs")
  13.766 +proof
  13.767 +  assume ?rhs
  13.768 +  then show ?lhs by simp
  13.769 +next
  13.770 +  assume ?lhs
  13.771 +  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
  13.772 +    by (auto intro: dvdI dest: sym)
  13.773 +  with \<open>coprime a d\<close> have "a dvd b"
  13.774 +    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
  13.775 +  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
  13.776 +    by (auto intro: dvdI dest: sym)
  13.777 +  with \<open>coprime b c\<close> have "b dvd a"
  13.778 +    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
  13.779 +  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
  13.780 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
  13.781 +  with \<open>coprime b c\<close> have "c dvd d"
  13.782 +    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
  13.783 +  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
  13.784 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
  13.785 +  with \<open>coprime a d\<close> have "d dvd c"
  13.786 +    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
  13.787 +  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
  13.788 +    by (rule associatedI)
  13.789 +  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
  13.790 +    by (rule associatedI)
  13.791 +  ultimately show ?rhs ..
  13.792 +qed
  13.793 +
  13.794 +lemma coprime_crossproduct':
  13.795 +  fixes a b c d
  13.796 +  assumes "b \<noteq> 0"
  13.797 +  assumes unit_factors: "unit_factor b = unit_factor d"
  13.798 +  assumes coprime: "coprime a b" "coprime c d"
  13.799 +  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
  13.800 +proof safe
  13.801 +  assume eq: "a * d = b * c"
  13.802 +  hence "normalize a * normalize d = normalize c * normalize b"
  13.803 +    by (simp only: normalize_mult [symmetric] mult_ac)
  13.804 +  with coprime have "normalize b = normalize d"
  13.805 +    by (subst (asm) coprime_crossproduct) simp_all
  13.806 +  from this and unit_factors show "b = d"
  13.807 +    by (rule normalize_unit_factor_eqI)
  13.808 +  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
  13.809 +  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
  13.810 +qed (simp_all add: mult_ac)
  13.811 +
  13.812 +lemma gcd_mult_left_left_cancel:
  13.813 +  "gcd (c * a) b = gcd a b" if "coprime b c"
  13.814 +proof -
  13.815 +  have "coprime (gcd b (a * c)) c"
  13.816 +    by (rule coprimeI) (auto intro: that coprime_common_divisor)
  13.817 +  then have "gcd b (a * c) dvd a"
  13.818 +    using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
  13.819 +    by simp
  13.820 +  then show ?thesis
  13.821 +    by (auto intro: associated_eqI simp add: ac_simps)
  13.822 +qed
  13.823 +
  13.824 +lemma gcd_mult_left_right_cancel:
  13.825 +  "gcd (a * c) b = gcd a b" if "coprime b c"
  13.826 +  using that gcd_mult_left_left_cancel [of b c a]
  13.827 +  by (simp add: ac_simps)
  13.828 +
  13.829 +lemma gcd_mult_right_left_cancel:
  13.830 +  "gcd a (c * b) = gcd a b" if "coprime a c"
  13.831 +  using that gcd_mult_left_left_cancel [of a c b]
  13.832 +  by (simp add: ac_simps)
  13.833 +
  13.834 +lemma gcd_mult_right_right_cancel:
  13.835 +  "gcd a (b * c) = gcd a b" if "coprime a c"
  13.836 +  using that gcd_mult_right_left_cancel [of a c b]
  13.837 +  by (simp add: ac_simps)
  13.838 +
  13.839 +lemma gcd_exp [simp]:
  13.840 +  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
  13.841 +proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
  13.842 +  case True
  13.843 +  then show ?thesis
  13.844 +    by (cases n) simp_all
  13.845 +next
  13.846 +  case False
  13.847 +  then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
  13.848 +    by (auto intro: div_gcd_coprime)
  13.849 +  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  13.850 +    by simp
  13.851 +  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  13.852 +    by simp
  13.853 +  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
  13.854 +    by simp
  13.855 +  also note gcd_mult_distrib
  13.856 +  also have "unit_factor (gcd a b ^ n) = 1"
  13.857 +    using False by (auto simp add: unit_factor_power unit_factor_gcd)
  13.858 +  also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
  13.859 +    by (simp add: ac_simps div_power dvd_power_same)
  13.860 +  also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
  13.861 +    by (simp add: ac_simps div_power dvd_power_same)
  13.862 +  finally show ?thesis by simp
  13.863 +qed
  13.864 +
  13.865 +lemma division_decomp:
  13.866 +  assumes "a dvd b * c"
  13.867 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  13.868 +proof (cases "gcd a b = 0")
  13.869 +  case True
  13.870 +  then have "a = 0 \<and> b = 0"
  13.871 +    by simp
  13.872 +  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
  13.873 +    by simp
  13.874 +  then show ?thesis by blast
  13.875 +next
  13.876 +  case False
  13.877 +  let ?d = "gcd a b"
  13.878 +  from gcd_coprime_exists [OF False]
  13.879 +    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
  13.880 +    by blast
  13.881 +  from ab'(1) have "a' dvd a" ..
  13.882 +  with assms have "a' dvd b * c"
  13.883 +    using dvd_trans [of a' a "b * c"] by simp
  13.884 +  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
  13.885 +    by simp
  13.886 +  then have "?d * a' dvd ?d * (b' * c)"
  13.887 +    by (simp add: mult_ac)
  13.888 +  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
  13.889 +    by simp
  13.890 +  then have "a' dvd c"
  13.891 +    using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff)
  13.892 +  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
  13.893 +    by (simp add: ac_simps)
  13.894 +  then show ?thesis by blast
  13.895 +qed
  13.896 +
  13.897 +lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)"
  13.898 +  by (subst lcm_gcd) simp
  13.899 +
  13.900 +end
  13.901 +
  13.902 +context ring_gcd
  13.903 +begin
  13.904 +
  13.905 +lemma coprime_minus_left_iff [simp]:
  13.906 +  "coprime (- a) b \<longleftrightarrow> coprime a b"
  13.907 +  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
  13.908 +
  13.909 +lemma coprime_minus_right_iff [simp]:
  13.910 +  "coprime a (- b) \<longleftrightarrow> coprime a b"
  13.911 +  using coprime_minus_left_iff [of b a] by (simp add: ac_simps)
  13.912 +
  13.913 +lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
  13.914 +  using coprime_add_one_right [of "a - 1"] by simp
  13.915 +
  13.916 +lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
  13.917 +  using coprime_diff_one_left [of a] by (simp add: ac_simps)
  13.918 +
  13.919 +end
  13.920 +
  13.921 +context semiring_Gcd
  13.922 +begin
  13.923 +
  13.924 +lemma Lcm_coprime:
  13.925 +  assumes "finite A"
  13.926 +    and "A \<noteq> {}"
  13.927 +    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b"
  13.928 +  shows "Lcm A = normalize (\<Prod>A)"
  13.929 +  using assms
  13.930 +proof (induct rule: finite_ne_induct)
  13.931 +  case singleton
  13.932 +  then show ?case by simp
  13.933 +next
  13.934 +  case (insert a A)
  13.935 +  have "Lcm (insert a A) = lcm a (Lcm A)"
  13.936 +    by simp
  13.937 +  also from insert have "Lcm A = normalize (\<Prod>A)"
  13.938 +    by blast
  13.939 +  also have "lcm a \<dots> = lcm a (\<Prod>A)"
  13.940 +    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
  13.941 +  also from insert have "coprime a (\<Prod>A)"
  13.942 +    by (subst coprime_commute, intro prod_coprime_left) auto
  13.943 +  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
  13.944 +    by (simp add: lcm_coprime)
  13.945 +  finally show ?case .
  13.946 +qed
  13.947 +
  13.948 +lemma Lcm_coprime':
  13.949 +  "card A \<noteq> 0 \<Longrightarrow>
  13.950 +    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow>
  13.951 +    Lcm A = normalize (\<Prod>A)"
  13.952 +  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
  13.953 +
  13.954 +end
  13.955 +
  13.956 +
  13.957  subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
  13.958  
  13.959  instantiation nat :: gcd
  13.960 @@ -1716,9 +1767,6 @@
  13.961     apply simp_all
  13.962    done
  13.963  
  13.964 -
  13.965 -text \<open>Specific to \<open>int\<close>.\<close>
  13.966 -
  13.967  lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
  13.968    by (simp add: gcd_int_def)
  13.969  
  13.970 @@ -1949,19 +1997,6 @@
  13.971    for k m n :: int
  13.972    by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
  13.973  
  13.974 -lemma coprime_crossproduct_nat:
  13.975 -  fixes a b c d :: nat
  13.976 -  assumes "coprime a d" and "coprime b c"
  13.977 -  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
  13.978 -  using assms coprime_crossproduct [of a d b c] by simp
  13.979 -
  13.980 -lemma coprime_crossproduct_int:
  13.981 -  fixes a b c d :: int
  13.982 -  assumes "coprime a d" and "coprime b c"
  13.983 -  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>"
  13.984 -  using assms coprime_crossproduct [of a d b c] by simp
  13.985 -
  13.986 -
  13.987  text \<open>\medskip Addition laws.\<close>
  13.988  
  13.989  (* TODO: add the other variations? *)
  13.990 @@ -2064,53 +2099,33 @@
  13.991    for k l :: int
  13.992    by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  13.993  
  13.994 -
  13.995 -subsection \<open>Coprimality\<close>
  13.996 -
  13.997 -lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  13.998 -  for a b :: nat
  13.999 -  using coprime [of a b] by simp
 13.1000 -
 13.1001 -lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
 13.1002 -  for a b :: nat
 13.1003 -  using coprime_nat by simp
 13.1004 -
 13.1005 -lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
 13.1006 -  for a b :: int
 13.1007 -  using gcd_unique_int [of 1 a b]
 13.1008 -  apply clarsimp
 13.1009 -  apply (erule subst)
 13.1010 -  apply (rule iffI)
 13.1011 -   apply force
 13.1012 -  using abs_dvd_iff abs_ge_zero apply blast
 13.1013 -  done
 13.1014 -
 13.1015 -lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
 13.1016 -  for a b n :: nat
 13.1017 -  using pow_divs_eq[of n] by simp
 13.1018 -
 13.1019 -lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
 13.1020 -  using coprime_plus_one[of n] by simp
 13.1021 -
 13.1022 -lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
 13.1023 -  for n :: nat
 13.1024 -  using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
 13.1025 -
 13.1026 -lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
 13.1027 -  for a b :: nat
 13.1028 -  by (metis gcd_greatest_iff nat_dvd_1_iff_1)
 13.1029 -
 13.1030 -lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
 13.1031 -  for a b :: int
 13.1032 -  using gcd_greatest_iff [of x a b] by auto
 13.1033 -
 13.1034 -lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
 13.1035 -  for m x y :: nat
 13.1036 -  by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
 13.1037 -
 13.1038 -lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
 13.1039 -  for m x y :: int
 13.1040 -  by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
 13.1041 +lemma coprime_Suc_left_nat [simp]:
 13.1042 +  "coprime (Suc n) n"
 13.1043 +  using coprime_add_one_left [of n] by simp
 13.1044 +
 13.1045 +lemma coprime_Suc_right_nat [simp]:
 13.1046 +  "coprime n (Suc n)"
 13.1047 +  using coprime_Suc_left_nat [of n] by (simp add: ac_simps)
 13.1048 +
 13.1049 +lemma coprime_diff_one_left_nat [simp]:
 13.1050 +  "coprime (n - 1) n" if "n > 0" for n :: nat
 13.1051 +  using that coprime_Suc_right_nat [of "n - 1"] by simp
 13.1052 +
 13.1053 +lemma coprime_diff_one_right_nat [simp]:
 13.1054 +  "coprime n (n - 1)" if "n > 0" for n :: nat
 13.1055 +  using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps)
 13.1056 +
 13.1057 +lemma coprime_crossproduct_nat:
 13.1058 +  fixes a b c d :: nat
 13.1059 +  assumes "coprime a d" and "coprime b c"
 13.1060 +  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
 13.1061 +  using assms coprime_crossproduct [of a d b c] by simp
 13.1062 +
 13.1063 +lemma coprime_crossproduct_int:
 13.1064 +  fixes a b c d :: int
 13.1065 +  assumes "coprime a d" and "coprime b c"
 13.1066 +  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>"
 13.1067 +  using assms coprime_crossproduct [of a d b c] by simp
 13.1068  
 13.1069  
 13.1070  subsection \<open>Bezout's theorem\<close>
 13.1071 @@ -2742,14 +2757,6 @@
 13.1072    for i m n :: int
 13.1073    by (fact dvd_lcmI2)
 13.1074  
 13.1075 -lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
 13.1076 -  for a b :: nat
 13.1077 -  by (fact coprime_exp2)
 13.1078 -
 13.1079 -lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
 13.1080 -  for a b :: int
 13.1081 -  by (fact coprime_exp2)
 13.1082 -
 13.1083  lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
 13.1084  lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
 13.1085  lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
    14.1 --- a/src/HOL/Isar_Examples/Fibonacci.thy	Sat Nov 11 18:33:35 2017 +0000
    14.2 +++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sat Nov 11 18:41:08 2017 +0000
    14.3 @@ -21,10 +21,6 @@
    14.4  text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
    14.5    Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
    14.6  
    14.7 -
    14.8 -declare One_nat_def [simp]
    14.9 -
   14.10 -
   14.11  subsection \<open>Fibonacci numbers\<close>
   14.12  
   14.13  fun fib :: "nat \<Rightarrow> nat"
   14.14 @@ -65,12 +61,13 @@
   14.15    finally show "?P (n + 2)" .
   14.16  qed
   14.17  
   14.18 -lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1"
   14.19 +lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
   14.20    (is "?P n")
   14.21  proof (induct n rule: fib_induct)
   14.22    show "?P 0" by simp
   14.23    show "?P 1" by simp
   14.24    fix n
   14.25 +  assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
   14.26    have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
   14.27      by simp
   14.28    also have "\<dots> = fib (n + 2) + fib (n + 1)"
   14.29 @@ -79,8 +76,10 @@
   14.30      by (rule gcd_add2)
   14.31    also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
   14.32      by (simp add: gcd.commute)
   14.33 -  also assume "\<dots> = 1"
   14.34 -  finally show "?P (n + 2)" .
   14.35 +  also have "\<dots> = 1"
   14.36 +    using P by simp
   14.37 +  finally show "?P (n + 2)"
   14.38 +    by (simp add: coprime_iff_gcd_eq_1)
   14.39  qed
   14.40  
   14.41  lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
   14.42 @@ -106,7 +105,8 @@
   14.43    also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
   14.44      by (simp add: gcd_mult_add)
   14.45    also have "\<dots> = gcd (fib n) (fib (k + 1))"
   14.46 -    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
   14.47 +    using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
   14.48 +    by (simp add: ac_simps)
   14.49    also have "\<dots> = gcd (fib m) (fib n)"
   14.50      using Suc by (simp add: gcd.commute)
   14.51    finally show ?thesis .
    15.1 --- a/src/HOL/Library/Multiset.thy	Sat Nov 11 18:33:35 2017 +0000
    15.2 +++ b/src/HOL/Library/Multiset.thy	Sat Nov 11 18:41:08 2017 +0000
    15.3 @@ -2155,6 +2155,42 @@
    15.4    "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
    15.5    by (induct n) simp_all
    15.6  
    15.7 +lemma replicate_mset_msubseteq_iff:
    15.8 +  "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
    15.9 +  by (cases m)
   15.10 +    (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
   15.11 +
   15.12 +lemma msubseteq_replicate_msetE:
   15.13 +  assumes "A \<subseteq># replicate_mset n a"
   15.14 +  obtains m where "m \<le> n" and "A = replicate_mset m a"
   15.15 +proof (cases "n = 0")
   15.16 +  case True
   15.17 +  with assms that show thesis
   15.18 +    by simp
   15.19 +next
   15.20 +  case False
   15.21 +  from assms have "set_mset A \<subseteq> set_mset (replicate_mset n a)"
   15.22 +    by (rule set_mset_mono)
   15.23 +  with False have "set_mset A \<subseteq> {a}"
   15.24 +    by simp
   15.25 +  then have "\<exists>m. A = replicate_mset m a"
   15.26 +  proof (induction A)
   15.27 +    case empty
   15.28 +    then show ?case
   15.29 +      by simp
   15.30 +  next
   15.31 +    case (add b A)
   15.32 +    then obtain m where "A = replicate_mset m a"
   15.33 +      by auto
   15.34 +    with add.prems show ?case
   15.35 +      by (auto intro: exI [of _ "Suc m"])
   15.36 +  qed
   15.37 +  then obtain m where A: "A = replicate_mset m a" ..
   15.38 +  with assms have "m \<le> n"
   15.39 +    by (auto simp add: replicate_mset_msubseteq_iff)
   15.40 +  then show thesis using A ..
   15.41 +qed
   15.42 +
   15.43  
   15.44  subsection \<open>Big operators\<close>
   15.45  
    16.1 --- a/src/HOL/Map.thy	Sat Nov 11 18:33:35 2017 +0000
    16.2 +++ b/src/HOL/Map.thy	Sat Nov 11 18:41:08 2017 +0000
    16.3 @@ -782,6 +782,20 @@
    16.4    with * \<open>x = (k, v)\<close> show ?case by simp
    16.5  qed
    16.6  
    16.7 +lemma eq_key_imp_eq_value:
    16.8 +  "v1 = v2"
    16.9 +  if "distinct (map fst xs)" "(k, v1) \<in> set xs" "(k, v2) \<in> set xs"
   16.10 +proof -
   16.11 +  from that have "inj_on fst (set xs)"
   16.12 +    by (simp add: distinct_map)
   16.13 +  moreover have "fst (k, v1) = fst (k, v2)"
   16.14 +    by simp
   16.15 +  ultimately have "(k, v1) = (k, v2)"
   16.16 +    by (rule inj_onD) (fact that)+
   16.17 +  then show ?thesis
   16.18 +    by simp
   16.19 +qed
   16.20 +
   16.21  lemma map_of_inject_set:
   16.22    assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
   16.23    shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
    17.1 --- a/src/HOL/Nitpick.thy	Sat Nov 11 18:33:35 2017 +0000
    17.2 +++ b/src/HOL/Nitpick.thy	Sat Nov 11 18:41:08 2017 +0000
    17.3 @@ -137,7 +137,7 @@
    17.4    by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
    17.5  
    17.6  definition Frac :: "int \<times> int \<Rightarrow> bool" where
    17.7 -  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> gcd a b = 1"
    17.8 +  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> coprime a b"
    17.9  
   17.10  consts
   17.11    Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
    18.1 --- a/src/HOL/Number_Theory/Cong.thy	Sat Nov 11 18:33:35 2017 +0000
    18.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sat Nov 11 18:41:08 2017 +0000
    18.3 @@ -229,7 +229,8 @@
    18.4  lemma cong_mult_rcancel_int:
    18.5    "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
    18.6    if "coprime k m" for a k m :: int
    18.7 -  by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
    18.8 +  using that by (simp add: cong_altdef_int)
    18.9 +    (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib') 
   18.10  
   18.11  lemma cong_mult_rcancel_nat:
   18.12    "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   18.13 @@ -242,7 +243,7 @@
   18.14    also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
   18.15      by (simp add: abs_mult nat_times_as_int)
   18.16    also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
   18.17 -    by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
   18.18 +    by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
   18.19    also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
   18.20      by (simp add: cong_altdef_nat')
   18.21    finally show ?thesis .
   18.22 @@ -320,11 +321,11 @@
   18.23  
   18.24  lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   18.25    for a b :: nat
   18.26 -  by (auto simp add: cong_gcd_eq_nat)
   18.27 +  by (auto simp add: cong_gcd_eq_nat coprime_iff_gcd_eq_1)
   18.28  
   18.29  lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   18.30    for a b :: int
   18.31 -  by (auto simp add: cong_gcd_eq_int)
   18.32 +  by (auto simp add: cong_gcd_eq_int coprime_iff_gcd_eq_1)
   18.33  
   18.34  lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   18.35    for a b :: nat
   18.36 @@ -490,36 +491,24 @@
   18.37  qed
   18.38  
   18.39  lemma cong_solve_coprime_nat:
   18.40 -  fixes a :: nat
   18.41 -  assumes "coprime a n"
   18.42 -  shows "\<exists>x. [a * x = 1] (mod n)"
   18.43 -proof (cases "a = 0")
   18.44 -  case True
   18.45 -  with assms show ?thesis
   18.46 -    by (simp add: cong_0_1_nat') 
   18.47 -next
   18.48 -  case False
   18.49 -  with assms show ?thesis
   18.50 -    by (metis cong_solve_nat)
   18.51 -qed
   18.52 +  "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
   18.53 +  using that cong_solve_nat [of a n] by (cases "a = 0") simp_all
   18.54  
   18.55 -lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
   18.56 -  apply (cases "a = 0")
   18.57 -   apply auto
   18.58 -   apply (cases "n \<ge> 0")
   18.59 -    apply auto
   18.60 -  apply (metis cong_solve_int)
   18.61 -  done
   18.62 +lemma cong_solve_coprime_int:
   18.63 +  "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
   18.64 +  using that cong_solve_int [of a n] by (cases "a = 0")
   18.65 +    (auto simp add: zabs_def split: if_splits)
   18.66  
   18.67  lemma coprime_iff_invertible_nat:
   18.68 -  "m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))"
   18.69 -  by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0)
   18.70 +  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))"
   18.71 +  by (auto intro: cong_solve_coprime_nat)
   18.72 +    (use cong_imp_coprime_nat cong_sym coprime_Suc_0_left coprime_mult_left_iff in blast)
   18.73  
   18.74 -lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   18.75 +lemma coprime_iff_invertible_int:
   18.76 +  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   18.77    for m :: int
   18.78 -  apply (auto intro: cong_solve_coprime_int)
   18.79 -  using cong_gcd_eq_int coprime_mul_eq' apply fastforce
   18.80 -  done
   18.81 +  by (auto intro: cong_solve_coprime_int)
   18.82 +    (meson cong_imp_coprime_int cong_sym coprime_1_left coprime_mult_left_iff)
   18.83  
   18.84  lemma coprime_iff_invertible'_nat:
   18.85    "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
   18.86 @@ -554,16 +543,16 @@
   18.87      and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   18.88    using that apply (induct A rule: infinite_finite_induct)
   18.89      apply auto
   18.90 -  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   18.91 +  apply (metis coprime_cong_mult_nat prod_coprime_right)
   18.92    done
   18.93  
   18.94 -lemma cong_cong_prod_coprime_int [rule_format]:
   18.95 +lemma cong_cong_prod_coprime_int:
   18.96    "[x = y] (mod (\<Prod>i\<in>A. m i))" if
   18.97      "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
   18.98      "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   18.99    using that apply (induct A rule: infinite_finite_induct)
  18.100 -  apply auto
  18.101 -  apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
  18.102 +    apply auto
  18.103 +  apply (metis coprime_cong_mult_int prod_coprime_right)
  18.104    done
  18.105  
  18.106  lemma binary_chinese_remainder_aux_nat:
  18.107 @@ -574,7 +563,7 @@
  18.108    from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
  18.109      by auto
  18.110    from a have b: "coprime m2 m1"
  18.111 -    by (subst gcd.commute)
  18.112 +    by (simp add: ac_simps)
  18.113    from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
  18.114      by auto
  18.115    have "[m1 * x1 = 0] (mod m1)"
  18.116 @@ -593,7 +582,7 @@
  18.117    from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
  18.118      by auto
  18.119    from a have b: "coprime m2 m1"
  18.120 -    by (subst gcd.commute)
  18.121 +    by (simp add: ac_simps)
  18.122    from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
  18.123      by auto
  18.124    have "[m1 * x1 = 0] (mod m1)"
  18.125 @@ -730,8 +719,8 @@
  18.126    fix i
  18.127    assume "i \<in> A"
  18.128    with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
  18.129 -    by (intro prod_coprime) auto
  18.130 -  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
  18.131 +    by (intro prod_coprime_left) auto
  18.132 +  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)"
  18.133      by (elim cong_solve_coprime_nat)
  18.134    then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
  18.135      by auto
  18.136 @@ -789,8 +778,8 @@
  18.137    if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
  18.138      and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
  18.139    using that apply (induct A rule: infinite_finite_induct)
  18.140 -  apply auto
  18.141 -  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
  18.142 +    apply auto
  18.143 +  apply (metis coprime_cong_mult_nat prod_coprime_right)
  18.144    done
  18.145  
  18.146  lemma chinese_remainder_unique_nat:
    19.1 --- a/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Nov 11 18:33:35 2017 +0000
    19.2 +++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Nov 11 18:41:08 2017 +0000
    19.3 @@ -65,7 +65,7 @@
    19.4  proof -
    19.5    have "~ p dvd x" using assms zdvd_not_zless S1_def by auto
    19.6    hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x] 
    19.7 -    by (simp add: gcd.commute)
    19.8 +    by (simp add: ac_simps)
    19.9    then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
   19.10    moreover define y where "y = y' * a mod p"
   19.11    ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
    20.1 --- a/src/HOL/Number_Theory/Fib.thy	Sat Nov 11 18:33:35 2017 +0000
    20.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sat Nov 11 18:41:08 2017 +0000
    20.3 @@ -87,17 +87,34 @@
    20.4  
    20.5  lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
    20.6    apply (induct n rule: fib.induct)
    20.7 -  apply auto
    20.8 -  apply (metis gcd_add1 add.commute)
    20.9 +    apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
   20.10 +  apply (simp add: add.assoc [symmetric])
   20.11    done
   20.12  
   20.13 -lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
   20.14 -  apply (simp add: gcd.commute [of "fib m"])
   20.15 -  apply (cases m)
   20.16 -  apply (auto simp add: fib_add)
   20.17 -  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
   20.18 -    gcd_add_mult gcd_mult_cancel gcd.commute)
   20.19 -  done
   20.20 +lemma gcd_fib_add:
   20.21 +  "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
   20.22 +proof (cases m)
   20.23 +  case 0
   20.24 +  then show ?thesis
   20.25 +    by simp
   20.26 +next
   20.27 +  case (Suc q)
   20.28 +  from coprime_fib_Suc_nat [of q]
   20.29 +  have "coprime (fib (Suc q)) (fib q)"
   20.30 +    by (simp add: ac_simps)
   20.31 +  have "gcd (fib q) (fib (Suc q)) = Suc 0"
   20.32 +    using coprime_fib_Suc_nat [of q] by simp
   20.33 +  then have *: "gcd (fib n * fib q) (fib n * fib (Suc q)) = fib n"
   20.34 +    by (simp add: gcd_mult_distrib_nat [symmetric])
   20.35 +  moreover have "gcd (fib (Suc q)) (fib n * fib q + fib (Suc n) * fib (Suc q)) =
   20.36 +    gcd (fib (Suc q)) (fib n * fib q)"
   20.37 +    using gcd_add_mult [of "fib (Suc q)"] by (simp add: ac_simps)
   20.38 +  moreover have "gcd (fib (Suc q)) (fib n * fib (Suc q)) = fib (Suc q)"
   20.39 +    by simp
   20.40 +  ultimately show ?thesis
   20.41 +    using Suc \<open>coprime (fib (Suc q)) (fib q)\<close>
   20.42 +    by (auto simp add: fib_add algebra_simps gcd_mult_right_right_cancel)
   20.43 +qed
   20.44  
   20.45  lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   20.46    by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
    21.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sat Nov 11 18:33:35 2017 +0000
    21.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sat Nov 11 18:41:08 2017 +0000
    21.3 @@ -115,8 +115,9 @@
    21.4    proof -
    21.5      from p_a_relprime have "\<not> p dvd a"
    21.6        by (simp add: cong_altdef_int)
    21.7 -    with p_prime have "coprime a (int p)"
    21.8 -      by (subst gcd.commute, intro prime_imp_coprime) auto
    21.9 +    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
   21.10 +    have "coprime a (int p)"
   21.11 +      by (simp_all add: zdvd_int ac_simps)
   21.12      with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
   21.13        by simp
   21.14      with cong_less_imp_eq_int [of x y p] p_minus_one_l
   21.15 @@ -149,8 +150,9 @@
   21.16        using cong_def by blast
   21.17      from p_a_relprime have "\<not>p dvd a"
   21.18        by (simp add: cong_altdef_int)
   21.19 -    with p_prime have "coprime a (int p)"
   21.20 -      by (subst gcd.commute, intro prime_imp_coprime) auto
   21.21 +    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
   21.22 +    have "coprime a (int p)"
   21.23 +      by (simp_all add: zdvd_int ac_simps)  
   21.24      with a' cong_mult_rcancel_int [of a "int p" x y]
   21.25      have "[x = y] (mod p)" by simp
   21.26      with cong_less_imp_eq_int [of x y p] p_minus_one_l
   21.27 @@ -219,13 +221,16 @@
   21.28    by (auto simp add: D_def C_def B_def A_def)
   21.29  
   21.30  lemma all_A_relprime:
   21.31 -  assumes "x \<in> A"
   21.32 -  shows "gcd x p = 1"
   21.33 -  using p_prime A_ncong_p [OF assms]
   21.34 -  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
   21.35 -
   21.36 -lemma A_prod_relprime: "gcd (prod id A) p = 1"
   21.37 -  by (metis id_def all_A_relprime prod_coprime)
   21.38 +  "coprime x p" if "x \<in> A"
   21.39 +proof -
   21.40 +  from A_ncong_p [OF that] have "\<not> int p dvd x"
   21.41 +    by (simp add: cong_altdef_int)
   21.42 +  with p_prime show ?thesis
   21.43 +    by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer)
   21.44 +qed
   21.45 +  
   21.46 +lemma A_prod_relprime: "coprime (prod id A) p"
   21.47 +  by (auto intro: prod_coprime_left all_A_relprime)
   21.48  
   21.49  
   21.50  subsection \<open>Relationships Between Gauss Sets\<close>
    22.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Sat Nov 11 18:33:35 2017 +0000
    22.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Nov 11 18:41:08 2017 +0000
    22.3 @@ -11,18 +11,11 @@
    22.4  subsection \<open>Lemmas about previously defined terms\<close>
    22.5  
    22.6  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)"
    22.7 -  unfolding prime_nat_iff
    22.8 -proof safe
    22.9 -  fix m
   22.10 -  assume p: "p > 0" "p \<noteq> 1"
   22.11 -    and m: "m dvd p" "m \<noteq> p"
   22.12 -    and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
   22.13 -  from p m have "m \<noteq> 0" by (intro notI) auto
   22.14 -  moreover from p m have "m < p" by (auto dest: dvd_imp_le)
   22.15 -  ultimately have "coprime p m"
   22.16 -    using * by blast
   22.17 -  with m show "m = 1" by simp
   22.18 -qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
   22.19 +  apply (auto simp add: prime_nat_iff)
   22.20 +   apply (rule coprimeI)
   22.21 +   apply (auto dest: nat_dvd_not_less simp add: ac_simps)
   22.22 +  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)
   22.23 +  done
   22.24  
   22.25  lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
   22.26  proof -
   22.27 @@ -46,7 +39,7 @@
   22.28    from bezout_add_strong_nat [OF this]
   22.29    obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
   22.30    from dxy(1,2) have d1: "d = 1"
   22.31 -    by (metis assms coprime_nat)
   22.32 +    using assms coprime_common_divisor [of a n d] by simp
   22.33    with dxy(3) have "a * x * b = (n * y + 1) * b"
   22.34      by simp
   22.35    then have "a * (x * b) = n * (y * b) + b"
   22.36 @@ -94,9 +87,9 @@
   22.37    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
   22.38  proof -
   22.39    from pa have ap: "coprime a p"
   22.40 -    by (metis gcd.commute)
   22.41 -  have px: "coprime x p"
   22.42 -    by (metis gcd.commute p prime_nat_iff'' x0 xp)
   22.43 +    by (simp add: ac_simps)
   22.44 +  from x0 xp p have px: "coprime x p"
   22.45 +    by (auto simp add: prime_nat_iff'' ac_simps)
   22.46    obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
   22.47      by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   22.48    have "y \<noteq> 0"
   22.49 @@ -104,8 +97,8 @@
   22.50      assume "y = 0"
   22.51      with y(2) have "p dvd a"
   22.52        using cong_dvd_iff by auto
   22.53 -    then show False
   22.54 -      by (metis gcd_nat.absorb1 not_prime_1 p pa)
   22.55 +    with not_prime_1 p pa show False
   22.56 +      by (auto simp add: gcd_nat.order_iff)
   22.57    qed
   22.58    with y show ?thesis
   22.59      by blast
   22.60 @@ -128,9 +121,9 @@
   22.61    obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
   22.62      by blast
   22.63    from ma nb x have "coprime x a" "coprime x b"
   22.64 -    by (metis cong_gcd_eq_nat)+
   22.65 +    using cong_imp_coprime_nat cong_sym by blast+
   22.66    then have "coprime x (a*b)"
   22.67 -    by (metis coprime_mul_eq)
   22.68 +    by simp
   22.69    with x show ?thesis
   22.70      by blast
   22.71  qed
   22.72 @@ -164,7 +157,8 @@
   22.73        from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
   22.74          by simp
   22.75      qed
   22.76 -    then show ?thesis by blast
   22.77 +    then show ?thesis
   22.78 +      by (auto intro: coprimeI)
   22.79    qed
   22.80  qed
   22.81  
   22.82 @@ -216,8 +210,8 @@
   22.83    from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
   22.84      by simp
   22.85    from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
   22.86 -  have an: "coprime a n" "coprime (a^(n - 1)) n"
   22.87 -    by (auto simp add: coprime_exp gcd.commute)
   22.88 +  have an: "coprime a n" "coprime (a ^ (n - 1)) n"
   22.89 +    using \<open>n \<ge> 2\<close> by simp_all
   22.90    have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
   22.91    proof -
   22.92      from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
   22.93 @@ -229,7 +223,7 @@
   22.94        let ?y = "a^ ((n - 1) div m * m)"
   22.95        note mdeq = div_mult_mod_eq[of "(n - 1)" m]
   22.96        have yn: "coprime ?y n"
   22.97 -        by (metis an(1) coprime_exp gcd.commute)
   22.98 +        using an(1) by (cases "(n - Suc 0) div m * m = 0") auto
   22.99        have "?y mod n = (a^m)^((n - 1) div m) mod n"
  22.100          by (simp add: algebra_simps power_mult)
  22.101        also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
  22.102 @@ -359,9 +353,11 @@
  22.103      next
  22.104        case (Suc d')
  22.105        then have d0: "d \<noteq> 0" by simp
  22.106 -      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
  22.107 +      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1"
  22.108 +        by (auto elim: not_coprimeE) 
  22.109        from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
  22.110 -        by (metis prem d0 gcd.commute lucas_coprime_lemma)
  22.111 +        using prem d0 lucas_coprime_lemma
  22.112 +        by (auto elim: not_coprimeE simp add: ac_simps)
  22.113        then have "a ^ d + n * q1 - n * q2 = 1" by simp
  22.114        with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
  22.115          by metis
  22.116 @@ -398,8 +394,10 @@
  22.117    qed
  22.118  qed
  22.119  
  22.120 -lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
  22.121 -  by (metis euler_theorem gcd.commute ord_divides that)
  22.122 +lemma order_divides_totient:
  22.123 +  "ord n a dvd totient n" if "coprime n a"
  22.124 +  using that euler_theorem [of a n]
  22.125 +  by (simp add: ord_divides [symmetric] ac_simps)
  22.126  
  22.127  lemma order_divides_expdiff:
  22.128    fixes n::nat and a::nat assumes na: "coprime n a"
  22.129 @@ -412,11 +410,11 @@
  22.130      from na ed have "\<exists>c. d = e + c" by presburger
  22.131      then obtain c where c: "d = e + c" ..
  22.132      from na have an: "coprime a n"
  22.133 -      by (metis gcd.commute)
  22.134 -    have aen: "coprime (a^e) n"
  22.135 -      by (metis coprime_exp gcd.commute na)
  22.136 -    have acn: "coprime (a^c) n"
  22.137 -      by (metis coprime_exp gcd.commute na)
  22.138 +      by (simp add: ac_simps)
  22.139 +    then have aen: "coprime (a ^ e) n"
  22.140 +      by (cases "e > 0") simp_all
  22.141 +    from an have acn: "coprime (a ^ c) n"
  22.142 +      by (cases "c > 0") simp_all
  22.143      from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
  22.144        by simp
  22.145      also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
  22.146 @@ -620,8 +618,9 @@
  22.147        by (metis cong_to_1_nat exps)
  22.148      from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
  22.149        using P0 by simp
  22.150 -    with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
  22.151 -    with p01 pn pd0 coprime_common_divisor_nat show False
  22.152 +    with caP have "coprime (a ^ (ord p (a ^ r) * t * r) - 1) n"
  22.153 +      by simp
  22.154 +    with p01 pn pd0 coprime_common_divisor [of _ n p] show False
  22.155        by auto
  22.156    qed
  22.157    with d have o: "ord p (a^r) = q" by simp
  22.158 @@ -632,12 +631,14 @@
  22.159      assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
  22.160      from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
  22.161      from n have "n \<noteq> 0" by simp
  22.162 -    then have False using d dp pn
  22.163 -      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
  22.164 +    then have False using d dp pn an
  22.165 +      by auto (metis One_nat_def Suc_lessI
  22.166 +        \<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) 
  22.167    }
  22.168 -  then have cpa: "coprime p a" by auto
  22.169 -  have arp: "coprime (a^r) p"
  22.170 -    by (metis coprime_exp cpa gcd.commute)
  22.171 +  then have cpa: "coprime p a"
  22.172 +    by (auto intro: coprimeI)
  22.173 +  then have arp: "coprime (a ^ r) p"
  22.174 +    by (cases "r > 0") (simp_all add: ac_simps)
  22.175    from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
  22.176      by simp
  22.177    then obtain d where d:"p - 1 = q * d"
    23.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Nov 11 18:33:35 2017 +0000
    23.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Nov 11 18:41:08 2017 +0000
    23.3 @@ -106,13 +106,9 @@
    23.4  
    23.5  lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
    23.6    using m_gt_one
    23.7 -  unfolding Units_def R_def residue_ring_def
    23.8 -  apply auto
    23.9 -    apply (subgoal_tac "x \<noteq> 0")
   23.10 -     apply auto
   23.11 -   apply (metis invertible_coprime_int)
   23.12 +  apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
   23.13    apply (subst (asm) coprime_iff_invertible'_int)
   23.14 -   apply (auto simp add: cong_def mult.commute)
   23.15 +   apply (auto simp add: cong_def)
   23.16    done
   23.17  
   23.18  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
   23.19 @@ -220,6 +216,22 @@
   23.20  context residues_prime
   23.21  begin
   23.22  
   23.23 +lemma p_coprime_left:
   23.24 +  "coprime p a \<longleftrightarrow> \<not> p dvd a"
   23.25 +  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
   23.26 +
   23.27 +lemma p_coprime_right:
   23.28 +  "coprime a p  \<longleftrightarrow> \<not> p dvd a"
   23.29 +  using p_coprime_left [of a] by (simp add: ac_simps)
   23.30 +
   23.31 +lemma p_coprime_left_int:
   23.32 +  "coprime (int p) a \<longleftrightarrow> \<not> int p dvd a"
   23.33 +  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
   23.34 +
   23.35 +lemma p_coprime_right_int:
   23.36 +  "coprime a (int p) \<longleftrightarrow> \<not> int p dvd a"
   23.37 +  using p_coprime_left_int [of a] by (simp add: ac_simps)
   23.38 +
   23.39  lemma is_field: "field R"
   23.40  proof -
   23.41    have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
   23.42 @@ -231,9 +243,7 @@
   23.43  
   23.44  lemma res_prime_units_eq: "Units R = {1..p - 1}"
   23.45    apply (subst res_units_eq)
   23.46 -  apply auto
   23.47 -  apply (subst gcd.commute)
   23.48 -  apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
   23.49 +  apply (auto simp add: p_coprime_right_int zdvd_not_zless)
   23.50    done
   23.51  
   23.52  end
   23.53 @@ -246,26 +256,27 @@
   23.54  
   23.55  subsection \<open>Euler's theorem\<close>
   23.56  
   23.57 -lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
   23.58 +lemma (in residues) totatives_eq:
   23.59 +  "totatives (nat m) = nat ` Units R"
   23.60  proof -
   23.61 +  from m_gt_one have "\<bar>m\<bar> > 1"
   23.62 +    by simp
   23.63 +  then have "totatives (nat \<bar>m\<bar>) = nat ` abs ` Units R"
   23.64 +    by (auto simp add: totatives_def res_units_eq image_iff le_less)
   23.65 +      (use m_gt_one zless_nat_eq_int_zless in force)
   23.66 +  moreover have "\<bar>m\<bar> = m" "abs ` Units R = Units R"
   23.67 +    using m_gt_one by (auto simp add: res_units_eq image_iff)
   23.68 +  ultimately show ?thesis
   23.69 +    by simp
   23.70 +qed
   23.71 +
   23.72 +lemma (in residues) totient_eq:
   23.73 +  "totient (nat m) = card (Units R)"
   23.74 +proof  -
   23.75    have *: "inj_on nat (Units R)"
   23.76      by (rule inj_onI) (auto simp add: res_units_eq)
   23.77 -  define m' where "m' = nat m"
   23.78 -  from m_gt_one have "m = int m'" "m' > 1"
   23.79 -    by (simp_all add: m'_def)
   23.80 -  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
   23.81 -    unfolding res_units_eq
   23.82 -    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
   23.83 -  then have "Units R = int ` totatives m'"
   23.84 -    by blast
   23.85 -  then have "totatives m' = nat ` Units R"
   23.86 -    by (simp add: image_image)
   23.87 -  then have "card (totatives (nat m)) = card (nat ` Units R)"
   23.88 -    by (simp add: m'_def)
   23.89 -  also have "\<dots> = card (Units R)"
   23.90 -    using * card_image [of nat "Units R"] by auto
   23.91 -  finally show ?thesis
   23.92 -    by (simp add: totient_def)
   23.93 +  then show ?thesis
   23.94 +    by (simp add: totient_def totatives_eq card_image)
   23.95  qed
   23.96  
   23.97  lemma (in residues_prime) totient_eq: "totient p = p - 1"
    24.1 --- a/src/HOL/Number_Theory/Totient.thy	Sat Nov 11 18:33:35 2017 +0000
    24.2 +++ b/src/HOL/Number_Theory/Totient.thy	Sat Nov 11 18:41:08 2017 +0000
    24.3 @@ -15,7 +15,7 @@
    24.4    
    24.5  definition totatives :: "nat \<Rightarrow> nat set" where
    24.6    "totatives n = {k \<in> {0<..n}. coprime k n}"
    24.7 -  
    24.8 +
    24.9  lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
   24.10    by (simp add: totatives_def)
   24.11    
   24.12 @@ -60,7 +60,7 @@
   24.13  lemma minus_one_in_totatives:
   24.14    assumes "n \<ge> 2"
   24.15    shows "n - 1 \<in> totatives n"
   24.16 -  using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff)
   24.17 +  using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
   24.18  
   24.19  lemma totatives_prime_power_Suc:
   24.20    assumes "prime p"
   24.21 @@ -72,7 +72,8 @@
   24.22    fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
   24.23    from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
   24.24    hence "coprime k (p ^ Suc n)"
   24.25 -    using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute)
   24.26 +    using prime_imp_coprime [OF assms, of k]
   24.27 +    by (cases "n > 0") (auto simp add: ac_simps)
   24.28    with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
   24.29  qed (auto simp: totatives_def)
   24.30  
   24.31 @@ -101,14 +102,15 @@
   24.32    proof safe
   24.33      fix x assume "x \<in> totatives (m1 * m2)"
   24.34      with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
   24.35 -      by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
   24.36 +      using coprime_common_divisor [of x m1 m1] coprime_common_divisor [of x m2 m2]
   24.37 +      by (auto simp add: in_totatives_iff mod_greater_zero_iff_not_dvd)
   24.38    next
   24.39      fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
   24.40      with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
   24.41      with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
   24.42        where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
   24.43      from x ab assms(3) have "x \<in> totatives (m1 * m2)"
   24.44 -      by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
   24.45 +      by (auto intro: ccontr simp add: in_totatives_iff)
   24.46      with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
   24.47    qed
   24.48  qed
   24.49 @@ -125,21 +127,18 @@
   24.50    show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
   24.51    proof (intro equalityI subsetI, goal_cases)
   24.52      case (1 k)
   24.53 -    thus ?case using assms
   24.54 -      by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d]
   24.55 -                                 gcd_mult_right gcd.commute)
   24.56 +    then show ?case using assms
   24.57 +      by (auto elim: dvdE simp add: in_totatives_iff ac_simps gcd_mult_right)
   24.58    next
   24.59      case (2 k)
   24.60      hence "d dvd k" by auto
   24.61      then obtain l where k: "k = l * d" by (elim dvdE) auto
   24.62 -    from 2 and assms show ?case unfolding k
   24.63 -      by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d] 
   24.64 -                                    gcd_mult_right elim!: dvdE)
   24.65 +    from 2 assms show ?case
   24.66 +      using gcd_mult_right [of _ d l]
   24.67 +      by (auto intro: gcd_eq_1_imp_coprime elim!: dvdE simp add: k image_iff in_totatives_iff ac_simps)
   24.68    qed
   24.69  qed
   24.70  
   24.71 -
   24.72 -
   24.73  definition totient :: "nat \<Rightarrow> nat" where
   24.74    "totient n = card (totatives n)"
   24.75    
   24.76 @@ -272,7 +271,8 @@
   24.77    proof -
   24.78      from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
   24.79      from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
   24.80 -    from that and nz have "\<not>coprime x p" by auto
   24.81 +    from that and nz have "\<not>coprime x p"
   24.82 +      by (auto elim: dvdE)
   24.83      hence "x \<notin> totatives p" by (simp add: totatives_def)
   24.84      also note *
   24.85      finally show False using that and le by auto
   24.86 @@ -299,7 +299,8 @@
   24.87    by simp_all
   24.88      
   24.89  lemma totient_6 [simp]: "totient 6 = 2"
   24.90 -  using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat)    
   24.91 +  using totient_mult_coprime [of 2 3] coprime_add_one_right [of 2]
   24.92 +  by simp
   24.93  
   24.94  lemma totient_even:
   24.95    assumes "n > 2"
   24.96 @@ -314,11 +315,14 @@
   24.97    have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
   24.98    then obtain m where m: "n = p ^ k * m" by (elim dvdE)
   24.99    with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
  24.100 -  from k_def m_pos p have "\<not>p dvd m"
  24.101 +  from k_def m_pos p have "\<not> p dvd m"
  24.102      by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib 
  24.103                            prime_elem_multiplicity_eq_zero_iff)
  24.104 -  hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)])
  24.105 -  thus ?thesis using p k_pos \<open>odd p\<close> 
  24.106 +  with \<open>prime p\<close> have "coprime p m"
  24.107 +    by (rule prime_imp_coprime)
  24.108 +  with \<open>k > 0\<close> have "coprime (p ^ k) m"
  24.109 +    by simp
  24.110 +  then show ?thesis using p k_pos \<open>odd p\<close> 
  24.111      by (auto simp add: m totient_mult_coprime totient_prime_power)
  24.112  next
  24.113    case False
  24.114 @@ -341,7 +345,7 @@
  24.115  proof (induction A rule: infinite_finite_induct)
  24.116    case (insert x A)
  24.117    have *: "coprime (prod f A) (f x)"
  24.118 -  proof (rule prod_coprime)
  24.119 +  proof (rule prod_coprime_left)
  24.120      fix y
  24.121      assume "y \<in> A"
  24.122      with \<open>x \<notin> A\<close> have "y \<noteq> x"
  24.123 @@ -388,10 +392,12 @@
  24.124    proof (rule totient_prod_coprime)
  24.125      show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
  24.126      proof (rule pairwiseI, clarify)
  24.127 -      fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
  24.128 +      fix p q assume *: "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
  24.129                       "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
  24.130 -      thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
  24.131 -        by (intro coprime_exp2 primes_coprime[of p q]) auto
  24.132 +      then have "multiplicity p n > 0" "multiplicity q n > 0"
  24.133 +        by (simp_all add: prime_factors_multiplicity)
  24.134 +      with * primes_coprime [of p q] show "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
  24.135 +        by auto
  24.136      qed
  24.137    next
  24.138      show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
  24.139 @@ -475,20 +481,22 @@
  24.140    by (subst totient_gcd [symmetric]) simp
  24.141  
  24.142  lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
  24.143 -  using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff)
  24.144 +  by (fact of_nat_eq_1_iff)
  24.145  
  24.146  (* TODO Move *)
  24.147 -lemma gcd_2_odd:
  24.148 +lemma odd_imp_coprime_nat:
  24.149    assumes "odd (n::nat)"
  24.150 -  shows   "gcd n 2 = 1"
  24.151 +  shows   "coprime n 2"
  24.152  proof -
  24.153    from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
  24.154 -  have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat)
  24.155 -  thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all
  24.156 +  have "coprime (Suc (2 * k)) (2 * k)"
  24.157 +    by (fact coprime_Suc_left_nat)
  24.158 +  then show ?thesis using n
  24.159 +    by simp
  24.160  qed
  24.161  
  24.162  lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
  24.163 -  by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd)
  24.164 +  by (simp add: totient_mult ac_simps odd_imp_coprime_nat)
  24.165  
  24.166  lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
  24.167  proof (induction m arbitrary: n)
    25.1 --- a/src/HOL/Parity.thy	Sat Nov 11 18:33:35 2017 +0000
    25.2 +++ b/src/HOL/Parity.thy	Sat Nov 11 18:41:08 2017 +0000
    25.3 @@ -318,6 +318,38 @@
    25.4    using mult_div_mod_eq [of 2 a]
    25.5    by (simp add: even_iff_mod_2_eq_zero)
    25.6  
    25.7 +lemma coprime_left_2_iff_odd [simp]:
    25.8 +  "coprime 2 a \<longleftrightarrow> odd a"
    25.9 +proof
   25.10 +  assume "odd a"
   25.11 +  show "coprime 2 a"
   25.12 +  proof (rule coprimeI)
   25.13 +    fix b
   25.14 +    assume "b dvd 2" "b dvd a"
   25.15 +    then have "b dvd a mod 2"
   25.16 +      by (auto intro: dvd_mod)
   25.17 +    with \<open>odd a\<close> show "is_unit b"
   25.18 +      by (simp add: mod_2_eq_odd)
   25.19 +  qed
   25.20 +next
   25.21 +  assume "coprime 2 a"
   25.22 +  show "odd a"
   25.23 +  proof (rule notI)
   25.24 +    assume "even a"
   25.25 +    then obtain b where "a = 2 * b" ..
   25.26 +    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
   25.27 +      by simp
   25.28 +    moreover have "\<not> coprime 2 (2 * b)"
   25.29 +      by (rule not_coprimeI [of 2]) simp_all
   25.30 +    ultimately show False
   25.31 +      by blast
   25.32 +  qed
   25.33 +qed
   25.34 +
   25.35 +lemma coprime_right_2_iff_odd [simp]:
   25.36 +  "coprime a 2 \<longleftrightarrow> odd a"
   25.37 +  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
   25.38 +
   25.39  end
   25.40  
   25.41  class ring_parity = ring + semiring_parity
    26.1 --- a/src/HOL/Rat.thy	Sat Nov 11 18:33:35 2017 +0000
    26.2 +++ b/src/HOL/Rat.thy	Sat Nov 11 18:41:08 2017 +0000
    26.3 @@ -999,7 +999,7 @@
    26.4  proof (cases p)
    26.5    case (Fract a b)
    26.6    then show ?thesis
    26.7 -    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
    26.8 +    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract ac_simps)
    26.9  qed
   26.10  
   26.11  lemma rat_divide_code [code abstract]:
   26.12 @@ -1008,9 +1008,10 @@
   26.13       in normalize (a * d, c * b))"
   26.14    by (cases p, cases q) (simp add: quotient_of_Fract)
   26.15  
   26.16 -lemma rat_abs_code [code abstract]: "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
   26.17 +lemma rat_abs_code [code abstract]:
   26.18 +  "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
   26.19    by (cases p) (simp add: quotient_of_Fract)
   26.20 -
   26.21 +  
   26.22  lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
   26.23  proof (cases p)
   26.24    case (Fract a b)
    27.1 --- a/src/HOL/Real.thy	Sat Nov 11 18:33:35 2017 +0000
    27.2 +++ b/src/HOL/Real.thy	Sat Nov 11 18:41:08 2017 +0000
    27.3 @@ -1245,7 +1245,7 @@
    27.4  
    27.5  lemma Rats_abs_nat_div_natE:
    27.6    assumes "x \<in> \<rat>"
    27.7 -  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
    27.8 +  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "coprime m n"
    27.9  proof -
   27.10    from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n"
   27.11      by (auto simp add: Rats_eq_int_div_nat)
   27.12 @@ -1281,6 +1281,8 @@
   27.13      with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
   27.14      with gcd show ?thesis by auto
   27.15    qed
   27.16 +  then have "coprime ?k ?l"
   27.17 +    by (simp only: coprime_iff_gcd_eq_1)
   27.18    ultimately show ?thesis ..
   27.19  qed
   27.20  
   27.21 @@ -1415,8 +1417,6 @@
   27.22    for m :: nat
   27.23    by (metis not_le real_of_nat_less_numeral_iff)
   27.24  
   27.25 -declare of_int_floor_le [simp]  (* FIXME duplicate!? *)
   27.26 -
   27.27  lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
   27.28    by (metis floor_of_int)
   27.29  
   27.30 @@ -1424,7 +1424,7 @@
   27.31    by linarith
   27.32  
   27.33  lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
   27.34 -  by linarith
   27.35 +  by (fact floor_unique)
   27.36  
   27.37  lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
   27.38    by linarith
    28.1 --- a/src/HOL/Rings.thy	Sat Nov 11 18:33:35 2017 +0000
    28.2 +++ b/src/HOL/Rings.thy	Sat Nov 11 18:41:08 2017 +0000
    28.3 @@ -1161,6 +1161,108 @@
    28.4    "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
    28.5    by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
    28.6  
    28.7 +
    28.8 +text \<open>Coprimality\<close>
    28.9 +
   28.10 +definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   28.11 +  where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)"
   28.12 +
   28.13 +lemma coprimeI:
   28.14 +  assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c"
   28.15 +  shows "coprime a b"
   28.16 +  using assms by (auto simp: coprime_def)
   28.17 +
   28.18 +lemma not_coprimeI:
   28.19 +  assumes "c dvd a" and "c dvd b" and "\<not> is_unit c"
   28.20 +  shows "\<not> coprime a b"
   28.21 +  using assms by (auto simp: coprime_def)
   28.22 +
   28.23 +lemma coprime_common_divisor:
   28.24 +  "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
   28.25 +  using that by (auto simp: coprime_def)
   28.26 +
   28.27 +lemma not_coprimeE:
   28.28 +  assumes "\<not> coprime a b"
   28.29 +  obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c"
   28.30 +  using assms by (auto simp: coprime_def)
   28.31 +
   28.32 +lemma coprime_imp_coprime:
   28.33 +  "coprime a b" if "coprime c d"
   28.34 +    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c"
   28.35 +    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d"
   28.36 +proof (rule coprimeI)
   28.37 +  fix e
   28.38 +  assume "e dvd a" and "e dvd b"
   28.39 +  with that have "e dvd c" and "e dvd d"
   28.40 +    by (auto intro: dvd_trans)
   28.41 +  with \<open>coprime c d\<close> show "is_unit e"
   28.42 +    by (rule coprime_common_divisor)
   28.43 +qed
   28.44 +
   28.45 +lemma coprime_divisors:
   28.46 +  "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
   28.47 +using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
   28.48 +  fix e
   28.49 +  assume "e dvd a" then show "e dvd c"
   28.50 +    using \<open>a dvd c\<close> by (rule dvd_trans)
   28.51 +  assume "e dvd b" then show "e dvd d"
   28.52 +    using \<open>b dvd d\<close> by (rule dvd_trans)
   28.53 +qed
   28.54 +
   28.55 +lemma coprime_self [simp]:
   28.56 +  "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
   28.57 +proof
   28.58 +  assume ?P
   28.59 +  then show ?Q
   28.60 +    by (rule coprime_common_divisor) simp_all
   28.61 +next
   28.62 +  assume ?Q
   28.63 +  show ?P
   28.64 +    by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
   28.65 +qed
   28.66 +
   28.67 +lemma coprime_commute [ac_simps]:
   28.68 +  "coprime b a \<longleftrightarrow> coprime a b"
   28.69 +  unfolding coprime_def by auto
   28.70 +
   28.71 +lemma is_unit_left_imp_coprime:
   28.72 +  "coprime a b" if "is_unit a"
   28.73 +proof (rule coprimeI)
   28.74 +  fix c
   28.75 +  assume "c dvd a"
   28.76 +  with that show "is_unit c"
   28.77 +    by (auto intro: dvd_unit_imp_unit)
   28.78 +qed
   28.79 +
   28.80 +lemma is_unit_right_imp_coprime:
   28.81 +  "coprime a b" if "is_unit b"
   28.82 +  using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)
   28.83 +
   28.84 +lemma coprime_1_left [simp]:
   28.85 +  "coprime 1 a"
   28.86 +  by (rule coprimeI)
   28.87 +
   28.88 +lemma coprime_1_right [simp]:
   28.89 +  "coprime a 1"
   28.90 +  by (rule coprimeI)
   28.91 +
   28.92 +lemma coprime_0_left_iff [simp]:
   28.93 +  "coprime 0 a \<longleftrightarrow> is_unit a"
   28.94 +  by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])
   28.95 +
   28.96 +lemma coprime_0_right_iff [simp]:
   28.97 +  "coprime a 0 \<longleftrightarrow> is_unit a"
   28.98 +  using coprime_0_left_iff [of a] by (simp add: ac_simps)
   28.99 +
  28.100 +lemma coprime_mult_self_left_iff [simp]:
  28.101 +  "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b"
  28.102 +  by (auto intro: coprime_common_divisor)
  28.103 +    (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+
  28.104 +
  28.105 +lemma coprime_mult_self_right_iff [simp]:
  28.106 +  "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
  28.107 +  using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
  28.108 +
  28.109  end
  28.110  
  28.111  class unit_factor =
  28.112 @@ -1430,6 +1532,14 @@
  28.113    shows "is_unit a \<longleftrightarrow> a = 1"
  28.114    using assms by (cases "a = 0") (auto dest: is_unit_normalize)
  28.115  
  28.116 +lemma coprime_normalize_left_iff [simp]:
  28.117 +  "coprime (normalize a) b \<longleftrightarrow> coprime a b"
  28.118 +  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
  28.119 +
  28.120 +lemma coprime_normalize_right_iff [simp]:
  28.121 +  "coprime a (normalize b) \<longleftrightarrow> coprime a b"
  28.122 +  using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)
  28.123 +
  28.124  text \<open>
  28.125    We avoid an explicit definition of associated elements but prefer explicit
  28.126    normalisation instead. In theory we could define an abbreviation like @{prop
  28.127 @@ -2435,8 +2545,8 @@
  28.128  subclass ordered_ring_abs
  28.129    by standard (auto simp: abs_if not_less mult_less_0_iff)
  28.130  
  28.131 -lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  28.132 -  by (simp add: abs_if)
  28.133 +lemma abs_mult_self: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
  28.134 +  by (fact abs_mult_self_eq)
  28.135  
  28.136  lemma abs_mult_less:
  28.137    assumes ac: "\<bar>a\<bar> < c"
    29.1 --- a/src/HOL/Set.thy	Sat Nov 11 18:33:35 2017 +0000
    29.2 +++ b/src/HOL/Set.thy	Sat Nov 11 18:41:08 2017 +0000
    29.3 @@ -1874,6 +1874,11 @@
    29.4  lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
    29.5    by (auto simp: pairwise_def)
    29.6  
    29.7 +lemma pairwise_imageI:
    29.8 +  "pairwise P (f ` A)"
    29.9 +  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)"
   29.10 +  using that by (auto intro: pairwiseI)
   29.11 +
   29.12  lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
   29.13    by (force simp: pairwise_def)
   29.14