Theory Bit_Operations

(*  Author:  Florian Haftmann, TUM
*)

section ‹Bit operations in suitable algebraic structures›

theory Bit_Operations
  imports
    Main
    "HOL-Library.Boolean_Algebra"
begin

subsection ‹Bit operations›

class semiring_bit_operations = semiring_bit_shifts +
  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›
  assumes bit_and_iff [bit_simps]: ‹⋀n. bit (a AND b) n ⟷ bit a n ∧ bit b n›
    and bit_or_iff [bit_simps]: ‹⋀n. bit (a OR b) n ⟷ bit a n ∨ bit b n›
    and bit_xor_iff [bit_simps]: ‹⋀n. bit (a XOR b) n ⟷ bit a n ≠ bit b n›
    and mask_eq_exp_minus_1: ‹mask n = 2 ^ n - 1›
begin

text ‹
  We want the bitwise operations to bind slightly weaker
  than ‹+› and ‹-›.
  For the sake of code generation
  the operations \<^const>‹and›, \<^const>‹or› and \<^const>‹xor›
  are specified as definitional class operations.
›

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

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

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

lemma zero_and_eq [simp]:
  "0 AND a = 0"
  by (simp add: bit_eq_iff bit_and_iff)

lemma and_zero_eq [simp]:
  "a AND 0 = 0"
  by (simp add: bit_eq_iff bit_and_iff)

lemma one_and_eq:
  "1 AND a = a mod 2"
  by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)

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)"
  by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff)

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)"
  by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred 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 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_take_bit_iff bit_and_iff)

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_take_bit_iff bit_or_iff)

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_take_bit_iff bit_xor_iff)

lemma push_bit_and [simp]:
  ‹push_bit n (a AND b) = push_bit n a AND push_bit n b›
  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff)

lemma push_bit_or [simp]:
  ‹push_bit n (a OR b) = push_bit n a OR push_bit n b›
  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff)

lemma push_bit_xor [simp]:
  ‹push_bit n (a XOR b) = push_bit n a XOR push_bit n b›
  by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff)

lemma drop_bit_and [simp]:
  ‹drop_bit n (a AND b) = drop_bit n a AND drop_bit n b›
  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff)

lemma drop_bit_or [simp]:
  ‹drop_bit n (a OR b) = drop_bit n a OR drop_bit n b›
  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff)

lemma drop_bit_xor [simp]:
  ‹drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b›
  by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff)

lemma bit_mask_iff [bit_simps]:
  ‹bit (mask m) n ⟷ 2 ^ n ≠ 0 ∧ n < m›
  by (simp add: mask_eq_exp_minus_1 bit_mask_iff)

lemma even_mask_iff:
  ‹even (mask n) ⟷ n = 0›
  using bit_mask_iff [of n 0] by auto

lemma mask_0 [simp]:
  ‹mask 0 = 0›
  by (simp add: mask_eq_exp_minus_1)

lemma mask_Suc_0 [simp]:
  ‹mask (Suc 0) = 1›
  by (simp add: mask_eq_exp_minus_1 add_implies_diff sym)

lemma mask_Suc_exp:
  ‹mask (Suc n) = 2 ^ n OR mask n›
  by (rule bit_eqI)
    (auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq)

lemma mask_Suc_double:
  ‹mask (Suc n) = 1 OR 2 * mask n›
proof (rule bit_eqI)
  fix q
  assume ‹2 ^ q ≠ 0›
  show ‹bit (mask (Suc n)) q ⟷ bit (1 OR 2 * mask n) q›
    by (cases q)
      (simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2)
qed

lemma mask_numeral:
  ‹mask (numeral n) = 1 + 2 * mask (pred_numeral n)›
  by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps)

lemma take_bit_mask [simp]:
  ‹take_bit m (mask n) = mask (min m n)›
  by (rule bit_eqI) (simp add: bit_simps)

lemma take_bit_eq_mask:
  ‹take_bit n a = a AND mask n›
  by (rule bit_eqI)
    (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff)

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

lemma disjunctive_add:
  ‹a + b = a OR b› if ‹⋀n. ¬ bit a n ∨ ¬ bit b n›
  by (rule bit_eqI) (use that in ‹simp add: bit_disjunctive_add_iff bit_or_iff›)

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: push_bit_of_1 bit_eq_iff bit_and_iff bit_push_bit_iff exp_eq_0_imp_not_bit)
  apply (simp_all add: bit_exp_iff)
  done

end

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

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›
  by (simp add: mod_2_eq_odd)

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 ⟷ 2 ^ n ≠ 0 ∧ ¬ bit (a - 1) n›
  by (simp add: minus_eq_not_minus_1 bit_not_iff)

lemma even_not_iff [simp]:
  "even (NOT a) ⟷ odd a"
  using bit_not_iff [of a 0] by auto

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

lemma bit_minus_1_iff [simp]:
  ‹bit (- 1) n ⟷ 2 ^ n ≠ 0›
  by (simp add: bit_minus_iff)

lemma bit_minus_exp_iff [bit_simps]:
  ‹bit (- (2 ^ m)) n ⟷ 2 ^ n ≠ 0 ∧ n ≥ m›
  by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)

lemma bit_minus_2_iff [simp]:
  ‹bit (- 2) n ⟷ 2 ^ n ≠ 0 ∧ n > 0›
  by (simp add: bit_minus_iff bit_1_iff)

lemma not_one [simp]:
  "NOT 1 = - 2"
  by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff)

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

sublocale bit: boolean_algebra ‹(AND)› ‹(OR)› NOT 0 ‹- 1›
  rewrites ‹bit.xor = (XOR)›
proof -
  interpret bit: boolean_algebra ‹(AND)› ‹(OR)› NOT 0 ‹- 1›
    by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
  show ‹boolean_algebra (AND) (OR) NOT 0 (- 1)›
    by standard
  show ‹boolean_algebra.xor (AND) (OR) NOT = (XOR)›
    by (rule ext, rule ext, rule bit_eqI)
      (auto simp add: bit.xor_def bit_and_iff bit_or_iff bit_xor_iff bit_not_iff)
qed

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

lemma not_add_distrib:
  ‹NOT (a + b) = NOT a - b›
  by (simp add: not_eq_complement algebra_simps)

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

lemma (in ring_bit_operations) and_eq_minus_1_iff:
  ‹a AND b = - 1 ⟷ a = - 1 ∧ b = - 1›
proof
  assume ‹a = - 1 ∧ b = - 1›
  then show ‹a AND b = - 1›
    by simp
next
  assume ‹a AND b = - 1›
  have *: ‹bit a n› ‹bit b n› if ‹2 ^ n ≠ 0› for n
  proof -
    from ‹a AND b = - 1›
    have ‹bit (a AND b) n = bit (- 1) n›
      by (simp add: bit_eq_iff)
    then show ‹bit a n› ‹bit b n›
      using that by (simp_all add: bit_and_iff)
  qed
  have ‹a = - 1›
    by (rule bit_eqI) (simp add: *)
  moreover have ‹b = - 1›
    by (rule bit_eqI) (simp add: *)
  ultimately show ‹a = - 1 ∧ b = - 1›
    by simp
qed

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›
    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
  then have ‹NOT (NOT a + b) = NOT (NOT a OR b)›
    by simp
  then show ?thesis
    by (simp add: not_add_distrib)
qed

lemma push_bit_minus:
  ‹push_bit n (- a) = - push_bit n a›
  by (simp add: push_bit_eq_mult)

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_eq_iff)
  apply (simp add: bit_not_iff bit_take_bit_iff bit_exp_iff)
  apply (use exp_eq_0_imp_not_bit in blast)
  done

