coercion "intify" to remove type constraints from integer algebraic laws

--- a/src/ZF/Integ/Int.ML	Wed Aug 02 16:06:54 2000 +0200
+++ b/src/ZF/Integ/Int.ML	Wed Aug 02 16:07:32 2000 +0200
@@ -25,8 +25,8 @@
 qed "intrel_iff";
 
 Goalw [intrel_def]
-    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
-\             <<x1,y1>,<x2,y2>>: intrel";
+    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]  \
+\    ==> <<x1,y1>,<x2,y2>>: intrel";
 by (fast_tac (claset() addIs prems) 1);
 qed "intrelI";
 
@@ -66,6 +66,11 @@
 qed "equiv_intrel";
 
 
+Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
+by (blast_tac (claset() addIs [quotientI]) 1);
+qed "image_intrel_int";
+
+
 Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
 	  add_0_right, add_succ_right];
 Addcongs [conj_cong];
@@ -74,25 +79,78 @@
 
 (** int_of: the injection from nat to int **)
 
-Goalw [int_def,quotient_def,int_of_def]
-    "m : nat ==> $#m : int";
+Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
 by Auto_tac;
 qed "int_of_type";
 
-Addsimps [int_of_type];
-AddTCs   [int_of_type];
+AddIffs [int_of_type];
+AddTCs  [int_of_type];
+
 
-Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
-by (dtac (sym RS eq_intrelD) 1);
+Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
+by Auto_tac;  
+qed "int_of_eq"; 
+AddIffs [int_of_eq];
+
+Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
+by (dtac (int_of_eq RS iffD1) 1);
 by Auto_tac;
 qed "int_of_inject";
 
-AddSDs [int_of_inject];
+
+(** intify: coercion from anything to int **)
+
+Goal "intify(x) : int";
+by (simp_tac (simpset() addsimps [intify_def]) 1);
+qed "intify_in_int";
+AddIffs [intify_in_int];
+AddTCs [intify_in_int];
+
+Goal "n : int ==> intify(n) = n";
+by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
+qed "intify_ident";
+Addsimps [intify_ident];
+
+
+(*** Collapsing rules: to remove intify from arithmetic expressions ***)
+
+Goal "intify(intify(x)) = intify(x)";
+by (Simp_tac 1);
+qed "intify_idem";
+Addsimps [intify_idem];
+
+Goal "$# (natify(m)) = $# m";
+by (simp_tac (simpset() addsimps [int_of_def]) 1);
+qed "int_of_natify";
 
-Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
-by (Blast_tac 1); 
-qed "int_of_eq"; 
-Addsimps [int_of_eq]; 
+Goal "$~ (intify(m)) = $~ m";
+by (simp_tac (simpset() addsimps [zminus_def]) 1);
+qed "zminus_intify";
+
+Addsimps [int_of_natify, zminus_intify];
+
+(** Addition **)
+
+Goal "intify(x) $+ y = x $+ y";
+by (simp_tac (simpset() addsimps [zadd_def]) 1);
+qed "zadd_intify1";
+
+Goal "x $+ intify(y) = x $+ y";
+by (simp_tac (simpset() addsimps [zadd_def]) 1);
+qed "zadd_intify2";
+Addsimps [zadd_intify1, zadd_intify2];
+
+(** Multiplication **)
+
+Goal "intify(x) $* y = x $* y";
+by (simp_tac (simpset() addsimps [zmult_def]) 1);
+qed "zmult_intify1";
+
+Goal "x $* intify(y) = x $* y";
+by (simp_tac (simpset() addsimps [zmult_def]) 1);
+qed "zmult_intify2";
+Addsimps [zmult_intify1, zmult_intify2];
+
 
 (**** zminus: unary negation on int ****)
 
@@ -106,34 +164,64 @@
 (*Resolve th against the corresponding facts for zminus*)
 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
 
-Goalw [int_def,zminus_def] "z : int ==> $~z : int";
+Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
 by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
+qed "raw_zminus_type";
+
+Goalw [zminus_def] "$~z : int";
+by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
 qed "zminus_type";
+AddIffs [zminus_type];
 AddTCs [zminus_type];
 
-Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
+
+Goalw [int_def,raw_zminus_def]
+     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
 by (etac (zminus_ize UN_equiv_class_inject) 1);
 by Safe_tac;
