# HG changeset patch
# User haftmann
# Date 1555925635 0
# Node ID b4bf82ed0ad5acfd85b8825c75d4b1fad38e86ef
# Parent  bdc835d934b78d991eaca13a5c4166cf0d5cc4f2
separate type class for bit comprehension

diff -r bdc835d934b7 -r b4bf82ed0ad5 src/HOL/Word/Bit_Comprehension.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bit_Comprehension.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -0,0 +1,37 @@
+(*  Title:      HOL/Word/Bit_Comprehension.thy
+    Author:     Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA
+*)
+
+section \<open>Comprehension syntax for bit expressions\<close>
+
+theory Bit_Comprehension
+  imports Bits_Int
+begin
+
+class bit_comprehension = bit_operations +
+  fixes set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
+
+instantiation int :: bit_comprehension
+begin
+
+definition
+  "set_bits f =
+    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+      in bl_to_bin (rev (map f [0..<n]))
+     else if \<exists>n. \<forall>n'\<ge>n. f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. f n'
+      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+     else 0 :: int)"
+
+instance ..
+
+end
+
+lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)"
+  by (simp add: set_bits_int_def)
+
+lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
+  by (auto simp add: set_bits_int_def bl_to_bin_def)
+
+end
\ No newline at end of file
diff -r bdc835d934b7 -r b4bf82ed0ad5 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Bits.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Word/Bits.thy
-    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
+    Author:     Brian Huffman, PSU and Gerwin Klein, NICTA
 *)
 
 section \<open>Syntactic type classes for bit operations\<close>
@@ -19,7 +19,6 @@
     and lsb :: "'a \<Rightarrow> bool"
     and msb :: "'a \<Rightarrow> bool"
     and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
-    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
 
 text \<open>
   We want the bitwise operations to bind slightly weaker
diff -r bdc835d934b7 -r b4bf82ed0ad5 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -1290,16 +1290,6 @@
 
 definition "set_bit i n b = bin_sc n b i"
 
-definition
-  "set_bits f =
-    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-      in bl_to_bin (rev (map f [0..<n]))
-     else if \<exists>n. \<forall>n'\<ge>n. f n' then
-      let n = LEAST n. \<forall>n'\<ge>n. f n'
-      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
-     else 0 :: int)"
-
 definition "shiftl x n = x * 2 ^ n" for x :: int
 
 definition "shiftr x n = x div 2 ^ n" for x :: int
@@ -2175,12 +2165,6 @@
   "bin_sc n True i = i OR (1 << n)"
 by(induct n arbitrary: i)(auto intro: bin_rl_eqI)
 
-lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
-  by (auto simp add: set_bits_int_def bl_to_bin_def)
-
-lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)"
-  by (simp add: set_bits_int_def)
-
 lemma msb_conv_bin_sign: "msb x \<longleftrightarrow> bin_sign x = -1"
 by(simp add: bin_sign_def not_le msb_int_def)
 
diff -r bdc835d934b7 -r b4bf82ed0ad5 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Apr 22 09:33:55 2019 +0000
+++ b/src/HOL/Word/Word.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -10,6 +10,7 @@
   "HOL-Library.Boolean_Algebra"
   Bits_Int
   Bits_Bit
+  Bit_Comprehension
   Misc_Typedef
   Misc_Arithmetic
 begin
@@ -384,8 +385,6 @@
 
 definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
 
-definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
-
 definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
 
 definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
@@ -480,8 +479,6 @@
   \<comment> \<open>Largest representable machine integer.\<close>
   where "max_word = word_of_int (2 ^ LENGTH('a) - 1)"
 
-lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
-
 
 subsection \<open>Theorems about typedefs\<close>
 
@@ -2429,36 +2426,6 @@
 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
 
-lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
-  "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
-    td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
-  for w :: "'a::len0 word"
-  apply (unfold word_size td_ext_def')
-  apply safe
-     apply (rule_tac [3] ext)
-     apply (rule_tac [4] ext)
-     apply (unfold word_size of_nth_def test_bit_bl)
-     apply safe
-       defer
-       apply (clarsimp simp: word_bl.Abs_inverse)+
-  apply (rule word_bl.Rep_inverse')
-  apply (rule sym [THEN trans])
-   apply (rule bl_of_nth_nth)
-  apply simp
-  apply (rule bl_of_nth_inj)
-  apply (clarsimp simp add : test_bit_bl word_size)
-  done
-
-interpretation test_bit:
-  td_ext
-    "(!!) :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool"
-    set_bits
-    "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len0)}"
-    "(\<lambda>h i. h i \<and> i < LENGTH('a::len0))"
-  by (rule td_ext_nth)
-
-lemmas td_nth = test_bit.td_thm
-
 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
   for w :: "'a::len0 word"
   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
@@ -2606,6 +2573,54 @@
   by (simp add: bl_word_not rev_map)
 
 
+subsection \<open>Bit comprehension\<close>
+
+instantiation word :: (len0) bit_comprehension
+begin
+
+definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
+
+instance ..
+
+end
+
+lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
+
+lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
+  "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
+    td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
+  for w :: "'a::len0 word"
+  apply (unfold word_size td_ext_def')
+  apply safe
+     apply (rule_tac [3] ext)
+     apply (rule_tac [4] ext)
+     apply (unfold word_size of_nth_def test_bit_bl)
+     apply safe
+       defer
+       apply (clarsimp simp: word_bl.Abs_inverse)+
+  apply (rule word_bl.Rep_inverse')
+  apply (rule sym [THEN trans])
+   apply (rule bl_of_nth_nth)
+  apply simp
+  apply (rule bl_of_nth_inj)
+  apply (clarsimp simp add : test_bit_bl word_size)
+  done
+
+interpretation test_bit:
+  td_ext
+    "(!!) :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool"
+    set_bits
+    "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len0)}"
+    "(\<lambda>h i. h i \<and> i < LENGTH('a::len0))"
+  by (rule td_ext_nth)
+
+lemmas td_nth = test_bit.td_thm
+
+lemma set_bits_K_False [simp]:
+  "set_bits (\<lambda>_. False) = (0 :: 'a :: len0 word)"
+  by (rule word_eqI) (simp add: test_bit.eq_norm)
+
+
 subsection \<open>Shifting, Rotating, and Splitting Words\<close>
 
 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
@@ -4517,10 +4532,6 @@
 
 subsection \<open>More\<close>
 
-lemma set_bits_K_False [simp]:
-  "set_bits (\<lambda>_. False) = (0 :: 'a :: len0 word)"
-  by (rule word_eqI) (simp add: test_bit.eq_norm)
-
 lemma test_bit_1' [simp]:
   "(1 :: 'a :: len0 word) !! n \<longleftrightarrow> 0 < LENGTH('a) \<and> n = 0"
   by (cases n) (simp_all only: one_word_def test_bit_wi bin_nth.simps, simp_all)