src/ZF/Integ/Int.ML
author paulson
Wed Aug 02 16:07:32 2000 +0200 (2000-08-02)
changeset 9496 07e33cac5d9c
parent 9491 1a36151ee2fc
child 9548 15bee2731e43
permissions -rw-r--r--
coercion "intify" to remove type constraints from integer algebraic laws
     1 (*  Title:      ZF/Integ/Int.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 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 AddSEs [quotientE];
    16 
    17 (*** Proving that intrel is an equivalence relation ***)
    18 
    19 (** Natural deduction for intrel **)
    20 
    21 Goalw [intrel_def]
    22     "<<x1,y1>,<x2,y2>>: intrel <-> \
    23 \    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
    24 by (Fast_tac 1);
    25 qed "intrel_iff";
    26 
    27 Goalw [intrel_def]
    28     "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]  \
    29 \    ==> <<x1,y1>,<x2,y2>>: intrel";
    30 by (fast_tac (claset() addIs prems) 1);
    31 qed "intrelI";
    32 
    33 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    34 Goalw [intrel_def]
    35   "p: intrel --> (EX x1 y1 x2 y2. \
    36 \                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    37 \                  x1: nat & y1: nat & x2: nat & y2: nat)";
    38 by (Fast_tac 1);
    39 qed "intrelE_lemma";
    40 
    41 val [major,minor] = goal thy
    42   "[| p: intrel;  \
    43 \     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    44 \                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    45 \  ==> Q";
    46 by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    47 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    48 qed "intrelE";
    49 
    50 AddSIs [intrelI];
    51 AddSEs [intrelE];
    52 
    53 val eqa::eqb::prems = goal Arith.thy 
    54     "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    55 by (res_inst_tac [("k","x2")] add_left_cancel 1);
    56 by (rtac (add_left_commute RS trans) 1);
    57 by Auto_tac;
    58 by (stac eqb 1);
    59 by (rtac (add_left_commute RS trans) 1);
    60 by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
    61 qed "int_trans_lemma";
    62 
    63 Goalw [equiv_def, refl_def, sym_def, trans_def]
    64     "equiv(nat*nat, intrel)";
    65 by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    66 qed "equiv_intrel";
    67 
    68 
    69 Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
    70 by (blast_tac (claset() addIs [quotientI]) 1);
    71 qed "image_intrel_int";
    72 
    73 
    74 Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    75 	  add_0_right, add_succ_right];
    76 Addcongs [conj_cong];
    77 
    78 val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
    79 
    80 (** int_of: the injection from nat to int **)
    81 
    82 Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
    83 by Auto_tac;
    84 qed "int_of_type";
    85 
    86 AddIffs [int_of_type];
    87 AddTCs  [int_of_type];
    88 
    89 
    90 Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
    91 by Auto_tac;  
    92 qed "int_of_eq"; 
    93 AddIffs [int_of_eq];
    94 
    95 Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
    96 by (dtac (int_of_eq RS iffD1) 1);
    97 by Auto_tac;
    98 qed "int_of_inject";
    99 
   100 
   101 (** intify: coercion from anything to int **)
   102 
   103 Goal "intify(x) : int";
   104 by (simp_tac (simpset() addsimps [intify_def]) 1);
   105 qed "intify_in_int";
   106 AddIffs [intify_in_int];
   107 AddTCs [intify_in_int];
   108 
   109 Goal "n : int ==> intify(n) = n";
   110 by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
   111 qed "intify_ident";
   112 Addsimps [intify_ident];
   113 
   114 
   115 (*** Collapsing rules: to remove intify from arithmetic expressions ***)
   116 
   117 Goal "intify(intify(x)) = intify(x)";
   118 by (Simp_tac 1);
   119 qed "intify_idem";
   120 Addsimps [intify_idem];
   121 
   122 Goal "$# (natify(m)) = $# m";
   123 by (simp_tac (simpset() addsimps [int_of_def]) 1);
   124 qed "int_of_natify";
   125 
   126 Goal "$~ (intify(m)) = $~ m";
   127 by (simp_tac (simpset() addsimps [zminus_def]) 1);
   128 qed "zminus_intify";
   129 
   130 Addsimps [int_of_natify, zminus_intify];
   131 
   132 (** Addition **)
   133 
   134 Goal "intify(x) $+ y = x $+ y";
   135 by (simp_tac (simpset() addsimps [zadd_def]) 1);
   136 qed "zadd_intify1";
   137 
   138 Goal "x $+ intify(y) = x $+ y";
   139 by (simp_tac (simpset() addsimps [zadd_def]) 1);
   140 qed "zadd_intify2";
   141 Addsimps [zadd_intify1, zadd_intify2];
   142 
   143 (** Multiplication **)
   144 
   145 Goal "intify(x) $* y = x $* y";
   146 by (simp_tac (simpset() addsimps [zmult_def]) 1);
   147 qed "zmult_intify1";
   148 
   149 Goal "x $* intify(y) = x $* y";
   150 by (simp_tac (simpset() addsimps [zmult_def]) 1);
   151 qed "zmult_intify2";
   152 Addsimps [zmult_intify1, zmult_intify2];
   153 
   154 
   155 (**** zminus: unary negation on int ****)
   156 
   157 Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   158 by Safe_tac;
   159 by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   160 qed "zminus_congruent";
   161 
   162 val RSLIST = curry (op MRS);
   163 
   164 (*Resolve th against the corresponding facts for zminus*)
   165 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   166 
   167 Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
   168 by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
   169 qed "raw_zminus_type";
   170 
   171 Goalw [zminus_def] "$~z : int";
   172 by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
   173 qed "zminus_type";
   174 AddIffs [zminus_type];
   175 AddTCs [zminus_type];
   176 
   177 
   178 Goalw [int_def,raw_zminus_def]
   179      "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
   180 by (etac (zminus_ize UN_equiv_class_inject) 1);
   181 by Safe_tac;
   182 by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
   183 qed "raw_zminus_inject";
   184 
   185 Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
   186 by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
   187 qed "zminus_inject_intify";
   188 
   189 AddSDs [zminus_inject_intify];
   190 
   191 Goal "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   192 by Auto_tac;  
   193 qed "zminus_inject";
   194 
   195 Goalw [raw_zminus_def]
   196     "[| x: nat;  y: nat |] \
   197 \    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
   198 by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   199 qed "raw_zminus";
   200 
   201 Goalw [zminus_def]
   202     "[| x: nat;  y: nat |] \
   203 \    ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   204 by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
   205 qed "zminus";
   206 
   207 Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
   208 by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
   209 qed "raw_zminus_zminus";
   210 
   211 Goal "$~ ($~ z) = intify(z)";
   212 by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
   213 	                          raw_zminus_zminus]) 1);
   214 qed "zminus_zminus_intify"; 
   215 
   216 Goalw [int_of_def] "$~ ($#0) = $#0";
   217 by (simp_tac (simpset() addsimps [zminus]) 1);
   218 qed "zminus_0";
   219 
   220 Addsimps [zminus_zminus_intify, zminus_0];
   221 
   222 Goal "z : int ==> $~ ($~ z) = z";
   223 by (Asm_simp_tac 1);
   224 qed "zminus_zminus";
   225 
   226 
   227 (**** znegative: the test for negative integers ****)
   228 
   229 (*No natural number is negative!*)
   230 Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
   231 by Safe_tac;
   232 by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   233 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   234 by (force_tac (claset(),
   235 	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
   236 qed "not_znegative_int_of";
   237 
   238 Addsimps [not_znegative_int_of];
   239 AddSEs   [not_znegative_int_of RS notE];
   240 
   241 Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
   242 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   243 by (blast_tac (claset() addIs [nat_0_le]) 1);
   244 qed "znegative_zminus_int_of";
   245 
   246 Addsimps [znegative_zminus_int_of];
   247 
   248 Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
   249 by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   250 by (dres_inst_tac [("x","0")] spec 1);
   251 by (auto_tac(claset(), 
   252              simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
   253 qed "not_znegative_imp_zero";
   254 
   255 (**** zmagnitude: magnitide of an integer, as a natural number ****)
   256 
   257 Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
   258 by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
   259 qed "zmagnitude_int_of";
   260 
   261 Goal "natify(x)=n ==> $#x = $# n";
   262 by (dtac sym 1);
   263 by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
   264 qed "natify_int_of_eq";
   265 
   266 Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
   267 by (rtac the_equality 1);
   268 by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
   269               simpset())
   270              delIffs [int_of_eq]));
   271 by Auto_tac;  
   272 qed "zmagnitude_zminus_int_of";
   273 
   274 Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   275 
   276 Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   277 by (rtac theI2 1);
   278 by Auto_tac;
   279 qed "zmagnitude_type";
   280 AddTCs [zmagnitude_type];
   281 
   282 Goalw [int_def, znegative_def, int_of_def]
   283      "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   284 by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   285 by (rename_tac "i j" 1);
   286 by (dres_inst_tac [("x", "i")] spec 1);
   287 by (dres_inst_tac [("x", "j")] spec 1);
   288 by (rtac bexI 1);
   289 by (rtac (add_diff_inverse2 RS sym) 1);
   290 by Auto_tac;
   291 by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
   292 qed "not_zneg_int_of";
   293 
   294 Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   295 by (dtac not_zneg_int_of 1);
   296 by Auto_tac;
   297 qed "not_zneg_mag"; 
   298 
   299 Addsimps [not_zneg_mag];
   300 
   301 
   302 Goalw [int_def, znegative_def, int_of_def]
   303      "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
   304 by (auto_tac(claset() addSDs [less_imp_Suc_add], 
   305 	     simpset() addsimps [zminus, image_singleton_iff]));
   306 by (rename_tac "m n j k" 1);
   307 by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
   308 by (rotate_tac ~2 2);
   309 by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   310 by (blast_tac (claset() addSDs [add_left_cancel]) 1);
   311 qed "zneg_int_of";
   312 
   313 Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   314 by (dtac zneg_int_of 1);
   315 by Auto_tac;
   316 qed "zneg_mag"; 
   317 
   318 Addsimps [zneg_mag];
   319 
   320 
   321 (**** zadd: addition on int ****)
   322 
   323 (** Congruence property for addition **)
   324 
   325 Goalw [congruent2_def]
   326     "congruent2(intrel, %z1 z2.                      \
   327 \         let <x1,y1>=z1; <x2,y2>=z2                 \
   328 \                           in intrel``{<x1#+x2, y1#+y2>})";
   329 (*Proof via congruent2_commuteI seems longer*)
   330 by Safe_tac;
   331 by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   332 (*The rest should be trivial, but rearranging terms is hard;
   333   add_ac does not help rewriting with the assumptions.*)
   334 by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   335 by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
   336 by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   337 qed "zadd_congruent2";
   338 
   339 (*Resolve th against the corresponding facts for zadd*)
   340 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   341 
   342 Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
   343 by (rtac (zadd_ize UN_equiv_class_type2) 1);
   344 by (simp_tac (simpset() addsimps [Let_def]) 3);
   345 by (REPEAT (assume_tac 1));
   346 qed "raw_zadd_type";
   347 
   348 Goal "z $+ w : int";
   349 by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
   350 qed "zadd_type";
   351 AddIffs [zadd_type];  AddTCs [zadd_type];
   352 
   353 Goalw [raw_zadd_def]
   354   "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
   355 \  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
   356 \      intrel `` {<x1#+x2, y1#+y2>}";
   357 by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   358 by (simp_tac (simpset() addsimps [Let_def]) 1);
   359 qed "raw_zadd";
   360 
   361 Goalw [zadd_def]
   362   "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
   363 \  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
   364 \      intrel `` {<x1#+x2, y1#+y2>}";
   365 by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
   366 qed "zadd";
   367 
   368 Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
   369 by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
   370 qed "raw_zadd_0";
   371 
   372 Goal "$#0 $+ z = intify(z)";
   373 by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
   374 qed "zadd_0_intify";
   375 Addsimps [zadd_0_intify];
   376 
   377 Goal "z: int ==> $#0 $+ z = z";
   378 by (Asm_simp_tac 1);
   379 qed "zadd_0";
   380 
   381 Goalw [int_def]
   382      "[| z: int;  w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
   383 by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
   384 qed "raw_zminus_zadd_distrib";
   385 
   386 Goal "$~ (z $+ w) = $~ z $+ $~ w";
   387 by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
   388 qed "zminus_zadd_distrib";
   389 
   390 Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
   391 by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
   392 qed "raw_zadd_commute";
   393 
   394 Goal "z $+ w = w $+ z";
   395 by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
   396 qed "zadd_commute";
   397 
   398 Goalw [int_def]
   399     "[| z1: int;  z2: int;  z3: int |]   \
   400 \    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
   401 by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
   402 qed "raw_zadd_assoc";
   403 
   404 Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   405 by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
   406 qed "zadd_assoc";
   407 
   408 (*For AC rewriting*)
   409 Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
   410 by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   411 by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
   412 qed "zadd_left_commute";
   413 
   414 (*Integer addition is an AC operator*)
   415 val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   416 
   417 Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
   418 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   419 qed "int_of_add";
   420 
   421 Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $~ z) = $#0";
   422 by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
   423 qed "raw_zadd_zminus_inverse";
   424 
   425 Goal "z $+ ($~ z) = $#0";
   426 by (simp_tac (simpset() addsimps [zadd_def]) 1);
   427 by (stac (zminus_intify RS sym) 1);
   428 by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
   429 qed "zadd_zminus_inverse";
   430 
   431 Goal "($~ z) $+ z = $#0";
   432 by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
   433 qed "zadd_zminus_inverse2";
   434 
   435 Goal "z $+ $#0 = intify(z)";
   436 by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
   437 qed "zadd_0_right_intify";
   438 Addsimps [zadd_0_right_intify];
   439 
   440 Goal "z:int ==> z $+ $#0 = z";
   441 by (Asm_simp_tac 1);
   442 qed "zadd_0_right";
   443 
   444 Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
   445 
   446 
   447 (*Need properties of $- ???  Or use $- just as an abbreviation?
   448      [| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
   449 *)
   450 
   451 (**** zmult: multiplication on int ****)
   452 
   453 (** Congruence property for multiplication **)
   454 
   455 Goal "congruent2(intrel, %p1 p2.                 \
   456 \               split(%x1 y1. split(%x2 y2.     \
   457 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   458 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   459 by Safe_tac;
   460 by (ALLGOALS Asm_simp_tac);
   461 (*Proof that zmult is congruent in one argument*)
   462 by (asm_simp_tac 
   463     (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
   464 by (asm_simp_tac
   465     (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
   466 (*Proof that zmult is commutative on representatives*)
   467 by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
   468 qed "zmult_congruent2";
   469 
   470 
   471 (*Resolve th against the corresponding facts for zmult*)
   472 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   473 
   474 Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
   475 by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   476                       split_type, add_type, mult_type, 
   477                       quotientI, SigmaI] 1));
   478 qed "raw_zmult_type";
   479 
   480 Goal "z $* w : int";
   481 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
   482 qed "zmult_type";
   483 AddIffs [zmult_type];  AddTCs [zmult_type];
   484 
   485 Goalw [raw_zmult_def]
   486      "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   487 \     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
   488 \         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   489 by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   490 qed "raw_zmult";
   491 
   492 Goalw [zmult_def]
   493      "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   494 \     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   495 \         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   496 by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
   497 qed "zmult";
   498 
   499 Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
   500 by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   501 qed "raw_zmult_0";
   502 
   503 Goal "$#0 $* z = $#0";
   504 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
   505 qed "zmult_0";
   506 Addsimps [zmult_0];
   507 
   508 Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
   509 by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   510 qed "raw_zmult_1";
   511 
   512 Goal "$#1 $* z = intify(z)";
   513 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
   514 qed "zmult_1_intify";
   515 Addsimps [zmult_1_intify];
   516 
   517 Goal "z : int ==> $#1 $* z = z";
   518 by (Asm_simp_tac 1);
   519 qed "zmult_1";
   520 
   521 Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
   522 by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
   523 qed "raw_zmult_commute";
   524 
   525 Goal "z $* w = w $* z";
   526 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
   527 qed "zmult_commute";
   528 
   529 Goalw [int_def]
   530      "[| z: int;  w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
   531 by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
   532 qed "raw_zmult_zminus";
   533 
   534 Goal "($~ z) $* w = $~ (z $* w)";
   535 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
   536 by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
   537 by Auto_tac;  
   538 qed "zmult_zminus";
   539 Addsimps [zmult_zminus];
   540 
   541 Goal "($~ z) $* ($~ w) = (z $* w)";
   542 by (stac zmult_zminus 1);
   543 by (stac zmult_commute 1 THEN stac zmult_zminus 1);
   544 by (simp_tac (simpset() addsimps [zmult_commute])1);
   545 qed "zmult_zminus_zminus";
   546 
   547 Goalw [int_def]
   548     "[| z1: int;  z2: int;  z3: int |]   \
   549 \    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
   550 by (auto_tac (claset(), 
   551   simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
   552 qed "raw_zmult_assoc";
   553 
   554 Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   555 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
   556                                   raw_zmult_assoc]) 1);
   557 qed "zmult_assoc";
   558 
   559 (*For AC rewriting*)
   560 Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
   561 by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   562 by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
   563 qed "zmult_left_commute";
   564 
   565 (*Integer multiplication is an AC operator*)
   566 val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   567 
   568 Goalw [int_def]
   569     "[| z1: int;  z2: int;  w: int |]  \
   570 \    ==> raw_zmult(raw_zadd(z1,z2), w) = \
   571 \        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
   572 by (auto_tac (claset(), 
   573               simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
   574                                  add_ac @ mult_ac));  
   575 qed "raw_zadd_zmult_distrib";
   576 
   577 Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   578 by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
   579      	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
   580 qed "zadd_zmult_distrib";
   581 
   582 Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
   583 by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
   584                                   zadd_zmult_distrib]) 1);
   585 qed "zadd_zmult_distrib_left";
   586 
   587 val int_typechecks =
   588     [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   589 
   590