move all neg-related lemmas to NatBin; make type of neg specific to int

--- a/src/HOL/Int.thy	Tue Dec 09 20:36:20 2008 -0800
+++ b/src/HOL/Int.thy	Tue Dec 09 22:13:16 2008 -0800
@@ -1076,47 +1076,17 @@
 
 text {* First version by Norbert Voelker *}
 
-definition
-  neg  :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
-where
-  "neg Z \<longleftrightarrow> Z < 0"
-
 definition (*for simplifying equalities*)
   iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
 where
   "iszero z \<longleftrightarrow> z = 0"
 
-lemma not_neg_int [simp]: "~ neg (of_nat n)"
-by (simp add: neg_def)
-
-lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
-by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
-
-lemmas neg_eq_less_0 = neg_def
-
-lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
-by (simp add: neg_def linorder_not_less)
-
-text{*To simplify inequalities when Numeral1 can get simplified to 1*}
-
-lemma not_neg_0: "~ neg 0"
-by (simp add: One_int_def neg_def)
-
-lemma not_neg_1: "~ neg 1"
-by (simp add: neg_def linorder_not_less zero_le_one)
-
 lemma iszero_0: "iszero 0"
 by (simp add: iszero_def)
 
 lemma not_iszero_1: "~ iszero 1"
 by (simp add: iszero_def eq_commute)
 
-lemma neg_nat: "neg z ==> nat z = 0"
-by (simp add: neg_def order_less_imp_le) 
-
-lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
-by (simp add: linorder_not_less neg_def)
-
 lemma eq_number_of_eq:
   "((number_of x::'a::number_ring) = number_of y) =
    iszero (number_of (x + uminus y) :: 'a)"
@@ -1196,26 +1166,6 @@
 
 subsubsection {* The Less-Than Relation *}
 
-lemma less_number_of_eq_neg:
-  "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
-  = neg (number_of (x + uminus y) :: 'a)"
-apply (subst less_iff_diff_less_0) 
-apply (simp add: neg_def diff_minus number_of_add number_of_minus)
-done
-
-text {*
-  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
-  @{term Numeral0} IS @{term "number_of Pls"}
-*}
-
-lemma not_neg_number_of_Pls:
-  "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
-  by (simp add: neg_def numeral_0_eq_0)
-
-lemma neg_number_of_Min:
-  "neg (number_of Min ::'a::{ordered_idom,number_ring})"
-  by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
-
 lemma double_less_0_iff:
   "(a + a < 0) = (a < (0::'a::ordered_idom))"
 proof -
@@ -1238,27 +1188,6 @@
     add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
 qed
 
-lemma neg_number_of_Bit0:
-  "neg (number_of (Bit0 w)::'a) = 
-  neg (number_of w :: 'a::{ordered_idom,number_ring})"
-by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
-
-lemma neg_number_of_Bit1:
-  "neg (number_of (Bit1 w)::'a) = 
-  neg (number_of w :: 'a::{ordered_idom,number_ring})"
-proof -
-  have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
-    by simp
-  also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
-  finally show ?thesis
-  by (simp add: neg_def number_of_eq numeral_simps)
-qed
-
-lemmas neg_simps [simp] =
-  not_neg_0 not_neg_1
-  not_neg_number_of_Pls neg_number_of_Min
-  neg_number_of_Bit0 neg_number_of_Bit1
-
 text {* Less-Than or Equals *}
 
 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
@@ -1267,11 +1196,6 @@
   linorder_not_less [of "number_of w" "number_of v", symmetric, 
   standard]
 
-lemma le_number_of_eq:
-    "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
-     = (~ (neg (number_of (y + uminus x) :: 'a)))"
-by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
-
 
 text {* Absolute value (@{term abs}) *}
 

--- a/src/HOL/Library/Float.thy	Tue Dec 09 20:36:20 2008 -0800
+++ b/src/HOL/Library/Float.thy	Tue Dec 09 22:13:16 2008 -0800
@@ -514,7 +514,7 @@
   by simp
 
 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
-  by (rule less_number_of_eq_neg)
+  unfolding neg_def number_of_is_id by simp
 
 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
   by simp

--- a/src/HOL/NatBin.thy	Tue Dec 09 20:36:20 2008 -0800
+++ b/src/HOL/NatBin.thy	Tue Dec 09 22:13:16 2008 -0800
@@ -39,6 +39,63 @@
   square  ("(_\<twosuperior>)" [1000] 999)
 
 
+subsection {* Predicate for negative binary numbers *}
+
+definition
+  neg  :: "int \<Rightarrow> bool"
+where
+  "neg Z \<longleftrightarrow> Z < 0"
+
+lemma not_neg_int [simp]: "~ neg (of_nat n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+text{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (simp add: neg_def order_less_imp_le) 
+
+lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
+by (simp add: linorder_not_less neg_def)
+
+text {*
+  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+  @{term Numeral0} IS @{term "number_of Pls"}
+*}
+
+lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
+  by (simp add: neg_def)
+
+lemma neg_number_of_Min: "neg (number_of Int.Min)"
+  by (simp add: neg_def)
+
+lemma neg_number_of_Bit0:
+  "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
+  by (simp add: neg_def)
+
+lemma neg_number_of_Bit1:
+  "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
+  by (simp add: neg_def)
+
+lemmas neg_simps [simp] =
+  not_neg_0 not_neg_1
+  not_neg_number_of_Pls neg_number_of_Min
+  neg_number_of_Bit0 neg_number_of_Bit1
+
+
 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
 
 declare nat_0 [simp] nat_1 [simp]