# HG changeset patch
# User nipkow
# Date 912182430 -3600
# Node ID 79e301a6a51bbbce2fe8329f895feeec28782216
# Parent  aeb97860d35210f1ae470eb7319c84f5a58fe891
At last: linear arithmetic for nat!

diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Arith.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -154,6 +154,7 @@
 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)";
@@ -184,6 +185,7 @@
 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))";
@@ -605,6 +607,311 @@
 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: 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 (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 (sign_of Arith.thy) (s, HOLogic.termTVar);
+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 = map prep_simproc
+  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
+   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
+   ("natle_cancel_sums", le_pats, LeCancelSums.proc),
+   ("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                                                      *)
+(*---------------------------------------------------------------------------*)
+
+(* Parameter data for general linear arithmetic functor *)
+structure Nat_LA_Data: LIN_ARITH_DATA =
+struct
+val ccontr = ccontr;
+val conjI = conjI;
+val lessD = Suc_leI;
+val nat_neqE = nat_neqE;
+val notI = notI;
+val not_leD = not_leE RS Suc_leI;
+val not_lessD = leI;
+val sym = sym;
+
+val nat = Type("nat",[]);
+
+fun nnb T = T = Type("fun",[nat,Type("fun",[nat,Type("bool",[])])])
+
+(* Turn term into list of summand * multiplicity plus a constant *)
+fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
+  | poly(Const("op +",Type("fun",[Type("nat",[]),_])) $ s $ t, pi) =
+      poly(s,poly(t,pi))
+  | poly(t,(p,i)) =
+      if t = Const("0",nat) then (p,i)
+      else (case assoc(p,t) of None => ((t,1)::p,i)
+            | Some m => (overwrite(p,(t,m+1)), i))
+
+fun decomp2(rel,T,lhs,rhs) =
+  if not(nnb T) then None else
+  let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],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)) = Some(x,i,"~"^rel,y,j)
+  | negate None = None;
+
+fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
+  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
+      negate(decomp2(rel,T,lhs,rhs))
+  | decomp _ = None
+(* reduce contradictory <= to False.
+   Most of the work is done by the cancel tactics.
+*)
+val add_rules = [Zero_not_Suc,Suc_not_Zero,le_0_eq];
+
+val cancel_sums_ss = HOL_basic_ss addsimps add_rules
+                                  addsimprocs nat_cancel_sums;
+
+val simp = simplify cancel_sums_ss;
+
+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)"
+];
+
+end;
+
+structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
+
+simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
+
+(*---------------------------------------------------------------------------*)
+(* End of proof procedures. Now go and USE them!                             *)
+(*---------------------------------------------------------------------------*)
+
+
 (*** Subtraction laws -- mostly from Clemens Ballarin ***)
 
 Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
@@ -628,7 +935,7 @@
   by (dres_inst_tac [("k","k")] add_less_mono1 1);
   by (Asm_full_simp_tac 1);
  by (rotate_tac 1 1);
