--- /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
--- 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
--- 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)
--- 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)