lemma take_bit_not_eq_mask_diff:
  ‹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))›
    by (simp add: take_bit_not_take_bit)
  also have ‹… = mask n AND NOT (take_bit n a)›
    by (simp add: take_bit_eq_mask ac_simps)
  also have ‹… = mask n - take_bit n a›
    by (subst disjunctive_diff)
      (auto simp add: bit_take_bit_iff bit_mask_iff exp_eq_0_imp_not_bit)
  finally show ?thesis
    by simp
qed

lemma mask_eq_take_bit_minus_one:
  ‹mask n = take_bit n (- 1)›
  by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute)

lemma take_bit_minus_one_eq_mask:
  ‹take_bit n (- 1) = mask n›
  by (simp add: mask_eq_take_bit_minus_one)

lemma minus_exp_eq_not_mask:
  ‹- (2 ^ n) = NOT (mask n)›
  by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1)

lemma push_bit_minus_one_eq_not_mask:
  ‹push_bit n (- 1) = NOT (mask n)›
  by (simp add: push_bit_eq_mult minus_exp_eq_not_mask)

lemma take_bit_not_mask_eq_0:
  ‹take_bit m (NOT (mask n)) = 0› if ‹n ≥ m›
  by (rule bit_eqI) (use that in ‹simp add: bit_take_bit_iff bit_not_iff bit_mask_iff›)

lemma take_bit_mask [simp]:
  ‹take_bit m (mask n) = mask (min m n)›
  by (simp add: mask_eq_take_bit_minus_one)

definition set_bit :: ‹nat ⇒ 'a ⇒ 'a›
  where ‹set_bit n a = a OR push_bit n 1›

definition unset_bit :: ‹nat ⇒ 'a ⇒ 'a›
  where ‹unset_bit n a = a AND NOT (push_bit n 1)›

definition flip_bit :: ‹nat ⇒ 'a ⇒ 'a›
  where ‹flip_bit n a = a XOR push_bit n 1›

lemma bit_set_bit_iff [bit_simps]:
  ‹bit (set_bit m a) n ⟷ bit a n ∨ (m = n ∧ 2 ^ n ≠ 0)›
  by (auto simp add: set_bit_def push_bit_of_1 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

lemma bit_unset_bit_iff [bit_simps]:
  ‹bit (unset_bit m a) n ⟷ bit a n ∧ m ≠ n›
  by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)

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

lemma bit_flip_bit_iff [bit_simps]:
  ‹bit (flip_bit m a) n ⟷ (m = n ⟷ ¬ bit a n) ∧ 2 ^ n ≠ 0›
  by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_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

lemma set_bit_0 [simp]:
  ‹set_bit 0 a = 1 + 2 * (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  then show ‹bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m›
    by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff)
      (cases m, simp_all add: bit_Suc)
qed

lemma set_bit_Suc:
  ‹set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  show ‹bit (set_bit (Suc n) a) m ⟷ bit (a mod 2 + 2 * set_bit n (a div 2)) m›
  proof (cases m)
    case 0
    then show ?thesis
      by (simp add: even_set_bit_iff)
  next
    case (Suc m)
    with * have ‹2 ^ m ≠ 0›
      using mult_2 by auto
    show ?thesis
      by (cases a rule: parity_cases)
        (simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *,
        simp_all add: Suc ‹2 ^ m ≠ 0› bit_Suc)
  qed
qed

lemma unset_bit_0 [simp]:
  ‹unset_bit 0 a = 2 * (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  then show ‹bit (unset_bit 0 a) m = bit (2 * (a div 2)) m›
    by (simp add: bit_unset_bit_iff bit_double_iff)
      (cases m, simp_all add: bit_Suc)
qed

lemma unset_bit_Suc:
  ‹unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  then show ‹bit (unset_bit (Suc n) a) m ⟷ bit (a mod 2 + 2 * unset_bit n (a div 2)) m›
  proof (cases m)
    case 0
    then show ?thesis
      by (simp add: even_unset_bit_iff)
  next
    case (Suc m)
    show ?thesis
      by (cases a rule: parity_cases)
        (simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *,
         simp_all add: Suc bit_Suc)
  qed
qed

lemma flip_bit_0 [simp]:
  ‹flip_bit 0 a = of_bool (even a) + 2 * (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  then show ‹bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m›
    by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff)
      (cases m, simp_all add: bit_Suc)
qed

lemma flip_bit_Suc:
  ‹flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  show ‹bit (flip_bit (Suc n) a) m ⟷ bit (a mod 2 + 2 * flip_bit n (a div 2)) m›
  proof (cases m)
    case 0
    then show ?thesis
      by (simp add: even_flip_bit_iff)
  next
    case (Suc m)
    with * have ‹2 ^ m ≠ 0›
      using mult_2 by auto
    show ?thesis
      by (cases a rule: parity_cases)
        (simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff,
        simp_all add: Suc ‹2 ^ m ≠ 0› bit_Suc)
  qed
qed

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)

end


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

lemma int_bit_bound:
  fixes k :: int
  obtains n where ‹⋀m. n ≤ m ⟹ bit k m ⟷ bit k n›
    and ‹n > 0 ⟹ bit k (n - 1) ≠ bit k n›
proof -
  obtain q where *: ‹⋀m. q ≤ m ⟹ bit k m ⟷ bit k q›
  proof (cases ‹k ≥ 0›)
    case True
    moreover from power_gt_expt [of 2 ‹nat k›]
    have ‹k < 2 ^ nat k› by simp
    ultimately have *: ‹k div 2 ^ nat k = 0›
      by simp
    show thesis
    proof (rule that [of ‹nat k›])
      fix m
      assume ‹nat k ≤ m›
      then show ‹bit k m ⟷ bit k (nat k)›
        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
    qed
  next
    case False
    moreover from power_gt_expt [of 2 ‹nat (- k)›]
    have ‹- k ≤ 2 ^ nat (- k)›
      by simp
    ultimately have ‹- k div - (2 ^ nat (- k)) = - 1›
      by (subst div_pos_neg_trivial) simp_all
    then have *: ‹k div 2 ^ nat (- k) = - 1›
      by simp
    show thesis
    proof (rule that [of ‹nat (- k)›])
      fix m
      assume ‹nat (- k) ≤ m›
      then show ‹bit k m ⟷ bit k (nat (- k))›
        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
    qed
  qed
  show thesis
  proof (cases ‹∀m. bit k m ⟷ bit k q›)
    case True
    then have ‹bit k 0 ⟷ bit k q›
      by blast
    with True that [of 0] show thesis
      by simp
  next
    case False
    then obtain r where **: ‹bit k r ≠ bit k q›
      by blast
    have ‹r < q›
      by (rule ccontr) (use * [of r] ** in simp)
    define N where ‹N = {n. n < q ∧ bit k n ≠ bit k q}›
    moreover have ‹finite N› ‹r ∈ N›
      using ** N_def ‹r < q› by auto
    moreover define n where ‹n = Suc (Max N)›
    ultimately have ‹⋀m. n ≤ m ⟹ bit k m ⟷ bit k n›
      apply auto
         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n ‹finite N› all_not_in_conv mem_Collect_eq not_le)
        apply (metis "*" Max_ge Suc_n_not_le_n ‹finite N› linorder_not_less mem_Collect_eq)
        apply (metis "*" Max_ge Suc_n_not_le_n ‹finite N› linorder_not_less mem_Collect_eq)
      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n ‹finite N› all_not_in_conv mem_Collect_eq not_le)
      done
    have ‹bit k (Max N) ≠ bit k n›
      by (metis (mono_tags, lifting) "*" Max_in N_def ‹⋀m. n ≤ m ⟹ bit k m = bit k n› ‹finite N› ‹r ∈ N› empty_iff le_cases mem_Collect_eq)
    show thesis apply (rule that [of n])
      using ‹⋀m. n ≤ m ⟹ bit k m = bit k n› apply blast
      using ‹bit k (Max N) ≠ bit k n› n_def by auto
  qed
