src/ZF/Integ/Int.ML
author paulson
Fri Jul 14 13:39:03 2000 +0200 (2000-07-14)
changeset 9333 5cacc383157a
parent 8201 a81d18b0a9b1
child 9491 1a36151ee2fc
permissions -rw-r--r--
changed the quotient syntax from / to //
paulson@5561
     1
(*  Title:      ZF/Integ/Int.ML
paulson@5561
     2
    ID:         $Id$
paulson@5561
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5561
     4
    Copyright   1993  University of Cambridge
paulson@5561
     5
paulson@5561
     6
The integers as equivalence classes over nat*nat.
paulson@5561
     7
paulson@5561
     8
Could also prove...
paulson@5561
     9
"znegative(z) ==> $# zmagnitude(z) = $~ z"
paulson@5561
    10
"~ znegative(z) ==> $# zmagnitude(z) = z"
paulson@5561
    11
$< is a linear ordering
paulson@5561
    12
$+ and $* are monotonic wrt $<
paulson@5561
    13
*)
paulson@5561
    14
paulson@5561
    15
AddSEs [quotientE];
paulson@5561
    16
paulson@5561
    17
(*** Proving that intrel is an equivalence relation ***)
paulson@5561
    18
paulson@5561
    19
(*By luck, requires no typing premises for y1, y2,y3*)
paulson@5561
    20
val eqa::eqb::prems = goal Arith.thy 
paulson@5561
    21
    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
paulson@5561
    22
\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
paulson@6153
    23
by (cut_facts_tac prems 1);
paulson@5561
    24
by (res_inst_tac [("k","x2")] add_left_cancel 1);
paulson@6153
    25
by (rtac (add_left_commute RS trans) 1);
paulson@6153
    26
by Auto_tac;
paulson@5561
    27
by (stac eqb 1);
paulson@6153
    28
by (rtac (add_left_commute RS trans) 1);
paulson@6153
    29
by (stac eqa 3);
paulson@6153
    30
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
paulson@5561
    31
qed "int_trans_lemma";
paulson@5561
    32
paulson@5561
    33
(** Natural deduction for intrel **)
paulson@5561
    34
paulson@5561
    35
Goalw [intrel_def]
paulson@5561
    36
    "<<x1,y1>,<x2,y2>>: intrel <-> \
paulson@5561
    37
\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
paulson@5561
    38
by (Fast_tac 1);
paulson@5561
    39
qed "intrel_iff";
paulson@5561
    40
paulson@5561
    41
Goalw [intrel_def]
paulson@5561
    42
    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
paulson@5561
    43
\             <<x1,y1>,<x2,y2>>: intrel";
paulson@5561
    44
by (fast_tac (claset() addIs prems) 1);
paulson@5561
    45
qed "intrelI";
paulson@5561
    46
paulson@5561
    47
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
paulson@5561
    48
Goalw [intrel_def]
paulson@5561
    49
  "p: intrel --> (EX x1 y1 x2 y2. \
paulson@5561
    50
\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
paulson@5561
    51
\                  x1: nat & y1: nat & x2: nat & y2: nat)";
paulson@5561
    52
by (Fast_tac 1);
paulson@5561
    53
qed "intrelE_lemma";
paulson@5561
    54
paulson@5561
    55
val [major,minor] = goal thy
paulson@5561
    56
  "[| p: intrel;  \
paulson@5561
    57
\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
paulson@5561
    58
\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
paulson@5561
    59
\  ==> Q";
paulson@5561
    60
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
paulson@5561
    61
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
paulson@5561
    62
qed "intrelE";
paulson@5561
    63
paulson@5561
    64
AddSIs [intrelI];
paulson@5561
    65
AddSEs [intrelE];
paulson@5561
    66
paulson@5561
    67
Goalw [equiv_def, refl_def, sym_def, trans_def]
paulson@5561
    68
    "equiv(nat*nat, intrel)";
paulson@5561
    69
by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
paulson@5561
    70
qed "equiv_intrel";
paulson@5561
    71
