src/HOL/Word/Word.thy
changeset 46604 9f9e85264e4d
parent 46603 83a5160e6b4d
child 46617 8c5d10d41391
--- a/src/HOL/Word/Word.thy	Thu Feb 23 12:45:00 2012 +0100
+++ b/src/HOL/Word/Word.thy	Thu Feb 23 13:16:18 2012 +0100
@@ -561,7 +561,7 @@
   using word_sint.Rep [of x] by (simp add: sints_num)
 
 lemma sign_uint_Pls [simp]: 
-  "bin_sign (uint x) = Int.Pls"
+  "bin_sign (uint x) = 0"
   by (simp add: sign_Pls_ge_0 number_of_eq)
 
 lemma uint_m2p_neg: "uint (x::'a::len0 word) - 2 ^ len_of TYPE('a) < 0"
@@ -587,7 +587,7 @@
   by (simp only: int_word_uint)
 
 lemma unat_number_of: 
-  "bin_sign b = Int.Pls \<Longrightarrow> 
+  "bin_sign (number_of b) = 0 \<Longrightarrow> 
   unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
   apply (unfold unat_def)
   apply (clarsimp simp only: uint_number_of)
@@ -2299,8 +2299,7 @@
   unfolding word_lsb_def bin_last_def by auto
 
 lemma word_msb_sint: "msb w = (sint w < 0)" 
-  unfolding word_msb_def
-  by (simp add : sign_Min_lt_0 number_of_is_id)
+  unfolding word_msb_def sign_Min_lt_0 ..
 
 lemma msb_word_of_int:
   "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"