# HG changeset patch
# User chaieb
# Date 1087041055 -7200
# Node ID a7525235e20fb5770c1da5f7136cd50ca0520f64
# Parent  0f5fde03e2b5bb336bd4b5d3b294f3547efaa4d4
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.

diff -r 0f5fde03e2b5 -r a7525235e20f src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Thu Jun 10 20:17:07 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Sat Jun 12 13:50:55 2004 +0200
@@ -6,7 +6,8 @@
 File containing the implementation of Cooper Algorithm
 decision procedure (intensively inspired from J.Harrison)
 *)
- 
+
+
 signature COOPER_DEC = 
 sig
   exception COOPER
@@ -41,6 +42,7 @@
   val plusinf : term -> term -> term
   val onatoms : (term -> term) -> term -> term
   val evalc : term -> term
+  val integer_qelim : Term.term -> Term.term
 end;
 
 structure  CooperDec : COOPER_DEC =
@@ -60,7 +62,6 @@
  
 (* ------------------------------------------------------------------------- *) 
  
- 
 (*Function is_arith_rel returns true if and only if the term is an atomar presburger 
 formula *) 
 fun is_arith_rel tm = case tm of 
@@ -560,10 +561,11 @@
   | Const ("op -->",_) $ p $ q => simpl1 (HOLogic.mk_imp(simpl p ,simpl q ))  
   | Const("op =", Type ("fun",[Type ("bool", []),_]))$ p $ q => simpl1 
   (HOLogic.mk_eq(simpl p ,simpl q ))  
-  | Const ("All",Ta) $ Abs(Vn,VT,p) => simpl1(Const("All",Ta) $ 
+(*  | Const ("All",Ta) $ Abs(Vn,VT,p) => simpl1(Const("All",Ta) $ 
   Abs(Vn,VT,simpl p ))  
   | Const ("Ex",Ta)  $ Abs(Vn,VT,p) => simpl1(Const("Ex",Ta)  $ 
   Abs(Vn,VT,simpl p ))  
+*)
   | _ => fm; 
  
 (* ------------------------------------------------------------------------- *) 
@@ -655,7 +657,8 @@
     val (xn,p1) = variant_abs (x0,T,p0)
     val x = Free (xn,T)
     val vars = (xn::vars1)
-    val p = unitycoeff x  (posineq (simpl p1))
+(*     val p = unitycoeff x  (posineq (simpl p1)) *)
+    val p = unitycoeff x  p1 
     val ast = aset x p
     val bst = bset x p
     val js = 1 upto divlcm x p
@@ -708,7 +711,26 @@
  
 (* ------------------------------------------------------------------------- *) 
 (* Lift procedure given literal modifier, formula normalizer & basic quelim. *) 
-(* ------------------------------------------------------------------------- *) 
+(* ------------------------------------------------------------------------- *)
+(*
+fun lift_qelim afn nfn qfn isat = 
+let 
+fun qelift vars fm = if (isat fm) then afn vars fm 
+else  
+case fm of 
+  Const ("Not",_) $ p => HOLogic.Not $ (qelift vars p) 
+  | Const ("op &",_) $ p $q => HOLogic.conj $ (qelift vars p) $ (qelift vars q) 
+  | Const ("op |",_) $ p $ q => HOLogic.disj $ (qelift vars p) $ (qelift vars q) 
+  | Const ("op -->",_) $ p $ q => HOLogic.imp $ (qelift vars p) $ (qelift vars q) 
+  | Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q)) 
+  | Const ("All",QT) $ Abs(x,T,p) => HOLogic.Not $(qelift vars (Const ("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p)))) 
+  | (e as Const ("Ex",_)) $ Abs (x,T,p)  =>  qfn vars (e$Abs (x,T,(nfn(qelift (x::vars) p))))
+  | _ => fm 
+ 
+in (fn fm => qelift (fv fm) fm)
+end; 
+*)
+ 
    
 fun lift_qelim afn nfn qfn isat = 
  let   fun qelim x vars p = 
@@ -736,7 +758,7 @@
  
   in (fn fm => simpl(qelift (fv fm) fm)) 
   end; 
- 
+
  
 (* ------------------------------------------------------------------------- *) 
 (* Cleverer (proposisional) NNF with conditional and literal modification.   *) 
@@ -771,11 +793,17 @@
     | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) => HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)) 
     | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_]))  $ p $ q)) => HOLogic.mk_disj(HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)),HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh q)) 
     | _ => lfn fm  
