Theory Bit_Comprehension

(*
 * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

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

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

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