src/HOL/Library/Bit.thy
changeset 54489 03ff4d1e6784
parent 53063 8f7ac535892f
child 55416 dd7992d4a61a
equal deleted inserted replaced
54488:b60f1fab408c 54489:03ff4d1e6784
   145 
   145 
   146 subsection {* Numerals at type @{typ bit} *}
   146 subsection {* Numerals at type @{typ bit} *}
   147 
   147 
   148 text {* All numerals reduce to either 0 or 1. *}
   148 text {* All numerals reduce to either 0 or 1. *}
   149 
   149 
   150 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
   150 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   151   by (simp only: minus_one [symmetric] uminus_bit_def)
   151   by (simp only: uminus_bit_def)
   152 
   152 
   153 lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
   153 lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
   154   by (simp only: neg_numeral_def uminus_bit_def)
   154   by (simp only: uminus_bit_def)
   155 
   155 
   156 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   156 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   157   by (simp only: numeral_Bit0 bit_add_self)
   157   by (simp only: numeral_Bit0 bit_add_self)
   158 
   158 
   159 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   159 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"