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