--- a/NEWS Tue Oct 21 17:23:16 2014 +0200
+++ b/NEWS Tue Oct 21 21:10:44 2014 +0200
@@ -51,10 +51,9 @@
dvd_plus_eq_left ~> dvd_add_left_iff
Minor INCOMPATIBILITY.
-* More foundational definition for predicate "even":
+* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _".
even_def ~> even_iff_mod_2_eq_zero
- even_iff_2_dvd ~> even_def
-Minor INCOMPATIBILITY.
+INCOMPATIBILITY.
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
Minor INCOMPATIBILITY.
--- a/src/HOL/Codegenerator_Test/Candidates.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Tue Oct 21 21:10:44 2014 +0200
@@ -12,11 +12,6 @@
"~~/src/HOL/ex/Records"
begin
-lemma [code]: -- {* Formal joining of hierarchy of implicit definitions in Scala *}
- fixes a :: "'a :: semiring_div_parity"
- shows "even a \<longleftrightarrow> a mod 2 = 0"
- by (fact even_iff_mod_2_eq_zero)
-
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
empty: "sublist [] xs"
--- a/src/HOL/Complex.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Complex.thy Tue Oct 21 21:10:44 2014 +0200
@@ -733,7 +733,7 @@
moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
ultimately have "d = 0"
unfolding sin_zero_iff
- by (auto simp add: numeral_2_eq_2 less_Suc_eq elim!: evenE)
+ by (auto elim!: evenE dest!: less_2_cases)
thus "a = x" unfolding d_def by simp
qed (simp add: assms del: Re_sgn Im_sgn)
with `z \<noteq> 0` show "arg z = x"
--- a/src/HOL/Old_Number_Theory/Primes.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Tue Oct 21 21:10:44 2014 +0200
@@ -68,7 +68,7 @@
proof-
from e have np: "n > 0" by presburger
from e have "2 dvd (n - 1)" by presburger
- then obtain k where "n - 1 = 2*k" using dvd_def by auto
+ then obtain k where "n - 1 = 2 * k" ..
hence k: "n = 2*k + 1" using e by presburger
hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra
thus ?thesis by blast
@@ -588,7 +588,6 @@
thus ?thesis by blast
qed
-lemma even_dvd[simp]: "even (n::nat) \<longleftrightarrow> 2 dvd n" by presburger
lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
@@ -828,6 +827,5 @@
done
declare power_Suc0[simp del]
-declare even_dvd[simp del]
end
--- a/src/HOL/Parity.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Parity.thy Tue Oct 21 21:10:44 2014 +0200
@@ -189,47 +189,41 @@
context semiring_parity
begin
-definition even :: "'a \<Rightarrow> bool"
+abbreviation even :: "'a \<Rightarrow> bool"
where
- [presburger, algebra]: "even a \<longleftrightarrow> 2 dvd a"
+ "even a \<equiv> 2 dvd a"
abbreviation odd :: "'a \<Rightarrow> bool"
where
- "odd a \<equiv> \<not> even a"
+ "odd a \<equiv> \<not> 2 dvd a"
lemma evenE [elim?]:
assumes "even a"
obtains b where "a = 2 * b"
-proof -
- from assms have "2 dvd a" by (simp add: even_def)
- then show thesis using that ..
-qed
+ using assms by (rule dvdE)
lemma oddE [elim?]:
assumes "odd a"
obtains b where "a = 2 * b + 1"
-proof -
- from assms have "\<not> 2 dvd a" by (simp add: even_def)
- then show thesis using that by (rule not_two_dvdE)
-qed
+ using assms by (rule not_two_dvdE)
lemma even_times_iff [simp, presburger, algebra]:
"even (a * b) \<longleftrightarrow> even a \<or> even b"
- by (auto simp add: even_def dest: two_is_prime)
+ by (auto simp add: dest: two_is_prime)
lemma even_zero [simp]:
"even 0"
- by (simp add: even_def)
+ by simp
lemma odd_one [simp]:
"odd 1"
- by (simp add: even_def)
+ by simp
lemma even_numeral [simp]:
"even (numeral (Num.Bit0 n))"
proof -
have "even (2 * numeral n)"
- unfolding even_times_iff by (simp add: even_def)
+ unfolding even_times_iff by simp
then have "even (numeral n + numeral n)"
unfolding mult_2 .
then show ?thesis
@@ -245,7 +239,7 @@
then have "even (2 * numeral n + 1)"
unfolding mult_2 .
then have "2 dvd numeral n * 2 + 1"
- unfolding even_def by (simp add: ac_simps)
+ by (simp add: ac_simps)
with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
have "2 dvd 1"
by simp
@@ -254,7 +248,7 @@
lemma even_add [simp]:
"even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
- by (auto simp add: even_def dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
+ by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
lemma odd_add [simp]:
"odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
@@ -271,7 +265,7 @@
lemma even_minus [simp, presburger, algebra]:
"even (- a) \<longleftrightarrow> even a"
- by (simp add: even_def)
+ by (fact dvd_minus_iff)
lemma even_diff [simp]:
"even (a - b) \<longleftrightarrow> even (a + b)"
@@ -300,7 +294,7 @@
lemma even_iff_mod_2_eq_zero:
"even a \<longleftrightarrow> a mod 2 = 0"
- by (simp add: even_def dvd_eq_mod_eq_0)
+ by (fact dvd_eq_mod_eq_0)
lemma even_succ_div_two [simp]:
"even a \<Longrightarrow> (a + 1) div 2 = a div 2"
@@ -312,7 +306,7 @@
lemma even_two_times_div_two:
"even a \<Longrightarrow> 2 * (a div 2) = a"
- by (rule dvd_mult_div_cancel) (simp add: even_def)
+ by (fact dvd_mult_div_cancel)
lemma odd_two_times_div_two_succ:
"odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
@@ -325,7 +319,7 @@
lemma even_Suc [simp, presburger, algebra]:
"even (Suc n) = odd n"
- by (simp add: even_def two_dvd_Suc_iff)
+ by (fact two_dvd_Suc_iff)
lemma odd_pos:
"odd (n :: nat) \<Longrightarrow> 0 < n"
@@ -334,11 +328,11 @@
lemma even_diff_nat [simp]:
fixes m n :: nat
shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
- by (simp add: even_def two_dvd_diff_nat_iff)
+ by (fact two_dvd_diff_nat_iff)
lemma even_int_iff:
"even (int n) \<longleftrightarrow> even n"
- by (simp add: even_def dvd_int_iff)
+ by (simp add: dvd_int_iff)
lemma even_nat_iff:
"0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
--- a/src/HOL/Transcendental.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Transcendental.thy Tue Oct 21 21:10:44 2014 +0200
@@ -3598,7 +3598,7 @@
qed
lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
- by (simp add: cos_double mult.assoc power_add [symmetric] numeral_2_eq_2)
+ by (cases "even n") (simp_all add: cos_double mult.assoc)
lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
--- a/src/HOL/Word/Misc_Numeric.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy Tue Oct 21 21:10:44 2014 +0200
@@ -25,7 +25,7 @@
lemma emep1:
fixes n d :: int
shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
- by (auto simp add: pos_zmod_mult_2 add.commute even_def dvd_def)
+ by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
lemma int_mod_ge:
"a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"