# HG changeset patch
# User huffman
# Date 1325093583 -3600
# Node ID 0a29b51f0b0d8e2c4f1d6c9f861fee9c5fbd4b70
# Parent  507331bd8a0883e3fae25d93f63915bce7ccc4db
restate lemma word_1_no in terms of Numeral1

diff -r 507331bd8a08 -r 0a29b51f0b0d src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Dec 28 18:27:34 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Dec 28 18:33:03 2011 +0100
@@ -1091,12 +1091,8 @@
 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
   by (simp add: word_number_of_alt)
 
-lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
-  unfolding Pls_def Bit_def by auto
-
-lemma word_1_no: 
-  "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
-  unfolding word_1_wi word_number_of_def int_one_bin by auto
+lemma word_1_no: "(1::'a::len0 word) = Numeral1"
+  by (simp add: word_number_of_alt)
 
 lemma word_m1_wi: "-1 = word_of_int -1" 
   by (rule word_number_of_alt)
@@ -1232,7 +1228,7 @@
 
 lemma word_sp_01 [simp] : 
   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
-  by (unfold word_0_no word_1_no) (auto simp: BIT_simps)
+  unfolding word_0_no word_1_no by simp
 
 (* alternative approach to lifting arithmetic equalities *)
 lemma word_of_int_Ex:
@@ -4567,7 +4563,7 @@
 
 
 lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
-  by (fact word_1_no [symmetric, unfolded BIT_simps])
+  by (fact word_1_no [symmetric])
 
 lemma word_no_0 [simp]: "(Numeral0::'a::len0 word) = 0"
   by (fact word_0_no [symmetric])