mk_number replaces number_of
authorhaftmann
Mon May 11 15:57:30 2009 +0200 (2009-05-11)
changeset 31102f1e3100e6c49
parent 31101 26c7bb764a38
child 31103 9820999467a7
mk_number replaces number_of
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon May 11 15:57:29 2009 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon May 11 15:57:30 2009 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5    (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*)
     1.6    val pre_tac: Proof.context -> int -> tactic
     1.7 -  val number_of: int * typ -> term
     1.8 +  val mk_number: typ -> int -> term
     1.9  
    1.10    (*the limit on the number of ~= allowed; because each ~= is split
    1.11      into two cases, this can lead to an explosion*)
    1.12 @@ -86,6 +86,9 @@
    1.13  
    1.14  signature FAST_LIN_ARITH =
    1.15  sig
    1.16 +  val cut_lin_arith_tac: simpset -> int -> tactic
    1.17 +  val lin_arith_tac: Proof.context -> bool -> int -> tactic
    1.18 +  val lin_arith_simproc: simpset -> term -> thm option
    1.19    val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    1.20                   lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
    1.21                   -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    1.22 @@ -93,9 +96,6 @@
    1.23                  -> Context.generic -> Context.generic
    1.24    val trace: bool ref
    1.25    val warning_count: int ref;
    1.26 -  val cut_lin_arith_tac: simpset -> int -> tactic
    1.27 -  val lin_arith_tac: Proof.context -> bool -> int -> tactic
    1.28 -  val lin_arith_simproc: simpset -> term -> thm option
    1.29  end;
    1.30  
    1.31  functor Fast_Lin_Arith
    1.32 @@ -429,7 +429,7 @@
    1.33  
    1.34  (* FIXME OPTIMIZE!!!! (partly done already)
    1.35     Addition/Multiplication need i*t representation rather than t+t+...
    1.36 -   Get rid of Mulitplied(2). For Nat LA_Data.number_of should return Suc^n
    1.37 +   Get rid of Mulitplied(2). For Nat LA_Data.mk_number should return Suc^n
    1.38     because Numerals are not known early enough.
    1.39  
    1.40  Simplification may detect a contradiction 'prematurely' due to type
    1.41 @@ -480,7 +480,7 @@
    1.42                get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
    1.43              fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
    1.44              val cv = cvar(mth, hd(prems_of mth));
    1.45 -            val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv)))
    1.46 +            val ct = cterm_of thy (LA_Data.mk_number (#T (rep_cterm cv)) n)
    1.47          in instantiate ([],[(cv,ct)]) mth end
    1.48  
    1.49        fun simp thm =