# HG changeset patch
# User huffman
# Date 1329997500 -3600
# Node ID 83a5160e6b4dab3c8901b61467a08e1031e19ded
# Parent  c71f3e9367bb0c0fa2946a55065c69b6843aed8f
removed unnecessary lemma zero_bintrunc

diff -r c71f3e9367bb -r 83a5160e6b4d src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Feb 23 12:24:34 2012 +0100
+++ b/src/HOL/Word/Word.thy	Thu Feb 23 12:45:00 2012 +0100
@@ -1645,16 +1645,6 @@
 
 subsection "Arithmetic type class instantiations"
 
-(* note that iszero_def is only for class comm_semiring_1_cancel,
-   which requires word length >= 1, ie 'a :: len word *) 
-lemma zero_bintrunc:
-  "iszero (number_of x :: 'a :: len word) = 
-    (bintrunc (len_of TYPE('a)) x = Int.Pls)"
-  apply (unfold iszero_def word_0_wi word_no_wi)
-  apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
-  apply (simp add : Pls_def [symmetric])
-  done
-
 lemmas word_le_0_iff [simp] =
   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
 
@@ -1662,14 +1652,14 @@
   "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   by (simp add: of_nat_nat word_of_int)
 
-lemma iszero_word_no [simp] : 
+(* note that iszero_def is only for class comm_semiring_1_cancel,
+   which requires word length >= 1, ie 'a :: len word *) 
+lemma iszero_word_no [simp]:
   "iszero (number_of bin :: 'a :: len word) = 
     iszero (bintrunc (len_of TYPE('a)) (number_of bin))"
-  apply (simp add: zero_bintrunc number_of_is_id)
-  apply (unfold iszero_def Pls_def)
-  apply (rule refl)
-  done
-    
+  using word_ubin.norm_eq_iff [where 'a='a, of "number_of bin" 0]
+  by (simp add: iszero_def [symmetric])
+
 
 subsection "Word and nat"