# HG changeset patch
# User paulson
# Date 965899654 -7200
# Node ID e16e168984e1818ef756927035eec7d1d36543d2
# Parent  68400ff46b0908ce313ad9eefc8f39042757dea4
installation of cancellation simprocs for the integers

diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Bool.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -8,7 +8,7 @@
 2 is equal to bool, but serves a different purpose
 *)
 
-Bool = upair + 
+Bool = pair + 
 consts
     bool        :: i
     cond        :: [i,i,i]=>i
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Integ/Bin.ML
--- a/src/ZF/Integ/Bin.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Bin.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -87,8 +87,7 @@
 (**** The carry/borrow functions, bin_succ and bin_pred ****)
 
 (*NCons preserves the integer value of its argument*)
-Goal "[| w: bin; b: bool |] ==>     \
-\         integ_of(NCons(w,b)) = integ_of(w BIT b)";
+Goal "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)";
 by (etac bin.elim 1);
 by (Asm_simp_tac 3);
 by (ALLGOALS (etac boolE));
@@ -134,10 +133,20 @@
 by (Asm_simp_tac 1);
 qed "bin_add_Pls";
 
+Goalw [bin_add_def] "w: bin ==> bin_add(w,Pls) = w";
+by (etac bin.induct 1);
+by Auto_tac;
+qed "bin_add_Pls_right";
+
 Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)";
 by (Asm_simp_tac 1);
 qed "bin_add_Min";
 
+Goalw [bin_add_def] "w: bin ==> bin_add(w,Min) = bin_pred(w)";
+by (etac bin.induct 1);
+by Auto_tac;
+qed "bin_add_Min_right";
+
 Goalw [bin_add_def] "bin_add(v BIT x,Pls) = v BIT x";
 by (Simp_tac 1);
 qed "bin_add_BIT_Pls";
@@ -166,6 +175,13 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
 qed_spec_mp "integ_of_add";
 
+(*Subtraction*)
+Goalw [zdiff_def]
+     "[| v: bin;  w: bin |]   \
+\     ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))";
+by (asm_simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
+qed "diff_integ_of_eq";
+
 
 (*** bin_mult: binary multiplication ***)
 
@@ -186,60 +202,64 @@
 
 Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
 by (Simp_tac 1);
-qed "bin_succ_BIT1";
+qed "bin_succ_1";
 
 Goal "bin_succ(w BIT 0) = NCons(w,1)";
 by (Simp_tac 1);
-qed "bin_succ_BIT0";
+qed "bin_succ_0";
 
 Goal "bin_pred(w BIT 1) = NCons(w,0)";
 by (Simp_tac 1);
-qed "bin_pred_BIT1";
+qed "bin_pred_1";
 
 Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
 by (Simp_tac 1);
-qed "bin_pred_BIT0";
+qed "bin_pred_0";
 
 (** extra rules for bin_minus **)
 
 Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))";
 by (Simp_tac 1);
-qed "bin_minus_BIT1";
+qed "bin_minus_1";
 
 Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
 by (Simp_tac 1);
-qed "bin_minus_BIT0";
+qed "bin_minus_0";
 
 (** extra rules for bin_add **)
 
 Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \
 \                    NCons(bin_add(v, bin_succ(w)), 0)";
 by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT11";
+qed "bin_add_BIT_11";
 
 Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) =  \
 \                    NCons(bin_add(v,w), 1)";
 by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT10";
+qed "bin_add_BIT_10";
 
-Goal "[| w: bin;  y: bool |] ==> \
-\           bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
+Goal "[| w: bin;  y: bool |] \
+\     ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
 by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT0";
+qed "bin_add_BIT_0";
 
 (** extra rules for bin_mult **)
 
 Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)";
 by (Simp_tac 1);
-qed "bin_mult_BIT1";
+qed "bin_mult_1";
 
 Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
 by (Simp_tac 1);
-qed "bin_mult_BIT0";
+qed "bin_mult_0";
 
 
 (** Simplification rules with integer constants **)
 
+Goal "$#0 = #0";
+by (Simp_tac 1);
+qed "int_of_0";
+
 Goal "#0 $+ z = intify(z)";
 by (Simp_tac 1);
 qed "zadd_0_intify";
@@ -272,6 +292,109 @@
 
 Addsimps [zmult_0, zmult_0_right];
 
