src/HOL/Arith.ML
author nipkow
Fri Nov 27 17:00:30 1998 +0100 (1998-11-27)
changeset 5983 79e301a6a51b
parent 5771 7c2c8cf20221
child 6055 fdf4638bf726
permissions -rw-r--r--
At last: linear arithmetic for nat!
     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]
   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);
   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: simproc list
   630   val nat_cancel_factor: simproc list
   631   val nat_cancel: simproc list
   632 end;
   633 
   634 structure ArithData: ARITH_DATA =
   635 struct
   636 
   637 
   638 (** abstract syntax of structure nat: 0, Suc, + **)
   639 
   640 (* mk_sum, mk_norm_sum *)
   641 
   642 val one = HOLogic.mk_nat 1;
   643 val mk_plus = HOLogic.mk_binop "op +";
   644 
   645 fun mk_sum [] = HOLogic.zero
   646   | mk_sum [t] = t
   647   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   648 
   649 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   650 fun mk_norm_sum ts =
   651   let val (ones, sums) = partition (equal one) ts in
   652     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   653   end;
   654 
   655 
   656 (* dest_sum *)
   657 
   658 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   659 
   660 fun dest_sum tm =
   661   if HOLogic.is_zero tm then []
   662   else
   663     (case try HOLogic.dest_Suc tm of
   664       Some t => one :: dest_sum t
   665     | None =>
   666         (case try dest_plus tm of
   667           Some (t, u) => dest_sum t @ dest_sum u
   668         | None => [tm]));
   669 
   670 
   671 (** generic proof tools **)
   672 
   673 (* prove conversions *)
   674 
   675 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   676 
   677 fun prove_conv expand_tac norm_tac sg (t, u) =
   678   mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
   679     (K [expand_tac, norm_tac]))
   680   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   681     (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
   682 
   683 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   684   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
   685 
   686 
   687 (* rewriting *)
   688 
   689 fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
   690 
   691 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   692 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
   693 
   694 
   695 
   696 (** cancel common summands **)
   697 
   698 structure Sum =
   699 struct
   700   val mk_sum = mk_norm_sum;
   701   val dest_sum = dest_sum;
   702   val prove_conv = prove_conv;
   703   val norm_tac = simp_all add_rules THEN simp_all add_ac;
   704 end;
   705 
   706 fun gen_uncancel_tac rule ct =
   707   rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
   708 
   709 
   710 (* nat eq *)
   711 
   712 structure EqCancelSums = CancelSumsFun
   713 (struct
   714   open Sum;
   715   val mk_bal = HOLogic.mk_eq;
   716   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   717   val uncancel_tac = gen_uncancel_tac add_left_cancel;
   718 end);
   719 
   720 
   721 (* nat less *)
   722 
   723 structure LessCancelSums = CancelSumsFun
   724 (struct
   725   open Sum;
   726   val mk_bal = HOLogic.mk_binrel "op <";
   727   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   728   val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   729 end);
   730 
   731 
   732 (* nat le *)
   733 
   734 structure LeCancelSums = CancelSumsFun
   735 (struct
   736   open Sum;
   737   val mk_bal = HOLogic.mk_binrel "op <=";
   738   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   739   val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   740 end);
   741 
   742 
   743 (* nat diff *)
   744 
   745 structure DiffCancelSums = CancelSumsFun
   746 (struct
   747   open Sum;
   748   val mk_bal = HOLogic.mk_binop "op -";
   749   val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   750   val uncancel_tac = gen_uncancel_tac diff_cancel;
   751 end);
   752 
   753 
   754 
   755 (** cancel common factor **)
   756 
   757 structure Factor =
   758 struct
   759   val mk_sum = mk_norm_sum;
   760   val dest_sum = dest_sum;
   761   val prove_conv = prove_conv;
   762   val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   763 end;
   764 
   765 fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   766 
   767 fun gen_multiply_tac rule k =
   768   if k > 0 then
   769     rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   770   else no_tac;
   771 
   772 
   773 (* nat eq *)
   774 
   775 structure EqCancelFactor = CancelFactorFun
   776 (struct
   777   open Factor;
   778   val mk_bal = HOLogic.mk_eq;
   779   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   780   val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   781 end);
   782 
   783 
   784 (* nat less *)
   785 
   786 structure LessCancelFactor = CancelFactorFun
   787 (struct
   788   open Factor;
   789   val mk_bal = HOLogic.mk_binrel "op <";
   790   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   791   val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   792 end);
   793 
   794 
   795 (* nat le *)
   796 
   797 structure LeCancelFactor = CancelFactorFun
   798 (struct
   799   open Factor;
   800   val mk_bal = HOLogic.mk_binrel "op <=";
   801   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   802   val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   803 end);
   804 
   805 
   806 
   807 (** prepare nat_cancel simprocs **)
   808 
   809 fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   810 val prep_pats = map prep_pat;
   811 
   812 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   813 
   814 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   815 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   816 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   817 val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
   818 
   819 val nat_cancel_sums = map prep_simproc
   820   [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   821    ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   822    ("natle_cancel_sums", le_pats, LeCancelSums.proc),
   823    ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
   824 
   825 val nat_cancel_factor = map prep_simproc
   826   [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   827    ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   828    ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   829 
   830 val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   831 
   832 
   833 end;
   834 
   835 open ArithData;
   836 
   837 Addsimprocs nat_cancel;
   838 
   839 (*---------------------------------------------------------------------------*)
   840 (* 2. Linear arithmetic                                                      *)
   841 (*---------------------------------------------------------------------------*)
   842 
   843 (* Parameter data for general linear arithmetic functor *)
   844 structure Nat_LA_Data: LIN_ARITH_DATA =
   845 struct
   846 val ccontr = ccontr;
   847 val conjI = conjI;
   848 val lessD = Suc_leI;
   849 val nat_neqE = nat_neqE;
   850 val notI = notI;
   851 val not_leD = not_leE RS Suc_leI;
   852 val not_lessD = leI;
   853 val sym = sym;
   854 
   855 val nat = Type("nat",[]);
   856 
   857 fun nnb T = T = Type("fun",[nat,Type("fun",[nat,Type("bool",[])])])
   858 
   859 (* Turn term into list of summand * multiplicity plus a constant *)
   860 fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
   861   | poly(Const("op +",Type("fun",[Type("nat",[]),_])) $ s $ t, pi) =
   862       poly(s,poly(t,pi))
   863   | poly(t,(p,i)) =
   864       if t = Const("0",nat) then (p,i)
   865       else (case assoc(p,t) of None => ((t,1)::p,i)
   866             | Some m => (overwrite(p,(t,m+1)), i))
   867 
   868 fun decomp2(rel,T,lhs,rhs) =
   869   if not(nnb T) then None else
   870   let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
   871   in case rel of
   872        "op <"  => Some(p,i,"<",q,j)
   873      | "op <=" => Some(p,i,"<=",q,j)
   874      | "op ="  => Some(p,i,"=",q,j)
   875      | _       => None
   876   end;
   877 
   878 fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   879   | negate None = None;
   880 
   881 fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   882   | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   883       negate(decomp2(rel,T,lhs,rhs))
   884   | decomp _ = None
   885 (* reduce contradictory <= to False.
   886    Most of the work is done by the cancel tactics.
   887 *)
   888 val add_rules = [Zero_not_Suc,Suc_not_Zero,le_0_eq];
   889 
   890 val cancel_sums_ss = HOL_basic_ss addsimps add_rules
   891                                   addsimprocs nat_cancel_sums;
   892 
   893 val simp = simplify cancel_sums_ss;
   894 
   895 val add_mono_thms = map (fn s => prove_goal Arith.thy s
   896  (fn prems => [cut_facts_tac prems 1,
   897                blast_tac (claset() addIs [add_le_mono]) 1]))
   898 ["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
   899  "(i = j) & (k <= l) ==> i + k <= j + (l::nat)",
   900  "(i <= j) & (k = l) ==> i + k <= j + (l::nat)",
   901  "(i = j) & (k = l) ==> i + k <= j + (l::nat)"
   902 ];
   903 
   904 end;
   905 
   906 structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
   907 
   908 simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
   909 
   910 (*---------------------------------------------------------------------------*)
   911 (* End of proof procedures. Now go and USE them!                             *)
   912 (*---------------------------------------------------------------------------*)
   913 
   914 
   915 (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   916 
   917 Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
   918 by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
   919 by (Full_simp_tac 1);
   920 by (subgoal_tac "c <= b" 1);
   921 by (blast_tac (claset() addIs [less_imp_le, le_trans]) 2);
   922 by (Asm_simp_tac 1);
   923 qed "diff_less_mono";
   924 
   925 Goal "a+b < (c::nat) ==> a < c-b";
   926 by (dtac diff_less_mono 1);
   927 by (rtac le_add2 1);
   928 by (Asm_full_simp_tac 1);
   929 qed "add_less_imp_less_diff";
   930 
   931 Goal "(i < j-k) = (i+k < (j::nat))";
   932 by (rtac iffI 1);
   933  by (case_tac "k <= j" 1);
   934   by (dtac le_add_diff_inverse2 1);
   935   by (dres_inst_tac [("k","k")] add_less_mono1 1);
   936   by (Asm_full_simp_tac 1);
   937  by (rotate_tac 1 1);
   938  by (Asm_full_simp_tac 1);
   939 by (etac add_less_imp_less_diff 1);
   940 qed "less_diff_conv";
   941 
   942 Goal "(j-k <= (i::nat)) = (j <= i+k)";
   943 by (simp_tac (simpset() addsimps [less_diff_conv, le_def]) 1);
   944 qed "le_diff_conv";
   945 
   946 Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
   947 by (asm_full_simp_tac
   948     (simpset() delsimps [less_Suc_eq_le]
   949                addsimps [less_Suc_eq_le RS sym, less_diff_conv,
   950 			 Suc_diff_le RS sym]) 1);
   951 qed "le_diff_conv2";
   952 
   953 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
   954 by (asm_full_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
   955 qed "Suc_diff_Suc";
   956 
   957 Goal "i <= (n::nat) ==> n - (n - i) = i";
   958 by (etac rev_mp 1);
   959 by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
   960 by (ALLGOALS (asm_simp_tac  (simpset() addsimps [Suc_diff_le])));
   961 qed "diff_diff_cancel";
   962 Addsimps [diff_diff_cancel];
   963 
   964 Goal "k <= (n::nat) ==> m <= n + m - k";
   965 by (etac rev_mp 1);
   966 by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
   967 by (Simp_tac 1);
   968 by (simp_tac (simpset() addsimps [le_add2, less_imp_le]) 1);
   969 by (Simp_tac 1);
   970 qed "le_add_diff";
   971 
   972 Goal "0<k ==> j<i --> j+k-i < k";
   973 by (res_inst_tac [("m","j"),("n","i")] diff_induct 1);
   974 by (ALLGOALS Asm_simp_tac);
   975 qed_spec_mp "add_diff_less";
   976 
   977 
   978 Goal "m-1 < n ==> m <= n";
   979 by (exhaust_tac "m" 1);
   980 by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
   981 qed "pred_less_imp_le";
   982 
   983 Goal "j<=i ==> i - j < Suc i - j";
   984 by (REPEAT (etac rev_mp 1));
   985 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   986 by Auto_tac;
   987 qed "diff_less_Suc_diff";
   988 
   989 Goal "i - j <= Suc i - j";
   990 by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   991 by Auto_tac;
   992 qed "diff_le_Suc_diff";
   993 AddIffs [diff_le_Suc_diff];
   994 
   995 Goal "n - Suc i <= n - i";
   996 by (case_tac "i<n" 1);
   997 by (dtac diff_Suc_less_diff 1);
   998 by (auto_tac (claset(), simpset() addsimps [less_imp_le, leI]));
   999 qed "diff_Suc_le_diff";
  1000 AddIffs [diff_Suc_le_diff];
  1001 
  1002 Goal "0 < n ==> (m <= n-1) = (m<n)";
  1003 by (exhaust_tac "n" 1);
  1004 by (auto_tac (claset(), simpset() addsimps le_simps));
  1005 qed "le_pred_eq";
  1006 
  1007 Goal "0 < n ==> (m-1 < n) = (m<=n)";
  1008 by (exhaust_tac "m" 1);
  1009 by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
  1010 qed "less_pred_eq";
  1011 
  1012 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
  1013 Goal "[| 0<n; ~ m<n |] ==> m - n < m";
  1014 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
  1015 by (Blast_tac 1);
  1016 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  1017 by (ALLGOALS(asm_simp_tac(simpset() addsimps [diff_less_Suc])));
  1018 qed "diff_less";
  1019 
  1020 Goal "[| 0<n; n<=m |] ==> m - n < m";
  1021 by (asm_simp_tac (simpset() addsimps [diff_less, not_less_iff_le]) 1);
  1022 qed "le_diff_less";
  1023 
  1024 
  1025 
  1026 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
  1027 
  1028 (* Monotonicity of subtraction in first argument *)
  1029 Goal "m <= (n::nat) --> (m-l) <= (n-l)";
  1030 by (induct_tac "n" 1);
  1031 by (Simp_tac 1);
  1032 by (simp_tac (simpset() addsimps [le_Suc_eq]) 1);
  1033 by (blast_tac (claset() addIs [diff_le_Suc_diff, le_trans]) 1);
  1034 qed_spec_mp "diff_le_mono";
  1035 
  1036 Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
  1037 by (induct_tac "l" 1);
  1038 by (Simp_tac 1);
  1039 by (case_tac "n <= na" 1);
  1040 by (subgoal_tac "m <= na" 1);
  1041 by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
  1042 by (fast_tac (claset() addEs [le_trans]) 1);
  1043 by (dtac not_leE 1);
  1044 by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
  1045 qed_spec_mp "diff_le_mono2";
  1046 
  1047 
  1048 (*This proof requires natdiff_cancel_sums*)
  1049 Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
  1050 by (induct_tac "l" 1);
  1051 by (Simp_tac 1);
  1052 by (Clarify_tac 1);
  1053 by (etac less_SucE 1);
  1054 by (Clarify_tac 2);
  1055 by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
  1056 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
  1057 				      Suc_diff_le, less_imp_le]) 1);
  1058 qed_spec_mp "diff_less_mono2";
  1059 
  1060 (** Elimination of `-' on nat due to John Harrison **)
  1061 (*This proof requires natle_cancel_sums*)
  1062 
  1063 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
  1064 by(case_tac "a <= b" 1);
  1065 by(Auto_tac);
  1066 by(eres_inst_tac [("x","b-a")] allE 1);
  1067 by(Auto_tac);
  1068 qed "nat_diff_split";
  1069 
  1070 (*
  1071 This is an example of the power of nat_diff_split. Many of the `-' thms in
  1072 Arith.ML could take advantage of this, but would need to be moved.
  1073 *)
  1074 Goal "m-n = 0  -->  n-m = 0  -->  m=n";
  1075 by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
  1076 qed_spec_mp "diffs0_imp_equal";
  1077