-(*The setloop is only needed because assumptions are in the wrong order!*)
-by (asm_full_simp_tac (simpset() addsimps add_ac
-                       setloop dtac eq_intrelD) 1);
+by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
+qed "raw_zminus_inject";
+
+Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
+by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
+qed "zminus_inject_intify";
+
+AddSDs [zminus_inject_intify];
+
+Goal "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
+by Auto_tac;  
 qed "zminus_inject";
 
+Goalw [raw_zminus_def]
+    "[| x: nat;  y: nat |] \
+\    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
+by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
+qed "raw_zminus";
+
 Goalw [zminus_def]
-    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
+    "[| x: nat;  y: nat |] \
+\    ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
+by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
 qed "zminus";
 
-Goalw [int_def] "z : int ==> $~ ($~ z) = z";
-by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_zminus";
+Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
+by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
+qed "raw_zminus_zminus";
 
-Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
+Goal "$~ ($~ z) = intify(z)";
+by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
+	                          raw_zminus_zminus]) 1);
+qed "zminus_zminus_intify"; 
+
+Goalw [int_of_def] "$~ ($#0) = $#0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_0";
 
-Addsimps [zminus_zminus, zminus_0];
+Addsimps [zminus_zminus_intify, zminus_0];
+
+Goal "z : int ==> $~ ($~ z) = z";
+by (Asm_simp_tac 1);
+qed "zminus_zminus";
 
 
 (**** znegative: the test for negative integers ****)
@@ -150,28 +238,37 @@
 Addsimps [not_znegative_int_of];
 AddSEs   [not_znegative_int_of RS notE];
 
-Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
+Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
 by (blast_tac (claset() addIs [nat_0_le]) 1);
 qed "znegative_zminus_int_of";
 
 Addsimps [znegative_zminus_int_of];
 
-Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
+Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
 by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
-by (etac natE 1);
-by (dres_inst_tac [("x","0")] spec 2);
-by Auto_tac;
+by (dres_inst_tac [("x","0")] spec 1);
+by (auto_tac(claset(), 
+             simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
 qed "not_znegative_imp_zero";
 
 (**** zmagnitude: magnitide of an integer, as a natural number ****)
 
-Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
-by Auto_tac;
+Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
+by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
 qed "zmagnitude_int_of";
 
-Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
-by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
+Goal "natify(x)=n ==> $#x = $# n";
+by (dtac sym 1);
+by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
+qed "natify_int_of_eq";
+
+Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
+by (rtac the_equality 1);
+by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
+              simpset())
+             delIffs [int_of_eq]));
+by Auto_tac;  
 qed "zmagnitude_zminus_int_of";
 
 Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
@@ -242,46 +339,74 @@
 (*Resolve th against the corresponding facts for zadd*)
 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
 
-Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
+Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
 by (rtac (zadd_ize UN_equiv_class_type2) 1);
 by (simp_tac (simpset() addsimps [Let_def]) 3);
-by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
-qed "zadd_type";
-AddTCs [zadd_type];
+by (REPEAT (assume_tac 1));
+qed "raw_zadd_type";
 