+Goal "#-1 $* z = $-z";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zmult_minus1";
+
+Goal "z $* #-1 = $-z";
+by (stac zmult_commute 1);
+by (rtac zmult_minus1 1);
+qed "zmult_minus1_right";
+
+Addsimps [zmult_minus1, zmult_minus1_right];
+
+
+(*** Simplification rules for comparison of binary numbers (N Voelker) ***)
+
+(** Equals (=) **)
+
+Goalw [iszero_def]
+     "[| v: bin;  w: bin |]   \
+\     ==> ((integ_of(v)) = integ_of(w)) <-> \
+\         iszero (integ_of (bin_add (v, bin_minus(w))))"; 
+by (asm_simp_tac (simpset() addsimps
+              (zcompare_rls @ [integ_of_add, integ_of_minus])) 1); 
+qed "eq_integ_of_eq"; 
+
+Goalw [iszero_def] "iszero (integ_of(Pls))"; 
+by (Simp_tac 1); 
+qed "iszero_integ_of_Pls";
+
+
+Goalw [iszero_def] "~ iszero (integ_of(Min))"; 
+by (simp_tac (simpset() addsimps [zminus_equation]) 1);
+qed "nonzero_integ_of_Min"; 
+
+Goalw [iszero_def]
+     "[| w: bin; x: bool |] \
+\     ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"; 
+by (Simp_tac 1);
+by (subgoal_tac "integ_of(w) : int" 1);
+by (Asm_simp_tac 2);
+by (dtac int_cases 1);
+by (auto_tac (claset() addSEs [boolE], 
+              simpset() addsimps [int_of_add RS sym]));  
+by (ALLGOALS (asm_full_simp_tac 
+	      (simpset() addsimps zcompare_rls @ 
+			  [zminus_zadd_distrib RS sym, int_of_add RS sym])));
+by (subgoal_tac "znegative ($- $# succ(x)) <-> znegative ($# succ(x))" 1);
+by (Asm_simp_tac 2);
+by (Full_simp_tac 1);
+qed "iszero_integ_of_BIT"; 
+
+Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; 
+by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
+qed "iszero_integ_of_0"; 
+
+Goal "w: bin ==> ~ iszero (integ_of (w BIT 1))"; 
+by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
+qed "iszero_integ_of_1"; 
+
+
+
+(** Less-than (<) **)
+
+Goalw [zless_def,zdiff_def] 
+     "[| v: bin;  w: bin |]   \
+\     ==> integ_of(v) $< integ_of(w) \
+\         <-> znegative (integ_of (bin_add (v, bin_minus(w))))";
+by (asm_simp_tac (simpset() addsimps [integ_of_minus, integ_of_add]) 1);
+qed "less_integ_of_eq_neg"; 
+
+Goal "~ znegative (integ_of(Pls))"; 
+by (Simp_tac 1); 
+qed "not_neg_integ_of_Pls"; 
+
+Goal "znegative (integ_of(Min))"; 
+by (Simp_tac 1);
+qed "neg_integ_of_Min"; 
+
+Goal "[| w: bin; x: bool |] \
+\     ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"; 
+by (Asm_simp_tac 1); 
+by (subgoal_tac "integ_of(w) : int" 1);
+by (Asm_simp_tac 2);
+by (dtac int_cases 1);
+by (auto_tac (claset() addSEs [boolE], 
+              simpset() addsimps [int_of_add RS sym] @ zcompare_rls));  
+by (ALLGOALS (asm_full_simp_tac 
+	      (simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def,
+				   int_of_add RS sym])));
+by (subgoal_tac "$#1 $- $# succ(succ(x #+ x)) = $- $# succ(x #+ x)" 1);
+by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1);
+by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
+qed "neg_integ_of_BIT"; 
+
+Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; 
+by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
+qed "iszero_integ_of_0"; 
+
+(** Less-than-or-equals (<=) **)
+
+Goal "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+qed "le_integ_of_eq_not_less"; 
+
 
 (*Delete the original rewrites, with their clumsy conditional expressions*)
 Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
@@ -281,17 +404,69 @@
 Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
 
 
-Addsimps [integ_of_add RS sym,   (*invoke bin_add*)
-	  integ_of_minus RS sym, (*invoke bin_minus*)
-	  integ_of_mult RS sym,  (*invoke bin_mult*)
-	  bin_succ_Pls, bin_succ_Min,
-	  bin_succ_BIT1, bin_succ_BIT0,
-	  bin_pred_Pls, bin_pred_Min,
-	  bin_pred_BIT1, bin_pred_BIT0,
-	  bin_minus_Pls, bin_minus_Min,
-	  bin_minus_BIT1, bin_minus_BIT0,
-	  bin_add_Pls, bin_add_Min, bin_add_BIT_Pls, 
-	  bin_add_BIT_Min, bin_add_BIT_BIT0, 
-	  bin_add_BIT_BIT10, bin_add_BIT_BIT11,
-	  bin_mult_Pls, bin_mult_Min,
-	  bin_mult_BIT1, bin_mult_BIT0];
+bind_thms ("NCons_simps", 
+	   [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
+
+
+bind_thms ("bin_arith_extra_simps",
+    [integ_of_add RS sym,   (*invoke bin_add*)
+     integ_of_minus RS sym, (*invoke bin_minus*)
+     integ_of_mult RS sym,  (*invoke bin_mult*)
+     bin_succ_1, bin_succ_0, 
+     bin_pred_1, bin_pred_0, 
+     bin_minus_1, bin_minus_0,  
+     bin_add_Pls_right, bin_add_Min_right,
+     bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
+     diff_integ_of_eq,
+     bin_mult_1, bin_mult_0] @ NCons_simps);
+
+
+(*For making a minimal simpset, one must include these default simprules
+  of thy.  Also include simp_thms, or at least (~False)=True*)
+bind_thms ("bin_arith_simps",
+    [bin_pred_Pls, bin_pred_Min,
+     bin_succ_Pls, bin_succ_Min,
+     bin_add_Pls, bin_add_Min,
+     bin_minus_Pls, bin_minus_Min,
+     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
+
+(*Simplification of relational operations*)
+bind_thms ("bin_rel_simps",
+    [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
+     iszero_integ_of_0, iszero_integ_of_1,
+     less_integ_of_eq_neg,
+     not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
+     le_integ_of_eq_not_less]);
+
+Addsimps bin_arith_simps;
+Addsimps bin_rel_simps;
+
+
+(** Simplification of arithmetic when nested to the right **)
+
+Goal "[| v: bin;  w: bin |]   \
+\     ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)";
+by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+qed "add_integ_of_left";
+
+Goal "[| v: bin;  w: bin |]   \
+\     ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)";
+by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
+qed "mult_integ_of_left";
+
+Goalw [zdiff_def]
+    "[| v: bin;  w: bin |]   \
+\     ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)";
+by (rtac add_integ_of_left 1);
+by Auto_tac;  
+qed "add_integ_of_diff1";
+
+Goal "[| v: bin;  w: bin |]   \
+\     ==> integ_of(v) $+ (c $- integ_of(w)) = \
+\         integ_of (bin_add (v, bin_minus(w))) $+ (c)";
+by (stac (diff_integ_of_eq RS sym) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zdiff_def::zadd_ac)));
+qed "add_integ_of_diff2";
+
+Addsimps [add_integ_of_left, mult_integ_of_left,
+	  add_integ_of_diff1, add_integ_of_diff2]; 
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Integ/Bin.thy
--- a/src/ZF/Integ/Bin.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Bin.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -18,13 +18,13 @@
 Division is not defined yet!
 *)
 
-Bin = Int + Datatype + 
+Bin = Int + Datatype +
 
 consts  bin :: i
 datatype
   "bin" = Pls
         | Min
-        | BIT ("w: bin", "b: bool")	(infixl 90)
+        | Bit ("w: bin", "b: bool")	(infixl "BIT" 90)
 
 syntax
   "_Int"           :: xnum => i        ("_")
@@ -104,85 +104,9 @@
     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
 				 NCons(bin_mult(v,w),0))"
 
