Theory Word_Lib.Generic_set_bit

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

(* Author: Jeremy Dawson, NICTA *)

section ‹Operation variant for setting and unsetting bits›

theory Generic_set_bit
  imports
    "HOL-Library.Word"
    Most_significant_bit
begin

class set_bit = semiring_bits +
  fixes set_bit :: ‹'a ⇒ nat ⇒ bool ⇒ 'a›
  assumes bit_set_bit_iff_2n:
    ‹bit (set_bit a m b) n ⟷
      (if m = n then b else bit a n) ∧ 2 ^ n ≠ 0›

lemmas bit_set_bit_iff[bit_simps] = bit_set_bit_iff_2n[simplified fold_possible_bit simp_thms]

lemma set_bit_eq:
  ‹set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a›
  for a :: ‹'a::{ring_bit_operations, set_bit}›
  by (rule bit_eqI) (simp add: bit_simps)

instantiation int :: set_bit
begin

definition set_bit_int :: ‹int ⇒ nat ⇒ bool ⇒ int›
  where ‹set_bit_int i n b = (if b then Bit_Operations.set_bit else Bit_Operations.unset_bit) n i›

instance
  by standard (simp_all add: set_bit_int_def bit_simps)

end

context
  includes bit_operations_syntax
begin

lemma fixes i :: int
  shows int_set_bit_True_conv_OR [code]: "Generic_set_bit.set_bit i n True = i OR push_bit n 1"
  and int_set_bit_False_conv_NAND [code]: "Generic_set_bit.set_bit i n False = i AND NOT (push_bit n 1)"
  and int_set_bit_conv_ops: "Generic_set_bit.set_bit i n b = (if b then i OR (push_bit n 1) else i AND NOT (push_bit n 1))"
  by (simp_all add: bit_eq_iff) (auto simp add: bit_simps)

end

instantiation word :: (len) set_bit
begin

definition set_bit_word :: ‹'a word ⇒ nat ⇒ bool ⇒ 'a word›
  where set_bit_unfold: ‹set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)›
  for w :: ‹'a::len word›

instance
  by standard (auto simp add: set_bit_unfold bit_simps dest: bit_imp_le_length)

end

lemma bit_set_bit_word_iff [bit_simps]:
  ‹bit (set_bit w m b) n ⟷ (if m = n then n < LENGTH('a) ∧ b else bit w n)›
  for w :: ‹'a::len word›
  by (auto simp add: bit_simps dest: bit_imp_le_length)

lemma test_bit_set_gen:
  "bit (set_bit w n x) m ⟷ (if m = n then n < size w ∧ x else bit w m)"
  for w :: "'a::len word"
  by (simp add: bit_set_bit_word_iff word_size)

lemma test_bit_set:
  "bit (set_bit w n x) n ⟷ n < size w ∧ x"
  for w :: "'a::len word"
  by (auto simp add: bit_simps word_size)

lemma word_set_nth: "set_bit w n (bit w n) = w"
  for w :: "'a::len word"
  by (rule bit_word_eqI) (simp add: bit_simps)

lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
  for w :: "'a::len word"
  by (rule word_eqI) (simp add : test_bit_set_gen word_size)

lemma word_set_set_diff:
  fixes w :: "'a::len word"
  assumes "m ≠ n"
  shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
  by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)

lemma word_set_nth_iff: "set_bit w n b = w ⟷ bit w n = b ∨ n ≥ size w"
  for w :: "'a::len word"
  apply (rule iffI)
   apply (rule disjCI)
   apply (drule word_eqD)
   apply (erule sym [THEN trans])
   apply (simp add: test_bit_set)
  apply (erule disjE)
   apply clarsimp
  apply (rule word_eqI)
   apply (clarsimp simp add : test_bit_set_gen)
   apply (auto simp add: word_size)
  apply (rule bit_eqI)
  apply (simp add: bit_simps)
  done

lemma word_clr_le: "w ≥ set_bit w n False"
  for w :: "'a::len word"
  apply (simp add: set_bit_unfold)
  apply transfer
  apply (simp add: take_bit_unset_bit_eq unset_bit_less_eq)
  done

lemma word_set_ge: "w ≤ set_bit w n True"
  for w :: "'a::len word"
  apply (simp add: set_bit_unfold)
  apply transfer
  apply (simp add: take_bit_set_bit_eq set_bit_greater_eq)
  done

lemma set_bit_beyond:
  "size x ≤ n ⟹ set_bit x n b = x" for x :: "'a :: len word"
  by (simp add: word_set_nth_iff)

lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n"
  apply (rule word_eqI)
  apply (auto simp add: word_size bit_simps)
  done

lemma one_bit_pow: "set_bit 0 n True = (2 :: 'a :: len word) ^ n"
  by (simp add: one_bit_shiftl shiftl_def)

instantiation integer :: set_bit
begin

context
  includes integer.lifting
begin

lift_definition set_bit_integer :: ‹integer ⇒ nat ⇒ bool ⇒ integer› is set_bit .

instance
  by (standard; transfer) (simp add: bit_simps)

end

end

end