# HG changeset patch
# User huffman
# Date 1228422758 28800
# Node ID af325cd29b1545fb8ef6fc2ac5a87c5fa7bda90e
# Parent  060832a1f0876d425292be43d8b16c3a995f3fe3
add named lemma lists: neg_simps and iszero_simps

diff -r 060832a1f087 -r af325cd29b15 src/HOL/Int.thy
--- 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. *}