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