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.72    "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
1.75
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"
```