paulson@5561
    72
paulson@5561
    73
Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
paulson@5561
    74
	  add_0_right, add_succ_right];
paulson@5561
    75
Addcongs [conj_cong];
paulson@5561
    76
paulson@5561
    77
val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
paulson@5561
    78
paulson@5561
    79
(** int_of: the injection from nat to int **)
paulson@5561
    80
paulson@5561
    81
Goalw [int_def,quotient_def,int_of_def]
paulson@5561
    82
    "m : nat ==> $#m : int";
paulson@6153
    83
by Auto_tac;
paulson@5561
    84
qed "int_of_type";
paulson@5561
    85
paulson@5561
    86
Addsimps [int_of_type];
paulson@6153
    87
AddTCs   [int_of_type];
paulson@5561
    88
paulson@5561
    89
Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
paulson@5561
    90
by (dtac (sym RS eq_intrelD) 1);
paulson@6153
    91
by Auto_tac;
paulson@5561
    92
qed "int_of_inject";
paulson@5561
    93
paulson@5561
    94
AddSDs [int_of_inject];
paulson@5561
    95
paulson@5561
    96
Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
paulson@5561
    97
by (Blast_tac 1); 
paulson@5561
    98
qed "int_of_eq"; 
paulson@5561
    99
Addsimps [int_of_eq]; 
paulson@5561
   100
paulson@5561
   101
(**** zminus: unary negation on int ****)
paulson@5561
   102
paulson@5561
   103
Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
paulson@5561
   104
by Safe_tac;
paulson@5561
   105
by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
paulson@5561
   106
qed "zminus_congruent";
paulson@5561
   107
paulson@9333
   108
val RSLIST = curry (op MRS);
paulson@9333
   109
paulson@5561
   110
(*Resolve th against the corresponding facts for zminus*)
paulson@5561
   111
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
paulson@5561
   112
paulson@5561
   113
Goalw [int_def,zminus_def] "z : int ==> $~z : int";
paulson@6153
   114
by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
paulson@5561
   115
qed "zminus_type";
paulson@6153
   116
AddTCs [zminus_type];
paulson@5561
   117
paulson@5561
   118
Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
paulson@5561
   119
by (etac (zminus_ize UN_equiv_class_inject) 1);
paulson@5561
   120
by Safe_tac;
paulson@5561
   121
(*The setloop is only needed because assumptions are in the wrong order!*)
paulson@5561
   122
by (asm_full_simp_tac (simpset() addsimps add_ac
paulson@5561
   123
                       setloop dtac eq_intrelD) 1);
paulson@5561
   124
qed "zminus_inject";
paulson@5561
   125
paulson@5561
   126
Goalw [zminus_def]
paulson@5561
   127
    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
paulson@5561
   128
by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
paulson@5561
   129
qed "zminus";
paulson@5561
   130
paulson@5561
   131
Goalw [int_def] "z : int ==> $~ ($~ z) = z";
paulson@5561
   132
by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
paulson@5561
   133
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
paulson@5561
   134
qed "zminus_zminus";
paulson@5561
   135
paulson@5561
   136
Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
paulson@5561
   137
by (simp_tac (simpset() addsimps [zminus]) 1);
paulson@5561
   138
qed "zminus_0";
paulson@5561
   139
paulson@5561
   140
Addsimps [zminus_zminus, zminus_0];
paulson@5561
   141
paulson@5561
   142
paulson@5561
   143
(**** znegative: the test for negative integers ****)
paulson@5561
   144
paulson@5561
   145
(*No natural number is negative!*)
paulson@5561
   146
Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
paulson@5561
   147
by Safe_tac;
paulson@5561
   148
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
paulson@5561
   149
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
paulson@5561
   150
