many renamings and changes. Simproc for cancelling common terms in relations

--- a/src/HOL/Integ/Bin.ML	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Tue Sep 29 15:57:42 1998 +0200
@@ -104,12 +104,12 @@
 Addsimps [integ_of_NCons];
 
 qed_goal "integ_of_succ" Bin.thy
-    "integ_of(bin_succ w) = $#1 + integ_of w"
+    "integ_of(bin_succ w) = int 1 + integ_of w"
  (fn _ =>[(rtac bin.induct 1),
           (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
 
 qed_goal "integ_of_pred" Bin.thy
-    "integ_of(bin_pred w) = - ($#1) + integ_of w"
+    "integ_of(bin_pred w) = - (int 1) + integ_of w"
  (fn _ =>[(rtac bin.induct 1),
           (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
 
@@ -166,7 +166,7 @@
 by (Simp_tac 1);
 qed "zadd_zminus_inverse2";
 
-(*These rewrite to $# 0.  Henceforth we should rewrite to #0  *)
+(*These rewrite to int 0.  Henceforth we should rewrite to #0  *)
 Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
 
 Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
@@ -177,6 +177,21 @@
 
 Addsimps [zminus_0];
 
+
+Goal "#0 - x = -x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff0";
+
+Goal "x - #0 = x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff0_right";
+
+Goal "x - x = #0";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_self";
+
+Addsimps [zdiff0, zdiff0_right, zdiff_self];
+
 Goal "#0 * z = #0";
 by (Simp_tac 1);
 qed "zmult_0";
@@ -218,10 +233,15 @@
 by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
 qed "neg_eq_less_0"; 
 
-Goal "(~neg x) = ($# 0 <= x)";
+Goal "(~neg x) = (int 0 <= x)";
 by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); 
 qed "not_neg_eq_ge_0"; 
 
+Goal "#0 <= int m";
+by (Simp_tac 1);
+qed "zero_zle_int";
+AddIffs [zero_zle_int];
+
 
 
 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
@@ -250,7 +270,7 @@
 by (ALLGOALS (asm_simp_tac 
 	      (simpset() addsimps zcompare_rls @ 
 				  [zminus_zadd_distrib RS sym, 
-				   add_nat]))); 
+				   zadd_int]))); 
 qed "iszero_integ_of_BIT"; 
 
 
@@ -274,7 +294,7 @@
 by (Asm_simp_tac 1); 
 by (int_case_tac "integ_of w" 1); 
 by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps [add_nat, neg_eq_less_nat0, 
+	      (simpset() addsimps [zadd_int, neg_eq_less_nat0, 
 				   symmetric zdiff_def] @ zcompare_rls))); 
 qed "neg_integ_of_BIT"; 
 
@@ -382,20 +402,13 @@
 qed "zless_zadd1_imp_zless";
 
 Goal "w + #-1 = w - #1";
-by (simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls) 1);
+by (Simp_tac 1);
 qed "zplus_minus1_conv";
 
-(*Eliminates neg from the subgoal, introduced e.g. by zcompare_0_rls*)
-val no_neg_ss = 
-    simpset()
-      delsimps [less_integ_of_eq_neg]  (*loops: it introduces neg*)
-      addsimps [zadd_assoc RS sym, zplus_minus1_conv,
-		neg_eq_less_0, iszero_def] @ zcompare_rls;
-
 
 (*** nat ***)
 
-Goal "#0 <= z ==> $# (nat z) = z"; 
+Goal "#0 <= z ==> int (nat z) = z"; 
 by (asm_full_simp_tac
     (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
 qed "nat_0_le"; 
@@ -407,14 +420,14 @@
 
 Addsimps [nat_0_le, nat_less_0];
 
-Goal "#0 <= w ==> (nat w = m) = (w = $# m)";
+Goal "#0 <= w ==> (nat w = m) = (w = int m)";
 by Auto_tac;
 qed "nat_eq_iff";
 
-Goal "#0 <= w ==> (nat w < m) = (w < $# m)";
+Goal "#0 <= w ==> (nat w < m) = (w < int m)";
 by (rtac iffI 1);
 by (asm_full_simp_tac 
-    (simpset() delsimps [zless_eq_less] addsimps [zless_eq_less RS sym]) 2);
+    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
 by (etac (nat_0_le RS subst) 1);
 by (Simp_tac 1);
 qed "nat_less_iff";
@@ -428,7 +441,7 @@
 
 Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
 by (stac nat_less_iff 1);
-ba 1;
+by (assume_tac 1);
 by (case_tac "neg z" 1);
 by (auto_tac (claset(), simpset() addsimps [not_neg_nat, neg_nat]));
 by (auto_tac (claset(), 
@@ -438,11 +451,11 @@
 
 
 (**Can these be generalized without evaluating large numbers?**)
-Goal "($# k = #0) = (k=0)";
+Goal "(int k = #0) = (k=0)";
 by (simp_tac (simpset() addsimps [integ_of_Pls]) 1);
 qed "nat_eq_0_conv";
 
-Goal "(#0 = $# k) = (k=0)";
+Goal "(#0 = int k) = (k=0)";
 by (auto_tac (claset(), simpset() addsimps [integ_of_Pls]));
 qed "nat_eq_0_conv'";
 

--- a/src/HOL/Integ/Bin.thy	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Tue Sep 29 15:57:42 1998 +0200
@@ -48,9 +48,9 @@
   NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
  
 primrec
-  integ_of_Pls  "integ_of Pls = $# 0"
-  integ_of_Min  "integ_of Min = - ($# 1)"
-  integ_of_BIT  "integ_of(w BIT x) = (if x then $# 1 else $# 0) +
+  integ_of_Pls  "integ_of Pls = int 0"
+  integ_of_Min  "integ_of Min = - (int 1)"
+  integ_of_BIT  "integ_of(w BIT x) = (if x then int 1 else int 0) +
 	                             (integ_of w) + (integ_of w)" 
 
 primrec

--- a/src/HOL/Integ/Int.ML	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/Int.ML	Tue Sep 29 15:57:42 1998 +0200
@@ -18,30 +18,25 @@
 by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
 qed "zle_eq_not_neg";
 
-(*This list of rewrites simplifies (in)equalities by subtracting the RHS
-  from the LHS, then using the cancellation simproc.  Use with zadd_ac.*)
-val zcompare_0_rls = 
-    [zdiff_def, zless_eq_neg, eq_eq_iszero, zle_eq_not_neg];
-
 
 (*** Monotonicity results ***)
 
 Goal "(v+z < w+z) = (v < (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (Simp_tac 1);
 qed "zadd_right_cancel_zless";
 
 Goal "(z+v < z+w) = (v < (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (Simp_tac 1);
 qed "zadd_left_cancel_zless";
 
 Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
 
 Goal "(v+z <= w+z) = (v <= (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (Simp_tac 1);
 qed "zadd_right_cancel_zle";
 
 Goal "(z+v <= z+w) = (v <= (w::int))";
-by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (Simp_tac 1);
 qed "zadd_left_cancel_zle";
 
 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
@@ -66,59 +61,59 @@
 (*** Comparison laws ***)
 
 Goal "(- x < - y) = (y < (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
 qed "zminus_zless_zminus"; 
 Addsimps [zminus_zless_zminus];
 
 Goal "(- x <= - y) = (y <= (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (simp_tac (simpset() addsimps [zle_def]) 1);
 qed "zminus_zle_zminus"; 
 Addsimps [zminus_zle_zminus];
 
 (** The next several equations can make the simplifier loop! **)
 
 Goal "(x < - y) = (y < - (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
 qed "zless_zminus"; 
 
 Goal "(- x < y) = (- y < (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
 qed "zminus_zless"; 
 
 Goal "(x <= - y) = (y <= - (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (simp_tac (simpset() addsimps [zle_def, zminus_zless]) 1);
 qed "zle_zminus"; 
 
 Goal "(- x <= y) = (- y <= (x::int))";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+by (simp_tac (simpset() addsimps [zle_def, zless_zminus]) 1);
 qed "zminus_zle"; 
 
-Goal "- $# Suc n < $# 0";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+Goal "- (int (Suc n)) < int 0";
+by (simp_tac (simpset() addsimps [zless_def]) 1);
 qed "negative_zless_0"; 
 
-Goal "- $# Suc n < $# m";
+Goal "- (int (Suc n)) < int m";
 by (rtac (negative_zless_0 RS zless_zle_trans) 1);
 by (Simp_tac 1); 
 qed "negative_zless"; 
 AddIffs [negative_zless]; 
 
-Goal "- $# n <= $#0";
-by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
+Goal "- int n <= int 0";
+by (simp_tac (simpset() addsimps [zminus_zle]) 1);
 qed "negative_zle_0"; 
 
-Goal "- $# n <= $# m";
-by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1);
+Goal "- int n <= int m";
+by (simp_tac (simpset() addsimps [zless_def, zle_def, zdiff_def, zadd_int]) 1);
 qed "negative_zle"; 
 AddIffs [negative_zle]; 
 
-Goal "~($# 0 <= - $# Suc n)";
+Goal "~(int 0 <= - (int (Suc n)))";
 by (stac zle_zminus 1);
 by (Simp_tac 1);
 qed "not_zle_0_negative"; 
 Addsimps [not_zle_0_negative]; 
 
-Goal "($# n <= - $# m) = (n = 0 & m = 0)"; 
+Goal "(int n <= - int m) = (n = 0 & m = 0)"; 
 by Safe_tac; 
 by (Simp_tac 3); 
 by (dtac (zle_zminus RS iffD1) 2); 
@@ -126,11 +121,11 @@
 by (ALLGOALS Asm_full_simp_tac); 
 qed "int_zle_neg"; 
 
-Goal "~($# n < - $# m)";
+Goal "~(int n < - int m)";
 by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); 
 qed "not_int_zless_negative"; 
 
-Goal "(- $# n = $# m) = (n = 0 & m = 0)"; 
+Goal "(- int n = int m) = (n = 0 & m = 0)"; 
 by (rtac iffI 1);
 by (rtac (int_zle_neg RS iffD1) 1); 
 by (dtac sym 1); 
@@ -140,44 +135,41 @@
 Addsimps [negative_eq_positive, not_int_zless_negative]; 
 
 
-Goal "(w <= z) = (EX n. z = w + $# n)";
-by (auto_tac (claset(),
+Goal "(w <= z) = (EX n. z = w + int n)";
+by (auto_tac (claset() addSIs [not_sym RS not0_implies_Suc],
 	      simpset() addsimps [zless_iff_Suc_zadd, integ_le_less]));
-by (ALLGOALS (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac)));
-by (ALLGOALS (full_simp_tac (simpset() addsimps [iszero_def])));
-by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
 qed "zle_iff_zadd";
 
 
-Goalw [zdiff_def,zless_def] "neg x = (x < $# 0)";
+Goalw [zdiff_def,zless_def] "neg x = (x < int 0)";
 by Auto_tac; 
 qed "neg_eq_less_nat0"; 
 
-Goalw [zle_def] "(~neg x) = ($# 0 <= x)";
+Goalw [zle_def] "(~neg x) = (int 0 <= x)";
 by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
 qed "not_neg_eq_ge_nat0"; 
 
 
 (**** nat: magnitide of an integer, as a natural number ****)
 
-Goalw [nat_def] "nat($# n) = n";
+Goalw [nat_def] "nat(int n) = n";
 by Auto_tac;
 qed "nat_nat";
 
-Goalw [nat_def] "nat(- $# n) = 0";
+Goalw [nat_def] "nat(- int n) = 0";
 by (auto_tac (claset(),
 	      simpset() addsimps [neg_eq_less_nat0, zminus_zless])); 
 qed "nat_zminus_nat";
 
 Addsimps [nat_nat, nat_zminus_nat];
 
-Goal "~ neg z ==> $# (nat z) = z"; 
+Goal "~ neg z ==> int (nat z) = z"; 
 by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1); 
 by (dtac zle_imp_zless_or_eq 1); 
 by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); 
 qed "not_neg_nat"; 
 
-Goal "neg x ==> ? n. x = - $# Suc n"; 
+Goal "neg x ==> ? n. x = - (int (Suc n))"; 
 by (auto_tac (claset(), 
 	      simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd,
 				  zdiff_eq_eq RS sym, zdiff_def])); 
@@ -189,7 +181,7 @@
 
 (* a case theorem distinguishing positive and negative int *)  
 
-val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; 
+val prems = Goal "[|!! n. P (int n); !! n. P (- (int (Suc n))) |] ==> P z"; 
 by (case_tac "neg z" 1); 
 by (blast_tac (claset() addSDs [negD] addSIs prems) 1); 
 by (etac (not_neg_nat RS subst) 1);

--- a/src/HOL/Integ/Int.thy	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/Int.thy	Tue Sep 29 15:57:42 1998 +0200
@@ -13,6 +13,6 @@
 
 constdefs
   nat  :: int => nat
-  "nat(Z) == if neg Z then 0 else (@ m. Z = $# m)"
+  "nat(Z) == if neg Z then 0 else (@ m. Z = int m)"
 
 end

--- a/src/HOL/Integ/IntDef.ML	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/IntDef.ML	Tue Sep 29 15:57:42 1998 +0200
@@ -137,7 +137,7 @@
 by (Asm_full_simp_tac 1);
 qed "inj_zminus";
 
-Goalw [int_def] "- ($# 0) = $# 0";
+Goalw [int_def] "- (int 0) = int 0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_nat0";
 
@@ -147,12 +147,12 @@
 (**** neg: the test for negative integers ****)
 
 
-Goalw [neg_def, int_def] "~ neg($# n)";
+Goalw [neg_def, int_def] "~ neg(int n)";
 by (Simp_tac 1);
 by Safe_tac;
 qed "not_neg_nat";
 
-Goalw [neg_def, int_def] "neg(- $# Suc(n))";
+Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "neg_zminus_nat";
 
@@ -214,30 +214,30 @@
 (*Integer addition is an AC operator*)
 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
 
-Goalw [int_def] "($#m) + ($#n) = $# (m + n)";
+Goalw [int_def] "(int m) + (int n) = int (m + n)";
 by (simp_tac (simpset() addsimps [zadd]) 1);
-qed "add_nat";
+qed "zadd_int";
 
-Goal "$# (Suc m) = $# 1 + ($# m)";
-by (simp_tac (simpset() addsimps [add_nat]) 1);
+Goal "int (Suc m) = int 1 + (int m)";
+by (simp_tac (simpset() addsimps [zadd_int]) 1);
 qed "int_Suc";
 
-Goalw [int_def] "$# 0 + z = z";
+Goalw [int_def] "int 0 + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "zadd_nat0";
 
-Goal "z + $# 0 = z";
+Goal "z + int 0 = z";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac zadd_nat0 1);
 qed "zadd_nat0_right";
 
