# HG changeset patch
# User wenzelm
# Date 964476406 -7200
# Node ID 62bb04ab4b01edf6945feacae0747e8a0b544abc
# Parent  c3a13a7d442435d3f1a81150e070558588c66111
rearranged setup of arithmetic procedures, avoiding global reference values;

diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Arith.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -3,1030 +3,13 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Proofs about elementary arithmetic: addition, multiplication, etc.
-Some from the Hoare example from Norbert Galm
+Further proofs about elementary arithmetic, using the arithmetic proof
+procedures.
 *)
 
-(*** Basic rewrite rules for the arithmetic operators ***)
-
-
-(** Difference **)
-
-Goal "0 - n = (0::nat)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_0_eq_0";
-
-(*Must simplify BEFORE the induction!  (Else we get a critical pair)
-  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
-Goal "Suc(m) - Suc(n) = m - n";
-by (Simp_tac 1);
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_Suc_Suc";
-
-Addsimps [diff_0_eq_0, diff_Suc_Suc];
-
-(* Could be (and is, below) generalized in various ways;
-   However, none of the generalizations are currently in the simpset,
-   and I dread to think what happens if I put them in *)
-Goal "0 < n ==> Suc(n-1) = n";
-by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
-qed "Suc_pred";
-Addsimps [Suc_pred];
-
-Delsimps [diff_Suc];
-
-
-(**** Inductive properties of the operators ****)
-
-(*** Addition ***)
-
-Goal "m + 0 = (m::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_0_right";
-
-Goal "m + Suc(n) = Suc(m+n)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_Suc_right";
-
-Addsimps [add_0_right,add_Suc_right];
-
-
-(*Associative law for addition*)
-Goal "(m + n) + k = m + ((n + k)::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_assoc";
-
-(*Commutative law for addition*)  
-Goal "m + n = n + (m::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_commute";
-
-Goal "x+(y+z)=y+((x+z)::nat)";
-by (rtac (add_commute RS trans) 1);
-by (rtac (add_assoc RS trans) 1);
-by (rtac (add_commute RS arg_cong) 1);
-qed "add_left_commute";
-
-(*Addition is an AC-operator*)
-bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
-
-Goal "(k + m = k + n) = (m=(n::nat))";
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_left_cancel";
-
-Goal "(m + k = n + k) = (m=(n::nat))";
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_right_cancel";
-
-Goal "(k + m <= k + n) = (m<=(n::nat))";
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_left_cancel_le";
-
-Goal "(k + m < k + n) = (m<(n::nat))";
-by (induct_tac "k" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_left_cancel_less";
-
-Addsimps [add_left_cancel, add_right_cancel,
-          add_left_cancel_le, add_left_cancel_less];
-
-(** Reasoning about m+0=0, etc. **)
-
-Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
-by (case_tac "m" 1);
-by (Auto_tac);
-qed "add_is_0";
-AddIffs [add_is_0];
-
-Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
-by (case_tac "m" 1);
-by (Auto_tac);
-qed "zero_is_add";
-AddIffs [zero_is_add];
-
-Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
-by (case_tac "m" 1);
-by (Auto_tac);
-qed "add_is_1";
-
-Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
-by (case_tac "m" 1);
-by (Auto_tac);
-qed "one_is_add";
-
-Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
-by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
-qed "add_gr_0";
-AddIffs [add_gr_0];
-
-(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
-Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
-by (case_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
-                                      addsplits [nat.split])));
-qed "add_pred";
-Addsimps [add_pred];
-
-Goal "!!m::nat. m + n = m ==> n = 0";
-by (dtac (add_0_right RS ssubst) 1);
-by (asm_full_simp_tac (simpset() addsimps [add_assoc]
-                                 delsimps [add_0_right]) 1);
-qed "add_eq_self_zero";
-
-
-(**** Additional theorems about "less than" ****)
-
-(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
-Goal "m<n --> (EX k. n=Suc(m+k))";
-by (induct_tac "n" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
-by (blast_tac (claset() addSEs [less_SucE] 
-                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
-qed_spec_mp "less_eq_Suc_add";
-
-Goal "n <= ((m + n)::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS Simp_tac);
-by (etac le_SucI 1);
-qed "le_add2";
-
-Goal "n <= ((n + m)::nat)";
-by (simp_tac (simpset() addsimps add_ac) 1);
-by (rtac le_add2 1);
-qed "le_add1";
-
-bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
-bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
-
-Goal "(m<n) = (EX k. n=Suc(m+k))";
-by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
-qed "less_iff_Suc_add";
-
-
-(*"i <= j ==> i <= j+m"*)
-bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
-
-(*"i <= j ==> i <= m+j"*)
-bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
-
-(*"i < j ==> i < j+m"*)
-bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
-
-(*"i < j ==> i < m+j"*)
-bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
-
-Goal "i+j < (k::nat) --> i<k";
-by (induct_tac "j" 1);
-by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addDs [Suc_lessD]) 1);
-qed_spec_mp "add_lessD1";
-
-Goal "~ (i+j < (i::nat))";
-by (rtac notI 1);
-by (etac (add_lessD1 RS less_irrefl) 1);
-qed "not_add_less1";
-
-Goal "~ (j+i < (i::nat))";
-by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
-qed "not_add_less2";
-AddIffs [not_add_less1, not_add_less2];
-
-Goal "m+k<=n --> m<=(n::nat)";
-by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
-qed_spec_mp "add_leD1";
-
-Goal "m+k<=n ==> k<=(n::nat)";
-by (full_simp_tac (simpset() addsimps [add_commute]) 1);
-by (etac add_leD1 1);
-qed_spec_mp "add_leD2";
-
-Goal "m+k<=n ==> m<=n & k<=(n::nat)";
-by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
-bind_thm ("add_leE", result() RS conjE);
-
-(*needs !!k for add_ac to work*)
-Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
-by (force_tac (claset(),
-	      simpset() delsimps [add_Suc_right]
-	                addsimps [less_iff_Suc_add,
-				  add_Suc_right RS sym] @ add_ac) 1);
-qed "less_add_eq_less";
-
-
-(*** Monotonicity of Addition ***)
-
-(*strict, in 1st argument*)
-Goal "i < j ==> i + k < j + (k::nat)";
-by (induct_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_less_mono1";
-
-(*strict, in both arguments*)
-Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
-by (rtac (add_less_mono1 RS less_trans) 1);
-by (REPEAT (assume_tac 1));
-by (induct_tac "j" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_less_mono";
-
-(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
-val [lt_mono,le] = Goal
-     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
-\        i <= j                                 \
-\     |] ==> f(i) <= (f(j)::nat)";
-by (cut_facts_tac [le] 1);
-by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
-by (blast_tac (claset() addSIs [lt_mono]) 1);
-qed "less_mono_imp_le_mono";
-
-(*non-strict, in 1st argument*)
-Goal "i<=j ==> i + k <= j + (k::nat)";
-by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
-by (etac add_less_mono1 1);
-by (assume_tac 1);
-qed "add_le_mono1";
-
-(*non-strict, in both arguments*)
-Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
-by (etac (add_le_mono1 RS le_trans) 1);
-by (simp_tac (simpset() addsimps [add_commute]) 1);
-qed "add_le_mono";
-
-
-(*** Multiplication ***)
-
-(*right annihilation in product*)
-Goal "!!m::nat. m * 0 = 0";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mult_0_right";
-
-(*right successor law for multiplication*)
-Goal  "m * Suc(n) = m + (m * n)";
-by (induct_tac "m" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
-qed "mult_Suc_right";
-
-Addsimps [mult_0_right, mult_Suc_right];
-
-Goal "1 * n = n";
-by (Asm_simp_tac 1);
-qed "mult_1";
-
-Goal "n * 1 = n";
-by (Asm_simp_tac 1);
-qed "mult_1_right";
-
-(*Commutative law for multiplication*)
-Goal "m * n = n * (m::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "mult_commute";
-
-(*addition distributes over multiplication*)
-Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
-qed "add_mult_distrib";
-
-Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
-qed "add_mult_distrib2";
-
-(*Associative law for multiplication*)
-Goal "(m * n) * k = m * ((n * k)::nat)";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
-qed "mult_assoc";
-
-Goal "x*(y*z) = y*((x*z)::nat)";
-by (rtac trans 1);
-by (rtac mult_commute 1);
-by (rtac trans 1);
-by (rtac mult_assoc 1);
-by (rtac (mult_commute RS arg_cong) 1);
-qed "mult_left_commute";
-
-bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
-
-Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
-by (induct_tac "m" 1);
-by (induct_tac "n" 2);
-by (ALLGOALS Asm_simp_tac);
-qed "mult_is_0";
-
-Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
-by (stac eq_commute 1 THEN stac mult_is_0 1);
-by Auto_tac;
-qed "zero_is_mult";
-
-Addsimps [mult_is_0, zero_is_mult];
-
-
-(*** Difference ***)
-
-Goal "!!m::nat. m - m = 0";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_self_eq_0";
-
-Addsimps [diff_self_eq_0];
-
-(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-Goal "~ m<n --> n+(m-n) = (m::nat)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "add_diff_inverse";
-
-Goal "n<=m ==> n+(m-n) = (m::nat)";
-by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
-qed "le_add_diff_inverse";
-
-Goal "n<=m ==> (m-n)+n = (m::nat)";
-by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
-qed "le_add_diff_inverse2";
-
-Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
-
-
-(*** More results about difference ***)
-
-Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
-by (etac rev_mp 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Suc_diff_le";
-
-Goal "m - n < Suc(m)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (etac less_SucE 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
-qed "diff_less_Suc";
-
-Goal "m - n <= (m::nat)";
-by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
-qed "diff_le_self";
-Addsimps [diff_le_self];
-
-(* j<k ==> j-n < k *)
-bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
-
-Goal "!!i::nat. i-j-k = i - (j+k)";
-by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_diff_left";
-
-Goal "(Suc m - n) - Suc k = m - n - k";
-by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
-qed "Suc_diff_diff";
-Addsimps [Suc_diff_diff];
-
-Goal "0<n ==> n - Suc i < n";
-by (case_tac "n" 1);
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps le_simps) 1);
-qed "diff_Suc_less";
-Addsimps [diff_Suc_less];
-
-(*This and the next few suggested by Florian Kammueller*)
-Goal "!!i::nat. i-j-k = i-k-j";
-by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
-qed "diff_commute";
-
-Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
-by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "diff_add_assoc";
-
-Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
-by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
-qed_spec_mp "diff_add_assoc2";
-
-Goal "(n+m) - n = (m::nat)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_add_inverse";
-
-Goal "(m+n) - n = (m::nat)";
-by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
-qed "diff_add_inverse2";
-
-Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
-by Safe_tac;
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
-qed "le_imp_diff_is_add";
-
-Goal "!!m::nat. (m-n = 0) = (m <= n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_is_0_eq";
-
-Goal "!!m::nat. (0 = m-n) = (m <= n)";
-by (stac (diff_is_0_eq RS sym) 1);
-by (rtac eq_sym_conv 1);
-qed "zero_is_diff_eq";
-Addsimps [diff_is_0_eq, zero_is_diff_eq];
-
-Goal "!!m::nat. (0<n-m) = (m<n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_diff";
-Addsimps [zero_less_diff];
-
-Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
-by (res_inst_tac [("x","j - i")] exI 1);
-by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
-qed "less_imp_add_positive";
-
-Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
-by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
-qed "zero_induct_lemma";
-
-val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
-by (rtac (diff_self_eq_0 RS subst) 1);
-by (rtac (zero_induct_lemma RS mp RS mp) 1);
-by (REPEAT (ares_tac ([impI,allI]@prems) 1));
-qed "zero_induct";
-
-Goal "(k+m) - (k+n) = m - (n::nat)";
-by (induct_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_cancel";
-
-Goal "(m+k) - (n+k) = m - (n::nat)";
-by (asm_simp_tac
-    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
-qed "diff_cancel2";
-
-Goal "n - (n+m) = (0::nat)";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_add_0";
-
-
-(** Difference distributes over multiplication **)
-
-Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
-qed "diff_mult_distrib" ;
-
-Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
-val mult_commute_k = read_instantiate [("m","k")] mult_commute;
-by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
-qed "diff_mult_distrib2" ;
-(*NOT added as rewrites, since sometimes they are used from right-to-left*)
-
-
-(*** Monotonicity of Multiplication ***)
-
-Goal "i <= (j::nat) ==> i*k<=j*k";
-by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
-qed "mult_le_mono1";
-
-Goal "i <= (j::nat) ==> k*i <= k*j";
-by (dtac mult_le_mono1 1);
-by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
-qed "mult_le_mono2";
-
-(* <= monotonicity, BOTH arguments*)
-Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
-by (etac (mult_le_mono1 RS le_trans) 1);
-by (etac mult_le_mono2 1);
-qed "mult_le_mono";
+(*legacy ...*)
+structure Arith = struct val thy = the_context () end;
 
-(*strict, in 1st argument; proof is by induction on k>0*)
-Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
-by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
-by (Asm_simp_tac 1);
-by (induct_tac "x" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
-qed "mult_less_mono2";
-
-Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
-by (dtac mult_less_mono2 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
-qed "mult_less_mono1";
-
-Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
-by (induct_tac "m" 1);
-by (case_tac "n" 2);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_mult_iff";
-Addsimps [zero_less_mult_iff];
-
-Goal "(1 <= m*n) = (1<=m & 1<=n)";
-by (induct_tac "m" 1);
-by (case_tac "n" 2);
-by (ALLGOALS Asm_simp_tac);
-qed "one_le_mult_iff";
-Addsimps [one_le_mult_iff];
-
-Goal "(m*n = 1) = (m=1 & n=1)";
-by (induct_tac "m" 1);
-by (Simp_tac 1);
-by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (fast_tac (claset() addss simpset()) 1);
-qed "mult_eq_1_iff";
-Addsimps [mult_eq_1_iff];
-
-Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
-by (safe_tac (claset() addSIs [mult_less_mono1]));
-by (cut_facts_tac [less_linear] 1);
-by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
-qed "mult_less_cancel2";
-
-Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
-by (dtac mult_less_cancel2 1);
-by (etac subst 1);
-by (simp_tac (simpset() addsimps [mult_commute]) 1);
-qed "mult_less_cancel1";
-Addsimps [mult_less_cancel1, mult_less_cancel2];
-
-Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "mult_le_cancel2";
-
-Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-qed "mult_le_cancel1";
-Addsimps [mult_le_cancel1, mult_le_cancel2];
-
-Goal "(Suc k * m < Suc k * n) = (m < n)";
-by (rtac mult_less_cancel1 1);
-by (Simp_tac 1);
-qed "Suc_mult_less_cancel1";
-
-Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
-by (simp_tac (simpset_of HOL.thy) 1);
-by (rtac Suc_mult_less_cancel1 1);
-qed "Suc_mult_le_cancel1";
-
-Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
-by (cut_facts_tac [less_linear] 1);
-by Safe_tac;
-by (assume_tac 2);
-by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
-by (ALLGOALS Asm_full_simp_tac);
-qed "mult_cancel2";
-
-Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
-by (dtac mult_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
-qed "mult_cancel1";
-Addsimps [mult_cancel1, mult_cancel2];
-
-Goal "(Suc k * m = Suc k * n) = (m = n)";
-by (rtac mult_cancel1 1);
-by (Simp_tac 1);
-qed "Suc_mult_cancel1";
-
-
-(*Lemma for gcd*)
-Goal "!!m::nat. m = m*n ==> n=1 | m=0";
-by (dtac sym 1);
-by (rtac disjCI 1);
-by (rtac nat_less_cases 1 THEN assume_tac 2);
-by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
-by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
-qed "mult_eq_self_implies_10";
-
-
-
-
-(*---------------------------------------------------------------------------*)
-(* Various arithmetic proof procedures                                       *)
-(*---------------------------------------------------------------------------*)
-
-(*---------------------------------------------------------------------------*)
-(* 1. Cancellation of common terms                                           *)
-(*---------------------------------------------------------------------------*)
-
-(*  Title:      HOL/arith_data.ML
-    ID:         $Id$
-    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
-
-Setup various arithmetic proof procedures.
-*)
-
-signature ARITH_DATA =
-sig
-  val nat_cancel_sums_add: simproc list
-  val nat_cancel_sums: simproc list
-  val nat_cancel_factor: simproc list
-  val nat_cancel: simproc list
-end;
-
-structure ArithData: ARITH_DATA =
-struct
-
-
-(** abstract syntax of structure nat: 0, Suc, + **)
-
-(* mk_sum, mk_norm_sum *)
-
-val one = HOLogic.mk_nat 1;
-val mk_plus = HOLogic.mk_binop "op +";
-
-fun mk_sum [] = HOLogic.zero
-  | mk_sum [t] = t
-  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
-fun mk_norm_sum ts =
-  let val (ones, sums) = partition (equal one) ts in
-    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
-  end;
-
-
-(* dest_sum *)
-
-val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
-
-fun dest_sum tm =
-  if HOLogic.is_zero tm then []
-  else
-    (case try HOLogic.dest_Suc tm of
-      Some t => one :: dest_sum t
-    | None =>
-        (case try dest_plus tm of
-          Some (t, u) => dest_sum t @ dest_sum u
-        | None => [tm]));
-
-
-(** generic proof tools **)
-
-(* prove conversions *)
-
-val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
-
-fun prove_conv expand_tac norm_tac sg (t, u) =
-  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
-    (K [expand_tac, norm_tac]))
-  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
-    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
-
-val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
-  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
-
-
-(* rewriting *)
-
-fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
-
-val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
-val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
-
-
-
-(** cancel common summands **)
-
-structure Sum =
-struct
-  val mk_sum = mk_norm_sum;
-  val dest_sum = dest_sum;
-  val prove_conv = prove_conv;
-  val norm_tac = simp_all add_rules THEN simp_all add_ac;
-end;
-
-fun gen_uncancel_tac rule ct =
-  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
-
-
-(* nat eq *)
-
-structure EqCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_eq;
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac add_left_cancel;
-end);
-
-
-(* nat less *)
-
-structure LessCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_binrel "op <";
-  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
-end);
-
-
-(* nat le *)
-
-structure LeCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_binrel "op <=";
-  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
-end);
-
-
-(* nat diff *)
-
-structure DiffCancelSums = CancelSumsFun
-(struct
-  open Sum;
-  val mk_bal = HOLogic.mk_binop "op -";
-  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac diff_cancel;
-end);
-
-
-
-(** cancel common factor **)
-
-structure Factor =
-struct
-  val mk_sum = mk_norm_sum;
-  val dest_sum = dest_sum;
-  val prove_conv = prove_conv;
-  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
-end;
-
-fun mk_cnat n = cterm_of (Theory.sign_of Nat.thy) (HOLogic.mk_nat n);
-
-fun gen_multiply_tac rule k =
-  if k > 0 then
-    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
-  else no_tac;
-
-
-(* nat eq *)
-
-structure EqCancelFactor = CancelFactorFun
-(struct
-  open Factor;
-  val mk_bal = HOLogic.mk_eq;
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
-  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
-end);
-
-
-(* nat less *)
-
-structure LessCancelFactor = CancelFactorFun
-(struct
-  open Factor;
-  val mk_bal = HOLogic.mk_binrel "op <";
-  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
-  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
-end);
-
-
-(* nat le *)
-
-structure LeCancelFactor = CancelFactorFun
-(struct
-  open Factor;
-  val mk_bal = HOLogic.mk_binrel "op <=";
-  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
-  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
-end);
-
-
-
-(** prepare nat_cancel simprocs **)
-
-fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
-val prep_pats = map prep_pat;
-
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-
-val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
-val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
-val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
-val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
-
-val nat_cancel_sums_add = map prep_simproc
-  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
-   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
-   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
-
-val nat_cancel_sums = nat_cancel_sums_add @
-  [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
-
-val nat_cancel_factor = map prep_simproc
-  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
-   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
-   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
-
-val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
-
-
-end;
-
-open ArithData;
-
-Addsimprocs nat_cancel;
-
-(*---------------------------------------------------------------------------*)
-(* 2. Linear arithmetic                                                      *)
-(*---------------------------------------------------------------------------*)
-
-(* Parameters data for general linear arithmetic functor *)
-
-structure LA_Logic: LIN_ARITH_LOGIC =
-struct
-val ccontr = ccontr;
-val conjI = conjI;
-val neqE = linorder_neqE;
-val notI = notI;
-val sym = sym;
-val not_lessD = linorder_not_less RS iffD1;
-val not_leD = linorder_not_le RS iffD1;
-
-
-fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
-
-val mk_Trueprop = HOLogic.mk_Trueprop;
-
-fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
-  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
-
-fun is_False thm =
-  let val _ $ t = #prop(rep_thm thm)
-  in t = Const("False",HOLogic.boolT) end;
-
-fun is_nat(t) = fastype_of1 t = HOLogic.natT;
-
-fun mk_nat_thm sg t =
-  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
-  in instantiate ([],[(cn,ct)]) le0 end;
-
-end;
-
-signature LIN_ARITH_DATA2 =
-sig
-  include LIN_ARITH_DATA
-  val discrete: (string * bool)list ref
-end;
-
-structure LA_Data_Ref: LIN_ARITH_DATA2 =
-struct
-  val add_mono_thms = ref ([]:thm list);
-  val lessD = ref ([]:thm list);
-  val ss_ref = ref HOL_basic_ss;
-  val discrete = ref ([]:(string*bool)list);
-
-(* Decomposition of terms *)
-
-fun nT (Type("fun",[N,_])) = N = HOLogic.natT
-  | nT _ = false;
-
-fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
-                           | Some n => (overwrite(p,(t,n+m:int)), i));
-
-(* Turn term into list of summand * multiplicity plus a constant *)
-fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
-  | poly(all as Const("op -",T) $ s $ t, m, pi) =
-      if nT T then add_atom(all,m,pi)
-      else poly(s,m,poly(t,~1*m,pi))
-  | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi)
-  | poly(Const("0",_), _, pi) = pi
-  | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m))
-  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)=
-      (poly(t,m*HOLogic.dest_binum c,pi)
-       handle TERM _ => add_atom(all,m,pi))
-  | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)=
-      (poly(t,m*HOLogic.dest_binum c,pi)
-       handle TERM _ => add_atom(all,m,pi))
-  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
-     ((p,i + m*HOLogic.dest_binum t)
-      handle TERM _ => add_atom(all,m,(p,i)))
-  | poly x  = add_atom x;
-
-fun decomp2(rel,lhs,rhs) =
-  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
-  in case rel of
-       "op <"  => Some(p,i,"<",q,j)
-     | "op <=" => Some(p,i,"<=",q,j)
-     | "op ="  => Some(p,i,"=",q,j)
-     | _       => None
-  end;
-
-fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
-  | negate None = None;
-
-fun decomp1 (T,xxx) =
-  (case T of
-     Type("fun",[Type(D,[]),_]) =>
-       (case assoc(!discrete,D) of
-          None => None
-        | Some d => (case decomp2 xxx of
-                       None => None
-                     | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
-   | _ => None);
-
-fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs))
-  | decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
-      negate(decomp1 (T,(rel,lhs,rhs)))
-  | decomp _ = None
-end;
-
-let
-
-(* reduce contradictory <= to False.
-   Most of the work is done by the cancel tactics.
-*)
-val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
-
-val add_mono_thms = map (fn s => prove_goal Arith.thy s
- (fn prems => [cut_facts_tac prems 1,
-               blast_tac (claset() addIs [add_le_mono]) 1]))
-["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
- "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
- "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
- "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
-];
-
-in
-LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
-LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI];
-LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
-                      addsimprocs nat_cancel_sums_add;
-LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)]
-end;
-
-structure Fast_Arith =
-  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
-
-val fast_arith_tac = Fast_Arith.lin_arith_tac
-and trace_arith    = Fast_Arith.trace;
-
-let
-val nat_arith_simproc_pats =
-  map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
-      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
-
-val fast_nat_arith_simproc = mk_simproc
-  "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
-in
-Addsimprocs [fast_nat_arith_simproc]
-end;
-
-(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
-useful to detect inconsistencies among the premises for subgoals which are
-*not* themselves (in)equalities, because the latter activate
-fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
-solver all the time rather than add the additional check. *)
-
-simpset_ref () := (simpset() addSolver
-   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
-
-(*Elimination of `-' on nat*)
-Goal "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))";
-by (case_tac "a < b" 1);
-by (auto_tac (claset(), simpset() addsimps [diff_is_0_eq RS iffD2]));
-qed "nat_diff_split";
-
-(* FIXME: K true should be replaced by a sensible test to speed things up
-   in case there are lots of irrelevant terms involved;
-   elimination of min/max can be optimized:
-   (max m n + k <= r) = (m+k <= r & n+k <= r)
-   (l <= min m n + k) = (l <= m+k & l <= n+k)
-*)
-val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max];
-fun arith_tac i =
-  refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms))
-             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i;
-
-
-(* proof method setup *)
-
-fun arith_method prems =
-  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
-
-val arith_setup =
- [Method.add_methods
-  [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]];
-
-(*---------------------------------------------------------------------------*)
-(* End of proof procedures. Now go and USE them!                             *)
-(*---------------------------------------------------------------------------*)
 
 Goal "m <= m*(m::nat)";
 by (induct_tac "m" 1);
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Arith.thy	Tue Jul 25 00:06:46 2000 +0200
@@ -1,29 +1,21 @@
 (*  Title:      HOL/Arith.thy
     ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
 
-Arithmetic operators + - and * (for div, mod and dvd, see Divides)
+Setup arithmetic proof procedures.
 *)
 
-Arith = Nat +
+theory Arith = Nat
+files "arith_data.ML":
 
-instance
-  nat :: {plus, minus, times, power}
-
-(* size of a datatype value; overloaded *)
-consts size :: 'a => nat
+setup arith_setup
 
-primrec
-  add_0    "0 + n = n"
-  add_Suc  "Suc m + n = Suc(m + n)"
+(*elimination of `-' on nat*)
+lemma nat_diff_split:
+    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
+  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [RS iffD2])
 
-primrec
-  diff_0   "m - 0 = m"
-  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+ML {* val nat_diff_split = thm "nat_diff_split" *}
 
-primrec
-  mult_0   "0 * n = 0"
-  mult_Suc "Suc m * n = n + (m * n)"
+lemmas [arith_split] = nat_diff_split split_min split_max
 
 end
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -258,7 +258,7 @@
 
 (*Negation of a coefficient*)
 Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
-by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1);
+by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1);
 qed "zminus_number_of_zmult";
 
 Addsimps [zminus_number_of_zmult];
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/Int.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -34,7 +34,7 @@
   val ss		= HOL_ss
   val eq_reflection	= eq_reflection
 