qed

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
  by (simp add: not_int_def)

lemma not_int_div_2:
  ‹NOT k div 2 = NOT (k div 2)› for k :: int
  by (simp add: not_int_def)

lemma bit_not_int_iff [bit_simps]:
  ‹bit (NOT k) n ⟷ ¬ bit k n›
  for k :: int
  by (simp add: bit_not_int_iff' not_int_def)

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
  by (relation ‹measure (λ(k, l). nat (¦k¦ + ¦l¦))›) auto

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
    by auto (simp_all add: and_int.simps)
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])
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

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)
    (simp add: not_int_def)

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)

definition mask_int :: ‹nat ⇒ int›
  where ‹mask n = (2 :: int) ^ n - 1›

instance proof
  fix k l :: int and n :: nat
  show ‹- k = NOT (k - 1)›
    by (simp add: not_int_def)
  show ‹bit (k AND l) n ⟷ bit k n ∧ bit l n›
    by (fact bit_and_int_iff)
  show ‹bit (k OR l) n ⟷ bit k n ∨ bit l n›
    by (fact bit_or_int_iff)
  show ‹bit (k XOR l) n ⟷ bit k n ≠ bit l n›
    by (fact bit_xor_int_iff)
qed (simp_all add: bit_not_int_iff mask_int_def)

end


lemma mask_half_int:
  ‹mask n div 2 = (mask (n - 1) :: int)›
  by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps)

lemma mask_nonnegative_int [simp]:
  ‹mask n ≥ (0::int)›
  by (simp add: mask_eq_exp_minus_1)

lemma not_mask_negative_int [simp]:
  ‹¬ mask n < (0::int)›
  by (simp add: not_less)

lemma not_nonnegative_int_iff [simp]:
  ‹NOT k ≥ 0 ⟷ k < 0› for k :: int
  by (simp add: not_int_def)

lemma not_negative_int_iff [simp]:
  ‹NOT k < 0 ⟷ k ≥ 0› for k :: int
  by (subst Not_eq_iff [symmetric]) (simp add: not_less not_le)

lemma and_nonnegative_int_iff [simp]:
  ‹k AND l ≥ 0 ⟷ k ≥ 0 ∨ l ≥ 0› for k l :: int
proof (induction k arbitrary: l rule: int_bit_induct)
  case zero
  then show ?case
    by simp
next
  case minus
  then show ?case
    by simp
next
  case (even k)
  then show ?case
    using and_int_rec [of ‹k * 2› l] by (simp add: pos_imp_zdiv_nonneg_iff)
next
  case (odd k)
  from odd have ‹0 ≤ k AND l div 2 ⟷ 0 ≤ k ∨ 0 ≤ l div 2›
    by simp
  then have ‹0 ≤ (1 + k * 2) div 2 AND l div 2 ⟷ 0 ≤ (1 + k * 2) div 2∨ 0 ≤ l div 2›
    by simp
  with and_int_rec [of ‹1 + k * 2› l]
  show ?case
    by auto
qed

lemma and_negative_int_iff [simp]:
  ‹k AND l < 0 ⟷ k < 0 ∧ l < 0› for k l :: int
  by (subst Not_eq_iff [symmetric]) (simp add: not_less)

lemma and_less_eq:
  ‹k AND l ≤ k› if ‹l < 0› for k l :: int
using that proof (induction k arbitrary: l rule: int_bit_induct)
  case zero
  then show ?case
    by simp
next
  case minus
  then show ?case
    by simp
next
  case (even k)
  from even.IH [of ‹l div 2›] even.hyps even.prems
  show ?case
    by (simp add: and_int_rec [of _ l])
next
  case (odd k)
  from odd.IH [of ‹l div 2›] odd.hyps odd.prems
  show ?case
    by (simp add: and_int_rec [of _ l])
qed

lemma or_nonnegative_int_iff [simp]:
  ‹k OR l ≥ 0 ⟷ k ≥ 0 ∧ l ≥ 0› for k l :: int
  by (simp only: or_eq_not_not_and not_nonnegative_int_iff) simp

lemma or_negative_int_iff [simp]:
  ‹k OR l < 0 ⟷ k < 0 ∨ l < 0› for k l :: int
  by (subst Not_eq_iff [symmetric]) (simp add: not_less)

lemma or_greater_eq:
  ‹k OR l ≥ k› if ‹l ≥ 0› for k l :: int
using that proof (induction k arbitrary: l rule: int_bit_induct)
  case zero
  then show ?case
    by simp
next
  case minus
  then show ?case
    by simp
next
  case (even k)
  from even.IH [of ‹l div 2›] even.hyps even.prems
  show ?case
    by (simp add: or_int_rec [of _ l])
next
  case (odd k)
  from odd.IH [of ‹l div 2›] odd.hyps odd.prems
  show ?case
    by (simp add: or_int_rec [of _ l])
qed

lemma xor_nonnegative_int_iff [simp]:
  ‹k XOR l ≥ 0 ⟷ (k ≥ 0 ⟷ l ≥ 0)› for k l :: int
  by (simp only: bit.xor_def or_nonnegative_int_iff) auto

lemma xor_negative_int_iff [simp]:
  ‹k XOR l < 0 ⟷ (k < 0) ≠ (l < 0)› for k l :: int
  by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)

lemma OR_upper: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ x" "x < 2 ^ n" "y < 2 ^ n"
  shows "x OR y < 2 ^ n"
using assms proof (induction x arbitrary: y n rule: int_bit_induct)
  case zero
  then show ?case
    by simp
next
  case minus
  then show ?case
    by simp
next
  case (even x)
  from even.IH [of ‹n - 1› ‹y div 2›] even.prems even.hyps
  show ?case 
    by (cases n) (auto simp add: or_int_rec [of ‹_ * 2›] elim: oddE)
next
  case (odd x)
  from odd.IH [of ‹n - 1› ‹y div 2›] odd.prems odd.hyps
  show ?case
    by (cases n) (auto simp add: or_int_rec [of ‹1 + _ * 2›], linarith)
qed

lemma XOR_upper: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ x" "x < 2 ^ n" "y < 2 ^ n"
  shows "x XOR y < 2 ^ n"
using assms proof (induction x arbitrary: y n rule: int_bit_induct)
  case zero
  then show ?case
    by simp
next
  case minus
  then show ?case
    by simp
next
  case (even x)
  from even.IH [of ‹n - 1› ‹y div 2›] even.prems even.hyps
  show ?case 
    by (cases n) (auto simp add: xor_int_rec [of ‹_ * 2›] elim: oddE)
next
  case (odd x)
  from odd.IH [of ‹n - 1› ‹y div 2›] odd.prems odd.hyps
  show ?case
    by (cases n) (auto simp add: xor_int_rec [of ‹1 + _ * 2›])
qed

lemma AND_lower [simp]: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ x"
  shows "0 ≤ x AND y"
  using assms by simp

lemma OR_lower [simp]: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ x" "0 ≤ y"
  shows "0 ≤ x OR y"
  using assms by simp

lemma XOR_lower [simp]: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ x" "0 ≤ y"
  shows "0 ≤ x XOR y"
  using assms by simp

lemma AND_upper1 [simp]: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ x"
  shows "x AND y ≤ x"
  using assms by (induction x arbitrary: y rule: int_bit_induct)
    (simp_all add: and_int_rec [of ‹_ * 2›] and_int_rec [of ‹1 + _ * 2›] add_increasing)

