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