-  val thy	= IntDef.thy
+  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context ()))
   val T		= HOLogic.intT
   val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
   val restrict_to_left  = restrict_to_left
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -1,575 +1,8 @@
-(*  Title:      HOL/Integ/IntArith.thy
+(*  Title:      HOL/Integ/IntArith.ML
     ID:         $Id$
     Authors:    Larry Paulson and Tobias Nipkow
-
-Simprocs and decision procedure for linear arithmetic.
 *)
 
-(*** Simprocs for numeric literals ***)
-
-(** Combining of literal coefficients in sums of products **)
-
-Goal "(x < y) = (x-y < (#0::int))";
-by (simp_tac (simpset() addsimps zcompare_rls) 1);
-qed "zless_iff_zdiff_zless_0";
-
-Goal "(x = y) = (x-y = (#0::int))";
-by (simp_tac (simpset() addsimps zcompare_rls) 1);
-qed "eq_iff_zdiff_eq_0";
-
-Goal "(x <= y) = (x-y <= (#0::int))";
-by (simp_tac (simpset() addsimps zcompare_rls) 1);
-qed "zle_iff_zdiff_zle_0";
-
-
-(** For combine_numerals **)
-
-Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
-by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
-qed "left_zadd_zmult_distrib";
-
-
-(** For cancel_numerals **)
-
-val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
-                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
-			   zle_iff_zdiff_zle_0] @
-		        map (inst "y" "n")
-                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
-			   zle_iff_zdiff_zle_0];
-
-Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
-		                     zadd_ac@rel_iff_rel_0_rls) 1);
-qed "eq_add_iff1";
-
-Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
-                                     zadd_ac@rel_iff_rel_0_rls) 1);
-qed "eq_add_iff2";
-
-Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
-                                     zadd_ac@rel_iff_rel_0_rls) 1);
-qed "less_add_iff1";
-
-Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
-                                     zadd_ac@rel_iff_rel_0_rls) 1);
-qed "less_add_iff2";
-
-Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
-                                     zadd_ac@rel_iff_rel_0_rls) 1);
-qed "le_add_iff1";
-
-Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
-                                     @zadd_ac@rel_iff_rel_0_rls) 1);
-qed "le_add_iff2";
-
-(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
-Goal "u = u' ==> (t==u) == (t==u')";
-by Auto_tac;
-qed "eq_cong2";
-
-
-structure Int_Numeral_Simprocs =
-struct
-
-(*Utilities*)
-
-fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
-                   NumeralSyntax.mk_bin n;
-
-(*Decodes a binary INTEGER*)
-fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
-     (NumeralSyntax.dest_bin w
-      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
-
-fun find_first_numeral past (t::terms) =
-	((dest_numeral t, rev past @ terms)
-	 handle TERM _ => find_first_numeral (t::past) terms)
-  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
-
-val zero = mk_numeral 0;
-val mk_plus = HOLogic.mk_binop "op +";
-
-val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
-
-(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
-fun mk_sum []        = zero
-  | mk_sum [t,u]     = mk_plus (t, u)
-  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum []        = zero
-  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
-
-(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
-        dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
-        dest_summing (pos, t, dest_summing (not pos, u, ts))
-  | dest_summing (pos, t, ts) =
-	if pos then t::ts else uminus_const$t :: ts;
-
-fun dest_sum t = dest_summing (true, t, []);
-
-val mk_diff = HOLogic.mk_binop "op -";
-val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT;
-
-val one = mk_numeral 1;
-val mk_times = HOLogic.mk_binop "op *";
-
-fun mk_prod [] = one
-  | mk_prod [t] = t
-  | mk_prod (t :: ts) = if t = one then mk_prod ts
-                        else mk_times (t, mk_prod ts);
-
-val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
-
-fun dest_prod t =
-      let val (t,u) = dest_times t 
-      in  dest_prod t @ dest_prod u  end
-      handle TERM _ => [t];
-
-(*DON'T do the obvious simplifications; that would create special cases*) 
-fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
-
-(*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
-  | dest_coeff sign t =
-    let val ts = sort Term.term_ord (dest_prod t)
-	val (n, ts') = find_first_numeral [] ts
-                          handle TERM _ => (1, ts)
-    in (sign*n, mk_prod ts') end;
-
-(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
-  | find_first_coeff past u (t::terms) =
-	let val (n,u') = dest_coeff 1 t
-	in  if u aconv u' then (n, rev past @ terms)
-			  else find_first_coeff (t::past) u terms
-	end
-	handle TERM _ => find_first_coeff (t::past) u terms;
-
-
-(*Simplify #1*n and n*#1 to n*)
-val add_0s = [zadd_0, zadd_0_right];
-val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
-
-(*To perform binary arithmetic*)
-val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
-
-(*To evaluate binary negations of coefficients*)
-val zminus_simps = NCons_simps @
-                   [number_of_minus RS sym, 
-		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
-		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
-
-(*To let us treat subtraction as addition*)
-val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
-
-(*Apply the given rewrite (if present) just once*)
-fun trans_tac None      = all_tac
-  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
-
-fun prove_conv name tacs sg (t, u) =
-  if t aconv u then None
-  else
-  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
-  in Some
-     (prove_goalw_cterm [] ct (K tacs)
-      handle ERROR => error 
-	  ("The error(s) above occurred while trying to prove " ^
-	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
-  end;
-
-fun simplify_meta_eq rules =
-    mk_meta_eq o
-    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
-
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT);
-val prep_pats = map prep_pat;
-
-structure CancelNumeralsCommon =
-  struct
-  val mk_sum    	= mk_sum
-  val dest_sum		= dest_sum
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff 1
-  val find_first_coeff	= find_first_coeff []
-  val trans_tac         = trans_tac
-  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
-                                                     zminus_simps@zadd_ac))
-                 THEN ALLGOALS
-                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
-                                               bin_simps@zadd_ac@zmult_ac))
-  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
-  end;
-
-
-structure EqCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "inteq_cancel_numerals"
-  val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
-  val bal_add1 = eq_add_iff1 RS trans
-  val bal_add2 = eq_add_iff2 RS trans
-);
-
-structure LessCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "intless_cancel_numerals"
-  val mk_bal   = HOLogic.mk_binrel "op <"
-  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
-  val bal_add1 = less_add_iff1 RS trans
-  val bal_add2 = less_add_iff2 RS trans
-);
-
-structure LeCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "intle_cancel_numerals"
-  val mk_bal   = HOLogic.mk_binrel "op <="
-  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
-  val bal_add1 = le_add_iff1 RS trans
-  val bal_add2 = le_add_iff2 RS trans
-);
-
-val cancel_numerals = 
-  map prep_simproc
-   [("inteq_cancel_numerals",
-     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
-		"(l::int) - m = n", "(l::int) = m - n", 
-		"(l::int) * m = n", "(l::int) = m * n"], 
-     EqCancelNumerals.proc),
-    ("intless_cancel_numerals", 
-     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
-		"(l::int) - m < n", "(l::int) < m - n", 
-		"(l::int) * m < n", "(l::int) < m * n"], 
-     LessCancelNumerals.proc),
-    ("intle_cancel_numerals", 
-     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
-		"(l::int) - m <= n", "(l::int) <= m - n", 
-		"(l::int) * m <= n", "(l::int) <= m * n"], 
-     LeCancelNumerals.proc)];
-
-
-structure CombineNumeralsData =
-  struct
-  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
-  val dest_sum		= dest_sum
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff 1
-  val left_distrib	= left_zadd_zmult_distrib RS trans
-  val prove_conv	= prove_conv "int_combine_numerals"
-  val trans_tac          = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
-                                              zminus_simps@zadd_ac))
-                 THEN ALLGOALS
-                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
-                                               bin_simps@zadd_ac@zmult_ac))
-  val numeral_simp_tac	= ALLGOALS 
-                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
-  end;
-
-structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-  
-val combine_numerals = 
-    prep_simproc ("int_combine_numerals",
-		  prep_pats ["(i::int) + j", "(i::int) - j"],
-		  CombineNumerals.proc);
-
-end;
-
-
-Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
-Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
-
-(*The Abel_Cancel simprocs are now obsolete*)
-Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1)); 
-
-test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
-
-test "#2*u = (u::int)";
-test "(i + j + #12 + (k::int)) - #15 = y";
-test "(i + j + #12 + (k::int)) - #5 = y";
-
-test "y - b < (b::int)";
-test "y - (#3*b + c) < (b::int) - #2*c";
-
-test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
-test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
-test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
-test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
-
-test "(i + j + #12 + (k::int)) = u + #15 + y";
-test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
-
-test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::int)";
-
-test "a + -(b+c) + b = (d::int)";
-test "a + -(b+c) - b = (d::int)";
-
-(*negative numerals*)
-test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
-test "(i + j + #-3 + (k::int)) < u + #5 + y";
-test "(i + j + #3 + (k::int)) < u + #-6 + y";
-test "(i + j + #-12 + (k::int)) - #15 = y";
-test "(i + j + #12 + (k::int)) - #-15 = y";
-test "(i + j + #-12 + (k::int)) - #-15 = y";
-*)
-
-
-(** Constant folding for integer plus and times **)
-
-(*We do not need
-    structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
-    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
-  because combine_numerals does the same thing*)
-
-structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-  val thy    = Bin.thy
-  val T	     = HOLogic.intT
-  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
-  val add_ac = zmult_ac
-end;
-
-structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
-
-Addsimprocs [Int_Times_Assoc.conv];
-
-
-(** The same for the naturals **)
-
-structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-  val thy    = Bin.thy
-  val T	     = HOLogic.natT
-  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
-  val add_ac = mult_ac
-end;
-
-structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
-
-Addsimprocs [Nat_Times_Assoc.conv];
-
-
-
-(*** decision procedure for linear arithmetic ***)
-
-(*---------------------------------------------------------------------------*)
-(* Linear arithmetic                                                         *)
-(*---------------------------------------------------------------------------*)
-
-(*
-Instantiation of the generic linear arithmetic package for int.
-*)
-
-(* Update parameters of arithmetic prover *)
-let
-
-(* reduce contradictory <= to False *)
-val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
-                [int_0, zadd_0, zadd_0_right, zdiff_def,
-		 zadd_zminus_inverse, zadd_zminus_inverse2, 
-		 zmult_0, zmult_0_right, 
-		 zmult_1, zmult_1_right, 
-		 zmult_minus1, zmult_minus1_right,
-		 zminus_zadd_distrib, zminus_zminus];
-
-val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
-               Int_Numeral_Simprocs.cancel_numerals;
-
-val add_mono_thms =
-  map (fn s => prove_goal Int.thy s
-                 (fn prems => [cut_facts_tac prems 1,
-                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
-    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
-     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
-     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
-     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
-    ];
-
-in
-LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
-LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
-LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
-                      addsimprocs simprocs
-                      addcongs [if_weak_cong];
-LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
-end;
-
-let
-val int_arith_simproc_pats =
-  map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
-      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
-
-val fast_int_arith_simproc = mk_simproc
-  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
-in
-Addsimprocs [fast_int_arith_simproc]
-end;
-
-(* Some test data
-Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
-\     ==> a+a <= j+j";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
-\     ==> a+a - - #-1 < j+j - #3";
-by (fast_arith_tac 1);
-Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by (arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a <= l";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a <= l+l+l+l";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a+a <= l+l+l+l+i";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
-by (fast_arith_tac 1);
-Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
-\     ==> #6*a <= #5*l+i";
-by (fast_arith_tac 1);
-*)
-
-(*---------------------------------------------------------------------------*)
-(* End of linear arithmetic                                                  *)
-(*---------------------------------------------------------------------------*)
-
-(** Simplification of inequalities involving numerical constants **)
-
-Goal "(w <= z - (#1::int)) = (w<(z::int))";
-by (arith_tac 1);
-qed "zle_diff1_eq";
-Addsimps [zle_diff1_eq];
-
-Goal "(w < z + #1) = (w<=(z::int))";
-by (arith_tac 1);
-qed "zle_add1_eq_le";
-Addsimps [zle_add1_eq_le];
-
-Goal "(z = z + w) = (w = (#0::int))";
-by (arith_tac 1);
-qed "zadd_left_cancel0";
-Addsimps [zadd_left_cancel0];
-
-
-(* nat *)
-
-Goal "#0 <= z ==> int (nat z) = z"; 
-by (asm_full_simp_tac
-    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
-qed "nat_0_le"; 
-
-Goal "z <= #0 ==> nat z = 0"; 
-by (case_tac "z = #0" 1);
-by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
-by (asm_full_simp_tac 
-    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
-qed "nat_le_0"; 
-
-Addsimps [nat_0_le, nat_le_0];
-
-val [major,minor] = Goal "[| #0 <= z;  !!m. z = int m ==> P |] ==> P"; 
-by (rtac (major RS nat_0_le RS sym RS minor) 1);
-qed "nonneg_eq_int"; 
-
-Goal "#0 <= w ==> (nat w = m) = (w = int m)";
-by Auto_tac;
-qed "nat_eq_iff";
-
-Goal "#0 <= w ==> (m = nat w) = (w = int m)";
-by Auto_tac;
-qed "nat_eq_iff2";
-
-Goal "#0 <= w ==> (nat w < m) = (w < int m)";
-by (rtac iffI 1);
-by (asm_full_simp_tac 
-    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
-by (etac (nat_0_le RS subst) 1);
-by (Simp_tac 1);
-qed "nat_less_iff";
-
-
-(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
-Addsimps [int_0, int_Suc, symmetric zdiff_def];
-
-Goal "nat #0 = 0";
-by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
-qed "nat_0";
-
-Goal "nat #1 = 1";
-by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
-qed "nat_1";
-
-Goal "nat #2 = 2";
-by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
-qed "nat_2";
-
-Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
-by (case_tac "neg z" 1);
-by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
-by (auto_tac (claset() addIs [zless_trans], 
-	      simpset() addsimps [neg_eq_less_0, zle_def]));
-qed "nat_less_eq_zless";
-
-Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
-by (auto_tac (claset(), 
-	      simpset() addsimps [linorder_not_less RS sym, 
-				  zless_nat_conj]));
-qed "nat_le_eq_zle";
-
-(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
-Goal "n<=m --> int m - int n = int (m-n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by Auto_tac;
-qed_spec_mp "zdiff_int";
-
-
-(*** abs: absolute value, as an integer ****)
-
-(* Simpler: use zabs_def as rewrite rule;
-   but arith_tac is not parameterized by such simp rules
-*)
-Goalw [zabs_def]
- "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))";
-by(Simp_tac 1);
-qed "zabs_split";
-
-arith_tac_split_thms := !arith_tac_split_thms @ [zabs_split];
-
 Goal "abs(abs(x::int)) = abs(x)";
 by(arith_tac 1);
 qed "abs_abs";
@@ -634,4 +67,3 @@
               simpset() addsimps [int_0_less_mult_iff, 
                                   linorder_not_less RS sym]));
 qed "zmult_le_0_iff";
-
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/IntArith.thy	Tue Jul 25 00:06:46 2000 +0200
@@ -1,2 +1,8 @@
-theory IntArith = Bin:
+
+theory IntArith = Bin
+files ("int_arith1.ML") ("int_arith2.ML"):
+
+use "int_arith1.ML"	setup int_arith_setup
+use "int_arith2.ML"	lemmas [arith_split] = zabs_split
+
 end
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -3,374 +3,9 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
-Simprocs for nat numerals
+Simprocs for nat numerals (see also nat_simprocs.ML).
 *)
 
-Goal "number_of v + (number_of v' + (k::nat)) = \
-\        (if neg (number_of v) then number_of v' + k \
-\         else if neg (number_of v') then number_of v + k \
-\         else number_of (bin_add v v') + k)";
-by (Simp_tac 1);
-qed "nat_number_of_add_left";
-
-
-(** For combine_numerals **)
-
-Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
-qed "left_add_mult_distrib";
-
-
-(** For cancel_numerals **)
-
-Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
-		            addsimps [add_mult_distrib]) 1);
-qed "nat_diff_add_eq1";
-
-Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
-		            addsimps [add_mult_distrib]) 1);
-qed "nat_diff_add_eq2";
-
-Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
-                                  addsimps [add_mult_distrib]));
-qed "nat_eq_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
-                                  addsimps [add_mult_distrib]));
-qed "nat_eq_add_iff2";
-
-Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
-                                  addsimps [add_mult_distrib]));
-qed "nat_less_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
-                                  addsimps [add_mult_distrib]));
-qed "nat_less_add_iff2";
-
-Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
-                                  addsimps [add_mult_distrib]));
-qed "nat_le_add_iff1";
-
-Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
-                                  addsimps [add_mult_distrib]));
-qed "nat_le_add_iff2";
-
-
-structure Nat_Numeral_Simprocs =
-struct
-
-(*Utilities*)
-
-fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ 
-                   NumeralSyntax.mk_bin n;
-
-(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
-fun dest_numeral (Const ("0", _)) = 0
-  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
-  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
-      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
-       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
-
-fun find_first_numeral past (t::terms) =
-	((dest_numeral t, t, rev past @ terms)
-	 handle TERM _ => find_first_numeral (t::past) terms)
-  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
-
-val zero = mk_numeral 0;
-val mk_plus = HOLogic.mk_binop "op +";
-
-(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
-fun mk_sum []        = zero
-  | mk_sum [t,u]     = mk_plus (t, u)
-  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-(*this version ALWAYS includes a trailing zero*)
-fun long_mk_sum []        = zero
-  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-
-val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
-
-(*extract the outer Sucs from a term and convert them to a binary numeral*)
-fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
-  | dest_Sucs (0, t) = t
-  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
-
-fun dest_sum t =
-      let val (t,u) = dest_plus t 
-      in  dest_sum t @ dest_sum u  end
-      handle TERM _ => [t];
-
-fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
-
-val trans_tac = Int_Numeral_Simprocs.trans_tac;
-
-val prove_conv = Int_Numeral_Simprocs.prove_conv;
-
-val bin_simps = [add_nat_number_of, nat_number_of_add_left,
-		 diff_nat_number_of, le_nat_number_of_eq_not_less, 
-		 less_nat_number_of, Let_number_of, nat_number_of] @ 
-                bin_arith_simps @ bin_rel_simps;
-
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
-val prep_pats = map prep_pat;
-
-
-(*** CancelNumerals simprocs ***)
-
-val one = mk_numeral 1;
-val mk_times = HOLogic.mk_binop "op *";
-
-fun mk_prod [] = one
-  | mk_prod [t] = t
-  | mk_prod (t :: ts) = if t = one then mk_prod ts
-                        else mk_times (t, mk_prod ts);
-
-val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
-
-fun dest_prod t =
-      let val (t,u) = dest_times t 
-      in  dest_prod t @ dest_prod u  end
-      handle TERM _ => [t];
-
-(*DON'T do the obvious simplifications; that would create special cases*) 
-fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
-
-(*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff t =
-    let val ts = sort Term.term_ord (dest_prod t)
-	val (n, _, ts') = find_first_numeral [] ts
-                          handle TERM _ => (1, one, ts)
-    in (n, mk_prod ts') end;
-
-(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
-  | find_first_coeff past u (t::terms) =
-	let val (n,u') = dest_coeff t
-	in  if u aconv u' then (n, rev past @ terms)
-			  else find_first_coeff (t::past) u terms
-	end
-	handle TERM _ => find_first_coeff (t::past) u terms;
-
-
-(*Simplify #1*n and n*#1 to n*)
-val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right];
-val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right];
-
-(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
-val simplify_meta_eq = 
-    Int_Numeral_Simprocs.simplify_meta_eq
-         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
-	 mult_0, mult_0_right, mult_1, mult_1_right];
-
-structure CancelNumeralsCommon =
-  struct
-  val mk_sum    	= mk_sum
-  val dest_sum		= dest_Sucs_sum
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff
-  val find_first_coeff	= find_first_coeff []
-  val trans_tac          = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
-                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
-                 THEN ALLGOALS (simp_tac
-				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
-  val numeral_simp_tac	= ALLGOALS
-                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq
-  end;
-
-
-structure EqCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "nateq_cancel_numerals"
-  val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
-  val bal_add1 = nat_eq_add_iff1 RS trans
-  val bal_add2 = nat_eq_add_iff2 RS trans
-);
-
-structure LessCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "natless_cancel_numerals"
-  val mk_bal   = HOLogic.mk_binrel "op <"
-  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
-  val bal_add1 = nat_less_add_iff1 RS trans
-  val bal_add2 = nat_less_add_iff2 RS trans
-);
-
-structure LeCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "natle_cancel_numerals"
-  val mk_bal   = HOLogic.mk_binrel "op <="
-  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
-  val bal_add1 = nat_le_add_iff1 RS trans
-  val bal_add2 = nat_le_add_iff2 RS trans
-);
-
-structure DiffCancelNumerals = CancelNumeralsFun
- (open CancelNumeralsCommon
-  val prove_conv = prove_conv "natdiff_cancel_numerals"
-  val mk_bal   = HOLogic.mk_binop "op -"
-  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
-  val bal_add1 = nat_diff_add_eq1 RS trans
-  val bal_add2 = nat_diff_add_eq2 RS trans
-);
-
-
-val cancel_numerals = 
-  map prep_simproc
-   [("nateq_cancel_numerals",
-     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", 
-		"(l::nat) * m = n", "(l::nat) = m * n", 
-		"Suc m = n", "m = Suc n"], 
-     EqCancelNumerals.proc),
-    ("natless_cancel_numerals", 
-     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", 
-		"(l::nat) * m < n", "(l::nat) < m * n", 
-		"Suc m < n", "m < Suc n"], 
-     LessCancelNumerals.proc),
-    ("natle_cancel_numerals", 
-     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", 
-		"(l::nat) * m <= n", "(l::nat) <= m * n", 
-		"Suc m <= n", "m <= Suc n"], 
-     LeCancelNumerals.proc),
-    ("natdiff_cancel_numerals", 
-     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", 
-		"(l::nat) * m - n", "(l::nat) - m * n", 
-		"Suc m - n", "m - Suc n"], 
-     DiffCancelNumerals.proc)];
-
-
-structure CombineNumeralsData =
-  struct
-  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
-  val dest_sum		= dest_Sucs_sum
-  val mk_coeff		= mk_coeff
-  val dest_coeff	= dest_coeff
-  val left_distrib	= left_add_mult_distrib RS trans
-  val prove_conv	= prove_conv "nat_combine_numerals"
-  val trans_tac          = trans_tac
-  val norm_tac = ALLGOALS
-                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
-                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
-                 THEN ALLGOALS (simp_tac
-				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
-  val numeral_simp_tac	= ALLGOALS
-                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq
-  end;
-
-structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-  
-val combine_numerals = 
-    prep_simproc ("nat_combine_numerals",
-		  prep_pats ["(i::nat) + j", "Suc (i + j)"],
-		  CombineNumerals.proc);
-
-end;
-
-
-Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
-Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1)); 
-
-(*cancel_numerals*)
-test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";
-test "(#2*length xs < #2*length xs + j)";
-test "(#2*length xs < length xs * #2 + j)";
-test "#2*u = (u::nat)";
-test "#2*u = Suc (u)";
-test "(i + j + #12 + (k::nat)) - #15 = y";
-test "(i + j + #12 + (k::nat)) - #5 = y";
-test "Suc u - #2 = y";
-test "Suc (Suc (Suc u)) - #2 = y";
-test "(i + j + #2 + (k::nat)) - 1 = y";
-test "(i + j + #1 + (k::nat)) - 2 = y";
-
-test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
-test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
-test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
-test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
-test "Suc ((u*v)*#4) - v*#3*u = w";
-test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
-
-test "(i + j + #12 + (k::nat)) = u + #15 + y";
-test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
-test "(i + j + #12 + (k::nat)) = u + #5 + y";
-(*Suc*)
-test "(i + j + #12 + k) = Suc (u + y)";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
-test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
-test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
-test "#2*y + #3*z + #2*u = Suc (u)";
-test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
-test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::nat)";
-test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
-test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
-
-(*negative numerals: FAIL*)
-test "(i + j + #-23 + (k::nat)) < u + #15 + y";
-test "(i + j + #3 + (k::nat)) < u + #-15 + y";
-test "(i + j + #-12 + (k::nat)) - #15 = y";
-test "(i + j + #12 + (k::nat)) - #-15 = y";
-test "(i + j + #-12 + (k::nat)) - #-15 = y";
-
-(*combine_numerals*)
-test "k + #3*k = (u::nat)";
-test "Suc (i + #3) = u";
-test "Suc (i + j + #3 + k) = u";
-test "k + j + #3*k + j = (u::nat)";
-test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
-test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
-(*negative numerals: FAIL*)
-test "Suc (i + j + #-3 + k) = u";
-*)
-
-
-(*** Prepare linear arithmetic for nat numerals ***)
-
-let
-
-(* reduce contradictory <= to False *)
-val add_rules =
-  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
-   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
-   le_Suc_number_of,le_number_of_Suc,
-   less_Suc_number_of,less_number_of_Suc,
-   Suc_eq_number_of,eq_number_of_Suc,
-   eq_number_of_0, eq_0_number_of, less_0_number_of,
-   nat_number_of, Let_number_of, if_True, if_False];
-
-val simprocs = [Nat_Times_Assoc.conv,
-		Nat_Numeral_Simprocs.combine_numerals]@ 
-		Nat_Numeral_Simprocs.cancel_numerals;
-
-in
-LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules 
-                                          addsimps basic_renamed_arith_simps
-                                          addsimprocs simprocs
-end;
-
-
-
 (** For simplifying  Suc m - #n **)
 
 Goal "#0 < n ==> Suc m - n = m - (n - #1)";
@@ -393,8 +28,8 @@
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (asm_full_simp_tac
-    (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, 
-				  neg_number_of_bin_pred_iff_0]) 1);
+    (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym,
+                                  neg_number_of_bin_pred_iff_0]) 1);
 qed "Suc_diff_number_of";
 
 (* now redundant because of the inverse_fold simproc
@@ -405,8 +40,8 @@
 \        if neg pv then a else f (nat pv))";
 by (simp_tac
     (simpset() addsplits [nat.split]
-			addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_number_of"; 
+                        addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
+qed "nat_case_number_of";
 
 Goal "nat_case a f ((number_of v) + n) = \
 \      (let pv = number_of (bin_pred v) in \
@@ -414,8 +49,8 @@
 by (stac add_eq_if 1);
 by (asm_simp_tac
     (simpset() addsplits [nat.split]
-               addsimps [Let_def, neg_imp_number_of_eq_0, 
-			 neg_number_of_bin_pred_iff_0]) 1);
+               addsimps [Let_def, neg_imp_number_of_eq_0,
+                         neg_number_of_bin_pred_iff_0]) 1);
 qed "nat_case_add_eq_if";
 
 Addsimps [nat_case_number_of, nat_case_add_eq_if];