- by (asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
+ by (Asm_full_simp_tac 1);
 by (etac add_less_imp_less_diff 1);
 qed "less_diff_conv";
 
@@ -736,3 +1043,35 @@
 by (dtac not_leE 1);
 by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
 qed_spec_mp "diff_le_mono2";
+
+
+(*This proof requires natdiff_cancel_sums*)
+Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
+by (induct_tac "l" 1);
+by (Simp_tac 1);
+by (Clarify_tac 1);
+by (etac less_SucE 1);
+by (Clarify_tac 2);
+by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
+by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
+				      Suc_diff_le, less_imp_le]) 1);
+qed_spec_mp "diff_less_mono2";
+
+(** Elimination of `-' on nat due to John Harrison **)
+(*This proof requires natle_cancel_sums*)
+
+Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
+by(case_tac "a <= b" 1);
+by(Auto_tac);
+by(eres_inst_tac [("x","b-a")] allE 1);
+by(Auto_tac);
+qed "nat_diff_split";
+
+(*
+This is an example of the power of nat_diff_split. Many of the `-' thms in
+Arith.ML could take advantage of this, but would need to be moved.
+*)
+Goal "m-n = 0  -->  n-m = 0  -->  m=n";
+by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed_spec_mp "diffs0_imp_equal";
+
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Auth/Kerberos_BAN.ML
--- a/src/HOL/Auth/Kerberos_BAN.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -33,7 +33,6 @@
           kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
 by possibility_tac;
 by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS trans_tac);
 result();
 
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Auth/Message.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -314,7 +314,7 @@
 by (blast_tac (claset() addSEs [add_leE]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);
-by (fast_tac (claset() addSEs [add_leE] addaltern ("trans_tac",trans_tac)) 1);
+by (auto_tac (claset() addSEs [add_leE], simpset()));
 qed "msg_Nonce_supply";
 
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Divides.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -176,9 +176,7 @@
 by (Clarify_tac 1);
 by (case_tac "n<k" 1);
 (* 1  case n<k *)
-by (subgoal_tac "m<k" 1);
 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
-by (trans_tac 1);
 (* 2  case n >= k *)
 by (case_tac "m<k" 1);
 (* 2.1  case m<k *)
@@ -191,14 +189,14 @@
 (* Antimonotonicity of div in second argument *)
 Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
 by (subgoal_tac "0<n" 1);
- by (trans_tac 2);
+ by (Simp_tac 2);
 by (res_inst_tac [("n","k")] less_induct 1);
 by (Simp_tac 1);
 by (rename_tac "k" 1);
 by (case_tac "k<n" 1);
  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
 by (subgoal_tac "~(k<m)" 1);
- by (trans_tac 2);
+ by (Simp_tac 2);
 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
 by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
@@ -211,7 +209,7 @@
 by (subgoal_tac "m div n <= m div 1" 1);
 by (Asm_full_simp_tac 1);
 by (rtac div_le_mono2 1);
-by (ALLGOALS trans_tac);
+by (ALLGOALS Simp_tac);
 qed "div_le_dividend";
 Addsimps [div_le_dividend];
 
@@ -223,7 +221,7 @@
 by (case_tac "m<n" 1);
  by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
 by (subgoal_tac "0<n" 1);
- by (trans_tac 2);
+ by (Simp_tac 2);
 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
 by (case_tac "n<m" 1);
  by (subgoal_tac "(m-n) div n < (m-n)" 1);
@@ -232,7 +230,7 @@
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
 (* case n=m *)
 by (subgoal_tac "m=n" 1);
- by (trans_tac 2);
+ by (Simp_tac 2);
 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
 qed_spec_mp "div_less_dividend";
 Addsimps [div_less_dividend];
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Hoare/Examples.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -151,8 +151,7 @@
 by (hoare_tac Asm_full_simp_tac 1);
     by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
     by(Clarify_tac 1);
-    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]
-                                    addSolver cut_trans_tac) 1);
+    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
    by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
   br conjI 1;
    by(Clarify_tac 1);
@@ -161,17 +160,16 @@
   br less_imp_diff_less 1;
   by(Blast_tac 1);
  by(Clarify_tac 1);
- by(asm_simp_tac (simpset() addsimps [nth_list_update]
-                            addSolver cut_trans_tac) 1);
+ by(asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
  by(Clarify_tac 1);
- by(trans_tac 1);
+ by(Simp_tac 1);
 by(Clarify_tac 1);
-by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+by(Asm_simp_tac 1);
 br conjI 1;
  by(Clarify_tac 1);
  br order_antisym 1;
-  by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
- by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+  by(Asm_simp_tac 1);
+ by(Asm_simp_tac 1);
 by(Clarify_tac 1);
-by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+by(Asm_simp_tac 1);
 qed "Partition";
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Induct/Multiset.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -327,8 +327,7 @@
 by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
  by(Blast_tac 2);
 by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
-                           addcongs [conj_cong]
-                           addSolver cut_trans_tac) 1);
+                           addcongs [conj_cong]) 1);
 val lemma = result();
 
 val major::prems = Goal
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Integ/IntDef.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -168,10 +168,7 @@
 \         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
 (*Proof via congruent2_commuteI seems longer*)
 by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [add_assoc]) 1);
-(*The rest should be trivial, but rearranging terms is hard*)
-by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
+by (Asm_simp_tac 1);
 qed "zadd_congruent2";
 
 (*Resolve th against the corresponding facts for zadd*)
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 27 17:00:30 1998 +0100
@@ -30,7 +30,7 @@
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
-  $(SRC)/Provers/Arith/nat_transitive.ML	\
+  $(SRC)/Provers/Arith/fast_lin_arith.ML	\
   $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Lambda/Eta.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -29,10 +29,9 @@
 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
-by (Blast_tac 2);
+by(Auto_tac);
 by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
-by (safe_tac HOL_cs);
-by (ALLGOALS trans_tac);
+by(Auto_tac);
 qed "free_lift";
 Addsimps [free_lift];
 
@@ -45,7 +44,7 @@
 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
                       addsplits [nat.split]) 1);
 by (safe_tac (HOL_cs addSEs [linorder_neqE]));
-by (ALLGOALS trans_tac);
+by (ALLGOALS Simp_tac);
 qed "free_subst";
 Addsimps [free_subst];
 
@@ -118,9 +117,7 @@
 
 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
 by (induct_tac "t" 1);
