# HG changeset patch
# User huffman
# Date 1329999378 -3600
# Node ID 9f9e85264e4d7fbe2f268ddc9aa080f3fe06b473
# Parent  83a5160e6b4dab3c8901b61467a08e1031e19ded
make uses of bin_sign respect int/bin distinction

diff -r 83a5160e6b4d -r 9f9e85264e4d src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Thu Feb 23 12:45:00 2012 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Thu Feb 23 13:16:18 2012 +0100
@@ -279,14 +279,15 @@
   done
 
 lemma le_int_or:
-  "bin_sign (y::int) = Int.Pls ==> x <= x OR y"
+  "bin_sign (y::int) = 0 ==> x <= x OR y"
   apply (induct y arbitrary: x rule: bin_induct)
     apply clarsimp
+   apply (simp only: Min_def)
    apply clarsimp
   apply (case_tac x rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] bit)
-     apply (auto simp: less_eq_int_code BIT_simps)
+     apply (auto simp: le_Bits)
   done
 
 lemmas int_and_le =
diff -r 83a5160e6b4d -r 9f9e85264e4d src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 12:45:00 2012 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Feb 23 13:16:18 2012 +0100
@@ -291,15 +291,12 @@
 
 lemma bin_sign_simps [simp]:
   "bin_sign 0 = 0"
+  "bin_sign 1 = 0"
   "bin_sign -1 = -1"
   "bin_sign (number_of (Int.Bit0 w)) = bin_sign (number_of w)"
   "bin_sign (number_of (Int.Bit1 w)) = bin_sign (number_of w)"
-  "bin_sign Int.Pls = Int.Pls"
-  "bin_sign Int.Min = Int.Min"
-  "bin_sign (Int.Bit0 w) = bin_sign w"
-  "bin_sign (Int.Bit1 w) = bin_sign w"
   "bin_sign (w BIT b) = bin_sign w"
-  unfolding bin_sign_def numeral_simps Bit_def bitval_def number_of_is_id
+  unfolding bin_sign_def Bit_def bitval_def
   by (simp_all split: bit.split)
 
 lemma bin_sign_rest [simp]: 
@@ -722,12 +719,12 @@
   by (case_tac bin rule: bin_exhaust) auto
 
 lemma sign_Pls_ge_0: 
-  "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
-  by (induct bin rule: numeral_induct) auto
+  "(bin_sign bin = 0) = (bin >= (0 :: int))"
+  unfolding bin_sign_def by simp
 
 lemma sign_Min_lt_0: 
-  "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
-  by (induct bin rule: numeral_induct) auto
+  "(bin_sign bin = -1) = (bin < (0 :: int))"
+  unfolding bin_sign_def by simp
 
 lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
 
diff -r 83a5160e6b4d -r 9f9e85264e4d src/HOL/Word/Word.thy
--- 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)"