+setup NumeralSyntax.setup
+
 end
 
 
 ML
-
-(** Concrete syntax for integers **)
-
-local
-  open Syntax;
-
-  (* Bits *)
-
-  fun mk_bit 0 = const "0"
-    | mk_bit 1 = const "succ" $ const "0"
-    | mk_bit _ = sys_error "mk_bit";
-
-  fun dest_bit (Const ("0", _)) = 0
-    | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
-    | dest_bit _ = raise Match;
-
-
-  (* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
-
-  fun prefix_len _ [] = 0
-    | prefix_len pred (x :: xs) =
-        if pred x then 1 + prefix_len pred xs else 0;
-
-  fun mk_bin str =
-    let
-      val (sign, digs) =
-        (case Symbol.explode str of
-          "#" :: "-" :: cs => (~1, cs)
-        | "#" :: cs => (1, cs)
-        | _ => raise ERROR);
-
-      val zs = prefix_len (equal "0") digs;
-
-      fun bin_of 0  = []
-        | bin_of ~1 = [~1]
-        | bin_of n  = (n mod 2) :: bin_of (n div 2);
-
-      fun term_of [] = const "Pls"
-        | term_of [~1] = const "Min"
-        | term_of (b :: bs) = const "op BIT" $ term_of bs $ mk_bit b;
-    in
-      term_of (bin_of (sign * (#1 (read_int digs))))
-    end;
-
-  fun dest_bin tm =
-    let
-      fun bin_of (Const ("Pls", _)) = []
-        | bin_of (Const ("Min", _)) = [~1]
-        | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
-        | bin_of _ = raise Match;
-
-      fun integ_of [] = 0
-        | integ_of (b :: bs) = b + 2 * integ_of bs;
-
-      val rev_digs = bin_of tm;
-      val (sign, zs) =
-        (case rev rev_digs of
-          ~1 :: bs => ("-", prefix_len (equal 1) bs)
-        | bs => ("", prefix_len (equal 0) bs));
-      val num = string_of_int (abs (integ_of rev_digs));
-    in
-      "#" ^ sign ^ implode (replicate zs "0") ^ num
-    end;
-
-
-  (* translation of integer constant tokens to and from binary *)
-
-  fun int_tr (*"_Int"*) [t as Free (str, _)] =
-        (const "integ_of" $
-          (mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
-    | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
-
-  fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
-    | int_tr' (*"integ_of"*) _ = raise Match;
-in
-  val parse_translation = [("_Int", int_tr)];
-  val print_translation = [("integ_of", int_tr')];
-end;
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Integ/Int.ML
--- a/src/ZF/Integ/Int.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Int.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -9,7 +9,6 @@
 "znegative(z) ==> $# zmagnitude(z) = $- z"
 "~ znegative(z) ==> $# zmagnitude(z) = z"
 $+ and $* are monotonic wrt $<
-[| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
 *)
 
 AddSEs [quotientE];
@@ -169,6 +168,15 @@
 qed "zless_intify2";
 Addsimps [zless_intify1, zless_intify2];
 
+Goal "intify(x) $<= y <-> x $<= y";
+by (simp_tac (simpset() addsimps [zle_def]) 1);
+qed "zle_intify1";
+
+Goal "x $<= intify(y) <-> x $<= y";
+by (simp_tac (simpset() addsimps [zle_def]) 1);
+qed "zle_intify2";
+Addsimps [zle_intify1, zle_intify2];
+
 
 (**** zminus: unary negation on int ****)
 
@@ -296,6 +304,7 @@
 by (rtac theI2 1);
 by Auto_tac;
 qed "zmagnitude_type";
+AddIffs [zmagnitude_type];
 AddTCs [zmagnitude_type];
 
 Goalw [int_def, znegative_def, int_of_def]
@@ -317,7 +326,6 @@
 
 Addsimps [not_zneg_mag];
 
-
 Goalw [int_def, znegative_def, int_of_def]
      "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))"; 
 by (auto_tac(claset() addSDs [less_imp_succ_add], 
@@ -331,6 +339,12 @@
 
 Addsimps [zneg_mag];
 
+Goal "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))"; 
+by (case_tac "znegative(z)" 1);
+by (blast_tac (claset() addDs [not_zneg_mag, sym]) 2);
+by (blast_tac (claset() addDs [zneg_int_of]) 1);
+qed "int_cases"; 
+
 
 (**** zadd: addition on int ****)
 
@@ -434,6 +448,17 @@
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "int_of_add";
 
+Goal "$# succ(m) = $# 1 $+ ($# m)";
+by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
+qed "int_succ_int_1";
+
+Goalw [int_of_def,zdiff_def]
+     "[| m: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)";
+by (ftac lt_nat_in_nat 1);
+by (asm_simp_tac (simpset() addsimps [zadd,zminus,add_diff_inverse2]) 2);
+by Auto_tac;  
+qed "int_of_diff";
+
 Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
 by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
 qed "raw_zadd_zminus_inverse";
@@ -550,11 +575,10 @@
 qed "zmult_zminus";
 Addsimps [zmult_zminus];
 
-Goal "($- z) $* ($- w) = (z $* w)";
-by (stac zmult_zminus 1);
-by (stac zmult_commute 1 THEN stac zmult_zminus 1);
-by (simp_tac (simpset() addsimps [zmult_commute])1);
-qed "zmult_zminus_zminus";
+Goal "w $* ($- z) = $- (w $* z)";
+by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute]) 1);
+qed "zmult_zminus_right";
+Addsimps [zmult_zminus_right];
 
 Goalw [int_def]
     "[| z1: int;  z2: int;  z3: int |]   \
@@ -602,6 +626,11 @@
 
 (*** Subtraction laws ***)
 
+Goal "z $- w : int";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_type";
+AddIffs [zdiff_type];  AddTCs [zdiff_type];
+
 Goal "$#0 $- x = $-x";
 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
 qed "zdiff_int0";
@@ -616,6 +645,15 @@
 
 Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
 
+Goal "$- (z $- y) = y $- z";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
+qed "zminus_zdiff_eq";
+Addsimps [zminus_zdiff_eq];
+
+Goal "$- (z $- y) = y $- z";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
+qed "zminus_zdiff_eq";
+Addsimps [zminus_zdiff_eq];
 
 Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
 by (stac zadd_zmult_distrib 1);
@@ -719,21 +757,57 @@
 by Auto_tac;  
 qed "zless_trans";
 
+(*** "Less Than or Equals", $<= ***)
 
 Goalw [zle_def] "z $<= z";
 by Auto_tac;  
 qed "zle_refl";
 
-Goalw [zle_def] "[| x $<= y; y $<= x |] ==> x=y";
+Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
+by Auto_tac;  
 by (blast_tac (claset() addDs [zless_trans]) 1);
 qed "zle_anti_sym";
 
-Goalw [zle_def] "[| x $<= y; y $<= z |] ==> x $<= z";
+Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";
+by Auto_tac;  
 by (blast_tac (claset() addIs [zless_trans]) 1);
+val lemma = result();
+
+Goal "[| x $<= y; y $<= z |] ==> x $<= z";
+by (subgoal_tac "intify(x) $<= intify(z)" 1);
+by (res_inst_tac [("y", "intify(y)")] lemma 2);
+by Auto_tac;  
 qed "zle_trans";
 
+Goal "[| i $<= j; j $< k |] ==> i $< k";
+by (auto_tac (claset(), simpset() addsimps [zle_def]));  
+by (blast_tac (claset() addIs [zless_trans]) 1);
+by (asm_full_simp_tac (simpset() addsimps [zless_def, zdiff_def, zadd_def]) 1);
+qed "zle_zless_trans";
 
-(*** More subtraction laws (for zcompare_rls): useful? ***)
+Goal "[| i $< j; j $<= k |] ==> i $< k";
+by (auto_tac (claset(), simpset() addsimps [zle_def]));  
+by (blast_tac (claset() addIs [zless_trans]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [zless_def, zdiff_def, zminus_def]) 1);
+qed "zless_zle_trans";
+
+Goal "~ (z $< w) <-> (w $<= z)";
+by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
+by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));  
+by (auto_tac (claset(), 
+            simpset() addsimps [zless_def, zdiff_def, zadd_def, zminus_def]));
+by (fold_tac [zless_def, zdiff_def, zadd_def, zminus_def]);
+by Auto_tac;  
+qed "not_zless_iff_zle";
+
+Goal "~ (z $<= w) <-> (w $< z)";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+qed "not_zle_iff_zless";
+
+
+
+(*** More subtraction laws (for zcompare_rls) ***)
 
 Goal "(x $- y) $- z = x $- (y $+ z)";
 by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
@@ -759,16 +833,33 @@
 by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
 qed "eq_zdiff_iff";
 
-(**Could not prove these!
 Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
-by (asm_simp_tac (simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]) 1);
-by Auto_tac;  
+by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zdiff_zless_iff]));  
+val lemma = result();
+
+Goal "(x$-y $<= z) <-> (x $<= z $+ y)";
+by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
+by (Asm_full_simp_tac 1);
 qed "zdiff_zle_iff";
 
-Goalw [zle_def] "(x $<= z$-y) <-> (x $+ y $<= z)";
-by (simp_tac (simpset() addsimps [zdiff_zless_iff]) 1);
+Goalw [zle_def] "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)";
+by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]));  
+by (auto_tac (claset(), simpset() addsimps [zdiff_def, zadd_assoc]));  
+val lemma = result();
+
+Goal "(x $<= z$-y) <-> (x $+ y $<= z)";
+by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
+by (Asm_full_simp_tac 1);
 qed "zle_zdiff_iff";
