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