generalized more lemmas
authorhaftmann
Thu Nov 23 17:03:27 2017 +0000 (17 months ago)
changeset 67087733017b19de9
parent 67086 59d07a95be0e
child 67088 89e82aed7813
generalized more lemmas
src/HOL/Euclidean_Division.thy
src/HOL/Number_Theory/Cong.thy
     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.11    by (simp add: cong_0_iff)
    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.56 -    (simp add: distrib_right [symmetric] add_eq_0_iff)
    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