-**)
+
+(*This list of rewrites simplifies (in)equalities by bringing subtractions
+  to the top and then moving negative terms to the other side.  
+  Use with zadd_ac*)
+bind_thms ("zcompare_rls",
+    [symmetric zdiff_def,
+     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
+     zdiff_zless_iff, zless_zdiff_iff, zdiff_zle_iff, zle_zdiff_iff, 
+     zdiff_eq_iff, eq_zdiff_iff]);
 
 
 (*** Monotonicity/cancellation results that could allow instantiation
@@ -816,14 +907,24 @@
 Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
 
 
-Goal "(w' $+ z $<= w $+ z) <-> (intify(w') $<= intify(w))";
+Goal "(w' $+ z $<= w $+ z) <-> w' $<= w";
 by (simp_tac (simpset() addsimps [zle_def]) 1);
 qed "zadd_right_cancel_zle";
 
-Goal "(z $+ w' $<= z $+ w) <->  (intify(w') $<= intify(w))";
+Goal "(z $+ w' $<= z $+ w) <->  w' $<= w";
 by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
                                   zadd_right_cancel_zle]) 1);
 qed "zadd_left_cancel_zle";
 
 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
 
+
+(*** More inequality lemmas ***)
+
+Goal "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)";
+by Auto_tac;
+qed "equation_zminus";
+
+Goal "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)";
+by Auto_tac;
+qed "zminus_equation";
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Integ/Int.thy
--- a/src/ZF/Integ/Int.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Int.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -30,7 +30,10 @@
 
   znegative   ::      i=>o
     "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
