--- a/src/HOL/Algebra/IntRing.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Algebra/IntRing.thy Sat Dec 02 16:50:53 2017 +0000
@@ -248,10 +248,12 @@
by (metis dvd_def mult.commute)
next
assume "UNIV = {uu. \<exists>x. uu = x * p}"
- then obtain x where "1 = x * p" by best
- then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute)
+ then obtain x where "1 = x * p"
+ by best
+ then have "\<bar>p * x\<bar> = 1"
+ by (simp add: ac_simps)
then show False using prime
- by (auto dest!: abs_zmult_eq_1 simp: prime_def)
+ by (auto simp add: abs_mult zmult_eq_1_iff)
qed
--- a/src/HOL/Computational_Algebra/Primes.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Computational_Algebra/Primes.thy Sat Dec 02 16:50:53 2017 +0000
@@ -115,15 +115,11 @@
"prime p" if "p \<ge> 2" and "\<And>m n. p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n" for p :: int
using that by (auto intro!: primeI prime_elemI)
-lemma prime_elem_nat_iff:
+lemma prime_elem_nat_iff [simp]:
"prime_elem n \<longleftrightarrow> prime n" for n :: nat
by (simp add: prime_def)
-lemma prime_nat_iff_prime_elem:
- "prime n \<longleftrightarrow> prime_elem n" for n :: nat
- by (simp add: prime_elem_nat_iff)
-
-lemma prime_elem_iff_prime_abs:
+lemma prime_elem_iff_prime_abs [simp]:
"prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
by (auto intro: primeI)
@@ -137,14 +133,13 @@
proof (rule prime_natI)
fix r s
assume "n dvd r * s"
- then have "int n dvd int (r * s)"
- by (simp add: zdvd_int)
- then have "int n dvd int r * int s"
+ with of_nat_dvd_iff [of n "r * s"] have "int n dvd int r * int s"
by simp
with \<open>?P\<close> have "int n dvd int r \<or> int n dvd int s"
- by (auto dest: prime_dvd_mult_iff)
+ using prime_dvd_mult_iff [of "int n" "int r" "int s"]
+ by simp
then show "n dvd r \<or> n dvd s"
- by (simp add: zdvd_int)
+ by simp
qed
next
assume ?Q
@@ -155,17 +150,18 @@
fix r s
assume "int n dvd r * s"
then have "n dvd nat \<bar>r * s\<bar>"
- by (simp add: zdvd_int)
+ by simp
then have "n dvd nat \<bar>r\<bar> * nat \<bar>s\<bar>"
by (simp add: nat_abs_mult_distrib)
with \<open>?Q\<close> have "n dvd nat \<bar>r\<bar> \<or> n dvd nat \<bar>s\<bar>"
- by (auto dest: prime_dvd_mult_iff)
+ using prime_dvd_mult_iff [of "n" "nat \<bar>r\<bar>" "nat \<bar>s\<bar>"]
+ by simp
then show "int n dvd r \<or> int n dvd s"
- by (simp add: zdvd_int)
+ by simp
qed
qed
-lemma prime_nat_iff_prime:
+lemma prime_nat_iff_prime [simp]:
"prime (nat k) \<longleftrightarrow> prime k"
proof (cases "k \<ge> 0")
case True
@@ -177,17 +173,9 @@
by (auto dest: prime_ge_2_int)
qed
-lemma prime_elem_int_nat_transfer:
- "prime_elem n \<longleftrightarrow> prime_elem (nat \<bar>n\<bar>)"
- by (simp add: prime_elem_iff_prime_abs prime_elem_nat_iff prime_nat_iff_prime)
-
-lemma prime_elem_nat_int_transfer [simp]:
- "prime_elem (int n) \<longleftrightarrow> prime_elem n"
- by (simp add: prime_elem_nat_iff prime_elem_iff_prime_abs)
-
lemma prime_int_nat_transfer:
"prime k \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
- by (auto simp add: prime_nat_iff_prime dest: prime_ge_2_int)
+ by (auto dest: prime_ge_2_int)
lemma prime_nat_naiveI:
"prime p" if "p \<ge> 2" and dvd: "\<And>n. n dvd p \<Longrightarrow> n = 1 \<or> n = p" for p :: nat
@@ -214,12 +202,12 @@
with \<open>p \<ge> 2\<close> have "n dvd nat \<bar>p\<bar>"
by simp
then have "int n dvd p"
- by (simp add: int_dvd_iff)
+ by simp
with dvd [of "int n"] show "n = 1 \<or> n = nat p"
by auto
qed
then show ?thesis
- by (simp add: prime_nat_iff_prime)
+ by simp
qed
lemma prime_nat_iff:
@@ -242,9 +230,9 @@
"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)?)
assume *: "prime n"
- hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
- from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
- by (auto simp: prime_def zabs_def not_less split: if_splits)
+ hence irred: "irreducible n" by (auto intro: prime_elem_imp_irreducible)
+ from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
+ by (auto simp add: prime_ge_0_int)
thus "n > 1" by presburger
fix m assume "m dvd n" \<open>m \<ge> 0\<close>
with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
@@ -256,7 +244,10 @@
moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
proof (intro allI impI)
fix m assume "m dvd nat n"
- with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
+ with \<open>n > 1\<close> have "m dvd nat \<bar>n\<bar>"
+ by simp
+ then have "int m dvd n"
+ by simp
with n(2) have "int m = 1 \<or> int m = n"
using of_nat_0_le_iff by blast
thus "m = 1 \<or> m = nat n" by auto
@@ -280,7 +271,7 @@
shows "\<not>n dvd p"
proof
assume "n dvd p"
- from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
+ from assms(1) have "irreducible p" by (auto intro: prime_elem_imp_irreducible)
from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
by (auto dest!: zdvd_imp_le)
qed
@@ -297,10 +288,10 @@
unfolding prime_int_iff by blast
lemma not_prime_eq_prod_nat:
- assumes "m > 1" "\<not>prime (m::nat)"
+ assumes "m > 1" "\<not> prime (m::nat)"
shows "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
using assms irreducible_altdef[of m]
- by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
+ by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
subsection \<open>Largest exponent of a prime factor\<close>
@@ -380,15 +371,20 @@
qed (auto simp: prime_nat_iff)
lemma prime_int_iff':
- "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?lhs = ?rhs")
-proof
- assume "?lhs"
- thus "?rhs"
- by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_iff')
+ "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?P \<longleftrightarrow> ?Q")
+proof (cases "p \<ge> 0")
+ case True
+ have "?P \<longleftrightarrow> prime (nat p)"
+ by simp
+ also have "\<dots> \<longleftrightarrow> p > 1 \<and> (\<forall>n\<in>{2..<nat p}. \<not> n dvd nat \<bar>p\<bar>)"
+ using True by (simp add: prime_nat_iff')
+ also have "{2..<nat p} = nat ` {2..<p}"
+ using True int_eq_iff by fastforce
+ finally show "?P \<longleftrightarrow> ?Q" by simp
next
- assume "?rhs"
- thus "?lhs"
- by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_iff')
+ case False
+ then show ?thesis
+ by (auto simp add: prime_ge_0_int)
qed
lemma prime_int_numeral_eq [simp]:
@@ -415,6 +411,24 @@
using prime_divisor_exists[of n]
by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
+lemma prime_factor_int:
+ fixes k :: int
+ assumes "\<bar>k\<bar> \<noteq> 1"
+ obtains p where "prime p" "p dvd k"
+proof (cases "k = 0")
+ case True
+ then have "prime (2::int)" and "2 dvd k"
+ by simp_all
+ with that show thesis
+ by blast
+next
+ case False
+ with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k"
+ by auto
+ with that show thesis
+ by blast
+qed
+
subsection \<open>Infinitely many primes\<close>
@@ -616,7 +630,7 @@
lemma prime_factorization_exists_nat:
"n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
- using prime_factorization_exists[of n] by (auto simp: prime_def)
+ using prime_factorization_exists[of n] by auto
lemma prod_mset_prime_factorization_nat [simp]:
"(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
--- a/src/HOL/Data_Structures/RBT_Set.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sat Dec 02 16:50:53 2017 +0000
@@ -303,7 +303,7 @@
by (simp add: powr_realpow bheight_size_bound rbt_def)
finally have "2 powr (height t / 2) \<le> size1 t" .
hence "height t / 2 \<le> log 2 (size1 t)"
- by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
+ by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
thus ?thesis by simp
qed
--- a/src/HOL/Decision_Procs/Ferrack.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Dec 02 16:50:53 2017 +0000
@@ -570,14 +570,15 @@
by simp
qed simp_all
-lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow>
- \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
- apply (cases "\<bar>i\<bar> = 0", simp_all add: gcd_int_def)
- apply (cases "\<bar>j\<bar> = 0", simp_all)
- apply (cases "\<bar>i\<bar> = 1", simp_all)
- apply (cases "\<bar>j\<bar> = 1", simp_all)
- apply auto
- done
+lemma zgcd_gt1:
+ "\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
+ if "gcd i j > 1" for i j :: int
+proof -
+ have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
+ by auto
+ with that show ?thesis
+ by (auto simp add: not_less)
+qed
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0"
by (induct t rule: numgcdh.induct) auto
--- a/src/HOL/Decision_Procs/MIR.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/MIR.thy Sat Dec 02 16:50:53 2017 +0000
@@ -665,14 +665,15 @@
from ismaxcoeff_mono[OF H1 thh1] show ?case by simp
qed simp_all
-lemma zgcd_gt1: "gcd i j > (1::int) \<Longrightarrow> ((\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1) \<or> (\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0))"
- apply (unfold gcd_int_def)
- apply (cases "i = 0", simp_all)
- apply (cases "j = 0", simp_all)
- apply (cases "\<bar>i\<bar> = 1", simp_all)
- apply (cases "\<bar>j\<bar> = 1", simp_all)
- apply auto
- done
+lemma zgcd_gt1:
+ "\<bar>i\<bar> > 1 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> = 0 \<and> \<bar>j\<bar> > 1 \<or> \<bar>i\<bar> > 1 \<and> \<bar>j\<bar> = 0"
+ if "gcd i j > 1" for i j :: int
+proof -
+ have "\<bar>k\<bar> \<le> 1 \<longleftrightarrow> k = - 1 \<or> k = 0 \<or> k = 1" for k :: int
+ by auto
+ with that show ?thesis
+ by (auto simp add: not_less)
+qed
lemma numgcdh0:"numgcdh t m = 0 \<Longrightarrow> m =0"
by (induct t rule: numgcdh.induct) auto
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Dec 02 16:50:53 2017 +0000
@@ -61,7 +61,7 @@
(* Simp rules for changing (n::int) to int n *)
val simpset1 =
put_simpset HOL_basic_ss ctxt
- addsimps @{thms zdvd_int} @ [@{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
+ addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
map (fn r => r RS sym) @{thms of_nat_numeral [where ?'a = int] int_int_eq zle_int of_nat_less_iff [where ?'a = int]}
|> Splitter.add_split @{thm zdiff_int_split}
(*simp rules for elimination of int n*)
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Dec 02 16:50:53 2017 +0000
@@ -84,7 +84,7 @@
@{thm "split_min"}, @{thm "split_max"}]
(* Simp rules for changing (n::int) to int n *)
val simpset1 = put_simpset HOL_basic_ss ctxt
- addsimps [@{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] @
+ addsimps @{thms int_dvd_int_iff [symmetric] of_nat_add of_nat_mult} @
map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff"}, @{thm nat_numeral}]
|> Splitter.add_split @{thm "zdiff_int_split"}
(*simp rules for elimination of int n*)
--- a/src/HOL/Divides.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Divides.thy Sat Dec 02 16:50:53 2017 +0000
@@ -384,7 +384,7 @@
by (cases l rule: int_cases3)
(auto simp del: of_nat_mult of_nat_add
simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
- eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
+ eucl_rel_int_iff divide_int_def modulo_int_def)
next
case (neg n)
then show ?thesis
@@ -392,7 +392,7 @@
by (cases l rule: int_cases3)
(auto simp del: of_nat_mult of_nat_add
simp add: mod_greater_zero_iff_not_dvd of_nat_mult [symmetric] of_nat_add [symmetric] algebra_simps
- eucl_rel_int_iff divide_int_def modulo_int_def int_dvd_iff)
+ eucl_rel_int_iff divide_int_def modulo_int_def)
qed
lemma divmod_int_unique:
@@ -1155,7 +1155,7 @@
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)
+ by simp
qed
lemma mod_eq_nat1E:
--- a/src/HOL/Euclidean_Division.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy Sat Dec 02 16:50:53 2017 +0000
@@ -1432,7 +1432,7 @@
then int (m div n)
else - int (m div n + of_bool (\<not> n dvd m)))"
by (auto simp add: divide_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
- nat_mult_distrib dvd_int_iff)
+ nat_mult_distrib)
instance proof
fix k :: int show "k div 0 = 0"
@@ -1460,7 +1460,7 @@
fix q
assume "q dvd m" "q dvd n"
then have "int q dvd int m" "int q dvd int n"
- by (simp_all add: zdvd_int)
+ by simp_all
with \<open>?P\<close> have "is_unit (int q)"
by (rule coprime_common_divisor)
then show "is_unit q"
@@ -1473,7 +1473,7 @@
fix k
assume "k dvd int m" "k dvd int n"
then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
- by (simp_all add: zdvd_int)
+ by simp_all
with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
by (rule coprime_common_divisor)
then show "is_unit k"
@@ -1525,7 +1525,7 @@
then sgn l * int (m mod n)
else sgn l * (int (n * of_bool (\<not> n dvd m)) - int (m mod n)))"
by (auto simp add: modulo_int_def sgn_0_0 sgn_1_pos sgn_mult abs_mult
- nat_mult_distrib dvd_int_iff)
+ nat_mult_distrib)
instance proof
fix k l :: int
@@ -1574,7 +1574,7 @@
by (blast intro: int_sgnE elim: that)
with that show ?thesis
by (simp add: modulo_int_unfold sgn_0_0 sgn_1_pos sgn_1_neg
- sgn_mult mod_eq_0_iff_dvd int_dvd_iff)
+ sgn_mult mod_eq_0_iff_dvd)
qed
instance proof
--- a/src/HOL/GCD.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/GCD.thy Sat Dec 02 16:50:53 2017 +0000
@@ -1756,6 +1756,59 @@
end
+lemma gcd_int_int_eq [simp]:
+ "gcd (int m) (int n) = int (gcd m n)"
+ by (simp add: gcd_int_def)
+
+lemma gcd_nat_abs_left_eq [simp]:
+ "gcd (nat \<bar>k\<bar>) n = nat (gcd k (int n))"
+ by (simp add: gcd_int_def)
+
+lemma gcd_nat_abs_right_eq [simp]:
+ "gcd n (nat \<bar>k\<bar>) = nat (gcd (int n) k)"
+ by (simp add: gcd_int_def)
+
+lemma abs_gcd_int [simp]:
+ "\<bar>gcd x y\<bar> = gcd x y"
+ for x y :: int
+ by (simp only: gcd_int_def)
+
+lemma gcd_abs1_int [simp]:
+ "gcd \<bar>x\<bar> y = gcd x y"
+ for x y :: int
+ by (simp only: gcd_int_def) simp
+
+lemma gcd_abs2_int [simp]:
+ "gcd x \<bar>y\<bar> = gcd x y"
+ for x y :: int
+ by (simp only: gcd_int_def) simp
+
+lemma lcm_int_int_eq [simp]:
+ "lcm (int m) (int n) = int (lcm m n)"
+ by (simp add: lcm_int_def)
+
+lemma lcm_nat_abs_left_eq [simp]:
+ "lcm (nat \<bar>k\<bar>) n = nat (lcm k (int n))"
+ by (simp add: lcm_int_def)
+
+lemma lcm_nat_abs_right_eq [simp]:
+ "lcm n (nat \<bar>k\<bar>) = nat (lcm (int n) k)"
+ by (simp add: lcm_int_def)
+
+lemma lcm_abs1_int [simp]:
+ "lcm \<bar>x\<bar> y = lcm x y"
+ for x y :: int
+ by (simp only: lcm_int_def) simp
+
+lemma lcm_abs2_int [simp]:
+ "lcm x \<bar>y\<bar> = lcm x y"
+ for x y :: int
+ by (simp only: lcm_int_def) simp
+
+lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
+ for i j :: int
+ by (simp only: lcm_int_def)
+
lemma gcd_nat_induct:
fixes m n :: nat
assumes "\<And>m. P m 0"
@@ -1767,35 +1820,13 @@
apply simp_all
done
-lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
- by (simp add: gcd_int_def)
-
-lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
- by (simp add: lcm_int_def)
-
lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
for x y :: int
- by (simp add: gcd_int_def)
+ by (simp only: gcd_int_def) simp
lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
for x y :: int
- by (simp add: gcd_int_def)
-
-lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
- for x y :: int
- by (simp add: gcd_int_def)
-
-lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
- for x y :: int
- by (simp add: gcd_int_def)
-
-lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
- for x y :: int
- by (metis abs_idempotent gcd_abs_int)
-
-lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
- for x y :: int
- by (metis abs_idempotent gcd_abs_int)
+ by (simp only: gcd_int_def) simp
lemma gcd_cases_int:
fixes x y :: int
@@ -1812,27 +1843,11 @@
lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
for x y :: int
- by (simp add: lcm_int_def)
+ by (simp only: lcm_int_def) simp
lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
for x y :: int
- by (simp add: lcm_int_def)
-
-lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
- for x y :: int
- by (simp add: lcm_int_def)
-
-lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
- for i j :: int
- by (simp add:lcm_int_def)
-
-lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
- for x y :: int
- by (metis abs_idempotent lcm_int_def)
-
-lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
- for x y :: int
- by (metis abs_idempotent lcm_int_def)
+ by (simp only: lcm_int_def) simp
lemma lcm_cases_int:
fixes x y :: int
@@ -1845,7 +1860,7 @@
lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
for x y :: int
- by (simp add: lcm_int_def)
+ by (simp only: lcm_int_def)
lemma gcd_0_nat: "gcd x 0 = x"
for x :: nat
@@ -1861,7 +1876,7 @@
lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
for x :: int
- by (auto simp:gcd_int_def)
+ by (auto simp: gcd_int_def)
lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
for x y :: nat
@@ -1923,9 +1938,20 @@
qed (simp_all add: lcm_nat_def)
instance int :: ring_gcd
- by standard
- (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
- zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
+proof
+ fix k l r :: int
+ show "gcd k l dvd k" "gcd k l dvd l"
+ using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+ gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+ by simp_all
+ show "lcm k l = normalize (k * l) div gcd k l"
+ using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+ by (simp add: nat_eq_iff of_nat_div abs_mult)
+ assume "r dvd k" "r dvd l"
+ then show "r dvd gcd k l"
+ using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+ by simp
+qed simp
lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
for a b :: nat
@@ -1975,7 +2001,7 @@
lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
for x y :: int
- by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
+ by (metis abs_dvd_iff gcd_0_left_int gcd_unique_int)
lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
for x y :: int
@@ -1995,7 +2021,7 @@
lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
for k m n :: int
- by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
+ using gcd_mult_distrib' [of k m n] by simp
text \<open>\medskip Addition laws.\<close>
@@ -2097,7 +2123,7 @@
lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
for k l :: int
- by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
+ using gcd_red_int [of "\<bar>k\<bar>" "\<bar>l\<bar>"] by simp
lemma coprime_Suc_left_nat [simp]:
"coprime (Suc n) n"
@@ -2421,8 +2447,8 @@
lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
for a b :: int
- by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
-
+ by (simp add: abs_mult lcm_gcd)
+
lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
for m n :: nat
unfolding lcm_nat_def
@@ -2439,11 +2465,11 @@
lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
for m n :: nat
- by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
+ using lcm_eq_0_iff [of m n] by auto
lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
for m n :: int
- by (simp add: lcm_int_def lcm_pos_nat)
+ by (simp add: less_le lcm_eq_0_iff)
lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0" (* FIXME move *)
for m n :: nat
@@ -2653,33 +2679,83 @@
subsubsection \<open>Setwise GCD and LCM for integers\<close>
-instantiation int :: semiring_Gcd
+instantiation int :: Gcd
begin
-definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
-
-definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
-
-instance
- by standard
- (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
- Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
+definition Gcd_int :: "int set \<Rightarrow> int"
+ where "Gcd K = int (GCD k\<in>K. (nat \<circ> abs) k)"
+
+definition Lcm_int :: "int set \<Rightarrow> int"
+ where "Lcm K = int (LCM k\<in>K. (nat \<circ> abs) k)"
+
+instance ..
end
-lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
+lemma Gcd_int_eq [simp]:
+ "(GCD n\<in>N. int n) = int (Gcd N)"
+ by (simp add: Gcd_int_def image_image)
+
+lemma Gcd_nat_abs_eq [simp]:
+ "(GCD k\<in>K. nat \<bar>k\<bar>) = nat (Gcd K)"
+ by (simp add: Gcd_int_def)
+
+lemma abs_Gcd_eq [simp]:
+ "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set"
+ by (simp only: Gcd_int_def)
+
+lemma Gcd_int_greater_eq_0 [simp]:
+ "Gcd K \<ge> 0"
for K :: "int set"
- using normalize_Gcd [of K] by simp
-
-lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
+ using abs_ge_zero [of "Gcd K"] by simp
+
+lemma Gcd_abs_eq [simp]:
+ "(GCD k\<in>K. \<bar>k\<bar>) = Gcd K"
for K :: "int set"
- using normalize_Lcm [of K] by simp
-
-lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
- by (simp add: Gcd_int_def comp_def image_image)
-
-lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
- by (simp add: Lcm_int_def comp_def image_image)
+ by (simp only: Gcd_int_def image_image) simp
+
+lemma Lcm_int_eq [simp]:
+ "(LCM n\<in>N. int n) = int (Lcm N)"
+ by (simp add: Lcm_int_def image_image)
+
+lemma Lcm_nat_abs_eq [simp]:
+ "(LCM k\<in>K. nat \<bar>k\<bar>) = nat (Lcm K)"
+ by (simp add: Lcm_int_def)
+
+lemma abs_Lcm_eq [simp]:
+ "\<bar>Lcm K\<bar> = Lcm K" for K :: "int set"
+ by (simp only: Lcm_int_def)
+
+lemma Lcm_int_greater_eq_0 [simp]:
+ "Lcm K \<ge> 0"
+ for K :: "int set"
+ using abs_ge_zero [of "Lcm K"] by simp
+
+lemma Lcm_abs_eq [simp]:
+ "(LCM k\<in>K. \<bar>k\<bar>) = Lcm K"
+ for K :: "int set"
+ by (simp only: Lcm_int_def image_image) simp
+
+instance int :: semiring_Gcd
+proof
+ fix K :: "int set" and k :: int
+ show "Gcd K dvd k" and "k dvd Lcm K" if "k \<in> K"
+ using that Gcd_dvd [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
+ dvd_Lcm [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
+ by (simp_all add: comp_def)
+ show "k dvd Gcd K" if "\<And>l. l \<in> K \<Longrightarrow> k dvd l"
+ proof -
+ have "nat \<bar>k\<bar> dvd (GCD k\<in>K. nat \<bar>k\<bar>)"
+ by (rule Gcd_greatest) (use that in auto)
+ then show ?thesis by simp
+ qed
+ show "Lcm K dvd k" if "\<And>l. l \<in> K \<Longrightarrow> l dvd k"
+ proof -
+ have "(LCM k\<in>K. nat \<bar>k\<bar>) dvd nat \<bar>k\<bar>"
+ by (rule Lcm_least) (use that in auto)
+ then show ?thesis by simp
+ qed
+qed simp_all
subsection \<open>GCD and LCM on @{typ integer}\<close>
--- a/src/HOL/Int.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Int.thy Sat Dec 02 16:50:53 2017 +0000
@@ -1499,43 +1499,64 @@
then show ?thesis by simp
qed
-theorem zdvd_int: "x dvd y \<longleftrightarrow> int x dvd int y"
+lemma int_dvd_int_iff [simp]:
+ "int m dvd int n \<longleftrightarrow> m dvd n"
proof -
- have "x dvd y" if "int y = int x * k" for k
+ have "m dvd n" if "int n = int m * k" for k
proof (cases k)
- case (nonneg n)
- with that have "y = x * n"
+ case (nonneg q)
+ with that have "n = m * q"
by (simp del: of_nat_mult add: of_nat_mult [symmetric])
then show ?thesis ..
next
- case (neg n)
- with that have "int y = int x * (- int (Suc n))"
+ case (neg q)
+ with that have "int n = int m * (- int (Suc q))"
by simp
- also have "\<dots> = - (int x * int (Suc n))"
+ also have "\<dots> = - (int m * int (Suc q))"
by (simp only: mult_minus_right)
- also have "\<dots> = - int (x * Suc n)"
+ also have "\<dots> = - int (m * Suc q)"
by (simp only: of_nat_mult [symmetric])
- finally have "- int (x * Suc n) = int y" ..
+ finally have "- int (m * Suc q) = int n" ..
then show ?thesis
by (simp only: negative_eq_positive) auto
qed
- then show ?thesis
- by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
+ then show ?thesis by (auto simp add: dvd_def)
qed
-lemma zdvd1_eq[simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
- (is "?lhs \<longleftrightarrow> ?rhs")
+lemma dvd_nat_abs_iff [simp]:
+ "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd k"
+proof -
+ have "n dvd nat \<bar>k\<bar> \<longleftrightarrow> int n dvd int (nat \<bar>k\<bar>)"
+ by (simp only: int_dvd_int_iff)
+ then show ?thesis
+ by simp
+qed
+
+lemma nat_abs_dvd_iff [simp]:
+ "nat \<bar>k\<bar> dvd n \<longleftrightarrow> k dvd int n"
+proof -
+ have "nat \<bar>k\<bar> dvd n \<longleftrightarrow> int (nat \<bar>k\<bar>) dvd int n"
+ by (simp only: int_dvd_int_iff)
+ then show ?thesis
+ by simp
+qed
+
+lemma zdvd1_eq [simp]: "x dvd 1 \<longleftrightarrow> \<bar>x\<bar> = 1" (is "?lhs \<longleftrightarrow> ?rhs")
for x :: int
proof
assume ?lhs
- then have "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
- then have "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
- then have "nat \<bar>x\<bar> = 1" by simp
- then show ?rhs by (cases "x < 0") auto
+ then have "nat \<bar>x\<bar> dvd nat \<bar>1\<bar>"
+ by (simp only: nat_abs_dvd_iff) simp
+ then have "nat \<bar>x\<bar> = 1"
+ by simp
+ then show ?rhs
+ by (cases "x < 0") simp_all
next
assume ?rhs
- then have "x = 1 \<or> x = - 1" by auto
- then show ?lhs by (auto intro: dvdI)
+ then have "x = 1 \<or> x = - 1"
+ by auto
+ then show ?lhs
+ by (auto intro: dvdI)
qed
lemma zdvd_mult_cancel1:
@@ -1554,17 +1575,8 @@
by (simp only: zdvd1_eq)
qed
-lemma int_dvd_iff: "int m dvd z \<longleftrightarrow> m dvd nat \<bar>z\<bar>"
- by (cases "z \<ge> 0") (simp_all add: zdvd_int)
-
-lemma dvd_int_iff: "z dvd int m \<longleftrightarrow> nat \<bar>z\<bar> dvd m"
- by (cases "z \<ge> 0") (simp_all add: zdvd_int)
-
-lemma dvd_int_unfold_dvd_nat: "k dvd l \<longleftrightarrow> nat \<bar>k\<bar> dvd nat \<bar>l\<bar>"
- by (simp add: dvd_int_iff [symmetric])
-
lemma nat_dvd_iff: "nat z dvd m \<longleftrightarrow> (if 0 \<le> z then z dvd int m else m = 0)"
- by (auto simp add: dvd_int_iff)
+ using nat_abs_dvd_iff [of z m] by (cases "z \<ge> 0") auto
lemma eq_nat_nat_iff: "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat z = nat z' \<longleftrightarrow> z = z'"
by (auto elim: nonneg_int_cases)
@@ -1603,7 +1615,7 @@
lemma zdvd_imp_le: "z dvd n \<Longrightarrow> 0 < n \<Longrightarrow> z \<le> n"
for n z :: int
apply (cases n)
- apply (auto simp add: dvd_int_iff)
+ apply auto
apply (cases z)
apply (auto simp add: dvd_imp_le)
done
--- a/src/HOL/Library/Float.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Library/Float.thy Sat Dec 02 16:50:53 2017 +0000
@@ -1193,6 +1193,7 @@
l_def[symmetric, THEN meta_eq_to_obj_eq]
apply transfer
apply (auto simp add: round_up_def truncate_up_rat_precision)
+ apply (metis dvd_triv_left of_nat_dvd_iff)
apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
done
next
@@ -1208,6 +1209,7 @@
l_def[symmetric, THEN meta_eq_to_obj_eq]
apply transfer
apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision)
+ apply (metis dvd_triv_left of_nat_dvd_iff)
apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
done
qed
--- a/src/HOL/Number_Theory/Euler_Criterion.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy Sat Dec 02 16:50:53 2017 +0000
@@ -17,8 +17,9 @@
using p_ge_2 p_prime prime_odd_nat by blast
private lemma p_minus_1_int:
- "int (p - 1) = int p - 1" using p_prime prime_ge_1_nat by force
-
+ "int (p - 1) = int p - 1"
+ by (metis of_nat_1 of_nat_diff p_prime prime_ge_1_nat)
+
private lemma p_not_eq_Suc_0 [simp]:
"p \<noteq> Suc 0"
using p_ge_2 by simp
@@ -46,8 +47,9 @@
proof -
have "[nat \<bar>b\<bar> ^ (p - 1) = 1] (mod p)"
using p_prime proof (rule fermat_theorem)
- show "\<not> p dvd nat \<bar>b\<bar>"
- by (metis b cong_altdef_int cong_dvd_iff diff_zero int_dvd_iff p_a_relprime p_prime prime_dvd_power_int_iff prime_nat_int_transfer rel_simps(51))
+ from b p_a_relprime show "\<not> p dvd nat \<bar>b\<bar>"
+ by (auto simp add: cong_altdef_int power2_eq_square)
+ (metis cong_altdef_int cong_dvd_iff dvd_mult2)
qed
then have "nat \<bar>b\<bar> ^ (p - 1) mod p = 1 mod p"
by (simp add: cong_def)
--- a/src/HOL/Number_Theory/Gauss.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy Sat Dec 02 16:50:53 2017 +0000
@@ -117,7 +117,7 @@
by (simp add: cong_altdef_int)
with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
have "coprime a (int p)"
- by (simp_all add: zdvd_int ac_simps)
+ by (simp_all add: ac_simps)
with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -152,7 +152,7 @@
by (simp add: cong_altdef_int)
with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
have "coprime a (int p)"
- by (simp_all add: zdvd_int ac_simps)
+ by (simp_all add: ac_simps)
with a' cong_mult_rcancel_int [of a "int p" x y]
have "[x = y] (mod p)" by simp
with cong_less_imp_eq_int [of x y p] p_minus_one_l
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sat Dec 02 16:50:53 2017 +0000
@@ -25,8 +25,8 @@
using p_ge_2 p_prime prime_odd_nat by blast
lemma p_ge_0: "0 < int p"
- using p_prime not_prime_0[where 'a = nat] by fastforce+
-
+ by (simp add: p_prime prime_gt_0_nat)
+
lemma p_eq2: "int p = (2 * ((int p - 1) div 2)) + 1"
using odd_p by simp
@@ -34,7 +34,7 @@
using q_ge_2 q_prime prime_odd_nat by blast
lemma q_ge_0: "0 < int q"
- using q_prime not_prime_0[where 'a = nat] by fastforce+
+ by (simp add: q_prime prime_gt_0_nat)
lemma q_eq2: "int q = (2 * ((int q - 1) div 2)) + 1"
using odd_q by simp
@@ -93,7 +93,7 @@
lemma Gpq: "GAUSS p q"
using p_prime pq_neq p_ge_2 q_prime
- by (auto simp: GAUSS_def cong_altdef_int zdvd_int [symmetric] dest: primes_dvd_imp_eq)
+ by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq)
lemma Gqp: "GAUSS q p"
by (simp add: QRqp QR.Gpq)
--- a/src/HOL/Number_Theory/Totient.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Totient.thy Sat Dec 02 16:50:53 2017 +0000
@@ -78,7 +78,7 @@
qed (auto simp: totatives_def)
lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}"
- using totatives_prime_power_Suc[of p 0] by fastforce
+ using totatives_prime_power_Suc [of p 0] by auto
lemma bij_betw_totatives:
assumes "m1 > 1" "m2 > 1" "coprime m1 m2"
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Tools/Qelim/cooper.ML Sat Dec 02 16:50:53 2017 +0000
@@ -811,7 +811,7 @@
val ss1 =
simpset_of (put_simpset comp_ss @{context}
addsimps @{thms simp_thms} @
- [@{thm "nat_numeral"} RS sym, @{thm "zdvd_int"}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}]
+ [@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}]
@ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}]
|> Splitter.add_split @{thm "zdiff_int_split"})
--- a/src/HOL/Word/Word.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Word/Word.thy Sat Dec 02 16:50:53 2017 +0000
@@ -3997,22 +3997,50 @@
done
qed
-lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
- apply (unfold word_rot_defs)
- apply (cut_tac y="size w" in gt_or_eq_0)
- apply (erule disjE)
- apply simp_all
- apply (safe intro!: abl_cong)
- apply (rule rotater_eqs)
- apply (simp add: word_size nat_mod_distrib)
- apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
- apply (rule rotater_eqs)
- apply (simp add: word_size nat_mod_distrib)
- apply (rule of_nat_eq_0_iff [THEN iffD1])
- apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
- using mod_mod_trivial mod_eq_dvd_iff
- apply blast
- done
+lemma word_roti_conv_mod':
+ "word_roti n w = word_roti (n mod int (size w)) w"
+proof (cases "size w = 0")
+ case True
+ then show ?thesis
+ by simp
+next
+ case False
+ then have [simp]: "l mod int (size w) \<ge> 0" for l
+ by simp
+ then have *: "word_roti (n mod int (size w)) w = word_rotr (nat (n mod int (size w))) w"
+ by (simp add: word_roti_def)
+ show ?thesis
+ proof (cases "n \<ge> 0")
+ case True
+ then show ?thesis
+ apply (auto simp add: not_le *)
+ apply (auto simp add: word_rot_defs)
+ apply (safe intro!: abl_cong)
+ apply (rule rotater_eqs)
+ apply (simp add: word_size nat_mod_distrib)
+ done
+ next
+ case False
+ moreover define k where "k = - n"
+ ultimately have n: "n = - k"
+ by simp_all
+ from False show ?thesis
+ apply (auto simp add: not_le *)
+ apply (auto simp add: word_rot_defs)
+ apply (simp add: n)
+ apply (safe intro!: abl_cong)
+ apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
+ apply (rule rotater_eqs)
+ apply (simp add: word_size [symmetric, of w])
+ apply (rule of_nat_eq_0_iff [THEN iffD1])
+ apply (auto simp add: nat_add_distrib [symmetric] mod_eq_0_iff_dvd)
+ using dvd_nat_abs_iff [of "size w" "- k mod int (size w) + k"]
+ apply (simp add: algebra_simps)
+ apply (simp add: word_size)
+ apply (metis (no_types, hide_lams) add.right_inverse dvd_0_right dvd_mod_imp_dvd dvd_refl minus_dvd_iff minus_equation_iff mod_0 mod_add_eq mod_minus_eq)
+ done
+ qed
+qed
lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
--- a/src/HOL/ex/Transfer_Int_Nat.thy Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Sat Dec 02 16:50:53 2017 +0000
@@ -86,7 +86,7 @@
unfolding rel_fun_def ZN_def by simp
lemma ZN_dvd [transfer_rule]: "(ZN ===> ZN ===> op =) (op dvd) (op dvd)"
- unfolding rel_fun_def ZN_def by (simp add: zdvd_int)
+ unfolding rel_fun_def ZN_def by simp
lemma ZN_div [transfer_rule]: "(ZN ===> ZN ===> ZN) (op div) (op div)"
unfolding rel_fun_def ZN_def by (simp add: zdiv_int)