-Goalw [int_def] "z + (- z) = $# 0";
+Goalw [int_def] "z + (- z) = int 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
 qed "zadd_zminus_inverse_nat";
 
-Goal "(- z) + z = $# 0";
+Goal "(- z) + z = int 0";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac zadd_zminus_inverse_nat 1);
 qed "zadd_zminus_inverse_nat2";
@@ -246,15 +246,25 @@
 	  zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
 
 Goal "z + (- z + w) = (w::int)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 qed "zadd_zminus_cancel";
 
 Goal "(-z) + (z + w) = (w::int)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 qed "zminus_zadd_cancel";
 
 Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
 
+Goal "int 0 - x = -x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_nat0";
+
+Goal "x - int 0 = x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_nat0_right";
+
+Addsimps [zdiff_nat0, zdiff_nat0_right];
+
 
 (** Lemmas **)
 
@@ -362,21 +372,21 @@
 by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
-Goalw [int_def] "$# 0 * z = $# 0";
+Goalw [int_def] "int 0 * z = int 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_nat0";
 
-Goalw [int_def] "$# 1 * z = z";
+Goalw [int_def] "int 1 * z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_nat1";
 
-Goal "z * $# 0 = $# 0";
+Goal "z * int 0 = int 0";
 by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1);
 qed "zmult_nat0_right";
 