-  
+
+  iszero      ::      i=>o
+    "iszero(z) == z = $# 0"
+    
   zmagnitude  ::      i=>i
     "zmagnitude(z) ==
      THE m. m : nat & ((~ znegative(z) & z = $# m) |
@@ -62,7 +65,7 @@
      "z1 $< z2 == znegative(z1 $- z2)"
   
   zle          ::      [i,i]=>o      (infixl "$<=" 50)
-     "z1 $<= z2 == z1 $< z2 | z1=z2"
+     "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
   
 (*div and mod await definitions!*)
 consts
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Integ/IntArith.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/IntArith.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -0,0 +1,5 @@
+
+theory IntArith = Bin
+files "int_arith.ML":
+
+end
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Integ/int_arith.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/int_arith.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -0,0 +1,391 @@
+(*  Title:      ZF/Integ/int_arith.ML
+    ID:         $Id$
+    Author:    Larry Paulson
+    Copyright   2000  University of Cambridge
+
+Simprocs for linear arithmetic.
+*)
+
+(*** Simprocs for numeric literals ***)
+
+(** Combining of literal coefficients in sums of products **)
+
+Goal "(x $< y) <-> (x$-y $< #0)";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zless_iff_zdiff_zless_0";
+
+Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
+by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "eq_iff_zdiff_eq_0";
+
+Goal "(x $<= y) <-> (x$-y $<= #0)";
+by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zle_iff_zdiff_zle_0";
+
+
+(** For combine_numerals **)
+
+Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
+by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1);
+qed "left_zadd_zmult_distrib";
+
+
+(** For cancel_numerals **)
+
+val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
+                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
+			   zle_iff_zdiff_zle_0] @
+		        map (inst "y" "n")
+                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
+			   zle_iff_zdiff_zle_0];
+
+Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "eq_add_iff1";
+
+Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "eq_add_iff2";
+
+Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+                                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "less_add_iff1";
+
+Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+                                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "less_add_iff2";
+
+Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= intify(n))";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "le_add_iff1";
+
+Goal "(i$*u $+ m $<= j$*u $+ n) <-> (intify(m) $<= (j$-i)$*u $+ n)";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "le_add_iff2";
+
+
+structure Int_Numeral_Simprocs =
+struct
+
+(*Utilities*)
+
+val integ_of_const = Const ("Bin.integ_of", iT --> iT);
+
+fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
+
+(*Decodes a binary INTEGER*)
+fun dest_numeral (Const("Bin.integ_of", _) $ w) = 
+     (NumeralSyntax.dest_bin w
+      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+
+fun find_first_numeral past (t::terms) =
+	((dest_numeral t, rev past @ terms)
+	 handle TERM _ => find_first_numeral (t::past) terms)
+  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+
+val zero = mk_numeral 0;
+val mk_plus = FOLogic.mk_binop "Int.zadd";
+
+val iT = Ind_Syntax.iT;
+
+val zminus_const = Const ("Int.zminus", iT --> iT);
+
+(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
+fun mk_sum []        = zero
+  | mk_sum [t,u]     = mk_plus (t, u)
+  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum []        = zero
+  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
+
+(*decompose additions AND subtractions as a sum*)
+fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
+        dest_summing (pos, t, dest_summing (pos, u, ts))
+  | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
+        dest_summing (pos, t, dest_summing (not pos, u, ts))
+  | dest_summing (pos, t, ts) =
+	if pos then t::ts else zminus_const$t :: ts;
+
+fun dest_sum t = dest_summing (true, t, []);
+
+val mk_diff = FOLogic.mk_binop "Int.zdiff";
+val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
+
+val one = mk_numeral 1;
+val mk_times = FOLogic.mk_binop "Int.zmult";
+
+fun mk_prod [] = one
+  | mk_prod [t] = t
+  | mk_prod (t :: ts) = if t = one then mk_prod ts
+                        else mk_times (t, mk_prod ts);
+
+val dest_times = FOLogic.dest_bin "Int.zmult" iT;
+
+fun dest_prod t =
+      let val (t,u) = dest_times t 
+      in  dest_prod t @ dest_prod u  end
+      handle TERM _ => [t];
+
+(*DON'T do the obvious simplifications; that would create special cases*) 
+fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
+
+(*Express t as a product of (possibly) a numeral with other sorted terms*)
+fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
+  | dest_coeff sign t =
+    let val ts = sort Term.term_ord (dest_prod t)
+	val (n, ts') = find_first_numeral [] ts
+                          handle TERM _ => (1, ts)
+    in (sign*n, mk_prod ts') end;
+
+(*Find first coefficient-term THAT MATCHES u*)
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
+  | find_first_coeff past u (t::terms) =
+	let val (n,u') = dest_coeff 1 t
+	in  if u aconv u' then (n, rev past @ terms)
+			  else find_first_coeff (t::past) u terms
+	end
+	handle TERM _ => find_first_coeff (t::past) u terms;
+
+
+(*Simplify #1*n and n*#1 to n*)
+val add_0s = [zadd_0_intify, zadd_0_right_intify];
+
+val mult_1s = [zmult_1_intify, zmult_1_right_intify, 
+               zmult_minus1, zmult_minus1_right];
+
+val tc_rules = [integ_of_type, intify_in_int, 
+                zadd_type, zdiff_type, zmult_type] @ bin.intrs;
+val intifys = [intify_ident, zadd_intify1, zadd_intify2,
+               zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
+               zless_intify1, zless_intify2, zle_intify1, zle_intify2];
+
+(*To perform binary arithmetic*)
+val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;
+
+(*To evaluate binary negations of coefficients*)
+val zminus_simps = NCons_simps @
+                   [integ_of_minus RS sym, 
+		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+
+(*To let us treat subtraction as addition*)
+val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
+                      (s, TypeInfer.anyT ["logic"]);
+val prep_pats = map prep_pat;
+
+structure CancelNumeralsCommon =
+  struct
+  val mk_sum    	= mk_sum
+  val dest_sum		= dest_sum
+  val mk_coeff		= mk_coeff
+  val dest_coeff	= dest_coeff 1
+  val find_first_coeff	= find_first_coeff []
+  val trans_tac		= ArithData.gen_trans_tac iff_trans
+  val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
+                                    zminus_simps@zadd_ac
+  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
+                                    bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
+  val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
+			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
+  end;
+
+
+structure EqCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
+  val mk_bal   = FOLogic.mk_eq
+  val dest_bal = FOLogic.dest_bin "op =" iT
+  val bal_add1 = eq_add_iff1 RS iff_trans
+  val bal_add2 = eq_add_iff2 RS iff_trans
+);
+
+structure LessCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
+  val mk_bal   = FOLogic.mk_binrel "Int.zless"
+  val dest_bal = FOLogic.dest_bin "Int.zless" iT
+  val bal_add1 = less_add_iff1 RS iff_trans
+  val bal_add2 = less_add_iff2 RS iff_trans
+);
+
+structure LeCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
+  val mk_bal   = FOLogic.mk_binrel "Int.zle"
+  val dest_bal = FOLogic.dest_bin "Int.zle" iT
+  val bal_add1 = le_add_iff1 RS iff_trans
+  val bal_add2 = le_add_iff2 RS iff_trans
+);
+
+val cancel_numerals = 
+  map prep_simproc
+   [("inteq_cancel_numerals",
+     prep_pats ["l $+ m = n", "l = m $+ n", 
+		"l $- m = n", "l = m $- n", 
+		"l $* m = n", "l = m $* n"], 
+     EqCancelNumerals.proc),
+    ("intless_cancel_numerals", 
+     prep_pats ["l $+ m $< n", "l $< m $+ n", 
+		"l $- m $< n", "l $< m $- n", 
+		"l $* m $< n", "l $< m $* n"], 
+     LessCancelNumerals.proc),
+    ("intle_cancel_numerals", 
+     prep_pats ["l $+ m $<= n", "l $<= m $+ n", 
+		"l $- m $<= n", "l $<= m $- n", 
+		"l $* m $<= n", "l $<= m $* n"], 
+     LeCancelNumerals.proc)];
+
+
+(*version without the hyps argument*)
+fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
+
+structure CombineNumeralsData =
+  struct
+  val add		= op + : int*int -> int 
+  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x $+ #3*x *)
+  val dest_sum		= dest_sum
+  val mk_coeff		= mk_coeff
+  val dest_coeff	= dest_coeff 1
+  val left_distrib	= left_zadd_zmult_distrib RS trans
+  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
+  val trans_tac         = ArithData.gen_trans_tac trans
+  val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
+                                    zminus_simps@zadd_ac
+  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
+                                    bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
+  val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
+			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
+  end;
+
+structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+  
+val combine_numerals = 
+    prep_simproc ("int_combine_numerals",
+		  prep_pats ["i $+ j", "i $- j"],
+		  CombineNumerals.proc);
+
+
+
+(** Constant folding for integer multiplication **)
+
+(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
+  the "sum" of #3, x, #4; the literals are then multiplied*)
+structure CombineNumeralsProdData =
+  struct
+  val add		= op * : int*int -> int
+  val mk_sum    	= mk_prod
+  val dest_sum		= dest_prod
+  fun mk_coeff (k, t) = mk_numeral k
+  val dest_coeff	= dest_coeff 1
+  val left_distrib	= zmult_assoc RS sym RS trans
+  val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
+  val trans_tac         = ArithData.gen_trans_tac trans
+  val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
+  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
+                                    bin_simps@zmult_ac@tc_rules@intifys
+  val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
+			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps bin_simps))
+  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
+  end;
+
+
+structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
+  
+val combine_numerals_prod = 
+    prep_simproc ("int_combine_numerals_prod",
+		  prep_pats ["i $* j", "i $* j"],
+		  CombineNumeralsProd.proc);
+
+end;
+
+
+Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
+Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
+	     Int_Numeral_Simprocs.combine_numerals_prod];
+
+
+(*examples:*)
+(*
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1)); 
+val sg = #sign (rep_thm (topthm()));
+val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
+val (t,_) = FOLogic.dest_eq t;
+
+(*combine_numerals_prod (products of separate literals) *)
+test "#5 $* x $* #3 = y";
+
+test "y2 $+ ?x42 = y $+ y2";
+
+test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
+
+test "#9$*x $+ y = x$*#23 $+ z";
+test "y $+ x = x $+ z";
+
+test "x : int ==> x $+ y $+ z = x $+ z";
+test "x : int ==> y $+ (z $+ x) = z $+ x";
+test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
+test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
+
+test "#-3 $* x $+ y $<= x $* #2 $+ z";
+test "y $+ x $<= x $+ z";
+test "x $+ y $+ z $<= x $+ z";
+
+test "y $+ (z $+ x) $< z $+ x";
+test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
+test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
+
+test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
+test "u : int ==> #2 $* u = u";
+test "(i $+ j $+ #12 $+ k) $- #15 = y";
+test "(i $+ j $+ #12 $+ k) $- #5 = y";
+
+test "y $- b $< b";
+test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
+
+test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
+test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
+test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
+test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
+
+test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
+test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
+
+test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv";
+
+test "a $+ $-(b$+c) $+ b = d";
+test "a $+ $-(b$+c) $- b = d";
+
+(*negative numerals*)
+test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
+test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
+test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
+test "(i $+ j $+ #-12 $+ k) $- #15 = y";
+test "(i $+ j $+ #12 $+ k) $- #-15 = y";
+test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
+*)
+
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/IsaMakefile	Thu Aug 10 11:27:34 2000 +0200
@@ -33,11 +33,14 @@
   Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
   Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML		\
   Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	\
-  Integ/Int.thy Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy	\
+  Integ/Int.thy Integ/twos_compl.ML \
+  Integ/int_arith.ML Integ/IntArith.thy \
+  Let.ML Let.thy List.ML List.thy	\
   Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML		\
   OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
   Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
-  Rel.ML Rel.thy Sum.ML Sum.thy Tools/cartprod.ML			\
+  Rel.ML Rel.thy Sum.ML Sum.thy \
+  Tools/numeral_syntax.ML Tools/cartprod.ML			\
   Tools/datatype_package.ML Tools/induct_tacs.ML			\
   Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML	\
   Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Main.thy
--- a/src/ZF/Main.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Main.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -2,5 +2,5 @@
 (*$Id$
   theory Main includes everything*)
 
-Main = Update + InfDatatype + List + EquivClass + Bin
+Main = Update + InfDatatype + List + EquivClass + IntArith
 
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Perm.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -9,7 +9,7 @@
   -- Lemmas for the Schroeder-Bernstein Theorem
 *)
 
