# HG changeset patch
# User haftmann
# Date 1512233453 0
# Node ID 2977773a481cb0f005c765cb9e45d08328b5cddc
# Parent  3d8626cbaff8bf86dd223346c3d144a7f79a43d9
generalized more lemmas

diff -r 3d8626cbaff8 -r 2977773a481c src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Dec 01 20:49:42 2017 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -154,7 +154,7 @@
   using cong_diff_iff_cong_0 [of b c a] cong_diff_iff_cong_0 [of "- b" "- c" a]
   by (simp add: cong_0_iff dvd_diff_commute)
 
-lemma cong_modulus_minus_iff:
+lemma cong_modulus_minus_iff [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"]
   by (simp add: cong_0_iff)
@@ -174,8 +174,85 @@
     by simp
 qed
 
+lemma cong_add_lcancel:
+  "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  by (simp add: cong_iff_lin algebra_simps)
+
+lemma cong_add_rcancel:
+  "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  by (simp add: cong_iff_lin algebra_simps)
+
+lemma cong_add_lcancel_0:
+  "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  using cong_add_lcancel [of a x 0 n] by simp
+
+lemma cong_add_rcancel_0:
+  "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  using cong_add_rcancel [of x a 0 n] by simp
+
+lemma cong_dvd_modulus:
+  "[x = y] (mod n)" if "[x = y] (mod m)" and "n dvd m"
+  using that by (auto intro: dvd_trans simp add: cong_iff_dvd_diff)
+
+lemma cong_modulus_mult:
+  "[x = y] (mod m)" if "[x = y] (mod m * n)"
+  using that by (simp add: cong_iff_dvd_diff) (rule dvd_mult_left)
+
 end
 
+lemma cong_abs [simp]:
+  "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
+  for x y :: "'a :: {unique_euclidean_ring, linordered_idom}"
+  by (simp add: cong_iff_dvd_diff)
+
+lemma cong_square:
+  "prime p \<Longrightarrow> 0 < a \<Longrightarrow> [a * a = 1] (mod p) \<Longrightarrow> [a = 1] (mod p) \<or> [a = - 1] (mod p)"
+  for a p :: "'a :: {normalization_semidom, linordered_idom, unique_euclidean_ring}"
+  by (auto simp add: cong_iff_dvd_diff square_diff_one_factored dest: prime_dvd_multD)
+
+lemma cong_mult_rcancel:
+  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+  if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
+  using that by (auto simp add: cong_iff_dvd_diff left_diff_distrib [symmetric] ac_simps coprime_dvd_mult_right_iff)
+
+lemma cong_mult_lcancel:
+  "[k * a = k * b] (mod m) = [a = b] (mod m)"
+  if "coprime k m" for a k m :: "'a::{unique_euclidean_ring, ring_gcd}"
+  using that cong_mult_rcancel [of k m a b] by (simp add: ac_simps)
+
+lemma coprime_cong_mult:
+  "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
+  for a b :: "'a :: {unique_euclidean_ring, semiring_gcd}"
+  by (simp add: cong_iff_dvd_diff divides_mult)
+
+lemma cong_gcd_eq:
+  "gcd a m = gcd b m" if "[a = b] (mod m)"
+  for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
+proof (cases "m = 0")
+  case True
+  with that show ?thesis
+    by simp
+next
+  case False
+  moreover have "gcd (a mod m) m = gcd (b mod m) m"
+    using that by (simp add: cong_def)
+  ultimately show ?thesis
+    by simp
+qed 
+
+lemma cong_imp_coprime:
+  "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+  for a b :: "'a :: {unique_euclidean_semiring, euclidean_semiring_gcd}"
+  by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq)
+
+lemma cong_cong_prod_coprime:
+  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
+    "(\<forall>i\<in>A. [x = y] (mod m i))"
+    "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
+  for x y :: "'a :: {unique_euclidean_ring, semiring_gcd}"
+  using that by (induct A rule: infinite_finite_induct)
+    (auto intro!: coprime_cong_mult prod_coprime_right)
+
 
 subsection \<open>Congruences on @{typ nat} and @{typ int}\<close>
 
@@ -228,29 +305,6 @@
   using cong_diff_iff_cong_0_nat' [of a b m]
   by (simp only: cong_0_iff [symmetric])
 