-Goal "z * $# 1 = z";
+Goal "z * int 1 = z";
 by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1);
 qed "zmult_nat1_right";
 
@@ -394,7 +404,7 @@
 
 (*This lemma allows direct proofs of other <-properties*)
 Goalw [zless_def, neg_def, zdiff_def, int_def] 
-    "(w < z) = (EX n. z = w + $#(Suc n))";
+    "(w < z) = (EX n. z = w + int(Suc n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (Clarify_tac 1);
@@ -404,16 +414,16 @@
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
 qed "zless_iff_Suc_zadd";
 
-Goal "z < z + $# (Suc n)";
+Goal "z < z + int (Suc n)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_nat]));
+				  zadd_int]));
 qed "zless_zadd_Suc";
 
 Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_nat]));
+				  zadd_int]));
 qed "zless_trans";
 
 Goal "!!w::int. z<w ==> ~w<z";
@@ -463,24 +473,24 @@
 (*** eliminates ~= in premises ***)
 bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
 
-Goal "($# m = $# n) = (m = n)"; 
+Goal "(int m = int n) = (m = n)"; 
 by (fast_tac (claset() addSEs [inj_nat RS injD]) 1); 
 qed "int_int_eq"; 
 AddIffs [int_int_eq]; 
 
-Goal "($#m < $#n) = (m<n)";
+Goal "(int m < int n) = (m<n)";
 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
