src/Provers/Arith/fast_lin_arith.ML
changeset 16458 4c6fd0c01d28
parent 16358 2e2a506553a3
child 16735 008d089822e3
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  and a simplification procedure
     1.6  
     1.7 -    lin_arith_prover: Sign.sg -> simpset -> term -> thm option
     1.8 +    lin_arith_prover: theory -> simpset -> term -> thm option
     1.9  
    1.10  Only take premises and conclusions into account that are already (negated)
    1.11  (in)equations. lin_arith_prover tries to prove or disprove the term.
    1.12 @@ -34,7 +34,7 @@
    1.13    val neg_prop: term -> term
    1.14    val is_False: thm -> bool
    1.15    val is_nat: typ list * term -> bool
    1.16 -  val mk_nat_thm: Sign.sg -> term -> thm
    1.17 +  val mk_nat_thm: theory -> term -> thm
    1.18  end;
    1.19  (*
    1.20  mk_Eq(~in) = `in == False'
    1.21 @@ -52,7 +52,7 @@
    1.22  signature LIN_ARITH_DATA =
    1.23  sig
    1.24    val decomp:
    1.25 -    Sign.sg -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option
    1.26 +    theory -> term -> ((term*rat)list * rat * string * (term*rat)list * rat * bool)option
    1.27    val number_of: IntInf.int * typ -> term
    1.28  end;
    1.29  (*
    1.30 @@ -77,7 +77,7 @@
    1.31                  -> theory -> theory
    1.32    val trace           : bool ref
    1.33    val fast_arith_neq_limit: int ref
    1.34 -  val lin_arith_prover: Sign.sg -> simpset -> term -> thm option
    1.35 +  val lin_arith_prover: theory -> simpset -> term -> thm option
    1.36    val     lin_arith_tac:     bool -> int -> tactic
    1.37    val cut_lin_arith_tac: thm list -> int -> tactic
    1.38  end;
    1.39 @@ -91,8 +91,8 @@
    1.40  
    1.41  (* data kind 'Provers/fast_lin_arith' *)
    1.42  
    1.43 -structure DataArgs =
    1.44 -struct
    1.45 +structure Data = TheoryDataFun
    1.46 +(struct
    1.47    val name = "Provers/fast_lin_arith";
    1.48    type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    1.49              lessD: thm list, neqE: thm list, simpset: Simplifier.simpset};
    1.50 @@ -100,12 +100,13 @@
    1.51    val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
    1.52                 lessD = [], neqE = [], simpset = Simplifier.empty_ss};
    1.53    val copy = I;
    1.54 -  val prep_ext = I;
    1.55 +  val extend = I;
    1.56  
    1.57 -  fun merge ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    1.58 -              lessD = lessD1, neqE=neqE1, simpset = simpset1},
    1.59 -             {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
    1.60 -              lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
    1.61 +  fun merge _
    1.62 +    ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    1.63 +      lessD = lessD1, neqE=neqE1, simpset = simpset1},
    1.64 +     {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
    1.65 +      lessD = lessD2, neqE=neqE2, simpset = simpset2}) =
    1.66      {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2),
    1.67       mult_mono_thms = Drule.merge_rules (mult_mono_thms1, mult_mono_thms2),
    1.68       inj_thms = Drule.merge_rules (inj_thms1, inj_thms2),
    1.69 @@ -114,9 +115,8 @@
    1.70       simpset = Simplifier.merge_ss (simpset1, simpset2)};
    1.71  
    1.72    fun print _ _ = ();
    1.73 -end;
    1.74 +end);
    1.75  
    1.76 -structure Data = TheoryDataFun(DataArgs);
    1.77  val map_data = Data.map;
    1.78  val setup = [Data.init];
    1.79  
    1.80 @@ -420,7 +420,7 @@
    1.81  in
    1.82  fun mkthm sg asms just =
    1.83    let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
    1.84 -          Data.get_sg sg;
    1.85 +          Data.get sg;
    1.86        val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
    1.87                              map fst lhs  union  (map fst rhs  union  ats))
    1.88                          ([], List.mapPartial (fn thm => if Thm.no_prems thm
    1.89 @@ -625,7 +625,7 @@
    1.90  fun refute_tac(i,justs) =
    1.91    fn state =>
    1.92      let val sg = #sign(rep_thm state)
    1.93 -        val {neqE, ...} = Data.get_sg sg;
    1.94 +        val {neqE, ...} = Data.get sg;
    1.95          fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
    1.96                        METAHYPS (fn asms => rtac (mkthm sg asms j) 1) i
    1.97      in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
    1.98 @@ -691,7 +691,7 @@
    1.99  in (ct1,ct2) end;
   1.100  
   1.101  fun splitasms sg asms =
   1.102 -let val {neqE, ...}  = Data.get_sg sg;
   1.103 +let val {neqE, ...}  = Data.get sg;
   1.104      fun split(asms',[]) = Tip(rev asms')
   1.105        | split(asms',asm::asms) =
   1.106        (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE