# HG changeset patch
# User haftmann
# Date 1507569048 -7200
# Node ID 6ba663ff2b1c8d584d8fb630329cec748436f7f5
# Parent  4eb431c3f9745d61a385e630284b484aa353fcf0
tuned proofs

diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Computational_Algebra/Primes.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -58,6 +58,9 @@
 declare [[coercion int]]
 declare [[coercion_enabled]]
 
+lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
+  using not_prime_1 [where ?'a = nat] by simp
+
 lemma prime_elem_nat_iff:
   "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
 proof safe
@@ -97,9 +100,17 @@
 lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
   by (auto simp: prime_elem_int_nat_transfer prime_def)
 
-lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
+lemma prime_int_nat_transfer: "prime (k::int) \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
   by (auto simp: prime_elem_int_nat_transfer prime_def)
 
+lemma prime_elem_iff_prime_abs:
+  "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
+  by (auto intro: primeI)
+
+lemma prime_nat_iff_prime:
+  "prime (nat k) \<longleftrightarrow> prime k"
+  by (cases "k \<ge> 0") (simp_all add: prime_int_nat_transfer)
+
 lemma prime_int_iff:
   "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
 proof (intro iffI conjI allI impI; (elim conjE)?)
@@ -259,9 +270,6 @@
 
 subsubsection \<open>Make prime naively executable\<close>
 
-lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
-  unfolding One_nat_def [symmetric] by (rule not_prime_1)
-
 lemma prime_nat_iff':
   "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)"
 proof safe
diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Divides.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -1164,16 +1164,40 @@
 apply (rule div_less_dividend, simp_all)
 done
 
-lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
+lemma mod_eq_dvd_iff_nat:
+  "m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat
+proof -
+  have "int m mod int q = int n mod int q \<longleftrightarrow> int q dvd int m - int n"
+    by (simp add: mod_eq_dvd_iff)
+  with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
+    by (simp only: of_nat_mod of_nat_diff)
+  then show ?thesis
+    by (simp add: zdvd_int)
+qed
+
+lemma mod_eq_nat1E:
+  fixes m n q :: nat
+  assumes "m mod q = n mod q" and "m \<ge> n"
+  obtains s where "m = n + q * s"
+proof -
+  from assms have "q dvd m - n"
+    by (simp add: mod_eq_dvd_iff_nat)
+  then obtain s where "m - n = q * s" ..
+  with \<open>m \<ge> n\<close> have "m = n + q * s"
+    by simp
+  with that show thesis .
+qed
+
+lemma mod_eq_nat2E:
+  fixes m n q :: nat
+  assumes "m mod q = n mod q" and "n \<ge> m"
+  obtains s where "n = m + q * s"
+  using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps)
+
+lemma nat_mod_eq_lemma:
+  assumes "(x::nat) mod n = y mod n" and "y \<le> x"
   shows "\<exists>q. x = y + n * q"
-proof-
-  from xy have th: "int x - int y = int (x - y)" by simp
-  from xyn have "int x mod int n = int y mod int n"
-    by (simp add: zmod_int [symmetric])
-  hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
-  hence "n dvd x - y" by (simp add: th zdvd_int)
-  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
-qed
+  using assms by (rule mod_eq_nat1E) rule
 
 lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
   (is "?lhs = ?rhs")
diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -488,6 +488,18 @@
   then show ?P by simp
 qed
 
+lemma mod_eqE:
+  assumes "a mod c = b mod c"
+  obtains d where "b = a + c * d"
+proof -
+  from assms have "c dvd a - b"
+    by (simp add: mod_eq_dvd_iff)
+  then obtain d where "a - b = c * d" ..
+  then have "b = a + c * - d"
+    by (simp add: algebra_simps)
+  with that show thesis .
+qed
+
 end
 
   
diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -64,7 +64,12 @@
 
 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
   for S :: "int set"
-  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
+proof -
+  have "inj_on nat (abs ` A)" for A
+    by (rule inj_onI) auto
+  then show ?thesis
+    by (auto simp add: image_comp [symmetric] dest: finite_image_absD finite_imageD)
+qed
 
 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
   for S :: "int set"
@@ -181,7 +186,7 @@
   by (simp_all add: MOST_Suc_iff)
 
 lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
-  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
+  by (simp add: cofinite_eq_sequentially)
 
 (* legacy names *)
 lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -318,9 +318,8 @@
 
 lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
   for a b :: int
-  apply (auto simp add: cong_altdef_int dvd_def)
-  apply (rule_tac [!] x = "-k" in exI, auto)
-  done
+  by (auto simp add: cong_altdef_int algebra_simps elim!: dvdE)
+    (simp add: distrib_right [symmetric] add_eq_0_iff)
 
 lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
   (is "?lhs = ?rhs")
@@ -512,7 +511,7 @@
 
 lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   for x y :: nat
-  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
+  by (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE)
 
 lemma cong_solve_nat:
   fixes a :: nat
diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -46,7 +46,7 @@
   using pq_neq p_prime primes_coprime_nat q_prime by blast
 
 lemma pq_coprime_int: "coprime (int p) (int q)"
-  using pq_coprime transfer_int_nat_gcd(1) by presburger
+  by (simp add: gcd_int_def pq_coprime)
 
 lemma qp_ineq: "int p * k \<le> (int p * int q - 1) div 2 \<longleftrightarrow> k \<le> (int q - 1) div 2"
 proof -
diff -r 4eb431c3f974 -r 6ba663ff2b1c src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 09 19:10:47 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Mon Oct 09 19:10:48 2017 +0200
@@ -222,12 +222,11 @@
 
 lemma is_field: "field R"
 proof -
-  have "gcd x (int p) \<noteq> 1 \<Longrightarrow> 0 \<le> x \<Longrightarrow> x < int p \<Longrightarrow> x = 0" for x
-    by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
+  have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
+    by (rule prime_imp_coprime) (auto simp add: zdvd_not_zless)
   then show ?thesis
-    apply (intro cring.field_intro2 cring)
-     apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
-    done
+    by (intro cring.field_intro2 cring)
+      (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq ac_simps)
 qed
 
 lemma res_prime_units_eq: "Units R = {1..p - 1}"
@@ -256,7 +255,7 @@
     by (simp_all add: m'_def)
   then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
     unfolding res_units_eq
-    by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
+    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
   then have "Units R = int ` totatives m'"
     by blast
   then have "totatives m' = nat ` Units R"
@@ -293,7 +292,7 @@
   case False
   with assms show ?thesis
     using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
-    by (auto simp add: residues_def transfer_int_nat_gcd(1)) force
+    by (auto simp add: residues_def gcd_int_def) force
 qed
 
 lemma fermat_theorem:
@@ -418,7 +417,7 @@
       using that \<open>p\<ge>2\<close> by force
     then show "?L \<subseteq> ?R" by blast
     have "n \<in> ?L" if "n \<in> ?R" for n
-      using that \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
+      using that \<open>p\<ge>2\<close> by (auto intro: rev_image_eqI [of "int n"])
     then show "?R \<subseteq> ?L" by blast
   qed
   moreover