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