lemmas AND_upper1' [simp] = order_trans [OF AND_upper1] ✐‹contributor ‹Stefan Berghofer››
lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1] ✐‹contributor ‹Stefan Berghofer››

lemma AND_upper2 [simp]: ✐‹contributor ‹Stefan Berghofer››
  fixes x y :: int
  assumes "0 ≤ y"
  shows "x AND y ≤ y"
  using assms AND_upper1 [of y x] by (simp add: ac_simps)

lemmas AND_upper2' [simp] = order_trans [OF AND_upper2] ✐‹contributor ‹Stefan Berghofer››
lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2] ✐‹contributor ‹Stefan Berghofer››

lemma plus_and_or: ‹(x AND y) + (x OR y) = x + y› for x y :: int
proof (induction x arbitrary: y rule: int_bit_induct)
  case zero
  then show ?case
    by simp
next
  case minus
  then show ?case
    by simp
next
  case (even x)
  from even.IH [of ‹y div 2›]
  show ?case
    by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
next
  case (odd x)
  from odd.IH [of ‹y div 2›]
  show ?case
    by (auto simp add: and_int_rec [of _ y] or_int_rec [of _ y] elim: oddE)
qed

lemma set_bit_nonnegative_int_iff [simp]:
  ‹set_bit n k ≥ 0 ⟷ k ≥ 0› for k :: int
  by (simp add: set_bit_def)

lemma set_bit_negative_int_iff [simp]:
  ‹set_bit n k < 0 ⟷ k < 0› for k :: int
  by (simp add: set_bit_def)

lemma unset_bit_nonnegative_int_iff [simp]:
  ‹unset_bit n k ≥ 0 ⟷ k ≥ 0› for k :: int
  by (simp add: unset_bit_def)

lemma unset_bit_negative_int_iff [simp]:
  ‹unset_bit n k < 0 ⟷ k < 0› for k :: int
  by (simp add: unset_bit_def)

lemma flip_bit_nonnegative_int_iff [simp]:
  ‹flip_bit n k ≥ 0 ⟷ k ≥ 0› for k :: int
  by (simp add: flip_bit_def)

lemma flip_bit_negative_int_iff [simp]:
  ‹flip_bit n k < 0 ⟷ k < 0› for k :: int
  by (simp add: flip_bit_def)

lemma set_bit_greater_eq:
  ‹set_bit n k ≥ k› for k :: int
  by (simp add: set_bit_def or_greater_eq)

lemma unset_bit_less_eq:
  ‹unset_bit n k ≤ k› for k :: int
  by (simp add: unset_bit_def and_less_eq)

lemma set_bit_eq:
  ‹set_bit n k = k + of_bool (¬ bit k n) * 2 ^ n› for k :: int
proof (rule bit_eqI)
  fix m
  show ‹bit (set_bit n k) m ⟷ bit (k + of_bool (¬ bit k n) * 2 ^ n) m›
  proof (cases ‹m = n›)
    case True
    then show ?thesis
      apply (simp add: bit_set_bit_iff)
      apply (simp add: bit_iff_odd div_plus_div_distrib_dvd_right)
      done
  next
    case False
    then show ?thesis
      apply (clarsimp simp add: bit_set_bit_iff)
      apply (subst disjunctive_add)
      apply (clarsimp simp add: bit_exp_iff)
      apply (clarsimp simp add: bit_or_iff bit_exp_iff)
      done
  qed
qed

lemma unset_bit_eq:
  ‹unset_bit n k = k - of_bool (bit k n) * 2 ^ n› for k :: int
proof (rule bit_eqI)
  fix m
  show ‹bit (unset_bit n k) m ⟷ bit (k - of_bool (bit k n) * 2 ^ n) m›
  proof (cases ‹m = n›)
    case True
    then show ?thesis
      apply (simp add: bit_unset_bit_iff)
      apply (simp add: bit_iff_odd)
      using div_plus_div_distrib_dvd_right [of ‹2 ^ n› ‹- (2 ^ n)› k]
      apply (simp add: dvd_neg_div)
      done
  next
    case False
    then show ?thesis
      apply (clarsimp simp add: bit_unset_bit_iff)
      apply (subst disjunctive_diff)
      apply (clarsimp simp add: bit_exp_iff)
      apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff)
      done
  qed
qed

lemma take_bit_eq_mask_iff:
  ‹take_bit n k = mask n ⟷ take_bit n (k + 1) = 0› (is ‹?P ⟷ ?Q›)
  for k :: int
proof
  assume ?P
  then have ‹take_bit n (take_bit n k + take_bit n 1) = 0›
    by (simp add: mask_eq_exp_minus_1)
  then show ?Q
    by (simp only: take_bit_add)
next
  assume ?Q
  then have ‹take_bit n (k + 1) - 1 = - 1›
    by simp
  then have ‹take_bit n (take_bit n (k + 1) - 1) = take_bit n (- 1)›
    by simp
  moreover have ‹take_bit n (take_bit n (k + 1) - 1) = take_bit n k›
    by (simp add: take_bit_eq_mod mod_simps)
  ultimately show ?P
    by (simp add: take_bit_minus_one_eq_mask)
qed

lemma take_bit_eq_mask_iff_exp_dvd:
  ‹take_bit n k = mask n ⟷ 2 ^ n dvd k + 1›
  for k :: int
  by (simp add: take_bit_eq_mask_iff flip: take_bit_eq_0_iff)

context ring_bit_operations
begin

lemma even_of_int_iff:
  ‹even (of_int k) ⟷ even k›
  by (induction k rule: int_bit_induct) simp_all

lemma bit_of_int_iff [bit_simps]:
  ‹bit (of_int k) n ⟷ (2::'a) ^ n ≠ 0 ∧ bit k n›
proof (cases ‹(2::'a) ^ n = 0›)
  case True
  then show ?thesis
    by (simp add: exp_eq_0_imp_not_bit)
next
  case False
  then have ‹bit (of_int k) n ⟷ bit k n›
  proof (induction k arbitrary: n rule: int_bit_induct)
    case zero
    then show ?case
      by simp
  next
    case minus
    then show ?case
      by simp
  next
    case (even k)
    then show ?case
      using bit_double_iff [of ‹of_int k› n] Parity.bit_double_iff [of k n]
      by (cases n) (auto simp add: ac_simps dest: mult_not_zero)
  next
    case (odd k)
    then show ?case
      using bit_double_iff [of ‹of_int k› n]
      by (cases n) (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Parity.bit_Suc dest: mult_not_zero)
  qed
  with False show ?thesis
    by simp
qed

lemma push_bit_of_int:
  ‹push_bit n (of_int k) = of_int (push_bit n k)›
  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)

lemma of_int_push_bit:
  ‹of_int (push_bit n k) = push_bit n (of_int k)›
  by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult)

lemma take_bit_of_int:
  ‹take_bit n (of_int k) = of_int (take_bit n k)›
  by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff)

lemma of_int_take_bit:
  ‹of_int (take_bit n k) = take_bit n (of_int k)›
  by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff)

lemma of_int_not_eq:
  ‹of_int (NOT k) = NOT (of_int k)›
  by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff)

lemma of_int_and_eq:
  ‹of_int (k AND l) = of_int k AND of_int l›
  by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff)

lemma of_int_or_eq:
  ‹of_int (k OR l) = of_int k OR of_int l›
  by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff)

lemma of_int_xor_eq:
  ‹of_int (k XOR l) = of_int k XOR of_int l›
  by (rule bit_eqI) (simp add: bit_of_int_iff bit_xor_iff Bit_Operations.bit_xor_iff)