-lemma cong_altdef_int:
-  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
-  for a b :: int
-  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
-  by (simp add: cong_iff_dvd_diff)
-
-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_iff_dvd_diff)
-  apply (subst prime_dvd_mult_eq_int [symmetric], assumption)
-  apply (auto simp add: field_simps)
-  done
-
-lemma cong_mult_rcancel_int:
-  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
-  if "coprime k m" for a k m :: int
-  using that by (simp add: cong_altdef_int)
-    (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib') 
-
 lemma cong_mult_rcancel_nat:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   if "coprime k m" for a k m :: nat
@@ -268,21 +322,11 @@
   finally show ?thesis .
 qed
 
-lemma cong_mult_lcancel_int:
-  "[k * a = k * b] (mod m) = [a = b] (mod m)"
-  if "coprime k m" for a k m :: int
-  using that by (simp add: cong_mult_rcancel_int ac_simps)
-
 lemma cong_mult_lcancel_nat:
   "[k * a = k * b] (mod m) = [a = b] (mod m)"
   if "coprime k m" for a k m :: nat
   using that by (simp add: cong_mult_rcancel_nat ac_simps)
 
-lemma coprime_cong_mult_int:
-  "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
-  for a b :: int
-  by (simp add: cong_altdef_int divides_mult)
-
 lemma coprime_cong_mult_nat:
   "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
   for a b :: nat
@@ -304,10 +348,6 @@
   for a m :: int
   by (auto simp: cong_def)  (metis mod_mod_trivial pos_mod_conj)
 
-lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
-  for a b :: int
-  by (fact cong_iff_lin)
-
 lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   (is "?lhs = ?rhs")
   for a b :: nat
@@ -329,22 +369,6 @@
     by (metis cong_def mult.commute nat_mod_eq_iff) 
 qed
 
-lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
-  for a b :: nat
-  by (auto simp add: cong_def) (metis gcd_red_nat)
-
-lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
-  for a b :: int
-  by (auto simp add: cong_def) (metis gcd_red_int)
-
-lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
-  for a b :: nat
-  by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_nat)
-
-lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
-  for a b :: int
-  by (auto simp add: coprime_iff_gcd_eq_1 dest: cong_gcd_eq_int)
-
 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: nat
   by simp
@@ -353,42 +377,22 @@
   for a b :: int
   by simp
 
-lemma cong_minus_int [iff]: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
-  for a b :: int
-  by (fact cong_modulus_minus_iff)
-
 lemma cong_add_lcancel_nat: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   for a x y :: nat
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
-  for a x y :: int
-  by (simp add: cong_iff_lin_int)
-
 lemma cong_add_rcancel_nat: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
   for a x y :: nat
   by (simp add: cong_iff_lin_nat)
 
-lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
-  for a x y :: int
-  by (simp add: cong_iff_lin_int)
-
 lemma cong_add_lcancel_0_nat: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   for a x :: nat
   using cong_add_lcancel_nat [of a x 0 n] by simp
 
-lemma cong_add_lcancel_0_int: "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
-  for a x :: int
-  using cong_add_lcancel_int [of a x 0 n] by simp
-
 lemma cong_add_rcancel_0_nat: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
   for a x :: nat
   using cong_add_rcancel_nat [of x a 0 n] by simp
 
-lemma cong_add_rcancel_0_int: "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
-  for a x :: int
-  using cong_add_rcancel_int [of x a 0 n] by simp
-
 lemma cong_dvd_modulus_nat: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
   for x y :: nat
   apply (auto simp add: cong_iff_lin_nat dvd_def)
@@ -397,10 +401,6 @@
   apply (simp add: field_simps)
   done
 
-lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
-  for x y :: int
-  by (auto simp add: cong_altdef_int dvd_def)
-
 lemma cong_to_1_nat:
   fixes a :: nat
   assumes "[a = 1] (mod n)"
@@ -455,7 +455,7 @@
    apply (rule_tac x = "-1" in exI)
    apply auto
   apply (insert bezout_int [of a n], auto)
-  apply (metis cong_iff_lin_int mult.commute)
+  apply (metis cong_iff_lin mult.commute)
   done
 
 lemma cong_solve_dvd_nat:
@@ -553,25 +553,15 @@
 
 lemma cong_cong_lcm_int: "[x = y] (mod a) \<Longrightarrow> [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   for x y :: int
-  by (auto simp add: cong_altdef_int lcm_least)
+  by (auto simp add: cong_iff_dvd_diff lcm_least)
 
 lemma cong_cong_prod_coprime_nat:
   "[x = y] (mod (\<Prod>i\<in>A. m i))" if
