src/ZF/Integ/Int.ML
changeset 9496 07e33cac5d9c
parent 9491 1a36151ee2fc
child 9548 15bee2731e43
     1.1 --- a/src/ZF/Integ/Int.ML	Wed Aug 02 16:06:54 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.ML	Wed Aug 02 16:07:32 2000 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4  qed "intrel_iff";
     1.5  
     1.6  Goalw [intrel_def]
     1.7 -    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
     1.8 -\             <<x1,y1>,<x2,y2>>: intrel";
     1.9 +    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]  \
    1.10 +\    ==> <<x1,y1>,<x2,y2>>: intrel";
    1.11  by (fast_tac (claset() addIs prems) 1);
    1.12  qed "intrelI";
    1.13  
    1.14 @@ -66,6 +66,11 @@
    1.15  qed "equiv_intrel";
    1.16  
    1.17  
    1.18 +Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
    1.19 +by (blast_tac (claset() addIs [quotientI]) 1);
    1.20 +qed "image_intrel_int";
    1.21 +
    1.22 +
    1.23  Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    1.24  	  add_0_right, add_succ_right];
    1.25  Addcongs [conj_cong];
    1.26 @@ -74,25 +79,78 @@
    1.27  
    1.28  (** int_of: the injection from nat to int **)
    1.29  
    1.30 -Goalw [int_def,quotient_def,int_of_def]
    1.31 -    "m : nat ==> $#m : int";
    1.32 +Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
    1.33  by Auto_tac;
    1.34  qed "int_of_type";
    1.35  
    1.36 -Addsimps [int_of_type];
    1.37 -AddTCs   [int_of_type];
    1.38 +AddIffs [int_of_type];
    1.39 +AddTCs  [int_of_type];
    1.40 +
    1.41  
    1.42 -Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
    1.43 -by (dtac (sym RS eq_intrelD) 1);
    1.44 +Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
    1.45 +by Auto_tac;  
    1.46 +qed "int_of_eq"; 
    1.47 +AddIffs [int_of_eq];
    1.48 +
    1.49 +Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
    1.50 +by (dtac (int_of_eq RS iffD1) 1);
    1.51  by Auto_tac;
    1.52  qed "int_of_inject";
    1.53  
    1.54 -AddSDs [int_of_inject];
    1.55 +
    1.56 +(** intify: coercion from anything to int **)
    1.57 +
    1.58 +Goal "intify(x) : int";
    1.59 +by (simp_tac (simpset() addsimps [intify_def]) 1);
    1.60 +qed "intify_in_int";
    1.61 +AddIffs [intify_in_int];
    1.62 +AddTCs [intify_in_int];
    1.63 +
    1.64 +Goal "n : int ==> intify(n) = n";
    1.65 +by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
    1.66 +qed "intify_ident";
    1.67 +Addsimps [intify_ident];
    1.68 +
    1.69 +
    1.70 +(*** Collapsing rules: to remove intify from arithmetic expressions ***)
    1.71 +
    1.72 +Goal "intify(intify(x)) = intify(x)";
    1.73 +by (Simp_tac 1);
    1.74 +qed "intify_idem";
    1.75 +Addsimps [intify_idem];
    1.76 +
    1.77 +Goal "$# (natify(m)) = $# m";
    1.78 +by (simp_tac (simpset() addsimps [int_of_def]) 1);
    1.79 +qed "int_of_natify";
    1.80  
    1.81 -Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
    1.82 -by (Blast_tac 1); 
    1.83 -qed "int_of_eq"; 
    1.84 -Addsimps [int_of_eq]; 
    1.85 +Goal "$~ (intify(m)) = $~ m";
    1.86 +by (simp_tac (simpset() addsimps [zminus_def]) 1);
    1.87 +qed "zminus_intify";
    1.88 +
    1.89 +Addsimps [int_of_natify, zminus_intify];
    1.90 +
    1.91 +(** Addition **)
    1.92 +
    1.93 +Goal "intify(x) $+ y = x $+ y";
    1.94 +by (simp_tac (simpset() addsimps [zadd_def]) 1);
    1.95 +qed "zadd_intify1";
    1.96 +
    1.97 +Goal "x $+ intify(y) = x $+ y";
    1.98 +by (simp_tac (simpset() addsimps [zadd_def]) 1);
    1.99 +qed "zadd_intify2";
   1.100 +Addsimps [zadd_intify1, zadd_intify2];
   1.101 +
   1.102 +(** Multiplication **)
   1.103 +
   1.104 +Goal "intify(x) $* y = x $* y";
   1.105 +by (simp_tac (simpset() addsimps [zmult_def]) 1);
   1.106 +qed "zmult_intify1";
   1.107 +
   1.108 +Goal "x $* intify(y) = x $* y";
   1.109 +by (simp_tac (simpset() addsimps [zmult_def]) 1);
   1.110 +qed "zmult_intify2";
   1.111 +Addsimps [zmult_intify1, zmult_intify2];
   1.112 +
   1.113  
   1.114  (**** zminus: unary negation on int ****)
   1.115  
   1.116 @@ -106,34 +164,64 @@
   1.117  (*Resolve th against the corresponding facts for zminus*)
   1.118  val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   1.119  
   1.120 -Goalw [int_def,zminus_def] "z : int ==> $~z : int";
   1.121 +Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
   1.122  by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
   1.123 +qed "raw_zminus_type";
   1.124 +
   1.125 +Goalw [zminus_def] "$~z : int";
   1.126 +by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
   1.127  qed "zminus_type";
   1.128 +AddIffs [zminus_type];
   1.129  AddTCs [zminus_type];
   1.130  
   1.131 -Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   1.132 +
   1.133 +Goalw [int_def,raw_zminus_def]
   1.134 +     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
   1.135  by (etac (zminus_ize UN_equiv_class_inject) 1);
   1.136  by Safe_tac;
   1.137 -(*The setloop is only needed because assumptions are in the wrong order!*)
   1.138 -by (asm_full_simp_tac (simpset() addsimps add_ac
   1.139 -                       setloop dtac eq_intrelD) 1);
   1.140 +by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
   1.141 +qed "raw_zminus_inject";
   1.142 +
   1.143 +Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
   1.144 +by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
   1.145 +qed "zminus_inject_intify";
   1.146 +
   1.147 +AddSDs [zminus_inject_intify];
   1.148 +
   1.149 +Goal "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   1.150 +by Auto_tac;  
   1.151  qed "zminus_inject";
   1.152  
   1.153 +Goalw [raw_zminus_def]
   1.154 +    "[| x: nat;  y: nat |] \
   1.155 +\    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
   1.156 +by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   1.157 +qed "raw_zminus";
   1.158 +
   1.159  Goalw [zminus_def]
   1.160 -    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   1.161 -by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   1.162 +    "[| x: nat;  y: nat |] \
   1.163 +\    ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   1.164 +by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
   1.165  qed "zminus";
   1.166  
   1.167 -Goalw [int_def] "z : int ==> $~ ($~ z) = z";
   1.168 -by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   1.169 -by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   1.170 -qed "zminus_zminus";
   1.171 +Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
   1.172 +by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
   1.173 +qed "raw_zminus_zminus";
   1.174  
   1.175 -Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
   1.176 +Goal "$~ ($~ z) = intify(z)";
   1.177 +by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
   1.178 +	                          raw_zminus_zminus]) 1);
   1.179 +qed "zminus_zminus_intify"; 
   1.180 +
   1.181 +Goalw [int_of_def] "$~ ($#0) = $#0";
   1.182  by (simp_tac (simpset() addsimps [zminus]) 1);
   1.183  qed "zminus_0";
   1.184  
   1.185 -Addsimps [zminus_zminus, zminus_0];
   1.186 +Addsimps [zminus_zminus_intify, zminus_0];
   1.187 +
   1.188 +Goal "z : int ==> $~ ($~ z) = z";
   1.189 +by (Asm_simp_tac 1);
   1.190 +qed "zminus_zminus";
   1.191  
   1.192  
   1.193  (**** znegative: the test for negative integers ****)
   1.194 @@ -150,28 +238,37 @@
   1.195  Addsimps [not_znegative_int_of];
   1.196  AddSEs   [not_znegative_int_of RS notE];
   1.197  
   1.198 -Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
   1.199 +Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
   1.200  by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   1.201  by (blast_tac (claset() addIs [nat_0_le]) 1);
   1.202  qed "znegative_zminus_int_of";
   1.203  
   1.204  Addsimps [znegative_zminus_int_of];
   1.205  
   1.206 -Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
   1.207 +Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
   1.208  by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   1.209 -by (etac natE 1);
   1.210 -by (dres_inst_tac [("x","0")] spec 2);
   1.211 -by Auto_tac;
   1.212 +by (dres_inst_tac [("x","0")] spec 1);
   1.213 +by (auto_tac(claset(), 
   1.214 +             simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
   1.215  qed "not_znegative_imp_zero";
   1.216  
   1.217  (**** zmagnitude: magnitide of an integer, as a natural number ****)
   1.218  
   1.219 -Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
   1.220 -by Auto_tac;
   1.221 +Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
   1.222 +by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
   1.223  qed "zmagnitude_int_of";
   1.224  
   1.225 -Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
   1.226 -by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
   1.227 +Goal "natify(x)=n ==> $#x = $# n";
   1.228 +by (dtac sym 1);
   1.229 +by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
   1.230 +qed "natify_int_of_eq";
   1.231 +
   1.232 +Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
   1.233 +by (rtac the_equality 1);
   1.234 +by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
   1.235 +              simpset())
   1.236 +             delIffs [int_of_eq]));
   1.237 +by Auto_tac;  
   1.238  qed "zmagnitude_zminus_int_of";
   1.239  
   1.240  Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   1.241 @@ -242,46 +339,74 @@
   1.242  (*Resolve th against the corresponding facts for zadd*)
   1.243  val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   1.244  
   1.245 -Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
   1.246 +Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
   1.247  by (rtac (zadd_ize UN_equiv_class_type2) 1);
   1.248  by (simp_tac (simpset() addsimps [Let_def]) 3);
   1.249 -by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
   1.250 -qed "zadd_type";
   1.251 -AddTCs [zadd_type];
   1.252 +by (REPEAT (assume_tac 1));
   1.253 +qed "raw_zadd_type";
   1.254  
   1.255 -Goalw [zadd_def]
   1.256 -  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
   1.257 -\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
   1.258 -\           intrel `` {<x1#+x2, y1#+y2>}";
   1.259 +Goal "z $+ w : int";
   1.260 +by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
   1.261 +qed "zadd_type";
   1.262 +AddIffs [zadd_type];  AddTCs [zadd_type];
   1.263 +
   1.264 +Goalw [raw_zadd_def]
   1.265 +  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
   1.266 +\  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
   1.267 +\      intrel `` {<x1#+x2, y1#+y2>}";
   1.268  by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   1.269  by (simp_tac (simpset() addsimps [Let_def]) 1);
   1.270 +qed "raw_zadd";
   1.271 +
   1.272 +Goalw [zadd_def]
   1.273 +  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
   1.274 +\  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
   1.275 +\      intrel `` {<x1#+x2, y1#+y2>}";
   1.276 +by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
   1.277  qed "zadd";
   1.278  
   1.279 -Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
   1.280 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.281 -by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   1.282 +Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
   1.283 +by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
   1.284 +qed "raw_zadd_0";
   1.285 +
   1.286 +Goal "$#0 $+ z = intify(z)";
   1.287 +by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
   1.288 +qed "zadd_0_intify";
   1.289 +Addsimps [zadd_0_intify];
   1.290 +
   1.291 +Goal "z: int ==> $#0 $+ z = z";
   1.292 +by (Asm_simp_tac 1);
   1.293  qed "zadd_0";
   1.294  
   1.295 -Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
   1.296 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.297 -by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
   1.298 +Goalw [int_def]
   1.299 +     "[| z: int;  w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
   1.300 +by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
   1.301 +qed "raw_zminus_zadd_distrib";
   1.302 +
   1.303 +Goal "$~ (z $+ w) = $~ z $+ $~ w";
   1.304 +by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
   1.305  qed "zminus_zadd_distrib";
   1.306  
   1.307 -Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
   1.308 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.309 -by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
   1.310 +Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
   1.311 +by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
   1.312 +qed "raw_zadd_commute";
   1.313 +
   1.314 +Goal "z $+ w = w $+ z";
   1.315 +by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
   1.316  qed "zadd_commute";
   1.317  
   1.318  Goalw [int_def]
   1.319      "[| z1: int;  z2: int;  z3: int |]   \
   1.320 -\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   1.321 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.322 -(*rewriting is much faster without intrel_iff, etc.*)
   1.323 -by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
   1.324 +\    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
   1.325 +by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
   1.326 +qed "raw_zadd_assoc";
   1.327 +
   1.328 +Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   1.329 +by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
   1.330  qed "zadd_assoc";
   1.331  
   1.332  (*For AC rewriting*)
   1.333 -Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
   1.334 +Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
   1.335  by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   1.336  by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
   1.337  qed "zadd_left_commute";
   1.338 @@ -289,31 +414,38 @@
   1.339  (*Integer addition is an AC operator*)
   1.340  val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   1.341  
   1.342 -Goalw [int_of_def]
   1.343 -    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
   1.344 +Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
   1.345  by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   1.346  qed "int_of_add";
   1.347  
   1.348 -Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
   1.349 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.350 -by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
   1.351 +Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $~ z) = $#0";
   1.352 +by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
   1.353 +qed "raw_zadd_zminus_inverse";
   1.354 +
   1.355 +Goal "z $+ ($~ z) = $#0";
   1.356 +by (simp_tac (simpset() addsimps [zadd_def]) 1);
   1.357 +by (stac (zminus_intify RS sym) 1);
   1.358 +by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
   1.359  qed "zadd_zminus_inverse";
   1.360  
   1.361 -Goal "z : int ==> ($~ z) $+ z = $#0";
   1.362 -by (asm_simp_tac
   1.363 -    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
   1.364 +Goal "($~ z) $+ z = $#0";
   1.365 +by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
   1.366  qed "zadd_zminus_inverse2";
   1.367  
   1.368 +Goal "z $+ $#0 = intify(z)";
   1.369 +by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
   1.370 +qed "zadd_0_right_intify";
   1.371 +Addsimps [zadd_0_right_intify];
   1.372 +
   1.373  Goal "z:int ==> z $+ $#0 = z";
   1.374 -by (rtac (zadd_commute RS trans) 1);
   1.375 -by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
   1.376 +by (Asm_simp_tac 1);
   1.377  qed "zadd_0_right";
   1.378  
   1.379 -Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
   1.380 +Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
   1.381  
   1.382  
   1.383  (*Need properties of $- ???  Or use $- just as an abbreviation?
   1.384 -     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
   1.385 +     [| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
   1.386  *)
   1.387  
   1.388  (**** zmult: multiplication on int ****)
   1.389 @@ -339,58 +471,93 @@
   1.390  (*Resolve th against the corresponding facts for zmult*)
   1.391  val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   1.392  
   1.393 -Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
   1.394 +Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
   1.395  by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   1.396                        split_type, add_type, mult_type, 
   1.397                        quotientI, SigmaI] 1));
   1.398 +qed "raw_zmult_type";
   1.399 +
   1.400 +Goal "z $* w : int";
   1.401 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
   1.402  qed "zmult_type";
   1.403 -AddTCs [zmult_type];
   1.404 +AddIffs [zmult_type];  AddTCs [zmult_type];
   1.405 +
   1.406 +Goalw [raw_zmult_def]
   1.407 +     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   1.408 +\     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
   1.409 +\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   1.410 +by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   1.411 +qed "raw_zmult";
   1.412  
   1.413  Goalw [zmult_def]
   1.414 -     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
   1.415 -\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   1.416 -\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   1.417 -by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   1.418 +     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   1.419 +\     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   1.420 +\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   1.421 +by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
   1.422  qed "zmult";
   1.423  
   1.424 -Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
   1.425 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.426 -by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   1.427 +Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
   1.428 +by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   1.429 +qed "raw_zmult_0";
   1.430 +
   1.431 +Goal "$#0 $* z = $#0";
   1.432 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
   1.433  qed "zmult_0";
   1.434 +Addsimps [zmult_0];
   1.435  
   1.436 -Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
   1.437 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.438 -by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
   1.439 +Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
   1.440 +by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   1.441 +qed "raw_zmult_1";
   1.442 +
   1.443 +Goal "$#1 $* z = intify(z)";
   1.444 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
   1.445 +qed "zmult_1_intify";
   1.446 +Addsimps [zmult_1_intify];
   1.447 +
   1.448 +Goal "z : int ==> $#1 $* z = z";
   1.449 +by (Asm_simp_tac 1);
   1.450  qed "zmult_1";
   1.451  
   1.452 -Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
   1.453 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.454 -by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   1.455 -qed "zmult_zminus";
   1.456 -
   1.457 -Addsimps [zmult_0, zmult_1, zmult_zminus];
   1.458 +Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
   1.459 +by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
   1.460 +qed "raw_zmult_commute";
   1.461  
   1.462 -Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
   1.463 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.464 -by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   1.465 -qed "zmult_zminus_zminus";
   1.466 -
   1.467 -Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
   1.468 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.469 -by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
   1.470 +Goal "z $* w = w $* z";
   1.471 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
   1.472  qed "zmult_commute";
   1.473  
   1.474  Goalw [int_def]
   1.475 -    "[| z1: int;  z2: int;  z3: int |]     \
   1.476 -\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   1.477 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.478 -by (asm_simp_tac 
   1.479 -    (simpset() addsimps [zmult, add_mult_distrib_left, 
   1.480 -                         add_mult_distrib] @ add_ac @ mult_ac) 1);
   1.481 +     "[| z: int;  w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
   1.482 +by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
   1.483 +qed "raw_zmult_zminus";
   1.484 +
   1.485 +Goal "($~ z) $* w = $~ (z $* w)";
   1.486 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
   1.487 +by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
   1.488 +by Auto_tac;  
   1.489 +qed "zmult_zminus";
   1.490 +Addsimps [zmult_zminus];
   1.491 +
   1.492 +Goal "($~ z) $* ($~ w) = (z $* w)";
   1.493 +by (stac zmult_zminus 1);
   1.494 +by (stac zmult_commute 1 THEN stac zmult_zminus 1);
   1.495 +by (simp_tac (simpset() addsimps [zmult_commute])1);
   1.496 +qed "zmult_zminus_zminus";
   1.497 +
   1.498 +Goalw [int_def]
   1.499 +    "[| z1: int;  z2: int;  z3: int |]   \
   1.500 +\    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
   1.501 +by (auto_tac (claset(), 
   1.502 +  simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
   1.503 +qed "raw_zmult_assoc";
   1.504 +
   1.505 +Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   1.506 +by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
   1.507 +                                  raw_zmult_assoc]) 1);
   1.508  qed "zmult_assoc";
   1.509  
   1.510  (*For AC rewriting*)
   1.511 -Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
   1.512 +Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
   1.513  by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   1.514  by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
   1.515  qed "zmult_left_commute";
   1.516 @@ -399,17 +566,25 @@
   1.517  val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   1.518  
   1.519  Goalw [int_def]
   1.520 -    "[| z1: int;  z2: int;  w: int |] ==> \
   1.521 -\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   1.522 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   1.523 -by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
   1.524 -by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
   1.525 +    "[| z1: int;  z2: int;  w: int |]  \
   1.526 +\    ==> raw_zmult(raw_zadd(z1,z2), w) = \
   1.527 +\        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
   1.528 +by (auto_tac (claset(), 
   1.529 +              simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
   1.530 +                                 add_ac @ mult_ac));  
   1.531 +qed "raw_zadd_zmult_distrib";
   1.532 +
   1.533 +Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   1.534 +by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
   1.535 +     	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
   1.536  qed "zadd_zmult_distrib";
   1.537  
   1.538 +Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
   1.539 +by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
   1.540 +                                  zadd_zmult_distrib]) 1);
   1.541 +qed "zadd_zmult_distrib_left";
   1.542 +
   1.543  val int_typechecks =
   1.544      [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   1.545  
   1.546 -Addsimps int_typechecks;
   1.547  
   1.548 -
   1.549 -