# Theory Bit_Operations

```(*  Author:  Florian Haftmann, TUM
*)

section ‹Bit operations in suitable algebraic structures›

theory Bit_Operations
imports Presburger Groups_List
begin

subsection ‹Abstract bit structures›

class semiring_bits = semiring_parity +
assumes bits_induct [case_names stable rec]:
‹(⋀a. a div 2 = a ⟹ P a)
⟹ (⋀a b. P a ⟹ (of_bool b + 2 * a) div 2 = a ⟹ P (of_bool b + 2 * a))
⟹ P a›
assumes bits_div_0 [simp]: ‹0 div a = 0›
and bits_div_by_1 [simp]: ‹a div 1 = a›
and bits_mod_div_trivial [simp]: ‹a mod b div b = 0›
and even_succ_div_2 [simp]: ‹even a ⟹ (1 + a) div 2 = a div 2›
and even_mask_div_iff: ‹even ((2 ^ m - 1) div 2 ^ n) ⟷ 2 ^ n = 0 ∨ m ≤ n›
and exp_div_exp_eq: ‹2 ^ m div 2 ^ n = of_bool (2 ^ m ≠ 0 ∧ m ≥ n) * 2 ^ (m - n)›
and div_exp_eq: ‹a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)›
and mod_exp_eq: ‹a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n›
and mult_exp_mod_exp_eq: ‹m ≤ n ⟹ (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m›
and div_exp_mod_exp_eq: ‹a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n›
and even_mult_exp_div_exp_iff: ‹even (a * 2 ^ m div 2 ^ n) ⟷ m > n ∨ 2 ^ n = 0 ∨ (m ≤ n ∧ even (a div 2 ^ (n - m)))›
fixes bit :: ‹'a ⇒ nat ⇒ bool›
assumes bit_iff_odd: ‹bit a n ⟷ odd (a div 2 ^ n)›
begin

text ‹
Having \<^const>‹bit› as definitional class operation
takes into account that specific instances can be implemented
differently wrt. code generation.
›

lemma bits_div_by_0 [simp]:
‹a div 0 = 0›
by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero)

lemma bits_1_div_2 [simp]:
‹1 div 2 = 0›
using even_succ_div_2 [of 0] by simp

lemma bits_1_div_exp [simp]:
‹1 div 2 ^ n = of_bool (n = 0)›
using div_exp_eq [of 1 1] by (cases n) simp_all

lemma even_succ_div_exp [simp]:
‹(1 + a) div 2 ^ n = a div 2 ^ n› if ‹even a› and ‹n > 0›
proof (cases n)
case 0
with that show ?thesis
by simp
next
case (Suc n)
with ‹even a› have ‹(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n›
proof (induction n)
case 0
then show ?case
by simp
next
case (Suc n)
then show ?case
using div_exp_eq [of _ 1 ‹Suc n›, symmetric]
by simp
qed
with Suc show ?thesis
by simp
qed

lemma even_succ_mod_exp [simp]:
‹(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)› if ‹even a› and ‹n > 0›
using div_mult_mod_eq [of ‹1 + a› ‹2 ^ n›] that
apply simp

lemma bits_mod_by_1 [simp]:
‹a mod 1 = 0›
using div_mult_mod_eq [of a 1] by simp

lemma bits_mod_0 [simp]:
‹0 mod a = 0›
using div_mult_mod_eq [of 0 a] by simp

lemma bits_one_mod_two_eq_one [simp]:
‹1 mod 2 = 1›

lemma bit_0:
‹bit a 0 ⟷ odd a›

lemma bit_Suc:
‹bit a (Suc n) ⟷ bit (a div 2) n›
using div_exp_eq [of a 1 n] by (simp add: bit_iff_odd)

lemma bit_rec:
‹bit a n ⟷ (if n = 0 then odd a else bit (a div 2) (n - 1))›
by (cases n) (simp_all add: bit_Suc bit_0)

lemma bit_0_eq [simp]:
‹bit 0 = bot›

context
fixes a
assumes stable: ‹a div 2 = a›
begin

‹a + a mod 2 = 0›
proof -
have ‹a div 2 * 2 + a mod 2 = a›
by (fact div_mult_mod_eq)
then have ‹a * 2 + a mod 2 = a›
then show ?thesis
qed

lemma stable_imp_bit_iff_odd:
‹bit a n ⟷ odd a›
by (induction n) (simp_all add: stable bit_Suc bit_0)

end

lemma bit_iff_idd_imp_stable:
‹a div 2 = a› if ‹⋀n. bit a n ⟷ odd a›
using that proof (induction a rule: bits_induct)
case (stable a)
then show ?case
by simp
next
case (rec a b)
from rec.prems [of 1] have [simp]: ‹b = odd a›
by (simp add: rec.hyps bit_Suc bit_0)
from rec.hyps have hyp: ‹(of_bool (odd a) + 2 * a) div 2 = a›
by simp
have ‹bit a n ⟷ odd a› for n
using rec.prems [of ‹Suc n›] by (simp add: hyp bit_Suc)
then have ‹a div 2 = a›
by (rule rec.IH)
then have ‹of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)›
also have ‹… = a›
using mult_div_mod_eq [of 2 a]
finally show ?case
using ‹a div 2 = a› by (simp add: hyp)
qed

lemma exp_eq_0_imp_not_bit:
‹¬ bit a n› if ‹2 ^ n = 0›
using that by (simp add: bit_iff_odd)

definition
possible_bit :: "'a itself ⇒ nat ⇒ bool"
where
"possible_bit tyrep n = (2 ^ n ≠ (0 :: 'a))"

lemma possible_bit_0[simp]:
"possible_bit ty 0"

lemma fold_possible_bit:
"2 ^ n = (0 :: 'a) ⟷ ¬ possible_bit TYPE('a) n"

lemmas impossible_bit = exp_eq_0_imp_not_bit[simplified fold_possible_bit]

lemma bit_imp_possible_bit:
"bit a n ⟹ possible_bit TYPE('a) n"
by (rule ccontr) (simp add: impossible_bit)

lemma possible_bit_less_imp:
"possible_bit tyrep i ⟹ j ≤ i ⟹ possible_bit tyrep j"
using power_add[of "2 :: 'a" j "i - j"]
by (clarsimp simp: possible_bit_def eq_commute[where a=0])

lemma possible_bit_min[simp]:
"possible_bit tyrep (min i j) ⟷ possible_bit tyrep i ∨ possible_bit tyrep j"
by (auto simp: min_def elim: possible_bit_less_imp)

lemma bit_eqI:
‹a = b› if ‹⋀n. possible_bit TYPE('a) n ⟹ bit a n ⟷ bit b n›
proof -
have ‹bit a n ⟷ bit b n› for n
proof (cases ‹2 ^ n = 0›)
case True
then show ?thesis
next
case False
then show ?thesis
by (rule that[unfolded possible_bit_def])
qed
then show ?thesis proof (induction a arbitrary: b rule: bits_induct)
case (stable a)
from stable(2) [of 0] have **: ‹even b ⟷ even a›
have ‹b div 2 = b›
proof (rule bit_iff_idd_imp_stable)
fix n
from stable have *: ‹bit b n ⟷ bit a n›
by simp
also have ‹bit a n ⟷ odd a›
using stable by (simp add: stable_imp_bit_iff_odd)
finally show ‹bit b n ⟷ odd b›
qed
from ** have ‹a mod 2 = b mod 2›
then have ‹a mod 2 + (a + b) = b mod 2 + (a + b)›
by simp
then have ‹a + a mod 2 + b = b + b mod 2 + a›
with ‹a div 2 = a› ‹b div 2 = b› show ?case
next
case (rec a p)
from rec.prems [of 0] have [simp]: ‹p = odd b›
from rec.hyps have ‹bit a n ⟷ bit (b div 2) n› for n
using rec.prems [of ‹Suc n›] by (simp add: bit_Suc)
then have ‹a = b div 2›
by (rule rec.IH)
then have ‹2 * a = 2 * (b div 2)›
by simp
then have ‹b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)›
by simp
also have ‹… = b›
by (fact mod_mult_div_eq)
finally show ?case
qed
qed

lemma bit_eq_iff:
‹a = b ⟷ (∀n. possible_bit TYPE('a) n ⟶ bit a n ⟷ bit b n)›
by (auto intro: bit_eqI)

named_theorems bit_simps ‹Simplification rules for \<^const>‹bit››

lemma bit_exp_iff [bit_simps]:
‹bit (2 ^ m) n ⟷ possible_bit TYPE('a) n ∧ m = n›
by (auto simp add: bit_iff_odd exp_div_exp_eq possible_bit_def)

lemma bit_1_iff [bit_simps]:
‹bit 1 n ⟷ n = 0›
using bit_exp_iff [of 0 n]
by auto

lemma bit_2_iff [bit_simps]:
‹bit 2 n ⟷ possible_bit TYPE('a) 1 ∧ n = 1›
using bit_exp_iff [of 1 n] by auto

lemma even_bit_succ_iff:
‹bit (1 + a) n ⟷ bit a n ∨ n = 0› if ‹even a›
using that by (cases ‹n = 0›) (simp_all add: bit_iff_odd)

lemma bit_double_iff [bit_simps]:
‹bit (2 * a) n ⟷ bit a (n - 1) ∧ n ≠ 0 ∧ possible_bit TYPE('a) n›
using even_mult_exp_div_exp_iff [of a 1 n]
by (cases n, auto simp add: bit_iff_odd ac_simps possible_bit_def)

lemma odd_bit_iff_bit_pred:
‹bit a n ⟷ bit (a - 1) n ∨ n = 0› if ‹odd a›
proof -
from ‹odd a› obtain b where ‹a = 2 * b + 1› ..
moreover have ‹bit (2 * b) n ∨ n = 0 ⟷ bit (1 + 2 * b) n›
using even_bit_succ_iff by simp
ultimately show ?thesis by (simp add: ac_simps)
qed

lemma bit_eq_rec:
‹a = b ⟷ (even a ⟷ even b) ∧ a div 2 = b div 2› (is ‹?P = ?Q›)
proof
assume ?P
then show ?Q
by simp
next
assume ?Q
then have ‹even a ⟷ even b› and ‹a div 2 = b div 2›
by simp_all
show ?P
proof (rule bit_eqI)
fix n
show ‹bit a n ⟷ bit b n›
proof (cases n)
case 0
with ‹even a ⟷ even b› show ?thesis
next
case (Suc n)
moreover from ‹a div 2 = b div 2› have ‹bit (a div 2) n = bit (b div 2) n›
by simp
ultimately show ?thesis
qed
qed
qed

lemma bit_mod_2_iff [simp]:
‹bit (a mod 2) n ⟷ n = 0 ∧ odd a›
by (cases a rule: parity_cases) (simp_all add: bit_iff_odd)

‹bit (2 ^ m - 1) n ⟷ possible_bit TYPE('a) n ∧ n < m›

‹2 ^ m ≠ 0› and ‹2 ^ n ≠ 0› if ‹2 ^ (m + n) ≠ 0›
proof -
have ‹¬ (2 ^ m = 0 ∨ 2 ^ n = 0)›
proof (rule notI)
assume ‹2 ^ m = 0 ∨ 2 ^ n = 0›
then have ‹2 ^ (m + n) = 0›
with that show False ..
qed
then show ‹2 ^ m ≠ 0› and ‹2 ^ n ≠ 0›
by simp_all
qed

‹bit (a + b) n ⟷ bit a n ∨ bit b n›
if ‹⋀n. ¬ bit a n ∨ ¬ bit b n›
proof (cases ‹2 ^ n = 0›)
case True
then show ?thesis
next
case False
with that show ?thesis proof (induction n arbitrary: a b)
case 0
from "0.prems"(1) [of 0] show ?case
next
case (Suc n)
from Suc.prems(1) [of 0] have even: ‹even a ∨ even b›
have bit: ‹¬ bit (a div 2) n ∨ ¬ bit (b div 2) n› for n
using Suc.prems(1) [of ‹Suc n›] by (simp add: bit_Suc)
from Suc.prems(2) have ‹2 * 2 ^ n ≠ 0› ‹2 ^ n ≠ 0›
have ‹a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)›
using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
also have ‹… = of_bool (odd a ∨ odd b) + 2 * (a div 2 + b div 2)›
using even by (auto simp add: algebra_simps mod2_eq_if)
finally have ‹bit ((a + b) div 2) n ⟷ bit (a div 2 + b div 2) n›
using ‹2 * 2 ^ n ≠ 0› by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
also have ‹… ⟷ bit (a div 2) n ∨ bit (b div 2) n›
using bit ‹2 ^ n ≠ 0› by (rule Suc.IH)
finally show ?case
qed
qed

lemma
exp_add_not_zero_imp_left: ‹2 ^ m ≠ 0›
and exp_add_not_zero_imp_right: ‹2 ^ n ≠ 0›
if ‹2 ^ (m + n) ≠ 0›
proof -
have ‹¬ (2 ^ m = 0 ∨ 2 ^ n = 0)›
proof (rule notI)
assume ‹2 ^ m = 0 ∨ 2 ^ n = 0›
then have ‹2 ^ (m + n) = 0›
with that show False ..
qed
then show ‹2 ^ m ≠ 0› and ‹2 ^ n ≠ 0›
by simp_all
qed

lemma exp_not_zero_imp_exp_diff_not_zero:
‹2 ^ (n - m) ≠ 0› if ‹2 ^ n ≠ 0›
proof (cases ‹m ≤ n›)
case True
moreover define q where ‹q = n - m›
ultimately have ‹n = m + q›
by simp
with that show ?thesis
next
case False
with that show ?thesis
by simp
qed

end

lemma nat_bit_induct [case_names zero even odd]:
"P n" if zero: "P 0"
and even: "⋀n. P n ⟹ n > 0 ⟹ P (2 * n)"
and odd: "⋀n. P n ⟹ P (Suc (2 * n))"
proof (induction n rule: less_induct)
case (less n)
show "P n"
proof (cases "n = 0")
case True with zero show ?thesis by simp
next
case False
with less have hyp: "P (n div 2)" by simp
show ?thesis
proof (cases "even n")
case True
then have "n ≠ 1"
by auto
with ‹n ≠ 0› have "n div 2 > 0"
by simp
with ‹even n› hyp even [of "n div 2"] show ?thesis
by simp
next
case False
with hyp odd [of "n div 2"] show ?thesis
by simp
qed
qed
qed

instantiation nat :: semiring_bits
begin

definition bit_nat :: ‹nat ⇒ nat ⇒ bool›
where ‹bit_nat m n ⟷ odd (m div 2 ^ n)›

instance
proof
show ‹P n› if stable: ‹⋀n. n div 2 = n ⟹ P n›
and rec: ‹⋀n b. P n ⟹ (of_bool b + 2 * n) div 2 = n ⟹ P (of_bool b + 2 * n)›
for P and n :: nat
proof (induction n rule: nat_bit_induct)
case zero
from stable [of 0] show ?case
by simp
next
case (even n)
with rec [of n False] show ?case
by simp
next
case (odd n)
with rec [of n True] show ?case
by simp
qed
show ‹q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n›
for q m n :: nat
apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes)
done
show ‹(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m› if ‹m ≤ n›
for q m n :: nat
using that
done
show ‹even ((2 ^ m - (1::nat)) div 2 ^ n) ⟷ 2 ^ n = (0::nat) ∨ m ≤ n›
for m n :: nat
using even_mask_div_iff' [where ?'a = nat, of m n] by simp
show ‹even (q * 2 ^ m div 2 ^ n) ⟷ n < m ∨ (2::nat) ^ n = 0 ∨ m ≤ n ∧ even (q div 2 ^ (n - m))›
for m n q r :: nat
apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc)
done

end

lemma possible_bit_nat[simp]:
"possible_bit TYPE(nat) n"

lemma not_bit_Suc_0_Suc [simp]:
‹¬ bit (Suc 0) (Suc n)›

lemma not_bit_Suc_0_numeral [simp]:
‹¬ bit (Suc 0) (numeral n)›

lemma int_bit_induct [case_names zero minus even odd]:
"P k" if zero_int: "P 0"
and minus_int: "P (- 1)"
and even_int: "⋀k. P k ⟹ k ≠ 0 ⟹ P (k * 2)"
and odd_int: "⋀k. P k ⟹ k ≠ - 1 ⟹ P (1 + (k * 2))" for k :: int
proof (cases "k ≥ 0")
case True
define n where "n = nat k"
with True have "k = int n"
by simp
then show "P k"
proof (induction n arbitrary: k rule: nat_bit_induct)
case zero
then show ?case
next
case (even n)
have "P (int n * 2)"
by (rule even_int) (use even in simp_all)
with even show ?case
next
case (odd n)
have "P (1 + (int n * 2))"
by (rule odd_int) (use odd in simp_all)
with odd show ?case
qed
next
case False
define n where "n = nat (- k - 1)"
with False have "k = - int n - 1"
by simp
then show "P k"
proof (induction n arbitrary: k rule: nat_bit_induct)
case zero
then show ?case
next
case (even n)
have "P (1 + (- int (Suc n) * 2))"
by (rule odd_int) (use even in ‹simp_all add: algebra_simps›)
also have "… = - int (2 * n) - 1"
finally show ?case
using even.prems by simp
next
case (odd n)
have "P (- int (Suc n) * 2)"
by (rule even_int) (use odd in ‹simp_all add: algebra_simps›)
also have "… = - int (Suc (2 * n)) - 1"
finally show ?case
using odd.prems by simp
qed
qed

context semiring_bits
begin

lemma bit_of_bool_iff [bit_simps]:
‹bit (of_bool b) n ⟷ b ∧ n = 0›

lemma bit_of_nat_iff [bit_simps]:
‹bit (of_nat m) n ⟷ possible_bit TYPE('a) n ∧ bit m n›
proof (cases ‹(2::'a) ^ n = 0›)
case True
then show ?thesis
next
case False
then have ‹bit (of_nat m) n ⟷ bit m n›
proof (induction m arbitrary: n rule: nat_bit_induct)
case zero
then show ?case
by simp
next
case (even m)
then show ?case
by (cases n)
(auto simp add: bit_double_iff Bit_Operations.bit_double_iff possible_bit_def bit_0 dest: mult_not_zero)
next
case (odd m)
then show ?case
by (cases n)
(auto simp add: bit_double_iff even_bit_succ_iff possible_bit_def
Bit_Operations.bit_Suc Bit_Operations.bit_0 dest: mult_not_zero)
qed
with False show ?thesis
qed

end

instantiation int :: semiring_bits
begin

definition bit_int :: ‹int ⇒ nat ⇒ bool›
where ‹bit_int k n ⟷ odd (k div 2 ^ n)›

instance
proof
show ‹P k› if stable: ‹⋀k. k div 2 = k ⟹ P k›
and rec: ‹⋀k b. P k ⟹ (of_bool b + 2 * k) div 2 = k ⟹ P (of_bool b + 2 * k)›
for P and k :: int
proof (induction k rule: int_bit_induct)
case zero
from stable [of 0] show ?case
by simp
next
case minus
from stable [of ‹- 1›] show ?case
by simp
next
case (even k)
with rec [of k False] show ?case
next
case (odd k)
with rec [of k True] show ?case
qed
show ‹(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m ≠ 0 ∧ n ≤ m) * 2 ^ (m - n)›
for m n :: nat
proof (cases ‹m < n›)
case True
then have ‹n = m + (n - m)›
by simp
then have ‹(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))›
by simp
also have ‹… = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))›
also have ‹… = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)›
finally show ?thesis using ‹m < n› by simp
next
case False
then show ?thesis
qed
show ‹k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n›
for m n :: nat and k :: int
using mod_exp_eq [of ‹nat k› m n]
apply (simp only: flip: mult.left_commute [of ‹2 ^ m›])
apply (subst zmod_zmult2_eq) apply simp_all
done
show ‹(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m›
if ‹m ≤ n› for m n :: nat and k :: int
using that
done
show ‹even ((2 ^ m - (1::int)) div 2 ^ n) ⟷ 2 ^ n = (0::int) ∨ m ≤ n›
for m n :: nat
using even_mask_div_iff' [where ?'a = int, of m n] by simp
show ‹even (k * 2 ^ m div 2 ^ n) ⟷ n < m ∨ (2::int) ^ n = 0 ∨ m ≤ n ∧ even (k div 2 ^ (n - m))›
for m n :: nat and k l :: int
apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2))
done

end

lemma possible_bit_int[simp]:
"possible_bit TYPE(int) n"

lemma bit_not_int_iff':
‹bit (- k - 1) n ⟷ ¬ bit k n›
for k :: int
proof (induction n arbitrary: k)
case 0
show ?case
next
case (Suc n)
have ‹- k - 1 = - (k + 2) + 1›
by simp
also have ‹(- (k + 2) + 1) div 2 = - (k div 2) - 1›
proof (cases ‹even k›)
case True
then have ‹- k div 2 = - (k div 2)›
by rule (simp flip: mult_minus_right)
with True show ?thesis
by simp
next
case False
have ‹4 = 2 * (2::int)›
by simp
also have ‹2 * 2 div 2 = (2::int)›
by (simp only: nonzero_mult_div_cancel_left)
finally have *: ‹4 div 2 = (2::int)› .
from False obtain l where k: ‹k = 2 * l + 1› ..
then have ‹- k - 2 = 2 * - (l + 2) + 1›
by simp
then have ‹(- k - 2) div 2 + 1 = - (k div 2) - 1›
with False show ?thesis
by simp
qed
finally have ‹(- k - 1) div 2 = - (k div 2) - 1› .
with Suc show ?case
qed

lemma bit_nat_iff [bit_simps]:
‹bit (nat k) n ⟷ k ≥ 0 ∧ bit k n›
proof (cases ‹k ≥ 0›)
case True
moreover define m where ‹m = nat k›
ultimately have ‹k = int m›
by simp
then show ?thesis
next
case False
then show ?thesis
by simp
qed

subsection ‹Bit operations›

class semiring_bit_operations = semiring_bits +
fixes "and" :: ‹'a ⇒ 'a ⇒ 'a›  (infixr ‹AND› 64)
and or :: ‹'a ⇒ 'a ⇒ 'a›  (infixr ‹OR› 59)
and xor :: ‹'a ⇒ 'a ⇒ 'a›  (infixr ‹XOR› 59)
and mask :: ‹nat ⇒ 'a›
and set_bit :: ‹nat ⇒ 'a ⇒ 'a›
and unset_bit :: ‹nat ⇒ 'a ⇒ 'a›
and flip_bit :: ‹nat ⇒ 'a ⇒ 'a›
and push_bit :: ‹nat ⇒ 'a ⇒ 'a›
and drop_bit :: ‹nat ⇒ 'a ⇒ 'a›
and take_bit :: ‹nat ⇒ 'a ⇒ 'a›
assumes bit_and_iff [bit_simps]: ‹bit (a AND b) n ⟷ bit a n ∧ bit b n›
and bit_or_iff [bit_simps]: ‹bit (a OR b) n ⟷ bit a n ∨ bit b n›
and bit_xor_iff [bit_simps]: ‹bit (a XOR b) n ⟷ bit a n ≠ bit b n›
and set_bit_eq_or: ‹set_bit n a = a OR push_bit n 1›
and bit_unset_bit_iff [bit_simps]: ‹bit (unset_bit m a) n ⟷ bit a n ∧ m ≠ n›
and flip_bit_eq_xor: ‹flip_bit n a = a XOR push_bit n 1›
and push_bit_eq_mult: ‹push_bit n a = a * 2 ^ n›
and drop_bit_eq_div: ‹drop_bit n a = a div 2 ^ n›
and take_bit_eq_mod: ‹take_bit n a = a mod 2 ^ n›
begin

text ‹
We want the bitwise operations to bind slightly weaker
than ‹+› and ‹-›.

Logically, \<^const>‹push_bit›,
\<^const>‹drop_bit› and \<^const>‹take_bit› are just aliases; having them
as separate operations makes proofs easier, otherwise proof automation
would fiddle with concrete expressions \<^term>‹2 ^ n› in a way obfuscating the basic
algebraic relationships between those operations.

For the sake of code generation operations
are specified as definitional class operations,
taking into account that specific instances of these can be implemented
differently wrt. code generation.
›

sublocale "and": semilattice ‹(AND)›
by standard (auto simp add: bit_eq_iff bit_and_iff)

sublocale or: semilattice_neutr ‹(OR)› 0
by standard (auto simp add: bit_eq_iff bit_or_iff)

sublocale xor: comm_monoid ‹(XOR)› 0
by standard (auto simp add: bit_eq_iff bit_xor_iff)

lemma even_and_iff:
‹even (a AND b) ⟷ even a ∨ even b›
using bit_and_iff [of a b 0] by (auto simp add: bit_0)

lemma even_or_iff:
‹even (a OR b) ⟷ even a ∧ even b›
using bit_or_iff [of a b 0] by (auto simp add: bit_0)

lemma even_xor_iff:
‹even (a XOR b) ⟷ (even a ⟷ even b)›
using bit_xor_iff [of a b 0] by (auto simp add: bit_0)

lemma zero_and_eq [simp]:
‹0 AND a = 0›

lemma and_zero_eq [simp]:
‹a AND 0 = 0›

lemma one_and_eq:
‹1 AND a = a mod 2›

lemma and_one_eq:
‹a AND 1 = a mod 2›
using one_and_eq [of a] by (simp add: ac_simps)

lemma one_or_eq:
‹1 OR a = a + of_bool (even a)›

lemma or_one_eq:
‹a OR 1 = a + of_bool (even a)›
using one_or_eq [of a] by (simp add: ac_simps)

lemma one_xor_eq:
‹1 XOR a = a + of_bool (even a) - of_bool (odd a)›
(auto simp add: bit_1_iff odd_bit_iff_bit_pred bit_0 elim: oddE)

lemma xor_one_eq:
‹a XOR 1 = a + of_bool (even a) - of_bool (odd a)›
using one_xor_eq [of a] by (simp add: ac_simps)

lemma xor_self_eq [simp]:
‹a XOR a = 0›
by (rule bit_eqI) (simp add: bit_simps)

lemma bit_iff_odd_drop_bit:
‹bit a n ⟷ odd (drop_bit n a)›

lemma even_drop_bit_iff_not_bit:
‹even (drop_bit n a) ⟷ ¬ bit a n›

lemma div_push_bit_of_1_eq_drop_bit:
‹a div push_bit n 1 = drop_bit n a›

lemma bits_ident:
"push_bit n (drop_bit n a) + take_bit n a = a"
using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)

lemma push_bit_push_bit [simp]:
"push_bit m (push_bit n a) = push_bit (m + n) a"

lemma push_bit_0_id [simp]:
"push_bit 0 = id"

lemma push_bit_of_0 [simp]:
"push_bit n 0 = 0"

lemma push_bit_of_1 [simp]:
"push_bit n 1 = 2 ^ n"

lemma push_bit_Suc [simp]:
"push_bit (Suc n) a = push_bit n (a * 2)"

lemma push_bit_double:
"push_bit n (a * 2) = push_bit n a * 2"

"push_bit n (a + b) = push_bit n a + push_bit n b"

lemma push_bit_numeral [simp]:
‹push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))›

lemma take_bit_0 [simp]:
"take_bit 0 a = 0"

lemma take_bit_Suc:
‹take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2›
proof -
have ‹take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)›
using even_succ_mod_exp [of ‹2 * (a div 2)› ‹Suc n›]
mult_exp_mod_exp_eq [of 1 ‹Suc n› ‹a div 2›]
by (auto simp add: take_bit_eq_mod ac_simps)
then show ?thesis
using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd)
qed

lemma take_bit_rec:
‹take_bit n a = (if n = 0 then 0 else take_bit (n - 1) (a div 2) * 2 + a mod 2)›
by (cases n) (simp_all add: take_bit_Suc)

lemma take_bit_Suc_0 [simp]:
‹take_bit (Suc 0) a = a mod 2›

lemma take_bit_of_0 [simp]:
"take_bit n 0 = 0"

lemma take_bit_of_1 [simp]:
"take_bit n 1 = of_bool (n > 0)"
by (cases n) (simp_all add: take_bit_Suc)

lemma drop_bit_of_0 [simp]:
"drop_bit n 0 = 0"

lemma drop_bit_of_1 [simp]:
"drop_bit n 1 = of_bool (n = 0)"

lemma drop_bit_0 [simp]:
"drop_bit 0 = id"

lemma drop_bit_Suc:
"drop_bit (Suc n) a = drop_bit n (a div 2)"
using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div)

lemma drop_bit_rec:
"drop_bit n a = (if n = 0 then a else drop_bit (n - 1) (a div 2))"
by (cases n) (simp_all add: drop_bit_Suc)

lemma drop_bit_half:
"drop_bit n (a div 2) = drop_bit n a div 2"
by (induction n arbitrary: a) (simp_all add: drop_bit_Suc)

lemma drop_bit_of_bool [simp]:
"drop_bit n (of_bool b) = of_bool (n = 0 ∧ b)"
by (cases n) simp_all

lemma even_take_bit_eq [simp]:
‹even (take_bit n a) ⟷ n = 0 ∨ even a›
by (simp add: take_bit_rec [of n a])

lemma take_bit_take_bit [simp]:
"take_bit m (take_bit n a) = take_bit (min m n) a"
by (simp add: take_bit_eq_mod mod_exp_eq ac_simps)

lemma drop_bit_drop_bit [simp]:
"drop_bit m (drop_bit n a) = drop_bit (m + n) a"

lemma push_bit_take_bit:
"push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)"
using mult_exp_mod_exp_eq [of m ‹m + n› a] apply (simp add: ac_simps power_add)
done

lemma take_bit_push_bit:
"take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)"
proof (cases "m ≤ n")
case True
then show ?thesis
using mult_exp_mod_exp_eq [of m m ‹a * 2 ^ n› for n]
done
next
case False
then show ?thesis
using push_bit_take_bit [of n "m - n" a]
by simp
qed

lemma take_bit_drop_bit:
"take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)"
by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq)

lemma drop_bit_take_bit:
"drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)"
proof (cases "m ≤ n")
case True
then show ?thesis
using take_bit_drop_bit [of "n - m" m a] by simp
next
case False
then obtain q where ‹m = n + q›
then have ‹drop_bit m (take_bit n a) = 0›
using div_exp_eq [of ‹a mod 2 ^ n› n q]
with False show ?thesis
by simp
qed

lemma even_push_bit_iff [simp]:
‹even (push_bit n a) ⟷ n ≠ 0 ∨ even a›

lemma bit_push_bit_iff [bit_simps]:
‹bit (push_bit m a) n ⟷ m ≤ n ∧ possible_bit TYPE('a) n ∧ bit a (n - m)›
by (auto simp add: bit_iff_odd push_bit_eq_mult even_mult_exp_div_exp_iff possible_bit_def)

lemma bit_drop_bit_eq [bit_simps]:
‹bit (drop_bit n a) = bit a ∘ (+) n›
by (simp add: bit_iff_odd fun_eq_iff ac_simps flip: drop_bit_eq_div)

lemma bit_take_bit_iff [bit_simps]:
‹bit (take_bit m a) n ⟷ n < m ∧ bit a n›
by (simp add: bit_iff_odd drop_bit_take_bit not_le flip: drop_bit_eq_div)

lemma stable_imp_drop_bit_eq:
‹drop_bit n a = a›
if ‹a div 2 = a›
by (induction n) (simp_all add: that drop_bit_Suc)

lemma stable_imp_take_bit_eq:
‹take_bit n a = (if even a then 0 else 2 ^ n - 1)›
if ‹a div 2 = a›
proof (rule bit_eqI[unfolded possible_bit_def])
fix m
assume ‹2 ^ m ≠ 0›
with that show ‹bit (take_bit n a) m ⟷ bit (if even a then 0 else 2 ^ n - 1) m›
qed

lemma exp_dvdE:
assumes ‹2 ^ n dvd a›
obtains b where ‹a = push_bit n b›
proof -
from assms obtain b where ‹a = 2 ^ n * b› ..
then have ‹a = push_bit n b›
with that show thesis .
qed

lemma take_bit_eq_0_iff:
‹take_bit n a = 0 ⟷ 2 ^ n dvd a› (is ‹?P ⟷ ?Q›)
proof
assume ?P
then show ?Q
next
assume ?Q
then obtain b where ‹a = push_bit n b›
by (rule exp_dvdE)
then show ?P
qed

lemma take_bit_tightened:
‹take_bit m a = take_bit m b› if ‹take_bit n a = take_bit n b› and ‹m ≤ n›
proof -
from that have ‹take_bit m (take_bit n a) = take_bit m (take_bit n b)›
by simp
then have ‹take_bit (min m n) a = take_bit (min m n) b›
by simp
with that show ?thesis
qed

lemma take_bit_eq_self_iff_drop_bit_eq_0:
‹take_bit n a = a ⟷ drop_bit n a = 0› (is ‹?P ⟷ ?Q›)
proof
assume ?P
show ?Q
proof (rule bit_eqI)
fix m
from ‹?P› have ‹a = take_bit n a› ..
also have ‹¬ bit (take_bit n a) (n + m)›
unfolding bit_simps
finally show ‹bit (drop_bit n a) m ⟷ bit 0 m›
qed
next
assume ?Q
show ?P
proof (rule bit_eqI)
fix m
from ‹?Q› have ‹¬ bit (drop_bit n a) (m - n)›
by simp
then have ‹ ¬ bit a (n + (m - n))›
then show ‹bit (take_bit n a) m ⟷ bit a m›
by (cases ‹m < n›) (auto simp add: bit_simps)
qed
qed

lemma drop_bit_exp_eq:
‹drop_bit m (2 ^ n) = of_bool (m ≤ n ∧ possible_bit TYPE('a) n) * 2 ^ (n - m)›
by (auto simp add: bit_eq_iff bit_simps)

lemma take_bit_and [simp]:
‹take_bit n (a AND b) = take_bit n a AND take_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma take_bit_or [simp]:
‹take_bit n (a OR b) = take_bit n a OR take_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma take_bit_xor [simp]:
‹take_bit n (a XOR b) = take_bit n a XOR take_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma push_bit_and [simp]:
‹push_bit n (a AND b) = push_bit n a AND push_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma push_bit_or [simp]:
‹push_bit n (a OR b) = push_bit n a OR push_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma push_bit_xor [simp]:
‹push_bit n (a XOR b) = push_bit n a XOR push_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma drop_bit_and [simp]:
‹drop_bit n (a AND b) = drop_bit n a AND drop_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma drop_bit_or [simp]:
‹drop_bit n (a OR b) = drop_bit n a OR drop_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

lemma drop_bit_xor [simp]:
‹drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b›
by (auto simp add: bit_eq_iff bit_simps)

‹bit (mask m) n ⟷ possible_bit TYPE('a) n ∧ n < m›

‹even (mask n) ⟷ n = 0›

by (auto simp add: bit_eq_iff bit_simps)

by (auto simp add: bit_eq_iff bit_simps elim: possible_bit_less_imp)

by (rule bit_eqI) (simp add: bit_simps)

‹take_bit n a = a AND mask n›
by (auto simp add: bit_eq_iff bit_simps)

lemma or_eq_0_iff:
‹a OR b = 0 ⟷ a = 0 ∧ b = 0›
by (auto simp add: bit_eq_iff bit_or_iff)

‹a + b = a OR b› if ‹⋀n. ¬ bit a n ∨ ¬ bit b n›

lemma bit_iff_and_drop_bit_eq_1:
‹bit a n ⟷ drop_bit n a AND 1 = 1›
by (simp add: bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)

lemma bit_iff_and_push_bit_not_eq_0:
‹bit a n ⟷ a AND push_bit n 1 ≠ 0›
apply (cases ‹2 ^ n = 0›)
apply (simp_all add: bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit)
done

lemmas set_bit_def = set_bit_eq_or

lemma bit_set_bit_iff [bit_simps]:
‹bit (set_bit m a) n ⟷ bit a n ∨ (m = n ∧ possible_bit TYPE('a) n)›
by (auto simp add: set_bit_def bit_or_iff bit_exp_iff)

lemma even_set_bit_iff:
‹even (set_bit m a) ⟷ even a ∧ m ≠ 0›
using bit_set_bit_iff [of m a 0] by (auto simp add: bit_0)

lemma even_unset_bit_iff:
‹even (unset_bit m a) ⟷ even a ∨ m = 0›
using bit_unset_bit_iff [of m a 0] by (auto simp add: bit_0)

lemma and_exp_eq_0_iff_not_bit:
‹a AND 2 ^ n = 0 ⟷ ¬ bit a n› (is ‹?P ⟷ ?Q›)
using bit_imp_possible_bit[of a n]
by (auto simp add: bit_eq_iff bit_simps)

lemmas flip_bit_def = flip_bit_eq_xor

lemma bit_flip_bit_iff [bit_simps]:
‹bit (flip_bit m a) n ⟷ (m = n ⟷ ¬ bit a n) ∧ possible_bit TYPE('a) n›
by (auto simp add: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)

lemma even_flip_bit_iff:
‹even (flip_bit m a) ⟷ ¬ (even a ⟷ m = 0)›
using bit_flip_bit_iff [of m a 0] by (auto simp: possible_bit_def  bit_0)

lemma set_bit_0 [simp]:
‹set_bit 0 a = 1 + 2 * (a div 2)›
by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)

lemma bit_sum_mult_2_cases:
assumes a: "∀j. ¬ bit a (Suc j)"
shows "bit (a + 2 * b) n = (if n = 0 then odd a else bit (2 * b) n)"
proof -
have a_eq: "bit a i ⟷ i = 0 ∧ odd a" for i
by (cases i) (simp_all add: a bit_0)
show ?thesis
qed

lemma set_bit_Suc:
‹set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)›
by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
elim: possible_bit_less_imp)

lemma unset_bit_0 [simp]:
‹unset_bit 0 a = 2 * (a div 2)›
by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)

lemma unset_bit_Suc:
‹unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)›
by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
elim: possible_bit_less_imp)

lemma flip_bit_0 [simp]:
‹flip_bit 0 a = of_bool (even a) + 2 * (a div 2)›
by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)

lemma flip_bit_Suc:
‹flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)›
by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
elim: possible_bit_less_imp)

lemma flip_bit_eq_if:
‹flip_bit n a = (if bit a n then unset_bit else set_bit) n a›
by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)

lemma take_bit_set_bit_eq:
‹take_bit n (set_bit m a) = (if n ≤ m then take_bit n a else set_bit m (take_bit n a))›
by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff)

lemma take_bit_unset_bit_eq:
‹take_bit n (unset_bit m a) = (if n ≤ m then take_bit n a else unset_bit m (take_bit n a))›
by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff)

lemma take_bit_flip_bit_eq:
‹take_bit n (flip_bit m a) = (if n ≤ m then take_bit n a else flip_bit m (take_bit n a))›
by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)

lemma bit_1_0 [simp]:
‹bit 1 0›

lemma not_bit_1_Suc [simp]:
‹¬ bit 1 (Suc n)›

lemma push_bit_Suc_numeral [simp]:
‹push_bit (Suc n) (numeral k) = push_bit n (numeral (Num.Bit0 k))›

‹mask n = 0 ⟷ n = 0›

end

class ring_bit_operations = semiring_bit_operations + ring_parity +
fixes not :: ‹'a ⇒ 'a›  (‹NOT›)
assumes bit_not_iff_eq: ‹⋀n. bit (NOT a) n ⟷ 2 ^ n ≠ 0 ∧ ¬ bit a n›
assumes minus_eq_not_minus_1: ‹- a = NOT (a - 1)›
begin

lemmas bit_not_iff[bit_simps] = bit_not_iff_eq[unfolded fold_possible_bit]

text ‹
For the sake of code generation \<^const>‹not› is specified as
definitional class operation.  Note that \<^const>‹not› has no
sensible definition for unlimited but only positive bit strings
(type \<^typ>‹nat›).
›

lemma bits_minus_1_mod_2_eq [simp]:
‹(- 1) mod 2 = 1›

lemma not_eq_complement:
‹NOT a = - a - 1›
using minus_eq_not_minus_1 [of ‹a + 1›] by simp

lemma minus_eq_not_plus_1:
‹- a = NOT a + 1›
using not_eq_complement [of a] by simp

lemma bit_minus_iff [bit_simps]:
‹bit (- a) n ⟷ possible_bit TYPE('a) n ∧ ¬ bit (a - 1) n›

lemma even_not_iff [simp]:
‹even (NOT a) ⟷ odd a›
using bit_not_iff [of a 0] by (auto simp add: bit_0)

lemma bit_not_exp_iff [bit_simps]:
‹bit (NOT (2 ^ m)) n ⟷ possible_bit TYPE('a) n ∧ n ≠ m›
by (auto simp add: bit_not_iff bit_exp_iff)

lemma bit_minus_1_iff [simp]:
‹bit (- 1) n ⟷ possible_bit TYPE('a) n›

lemma bit_minus_exp_iff [bit_simps]:
‹bit (- (2 ^ m)) n ⟷ possible_bit TYPE('a) n ∧ n ≥ m›

lemma bit_minus_2_iff [simp]:
‹bit (- 2) n ⟷ possible_bit TYPE('a) n ∧ n > 0›

lemma not_one_eq [simp]:
‹NOT 1 = - 2›

sublocale "and": semilattice_neutr ‹(AND)› ‹- 1›
by standard (rule bit_eqI, simp add: bit_and_iff)

sublocale bit: abstract_boolean_algebra ‹(AND)› ‹(OR)› NOT 0 ‹- 1›
by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)

sublocale bit: abstract_boolean_algebra_sym_diff ‹(AND)› ‹(OR)› NOT 0 ‹- 1› ‹(XOR)›
apply standard
apply (rule bit_eqI)
done

lemma and_eq_not_not_or:
‹a AND b = NOT (NOT a OR NOT b)›
by simp

lemma or_eq_not_not_and:
‹a OR b = NOT (NOT a AND NOT b)›
by simp

‹NOT (a + b) = NOT a - b›

lemma not_diff_distrib:
‹NOT (a - b) = NOT a + b›
using not_add_distrib [of a ‹- b›] by simp

lemma and_eq_minus_1_iff:
‹a AND b = - 1 ⟷ a = - 1 ∧ b = - 1›
by (auto simp: bit_eq_iff bit_simps)

lemma disjunctive_diff:
‹a - b = a AND NOT b› if ‹⋀n. bit b n ⟹ bit a n›
proof -
have ‹NOT a + b = NOT a OR b›
then have ‹NOT (NOT a + b) = NOT (NOT a OR b)›
by simp
then show ?thesis
qed

lemma push_bit_minus:
‹push_bit n (- a) = - push_bit n a›

lemma take_bit_not_take_bit:
‹take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)›
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)

lemma take_bit_not_iff:
‹take_bit n (NOT a) = take_bit n (NOT b) ⟷ take_bit n a = take_bit n b›
apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
apply (use exp_eq_0_imp_not_bit in blast)
done

‹take_bit n (NOT a) = mask n - take_bit n a›
proof -
have ‹take_bit n (NOT a) = take_bit n (NOT (take_bit n a))›
also have ‹… = mask n AND NOT (take_bit n a)›
also have ‹… = mask n - take_bit n a›
by (subst disjunctive_diff)
finally show ?thesis
by simp
qed

‹mask n = take_bit n (- 1)›

‹take_bit n (- 1) = mask n›

‹- (2 ^ n) = NOT (mask n)›

‹push_bit n (- 1) = NOT (mask n)›

‹take_bit m (NOT (mask n)) = 0› if ‹n ≥ m›

lemma unset_bit_eq_and_not:
‹unset_bit n a = a AND NOT (push_bit n 1)›
by (rule bit_eqI) (auto simp add: bit_simps)

lemmas unset_bit_def = unset_bit_eq_and_not

lemma push_bit_Suc_minus_numeral [simp]:
‹push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))›
apply (simp only: numeral_Bit0)
apply simp
apply (simp only: numeral_mult mult_2_right numeral_add)
done

lemma push_bit_minus_numeral [simp]:
‹push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))›
by (simp only: numeral_eq_Suc push_bit_Suc_minus_numeral)

lemma take_bit_Suc_minus_1_eq:
‹take_bit (Suc n) (- 1) = 2 ^ Suc n - 1›

lemma take_bit_numeral_minus_1_eq:
‹take_bit (numeral k) (- 1) = 2 ^ numeral k - 1›

apply (rule bit_eqI)
apply (auto simp add: bit_simps not_less possible_bit_def)
apply (drule sym [of 0])
apply (simp only:)
using exp_not_zero_imp_exp_diff_not_zero apply (blast dest: exp_not_zero_imp_exp_diff_not_zero)
done

‹push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)›
by (rule bit_eqI) (auto simp add: bit_simps)

lemma push_bit_numeral_minus_1 [simp]:
‹push_bit (numeral n) (- 1) = - (2 ^ numeral n)›

end

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

instantiation int :: ring_bit_operations
begin

definition not_int :: ‹int ⇒ int›
where ‹not_int k = - k - 1›

lemma not_int_rec:
‹NOT k = of_bool (even k) + 2 * NOT (k div 2)› for k :: int
by (auto simp add: not_int_def elim: oddE)

lemma even_not_iff_int:
‹even (NOT k) ⟷ odd k› for k :: int

lemma not_int_div_2:
‹NOT k div 2 = NOT (k div 2)› for k :: int

lemma bit_not_int_iff:
‹bit (NOT k) n ⟷ ¬ bit k n›
for k :: int

function and_int :: ‹int ⇒ int ⇒ int›
where ‹(k::int) AND l = (if k ∈ {0, - 1} ∧ l ∈ {0, - 1}
then - of_bool (odd k ∧ odd l)
else of_bool (odd k ∧ odd l) + 2 * ((k div 2) AND (l div 2)))›
by auto

termination proof (relation ‹measure (λ(k, l). nat (¦k¦ + ¦l¦))›)
show ‹wf (measure (λ(k, l). nat (¦k¦ + ¦l¦)))›
by simp
show ‹((k div 2, l div 2), k, l) ∈ measure (λ(k, l). nat (¦k¦ + ¦l¦))›
if ‹¬ (k ∈ {0, - 1} ∧ l ∈ {0, - 1})› for k l
proof -
have less_eq: ‹¦k div 2¦ ≤ ¦k¦› for k :: int
have less: ‹¦k div 2¦ < ¦k¦› if ‹k ∉ {0, - 1}› for k :: int
proof (cases k)
case (nonneg n)
with that show ?thesis
next
case (neg n)
with that have ‹n ≠ 0›
by simp
then have ‹n div 2 < n›
with neg that show ?thesis
qed
from that have *: ‹k ∉ {0, - 1} ∨ l ∉ {0, - 1}›
by simp
then have ‹0 < ¦k¦ + ¦l¦›
by auto
moreover from * have ‹¦k div 2¦ + ¦l div 2¦ < ¦k¦ + ¦l¦›
proof
assume ‹k ∉ {0, - 1}›
then have ‹¦k div 2¦ < ¦k¦›
by (rule less)
with less_eq [of l] show ?thesis
by auto
next
assume ‹l ∉ {0, - 1}›
then have ‹¦l div 2¦ < ¦l¦›
by (rule less)
with less_eq [of k] show ?thesis
by auto
qed
ultimately show ?thesis
by simp
qed
qed

declare and_int.simps [simp del]

lemma and_int_rec:
‹k AND l = of_bool (odd k ∧ odd l) + 2 * ((k div 2) AND (l div 2))›
for k l :: int
proof (cases ‹k ∈ {0, - 1} ∧ l ∈ {0, - 1}›)
case True
then show ?thesis
next
case False
then show ?thesis
by (auto simp add: ac_simps and_int.simps [of k l])
qed

lemma bit_and_int_iff:
‹bit (k AND l) n ⟷ bit k n ∧ bit l n› for k l :: int
proof (induction n arbitrary: k l)
case 0
then show ?case
by (simp add: and_int_rec [of k l] bit_0)
next
case (Suc n)
then show ?case
by (simp add: and_int_rec [of k l] bit_Suc)
qed

lemma even_and_iff_int:
‹even (k AND l) ⟷ even k ∨ even l› for k l :: int
using bit_and_int_iff [of k l 0] by (auto simp add: bit_0)

definition or_int :: ‹int ⇒ int ⇒ int›
where ‹k OR l = NOT (NOT k AND NOT l)› for k l :: int

lemma or_int_rec:
‹k OR l = of_bool (odd k ∨ odd l) + 2 * ((k div 2) OR (l div 2))›
for k l :: int
using and_int_rec [of ‹NOT k› ‹NOT l›]
by (simp add: or_int_def even_not_iff_int not_int_div_2)

lemma bit_or_int_iff:
‹bit (k OR l) n ⟷ bit k n ∨ bit l n› for k l :: int
by (simp add: or_int_def bit_not_int_iff bit_and_int_iff)

definition xor_int :: ‹int ⇒ int ⇒ int›
where ‹k XOR l = k AND NOT l OR NOT k AND l› for k l :: int

lemma xor_int_rec:
‹k XOR l = of_bool (odd k ≠ odd l) + 2 * ((k div 2) XOR (l div 2))›
for k l :: int
by (simp add: xor_int_def or_int_rec [of ‹k AND NOT l› ‹NOT k AND l›] even_and_iff_int even_not_iff_int)
(simp add: and_int_rec [of ‹NOT k› ‹l›] and_int_rec [of ‹k› ‹NOT l›] not_int_div_2)

lemma bit_xor_int_iff:
‹bit (k XOR l) n ⟷ bit k n ≠ bit l n› for k l :: int
by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff)