# Theory Misc_set_bit

theory Misc_set_bit
imports Misc_msb
```(*  Author:     Jeremy Dawson, NICTA
*)

section ‹Operation variant for setting and unsetting bits›

theory Misc_set_bit
imports Word Misc_msb
begin

class set_bit = ring_bit_operations +
fixes set_bit :: ‹'a ⇒ nat ⇒ bool ⇒ 'a›
assumes set_bit_eq: ‹set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a›

instantiation int :: set_bit
begin

definition set_bit_int :: ‹int ⇒ nat ⇒ bool ⇒ int›
where ‹set_bit i n b = bin_sc n b i›

instance
by standard (simp add: set_bit_int_def bin_sc_eq)

end

lemma int_set_bit_0 [simp]: fixes x :: int shows
"set_bit x 0 b = of_bool b + 2 * (x div 2)"
by (auto simp add: set_bit_int_def intro: bin_rl_eqI)

lemma int_set_bit_Suc: fixes x :: int shows
"set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b"
by (auto simp add: set_bit_int_def intro: bin_rl_eqI)

lemma bin_last_set_bit:
"bin_last (set_bit x n b) = (if n > 0 then bin_last x else b)"
by (cases n) (simp_all add: int_set_bit_Suc)

lemma bin_rest_set_bit:
"bin_rest (set_bit x n b) = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)"
by (cases n) (simp_all add: int_set_bit_Suc)

lemma int_set_bit_numeral: fixes x :: int shows
"set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b"

lemmas int_set_bit_numerals [simp] =
int_set_bit_numeral[where x="numeral w'"]
int_set_bit_numeral[where x="- numeral w'"]
int_set_bit_numeral[where x="Numeral1"]
int_set_bit_numeral[where x="1"]
int_set_bit_numeral[where x="0"]
int_set_bit_Suc[where x="numeral w'"]
int_set_bit_Suc[where x="- numeral w'"]
int_set_bit_Suc[where x="Numeral1"]
int_set_bit_Suc[where x="1"]
int_set_bit_Suc[where x="0"]
for w'

lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) ⟷ msb x"

instantiation word :: (len) set_bit
begin

definition set_bit_word :: ‹'a word ⇒ nat ⇒ bool ⇒ 'a word›
where word_set_bit_def: ‹set_bit a n x = word_of_int (bin_sc n x (uint a))›

instance
apply standard
apply (simp add: word_set_bit_def bin_sc_eq Bit_Operations.set_bit_def unset_bit_def)
apply transfer
apply simp
done

end

lemma 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›

lemma bit_set_bit_word_iff:
‹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: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length)

lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
for w :: "'a::len word"
by (auto simp: word_test_bit_def word_set_bit_def)

lemma test_bit_set: "(set_bit w n x) !! n ⟷ n < size w ∧ x"
for w :: "'a::len word"
by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)

lemma test_bit_set_gen:
"test_bit (set_bit w n x) m = (if m = n then n < size w ∧ x else test_bit w m)"
for w :: "'a::len word"
apply (unfold word_size word_test_bit_def word_set_bit_def)
apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
apply (auto elim!: test_bit_size [unfolded word_size]
done

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 set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
unfolding word_set_bit_def
by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)

lemma word_set_numeral [simp]:
"set_bit (numeral bin::'a::len word) n b =
word_of_int (bin_sc n b (numeral bin))"
unfolding word_numeral_alt by (rule set_bit_word_of_int)

lemma word_set_neg_numeral [simp]:
"set_bit (- numeral bin::'a::len word) n b =
word_of_int (bin_sc n b (- numeral bin))"
unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)

lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
unfolding word_0_wi by (rule set_bit_word_of_int)

lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
unfolding word_1_wi by (rule set_bit_word_of_int)

lemma word_set_nth_iff: "set_bit w n b = w ⟷ 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 (erule disjE)
apply clarsimp
apply (rule word_eqI)
apply (clarsimp simp add : test_bit_set_gen)
apply (drule test_bit_size)
apply force
done

lemma word_clr_le: "w ≥ set_bit w n False"
for w :: "'a::len word"
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
apply (rule order_trans)
apply (rule bintr_bin_clr_le)
apply simp
done

lemma word_set_ge: "w ≤ set_bit w n True"
for w :: "'a::len word"
apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
apply (rule order_trans [OF _ bintr_bin_set_ge])
apply simp
done

lemma set_bit_beyond:
"size x ≤ n ⟹ set_bit x n b = x" for x :: "'a :: len word"
by (auto intro: word_eqI simp add: test_bit_set_gen word_size)

end
```