lemma of_int_mask_eq:
  ‹of_int (mask n) = mask n›
  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_int_or_eq)

end

text ‹FIXME: The rule sets below are very large (24 rules for each
  operator). Is there a simpler way to do this?›

context
begin

private lemma eqI:
  ‹k = l›
  if num: ‹⋀n. bit k (numeral n) ⟷ bit l (numeral n)›
    and even: ‹even k ⟷ even l›
  for k l :: int
proof (rule bit_eqI)
  fix n
  show ‹bit k n ⟷ bit l n›
  proof (cases n)
    case 0
    with even show ?thesis
      by simp
  next
    case (Suc n)
    with num [of ‹num_of_nat (Suc n)›] show ?thesis
      by (simp only: numeral_num_of_nat)
  qed
qed

lemma int_and_numerals [simp]:
  "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
  "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND numeral y)"
  "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND numeral y)"
  "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND numeral y)"
  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (numeral x AND - numeral (y + Num.One))"
  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (numeral x AND - numeral y)"
  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x AND - numeral (y + Num.One))"
  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND numeral y)"
  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND numeral y)"
  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND numeral y)"
  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x AND - numeral y)"
  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (2 :: int) * (- numeral x AND - numeral (y + Num.One))"
  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (2 :: int) * (- numeral (x + Num.One) AND - numeral y)"
  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) AND - numeral (y + Num.One))"
  "(1::int) AND numeral (Num.Bit0 y) = 0"
  "(1::int) AND numeral (Num.Bit1 y) = 1"
  "(1::int) AND - numeral (Num.Bit0 y) = 0"
  "(1::int) AND - numeral (Num.Bit1 y) = 1"
  "numeral (Num.Bit0 x) AND (1::int) = 0"
  "numeral (Num.Bit1 x) AND (1::int) = 1"
  "- numeral (Num.Bit0 x) AND (1::int) = 0"
  "- numeral (Num.Bit1 x) AND (1::int) = 1"
  by (auto simp add: bit_and_iff bit_minus_iff even_and_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq intro: eqI)

lemma int_or_numerals [simp]:
  "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR numeral y)"
  "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
  "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
  "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR numeral y)"
  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x OR - numeral y)"
  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x OR - numeral y)"
  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x OR - numeral (y + Num.One))"
  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR numeral y)"
  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR numeral y)"
  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR numeral y)"
  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x OR - numeral y)"
  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x OR - numeral (y + Num.One))"
  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral y)"
  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral (x + Num.One) OR - numeral (y + Num.One))"
  "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
  "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
  "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
  "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
  "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
  "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
  "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
  "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
  by (auto simp add: bit_or_iff bit_minus_iff even_or_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)

lemma int_xor_numerals [simp]:
  "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR numeral y)"
  "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
  "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR numeral y)"
  "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR numeral y)"
  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (numeral x XOR - numeral y)"
  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (numeral x XOR - numeral y)"
  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (numeral x XOR - numeral (y + Num.One))"
  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR numeral y)"
  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR numeral y)"
  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR numeral y)"
  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (2 :: int) * (- numeral x XOR - numeral y)"
  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = 1 + (2 :: int) * (- numeral x XOR - numeral (y + Num.One))"
  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = 1 + (2 :: int) * (- numeral (x + Num.One) XOR - numeral y)"
  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (2 :: int) * (- numeral (x + Num.One) XOR - numeral (y + Num.One))"
  "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
  "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
  "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
  "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
  "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
  "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
  "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
  "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
  by (auto simp add: bit_xor_iff bit_minus_iff even_xor_iff bit_double_iff even_bit_succ_iff add_One sub_inc_One_eq sub_BitM_One_eq intro: eqI)

end


subsection ‹Bit concatenation›

definition concat_bit :: ‹nat ⇒ int ⇒ int ⇒ int›
  where ‹concat_bit n k l = take_bit n k OR push_bit n l›

lemma bit_concat_bit_iff [bit_simps]:
  ‹bit (concat_bit m k l) n ⟷ n < m ∧ bit k n ∨ m ≤ n ∧ bit l (n - m)›
  by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps)

lemma concat_bit_eq:
  ‹concat_bit n k l = take_bit n k + push_bit n l›
  by (simp add: concat_bit_def take_bit_eq_mask
    bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add)

lemma concat_bit_0 [simp]:
  ‹concat_bit 0 k l = l›
  by (simp add: concat_bit_def)

lemma concat_bit_Suc:
  ‹concat_bit (Suc n) k l = k mod 2 + 2 * concat_bit n (k div 2) l›
  by (simp add: concat_bit_eq take_bit_Suc push_bit_double)

lemma concat_bit_of_zero_1 [simp]:
  ‹concat_bit n 0 l = push_bit n l›
  by (simp add: concat_bit_def)

lemma concat_bit_of_zero_2 [simp]:
  ‹concat_bit n k 0 = take_bit n k›
  by (simp add: concat_bit_def take_bit_eq_mask)

lemma concat_bit_nonnegative_iff [simp]:
  ‹concat_bit n k l ≥ 0 ⟷ l ≥ 0›
  by (simp add: concat_bit_def)

lemma concat_bit_negative_iff [simp]:
  ‹concat_bit n k l < 0 ⟷ l < 0›
  by (simp add: concat_bit_def)

lemma concat_bit_assoc:
  ‹concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r›
  by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps)

lemma concat_bit_assoc_sym:
  ‹concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)›
  by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def)

lemma concat_bit_eq_iff:
  ‹concat_bit n k l = concat_bit n r s
    ⟷ take_bit n k = take_bit n r ∧ l = s› (is ‹?P ⟷ ?Q›)
proof
  assume ?Q
  then show ?P
    by (simp add: concat_bit_def)
next
  assume ?P
  then have *: ‹bit (concat_bit n k l) m = bit (concat_bit n r s) m› for m
    by (simp add: bit_eq_iff)
  have ‹take_bit n k = take_bit n r›
  proof (rule bit_eqI)
    fix m
    from * [of m]
    show ‹bit (take_bit n k) m ⟷ bit (take_bit n r) m›
      by (auto simp add: bit_take_bit_iff bit_concat_bit_iff)
  qed
  moreover have ‹push_bit n l = push_bit n s›
  proof (rule bit_eqI)
    fix m
    from * [of m]
    show ‹bit (push_bit n l) m ⟷ bit (push_bit n s) m›
      by (auto simp add: bit_push_bit_iff bit_concat_bit_iff)
  qed
  then have ‹l = s›
    by (simp add: push_bit_eq_mult)
  ultimately show ?Q
    by (simp add: concat_bit_def)
qed

lemma take_bit_concat_bit_eq:
  ‹take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)›
  by (rule bit_eqI)
    (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def)  

lemma concat_bit_take_bit_eq:
  ‹concat_bit n (take_bit n b) = concat_bit n b›
  by (simp add: concat_bit_def [abs_def])


subsection ‹Taking bits with sign propagation›

context ring_bit_operations
begin

definition signed_take_bit :: ‹nat ⇒ 'a ⇒ 'a›
  where ‹signed_take_bit n a = take_bit n a OR (of_bool (bit a n) * NOT (mask n))›

lemma signed_take_bit_eq_if_positive:
  ‹signed_take_bit n a = take_bit n a› if ‹¬ bit a n›
  using that by (simp add: signed_take_bit_def)

lemma signed_take_bit_eq_if_negative:
  ‹signed_take_bit n a = take_bit n a OR NOT (mask n)› if ‹bit a n›
  using that by (simp add: signed_take_bit_def)

lemma even_signed_take_bit_iff:
  ‹even (signed_take_bit m a) ⟷ even a›
  by (auto simp add: signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)