-Perm = upair + mono + func +
+Perm = mono + func +
 consts
   O     :: [i,i]=>i      (infixr 60)
 
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/ROOT.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -19,9 +19,8 @@
 use     "thy_syntax";
 
 use "~~/src/Provers/Arith/cancel_numerals.ML";
+use "~~/src/Provers/Arith/combine_numerals.ML";
 
-use_thy "ZF";
-use     "Tools/typechk";
 use_thy "mono";
 use     "ind_syntax";
 use     "Tools/cartprod";
@@ -32,6 +31,7 @@
 use_thy "QUniv";
 use     "Tools/datatype_package";
 
+use     "Tools/numeral_syntax";
 (*the all-in-one theory*)
 with_path "Integ" use_thy "Main";
 
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/Tools/numeral_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Tools/numeral_syntax.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -0,0 +1,117 @@
+(*  Title:      ZF/Tools/numeral_syntax.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Concrete syntax for generic numerals.  Assumes consts and syntax of
+theory ZF/Integ/Bin.
+*)
+
+signature NUMERAL_SYNTAX =
+sig
+  val dest_bin : term -> int
+  val mk_bin   : int -> term
+  val int_tr   : term list -> term
+  val int_tr'  : bool -> typ -> term list -> term
+  val setup    : (theory -> theory) list
+end;
+
+structure NumeralSyntax: NUMERAL_SYNTAX =
+struct
+
+open Syntax;
+
+(* Bits *)
+
+val zero = Const("0", iT);
+val succ = Const("succ", iT --> iT);
+
+fun mk_bit 0 = zero
+  | mk_bit 1 = succ$zero
+  | mk_bit _ = sys_error "mk_bit";
+
+fun dest_bit (Const ("0", _)) = 0
+  | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
+  | dest_bit _ = raise Match;
+
+
+(* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
+
+fun prefix_len _ [] = 0
+  | prefix_len pred (x :: xs) =
+      if pred x then 1 + prefix_len pred xs else 0;
+
+fun scan_int str =
+  let val (sign, digs) =
+       (case Symbol.explode str of
+	 "#" :: "-" :: cs => (~1, cs)
+       | "#" :: cs => (1, cs)
+       | _ => raise ERROR);
+
+  in  sign * (#1 (read_int digs))  end;
+
+
+val pls_const = Const ("Bin.bin.Pls", iT)
+and min_const = Const ("Bin.bin.Min", iT)
+and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
+
+fun mk_bin i =
+  let fun bin_of 0  = []
+	| bin_of ~1 = [~1]
+	| bin_of n  = (n mod 2) :: bin_of (n div 2);
+
+      fun term_of []   = pls_const
+	| term_of [~1] = min_const
+	| term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
+  in
+    term_of (bin_of i)
+  end;
+
+(*we consider all "spellings", since they could vary depending on the caller*)
+fun bin_of (Const ("Pls", _)) = []
+  | bin_of (Const ("bin.Pls", _)) = []
+  | bin_of (Const ("Bin.bin.Pls", _)) = []
+  | bin_of (Const ("Min", _)) = [~1]
+  | bin_of (Const ("bin.Min", _)) = [~1]
+  | bin_of (Const ("Bin.bin.Min", _)) = [~1]
+  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+  | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+  | bin_of _ = raise Match;
+
+fun integ_of [] = 0
+  | integ_of (b :: bs) = b + 2 * integ_of bs;
+
+val dest_bin = integ_of o bin_of;
+
+(*leading 0s and (for negative numbers) -1s cause complications,
+  though they should never arise in normal use.*)
+fun show_int t =
+  let
+    val rev_digs = bin_of t;
+    val (sign, zs) =
+	(case rev rev_digs of
+	     ~1 :: bs => ("-", prefix_len (equal 1) bs)
+	   | bs =>       ("",  prefix_len (equal 0) bs));
+    val num = string_of_int (abs (integ_of rev_digs));
+  in
+    "#" ^ sign ^ implode (replicate zs "0") ^ num
+  end;
+
+
+
+(* translation of integer constant tokens to and from binary *)
+
+fun int_tr (*"_Int"*) [t as Free (str, _)] =
+      (const "integ_of" $
+	(mk_bin (scan_int str) handle ERROR => raise TERM ("int_tr", [t])))
+  | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
+
+fun int_tr' _ _ (*"integ_of"*) [t] = const "_Int" $ free (show_int t)
+  | int_tr' (_:bool) (_:typ)     _ = raise Match;
+
+
+val setup =
+ [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
+  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
+
+end;
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/arith_data.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -8,9 +8,16 @@
 
 signature ARITH_DATA =
 sig
+  (*the main outcome*)
   val nat_cancel: simproc list
+  (*tools for use in similar applications*)
+  val gen_trans_tac: thm -> thm option -> tactic
+  val prove_conv: string -> tactic list -> Sign.sg -> 
+                  thm list -> term * term -> thm option
+  val simplify_meta_eq: thm list -> thm -> thm
 end;
 
+
 structure ArithData: ARITH_DATA =
 struct
 
@@ -21,11 +28,7 @@
 fun mk_succ t = succ $ t;
 val one = mk_succ zero;
 
-(*Not FOLogic.mk_binop, since it calls fastype_of, which can fail*)
-fun mk_binop_i  c (t,u) = Const (c, [iT,iT] ---> iT) $ t $ u;
-fun mk_binrel_i c (t,u) = Const (c, [iT,iT] ---> oT) $ t $ u;
-
-val mk_plus = mk_binop_i "Arith.add";
+val mk_plus = FOLogic.mk_binop "Arith.add";
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -81,7 +84,7 @@
 (*** Use CancelNumerals simproc without binary numerals, 
      just for cancellation ***)
 
-val mk_times = mk_binop_i "Arith.mult";
+val mk_times = FOLogic.mk_binop "Arith.mult";
 
 fun mk_prod [] = one
   | mk_prod [t] = t
@@ -120,14 +123,14 @@
 val mult_1s = [mult_1_natify, mult_1_right_natify];
 val tc_rules = [natify_in_nat, add_type, diff_type, mult_type];
 val natifys = [natify_0, natify_ident, add_natify1, add_natify2,
-               add_natify1, add_natify2, diff_natify1, diff_natify2];
+               diff_natify1, diff_natify2];
 
 (*Final simplification: cancel + and **)
 fun simplify_meta_eq rules =
     mk_meta_eq o
     simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2] 
                      delsimps iff_simps (*these could erase the whole rule!*)
-		     addsimps rules)
+		     addsimps rules);
 
 val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
 
