At last: linear arithmetic for nat!
authornipkow
Fri Nov 27 17:00:30 1998 +0100 (1998-11-27)
changeset 598379e301a6a51b
parent 5982 aeb97860d352
child 5984 4c2fc177f4d3
At last: linear arithmetic for nat!
src/HOL/Arith.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Message.ML
src/HOL/Divides.ML
src/HOL/Hoare/Examples.ML
src/HOL/Induct/Multiset.ML
src/HOL/Integ/IntDef.ML
src/HOL/IsaMakefile
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/List.ML
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/Type.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/ROOT.ML
src/HOL/UNITY/LessThan.ML
src/HOL/UNITY/Mutex.ML
src/HOL/arith_data.ML
src/HOL/ex/Primrec.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Nov 27 16:54:59 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Fri Nov 27 17:00:30 1998 +0100
     1.3 @@ -154,6 +154,7 @@
     1.4  Goal "n <= ((m + n)::nat)";
     1.5  by (induct_tac "m" 1);
     1.6  by (ALLGOALS Simp_tac);
     1.7 +by (etac le_SucI 1);
     1.8  qed "le_add2";
     1.9  
    1.10  Goal "n <= ((n + m)::nat)";
    1.11 @@ -184,6 +185,7 @@
    1.12  Goal "i+j < (k::nat) --> i<k";
    1.13  by (induct_tac "j" 1);
    1.14  by (ALLGOALS Asm_simp_tac);
    1.15 +by(blast_tac (claset() addDs [Suc_lessD]) 1);
    1.16  qed_spec_mp "add_lessD1";
    1.17  
    1.18  Goal "~ (i+j < (i::nat))";
    1.19 @@ -605,6 +607,311 @@
    1.20  qed "mult_eq_self_implies_10";
    1.21  
    1.22  
    1.23 +
    1.24 +
    1.25 +(*---------------------------------------------------------------------------*)
    1.26 +(* Various arithmetic proof procedures                                       *)
    1.27 +(*---------------------------------------------------------------------------*)
    1.28 +
    1.29 +(*---------------------------------------------------------------------------*)
    1.30 +(* 1. Cancellation of common terms                                           *)
    1.31 +(*---------------------------------------------------------------------------*)
    1.32 +
    1.33 +(*  Title:      HOL/arith_data.ML
    1.34 +    ID:         $Id$
    1.35 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    1.36 +
    1.37 +Setup various arithmetic proof procedures.
    1.38 +*)
    1.39 +
    1.40 +signature ARITH_DATA =
    1.41 +sig
    1.42 +  val nat_cancel_sums: simproc list
    1.43 +  val nat_cancel_factor: simproc list
    1.44 +  val nat_cancel: simproc list
    1.45 +end;
    1.46 +
    1.47 +structure ArithData: ARITH_DATA =
    1.48 +struct
    1.49 +
    1.50 +
    1.51 +(** abstract syntax of structure nat: 0, Suc, + **)
    1.52 +
    1.53 +(* mk_sum, mk_norm_sum *)
    1.54 +
    1.55 +val one = HOLogic.mk_nat 1;
    1.56 +val mk_plus = HOLogic.mk_binop "op +";
    1.57 +
    1.58 +fun mk_sum [] = HOLogic.zero
    1.59 +  | mk_sum [t] = t
    1.60 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.61 +
    1.62 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    1.63 +fun mk_norm_sum ts =
    1.64 +  let val (ones, sums) = partition (equal one) ts in
    1.65 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    1.66 +  end;
    1.67 +
    1.68 +
    1.69 +(* dest_sum *)
    1.70 +
    1.71 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
    1.72 +
    1.73 +fun dest_sum tm =
    1.74 +  if HOLogic.is_zero tm then []
    1.75 +  else
    1.76 +    (case try HOLogic.dest_Suc tm of
    1.77 +      Some t => one :: dest_sum t
    1.78 +    | None =>
    1.79 +        (case try dest_plus tm of
    1.80 +          Some (t, u) => dest_sum t @ dest_sum u
    1.81 +        | None => [tm]));
    1.82 +
    1.83 +
    1.84 +(** generic proof tools **)
    1.85 +
    1.86 +(* prove conversions *)
    1.87 +
    1.88 +val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    1.89 +
    1.90 +fun prove_conv expand_tac norm_tac sg (t, u) =
    1.91 +  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
    1.92 +    (K [expand_tac, norm_tac]))
    1.93 +  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.94 +    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
    1.95 +
    1.96 +val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    1.97 +  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    1.98 +
    1.99 +
   1.100 +(* rewriting *)
   1.101 +
   1.102 +fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
   1.103 +
   1.104 +val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   1.105 +val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
   1.106 +
   1.107 +
   1.108 +
   1.109 +(** cancel common summands **)
   1.110 +
   1.111 +structure Sum =
   1.112 +struct
   1.113 +  val mk_sum = mk_norm_sum;
   1.114 +  val dest_sum = dest_sum;
   1.115 +  val prove_conv = prove_conv;
   1.116 +  val norm_tac = simp_all add_rules THEN simp_all add_ac;
   1.117 +end;
   1.118 +
   1.119 +fun gen_uncancel_tac rule ct =
   1.120 +  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
   1.121 +
   1.122 +
   1.123 +(* nat eq *)
   1.124 +
   1.125 +structure EqCancelSums = CancelSumsFun
   1.126 +(struct
   1.127 +  open Sum;
   1.128 +  val mk_bal = HOLogic.mk_eq;
   1.129 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.130 +  val uncancel_tac = gen_uncancel_tac add_left_cancel;
   1.131 +end);
   1.132 +
   1.133 +
   1.134 +(* nat less *)
   1.135 +
   1.136 +structure LessCancelSums = CancelSumsFun
   1.137 +(struct
   1.138 +  open Sum;
   1.139 +  val mk_bal = HOLogic.mk_binrel "op <";
   1.140 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.141 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   1.142 +end);
   1.143 +
   1.144 +
   1.145 +(* nat le *)
   1.146 +
   1.147 +structure LeCancelSums = CancelSumsFun
   1.148 +(struct
   1.149 +  open Sum;
   1.150 +  val mk_bal = HOLogic.mk_binrel "op <=";
   1.151 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.152 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   1.153 +end);
   1.154 +
   1.155 +
   1.156 +(* nat diff *)
   1.157 +
   1.158 +structure DiffCancelSums = CancelSumsFun
   1.159 +(struct
   1.160 +  open Sum;
   1.161 +  val mk_bal = HOLogic.mk_binop "op -";
   1.162 +  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   1.163 +  val uncancel_tac = gen_uncancel_tac diff_cancel;
   1.164 +end);
   1.165 +
   1.166 +
   1.167 +
   1.168 +(** cancel common factor **)
   1.169 +
   1.170 +structure Factor =
   1.171 +struct
   1.172 +  val mk_sum = mk_norm_sum;
   1.173 +  val dest_sum = dest_sum;
   1.174 +  val prove_conv = prove_conv;
   1.175 +  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   1.176 +end;
   1.177 +
   1.178 +fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   1.179 +
   1.180 +fun gen_multiply_tac rule k =
   1.181 +  if k > 0 then
   1.182 +    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   1.183 +  else no_tac;
   1.184 +
   1.185 +
   1.186 +(* nat eq *)
   1.187 +
   1.188 +structure EqCancelFactor = CancelFactorFun
   1.189 +(struct
   1.190 +  open Factor;
   1.191 +  val mk_bal = HOLogic.mk_eq;
   1.192 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.193 +  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   1.194 +end);
   1.195 +
   1.196 +
   1.197 +(* nat less *)
   1.198 +
   1.199 +structure LessCancelFactor = CancelFactorFun
   1.200 +(struct
   1.201 +  open Factor;
   1.202 +  val mk_bal = HOLogic.mk_binrel "op <";
   1.203 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.204 +  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   1.205 +end);
   1.206 +
   1.207 +
   1.208 +(* nat le *)
   1.209 +
   1.210 +structure LeCancelFactor = CancelFactorFun
   1.211 +(struct
   1.212 +  open Factor;
   1.213 +  val mk_bal = HOLogic.mk_binrel "op <=";
   1.214 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.215 +  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   1.216 +end);
   1.217 +
   1.218 +
   1.219 +
   1.220 +(** prepare nat_cancel simprocs **)
   1.221 +
   1.222 +fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   1.223 +val prep_pats = map prep_pat;
   1.224 +
   1.225 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.226 +
   1.227 +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   1.228 +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   1.229 +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   1.230 +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
   1.231 +
   1.232 +val nat_cancel_sums = map prep_simproc
   1.233 +  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   1.234 +   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   1.235 +   ("natle_cancel_sums", le_pats, LeCancelSums.proc),
   1.236 +   ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
   1.237 +
   1.238 +val nat_cancel_factor = map prep_simproc
   1.239 +  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   1.240 +   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   1.241 +   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   1.242 +
   1.243 +val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   1.244 +
   1.245 +
   1.246 +end;
   1.247 +
   1.248 +open ArithData;
   1.249 +
   1.250 +Addsimprocs nat_cancel;
   1.251 +
   1.252 +(*---------------------------------------------------------------------------*)
   1.253 +(* 2. Linear arithmetic                                                      *)
   1.254 +(*---------------------------------------------------------------------------*)
   1.255 +
   1.256 +(* Parameter data for general linear arithmetic functor *)
   1.257 +structure Nat_LA_Data: LIN_ARITH_DATA =
   1.258 +struct
   1.259 +val ccontr = ccontr;
   1.260 +val conjI = conjI;
   1.261 +val lessD = Suc_leI;
   1.262 +val nat_neqE = nat_neqE;
   1.263 +val notI = notI;
   1.264 +val not_leD = not_leE RS Suc_leI;
   1.265 +val not_lessD = leI;
   1.266 +val sym = sym;
   1.267 +
   1.268 +val nat = Type("nat",[]);
   1.269 +
   1.270 +fun nnb T = T = Type("fun",[nat,Type("fun",[nat,Type("bool",[])])])
   1.271 +
   1.272 +(* Turn term into list of summand * multiplicity plus a constant *)
   1.273 +fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
   1.274 +  | poly(Const("op +",Type("fun",[Type("nat",[]),_])) $ s $ t, pi) =
   1.275 +      poly(s,poly(t,pi))
   1.276 +  | poly(t,(p,i)) =
   1.277 +      if t = Const("0",nat) then (p,i)
   1.278 +      else (case assoc(p,t) of None => ((t,1)::p,i)
   1.279 +            | Some m => (overwrite(p,(t,m+1)), i))
   1.280 +
   1.281 +fun decomp2(rel,T,lhs,rhs) =
   1.282 +  if not(nnb T) then None else
   1.283 +  let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
   1.284 +  in case rel of
   1.285 +       "op <"  => Some(p,i,"<",q,j)
   1.286 +     | "op <=" => Some(p,i,"<=",q,j)
   1.287 +     | "op ="  => Some(p,i,"=",q,j)
   1.288 +     | _       => None
   1.289 +  end;
   1.290 +
   1.291 +fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   1.292 +  | negate None = None;
   1.293 +
   1.294 +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   1.295 +  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   1.296 +      negate(decomp2(rel,T,lhs,rhs))
   1.297 +  | decomp _ = None
   1.298 +(* reduce contradictory <= to False.
   1.299 +   Most of the work is done by the cancel tactics.
   1.300 +*)
   1.301 +val add_rules = [Zero_not_Suc,Suc_not_Zero,le_0_eq];
   1.302 +
   1.303 +val cancel_sums_ss = HOL_basic_ss addsimps add_rules
   1.304 +                                  addsimprocs nat_cancel_sums;
   1.305 +
   1.306 +val simp = simplify cancel_sums_ss;
   1.307 +
   1.308 +val add_mono_thms = map (fn s => prove_goal Arith.thy s
   1.309 + (fn prems => [cut_facts_tac prems 1,
   1.310 +               blast_tac (claset() addIs [add_le_mono]) 1]))
   1.311 +["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
   1.312 + "(i = j) & (k <= l) ==> i + k <= j + (l::nat)",
   1.313 + "(i <= j) & (k = l) ==> i + k <= j + (l::nat)",
   1.314 + "(i = j) & (k = l) ==> i + k <= j + (l::nat)"
   1.315 +];
   1.316 +
   1.317 +end;
   1.318 +
   1.319 +structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
   1.320 +
   1.321 +simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
   1.322 +
   1.323 +(*---------------------------------------------------------------------------*)
   1.324 +(* End of proof procedures. Now go and USE them!                             *)
   1.325 +(*---------------------------------------------------------------------------*)
   1.326 +
   1.327 +
   1.328  (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   1.329  
   1.330  Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
   1.331 @@ -628,7 +935,7 @@
   1.332    by (dres_inst_tac [("k","k")] add_less_mono1 1);
   1.333    by (Asm_full_simp_tac 1);
   1.334   by (rotate_tac 1 1);
   1.335 - by (asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
   1.336 + by (Asm_full_simp_tac 1);
   1.337  by (etac add_less_imp_less_diff 1);
   1.338  qed "less_diff_conv";
   1.339  
   1.340 @@ -736,3 +1043,35 @@
   1.341  by (dtac not_leE 1);
   1.342  by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
   1.343  qed_spec_mp "diff_le_mono2";
   1.344 +
   1.345 +
   1.346 +(*This proof requires natdiff_cancel_sums*)
   1.347 +Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
   1.348 +by (induct_tac "l" 1);
   1.349 +by (Simp_tac 1);
   1.350 +by (Clarify_tac 1);
   1.351 +by (etac less_SucE 1);
   1.352 +by (Clarify_tac 2);
   1.353 +by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
   1.354 +by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
   1.355 +				      Suc_diff_le, less_imp_le]) 1);
   1.356 +qed_spec_mp "diff_less_mono2";
   1.357 +
   1.358 +(** Elimination of `-' on nat due to John Harrison **)
   1.359 +(*This proof requires natle_cancel_sums*)
   1.360 +
   1.361 +Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
   1.362 +by(case_tac "a <= b" 1);
   1.363 +by(Auto_tac);
   1.364 +by(eres_inst_tac [("x","b-a")] allE 1);
   1.365 +by(Auto_tac);
   1.366 +qed "nat_diff_split";
   1.367 +
   1.368 +(*
   1.369 +This is an example of the power of nat_diff_split. Many of the `-' thms in
   1.370 +Arith.ML could take advantage of this, but would need to be moved.
   1.371 +*)
   1.372 +Goal "m-n = 0  -->  n-m = 0  -->  m=n";
   1.373 +by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.374 +qed_spec_mp "diffs0_imp_equal";
   1.375 +
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Fri Nov 27 16:54:59 1998 +0100
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Fri Nov 27 17:00:30 1998 +0100
     2.3 @@ -33,7 +33,6 @@
     2.4            kerberos_ban.Kb3 RS kerberos_ban.Kb4) 2);
     2.5  by possibility_tac;
     2.6  by (ALLGOALS Asm_simp_tac);
     2.7 -by (ALLGOALS trans_tac);
     2.8  result();
     2.9  
    2.10  
     3.1 --- a/src/HOL/Auth/Message.ML	Fri Nov 27 16:54:59 1998 +0100
     3.2 +++ b/src/HOL/Auth/Message.ML	Fri Nov 27 17:00:30 1998 +0100
     3.3 @@ -314,7 +314,7 @@
     3.4  by (blast_tac (claset() addSEs [add_leE]) 2);
     3.5  (*Nonce case*)
     3.6  by (res_inst_tac [("x","N + Suc nat")] exI 1);
     3.7 -by (fast_tac (claset() addSEs [add_leE] addaltern ("trans_tac",trans_tac)) 1);
     3.8 +by (auto_tac (claset() addSEs [add_leE], simpset()));
     3.9  qed "msg_Nonce_supply";
    3.10  
    3.11  
     4.1 --- a/src/HOL/Divides.ML	Fri Nov 27 16:54:59 1998 +0100
     4.2 +++ b/src/HOL/Divides.ML	Fri Nov 27 17:00:30 1998 +0100
     4.3 @@ -176,9 +176,7 @@
     4.4  by (Clarify_tac 1);
     4.5  by (case_tac "n<k" 1);
     4.6  (* 1  case n<k *)
     4.7 -by (subgoal_tac "m<k" 1);
     4.8  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
     4.9 -by (trans_tac 1);
    4.10  (* 2  case n >= k *)
    4.11  by (case_tac "m<k" 1);
    4.12  (* 2.1  case m<k *)
    4.13 @@ -191,14 +189,14 @@
    4.14  (* Antimonotonicity of div in second argument *)
    4.15  Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
    4.16  by (subgoal_tac "0<n" 1);
    4.17 - by (trans_tac 2);
    4.18 + by (Simp_tac 2);
    4.19  by (res_inst_tac [("n","k")] less_induct 1);
    4.20  by (Simp_tac 1);
    4.21  by (rename_tac "k" 1);
    4.22  by (case_tac "k<n" 1);
    4.23   by (asm_simp_tac (simpset() addsimps [div_less]) 1);
    4.24  by (subgoal_tac "~(k<m)" 1);
    4.25 - by (trans_tac 2);
    4.26 + by (Simp_tac 2);
    4.27  by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
    4.28  by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
    4.29  by (REPEAT (eresolve_tac [div_le_mono,diff_le_mono2] 2));
    4.30 @@ -211,7 +209,7 @@
    4.31  by (subgoal_tac "m div n <= m div 1" 1);
    4.32  by (Asm_full_simp_tac 1);
    4.33  by (rtac div_le_mono2 1);
    4.34 -by (ALLGOALS trans_tac);
    4.35 +by (ALLGOALS Simp_tac);
    4.36  qed "div_le_dividend";
    4.37  Addsimps [div_le_dividend];
    4.38  
    4.39 @@ -223,7 +221,7 @@
    4.40  by (case_tac "m<n" 1);
    4.41   by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
    4.42  by (subgoal_tac "0<n" 1);
    4.43 - by (trans_tac 2);
    4.44 + by (Simp_tac 2);
    4.45  by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
    4.46  by (case_tac "n<m" 1);
    4.47   by (subgoal_tac "(m-n) div n < (m-n)" 1);
    4.48 @@ -232,7 +230,7 @@
    4.49   by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
    4.50  (* case n=m *)
    4.51  by (subgoal_tac "m=n" 1);
    4.52 - by (trans_tac 2);
    4.53 + by (Simp_tac 2);
    4.54  by (asm_simp_tac (simpset() addsimps [div_less]) 1);
    4.55  qed_spec_mp "div_less_dividend";
    4.56  Addsimps [div_less_dividend];
     5.1 --- a/src/HOL/Hoare/Examples.ML	Fri Nov 27 16:54:59 1998 +0100
     5.2 +++ b/src/HOL/Hoare/Examples.ML	Fri Nov 27 17:00:30 1998 +0100
     5.3 @@ -151,8 +151,7 @@
     5.4  by (hoare_tac Asm_full_simp_tac 1);
     5.5      by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
     5.6      by(Clarify_tac 1);
     5.7 -    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]
     5.8 -                                    addSolver cut_trans_tac) 1);
     5.9 +    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
    5.10     by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
    5.11    br conjI 1;
    5.12     by(Clarify_tac 1);
    5.13 @@ -161,17 +160,16 @@
    5.14    br less_imp_diff_less 1;
    5.15    by(Blast_tac 1);
    5.16   by(Clarify_tac 1);
    5.17 - by(asm_simp_tac (simpset() addsimps [nth_list_update]
    5.18 -                            addSolver cut_trans_tac) 1);
    5.19 + by(asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
    5.20   by(Clarify_tac 1);
    5.21 - by(trans_tac 1);
    5.22 + by(Simp_tac 1);
    5.23  by(Clarify_tac 1);
    5.24 -by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    5.25 +by(Asm_simp_tac 1);
    5.26  br conjI 1;
    5.27   by(Clarify_tac 1);
    5.28   br order_antisym 1;
    5.29 -  by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    5.30 - by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    5.31 +  by(Asm_simp_tac 1);
    5.32 + by(Asm_simp_tac 1);
    5.33  by(Clarify_tac 1);
    5.34 -by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    5.35 +by(Asm_simp_tac 1);
    5.36  qed "Partition";
     6.1 --- a/src/HOL/Induct/Multiset.ML	Fri Nov 27 16:54:59 1998 +0100
     6.2 +++ b/src/HOL/Induct/Multiset.ML	Fri Nov 27 17:00:30 1998 +0100
     6.3 @@ -327,8 +327,7 @@
     6.4  by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
     6.5   by(Blast_tac 2);
     6.6  by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
     6.7 -                           addcongs [conj_cong]
     6.8 -                           addSolver cut_trans_tac) 1);
     6.9 +                           addcongs [conj_cong]) 1);
    6.10  val lemma = result();
    6.11  
    6.12  val major::prems = Goal
     7.1 --- a/src/HOL/Integ/IntDef.ML	Fri Nov 27 16:54:59 1998 +0100
     7.2 +++ b/src/HOL/Integ/IntDef.ML	Fri Nov 27 17:00:30 1998 +0100
     7.3 @@ -168,10 +168,7 @@
     7.4  \         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
     7.5  (*Proof via congruent2_commuteI seems longer*)
     7.6  by Safe_tac;
     7.7 -by (asm_simp_tac (simpset() addsimps [add_assoc]) 1);
     7.8 -(*The rest should be trivial, but rearranging terms is hard*)
     7.9 -by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
    7.10 -by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
    7.11 +by (Asm_simp_tac 1);
    7.12  qed "zadd_congruent2";
    7.13  
    7.14  (*Resolve th against the corresponding facts for zadd*)
     8.1 --- a/src/HOL/IsaMakefile	Fri Nov 27 16:54:59 1998 +0100
     8.2 +++ b/src/HOL/IsaMakefile	Fri Nov 27 17:00:30 1998 +0100
     8.3 @@ -30,7 +30,7 @@
     8.4  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     8.5  
     8.6  $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/cancel_sums.ML \
     8.7 -  $(SRC)/Provers/Arith/nat_transitive.ML	\
     8.8 +  $(SRC)/Provers/Arith/fast_lin_arith.ML	\
     8.9    $(SRC)/Provers/Arith/abel_cancel.ML $(SRC)/Provers/blast.ML \
    8.10    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
    8.11    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
     9.1 --- a/src/HOL/Lambda/Eta.ML	Fri Nov 27 16:54:59 1998 +0100
     9.2 +++ b/src/HOL/Lambda/Eta.ML	Fri Nov 27 17:00:30 1998 +0100
     9.3 @@ -29,10 +29,9 @@
     9.4  Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
     9.5  by (induct_tac "t" 1);
     9.6  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
     9.7 -by (Blast_tac 2);
     9.8 +by(Auto_tac);
     9.9  by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
    9.10 -by (safe_tac HOL_cs);
    9.11 -by (ALLGOALS trans_tac);
    9.12 +by(Auto_tac);
    9.13  qed "free_lift";
    9.14  Addsimps [free_lift];
    9.15  
    9.16 @@ -45,7 +44,7 @@
    9.17  by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
    9.18                        addsplits [nat.split]) 1);
    9.19  by (safe_tac (HOL_cs addSEs [linorder_neqE]));
    9.20 -by (ALLGOALS trans_tac);
    9.21 +by (ALLGOALS Simp_tac);
    9.22  qed "free_subst";
    9.23  Addsimps [free_subst];
    9.24  
    9.25 @@ -118,9 +117,7 @@
    9.26  
    9.27  Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
    9.28  by (induct_tac "t" 1);
    9.29 -by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
    9.30 -by (safe_tac (HOL_cs addSEs [linorder_neqE]));
    9.31 -by (ALLGOALS trans_tac);
    9.32 +by(auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
    9.33  qed_spec_mp "subst_Var_Suc";
    9.34  Addsimps [subst_Var_Suc];
    9.35  
    10.1 --- a/src/HOL/Lambda/Lambda.ML	Fri Nov 27 16:54:59 1998 +0100
    10.2 +++ b/src/HOL/Lambda/Lambda.ML	Fri Nov 27 17:00:30 1998 +0100
    10.3 @@ -65,28 +65,21 @@
    10.4  Goal
    10.5    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
    10.6  by (induct_tac "t" 1);
    10.7 -by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
    10.8 -by (safe_tac HOL_cs);
    10.9 -by (ALLGOALS trans_tac);
   10.10 +by (Auto_tac);
   10.11  qed_spec_mp "lift_lift";
   10.12  
   10.13  Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
   10.14  by (induct_tac "t" 1);
   10.15  by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
   10.16 -                                addsplits [nat.split]
   10.17 -                                addSolver cut_trans_tac)));
   10.18 -by (safe_tac HOL_cs);
   10.19 -by (ALLGOALS trans_tac);
   10.20 +                                addsplits [nat.split])));
   10.21 +by (Auto_tac);
   10.22  qed "lift_subst";
   10.23  Addsimps [lift_subst];
   10.24  
   10.25  Goal
   10.26    "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
   10.27  by (induct_tac "t" 1);
   10.28 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
   10.29 -                                addSolver cut_trans_tac)));
   10.30 -by (safe_tac (HOL_cs addSEs [nat_neqE]));
   10.31 -by (ALLGOALS trans_tac);
   10.32 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift])));
   10.33  qed "lift_subst_lt";
   10.34  
   10.35  Goal "!k s. (lift t k)[s/k] = t";
   10.36 @@ -100,12 +93,9 @@
   10.37  by (induct_tac "t" 1);
   10.38  by (ALLGOALS(asm_simp_tac
   10.39        (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
   10.40 -                 delsplits [split_if]
   10.41 -                 addsplits [nat.split]
   10.42 -                 addloop ("if",split_inside_tac[split_if])
   10.43 -                addSolver cut_trans_tac)));
   10.44 +                 addsplits [nat.split])));
   10.45  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   10.46 -by (ALLGOALS trans_tac);
   10.47 +by (ALLGOALS Simp_tac);
   10.48  qed_spec_mp "subst_subst";
   10.49  
   10.50  
    11.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Nov 27 16:54:59 1998 +0100
    11.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Nov 27 17:00:30 1998 +0100
    11.3 @@ -130,9 +130,9 @@
    11.4  qed_spec_mp "deltas_concat";
    11.5  Addsimps [deltas_concat];
    11.6  
    11.7 -goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
    11.8 +goal Arith.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
    11.9  by (etac linorder_neqE 1);
   11.10 -by (ALLGOALS trans_tac);
   11.11 +by (ALLGOALS Simp_tac);
   11.12  val lemma = result();
   11.13  
   11.14  Goal
    12.1 --- a/src/HOL/List.ML	Fri Nov 27 16:54:59 1998 +0100
    12.2 +++ b/src/HOL/List.ML	Fri Nov 27 17:00:30 1998 +0100
    12.3 @@ -878,12 +878,11 @@
    12.4  Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
    12.5  by(induct_tac "j" 1);
    12.6  by Auto_tac;
    12.7 -by(REPEAT(trans_tac 1));
    12.8  qed "upt_rec";
    12.9  
   12.10  Goal "j<=i ==> [i..j(] = []";
   12.11  by(stac upt_rec 1);
   12.12 -by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
   12.13 +by(Asm_simp_tac 1);
   12.14  qed "upt_conv_Nil";
   12.15  Addsimps [upt_conv_Nil];
   12.16  
   12.17 @@ -901,29 +900,28 @@
   12.18  Goal "length [i..j(] = j-i";
   12.19  by(induct_tac "j" 1);
   12.20   by (Simp_tac 1);
   12.21 -by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
   12.22 +by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
   12.23  qed "length_upt";
   12.24  Addsimps [length_upt];
   12.25  
   12.26  Goal "i+k < j --> [i..j(] ! k = i+k";
   12.27  by(induct_tac "j" 1);
   12.28   by(Simp_tac 1);
   12.29 -by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac
   12.30 -                           addSolver cut_trans_tac) 1);
   12.31 +by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
   12.32  br conjI 1;
   12.33   by(Clarify_tac 1);
   12.34   bd add_lessD1 1;
   12.35 - by(trans_tac 1);
   12.36 + by(Simp_tac 1);
   12.37  by(Clarify_tac 1);
   12.38  br conjI 1;
   12.39   by(Clarify_tac 1);
   12.40   by(subgoal_tac "n=i+k" 1);
   12.41    by(Asm_full_simp_tac 1);
   12.42 - by(trans_tac 1);
   12.43 + by(Simp_tac 1);
   12.44  by(Clarify_tac 1);
   12.45  by(subgoal_tac "n=i+k" 1);
   12.46   by(Asm_full_simp_tac 1);
   12.47 -by(trans_tac 1);
   12.48 +by(Simp_tac 1);
   12.49  qed_spec_mp "nth_upt";
   12.50  Addsimps [nth_upt];
   12.51  
    13.1 --- a/src/HOL/MiniML/Instance.ML	Fri Nov 27 16:54:59 1998 +0100
    13.2 +++ b/src/HOL/MiniML/Instance.ML	Fri Nov 27 17:00:30 1998 +0100
    13.3 @@ -90,7 +90,6 @@
    13.4  \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
    13.5  by (induct_tac "sch" 1);
    13.6  by Auto_tac;
    13.7 -by (ALLGOALS trans_tac);
    13.8  val aux2 = result () RS mp;
    13.9  
   13.10  
    14.1 --- a/src/HOL/MiniML/Type.ML	Fri Nov 27 16:54:59 1998 +0100
    14.2 +++ b/src/HOL/MiniML/Type.ML	Fri Nov 27 17:00:30 1998 +0100
    14.3 @@ -438,7 +438,7 @@
    14.4  by Safe_tac;
    14.5  by (dtac spec 1);
    14.6  by (mp_tac 1);
    14.7 -by (trans_tac 1);
    14.8 +by (Simp_tac 1);
    14.9  qed "new_tv_le";
   14.10  Addsimps [lessI RS less_imp_le RS new_tv_le];
   14.11  
   14.12 @@ -531,9 +531,7 @@
   14.13  Addsimps [new_tv_not_free_tv];
   14.14  
   14.15  Goalw [max_def] "!!n::nat. m < n ==> m < max n n'";
   14.16 -by (Simp_tac 1);
   14.17 -by Safe_tac;
   14.18 -by (trans_tac 1);
   14.19 +by (Auto_tac);
   14.20  qed "less_maxL";
   14.21  
   14.22  Goalw [max_def] "!!n::nat. m < n' ==> m < max n n'";
    15.1 --- a/src/HOL/Nat.ML	Fri Nov 27 16:54:59 1998 +0100
    15.2 +++ b/src/HOL/Nat.ML	Fri Nov 27 17:00:30 1998 +0100
    15.3 @@ -106,12 +106,12 @@
    15.4  
    15.5  Goal "min 0 n = 0";
    15.6  by (rtac min_leastL 1);
    15.7 -by (trans_tac 1);
    15.8 +by (Simp_tac 1);
    15.9  qed "min_0L";
   15.10  
   15.11  Goal "min n 0 = 0";
   15.12  by (rtac min_leastR 1);
   15.13 -by (trans_tac 1);
   15.14 +by (Simp_tac 1);
   15.15  qed "min_0R";
   15.16  
   15.17  Goalw [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    16.1 --- a/src/HOL/NatDef.ML	Fri Nov 27 16:54:59 1998 +0100
    16.2 +++ b/src/HOL/NatDef.ML	Fri Nov 27 17:00:30 1998 +0100
    16.3 @@ -550,72 +550,5 @@
    16.4  by (etac (rewrite_rule [le_def] Least_le RS notE) 1 THEN assume_tac 1);
    16.5  qed "not_less_Least";
    16.6  
    16.7 -(*** Instantiation of transitivity prover ***)
    16.8 -
    16.9 -structure Less_Arith =
   16.10 -struct
   16.11 -val nat_leI = leI;
   16.12 -val nat_leD = leD;
   16.13 -val lessI = lessI;
   16.14 -val zero_less_Suc = zero_less_Suc;
   16.15 -val less_reflE = less_irrefl;
   16.16 -val less_zeroE = less_zeroE;
   16.17 -val less_incr = Suc_mono;
   16.18 -val less_decr = Suc_less_SucD;
   16.19 -val less_incr_rhs = Suc_mono RS Suc_lessD;
   16.20 -val less_decr_lhs = Suc_lessD;
   16.21 -val less_trans_Suc = less_trans_Suc;
   16.22 -val leI = Suc_leI RS (Suc_le_mono RS iffD1);
   16.23 -val not_lessI = leI RS leD
   16.24 -val not_leI = prove_goal thy "!!m::nat. n < m ==> ~ m <= n"
   16.25 -  (fn _ => [etac swap2 1, etac leD 1]);
   16.26 -val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
   16.27 -  (fn _ => [etac less_SucE 1,
   16.28 -            blast_tac (claset() addSDs [Suc_less_SucD] addSEs [less_irrefl]
   16.29 -                              addDs [less_trans_Suc]) 1,
   16.30 -            assume_tac 1]);
   16.31 -val leD = le_imp_less_Suc;
   16.32 -val not_lessD = nat_leI RS leD;
   16.33 -val not_leD = not_leE
   16.34 -val eqD1 = prove_goal thy  "!!n. m = n ==> m < Suc n"
   16.35 - (fn _ => [etac subst 1, rtac lessI 1]);
   16.36 -val eqD2 = sym RS eqD1;
   16.37 -
   16.38 -fun is_zero(t) =  t = Const("0",Type("nat",[]));
   16.39 -
   16.40 -fun nnb T = T = Type("fun",[Type("nat",[]),
   16.41 -                            Type("fun",[Type("nat",[]),
   16.42 -                                        Type("bool",[])])])
   16.43 -
   16.44 -fun decomp_Suc(Const("Suc",_)$t) = let val (a,i) = decomp_Suc t in (a,i+1) end
   16.45 -  | decomp_Suc t = (t,0);
   16.46 -
   16.47 -fun decomp2(rel,T,lhs,rhs) =
   16.48 -  if not(nnb T) then None else
   16.49 -  let val (x,i) = decomp_Suc lhs
   16.50 -      val (y,j) = decomp_Suc rhs
   16.51 -  in case rel of
   16.52 -       "op <"  => Some(x,i,"<",y,j)
   16.53 -     | "op <=" => Some(x,i,"<=",y,j)
   16.54 -     | "op ="  => Some(x,i,"=",y,j)
   16.55 -     | _       => None
   16.56 -  end;
   16.57 -
   16.58 -fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   16.59 -  | negate None = None;
   16.60 -
   16.61 -fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   16.62 -  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   16.63 -      negate(decomp2(rel,T,lhs,rhs))
   16.64 -  | decomp _ = None
   16.65 -
   16.66 -end;
   16.67 -
   16.68 -structure Trans_Tac = Trans_Tac_Fun(Less_Arith);
   16.69 -
   16.70 -open Trans_Tac;
   16.71 -
   16.72 -simpset_ref () := (simpset() addSolver cut_trans_tac);
   16.73 -
   16.74 -(*** eliminates ~= in premises, which trans_tac cannot deal with ***)
   16.75 +(* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *)
   16.76  bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);
    17.1 --- a/src/HOL/ROOT.ML	Fri Nov 27 16:54:59 1998 +0100
    17.2 +++ b/src/HOL/ROOT.ML	Fri Nov 27 17:00:30 1998 +0100
    17.3 @@ -23,7 +23,7 @@
    17.4  use "$ISABELLE_HOME/src/Provers/classical.ML";
    17.5  use "$ISABELLE_HOME/src/Provers/blast.ML";
    17.6  use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    17.7 -use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
    17.8 +use "$ISABELLE_HOME/src/Provers/Arith/fast_lin_arith.ML";
    17.9  use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
   17.10  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
   17.11  use "$ISABELLE_HOME/src/Provers/Arith/abel_cancel.ML";
   17.12 @@ -57,7 +57,6 @@
   17.13  use_thy "Record";
   17.14  
   17.15  use_thy "Arith";
   17.16 -use "arith_data.ML";
   17.17  
   17.18  use_thy "Recdef";
   17.19  (*TFL: recursive function definitions*)
    18.1 --- a/src/HOL/UNITY/LessThan.ML	Fri Nov 27 16:54:59 1998 +0100
    18.2 +++ b/src/HOL/UNITY/LessThan.ML	Fri Nov 27 17:00:30 1998 +0100
    18.3 @@ -7,8 +7,8 @@
    18.4  *)
    18.5  
    18.6  
    18.7 -(*Make Auto_tac and Force_tac try trans_tac!*)
    18.8 -claset_ref() := claset() addaltern ("trans_tac",trans_tac);
    18.9 +(*Make Auto_tac and Force_tac try lin_arith_tac!*)
   18.10 +claset_ref() := claset() addaltern ("lin_arith_tac",Fast_Nat_Arith.lin_arith_tac);
   18.11  
   18.12  
   18.13  (*** lessThan ***)
    19.1 --- a/src/HOL/UNITY/Mutex.ML	Fri Nov 27 16:54:59 1998 +0100
    19.2 +++ b/src/HOL/UNITY/Mutex.ML	Fri Nov 27 17:00:30 1998 +0100
    19.3 @@ -69,10 +69,6 @@
    19.4  	      simpset_of Int.thy addsimps
    19.5  	        [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, 
    19.6  		 integ_of_BIT]));
    19.7 -by (exhaust_tac "na" 1);
    19.8 -by (exhaust_tac "nat" 2);
    19.9 -by (exhaust_tac "n" 3);
   19.10 -by Auto_tac;
   19.11  qed "eq_123";
   19.12  
   19.13  
    20.1 --- a/src/HOL/arith_data.ML	Fri Nov 27 16:54:59 1998 +0100
    20.2 +++ b/src/HOL/arith_data.ML	Fri Nov 27 17:00:30 1998 +0100
    20.3 @@ -250,3 +250,8 @@
    20.4  Goal "m-n = 0  -->  n-m = 0  -->  m=n";
    20.5  by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
    20.6  qed_spec_mp "diffs0_imp_equal";
    20.7 +
    20.8 +use"fast_nat_decider";
    20.9 +
   20.10 +simpset_ref () := (simpset() addSolver
   20.11 +  (fn thms => cut_facts_tac thms THEN' Fast_Nat_Decider.nat_arith_tac));
    21.1 --- a/src/HOL/ex/Primrec.ML	Fri Nov 27 16:54:59 1998 +0100
    21.2 +++ b/src/HOL/ex/Primrec.ML	Fri Nov 27 17:00:30 1998 +0100
    21.3 @@ -50,7 +50,6 @@
    21.4  Goal "j < ack(i,j)";
    21.5  by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
    21.6  by (ALLGOALS Asm_simp_tac);
    21.7 -by (ALLGOALS trans_tac);
    21.8  qed "less_ack2";
    21.9  
   21.10  AddIffs [less_ack2];