1.1 --- a/src/HOL/Word/WordBitwise.thy Wed Aug 22 16:54:43 2007 +0200
1.2 +++ b/src/HOL/Word/WordBitwise.thy Wed Aug 22 16:55:46 2007 +0200
1.3 @@ -7,7 +7,7 @@
1.4
1.5 header {* Bitwise Operations on Words *}
1.6
1.7 -theory WordBitwise imports WordArith WordBoolList begin
1.8 +theory WordBitwise imports WordArith begin
1.9
1.10 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
1.11
1.12 @@ -201,36 +201,12 @@
1.13 lemmas word_and_le2 =
1.14 xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2, standard]
1.15
1.16 -lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
1.17 - unfolding to_bl_def word_log_defs
1.18 - by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric])
1.19 -
1.20 -lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)"
1.21 - unfolding to_bl_def word_log_defs bl_xor_bin
1.22 - by (simp add: number_of_is_id word_no_wi [symmetric])
1.23 -
1.24 -lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)"
1.25 - unfolding to_bl_def word_log_defs
1.26 - by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
1.27 -
1.28 -lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)"
1.29 - unfolding to_bl_def word_log_defs
1.30 - by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
1.31 -
1.32 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
1.33 by (auto simp: word_test_bit_def word_lsb_def)
1.34
1.35 lemma word_lsb_1_0: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
1.36 unfolding word_lsb_def word_1_no word_0_no by auto
1.37
1.38 -lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
1.39 - apply (unfold word_lsb_def uint_bl bin_to_bl_def)
1.40 - apply (rule_tac bin="uint w" in bin_exhaust)
1.41 - apply (cases "size w")
1.42 - apply auto
1.43 - apply (auto simp add: bin_to_bl_aux_alt)
1.44 - done
1.45 -
1.46 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
1.47 unfolding word_lsb_def bin_last_mod by auto
1.48
1.49 @@ -253,40 +229,10 @@
1.50
1.51 lemmas word_msb_nth = word_msb_nth' [unfolded word_size]
1.52
1.53 -lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
1.54 - apply (unfold word_msb_nth uint_bl)
1.55 - apply (subst hd_conv_nth)
1.56 - apply (rule length_greater_0_conv [THEN iffD1])
1.57 - apply simp
1.58 - apply (simp add : nth_bin_to_bl word_size)
1.59 - done
1.60 -
1.61 lemma word_set_nth:
1.62 "set_bit w n (test_bit w n) = (w::'a::len0 word)"
1.63 unfolding word_test_bit_def word_set_bit_def by auto
1.64
1.65 -lemma bin_nth_uint':
1.66 - "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
1.67 - apply (unfold word_size)
1.68 - apply (safe elim!: bin_nth_uint_imp)
1.69 - apply (frule bin_nth_uint_imp)
1.70 - apply (fast dest!: bin_nth_bl)+
1.71 - done
1.72 -
1.73 -lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
1.74 -
1.75 -lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
1.76 - unfolding to_bl_def word_test_bit_def word_size
1.77 - by (rule bin_nth_uint)
1.78 -
1.79 -lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
1.80 - apply (unfold test_bit_bl)
1.81 - apply clarsimp
1.82 - apply (rule trans)
1.83 - apply (rule nth_rev_alt)
1.84 - apply (auto simp add: word_size)
1.85 - done
1.86 -
1.87 lemma test_bit_set:
1.88 fixes w :: "'a::len0 word"
1.89 shows "(set_bit w n x) !! n = (n < size w & x)"
1.90 @@ -303,9 +249,6 @@
1.91 simp add: word_test_bit_def [symmetric])
1.92 done
1.93
1.94 -lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
1.95 - unfolding of_bl_def bl_to_bin_rep_F by auto
1.96 -
1.97 lemma msb_nth':
1.98 fixes w :: "'a::len word"
1.99 shows "msb w = w !! (size w - 1)"
1.100 @@ -321,39 +264,6 @@
1.101 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size], standard]
1.102 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
1.103
1.104 -lemma td_ext_nth':
1.105 - "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==>
1.106 - td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
1.107 - apply (unfold word_size td_ext_def')
1.108 - apply safe
1.109 - apply (rule_tac [3] ext)
1.110 - apply (rule_tac [4] ext)
1.111 - apply (unfold word_size of_nth_def test_bit_bl)
1.112 - apply safe
1.113 - defer
1.114 - apply (clarsimp simp: word_bl.Abs_inverse)+
1.115 - apply (rule word_bl.Rep_inverse')
1.116 - apply (rule sym [THEN trans])
1.117 - apply (rule bl_of_nth_nth)
1.118 - apply simp
1.119 - apply (rule bl_of_nth_inj)
1.120 - apply (clarsimp simp add : test_bit_bl word_size)
1.121 - done
1.122 -
1.123 -lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
1.124 -
1.125 -interpretation test_bit:
1.126 - td_ext ["op !! :: 'a::len0 word => nat => bool"
1.127 - set_bits
1.128 - "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
1.129 - "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
1.130 - by (rule td_ext_nth)
1.131 -
1.132 -declare test_bit.Rep' [simp del]
1.133 -declare test_bit.Rep' [rule del]
1.134 -
1.135 -lemmas td_nth = test_bit.td_thm
1.136 -
1.137 lemma word_set_set_same:
1.138 fixes w :: "'a::len0 word"
1.139 shows "set_bit (set_bit w n x) n y = set_bit w n y"
1.140 @@ -402,17 +312,9 @@
1.141 lemmas clearBit_no = clearBit_def [THEN trans [OF meta_eq_to_obj_eq word_set_no],
1.142 simplified if_simps, THEN eq_reflection, standard]
1.143
1.144 -lemma to_bl_n1:
1.145 - "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
1.146 - apply (rule word_bl.Abs_inverse')
1.147 - apply simp
1.148 - apply (rule word_eqI)
1.149 - apply (clarsimp simp add: word_size test_bit_no)
1.150 - apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
1.151 - done
1.152 -
1.153 lemma word_msb_n1: "msb (-1::'a::len word)"
1.154 - unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
1.155 + unfolding word_msb_def sint_sbintrunc number_of_is_id bin_sign_lem
1.156 + by (rule bin_nth_Min)
1.157
1.158 declare word_set_set_same [simp] word_set_nth [simp]
1.159 test_bit_no [simp] word_set_no [simp] nth_0 [simp]
2.1 --- a/src/HOL/Word/WordBoolList.thy Wed Aug 22 16:54:43 2007 +0200
2.2 +++ b/src/HOL/Word/WordBoolList.thy Wed Aug 22 16:55:46 2007 +0200
2.3 @@ -5,7 +5,7 @@
2.4
2.5 header {* Bool Lists and Words *}
2.6
2.7 -theory WordBoolList imports BinBoolList WordArith begin
2.8 +theory WordBoolList imports BinBoolList WordBitwise begin
2.9
2.10 constdefs
2.11 of_bl :: "bool list => 'a :: len0 word"
2.12 @@ -258,4 +258,105 @@
2.13 apply (rule bl_to_bin_lt2p)
2.14 done
2.15
2.16 +subsection "Bitwise operations on bool lists"
2.17 +
2.18 +lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
2.19 + unfolding to_bl_def word_log_defs
2.20 + by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric])
2.21 +
2.22 +lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)"
2.23 + unfolding to_bl_def word_log_defs bl_xor_bin
2.24 + by (simp add: number_of_is_id word_no_wi [symmetric])
2.25 +
2.26 +lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)"
2.27 + unfolding to_bl_def word_log_defs
2.28 + by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
2.29 +
2.30 +lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)"
2.31 + unfolding to_bl_def word_log_defs
2.32 + by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
2.33 +
2.34 +lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
2.35 + apply (unfold word_lsb_def uint_bl bin_to_bl_def)
2.36 + apply (rule_tac bin="uint w" in bin_exhaust)
2.37 + apply (cases "size w")
2.38 + apply auto
2.39 + apply (auto simp add: bin_to_bl_aux_alt)
2.40 + done
2.41 +
2.42 +lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
2.43 + apply (unfold word_msb_nth uint_bl)
2.44 + apply (subst hd_conv_nth)
2.45 + apply (rule length_greater_0_conv [THEN iffD1])
2.46 + apply simp
2.47 + apply (simp add : nth_bin_to_bl word_size)
2.48 + done
2.49 +
2.50 +lemma bin_nth_uint':
2.51 + "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
2.52 + apply (unfold word_size)
2.53 + apply (safe elim!: bin_nth_uint_imp)
2.54 + apply (frule bin_nth_uint_imp)
2.55 + apply (fast dest!: bin_nth_bl)+
2.56 + done
2.57 +
2.58 +lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
2.59 +
2.60 +lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
2.61 + unfolding to_bl_def word_test_bit_def word_size
2.62 + by (rule bin_nth_uint)
2.63 +
2.64 +lemma to_bl_nth: "n < size w ==> to_bl w ! n = w !! (size w - Suc n)"
2.65 + apply (unfold test_bit_bl)
2.66 + apply clarsimp
2.67 + apply (rule trans)
2.68 + apply (rule nth_rev_alt)
2.69 + apply (auto simp add: word_size)
2.70 + done
2.71 +
2.72 +lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
2.73 + unfolding of_bl_def bl_to_bin_rep_F by auto
2.74 +
2.75 +lemma td_ext_nth':
2.76 + "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==>
2.77 + td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
2.78 + apply (unfold word_size td_ext_def')
2.79 + apply safe
2.80 + apply (rule_tac [3] ext)
2.81 + apply (rule_tac [4] ext)
2.82 + apply (unfold word_size of_nth_def test_bit_bl)
2.83 + apply safe
2.84 + defer
2.85 + apply (clarsimp simp: word_bl.Abs_inverse)+
2.86 + apply (rule word_bl.Rep_inverse')
2.87 + apply (rule sym [THEN trans])
2.88 + apply (rule bl_of_nth_nth)
2.89 + apply simp
2.90 + apply (rule bl_of_nth_inj)
2.91 + apply (clarsimp simp add : test_bit_bl word_size)
2.92 + done
2.93 +
2.94 +lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size]
2.95 +
2.96 +interpretation test_bit:
2.97 + td_ext ["op !! :: 'a::len0 word => nat => bool"
2.98 + set_bits
2.99 + "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
2.100 + "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"]
2.101 + by (rule td_ext_nth)
2.102 +
2.103 +declare test_bit.Rep' [simp del]
2.104 +declare test_bit.Rep' [rule del]
2.105 +
2.106 +lemmas td_nth = test_bit.td_thm
2.107 +
2.108 +lemma to_bl_n1:
2.109 + "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
2.110 + apply (rule word_bl.Abs_inverse')
2.111 + apply simp
2.112 + apply (rule word_eqI)
2.113 + apply (clarsimp simp add: word_size test_bit_no)
2.114 + apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
2.115 + done
2.116 +
2.117 end
2.118 \ No newline at end of file
3.1 --- a/src/HOL/Word/WordShift.thy Wed Aug 22 16:54:43 2007 +0200
3.2 +++ b/src/HOL/Word/WordShift.thy Wed Aug 22 16:55:46 2007 +0200
3.3 @@ -7,7 +7,7 @@
3.4
3.5 header {* Shifting, Rotating, and Splitting Words *}
3.6
3.7 -theory WordShift imports WordBitwise begin
3.8 +theory WordShift imports WordBitwise WordBoolList begin
3.9
3.10 subsection "Bit shifting"
3.11