src/HOL/Number_Theory/Cong.thy
 changeset 67051 e7e54a0b9197 parent 66954 0230af0f3c59 child 67085 f5d7f37b4143
```     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -229,7 +229,8 @@
1.4  lemma cong_mult_rcancel_int:
1.5    "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
1.6    if "coprime k m" for a k m :: int
1.7 -  by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
1.8 +  using that by (simp add: cong_altdef_int)
1.9 +    (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib')
1.10
1.11  lemma cong_mult_rcancel_nat:
1.12    "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
1.13 @@ -242,7 +243,7 @@
1.14    also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
1.15      by (simp add: abs_mult nat_times_as_int)
1.16    also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
1.17 -    by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
1.18 +    by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
1.19    also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
1.21    finally show ?thesis .
1.22 @@ -320,11 +321,11 @@
1.23
1.24  lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.25    for a b :: nat
1.26 -  by (auto simp add: cong_gcd_eq_nat)
1.27 +  by (auto simp add: cong_gcd_eq_nat coprime_iff_gcd_eq_1)
1.28
1.29  lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
1.30    for a b :: int
1.31 -  by (auto simp add: cong_gcd_eq_int)
1.32 +  by (auto simp add: cong_gcd_eq_int coprime_iff_gcd_eq_1)
1.33
1.34  lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
1.35    for a b :: nat
1.36 @@ -490,36 +491,24 @@
1.37  qed
1.38
1.39  lemma cong_solve_coprime_nat:
1.40 -  fixes a :: nat
1.41 -  assumes "coprime a n"
1.42 -  shows "\<exists>x. [a * x = 1] (mod n)"
1.43 -proof (cases "a = 0")
1.44 -  case True
1.45 -  with assms show ?thesis
1.46 -    by (simp add: cong_0_1_nat')
1.47 -next
1.48 -  case False
1.49 -  with assms show ?thesis
1.50 -    by (metis cong_solve_nat)
1.51 -qed
1.52 +  "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
1.53 +  using that cong_solve_nat [of a n] by (cases "a = 0") simp_all
1.54
1.55 -lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
1.56 -  apply (cases "a = 0")
1.57 -   apply auto
1.58 -   apply (cases "n \<ge> 0")
1.59 -    apply auto
1.60 -  apply (metis cong_solve_int)
1.61 -  done
1.62 +lemma cong_solve_coprime_int:
1.63 +  "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
1.64 +  using that cong_solve_int [of a n] by (cases "a = 0")
1.65 +    (auto simp add: zabs_def split: if_splits)
1.66
1.67  lemma coprime_iff_invertible_nat:
1.68 -  "m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))"
1.69 -  by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0)
1.70 +  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))"
1.71 +  by (auto intro: cong_solve_coprime_nat)
1.72 +    (use cong_imp_coprime_nat cong_sym coprime_Suc_0_left coprime_mult_left_iff in blast)
1.73
1.74 -lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
1.75 +lemma coprime_iff_invertible_int:
1.76 +  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
1.77    for m :: int
1.78 -  apply (auto intro: cong_solve_coprime_int)
1.79 -  using cong_gcd_eq_int coprime_mul_eq' apply fastforce
1.80 -  done
1.81 +  by (auto intro: cong_solve_coprime_int)
1.82 +    (meson cong_imp_coprime_int cong_sym coprime_1_left coprime_mult_left_iff)
1.83
1.84  lemma coprime_iff_invertible'_nat:
1.85    "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
1.86 @@ -554,16 +543,16 @@
1.87      and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
1.88    using that apply (induct A rule: infinite_finite_induct)
1.89      apply auto
1.90 -  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
1.91 +  apply (metis coprime_cong_mult_nat prod_coprime_right)
1.92    done
1.93
1.94 -lemma cong_cong_prod_coprime_int [rule_format]:
1.95 +lemma cong_cong_prod_coprime_int:
1.96    "[x = y] (mod (\<Prod>i\<in>A. m i))" if
1.97      "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
1.98      "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
1.99    using that apply (induct A rule: infinite_finite_induct)
1.100 -  apply auto
1.101 -  apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
1.102 +    apply auto
1.103 +  apply (metis coprime_cong_mult_int prod_coprime_right)
1.104    done
1.105
1.106  lemma binary_chinese_remainder_aux_nat:
1.107 @@ -574,7 +563,7 @@
1.108    from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
1.109      by auto
1.110    from a have b: "coprime m2 m1"
1.111 -    by (subst gcd.commute)
1.112 +    by (simp add: ac_simps)
1.113    from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
1.114      by auto
1.115    have "[m1 * x1 = 0] (mod m1)"
1.116 @@ -593,7 +582,7 @@
1.117    from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
1.118      by auto
1.119    from a have b: "coprime m2 m1"
1.120 -    by (subst gcd.commute)
1.121 +    by (simp add: ac_simps)
1.122    from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
1.123      by auto
1.124    have "[m1 * x1 = 0] (mod m1)"
1.125 @@ -730,8 +719,8 @@
1.126    fix i
1.127    assume "i \<in> A"
1.128    with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
1.129 -    by (intro prod_coprime) auto
1.130 -  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
1.131 +    by (intro prod_coprime_left) auto
1.132 +  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)"
1.133      by (elim cong_solve_coprime_nat)
1.134    then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
1.135      by auto
1.136 @@ -789,8 +778,8 @@
1.137    if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
1.138      and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
1.139    using that apply (induct A rule: infinite_finite_induct)
1.140 -  apply auto
1.141 -  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
1.142 +    apply auto
1.143 +  apply (metis coprime_cong_mult_nat prod_coprime_right)
1.144    done
1.145
1.146  lemma chinese_remainder_unique_nat:
```