--- 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";
+
--- 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();
--- 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";
--- 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];
--- 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";
--- 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
--- 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*)
--- 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 \
--- 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];
--- 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";
--- 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
--- 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];
--- 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;
--- 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'";
--- 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)";
--- 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);
--- 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*)
--- 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 ***)
--- 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";
--- 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));
--- 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];