src/HOL/Parity.thy
changeset 58740 cb9d84d3e7f2
parent 58718 48395c763059
child 58769 70fff47875cd
     1.1 --- a/src/HOL/Parity.thy	Tue Oct 21 17:23:16 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Tue Oct 21 21:10:44 2014 +0200
     1.3 @@ -189,47 +189,41 @@
     1.4  context semiring_parity
     1.5  begin
     1.6  
     1.7 -definition even :: "'a \<Rightarrow> bool"
     1.8 +abbreviation even :: "'a \<Rightarrow> bool"
     1.9  where
    1.10 -  [presburger, algebra]: "even a \<longleftrightarrow> 2 dvd a"
    1.11 +  "even a \<equiv> 2 dvd a"
    1.12  
    1.13  abbreviation odd :: "'a \<Rightarrow> bool"
    1.14  where
    1.15 -  "odd a \<equiv> \<not> even a"
    1.16 +  "odd a \<equiv> \<not> 2 dvd a"
    1.17  
    1.18  lemma evenE [elim?]:
    1.19    assumes "even a"
    1.20    obtains b where "a = 2 * b"
    1.21 -proof -
    1.22 -  from assms have "2 dvd a" by (simp add: even_def)
    1.23 -  then show thesis using that ..
    1.24 -qed
    1.25 +  using assms by (rule dvdE)
    1.26  
    1.27  lemma oddE [elim?]:
    1.28    assumes "odd a"
    1.29    obtains b where "a = 2 * b + 1"
    1.30 -proof -
    1.31 -  from assms have "\<not> 2 dvd a" by (simp add: even_def)
    1.32 -  then show thesis using that by (rule not_two_dvdE)
    1.33 -qed
    1.34 +  using assms by (rule not_two_dvdE)
    1.35    
    1.36  lemma even_times_iff [simp, presburger, algebra]:
    1.37    "even (a * b) \<longleftrightarrow> even a \<or> even b"
    1.38 -  by (auto simp add: even_def dest: two_is_prime)
    1.39 +  by (auto simp add: dest: two_is_prime)
    1.40  
    1.41  lemma even_zero [simp]:
    1.42    "even 0"
    1.43 -  by (simp add: even_def)
    1.44 +  by simp
    1.45  
    1.46  lemma odd_one [simp]:
    1.47    "odd 1"
    1.48 -  by (simp add: even_def)
    1.49 +  by simp
    1.50  
    1.51  lemma even_numeral [simp]:
    1.52    "even (numeral (Num.Bit0 n))"
    1.53  proof -
    1.54    have "even (2 * numeral n)"
    1.55 -    unfolding even_times_iff by (simp add: even_def)
    1.56 +    unfolding even_times_iff by simp
    1.57    then have "even (numeral n + numeral n)"
    1.58      unfolding mult_2 .
    1.59    then show ?thesis
    1.60 @@ -245,7 +239,7 @@
    1.61    then have "even (2 * numeral n + 1)"
    1.62      unfolding mult_2 .
    1.63    then have "2 dvd numeral n * 2 + 1"
    1.64 -    unfolding even_def by (simp add: ac_simps)
    1.65 +    by (simp add: ac_simps)
    1.66    with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
    1.67      have "2 dvd 1"
    1.68      by simp
    1.69 @@ -254,7 +248,7 @@
    1.70  
    1.71  lemma even_add [simp]:
    1.72    "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
    1.73 -  by (auto simp add: even_def dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
    1.74 +  by (auto simp add: dvd_add_right_iff dvd_add_left_iff not_dvd_not_dvd_dvd_add)
    1.75  
    1.76  lemma odd_add [simp]:
    1.77    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
    1.78 @@ -271,7 +265,7 @@
    1.79  
    1.80  lemma even_minus [simp, presburger, algebra]:
    1.81    "even (- a) \<longleftrightarrow> even a"
    1.82 -  by (simp add: even_def)
    1.83 +  by (fact dvd_minus_iff)
    1.84  
    1.85  lemma even_diff [simp]:
    1.86    "even (a - b) \<longleftrightarrow> even (a + b)"
    1.87 @@ -300,7 +294,7 @@
    1.88  
    1.89  lemma even_iff_mod_2_eq_zero:
    1.90    "even a \<longleftrightarrow> a mod 2 = 0"
    1.91 -  by (simp add: even_def dvd_eq_mod_eq_0)
    1.92 +  by (fact dvd_eq_mod_eq_0)
    1.93  
    1.94  lemma even_succ_div_two [simp]:
    1.95    "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    1.96 @@ -312,7 +306,7 @@
    1.97  
    1.98  lemma even_two_times_div_two:
    1.99    "even a \<Longrightarrow> 2 * (a div 2) = a"
   1.100 -  by (rule dvd_mult_div_cancel) (simp add: even_def)
   1.101 +  by (fact dvd_mult_div_cancel)
   1.102  
   1.103  lemma odd_two_times_div_two_succ:
   1.104    "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
   1.105 @@ -325,7 +319,7 @@
   1.106  
   1.107  lemma even_Suc [simp, presburger, algebra]:
   1.108    "even (Suc n) = odd n"
   1.109 -  by (simp add: even_def two_dvd_Suc_iff)
   1.110 +  by (fact two_dvd_Suc_iff)
   1.111  
   1.112  lemma odd_pos: 
   1.113    "odd (n :: nat) \<Longrightarrow> 0 < n"
   1.114 @@ -334,11 +328,11 @@
   1.115  lemma even_diff_nat [simp]:
   1.116    fixes m n :: nat
   1.117    shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
   1.118 -  by (simp add: even_def two_dvd_diff_nat_iff)
   1.119 +  by (fact two_dvd_diff_nat_iff)
   1.120  
   1.121  lemma even_int_iff:
   1.122    "even (int n) \<longleftrightarrow> even n"
   1.123 -  by (simp add: even_def dvd_int_iff)
   1.124 +  by (simp add: dvd_int_iff)
   1.125  
   1.126  lemma even_nat_iff:
   1.127    "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"