author webertj Tue, 10 Mar 2009 08:47:45 +0000 changeset 30406 15dc25f8a0e2 parent 30403 042641837e79 child 30407 81218f70997f child 30415 9501af91c4a3
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
```--- 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;
```