src/HOL/Arith.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 6157 29942d3a1818
child 6394 3d9fd50fcc43
permissions -rw-r--r--
expandshort
     1 (*  Title:      HOL/Arith.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Proofs about elementary arithmetic: addition, multiplication, etc.
     7 Some from the Hoare example from Norbert Galm
     8 *)
     9 
    10 (*** Basic rewrite rules for the arithmetic operators ***)
    11 
    12 
    13 (** Difference **)
    14 
    15 qed_goal "diff_0_eq_0" thy
    16     "0 - n = 0"
    17  (fn _ => [induct_tac "n" 1,  ALLGOALS Asm_simp_tac]);
    18 
    19 (*Must simplify BEFORE the induction!  (Else we get a critical pair)
    20   Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    21 qed_goal "diff_Suc_Suc" thy
    22     "Suc(m) - Suc(n) = m - n"
    23  (fn _ =>
    24   [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
    25 
    26 Addsimps [diff_0_eq_0, diff_Suc_Suc];
    27 
    28 (* Could be (and is, below) generalized in various ways;
    29    However, none of the generalizations are currently in the simpset,
    30    and I dread to think what happens if I put them in *)
    31 Goal "0 < n ==> Suc(n-1) = n";
    32 by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
    33 qed "Suc_pred";
    34 Addsimps [Suc_pred];
    35 
    36 Delsimps [diff_Suc];
    37 
    38 
    39 (**** Inductive properties of the operators ****)
    40 
    41 (*** Addition ***)
    42 
    43 qed_goal "add_0_right" thy "m + 0 = m"
    44  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    45 
    46 qed_goal "add_Suc_right" thy "m + Suc(n) = Suc(m+n)"
    47  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    48 
    49 Addsimps [add_0_right,add_Suc_right];
    50 
    51 (*Associative law for addition*)
    52 qed_goal "add_assoc" thy "(m + n) + k = m + ((n + k)::nat)"
    53  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    54 
    55 (*Commutative law for addition*)  
    56 qed_goal "add_commute" thy "m + n = n + (m::nat)"
    57  (fn _ =>  [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
    58 
    59 qed_goal "add_left_commute" thy "x+(y+z)=y+((x+z)::nat)"
    60  (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
    61            rtac (add_commute RS arg_cong) 1]);
    62 
    63 (*Addition is an AC-operator*)
    64 val add_ac = [add_assoc, add_commute, add_left_commute];
    65 
    66 Goal "(k + m = k + n) = (m=(n::nat))";
    67 by (induct_tac "k" 1);
    68 by (Simp_tac 1);
    69 by (Asm_simp_tac 1);
    70 qed "add_left_cancel";
    71 
    72 Goal "(m + k = n + k) = (m=(n::nat))";
    73 by (induct_tac "k" 1);
    74 by (Simp_tac 1);
    75 by (Asm_simp_tac 1);
    76 qed "add_right_cancel";
    77 
    78 Goal "(k + m <= k + n) = (m<=(n::nat))";
    79 by (induct_tac "k" 1);
    80 by (Simp_tac 1);
    81 by (Asm_simp_tac 1);
    82 qed "add_left_cancel_le";
    83 
    84 Goal "(k + m < k + n) = (m<(n::nat))";
    85 by (induct_tac "k" 1);
    86 by (Simp_tac 1);
    87 by (Asm_simp_tac 1);
    88 qed "add_left_cancel_less";
    89 
    90 Addsimps [add_left_cancel, add_right_cancel,
    91           add_left_cancel_le, add_left_cancel_less];
    92 
    93 (** Reasoning about m+0=0, etc. **)
    94 
    95 Goal "(m+n = 0) = (m=0 & n=0)";
    96 by (exhaust_tac "m" 1);
    97 by (Auto_tac);
    98 qed "add_is_0";
    99 AddIffs [add_is_0];
   100 
   101 Goal "(0 = m+n) = (m=0 & n=0)";
   102 by (exhaust_tac "m" 1);
   103 by (Auto_tac);
   104 qed "zero_is_add";
   105 AddIffs [zero_is_add];
   106 
   107 Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
   108 by (exhaust_tac "m" 1);
   109 by (Auto_tac);
   110 qed "add_is_1";
   111 
   112 Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
   113 by (exhaust_tac "m" 1);
   114 by (Auto_tac);
   115 qed "one_is_add";
   116 
   117 Goal "(0<m+n) = (0<m | 0<n)";
   118 by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
   119 qed "add_gr_0";
   120 AddIffs [add_gr_0];
   121 
   122 (* FIXME: really needed?? *)
   123 Goal "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
   124 by (exhaust_tac "m" 1);
   125 by (ALLGOALS (fast_tac (claset() addss (simpset()))));
   126 qed "pred_add_is_0";
   127 (*Addsimps [pred_add_is_0];*)
   128 
   129 (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
   130 Goal "0<n ==> m + (n-1) = (m+n)-1";
   131 by (exhaust_tac "m" 1);
   132 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
   133                                       addsplits [nat.split])));
   134 qed "add_pred";
   135 Addsimps [add_pred];
   136 
   137 Goal "m + n = m ==> n = 0";
   138 by (dtac (add_0_right RS ssubst) 1);
   139 by (asm_full_simp_tac (simpset() addsimps [add_assoc]
   140                                  delsimps [add_0_right]) 1);
   141 qed "add_eq_self_zero";
   142 
   143 
   144 (**** Additional theorems about "less than" ****)
   145 
   146 (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
   147 Goal "m<n --> (? k. n=Suc(m+k))";
   148 by (induct_tac "n" 1);
   149 by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
   150 by (blast_tac (claset() addSEs [less_SucE] 
   151                         addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
   152 qed_spec_mp "less_eq_Suc_add";
   153 
   154 Goal "n <= ((m + n)::nat)";
   155 by (induct_tac "m" 1);
   156 by (ALLGOALS Simp_tac);
   157 by (etac le_SucI 1);
   158 qed "le_add2";
   159 
   160 Goal "n <= ((n + m)::nat)";
   161 by (simp_tac (simpset() addsimps add_ac) 1);
   162 by (rtac le_add2 1);
   163 qed "le_add1";
   164 
   165 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
   166 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
   167 
   168 Goal "(m<n) = (? k. n=Suc(m+k))";
   169 by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
   170 qed "less_iff_Suc_add";
   171 
   172 
   173 (*"i <= j ==> i <= j+m"*)
   174 bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
   175 
   176 (*"i <= j ==> i <= m+j"*)
   177 bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
   178 
   179 (*"i < j ==> i < j+m"*)
   180 bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
   181 
   182 (*"i < j ==> i < m+j"*)
   183 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
   184 
   185 Goal "i+j < (k::nat) --> i<k";
   186 by (induct_tac "j" 1);
   187 by (ALLGOALS Asm_simp_tac);
   188 by (blast_tac (claset() addDs [Suc_lessD]) 1);
   189 qed_spec_mp "add_lessD1";
   190 
   191 Goal "~ (i+j < (i::nat))";
   192 by (rtac notI 1);
   193 by (etac (add_lessD1 RS less_irrefl) 1);
   194 qed "not_add_less1";
   195 
   196 Goal "~ (j+i < (i::nat))";
   197 by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
   198 qed "not_add_less2";
   199 AddIffs [not_add_less1, not_add_less2];
   200 
   201 Goal "m+k<=n --> m<=(n::nat)";
   202 by (induct_tac "k" 1);
   203 by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
   204 qed_spec_mp "add_leD1";
   205 
   206 Goal "m+k<=n ==> k<=(n::nat)";
   207 by (full_simp_tac (simpset() addsimps [add_commute]) 1);
   208 by (etac add_leD1 1);
   209 qed_spec_mp "add_leD2";
   210 
   211 Goal "m+k<=n ==> m<=n & k<=(n::nat)";
   212 by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
   213 bind_thm ("add_leE", result() RS conjE);
   214 
   215 (*needs !!k for add_ac to work*)
   216 Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
   217 by (force_tac (claset(),
   218 	      simpset() delsimps [add_Suc_right]
   219 	                addsimps [less_iff_Suc_add,
   220 				  add_Suc_right RS sym] @ add_ac) 1);
   221 qed "less_add_eq_less";
   222 
   223 
   224 (*** Monotonicity of Addition ***)
   225 
   226 (*strict, in 1st argument*)
   227 Goal "i < j ==> i + k < j + (k::nat)";
   228 by (induct_tac "k" 1);
   229 by (ALLGOALS Asm_simp_tac);
   230 qed "add_less_mono1";
   231 
   232 (*strict, in both arguments*)
   233 Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
   234 by (rtac (add_less_mono1 RS less_trans) 1);
   235 by (REPEAT (assume_tac 1));
   236 by (induct_tac "j" 1);
   237 by (ALLGOALS Asm_simp_tac);
   238 qed "add_less_mono";
   239 
   240 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
   241 val [lt_mono,le] = Goal
   242      "[| !!i j::nat. i<j ==> f(i) < f(j);       \
   243 \        i <= j                                 \
   244 \     |] ==> f(i) <= (f(j)::nat)";
   245 by (cut_facts_tac [le] 1);
   246 by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
   247 by (blast_tac (claset() addSIs [lt_mono]) 1);
   248 qed "less_mono_imp_le_mono";
   249 
   250 (*non-strict, in 1st argument*)
   251 Goal "i<=j ==> i + k <= j + (k::nat)";
   252 by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
   253 by (etac add_less_mono1 1);
   254 by (assume_tac 1);
   255 qed "add_le_mono1";
   256 
   257 (*non-strict, in both arguments*)
   258 Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
   259 by (etac (add_le_mono1 RS le_trans) 1);
   260 by (simp_tac (simpset() addsimps [add_commute]) 1);
   261 qed "add_le_mono";
   262 
   263 
   264 (*** Multiplication ***)
   265 
   266 (*right annihilation in product*)
   267 qed_goal "mult_0_right" thy "m * 0 = 0"
   268  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   269 
   270 (*right successor law for multiplication*)
   271 qed_goal "mult_Suc_right" thy  "m * Suc(n) = m + (m * n)"
   272  (fn _ => [induct_tac "m" 1,
   273            ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
   274 
   275 Addsimps [mult_0_right, mult_Suc_right];
   276 
   277 Goal "1 * n = n";
   278 by (Asm_simp_tac 1);
   279 qed "mult_1";
   280 
   281 Goal "n * 1 = n";
   282 by (Asm_simp_tac 1);
   283 qed "mult_1_right";
   284 
   285 (*Commutative law for multiplication*)
   286 qed_goal "mult_commute" thy "m * n = n * (m::nat)"
   287  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   288 
   289 (*addition distributes over multiplication*)
   290 qed_goal "add_mult_distrib" thy "(m + n)*k = (m*k) + ((n*k)::nat)"
   291  (fn _ => [induct_tac "m" 1,
   292            ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
   293 
   294 qed_goal "add_mult_distrib2" thy "k*(m + n) = (k*m) + ((k*n)::nat)"
   295  (fn _ => [induct_tac "m" 1,
   296            ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
   297 
   298 (*Associative law for multiplication*)
   299 qed_goal "mult_assoc" thy "(m * n) * k = m * ((n * k)::nat)"
   300   (fn _ => [induct_tac "m" 1, 
   301             ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]);
   302 
   303 qed_goal "mult_left_commute" thy "x*(y*z) = y*((x*z)::nat)"
   304  (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
   305            rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
   306 
   307 val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
   308 
   309 Goal "(m*n = 0) = (m=0 | n=0)";
   310 by (induct_tac "m" 1);
   311 by (induct_tac "n" 2);
   312 by (ALLGOALS Asm_simp_tac);
   313 qed "mult_is_0";
   314 Addsimps [mult_is_0];
   315 
   316 Goal "m <= m*(m::nat)";
   317 by (induct_tac "m" 1);
   318 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
   319 by (etac (le_add2 RSN (2,le_trans)) 1);
   320 qed "le_square";
   321 
   322 
   323 (*** Difference ***)
   324 
   325 
   326 qed_goal "diff_self_eq_0" thy "m - m = 0"
   327  (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
   328 Addsimps [diff_self_eq_0];
   329 
   330 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   331 Goal "~ m<n --> n+(m-n) = (m::nat)";
   332 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   333 by (ALLGOALS Asm_simp_tac);
   334 qed_spec_mp "add_diff_inverse";
   335 
   336 Goal "n<=m ==> n+(m-n) = (m::nat)";
   337 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
   338 qed "le_add_diff_inverse";
   339 
   340 Goal "n<=m ==> (m-n)+n = (m::nat)";
   341 by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
   342 qed "le_add_diff_inverse2";
   343 
   344 Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
   345 
   346 
   347 (*** More results about difference ***)
   348 
   349 Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
   350 by (etac rev_mp 1);
   351 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   352 by (ALLGOALS Asm_simp_tac);
   353 qed "Suc_diff_le";
   354 
   355 Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
   356 by (res_inst_tac [("m","n"),("n","l")] diff_induct 1);
   357 by (ALLGOALS Asm_simp_tac);
   358 qed_spec_mp "Suc_diff_add_le";
   359 
   360 Goal "m - n < Suc(m)";
   361 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   362 by (etac less_SucE 3);
   363 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   364 qed "diff_less_Suc";
   365 
   366 Goal "m - n <= (m::nat)";
   367 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   368 by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
   369 qed "diff_le_self";
   370 Addsimps [diff_le_self];
   371 
   372 (* j<k ==> j-n < k *)
   373 bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
   374 
   375 Goal "!!i::nat. i-j-k = i - (j+k)";
   376 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   377 by (ALLGOALS Asm_simp_tac);
   378 qed "diff_diff_left";
   379 
   380 Goal "(Suc m - n) - Suc k = m - n - k";
   381 by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
   382 qed "Suc_diff_diff";
   383 Addsimps [Suc_diff_diff];
   384 
   385 Goal "0<n ==> n - Suc i < n";
   386 by (exhaust_tac "n" 1);
   387 by Safe_tac;
   388 by (asm_simp_tac (simpset() addsimps le_simps) 1);
   389 qed "diff_Suc_less";
   390 Addsimps [diff_Suc_less];
   391 
   392 Goal "i<n ==> n - Suc i < n - i";
   393 by (exhaust_tac "n" 1);
   394 by (auto_tac (claset(),
   395 	      simpset() addsimps [Suc_diff_le]@le_simps));
   396 qed "diff_Suc_less_diff";
   397 
   398 (*This and the next few suggested by Florian Kammueller*)
   399 Goal "!!i::nat. i-j-k = i-k-j";
   400 by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   401 qed "diff_commute";
   402 
   403 Goal "k<=j --> j<=i --> i - (j - k) = i - j + (k::nat)";
   404 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   405 by (ALLGOALS Asm_simp_tac);
   406 by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
   407 qed_spec_mp "diff_diff_right";
   408 
   409 Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
   410 by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
   411 by (ALLGOALS Asm_simp_tac);
   412 qed_spec_mp "diff_add_assoc";
   413 
   414 Goal "k <= (j::nat) --> (j + i) - k = i + (j - k)";
   415 by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
   416 qed_spec_mp "diff_add_assoc2";
   417 
   418 Goal "(n+m) - n = (m::nat)";
   419 by (induct_tac "n" 1);
   420 by (ALLGOALS Asm_simp_tac);
   421 qed "diff_add_inverse";
   422 Addsimps [diff_add_inverse];
   423 
   424 Goal "(m+n) - n = (m::nat)";
   425 by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
   426 qed "diff_add_inverse2";
   427 Addsimps [diff_add_inverse2];
   428 
   429 Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
   430 by Safe_tac;
   431 by (ALLGOALS Asm_simp_tac);
   432 qed "le_imp_diff_is_add";
   433 
   434 Goal "(m-n = 0) = (m <= n)";
   435 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   436 by (ALLGOALS Asm_simp_tac);
   437 qed "diff_is_0_eq";
   438 Addsimps [diff_is_0_eq RS iffD2];
   439 
   440 Goal "(0<n-m) = (m<n)";
   441 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   442 by (ALLGOALS Asm_simp_tac);
   443 qed "zero_less_diff";
   444 Addsimps [zero_less_diff];
   445 
   446 Goal "i < j  ==> ? k. 0<k & i+k = j";
   447 by (res_inst_tac [("x","j - i")] exI 1);
   448 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
   449 qed "less_imp_add_positive";
   450 
   451 Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   452 by (simp_tac (simpset() addsimps [leI, Suc_le_eq, Suc_diff_le]) 1);
   453 qed "if_Suc_diff_le";
   454 
   455 Goal "Suc(m)-n <= Suc(m-n)";
   456 by (simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
   457 qed "diff_Suc_le_Suc_diff";
   458 
   459 Goal "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
   460 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
   461 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
   462 qed "zero_induct_lemma";
   463 
   464 val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
   465 by (rtac (diff_self_eq_0 RS subst) 1);
   466 by (rtac (zero_induct_lemma RS mp RS mp) 1);
   467 by (REPEAT (ares_tac ([impI,allI]@prems) 1));
   468 qed "zero_induct";
   469 
   470 Goal "(k+m) - (k+n) = m - (n::nat)";
   471 by (induct_tac "k" 1);
   472 by (ALLGOALS Asm_simp_tac);
   473 qed "diff_cancel";
   474 Addsimps [diff_cancel];
   475 
   476 Goal "(m+k) - (n+k) = m - (n::nat)";
   477 val add_commute_k = read_instantiate [("n","k")] add_commute;
   478 by (asm_simp_tac (simpset() addsimps [add_commute_k]) 1);
   479 qed "diff_cancel2";
   480 Addsimps [diff_cancel2];
   481 
   482 (*From Clemens Ballarin, proof by lcp*)
   483 Goal "[| k<=n; n<=m |] ==> (m-k) - (n-k) = m-(n::nat)";
   484 by (REPEAT (etac rev_mp 1));
   485 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   486 by (ALLGOALS Asm_simp_tac);
   487 (*a confluence problem*)
   488 by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
   489 qed "diff_right_cancel";
   490 
   491 Goal "n - (n+m) = 0";
   492 by (induct_tac "n" 1);
   493 by (ALLGOALS Asm_simp_tac);
   494 qed "diff_add_0";
   495 Addsimps [diff_add_0];
   496 
   497 
   498 (** Difference distributes over multiplication **)
   499 
   500 Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
   501 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   502 by (ALLGOALS Asm_simp_tac);
   503 qed "diff_mult_distrib" ;
   504 
   505 Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
   506 val mult_commute_k = read_instantiate [("m","k")] mult_commute;
   507 by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
   508 qed "diff_mult_distrib2" ;
   509 (*NOT added as rewrites, since sometimes they are used from right-to-left*)
   510 
   511 
   512 (*** Monotonicity of Multiplication ***)
   513 
   514 Goal "i <= (j::nat) ==> i*k<=j*k";
   515 by (induct_tac "k" 1);
   516 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   517 qed "mult_le_mono1";
   518 
   519 (*<=monotonicity, BOTH arguments*)
   520 Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
   521 by (etac (mult_le_mono1 RS le_trans) 1);
   522 by (rtac le_trans 1);
   523 by (stac mult_commute 2);
   524 by (etac mult_le_mono1 2);
   525 by (simp_tac (simpset() addsimps [mult_commute]) 1);
   526 qed "mult_le_mono";
   527 
   528 (*strict, in 1st argument; proof is by induction on k>0*)
   529 Goal "[| i<j; 0<k |] ==> k*i < k*j";
   530 by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
   531 by (Asm_simp_tac 1);
   532 by (induct_tac "x" 1);
   533 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
   534 qed "mult_less_mono2";
   535 
   536 Goal "[| i<j; 0<k |] ==> i*k < j*k";
   537 by (dtac mult_less_mono2 1);
   538 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
   539 qed "mult_less_mono1";
   540 
   541 Goal "(0 < m*n) = (0<m & 0<n)";
   542 by (induct_tac "m" 1);
   543 by (induct_tac "n" 2);
   544 by (ALLGOALS Asm_simp_tac);
   545 qed "zero_less_mult_iff";
   546 Addsimps [zero_less_mult_iff];
   547 
   548 Goal "(m*n = 1) = (m=1 & n=1)";
   549 by (induct_tac "m" 1);
   550 by (Simp_tac 1);
   551 by (induct_tac "n" 1);
   552 by (Simp_tac 1);
   553 by (fast_tac (claset() addss simpset()) 1);
   554 qed "mult_eq_1_iff";
   555 Addsimps [mult_eq_1_iff];
   556 
   557 Goal "0<k ==> (m*k < n*k) = (m<n)";
   558 by (safe_tac (claset() addSIs [mult_less_mono1]));
   559 by (cut_facts_tac [less_linear] 1);
   560 by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
   561 qed "mult_less_cancel2";
   562 
   563 Goal "0<k ==> (k*m < k*n) = (m<n)";
   564 by (dtac mult_less_cancel2 1);
   565 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   566 qed "mult_less_cancel1";
   567 Addsimps [mult_less_cancel1, mult_less_cancel2];
   568 
   569 Goal "(Suc k * m < Suc k * n) = (m < n)";
   570 by (rtac mult_less_cancel1 1);
   571 by (Simp_tac 1);
   572 qed "Suc_mult_less_cancel1";
   573 
   574 Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
   575 by (simp_tac (simpset_of HOL.thy) 1);
   576 by (rtac Suc_mult_less_cancel1 1);
   577 qed "Suc_mult_le_cancel1";
   578 
   579 Goal "0<k ==> (m*k = n*k) = (m=n)";
   580 by (cut_facts_tac [less_linear] 1);
   581 by Safe_tac;
   582 by (assume_tac 2);
   583 by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
   584 by (ALLGOALS Asm_full_simp_tac);
   585 qed "mult_cancel2";
   586 
   587 Goal "0<k ==> (k*m = k*n) = (m=n)";
   588 by (dtac mult_cancel2 1);
   589 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   590 qed "mult_cancel1";
   591 Addsimps [mult_cancel1, mult_cancel2];
   592 
   593 Goal "(Suc k * m = Suc k * n) = (m = n)";
   594 by (rtac mult_cancel1 1);
   595 by (Simp_tac 1);
   596 qed "Suc_mult_cancel1";
   597 
   598 
   599 (** Lemma for gcd **)
   600 
   601 Goal "m = m*n ==> n=1 | m=0";
   602 by (dtac sym 1);
   603 by (rtac disjCI 1);
   604 by (rtac nat_less_cases 1 THEN assume_tac 2);
   605 by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
   606 by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
   607 qed "mult_eq_self_implies_10";
   608 
   609 
   610 
   611 
   612 (*---------------------------------------------------------------------------*)
   613 (* Various arithmetic proof procedures                                       *)
   614 (*---------------------------------------------------------------------------*)
   615 
   616 (*---------------------------------------------------------------------------*)
   617 (* 1. Cancellation of common terms                                           *)
   618 (*---------------------------------------------------------------------------*)
   619 
   620 (*  Title:      HOL/arith_data.ML
   621     ID:         $Id$
   622     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
   623 
   624 Setup various arithmetic proof procedures.
   625 *)
   626 
   627 signature ARITH_DATA =
   628 sig
   629   val nat_cancel_sums_add: simproc list
   630   val nat_cancel_sums: simproc list
   631   val nat_cancel_factor: simproc list
   632   val nat_cancel: simproc list
   633 end;
   634 
   635 structure ArithData: ARITH_DATA =
   636 struct
   637 
   638 
   639 (** abstract syntax of structure nat: 0, Suc, + **)
   640 
   641 (* mk_sum, mk_norm_sum *)
   642 
   643 val one = HOLogic.mk_nat 1;
   644 val mk_plus = HOLogic.mk_binop "op +";
   645 
   646 fun mk_sum [] = HOLogic.zero
   647   | mk_sum [t] = t
   648   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   649 
   650 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   651 fun mk_norm_sum ts =
   652   let val (ones, sums) = partition (equal one) ts in
   653     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   654   end;
   655 
   656 
   657 (* dest_sum *)
   658 
   659 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   660 
   661 fun dest_sum tm =
   662   if HOLogic.is_zero tm then []
   663   else
   664     (case try HOLogic.dest_Suc tm of
   665       Some t => one :: dest_sum t
   666     | None =>
   667         (case try dest_plus tm of
   668           Some (t, u) => dest_sum t @ dest_sum u
   669         | None => [tm]));
   670 
   671 
   672 (** generic proof tools **)
   673 
   674 (* prove conversions *)
   675 
   676 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   677 
   678 fun prove_conv expand_tac norm_tac sg (t, u) =
   679   mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
   680     (K [expand_tac, norm_tac]))
   681   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   682     (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
   683 
   684 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   685   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
   686 
   687 
   688 (* rewriting *)
   689 
   690 fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
   691 
   692 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   693 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
   694 
   695 
   696 
   697 (** cancel common summands **)
   698 
   699 structure Sum =
   700 struct
   701   val mk_sum = mk_norm_sum;
   702   val dest_sum = dest_sum;
   703   val prove_conv = prove_conv;
   704   val norm_tac = simp_all add_rules THEN simp_all add_ac;
   705 end;
   706 
   707 fun gen_uncancel_tac rule ct =
   708   rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
   709 
   710 
   711 (* nat eq *)
   712 
   713 structure EqCancelSums = CancelSumsFun
   714 (struct
   715   open Sum;
   716   val mk_bal = HOLogic.mk_eq;
   717   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   718   val uncancel_tac = gen_uncancel_tac add_left_cancel;
   719 end);
   720 
   721 
   722 (* nat less *)
   723 
   724 structure LessCancelSums = CancelSumsFun
   725 (struct
   726   open Sum;
   727   val mk_bal = HOLogic.mk_binrel "op <";
   728   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   729   val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   730 end);
   731 
   732 
   733 (* nat le *)
   734 
   735 structure LeCancelSums = CancelSumsFun
   736 (struct
   737   open Sum;
   738   val mk_bal = HOLogic.mk_binrel "op <=";
   739   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   740   val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   741 end);
   742 
   743 
   744 (* nat diff *)
   745 
   746 structure DiffCancelSums = CancelSumsFun
   747 (struct
   748   open Sum;
   749   val mk_bal = HOLogic.mk_binop "op -";
   750   val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   751   val uncancel_tac = gen_uncancel_tac diff_cancel;
   752 end);
   753 
   754 
   755 
   756 (** cancel common factor **)
   757 
   758 structure Factor =
   759 struct
   760   val mk_sum = mk_norm_sum;
   761   val dest_sum = dest_sum;
   762   val prove_conv = prove_conv;
   763   val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   764 end;
   765 
   766 fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   767 
   768 fun gen_multiply_tac rule k =
   769   if k > 0 then
   770     rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   771   else no_tac;
   772 
   773 
   774 (* nat eq *)
   775 
   776 structure EqCancelFactor = CancelFactorFun
   777 (struct
   778   open Factor;
   779   val mk_bal = HOLogic.mk_eq;
   780   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   781   val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   782 end);
   783 
   784 
   785 (* nat less *)
   786 
   787 structure LessCancelFactor = CancelFactorFun
   788 (struct
   789   open Factor;
   790   val mk_bal = HOLogic.mk_binrel "op <";
   791   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   792   val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   793 end);
   794 
   795 
   796 (* nat le *)
   797 
   798 structure LeCancelFactor = CancelFactorFun
   799 (struct
   800   open Factor;
   801   val mk_bal = HOLogic.mk_binrel "op <=";
   802   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   803   val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   804 end);
   805 
   806 
   807 
   808 (** prepare nat_cancel simprocs **)
   809 
   810 fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   811 val prep_pats = map prep_pat;
   812 
   813 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   814 
   815 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   816 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   817 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   818 val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
   819 
   820 val nat_cancel_sums_add = map prep_simproc
   821   [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   822    ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   823    ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
   824 
   825 val nat_cancel_sums = nat_cancel_sums_add @
   826   [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
   827 
   828 val nat_cancel_factor = map prep_simproc
   829   [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   830    ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   831    ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   832 
   833 val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   834 
   835 
   836 end;
   837 
   838 open ArithData;
   839 
   840 Addsimprocs nat_cancel;
   841 
   842 (*---------------------------------------------------------------------------*)
   843 (* 2. Linear arithmetic                                                      *)
   844 (*---------------------------------------------------------------------------*)
   845 
   846 (* Parameters data for general linear arithmetic functor *)
   847 
   848 structure LA_Logic: LIN_ARITH_LOGIC =
   849 struct
   850 val ccontr = ccontr;
   851 val conjI = conjI;
   852 val neqE = linorder_neqE;
   853 val notI = notI;
   854 val sym = sym;
   855 val not_lessD = linorder_not_less RS iffD1;
   856 val not_leD = linorder_not_le RS iffD1;
   857 
   858 
   859 fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI);
   860 
   861 val mk_Trueprop = HOLogic.mk_Trueprop;
   862 
   863 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
   864   | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
   865 
   866 fun is_False thm =
   867   let val _ $ t = #prop(rep_thm thm)
   868   in t = Const("False",HOLogic.boolT) end;
   869 
   870 fun is_nat(t) = fastype_of1 t = HOLogic.natT;
   871 
   872 fun mk_nat_thm sg t =
   873   let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   874   in instantiate ([],[(cn,ct)]) le0 end;
   875 
   876 end;
   877 
   878 structure Nat_LA_Data (* : LIN_ARITH_DATA *) =
   879 struct
   880 
   881 val lessD = [Suc_leI];
   882 
   883 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   884 
   885 (* Turn term into list of summand * multiplicity plus a constant *)
   886 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
   887   | poly(Const("op +",_) $ s $ t, pi) = poly(s,poly(t,pi))
   888   | poly(t,(p,i)) =
   889       if t = Const("0",HOLogic.natT) then (p,i)
   890       else (case assoc(p,t) of None => ((t,1)::p,i)
   891             | Some m => (overwrite(p,(t,m+1)), i))
   892 fun poly(t, pi as (p,i)) =
   893   if HOLogic.is_zero t then pi else
   894   (case try HOLogic.dest_Suc t of
   895     Some u => poly(u, (p,i+1))
   896   | None => (case try dest_plus t of
   897                Some(r,s) => poly(r,poly(s,pi))
   898              | None => (case assoc(p,t) of None => ((t,1)::p,i)
   899                         | Some m => (overwrite(p,(t,m+1)), i))))
   900 
   901 fun nnb T = T = ([HOLogic.natT,HOLogic.natT] ---> HOLogic.boolT);
   902 
   903 fun decomp2(rel,lhs,rhs) =
   904   let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
   905   in case rel of
   906        "op <"  => Some(p,i,"<",q,j)
   907      | "op <=" => Some(p,i,"<=",q,j)
   908      | "op ="  => Some(p,i,"=",q,j)
   909      | _       => None
   910   end;
   911 
   912 fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   913   | negate None = None;
   914 
   915 fun decomp1(T,xxx) = if nnb T then decomp2 xxx else None;
   916 
   917 fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
   918   | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   919       negate(decomp1(T,(rel,lhs,rhs)))
   920   | decomp _ = None
   921 
   922 (* reduce contradictory <= to False.
   923    Most of the work is done by the cancel tactics.
   924 *)
   925 val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
   926 
   927 val cancel_sums_ss = HOL_basic_ss addsimps add_rules
   928                                   addsimprocs nat_cancel_sums_add;
   929 
   930 val simp = simplify cancel_sums_ss;
   931 
   932 val add_mono_thms = map (fn s => prove_goal Arith.thy s
   933  (fn prems => [cut_facts_tac prems 1,
   934                blast_tac (claset() addIs [add_le_mono]) 1]))
   935 ["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
   936  "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
   937  "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
   938  "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
   939 ];
   940 
   941 end;
   942 
   943 structure LA_Data_Ref =
   944 struct
   945   val add_mono_thms = ref Nat_LA_Data.add_mono_thms
   946   val lessD = ref Nat_LA_Data.lessD
   947   val decomp = ref Nat_LA_Data.decomp
   948   val simp = ref Nat_LA_Data.simp
   949 end;
   950 
   951 structure Fast_Arith =
   952   Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
   953 
   954 val fast_arith_tac = Fast_Arith.lin_arith_tac;
   955 
   956 val nat_arith_simproc_pats =
   957   map (fn s => Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT))
   958       ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
   959 
   960 val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
   961                                         Fast_Arith.lin_arith_prover;
   962 
   963 Addsimprocs [fast_nat_arith_simproc];
   964 
   965 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   966 useful to detect inconsistencies among the premises for subgoals which are
   967 *not* themselves (in)equalities, because the latter activate
   968 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   969 solver all the time rather than add the additional check. *)
   970 
   971 simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
   972 
   973 (* Elimination of `-' on nat due to John Harrison *)
   974 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
   975 by (case_tac "a <= b" 1);
   976 by (Auto_tac);
   977 by (eres_inst_tac [("x","b-a")] allE 1);
   978 by (Auto_tac);
   979 qed "nat_diff_split";
   980 
   981 (* FIXME: K true should be replaced by a sensible test to speed things up
   982    in case there are lots of irrelevant terms involved;
   983    elimination of min/max can be optimized:
   984    (max m n + k <= r) = (m+k <= r & n+k <= r)
   985    (l <= min m n + k) = (l <= m+k & l <= n+k)
   986 *)
   987 val arith_tac =
   988   refute_tac (K true) (REPEAT o split_tac[nat_diff_split,split_min,split_max])
   989              ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
   990 
   991 (*---------------------------------------------------------------------------*)
   992 (* End of proof procedures. Now go and USE them!                             *)
   993 (*---------------------------------------------------------------------------*)
   994 
   995 (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   996 
   997 Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
   998 by (arith_tac 1);
   999 qed "diff_less_mono";
  1000 
  1001 Goal "a+b < (c::nat) ==> a < c-b";
  1002 by (arith_tac 1);
  1003 qed "add_less_imp_less_diff";
  1004 
  1005 Goal "(i < j-k) = (i+k < (j::nat))";
  1006 by (arith_tac 1);
  1007 qed "less_diff_conv";
  1008 
  1009 Goal "(j-k <= (i::nat)) = (j <= i+k)";
  1010 by (arith_tac 1);
  1011 qed "le_diff_conv";
  1012 
  1013 Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
  1014 by (arith_tac 1);
  1015 qed "le_diff_conv2";
  1016 
  1017 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
  1018 by (arith_tac 1);
  1019 qed "Suc_diff_Suc";
  1020 
  1021 Goal "i <= (n::nat) ==> n - (n - i) = i";
  1022 by (arith_tac 1);
  1023 qed "diff_diff_cancel";
  1024 Addsimps [diff_diff_cancel];
  1025 
  1026 Goal "k <= (n::nat) ==> m <= n + m - k";
  1027 by (arith_tac 1);
  1028 qed "le_add_diff";
  1029 
  1030 Goal "[| 0<k; j<i |] ==> j+k-i < k";
  1031 by (arith_tac 1);
  1032 qed "add_diff_less";
  1033 
  1034 Goal "m-1 < n ==> m <= n";
  1035 by (arith_tac 1);
  1036 qed "pred_less_imp_le";
  1037 
  1038 Goal "j<=i ==> i - j < Suc i - j";
  1039 by (arith_tac 1);
  1040 qed "diff_less_Suc_diff";
  1041 
  1042 Goal "i - j <= Suc i - j";
  1043 by (arith_tac 1);
  1044 qed "diff_le_Suc_diff";
  1045 AddIffs [diff_le_Suc_diff];
  1046 
  1047 Goal "n - Suc i <= n - i";
  1048 by (arith_tac 1);
  1049 qed "diff_Suc_le_diff";
  1050 AddIffs [diff_Suc_le_diff];
  1051 
  1052 Goal "0 < n ==> (m <= n-1) = (m<n)";
  1053 by (arith_tac 1);
  1054 qed "le_pred_eq";
  1055 
  1056 Goal "0 < n ==> (m-1 < n) = (m<=n)";
  1057 by (arith_tac 1);
  1058 qed "less_pred_eq";
  1059 
  1060 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
  1061 Goal "[| 0<n; ~ m<n |] ==> m - n < m";
  1062 by (arith_tac 1);
  1063 qed "diff_less";
  1064 
  1065 Goal "[| 0<n; n<=m |] ==> m - n < m";
  1066 by (arith_tac 1);
  1067 qed "le_diff_less";
  1068 
  1069 
  1070 
  1071 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
  1072 
  1073 (* Monotonicity of subtraction in first argument *)
  1074 Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
  1075 by (arith_tac 1);
  1076 qed "diff_le_mono";
  1077 
  1078 Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
  1079 by (arith_tac 1);
  1080 qed "diff_le_mono2";
  1081 
  1082 
  1083 (*This proof requires natdiff_cancel_sums*)
  1084 Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
  1085 by (arith_tac 1);
  1086 qed "diff_less_mono2";
  1087 
  1088 Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
  1089 by (arith_tac 1);
  1090 qed "diffs0_imp_equal";