--- a/NEWS Sun May 06 18:20:25 2018 +0000
+++ b/NEWS Sun May 06 18:20:25 2018 +0000
@@ -278,10 +278,6 @@
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
INCOMPATIBILITY.
-* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid
-clash with fact mod_mult_self4 (on more generic semirings).
-INCOMPATIBILITY.
-
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
interpretation of abstract locales. INCOMPATIBILITY.
@@ -318,6 +314,18 @@
* Code generation: Code generation takes an explicit option
"case_insensitive" to accomodate case-insensitive file systems.
+* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
+clash with fact mod_mult_self4 (on more generic semirings).
+INCOMPATIBILITY.
+
+* Eliminated some theorem aliasses:
+
+ even_times_iff ~> even_mult_iff
+ mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
+ even_of_nat ~> even_int_iff
+
+INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Divides.thy Sun May 06 18:20:25 2018 +0000
+++ b/src/HOL/Divides.thy Sun May 06 18:20:25 2018 +0000
@@ -1295,10 +1295,6 @@
subsubsection \<open>Lemmas of doubtful value\<close>
-lemma mod_mult_self3':
- "Suc (k * n + m) mod n = Suc m mod n"
- by (fact Suc_mod_mult_self3)
-
lemma mod_Suc_eq_Suc_mod:
"Suc m mod n = Suc (m mod n) mod n"
by (simp add: mod_simps)
@@ -1327,16 +1323,6 @@
then show ?thesis ..
qed
-lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close>
-
-lemma mod_2_not_eq_zero_eq_one_nat:
- fixes n :: nat
- shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
- by (fact not_mod_2_eq_0_eq_1)
-
-lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
- by (fact even_of_nat)
-
lemma is_unit_int:
"is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
by auto
--- a/src/HOL/Groebner_Basis.thy Sun May 06 18:20:25 2018 +0000
+++ b/src/HOL/Groebner_Basis.thy Sun May 06 18:20:25 2018 +0000
@@ -78,7 +78,7 @@
context semiring_parity
begin
-declare even_times_iff [algebra]
+declare even_mult_iff [algebra]
declare even_power [algebra]
end
--- a/src/HOL/Presburger.thy Sun May 06 18:20:25 2018 +0000
+++ b/src/HOL/Presburger.thy Sun May 06 18:20:25 2018 +0000
@@ -435,7 +435,7 @@
context semiring_parity
begin
-declare even_times_iff [presburger]
+declare even_mult_iff [presburger]
declare even_power [presburger]
--- a/src/HOL/Transcendental.thy Sun May 06 18:20:25 2018 +0000
+++ b/src/HOL/Transcendental.thy Sun May 06 18:20:25 2018 +0000
@@ -4173,10 +4173,10 @@
lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
proof safe
assume "cos x = 0"
- then show "\<exists>n. odd n \<and> x = of_int n * (pi/2)"
- apply (simp add: cos_zero_iff)
- apply safe
- apply (metis even_int_iff of_int_of_nat_eq)
+ then show "\<exists>n. odd n \<and> x = of_int n * (pi / 2)"
+ unfolding cos_zero_iff
+ apply (auto simp add: cos_zero_iff)
+ apply (metis even_of_nat of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI)
apply simp
done
@@ -4196,7 +4196,7 @@
then show "\<exists>n. even n \<and> x = of_int n * (pi / 2)"
apply (simp add: sin_zero_iff)
apply safe
- apply (metis even_int_iff of_int_of_nat_eq)
+ apply (metis even_of_nat of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI)
apply simp
done