-by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
-by (safe_tac (HOL_cs addSEs [linorder_neqE]));
-by (ALLGOALS trans_tac);
+by(auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
 qed_spec_mp "subst_Var_Suc";
 Addsimps [subst_Var_Suc];
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Lambda/Lambda.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -65,28 +65,21 @@
 Goal
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
 by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
-by (safe_tac HOL_cs);
-by (ALLGOALS trans_tac);
+by (Auto_tac);
 qed_spec_mp "lift_lift";
 
 Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
-                                addsplits [nat.split]
-                                addSolver cut_trans_tac)));
-by (safe_tac HOL_cs);
-by (ALLGOALS trans_tac);
+                                addsplits [nat.split])));
+by (Auto_tac);
 qed "lift_subst";
 Addsimps [lift_subst];
 
 Goal
   "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
 by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
-                                addSolver cut_trans_tac)));
-by (safe_tac (HOL_cs addSEs [nat_neqE]));
-by (ALLGOALS trans_tac);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift])));
 qed "lift_subst_lt";
 
 Goal "!k s. (lift t k)[s/k] = t";
@@ -100,12 +93,9 @@
 by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
-                 delsplits [split_if]
-                 addsplits [nat.split]
-                 addloop ("if",split_inside_tac[split_if])
-                addSolver cut_trans_tac)));
+                 addsplits [nat.split])));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
-by (ALLGOALS trans_tac);
+by (ALLGOALS Simp_tac);
 qed_spec_mp "subst_subst";
 
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -130,9 +130,9 @@
 qed_spec_mp "deltas_concat";
 Addsimps [deltas_concat];
 
-goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
+goal Arith.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
 by (etac linorder_neqE 1);
-by (ALLGOALS trans_tac);
+by (ALLGOALS Simp_tac);
 val lemma = result();
 
 Goal
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/List.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -878,12 +878,11 @@
 Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
 by(induct_tac "j" 1);
 by Auto_tac;
-by(REPEAT(trans_tac 1));
 qed "upt_rec";
 
 Goal "j<=i ==> [i..j(] = []";
 by(stac upt_rec 1);
-by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+by(Asm_simp_tac 1);
 qed "upt_conv_Nil";
 Addsimps [upt_conv_Nil];
 
@@ -901,29 +900,28 @@
 Goal "length [i..j(] = j-i";
 by(induct_tac "j" 1);
  by (Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
+by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
 qed "length_upt";
 Addsimps [length_upt];
 
 Goal "i+k < j --> [i..j(] ! k = i+k";
 by(induct_tac "j" 1);
  by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac
-                           addSolver cut_trans_tac) 1);
+by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
 br conjI 1;
  by(Clarify_tac 1);
  bd add_lessD1 1;
- by(trans_tac 1);
+ by(Simp_tac 1);
 by(Clarify_tac 1);
 br conjI 1;
  by(Clarify_tac 1);
  by(subgoal_tac "n=i+k" 1);
   by(Asm_full_simp_tac 1);
- by(trans_tac 1);
+ by(Simp_tac 1);
 by(Clarify_tac 1);
 by(subgoal_tac "n=i+k" 1);
  by(Asm_full_simp_tac 1);
-by(trans_tac 1);
+by(Simp_tac 1);
 qed_spec_mp "nth_upt";
 Addsimps [nth_upt];
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/MiniML/Instance.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -90,7 +90,6 @@
 \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
 by (induct_tac "sch" 1);
 by Auto_tac;
-by (ALLGOALS trans_tac);
 val aux2 = result () RS mp;
 
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/MiniML/Type.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -438,7 +438,7 @@
 by Safe_tac;
 by (dtac spec 1);
 by (mp_tac 1);
-by (trans_tac 1);
+by (Simp_tac 1);
 qed "new_tv_le";
 Addsimps [lessI RS less_imp_le RS new_tv_le];
 
@@ -531,9 +531,7 @@
 Addsimps [new_tv_not_free_tv];
 
 Goalw [max_def] "!!n::nat. m < n ==> m < max n n'";
-by (Simp_tac 1);
-by Safe_tac;
-by (trans_tac 1);
+by (Auto_tac);
 qed "less_maxL";
 
 Goalw [max_def] "!!n::nat. m < n' ==> m < max n n'";
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/Nat.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -106,12 +106,12 @@
 
 Goal "min 0 n = 0";
 by (rtac min_leastL 1);
-by (trans_tac 1);
+by (Simp_tac 1);
 qed "min_0L";
 
 Goal "min n 0 = 0";
 by (rtac min_leastR 1);
-by (trans_tac 1);
+by (Simp_tac 1);
 qed "min_0R";
 
 Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/NatDef.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -550,72 +550,5 @@
 by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
 qed "not_less_Least";
 
