author haftmann Thu, 23 Nov 2017 17:03:27 +0000 changeset 67087 733017b19de9 parent 67086 59d07a95be0e child 67088 89e82aed7813
generalized more lemmas
 src/HOL/Euclidean_Division.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Euclidean_Division.thy	Thu Nov 23 17:03:26 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy	Thu Nov 23 17:03:27 2017 +0000
@@ -139,7 +139,7 @@
class euclidean_ring = idom_modulo + euclidean_semiring
begin

-lemma dvd_diff_commute:
+lemma dvd_diff_commute [ac_simps]:
"a dvd c - b \<longleftrightarrow> a dvd b - c"
proof -
have "a dvd c - b \<longleftrightarrow> a dvd (c - b) * - 1"```
```--- a/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:26 2017 +0000
+++ b/src/HOL/Number_Theory/Cong.thy	Thu Nov 23 17:03:27 2017 +0000
@@ -154,10 +154,26 @@
using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]

-lemma cong_modulus_minus_iff: "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
+lemma cong_modulus_minus_iff:
+  "[b = c] (mod - a) \<longleftrightarrow> [b = c] (mod a)"
using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of b c " -a"]

+lemma cong_iff_dvd_diff:
+  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
+
+lemma cong_iff_lin:
+  "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)" (is "?P \<longleftrightarrow> ?Q")
+proof -
+  have "?P \<longleftrightarrow> m dvd b - a"
+    by (simp add: cong_iff_dvd_diff dvd_diff_commute)
+  also have "\<dots> \<longleftrightarrow> ?Q"
+    by (auto simp add: algebra_simps elim!: dvdE)
+  finally show ?thesis
+    by simp
+qed
+
end

@@ -215,16 +231,16 @@
lemma cong_altdef_int:
"[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
for a b :: int
-  by (simp add: cong_0_iff [symmetric] cong_diff_iff_cong_0)
+  by (fact cong_iff_dvd_diff)

lemma cong_abs_int [simp]: "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
for x y :: int

lemma cong_square_int:
"prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
for a :: int
-  apply (simp only: cong_altdef_int)
+  apply (simp only: cong_iff_dvd_diff)
apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
done
@@ -290,8 +306,7 @@

lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
for a b :: int
-  by (auto simp add: cong_altdef_int algebra_simps elim!: dvdE)