-Goalw [zadd_def]
-  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
-\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
-\           intrel `` {<x1#+x2, y1#+y2>}";
+Goal "z $+ w : int";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
+qed "zadd_type";
+AddIffs [zadd_type];  AddTCs [zadd_type];
+
+Goalw [raw_zadd_def]
+  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
+\  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
+\      intrel `` {<x1#+x2, y1#+y2>}";
 by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
 by (simp_tac (simpset() addsimps [Let_def]) 1);
+qed "raw_zadd";
+
+Goalw [zadd_def]
+  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
+\  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
+\      intrel `` {<x1#+x2, y1#+y2>}";
+by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
 qed "zadd";
 
-Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zadd]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
+by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
+qed "raw_zadd_0";
+
+Goal "$#0 $+ z = intify(z)";
+by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
+qed "zadd_0_intify";
+Addsimps [zadd_0_intify];
+
+Goal "z: int ==> $#0 $+ z = z";
+by (Asm_simp_tac 1);
 qed "zadd_0";
 
-Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
+Goalw [int_def]
+     "[| z: int;  w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
+by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
+qed "raw_zminus_zadd_distrib";
+
+Goal "$~ (z $+ w) = $~ z $+ $~ w";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
 qed "zminus_zadd_distrib";
 
-Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
+Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
+by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
+qed "raw_zadd_commute";
+
+Goal "z $+ w = w $+ z";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
 qed "zadd_commute";
 
 Goalw [int_def]
     "[| z1: int;  z2: int;  z3: int |]   \
-\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-(*rewriting is much faster without intrel_iff, etc.*)
-by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
+\    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
+by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
+qed "raw_zadd_assoc";
+
+Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
 qed "zadd_assoc";
 
 (*For AC rewriting*)
-Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
+Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
 by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
 qed "zadd_left_commute";
@@ -289,31 +414,38 @@
 (*Integer addition is an AC operator*)
 val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
 
-Goalw [int_of_def]
-    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
+Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "int_of_add";
 
-Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
+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";
+
+Goal "z $+ ($~ z) = $#0";
+by (simp_tac (simpset() addsimps [zadd_def]) 1);
+by (stac (zminus_intify RS sym) 1);
+by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
 qed "zadd_zminus_inverse";
 
-Goal "z : int ==> ($~ z) $+ z = $#0";
-by (asm_simp_tac
-    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
+Goal "($~ z) $+ z = $#0";
+by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
 qed "zadd_zminus_inverse2";
 
+Goal "z $+ $#0 = intify(z)";
+by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
+qed "zadd_0_right_intify";
+Addsimps [zadd_0_right_intify];
+
 Goal "z:int ==> z $+ $#0 = z";
-by (rtac (zadd_commute RS trans) 1);
-by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
+by (Asm_simp_tac 1);
 qed "zadd_0_right";
 
-Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
+Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
 
 
 (*Need properties of $- ???  Or use $- just as an abbreviation?
-     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
+     [| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
 *)
 
 (**** zmult: multiplication on int ****)
@@ -339,58 +471,93 @@
 (*Resolve th against the corresponding facts for zmult*)
 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
 
-Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
+Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
 by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
                       split_type, add_type, mult_type, 
                       quotientI, SigmaI] 1));
+qed "raw_zmult_type";
+
+Goal "z $* w : int";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
 qed "zmult_type";
-AddTCs [zmult_type];
+AddIffs [zmult_type];  AddTCs [zmult_type];
+
+Goalw [raw_zmult_def]
+     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
+\     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
+\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
+by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
+qed "raw_zmult";
 
 Goalw [zmult_def]
-     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
-\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
-\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
+     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
+\     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
+\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
+by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
 qed "zmult";
 
-Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
+by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
+qed "raw_zmult_0";
+
+Goal "$#0 $* z = $#0";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
 qed "zmult_0";
+Addsimps [zmult_0];
 
-Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
+by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
+qed "raw_zmult_1";
+
+Goal "$#1 $* z = intify(z)";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
+qed "zmult_1_intify";
+Addsimps [zmult_1_intify];
+
+Goal "z : int ==> $#1 $* z = z";
+by (Asm_simp_tac 1);
 qed "zmult_1";
 
-Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
-qed "zmult_zminus";
-
-Addsimps [zmult_0, zmult_1, zmult_zminus];
+Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
+by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
+qed "raw_zmult_commute";
 
-Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
-qed "zmult_zminus_zminus";
-
-Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
+Goal "z $* w = w $* z";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
 qed "zmult_commute";
 
 Goalw [int_def]
-    "[| z1: int;  z2: int;  z3: int |]     \
-\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac 
-    (simpset() addsimps [zmult, add_mult_distrib_left, 
-                         add_mult_distrib] @ add_ac @ mult_ac) 1);
+     "[| z: int;  w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
+by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
+qed "raw_zmult_zminus";
+
+Goal "($~ z) $* w = $~ (z $* w)";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
+by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
+by Auto_tac;  
+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";
+
+Goalw [int_def]
+    "[| z1: int;  z2: int;  z3: int |]   \
+\    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
+by (auto_tac (claset(), 
+  simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
+qed "raw_zmult_assoc";
+
+Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
+                                  raw_zmult_assoc]) 1);
 qed "zmult_assoc";
 
 (*For AC rewriting*)
-Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
+Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
 by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
 by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
 qed "zmult_left_commute";
@@ -399,17 +566,25 @@
 val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
 
 Goalw [int_def]
