src/HOL/Parity.thy
changeset 58678 398e05aa84d4
parent 58645 94bef115c08f
child 58679 33c90658448a
     1.1 --- a/src/HOL/Parity.thy	Tue Oct 14 16:19:42 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -9,50 +9,211 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -class even_odd = semiring_div_parity
     1.8 +subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
     1.9 +
    1.10 +lemma two_dvd_Suc_Suc_iff [simp]:
    1.11 +  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
    1.12 +  using dvd_add_triv_right_iff [of 2 n] by simp
    1.13 +
    1.14 +lemma two_dvd_Suc_iff:
    1.15 +  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
    1.16 +  by (induct n) auto
    1.17 +
    1.18 +lemma two_dvd_diff_iff:
    1.19 +  fixes k l :: int
    1.20 +  shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
    1.21 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
    1.22 +
    1.23 +lemma two_dvd_abs_add_iff:
    1.24 +  fixes k l :: int
    1.25 +  shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
    1.26 +  by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
    1.27 +
    1.28 +lemma two_dvd_add_abs_iff:
    1.29 +  fixes k l :: int
    1.30 +  shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
    1.31 +  using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps)
    1.32 +
    1.33 +
    1.34 +subsection {* Ring structures with parity *}
    1.35 +
    1.36 +class semiring_parity = semiring_dvd + semiring_numeral +
    1.37 +  assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
    1.38 +  assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    1.39 +  assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
    1.40 +begin
    1.41 +
    1.42 +lemma two_dvd_plus_one_iff [simp]:
    1.43 +  "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
    1.44 +  by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add)
    1.45 +
    1.46 +end
    1.47 +
    1.48 +instance nat :: semiring_parity
    1.49 +proof
    1.50 +  show "\<not> (2 :: nat) dvd 1"
    1.51 +    by (rule notI, erule dvdE) simp
    1.52 +next
    1.53 +  fix m n :: nat
    1.54 +  assume "\<not> 2 dvd m"
    1.55 +  moreover assume "\<not> 2 dvd n"
    1.56 +  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
    1.57 +    by (simp add: two_dvd_Suc_iff)
    1.58 +  then have "2 dvd Suc m + Suc n"
    1.59 +    by (blast intro: dvd_add)
    1.60 +  also have "Suc m + Suc n = m + n + 2"
    1.61 +    by simp
    1.62 +  finally show "2 dvd m + n"
    1.63 +    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
    1.64 +next
    1.65 +  fix m n :: nat
    1.66 +  assume *: "2 dvd m * n"
    1.67 +  show "2 dvd m \<or> 2 dvd n"
    1.68 +  proof (rule disjCI)
    1.69 +    assume "\<not> 2 dvd n"
    1.70 +    then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff)
    1.71 +    then obtain r where "Suc n = 2 * r" ..
    1.72 +    moreover from * obtain s where "m * n = 2 * s" ..
    1.73 +    then have "2 * s + m = m * Suc n" by simp
    1.74 +    ultimately have " 2 * s + m = 2 * (m * r)" by simp
    1.75 +    then have "m = 2 * (m * r - s)" by simp
    1.76 +    then show "2 dvd m" ..
    1.77 +  qed
    1.78 +qed
    1.79 +
    1.80 +class ring_parity = comm_ring_1 + semiring_parity
    1.81 +
    1.82 +instance int :: ring_parity
    1.83 +proof
    1.84 +  show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
    1.85 +  fix k l :: int
    1.86 +  assume "\<not> 2 dvd k"
    1.87 +  moreover assume "\<not> 2 dvd l"
    1.88 +  ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" 
    1.89 +    by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add)
    1.90 +  then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>"
    1.91 +    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
    1.92 +  then show "2 dvd k + l"
    1.93 +    by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff)
    1.94 +qed (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
    1.95 +
    1.96 +context semiring_div_parity
    1.97 +begin
    1.98 +
    1.99 +subclass semiring_parity
   1.100 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
   1.101 +  fix a b c
   1.102 +  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
   1.103 +    by simp
   1.104 +next
   1.105 +  fix a b c
   1.106 +  assume "(b + c) mod a = 0"
   1.107 +  with mod_add_eq [of b c a]
   1.108 +  have "(b mod a + c mod a) mod a = 0"
   1.109 +    by simp
   1.110 +  moreover assume "b mod a = 0"
   1.111 +  ultimately show "c mod a = 0"
   1.112 +    by simp
   1.113 +next
   1.114 +  show "1 mod 2 = 1"
   1.115 +    by (fact one_mod_two_eq_one)
   1.116 +next
   1.117 +  fix a b
   1.118 +  assume "a mod 2 = 1"
   1.119 +  moreover assume "b mod 2 = 1"
   1.120 +  ultimately show "(a + b) mod 2 = 0"
   1.121 +    using mod_add_eq [of a b 2] by simp
   1.122 +next
   1.123 +  fix a b
   1.124 +  assume "(a * b) mod 2 = 0"
   1.125 +  then have "(a mod 2) * (b mod 2) = 0"
   1.126 +    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
   1.127 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
   1.128 +    by (rule divisors_zero)
   1.129 +qed
   1.130 +
   1.131 +end
   1.132 +
   1.133 +
   1.134 +subsection {* Dedicated @{text even}/@{text odd} predicate *}
   1.135 +
   1.136 +context semiring_parity
   1.137  begin
   1.138  
   1.139  definition even :: "'a \<Rightarrow> bool"
   1.140  where
   1.141    [algebra]: "even a \<longleftrightarrow> 2 dvd a"
   1.142  
   1.143 -lemmas even_iff_2_dvd = even_def
   1.144 +abbreviation odd :: "'a \<Rightarrow> bool"
   1.145 +where
   1.146 +  "odd a \<equiv> \<not> even a"
   1.147 +
   1.148 +lemma even_times_iff [simp, presburger, algebra]:
   1.149 +  "even (a * b) \<longleftrightarrow> even a \<or> even b"
   1.150 +  by (auto simp add: even_def dest: two_is_prime)
   1.151 +
   1.152 +lemma even_zero [simp]:
   1.153 +  "even 0"
   1.154 +  by (simp add: even_def)
   1.155 +
   1.156 +lemma odd_one [simp]:
   1.157 +  "odd 1"
   1.158 +  by (simp add: even_def)
   1.159 +
   1.160 +lemma even_numeral [simp]:
   1.161 +  "even (numeral (Num.Bit0 n))"
   1.162 +proof -
   1.163 +  have "even (2 * numeral n)"
   1.164 +    unfolding even_times_iff by (simp add: even_def)
   1.165 +  then have "even (numeral n + numeral n)"
   1.166 +    unfolding mult_2 .
   1.167 +  then show ?thesis
   1.168 +    unfolding numeral.simps .
   1.169 +qed
   1.170 +
   1.171 +lemma odd_numeral [simp]:
   1.172 +  "odd (numeral (Num.Bit1 n))"
   1.173 +proof
   1.174 +  assume "even (numeral (num.Bit1 n))"
   1.175 +  then have "even (numeral n + numeral n + 1)"
   1.176 +    unfolding numeral.simps .
   1.177 +  then have "even (2 * numeral n + 1)"
   1.178 +    unfolding mult_2 .
   1.179 +  then have "2 dvd numeral n * 2 + 1"
   1.180 +    unfolding even_def by (simp add: ac_simps)
   1.181 +  with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
   1.182 +    have "2 dvd 1"
   1.183 +    by simp
   1.184 +  then show False by simp
   1.185 +qed
   1.186 +
   1.187 +end
   1.188 +
   1.189 +context semiring_div_parity
   1.190 +begin
   1.191  
   1.192  lemma even_iff_mod_2_eq_zero [presburger]:
   1.193    "even a \<longleftrightarrow> a mod 2 = 0"
   1.194    by (simp add: even_def dvd_eq_mod_eq_0)
   1.195  
   1.196 -lemma even_zero [simp]:
   1.197 -  "even 0"
   1.198 -  by (simp add: even_iff_mod_2_eq_zero)
   1.199 -
   1.200  lemma even_times_anything:
   1.201    "even a \<Longrightarrow> even (a * b)"
   1.202 -  by (simp add: even_iff_2_dvd)
   1.203 +  by (simp add: even_def)
   1.204  
   1.205  lemma anything_times_even:
   1.206    "even a \<Longrightarrow> even (b * a)"
   1.207 -  by (simp add: even_iff_2_dvd)
   1.208 -
   1.209 -abbreviation odd :: "'a \<Rightarrow> bool"
   1.210 -where
   1.211 -  "odd a \<equiv> \<not> even a"
   1.212 +  by (simp add: even_def)
   1.213  
   1.214  lemma odd_times_odd:
   1.215    "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)" 
   1.216    by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)
   1.217  
   1.218 -lemma even_product [simp, presburger]:
   1.219 +lemma even_product:
   1.220    "even (a * b) \<longleftrightarrow> even a \<or> even b"
   1.221 -  apply (auto simp add: even_times_anything anything_times_even)
   1.222 -  apply (rule ccontr)
   1.223 -  apply (auto simp add: odd_times_odd)
   1.224 -  done
   1.225 +  by (fact even_times_iff)
   1.226  
   1.227  end
   1.228  
   1.229 -instance nat and int  :: even_odd ..
   1.230 -
   1.231  lemma even_nat_def [presburger]:
   1.232    "even x \<longleftrightarrow> even (int x)"
   1.233    by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)
   1.234 @@ -65,31 +226,8 @@
   1.235    transfer_int_nat_relations
   1.236  ]
   1.237  
   1.238 -lemma odd_one_int [simp]:
   1.239 -  "odd (1::int)"
   1.240 -  by presburger
   1.241 -
   1.242 -lemma odd_1_nat [simp]:
   1.243 -  "odd (1::nat)"
   1.244 -  by presburger
   1.245 -
   1.246 -lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
   1.247 -  unfolding even_iff_mod_2_eq_zero by simp
   1.248 -
   1.249 -lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
   1.250 -  unfolding even_iff_mod_2_eq_zero by simp
   1.251 -
   1.252 -(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
   1.253  declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v
   1.254  
   1.255 -lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
   1.256 -  unfolding even_nat_def by simp
   1.257 -
   1.258 -lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
   1.259 -  unfolding even_nat_def by simp
   1.260 -
   1.261 -subsection {* Even and odd are mutually exclusive *}
   1.262 -
   1.263  
   1.264  subsection {* Behavior under integer arithmetic operations *}
   1.265  
   1.266 @@ -128,7 +266,7 @@
   1.267  lemma two_times_odd_div_two_plus_one:
   1.268    "odd (x::int) ==> 2 * (x div 2) + 1 = x"
   1.269  by presburger
   1.270 -
   1.271 +  
   1.272  lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" by presburger
   1.273  
   1.274  lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" by presburger
   1.275 @@ -138,9 +276,9 @@
   1.276  lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
   1.277  by (simp add: even_nat_def)
   1.278  
   1.279 -lemma even_product_nat[simp,presburger,algebra]:
   1.280 +lemma even_product_nat:
   1.281    "even((x::nat) * y) = (even x | even y)"
   1.282 -by (simp add: even_nat_def int_mult)
   1.283 +  by (fact even_times_iff)
   1.284  
   1.285  lemma even_sum_nat[simp,presburger,algebra]:
   1.286    "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"