--- 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
--- 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")
--- 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
--- 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)
--- 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
--- 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 -
--- 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