tuned and generalized
authorhaftmann
Thu Nov 23 17:03:21 2017 +0000 (17 months ago)
changeset 67085f5d7f37b4143
parent 67084 e138d96ed083
child 67086 59d07a95be0e
tuned and generalized
src/HOL/Number_Theory/Cong.thy
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:20 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:21 2017 +0000
     1.3 @@ -43,26 +43,6 @@
     1.4  abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(1[_ \<noteq> _] '(()mod _'))")
     1.5    where "notcong b c a \<equiv> \<not> cong b c a"
     1.6  
     1.7 -lemma cong_mod_left [simp]:
     1.8 -  "[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
     1.9 -  by (simp add: cong_def)  
    1.10 -
    1.11 -lemma cong_mod_right [simp]:
    1.12 -  "[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)"
    1.13 -  by (simp add: cong_def)  
    1.14 -
    1.15 -lemma cong_dvd_iff:
    1.16 -  "a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)"
    1.17 -  using that by (auto simp: cong_def dvd_eq_mod_eq_0)
    1.18 -
    1.19 -lemma cong_0 [simp, presburger]:
    1.20 -  "[b = c] (mod 0) \<longleftrightarrow> b = c"
    1.21 -  by (simp add: cong_def)
    1.22 -
    1.23 -lemma cong_1 [simp, presburger]:
    1.24 -  "[b = c] (mod 1)"
    1.25 -  by (simp add: cong_def)
    1.26 -
    1.27  lemma cong_refl [simp]:
    1.28    "[b = b] (mod a)"
    1.29    by (simp add: cong_def)
    1.30 @@ -79,6 +59,37 @@
    1.31    "[b = c] (mod a) \<Longrightarrow> [c = d] (mod a) \<Longrightarrow> [b = d] (mod a)"
    1.32    by (simp add: cong_def)
    1.33  
    1.34 +lemma cong_mult_self_right:
    1.35 +  "[b * a = 0] (mod a)"
    1.36 +  by (simp add: cong_def)
    1.37 +
    1.38 +lemma cong_mult_self_left:
    1.39 +  "[a * b = 0] (mod a)"
    1.40 +  by (simp add: cong_def)
    1.41 +
    1.42 +lemma cong_mod_left [simp]:
    1.43 +  "[b mod a = c] (mod a) \<longleftrightarrow> [b = c] (mod a)"
    1.44 +  by (simp add: cong_def)  
    1.45 +
    1.46 +lemma cong_mod_right [simp]:
    1.47 +  "[b = c mod a] (mod a) \<longleftrightarrow> [b = c] (mod a)"
    1.48 +  by (simp add: cong_def)  
    1.49 +
    1.50 +lemma cong_0 [simp, presburger]:
    1.51 +  "[b = c] (mod 0) \<longleftrightarrow> b = c"
    1.52 +  by (simp add: cong_def)
    1.53 +
    1.54 +lemma cong_1 [simp, presburger]:
    1.55 +  "[b = c] (mod 1)"
    1.56 +  by (simp add: cong_def)
    1.57 +
    1.58 +lemma cong_dvd_iff:
    1.59 +  "a dvd b \<longleftrightarrow> a dvd c" if "[b = c] (mod a)"
    1.60 +  using that by (auto simp: cong_def dvd_eq_mod_eq_0)
    1.61 +
    1.62 +lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b"
    1.63 +  by (simp add: cong_def dvd_eq_mod_eq_0)
    1.64 +
    1.65  lemma cong_add:
    1.66    "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b + d = c + e] (mod a)"
    1.67    by (auto simp add: cong_def intro: mod_add_cong)
    1.68 @@ -87,6 +98,14 @@
    1.69    "[b = c] (mod a) \<Longrightarrow> [d = e] (mod a) \<Longrightarrow> [b * d = c * e] (mod a)"
    1.70    by (auto simp add: cong_def intro: mod_mult_cong)
    1.71  
    1.72 +lemma cong_scalar_right:
    1.73 +  "[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)"
    1.74 +  by (simp add: cong_mult)
    1.75 +
    1.76 +lemma cong_scalar_left:
    1.77 +  "[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)"
    1.78 +  by (simp add: cong_mult)
    1.79 +
    1.80  lemma cong_pow:
    1.81    "[b = c] (mod a) \<Longrightarrow> [b ^ n = c ^ n] (mod a)"
    1.82    by (simp add: cong_def power_mod [symmetric, of b n a] power_mod [symmetric, of c n a])
    1.83 @@ -99,23 +118,6 @@
    1.84    "[prod f A = prod g A] (mod a)" if "(\<And>x. x \<in> A \<Longrightarrow> [f x = g x] (mod a))"
    1.85    using that by (induct A rule: infinite_finite_induct) (auto intro: cong_mult)
    1.86  
    1.87 -lemma cong_scalar_right:
    1.88 -  "[b = c] (mod a) \<Longrightarrow> [b * d = c * d] (mod a)"
    1.89 -  by (simp add: cong_mult)
    1.90 -
    1.91 -lemma cong_scalar_left:
    1.92 -  "[b = c] (mod a) \<Longrightarrow> [d * b = d * c] (mod a)"
    1.93 -  by (simp add: cong_mult)
    1.94 -
    1.95 -lemma cong_mult_self_right: "[b * a = 0] (mod a)"
    1.96 -  by (simp add: cong_def)
    1.97 -
    1.98 -lemma cong_mult_self_left: "[a * b = 0] (mod a)"
    1.99 -  by (simp add: cong_def)
   1.100 -
   1.101 -lemma cong_0_iff: "[b = 0] (mod a) \<longleftrightarrow> a dvd b"
   1.102 -  by (simp add: cong_def dvd_eq_mod_eq_0)
   1.103 -
   1.104  lemma mod_mult_cong_right:
   1.105    "[c mod (a * b) = d] (mod a) \<longleftrightarrow> [c = d] (mod a)"
   1.106    by (simp add: cong_def mod_mod_cancel mod_add_left_eq)
   1.107 @@ -207,14 +209,15 @@
   1.108  
   1.109  lemma cong_altdef_nat':
   1.110    "[a = b] (mod m) \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
   1.111 -  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0_nat')
   1.112 +  using cong_diff_iff_cong_0_nat' [of a b m]
   1.113 +  by (simp only: cong_0_iff [symmetric])
   1.114  
   1.115  lemma cong_altdef_int:
   1.116    "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
   1.117    for a b :: int
   1.118    by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
   1.119  
   1.120 -lemma cong_abs_int [simp]: "[x = y] (mod abs m) \<longleftrightarrow> [x = y] (mod m)"
   1.121 +lemma cong_abs_int [simp]: "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
   1.122    for x y :: int
   1.123    by (simp add: cong_altdef_int)
   1.124  
   1.125 @@ -321,11 +324,11 @@
   1.126  
   1.127  lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   1.128    for a b :: nat
   1.129 -  by (auto simp add: cong_gcd_eq_nat coprime_iff_gcd_eq_1)
   1.130 +  by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_nat)
   1.131  
   1.132  lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   1.133    for a b :: int
   1.134 -  by (auto simp add: cong_gcd_eq_int coprime_iff_gcd_eq_1)
   1.135 +  by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_int)
   1.136  
   1.137  lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   1.138    for a b :: nat
   1.139 @@ -339,23 +342,6 @@
   1.140    for a b :: int
   1.141    by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
   1.142  
   1.143 -(*
   1.144 -lemma mod_dvd_mod_int:
   1.145 -    "0 < (m::int) \<Longrightarrow> m dvd b \<Longrightarrow> (a mod b mod m) = (a mod m)"
   1.146 -  apply (unfold dvd_def, auto)
   1.147 -  apply (rule mod_mod_cancel)
   1.148 -  apply auto
   1.149 -  done
   1.150 -
   1.151 -lemma mod_dvd_mod:
   1.152 -  assumes "0 < (m::nat)" and "m dvd b"
   1.153 -  shows "(a mod b mod m) = (a mod m)"
   1.154 -
   1.155 -  apply (rule mod_dvd_mod_int [transferred])
   1.156 -  using assms apply auto
   1.157 -  done
   1.158 -*)
   1.159 -
   1.160  lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   1.161    for a x y :: nat
   1.162    by (simp add: cong_iff_lin_nat)
   1.163 @@ -374,19 +360,19 @@
   1.164  
   1.165  lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   1.166    for a x :: nat
   1.167 -  by (simp add: cong_iff_lin_nat)
   1.168 +  using cong_add_lcancel_nat [of a x 0 n] by simp
   1.169  
   1.170  lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   1.171    for a x :: int
   1.172 -  by (simp add: cong_iff_lin_int)
   1.173 +  using cong_add_lcancel_int [of a x 0 n] by simp
   1.174  
   1.175  lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   1.176    for a x :: nat
   1.177 -  by (simp add: cong_iff_lin_nat)
   1.178 +  using cong_add_rcancel_nat [of x a 0 n] by simp
   1.179  
   1.180  lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   1.181    for a x :: int
   1.182 -  by (simp add: cong_iff_lin_int)
   1.183 +  using cong_add_rcancel_int [of x a 0 n] by simp
   1.184  
   1.185  lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   1.186    for x y :: nat
   1.187 @@ -500,15 +486,32 @@
   1.188      (auto simp add: zabs_def split: if_splits)
   1.189  
   1.190  lemma coprime_iff_invertible_nat:
   1.191 -  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))"
   1.192 -  by (auto intro: cong_solve_coprime_nat)
   1.193 -    (use cong_imp_coprime_nat cong_sym coprime_Suc_0_left coprime_mult_left_iff in blast)
   1.194 +  "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))" (is "?P \<longleftrightarrow> ?Q")
   1.195 +proof
   1.196 +  assume ?P then show ?Q
   1.197 +    by (auto dest!: cong_solve_coprime_nat)
   1.198 +next
   1.199 +  assume ?Q
   1.200 +  then obtain b where "[a * b = Suc 0] (mod m)"
   1.201 +    by blast
   1.202 +  with coprime_mod_left_iff [of m "a * b"] show ?P
   1.203 +    by (cases "m = 0 \<or> m = 1")
   1.204 +      (unfold cong_def, auto simp add: cong_def)
   1.205 +qed
   1.206  
   1.207  lemma coprime_iff_invertible_int:
   1.208 -  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   1.209 -  for m :: int
   1.210 -  by (auto intro: cong_solve_coprime_int)
   1.211 -    (meson cong_imp_coprime_int cong_sym coprime_1_left coprime_mult_left_iff)
   1.212 +  "coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))" (is "?P \<longleftrightarrow> ?Q") for m :: int
   1.213 +proof
   1.214 +  assume ?P then show ?Q
   1.215 +    by (auto dest: cong_solve_coprime_int)
   1.216 +next
   1.217 +  assume ?Q
   1.218 +  then obtain b where "[a * b = 1] (mod m)"
   1.219 +    by blast
   1.220 +  with coprime_mod_left_iff [of m "a * b"] show ?P
   1.221 +    by (cases "m = 0 \<or> m = 1")
   1.222 +      (unfold cong_def, auto simp add: zmult_eq_1_iff)
   1.223 +qed
   1.224  
   1.225  lemma coprime_iff_invertible'_nat:
   1.226    "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
   1.227 @@ -637,12 +640,8 @@
   1.228  lemma cong_modulus_mult_nat: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
   1.229    for x y :: nat
   1.230    apply (cases "y \<le> x")
   1.231 -   apply (simp add: cong_altdef_nat)
   1.232 -   apply (erule dvd_mult_left)
   1.233 -  apply (rule cong_sym)
   1.234 -  apply (subst (asm) cong_sym_eq)
   1.235 -  apply (simp add: cong_altdef_nat)
   1.236 -  apply (erule dvd_mult_left)
   1.237 +   apply (auto simp add: cong_altdef_nat elim: dvd_mult_left)
   1.238 +  apply (metis cong_def mod_mult_cong_right)
   1.239    done
   1.240  
   1.241  lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
   1.242 @@ -702,9 +701,7 @@
   1.243      ultimately have "[?x = z] (mod m1 * m2)"
   1.244        using a by (auto intro: coprime_cong_mult_nat simp add: mod_mult_cong_left mod_mult_cong_right)
   1.245      with \<open>z < m1 * m2\<close> \<open>?x < m1 * m2\<close> show "z = ?x"
   1.246 -      apply (intro cong_less_modulus_unique_nat)
   1.247 -        apply (auto, erule cong_sym)
   1.248 -      done
   1.249 +      by (auto simp add: cong_def)
   1.250    qed
   1.251    with less 1 2 show ?thesis by auto
   1.252   qed
   1.253 @@ -759,13 +756,9 @@
   1.254          using b a apply blast
   1.255          apply (rule cong_sum)
   1.256          apply (rule cong_scalar_left)
   1.257 -        using b apply auto
   1.258 -        apply (rule cong_dvd_modulus_nat)
   1.259 -         apply (drule (1) bspec)
   1.260 -         apply (erule conjE)
   1.261 -         apply assumption
   1.262 -        apply rule
   1.263 -        using fin a apply auto
   1.264 +        using b apply (auto simp add: mod_eq_0_iff_dvd cong_def)
   1.265 +        apply (rule dvd_trans [of _ "prod m (A - {x})" "b x" for x])
   1.266 +        using a fin apply auto
   1.267          done
   1.268        finally show ?thesis
   1.269          by simp
   1.270 @@ -800,35 +793,19 @@
   1.271    then have less: "?x < (\<Prod>i\<in>A. m i)"
   1.272      by auto
   1.273    have cong: "\<forall>i\<in>A. [?x = u i] (mod m i)"
   1.274 -    apply auto
   1.275 -    apply (rule cong_trans)
   1.276 -     prefer 2
   1.277 -    using one apply auto
   1.278 -    apply (rule cong_dvd_modulus_nat [of _ _ "prod m A"])
   1.279 -     apply simp
   1.280 -    using fin apply auto
   1.281 -    done
   1.282 +    using fin one
   1.283 +    by (auto simp add: cong_def dvd_prod_eqI mod_mod_cancel) 
   1.284    have unique: "\<forall>z. z < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
   1.285    proof clarify
   1.286      fix z
   1.287      assume zless: "z < (\<Prod>i\<in>A. m i)"
   1.288      assume zcong: "(\<forall>i\<in>A. [z = u i] (mod m i))"
   1.289      have "\<forall>i\<in>A. [?x = z] (mod m i)"
   1.290 -      apply clarify
   1.291 -      apply (rule cong_trans)
   1.292 -      using cong apply (erule bspec)
   1.293 -      apply (rule cong_sym)
   1.294 -      using zcong apply auto
   1.295 -      done
   1.296 +      using cong zcong by (auto simp add: cong_def)
   1.297      with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
   1.298 -      apply (intro coprime_cong_prod_nat)
   1.299 -        apply auto
   1.300 -      done
   1.301 +      by (intro coprime_cong_prod_nat) auto
   1.302      with zless less show "z = ?x"
   1.303 -      apply (intro cong_less_modulus_unique_nat)
   1.304 -        apply auto
   1.305 -      apply (erule cong_sym)
   1.306 -      done
   1.307 +      by (auto simp add: cong_def)
   1.308    qed
   1.309    from less cong unique show ?thesis
   1.310      by blast