by (force_tac (claset(),
paulson@5561
   151
	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
paulson@5561
   152
qed "not_znegative_int_of";
paulson@5561
   153
paulson@5561
   154
Addsimps [not_znegative_int_of];
paulson@5561
   155
AddSEs   [not_znegative_int_of RS notE];
paulson@5561
   156
paulson@5561
   157
Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
paulson@5561
   158
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
paulson@5561
   159
by (blast_tac (claset() addIs [nat_0_le]) 1);
paulson@5561
   160
qed "znegative_zminus_int_of";
paulson@5561
   161
paulson@5561
   162
Addsimps [znegative_zminus_int_of];
paulson@5561
   163
paulson@5561
   164
Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
paulson@5561
   165
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
paulson@6153
   166
by (etac natE 1);
paulson@5561
   167
by (dres_inst_tac [("x","0")] spec 2);
paulson@5561
   168
by Auto_tac;
paulson@5561
   169
qed "not_znegative_imp_zero";
paulson@5561
   170
paulson@5561
   171
(**** zmagnitude: magnitide of an integer, as a natural number ****)
paulson@5561
   172
paulson@5561
   173
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
paulson@5561
   174
by Auto_tac;
paulson@5561
   175
qed "zmagnitude_int_of";
paulson@5561
   176
paulson@5561
   177
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
oheimb@5758
   178
by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
paulson@5561
   179
qed "zmagnitude_zminus_int_of";
paulson@5561
   180
paulson@5561
   181
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
paulson@5561
   182
paulson@5561
   183
Goalw [zmagnitude_def] "zmagnitude(z) : nat";
paulson@6153
   184
by (rtac theI2 1);
paulson@5561
   185
by Auto_tac;
paulson@5561
   186
qed "zmagnitude_type";
paulson@6153
   187
AddTCs [zmagnitude_type];
paulson@5561
   188
paulson@5561
   189
Goalw [int_def, znegative_def, int_of_def]
paulson@5561
   190
     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
paulson@5561
   191
by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
paulson@5561
   192
by (rename_tac "i j" 1);
paulson@5561
   193
by (dres_inst_tac [("x", "i")] spec 1);
paulson@5561
   194
by (dres_inst_tac [("x", "j")] spec 1);
paulson@6153
   195
by (rtac bexI 1);
paulson@6153
   196
by (rtac (add_diff_inverse2 RS sym) 1);
paulson@5561
   197
by Auto_tac;
paulson@8201
   198
by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
paulson@5561
   199
qed "not_zneg_int_of";
paulson@5561
   200
paulson@5561
   201
Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
paulson@6153
   202
by (dtac not_zneg_int_of 1);
paulson@5561
   203
by Auto_tac;
paulson@5561
   204
qed "not_zneg_mag"; 
paulson@5561
   205
paulson@5561
   206
Addsimps [not_zneg_mag];
paulson@5561
   207
paulson@5561
   208
paulson@5561
   209
Goalw [int_def, znegative_def, int_of_def]
paulson@5561
   210
     "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
paulson@5561
   211
by (auto_tac(claset() addSDs [less_imp_Suc_add], 
paulson@5561
   212
	     simpset() addsimps [zminus, image_singleton_iff]));
paulson@5561
   213
by (rename_tac "m n j k" 1);
paulson@5561
   214
by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
paulson@5561
   215
by (rotate_tac ~2 2);
paulson@5561
   216
by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
paulson@5561
   217
by (blast_tac (claset() addSDs [add_left_cancel]) 1);
paulson@5561
   218
qed "zneg_int_of";
paulson@5561
   219
paulson@5561
   220
Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
paulson@6153
   221
by (dtac zneg_int_of 1);
paulson@5561
   222
by Auto_tac;
paulson@5561
   223
qed "zneg_mag"; 
paulson@5561
   224
paulson@5561
   225
Addsimps [zneg_mag];
paulson@5561
   226
paulson@5561
   227
paulson@5561
   228
(**** zadd: addition on int ****)
paulson@5561
   229
paulson@5561
   230
(** Congruence property for addition **)
paulson@5561
   231
paulson@5561
   232
Goalw [congruent2_def]
paulson@5561
   233
    "congruent2(intrel, %z1 z2.                      \
paulson@5561
   234
\         let <x1,y1>=z1; <x2,y2>=z2                 \
paulson@5561
   235
\                           in intrel``{<x1#+x2, y1#+y2>})";
paulson@5561
   236
(*Proof via congruent2_commuteI seems longer*)
paulson@5561
   237
by Safe_tac;
paulson@5561
   238
by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
paulson@5561
   239
(*The rest should be trivial, but rearranging terms is hard;
paulson@5561
   240
  add_ac does not help rewriting with the assumptions.*)
paulson@5561
   241
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
paulson@5561
   242
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
paulson@6153
   243
by Auto_tac;
paulson@5561
   244
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
paulson@5561
   245
qed "zadd_congruent2";
paulson@5561
   246
paulson@5561
   247
(*Resolve th against the corresponding facts for zadd*)
paulson@5561
   248
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
paulson@5561
   249
paulson@5561
   250
Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
paulson@5561
   251
by (rtac (zadd_ize UN_equiv_class_type2) 1);
paulson@5561
   252
by (simp_tac (simpset() addsimps [Let_def]) 3);
paulson@5561
   253
by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
paulson@5561
   254
qed "zadd_type";
paulson@6153
   255
AddTCs [zadd_type];
paulson@5561
   256
paulson@5561
   257
Goalw [zadd_def]
paulson@5561
   258
  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
paulson@5561
   259
\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
paulson@5561
   260
\           intrel `` {<x1#+x2, y1#+y2>}";
paulson@5561
   261
by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
paulson@5561
   262
by (simp_tac (simpset() addsimps [Let_def]) 1);
paulson@5561
   263
qed "zadd";
paulson@5561
   264
paulson@5561
   265
Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
paulson@5561
   266
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   267
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
paulson@5561
   268
qed "zadd_0";
paulson@5561
   269
paulson@5561
   270
Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
paulson@5561
   271
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   272
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
paulson@5561
   273
qed "zminus_zadd_distrib";
paulson@5561
   274
paulson@5561
   275
Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
paulson@5561
   276
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   277
by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
paulson@5561
   278
qed "zadd_commute";
paulson@5561
   279
paulson@5561
   280
Goalw [int_def]
paulson@5561
   281
    "[| z1: int;  z2: int;  z3: int |]   \
paulson@5561
   282
\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
paulson@5561
   283
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   284
(*rewriting is much faster without intrel_iff, etc.*)
paulson@5561
   285
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
paulson@5561
   286
qed "zadd_assoc";
paulson@5561
   287
paulson@5561
   288
(*For AC rewriting*)
paulson@5561
   289
Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
paulson@6153
   290
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
paulson@6153
   291
by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
paulson@5561
   292
qed "zadd_left_commute";
paulson@5561
   293
paulson@5561
   294
(*Integer addition is an AC operator*)
paulson@5561
   295
val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
paulson@5561
   296
paulson@5561
   297
Goalw [int_of_def]
paulson@5561
   298
    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
paulson@5561
   299
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
paulson@5561
   300
qed "int_of_add";
paulson@5561
   301
paulson@5561
   302
Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
paulson@5561
   303
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   304
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
paulson@5561
   305
qed "zadd_zminus_inverse";
paulson@5561
   306
paulson@5561
   307
Goal "z : int ==> ($~ z) $+ z = $#0";
paulson@5561
   308
by (asm_simp_tac
paulson@5561
   309
    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
paulson@5561
   310
qed "zadd_zminus_inverse2";
paulson@5561
   311
paulson@5561
   312
Goal "z:int ==> z $+ $#0 = z";
paulson@5561
   313
by (rtac (zadd_commute RS trans) 1);
paulson@5561
   314
by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
paulson@5561
   315
qed "zadd_0_right";
paulson@5561
   316
paulson@5561
   317
Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
paulson@5561
   318
paulson@5561
   319
paulson@5561
   320
(*Need properties of $- ???  Or use $- just as an abbreviation?
paulson@5561
   321
     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
paulson@5561
   322
*)
paulson@5561
   323
paulson@5561
   324
(**** zmult: multiplication on int ****)
paulson@5561
   325
paulson@5561
   326
(** Congruence property for multiplication **)
paulson@5561
   327
paulson@5561
   328
Goal "congruent2(intrel, %p1 p2.                 \
paulson@5561
   329
\               split(%x1 y1. split(%x2 y2.     \
paulson@5561
   330
\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
paulson@5561
   331
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
paulson@5561
   332
by Safe_tac;
paulson@5561
   333
by (ALLGOALS Asm_simp_tac);
paulson@5561
   334
(*Proof that zmult is congruent in one argument*)
paulson@5561
   335
by (asm_simp_tac 
paulson@5561
   336
    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
paulson@5561
   337
by (asm_simp_tac
paulson@5561
   338
    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
paulson@5561
   339
(*Proof that zmult is commutative on representatives*)
paulson@5561
   340
by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
paulson@5561
   341
qed "zmult_congruent2";
paulson@5561
   342
paulson@5561
   343
paulson@5561
   344
(*Resolve th against the corresponding facts for zmult*)
paulson@5561
   345
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
paulson@5561
   346
paulson@5561
   347
Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
paulson@5561
   348
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
paulson@5561
   349
                      split_type, add_type, mult_type, 
paulson@5561
   350
                      quotientI, SigmaI] 1));
paulson@5561
   351
qed "zmult_type";
paulson@6153
   352
AddTCs [zmult_type];
paulson@5561
   353
paulson@5561
   354
Goalw [zmult_def]
paulson@5561
   355
     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
paulson@5561
   356
\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
paulson@5561
   357
\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
paulson@5561
   358
by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
paulson@5561
   359
qed "zmult";
paulson@5561
   360
paulson@5561
   361
Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
paulson@5561
   362
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   363
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
paulson@5561
   364
qed "zmult_0";
paulson@5561
   365
paulson@5561
   366
Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
paulson@5561
   367
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   368
by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
paulson@5561
   369
qed "zmult_1";
paulson@5561
   370
paulson@5561
   371
Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
paulson@5561
   372
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   373
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
paulson@5561
   374
qed "zmult_zminus";
paulson@5561
   375
paulson@5561
   376
Addsimps [zmult_0, zmult_1, zmult_zminus];
paulson@5561
   377
paulson@5561
   378
Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
paulson@5561
   379
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   380
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
paulson@5561
   381
qed "zmult_zminus_zminus";
paulson@5561
   382
paulson@5561
   383
Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
paulson@5561
   384
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   385
by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
paulson@5561
   386
qed "zmult_commute";
paulson@5561
   387
paulson@5561
   388
Goalw [int_def]
paulson@5561
   389
    "[| z1: int;  z2: int;  z3: int |]     \
paulson@5561
   390
\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
paulson@5561
   391
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   392
by (asm_simp_tac 
paulson@5561
   393
    (simpset() addsimps [zmult, add_mult_distrib_left, 
paulson@5561
   394
                         add_mult_distrib] @ add_ac @ mult_ac) 1);
paulson@5561
   395
qed "zmult_assoc";
paulson@5561
   396
paulson@5561
   397
(*For AC rewriting*)
paulson@5561
   398
Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
paulson@6153
   399
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
paulson@6153
   400
by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
paulson@5561
   401
qed "zmult_left_commute";
paulson@5561
   402
paulson@5561
   403
(*Integer multiplication is an AC operator*)
paulson@5561
   404
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
paulson@5561
   405
paulson@5561
   406
Goalw [int_def]
paulson@5561
   407
    "[| z1: int;  z2: int;  w: int |] ==> \
paulson@5561
   408
\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
paulson@5561
   409
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
paulson@5561
   410
by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
paulson@5561
   411
by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
paulson@5561
   412
qed "zadd_zmult_distrib";
paulson@5561
   413
paulson@5561
   414
val int_typechecks =
paulson@5561
   415
    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
paulson@5561
   416
paulson@5561
   417
Addsimps int_typechecks;
paulson@5561
   418
paulson@5561
   419
paulson@5561
   420