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