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