-  in cnnfh o simpl
-  end; 
+in cnnfh
+ end; 
  
 (*End- function the quantifierelimination an decion procedure of presburger formulas.*)   
+
+(*
 val integer_qelim = simpl o evalc o (lift_qelim linform (simpl o (cnnf posineq o evalc)) cooper is_arith_rel) ; 
+*)
+val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; 
+
 
 end;
- 
\ No newline at end of file
+
+
diff -r 0f5fde03e2b5 -r a7525235e20f src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Thu Jun 10 20:17:07 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Sat Jun 12 13:50:55 2004 +0200
@@ -7,6 +7,7 @@
 generation for Cooper Algorithm
 *)
 
+
 signature COOPER_PROOF =
 sig
   val qe_Not : thm
@@ -957,3 +958,4 @@
   end;
 
 end;
+
diff -r 0f5fde03e2b5 -r a7525235e20f src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Thu Jun 10 20:17:07 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Sat Jun 12 13:50:55 2004 +0200
@@ -267,10 +267,18 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+    let val pth = 
+          (* If quick_and_dirty then run without proof generation as oracle*)
+             if !quick_and_dirty 
+             then 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" ^
              Sign.string_of_term sg t1);
-           ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
+           ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
+    end
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i 
       THEN tac) st
@@ -300,4 +308,4 @@
 
 end;
 
-val presburger_tac = Presburger.presburger_tac true true;
+val presburger_tac = Presburger.presburger_tac true false;
diff -r 0f5fde03e2b5 -r a7525235e20f src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Jun 10 20:17:07 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Jun 12 13:50:55 2004 +0200
@@ -6,7 +6,8 @@
 File containing the implementation of Cooper Algorithm
 decision procedure (intensively inspired from J.Harrison)
 *)
- 
+
+
 signature COOPER_DEC = 
 sig
   exception COOPER
@@ -41,6 +42,7 @@
   val plusinf : term -> term -> term
   val onatoms : (term -> term) -> term -> term
   val evalc : term -> term
+  val integer_qelim : Term.term -> Term.term
 end;
 
 structure  CooperDec : COOPER_DEC =
@@ -60,7 +62,6 @@
  
 (* ------------------------------------------------------------------------- *) 
  
- 
 (*Function is_arith_rel returns true if and only if the term is an atomar presburger 
 formula *) 
 fun is_arith_rel tm = case tm of 
@@ -560,10 +561,11 @@
   | Const ("op -->",_) $ p $ q => simpl1 (HOLogic.mk_imp(simpl p ,simpl q ))  
   | Const("op =", Type ("fun",[Type ("bool", []),_]))$ p $ q => simpl1 
   (HOLogic.mk_eq(simpl p ,simpl q ))  