-				  add_nat]) 1);
-qed "zless_eq_less";
-Addsimps [zless_eq_less];
+				  zadd_int]) 1);
+qed "zless_int";
+Addsimps [zless_int];
 
 
 (*** Properties of <= ***)
 
-Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
+Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)";
 by (Simp_tac 1);
-qed "zle_eq_le";
-Addsimps [zle_eq_le];
+qed "zle_int";
+Addsimps [zle_int];
 
 Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
 by (assume_tac 1);
@@ -633,10 +643,9 @@
 Addsimps [zadd_right_cancel];
 
 
-Goal "(w < z + $# 1) = (w<z | w=z)";
+Goal "(w < z + int 1) = (w<z | w=z)";
 by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_nat]));
+	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int]));
 by (cut_inst_tac [("m","n")] int_Suc 1);
 by (exhaust_tac "n" 1);
 by Auto_tac;
@@ -645,8 +654,9 @@
 qed "zless_add_nat1_eq";
 
 
-Goal "(w + $# 1 <= z) = (w<z)";
+Goal "(w + int 1 <= z) = (w<z)";
 by (simp_tac (simpset() addsimps [zle_def, zless_add_nat1_eq]) 1);
 by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
 	      simpset() addsimps [symmetric zle_def]));
 qed "add_nat1_zle_eq";
