src/ZF/ex/Integ.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 7 268f93ab3bc4
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	ZF/ex/integ.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 For integ.thy.  The integers as equivalence classes over nat*nat.
     7 
     8 Could also prove...
     9 "znegative(z) ==> $# zmagnitude(z) = $~ z"
    10 "~ znegative(z) ==> $# zmagnitude(z) = z"
    11 $< is a linear ordering
    12 $+ and $* are monotonic wrt $<
    13 *)
    14 
    15 open Integ;
    16 
    17 val [add_cong] = mk_congs Arith.thy ["op #+"];
    18 
    19 (*** Proving that intrel is an equivalence relation ***)
    20 
    21 val prems = goal Arith.thy 
    22     "[| m #+ n = m' #+ n';  m: nat; m': nat |]   \
    23 \    ==> m #+ (n #+ k) = m' #+ (n' #+ k)";
    24 by (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym] @ prems)) 1);
    25 val add_assoc_cong = result();
    26 
    27 val prems = goal Arith.thy 
    28     "[| m: nat; n: nat |]   \
    29 \    ==> m #+ (n #+ k) = n #+ (m #+ k)";
    30 by (REPEAT (resolve_tac ([add_commute RS add_assoc_cong] @ prems) 1));
    31 val add_assoc_swap = result();
    32 
    33 val add_kill = (refl RS add_cong);
    34 val add_assoc_swap_kill = add_kill RSN (3, add_assoc_swap RS trans);
    35 
    36 (*By luck, requires no typing premises for y1, y2,y3*)
    37 val eqa::eqb::prems = goal Arith.thy 
    38     "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    39 \       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    40 by (res_inst_tac [("k","x2")] add_left_cancel 1);
    41 by (resolve_tac prems 1);
    42 by (rtac (add_assoc_swap RS trans) 1 THEN typechk_tac prems);
    43 by (rtac (eqb RS ssubst) 1);
    44 by (rtac (add_assoc_swap RS trans) 1 THEN typechk_tac prems);
    45 by (rtac (eqa RS ssubst) 1);
    46 by (rtac (add_assoc_swap) 1 THEN typechk_tac prems);
    47 val integ_trans_lemma = result();
    48 
    49 (** Natural deduction for intrel **)
    50 
    51 val prems = goalw Integ.thy [intrel_def]
    52     "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
    53 \    <<x1,y1>,<x2,y2>>: intrel";
    54 by (fast_tac (ZF_cs addIs prems) 1);
    55 val intrelI = result();
    56 
    57 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    58 goalw Integ.thy [intrel_def]
    59   "p: intrel --> (EX x1 y1 x2 y2. \
    60 \                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    61 \                  x1: nat & y1: nat & x2: nat & y2: nat)";
    62 by (fast_tac ZF_cs 1);
    63 val intrelE_lemma = result();
    64 
    65 val [major,minor] = goal Integ.thy
    66   "[| p: intrel;  \
    67 \     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    68 \                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    69 \  ==> Q";
    70 by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    71 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    72 val intrelE = result();
    73 
    74 val intrel_cs = ZF_cs addSIs [intrelI] addSEs [intrelE];
    75 
    76 goal Integ.thy
    77     "<<x1,y1>,<x2,y2>>: intrel <-> \
    78 \    x1#+y2 = x2#+y1 & x1: nat & y1: nat & x2: nat & y2: nat";
    79 by (fast_tac intrel_cs 1);
    80 val intrel_iff = result();
    81 
    82 val prems = goalw Integ.thy [equiv_def] "equiv(nat*nat, intrel)";
    83 by (safe_tac intrel_cs);
    84 by (rewtac refl_def);
    85 by (fast_tac intrel_cs 1);
    86 by (rewtac sym_def);
    87 by (fast_tac (intrel_cs addSEs [sym]) 1);
    88 by (rewtac trans_def);
    89 by (fast_tac (intrel_cs addSEs [integ_trans_lemma]) 1);
    90 val equiv_intrel = result();
    91 
    92 
    93 val integ_congs = mk_congs Integ.thy
    94   ["znat", "zminus", "znegative", "zmagnitude", "op $+", "op $-", "op $*"];
    95 
    96 val intrel_ss0 = arith_ss addcongs integ_congs;
    97 
    98 val intrel_ss = 
    99     intrel_ss0 addrews [equiv_intrel RS eq_equiv_class_iff, intrel_iff];
   100 
   101 (*More than twice as fast as simplifying with intrel_ss*)
   102 fun INTEG_SIMP_TAC ths = 
   103   let val ss = intrel_ss0 addrews ths 
   104   in fn i =>
   105        EVERY [ASM_SIMP_TAC ss i,
   106 	      rtac (intrelI RS (equiv_intrel RS equiv_class_eq)) i,
   107 	      typechk_tac (ZF_typechecks@nat_typechecks@arith_typechecks),
   108 	      ASM_SIMP_TAC ss i]
   109   end;
   110 
   111 
   112 (** znat: the injection from nat to integ **)
   113 
   114 val prems = goalw Integ.thy [integ_def,quotient_def,znat_def]
   115     "m : nat ==> $#m : integ";
   116 by (fast_tac (ZF_cs addSIs (nat_0I::prems)) 1);
   117 val znat_type = result();
   118 
   119 val [major,nnat] = goalw Integ.thy [znat_def]
   120     "[| $#m = $#n;  n: nat |] ==> m=n";
   121 by (rtac (make_elim (major RS eq_equiv_class)) 1);
   122 by (rtac equiv_intrel 1);
   123 by (typechk_tac [nat_0I,nnat,SigmaI]);
   124 by (safe_tac (intrel_cs addSEs [box_equals,add_0_right]));
   125 val znat_inject = result();
   126 
   127 
   128 (**** zminus: unary negation on integ ****)
   129 
   130 goalw Integ.thy [congruent_def]
   131     "congruent(intrel, split(%x y. intrel``{<y,x>}))";
   132 by (safe_tac intrel_cs);
   133 by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
   134 by (etac (box_equals RS sym) 1);
   135 by (REPEAT (ares_tac [add_commute] 1));
   136 val zminus_congruent = result();
   137 
   138 (*Resolve th against the corresponding facts for zminus*)
   139 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   140 
   141 val [prem] = goalw Integ.thy [integ_def,zminus_def]
   142     "z : integ ==> $~z : integ";
   143 by (typechk_tac [split_type, SigmaI, prem, zminus_ize UN_equiv_class_type,
   144 		 quotientI]);
   145 val zminus_type = result();
   146 
   147 val major::prems = goalw Integ.thy [integ_def,zminus_def]
   148     "[| $~z = $~w;  z: integ;  w: integ |] ==> z=w";
   149 by (rtac (major RS zminus_ize UN_equiv_class_inject) 1);
   150 by (REPEAT (ares_tac prems 1));
   151 by (REPEAT (etac SigmaE 1));
   152 by (etac rev_mp 1);
   153 by (ASM_SIMP_TAC ZF_ss 1);
   154 by (fast_tac (intrel_cs addSIs [SigmaI, equiv_intrel]
   155 			addSEs [box_equals RS sym, add_commute,
   156 			        make_elim eq_equiv_class]) 1);
   157 val zminus_inject = result();
   158 
   159 val prems = goalw Integ.thy [zminus_def]
   160     "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   161 by (ASM_SIMP_TAC 
   162     (ZF_ss addrews (prems@[zminus_ize UN_equiv_class, SigmaI])) 1);
   163 val zminus = result();
   164 
   165 goalw Integ.thy [integ_def] "!!z. z : integ ==> $~ ($~ z) = z";
   166 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   167 by (ASM_SIMP_TAC (ZF_ss addrews [zminus] addcongs integ_congs) 1);
   168 val zminus_zminus = result();
   169 
   170 goalw Integ.thy [integ_def, znat_def] "$~ ($#0) = $#0";
   171 by (SIMP_TAC (arith_ss addrews [zminus]) 1);
   172 val zminus_0 = result();
   173 
   174 
   175 (**** znegative: the test for negative integers ****)
   176 
   177 goalw Integ.thy [znegative_def, znat_def]
   178     "~ znegative($# n)";
   179 by (safe_tac intrel_cs);
   180 by (rtac (add_not_less_self RS notE) 1);
   181 by (etac ssubst 3);
   182 by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 3);
   183 by (REPEAT (assume_tac 1));
   184 val not_znegative_znat = result();
   185 
   186 val [nnat] = goalw Integ.thy [znegative_def, znat_def]
   187     "n: nat ==> znegative($~ $# succ(n))";
   188 by (SIMP_TAC (intrel_ss addrews [zminus,nnat]) 1);
   189 by (REPEAT 
   190     (resolve_tac [refl, exI, conjI, naturals_are_ordinals RS Ord_0_mem_succ,
   191 		  refl RS intrelI RS imageI, consI1, nnat, nat_0I,
   192 		  nat_succI] 1));
   193 val znegative_zminus_znat = result();
   194 
   195 
   196 (**** zmagnitude: magnitide of an integer, as a natural number ****)
   197 
   198 goalw Integ.thy [congruent_def]
   199     "congruent(intrel, split(%x y. (y#-x) #+ (x#-y)))";
   200 by (safe_tac intrel_cs);
   201 by (ALLGOALS (ASM_SIMP_TAC intrel_ss));
   202 by (etac rev_mp 1);
   203 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
   204 by (REPEAT (assume_tac 1));
   205 by (ASM_SIMP_TAC (arith_ss addrews [add_succ_right,succ_inject_iff]) 3);
   206 by (ASM_SIMP_TAC
   207     (arith_ss addrews [diff_add_inverse,diff_add_0,add_0_right]) 2);
   208 by (ASM_SIMP_TAC (arith_ss addrews [add_0_right]) 1);
   209 by (rtac impI 1);
   210 by (etac subst 1);
   211 by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
   212 by (REPEAT (assume_tac 1));
   213 by (ASM_SIMP_TAC (arith_ss addrews [diff_add_inverse,diff_add_0]) 1);
   214 val zmagnitude_congruent = result();
   215 
   216 (*Resolve th against the corresponding facts for zmagnitude*)
   217 val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
   218 
   219 val [prem] = goalw Integ.thy [integ_def,zmagnitude_def]
   220     "z : integ ==> zmagnitude(z) : nat";
   221 by (typechk_tac [split_type, prem, zmagnitude_ize UN_equiv_class_type,
   222 		 add_type, diff_type]);
   223 val zmagnitude_type = result();
   224 
   225 val prems = goalw Integ.thy [zmagnitude_def]
   226     "[| x: nat;  y: nat |] ==> \
   227 \    zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)";
   228 by (ASM_SIMP_TAC 
   229     (ZF_ss addrews (prems@[zmagnitude_ize UN_equiv_class, SigmaI])) 1);
   230 val zmagnitude = result();
   231 
   232 val [nnat] = goalw Integ.thy [znat_def]
   233     "n: nat ==> zmagnitude($# n) = n";
   234 by (SIMP_TAC (intrel_ss addrews [zmagnitude,nnat]) 1);
   235 val zmagnitude_znat = result();
   236 
   237 val [nnat] = goalw Integ.thy [znat_def]
   238     "n: nat ==> zmagnitude($~ $# n) = n";
   239 by (SIMP_TAC (intrel_ss addrews [zmagnitude,zminus,nnat,add_0_right]) 1);
   240 val zmagnitude_zminus_znat = result();
   241 
   242 
   243 (**** zadd: addition on integ ****)
   244 
   245 (** Congruence property for addition **)
   246 
   247 goalw Integ.thy [congruent2_def]
   248     "congruent2(intrel, %p1 p2.                  \
   249 \         split(%x1 y1. split(%x2 y2. intrel `` {<x1#+x2, y1#+y2>}, p2), p1))";
   250 (*Proof via congruent2_commuteI seems longer*)
   251 by (safe_tac intrel_cs);
   252 by (INTEG_SIMP_TAC [add_assoc] 1);
   253 (*The rest should be trivial, but rearranging terms is hard*)
   254 by (res_inst_tac [("m1","x1a")] (add_assoc_swap RS ssubst) 1);
   255 by (res_inst_tac [("m1","x2a")] (add_assoc_swap RS ssubst) 3);
   256 by (typechk_tac [add_type]);
   257 by (ASM_SIMP_TAC (arith_ss addrews [add_assoc RS sym]) 1);
   258 val zadd_congruent2 = result();
   259 
   260 (*Resolve th against the corresponding facts for zadd*)
   261 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   262 
   263 val prems = goalw Integ.thy [integ_def,zadd_def]
   264     "[| z: integ;  w: integ |] ==> z $+ w : integ";
   265 by (REPEAT (ares_tac (prems@[zadd_ize UN_equiv_class_type2,
   266 			     split_type, add_type, quotientI, SigmaI]) 1));
   267 val zadd_type = result();
   268 
   269 val prems = goalw Integ.thy [zadd_def]
   270   "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==> \
   271 \ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = intrel `` {<x1#+x2, y1#+y2>}";
   272 by (ASM_SIMP_TAC (ZF_ss addrews 
   273 		  (prems @ [zadd_ize UN_equiv_class2, SigmaI])) 1);
   274 val zadd = result();
   275 
   276 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $+ z = z";
   277 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   278 by (ASM_SIMP_TAC (arith_ss addrews [zadd]) 1);
   279 val zadd_0 = result();
   280 
   281 goalw Integ.thy [integ_def]
   282     "!!z w. [| z: integ;  w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
   283 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   284 by (ASM_SIMP_TAC (arith_ss addrews [zminus,zadd] addcongs integ_congs) 1);
   285 val zminus_zadd_distrib = result();
   286 
   287 goalw Integ.thy [integ_def]
   288     "!!z w. [| z: integ;  w: integ |] ==> z $+ w = w $+ z";
   289 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   290 by (INTEG_SIMP_TAC [zadd] 1);
   291 by (REPEAT (ares_tac [add_commute,add_cong] 1));
   292 val zadd_commute = result();
   293 
   294 goalw Integ.thy [integ_def]
   295     "!!z1 z2 z3. [| z1: integ;  z2: integ;  z3: integ |] ==> \
   296 \                (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   297 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   298 (*rewriting is much faster without intrel_iff, etc.*)
   299 by (ASM_SIMP_TAC (intrel_ss0 addrews [zadd,add_assoc]) 1);
   300 val zadd_assoc = result();
   301 
   302 val prems = goalw Integ.thy [znat_def]
   303     "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
   304 by (ASM_SIMP_TAC (arith_ss addrews (zadd::prems)) 1);
   305 val znat_add = result();
   306 
   307 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> z $+ ($~ z) = $#0";
   308 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   309 by (ASM_SIMP_TAC (intrel_ss addrews [zminus,zadd,add_0_right]) 1);
   310 by (REPEAT (ares_tac [add_commute] 1));
   311 val zadd_zminus_inverse = result();
   312 
   313 val prems = goal Integ.thy 
   314     "z : integ ==> ($~ z) $+ z = $#0";
   315 by (rtac (zadd_commute RS trans) 1);
   316 by (REPEAT (resolve_tac (prems@[zminus_type, zadd_zminus_inverse]) 1));
   317 val zadd_zminus_inverse2 = result();
   318 
   319 val prems = goal Integ.thy "z:integ ==> z $+ $#0 = z";
   320 by (rtac (zadd_commute RS trans) 1);
   321 by (REPEAT (resolve_tac (prems@[znat_type,nat_0I,zadd_0]) 1));
   322 val zadd_0_right = result();
   323 
   324 
   325 (*Need properties of $- ???  Or use $- just as an abbreviation?
   326      [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
   327 *)
   328 
   329 (**** zmult: multiplication on integ ****)
   330 
   331 (** Congruence property for multiplication **)
   332 
   333 val prems = goalw Integ.thy [znat_def]
   334     "[| k: nat;  l: nat;  m: nat;  n: nat |] ==> 	\
   335 \    (k #+ l) #+ (m #+ n) = (k #+ m) #+ (n #+ l)";
   336 val add_commute' = read_instantiate [("m","l")] add_commute;
   337 by (SIMP_TAC (arith_ss addrews ([add_commute',add_assoc]@prems)) 1);
   338 val zmult_congruent_lemma = result();
   339 
   340 goal Integ.thy 
   341     "congruent2(intrel, %p1 p2.  		\
   342 \               split(%x1 y1. split(%x2 y2. 	\
   343 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   344 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   345 by (safe_tac intrel_cs);
   346 by (ALLGOALS (INTEG_SIMP_TAC []));
   347 (*Proof that zmult is congruent in one argument*)
   348 by (rtac (zmult_congruent_lemma RS trans) 2);
   349 by (rtac (zmult_congruent_lemma RS trans RS sym) 6);
   350 by (typechk_tac [mult_type]);
   351 by (ASM_SIMP_TAC (arith_ss addrews [add_mult_distrib_left RS sym]) 2);
   352 (*Proof that zmult is commutative on representatives*)
   353 by (rtac add_cong 1);
   354 by (rtac (add_commute RS trans) 2);
   355 by (REPEAT (ares_tac [mult_commute,add_type,mult_type,add_cong] 1));
   356 val zmult_congruent2 = result();
   357 
   358 (*Resolve th against the corresponding facts for zmult*)
   359 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   360 
   361 val prems = goalw Integ.thy [integ_def,zmult_def]
   362     "[| z: integ;  w: integ |] ==> z $* w : integ";
   363 by (REPEAT (ares_tac (prems@[zmult_ize UN_equiv_class_type2,
   364 			     split_type, add_type, mult_type, 
   365 			     quotientI, SigmaI]) 1));
   366 val zmult_type = result();
   367 
   368 
   369 val prems = goalw Integ.thy [zmult_def]
   370      "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==> 	\
   371 \     (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = 	\
   372 \     intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   373 by (ASM_SIMP_TAC (ZF_ss addrews 
   374 		  (prems @ [zmult_ize UN_equiv_class2, SigmaI])) 1);
   375 val zmult = result();
   376 
   377 goalw Integ.thy [integ_def,znat_def] "!!z. z : integ ==> $#0 $* z = $#0";
   378 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   379 by (ASM_SIMP_TAC (arith_ss addrews [zmult]) 1);
   380 val zmult_0 = result();
   381 
   382 goalw Integ.thy [integ_def,znat_def,one_def]
   383     "!!z. z : integ ==> $#1 $* z = z";
   384 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   385 by (ASM_SIMP_TAC (arith_ss addrews [zmult,add_0_right]) 1);
   386 val zmult_1 = result();
   387 
   388 goalw Integ.thy [integ_def]
   389     "!!z w. [| z: integ;  w: integ |] ==> ($~ z) $* w = $~ (z $* w)";
   390 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   391 by (INTEG_SIMP_TAC [zminus,zmult] 1);
   392 by (REPEAT (ares_tac [mult_type,add_commute,add_cong] 1));
   393 val zmult_zminus = result();
   394 
   395 goalw Integ.thy [integ_def]
   396     "!!z w. [| z: integ;  w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)";
   397 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   398 by (INTEG_SIMP_TAC [zminus,zmult] 1);
   399 by (REPEAT (ares_tac [mult_type,add_commute,add_cong] 1));
   400 val zmult_zminus_zminus = result();
   401 
   402 goalw Integ.thy [integ_def]
   403     "!!z w. [| z: integ;  w: integ |] ==> z $* w = w $* z";
   404 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   405 by (INTEG_SIMP_TAC [zmult] 1);
   406 by (res_inst_tac [("m1","xc #* y")] (add_commute RS ssubst) 1);
   407 by (REPEAT (ares_tac [mult_type,mult_commute,add_cong] 1));
   408 val zmult_commute = result();
   409 
   410 goalw Integ.thy [integ_def]
   411     "!!z1 z2 z3. [| z1: integ;  z2: integ;  z3: integ |] ==> \
   412 \                (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   413 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   414 by (INTEG_SIMP_TAC [zmult, add_mult_distrib_left, 
   415 		    add_mult_distrib, add_assoc, mult_assoc] 1);
   416 (*takes 54 seconds due to wasteful type-checking*)
   417 by (REPEAT (ares_tac [add_type, mult_type, add_commute, add_kill, 
   418 		      add_assoc_swap_kill, add_assoc_swap_kill RS sym] 1));
   419 val zmult_assoc = result();
   420 
   421 goalw Integ.thy [integ_def]
   422     "!!z1 z2 z3. [| z1: integ;  z2: integ;  w: integ |] ==> \
   423 \                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   424 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   425 by (INTEG_SIMP_TAC [zadd, zmult, add_mult_distrib, add_assoc] 1);
   426 (*takes 30 seconds due to wasteful type-checking*)
   427 by (REPEAT (ares_tac [add_type, mult_type, refl, add_commute, add_kill, 
   428 		      add_assoc_swap_kill, add_assoc_swap_kill RS sym] 1));
   429 val zadd_zmult_distrib = result();
   430 
   431 val integ_typechecks =
   432     [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   433 
   434 val integ_ss =
   435     arith_ss addcongs integ_congs
   436              addrews  ([zminus_zminus,zmagnitude_znat,zmagnitude_zminus_znat,
   437 		        zadd_0] @ integ_typechecks);