# HG changeset patch
# User huffman
# Date 1228371380 28800
# Node ID a4f3db5d139390c98a25466941c7d6296a1719a1
# Parent  3bdb1eae352c25a2fc84920ccaeca1c28128646b
change some lemmas to avoid using iszero

diff -r 3bdb1eae352c -r a4f3db5d1393 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Wed Dec 03 21:50:36 2008 -0800
+++ b/src/HOL/NatBin.thy	Wed Dec 03 22:16:20 2008 -0800
@@ -441,13 +441,11 @@
 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
 
 lemma eq_number_of_0 [simp]:
-     "(number_of v = (0::nat)) =  
-      (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] iszero_0)
+  "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"  
+  unfolding nat_number_of_def number_of_is_id by auto
 
 lemma eq_0_number_of [simp]:
-     "((0::nat) = number_of v) =  
-      (if neg (number_of v :: int) then True else iszero (number_of v :: int))"
+  "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"  
 by (rule trans [OF eq_sym_conv eq_number_of_0])
 
 lemma less_0_number_of [simp]:
@@ -656,13 +654,9 @@
   "number_of (Int.Bit1 w) =
     (if neg (number_of w :: int) then 0
      else let n = number_of w in Suc (n + n))"
-  apply (simp only: nat_number_of_def Let_def split: split_if)
-  apply (intro conjI impI)
-   apply (simp add: neg_nat neg_number_of_Bit1)
-  apply (rule int_int_eq [THEN iffD1])
-  apply (simp only: not_neg_nat neg_number_of_Bit1 int_Suc zadd_int [symmetric] simp_thms)
-  apply (simp only: number_of_Bit1 zadd_assoc)
-  done
+  unfolding nat_number_of_def number_of_Bit1
+  unfolding number_of_is_id neg_def Let_def
+  by auto
 
 lemmas nat_number =
   nat_number_of_Pls nat_number_of_Min
@@ -708,7 +702,8 @@
          (if neg (number_of v :: int) then number_of v' + k  
           else if neg (number_of v' :: int) then number_of v + k  
           else number_of (v + v') + k)"
-by simp
+  unfolding nat_number_of_def number_of_is_id neg_def
+  by auto
 
 lemma nat_number_of_mult_left:
      "number_of v * (number_of v' * (k::nat)) =