# HG changeset patch
# User wenzelm
# Date 1334439258 -7200
# Node ID 92d1c566ebbf8e8d8ada69bc5b8538ac61259ada
# Parent  80ddf2016b6c82268dd27dd1318e8925d7e82ce8
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
clarified thin_prems_tac: fail as tactic without error;

diff -r 80ddf2016b6c -r 92d1c566ebbf src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Apr 14 20:44:53 2012 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Apr 14 23:34:18 2012 +0200
@@ -721,8 +721,12 @@
      val ntac = (case qs of [] => q aconvc @{cterm "False"}
                          | _ => false)
     in 
-    if ntac then no_tac
-      else rtac (Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) i
+      if ntac then no_tac
+      else
+        (case try (fn () =>
+            Goal.prove_internal [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
+          NONE => no_tac
+        | SOME r => rtac r i)
     end)
 end;
 
@@ -835,26 +839,27 @@
 fun finish_tac q = SUBGOAL (fn (_, i) =>
   (if q then I else TRY) (rtac TrueI i));
 
-fun tac elim add_ths del_ths ctxt =
-let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
+fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} =>
+  let
+    val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
     val aprems = Arith_Data.get_arith_facts ctxt
-in
-  Method.insert_tac aprems
-  THEN_ALL_NEW Object_Logic.full_atomize_tac
-  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
-  THEN_ALL_NEW simp_tac ss
-  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
-  THEN_ALL_NEW Object_Logic.full_atomize_tac
-  THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
-  THEN_ALL_NEW Object_Logic.full_atomize_tac
-  THEN_ALL_NEW div_mod_tac ctxt
-  THEN_ALL_NEW splits_tac ctxt
-  THEN_ALL_NEW simp_tac ss
-  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
-  THEN_ALL_NEW nat_to_int_tac ctxt
-  THEN_ALL_NEW (core_tac ctxt)
-  THEN_ALL_NEW finish_tac elim
-end;
+  in
+    Method.insert_tac aprems
+    THEN_ALL_NEW Object_Logic.full_atomize_tac
+    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
+    THEN_ALL_NEW simp_tac ss
+    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
+    THEN_ALL_NEW Object_Logic.full_atomize_tac
+    THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
+    THEN_ALL_NEW Object_Logic.full_atomize_tac
+    THEN_ALL_NEW div_mod_tac ctxt
+    THEN_ALL_NEW splits_tac ctxt
+    THEN_ALL_NEW simp_tac ss
+    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
+    THEN_ALL_NEW nat_to_int_tac ctxt
+    THEN_ALL_NEW (core_tac ctxt)
+    THEN_ALL_NEW finish_tac elim
+  end 1);
 
 
 (* theory setup *)