# HG changeset patch
# User huffman
# Date 1235075192 28800
# Node ID 62efbd0ef132b04ffd23f48f4c71e3f71829df7b
# Parent  6ca6b6bd6e151637edf22de3c59bb3662ec00db7
add rule for minus 1 at type bit

diff -r 6ca6b6bd6e15 -r 62efbd0ef132 src/HOL/Library/Bit.thy
--- 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)