1(*  Title:      HOL/Word/Bit_Comprehension.thy
2    Author:     Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
3*)
4
5section \<open>Comprehension syntax for bit expressions\<close>
6
7theory Bit_Comprehension
8  imports Bits_Int
9begin
10
11class bit_comprehension = bit_operations +
12  fixes set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
13
14instantiation int :: bit_comprehension
15begin
16
17definition
18  "set_bits f =
19    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
20      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
21      in bl_to_bin (rev (map f [0..<n]))
22     else if \<exists>n. \<forall>n'\<ge>n. f n' then
23      let n = LEAST n. \<forall>n'\<ge>n. f n'
24      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
25     else 0 :: int)"
26
27instance ..
28
29end
30
31lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)"
32  by (simp add: set_bits_int_def)
33
34lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
35  by (auto simp add: set_bits_int_def bl_to_bin_def)
36
37end