@@ -161,7 +164,7 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = prove_conv "natless_cancel_numerals"
-  val mk_bal   = mk_binrel_i "Ordinal.op <"
+  val mk_bal   = FOLogic.mk_binrel "Ordinal.op <"
   val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
   val bal_add1 = less_add_iff RS iff_trans
   val bal_add2 = less_add_iff RS iff_trans
@@ -171,7 +174,7 @@
 structure DiffCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = prove_conv "natdiff_cancel_numerals"
-  val mk_bal   = mk_binop_i "Arith.diff"
+  val mk_bal   = FOLogic.mk_binop "Arith.diff"
   val dest_bal = FOLogic.dest_bin "Arith.diff" iT
   val bal_add1 = diff_add_eq RS trans
   val bal_add2 = diff_add_eq RS trans
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/ex/BinEx.ML
--- a/src/ZF/ex/BinEx.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/ex/BinEx.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -51,3 +51,30 @@
 Goal "#1359  $*  #-2468 = #-3354012";
 by (Simp_tac 1);    (*1.04 secs*)
 result();
+
+
+(** Comparisons **)
+
+Goal "(#89) $* #10 ~= #889";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#13) $< #18 $- #4";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#-345) $< #-242 $+ #-100";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#13557456) $< #18678654";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#999999) $<= (#1000001 $+ #1) $- #2";  
+by (Simp_tac 1); 
+result();
+
+Goal "(#1234567) $<= #1234567";  
+by (Simp_tac 1); 
+result();
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/pair.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -1,4 +1,5 @@
-(*Dummy theory to document dependencies *)
+theory pair = upair
+files "simpdata":
+end
 
