# Theory Parity

```(*  Title:      HOL/Parity.thy
Author:     Jacques D. Fleuriot
*)

section ‹Parity in rings and semirings›

theory Parity
imports Euclidean_Rings
begin

subsection ‹Ring structures with parity and ‹even›/‹odd› predicates›

class semiring_parity = comm_semiring_1 + semiring_modulo +
assumes even_iff_mod_2_eq_zero: "2 dvd a ⟷ a mod 2 = 0"
and odd_iff_mod_2_eq_one: "¬ 2 dvd a ⟷ a mod 2 = 1"
and odd_one [simp]: "¬ 2 dvd 1"
begin

abbreviation even :: "'a ⇒ bool"
where "even a ≡ 2 dvd a"

abbreviation odd :: "'a ⇒ bool"
where "odd a ≡ ¬ 2 dvd a"

end

class ring_parity = ring + semiring_parity
begin

subclass comm_ring_1 ..

end

instance nat :: semiring_parity

instance int :: ring_parity
by standard (auto simp add: dvd_eq_mod_eq_0)

context semiring_parity
begin

lemma parity_cases [case_names even odd]:
assumes "even a ⟹ a mod 2 = 0 ⟹ P"
assumes "odd a ⟹ a mod 2 = 1 ⟹ P"
shows P
using assms by (cases "even a")
(simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric])

lemma odd_of_bool_self [simp]:
‹odd (of_bool p) ⟷ p›
by (cases p) simp_all

lemma not_mod_2_eq_0_eq_1 [simp]:
"a mod 2 ≠ 0 ⟷ a mod 2 = 1"
by (cases a rule: parity_cases) simp_all

lemma not_mod_2_eq_1_eq_0 [simp]:
"a mod 2 ≠ 1 ⟷ a mod 2 = 0"
by (cases a rule: parity_cases) simp_all

lemma evenE [elim?]:
assumes "even a"
obtains b where "a = 2 * b"
using assms by (rule dvdE)

lemma oddE [elim?]:
assumes "odd a"
obtains b where "a = 2 * b + 1"
proof -
have "a = 2 * (a div 2) + a mod 2"
with assms have "a = 2 * (a div 2) + 1"
then show ?thesis ..
qed

lemma mod_2_eq_odd:
"a mod 2 = of_bool (odd a)"
by (auto elim: oddE simp add: even_iff_mod_2_eq_zero)

lemma of_bool_odd_eq_mod_2:
"of_bool (odd a) = a mod 2"

lemma even_mod_2_iff [simp]:
‹even (a mod 2) ⟷ even a›

lemma mod2_eq_if:
"a mod 2 = (if even a then 0 else 1)"

lemma even_zero [simp]:
"even 0"
by (fact dvd_0_right)

"even (a + b)" if "odd a" and "odd b"
proof -
from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
by (blast elim: oddE)
then have "a + b = 2 * c + 2 * d + (1 + 1)"
by (simp only: ac_simps)
also have "… = 2 * (c + d + 1)"
finally show ?thesis ..
qed

"even (a + b) ⟷ (even a ⟷ even b)"

"odd (a + b) ⟷ ¬ (odd a ⟷ odd b)"
by simp

lemma even_plus_one_iff [simp]:
"even (a + 1) ⟷ odd a"

lemma even_mult_iff [simp]:
"even (a * b) ⟷ even a ∨ even b" (is "?P ⟷ ?Q")
proof
assume ?Q
then show ?P
by auto
next
assume ?P
show ?Q
proof (rule ccontr)
assume "¬ (even a ∨ even b)"
then have "odd a" and "odd b"
by auto
then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
by (blast elim: oddE)
then have "a * b = (2 * r + 1) * (2 * s + 1)"
by simp
also have "… = 2 * (2 * r * s + r + s) + 1"
finally have "odd (a * b)"
by simp
with ‹?P› show False
by auto
qed
qed

lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
proof -
have "even (2 * numeral n)"
unfolding even_mult_iff by simp
then have "even (numeral n + numeral n)"
unfolding mult_2 .
then show ?thesis
unfolding numeral.simps .
qed

lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))"
proof
assume "even (numeral (num.Bit1 n))"
then have "even (numeral n + numeral n + 1)"
unfolding numeral.simps .
then have "even (2 * numeral n + 1)"
unfolding mult_2 .
then have "2 dvd numeral n * 2 + 1"
then have "2 dvd 1"
using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp
then show False by simp
qed

lemma odd_numeral_BitM [simp]:
‹odd (numeral (Num.BitM w))›
by (cases w) simp_all

lemma even_power [simp]: "even (a ^ n) ⟷ even a ∧ n > 0"
by (induct n) auto

lemma even_prod_iff:
‹even (prod f A) ⟷ (∃a∈A. even (f a))› if ‹finite A›
using that by (induction A) simp_all

‹2 ^ n - 1 = (∑m∈{q. q < n}. 2 ^ m)›
proof -
have *: ‹{q. q < Suc m} = insert m {q. q < m}› for m
by auto
have ‹2 ^ n = (∑m∈{q. q < n}. 2 ^ m) + 1›
by (induction n) (simp_all add: ac_simps mult_2 *)
then have ‹2 ^ n - 1 = (∑m∈{q. q < n}. 2 ^ m) + 1 - 1›
by simp
then show ?thesis
by simp
qed

‹2 ^ n - Suc 0 = (∑m∈{q. q < n}. 2 ^ m)›
using mask_eq_sum_exp [where ?'a = nat] by simp

end

context ring_parity
begin

lemma even_minus:
"even (- a) ⟷ even a"
by (fact dvd_minus_iff)

lemma even_diff [simp]:
"even (a - b) ⟷ even (a + b)"
using even_add [of a "- b"] by simp

end

subsection ‹Instance for \<^typ>‹nat››

lemma even_Suc_Suc_iff [simp]:
"even (Suc (Suc n)) ⟷ even n"
using dvd_add_triv_right_iff [of 2 n] by simp

lemma even_Suc [simp]: "even (Suc n) ⟷ odd n"
using even_plus_one_iff [of n] by simp

lemma even_diff_nat [simp]:
"even (m - n) ⟷ m < n ∨ even (m + n)" for m n :: nat
proof (cases "n ≤ m")
case True
then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
moreover have "even (m - n) ⟷ even (m - n + n * 2)" by simp
ultimately have "even (m - n) ⟷ even (m + n)" by (simp only:)
then show ?thesis by auto
next
case False
then show ?thesis by simp
qed

lemma odd_pos:
"odd n ⟹ 0 < n" for n :: nat
by (auto elim: oddE)

lemma Suc_double_not_eq_double:
"Suc (2 * m) ≠ 2 * n"
proof
assume "Suc (2 * m) = 2 * n"
moreover have "odd (Suc (2 * m))" and "even (2 * n)"
by simp_all
ultimately show False by simp
qed

lemma double_not_eq_Suc_double:
"2 * m ≠ Suc (2 * n)"
using Suc_double_not_eq_double [of n m] by simp

lemma odd_Suc_minus_one [simp]: "odd n ⟹ Suc (n - Suc 0) = n"
by (auto elim: oddE)

lemma even_Suc_div_two [simp]:
"even n ⟹ Suc n div 2 = n div 2"
by auto

lemma odd_Suc_div_two [simp]:
"odd n ⟹ Suc n div 2 = Suc (n div 2)"
by (auto elim: oddE)

lemma odd_two_times_div_two_nat [simp]:
assumes "odd n"
shows "2 * (n div 2) = n - (1 :: nat)"
proof -
from assms have "2 * (n div 2) + 1 = n"
by (auto elim: oddE)
then have "Suc (2 * (n div 2)) - 1 = n - 1"
by simp
then show ?thesis
by simp
qed

lemma not_mod2_eq_Suc_0_eq_0 [simp]:
"n mod 2 ≠ Suc 0 ⟷ n mod 2 = 0"
using not_mod_2_eq_1_eq_0 [of n] by simp

lemma odd_card_imp_not_empty:
‹A ≠ {}› if ‹odd (card A)›
using that by auto

lemma nat_induct2 [case_names 0 1 step]:
assumes "P 0" "P 1" and step: "⋀n::nat. P n ⟹ P (n + 2)"
shows "P n"
proof (induct n rule: less_induct)
case (less n)
show ?case
proof (cases "n < Suc (Suc 0)")
case True
then show ?thesis
using assms by (auto simp: less_Suc_eq)
next
case False
then obtain k where k: "n = Suc (Suc k)"
then have "k<n"
by simp
with less assms have "P (k+2)"
by blast
then show ?thesis
qed
qed

context semiring_parity
begin

lemma even_sum_iff:
‹even (sum f A) ⟷ even (card {a∈A. odd (f a)})› if ‹finite A›
using that proof (induction A)
case empty
then show ?case
by simp
next
case (insert a A)
moreover have ‹{b ∈ insert a A. odd (f b)} = (if odd (f a) then {a} else {}) ∪ {b ∈ A. odd (f b)}›
by auto
ultimately show ?case
by simp
qed

‹even (2 ^ n - 1) ⟷ n = 0›
proof (cases ‹n = 0›)
case True
then show ?thesis
by simp
next
case False
then have ‹{a. a = 0 ∧ a < n} = {0}›
by auto
then show ?thesis
qed

lemma even_of_nat_iff [simp]:
"even (of_nat n) ⟷ even n"
by (induction n) simp_all

end

subsection ‹Parity and powers›

context ring_1
begin

lemma power_minus_even [simp]: "even n ⟹ (- a) ^ n = a ^ n"
by (auto elim: evenE)

lemma power_minus_odd [simp]: "odd n ⟹ (- a) ^ n = - (a ^ n)"
by (auto elim: oddE)

lemma uminus_power_if:
"(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
by auto

lemma neg_one_even_power [simp]: "even n ⟹ (- 1) ^ n = 1"
by simp

lemma neg_one_odd_power [simp]: "odd n ⟹ (- 1) ^ n = - 1"
by simp

lemma neg_one_power_add_eq_neg_one_power_diff: "k ≤ n ⟹ (- 1) ^ (n + k) = (- 1) ^ (n - k)"
by (cases "even (n + k)") auto

lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)"
by (induct n) auto

end

context linordered_idom
begin

lemma zero_le_even_power: "even n ⟹ 0 ≤ a ^ n"
by (auto elim: evenE)

lemma zero_le_odd_power: "odd n ⟹ 0 ≤ a ^ n ⟷ 0 ≤ a"
by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)

lemma zero_le_power_eq: "0 ≤ a ^ n ⟷ even n ∨ odd n ∧ 0 ≤ a"
by (auto simp add: zero_le_even_power zero_le_odd_power)

lemma zero_less_power_eq: "0 < a ^ n ⟷ n = 0 ∨ even n ∧ a ≠ 0 ∨ odd n ∧ 0 < a"
proof -
have [simp]: "0 = a ^ n ⟷ a = 0 ∧ n > 0"
unfolding power_eq_0_iff [of a n, symmetric] by blast
show ?thesis
unfolding less_le zero_le_power_eq by auto
qed

lemma power_less_zero_eq [simp]: "a ^ n < 0 ⟷ odd n ∧ a < 0"
unfolding not_le [symmetric] zero_le_power_eq by auto

lemma power_le_zero_eq: "a ^ n ≤ 0 ⟷ n > 0 ∧ (odd n ∧ a ≤ 0 ∨ even n ∧ a = 0)"
unfolding not_less [symmetric] zero_less_power_eq by auto

lemma power_even_abs: "even n ⟹ ¦a¦ ^ n = a ^ n"
using power_abs [of a n] by (simp add: zero_le_even_power)

lemma power_mono_even:
assumes "even n" and "¦a¦ ≤ ¦b¦"
shows "a ^ n ≤ b ^ n"
proof -
have "0 ≤ ¦a¦" by auto
with ‹¦a¦ ≤ ¦b¦› have "¦a¦ ^ n ≤ ¦b¦ ^ n"
by (rule power_mono)
with ‹even n› show ?thesis
qed

lemma power_mono_odd:
assumes "odd n" and "a ≤ b"
shows "a ^ n ≤ b ^ n"
proof (cases "b < 0")
case True
with ‹a ≤ b› have "- b ≤ - a" and "0 ≤ - b" by auto
then have "(- b) ^ n ≤ (- a) ^ n" by (rule power_mono)
with ‹odd n› show ?thesis by simp
next
case False
then have "0 ≤ b" by auto
show ?thesis
proof (cases "a < 0")
case True
then have "n ≠ 0" and "a ≤ 0" using ‹odd n› [THEN odd_pos] by auto
then have "a ^ n ≤ 0" unfolding power_le_zero_eq using ‹odd n› by auto
moreover from ‹0 ≤ b› have "0 ≤ b ^ n" by auto
ultimately show ?thesis by auto
next
case False
then have "0 ≤ a" by auto
with ‹a ≤ b› show ?thesis
using power_mono by auto
qed
qed

text ‹Simplify, when the exponent is a numeral›

lemma zero_le_power_eq_numeral [simp]:
"0 ≤ a ^ numeral w ⟷ even (numeral w :: nat) ∨ odd (numeral w :: nat) ∧ 0 ≤ a"
by (fact zero_le_power_eq)

lemma zero_less_power_eq_numeral [simp]:
"0 < a ^ numeral w ⟷
numeral w = (0 :: nat) ∨
even (numeral w :: nat) ∧ a ≠ 0 ∨
odd (numeral w :: nat) ∧ 0 < a"
by (fact zero_less_power_eq)

lemma power_le_zero_eq_numeral [simp]:
"a ^ numeral w ≤ 0 ⟷
(0 :: nat) < numeral w ∧
(odd (numeral w :: nat) ∧ a ≤ 0 ∨ even (numeral w :: nat) ∧ a = 0)"
by (fact power_le_zero_eq)

lemma power_less_zero_eq_numeral [simp]:
"a ^ numeral w < 0 ⟷ odd (numeral w :: nat) ∧ a < 0"
by (fact power_less_zero_eq)

lemma power_even_abs_numeral [simp]:
"even (numeral w :: nat) ⟹ ¦a¦ ^ numeral w = a ^ numeral w"
by (fact power_even_abs)

end

subsection ‹Instance for \<^typ>‹int››

lemma even_diff_iff:
"even (k - l) ⟷ even (k + l)" for k l :: int
by (fact even_diff)

"even (¦k¦ + l) ⟷ even (k + l)" for k l :: int
by simp

"even (k + ¦l¦) ⟷ even (k + l)" for k l :: int
by simp

lemma even_nat_iff: "0 ≤ k ⟹ even (nat k) ⟷ even k"
by (simp add: even_of_nat_iff [of "nat k", where ?'a = int, symmetric])

context
assumes "SORT_CONSTRAINT('a::division_ring)"
begin

lemma power_int_minus_left:
"power_int (-a :: 'a) n = (if even n then power_int a n else -power_int a n)"
by (auto simp: power_int_def minus_one_power_iff even_nat_iff)

lemma power_int_minus_left_even [simp]: "even n ⟹ power_int (-a :: 'a) n = power_int a n"

lemma power_int_minus_left_odd [simp]: "odd n ⟹ power_int (-a :: 'a) n = -power_int a n"

lemma power_int_minus_left_distrib:
"NO_MATCH (-1) x ⟹ power_int (-a :: 'a) n = power_int (-1) n * power_int a n"

lemma power_int_minus_one_minus: "power_int (-1 :: 'a) (-n) = power_int (-1) n"

lemma power_int_minus_one_diff_commute: "power_int (-1 :: 'a) (a - b) = power_int (-1) (b - a)"
by (subst power_int_minus_one_minus [symmetric]) auto

lemma power_int_minus_one_mult_self [simp]:
"power_int (-1 :: 'a) m * power_int (-1) m = 1"

lemma power_int_minus_one_mult_self' [simp]:
"power_int (-1 :: 'a) m * (power_int (-1) m * b) = b"

end

subsection ‹Special case: euclidean rings containing the natural numbers›

class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
begin

lemma division_segment_eq_iff:
"a = b" if "division_segment a = division_segment b"
and "euclidean_size a = euclidean_size b"
using that division_segment_euclidean_size [of a] by simp

lemma euclidean_size_of_nat [simp]:
"euclidean_size (of_nat n) = n"
proof -
have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
by (fact division_segment_euclidean_size)
then show ?thesis by simp
qed

lemma of_nat_euclidean_size:
"of_nat (euclidean_size a) = a div division_segment a"
proof -
have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
by (subst nonzero_mult_div_cancel_left) simp_all
also have "… = a div division_segment a"
by simp
finally show ?thesis .
qed

lemma division_segment_1 [simp]:
"division_segment 1 = 1"
using division_segment_of_nat [of 1] by simp

lemma division_segment_numeral [simp]:
"division_segment (numeral k) = 1"
using division_segment_of_nat [of "numeral k"] by simp

lemma euclidean_size_1 [simp]:
"euclidean_size 1 = 1"
using euclidean_size_of_nat [of 1] by simp

lemma euclidean_size_numeral [simp]:
"euclidean_size (numeral k) = numeral k"
using euclidean_size_of_nat [of "numeral k"] by simp

lemma of_nat_dvd_iff:
"of_nat m dvd of_nat n ⟷ m dvd n" (is "?P ⟷ ?Q")
proof (cases "m = 0")
case True
then show ?thesis
by simp
next
case False
show ?thesis
proof
assume ?Q
then show ?P
by auto
next
assume ?P
with False have "of_nat n = of_nat n div of_nat m * of_nat m"
by simp
then have "of_nat n = of_nat (n div m * m)"
then have "n = n div m * m"
by (simp only: of_nat_eq_iff)
then have "n = m * (n div m)"
then show ?Q ..
qed
qed

lemma of_nat_mod:
"of_nat (m mod n) = of_nat m mod of_nat n"
proof -
have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
also have "of_nat m = of_nat (m div n * n + m mod n)"
by simp
finally show ?thesis
by (simp only: of_nat_div of_nat_mult of_nat_add) simp
qed

lemma one_div_two_eq_zero [simp]:
"1 div 2 = 0"
proof -
from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
by (simp only:) simp
then show ?thesis
by simp
qed

lemma one_mod_two_eq_one [simp]:
"1 mod 2 = 1"
proof -
from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
by (simp only:) simp
then show ?thesis
by simp
qed

lemma one_mod_2_pow_eq [simp]:
"1 mod (2 ^ n) = of_bool (n > 0)"
proof -
have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
using of_nat_mod [of 1 "2 ^ n"] by simp
also have "… = of_bool (n > 0)"
by simp
finally show ?thesis .
qed

lemma one_div_2_pow_eq [simp]:
"1 div (2 ^ n) = of_bool (n = 0)"
using div_mult_mod_eq [of 1 "2 ^ n"] by auto

lemma div_mult2_eq':
‹a div (of_nat m * of_nat n) = a div of_nat m div of_nat n›
proof (cases ‹m = 0 ∨ n = 0›)
case True
then show ?thesis
by auto
next
case False
then have ‹m > 0› ‹n > 0›
by simp_all
show ?thesis
proof (cases ‹of_nat m * of_nat n dvd a›)
case True
then obtain b where ‹a = (of_nat m * of_nat n) * b› ..
then have ‹a = of_nat m * (of_nat n * b)›
then show ?thesis
by simp
next
case False
define q where ‹q = a div (of_nat m * of_nat n)›
define r where ‹r = a mod (of_nat m * of_nat n)›
from ‹m > 0› ‹n > 0› ‹¬ of_nat m * of_nat n dvd a› r_def have "division_segment r = 1"
using division_segment_of_nat [of "m * n"] by (simp add: division_segment_mod)
with division_segment_euclidean_size [of r]
have "of_nat (euclidean_size r) = r"
by simp
have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0"
by simp
with ‹m > 0› ‹n > 0› r_def have "r div (of_nat m * of_nat n) = 0"
by simp
with ‹of_nat (euclidean_size r) = r›
have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0"
by simp
then have "of_nat (euclidean_size r div (m * n)) = 0"
then have "of_nat (euclidean_size r div m div n) = 0"
with ‹of_nat (euclidean_size r) = r› have "r div of_nat m div of_nat n = 0"
with ‹m > 0› ‹n > 0› q_def
have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n"
by simp
moreover have ‹a = q * (of_nat m * of_nat n) + r›
by (simp add: q_def r_def div_mult_mod_eq)
ultimately show ‹a div (of_nat m * of_nat n) = a div of_nat m div of_nat n›
using q_def [symmetric] div_plus_div_distrib_dvd_right [of ‹of_nat m› ‹q * (of_nat m * of_nat n)› r]
qed
qed

lemma mod_mult2_eq':
"a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m"
proof -
have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)"
moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)"
ultimately show ?thesis
qed

lemma div_mult2_numeral_eq:
"a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
proof -
have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
by simp
also have "… = a div (of_nat (numeral k) * of_nat (numeral l))"
by (fact div_mult2_eq' [symmetric])
also have "… = ?B"
by simp
finally show ?thesis .
qed

lemma numeral_Bit0_div_2:
"numeral (num.Bit0 n) div 2 = numeral n"
proof -
have "numeral (num.Bit0 n) = numeral n + numeral n"
by (simp only: numeral.simps)
also have "… = numeral n * 2"
finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2"
by simp
also have "… = numeral n"
by (rule nonzero_mult_div_cancel_right) simp
finally show ?thesis .
qed

lemma numeral_Bit1_div_2:
"numeral (num.Bit1 n) div 2 = numeral n"
proof -
have "numeral (num.Bit1 n) = numeral n + numeral n + 1"
by (simp only: numeral.simps)
also have "… = numeral n * 2 + 1"
finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2"
by simp
also have "… = numeral n * 2 div 2 + 1 div 2"
using dvd_triv_right by (rule div_plus_div_distrib_dvd_left)
also have "… = numeral n * 2 div 2"
by simp
also have "… = numeral n"
by (rule nonzero_mult_div_cancel_right) simp
finally show ?thesis .
qed

lemma exp_mod_exp:
‹2 ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m›
proof -
have ‹(2::nat) ^ m mod 2 ^ n = of_bool (m < n) * 2 ^ m› (is ‹?lhs = ?rhs›)
then have ‹of_nat ?lhs = of_nat ?rhs›
by simp
then show ?thesis
qed

‹(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - 1›
proof -
have ‹(2 ^ n - 1) mod 2 ^ m = 2 ^ min m n - (1::nat)› (is ‹?lhs = ?rhs›)
proof (cases ‹n ≤ m›)
case True
then show ?thesis
next
case False
then have ‹m < n›
by simp
then obtain q where n: ‹n = Suc q + m›
then have ‹min m n = m›
by simp
moreover have ‹(2::nat) ^ m ≤ 2 * 2 ^ q * 2 ^ m›
using mult_le_mono1 [of 1 ‹2 * 2 ^ q› ‹2 ^ m›] by simp
with n have ‹2 ^ n - 1 = (2 ^ Suc q - 1) * 2 ^ m + (2 ^ m - (1::nat))›
ultimately show ?thesis
by (simp only: euclidean_semiring_cancel_class.mod_mult_self3) simp
qed
then have ‹of_nat ?lhs = of_nat ?rhs›
by simp
then show ?thesis
qed

lemma of_bool_half_eq_0 [simp]:
‹of_bool b div 2 = 0›
by simp

end

class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat

instance nat :: unique_euclidean_semiring_with_nat

instance int :: unique_euclidean_ring_with_nat
by standard (auto simp add: divide_int_def division_segment_int_def elim: contrapos_np)

context unique_euclidean_semiring_with_nat
begin

subclass semiring_parity
proof
show "2 dvd a ⟷ a mod 2 = 0" for a
by (fact dvd_eq_mod_eq_0)
show "¬ 2 dvd a ⟷ a mod 2 = 1" for a
proof
assume "a mod 2 = 1"
then show "¬ 2 dvd a"
by auto
next
assume "¬ 2 dvd a"
have eucl: "euclidean_size (a mod 2) = 1"
proof (rule order_antisym)
show "euclidean_size (a mod 2) ≤ 1"
using mod_size_less [of 2 a] by simp
show "1 ≤ euclidean_size (a mod 2)"
using ‹¬ 2 dvd a› by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
qed
from ‹¬ 2 dvd a› have "¬ of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
by simp
then have "¬ of_nat 2 dvd of_nat (euclidean_size a)"
by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
then have "¬ 2 dvd euclidean_size a"
using of_nat_dvd_iff [of 2] by simp
then have "euclidean_size a mod 2 = 1"
then have "of_nat (euclidean_size a mod 2) = of_nat 1"
by simp
then have "of_nat (euclidean_size a) mod 2 = 1"
from ‹¬ 2 dvd a› eucl
show "a mod 2 = 1"
by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
qed
show "¬ is_unit 2"
proof (rule notI)
assume "is_unit 2"
then have "of_nat 2 dvd of_nat 1"
by simp
then have "is_unit (2::nat)"
by (simp only: of_nat_dvd_iff)
then show False
by simp
qed
qed

lemma even_succ_div_two [simp]:
"even a ⟹ (a + 1) div 2 = a div 2"
by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)

lemma odd_succ_div_two [simp]:
"odd a ⟹ (a + 1) div 2 = a div 2 + 1"

lemma even_two_times_div_two:
"even a ⟹ 2 * (a div 2) = a"
by (fact dvd_mult_div_cancel)

lemma odd_two_times_div_two_succ [simp]:
"odd a ⟹ 2 * (a div 2) + 1 = a"
using mult_div_mod_eq [of 2 a]

lemma coprime_left_2_iff_odd [simp]:
"coprime 2 a ⟷ odd a"
proof
assume "odd a"
show "coprime 2 a"
proof (rule coprimeI)
fix b
assume "b dvd 2" "b dvd a"
then have "b dvd a mod 2"
by (auto intro: dvd_mod)
with ‹odd a› show "is_unit b"
qed
next
assume "coprime 2 a"
show "odd a"
proof (rule notI)
assume "even a"
then obtain b where "a = 2 * b" ..
with ‹coprime 2 a› have "coprime 2 (2 * b)"
by simp
moreover have "¬ coprime 2 (2 * b)"
by (rule not_coprimeI [of 2]) simp_all
ultimately show False
by blast
qed
qed

lemma coprime_right_2_iff_odd [simp]:
"coprime a 2 ⟷ odd a"
using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)

end

context unique_euclidean_ring_with_nat
begin

subclass ring_parity ..

lemma minus_1_mod_2_eq [simp]:
"- 1 mod 2 = 1"

lemma minus_1_div_2_eq [simp]:
"- 1 div 2 = - 1"
proof -
from div_mult_mod_eq [of "- 1" 2]
have "- 1 div 2 * 2 = - 1 * 2"
then show ?thesis
using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
qed

end

context unique_euclidean_semiring_with_nat
begin

‹even ((2 ^ m - 1) div 2 ^ n) ⟷ m ≤ n›
proof -
have ‹even ((2 ^ m - 1) div 2 ^ n) ⟷ even (of_nat ((2 ^ m - Suc 0) div 2 ^ n))›
by (simp only: of_nat_div) (simp add: of_nat_diff)
also have ‹… ⟷ even ((2 ^ m - Suc 0) div 2 ^ n)›
by simp
also have ‹… ⟷ m ≤ n›
proof (cases ‹m ≤ n›)
case True
then show ?thesis
next
case False
then obtain r where r: ‹m = n + Suc r›
from r have ‹{q. q < m} ∩ {q. 2 ^ n dvd (2::nat) ^ q} = {q. n ≤ q ∧ q < m}›
moreover from r have ‹{q. q < m} ∩ {q. ¬ 2 ^ n dvd (2::nat) ^ q} = {q. q < n}›
moreover from False have ‹{q. n ≤ q ∧ q < m ∧ q ≤ n} = {n}›
by auto
then have ‹odd ((∑a∈{q. n ≤ q ∧ q < m}. 2 ^ a div (2::nat) ^ n) + sum ((^) 2) {q. q < n} div 2 ^ n)›
ultimately have ‹odd (sum ((^) (2::nat)) {q. q < m} div 2 ^ n)›
by (subst euclidean_semiring_cancel_class.sum_div_partition) simp_all
with False show ?thesis
qed
finally show ?thesis .
qed

end

subsection ‹Generic symbolic computations›

text ‹
The following type class contains everything necessary to formulate
a division algorithm in ring structures with numerals, restricted
to its positive segments.
›

class unique_euclidean_semiring_with_nat_division = unique_euclidean_semiring_with_nat +
fixes divmod :: ‹num ⇒ num ⇒ 'a × 'a›
and divmod_step :: ‹'a ⇒ 'a × 'a ⇒ 'a × 'a› ― ‹
These are conceptually definitions but force generated code
to be monomorphic wrt. particular instances of this class which
yields a significant speedup.›
assumes divmod_def: ‹divmod m n = (numeral m div numeral n, numeral m mod numeral n)›
and divmod_step_def [simp]: ‹divmod_step l (q, r) =
(if euclidean_size l ≤ euclidean_size r then (2 * q + 1, r - l)
else (2 * q, r))› ― ‹
This is a formulation of one step (referring to one digit position)
in school-method division: compare the dividend at the current
digit position with the remainder from previous division steps
and evaluate accordingly.›
begin

lemma fst_divmod:
‹fst (divmod m n) = numeral m div numeral n›

lemma snd_divmod:
‹snd (divmod m n) = numeral m mod numeral n›

text ‹
Following a formulation of school-method division.
If the divisor is smaller than the dividend, terminate.
If not, shift the dividend to the right until termination
occurs and then reiterate single division steps in the
opposite direction.
›

lemma divmod_divmod_step:
‹divmod m n = (if m < n then (0, numeral m)
else divmod_step (numeral n) (divmod m (Num.Bit0 n)))›
proof (cases ‹m < n›)
case True
then show ?thesis
by (simp add: prod_eq_iff fst_divmod snd_divmod flip: of_nat_numeral of_nat_div of_nat_mod)
next
case False
define r s t where ‹r = (numeral m :: nat)› ‹s = (numeral n :: nat)› ‹t = 2 * s›
then have *: ‹numeral m = of_nat r› ‹numeral n = of_nat s› ‹numeral (num.Bit0 n) = of_nat t›
and ‹¬ s ≤ r mod s›
have t: ‹2 * (r div t) = r div s - r div s mod 2›
‹r mod t = s * (r div s mod 2) + r mod s›
by (simp add: Rings.minus_mod_eq_mult_div Groups.mult.commute [of 2] Euclidean_Rings.div_mult2_eq ‹t = 2 * s›)
(use mod_mult2_eq [of r s 2] in ‹simp add: ac_simps ‹t = 2 * s››)
have rs: ‹r div s mod 2 = 0 ∨ r div s mod 2 = Suc 0›
by auto
from ‹¬ s ≤ r mod s› have ‹s ≤ r mod t ⟹
r div s = Suc (2 * (r div t)) ∧
r mod s = r mod t - s›
using rs
moreover have ‹r mod t < s ⟹
r div s = 2 * (r div t) ∧
r mod s = r mod t›
using rs
ultimately show ?thesis
by (simp add: divmod_def prod_eq_iff split_def Let_def
not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *)
(simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff)
qed

text ‹The division rewrite proper -- first, trivial results involving ‹1››

lemma divmod_trivial [simp]:
"divmod m Num.One = (numeral m, 0)"
"divmod num.One (num.Bit0 n) = (0, Numeral1)"
"divmod num.One (num.Bit1 n) = (0, Numeral1)"
using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)

text ‹Division by an even number is a right-shift›

lemma divmod_cancel [simp]:
‹divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) ⇒ (q, 2 * r))› (is ?P)
‹divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) ⇒ (q, 2 * r + 1))› (is ?Q)
proof -
define r s where ‹r = (numeral m :: nat)› ‹s = (numeral n :: nat)›
then have *: ‹numeral m = of_nat r› ‹numeral n = of_nat s›
‹numeral (num.Bit0 m) = of_nat (2 * r)› ‹numeral (num.Bit0 n) = of_nat (2 * s)›
‹numeral (num.Bit1 m) = of_nat (Suc (2 * r))›
by simp_all
have **: ‹Suc (2 * r) div 2 = r›
by simp
show ?P and ?Q
(simp_all flip: of_nat_numeral of_nat_div of_nat_mod of_nat_mult add.commute [of 1] of_nat_Suc
add: Euclidean_Rings.mod_mult_mult1 div_mult2_eq [of _ 2] mod_mult2_eq [of _ 2] **)
qed

text ‹The really hard work›

lemma divmod_steps [simp]:
"divmod (num.Bit0 m) (num.Bit1 n) =
(if m ≤ n then (0, numeral (num.Bit0 m))
else divmod_step (numeral (num.Bit1 n))
(divmod (num.Bit0 m)
(num.Bit0 (num.Bit1 n))))"
"divmod (num.Bit1 m) (num.Bit1 n) =
(if m < n then (0, numeral (num.Bit1 m))
else divmod_step (numeral (num.Bit1 n))
(divmod (num.Bit1 m)
(num.Bit0 (num.Bit1 n))))"

lemmas divmod_algorithm_code = divmod_trivial divmod_cancel divmod_steps

text ‹Special case: divisibility›

definition divides_aux :: "'a × 'a ⇒ bool"
where
"divides_aux qr ⟷ snd qr = 0"

lemma divides_aux_eq [simp]:
"divides_aux (q, r) ⟷ r = 0"

lemma dvd_numeral_simp [simp]:
"numeral m dvd numeral n ⟷ divides_aux (divmod n m)"

text ‹Generic computation of quotient and remainder›

lemma numeral_div_numeral [simp]:
"numeral k div numeral l = fst (divmod k l)"

lemma numeral_mod_numeral [simp]:
"numeral k mod numeral l = snd (divmod k l)"

lemma one_div_numeral [simp]:
"1 div numeral n = fst (divmod num.One n)"

lemma one_mod_numeral [simp]:
"1 mod numeral n = snd (divmod num.One n)"

end

instantiation nat :: unique_euclidean_semiring_with_nat_division
begin

definition divmod_nat :: "num ⇒ num ⇒ nat × nat"
where
divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"

definition divmod_step_nat :: "nat ⇒ nat × nat ⇒ nat × nat"
where
"divmod_step_nat l qr = (let (q, r) = qr
in if r ≥ l then (2 * q + 1, r - l)
else (2 * q, r))"

instance
by standard (simp_all add: divmod'_nat_def divmod_step_nat_def)

end

declare divmod_algorithm_code [where ?'a = nat, code]

lemma Suc_0_div_numeral [simp]:
‹Suc 0 div numeral Num.One = 1›
‹Suc 0 div numeral (Num.Bit0 n) = 0›
‹Suc 0 div numeral (Num.Bit1 n) = 0›
by simp_all

lemma Suc_0_mod_numeral [simp]:
‹Suc 0 mod numeral Num.One = 0›
‹Suc 0 mod numeral (Num.Bit0 n) = 1›
‹Suc 0 mod numeral (Num.Bit1 n) = 1›
by simp_all

instantiation int :: unique_euclidean_semiring_with_nat_division
begin

definition divmod_int :: "num ⇒ num ⇒ int × int"
where
"divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"

definition divmod_step_int :: "int ⇒ int × int ⇒ int × int"
where
"divmod_step_int l qr = (let (q, r) = qr
in if ¦l¦ ≤ ¦r¦ then (2 * q + 1, r - l)
else (2 * q, r))"

instance
by standard (auto simp add: divmod_int_def divmod_step_int_def)

end

declare divmod_algorithm_code [where ?'a = int, code]

context
begin

qualified definition adjust_div :: "int × int ⇒ int"
where
"adjust_div qr = (let (q, r) = qr in q + of_bool (r ≠ 0))"

"adjust_div (q, r) = q + of_bool (r ≠ 0)"

qualified definition adjust_mod :: "num ⇒ int ⇒ int"
where
[simp]: "adjust_mod l r = (if r = 0 then 0 else numeral l - r)"

lemma minus_numeral_div_numeral [simp]:
"- numeral m div numeral n = - (adjust_div (divmod m n) :: int)"
proof -
have "int (fst (divmod m n)) = fst (divmod m n)"
by (simp only: fst_divmod divide_int_def) auto
then show ?thesis
qed

lemma minus_numeral_mod_numeral [simp]:
"- numeral m mod numeral n = adjust_mod n (snd (divmod m n) :: int)"
proof (cases "snd (divmod m n) = (0::int)")
case True
then show ?thesis
next
case False
then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) ≠ (0::int)"
by (simp only: snd_divmod modulo_int_def) auto
then show ?thesis
qed

lemma numeral_div_minus_numeral [simp]:
"numeral m div - numeral n = - (adjust_div (divmod m n) :: int)"
proof -
have "int (fst (divmod m n)) = fst (divmod m n)"
by (simp only: fst_divmod divide_int_def) auto
then show ?thesis
qed

lemma numeral_mod_minus_numeral [simp]:
"numeral m mod - numeral n = - adjust_mod n (snd (divmod m n) :: int)"
proof (cases "snd (divmod m n) = (0::int)")
case True
then show ?thesis
next
case False
then have "int (snd (divmod m n)) = snd (divmod m n)" if "snd (divmod m n) ≠ (0::int)"
by (simp only: snd_divmod modulo_int_def) auto
then show ?thesis
qed

lemma minus_one_div_numeral [simp]:
"- 1 div numeral n = - (adjust_div (divmod Num.One n) :: int)"
using minus_numeral_div_numeral [of Num.One n] by simp

lemma minus_one_mod_numeral [simp]:
"- 1 mod numeral n = adjust_mod n (snd (divmod Num.One n) :: int)"
using minus_numeral_mod_numeral [of Num.One n] by simp

lemma one_div_minus_numeral [simp]:
"1 div - numeral n = - (adjust_div (divmod Num.One n) :: int)"
using numeral_div_minus_numeral [of Num.One n] by simp

lemma one_mod_minus_numeral [simp]:
"1 mod - numeral n = - adjust_mod n (snd (divmod Num.One n) :: int)"
using numeral_mod_minus_numeral [of Num.One n] by simp

lemma [code]:
fixes k :: int
shows
"k div 0 = 0"
"k mod 0 = k"
"0 div k = 0"
"0 mod k = 0"
"k div Int.Pos Num.One = k"
"k mod Int.Pos Num.One = 0"
"k div Int.Neg Num.One = - k"
"k mod Int.Neg Num.One = 0"
"Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
"Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
"Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)"
"Int.Neg m mod Int.Pos n = adjust_mod n (snd (divmod m n) :: int)"
"Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
"Int.Pos m mod Int.Neg n = - adjust_mod n (snd (divmod m n) :: int)"
"Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
"Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
by simp_all

end

lemma divmod_BitM_2_eq [simp]:
‹divmod (Num.BitM m) (Num.Bit0 Num.One) = (numeral m - 1, (1 :: int))›
by (cases m) simp_all

subsubsection ‹Computation by simplification›

lemma euclidean_size_nat_less_eq_iff:
‹euclidean_size m ≤ euclidean_size n ⟷ m ≤ n› for m n :: nat
by simp

lemma euclidean_size_int_less_eq_iff:
‹euclidean_size k ≤ euclidean_size l ⟷ ¦k¦ ≤ ¦l¦› for k l :: int
by auto

simproc_setup numeral_divmod
("0 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
"0 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
"0 div - 1 :: int" | "0 mod - 1 :: int" |
"0 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "0 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
"0 div - numeral b :: int" | "0 mod - numeral b :: int" |
"1 div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
"1 div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
"1 div - 1 :: int" | "1 mod - 1 :: int" |
"1 div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "1 mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
"1 div - numeral b :: int" |"1 mod - numeral b :: int" |
"- 1 div 0 :: int" | "- 1 mod 0 :: int" | "- 1 div 1 :: int" | "- 1 mod 1 :: int" |
"- 1 div - 1 :: int" | "- 1 mod - 1 :: int" | "- 1 div numeral b :: int" | "- 1 mod numeral b :: int" |
"- 1 div - numeral b :: int" | "- 1 mod - numeral b :: int" |
"numeral a div 0 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 0 :: 'a :: unique_euclidean_semiring_with_nat_division" |
"numeral a div 1 :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod 1 :: 'a :: unique_euclidean_semiring_with_nat_division" |
"numeral a div - 1 :: int" | "numeral a mod - 1 :: int" |
"numeral a div numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" | "numeral a mod numeral b :: 'a :: unique_euclidean_semiring_with_nat_division" |
"numeral a div - numeral b :: int" | "numeral a mod - numeral b :: int" |
"- numeral a div 0 :: int" | "- numeral a mod 0 :: int" |
"- numeral a div 1 :: int" | "- numeral a mod 1 :: int" |
"- numeral a div - 1 :: int" | "- numeral a mod - 1 :: int" |
"- numeral a div numeral b :: int" | "- numeral a mod numeral b :: int" |
"- numeral a div - numeral b :: int" | "- numeral a mod - numeral b :: int") = ‹
let
val if_cong = the (Code.get_case_cong \<^theory> \<^const_name>‹If›);
fun successful_rewrite ctxt ct =
let
val thm = Simplifier.rewrite ctxt ct
in if Thm.is_reflexive thm then NONE else SOME thm end;
val simps = @{thms div_0 mod_0 div_by_0 mod_by_0 div_by_1 mod_by_1
one_div_numeral one_mod_numeral minus_one_div_numeral minus_one_mod_numeral
one_div_minus_numeral one_mod_minus_numeral
numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
numeral_div_minus_numeral numeral_mod_minus_numeral
numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
divmod_cancel divmod_steps divmod_step_def fst_conv snd_conv numeral_One
minus_minus numeral_times_numeral mult_zero_right mult_1_right
euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
@ [@{lemma "0 = 0 ⟷ True" by simp}];
val simpset =
HOL_ss |> Simplifier.simpset_map \<^context>
in K (fn ctxt => successful_rewrite (Simplifier.put_simpset simpset ctxt)) end
› ― ‹
There is space for improvement here: the calculation itself
could be carried out outside the logic, and a generic simproc
(simplifier setup) for generic calculation would be helpful.
›

subsection ‹Computing congruences modulo ‹2 ^ q››

context unique_euclidean_semiring_with_nat_division
begin

lemma cong_exp_iff_simps:
"numeral n mod numeral Num.One = 0
⟷ True"
"numeral (Num.Bit0 n) mod numeral (Num.Bit0 q) = 0
⟷ numeral n mod numeral q = 0"
"numeral (Num.Bit1 n) mod numeral (Num.Bit0 q) = 0
⟷ False"
"numeral m mod numeral Num.One = (numeral n mod numeral Num.One)
⟷ True"
"numeral Num.One mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
⟷ True"
"numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
⟷ False"
"numeral Num.One mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
⟷ (numeral n mod numeral q) = 0"
"numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
⟷ False"
"numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
⟷ numeral m mod numeral q = (numeral n mod numeral q)"
"numeral (Num.Bit0 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
⟷ False"
"numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral Num.One mod numeral (Num.Bit0 q))
⟷ (numeral m mod numeral q) = 0"
"numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit0 n) mod numeral (Num.Bit0 q))
⟷ False"
"numeral (Num.Bit1 m) mod numeral (Num.Bit0 q) = (numeral (Num.Bit1 n) mod numeral (Num.Bit0 q))
⟷ numeral m mod numeral q = (numeral n mod numeral q)"
by (auto simp add: case_prod_beta dest: arg_cong [of _ _ even])

end

code_identifier
code_module Parity ⇀ (SML) Arith and (OCaml) Arith and (Haskell) Arith

lemmas even_of_nat = even_of_nat_iff

end
```