# HG changeset patch # User haftmann # Date 1207309226 -7200 # Node ID 799983936aad1c33affb97a379e54df36487b0d5 # Parent 7fcc10088e727533714e906d529b9fe88856cb94 syntactic classes for bit operations diff -r 7fcc10088e72 -r 799983936aad src/HOL/Word/BitSyntax.thy --- a/src/HOL/Word/BitSyntax.thy Fri Apr 04 13:40:25 2008 +0200 +++ b/src/HOL/Word/BitSyntax.thy Fri Apr 04 13:40:26 2008 +0200 @@ -6,17 +6,17 @@ *) -header {* Syntactic class for bitwise operations *} +header {* Syntactic classes for bitwise operations *} theory BitSyntax -imports Main Num_Lemmas +imports BinGeneral begin class bit = type + - fixes bitNOT :: "'a \ 'a" - and bitAND :: "'a \ 'a \ 'a" - and bitOR :: "'a \ 'a \ 'a" - and bitXOR :: "'a \ 'a \ 'a" + fixes bitNOT :: "'a \ 'a" ("NOT _" [70] 71) + and bitAND :: "'a \ 'a \ 'a" (infixr "AND" 64) + and bitOR :: "'a \ 'a \ 'a" (infixr "OR" 59) + and bitXOR :: "'a \ 'a \ 'a" (infixr "XOR" 59) text {* We want the bitwise operations to bind slightly weaker @@ -24,23 +24,20 @@ bind slightly stronger than @{text "*"}. *} -notation - bitNOT ("NOT _" [70] 71) and - bitAND (infixr "AND" 64) and - bitOR (infixr "OR" 59) and - bitXOR (infixr "XOR" 59) - text {* Testing and shifting operations. *} -consts - test_bit :: "'a::bit \ nat \ bool" (infixl "!!" 100) - lsb :: "'a::bit \ bool" - msb :: "'a::bit \ bool" - set_bit :: "'a::bit \ nat \ bool \ 'a" - set_bits :: "(nat \ bool) \ 'a::bit" (binder "BITS " 10) - shiftl :: "'a::bit \ nat \ 'a" (infixl "<<" 55) - shiftr :: "'a::bit \ nat \ 'a" (infixl ">>" 55) + +class bits = bit + + fixes test_bit :: "'a \ nat \ bool" (infixl "!!" 100) + and lsb :: "'a \ bool" + and set_bit :: "'a \ nat \ bool \ 'a" + and set_bits :: "(nat \ bool) \ 'a" (binder "BITS " 10) + and shiftl :: "'a \ nat \ 'a" (infixl "<<" 55) + and shiftr :: "'a \ nat \ 'a" (infixl ">>" 55) + +class bitss = bits + + fixes msb :: "'a \ bool" subsection {* Bitwise operations on @{typ bit} *} @@ -48,33 +45,28 @@ instantiation bit :: bit begin -definition - NOT_bit_def: "NOT x = (case x of bit.B0 \ bit.B1 | bit.B1 \ bit.B0)" +primrec bitNOT_bit where + "NOT bit.B0 = bit.B1" + | "NOT bit.B1 = bit.B0" -definition - AND_bit_def: "x AND y = (case x of bit.B0 \ bit.B0 | bit.B1 \ y)" +primrec bitAND_bit where + "bit.B0 AND y = bit.B0" + | "bit.B1 AND y = y" -definition - OR_bit_def: "(x OR y \ bit) = NOT (NOT x AND NOT y)" +primrec bitOR_bit where + "bit.B0 OR y = y" + | "bit.B1 OR y = bit.B1" -definition - XOR_bit_def: "(x XOR y \ bit) = (x AND NOT y) OR (NOT x AND y)" +primrec bitXOR_bit where + "bit.B0 XOR y = y" + | "bit.B1 XOR y = NOT y" instance .. end -lemma bit_simps [simp]: - "NOT bit.B0 = bit.B1" - "NOT bit.B1 = bit.B0" - "bit.B0 AND y = bit.B0" - "bit.B1 AND y = y" - "bit.B0 OR y = y" - "bit.B1 OR y = bit.B1" - "bit.B0 XOR y = y" - "bit.B1 XOR y = NOT y" - by (simp_all add: NOT_bit_def AND_bit_def OR_bit_def - XOR_bit_def split: bit.split) +lemmas bit_simps = + bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps lemma bit_extra_simps [simp]: "x AND bit.B0 = bit.B0" diff -r 7fcc10088e72 -r 799983936aad src/HOL/Word/WordDefinition.thy --- a/src/HOL/Word/WordDefinition.thy Fri Apr 04 13:40:25 2008 +0200 +++ b/src/HOL/Word/WordDefinition.thy Fri Apr 04 13:40:26 2008 +0200 @@ -8,7 +8,9 @@ header {* Definition of Word Type *} -theory WordDefinition imports Size BinBoolList TdThs begin +theory WordDefinition +imports Size BinBoolList TdThs +begin typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto @@ -97,9 +99,8 @@ declare uint_def [code func del] lemma [code func]: "uint (word_of_int w \ 'a\len0 word) = bintrunc (len_of TYPE('a)) w" - unfolding uint_def word_of_int_def - apply (rule Abs_word_inverse) - using range_bintrunc by auto + by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse) + (insert range_bintrunc, auto) instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}" begin @@ -187,25 +188,54 @@ "(x bin_last (uint a) = bit.B1" + +definition shiftl1 :: "'a word \ 'a word" where + "shiftl1 w = word_of_int (uint w BIT bit.B0)" + +definition shiftr1 :: "'a word \ 'a word" where + -- "shift right as unsigned or as signed, ie logical or arithmetic" + "shiftr1 w = word_of_int (bin_rest (uint w))" + +definition + shiftl_def: "w << n = (shiftl1 ^ n) w" - word_lsb_def: - "lsb (a::'a::len0 word) == bin_last (uint a) = bit.B1" +definition + shiftr_def: "w >> n = (shiftr1 ^ n) w" + +instance .. + +end +instantiation word :: (len) bitss +begin + +definition word_msb_def: - "msb (a::'a::len word) == bin_sign (sint a) = Int.Min" + "msb a \ bin_sign (sint a) = Int.Min" +instance .. + +end constdefs setBit :: "'a :: len0 word => nat => 'a word" @@ -218,13 +248,6 @@ subsection "Shift operations" constdefs - shiftl1 :: "'a :: len0 word => 'a word" - "shiftl1 w == word_of_int (uint w BIT bit.B0)" - - -- "shift right as unsigned or as signed, ie logical or arithmetic" - shiftr1 :: "'a :: len0 word => 'a word" - "shiftr1 w == word_of_int (bin_rest (uint w))" - sshiftr1 :: "'a :: len word => 'a word" "sshiftr1 w == word_of_int (bin_rest (sint w))" @@ -247,11 +270,6 @@ "slice n w == slice1 (size w - n) w" -defs (overloaded) - shiftl_def: "(w::'a::len0 word) << n == (shiftl1 ^ n) w" - shiftr_def: "(w::'a::len0 word) >> n == (shiftr1 ^ n) w" - - subsection "Rotation" constdefs @@ -304,7 +322,6 @@ "of_bool True = 1" - lemmas of_nth_def = word_set_bits_def lemmas word_size_gt_0 [iff] = @@ -936,7 +953,7 @@ lemmas ucast_down_bl = ucast_down_bl' [OF refl] lemmas slice_def' = slice_def [unfolded word_size] -lemmas test_bit_def' = word_test_bit_def [THEN meta_eq_to_obj_eq, THEN fun_cong] +lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def lemmas word_log_bin_defs = word_log_defs