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);
```