@@ -426,9 +61,9 @@
 \        if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))";
 by (case_tac "(number_of v)::nat" 1);
 by (ALLGOALS (asm_simp_tac
-	      (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
+              (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
 by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
-qed "nat_rec_number_of"; 
+qed "nat_rec_number_of";
 
 Goal "nat_rec a f (number_of v + n) = \
 \       (let pv = number_of (bin_pred v) in \
@@ -437,9 +72,9 @@
 by (stac add_eq_if 1);
 by (asm_simp_tac
     (simpset() addsplits [nat.split]
-               addsimps [Let_def, neg_imp_number_of_eq_0, 
-			 neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_rec_add_eq_if"; 
+               addsimps [Let_def, neg_imp_number_of_eq_0,
+                         neg_number_of_bin_pred_iff_0]) 1);
+qed "nat_rec_add_eq_if";
 
 Addsimps [nat_rec_number_of, nat_rec_add_eq_if];
 
@@ -476,7 +111,7 @@
 by (Asm_simp_tac 2);
 by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
 qed "mod2_gr_0";
-Addsimps [mod2_gr_0, rename_numerals thy mod2_gr_0];
+Addsimps [mod2_gr_0, rename_numerals mod2_gr_0];
 
 (** Removal of small numerals: #0, #1 and (in additive positions) #2 **)
 
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/NatSimprocs.thy
--- a/src/HOL/Integ/NatSimprocs.thy	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.thy	Tue Jul 25 00:06:46 2000 +0200
@@ -1,2 +1,7 @@
-theory NatSimprocs = NatBin:
+
+theory NatSimprocs = NatBin
+files "nat_simprocs.ML":
+
+setup nat_simprocs_setup
+
 end
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/int_arith1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/int_arith1.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,467 @@
+(*  Title:      HOL/Integ/int_arith1.ML
+    ID:         $Id$
+    Authors:    Larry Paulson and Tobias Nipkow
+
+Simprocs and decision procedure for linear arithmetic.
+*)
+
+(*** Simprocs for numeric literals ***)
+
+(** Combining of literal coefficients in sums of products **)
+
+Goal "(x < y) = (x-y < (#0::int))";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zless_iff_zdiff_zless_0";
+
+Goal "(x = y) = (x-y = (#0::int))";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "eq_iff_zdiff_eq_0";
+
+Goal "(x <= y) = (x-y <= (#0::int))";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zle_iff_zdiff_zle_0";
+
+
+(** For combine_numerals **)
+
+Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
+by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
+qed "left_zadd_zmult_distrib";
+
+
+(** For cancel_numerals **)
+
+val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
+                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
+			   zle_iff_zdiff_zle_0] @
+		        map (inst "y" "n")
+                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
+			   zle_iff_zdiff_zle_0];
+
+Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+		                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "eq_add_iff1";
+
+Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+                                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "eq_add_iff2";
+
+Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+                                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "less_add_iff1";
+
+Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+                                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "less_add_iff2";
+
+Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+                                     zadd_ac@rel_iff_rel_0_rls) 1);
+qed "le_add_iff1";
+
+Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
+                                     @zadd_ac@rel_iff_rel_0_rls) 1);
+qed "le_add_iff2";
+
+(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
+Goal "u = u' ==> (t==u) == (t==u')";
+by Auto_tac;
+qed "eq_cong2";
+
+
+structure Int_Numeral_Simprocs =
+struct
+
+(*Utilities*)
+
+fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
+                   NumeralSyntax.mk_bin n;
+
+(*Decodes a binary INTEGER*)
+fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
+     (NumeralSyntax.dest_bin w
+      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+
+fun find_first_numeral past (t::terms) =
+	((dest_numeral t, rev past @ terms)
+	 handle TERM _ => find_first_numeral (t::past) terms)
+  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+
+val zero = mk_numeral 0;
+val mk_plus = HOLogic.mk_binop "op +";
+
+val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
+
+(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
+fun mk_sum []        = zero
+  | mk_sum [t,u]     = mk_plus (t, u)
+  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum []        = zero
+  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
+
+(*decompose additions AND subtractions as a sum*)
+fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
+        dest_summing (pos, t, dest_summing (pos, u, ts))
+  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
+        dest_summing (pos, t, dest_summing (not pos, u, ts))
+  | dest_summing (pos, t, ts) =
+	if pos then t::ts else uminus_const$t :: ts;
+
+fun dest_sum t = dest_summing (true, t, []);
+
+val mk_diff = HOLogic.mk_binop "op -";
+val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT;
+
+val one = mk_numeral 1;
+val mk_times = HOLogic.mk_binop "op *";
+
+fun mk_prod [] = one
+  | mk_prod [t] = t
+  | mk_prod (t :: ts) = if t = one then mk_prod ts
+                        else mk_times (t, mk_prod ts);
+
+val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
+
+fun dest_prod t =
+      let val (t,u) = dest_times t 
+      in  dest_prod t @ dest_prod u  end
+      handle TERM _ => [t];
+
+(*DON'T do the obvious simplifications; that would create special cases*) 
+fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
+
+(*Express t as a product of (possibly) a numeral with other sorted terms*)
+fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
+  | dest_coeff sign t =
+    let val ts = sort Term.term_ord (dest_prod t)
+	val (n, ts') = find_first_numeral [] ts
+                          handle TERM _ => (1, ts)
+    in (sign*n, mk_prod ts') end;
+
+(*Find first coefficient-term THAT MATCHES u*)
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
+  | find_first_coeff past u (t::terms) =
+	let val (n,u') = dest_coeff 1 t
+	in  if u aconv u' then (n, rev past @ terms)
+			  else find_first_coeff (t::past) u terms
+	end
+	handle TERM _ => find_first_coeff (t::past) u terms;
+
+
+(*Simplify #1*n and n*#1 to n*)
+val add_0s = [zadd_0, zadd_0_right];
+val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
+
+(*To perform binary arithmetic*)
+val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
+
+(*To evaluate binary negations of coefficients*)
+val zminus_simps = NCons_simps @
+                   [number_of_minus RS sym, 
+		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+
+(*To let us treat subtraction as addition*)
+val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
+
+(*Apply the given rewrite (if present) just once*)
+fun trans_tac None      = all_tac
+  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
+
+fun prove_conv name tacs sg (t, u) =
+  if t aconv u then None
+  else
+  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
+  in Some
+     (prove_goalw_cterm [] ct (K tacs)
+      handle ERROR => error 
+	  ("The error(s) above occurred while trying to prove " ^
+	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
+  end;
+
+fun simplify_meta_eq rules =
+    mk_meta_eq o
+    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT);
+val prep_pats = map prep_pat;
+
+structure CancelNumeralsCommon =
+  struct
+  val mk_sum    	= mk_sum
+  val dest_sum		= dest_sum
+  val mk_coeff		= mk_coeff
+  val dest_coeff	= dest_coeff 1
+  val find_first_coeff	= find_first_coeff []
+  val trans_tac         = trans_tac
+  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+                                                     zminus_simps@zadd_ac))
+                 THEN ALLGOALS
+                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
+                                               bin_simps@zadd_ac@zmult_ac))
+  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  end;
+
+
+structure EqCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "inteq_cancel_numerals"
+  val mk_bal   = HOLogic.mk_eq
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
+  val bal_add1 = eq_add_iff1 RS trans
+  val bal_add2 = eq_add_iff2 RS trans
+);
+
+structure LessCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "intless_cancel_numerals"
+  val mk_bal   = HOLogic.mk_binrel "op <"
+  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
+  val bal_add1 = less_add_iff1 RS trans
+  val bal_add2 = less_add_iff2 RS trans
+);
+
+structure LeCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "intle_cancel_numerals"
+  val mk_bal   = HOLogic.mk_binrel "op <="
+  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
+  val bal_add1 = le_add_iff1 RS trans
+  val bal_add2 = le_add_iff2 RS trans
+);
+
+val cancel_numerals = 
+  map prep_simproc
+   [("inteq_cancel_numerals",
+     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
+		"(l::int) - m = n", "(l::int) = m - n", 
+		"(l::int) * m = n", "(l::int) = m * n"], 
+     EqCancelNumerals.proc),
+    ("intless_cancel_numerals", 
+     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
+		"(l::int) - m < n", "(l::int) < m - n", 
+		"(l::int) * m < n", "(l::int) < m * n"], 
+     LessCancelNumerals.proc),
+    ("intle_cancel_numerals", 
+     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
+		"(l::int) - m <= n", "(l::int) <= m - n", 
+		"(l::int) * m <= n", "(l::int) <= m * n"], 
+     LeCancelNumerals.proc)];
+
+
+structure CombineNumeralsData =
+  struct
+  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
+  val dest_sum		= dest_sum
+  val mk_coeff		= mk_coeff
+  val dest_coeff	= dest_coeff 1
+  val left_distrib	= left_zadd_zmult_distrib RS trans
+  val prove_conv	= prove_conv "int_combine_numerals"
+  val trans_tac          = trans_tac
+  val norm_tac = ALLGOALS
+                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+                                              zminus_simps@zadd_ac))
+                 THEN ALLGOALS
+                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
+                                               bin_simps@zadd_ac@zmult_ac))
+  val numeral_simp_tac	= ALLGOALS 
+                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  end;
+
+structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+  
+val combine_numerals = 
+    prep_simproc ("int_combine_numerals",
+		  prep_pats ["(i::int) + j", "(i::int) - j"],
+		  CombineNumerals.proc);
+
+end;
+
+Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
+Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
+
+(*The Abel_Cancel simprocs are now obsolete*)
+Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Simp_tac 1)); 
+
+test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
+
+test "#2*u = (u::int)";
+test "(i + j + #12 + (k::int)) - #15 = y";
+test "(i + j + #12 + (k::int)) - #5 = y";
+
+test "y - b < (b::int)";
+test "y - (#3*b + c) < (b::int) - #2*c";
+
+test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
+test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
+test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
+test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
+
+test "(i + j + #12 + (k::int)) = u + #15 + y";
+test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
+
+test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::int)";
+
+test "a + -(b+c) + b = (d::int)";
+test "a + -(b+c) - b = (d::int)";
+
+(*negative numerals*)
+test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
+test "(i + j + #-3 + (k::int)) < u + #5 + y";
+test "(i + j + #3 + (k::int)) < u + #-6 + y";
+test "(i + j + #-12 + (k::int)) - #15 = y";
+test "(i + j + #12 + (k::int)) - #-15 = y";
+test "(i + j + #-12 + (k::int)) - #-15 = y";
+*)
+
+
+(** Constant folding for integer plus and times **)
+
+(*We do not need
+    structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
+    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
+  because combine_numerals does the same thing*)
+
+structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
+  val T	     = HOLogic.intT
+  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
+  val add_ac = zmult_ac
+end;
+
+structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
+
+Addsimprocs [Int_Times_Assoc.conv];
+
+
+(** The same for the naturals **)
+
+structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
+  val T	     = HOLogic.natT
+  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
+  val add_ac = mult_ac
+end;
+
+structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
+
+Addsimprocs [Nat_Times_Assoc.conv];
+
+
+(*** decision procedure for linear arithmetic ***)
+
+(*---------------------------------------------------------------------------*)
+(* Linear arithmetic                                                         *)
+(*---------------------------------------------------------------------------*)
+
+(*
+Instantiation of the generic linear arithmetic package for int.
+*)
+
+(* Update parameters of arithmetic prover *)
+local
+
+(* reduce contradictory <= to False *)
+val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
+                [int_0, zadd_0, zadd_0_right, zdiff_def,
+		 zadd_zminus_inverse, zadd_zminus_inverse2, 
+		 zmult_0, zmult_0_right, 
+		 zmult_1, zmult_1_right, 
+		 zmult_minus1, zmult_minus1_right,
+		 zminus_zadd_distrib, zminus_zminus];
+
+val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
+               Int_Numeral_Simprocs.cancel_numerals;
+
+val add_mono_thms_int =
+  map (fn s => prove_goal (the_context ()) s
+                 (fn prems => [cut_facts_tac prems 1,
+                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
+    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
+     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
+     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
+     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
+    ];
+
+in
+
+val int_arith_setup =
+ [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
+   {add_mono_thms = add_mono_thms @ add_mono_thms_int,
+    lessD = lessD @ [add1_zle_eq RS iffD2],
+    simpset = simpset addsimps add_rules
+                      addsimprocs simprocs
+                      addcongs [if_weak_cong]}),
+  arith_discrete ("IntDef.int", true)];
+
+end;
+
+let
+val int_arith_simproc_pats =
+  map (fn s => Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.boolT))
+      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
+
+val fast_int_arith_simproc = mk_simproc
+  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
+in
+Addsimprocs [fast_int_arith_simproc]
+end;
+
+(* Some test data
+Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
+\     ==> a+a <= j+j";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
+\     ==> a+a - - #-1 < j+j - #3";
+by (fast_arith_tac 1);
+Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
+by (arith_tac 1);
+Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a <= l";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a <= l+l+l+l";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a+a <= l+l+l+l+i";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
+by (fast_arith_tac 1);
+Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> #6*a <= #5*l+i";
+by (fast_arith_tac 1);
+*)
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/int_arith2.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/int_arith2.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,107 @@
+(*  Title:      HOL/Integ/int_arith2.ML
+    ID:         $Id$
+    Authors:    Larry Paulson and Tobias Nipkow
+*)
+
+(** Simplification of inequalities involving numerical constants **)
+
+Goal "(w <= z - (#1::int)) = (w<(z::int))";
+by (arith_tac 1);
+qed "zle_diff1_eq";
+Addsimps [zle_diff1_eq];
+
+Goal "(w < z + #1) = (w<=(z::int))";
+by (arith_tac 1);
+qed "zle_add1_eq_le";
+Addsimps [zle_add1_eq_le];
+
+Goal "(z = z + w) = (w = (#0::int))";
+by (arith_tac 1);
+qed "zadd_left_cancel0";
+Addsimps [zadd_left_cancel0];
+
+
+(* nat *)
+
+Goal "#0 <= z ==> int (nat z) = z"; 
+by (asm_full_simp_tac
+    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
+qed "nat_0_le"; 
+
+Goal "z <= #0 ==> nat z = 0"; 
+by (case_tac "z = #0" 1);
+by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
+by (asm_full_simp_tac 
+    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
+qed "nat_le_0"; 
+
+Addsimps [nat_0_le, nat_le_0];
+
+val [major,minor] = Goal "[| #0 <= z;  !!m. z = int m ==> P |] ==> P"; 
+by (rtac (major RS nat_0_le RS sym RS minor) 1);
+qed "nonneg_eq_int"; 
+
+Goal "#0 <= w ==> (nat w = m) = (w = int m)";
+by Auto_tac;
+qed "nat_eq_iff";
+
+Goal "#0 <= w ==> (m = nat w) = (w = int m)";
+by Auto_tac;
+qed "nat_eq_iff2";
+
+Goal "#0 <= w ==> (nat w < m) = (w < int m)";
+by (rtac iffI 1);
+by (asm_full_simp_tac 
+    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
+by (etac (nat_0_le RS subst) 1);
+by (Simp_tac 1);
+qed "nat_less_iff";
+
+
+(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
+Addsimps [int_0, int_Suc, symmetric zdiff_def];
+
+Goal "nat #0 = 0";
+by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
+qed "nat_0";
+
+Goal "nat #1 = 1";
+by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
+qed "nat_1";
+
+Goal "nat #2 = 2";
+by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
+qed "nat_2";
+
+Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
+by (case_tac "neg z" 1);
+by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
+by (auto_tac (claset() addIs [zless_trans], 
+	      simpset() addsimps [neg_eq_less_0, zle_def]));
+qed "nat_less_eq_zless";
+
+Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
+by (auto_tac (claset(), 
+	      simpset() addsimps [linorder_not_less RS sym, 
+				  zless_nat_conj]));
+qed "nat_le_eq_zle";
+
+(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
+Goal "n<=m --> int m - int n = int (m-n)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by Auto_tac;
+qed_spec_mp "zdiff_int";
+
+
+(*** abs: absolute value, as an integer ****)
+
+(* Simpler: use zabs_def as rewrite rule;
+   but arith_tac is not parameterized by such simp rules
+*)
+
+Goalw [zabs_def]
+ "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))";
+by(Simp_tac 1);
+qed "zabs_split";
+
+(*continued in IntArith.ML ...*)
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Integ/nat_simprocs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/nat_simprocs.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,375 @@
+(*  Title:      HOL/nat_simprocs.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Simprocs for nat numerals.
+*)
+
+Goal "number_of v + (number_of v' + (k::nat)) = \
+\        (if neg (number_of v) then number_of v' + k \
+\         else if neg (number_of v') then number_of v + k \
+\         else number_of (bin_add v v') + k)";
+by (Simp_tac 1);
+qed "nat_number_of_add_left";
+
+
+(** For combine_numerals **)
+
+Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
+by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
+qed "left_add_mult_distrib";
+
+
+(** For cancel_numerals **)
+
+Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]
+                            addsimps [add_mult_distrib]) 1);
+qed "nat_diff_add_eq1";
+
+Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]
+                            addsimps [add_mult_distrib]) 1);
+qed "nat_diff_add_eq2";
+
+Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
+                                  addsimps [add_mult_distrib]));
+qed "nat_eq_add_iff1";
+
+Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
+                                  addsimps [add_mult_distrib]));
+qed "nat_eq_add_iff2";
+
+Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
+                                  addsimps [add_mult_distrib]));
+qed "nat_less_add_iff1";
+
+Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
+                                  addsimps [add_mult_distrib]));
+qed "nat_less_add_iff2";
+
+Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
+                                  addsimps [add_mult_distrib]));
+qed "nat_le_add_iff1";
+
+Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
+                                  addsimps [add_mult_distrib]));
+qed "nat_le_add_iff2";
+
+
+structure Nat_Numeral_Simprocs =
+struct
+
+(*Utilities*)
+
+fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $
+                   NumeralSyntax.mk_bin n;
+
+(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
+fun dest_numeral (Const ("0", _)) = 0
+  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
+  | dest_numeral (Const("Numeral.number_of", _) $ w) =
+      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
+       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
+  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
+
+fun find_first_numeral past (t::terms) =
+        ((dest_numeral t, t, rev past @ terms)
+         handle TERM _ => find_first_numeral (t::past) terms)
+  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+
+val zero = mk_numeral 0;
+val mk_plus = HOLogic.mk_binop "op +";
+
+(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
+fun mk_sum []        = zero
+  | mk_sum [t,u]     = mk_plus (t, u)
+  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum []        = zero
+  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+
+(*extract the outer Sucs from a term and convert them to a binary numeral*)
+fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
+  | dest_Sucs (0, t) = t
+  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
+
+fun dest_sum t =
+      let val (t,u) = dest_plus t
+      in  dest_sum t @ dest_sum u  end
+      handle TERM _ => [t];
+
+fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
+
+val trans_tac = Int_Numeral_Simprocs.trans_tac;
+
+val prove_conv = Int_Numeral_Simprocs.prove_conv;
+
+val bin_simps = [add_nat_number_of, nat_number_of_add_left,
+                 diff_nat_number_of, le_nat_number_of_eq_not_less,
+                 less_nat_number_of, Let_number_of, nat_number_of] @
+                bin_arith_simps @ bin_rel_simps;
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
+val prep_pats = map prep_pat;
+
+
+(*** CancelNumerals simprocs ***)
+
+val one = mk_numeral 1;
+val mk_times = HOLogic.mk_binop "op *";
+
+fun mk_prod [] = one
+  | mk_prod [t] = t
+  | mk_prod (t :: ts) = if t = one then mk_prod ts
+                        else mk_times (t, mk_prod ts);
+
+val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
+
+fun dest_prod t =
+      let val (t,u) = dest_times t
+      in  dest_prod t @ dest_prod u  end
+      handle TERM _ => [t];
+
+(*DON'T do the obvious simplifications; that would create special cases*)
+fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
+
+(*Express t as a product of (possibly) a numeral with other sorted terms*)
+fun dest_coeff t =
+    let val ts = sort Term.term_ord (dest_prod t)
+        val (n, _, ts') = find_first_numeral [] ts
+                          handle TERM _ => (1, one, ts)
+    in (n, mk_prod ts') end;
+
+(*Find first coefficient-term THAT MATCHES u*)
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+  | find_first_coeff past u (t::terms) =
+        let val (n,u') = dest_coeff t
+        in  if u aconv u' then (n, rev past @ terms)
+                          else find_first_coeff (t::past) u terms
+        end
+        handle TERM _ => find_first_coeff (t::past) u terms;
+
+
+(*Simplify #1*n and n*#1 to n*)
+val add_0s = map rename_numerals [add_0, add_0_right];
+val mult_1s = map rename_numerals [mult_1, mult_1_right];
+
+(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
+val simplify_meta_eq =
+    Int_Numeral_Simprocs.simplify_meta_eq
+         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
+         mult_0, mult_0_right, mult_1, mult_1_right];
+
+structure CancelNumeralsCommon =
+  struct
+  val mk_sum            = mk_sum
+  val dest_sum          = dest_Sucs_sum
+  val mk_coeff          = mk_coeff
+  val dest_coeff        = dest_coeff
+  val find_first_coeff  = find_first_coeff []
+  val trans_tac          = trans_tac
+  val norm_tac = ALLGOALS
+                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
+                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
+                 THEN ALLGOALS (simp_tac
+                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
+  val numeral_simp_tac  = ALLGOALS
+                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
+  val simplify_meta_eq  = simplify_meta_eq
+  end;
+
+
+structure EqCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "nateq_cancel_numerals"
+  val mk_bal   = HOLogic.mk_eq
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+  val bal_add1 = nat_eq_add_iff1 RS trans
+  val bal_add2 = nat_eq_add_iff2 RS trans
+);
+
+structure LessCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "natless_cancel_numerals"
+  val mk_bal   = HOLogic.mk_binrel "op <"
+  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
+  val bal_add1 = nat_less_add_iff1 RS trans
+  val bal_add2 = nat_less_add_iff2 RS trans
+);
+
+structure LeCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "natle_cancel_numerals"
+  val mk_bal   = HOLogic.mk_binrel "op <="
+  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
+  val bal_add1 = nat_le_add_iff1 RS trans
+  val bal_add2 = nat_le_add_iff2 RS trans
+);
+
+structure DiffCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+  val prove_conv = prove_conv "natdiff_cancel_numerals"
+  val mk_bal   = HOLogic.mk_binop "op -"
+  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
+  val bal_add1 = nat_diff_add_eq1 RS trans
+  val bal_add2 = nat_diff_add_eq2 RS trans
+);
+
+
+val cancel_numerals =
+  map prep_simproc
+   [("nateq_cancel_numerals",
+     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n",
+                "(l::nat) * m = n", "(l::nat) = m * n",
+                "Suc m = n", "m = Suc n"],
+     EqCancelNumerals.proc),
+    ("natless_cancel_numerals",
+     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n",
+                "(l::nat) * m < n", "(l::nat) < m * n",
+                "Suc m < n", "m < Suc n"],
+     LessCancelNumerals.proc),
+    ("natle_cancel_numerals",
+     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n",
+                "(l::nat) * m <= n", "(l::nat) <= m * n",
+                "Suc m <= n", "m <= Suc n"],
+     LeCancelNumerals.proc),
+    ("natdiff_cancel_numerals",
+     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)",
+                "(l::nat) * m - n", "(l::nat) - m * n",
+                "Suc m - n", "m - Suc n"],
+     DiffCancelNumerals.proc)];
+
+
+structure CombineNumeralsData =
+  struct
+  val mk_sum            = long_mk_sum    (*to work for e.g. #2*x + #3*x *)
+  val dest_sum          = dest_Sucs_sum
+  val mk_coeff          = mk_coeff
+  val dest_coeff        = dest_coeff
+  val left_distrib      = left_add_mult_distrib RS trans
+  val prove_conv        = prove_conv "nat_combine_numerals"
+  val trans_tac          = trans_tac
+  val norm_tac = ALLGOALS
+                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
+                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
+                 THEN ALLGOALS (simp_tac
+                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
+  val numeral_simp_tac  = ALLGOALS
+                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
+  val simplify_meta_eq  = simplify_meta_eq
+  end;
+
+structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+
+val combine_numerals =
+    prep_simproc ("nat_combine_numerals",
+                  prep_pats ["(i::nat) + j", "Suc (i + j)"],
+                  CombineNumerals.proc);
+
+end;
+
+
+Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
+Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
+
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Simp_tac 1));
+
+(*cancel_numerals*)
+test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";
+test "(#2*length xs < #2*length xs + j)";
+test "(#2*length xs < length xs * #2 + j)";
+test "#2*u = (u::nat)";
+test "#2*u = Suc (u)";
+test "(i + j + #12 + (k::nat)) - #15 = y";
+test "(i + j + #12 + (k::nat)) - #5 = y";
+test "Suc u - #2 = y";
+test "Suc (Suc (Suc u)) - #2 = y";
+test "(i + j + #2 + (k::nat)) - 1 = y";
+test "(i + j + #1 + (k::nat)) - 2 = y";
+
+test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
+test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
+test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
+test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
+test "Suc ((u*v)*#4) - v*#3*u = w";
+test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
+
+test "(i + j + #12 + (k::nat)) = u + #15 + y";
+test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
+test "(i + j + #12 + (k::nat)) = u + #5 + y";
+(*Suc*)
+test "(i + j + #12 + k) = Suc (u + y)";
+test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
+test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
+test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
+test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
+test "#2*y + #3*z + #2*u = Suc (u)";
+test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
+test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::nat)";
+test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
+test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
+
+(*negative numerals: FAIL*)
+test "(i + j + #-23 + (k::nat)) < u + #15 + y";
+test "(i + j + #3 + (k::nat)) < u + #-15 + y";
+test "(i + j + #-12 + (k::nat)) - #15 = y";
+test "(i + j + #12 + (k::nat)) - #-15 = y";
+test "(i + j + #-12 + (k::nat)) - #-15 = y";
+
+(*combine_numerals*)
+test "k + #3*k = (u::nat)";
+test "Suc (i + #3) = u";
+test "Suc (i + j + #3 + k) = u";
+test "k + j + #3*k + j = (u::nat)";
+test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
+test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
+(*negative numerals: FAIL*)
+test "Suc (i + j + #-3 + k) = u";
+*)
+
+
+(*** Prepare linear arithmetic for nat numerals ***)
+
+local
+
+(* reduce contradictory <= to False *)
+val add_rules =
+  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
+   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
+   le_Suc_number_of,le_number_of_Suc,
+   less_Suc_number_of,less_number_of_Suc,
+   Suc_eq_number_of,eq_number_of_Suc,
+   eq_number_of_0, eq_0_number_of, less_0_number_of,
+   nat_number_of, Let_number_of, if_True, if_False];
+
+val simprocs = [Nat_Times_Assoc.conv,
+                Nat_Numeral_Simprocs.combine_numerals]@
+                Nat_Numeral_Simprocs.cancel_numerals;
+
+in
+
+val nat_simprocs_setup =
+ [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
+   {add_mono_thms = add_mono_thms, lessD = lessD,
+    simpset = simpset addsimps add_rules
+                      addsimps basic_renamed_arith_simps
+                      addsimprocs simprocs})];
+
+end;
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 25 00:06:46 2000 +0200
@@ -8,10 +8,11 @@
 
 default: HOL
 images: HOL HOL-Real TLA
