# HG changeset patch
# User nipkow
# Date 915891851 -3600
# Node ID fba734ba6894ef46eaa7ff6cc636a2570c87eb2a
# Parent  5583261db33db1d0f594703e33a532f2926215bf
Refined arith tactic.

diff -r 5583261db33d -r fba734ba6894 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/Arith.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -855,6 +855,13 @@
 val not_lessD = leI;
 val sym = sym;
 
+fun mkEqTrue thm = thm RS (eqTrueI RS eq_reflection);
+val mk_Trueprop = HOLogic.mk_Trueprop;
+
+fun neg_prop(TP$(Const("Not",_)$t)) = (TP$t, true)
+  | neg_prop(TP$t) =
+      (TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t), false);
+
 (* 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 +",_) $ s $ t, pi) = poly(s,poly(t,pi))
@@ -916,9 +923,29 @@
 
 structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
 
-simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
+val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
+
+local
+fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT);
+
+val pats = map prep_pat
+  ["(m::nat) < n","(m::nat) <= n", "~ (m::nat) < n","~ (m::nat) <= n",
+   "(m::nat) = n"]
 
-val fast_nat_arith_tac = Fast_Nat_Arith.lin_arith_tac;
+in
+val fast_nat_arith_simproc =
+  mk_simproc "fast_nat_arith" pats Fast_Nat_Arith.lin_arith_prover;
+end;
+
+Addsimprocs [fast_nat_arith_simproc];
+
+(* 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 Fast_Nat_Arith.cut_lin_arith_tac);
 
 (* Elimination of `-' on nat due to John Harrison *)
 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
diff -r 5583261db33d -r fba734ba6894 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/Divides.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -189,14 +189,13 @@
 (* Antimonotonicity of div in second argument *)
 Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
 by (subgoal_tac "0<n" 1);
- by (Simp_tac 2);
+ by (Asm_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 (Simp_tac 2);
+ by (Asm_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));
@@ -209,19 +208,18 @@
 by (subgoal_tac "m div n <= m div 1" 1);
 by (Asm_full_simp_tac 1);
 by (rtac div_le_mono2 1);
-by (ALLGOALS Simp_tac);
+by (ALLGOALS Asm_simp_tac);
 qed "div_le_dividend";
 Addsimps [div_le_dividend];
 
 (* Similar for "less than" *)
 Goal "1<n ==> (0 < m) --> (m div n < m)";
 by (res_inst_tac [("n","m")] less_induct 1);
-by (Simp_tac 1);
 by (rename_tac "m" 1);
 by (case_tac "m<n" 1);
  by (asm_full_simp_tac (simpset() addsimps [div_less]) 1);
 by (subgoal_tac "0<n" 1);
- by (Simp_tac 2);
+ by (Asm_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);
@@ -230,7 +228,7 @@
  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
 (* case n=m *)
 by (subgoal_tac "m=n" 1);
- by (Simp_tac 2);
+ by (Asm_simp_tac 2);
 by (asm_simp_tac (simpset() addsimps [div_less]) 1);
 qed_spec_mp "div_less_dividend";
 Addsimps [div_less_dividend];
diff -r 5583261db33d -r fba734ba6894 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/Integ/Bin.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -410,6 +410,10 @@
 val not_lessD = zleI;
 val sym = sym;
 
+val mk_Trueprop = Nat_LA_Data.mk_Trueprop;
+val neg_prop = Nat_LA_Data.neg_prop;
+val mkEqTrue = Nat_LA_Data.mkEqTrue;
+
 val intT = Type("IntDef.int",[]);
 
 (* borrowed from Bin.thy: *)
diff -r 5583261db33d -r fba734ba6894 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/List.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -906,20 +906,10 @@
 by(induct_tac "j" 1);
  by(Simp_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(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(Simp_tac 1);
 by(Clarify_tac 1);
 by(subgoal_tac "n=i+k" 1);
- by(Asm_full_simp_tac 1);
-by(Simp_tac 1);
+ by(Asm_simp_tac 2);
+by(Asm_simp_tac 1);
 qed_spec_mp "nth_upt";
 Addsimps [nth_upt];
 
diff -r 5583261db33d -r fba734ba6894 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/MiniML/Type.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -530,15 +530,6 @@
 qed "new_tv_not_free_tv";
 Addsimps [new_tv_not_free_tv];
 
-Goalw [max_def] "!!n::nat. m < n ==> m < max n n'";
-by (Auto_tac);
-qed "less_maxL";
-
-Goalw [max_def] "!!n::nat. m < n' ==> m < max n n'";
-by (Simp_tac 1);
-by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
-val less_maxR = result();
-
 Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
 by (induct_tac "t" 1);
 by (res_inst_tac [("x","Suc nat")] exI 1);
@@ -546,8 +537,8 @@
 by (REPEAT (etac exE 1));
 by (rename_tac "n'" 1);
 by (res_inst_tac [("x","max n n'")] exI 1);
-by (Simp_tac 1);
-by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
+by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1);
+by (Blast_tac 1);
 qed "fresh_variable_types";
 
 Addsimps [fresh_variable_types];
@@ -561,21 +552,12 @@
 by (REPEAT (etac exE 1));
 by (rename_tac "n'" 1);
 by (res_inst_tac [("x","max n n'")] exI 1);
-by (Simp_tac 1);
-by (fast_tac (claset() addIs [less_maxR,less_maxL]) 1);
+by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1);
+by (Blast_tac 1);
 qed "fresh_variable_type_schemes";
 
 Addsimps [fresh_variable_type_schemes];
 
-Goalw [max_def] "!!n::nat. n <= (max n n')";
-by (Simp_tac 1);
-val le_maxL = result();
-
-Goalw [max_def] "!!n'::nat. n' <= (max n n')";
-by (Simp_tac 1);
-by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
-val le_maxR = result();
-
 Goal "!!A::type_scheme list. ? n. (new_tv n A)";
 by (induct_tac "A" 1);
 by (Simp_tac 1);
@@ -588,7 +570,7 @@
 by (subgoal_tac "n <= (max n n')" 1);
 by (subgoal_tac "n' <= (max n n')" 1);
 by (fast_tac (claset() addDs [new_tv_le]) 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [le_maxR,le_maxL])));
+by (ALLGOALS (simp_tac (simpset() addsimps [le_max_iff_disj])));
 qed "fresh_variable_type_scheme_lists";
 
 Addsimps [fresh_variable_type_scheme_lists];
@@ -600,7 +582,7 @@
 by (subgoal_tac "n1 <= max n1 n2" 1);
 by (subgoal_tac "n2 <= max n1 n2" 1);
 by (fast_tac (claset() addDs [new_tv_le]) 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [le_maxL,le_maxR])));
+by (ALLGOALS (simp_tac (simpset() addsimps [le_max_iff_disj])));
 qed "make_one_new_out_of_two";
 
 Goal "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ). \
@@ -620,7 +602,8 @@
 by (rename_tac "n2 n1" 1);
 by (res_inst_tac [("x","(max n1 n2)")] exI 1);
 by (rewtac new_tv_def);
-by (fast_tac (claset() addIs [less_maxL,less_maxR]) 1);
+by (simp_tac (simpset() addsimps [less_max_iff_disj]) 1);
+by (Blast_tac 1);
 qed "ex_fresh_variable";
 
 (* mgu does not introduce new type variables *)
diff -r 5583261db33d -r fba734ba6894 src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/MiniML/W.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -62,10 +62,6 @@
 by (rtac add_le_mono 1);
  by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [max_def]) 1);
-by (strip_tac 1);
-by (dtac not_leE 1);
-by (rtac less_or_eq_imp_le 1);
-by (Fast_tac 1);
 qed_spec_mp "new_tv_bound_typ_inst_sch";
 
 Addsimps [new_tv_bound_typ_inst_sch];
diff -r 5583261db33d -r fba734ba6894 src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/Ord.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -55,6 +55,13 @@
 (* [| n<m;  ~P ==> m<n |] ==> P *)
 bind_thm ("order_less_asym", order_less_not_sym RS swap);
 
+(* Transitivity *)
+
+Goal "!!x::'a::order. [| x < y; y < z |] ==> x < z";
+by (asm_full_simp_tac (simpset() addsimps [order_less_le]) 1);
+by (blast_tac (claset() addIs [order_trans,order_antisym]) 1);
+qed "order_less_trans";
+
 
 (** Useful for simplification, but too risky to include by default. **)
 
@@ -103,6 +110,12 @@
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_max_iff_disj";
 
+Goalw [max_def] "!!z::'a::linorder. (z < max x y) = (z < x | z < y)";
+by (simp_tac (simpset() addsimps [order_le_less]) 1);
+by (cut_facts_tac [linorder_less_linear] 1);
+by (blast_tac (claset() addIs [order_less_trans]) 1);
+qed "less_max_iff_disj";
+
 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
 by (Simp_tac 1);
 by (cut_facts_tac [linorder_linear] 1);
diff -r 5583261db33d -r fba734ba6894 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/Real/PNat.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -456,7 +456,6 @@
 Goal "m + k <= n --> m <= (n::pnat)";
 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
     sum_Rep_pnat_sum RS sym]) 1);
-by (fast_tac (claset() addIs [add_leD1]) 1);
 qed_spec_mp "pnat_add_leD1";
 
 Goal "!!n::pnat. m + k <= n ==> k <= n";
diff -r 5583261db33d -r fba734ba6894 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOL/ex/Primes.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -47,7 +47,6 @@
 Goal "0<n ==> gcd(m,n) = gcd (n, m mod n)";
 by (rtac (gcd_eq RS trans) 1);
 by (Asm_simp_tac 1);
-by (Blast_tac 1);
 qed "gcd_non_0";
 
 Goal "gcd(m,1) = 1";
diff -r 5583261db33d -r fba734ba6894 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Jan 08 14:02:04 1999 +0100
+++ b/src/HOLCF/Fix.ML	Sat Jan 09 15:24:11 1999 +0100
@@ -689,7 +689,7 @@
         ALLGOALS Asm_simp_tac
         ]);
 
-  val adm_disj_lemma4 = prove_goal Nat.thy
+  val adm_disj_lemma4 = prove_goal Arith.thy
   "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
  (fn _ =>
         [Asm_simp_tac 1]);
@@ -701,10 +701,10 @@
         [
         safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
         atac 2,
-        Asm_simp_tac 1,
         res_inst_tac [("x","i")] exI 1,
-        strip_tac 1,
-        Simp_tac 1
+        Simp_tac 1,
+	strip_tac 1,
+        Asm_simp_tac 1
         ]);
 
   val adm_disj_lemma6 = prove_goal thy