author | huffman |
Thu, 19 Feb 2009 12:26:32 -0800 | |
changeset 29995 | 62efbd0ef132 |
parent 29994 | 6ca6b6bd6e15 |
child 29996 | c09f348ca88a |
--- a/src/HOL/Library/Bit.thy Thu Feb 19 12:03:31 2009 -0800 +++ b/src/HOL/Library/Bit.thy Thu Feb 19 12:26:32 2009 -0800 @@ -115,6 +115,9 @@ text {* All numerals reduce to either 0 or 1. *} +lemma bit_minus1 [simp]: "-1 = (1 :: bit)" + by (simp only: number_of_Min uminus_bit_def) + lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)" by (simp only: number_of_Bit0 add_0_left bit_add_self)