lemma bit_signed_take_bit_iff [bit_simps]:
  ‹bit (signed_take_bit m a) n ⟷ 2 ^ n ≠ 0 ∧ bit a (min m n)›
  by (simp add: signed_take_bit_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff min_def not_le)
    (use exp_eq_0_imp_not_bit in blast)

lemma signed_take_bit_0 [simp]:
  ‹signed_take_bit 0 a = - (a mod 2)›
  by (simp add: signed_take_bit_def odd_iff_mod_2_eq_one)

lemma signed_take_bit_Suc:
  ‹signed_take_bit (Suc n) a = a mod 2 + 2 * signed_take_bit n (a div 2)›
proof (rule bit_eqI)
  fix m
  assume *: ‹2 ^ m ≠ 0›
  show ‹bit (signed_take_bit (Suc n) a) m ⟷
    bit (a mod 2 + 2 * signed_take_bit n (a div 2)) m›
  proof (cases m)
    case 0
    then show ?thesis
      by (simp add: even_signed_take_bit_iff)
  next
    case (Suc m)
    with * have ‹2 ^ m ≠ 0›
      by (metis mult_not_zero power_Suc)
    with Suc show ?thesis
      by (simp add: bit_signed_take_bit_iff mod2_eq_if bit_double_iff even_bit_succ_iff
        ac_simps flip: bit_Suc)
  qed
qed

lemma signed_take_bit_of_0 [simp]:
  ‹signed_take_bit n 0 = 0›
  by (simp add: signed_take_bit_def)

lemma signed_take_bit_of_minus_1 [simp]:
  ‹signed_take_bit n (- 1) = - 1›
  by (simp add: signed_take_bit_def take_bit_minus_one_eq_mask mask_eq_exp_minus_1)

lemma signed_take_bit_Suc_1 [simp]:
  ‹signed_take_bit (Suc n) 1 = 1›
  by (simp add: signed_take_bit_Suc)

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

lemma signed_take_bit_eq_iff_take_bit_eq:
  ‹signed_take_bit n a = signed_take_bit n b ⟷ take_bit (Suc n) a = take_bit (Suc n) b›
proof -
  have ‹bit (signed_take_bit n a) = bit (signed_take_bit n b) ⟷ bit (take_bit (Suc n) a) = bit (take_bit (Suc n) b)›
    by (simp add: fun_eq_iff bit_signed_take_bit_iff bit_take_bit_iff not_le less_Suc_eq_le min_def)
      (use exp_eq_0_imp_not_bit in fastforce)
  then show ?thesis
    by (simp add: bit_eq_iff fun_eq_iff)
qed

lemma signed_take_bit_signed_take_bit [simp]:
  ‹signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a›
proof (rule bit_eqI)
  fix q
  show ‹bit (signed_take_bit m (signed_take_bit n a)) q ⟷
    bit (signed_take_bit (min m n) a) q›
    by (simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff)
      (use le_Suc_ex exp_add_not_zero_imp in blast)
qed

lemma signed_take_bit_take_bit:
  ‹signed_take_bit m (take_bit n a) = (if n ≤ m then take_bit n else signed_take_bit m) a›
  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)

lemma take_bit_signed_take_bit:
  ‹take_bit m (signed_take_bit n a) = take_bit m a› if ‹m ≤ Suc n›
  using that by (rule le_SucE; intro bit_eqI)
   (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)

end

text ‹Modulus centered around 0›

lemma signed_take_bit_eq_concat_bit:
  ‹signed_take_bit n k = concat_bit n k (- of_bool (bit k n))›
  by (simp add: concat_bit_def signed_take_bit_def push_bit_minus_one_eq_not_mask)

lemma signed_take_bit_add:
  ‹signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)›
  for k l :: int
proof -
  have ‹take_bit (Suc n)
     (take_bit (Suc n) (signed_take_bit n k) +
      take_bit (Suc n) (signed_take_bit n l)) =
    take_bit (Suc n) (k + l)›
    by (simp add: take_bit_signed_take_bit take_bit_add)
  then show ?thesis
    by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_add)
qed

lemma signed_take_bit_diff:
  ‹signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)›
  for k l :: int
proof -
  have ‹take_bit (Suc n)
     (take_bit (Suc n) (signed_take_bit n k) -
      take_bit (Suc n) (signed_take_bit n l)) =
    take_bit (Suc n) (k - l)›
    by (simp add: take_bit_signed_take_bit take_bit_diff)
  then show ?thesis
    by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_diff)
qed

lemma signed_take_bit_minus:
  ‹signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)›
  for k :: int
proof -
  have ‹take_bit (Suc n)
     (- take_bit (Suc n) (signed_take_bit n k)) =
    take_bit (Suc n) (- k)›
    by (simp add: take_bit_signed_take_bit take_bit_minus)
  then show ?thesis
    by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_minus)
qed

lemma signed_take_bit_mult:
  ‹signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)›
  for k l :: int
proof -
  have ‹take_bit (Suc n)
     (take_bit (Suc n) (signed_take_bit n k) *
      take_bit (Suc n) (signed_take_bit n l)) =
    take_bit (Suc n) (k * l)›
    by (simp add: take_bit_signed_take_bit take_bit_mult)
  then show ?thesis
    by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult)
qed

lemma signed_take_bit_eq_take_bit_minus:
  ‹signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)›
  for k :: int
proof (cases ‹bit k n›)
  case True
  have ‹signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))›
    by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True)
  then have ‹signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n))›
    by (simp add: disjunctive_add bit_take_bit_iff bit_not_iff bit_mask_iff)
  with True show ?thesis
    by (simp flip: minus_exp_eq_not_mask)
next
  case False
  show ?thesis
    by (rule bit_eqI) (simp add: False bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq)
qed

lemma signed_take_bit_eq_take_bit_shift:
  ‹signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n›
  for k :: int
proof -
  have *: ‹take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n›
    by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff)
  have ‹take_bit n k - 2 ^ n = take_bit n k + NOT (mask n)›
    by (simp add: minus_exp_eq_not_mask)
  also have ‹… = take_bit n k OR NOT (mask n)›
    by (rule disjunctive_add)
      (simp add: bit_exp_iff bit_take_bit_iff bit_not_iff bit_mask_iff)
  finally have **: ‹take_bit n k - 2 ^ n = take_bit n k OR NOT (mask n)› .
  have ‹take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (take_bit (Suc n) k + take_bit (Suc n) (2 ^ n))›
    by (simp only: take_bit_add)
  also have ‹take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k›
    by (simp add: take_bit_Suc_from_most)
  finally have ‹take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (2 ^ (n + of_bool (bit k n)) + take_bit n k)›
    by (simp add: ac_simps)
  also have ‹2 ^ (n + of_bool (bit k n)) + take_bit n k = 2 ^ (n + of_bool (bit k n)) OR take_bit n k›
    by (rule disjunctive_add)
      (auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff)
  finally show ?thesis
    using * ** by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps)
qed

lemma signed_take_bit_nonnegative_iff [simp]:
  ‹0 ≤ signed_take_bit n k ⟷ ¬ bit k n›
  for k :: int
  by (simp add: signed_take_bit_def not_less concat_bit_def)

lemma signed_take_bit_negative_iff [simp]:
  ‹signed_take_bit n k < 0 ⟷ bit k n›
  for k :: int
  by (simp add: signed_take_bit_def not_less concat_bit_def)

lemma signed_take_bit_int_eq_self_iff:
  ‹signed_take_bit n k = k ⟷ - (2 ^ n) ≤ k ∧ k < 2 ^ n›
  for k :: int
  by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)

