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.20      by (simp add: cong_altdef_nat')
    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: