# HG changeset patch
# User paulson
# Date 909161264 -7200
# Node ID 387b5bf9326a3a904e475912cf7c2edf8e453131
# Parent  4f0978bb8271d3edc331421a67a1235327607455
Now users will never see (int 0)

diff -r 4f0978bb8271 -r 387b5bf9326a src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Oct 23 18:47:20 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Oct 23 18:47:44 1998 +0200
@@ -244,6 +244,28 @@
 AddIffs [zero_zle_int];
 
 
+(** Needed because (int 0) rewrites to #0.
+    Can these be generalized without evaluating large numbers?**)
+
+Goal "~ (int k < #0)";
+by (Simp_tac 1);
+qed "int_less_0_conv";
+
+Goal "(int k <= #0) = (k=0)";
+by (Simp_tac 1);
+qed "int_le_0_conv";
+
+Goal "(int k = #0) = (k=0)";
+by (Simp_tac 1);
+qed "int_eq_0_conv";
+
+Goal "(#0 = int k) = (k=0)";
+by Auto_tac;
+qed "int_eq_0_conv'";
+
+Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv'];
+
+
 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
 
 (** Equals (=) **)
@@ -445,9 +467,14 @@
 by (Simp_tac 1);
 qed "nat_less_iff";
 
+
+(*Otherwise (int 0) sometimes turns up...*)
+Addsimps [int_0];
+
 Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
 by (case_tac "neg z" 1);
 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
 by (auto_tac (claset() addIs [zless_trans], 
-	      simpset() addsimps [neg_eq_less_0, zle_def, int_0]));
+	      simpset() addsimps [neg_eq_less_0, zle_def]));
 qed "nat_less_eq_zless";
+
diff -r 4f0978bb8271 -r 387b5bf9326a src/HOL/ex/BinEx.ML
--- a/src/HOL/ex/BinEx.ML	Fri Oct 23 18:47:20 1998 +0200
+++ b/src/HOL/ex/BinEx.ML	Fri Oct 23 18:47:44 1998 +0200
@@ -85,39 +85,39 @@
 
 (** Testing the cancellation of complementary terms **)
 
-Goal "y + (x + -x) = int 0 + y";
+Goal "y + (x + -x) = #0 + y";
 by (Simp_tac 1);
 result();
 
-Goal "y + (-x + (- y + x)) = int 0";
+Goal "y + (-x + (- y + x)) = #0";
 by (Simp_tac 1);
 result();
 
-Goal "-x + (y + (- y + x)) = int 0";
+Goal "-x + (y + (- y + x)) = #0";
 by (Simp_tac 1);
 result();
 
-Goal "x + (x + (- x + (- x + (- y + - z)))) = int 0 - y - z";
+Goal "x + (x + (- x + (- x + (- y + - z)))) = #0 - y - z";
 by (Simp_tac 1);
 result();
 
-Goal "x + x - x - x - y - z = int 0 - y - z";
+Goal "x + x - x - x - y - z = #0 - y - z";
 by (Simp_tac 1);
 result();
 
-Goal "x + y + z - (x + z) = y - int 0";
+Goal "x + y + z - (x + z) = y - #0";
 by (Simp_tac 1);
 result();
 
-Goal "x+(y+(y+(y+ (-x + -x)))) = int 0 + y - x + y + y";
+Goal "x+(y+(y+(y+ (-x + -x)))) = #0 + y - x + y + y";
 by (Simp_tac 1);
 result();
 
-Goal "x+(y+(y+(y+ (-y + -x)))) = y + int 0 + y";
+Goal "x+(y+(y+(y+ (-y + -x)))) = y + #0 + y";
 by (Simp_tac 1);
 result();
 
-Goal "x + y - x + z - x - y - z + x < int 1";
+Goal "x + y - x + z - x - y - z + x < #1";
 by (Simp_tac 1);
 result();