lemma signed_take_bit_int_eq_self:
  ‹signed_take_bit n k = k› if ‹- (2 ^ n) ≤ k› ‹k < 2 ^ n›
  for k :: int
  using that by (simp add: signed_take_bit_int_eq_self_iff)

lemma signed_take_bit_int_less_eq_self_iff:
  ‹signed_take_bit n k ≤ k ⟷ - (2 ^ n) ≤ k›
  for k :: int
  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_eq_self_iff algebra_simps)
    linarith

lemma signed_take_bit_int_less_self_iff:
  ‹signed_take_bit n k < k ⟷ 2 ^ n ≤ k›
  for k :: int
  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_less_self_iff algebra_simps)

lemma signed_take_bit_int_greater_self_iff:
  ‹k < signed_take_bit n k ⟷ k < - (2 ^ n)›
  for k :: int
  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_self_iff algebra_simps)
    linarith

lemma signed_take_bit_int_greater_eq_self_iff:
  ‹k ≤ signed_take_bit n k ⟷ k < 2 ^ n›
  for k :: int
  by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_greater_eq_self_iff algebra_simps)

lemma signed_take_bit_int_greater_eq:
  ‹k + 2 ^ Suc n ≤ signed_take_bit n k› if ‹k < - (2 ^ n)›
  for k :: int
  using that take_bit_int_greater_eq [of ‹k + 2 ^ n› ‹Suc n›]
  by (simp add: signed_take_bit_eq_take_bit_shift)

lemma signed_take_bit_int_less_eq:
  ‹signed_take_bit n k ≤ k - 2 ^ Suc n› if ‹k ≥ 2 ^ n›
  for k :: int
  using that take_bit_int_less_eq [of ‹Suc n› ‹k + 2 ^ n›]
  by (simp add: signed_take_bit_eq_take_bit_shift)

lemma signed_take_bit_Suc_bit0 [simp]:
  ‹signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * (2 :: int)›
  by (simp add: signed_take_bit_Suc)

lemma signed_take_bit_Suc_bit1 [simp]:
  ‹signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + (1 :: int)›
  by (simp add: signed_take_bit_Suc)

lemma signed_take_bit_Suc_minus_bit0 [simp]:
  ‹signed_take_bit (Suc n) (- numeral (Num.Bit0 k)) = signed_take_bit n (- numeral k) * (2 :: int)›
  by (simp add: signed_take_bit_Suc)

lemma signed_take_bit_Suc_minus_bit1 [simp]:
  ‹signed_take_bit (Suc n) (- numeral (Num.Bit1 k)) = signed_take_bit n (- numeral k - 1) * 2 + (1 :: int)›
  by (simp add: signed_take_bit_Suc)

lemma signed_take_bit_numeral_bit0 [simp]:
  ‹signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * (2 :: int)›
  by (simp add: signed_take_bit_rec)

lemma signed_take_bit_numeral_bit1 [simp]:
  ‹signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + (1 :: int)›
  by (simp add: signed_take_bit_rec)

lemma signed_take_bit_numeral_minus_bit0 [simp]:
  ‹signed_take_bit (numeral l) (- numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (- numeral k) * (2 :: int)›
  by (simp add: signed_take_bit_rec)

lemma signed_take_bit_numeral_minus_bit1 [simp]:
  ‹signed_take_bit (numeral l) (- numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (- numeral k - 1) * 2 + (1 :: int)›
  by (simp add: signed_take_bit_rec)

lemma signed_take_bit_code [code]:
  ‹signed_take_bit n a =
  (let l = take_bit (Suc n) a
   in if bit l n then l + push_bit (Suc n) (- 1) else l)›
proof -
  have *: ‹take_bit (Suc n) a + push_bit n (- 2) =
    take_bit (Suc n) a OR NOT (mask (Suc n))›
    by (auto simp add: bit_take_bit_iff bit_push_bit_iff bit_not_iff bit_mask_iff disjunctive_add
       simp flip: push_bit_minus_one_eq_not_mask)
  show ?thesis
    by (rule bit_eqI)
      (auto simp add: Let_def * bit_signed_take_bit_iff bit_take_bit_iff min_def less_Suc_eq bit_not_iff bit_mask_iff bit_or_iff)
qed

lemma not_minus_numeral_inc_eq:
  ‹NOT (- numeral (Num.inc n)) = (numeral n :: int)›
  by (simp add: not_int_def sub_inc_One_eq)


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

instantiation nat :: semiring_bit_operations
begin

definition and_nat :: ‹nat ⇒ nat ⇒ nat›
  where ‹m AND n = nat (int m AND int n)› for m n :: nat

definition or_nat :: ‹nat ⇒ nat ⇒ nat›
  where ‹m OR n = nat (int m OR int n)› for m n :: nat

definition xor_nat :: ‹nat ⇒ nat ⇒ nat›
  where ‹m XOR n = nat (int m XOR int n)› for m n :: nat

definition mask_nat :: ‹nat ⇒ nat›
  where ‹mask n = (2 :: nat) ^ n - 1›

instance proof
  fix m n q :: nat
  show ‹bit (m AND n) q ⟷ bit m q ∧ bit n q›
    by (simp add: and_nat_def bit_simps)
  show ‹bit (m OR n) q ⟷ bit m q ∨ bit n q›
    by (simp add: or_nat_def bit_simps)
  show ‹bit (m XOR n) q ⟷ bit m q ≠ bit n q›
    by (simp add: xor_nat_def bit_simps)
qed (simp add: mask_nat_def)

end

lemma and_nat_rec:
  ‹m AND n = of_bool (odd m ∧ odd n) + 2 * ((m div 2) AND (n div 2))› for m n :: nat
  by (simp add: and_nat_def and_int_rec [of ‹int m› ‹int n›] zdiv_int nat_add_distrib nat_mult_distrib)

lemma or_nat_rec:
  ‹m OR n = of_bool (odd m ∨ odd n) + 2 * ((m div 2) OR (n div 2))› for m n :: nat
  by (simp add: or_nat_def or_int_rec [of ‹int m› ‹int n›] zdiv_int nat_add_distrib nat_mult_distrib)

lemma xor_nat_rec:
  ‹m XOR n = of_bool (odd m ≠ odd n) + 2 * ((m div 2) XOR (n div 2))› for m n :: nat
  by (simp add: xor_nat_def xor_int_rec [of ‹int m› ‹int n›] zdiv_int nat_add_distrib nat_mult_distrib)

lemma Suc_0_and_eq [simp]:
  ‹Suc 0 AND n = n mod 2›
  using one_and_eq [of n] by simp

lemma and_Suc_0_eq [simp]:
  ‹n AND Suc 0 = n mod 2›
  using and_one_eq [of n] by simp

lemma Suc_0_or_eq:
  ‹Suc 0 OR n = n + of_bool (even n)›
  using one_or_eq [of n] by simp

lemma or_Suc_0_eq:
  ‹n OR Suc 0 = n + of_bool (even n)›
  using or_one_eq [of n] by simp

lemma Suc_0_xor_eq:
  ‹Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)›
  using one_xor_eq [of n] by simp

lemma xor_Suc_0_eq:
  ‹n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)›
  using xor_one_eq [of n] by simp

context semiring_bit_operations
begin

lemma of_nat_and_eq:
  ‹of_nat (m AND n) = of_nat m AND of_nat n›
  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff)

lemma of_nat_or_eq:
  ‹of_nat (m OR n) = of_nat m OR of_nat n›
  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff)

lemma of_nat_xor_eq:
  ‹of_nat (m XOR n) = of_nat m XOR of_nat n›
  by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff)

end

context ring_bit_operations
begin

lemma of_nat_mask_eq:
  ‹of_nat (mask n) = mask n›
  by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq)

end

