equal
deleted
inserted
replaced
113 |
113 |
114 end |
114 end |
115 |
115 |
116 text {* All numerals reduce to either 0 or 1. *} |
116 text {* All numerals reduce to either 0 or 1. *} |
117 |
117 |
|
118 lemma bit_minus1 [simp]: "-1 = (1 :: bit)" |
|
119 by (simp only: number_of_Min uminus_bit_def) |
|
120 |
118 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)" |
121 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)" |
119 by (simp only: number_of_Bit0 add_0_left bit_add_self) |
122 by (simp only: number_of_Bit0 add_0_left bit_add_self) |
120 |
123 |
121 lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)" |
124 lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)" |
122 by (simp only: number_of_Bit1 add_assoc bit_add_self |
125 by (simp only: number_of_Bit1 add_assoc bit_add_self |