--- a/src/HOL/Int.thy Thu Dec 04 11:14:24 2008 -0800
+++ b/src/HOL/Int.thy Thu Dec 04 12:32:38 2008 -0800
@@ -855,7 +855,7 @@
add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
qed
-lemma neg_simps:
+lemma bin_less_0_simps:
"Pls < 0 \<longleftrightarrow> False"
"Min < 0 \<longleftrightarrow> True"
"Bit0 w < 0 \<longleftrightarrow> w < 0"
@@ -908,7 +908,7 @@
less_bin_lemma [of "Bit1 k"]
less_bin_lemma [of "pred Pls"]
less_bin_lemma [of "pred k"]
- by (simp_all add: neg_simps succ_pred)
+ by (simp_all add: bin_less_0_simps succ_pred)
text {* Less-than-or-equal *}
@@ -1187,6 +1187,12 @@
by (auto simp add: iszero_def number_of_eq numeral_simps)
qed
+lemmas iszero_simps =
+ iszero_0 not_iszero_1
+ iszero_number_of_Pls nonzero_number_of_Min
+ iszero_number_of_Bit0 iszero_number_of_Bit1
+(* iszero_number_of_Pls would never normally be used
+ because its lhs simplifies to "iszero 0" *)
subsubsection {* The Less-Than Relation *}
@@ -1248,6 +1254,10 @@
by (simp add: neg_def number_of_eq numeral_simps)
qed
+lemmas neg_simps =
+ not_neg_0 not_neg_1
+ not_neg_number_of_Pls neg_number_of_Min
+ neg_number_of_Bit0 neg_number_of_Bit1
text {* Less-Than or Equals *}
@@ -1315,12 +1325,7 @@
less_number_of less_bin_simps
le_number_of le_bin_simps
eq_number_of eq_bin_simps
- iszero_0 nonzero_number_of_Min
- iszero_number_of_Bit0 iszero_number_of_Bit1
- not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
- neg_number_of_Min neg_number_of_Bit0 neg_number_of_Bit1
-(* iszero_number_of_Pls would never be used
- because its lhs simplifies to "iszero 0" *)
+ iszero_simps neg_simps
subsubsection {* Simplification of arithmetic when nested to the right. *}