lemma Suc_mask_eq_exp:
  ‹Suc (mask n) = 2 ^ n›
  by (simp add: mask_eq_exp_minus_1)

lemma less_eq_mask:
  ‹n ≤ mask n›
  by (simp add: mask_eq_exp_minus_1 le_diff_conv2)
    (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0)

lemma less_mask:
  ‹n < mask n› if ‹Suc 0 < n›
proof -
  define m where ‹m = n - 2›
  with that have *: ‹n = m + 2›
    by simp
  have ‹Suc (Suc (Suc m)) < 4 * 2 ^ m›
    by (induction m) simp_all
  then have ‹Suc (m + 2) < Suc (mask (m + 2))›
    by (simp add: Suc_mask_eq_exp)
  then have ‹m + 2 < mask (m + 2)›
    by (simp add: less_le)
  with * show ?thesis
    by simp
qed


subsection ‹Instances for \<^typ>‹integer› and \<^typ>‹natural››

unbundle integer.lifting natural.lifting

instantiation integer :: ring_bit_operations
begin

lift_definition not_integer :: ‹integer ⇒ integer›
  is not .

lift_definition and_integer :: ‹integer ⇒ integer ⇒ integer›
  is ‹and› .

lift_definition or_integer :: ‹integer ⇒ integer ⇒ integer›
  is or .

lift_definition xor_integer ::  ‹integer ⇒ integer ⇒ integer›
  is xor .

lift_definition mask_integer :: ‹nat ⇒ integer›
  is mask .

instance by (standard; transfer)
  (simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1
    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)

end

lemma [code]:
  ‹mask n = 2 ^ n - (1::integer)›
  by (simp add: mask_eq_exp_minus_1)

instantiation natural :: semiring_bit_operations
begin

lift_definition and_natural :: ‹natural ⇒ natural ⇒ natural›
  is ‹and› .

lift_definition or_natural :: ‹natural ⇒ natural ⇒ natural›
  is or .

lift_definition xor_natural ::  ‹natural ⇒ natural ⇒ natural›
  is xor .

lift_definition mask_natural :: ‹nat ⇒ natural›
  is mask .

instance by (standard; transfer)
  (simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff)

end

lemma [code]:
  ‹integer_of_natural (mask n) = mask n›
  by transfer (simp add: mask_eq_exp_minus_1 of_nat_diff)

lifting_update integer.lifting
lifting_forget integer.lifting

lifting_update natural.lifting
lifting_forget natural.lifting


subsection ‹Key ideas of bit operations›

text ‹
  When formalizing bit operations, it is tempting to represent
  bit values as explicit lists over a binary type. This however
  is a bad idea, mainly due to the inherent ambiguities in
  representation concerning repeating leading bits.

  Hence this approach avoids such explicit lists altogether
  following an algebraic path:

  ▪ Bit values are represented by numeric types: idealized
    unbounded bit values can be represented by type \<^typ>‹int›,
    bounded bit values by quotient types over \<^typ>‹int›.

  ▪ (A special case are idealized unbounded bit values ending
    in @{term [source] 0} which can be represented by type \<^typ>‹nat› but
    only support a restricted set of operations).

  ▪ From this idea follows that

      ▪ multiplication by \<^term>‹2 :: int› is a bit shift to the left and

      ▪ division by \<^term>‹2 :: int› is a bit shift to the right.

  ▪ Concerning bounded bit values, iterated shifts to the left
    may result in eliminating all bits by shifting them all
    beyond the boundary.  The property \<^prop>‹(2 :: int) ^ n ≠ 0›
    represents that \<^term>‹n› is ∗‹not› beyond that boundary.

  ▪ The projection on a single bit is then @{thm bit_iff_odd [where ?'a = int, no_vars]}.

  ▪ This leads to the most fundamental properties of bit values:

      ▪ Equality rule: @{thm bit_eqI [where ?'a = int, no_vars]}

      ▪ Induction rule: @{thm bits_induct [where ?'a = int, no_vars]}

  ▪ Typical operations are characterized as follows:

      ▪ Singleton \<^term>‹n›th bit: \<^term>‹(2 :: int) ^ n›

      ▪ Bit mask upto bit \<^term>‹n›: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]}

      ▪ Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]}

      ▪ Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]}

      ▪ Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]}

      ▪ Negation: @{thm bit_not_iff [where ?'a = int, no_vars]}

      ▪ And: @{thm bit_and_iff [where ?'a = int, no_vars]}

      ▪ Or: @{thm bit_or_iff [where ?'a = int, no_vars]}

      ▪ Xor: @{thm bit_xor_iff [where ?'a = int, no_vars]}

      ▪ Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]}

      ▪ Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]}

      ▪ Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]}

      ▪ Signed truncation, or modulus centered around \<^term>‹0::int›: @{thm signed_take_bit_def [no_vars]}

      ▪ Bit concatenation: @{thm concat_bit_def [no_vars]}

      ▪ (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]}
›

code_identifier
  type_class semiring_bits ⇀
  (SML) Bit_Operations.semiring_bits and (OCaml) Bit_Operations.semiring_bits and (Haskell) Bit_Operations.semiring_bits and (Scala) Bit_Operations.semiring_bits
| class_relation semiring_bits < semiring_parity ⇀
  (SML) Bit_Operations.semiring_parity_semiring_bits and (OCaml) Bit_Operations.semiring_parity_semiring_bits and (Haskell) Bit_Operations.semiring_parity_semiring_bits and (Scala) Bit_Operations.semiring_parity_semiring_bits
| constant bit ⇀
  (SML) Bit_Operations.bit and (OCaml) Bit_Operations.bit and (Haskell) Bit_Operations.bit and (Scala) Bit_Operations.bit
| class_instance nat :: semiring_bits ⇀
  (SML) Bit_Operations.semiring_bits_nat and (OCaml) Bit_Operations.semiring_bits_nat and (Haskell) Bit_Operations.semiring_bits_nat and (Scala) Bit_Operations.semiring_bits_nat
| class_instance int :: semiring_bits ⇀
  (SML) Bit_Operations.semiring_bits_int and (OCaml) Bit_Operations.semiring_bits_int and (Haskell) Bit_Operations.semiring_bits_int and (Scala) Bit_Operations.semiring_bits_int
| type_class semiring_bit_shifts ⇀
  (SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bits and (Scala) Bit_Operations.semiring_bit_shifts
| class_relation semiring_bit_shifts < semiring_bits ⇀
  (SML) Bit_Operations.semiring_bits_semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bits_semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bits_semiring_bit_shifts and (Scala) Bit_Operations.semiring_bits_semiring_bit_shifts
| constant push_bit ⇀
  (SML) Bit_Operations.push_bit and (OCaml) Bit_Operations.push_bit and (Haskell) Bit_Operations.push_bit and (Scala) Bit_Operations.push_bit
| constant drop_bit ⇀
  (SML) Bit_Operations.drop_bit and (OCaml) Bit_Operations.drop_bit and (Haskell) Bit_Operations.drop_bit and (Scala) Bit_Operations.drop_bit
| constant take_bit ⇀
  (SML) Bit_Operations.take_bit and (OCaml) Bit_Operations.take_bit and (Haskell) Bit_Operations.take_bit and (Scala) Bit_Operations.take_bit
| class_instance nat :: semiring_bit_shifts ⇀
  (SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bit_shifts and (Scala) Bit_Operations.semiring_bit_shifts
| class_instance int :: semiring_bit_shifts ⇀
  (SML) Bit_Operations.semiring_bit_shifts and (OCaml) Bit_Operations.semiring_bit_shifts and (Haskell) Bit_Operations.semiring_bit_shifts and (Scala) Bit_Operations.semiring_bit_shifts

end