src/HOL/Parity.thy
 changeset 54228 229282d53781 parent 54227 63b441f49645 child 54489 03ff4d1e6784
```     1.1 --- a/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
1.3 @@ -9,29 +9,52 @@
1.4  imports Main
1.5  begin
1.6
1.7 -class even_odd =
1.8 -  fixes even :: "'a \<Rightarrow> bool"
1.9 +class even_odd = semiring_div_parity
1.10  begin
1.11
1.12 +definition even :: "'a \<Rightarrow> bool"
1.13 +where
1.14 +  even_def [presburger]: "even a \<longleftrightarrow> a mod 2 = 0"
1.15 +
1.16 +lemma even_iff_2_dvd [algebra]:
1.17 +  "even a \<longleftrightarrow> 2 dvd a"
1.18 +  by (simp add: even_def dvd_eq_mod_eq_0)
1.19 +
1.20 +lemma even_zero [simp]:
1.21 +  "even 0"
1.22 +  by (simp add: even_def)
1.23 +
1.24 +lemma even_times_anything:
1.25 +  "even a \<Longrightarrow> even (a * b)"
1.26 +  by (simp add: even_iff_2_dvd)
1.27 +
1.28 +lemma anything_times_even:
1.29 +  "even a \<Longrightarrow> even (b * a)"
1.30 +  by (simp add: even_iff_2_dvd)
1.31 +
1.32  abbreviation odd :: "'a \<Rightarrow> bool"
1.33  where
1.34 -  "odd x \<equiv> \<not> even x"
1.35 +  "odd a \<equiv> \<not> even a"
1.36 +
1.37 +lemma odd_times_odd:
1.38 +  "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)"
1.39 +  by (auto simp add: even_def mod_mult_left_eq)
1.40 +
1.41 +lemma even_product [simp, presburger]:
1.42 +  "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.43 +  apply (auto simp add: even_times_anything anything_times_even)
1.44 +  apply (rule ccontr)
1.45 +  apply (auto simp add: odd_times_odd)
1.46 +  done
1.47
1.48  end
1.49
1.50 -instantiation nat and int  :: even_odd
1.51 -begin
1.52 -
1.53 -definition
1.54 -  even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"
1.55 +instance nat and int  :: even_odd ..
1.56
1.57 -definition
1.58 -  even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"
1.59 -
1.60 -instance ..
1.61 -
1.62 -end
1.63 -
1.64 +lemma even_nat_def [presburger]:
1.65 +  "even x \<longleftrightarrow> even (int x)"
1.66 +  by (auto simp add: even_def int_eq_iff int_mult nat_mult_distrib)
1.67 +
1.68  lemma transfer_int_nat_relations:
1.69    "even (int x) \<longleftrightarrow> even x"
1.71 @@ -40,13 +63,13 @@
1.72    transfer_int_nat_relations
1.73  ]
1.74
1.75 -lemma even_zero_int[simp]: "even (0::int)" by presburger
1.76 -
1.77 -lemma odd_one_int[simp]: "odd (1::int)" by presburger
1.78 +lemma odd_one_int [simp]:
1.79 +  "odd (1::int)"
1.80 +  by presburger
1.81
1.82 -lemma even_zero_nat[simp]: "even (0::nat)" by presburger
1.83 -
1.84 -lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
1.85 +lemma odd_1_nat [simp]:
1.86 +  "odd (1::nat)"
1.87 +  by presburger
1.88
1.89  lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
1.90    unfolding even_def by simp
1.91 @@ -67,25 +90,6 @@
1.92
1.93
1.94  subsection {* Behavior under integer arithmetic operations *}
1.95 -declare dvd_def[algebra]
1.96 -lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x"
1.97 -  by presburger
1.98 -lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x"
1.99 -  by presburger
1.100 -
1.101 -lemma even_times_anything: "even (x::int) ==> even (x * y)"
1.102 -  by algebra
1.103 -
1.104 -lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
1.105 -
1.106 -lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
1.107 -  by (simp add: even_def mod_mult_right_eq)
1.108 -
1.109 -lemma even_product[simp,presburger]: "even((x::int) * y) = (even x | even y)"
1.110 -  apply (auto simp add: even_times_anything anything_times_even)
1.111 -  apply (rule ccontr)
1.112 -  apply (auto simp add: odd_times_odd)
1.113 -  done
1.114
1.115  lemma even_plus_even: "even (x::int) ==> even y ==> even (x + y)"
1.116  by presburger
1.117 @@ -181,45 +185,19 @@
1.118
1.119  subsection {* Parity and powers *}
1.120
1.121 -lemma  minus_one_even_odd_power:
1.122 -     "(even x --> (- 1::'a::{comm_ring_1})^x = 1) &
1.123 -      (odd x --> (- 1::'a)^x = - 1)"
1.124 -  apply (induct x)
1.125 -  apply (rule conjI)
1.126 -  apply simp
1.127 -  apply (insert even_zero_nat, blast)
1.128 -  apply simp
1.129 -  done
1.130 -
1.131 -lemma minus_one_even_power [simp]:
1.132 -    "even x ==> (- 1::'a::{comm_ring_1})^x = 1"
1.133 -  using minus_one_even_odd_power by blast
1.134 -
1.135 -lemma minus_one_odd_power [simp]:
1.136 -    "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1"
1.137 -  using minus_one_even_odd_power by blast
1.138 +lemma (in comm_ring_1) neg_power_if:
1.139 +  "(- a) ^ n = (if even n then (a ^ n) else - (a ^ n))"
1.140 +  by (induct n) simp_all
1.141
1.142 -lemma neg_one_even_odd_power:
1.143 -     "(even x --> (-1::'a::{comm_ring_1})^x = 1) &
1.144 -      (odd x --> (-1::'a)^x = -1)"
1.145 -  apply (induct x)
1.146 -  apply (simp, simp)
1.147 -  done
1.148 -
1.149 -lemma neg_one_even_power [simp]:
1.150 -    "even x ==> (-1::'a::{comm_ring_1})^x = 1"
1.151 -  using neg_one_even_odd_power by blast
1.152 +lemma (in comm_ring_1)
1.153 +  shows minus_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
1.154 +  and minus_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
1.155 +  by (simp_all add: neg_power_if del: minus_one)
1.156
1.157 -lemma neg_one_odd_power [simp]:
1.158 -    "odd x ==> (-1::'a::{comm_ring_1})^x = -1"
1.159 -  using neg_one_even_odd_power by blast
1.160 -
1.161 -lemma neg_power_if:
1.162 -     "(-x::'a::{comm_ring_1}) ^ n =
1.163 -      (if even n then (x ^ n) else -(x ^ n))"
1.164 -  apply (induct n)
1.165 -  apply simp_all
1.166 -  done
1.167 +lemma (in comm_ring_1)
1.168 +  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (-1) ^ n = 1"
1.169 +  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (-1) ^ n = - 1"
1.170 +  by (simp_all add: minus_one [symmetric] del: minus_one)
1.171
1.172  lemma zero_le_even_power: "even n ==>
1.173      0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
```