# HG changeset patch
# User berghofe
# Date 1059061958 -7200
# Node ID 398bc4a885d6c11feb93ae940bb415c239ad000d
# Parent  d4e2ab7cc86bd15b8593ffc5b3c0890d2cdaf91f
Fixed two bugs:
- presburger_tac now calls ObjectLogic.atomize_tac first to avoid
  failure when premises contain meta-level quantifiers or implications
- The preprocessor now also filters out premises containing variables
  that are not of type int or nat.

diff -r d4e2ab7cc86b -r 398bc4a885d6 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu Jul 24 17:47:56 2003 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu Jul 24 17:52:38 2003 +0200
@@ -124,7 +124,10 @@
    ("True", bT)];
 
 (*returns true if the formula is relevant for presburger arithmetic tactic*)
-fun relevant t = (term_typed_consts t) subset allowed_consts;
+fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
+  map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
+  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
+  subset [iT, nT];
 
 (* Preparation of the formula to be sent to the Integer quantifier *)
 (* elimination procedure                                           *)
@@ -136,13 +139,13 @@
     val ps = Logic.strip_params fm
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
-    val _ = if relevant c then () else raise CooperDec.COOPER
+    val _ = if relevant (rev ps) c then () else raise CooperDec.COOPER
     fun mk_all ((s, T), (P,n)) =
       if 0 mem loose_bnos P then
         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
-    val (rhs,irhs) = partition relevant hs
+    val (rhs,irhs) = partition (relevant (rev ps)) hs
     val np = length ps
     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (ps,(foldr HOLogic.mk_imp (rhs, c), np))
@@ -158,7 +161,7 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 (* the presburger tactic*)
-fun presburger_tac q i st =
+fun presburger_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
   let
     val g = BasisLibrary.List.nth (prems_of st, i - 1);
     val sg = sign_of_thm st;
@@ -203,7 +206,7 @@
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
-  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st;
+  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
 
 fun presburger_args meth =
   Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)
diff -r d4e2ab7cc86b -r 398bc4a885d6 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 24 17:47:56 2003 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 24 17:52:38 2003 +0200
@@ -124,7 +124,10 @@
    ("True", bT)];
 
 (*returns true if the formula is relevant for presburger arithmetic tactic*)
-fun relevant t = (term_typed_consts t) subset allowed_consts;
+fun relevant ps t = (term_typed_consts t) subset allowed_consts andalso
+  map (fn i => snd (nth_elem (i, ps))) (loose_bnos t) @
+  map (snd o dest_Free) (term_frees t) @ map (snd o dest_Var) (term_vars t)
+  subset [iT, nT];
 
 (* Preparation of the formula to be sent to the Integer quantifier *)
 (* elimination procedure                                           *)
@@ -136,13 +139,13 @@
     val ps = Logic.strip_params fm
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
-    val _ = if relevant c then () else raise CooperDec.COOPER
+    val _ = if relevant (rev ps) c then () else raise CooperDec.COOPER
     fun mk_all ((s, T), (P,n)) =
       if 0 mem loose_bnos P then
         (HOLogic.all_const T $ Abs (s, T, P), n)
       else (incr_boundvars ~1 P, n-1)
     fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
-    val (rhs,irhs) = partition relevant hs
+    val (rhs,irhs) = partition (relevant (rev ps)) hs
     val np = length ps
     val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
       (ps,(foldr HOLogic.mk_imp (rhs, c), np))
@@ -158,7 +161,7 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 (* the presburger tactic*)
-fun presburger_tac q i st =
+fun presburger_tac q i = ObjectLogic.atomize_tac i THEN (fn st =>
   let
     val g = BasisLibrary.List.nth (prems_of st, i - 1);
     val sg = sign_of_thm st;
@@ -203,7 +206,7 @@
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i THEN tac) st
-  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st;
+  end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st);
 
 fun presburger_args meth =
   Method.simple_args (Scan.optional (Args.$$$ "no_quantify" >> K false) true)