# HG changeset patch
# User huffman
# Date 1228621193 28800
# Node ID 9140227dc8c5277fedfbb3a0e4157f25353161fe
# Parent  a47003001699208d3596fbc330dcc898caf76b59
change lemmas to avoid using neg

diff -r a47003001699 -r 9140227dc8c5 src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/Arith_Tools.thy	Sat Dec 06 19:39:53 2008 -0800
@@ -40,7 +40,7 @@
 text{*No longer required as a simprule because of the @{text inverse_fold}
    simproc*}
 lemma Suc_diff_number_of:
-     "neg (number_of (uminus v)::int) ==>
+     "Int.Pls < v ==>
       Suc m - (number_of v) = m - (number_of (Int.pred v))"
 apply (subst Suc_diff_eq_diff_pred)
 apply simp
diff -r a47003001699 -r 9140227dc8c5 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/Library/Nat_Infinity.thy	Sat Dec 06 19:39:53 2008 -0800
@@ -146,8 +146,8 @@
   by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
 
 lemma plus_inat_number [simp]:
-  "(number_of k \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
-    else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
+  "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
+    else if l < Int.Pls then number_of k else number_of (k + l))"
   unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
 
 lemma iSuc_number [simp]:
diff -r a47003001699 -r 9140227dc8c5 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 05 17:35:22 2008 -0800
+++ b/src/HOL/NatBin.thy	Sat Dec 06 19:39:53 2008 -0800
@@ -141,10 +141,10 @@
 (*"neg" is used in rewrite rules for binary comparisons*)
 lemma add_nat_number_of [simp]:
      "(number_of v :: nat) + number_of v' =  
-         (if neg (number_of v :: int) then number_of v'  
-          else if neg (number_of v' :: int) then number_of v  
+         (if v < Int.Pls then number_of v'  
+          else if v' < Int.Pls then number_of v  
           else number_of (v + v'))"
-  unfolding nat_number_of_def number_of_is_id neg_def
+  unfolding nat_number_of_def number_of_is_id numeral_simps
   by (simp add: nat_add_distrib)
 
 
@@ -160,19 +160,19 @@
 
 lemma diff_nat_number_of [simp]: 
      "(number_of v :: nat) - number_of v' =  
-        (if neg (number_of v' :: int) then number_of v  
+        (if v' < Int.Pls then number_of v  
          else let d = number_of (v + uminus v') in     
               if neg d then 0 else nat d)"
-by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
-
+  unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
+  by auto
 
 
 subsubsection{*Multiplication *}
 
 lemma mult_nat_number_of [simp]:
      "(number_of v :: nat) * number_of v' =  
-       (if neg (number_of v :: int) then 0 else number_of (v * v'))"
-  unfolding nat_number_of_def number_of_is_id neg_def
+       (if v < Int.Pls then 0 else number_of (v * v'))"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
   by (simp add: nat_mult_distrib)
 
 
@@ -446,17 +446,18 @@
 text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
 
 lemma eq_number_of_0 [simp]:
-  "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"  
-  unfolding nat_number_of_def number_of_is_id by auto
+  "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by auto
 
 lemma eq_0_number_of [simp]:
-  "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"  
+  "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
 by (rule trans [OF eq_sym_conv eq_number_of_0])
 
 lemma less_0_number_of [simp]:
-     "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
-
+   "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by simp
 
 lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
 by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
@@ -705,7 +706,7 @@
 
 lemma nat_number_of_mult_left:
      "number_of v * (number_of v' * (k::nat)) =  
-         (if neg (number_of v :: int) then 0
+         (if v < Int.Pls then 0
           else number_of (v * v') * k)"
 by simp