-test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \
-  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML \
-  HOL-BCV HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
-  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
+test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \
+  HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \
+  HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
+  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
+  HOL-AxClasses-Tutorial HOL-Quot HOL-Real-ex \
   HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
 
 all: images test
@@ -31,44 +32,43 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
-  $(SRC)/Provers/Arith/cancel_sums.ML		\
-  $(SRC)/Provers/Arith/assoc_fold.ML		\
-  $(SRC)/Provers/Arith/combine_numerals.ML	\
-  $(SRC)/Provers/Arith/cancel_numerals.ML	\
-  $(SRC)/Provers/Arith/fast_lin_arith.ML \
-  $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
-  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
-  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
-  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
-  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
-  $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
-  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
-  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
-  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
-  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
-  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
-  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
-  Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
-  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
-  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
-  Integ/NatSimprocs.thy Integ/NatSimprocs.ML \
-  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
-  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
-  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
-  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
-  Relation.ML Relation.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \
-  String.thy SVC_Oracle.ML \
-  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
-  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
-  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
-  Tools/induct_method.ML Tools/inductive_package.ML \
-  Tools/numeral_syntax.ML Tools/primrec_package.ML \
-  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
-  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
-  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
-  simpdata.ML subset.ML subset.thy thy_syntax.ML
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
+  $(SRC)/Provers/Arith/cancel_sums.ML					\
+  $(SRC)/Provers/Arith/assoc_fold.ML					\
+  $(SRC)/Provers/Arith/combine_numerals.ML				\
+  $(SRC)/Provers/Arith/cancel_numerals.ML				\
+  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
+  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML			\
+  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML		\
+  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML	\
+  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml	\
+  $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig		\
+  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml		\
+  $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig	\
+  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml	\
+  Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML		\
+  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy	\
+  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML		\
+  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML	\
+  Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML	\
+  Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
+  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
+  Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
+  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML        \
+  Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML  \
+  Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML       \
+  Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy   \
+  Set.ML Set.thy SetInterval.ML	SetInterval.thy String.thy              \
+  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML     \
+  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML Tools/datatype_prop.ML	\
+  Tools/datatype_rep_proofs.ML Tools/induct_method.ML			\
+  Tools/inductive_package.ML Tools/numeral_syntax.ML			\
+  Tools/primrec_package.ML Tools/recdef_package.ML			\
+  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML	\
+  Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML	\
+  WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML blastdata.ML cladata.ML	\
+  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML	\
+  subset.ML subset.thy thy_syntax.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
 
