--- 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"
--- 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;
--- 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" ^
--- 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"
--- 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;
--- 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" ^