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.70    by (simp add: even_nat_def)
    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"