src/HOL/Word/Word.thy

   by (simp only: Pls_def word_0_wi)
 
 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)
 
 lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"

   unfolding word_number_of_def Int.succ_def Int.pred_def
   by (simp add: word_of_int_homs)
 
 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:
   "\<exists>y. x = word_of_int y"
   by (rule_tac x="uint x" in exI) simp

   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   by unat_arith
 
 
 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])
 
 declare bin_to_bl_def [simp]