-    "[| z1: int;  z2: int;  w: int |] ==> \
-\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
-by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
+    "[| z1: int;  z2: int;  w: int |]  \
+\    ==> raw_zmult(raw_zadd(z1,z2), w) = \
+\        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
+by (auto_tac (claset(), 
+              simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
+                                 add_ac @ mult_ac));  
+qed "raw_zadd_zmult_distrib";
+
+Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
+by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
+     	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib";
 
+Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
+by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
+                                  zadd_zmult_distrib]) 1);
+qed "zadd_zmult_distrib_left";
+
 val int_typechecks =
     [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
 
-Addsimps int_typechecks;
 
-
-

--- a/src/ZF/Integ/Int.thy	Wed Aug 02 16:06:54 2000 +0200
+++ b/src/ZF/Integ/Int.thy	Wed Aug 02 16:07:32 2000 +0200
@@ -7,54 +7,64 @@
 *)
 
 Int = EquivClass + Arith +
-consts
-    intrel,int::      i
-    int_of      ::      i=>i            ("$# _" [80] 80)
-    zminus      ::      i=>i            ("$~ _" [80] 80)
-    znegative   ::      i=>o
-    zmagnitude  ::      i=>i
-    "$*"        ::      [i,i]=>i      (infixl 70)
-    "$'/"       ::      [i,i]=>i      (infixl 70) 
-    "$'/'/"     ::      [i,i]=>i      (infixl 70)
-    "$+"        ::      [i,i]=>i      (infixl 65)
-    "$-"        ::      [i,i]=>i      (infixl 65)
-    "$<"        ::      [i,i]=>o        (infixl 50)
+
+constdefs
+  intrel :: i
+    "intrel == {p:(nat*nat)*(nat*nat).                 
+                EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
 
-defs
+  int :: i
+    "int == (nat*nat)//intrel"  
+
+  int_of :: i=>i (*coercion from nat to int*)    ("$# _" [80] 80)
+    "$# m == intrel `` {<natify(m), 0>}"
+
+  intify :: i=>i (*coercion from ANYTHING to int*) 
+    "intify(m) == if m : int then m else $#0"
 
-    intrel_def
-     "intrel == {p:(nat*nat)*(nat*nat).                 
-        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+  raw_zminus :: i=>i
+    "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
+
+  zminus :: i=>i                                 ("$~ _" [80] 80)
+    "$~ z == raw_zminus (intify(z))"
 
-    int_def   "int == (nat*nat)//intrel"
-    
-    int_of_def  "$# m == intrel `` {<m,0>}"
-    
-    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
-    
-    znegative_def
-        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
-    
-    zmagnitude_def
-        "zmagnitude(Z) ==
-	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
-	                   (znegative(Z) & $~ Z = $# m))"
-    
-    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
+  znegative   ::      i=>o
+    "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
+  
+  zmagnitude  ::      i=>i
+    "zmagnitude(z) ==
+     THE m. m : nat & ((~ znegative(z) & z = $# m) |
+		       (znegative(z) & $~ z = $# m))"
+
+  raw_zmult   ::      [i,i]=>i
+    (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
       Perhaps a "curried" or even polymorphic congruent predicate would be
       better.*)
-    zadd_def
-     "Z1 $+ Z2 == 
-       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
+     "raw_zmult(z1,z2) == 
+       UN p1:z1. UN p2:z2.  split(%x1 y1. split(%x2 y2.        
+                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+
+  zmult       ::      [i,i]=>i      (infixl "$*" 70)
+     "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
+
+  raw_zadd    ::      [i,i]=>i
+     "raw_zadd (z1, z2) == 
+       UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2                 
                            in intrel``{<x1#+x2, y1#+y2>}"
-    
-    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
-    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
+
+  zadd        ::      [i,i]=>i      (infixl "$+" 65)
+     "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
+
+  zdiff        ::      [i,i]=>i      (infixl "$-" 65)
+     "z1 $- z2 == z1 $+ zminus(z2)"
+
+  zless        ::      [i,i]=>o      (infixl "$<" 50)
+     "z1 $< z2 == znegative(z1 $- z2)"
+  
+(*div and mod await definitions!*)
+consts
+  "$'/"       ::      [i,i]=>i      (infixl 70) 
+
+  "$'/'/"     ::      [i,i]=>i      (infixl 70)
     
-    (*This illustrates the primitive form of definitions (no patterns)*)
-    zmult_def
-     "Z1 $* Z2 == 
-       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
-                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
-    
- end
+end