+

--- a/src/HOL/Integ/IntDef.thy	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue Sep 29 15:57:42 1998 +0200
@@ -23,15 +23,15 @@
 
 constdefs
 
-  int :: nat => int                                  ("$# _" [80] 80)
-  "$# m == Abs_Integ(intrel ^^ {(m,0)})"
+  int :: nat => int
+  "int m == Abs_Integ(intrel ^^ {(m,0)})"
 
   neg   :: int => bool
   "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
 
   (*For simplifying equalities*)
   iszero :: int => bool
-  "iszero z == z = $# 0"
+  "iszero z == z = int 0"
   
 defs
   zadd_def

--- a/src/HOL/Integ/simproc.ML	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/simproc.ML	Tue Sep 29 15:57:42 1998 +0200
@@ -3,44 +3,84 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Simplification procedures for the integers
-
-This one cancels complementary terms in sums.  Examples:
-   x + (y + -x)   =   x + (-x + y)  =  y
-   -x + (y + (x + z))   =   -x + (x + (y + z))  =  y + z
-
-Should be used with zdiff_def (to eliminate subtraction) and zadd_ac.
+Simplification procedures for abelian groups (e.g. integers, reals)
 *)
 
 
-structure Int_Cancel =
+
+(*Deletion of other terms in the formula, seeking the -x at the front of z*)
+Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)";
+by (stac zadd_left_commute 1);
+by (rtac zadd_left_cancel 1);
+qed "zadd_cancel_21";
+
+(*A further rule to deal with the case that
+  everything gets cancelled on the right.*)
+Goal "((x::int) + (y + z) = y) = (x = -z)";
+by (stac zadd_left_commute 1);
+by (res_inst_tac [("t", "y")] (zadd_nat0_right RS subst) 1
+    THEN stac zadd_left_cancel 1);
+by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1);
+qed "zadd_cancel_minus";
+
+
+val prepare_ss = HOL_ss addsimps [zadd_assoc, zdiff_def, 
+				  zminus_zadd_distrib, zminus_zminus,
+				  zminus_nat0, zadd_nat0, zadd_nat0_right];
+
+
+
+(*prove while suppressing timing information*)
+fun prove ct = setmp Goals.proof_timing false (prove_goalw_cterm [] ct);
+
+
+(*This one cancels complementary terms in sums.  Examples:
+   x-x = 0    x+(y-x) = y   -x+(y+(x+z)) = y+z
+  It will unfold the definition of diff and associate to the right if 
+  necessary.  With big formulae, rewriting is faster if the formula is already
+  in that form.
+*)
+structure Sum_Cancel =
 struct
 