-pair = upair
 
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/simpdata.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -10,7 +10,7 @@
 
 local
   (*For proving rewrite rules*)
-  fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
+  fun prover s = (prove_goal (the_context ()) s (fn _ => [Blast_tac 1]));
 
 in
 
@@ -106,7 +106,8 @@
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
 simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
-                           addsplits [split_if]
+                           addcongs [if_weak_cong]
+		           addsplits [split_if]
                            setSolver (mk_solver "types" Type_solver_tac);
 
 val ZF_ss = simpset();
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/subset.thy
--- a/src/ZF/subset.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/subset.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-subset = upair
+subset = pair
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/upair.ML	Thu Aug 10 11:27:34 2000 +0200
@@ -269,6 +269,12 @@
 by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
 qed "if_cong";
 
+(*Prevents simplification of x and y: faster and allows the execution
+  of functional programs. NOW THE DEFAULT.*)
+Goal "P<->Q ==> (if P then x else y) = (if Q then x else y)";
+by (Asm_simp_tac 1);
+qed "if_weak_cong";
+
 (*Not needed for rewriting, since P would rewrite to True anyway*)
 Goalw [if_def] "P ==> (if P then a else b) = a";
 by (Blast_tac 1);
@@ -398,4 +404,3 @@
 (*Not needed now that cons is available.  Deletion reduces the search space.*)
 Delrules [UpairI1,UpairI2,UpairE];
 
-use"simpdata.ML";
diff -r 68400ff46b09 -r e16e168984e1 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/upair.thy	Thu Aug 10 11:27:34 2000 +0200
@@ -6,7 +6,8 @@
 Dummy theory, but holds the standard ZF simpset.
 *)
 
-upair = ZF +
+theory upair = ZF
+files "Tools/typechk":
 
 setup
   TypeCheck.setup