fast_lin_arith uses proper multiplication instead of unfolding to additions
authorboehmes
Mon Jun 08 22:29:37 2009 +0200 (2009-06-08)
changeset 31510e0f2bb4b0021
parent 31509 00ede188c5d6
child 31511 dd989ea86cf0
child 31512 27118561c2e0
fast_lin_arith uses proper multiplication instead of unfolding to additions
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Tools/int_arith.ML	Mon Jun 08 20:43:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Mon Jun 08 22:29:37 2009 +0200
     1.3 @@ -87,6 +87,12 @@
     1.4  val global_setup = Simplifier.map_simpset
     1.5    (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
     1.6  
     1.7 +
     1.8 +fun number_of thy T n =
     1.9 +  if not (Sign.of_sort thy (T, @{sort number}))
    1.10 +  then raise CTERM ("number_of", [])
    1.11 +  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
    1.12 +
    1.13  val setup =
    1.14    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
    1.15    #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
    1.16 @@ -95,6 +101,7 @@
    1.17    #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc
    1.18        :: Numeral_Simprocs.combine_numerals
    1.19        :: Numeral_Simprocs.cancel_numerals)
    1.20 +  #> Lin_Arith.set_number_of number_of
    1.21    #> Lin_Arith.add_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT)
    1.22    #> Lin_Arith.add_discrete_type @{type_name Int.int}
    1.23  
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Mon Jun 08 20:43:57 2009 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Mon Jun 08 22:29:37 2009 +0200
     2.3 @@ -16,6 +16,8 @@
     2.4    val add_simprocs: simproc list -> Context.generic -> Context.generic
     2.5    val add_inj_const: string * typ -> Context.generic -> Context.generic
     2.6    val add_discrete_type: string -> Context.generic -> Context.generic
     2.7 +  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic ->
     2.8 +    Context.generic
     2.9    val setup: Context.generic -> Context.generic
    2.10    val global_setup: theory -> theory
    2.11    val split_limit: int Config.T
    2.12 @@ -36,6 +38,7 @@
    2.13  val conjI = conjI;
    2.14  val notI = notI;
    2.15  val sym = sym;
    2.16 +val trueI = TrueI;
    2.17  val not_lessD = @{thm linorder_not_less} RS iffD1;
    2.18  val not_leD = @{thm linorder_not_le} RS iffD1;
    2.19  
    2.20 @@ -274,7 +277,6 @@
    2.21    | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
    2.22    | domain_is_nat _                                                 = false;
    2.23  
    2.24 -val mk_number = HOLogic.mk_number;
    2.25  
    2.26  (*---------------------------------------------------------------------------*)
    2.27  (* the following code performs splitting of certain constants (e.g. min,     *)
    2.28 @@ -752,23 +754,30 @@
    2.29  
    2.30  val map_data = Fast_Arith.map_data;
    2.31  
    2.32 -fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
    2.33 +fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.34    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
    2.35 -    lessD = lessD, neqE = neqE, simpset = simpset};
    2.36 +    lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
    2.37  
    2.38 -fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
    2.39 +fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.40    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    2.41 -    lessD = f lessD, neqE = neqE, simpset = simpset};
    2.42 +    lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
    2.43  
    2.44 -fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =
    2.45 +fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.46    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    2.47 -    lessD = lessD, neqE = neqE, simpset = f simpset};
    2.48 +    lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
    2.49 +
    2.50 +fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.51 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    2.52 +    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
    2.53  
    2.54  fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
    2.55  fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
    2.56  fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
    2.57  fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
    2.58  
    2.59 +fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f)))
    2.60 +
    2.61 +
    2.62  fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    2.63  val lin_arith_tac = Fast_Arith.lin_arith_tac;
    2.64  val trace = Fast_Arith.trace;
    2.65 @@ -778,13 +787,16 @@
    2.66     Most of the work is done by the cancel tactics. *)
    2.67  
    2.68  val init_arith_data =
    2.69 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    2.70 +  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, number_of, ...} =>
    2.71     {add_mono_thms = @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field} @ add_mono_thms,
    2.72 -    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms,
    2.73 +    mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} ::
    2.74 +      @{lemma "a = b ==> c*a = c*b" by (rule arg_cong)} :: mult_mono_thms,
    2.75      inj_thms = inj_thms,
    2.76      lessD = lessD @ [@{thm "Suc_leI"}],
    2.77      neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}],
    2.78      simpset = HOL_basic_ss
    2.79 +      addsimps @{thms ring_distribs}
    2.80 +      addsimps [@{thm if_True}, @{thm if_False}]
    2.81        addsimps
    2.82         [@{thm "monoid_add_class.add_0_left"},
    2.83          @{thm "monoid_add_class.add_0_right"},
    2.84 @@ -795,7 +807,8 @@
    2.85        addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv]
    2.86         (*abel_cancel helps it work in abstract algebraic domains*)
    2.87        addsimprocs Nat_Arith.nat_cancel_sums_add
    2.88 -      addcongs [if_weak_cong]}) #>
    2.89 +      addcongs [if_weak_cong],
    2.90 +    number_of = number_of}) #>
    2.91    add_discrete_type @{type_name nat};
    2.92  
    2.93  fun add_arith_facts ss =
     3.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jun 08 20:43:57 2009 +0200
     3.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Jun 08 22:29:37 2009 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      Provers/Arith/fast_lin_arith.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Tobias Nipkow and Tjark Weber
     3.7 +    Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
     3.8  
     3.9  A generic linear arithmetic package.  It provides two tactics
    3.10  (cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
    3.11 @@ -21,6 +21,7 @@
    3.12    val not_lessD   : thm  (* ~(m < n) ==> n <= m *)
    3.13    val not_leD     : thm  (* ~(m <= n) ==> n < m *)
    3.14    val sym         : thm  (* x = y ==> y = x *)
    3.15 +  val trueI       : thm  (* True *)
    3.16    val mk_Eq       : thm -> thm
    3.17    val atomize     : thm -> thm list
    3.18    val mk_Trueprop : term -> term
    3.19 @@ -56,7 +57,6 @@
    3.20  
    3.21    (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
    3.22    val pre_tac: Proof.context -> int -> tactic
    3.23 -  val mk_number: typ -> int -> term
    3.24  
    3.25    (*the limit on the number of ~= allowed; because each ~= is split
    3.26      into two cases, this can lead to an explosion*)
    3.27 @@ -90,9 +90,11 @@
    3.28    val lin_arith_tac: Proof.context -> bool -> int -> tactic
    3.29    val lin_arith_simproc: simpset -> term -> thm option
    3.30    val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    3.31 -                 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
    3.32 +                 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
    3.33 +                 number_of : serial * (theory -> typ -> int -> cterm)}
    3.34                   -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    3.35 -                     lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
    3.36 +                     lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
    3.37 +                     number_of : serial * (theory -> typ -> int -> cterm)})
    3.38                  -> Context.generic -> Context.generic
    3.39    val trace: bool ref
    3.40    val warning_count: int ref;
    3.41 @@ -105,6 +107,8 @@
    3.42  
    3.43  (** theory data **)
    3.44  
    3.45 +fun no_number_of _ _ _ = raise CTERM ("number_of", [])
    3.46 +
    3.47  structure Data = GenericDataFun
    3.48  (
    3.49    type T =
    3.50 @@ -113,22 +117,27 @@
    3.51      inj_thms: thm list,
    3.52      lessD: thm list,
    3.53      neqE: thm list,
    3.54 -    simpset: Simplifier.simpset};
    3.55 +    simpset: Simplifier.simpset,
    3.56 +    number_of : serial * (theory -> typ -> int -> cterm)};
    3.57  
    3.58    val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
    3.59 -               lessD = [], neqE = [], simpset = Simplifier.empty_ss};
    3.60 +               lessD = [], neqE = [], simpset = Simplifier.empty_ss,
    3.61 +               number_of = (serial (), no_number_of) };
    3.62    val extend = I;
    3.63    fun merge _
    3.64      ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    3.65 -      lessD = lessD1, neqE=neqE1, simpset = simpset1},
    3.66 +      lessD = lessD1, neqE=neqE1, simpset = simpset1,
    3.67 +      number_of = (number_of1 as (s1, _))},
    3.68       {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
    3.69 -      lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
    3.70 +      lessD = lessD2, neqE=neqE2, simpset = simpset2,
    3.71 +      number_of = (number_of2 as (s2, _))}) =
    3.72      {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
    3.73       mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
    3.74       inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
    3.75       lessD = Thm.merge_thms (lessD1, lessD2),
    3.76       neqE = Thm.merge_thms (neqE1, neqE2),
    3.77 -     simpset = Simplifier.merge_ss (simpset1, simpset2)};
    3.78 +     simpset = Simplifier.merge_ss (simpset1, simpset2),
    3.79 +     number_of = if s1 > s2 then number_of1 else number_of2};
    3.80  );
    3.81  
    3.82  val map_data = Data.map;
    3.83 @@ -320,7 +329,7 @@
    3.84          else (m1,m2)
    3.85        val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1)
    3.86                      then (~n1,~n2) else (n1,n2)
    3.87 -  in add_ineq (multiply_ineq n1 i1) (multiply_ineq n2 i2) end;
    3.88 +  in add_ineq (multiply_ineq p1 i1) (multiply_ineq p2 i2) end;
    3.89  
    3.90  (* ------------------------------------------------------------------------- *)
    3.91  (* The main refutation-finding code.                                         *)
    3.92 @@ -328,7 +337,7 @@
    3.93  
    3.94  fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l;
    3.95  
    3.96 -fun is_answer (ans as Lineq(k,ty,l,_)) =
    3.97 +fun is_contradictory (ans as Lineq(k,ty,l,_)) =
    3.98    case ty  of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0;
    3.99  
   3.100  fun calc_blowup l =
   3.101 @@ -347,13 +356,10 @@
   3.102  (* blowup (number of consequences generated) and eliminates it.              *)
   3.103  (* ------------------------------------------------------------------------- *)
   3.104  
   3.105 -fun allpairs f xs ys =
   3.106 -  maps (fn x => map (fn y => f x y) ys) xs;
   3.107 -
   3.108  fun extract_first p =
   3.109 -  let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
   3.110 -                               else extract (y::xs) ys
   3.111 -        | extract xs []      = (NONE,xs)
   3.112 +  let
   3.113 +    fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
   3.114 +      | extract xs [] = raise Empty
   3.115    in extract [] end;
   3.116  
   3.117  fun print_ineqs ineqs =
   3.118 @@ -368,10 +374,10 @@
   3.119  datatype result = Success of injust | Failure of history;
   3.120  
   3.121  fun elim (ineqs, hist) =
   3.122 -  let val dummy = print_ineqs ineqs
   3.123 +  let val _ = print_ineqs ineqs
   3.124        val (triv, nontriv) = List.partition is_trivial ineqs in
   3.125    if not (null triv)
   3.126 -  then case Library.find_first is_answer triv of
   3.127 +  then case Library.find_first is_contradictory triv of
   3.128           NONE => elim (nontriv, hist)
   3.129         | SOME(Lineq(_,_,_,j)) => Success j
   3.130    else
   3.131 @@ -379,11 +385,12 @@
   3.132    else
   3.133    let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
   3.134    if not (null eqs) then
   3.135 -     let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
   3.136 -         val sclist = sort (fn (x,y) => int_ord (abs x, abs y))
   3.137 -                           (List.filter (fn i => i<>0) clist)
   3.138 -         val c = hd sclist
   3.139 -         val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
   3.140 +     let val c =
   3.141 +           fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs []
   3.142 +           |> filter (fn i => i <> 0)
   3.143 +           |> sort (int_ord o pairself abs)
   3.144 +           |> hd
   3.145 +         val (eq as Lineq(_,_,ceq,_),othereqs) =
   3.146                 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
   3.147           val v = find_index_eq c ceq
   3.148           val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
   3.149 @@ -402,7 +409,7 @@
   3.150       let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows)
   3.151           val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs
   3.152           val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes
   3.153 -     in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end
   3.154 +     in elim(no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end
   3.155    end
   3.156    end
   3.157    end;
   3.158 @@ -427,11 +434,12 @@
   3.159  val union_bterm = curry (gen_union
   3.160    (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')));
   3.161  
   3.162 -(* FIXME OPTIMIZE!!!! (partly done already)
   3.163 -   Addition/Multiplication need i*t representation rather than t+t+...
   3.164 -   Get rid of Mulitplied(2). For Nat LA_Data.mk_number should return Suc^n
   3.165 -   because Numerals are not known early enough.
   3.166 +fun add_atoms (lhs, _, _, rhs, _, _) =
   3.167 +  union_term (map fst lhs) o union_term (map fst rhs);
   3.168  
   3.169 +fun atoms_of ds = fold add_atoms ds [];
   3.170 +
   3.171 +(*
   3.172  Simplification may detect a contradiction 'prematurely' due to type
   3.173  information: n+1 <= 0 is simplified to False and does not need to be crossed
   3.174  with 0 <= n.
   3.175 @@ -444,58 +452,78 @@
   3.176    let
   3.177      val ctxt = Simplifier.the_context ss;
   3.178      val thy = ProofContext.theory_of ctxt;
   3.179 -    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt;
   3.180 +    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset,
   3.181 +      number_of = (_, num_of), ...} = get_data ctxt;
   3.182      val simpset' = Simplifier.inherit_context ss simpset;
   3.183 -    val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
   3.184 -                            union_term (map fst lhs) (union_term (map fst rhs) ats))
   3.185 -                        ([], List.mapPartial (fn thm => if Thm.no_prems thm
   3.186 -                                              then LA_Data.decomp ctxt (Thm.concl_of thm)
   3.187 -                                              else NONE) asms)
   3.188 +    fun only_concl f thm =
   3.189 +      if Thm.no_prems thm then f (Thm.concl_of thm) else NONE;
   3.190 +    val atoms = atoms_of (map_filter (only_concl (LA_Data.decomp ctxt)) asms);
   3.191 +
   3.192 +    fun use_first rules thm =
   3.193 +      get_first (fn th => SOME (thm RS th) handle THM _ => NONE) rules
   3.194 +
   3.195 +    fun add2 thm1 thm2 =
   3.196 +      use_first add_mono_thms (thm1 RS (thm2 RS LA_Logic.conjI));
   3.197 +    fun try_add thms thm = get_first (fn th => add2 th thm) thms;
   3.198  
   3.199 -      fun add2 thm1 thm2 =
   3.200 -        let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
   3.201 -        in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms
   3.202 -        end;
   3.203 -      fun try_add [] _ = NONE
   3.204 -        | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
   3.205 -             NONE => try_add thm1s thm2 | some => some;
   3.206 +    fun add_thms thm1 thm2 =
   3.207 +      (case add2 thm1 thm2 of
   3.208 +        NONE =>
   3.209 +          (case try_add ([thm1] RL inj_thms) thm2 of
   3.210 +            NONE =>
   3.211 +              (the (try_add ([thm2] RL inj_thms) thm1)
   3.212 +                handle Option =>
   3.213 +                  (trace_thm "" thm1; trace_thm "" thm2;
   3.214 +                   sys_error "Linear arithmetic: failed to add thms"))
   3.215 +          | SOME thm => thm)
   3.216 +      | SOME thm => thm);
   3.217 +
   3.218 +    fun mult_by_add n thm =
   3.219 +      let fun mul i th = if i = 1 then th else mul (i - 1) (add_thms thm th)
   3.220 +      in mul n thm end;
   3.221  
   3.222 -      fun addthms thm1 thm2 =
   3.223 -        case add2 thm1 thm2 of
   3.224 -          NONE => (case try_add ([thm1] RL inj_thms) thm2 of
   3.225 -                     NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
   3.226 -                               handle Option =>
   3.227 -                               (trace_thm "" thm1; trace_thm "" thm2;
   3.228 -                                sys_error "Linear arithmetic: failed to add thms")
   3.229 -                             )
   3.230 -                   | SOME thm => thm)
   3.231 -        | SOME thm => thm;
   3.232 -
   3.233 -      fun multn(n,thm) =
   3.234 -        let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
   3.235 -        in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
   3.236 +    val rewr = Simplifier.rewrite simpset';
   3.237 +    val rewrite_concl = Conv.fconv_rule (Conv.concl_conv ~1 (Conv.arg_conv
   3.238 +      (Conv.binop_conv rewr)));
   3.239 +    fun discharge_prem thm = if Thm.nprems_of thm = 0 then thm else
   3.240 +      let val cv = Conv.arg1_conv (Conv.arg_conv rewr)
   3.241 +      in Thm.implies_elim (Conv.fconv_rule cv thm) LA_Logic.trueI end
   3.242  
   3.243 -      fun multn2(n,thm) =
   3.244 -        let val SOME(mth) =
   3.245 -              get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
   3.246 -            fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
   3.247 -            val cv = cvar(mth, hd(prems_of mth));
   3.248 -            val ct = cterm_of thy (LA_Data.mk_number (#T (rep_cterm cv)) n)
   3.249 -        in instantiate ([],[(cv,ct)]) mth end
   3.250 +    fun mult n thm =
   3.251 +      (case use_first mult_mono_thms thm of
   3.252 +        NONE => mult_by_add n thm
   3.253 +      | SOME mth =>
   3.254 +          let
   3.255 +            val cv = mth |> Thm.cprop_of |> Drule.strip_imp_concl
   3.256 +              |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg1
   3.257 +            val T = #T (Thm.rep_cterm cv)
   3.258 +          in
   3.259 +            mth
   3.260 +            |> Thm.instantiate ([], [(cv, num_of thy T n)])
   3.261 +            |> rewrite_concl
   3.262 +            |> discharge_prem
   3.263 +            handle CTERM _ => mult_by_add n thm
   3.264 +                 | THM _ => mult_by_add n thm
   3.265 +          end);
   3.266  
   3.267 -      fun simp thm =
   3.268 -        let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
   3.269 -        in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
   3.270 +    fun mult_thm (n, thm) =
   3.271 +      if n = ~1 then thm RS LA_Logic.sym
   3.272 +      else if n < 0 then mult (~n) thm RS LA_Logic.sym
   3.273 +      else mult n thm;
   3.274 +
   3.275 +    fun simp thm =
   3.276 +      let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
   3.277 +      in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end;
   3.278  
   3.279 -      fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
   3.280 -        | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   3.281 -        | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
   3.282 -        | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
   3.283 -        | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   3.284 -        | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
   3.285 -        | mk (Added (j1, j2))     = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
   3.286 -        | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (multn (n, mk j)))
   3.287 -        | mk (Multiplied2 (n, j)) = simp (trace_msg ("**" ^ string_of_int n); trace_thm "**" (multn2 (n, mk j)))
   3.288 +    fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i)
   3.289 +      | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i))
   3.290 +      | mk (LessD j)            = trace_thm "L" (hd ([mk j] RL lessD))
   3.291 +      | mk (NotLeD j)           = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
   3.292 +      | mk (NotLeDD j)          = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD))
   3.293 +      | mk (NotLessD j)         = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
   3.294 +      | mk (Added (j1, j2))     = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
   3.295 +      | mk (Multiplied (n, j))  = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
   3.296 +      | mk (Multiplied2 (n, j)) = (trace_msg ("**" ^ string_of_int n); trace_thm "**" (mult_thm (n, mk j)))
   3.297  
   3.298    in
   3.299      let
   3.300 @@ -676,9 +704,6 @@
   3.301    result
   3.302  end;
   3.303  
   3.304 -fun add_atoms (ats : term list, ((lhs,_,_,rhs,_,_) : LA_Data.decomp, _)) : term list =
   3.305 -    union_term (map fst lhs) (union_term (map fst rhs) ats);
   3.306 -
   3.307  fun add_datoms (dats : (bool * term) list, ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _)) :
   3.308    (bool * term) list =
   3.309    union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats);
   3.310 @@ -691,7 +716,7 @@
   3.311    let
   3.312      fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) =
   3.313            let
   3.314 -            val atoms = Library.foldl add_atoms ([], initems)
   3.315 +            val atoms = atoms_of (map fst initems)
   3.316              val n = length atoms
   3.317              val mkleq = mklineq n atoms
   3.318              val ixs = 0 upto (n - 1)