-  | Const ("All",Ta) $ Abs(Vn,VT,p) => simpl1(Const("All",Ta) $ 
+(*  | Const ("All",Ta) $ Abs(Vn,VT,p) => simpl1(Const("All",Ta) $ 
   Abs(Vn,VT,simpl p ))  
   | Const ("Ex",Ta)  $ Abs(Vn,VT,p) => simpl1(Const("Ex",Ta)  $ 
   Abs(Vn,VT,simpl p ))  
+*)
   | _ => fm; 
  
 (* ------------------------------------------------------------------------- *) 
@@ -655,7 +657,8 @@
     val (xn,p1) = variant_abs (x0,T,p0)
     val x = Free (xn,T)
     val vars = (xn::vars1)
-    val p = unitycoeff x  (posineq (simpl p1))
+(*     val p = unitycoeff x  (posineq (simpl p1)) *)
+    val p = unitycoeff x  p1 
     val ast = aset x p
     val bst = bset x p
     val js = 1 upto divlcm x p
@@ -708,7 +711,26 @@
  
 (* ------------------------------------------------------------------------- *) 
 (* Lift procedure given literal modifier, formula normalizer & basic quelim. *) 
-(* ------------------------------------------------------------------------- *) 
+(* ------------------------------------------------------------------------- *)
+(*
+fun lift_qelim afn nfn qfn isat = 
+let 
+fun qelift vars fm = if (isat fm) then afn vars fm 
+else  
+case fm of 
+  Const ("Not",_) $ p => HOLogic.Not $ (qelift vars p) 
+  | Const ("op &",_) $ p $q => HOLogic.conj $ (qelift vars p) $ (qelift vars q) 
+  | Const ("op |",_) $ p $ q => HOLogic.disj $ (qelift vars p) $ (qelift vars q) 
+  | Const ("op -->",_) $ p $ q => HOLogic.imp $ (qelift vars p) $ (qelift vars q) 
+  | Const ("op =",Type ("fun",[Type ("bool", []),_])) $ p $ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q)) 
+  | Const ("All",QT) $ Abs(x,T,p) => HOLogic.Not $(qelift vars (Const ("Ex",QT) $ Abs(x,T,(HOLogic.Not $ p)))) 
+  | (e as Const ("Ex",_)) $ Abs (x,T,p)  =>  qfn vars (e$Abs (x,T,(nfn(qelift (x::vars) p))))
+  | _ => fm 
+ 
+in (fn fm => qelift (fv fm) fm)
+end; 
+*)
+ 
    
 fun lift_qelim afn nfn qfn isat = 
  let   fun qelim x vars p = 
@@ -736,7 +758,7 @@
  
   in (fn fm => simpl(qelift (fv fm) fm)) 
   end; 
- 
+
  
 (* ------------------------------------------------------------------------- *) 
 (* Cleverer (proposisional) NNF with conditional and literal modification.   *) 
@@ -771,11 +793,17 @@
     | (Const ("Not",_) $ (Const ("op -->",_) $ p $q)) => HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)) 
     | (Const ("Not",_) $ (Const ("op =",Type ("fun",[Type ("bool", []),_]))  $ p $ q)) => HOLogic.mk_disj(HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not $ q)),HOLogic.mk_conj(cnnfh(HOLogic.Not $ p),cnnfh q)) 
     | _ => lfn fm  
-  in cnnfh o simpl
-  end; 
+in cnnfh
+ end; 
  
 (*End- function the quantifierelimination an decion procedure of presburger formulas.*)   
+
+(*
 val integer_qelim = simpl o evalc o (lift_qelim linform (simpl o (cnnf posineq o evalc)) cooper is_arith_rel) ; 
+*)
+val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; 
+
 
 end;
- 
\ No newline at end of file
+
+
diff -r 0f5fde03e2b5 -r a7525235e20f src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Jun 10 20:17:07 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jun 12 13:50:55 2004 +0200
@@ -7,6 +7,7 @@
 generation for Cooper Algorithm
 *)
 
+
 signature COOPER_PROOF =
 sig
   val qe_Not : thm
@@ -957,3 +958,4 @@
   end;
 
 end;
+
diff -r 0f5fde03e2b5 -r a7525235e20f src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jun 10 20:17:07 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Jun 12 13:50:55 2004 +0200
@@ -267,10 +267,18 @@
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
+    let val pth = 
+          (* If quick_and_dirty then run without proof generation as oracle*)
+             if !quick_and_dirty 
+             then 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" ^
              Sign.string_of_term sg t1);
-           ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
+           ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
+    end
       | _ => (pre_thm, assm_tac i)
   in (rtac (((mp_step nh) o (spec_step np)) th) i 
       THEN tac) st
@@ -300,4 +308,4 @@
 
 end;
 
-val presburger_tac = Presburger.presburger_tac true true;
+val presburger_tac = Presburger.presburger_tac true false;