# HG changeset patch # User webertj # Date 1236674865 0 # Node ID 15dc25f8a0e2bf994cbb00bb6e4ebd498bf89fcf # Parent 042641837e79de56e6d1db4d7a87d2c459cdd5c5 Instead of giving up entirely, arith now ignores all inequalities when there are too many. diff -r 042641837e79 -r 15dc25f8a0e2 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Mon Mar 09 23:29:13 2009 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Mar 10 08:47:45 2009 +0000 @@ -619,7 +619,7 @@ (* failure as soon as a case could not be refuted; i.e. delay further *) (* splitting until after a refutation for other cases has been found. *) -fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decomp * int) list) list = +fun split_items ctxt do_pre split_neq (Ts, terms) : (typ list * (LA_Data.decomp * int) list) list = let (* splits inequalities '~=' into '<' and '>'; this corresponds to *) (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *) @@ -649,6 +649,10 @@ |> maps (elim_neq' false) end + fun ignore_neq (NONE, bool) = (NONE, bool) + | ignore_neq (ineq as SOME (_, _, rel, _, _, _), bool) = + if rel = "~=" then (NONE, bool) else (ineq, bool) + fun number_hyps _ [] = [] | number_hyps n (NONE::xs) = number_hyps (n+1) xs | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs @@ -661,7 +665,8 @@ |> (* produce the internal encoding of (in-)equalities *) map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t)))) |> (* splitting of inequalities *) - map (apsnd elim_neq) + map (apsnd (if split_neq then elim_neq else + Library.single o map ignore_neq)) |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals) |> (* numbering of hypotheses, ignoring irrelevant ones *) map (apsnd (number_hyps 0)) @@ -712,12 +717,13 @@ | refute [] js = SOME js in refute end; -fun refute ctxt params show_ex do_pre terms : injust list option = - refutes ctxt params show_ex (split_items ctxt do_pre (map snd params, terms)) []; +fun refute ctxt params show_ex do_pre split_neq terms : injust list option = + refutes ctxt params show_ex (split_items ctxt do_pre split_neq + (map snd params, terms)) []; fun count P xs = length (filter P xs); -fun prove ctxt params show_ex do_pre Hs concl : injust list option = +fun prove ctxt params show_ex do_pre Hs concl : bool * injust list option = let val _ = trace_msg "prove:" (* append the negated conclusion to 'Hs' -- this corresponds to *) @@ -726,21 +732,23 @@ val Hs' = Hs @ [LA_Logic.neg_prop concl] fun is_neq NONE = false | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") - val neq_limit = Config.get ctxt LA_Data.fast_arith_neq_limit; + val neq_limit = Config.get ctxt LA_Data.fast_arith_neq_limit + val split_neq = count is_neq (map (LA_Data.decomp ctxt) Hs') <= neq_limit in - if count is_neq (map (LA_Data.decomp ctxt) Hs') > neq_limit then - (trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ - string_of_int neq_limit ^ ")"); NONE) + if split_neq then () else - refute ctxt params show_ex do_pre Hs' + trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ + string_of_int neq_limit ^ "), ignoring all inequalities"); + (split_neq, refute ctxt params show_ex do_pre split_neq Hs') end handle TERM ("neg_prop", _) => (* since no meta-logic negation is available, we can only fail if *) (* the conclusion is not of the form 'Trueprop $ _' (simply *) (* dropping the conclusion doesn't work either, because even *) (* 'False' does not imply arbitrary 'concl::prop') *) - (trace_msg "prove failed (cannot negate conclusion)."; NONE); + (trace_msg "prove failed (cannot negate conclusion)."; + (false, NONE)); -fun refute_tac ss (i, justs) = +fun refute_tac ss (i, split_neq, justs) = fn state => let val ctxt = Simplifier.the_context ss; @@ -749,7 +757,10 @@ val {neqE, ...} = get_data ctxt; fun just1 j = (* eliminate inequalities *) - REPEAT_DETERM (eresolve_tac neqE i) THEN + (if split_neq then + REPEAT_DETERM (eresolve_tac neqE i) + else + all_tac) THEN PRIMITIVE (trace_thm "State after neqE:") THEN (* use theorems generated from the actual justifications *) METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i @@ -776,8 +787,9 @@ val _ = trace_term ctxt ("Trying to refute subgoal " ^ string_of_int i) A in case prove ctxt params show_ex true Hs concl of - NONE => (trace_msg "Refutation failed."; no_tac) - | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) + (_, NONE) => (trace_msg "Refutation failed."; no_tac) + | (split_neq, SOME js) => (trace_msg "Refutation succeeded."; + refute_tac ss (i, split_neq, js)) end); fun cut_lin_arith_tac ss = @@ -835,14 +847,14 @@ in (thm2' COMP (thm1' COMP thm), js2) end; (* FIXME needs handle THM _ => NONE ? *) -fun prover ss thms Tconcl (js : injust list) pos : thm option = +fun prover ss thms Tconcl (js : injust list) split_neq pos : thm option = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt val nTconcl = LA_Logic.neg_prop Tconcl val cnTconcl = cterm_of thy nTconcl val nTconclthm = assume cnTconcl - val tree = splitasms ctxt (thms @ [nTconclthm]) + val tree = (if split_neq then splitasms ctxt else Tip) (thms @ [nTconclthm]) val (Falsethm, _) = fwdproof ss tree js val contr = if pos then LA_Logic.ccontr else LA_Logic.notI val concl = implies_intr cnTconcl Falsethm COMP contr @@ -864,12 +876,12 @@ val Tconcl = LA_Logic.mk_Trueprop concl in case prove ctxt [] false false Hs Tconcl of (* concl provable? *) - SOME js => prover ss thms Tconcl js true - | NONE => + (split_neq, SOME js) => prover ss thms Tconcl js split_neq true + | (_, NONE) => let val nTconcl = LA_Logic.neg_prop Tconcl in case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *) - SOME js => prover ss thms nTconcl js false - | NONE => NONE + (split_neq, SOME js) => prover ss thms nTconcl js split_neq false + | (_, NONE) => NONE end end;