# HG changeset patch # User wenzelm # Date 964475309 -7200 # Node ID d4e9f60fe25af0d75a7b36d21c53df264cbe85f3 # Parent e46de4af70e41d9ca61a252c8b3687597d69cc83 avoid global references; diff -r e46de4af70e4 -r d4e9f60fe25a src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Mon Jul 24 23:47:57 2000 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Jul 24 23:48:29 2000 +0200 @@ -52,12 +52,8 @@ signature LIN_ARITH_DATA = sig - val add_mono_thms: thm list ref - (* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *) - val lessD: thm list ref (* m < n ==> m+1 <= n *) val decomp: - term -> ((term*int)list * int * string * (term*int)list * int * bool)option - val ss_ref: simpset ref + Sign.sg -> term -> ((term*int)list * int * string * (term*int)list * int * bool)option end; (* decomp(`x Rel y') should yield (p,i,Rel,q,j,d) @@ -66,13 +62,17 @@ of summand * multiplicity pairs and a constant summand and d indicates if the domain is discrete. -ss_ref must reduce contradictory <= to False. +ss must reduce contradictory <= to False. It should also cancel common summands to keep <= reduced; otherwise <= can grow to massive proportions. *) signature FAST_LIN_ARITH = sig + val setup: (theory -> theory) list + val map_data: ({add_mono_thms: thm list, lessD: thm list, simpset: Simplifier.simpset} + -> {add_mono_thms: thm list, lessD: thm list, simpset: Simplifier.simpset}) + -> theory -> theory val trace : bool ref val lin_arith_prover: Sign.sg -> thm list -> term -> thm option val lin_arith_tac: int -> tactic @@ -83,6 +83,35 @@ and LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH = struct + +(** theory data **) + +(* data kind 'Provers/fast_lin_arith' *) + +structure DataArgs = +struct + val name = "Provers/fast_lin_arith"; + type T = {add_mono_thms: thm list, lessD: thm list, simpset: Simplifier.simpset}; + + val empty = {add_mono_thms = [], lessD = [], simpset = Simplifier.empty_ss}; + val copy = I; + val prep_ext = I; + + fun merge ({add_mono_thms = add_mono_thms1, lessD = lessD1, simpset = simpset1}, + {add_mono_thms = add_mono_thms2, lessD = lessD2, simpset = simpset2}) = + {add_mono_thms = Drule.merge_rules (add_mono_thms1, add_mono_thms2), + lessD = Drule.merge_rules (lessD1, lessD2), + simpset = Simplifier.merge_ss (simpset1, simpset2)}; + + fun print _ _ = (); +end; + +structure Data = TheoryDataFun(DataArgs); +val map_data = Data.map; +val setup = [Data.init]; + + + (*** A fast decision procedure ***) (*** Code ported from HOL Light ***) (* possible optimizations: @@ -263,14 +292,14 @@ exception FalseE of thm in fun mkthm sg asms just = - let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) => + let val {add_mono_thms, lessD, simpset} = Data.get_sg sg; + val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) => map fst lhs union (map fst rhs union ats)) - ([], mapfilter (LA_Data.decomp o concl_of) asms) + ([], mapfilter (LA_Data.decomp sg o concl_of) asms) fun addthms thm1 thm2 = let val conj = thm1 RS (thm2 RS LA_Logic.conjI) - in the(get_first (fn th => Some(conj RS th) handle _ => None) - (!LA_Data.add_mono_thms)) + in the(get_first (fn th => Some(conj RS th) handle _ => None) add_mono_thms) end; fun multn(n,thm) = @@ -278,22 +307,21 @@ in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; fun simp thm = - let val thm' = simplify (!LA_Data.ss_ref) thm + let val thm' = simplify simpset thm in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end fun mk(Asm i) = trace_thm "Asm" (nth_elem(i,asms)) | mk(Nat(i)) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) - | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL !LA_Data.lessD)) + | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD)) | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) - | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL - !LA_Data.lessD)) + | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD)) | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) | mk(Multiplied(n,j)) = (trace_msg "*"; multn(n,mk j)) in trace_msg "mkthm"; - simplify (!LA_Data.ss_ref) (mk just) handle FalseE thm => thm end + simplify simpset (mk just) handle FalseE thm => thm end end; fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i; @@ -367,12 +395,12 @@ end state; -fun prove(pTs,Hs,concl) = +fun prove sg (pTs,Hs,concl) = let val nHs = length Hs val ixHs = Hs ~~ (0 upto (nHs-1)) - val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of + val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp sg h of None => None | Some(it) => Some(it,i)) ixHs -in case LA_Data.decomp concl of +in case LA_Data.decomp sg concl of None => if null Hitems then [] else refute1(pTs,Hitems) | Some(citem as (r,i,rel,l,j,d)) => if rel = "=" @@ -386,15 +414,15 @@ Fast but very incomplete decider. Only premises and conclusions that are already (negated) (in)equations are taken into account. *) -val lin_arith_tac = SUBGOAL (fn (A,n) => +fun lin_arith_tac i st = SUBGOAL (fn (A,n) => let val pTs = rev(map snd (Logic.strip_params A)) val Hs = Logic.strip_assums_hyp A val concl = Logic.strip_assums_concl A - in case prove(pTs,Hs,concl) of + in case prove (Thm.sign_of_thm st) (pTs,Hs,concl) of [j] => refute1_tac(n,j) | [j1,j2] => refute2_tac(n,j1,j2) | _ => no_tac - end); + end) i st; fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac i; @@ -427,11 +455,11 @@ fun lin_arith_prover sg thms concl = let val Hs = map (#prop o rep_thm) thms val Tconcl = LA_Logic.mk_Trueprop concl -in case prove([],Hs,Tconcl) of +in case prove sg ([],Hs,Tconcl) of [j] => prover1(j,sg,thms,Tconcl,true) | [j1,j2] => prover2(j1,j2,sg,thms,Tconcl) | _ => let val nTconcl = LA_Logic.neg_prop Tconcl - in case prove([],Hs,nTconcl) of + in case prove sg ([],Hs,nTconcl) of [j] => prover1(j,sg,thms,nTconcl,false) (* [_,_] impossible because of negation *) | _ => None