# HG changeset patch # User haftmann # Date 1413918644 -7200 # Node ID cb9d84d3e7f270c8541484cc248abfa08a9a0e8a # Parent cf78e16caa3af33cdffd1c13e6bbced59f7e315e turn even into an abbreviation diff -r cf78e16caa3a -r cb9d84d3e7f2 NEWS --- 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. diff -r cf78e16caa3a -r cb9d84d3e7f2 src/HOL/Codegenerator_Test/Candidates.thy --- 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 \ a mod 2 = 0" - by (fact even_iff_mod_2_eq_zero) - inductive sublist :: "'a list \ 'a list \ bool" where empty: "sublist [] xs" diff -r cf78e16caa3a -r cb9d84d3e7f2 src/HOL/Complex.thy --- 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 \ 0` show "arg z = x" diff -r cf78e16caa3a -r cb9d84d3e7f2 src/HOL/Old_Number_Theory/Primes.thy --- 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) \ 2 dvd n" by presburger lemma prime_odd: "prime p \ p = 2 \ odd p" unfolding prime_def by auto @@ -828,6 +827,5 @@ done declare power_Suc0[simp del] -declare even_dvd[simp del] end diff -r cf78e16caa3a -r cb9d84d3e7f2 src/HOL/Parity.thy --- 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 \ bool" +abbreviation even :: "'a \ bool" where - [presburger, algebra]: "even a \ 2 dvd a" + "even a \ 2 dvd a" abbreviation odd :: "'a \ bool" where - "odd a \ \ even a" + "odd a \ \ 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 "\ 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) \ even a \ 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) \ (even a \ 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) \ (\ (odd a \ odd b))" @@ -271,7 +265,7 @@ lemma even_minus [simp, presburger, algebra]: "even (- a) \ even a" - by (simp add: even_def) + by (fact dvd_minus_iff) lemma even_diff [simp]: "even (a - b) \ even (a + b)" @@ -300,7 +294,7 @@ lemma even_iff_mod_2_eq_zero: "even a \ 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 \ (a + 1) div 2 = a div 2" @@ -312,7 +306,7 @@ lemma even_two_times_div_two: "even a \ 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 \ 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) \ 0 < n" @@ -334,11 +328,11 @@ lemma even_diff_nat [simp]: fixes m n :: nat shows "even (m - n) \ m < n \ 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) \ even n" - by (simp add: even_def dvd_int_iff) + by (simp add: dvd_int_iff) lemma even_nat_iff: "0 \ k \ even (nat k) \ even k" diff -r cf78e16caa3a -r cb9d84d3e7f2 src/HOL/Transcendental.thy --- 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) diff -r cf78e16caa3a -r cb9d84d3e7f2 src/HOL/Word/Misc_Numeric.thy --- 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 \ even d \ 0 \ d \ (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 \ 0 < (n :: int) \ a \ a mod n"