+val thy = IntDef.thy;
+
 val intT = Type ("IntDef.int", []);
 
 val zplus = Const ("op +", [intT,intT] ---> intT);
 val zminus = Const ("uminus", intT --> intT);
 
-val ssubst_left = read_instantiate [("P", "%x. ?lhs x = ?rhs")] ssubst;
-
-fun inst_left_commute ct = instantiate' [] [None, Some ct] zadd_left_commute;
+val zero = Const ("IntDef.int", HOLogic.natT --> intT) $ HOLogic.zero;
 
-(*Can LOOP, so include only if the first occurrence at the very end*)
-fun inst_commute ct = instantiate' [] [None, Some ct] zadd_commute;
+(*These rules eliminate the first two terms, if they cancel*)
+val cancel_laws = 
+    [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2,
+     zadd_zminus_cancel, zminus_zadd_cancel, 
+     zadd_cancel_21, zadd_cancel_minus, zminus_zminus];
 
-fun terms (t as f$x$y) =
-        if f=zplus then x :: terms y else [t]
-  | terms t = [t];
+
+val cancel_ss = HOL_ss addsimps cancel_laws;
 
-val mk_sum = foldr1 (fn (x,y) => zplus $ x $ y);
+fun mk_sum []  = zero
+  | mk_sum tms = foldr1 (fn (x,y) => zplus $ x $ y) tms;
 
 (*We map -t to t and (in other cases) t to -t.  No need to check the type of
   uminus, since the simproc is only called on integer sums.*)
 fun negate (Const("uminus",_) $ t) = t
   | negate t                       = zminus $ t;
 
-(*These rules eliminate the first two terms, if they cancel*)
-val cancel_laws = [zadd_zminus_cancel, zminus_zadd_cancel];
+(*Flatten a formula built from +, binary - and unary -.
+  No need to check types PROVIDED they are checked upon entry!*)
+fun add_terms neg (Const ("op +", _) $ x $ y, ts) =
+	add_terms neg (x, add_terms neg (y, ts))
+  | add_terms neg (Const ("op -", _) $ x $ y, ts) =
+	add_terms neg (x, add_terms (not neg) (y, ts))
+  | add_terms neg (Const ("uminus", _) $ x, ts) = 
+	add_terms (not neg) (x, ts)
+  | add_terms neg (x, ts) = 
+	(if neg then negate x else x) :: ts;
+
+fun terms fml = add_terms false (fml, []);
 
 exception Cancel;
 
@@ -49,35 +89,28 @@
     let fun find ([], _) = raise Cancel
 	  | find (t::ts, heads) = if head' aconv t then rev heads @ ts
 				  else find (ts, t::heads)
-    in  mk_sum (find (tail, []))  end;
+    in  mk_sum (find (tail, []))   end;
 
 
 val trace = ref false;
 
 fun proc sg _ lhs =
-  let val _ = if !trace then prs ("lhs = " ^ string_of_cterm (cterm_of sg lhs))
+  let val _ = if !trace then writeln ("cancel_sums: LHS = " ^ 
+				      string_of_cterm (cterm_of sg lhs))
               else ()
       val (head::tail) = terms lhs
       val head' = negate head
       val rhs = cancelled head' tail
       and chead' = Thm.cterm_of sg head'
