# Theory Word_Lib.Bit_Comprehension

```(*
* Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
*
*)

section ‹Comprehension syntax for bit expressions›

theory Bit_Comprehension
imports
"HOL-Library.Word"
begin

class bit_comprehension = ring_bit_operations +
fixes set_bits :: ‹(nat ⇒ bool) ⇒ 'a›  (binder ‹BITS › 10)
assumes set_bits_bit_eq: ‹set_bits (bit a) = a›
begin

lemma set_bits_False_eq [simp]:
‹(BITS _. False) = 0›
using set_bits_bit_eq [of 0] by (simp add: bot_fun_def)

end

instantiation word :: (len) bit_comprehension
begin

definition word_set_bits_def:
‹(BITS n. P n) = (horner_sum of_bool 2 (map P [0..<LENGTH('a)]) :: 'a word)›

instance by standard

end

lemma bit_set_bits_word_iff [bit_simps]:
‹bit (set_bits P :: 'a::len word) n ⟷ n < LENGTH('a) ∧ P n›
by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)

lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. bit i n)"
by (rule bit_eqI) (auto simp add: bit_simps)

lemma set_bits_K_False:
‹set_bits (λ_. False) = (0 :: 'a :: len word)›
by (fact set_bits_False_eq)

lemma word_test_bit_set_bits: "bit (BITS n. f n :: 'a :: len word) n ⟷ n < LENGTH('a) ∧ f n"
by (fact bit_set_bits_word_iff)

context
includes bit_operations_syntax
fixes f :: ‹nat ⇒ bool›
begin

definition set_bits_aux :: ‹nat ⇒ 'a word ⇒ 'a::len word›
where ‹set_bits_aux n w = push_bit n w OR take_bit n (set_bits f)›

lemma bit_set_bit_aux [bit_simps]:
‹bit (set_bits_aux n w) m ⟷ m < LENGTH('a) ∧
(if m < n then f m else bit w (m - n))› for w :: ‹'a::len word›
by (auto simp add: bit_simps set_bits_aux_def)

corollary set_bits_conv_set_bits_aux:
‹set_bits f = (set_bits_aux LENGTH('a) 0 :: 'a :: len word)›
by (rule bit_word_eqI) (simp add: bit_simps)

lemma set_bits_aux_0 [simp]:
‹set_bits_aux 0 w = w›

lemma set_bits_aux_Suc [simp]:
‹set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))›
by (rule bit_word_eqI) (auto simp add: bit_simps le_less_Suc_eq mult.commute [of _ 2])

lemma set_bits_aux_simps [code]:
‹set_bits_aux 0 w = w›
‹set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))›
by simp_all

lemma set_bits_aux_rec:
‹set_bits_aux n w =
(if n = 0 then w
else let n' = n - 1 in set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))›
by (cases n) simp_all

end

end
```