author haftmann Thu Nov 23 17:03:27 2017 +0000 (17 months ago) changeset 67087 733017b19de9 parent 67086 59d07a95be0e child 67088 89e82aed7813
generalized more lemmas
 src/HOL/Euclidean_Division.thy file | annotate | diff | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Euclidean_Division.thy	Thu Nov 23 17:03:26 2017 +0000
1.2 +++ b/src/HOL/Euclidean_Division.thy	Thu Nov 23 17:03:27 2017 +0000
1.3 @@ -139,7 +139,7 @@
1.4  class euclidean_ring = idom_modulo + euclidean_semiring
1.5  begin
1.6
1.7 -lemma dvd_diff_commute:
1.8 +lemma dvd_diff_commute [ac_simps]:
1.9    "a dvd c - b \<longleftrightarrow> a dvd b - c"
1.10  proof -
1.11    have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"
```
```     2.1 --- a/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:26 2017 +0000
2.2 +++ b/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:27 2017 +0000
2.3 @@ -154,10 +154,26 @@
2.4    using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
2.5    by (simp add: cong_0_iff dvd_diff_commute)
2.6
2.7 -lemma cong_modulus_minus_iff: "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
2.8 +lemma cong_modulus_minus_iff:
2.9 +  "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
2.10    using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]
2.12
2.13 +lemma cong_iff_dvd_diff:
2.14 +  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
2.15 +  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
2.16 +
2.17 +lemma cong_iff_lin:
2.18 +  "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" (is "?P \<longleftrightarrow> ?Q")
2.19 +proof -
2.20 +  have "?P \<longleftrightarrow> m dvd b - a"
2.21 +    by (simp add: cong_iff_dvd_diff dvd_diff_commute)
2.22 +  also have "\<dots> \<longleftrightarrow> ?Q"
2.23 +    by (auto simp add: algebra_simps elim!: dvdE)
2.24 +  finally show ?thesis
2.25 +    by simp
2.26 +qed
2.27 +
2.28  end
2.29
2.30
2.31 @@ -215,16 +231,16 @@
2.32  lemma cong_altdef_int:
2.33    "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
2.34    for a b :: int
2.35 -  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
2.36 +  by (fact cong_iff_dvd_diff)
2.37
2.38  lemma cong_abs_int [simp]: "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
2.39    for x y :: int
2.40 -  by (simp add: cong_altdef_int)
2.41 +  by (simp add: cong_iff_dvd_diff)
2.42
2.43  lemma cong_square_int:
2.44    "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
2.45    for a :: int
2.46 -  apply (simp only: cong_altdef_int)
2.47 +  apply (simp only: cong_iff_dvd_diff)
2.48    apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
2.49    apply (auto simp add: field_simps)
2.50    done
2.51 @@ -290,8 +306,7 @@
2.52
2.53  lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
2.54    for a b :: int
2.55 -  by (auto simp add: cong_altdef_int algebra_simps elim!: dvdE)
2.57 +  by (fact cong_iff_lin)
2.58
2.59  lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
2.60    (is "?lhs = ?rhs")
2.61 @@ -340,7 +355,7 @@
2.62
2.63  lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
2.64    for a b :: int
2.65 -  by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
2.66 +  by (fact cong_modulus_minus_iff)
2.67
2.68  lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
2.69    for a x y :: nat
```