-(*** Instantiation of transitivity prover ***)
-
-structure Less_Arith =
-struct
-val nat_leI = leI;
-val nat_leD = leD;
-val lessI = lessI;
-val zero_less_Suc = zero_less_Suc;
-val less_reflE = less_irrefl;
-val less_zeroE = less_zeroE;
-val less_incr = Suc_mono;
-val less_decr = Suc_less_SucD;
-val less_incr_rhs = Suc_mono RS Suc_lessD;
-val less_decr_lhs = Suc_lessD;
-val less_trans_Suc = less_trans_Suc;
-val leI = Suc_leI RS (Suc_le_mono RS iffD1);
-val not_lessI = leI RS leD
-val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n"
-  (fn _ => [etac swap2 1, etac leD 1]);
-val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
-  (fn _ => [etac less_SucE 1,
-            blast_tac (claset() addSDs [Suc_less_SucD] addSEs [less_irrefl]
-                              addDs [less_trans_Suc]) 1,
-            assume_tac 1]);
-val leD = le_imp_less_Suc;
-val not_lessD = nat_leI RS leD;
-val not_leD = not_leE
-val eqD1 = prove_goal thy  "!!n. m = n ==> m < Suc n"
- (fn _ => [etac subst 1, rtac lessI 1]);
-val eqD2 = sym RS eqD1;
-
-fun is_zero(t) =  t = Const("0",Type("nat",[]));
-
-fun nnb T = T = Type("fun",[Type("nat",[]),
-                            Type("fun",[Type("nat",[]),
-                                        Type("bool",[])])])
-
-fun decomp_Suc(Const("Suc",_)$t) = let val (a,i) = decomp_Suc t in (a,i+1) end
-  | decomp_Suc t = (t,0);
-
-fun decomp2(rel,T,lhs,rhs) =
-  if not(nnb T) then None else
-  let val (x,i) = decomp_Suc lhs
-      val (y,j) = decomp_Suc rhs
-  in case rel of
-       "op <"  => Some(x,i,"<",y,j)
-     | "op <=" => Some(x,i,"<=",y,j)
-     | "op ="  => Some(x,i,"=",y,j)
-     | _       => None
-  end;
-
-fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
-  | negate None = None;
-
-fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
-  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
-      negate(decomp2(rel,T,lhs,rhs))
-  | decomp _ = None
-
-end;
-
-structure Trans_Tac = Trans_Tac_Fun(Less_Arith);
-
-open Trans_Tac;
-
-simpset_ref () := (simpset() addSolver cut_trans_tac);
-
-(*** eliminates ~= in premises, which trans_tac cannot deal with ***)
+(* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
 bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/ROOT.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -23,7 +23,7 @@
 use "$ISABELLE_HOME/src/Provers/classical.ML";
 use "$ISABELLE_HOME/src/Provers/blast.ML";
 use "$ISABELLE_HOME/src/Provers/clasimp.ML";
-use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
+use "$ISABELLE_HOME/src/Provers/Arith/fast_lin_arith.ML";
 use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
 use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
 use "$ISABELLE_HOME/src/Provers/Arith/abel_cancel.ML";
@@ -57,7 +57,6 @@
 use_thy "Record";
 
 use_thy "Arith";
-use "arith_data.ML";
 
 use_thy "Recdef";
 (*TFL: recursive function definitions*)
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/UNITY/LessThan.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -7,8 +7,8 @@
 *)
 
 
-(*Make Auto_tac and Force_tac try trans_tac!*)
-claset_ref() := claset() addaltern ("trans_tac",trans_tac);
+(*Make Auto_tac and Force_tac try lin_arith_tac!*)
+claset_ref() := claset() addaltern ("lin_arith_tac",Fast_Nat_Arith.lin_arith_tac);
 
 
 (*** lessThan ***)
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/UNITY/Mutex.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -69,10 +69,6 @@
 	      simpset_of Int.thy addsimps
 	        [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, 
 		 integ_of_BIT]));
-by (exhaust_tac "na" 1);
-by (exhaust_tac "nat" 2);
-by (exhaust_tac "n" 3);
-by Auto_tac;
 qed "eq_123";
 
 
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/arith_data.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -250,3 +250,8 @@
 Goal "m-n = 0  -->  n-m = 0  -->  m=n";
 by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
 qed_spec_mp "diffs0_imp_equal";
+
+use"fast_nat_decider";
+
+simpset_ref () := (simpset() addSolver
+  (fn thms => cut_facts_tac thms THEN' Fast_Nat_Decider.nat_arith_tac));
diff -r aeb97860d352 -r 79e301a6a51b src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Fri Nov 27 16:54:59 1998 +0100
+++ b/src/HOL/ex/Primrec.ML	Fri Nov 27 17:00:30 1998 +0100
@@ -50,7 +50,6 @@
 Goal "j < ack(i,j)";
 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS trans_tac);
 qed "less_ack2";
 
 AddIffs [less_ack2];