# HG changeset patch
# User chaieb
# Date 1087224408 -7200
# Node ID 1edb674e0c33f2524691cf7a42c62c088d267de0
# Parent  b9ab8babd8b348a44f144315766b32bf60b62118
Oracle corrected

diff -r b9ab8babd8b3 -r 1edb674e0c33 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy	Mon Jun 14 16:46:48 2004 +0200
@@ -985,6 +985,9 @@
   by (simp cong: conj_cong)
 
 use "cooper_dec.ML"
+oracle
+  presburger_oracle = CooperDec.mk_presburger_oracle
+
 use "cooper_proof.ML"
 use "qelim.ML"
 use "presburger.ML"
diff -r b9ab8babd8b3 -r 1edb674e0c33 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Mon Jun 14 16:46:48 2004 +0200
@@ -11,6 +11,7 @@
 signature COOPER_DEC = 
 sig
   exception COOPER
+  exception COOPER_ORACLE of term
   val is_arith_rel : term -> bool
   val mk_numeral : int -> term
   val dest_numeral : term -> int
@@ -43,6 +44,7 @@
   val onatoms : (term -> term) -> term -> term
   val evalc : term -> term
   val integer_qelim : Term.term -> Term.term
+  val mk_presburger_oracle : (Sign.sg * exn) -> term
 end;
 
 structure  CooperDec : COOPER_DEC =
@@ -53,6 +55,10 @@
 (* ========================================================================= *) 
 exception COOPER;
 
+(* Exception for the oracle *)
+exception COOPER_ORACLE of term;
+
+
 (* ------------------------------------------------------------------------- *) 
 (* Lift operations up to numerals.                                           *) 
 (* ------------------------------------------------------------------------- *) 
@@ -803,6 +809,10 @@
 *)
 val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; 
 
+fun mk_presburger_oracle (sg,COOPER_ORACLE t) = 
+    if (!quick_and_dirty) 
+    then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
+    else raise COOPER_ORACLE t;
 
 end;
 
diff -r b9ab8babd8b3 -r 1edb674e0c33 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Mon Jun 14 16:46:48 2004 +0200
@@ -28,6 +28,13 @@
 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
 (*-----------------------------------------------------------------*)
 
+
+(* Invoking the oracle *)
+
+fun pres_oracle sg t = 
+  invoke_oracle (the_context()) "presburger_oracle" 
+     (sg, CooperDec.COOPER_ORACLE t) ;
+
 val presburger_ss = simpset_of (theory "Presburger");
 
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
@@ -270,8 +277,11 @@
     let val pth = 
           (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty 
-             then assume (cterm_of sg 
+             then pres_oracle sg (Pattern.eta_long [] t1)
+(*
+assume (cterm_of sg 
 	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
+*)
 	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
diff -r b9ab8babd8b3 -r 1edb674e0c33 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Presburger.thy	Mon Jun 14 16:46:48 2004 +0200
@@ -985,6 +985,9 @@
   by (simp cong: conj_cong)
 
 use "cooper_dec.ML"
+oracle
+  presburger_oracle = CooperDec.mk_presburger_oracle
+
 use "cooper_proof.ML"
 use "qelim.ML"
 use "presburger.ML"
diff -r b9ab8babd8b3 -r 1edb674e0c33 src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Jun 14 16:46:48 2004 +0200
@@ -11,6 +11,7 @@
 signature COOPER_DEC = 
 sig
   exception COOPER
+  exception COOPER_ORACLE of term
   val is_arith_rel : term -> bool
   val mk_numeral : int -> term
   val dest_numeral : term -> int
@@ -43,6 +44,7 @@
   val onatoms : (term -> term) -> term -> term
   val evalc : term -> term
   val integer_qelim : Term.term -> Term.term
+  val mk_presburger_oracle : (Sign.sg * exn) -> term
 end;
 
 structure  CooperDec : COOPER_DEC =
@@ -53,6 +55,10 @@
 (* ========================================================================= *) 
 exception COOPER;
 
+(* Exception for the oracle *)
+exception COOPER_ORACLE of term;
+
+
 (* ------------------------------------------------------------------------- *) 
 (* Lift operations up to numerals.                                           *) 
 (* ------------------------------------------------------------------------- *) 
@@ -803,6 +809,10 @@
 *)
 val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; 
 
+fun mk_presburger_oracle (sg,COOPER_ORACLE t) = 
+    if (!quick_and_dirty) 
+    then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
+    else raise COOPER_ORACLE t;
 
 end;
 
diff -r b9ab8babd8b3 -r 1edb674e0c33 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Mon Jun 14 14:20:55 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Mon Jun 14 16:46:48 2004 +0200
@@ -28,6 +28,13 @@
 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*)
 (*-----------------------------------------------------------------*)
 
+
+(* Invoking the oracle *)
+
+fun pres_oracle sg t = 
+  invoke_oracle (the_context()) "presburger_oracle" 
+     (sg, CooperDec.COOPER_ORACLE t) ;
+
 val presburger_ss = simpset_of (theory "Presburger");
 
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
@@ -270,8 +277,11 @@
     let val pth = 
           (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty 
-             then assume (cterm_of sg 
+             then pres_oracle sg (Pattern.eta_long [] t1)
+(*
+assume (cterm_of sg 
 	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
+*)
 	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^