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