made mult_mono_thms generic.

--- a/src/HOL/Hyperreal/hypreal_arith.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -8,26 +8,11 @@
 Instantiation of the generic linear arithmetic package for type hypreal.
 *)
 
-(*FIXME DELETE*)
-val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
-
-val hypreal_mult_left_mono =
-    read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono;
-
-
 (****Instantiation of the generic linear arithmetic package****)
 
 
 local
 
-fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
-
-val hypreal_mult_mono_thms =
- [(rotate_prems 1 hypreal_mult_less_mono2,
-   cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))),
-  (hypreal_mult_left_mono,
-   cvar(hypreal_mult_left_mono, hd(tl(prems_of hypreal_mult_left_mono))))]
-
 val real_inj_thms = [hypreal_of_real_le_iff RS iffD2, 
                      hypreal_of_real_less_iff RS iffD2,
                      hypreal_of_real_eq_iff RS iffD2];
@@ -45,7 +30,7 @@
 val hypreal_arith_setup =
  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    {add_mono_thms = add_mono_thms,
-    mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms,
+    mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms @ real_inj_thms, 
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
     simpset = simpset}),

--- a/src/HOL/Integ/int_arith1.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -516,7 +516,7 @@
 val int_arith_setup =
  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    {add_mono_thms = add_mono_thms,
-    mult_mono_thms = mult_mono_thms,
+    mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
     inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
     lessD = lessD @ [zless_imp_add1_zle],
     simpset = simpset addsimps add_rules

--- a/src/HOL/Real/rat_arith.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/HOL/Real/rat_arith.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -8,29 +8,12 @@
 Instantiation of the generic linear arithmetic package for type rat.
 *)
 
-(*FIXME: these monomorphic versions are necessary because of a bug in the arith
-  procedure*)
-val rat_mult_strict_left_mono =
-    read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono;
-
-val rat_mult_left_mono =
- read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono;
-
-
 (****Instantiation of the generic linear arithmetic package for fields****)
 
 local
 
 val simprocs = field_cancel_numeral_factors
 
-fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
-
-val rat_mult_mono_thms =
- [(rat_mult_strict_left_mono,
-   cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))),
-  (rat_mult_left_mono,
-   cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))]
-
 val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
              inst "a" "(number_of ?v)" right_distrib,
              divide_1, divide_zero_left,
@@ -57,7 +40,7 @@
 val rat_arith_setup =
  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    {add_mono_thms = add_mono_thms,
-    mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms,
+    mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ inj_thms,
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
     simpset = simpset addsimps simps

--- a/src/HOL/Real/real_arith.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/HOL/Real/real_arith.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -8,10 +8,6 @@
 Instantiation of the generic linear arithmetic package for type real.
 *)
 
-(*FIXME DELETE*)
-val real_mult_left_mono =
-    read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono;
-
 val real_le_def = thm "real_le_def";
 val real_diff_def = thm "real_diff_def";
 val real_divide_def = thm "real_divide_def";
@@ -102,14 +98,6 @@
 
 local
 
-fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
-
-val real_mult_mono_thms =
- [(rotate_prems 1 real_mult_less_mono2,
-   cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
-  (real_mult_left_mono,
-   cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))]
-
 val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
        real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
        real_of_int_minus RS sym, real_of_int_diff RS sym,
@@ -132,7 +120,7 @@
 val real_arith_setup =
  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    {add_mono_thms = add_mono_thms,
-    mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
+    mult_mono_thms = mult_mono_thms,
     inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
     simpset = simpset addsimps simps}),

--- a/src/HOL/arith_data.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/HOL/arith_data.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -393,7 +393,8 @@
 *)
 val add_rules =
  [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
-  One_nat_def,isolateSuc];
+  One_nat_def,isolateSuc,
+  order_less_irrefl];
 
 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
  (fn prems => [cut_facts_tac prems 1,

--- a/src/HOL/simpdata.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/HOL/simpdata.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -338,17 +338,18 @@
    where the Ai are atomic, i.e. no top-level &, | or EX
 *)
 
-fun refute_tac test prep_tac ref_tac =
-  let val nnf_simps =
+local
+  val nnf_simps =
         [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
          not_all,not_ex,not_not];
-      val nnf_simpset =
+  val nnf_simpset =
         empty_ss setmkeqTrue mk_eq_True
                  setmksimps (mksimps mksimps_pairs)
                  addsimps nnf_simps;
-      val prem_nnf_tac = full_simp_tac nnf_simpset;
-
-      val refute_prems_tac =
+  val prem_nnf_tac = full_simp_tac nnf_simpset
+in
+fun refute_tac test prep_tac ref_tac =
+  let val refute_prems_tac =
         REPEAT_DETERM
               (eresolve_tac [conjE, exE] 1 ORELSE
                filter_prems_tac test 1 ORELSE
@@ -359,3 +360,4 @@
             REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   end;
+end;
\ No newline at end of file

--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Sep 06 16:45:10 2004 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Sep 06 17:37:35 2004 +0200
@@ -71,9 +71,9 @@
 signature FAST_LIN_ARITH =
 sig
   val setup: (theory -> theory) list
-  val map_data: ({add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list,
+  val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
                  lessD: thm list, simpset: Simplifier.simpset}
-                 -> {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list,
+                 -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
                      lessD: thm list, simpset: Simplifier.simpset})
                 -> theory -> theory
   val trace           : bool ref
@@ -95,7 +95,7 @@
 structure DataArgs =
 struct
   val name = "Provers/fast_lin_arith";
-  type T = {add_mono_thms: thm list, mult_mono_thms: (thm*cterm)list, inj_thms: thm list,
+  type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
             lessD: thm list, simpset: Simplifier.simpset};
 
   val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
@@ -108,8 +108,7 @@
              {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
               lessD = lessD2, simpset = simpset2}) =
     {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
-     mult_mono_thms = gen_merge_lists' (Drule.eq_thm_prop o pairself fst)
-       mult_mono_thms1 mult_mono_thms2,
+     mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
      inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
      lessD = Drule.merge_rules (lessD1, lessD2),
      simpset = Simplifier.merge_ss (simpset1, simpset2)};
@@ -450,12 +449,20 @@
       fun multn(n,thm) =
         let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
         in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
-
+(*
       fun multn2(n,thm) =
         let val Some(mth,cv) =
               get_first (fn (th,cv) => Some(thm RS th,cv) handle THM _ => None) mult_mono_thms
             val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
         in instantiate ([],[(cv,ct)]) mth end
+*)
+      fun multn2(n,thm) =
+        let val Some(mth) =
+              get_first (fn th => Some(thm RS th) handle THM _ => None) mult_mono_thms
+            fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
+            val cv = cvar(mth, hd(prems_of mth));
+            val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
+        in instantiate ([],[(cv,ct)]) mth end
 
       fun simp thm =
         let val thm' = trace_thm "Simplified:" (full_simplify simpset thm)