-    "(\<forall>i\<in>A. [(x::nat) = y] (mod m i))"
-    and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
-  using that apply (induct A rule: infinite_finite_induct)
-    apply auto
-  apply (metis coprime_cong_mult_nat prod_coprime_right)
-  done
-
-lemma cong_cong_prod_coprime_int:
-  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
-    "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
+    "(\<forall>i\<in>A. [x = y] (mod m i))"
     "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
-  using that apply (induct A rule: infinite_finite_induct)
-    apply auto
-  apply (metis coprime_cong_mult_int prod_coprime_right)
-  done
+  for x y :: nat
+  using that by (induct A rule: infinite_finite_induct)
+    (auto intro!: coprime_cong_mult_nat prod_coprime_right)
 
 lemma binary_chinese_remainder_nat:
   fixes m1 m2 :: nat
@@ -651,12 +641,6 @@
   apply (metis cong_def mod_mult_cong_right)
   done
 
-lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
-  for x y :: int
-  apply (simp add: cong_altdef_int)
-  apply (erule dvd_mult_left)
-  done
-
 lemma cong_less_modulus_unique_nat: "[x = y] (mod m) \<Longrightarrow> x < m \<Longrightarrow> y < m \<Longrightarrow> x = y"
   for x y :: nat
   by (simp add: cong_def)
@@ -811,4 +795,94 @@
     by blast
 qed
 
+
+subsection \<open>Aliasses\<close>
+
+lemma cong_altdef_int:
+  "[a = b] (mod m) \<longleftrightarrow> m dvd (a - b)"
+  for a b :: int
+  by (fact cong_iff_dvd_diff)
+
+lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
+  for a b :: int
+  by (fact cong_iff_lin)
+
+lemma cong_minus_int: "[a = b] (mod - m) \<longleftrightarrow> [a = b] (mod m)"
+  for a b :: int
+  by (fact cong_modulus_minus_iff)
+
+lemma cong_add_lcancel_int: "[a + x = a + y] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  for a x y :: int
+  by (fact cong_add_lcancel)
+
+lemma cong_add_rcancel_int: "[x + a = y + a] (mod n) \<longleftrightarrow> [x = y] (mod n)"
+  for a x y :: int
+  by (fact cong_add_rcancel)
+
+lemma cong_add_lcancel_0_int:
+  "[a + x = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  for a x :: int
+  by (fact cong_add_lcancel_0)
+
+lemma cong_add_rcancel_0_int:
+  "[x + a = a] (mod n) \<longleftrightarrow> [x = 0] (mod n)"
+  for a x :: int
+  by (fact cong_add_rcancel_0) 
+
+lemma cong_dvd_modulus_int: "[x = y] (mod m) \<Longrightarrow> n dvd m \<Longrightarrow> [x = y] (mod n)"
+  for x y :: int
+  by (fact cong_dvd_modulus)
+
+lemma cong_abs_int:
+  "[x = y] (mod \<bar>m\<bar>) \<longleftrightarrow> [x = y] (mod m)"
+  for x y :: int
+  by (fact cong_abs)
+
+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
+  by (fact cong_square)
+
+lemma cong_mult_rcancel_int:
+  "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
+  if "coprime k m" for a k m :: int
+  using that by (fact cong_mult_rcancel)
+
+lemma cong_mult_lcancel_int:
+  "[k * a = k * b] (mod m) = [a = b] (mod m)"
+  if "coprime k m" for a k m :: int
+  using that by (fact cong_mult_lcancel)
+
+lemma coprime_cong_mult_int:
+  "[a = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n \<Longrightarrow> [a = b] (mod m * n)"
+  for a b :: int
+  by (fact coprime_cong_mult)
+
+lemma cong_gcd_eq_nat: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+  for a b :: nat
+  by (fact cong_gcd_eq)
+
+lemma cong_gcd_eq_int: "[a = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
+  for a b :: int
+  by (fact cong_gcd_eq)
+
+lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+  for a b :: nat
+  by (fact cong_imp_coprime)
+
+lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
+  for a b :: int
+  by (fact cong_imp_coprime)
+
+lemma cong_cong_prod_coprime_int:
+  "[x = y] (mod (\<Prod>i\<in>A. m i))" if
+    "(\<forall>i\<in>A. [x = y] (mod m i))"
+    "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
+  for x y :: int
+  using that by (fact cong_cong_prod_coprime)
+
+lemma cong_modulus_mult_int: "[x = y] (mod m * n) \<Longrightarrow> [x = y] (mod m)"
+  for x y :: int
+  by (fact cong_modulus_mult)
+
 end