purely algebraic characterization of even and odd
authorhaftmann
Tue Oct 14 08:23:23 2014 +0200 (2014-10-14)
changeset 58678398e05aa84d4
parent 58677 74a81d6f3c54
child 58679 33c90658448a
purely algebraic characterization of even and odd
NEWS
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
src/HOL/Parity.thy
     1.1 --- a/NEWS	Tue Oct 14 16:19:42 2014 +0200
     1.2 +++ b/NEWS	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -50,6 +50,7 @@
     1.4  
     1.5  * More foundational definition for predicate "even":
     1.6    even_def ~> even_iff_mod_2_eq_zero
     1.7 +  even_iff_2_dvd ~> even_def
     1.8  Minor INCOMPATIBILITY.
     1.9  
    1.10  * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
     2.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 14 16:19:42 2014 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Oct 14 08:23:23 2014 +0200
     2.3 @@ -12,6 +12,11 @@
     2.4    "~~/src/HOL/ex/Records"
     2.5  begin
     2.6  
     2.7 +lemma [code]: -- {* Formal joining of hierarchy of implicit definitions in Scala *}
     2.8 +  fixes a :: "'a :: semiring_div_parity"
     2.9 +  shows "even a \<longleftrightarrow> a mod 2 = 0"
    2.10 +  by (fact even_iff_mod_2_eq_zero)
    2.11 +
    2.12  inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.13  where
    2.14    empty: "sublist [] xs"
     3.1 --- a/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Tue Oct 14 16:19:42 2014 +0200
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Tue Oct 14 08:23:23 2014 +0200
     3.3 @@ -16,20 +16,6 @@
     3.4    by a corresponding @{text export_code} command.
     3.5  *}
     3.6  
     3.7 -text {* Formal joining of hierarchy of implicit definitions in Scala *}
     3.8 -
     3.9 -class semiring_numeral_even_odd = semiring_numeral_div + even_odd
    3.10 -
    3.11 -instance nat :: semiring_numeral_even_odd ..
    3.12 -
    3.13 -definition semiring_numeral_even_odd :: "'a itself \<Rightarrow> 'a::semiring_numeral_even_odd"
    3.14 -where
    3.15 -  "semiring_numeral_even_odd TYPE('a) = undefined"
    3.16 -
    3.17 -definition semiring_numeral_even_odd_nat :: "nat itself \<Rightarrow> nat"
    3.18 -where
    3.19 -  "semiring_numeral_even_odd_nat = semiring_numeral_even_odd"
    3.20 -
    3.21 -export_code _ checking  SML OCaml? Haskell? Scala
    3.22 +export_code _ checking SML OCaml? Haskell? Scala
    3.23  
    3.24  end
     4.1 --- a/src/HOL/Parity.thy	Tue Oct 14 16:19:42 2014 +0200
     4.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     4.3 @@ -9,50 +9,211 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 -class even_odd = semiring_div_parity
     4.8 +subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
     4.9 +
    4.10 +lemma two_dvd_Suc_Suc_iff [simp]:
    4.11 +  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
    4.12 +  using dvd_add_triv_right_iff [of 2 n] by simp
    4.13 +
    4.14 +lemma two_dvd_Suc_iff:
    4.15 +  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
    4.16 +  by (induct n) auto
    4.17 +
    4.18 +lemma two_dvd_diff_iff:
    4.19 +  fixes k l :: int
    4.20 +  shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
    4.21 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
    4.22 +
    4.23 +lemma two_dvd_abs_add_iff:
    4.24 +  fixes k l :: int
    4.25 +  shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
    4.26 +  by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
    4.27 +
    4.28 +lemma two_dvd_add_abs_iff:
    4.29 +  fixes k l :: int
    4.30 +  shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
    4.31 +  using two_dvd_abs_add_iff [of l k] by (simp add: ac_simps)
    4.32 +
    4.33 +
    4.34 +subsection {* Ring structures with parity *}
    4.35 +
    4.36 +class semiring_parity = semiring_dvd + semiring_numeral +
    4.37 +  assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
    4.38 +  assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    4.39 +  assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
    4.40 +begin
    4.41 +
    4.42 +lemma two_dvd_plus_one_iff [simp]:
    4.43 +  "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
    4.44 +  by (auto simp add: dvd_add_right_iff intro: not_dvd_not_dvd_dvd_add)
    4.45 +
    4.46 +end
    4.47 +
    4.48 +instance nat :: semiring_parity
    4.49 +proof
    4.50 +  show "\<not> (2 :: nat) dvd 1"
    4.51 +    by (rule notI, erule dvdE) simp
    4.52 +next
    4.53 +  fix m n :: nat
    4.54 +  assume "\<not> 2 dvd m"
    4.55 +  moreover assume "\<not> 2 dvd n"
    4.56 +  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
    4.57 +    by (simp add: two_dvd_Suc_iff)
    4.58 +  then have "2 dvd Suc m + Suc n"
    4.59 +    by (blast intro: dvd_add)
    4.60 +  also have "Suc m + Suc n = m + n + 2"
    4.61 +    by simp
    4.62 +  finally show "2 dvd m + n"
    4.63 +    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
    4.64 +next
    4.65 +  fix m n :: nat
    4.66 +  assume *: "2 dvd m * n"
    4.67 +  show "2 dvd m \<or> 2 dvd n"
    4.68 +  proof (rule disjCI)
    4.69 +    assume "\<not> 2 dvd n"
    4.70 +    then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff)
    4.71 +    then obtain r where "Suc n = 2 * r" ..
    4.72 +    moreover from * obtain s where "m * n = 2 * s" ..
    4.73 +    then have "2 * s + m = m * Suc n" by simp
    4.74 +    ultimately have " 2 * s + m = 2 * (m * r)" by simp
    4.75 +    then have "m = 2 * (m * r - s)" by simp
    4.76 +    then show "2 dvd m" ..
    4.77 +  qed
    4.78 +qed
    4.79 +
    4.80 +class ring_parity = comm_ring_1 + semiring_parity
    4.81 +
    4.82 +instance int :: ring_parity
    4.83 +proof
    4.84 +  show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
    4.85 +  fix k l :: int
    4.86 +  assume "\<not> 2 dvd k"
    4.87 +  moreover assume "\<not> 2 dvd l"
    4.88 +  ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>" 
    4.89 +    by (auto simp add: dvd_int_unfold_dvd_nat intro: not_dvd_not_dvd_dvd_add)
    4.90 +  then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>"
    4.91 +    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
    4.92 +  then show "2 dvd k + l"
    4.93 +    by (simp add: two_dvd_abs_add_iff two_dvd_add_abs_iff)
    4.94 +qed (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
    4.95 +
    4.96 +context semiring_div_parity
    4.97 +begin
    4.98 +
    4.99 +subclass semiring_parity
   4.100 +proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
   4.101 +  fix a b c
   4.102 +  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
   4.103 +    by simp
   4.104 +next
   4.105 +  fix a b c
   4.106 +  assume "(b + c) mod a = 0"
   4.107 +  with mod_add_eq [of b c a]
   4.108 +  have "(b mod a + c mod a) mod a = 0"
   4.109 +    by simp
   4.110 +  moreover assume "b mod a = 0"
   4.111 +  ultimately show "c mod a = 0"
   4.112 +    by simp
   4.113 +next
   4.114 +  show "1 mod 2 = 1"
   4.115 +    by (fact one_mod_two_eq_one)
   4.116 +next
   4.117 +  fix a b
   4.118 +  assume "a mod 2 = 1"
   4.119 +  moreover assume "b mod 2 = 1"
   4.120 +  ultimately show "(a + b) mod 2 = 0"
   4.121 +    using mod_add_eq [of a b 2] by simp
   4.122 +next
   4.123 +  fix a b
   4.124 +  assume "(a * b) mod 2 = 0"
   4.125 +  then have "(a mod 2) * (b mod 2) = 0"
   4.126 +    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
   4.127 +  then show "a mod 2 = 0 \<or> b mod 2 = 0"
   4.128 +    by (rule divisors_zero)
   4.129 +qed
   4.130 +
   4.131 +end
   4.132 +
   4.133 +
   4.134 +subsection {* Dedicated @{text even}/@{text odd} predicate *}
   4.135 +
   4.136 +context semiring_parity
   4.137  begin
   4.138  
   4.139  definition even :: "'a \<Rightarrow> bool"
   4.140  where
   4.141    [algebra]: "even a \<longleftrightarrow> 2 dvd a"
   4.142  
   4.143 -lemmas even_iff_2_dvd = even_def
   4.144 +abbreviation odd :: "'a \<Rightarrow> bool"
   4.145 +where
   4.146 +  "odd a \<equiv> \<not> even a"
   4.147 +
   4.148 +lemma even_times_iff [simp, presburger, algebra]:
   4.149 +  "even (a * b) \<longleftrightarrow> even a \<or> even b"
   4.150 +  by (auto simp add: even_def dest: two_is_prime)
   4.151 +
   4.152 +lemma even_zero [simp]:
   4.153 +  "even 0"
   4.154 +  by (simp add: even_def)
   4.155 +
   4.156 +lemma odd_one [simp]:
   4.157 +  "odd 1"
   4.158 +  by (simp add: even_def)
   4.159 +
   4.160 +lemma even_numeral [simp]:
   4.161 +  "even (numeral (Num.Bit0 n))"
   4.162 +proof -
   4.163 +  have "even (2 * numeral n)"
   4.164 +    unfolding even_times_iff by (simp add: even_def)
   4.165 +  then have "even (numeral n + numeral n)"
   4.166 +    unfolding mult_2 .
   4.167 +  then show ?thesis
   4.168 +    unfolding numeral.simps .
   4.169 +qed
   4.170 +
   4.171 +lemma odd_numeral [simp]:
   4.172 +  "odd (numeral (Num.Bit1 n))"
   4.173 +proof
   4.174 +  assume "even (numeral (num.Bit1 n))"
   4.175 +  then have "even (numeral n + numeral n + 1)"
   4.176 +    unfolding numeral.simps .
   4.177 +  then have "even (2 * numeral n + 1)"
   4.178 +    unfolding mult_2 .
   4.179 +  then have "2 dvd numeral n * 2 + 1"
   4.180 +    unfolding even_def by (simp add: ac_simps)
   4.181 +  with dvd_add_times_triv_left_iff [of 2 "numeral n" 1]
   4.182 +    have "2 dvd 1"
   4.183 +    by simp
   4.184 +  then show False by simp
   4.185 +qed
   4.186 +
   4.187 +end
   4.188 +
   4.189 +context semiring_div_parity
   4.190 +begin
   4.191  
   4.192  lemma even_iff_mod_2_eq_zero [presburger]:
   4.193    "even a \<longleftrightarrow> a mod 2 = 0"
   4.194    by (simp add: even_def dvd_eq_mod_eq_0)
   4.195  
   4.196 -lemma even_zero [simp]:
   4.197 -  "even 0"
   4.198 -  by (simp add: even_iff_mod_2_eq_zero)
   4.199 -
   4.200  lemma even_times_anything:
   4.201    "even a \<Longrightarrow> even (a * b)"
   4.202 -  by (simp add: even_iff_2_dvd)
   4.203 +  by (simp add: even_def)
   4.204  
   4.205  lemma anything_times_even:
   4.206    "even a \<Longrightarrow> even (b * a)"
   4.207 -  by (simp add: even_iff_2_dvd)
   4.208 -
   4.209 -abbreviation odd :: "'a \<Rightarrow> bool"
   4.210 -where
   4.211 -  "odd a \<equiv> \<not> even a"
   4.212 +  by (simp add: even_def)
   4.213  
   4.214  lemma odd_times_odd:
   4.215    "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)" 
   4.216    by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)
   4.217  
   4.218 -lemma even_product [simp, presburger]:
   4.219 +lemma even_product:
   4.220    "even (a * b) \<longleftrightarrow> even a \<or> even b"
   4.221 -  apply (auto simp add: even_times_anything anything_times_even)
   4.222 -  apply (rule ccontr)
   4.223 -  apply (auto simp add: odd_times_odd)
   4.224 -  done
   4.225 +  by (fact even_times_iff)
   4.226  
   4.227  end
   4.228  
   4.229 -instance nat and int  :: even_odd ..
   4.230 -
   4.231  lemma even_nat_def [presburger]:
   4.232    "even x \<longleftrightarrow> even (int x)"
   4.233    by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)
   4.234 @@ -65,31 +226,8 @@
   4.235    transfer_int_nat_relations
   4.236  ]
   4.237  
   4.238 -lemma odd_one_int [simp]:
   4.239 -  "odd (1::int)"
   4.240 -  by presburger
   4.241 -
   4.242 -lemma odd_1_nat [simp]:
   4.243 -  "odd (1::nat)"
   4.244 -  by presburger
   4.245 -
   4.246 -lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
   4.247 -  unfolding even_iff_mod_2_eq_zero by simp
   4.248 -
   4.249 -lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
   4.250 -  unfolding even_iff_mod_2_eq_zero by simp
   4.251 -
   4.252 -(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
   4.253  declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v
   4.254  
   4.255 -lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
   4.256 -  unfolding even_nat_def by simp
   4.257 -
   4.258 -lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
   4.259 -  unfolding even_nat_def by simp
   4.260 -
   4.261 -subsection {* Even and odd are mutually exclusive *}
   4.262 -
   4.263  
   4.264  subsection {* Behavior under integer arithmetic operations *}
   4.265  
   4.266 @@ -128,7 +266,7 @@
   4.267  lemma two_times_odd_div_two_plus_one:
   4.268    "odd (x::int) ==> 2 * (x div 2) + 1 = x"
   4.269  by presburger
   4.270 -
   4.271 +  
   4.272  lemma even_equiv_def: "even (x::int) = (EX y. x = 2 * y)" by presburger
   4.273  
   4.274  lemma odd_equiv_def: "odd (x::int) = (EX y. x = 2 * y + 1)" by presburger
   4.275 @@ -138,9 +276,9 @@
   4.276  lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
   4.277  by (simp add: even_nat_def)
   4.278  
   4.279 -lemma even_product_nat[simp,presburger,algebra]:
   4.280 +lemma even_product_nat:
   4.281    "even((x::nat) * y) = (even x | even y)"
   4.282 -by (simp add: even_nat_def int_mult)
   4.283 +  by (fact even_times_iff)
   4.284  
   4.285  lemma even_sum_nat[simp,presburger,algebra]:
   4.286    "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"