src/ZF/Integ/Int.ML
author paulson
Mon Aug 07 10:29:54 2000 +0200 (2000-08-07)
changeset 9548 15bee2731e43
parent 9496 07e33cac5d9c
child 9570 e16e168984e1
permissions -rw-r--r--
instantiated Cancel_Numerals for "nat" in ZF
     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 $+ and $* are monotonic wrt $<
    12 [| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
    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 Goal "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
    54 by (rtac sym 1);
    55 by (REPEAT (etac add_left_cancel 1));
    56 by (ALLGOALS Asm_simp_tac);
    57 qed "int_trans_lemma";
    58 
    59 Goalw [equiv_def, refl_def, sym_def, trans_def]
    60     "equiv(nat*nat, intrel)";
    61 by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    62 qed "equiv_intrel";
    63 
    64 
    65 Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
    66 by (blast_tac (claset() addIs [quotientI]) 1);
    67 qed "image_intrel_int";
    68 
    69 
    70 Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    71 	  add_0_right, add_succ_right];
    72 Addcongs [conj_cong];
    73 
    74 val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
    75 
    76 (** int_of: the injection from nat to int **)
    77 
    78 Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
    79 by Auto_tac;
    80 qed "int_of_type";
    81 
    82 AddIffs [int_of_type];
    83 AddTCs  [int_of_type];
    84 
    85 
    86 Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
    87 by Auto_tac;  
    88 qed "int_of_eq"; 
    89 AddIffs [int_of_eq];
    90 
    91 Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
    92 by (dtac (int_of_eq RS iffD1) 1);
    93 by Auto_tac;
    94 qed "int_of_inject";
    95 
    96 
    97 (** intify: coercion from anything to int **)
    98 
    99 Goal "intify(x) : int";
   100 by (simp_tac (simpset() addsimps [intify_def]) 1);
   101 qed "intify_in_int";
   102 AddIffs [intify_in_int];
   103 AddTCs [intify_in_int];
   104 
   105 Goal "n : int ==> intify(n) = n";
   106 by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
   107 qed "intify_ident";
   108 Addsimps [intify_ident];
   109 
   110 
   111 (*** Collapsing rules: to remove intify from arithmetic expressions ***)
   112 
   113 Goal "intify(intify(x)) = intify(x)";
   114 by (Simp_tac 1);
   115 qed "intify_idem";
   116 Addsimps [intify_idem];
   117 
   118 Goal "$# (natify(m)) = $# m";
   119 by (simp_tac (simpset() addsimps [int_of_def]) 1);
   120 qed "int_of_natify";
   121 
   122 Goal "$- (intify(m)) = $- m";
   123 by (simp_tac (simpset() addsimps [zminus_def]) 1);
   124 qed "zminus_intify";
   125 
   126 Addsimps [int_of_natify, zminus_intify];
   127 
   128 (** Addition **)
   129 
   130 Goal "intify(x) $+ y = x $+ y";
   131 by (simp_tac (simpset() addsimps [zadd_def]) 1);
   132 qed "zadd_intify1";
   133 
   134 Goal "x $+ intify(y) = x $+ y";
   135 by (simp_tac (simpset() addsimps [zadd_def]) 1);
   136 qed "zadd_intify2";
   137 Addsimps [zadd_intify1, zadd_intify2];
   138 
   139 (** Subtraction **)
   140 
   141 Goal "intify(x) $- y = x $- y";
   142 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   143 qed "zdiff_intify1";
   144 
   145 Goal "x $- intify(y) = x $- y";
   146 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   147 qed "zdiff_intify2";
   148 Addsimps [zdiff_intify1, zdiff_intify2];
   149 
   150 (** Multiplication **)
   151 
   152 Goal "intify(x) $* y = x $* y";
   153 by (simp_tac (simpset() addsimps [zmult_def]) 1);
   154 qed "zmult_intify1";
   155 
   156 Goal "x $* intify(y) = x $* y";
   157 by (simp_tac (simpset() addsimps [zmult_def]) 1);
   158 qed "zmult_intify2";
   159 Addsimps [zmult_intify1, zmult_intify2];
   160 
   161 (** Orderings **)
   162 
   163 Goal "intify(x) $< y <-> x $< y";
   164 by (simp_tac (simpset() addsimps [zless_def]) 1);
   165 qed "zless_intify1";
   166 
   167 Goal "x $< intify(y) <-> x $< y";
   168 by (simp_tac (simpset() addsimps [zless_def]) 1);
   169 qed "zless_intify2";
   170 Addsimps [zless_intify1, zless_intify2];
   171 
   172 
   173 (**** zminus: unary negation on int ****)
   174 
   175 Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   176 by Safe_tac;
   177 by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   178 qed "zminus_congruent";
   179 
   180 val RSLIST = curry (op MRS);
   181 
   182 (*Resolve th against the corresponding facts for zminus*)
   183 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   184 
   185 Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
   186 by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
   187 qed "raw_zminus_type";
   188 
   189 Goalw [zminus_def] "$-z : int";
   190 by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
   191 qed "zminus_type";
   192 AddIffs [zminus_type];
   193 AddTCs [zminus_type];
   194 
   195 
   196 Goalw [int_def,raw_zminus_def]
   197      "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
   198 by (etac (zminus_ize UN_equiv_class_inject) 1);
   199 by Safe_tac;
   200 by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
   201 qed "raw_zminus_inject";
   202 
   203 Goalw [zminus_def] "$-z = $-w ==> intify(z) = intify(w)";
   204 by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
   205 qed "zminus_inject_intify";
   206 
   207 AddSDs [zminus_inject_intify];
   208 
   209 Goal "[| $-z = $-w;  z: int;  w: int |] ==> z=w";
   210 by Auto_tac;  
   211 qed "zminus_inject";
   212 
   213 Goalw [raw_zminus_def]
   214     "[| x: nat;  y: nat |] \
   215 \    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
   216 by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   217 qed "raw_zminus";
   218 
   219 Goalw [zminus_def]
   220     "[| x: nat;  y: nat |] \
   221 \    ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}";
   222 by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
   223 qed "zminus";
   224 
   225 Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
   226 by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
   227 qed "raw_zminus_zminus";
   228 
   229 Goal "$- ($- z) = intify(z)";
   230 by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
   231 	                          raw_zminus_zminus]) 1);
   232 qed "zminus_zminus_intify"; 
   233 
   234 Goalw [int_of_def] "$- ($#0) = $#0";
   235 by (simp_tac (simpset() addsimps [zminus]) 1);
   236 qed "zminus_0";
   237 
   238 Addsimps [zminus_zminus_intify, zminus_0];
   239 
   240 Goal "z : int ==> $- ($- z) = z";
   241 by (Asm_simp_tac 1);
   242 qed "zminus_zminus";
   243 
   244 
   245 (**** znegative: the test for negative integers ****)
   246 
   247 (*No natural number is negative!*)
   248 Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
   249 by Safe_tac;
   250 by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   251 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   252 by (force_tac (claset(),
   253 	       simpset() addsimps [add_le_self2 RS le_imp_not_lt,
   254 				   natify_succ]) 1);
   255 qed "not_znegative_int_of";
   256 
   257 Addsimps [not_znegative_int_of];
   258 AddSEs   [not_znegative_int_of RS notE];
   259 
   260 Goalw [znegative_def, int_of_def] "znegative($- $# succ(n))";
   261 by (asm_simp_tac (simpset() addsimps [zminus, natify_succ]) 1);
   262 by (blast_tac (claset() addIs [nat_0_le]) 1);
   263 qed "znegative_zminus_int_of";
   264 
   265 Addsimps [znegative_zminus_int_of];
   266 
   267 Goalw [znegative_def, int_of_def] "~ znegative($- $# n) ==> natify(n)=0";
   268 by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   269 by (dres_inst_tac [("x","0")] spec 1);
   270 by (auto_tac(claset(), 
   271              simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
   272 qed "not_znegative_imp_zero";
   273 
   274 (**** zmagnitude: magnitide of an integer, as a natural number ****)
   275 
   276 Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
   277 by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
   278 qed "zmagnitude_int_of";
   279 
   280 Goal "natify(x)=n ==> $#x = $# n";
   281 by (dtac sym 1);
   282 by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
   283 qed "natify_int_of_eq";
   284 
   285 Goalw [zmagnitude_def] "zmagnitude($- $# n) = natify(n)";
   286 by (rtac the_equality 1);
   287 by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
   288               simpset())
   289              delIffs [int_of_eq]));
   290 by Auto_tac;  
   291 qed "zmagnitude_zminus_int_of";
   292 
   293 Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   294 
   295 Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   296 by (rtac theI2 1);
   297 by Auto_tac;
   298 qed "zmagnitude_type";
   299 AddTCs [zmagnitude_type];
   300 
   301 Goalw [int_def, znegative_def, int_of_def]
   302      "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   303 by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   304 by (rename_tac "i j" 1);
   305 by (dres_inst_tac [("x", "i")] spec 1);
   306 by (dres_inst_tac [("x", "j")] spec 1);
   307 by (rtac bexI 1);
   308 by (rtac (add_diff_inverse2 RS sym) 1);
   309 by Auto_tac;
   310 by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
   311 qed "not_zneg_int_of";
   312 
   313 Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   314 by (dtac not_zneg_int_of 1);
   315 by Auto_tac;
   316 qed "not_zneg_mag"; 
   317 
   318 Addsimps [not_zneg_mag];
   319 
   320 
   321 Goalw [int_def, znegative_def, int_of_def]
   322      "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))"; 
   323 by (auto_tac(claset() addSDs [less_imp_succ_add], 
   324 	     simpset() addsimps [zminus, image_singleton_iff]));
   325 qed "zneg_int_of";
   326 
   327 Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $- z"; 
   328 by (dtac zneg_int_of 1);
   329 by Auto_tac;
   330 qed "zneg_mag"; 
   331 
   332 Addsimps [zneg_mag];
   333 
   334 
   335 (**** zadd: addition on int ****)
   336 
   337 (** Congruence property for addition **)
   338 
   339 Goalw [congruent2_def]
   340     "congruent2(intrel, %z1 z2.                      \
   341 \         let <x1,y1>=z1; <x2,y2>=z2                 \
   342 \                           in intrel``{<x1#+x2, y1#+y2>})";
   343 (*Proof via congruent2_commuteI seems longer*)
   344 by Safe_tac;
   345 by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   346 (*The rest should be trivial, but rearranging terms is hard;
   347   add_ac does not help rewriting with the assumptions.*)
   348 by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   349 by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
   350 by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   351 qed "zadd_congruent2";
   352 
   353 (*Resolve th against the corresponding facts for zadd*)
   354 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   355 
   356 Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
   357 by (rtac (zadd_ize UN_equiv_class_type2) 1);
   358 by (simp_tac (simpset() addsimps [Let_def]) 3);
   359 by (REPEAT (assume_tac 1));
   360 qed "raw_zadd_type";
   361 
   362 Goal "z $+ w : int";
   363 by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
   364 qed "zadd_type";
   365 AddIffs [zadd_type];  AddTCs [zadd_type];
   366 
   367 Goalw [raw_zadd_def]
   368   "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
   369 \  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
   370 \      intrel `` {<x1#+x2, y1#+y2>}";
   371 by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   372 by (simp_tac (simpset() addsimps [Let_def]) 1);
   373 qed "raw_zadd";
   374 
   375 Goalw [zadd_def]
   376   "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
   377 \  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
   378 \      intrel `` {<x1#+x2, y1#+y2>}";
   379 by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
   380 qed "zadd";
   381 
   382 Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
   383 by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
   384 qed "raw_zadd_int0";
   385 
   386 Goal "$#0 $+ z = intify(z)";
   387 by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_int0]) 1);
   388 qed "zadd_int0_intify";
   389 Addsimps [zadd_int0_intify];
   390 
   391 Goal "z: int ==> $#0 $+ z = z";
   392 by (Asm_simp_tac 1);
   393 qed "zadd_int0";
   394 
   395 Goalw [int_def]
   396      "[| z: int;  w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)";
   397 by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
   398 qed "raw_zminus_zadd_distrib";
   399 
   400 Goal "$- (z $+ w) = $- z $+ $- w";
   401 by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
   402 qed "zminus_zadd_distrib";
   403 
   404 Addsimps [zminus_zadd_distrib];
   405 
   406 Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
   407 by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
   408 qed "raw_zadd_commute";
   409 
   410 Goal "z $+ w = w $+ z";
   411 by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
   412 qed "zadd_commute";
   413 
   414 Goalw [int_def]
   415     "[| z1: int;  z2: int;  z3: int |]   \
   416 \    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
   417 by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
   418 qed "raw_zadd_assoc";
   419 
   420 Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   421 by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
   422 qed "zadd_assoc";
   423 
   424 (*For AC rewriting*)
   425 Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
   426 by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   427 by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
   428 qed "zadd_left_commute";
   429 
   430 (*Integer addition is an AC operator*)
   431 val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   432 
   433 Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
   434 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   435 qed "int_of_add";
   436 
   437 Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
   438 by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
   439 qed "raw_zadd_zminus_inverse";
   440 
   441 Goal "z $+ ($- z) = $#0";
   442 by (simp_tac (simpset() addsimps [zadd_def]) 1);
   443 by (stac (zminus_intify RS sym) 1);
   444 by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
   445 qed "zadd_zminus_inverse";
   446 
   447 Goal "($- z) $+ z = $#0";
   448 by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
   449 qed "zadd_zminus_inverse2";
   450 
   451 Goal "z $+ $#0 = intify(z)";
   452 by (rtac ([zadd_commute, zadd_int0_intify] MRS trans) 1);
   453 qed "zadd_int0_right_intify";
   454 Addsimps [zadd_int0_right_intify];
   455 
   456 Goal "z:int ==> z $+ $#0 = z";
   457 by (Asm_simp_tac 1);
   458 qed "zadd_int0_right";
   459 
   460 Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
   461 
   462 
   463 
   464 (**** zmult: multiplication on int ****)
   465 
   466 (** Congruence property for multiplication **)
   467 
   468 Goal "congruent2(intrel, %p1 p2.                 \
   469 \               split(%x1 y1. split(%x2 y2.     \
   470 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   471 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   472 by Auto_tac;
   473 (*Proof that zmult is congruent in one argument*)
   474 by (rename_tac "x y" 1);
   475 by (forw_inst_tac [("t", "%u. x#*u")] (sym RS subst_context) 1);
   476 by (dres_inst_tac [("t", "%u. y#*u")] subst_context 1);
   477 by (REPEAT (etac add_left_cancel 1));
   478 by (asm_simp_tac (simpset() addsimps [add_mult_distrib_left]) 1);
   479 by Auto_tac;
   480 qed "zmult_congruent2";
   481 
   482 
   483 (*Resolve th against the corresponding facts for zmult*)
   484 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   485 
   486 Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
   487 by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   488                       split_type, add_type, mult_type, 
   489                       quotientI, SigmaI] 1));
   490 qed "raw_zmult_type";
   491 
   492 Goal "z $* w : int";
   493 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
   494 qed "zmult_type";
   495 AddIffs [zmult_type];  AddTCs [zmult_type];
   496 
   497 Goalw [raw_zmult_def]
   498      "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   499 \     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
   500 \         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   501 by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   502 qed "raw_zmult";
   503 
   504 Goalw [zmult_def]
   505      "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
   506 \     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   507 \         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   508 by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
   509 qed "zmult";
   510 
   511 Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
   512 by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   513 qed "raw_zmult_int0";
   514 
   515 Goal "$#0 $* z = $#0";
   516 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int0]) 1);
   517 qed "zmult_int0";
   518 Addsimps [zmult_int0];
   519 
   520 Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
   521 by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
   522 qed "raw_zmult_int1";
   523 
   524 Goal "$#1 $* z = intify(z)";
   525 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int1]) 1);
   526 qed "zmult_int1_intify";
   527 Addsimps [zmult_int1_intify];
   528 
   529 Goal "z : int ==> $#1 $* z = z";
   530 by (Asm_simp_tac 1);
   531 qed "zmult_int1";
   532 
   533 Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
   534 by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
   535 qed "raw_zmult_commute";
   536 
   537 Goal "z $* w = w $* z";
   538 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
   539 qed "zmult_commute";
   540 
   541 Goalw [int_def]
   542      "[| z: int;  w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)";
   543 by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
   544 qed "raw_zmult_zminus";
   545 
   546 Goal "($- z) $* w = $- (z $* w)";
   547 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
   548 by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
   549 by Auto_tac;  
   550 qed "zmult_zminus";
   551 Addsimps [zmult_zminus];
   552 
   553 Goal "($- z) $* ($- w) = (z $* w)";
   554 by (stac zmult_zminus 1);
   555 by (stac zmult_commute 1 THEN stac zmult_zminus 1);
   556 by (simp_tac (simpset() addsimps [zmult_commute])1);
   557 qed "zmult_zminus_zminus";
   558 
   559 Goalw [int_def]
   560     "[| z1: int;  z2: int;  z3: int |]   \
   561 \    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
   562 by (auto_tac (claset(), 
   563   simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
   564 qed "raw_zmult_assoc";
   565 
   566 Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   567 by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
   568                                   raw_zmult_assoc]) 1);
   569 qed "zmult_assoc";
   570 
   571 (*For AC rewriting*)
   572 Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
   573 by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   574 by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
   575 qed "zmult_left_commute";
   576 
   577 (*Integer multiplication is an AC operator*)
   578 val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   579 
   580 Goalw [int_def]
   581     "[| z1: int;  z2: int;  w: int |]  \
   582 \    ==> raw_zmult(raw_zadd(z1,z2), w) = \
   583 \        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
   584 by (auto_tac (claset(), 
   585               simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
   586                                  add_ac @ mult_ac));  
   587 qed "raw_zadd_zmult_distrib";
   588 
   589 Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   590 by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
   591      	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
   592 qed "zadd_zmult_distrib";
   593 
   594 Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
   595 by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
   596                                   zadd_zmult_distrib]) 1);
   597 qed "zadd_zmult_distrib_left";
   598 
   599 val int_typechecks =
   600     [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   601 
   602 
   603 (*** Subtraction laws ***)
   604 
   605 Goal "$#0 $- x = $-x";
   606 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   607 qed "zdiff_int0";
   608 
   609 Goal "x $- $#0 = intify(x)";
   610 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   611 qed "zdiff_int0_right";
   612 
   613 Goal "x $- x = $#0";
   614 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   615 qed "zdiff_self";
   616 
   617 Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
   618 
   619 
   620 Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
   621 by (stac zadd_zmult_distrib 1);
   622 by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
   623 qed "zdiff_zmult_distrib";
   624 
   625 val zmult_commute'= inst "z" "w" zmult_commute;
   626 
   627 Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
   628 by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
   629 qed "zdiff_zmult_distrib2";
   630 
   631 Goal "x $+ (y $- z) = (x $+ y) $- z";
   632 by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   633 qed "zadd_zdiff_eq";
   634 
   635 Goal "(x $- y) $+ z = (x $+ z) $- y";
   636 by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   637 qed "zdiff_zadd_eq";
   638 
   639 
   640 (*** "Less Than" ***)
   641 
   642 (*"Less than" is a linear ordering*)
   643 Goalw [int_def, zless_def, znegative_def, zdiff_def] 
   644      "[| z: int; w: int |] ==> z$<w | z=w | w$<z"; 
   645 by Auto_tac;  
   646 by (asm_full_simp_tac
   647     (simpset() addsimps [zadd, zminus, image_iff, Bex_def]) 1);
   648 by (res_inst_tac [("i", "xb#+ya"), ("j", "xc #+ y")] Ord_linear_lt 1);
   649 by (ALLGOALS (force_tac (claset() addSDs [spec], 
   650                          simpset() addsimps add_ac)));
   651 qed "zless_linear_lemma";
   652 
   653 Goal "z$<w | intify(z)=intify(w) | w$<z"; 
   654 by (cut_inst_tac [("z"," intify(z)"),("w"," intify(w)")] zless_linear_lemma 1);
   655 by Auto_tac;  
   656 qed "zless_linear";
   657 
   658 Goal "~ (z$<z)";
   659 by (auto_tac (claset(), 
   660               simpset() addsimps  [zless_def, znegative_def, int_of_def]));  
   661 by (rotate_tac 2 1);
   662 by Auto_tac;  
   663 qed "zless_not_refl";
   664 AddIffs [zless_not_refl];
   665 
   666 (*This lemma allows direct proofs of other <-properties*)
   667 Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   668     "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
   669 by (auto_tac (claset() addSDs [less_imp_succ_add], 
   670               simpset() addsimps [zadd, zminus, int_of_def]));  
   671 by (res_inst_tac [("x","k")] exI 1);
   672 by (etac add_left_cancel 1);
   673 by Auto_tac;  
   674 qed "zless_imp_succ_zadd_lemma";
   675 
   676 Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
   677 by (subgoal_tac "intify(w) $< intify(z)" 1);
   678 by (dres_inst_tac [("w","intify(w)")] zless_imp_succ_zadd_lemma 1);
   679 by Auto_tac;  
   680 qed "zless_imp_succ_zadd";
   681 
   682 Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   683     "w : int ==> w $< w $+ $# succ(n)";
   684 by (auto_tac (claset(), 
   685               simpset() addsimps [zadd, zminus, int_of_def, image_iff]));  
   686 by (res_inst_tac [("x","0")] exI 1);
   687 by Auto_tac;  
   688 qed "zless_succ_zadd_lemma";
   689 
   690 Goal "w $< w $+ $# succ(n)";
   691 by (cut_facts_tac [intify_in_int RS zless_succ_zadd_lemma] 1);
   692 by Auto_tac;  
   693 qed "zless_succ_zadd";
   694 
   695 Goal "w $< z <-> (EX n. w $+ $#(succ(n)) = intify(z))";
   696 by (rtac iffI 1);
   697 by (etac zless_imp_succ_zadd 1);
   698 by Auto_tac;  
   699 by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
   700 by Auto_tac;  
   701 qed "zless_iff_succ_zadd";
   702 
   703 Goalw [zless_def, znegative_def, zdiff_def, int_def] 
   704     "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"; 
   705 by (auto_tac (claset(), 
   706               simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
   707 by (rename_tac "x1 x2 y1 y2" 1);
   708 by (res_inst_tac [("x","x1#+x2")] exI 1);  
   709 by (res_inst_tac [("x","y1#+y2")] exI 1);  
   710 by (auto_tac (claset(), simpset() addsimps [add_lt_mono]));  
   711 by (rtac sym 1);
   712 by (REPEAT (etac add_left_cancel 1));
   713 by Auto_tac;  
   714 qed "zless_trans_lemma";
   715 
   716 Goal "[| x $< y; y $< z |] ==> x $< z"; 
   717 by (subgoal_tac "intify(x) $< intify(z)" 1);
   718 by (res_inst_tac [("y", "intify(y)")] zless_trans_lemma 2);
   719 by Auto_tac;  
   720 qed "zless_trans";
   721 
   722 
   723 Goalw [zle_def] "z $<= z";
   724 by Auto_tac;  
   725 qed "zle_refl";
   726 
   727 Goalw [zle_def] "[| x $<= y; y $<= x |] ==> x=y";
   728 by (blast_tac (claset() addDs [zless_trans]) 1);
   729 qed "zle_anti_sym";
   730 
   731 Goalw [zle_def] "[| x $<= y; y $<= z |] ==> x $<= z";
   732 by (blast_tac (claset() addIs [zless_trans]) 1);
   733 qed "zle_trans";
   734 
   735 
   736 (*** More subtraction laws (for zcompare_rls): useful? ***)
   737 
   738 Goal "(x $- y) $- z = x $- (y $+ z)";
   739 by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   740 qed "zdiff_zdiff_eq";
   741 
   742 Goal "x $- (y $- z) = (x $+ z) $- y";
   743 by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   744 qed "zdiff_zdiff_eq2";
   745 
   746 Goalw [zless_def, zdiff_def] "(x$-y $< z) <-> (x $< z $+ y)";
   747 by (simp_tac (simpset() addsimps zadd_ac) 1);
   748 qed "zdiff_zless_iff";
   749 
   750 Goalw [zless_def, zdiff_def] "(x $< z$-y) <-> (x $+ y $< z)";
   751 by (simp_tac (simpset() addsimps zadd_ac) 1);
   752 qed "zless_zdiff_iff";
   753 
   754 Goalw [zdiff_def] "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)";
   755 by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   756 qed "zdiff_eq_iff";
   757 
   758 Goalw [zdiff_def] "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)";
   759 by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   760 qed "eq_zdiff_iff";
   761 
   762 (**Could not prove these!
   763 Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
   764 by (asm_simp_tac (simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]) 1);
   765 by Auto_tac;  
   766 qed "zdiff_zle_iff";
   767 
   768 Goalw [zle_def] "(x $<= z$-y) <-> (x $+ y $<= z)";
   769 by (simp_tac (simpset() addsimps [zdiff_zless_iff]) 1);
   770 qed "zle_zdiff_iff";
   771 **)
   772 
   773 
   774 (*** Monotonicity/cancellation results that could allow instantiation
   775      of the CancelNumerals simprocs ***)
   776 
   777 Goal "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)";
   778 by Safe_tac;
   779 by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
   780 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   781 qed "zadd_left_cancel";
   782 
   783 Goal "(z $+ w' = z $+ w) <-> intify(w') = intify(w)";
   784 by (rtac iff_trans 1);
   785 by (rtac zadd_left_cancel 2);
   786 by Auto_tac;  
   787 qed "zadd_left_cancel_intify";
   788 
   789 Addsimps [zadd_left_cancel_intify];
   790 
   791 Goal "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)";
   792 by Safe_tac;
   793 by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
   794 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   795 qed "zadd_right_cancel";
   796 
   797 Goal "(w' $+ z = w $+ z) <-> intify(w') = intify(w)";
   798 by (rtac iff_trans 1);
   799 by (rtac zadd_right_cancel 2);
   800 by Auto_tac;  
   801 qed "zadd_right_cancel_intify";
   802 
   803 Addsimps [zadd_right_cancel_intify];
   804 
   805 
   806 Goal "(w' $+ z $< w $+ z) <-> (w' $< w)";
   807 by (simp_tac (simpset() addsimps [zdiff_zless_iff RS iff_sym]) 1);
   808 by (simp_tac (simpset() addsimps [zdiff_def, zadd_assoc]) 1);
   809 qed "zadd_right_cancel_zless";
   810 
   811 Goal "(z $+ w' $< z $+ w) <-> (w' $< w)";
   812 by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   813                                   zadd_right_cancel_zless]) 1);
   814 qed "zadd_left_cancel_zless";
   815 
   816 Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
   817 
   818 
   819 Goal "(w' $+ z $<= w $+ z) <-> (intify(w') $<= intify(w))";
   820 by (simp_tac (simpset() addsimps [zle_def]) 1);
   821 qed "zadd_right_cancel_zle";
   822 
   823 Goal "(z $+ w' $<= z $+ w) <->  (intify(w') $<= intify(w))";
   824 by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   825                                   zadd_right_cancel_zle]) 1);
   826 qed "zadd_left_cancel_zle";
   827 
   828 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
   829