@@ -76,16 +76,17 @@
 
 HOL-Real: HOL $(OUT)/HOL-Real
 
-$(OUT)/HOL-Real: $(OUT)/HOL Real/Lubs.ML Real/Lubs.thy Real/PNat.ML \
-  Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \
-  Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \
-  Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \
-  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
-  Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \
-  Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \
-  Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \
-  Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \
-  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
+$(OUT)/HOL-Real: $(OUT)/HOL Real/Hyperreal/Filter.ML			\
+  Real/Hyperreal/Filter.thy Real/Hyperreal/HyperDef.ML			\
+  Real/Hyperreal/HyperDef.thy Real/Hyperreal/Zorn.ML			\
+  Real/Hyperreal/Zorn.thy Real/Hyperreal/fuf.ML Real/Lubs.ML		\
+  Real/Lubs.thy Real/PNat.ML Real/PNat.thy Real/PRat.ML Real/PRat.thy	\
+  Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy	\
+  Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy		\
+  Real/RealArith.ML Real/RealArith.thy Real/RealBin.ML			\
+  Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML	\
+  Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML	\
+  Real/RealPow.thy Real/real_arith.ML
 	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
 
 
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Nat.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -1,7 +1,9 @@
 (*  Title:      HOL/Nat.ML
     ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1997 TU Muenchen
+    Author:     Lawrence C Paulson and Tobias Nipkow
+
+Proofs about natural numbers and elementary arithmetic: addition,
+multiplication, etc.  Some from the Hoare example from Norbert Galm.
 *)
 
 (** conversion rules for nat_rec **)
