turn even into an abbreviation
authorhaftmann
Tue Oct 21 21:10:44 2014 +0200 (2014-10-21)
changeset 58740cb9d84d3e7f2
parent 58739 cf78e16caa3a
child 58759 e55fe82f3803
turn even into an abbreviation
NEWS
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Complex.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Parity.thy
src/HOL/Transcendental.thy
src/HOL/Word/Misc_Numeric.thy
     1.1 --- a/NEWS	Tue Oct 21 17:23:16 2014 +0200
     1.2 +++ b/NEWS	Tue Oct 21 21:10:44 2014 +0200
     1.3 @@ -51,10 +51,9 @@
     1.4    dvd_plus_eq_left ~> dvd_add_left_iff
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 -* More foundational definition for predicate "even":
     1.8 +* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _".
     1.9    even_def ~> even_iff_mod_2_eq_zero
    1.10 -  even_iff_2_dvd ~> even_def
    1.11 -Minor INCOMPATIBILITY.
    1.12 +INCOMPATIBILITY.
    1.13  
    1.14  * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
    1.15  Minor INCOMPATIBILITY.
     2.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 21 17:23:16 2014 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 21 21:10:44 2014 +0200
     2.3 @@ -12,11 +12,6 @@
     2.4    "~~/src/HOL/ex/Records"
     2.5  begin
     2.6  
     2.7 -lemma [code]: -- {* Formal joining of hierarchy of implicit definitions in Scala *}
     2.8 -  fixes a :: "'a :: semiring_div_parity"
     2.9 -  shows "even a \<longleftrightarrow> a mod 2 = 0"
    2.10 -  by (fact even_iff_mod_2_eq_zero)
    2.11 -
    2.12  inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.13  where
    2.14    empty: "sublist [] xs"
     3.1 --- a/src/HOL/Complex.thy	Tue Oct 21 17:23:16 2014 +0200
     3.2 +++ b/src/HOL/Complex.thy	Tue Oct 21 21:10:44 2014 +0200
     3.3 @@ -733,7 +733,7 @@
     3.4      moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
     3.5      ultimately have "d = 0"
     3.6        unfolding sin_zero_iff
     3.7 -      by (auto simp add: numeral_2_eq_2 less_Suc_eq elim!: evenE)
     3.8 +      by (auto elim!: evenE dest!: less_2_cases)
     3.9      thus "a = x" unfolding d_def by simp
    3.10    qed (simp add: assms del: Re_sgn Im_sgn)
    3.11    with `z \<noteq> 0` show "arg z = x"
     4.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Tue Oct 21 17:23:16 2014 +0200
     4.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Tue Oct 21 21:10:44 2014 +0200
     4.3 @@ -68,7 +68,7 @@
     4.4  proof-
     4.5    from e have np: "n > 0" by presburger
     4.6    from e have "2 dvd (n - 1)" by presburger
     4.7 -  then obtain k where "n - 1 = 2*k" using dvd_def by auto
     4.8 +  then obtain k where "n - 1 = 2 * k" ..
     4.9    hence k: "n = 2*k + 1"  using e by presburger 
    4.10    hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra   
    4.11    thus ?thesis by blast
    4.12 @@ -588,7 +588,6 @@
    4.13  thus ?thesis by blast
    4.14  qed
    4.15  
    4.16 -lemma even_dvd[simp]: "even (n::nat) \<longleftrightarrow> 2 dvd n" by presburger
    4.17  lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
    4.18  
    4.19  
    4.20 @@ -828,6 +827,5 @@
    4.21  done
    4.22  
    4.23  declare power_Suc0[simp del]
    4.24 -declare even_dvd[simp del]
    4.25  
    4.26  end
     5.1 --- a/src/HOL/Parity.thy	Tue Oct 21 17:23:16 2014 +0200
     5.2 +++ b/src/HOL/Parity.thy	Tue Oct 21 21:10:44 2014 +0200
     5.3 @@ -189,47 +189,41 @@
     5.4  context semiring_parity
     5.5  begin
     5.6  
     5.7 -definition even :: "'a \<Rightarrow> bool"
     5.8 +abbreviation even :: "'a \<Rightarrow> bool"
     5.9  where
    5.10 -  [presburger, algebra]: "even a \<longleftrightarrow> 2 dvd a"
    5.11 +  "even a \<equiv> 2 dvd a"
    5.12  
    5.13  abbreviation odd :: "'a \<Rightarrow> bool"
    5.14  where
    5.15 -  "odd a \<equiv> \<not> even a"
    5.16 +  "odd a \<equiv> \<not> 2 dvd a"
    5.17  
    5.18  lemma evenE [elim?]:
    5.19    assumes "even a"
    5.20    obtains b where "a = 2 * b"
    5.21 -proof -
    5.22 -  from assms have "2 dvd a" by (simp add: even_def)
    5.23 -  then show thesis using that ..
    5.24 -qed
    5.25 +  using assms by (rule dvdE)
    5.26  
    5.27  lemma oddE [elim?]:
    5.28    assumes "odd a"
    5.29    obtains b where "a = 2 * b + 1"
    5.30 -proof -
    5.31 -  from assms have "\<not> 2 dvd a" by (simp add: even_def)
    5.32 -  then show thesis using that by (rule not_two_dvdE)
    5.33 -qed
    5.34 +  using assms by (rule not_two_dvdE)
    5.35    
    5.36  lemma even_times_iff [simp, presburger, algebra]:
    5.37    "even (a * b) \<longleftrightarrow> even a \<or> even b"
    5.38 -  by (auto simp add: even_def dest: two_is_prime)
    5.39 +  by (auto simp add: dest: two_is_prime)
    5.40  
    5.41  lemma even_zero [simp]:
    5.42    "even 0"
    5.43 -  by (simp add: even_def)
    5.44 +  by simp
    5.45  
    5.46  lemma odd_one [simp]:
    5.47    "odd 1"
    5.48 -  by (simp add: even_def)
    5.49 +  by simp
    5.50  
    5.51  lemma even_numeral [simp]:
    5.52    "even (numeral (Num.Bit0 n))"
    5.53  proof -
    5.54    have "even (2 * numeral n)"
    5.55 -    unfolding even_times_iff by (simp add: even_def)
    5.56 +    unfolding even_times_iff by simp
    5.57    then have "even (numeral n + numeral n)"
    5.58      unfolding mult_2 .
    5.59    then show ?thesis
    5.60 @@ -245,7 +239,7 @@
    5.61    then have "even (2 * numeral n + 1)"
    5.62      unfolding mult_2 .
    5.63    then have "2 dvd numeral n * 2 + 1"
    5.64 -    unfolding even_def by (simp add: ac_simps)
    5.65 +    by (simp add: ac_simps)
    5.66    with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
    5.67      have "2 dvd 1"
    5.68      by simp
    5.69 @@ -254,7 +248,7 @@
    5.70  
    5.71  lemma even_add [simp]:
    5.72    "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
    5.73 -  by (auto simp add: even_def dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
    5.74 +  by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
    5.75  
    5.76  lemma odd_add [simp]:
    5.77    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
    5.78 @@ -271,7 +265,7 @@
    5.79  
    5.80  lemma even_minus [simp, presburger, algebra]:
    5.81    "even (- a) \<longleftrightarrow> even a"
    5.82 -  by (simp add: even_def)
    5.83 +  by (fact dvd_minus_iff)
    5.84  
    5.85  lemma even_diff [simp]:
    5.86    "even (a - b) \<longleftrightarrow> even (a + b)"
    5.87 @@ -300,7 +294,7 @@
    5.88  
    5.89  lemma even_iff_mod_2_eq_zero:
    5.90    "even a \<longleftrightarrow> a mod 2 = 0"
    5.91 -  by (simp add: even_def dvd_eq_mod_eq_0)
    5.92 +  by (fact dvd_eq_mod_eq_0)
    5.93  
    5.94  lemma even_succ_div_two [simp]:
    5.95    "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    5.96 @@ -312,7 +306,7 @@
    5.97  
    5.98  lemma even_two_times_div_two:
    5.99    "even a \<Longrightarrow> 2 * (a div 2) = a"
   5.100 -  by (rule dvd_mult_div_cancel) (simp add: even_def)
   5.101 +  by (fact dvd_mult_div_cancel)
   5.102  
   5.103  lemma odd_two_times_div_two_succ:
   5.104    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   5.105 @@ -325,7 +319,7 @@
   5.106  
   5.107  lemma even_Suc [simp, presburger, algebra]:
   5.108    "even (Suc n) = odd n"
   5.109 -  by (simp add: even_def two_dvd_Suc_iff)
   5.110 +  by (fact two_dvd_Suc_iff)
   5.111  
   5.112  lemma odd_pos: 
   5.113    "odd (n :: nat) \<Longrightarrow> 0 < n"
   5.114 @@ -334,11 +328,11 @@
   5.115  lemma even_diff_nat [simp]:
   5.116    fixes m n :: nat
   5.117    shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
   5.118 -  by (simp add: even_def two_dvd_diff_nat_iff)
   5.119 +  by (fact two_dvd_diff_nat_iff)
   5.120  
   5.121  lemma even_int_iff:
   5.122    "even (int n) \<longleftrightarrow> even n"
   5.123 -  by (simp add: even_def dvd_int_iff)
   5.124 +  by (simp add: dvd_int_iff)
   5.125  
   5.126  lemma even_nat_iff:
   5.127    "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
     6.1 --- a/src/HOL/Transcendental.thy	Tue Oct 21 17:23:16 2014 +0200
     6.2 +++ b/src/HOL/Transcendental.thy	Tue Oct 21 21:10:44 2014 +0200
     6.3 @@ -3598,7 +3598,7 @@
     6.4  qed
     6.5  
     6.6  lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
     6.7 -  by (simp add: cos_double mult.assoc power_add [symmetric] numeral_2_eq_2)
     6.8 +  by (cases "even n") (simp_all add: cos_double mult.assoc)
     6.9  
    6.10  lemma cos_3over2_pi [simp]: "cos (3 / 2 * pi) = 0"
    6.11    apply (subgoal_tac "cos (pi + pi/2) = 0", simp)
     7.1 --- a/src/HOL/Word/Misc_Numeric.thy	Tue Oct 21 17:23:16 2014 +0200
     7.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Tue Oct 21 21:10:44 2014 +0200
     7.3 @@ -25,7 +25,7 @@
     7.4  lemma emep1:
     7.5    fixes n d :: int
     7.6    shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
     7.7 -  by (auto simp add: pos_zmod_mult_2 add.commute even_def dvd_def)
     7.8 +  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
     7.9  
    7.10  lemma int_mod_ge:
    7.11    "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"