# HG changeset patch
# User wenzelm
# Date 1127506913 -7200
# Node ID 072c21e31b420d035c6778c620e2f9b1ab0c248b
# Parent  5b37787d2d9ef36584dcb960f52cc72953285c53
Simplifier.inherit_bounds;

diff -r 5b37787d2d9e -r 072c21e31b42 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Fri Sep 23 22:21:52 2005 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Fri Sep 23 22:21:53 2005 +0200
@@ -22,13 +22,13 @@
   val div_mod_eqs: thm list
   (* (n*(m div n) + m mod n) + k == m + k and
      ((m div n)*n + m mod n) + k == m + k *)
-  val prove_eq_sums: Sign.sg -> term * term -> thm
+  val prove_eq_sums: theory -> simpset -> term * term -> thm
   (* must prove ac0-equivalence of sums *)
 end;
 
 signature CANCEL_DIV_MOD =
 sig
-  val proc: Sign.sg -> simpset -> term -> thm option
+  val proc: theory -> simpset -> term -> thm option
 end;
 
 
@@ -67,16 +67,16 @@
       val m = Data.mk_binop Data.mod_name pq
   in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
 
-fun cancel sg t pq =
-  let val teqt' = Data.prove_eq_sums sg (t, rearrange t pq)
+fun cancel thy ss t pq =
+  let val teqt' = Data.prove_eq_sums thy ss (t, rearrange t pq)
   in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
 
-fun proc sg _ t =
+fun proc thy ss t =
   let val (divs,mods) = coll_div_mod t ([],[])
   in if null divs orelse null mods then NONE
      else case divs inter mods of
-            pq :: _ => SOME(cancel sg t pq)
+            pq :: _ => SOME(cancel thy ss t pq)
           | [] => NONE
   end
 
-end
\ No newline at end of file
+end
diff -r 5b37787d2d9e -r 072c21e31b42 src/Provers/Arith/cancel_sums.ML
--- a/src/Provers/Arith/cancel_sums.ML	Fri Sep 23 22:21:52 2005 +0200
+++ b/src/Provers/Arith/cancel_sums.ML	Fri Sep 23 22:21:53 2005 +0200
@@ -17,14 +17,14 @@
   val mk_bal: term * term -> term
   val dest_bal: term -> term * term
   (*rules*)
-  val prove_conv: tactic -> tactic -> Sign.sg -> term * term -> thm
-  val norm_tac: tactic                   	(*AC0 etc.*)
-  val uncancel_tac: cterm -> tactic      	(*apply A ~~ B  ==  x + A ~~ x + B*)
+  val prove_conv: tactic -> (simpset -> tactic) -> theory -> simpset -> term * term -> thm
+  val norm_tac: simpset -> tactic            (*AC0 etc.*)
+  val uncancel_tac: cterm -> tactic          (*apply A ~~ B  ==  x + A ~~ x + B*)
 end;
 
 signature CANCEL_SUMS =
 sig
-  val proc: Sign.sg -> simpset -> term -> thm option
+  val proc: theory -> simpset -> term -> thm option
 end;
 
 
@@ -51,14 +51,14 @@
 (* uncancel *)
 
 fun uncancel_sums_tac _ [] = all_tac
-  | uncancel_sums_tac sg (t :: ts) =
-      Data.uncancel_tac (Thm.cterm_of sg t) THEN
-      uncancel_sums_tac sg ts;
+  | uncancel_sums_tac thy (t :: ts) =
+      Data.uncancel_tac (Thm.cterm_of thy t) THEN
+      uncancel_sums_tac thy ts;
 
 
 (* the simplification procedure *)
 
-fun proc sg _ t =
+fun proc thy ss t =
   (case try Data.dest_bal t of
     NONE => NONE
   | SOME bal =>
@@ -68,7 +68,7 @@
       in
         if null vs then NONE
         else SOME
-          (Data.prove_conv (uncancel_sums_tac sg vs) Data.norm_tac sg
+          (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac thy ss
             (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
       end);
 
diff -r 5b37787d2d9e -r 072c21e31b42 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Sep 23 22:21:52 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Sep 23 22:21:53 2005 +0200
@@ -80,7 +80,7 @@
   val fast_arith_neq_limit: int ref
   val lin_arith_prover: theory -> simpset -> term -> thm option
   val     lin_arith_tac:     bool -> int -> tactic
-  val cut_lin_arith_tac: thm list -> int -> tactic
+  val cut_lin_arith_tac: simpset -> int -> tactic
 end;
 
 functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC 
@@ -619,12 +619,12 @@
 
 fun refute sg ps ex items = refutes sg ps ex (split_items items) [];
 
-fun refute_tac(i,justs) =
+fun refute_tac ss (i,justs) =
   fn state =>
     let val sg = #sign(rep_thm state)
         val {neqE, ...} = Data.get sg;
         fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
-                      METAHYPS (fn asms => rtac (mkthm (sg, Simplifier.empty_ss) asms j) 1) i
+          METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
     in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
        EVERY(map just1 justs)
     end
@@ -654,7 +654,7 @@
 Fast but very incomplete decider. Only premises and conclusions
 that are already (negated) (in)equations are taken into account.
 *)
-fun lin_arith_tac ex i st = SUBGOAL (fn (A,_) =>
+fun simpset_lin_arith_tac ss ex i st = SUBGOAL (fn (A,_) =>
   let val params = rev(Logic.strip_params A)
       val pTs = map snd params
       val Hs = Logic.strip_assums_hyp A
@@ -662,10 +662,14 @@
   in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
      case prove (Thm.sign_of_thm st) (pTs,params) ex Hs concl of
        NONE => (trace_msg "Refutation failed."; no_tac)
-     | SOME js => (trace_msg "Refutation succeeded."; refute_tac(i,js))
+     | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
   end) i st;
 
-fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac false i;
+val lin_arith_tac = simpset_lin_arith_tac Simplifier.empty_ss;
+
+fun cut_lin_arith_tac ss i =
+  cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
+  simpset_lin_arith_tac ss false i;
 
 (** Forward proof from theorems **)