@@ -128,3 +130,606 @@
 qed "max_Suc_Suc";
 
 Addsimps [max_0L,max_0R,max_Suc_Suc];
+
+
+(*** Basic rewrite rules for the arithmetic operators ***)
+
+(** Difference **)
+
+Goal "0 - n = (0::nat)";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_0_eq_0";
+
+(*Must simplify BEFORE the induction!  (Else we get a critical pair)
+  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
+Goal "Suc(m) - Suc(n) = m - n";
+by (Simp_tac 1);
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_Suc_Suc";
+
+Addsimps [diff_0_eq_0, diff_Suc_Suc];
+
+(* Could be (and is, below) generalized in various ways;
+   However, none of the generalizations are currently in the simpset,
+   and I dread to think what happens if I put them in *)
+Goal "0 < n ==> Suc(n-1) = n";
+by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
+qed "Suc_pred";
+Addsimps [Suc_pred];
+
+Delsimps [diff_Suc];
+
+
+(**** Inductive properties of the operators ****)
+
+(*** Addition ***)
+
+Goal "m + 0 = (m::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_0_right";
+
+Goal "m + Suc(n) = Suc(m+n)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_Suc_right";
+
+Addsimps [add_0_right,add_Suc_right];
+
+
+(*Associative law for addition*)
+Goal "(m + n) + k = m + ((n + k)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_assoc";
+
+(*Commutative law for addition*)
+Goal "m + n = n + (m::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_commute";
+
+Goal "x+(y+z)=y+((x+z)::nat)";
+by (rtac (add_commute RS trans) 1);
+by (rtac (add_assoc RS trans) 1);
+by (rtac (add_commute RS arg_cong) 1);
+qed "add_left_commute";
+
+(*Addition is an AC-operator*)
+bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
+
+Goal "(k + m = k + n) = (m=(n::nat))";
+by (induct_tac "k" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "add_left_cancel";
+
+Goal "(m + k = n + k) = (m=(n::nat))";
+by (induct_tac "k" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "add_right_cancel";
+
+Goal "(k + m <= k + n) = (m<=(n::nat))";
+by (induct_tac "k" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "add_left_cancel_le";
+
+Goal "(k + m < k + n) = (m<(n::nat))";
+by (induct_tac "k" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+qed "add_left_cancel_less";
+
+Addsimps [add_left_cancel, add_right_cancel,
+          add_left_cancel_le, add_left_cancel_less];
+
+(** Reasoning about m+0=0, etc. **)
+
+Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
+by (case_tac "m" 1);
+by (Auto_tac);
+qed "add_is_0";
+AddIffs [add_is_0];
+
+Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
+by (case_tac "m" 1);
+by (Auto_tac);
+qed "zero_is_add";
+AddIffs [zero_is_add];
+
+Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
+by (case_tac "m" 1);
+by (Auto_tac);
+qed "add_is_1";
+
+Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
+by (case_tac "m" 1);
+by (Auto_tac);
+qed "one_is_add";
+
+Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
+by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
+qed "add_gr_0";
+AddIffs [add_gr_0];
+
+(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
+Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
+by (case_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
+                                      addsplits [nat.split])));
+qed "add_pred";
+Addsimps [add_pred];
+
+Goal "!!m::nat. m + n = m ==> n = 0";
+by (dtac (add_0_right RS ssubst) 1);
+by (asm_full_simp_tac (simpset() addsimps [add_assoc]
+                                 delsimps [add_0_right]) 1);
+qed "add_eq_self_zero";
+
+
+(**** Additional theorems about "less than" ****)
+
+(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
+Goal "m<n --> (EX k. n=Suc(m+k))";
+by (induct_tac "n" 1);
+by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
+by (blast_tac (claset() addSEs [less_SucE]
+                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
+qed_spec_mp "less_eq_Suc_add";
+
+Goal "n <= ((m + n)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Simp_tac);
+by (etac le_SucI 1);
+qed "le_add2";
+
+Goal "n <= ((n + m)::nat)";
+by (simp_tac (simpset() addsimps add_ac) 1);
+by (rtac le_add2 1);
+qed "le_add1";
+
+bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
+bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
+
+Goal "(m<n) = (EX k. n=Suc(m+k))";
+by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
+qed "less_iff_Suc_add";
+
+
+(*"i <= j ==> i <= j+m"*)
+bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
+
+(*"i <= j ==> i <= m+j"*)
+bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
+
+(*"i < j ==> i < j+m"*)
+bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
+
+(*"i < j ==> i < m+j"*)
+bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
+
+Goal "i+j < (k::nat) --> i<k";
+by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+by (blast_tac (claset() addDs [Suc_lessD]) 1);
+qed_spec_mp "add_lessD1";
+
+Goal "~ (i+j < (i::nat))";
+by (rtac notI 1);
+by (etac (add_lessD1 RS less_irrefl) 1);
+qed "not_add_less1";
+
+Goal "~ (j+i < (i::nat))";
+by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
+qed "not_add_less2";
+AddIffs [not_add_less1, not_add_less2];
+
+Goal "m+k<=n --> m<=(n::nat)";
+by (induct_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
+qed_spec_mp "add_leD1";
+
+Goal "m+k<=n ==> k<=(n::nat)";
+by (full_simp_tac (simpset() addsimps [add_commute]) 1);
+by (etac add_leD1 1);
+qed_spec_mp "add_leD2";
+
+Goal "m+k<=n ==> m<=n & k<=(n::nat)";
+by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
+bind_thm ("add_leE", result() RS conjE);
+
+(*needs !!k for add_ac to work*)
+Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
+by (force_tac (claset(),
+              simpset() delsimps [add_Suc_right]
+                        addsimps [less_iff_Suc_add,
+                                  add_Suc_right RS sym] @ add_ac) 1);
+qed "less_add_eq_less";
+
+
+(*** Monotonicity of Addition ***)
+
+(*strict, in 1st argument*)
+Goal "i < j ==> i + k < j + (k::nat)";
+by (induct_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_less_mono1";
+
+(*strict, in both arguments*)
+Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
+by (rtac (add_less_mono1 RS less_trans) 1);
+by (REPEAT (assume_tac 1));
+by (induct_tac "j" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_less_mono";
+
+(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
+val [lt_mono,le] = Goal
+     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
+\        i <= j                                 \
+\     |] ==> f(i) <= (f(j)::nat)";
+by (cut_facts_tac [le] 1);
+by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
+by (blast_tac (claset() addSIs [lt_mono]) 1);
+qed "less_mono_imp_le_mono";
+
+(*non-strict, in 1st argument*)
+Goal "i<=j ==> i + k <= j + (k::nat)";
+by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
+by (etac add_less_mono1 1);
+by (assume_tac 1);
+qed "add_le_mono1";
+
+(*non-strict, in both arguments*)
+Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
+by (etac (add_le_mono1 RS le_trans) 1);
+by (simp_tac (simpset() addsimps [add_commute]) 1);
+qed "add_le_mono";
+
+
+(*** Multiplication ***)
+
+(*right annihilation in product*)
+Goal "!!m::nat. m * 0 = 0";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_0_right";
+
+(*right successor law for multiplication*)
+Goal  "m * Suc(n) = m + (m * n)";
+by (induct_tac "m" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
+qed "mult_Suc_right";
+
+Addsimps [mult_0_right, mult_Suc_right];
+
+Goal "1 * n = n";
+by (Asm_simp_tac 1);
+qed "mult_1";
+
+Goal "n * 1 = n";
+by (Asm_simp_tac 1);
+qed "mult_1_right";
+
+(*Commutative law for multiplication*)
+Goal "m * n = n * (m::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_commute";
+
+(*addition distributes over multiplication*)
+Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
+qed "add_mult_distrib";
+
+Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
+qed "add_mult_distrib2";
+
+(*Associative law for multiplication*)
+Goal "(m * n) * k = m * ((n * k)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
+qed "mult_assoc";
+
+Goal "x*(y*z) = y*((x*z)::nat)";
+by (rtac trans 1);
+by (rtac mult_commute 1);
+by (rtac trans 1);
+by (rtac mult_assoc 1);
+by (rtac (mult_commute RS arg_cong) 1);
+qed "mult_left_commute";
+
+bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
+
+Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
+by (induct_tac "m" 1);
+by (induct_tac "n" 2);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_is_0";
+
+Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
+by (stac eq_commute 1 THEN stac mult_is_0 1);
+by Auto_tac;
+qed "zero_is_mult";
+
+Addsimps [mult_is_0, zero_is_mult];
+
+
+(*** Difference ***)
+
+Goal "!!m::nat. m - m = 0";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_self_eq_0";
+
+Addsimps [diff_self_eq_0];
+
+(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
+Goal "~ m<n --> n+(m-n) = (m::nat)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "add_diff_inverse";
+
+Goal "n<=m ==> n+(m-n) = (m::nat)";
+by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
+qed "le_add_diff_inverse";
+
+Goal "n<=m ==> (m-n)+n = (m::nat)";
+by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
+qed "le_add_diff_inverse2";
+
+Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
+
+
+(*** More results about difference ***)
+
+Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
+by (etac rev_mp 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "Suc_diff_le";
+
+Goal "m - n < Suc(m)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (etac less_SucE 3);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
+qed "diff_less_Suc";
+
+Goal "m - n <= (m::nat)";
+by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
+qed "diff_le_self";
+Addsimps [diff_le_self];
+
+(* j<k ==> j-n < k *)
+bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
+
+Goal "!!i::nat. i-j-k = i - (j+k)";
+by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_diff_left";
+
+Goal "(Suc m - n) - Suc k = m - n - k";
+by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
+qed "Suc_diff_diff";
+Addsimps [Suc_diff_diff];
+
+Goal "0<n ==> n - Suc i < n";
+by (case_tac "n" 1);
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps le_simps) 1);
+qed "diff_Suc_less";
+Addsimps [diff_Suc_less];
+
+(*This and the next few suggested by Florian Kammueller*)
+Goal "!!i::nat. i-j-k = i-k-j";
+by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
+qed "diff_commute";
+
+Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
+by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "diff_add_assoc";
+
+Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
+by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
+qed_spec_mp "diff_add_assoc2";
+
+Goal "(n+m) - n = (m::nat)";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_add_inverse";
+
+Goal "(m+n) - n = (m::nat)";
+by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
+qed "diff_add_inverse2";
+
+Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
+by Safe_tac;
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
+qed "le_imp_diff_is_add";
+
+Goal "!!m::nat. (m-n = 0) = (m <= n)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_is_0_eq";
+
+Goal "!!m::nat. (0 = m-n) = (m <= n)";
+by (stac (diff_is_0_eq RS sym) 1);
+by (rtac eq_sym_conv 1);
+qed "zero_is_diff_eq";
+Addsimps [diff_is_0_eq, zero_is_diff_eq];
+
+Goal "!!m::nat. (0<n-m) = (m<n)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_less_diff";
+Addsimps [zero_less_diff];
+
+Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
+by (res_inst_tac [("x","j - i")] exI 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
+qed "less_imp_add_positive";
+
+Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
+by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
+by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
+qed "zero_induct_lemma";
+
+val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
+by (rtac (diff_self_eq_0 RS subst) 1);
+by (rtac (zero_induct_lemma RS mp RS mp) 1);
+by (REPEAT (ares_tac ([impI,allI]@prems) 1));
+qed "zero_induct";
+
+Goal "(k+m) - (k+n) = m - (n::nat)";
+by (induct_tac "k" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_cancel";
+
+Goal "(m+k) - (n+k) = m - (n::nat)";
+by (asm_simp_tac
+    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
+qed "diff_cancel2";
+
+Goal "n - (n+m) = (0::nat)";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_add_0";
+
+
+(** Difference distributes over multiplication **)
+
+Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
+qed "diff_mult_distrib" ;
+
+Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
+val mult_commute_k = read_instantiate [("m","k")] mult_commute;
+by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
+qed "diff_mult_distrib2" ;
+(*NOT added as rewrites, since sometimes they are used from right-to-left*)
+
+
+(*** Monotonicity of Multiplication ***)
+
+Goal "i <= (j::nat) ==> i*k<=j*k";
+by (induct_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
+qed "mult_le_mono1";
+
+Goal "i <= (j::nat) ==> k*i <= k*j";
+by (dtac mult_le_mono1 1);
+by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
+qed "mult_le_mono2";
+
+(* <= monotonicity, BOTH arguments*)
+Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
+by (etac (mult_le_mono1 RS le_trans) 1);
+by (etac mult_le_mono2 1);
+qed "mult_le_mono";
+
+(*strict, in 1st argument; proof is by induction on k>0*)
+Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
+by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
+by (Asm_simp_tac 1);
+by (induct_tac "x" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
+qed "mult_less_mono2";
+
+Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
+by (dtac mult_less_mono2 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
+qed "mult_less_mono1";
+
+Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
+by (induct_tac "m" 1);
+by (case_tac "n" 2);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_less_mult_iff";
+Addsimps [zero_less_mult_iff];
+
+Goal "(1 <= m*n) = (1<=m & 1<=n)";
+by (induct_tac "m" 1);
+by (case_tac "n" 2);
+by (ALLGOALS Asm_simp_tac);
+qed "one_le_mult_iff";
+Addsimps [one_le_mult_iff];
+
+Goal "(m*n = 1) = (m=1 & n=1)";
+by (induct_tac "m" 1);
+by (Simp_tac 1);
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by (fast_tac (claset() addss simpset()) 1);
+qed "mult_eq_1_iff";
+Addsimps [mult_eq_1_iff];
+
+Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
+by (safe_tac (claset() addSIs [mult_less_mono1]));
+by (cut_facts_tac [less_linear] 1);
+by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
+qed "mult_less_cancel2";
+
+Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
+by (dtac mult_less_cancel2 1);
+by (etac subst 1);
+by (simp_tac (simpset() addsimps [mult_commute]) 1);
+qed "mult_less_cancel1";
+Addsimps [mult_less_cancel1, mult_less_cancel2];
+
+Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "mult_le_cancel2";
+
+Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "mult_le_cancel1";
+Addsimps [mult_le_cancel1, mult_le_cancel2];
+
+Goal "(Suc k * m < Suc k * n) = (m < n)";
+by (rtac mult_less_cancel1 1);
+by (Simp_tac 1);
+qed "Suc_mult_less_cancel1";
+
+Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
+by (simp_tac (simpset_of HOL.thy) 1);
+by (rtac Suc_mult_less_cancel1 1);
+qed "Suc_mult_le_cancel1";
+
+Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
+by (cut_facts_tac [less_linear] 1);
+by Safe_tac;
+by (assume_tac 2);
+by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
+by (ALLGOALS Asm_full_simp_tac);
+qed "mult_cancel2";
+
+Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
+by (dtac mult_cancel2 1);
+by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
+qed "mult_cancel1";
+Addsimps [mult_cancel1, mult_cancel2];
+
+Goal "(Suc k * m = Suc k * n) = (m = n)";
+by (rtac mult_cancel1 1);
+by (Simp_tac 1);
+qed "Suc_mult_cancel1";
+
+
+(*Lemma for gcd*)
+Goal "!!m::nat. m = m*n ==> n=1 | m=0";
+by (dtac sym 1);
+by (rtac disjCI 1);
+by (rtac nat_less_cases 1 THEN assume_tac 2);
+by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
+by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
+qed "mult_eq_self_implies_10";
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Nat.thy	Tue Jul 25 00:06:46 2000 +0200
@@ -1,13 +1,15 @@
 (*  Title:      HOL/Nat.thy
     ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1997 TU Muenchen
+    Author:     Tobias Nipkow and Lawrence C Paulson
 
-Type "nat" is a linear order, and a datatype
+Type "nat" is a linear order, and a datatype; arithmetic operators + -
+and * (for div, mod and dvd, see theory Divides).
 *)
 
 Nat = NatDef + Inductive +
 
+(* type "nat" is a linear order, and a datatype *)
+
 rep_datatype nat
   distinct Suc_not_Zero, Zero_not_Suc
   inject   Suc_Suc_eq
@@ -19,4 +21,25 @@
 consts
   "^"           :: ['a::power,nat] => 'a            (infixr 80)
 
+
+(* arithmetic operators + - and * *)
+
+instance
+  nat :: {plus, minus, times, power}
+
+(* size of a datatype value; overloaded *)
+consts size :: 'a => nat
+
+primrec
+  add_0    "0 + n = n"
+  add_Suc  "Suc m + n = Suc(m + n)"
+
+primrec
+  diff_0   "m - 0 = m"
+  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+
+primrec
+  mult_0   "0 * n = 0"
+  mult_Suc "Suc m * n = n + (m * n)"
+
 end
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Real/RealArith.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealArith.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,6 @@
+
+(*useful??*)
+Goal "(z = z + w) = (w = (#0::real))";
+by Auto_tac;
+qed "real_add_left_cancel0";
+Addsimps [real_add_left_cancel0];
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Real/RealArith.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/RealArith.thy	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,7 @@
+
+theory RealArith = RealBin
+files "real_arith.ML":
+
+setup real_arith_setup
+
+end
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Real/real_arith.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/real_arith.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,109 @@
+(*  Title:      HOL/Real/real_arith.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow, TU Muenchen
+    Copyright   1999 TU Muenchen
+
+Instantiation of the generic linear arithmetic package for type real.
+*)
+
+local
+
+(* reduce contradictory <= to False *)
+val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
+             add_real_number_of, minus_real_number_of, diff_real_number_of,
+             mult_real_number_of, eq_real_number_of, less_real_number_of,
+             le_real_number_of_eq_not_less, real_diff_def,
+             real_minus_add_distrib, real_minus_minus];
+
+val add_rules =
+    map rename_numerals
+        [real_add_zero_left, real_add_zero_right,
+         real_add_minus, real_add_minus_left,
+         real_mult_0, real_mult_0_right,
+         real_mult_1, real_mult_1_right,
+         real_mult_minus_1, real_mult_minus_1_right];
+
+val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
+               Real_Numeral_Simprocs.cancel_numerals;
+
+val mono_ss = simpset() addsimps
+                [real_add_le_mono,real_add_less_mono,
+                 real_add_less_le_mono,real_add_le_less_mono];
+
+val add_mono_thms_real =
+  map (fn s => prove_goal (the_context ()) s
+                 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
+    ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
+     "(i  = j) & (k <= l) ==> i + k <= j + (l::real)",
+     "(i <= j) & (k  = l) ==> i + k <= j + (l::real)",
+     "(i  = j) & (k  = l) ==> i + k  = j + (l::real)",
+     "(i < j) & (k = l)   ==> i + k < j + (l::real)",
+     "(i = j) & (k < l)   ==> i + k < j + (l::real)",
+     "(i < j) & (k <= l)  ==> i + k < j + (l::real)",
+     "(i <= j) & (k < l)  ==> i + k < j + (l::real)",
+     "(i < j) & (k < l)   ==> i + k < j + (l::real)"];
+
+val real_arith_simproc_pats =
+  map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
+      ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
+
+in
+
+val fast_real_arith_simproc = mk_simproc
+  "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
+
+val real_arith_setup =
+ [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
+   {add_mono_thms = add_mono_thms @ add_mono_thms_real,
+    lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
+    simpset = simpset addsimps simps@add_rules
+                      addsimprocs simprocs
+                      addcongs [if_weak_cong]}),
+  arith_discrete ("RealDef.real",false),
+  Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
+
+end;
+
+
+(* Some test data [omitting examples that assume the ordering to be discrete!]
+Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
+by (arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a <= l";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a <= l+l+l+l";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a+a <= l+l+l+l+i";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
+by (fast_arith_tac 1);
+qed "";
+
+Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
+\     ==> #6*a <= #5*l+i";
+by (fast_arith_tac 1);
+qed "";
+*)
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/Univ.thy
--- a/src/HOL/Univ.thy	Tue Jul 25 00:03:39 2000 +0200
+++ b/src/HOL/Univ.thy	Tue Jul 25 00:06:46 2000 +0200
@@ -11,8 +11,6 @@
 
 Univ = Arith + Sum +
 
-setup arith_setup
-
 
 (** lists, trees will be sets of nodes **)
 
diff -r c3a13a7d4424 -r 62bb04ab4b01 src/HOL/arith_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/arith_data.ML	Tue Jul 25 00:06:46 2000 +0200
@@ -0,0 +1,429 @@
+(*  Title:      HOL/arith_data.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, Stefan Berghofer and Tobias Nipkow
+
+Various arithmetic proof procedures.
+*)
+
+(*---------------------------------------------------------------------------*)
+(* 1. Cancellation of common terms                                           *)
+(*---------------------------------------------------------------------------*)
+
+signature ARITH_DATA =
+sig
+  val nat_cancel_sums_add: simproc list
+  val nat_cancel_sums: simproc list
+  val nat_cancel_factor: simproc list
+  val nat_cancel: simproc list
+end;
+
+structure ArithData: ARITH_DATA =
+struct
+
+
+(** abstract syntax of structure nat: 0, Suc, + **)
+
+(* mk_sum, mk_norm_sum *)
+
+val one = HOLogic.mk_nat 1;
+val mk_plus = HOLogic.mk_binop "op +";
+
+fun mk_sum [] = HOLogic.zero
+  | mk_sum [t] = t
+  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
+fun mk_norm_sum ts =
+  let val (ones, sums) = partition (equal one) ts in
+    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
+  end;
+
+
+(* dest_sum *)
+
+val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+
+fun dest_sum tm =
+  if HOLogic.is_zero tm then []
+  else
+    (case try HOLogic.dest_Suc tm of
+      Some t => one :: dest_sum t
+    | None =>
+        (case try dest_plus tm of
+          Some (t, u) => dest_sum t @ dest_sum u
+        | None => [tm]));
+
+
+(** generic proof tools **)
+
+(* prove conversions *)
+
+val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
+fun prove_conv expand_tac norm_tac sg (t, u) =
+  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
+    (K [expand_tac, norm_tac]))
+  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
+    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
+
+val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
+  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
+
+
+(* rewriting *)
+
+fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
+
+val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
+val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
+
+
+
+(** cancel common summands **)
+
+structure Sum =
+struct
+  val mk_sum = mk_norm_sum;
+  val dest_sum = dest_sum;
+  val prove_conv = prove_conv;
+  val norm_tac = simp_all add_rules THEN simp_all add_ac;
+end;
+
+fun gen_uncancel_tac rule ct =
+  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
+
+
+(* nat eq *)
+
+structure EqCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_eq;
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac add_left_cancel;
+end);
+
+
+(* nat less *)
+
+structure LessCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_binrel "op <";
+  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
+end);
+
+
+(* nat le *)
+
+structure LeCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_binrel "op <=";
+  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
+end);
+
+
+(* nat diff *)
+
+structure DiffCancelSums = CancelSumsFun
+(struct
+  open Sum;
+  val mk_bal = HOLogic.mk_binop "op -";
+  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
+  val uncancel_tac = gen_uncancel_tac diff_cancel;
+end);
+
+
+
+(** cancel common factor **)
+
+structure Factor =
+struct
+  val mk_sum = mk_norm_sum;
+  val dest_sum = dest_sum;
+  val prove_conv = prove_conv;
+  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
+end;
+
+fun mk_cnat n = cterm_of (Theory.sign_of (the_context ())) (HOLogic.mk_nat n);
+
+fun gen_multiply_tac rule k =
+  if k > 0 then
+    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
+  else no_tac;
+
+
+(* nat eq *)
+
+structure EqCancelFactor = CancelFactorFun
+(struct
+  open Factor;
+  val mk_bal = HOLogic.mk_eq;
+  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
+  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
+end);
+
+
+(* nat less *)
+
+structure LessCancelFactor = CancelFactorFun
+(struct
+  open Factor;
+  val mk_bal = HOLogic.mk_binrel "op <";
+  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
+  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
+end);
+
+
+(* nat le *)
+
+structure LeCancelFactor = CancelFactorFun
+(struct
+  open Factor;
+  val mk_bal = HOLogic.mk_binrel "op <=";
+  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
+  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
+end);
+
+
+
+(** prepare nat_cancel simprocs **)
+
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
+val prep_pats = map prep_pat;
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+
+val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
+val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
+val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
+val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
+
+val nat_cancel_sums_add = map prep_simproc
+  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
+   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
+   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
+
+val nat_cancel_sums = nat_cancel_sums_add @
+  [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
+
+val nat_cancel_factor = map prep_simproc
+  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
+   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
+   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
+
+val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
+
+
+end;
+
+open ArithData;
+
+
+(*---------------------------------------------------------------------------*)
+(* 2. Linear arithmetic                                                      *)
+(*---------------------------------------------------------------------------*)
+
+(* Parameters data for general linear arithmetic functor *)
+
+structure LA_Logic: LIN_ARITH_LOGIC =
+struct
+val ccontr = ccontr;
+val conjI = conjI;
+val neqE = linorder_neqE;
+val notI = notI;
+val sym = sym;
+val not_lessD = linorder_not_less RS iffD1;
+val not_leD = linorder_not_le RS iffD1;
+
+
+fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
+
+val mk_Trueprop = HOLogic.mk_Trueprop;
+
+fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
+  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
+
+fun is_False thm =
+  let val _ $ t = #prop(rep_thm thm)
+  in t = Const("False",HOLogic.boolT) end;
+
+fun is_nat(t) = fastype_of1 t = HOLogic.natT;
+
+fun mk_nat_thm sg t =
+  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
+  in instantiate ([],[(cn,ct)]) le0 end;
+
+end;
+
+
+(* arith theory data *)
+
+structure ArithDataArgs =
+struct
+  val name = "HOL/arith";
+  type T = {splits: thm list, discrete: (string * bool) list};
+
+  val empty = {splits = [], discrete = []};
+  val copy = I;
+  val prep_ext = I;
+  fun merge ({splits = splits1, discrete = discrete1}, {splits = splits2, discrete = discrete2}) =
+   {splits = Drule.merge_rules (splits1, splits2),
+    discrete = merge_alists discrete1 discrete2};
+  fun print _ _ = ();
+end;
+
+structure ArithData = TheoryDataFun(ArithDataArgs);
+
+fun arith_split_add (thy, thm) = (ArithData.map (fn {splits, discrete} =>
+  {splits = thm :: splits, discrete = discrete}) thy, thm);
+
+fun arith_discrete d = ArithData.map (fn {splits, discrete} =>
+  {splits = splits, discrete = d :: discrete});
+
+
+structure LA_Data_Ref: LIN_ARITH_DATA =
+struct
+
+(* Decomposition of terms *)
+
+fun nT (Type("fun",[N,_])) = N = HOLogic.natT
+  | nT _ = false;
+
+fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
+                           | Some n => (overwrite(p,(t,n+m:int)), i));
+
+(* Turn term into list of summand * multiplicity plus a constant *)
+fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
+  | poly(all as Const("op -",T) $ s $ t, m, pi) =
+      if nT T then add_atom(all,m,pi)
+      else poly(s,m,poly(t,~1*m,pi))
+  | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi)
+  | poly(Const("0",_), _, pi) = pi
+  | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m))
+  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)=
+      (poly(t,m*HOLogic.dest_binum c,pi)
+       handle TERM _ => add_atom(all,m,pi))
+  | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)=
+      (poly(t,m*HOLogic.dest_binum c,pi)
+       handle TERM _ => add_atom(all,m,pi))
+  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
+     ((p,i + m*HOLogic.dest_binum t)
+      handle TERM _ => add_atom(all,m,(p,i)))
+  | poly x  = add_atom x;
+
+fun decomp2(rel,lhs,rhs) =
+  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
+  in case rel of
+       "op <"  => Some(p,i,"<",q,j)
+     | "op <=" => Some(p,i,"<=",q,j)
+     | "op ="  => Some(p,i,"=",q,j)
+     | _       => None
+  end;
+
+fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
+  | negate None = None;
+
+fun decomp1 discrete (T,xxx) =
+  (case T of
+     Type("fun",[Type(D,[]),_]) =>
+       (case assoc(discrete,D) of
+          None => None
+        | Some d => (case decomp2 xxx of
+                       None => None
+                     | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
+   | _ => None);
+
+fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs))
+  | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
+      negate(decomp1 discrete (T,(rel,lhs,rhs)))
+  | decomp2 discrete _ = None
+
+val decomp = decomp2 o #discrete o ArithData.get_sg;
+
+end;
+
+
+structure Fast_Arith =
+  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
+
+val fast_arith_tac = Fast_Arith.lin_arith_tac
+and trace_arith    = Fast_Arith.trace;
+
+local
+
+(* reduce contradictory <= to False.
+   Most of the work is done by the cancel tactics.
+*)
+val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
+
+val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
+ (fn prems => [cut_facts_tac prems 1,
+               blast_tac (claset() addIs [add_le_mono]) 1]))
+["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
+ "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
+ "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
+ "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
+];
+
+in
+
+val init_lin_arith_data =
+ Fast_Arith.setup @
+ [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} =>
+   {add_mono_thms = add_mono_thms @ add_mono_thms_nat,
+    lessD = lessD @ [Suc_leI],
+    simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
+  ArithData.init, arith_discrete ("nat", true)];
+
+end;
+
+
+local
+val nat_arith_simproc_pats =
+  map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
+      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
+in
+val fast_nat_arith_simproc = mk_simproc
+  "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
+end;
+
+(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
+useful to detect inconsistencies among the premises for subgoals which are
+*not* themselves (in)equalities, because the latter activate
+fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
+solver all the time rather than add the additional check. *)
+
+
+(* arith proof method *)
+
+(* FIXME: K true should be replaced by a sensible test to speed things up
+   in case there are lots of irrelevant terms involved;
+   elimination of min/max can be optimized:
+   (max m n + k <= r) = (m+k <= r & n+k <= r)
+   (l <= min m n + k) = (l <= m+k & l <= n+k)
+*)
+fun arith_tac i st =
+  refute_tac (K true) (REPEAT o split_tac (#splits (ArithData.get_sg (Thm.sign_of_thm st))))
+             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
+
+fun arith_method prems =
+  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
+
+
+(* theory setup *)
+
+val arith_setup =
+ [Simplifier.change_simpset_of (op addsimprocs) nat_cancel] @
+  init_lin_arith_data @
+  [Simplifier.change_simpset_of (op addSolver)
+   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
+  Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
+  Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
+    "decide linear arithmethic")],
+  Attrib.add_attributes [("arith_split",
+    (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
+    "declare split rules for arithmetic procedure")]];