# HG changeset patch
# User paulson
# Date 906643427 -7200
# Node ID 29f09a7780379b396d9887d97c889a777778ee33
# Parent  a48cbe410618f9f2db4565efbb0210a267764d0f
Function nat_of now maps negative integers to zero, not their absolute value

diff -r a48cbe410618 -r 29f09a778037 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Thu Sep 24 15:21:30 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Thu Sep 24 15:23:47 1998 +0200
@@ -164,8 +164,9 @@
 by Auto_tac;
 qed "nat_of_nat";
 
-Goalw [nat_of_def] "nat_of(- $# n) = n";
-by Auto_tac;
+Goalw [nat_of_def] "nat_of(- $# n) = 0";
+by (auto_tac (claset(),
+	      simpset() addsimps [neg_eq_less_nat0, zminus_zless])); 
 qed "nat_of_zminus_nat";
 
 Addsimps [nat_of_nat, nat_of_zminus_nat];
@@ -182,8 +183,7 @@
 				  zdiff_eq_eq RS sym, zdiff_def])); 
 qed "negD"; 
 
-Goal "neg z ==> $# (nat_of z) = -z"; 
-by (dtac negD 1);
+Goalw [nat_of_def] "neg z ==> nat_of z = 0"; 
 by Auto_tac; 
 qed "neg_nat_of"; 
 
diff -r a48cbe410618 -r 29f09a778037 src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Thu Sep 24 15:21:30 1998 +0200
+++ b/src/HOL/Integ/Integ.thy	Thu Sep 24 15:23:47 1998 +0200
@@ -13,6 +13,6 @@
 
 constdefs
   nat_of  :: int => nat
-  "nat_of(Z) == @m. Z = $# m | -Z = $# m"
+  "nat_of(Z) == if neg Z then 0 else (@ m. Z = $# m)"
 
 end