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