# HG changeset patch # User huffman # Date 1187794546 -7200 # Node ID d9d2aa843a3b0444257b0af69244d43870b9001e # Parent 199bb6d451e554e40df71447609fa57896f3f001 move bool list operations from WordBitwise to WordBoolList diff -r 199bb6d451e5 -r d9d2aa843a3b src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Aug 22 16:54:43 2007 +0200 +++ b/src/HOL/Word/WordBitwise.thy Wed Aug 22 16:55:46 2007 +0200 @@ -7,7 +7,7 @@ header {* Bitwise Operations on Words *} -theory WordBitwise imports WordArith WordBoolList begin +theory WordBitwise imports WordArith begin lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or @@ -201,36 +201,12 @@ lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard] -lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" - unfolding to_bl_def word_log_defs - by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) - -lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)" - unfolding to_bl_def word_log_defs bl_xor_bin - by (simp add: number_of_is_id word_no_wi [symmetric]) - -lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)" - unfolding to_bl_def word_log_defs - by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric]) - -lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)" - unfolding to_bl_def word_log_defs - by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric]) - lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0" by (auto simp: word_test_bit_def word_lsb_def) lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)" unfolding word_lsb_def word_1_no word_0_no by auto -lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)" - apply (unfold word_lsb_def uint_bl bin_to_bl_def) - apply (rule_tac bin="uint w" in bin_exhaust) - apply (cases "size w") - apply auto - apply (auto simp add: bin_to_bl_aux_alt) - done - lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)" unfolding word_lsb_def bin_last_mod by auto @@ -253,40 +229,10 @@ lemmas word_msb_nth = word_msb_nth' [unfolded word_size] -lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)" - apply (unfold word_msb_nth uint_bl) - apply (subst hd_conv_nth) - apply (rule length_greater_0_conv [THEN iffD1]) - apply simp - apply (simp add : nth_bin_to_bl word_size) - done - lemma word_set_nth: "set_bit w n (test_bit w n) = (w::'a::len0 word)" unfolding word_test_bit_def word_set_bit_def by auto -lemma bin_nth_uint': - "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)" - apply (unfold word_size) - apply (safe elim!: bin_nth_uint_imp) - apply (frule bin_nth_uint_imp) - apply (fast dest!: bin_nth_bl)+ - done - -lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size] - -lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)" - unfolding to_bl_def word_test_bit_def word_size - by (rule bin_nth_uint) - -lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)" - apply (unfold test_bit_bl) - apply clarsimp - apply (rule trans) - apply (rule nth_rev_alt) - apply (auto simp add: word_size) - done - lemma test_bit_set: fixes w :: "'a::len0 word" shows "(set_bit w n x) !! n = (n < size w & x)" @@ -303,9 +249,6 @@ simp add: word_test_bit_def [symmetric]) done -lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" - unfolding of_bl_def bl_to_bin_rep_F by auto - lemma msb_nth': fixes w :: "'a::len word" shows "msb w = w !! (size w - 1)" @@ -321,39 +264,6 @@ lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size], standard] lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt] -lemma td_ext_nth': - "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> - td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)" - 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 - -lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] - -interpretation test_bit: - td_ext ["op !! :: 'a::len0 word => nat => bool" - set_bits - "{f. \i. f i \ i < len_of TYPE('a::len0)}" - "(\h i. h i \ i < len_of TYPE('a::len0))"] - by (rule td_ext_nth) - -declare test_bit.Rep' [simp del] -declare test_bit.Rep' [rule del] - -lemmas td_nth = test_bit.td_thm - lemma word_set_set_same: fixes w :: "'a::len0 word" shows "set_bit (set_bit w n x) n y = set_bit w n y" @@ -402,17 +312,9 @@ lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no], simplified if_simps, THEN eq_reflection, standard] -lemma to_bl_n1: - "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True" - apply (rule word_bl.Abs_inverse') - apply simp - apply (rule word_eqI) - apply (clarsimp simp add: word_size test_bit_no) - apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) - done - lemma word_msb_n1: "msb (-1::'a::len word)" - unfolding word_msb_alt word_msb_alt to_bl_n1 by simp + unfolding word_msb_def sint_sbintrunc number_of_is_id bin_sign_lem + by (rule bin_nth_Min) declare word_set_set_same [simp] word_set_nth [simp] test_bit_no [simp] word_set_no [simp] nth_0 [simp] diff -r 199bb6d451e5 -r d9d2aa843a3b src/HOL/Word/WordBoolList.thy --- a/src/HOL/Word/WordBoolList.thy Wed Aug 22 16:54:43 2007 +0200 +++ b/src/HOL/Word/WordBoolList.thy Wed Aug 22 16:55:46 2007 +0200 @@ -5,7 +5,7 @@ header {* Bool Lists and Words *} -theory WordBoolList imports BinBoolList WordArith begin +theory WordBoolList imports BinBoolList WordBitwise begin constdefs of_bl :: "bool list => 'a :: len0 word" @@ -258,4 +258,105 @@ apply (rule bl_to_bin_lt2p) done +subsection "Bitwise operations on bool lists" + +lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" + unfolding to_bl_def word_log_defs + by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric]) + +lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)" + unfolding to_bl_def word_log_defs bl_xor_bin + by (simp add: number_of_is_id word_no_wi [symmetric]) + +lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)" + unfolding to_bl_def word_log_defs + by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric]) + +lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)" + unfolding to_bl_def word_log_defs + by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric]) + +lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)" + apply (unfold word_lsb_def uint_bl bin_to_bl_def) + apply (rule_tac bin="uint w" in bin_exhaust) + apply (cases "size w") + apply auto + apply (auto simp add: bin_to_bl_aux_alt) + done + +lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)" + apply (unfold word_msb_nth uint_bl) + apply (subst hd_conv_nth) + apply (rule length_greater_0_conv [THEN iffD1]) + apply simp + apply (simp add : nth_bin_to_bl word_size) + done + +lemma bin_nth_uint': + "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)" + apply (unfold word_size) + apply (safe elim!: bin_nth_uint_imp) + apply (frule bin_nth_uint_imp) + apply (fast dest!: bin_nth_bl)+ + done + +lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size] + +lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)" + unfolding to_bl_def word_test_bit_def word_size + by (rule bin_nth_uint) + +lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)" + apply (unfold test_bit_bl) + apply clarsimp + apply (rule trans) + apply (rule nth_rev_alt) + apply (auto simp add: word_size) + done + +lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" + unfolding of_bl_def bl_to_bin_rep_F by auto + +lemma td_ext_nth': + "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> + td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)" + 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 + +lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] + +interpretation test_bit: + td_ext ["op !! :: 'a::len0 word => nat => bool" + set_bits + "{f. \i. f i \ i < len_of TYPE('a::len0)}" + "(\h i. h i \ i < len_of TYPE('a::len0))"] + by (rule td_ext_nth) + +declare test_bit.Rep' [simp del] +declare test_bit.Rep' [rule del] + +lemmas td_nth = test_bit.td_thm + +lemma to_bl_n1: + "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True" + apply (rule word_bl.Abs_inverse') + apply simp + apply (rule word_eqI) + apply (clarsimp simp add: word_size test_bit_no) + apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) + done + end \ No newline at end of file diff -r 199bb6d451e5 -r d9d2aa843a3b src/HOL/Word/WordShift.thy --- a/src/HOL/Word/WordShift.thy Wed Aug 22 16:54:43 2007 +0200 +++ b/src/HOL/Word/WordShift.thy Wed Aug 22 16:55:46 2007 +0200 @@ -7,7 +7,7 @@ header {* Shifting, Rotating, and Splitting Words *} -theory WordShift imports WordBitwise begin +theory WordShift imports WordBitwise WordBoolList begin subsection "Bit shifting"