--- 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";
+
--- 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();