-      val comms = [inst_left_commute chead' RS ssubst_left,
-		   inst_commute chead' RS ssubst_left]
       val _ = if !trace then 
-	        writeln ("rhs = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+	        writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
               else ()
       val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
-      (*Simplification is much faster than substitution, but loops for terms
-        like (x + (-x + (-x + y))).  Substitution finds the outermost -x, so
-        is seems not to loop, and the counter prevents looping for sure.*)
-      fun cancel_tac 0 = no_tac   
-	| cancel_tac n = 
-	      (resolve_tac cancel_laws 1 ORELSE
-	       resolve_tac comms 1 THEN cancel_tac (n-1));
-      val thm = prove_goalw_cterm [] ct 
-	          (fn _ => [cancel_tac (length tail + 1)])
+      val thm = prove ct 
+	          (fn _ => [simp_tac prepare_ss 1,
+			    IF_UNSOLVED (simp_tac cancel_ss 1)])
 	handle ERROR =>
-	error("The error(s) above occurred while trying to prove " ^
+	error("cancel_sums simproc:\nThe error(s) above occurred while trying to prove " ^
 	      string_of_cterm ct)
   in Some (mk_meta_eq thm) end
   handle Cancel => None;
@@ -85,11 +118,100 @@
 
 val conv = 
     Simplifier.mk_simproc "cancel_sums"
-      [Thm.read_cterm (sign_of IntDef.thy) ("x + (y + (z::int))", intT)]
+      (map (Thm.read_cterm (sign_of thy)) 
+       [("x + y", intT), ("x - y", intT)])
       proc;
 
 end;
 
 
-Addsimprocs [Int_Cancel.conv];
+
+Addsimprocs [Sum_Cancel.conv];
+
+
+(** The idea is to cancel like terms on opposite sides via subtraction **)
+
+Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')";
+by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
+qed "zless_eqI";
+
+Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')";
+bd zless_eqI 1;
+by (asm_simp_tac (simpset() addsimps [zle_def]) 1);
+qed "zle_eqI";
+
+Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')";
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [zdiff_eq_eq]) 1);
+qed "zeq_eqI";
+
+
+
+(** For simplifying relations **)
+
+structure Rel_Cancel =
+struct
+
+(*Cancel the FIRST occurrence of a term.  If it's repeated, then repeated
+  calls to the simproc will be needed.*)
+fun cancel1 ([], u)    = raise Match (*impossible: it's a common term*)
+  | cancel1 (t::ts, u) = if t aconv u then ts
+                         else t :: cancel1 (ts,u);
+    
+
+exception Relation;
+
+val trace = ref false;
+
+val sum_cancel_ss = HOL_ss addsimprocs [Sum_Cancel.conv]
+                           addsimps [zadd_nat0, zadd_nat0_right];
 
+fun proc sg _ (lhs as (rel$lt$rt)) =
+  let val _ = if !trace then writeln ("cancel_relations: LHS = " ^ 
+				      string_of_cterm (cterm_of sg lhs))
+              else ()
+      val ltms = Sum_Cancel.terms lt
+      and rtms = Sum_Cancel.terms rt
+      val common = gen_distinct (op aconv)
+	               (inter_term (ltms, rtms))
+      val _ = if null common then raise Relation  (*nothing to do*)
+	                          else ()
+
+      fun cancelled tms = Sum_Cancel.mk_sum (foldl cancel1 (tms, common))
+
+      val lt' = cancelled ltms
+      and rt' = cancelled rtms
+
+      val rhs = rel$lt'$rt'
+      val _ = if !trace then 
+	        writeln ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+              else ()
+      val ct = Thm.cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
+
+      val thm = prove ct 
+	          (fn _ => [resolve_tac [zless_eqI, zeq_eqI, zle_eqI] 1,
+			    simp_tac prepare_ss 1,
+			    simp_tac sum_cancel_ss 1,
+			    IF_UNSOLVED
+			      (simp_tac (HOL_ss addsimps zadd_ac) 1)])
+	handle ERROR =>
+	error("cancel_relations simproc:\nThe error(s) above occurred while trying to prove " ^
+	      string_of_cterm ct)
+  in Some (mk_meta_eq thm) end
+  handle Relation => None;
+
+
+val conv = 
+    Simplifier.mk_simproc "cancel_relations"
+      (map (Thm.read_cterm (sign_of thy)) 
+       [("x < (y::int)", HOLogic.boolT), 
+	("x = (y::int)", HOLogic.boolT), 
+	("x <= (y::int)", HOLogic.boolT)])
+      proc;
+
+end;
+
+
+
+Addsimprocs [Rel_Cancel.conv];