# HG changeset patch
# User huffman
# Date 1228418064 28800
# Node ID 060832a1f0876d425292be43d8b16c3a995f3fe3
# Parent  1c743f58781af2f6873ec273d0e8c1d234c78729
change arith_special simps to avoid using neg

diff -r 1c743f58781a -r 060832a1f087 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Dec 04 09:12:41 2008 -0800
+++ b/src/HOL/Int.thy	Thu Dec 04 11:14:24 2008 -0800
@@ -1581,17 +1581,17 @@
 
 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
 lemmas less_special =
-  binop_eq [of "op <", OF less_number_of_eq_neg numeral_0_eq_0 refl, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg numeral_1_eq_1 refl, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_0_eq_0, standard]
-  binop_eq [of "op <", OF less_number_of_eq_neg refl numeral_1_eq_1, standard]
+  binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
+  binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
+  binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
+  binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
 
 text{*Allow 0 or 1 on either side with a binary numeral on the other*}
 lemmas le_special =
-    binop_eq [of "op \<le>", OF le_number_of_eq numeral_0_eq_0 refl, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq numeral_1_eq_1 refl, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_0_eq_0, standard]
-    binop_eq [of "op \<le>", OF le_number_of_eq refl numeral_1_eq_1, standard]
+    binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
+    binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
+    binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
+    binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
 
 lemmas arith_special[simp] = 
        add_special diff_special eq_special less_special le_special
diff -r 1c743f58781a -r 060832a1f087 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Thu Dec 04 09:12:41 2008 -0800
+++ b/src/HOL/NatBin.thy	Thu Dec 04 11:14:24 2008 -0800
@@ -111,8 +111,8 @@
      "int (number_of v) =  
          (if neg (number_of v :: int) then 0  
           else (number_of v :: int))"
-by (simp del: nat_number_of
-	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by simp
 
 
 subsubsection{*Successor *}
@@ -124,10 +124,9 @@
 
 lemma Suc_nat_number_of_add:
      "Suc (number_of v + n) =  
-        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)" 
-by (simp del: nat_number_of 
-         add: nat_number_of_def neg_nat
-              Suc_nat_eq_nat_zadd1 number_of_succ) 
+        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)"
+  unfolding nat_number_of_def number_of_is_id neg_def numeral_simps
+  by (simp add: Suc_nat_eq_nat_zadd1 add_ac)
 
 lemma Suc_nat_number_of [simp]:
      "Suc (number_of v) =  
@@ -145,7 +144,8 @@
          (if neg (number_of v :: int) then number_of v'  
           else if neg (number_of v' :: int) then number_of v  
           else number_of (v + v'))"
-by (simp add: neg_nat nat_number_of_def nat_add_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_add_distrib)
 
 
 subsubsection{*Subtraction *}
@@ -172,7 +172,8 @@
 lemma mult_nat_number_of [simp]:
      "(number_of v :: nat) * number_of v' =  
        (if neg (number_of v :: int) then 0 else number_of (v * v'))"
-by (simp add: neg_nat nat_number_of_def nat_mult_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mult_distrib)
 
 
 subsubsection{*Quotient *}
@@ -181,7 +182,8 @@
      "(number_of v :: nat)  div  number_of v' =  
           (if neg (number_of v :: int) then 0  
            else nat (number_of v div number_of v'))"
-by (simp add: neg_nat nat_number_of_def nat_div_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_div_distrib)
 
 lemma one_div_nat_number_of [simp]:
      "Suc 0 div number_of v' = nat (1 div number_of v')" 
@@ -195,7 +197,8 @@
         (if neg (number_of v :: int) then 0  
          else if neg (number_of v' :: int) then number_of v  
          else nat (number_of v mod number_of v'))"
-by (simp add: neg_nat nat_number_of_def nat_mod_distrib [symmetric] del: nat_number_of)
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by (simp add: nat_mod_distrib)
 
 lemma one_mod_nat_number_of [simp]:
      "Suc 0 mod number_of v' =