Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
authorchaieb
Sat, 12 Jun 2004 13:50:55 +0200
changeset 14920 a7525235e20f
parent 14919 0f5fde03e2b5
child 14921 4ad751fa50c1
An oracle is built in. The tactic will not generate any proofs any more, if the quick_and_dirty flag is set on.
src/HOL/Integ/cooper_dec.ML file | annotate | diff | comparison | revisions
src/HOL/Integ/cooper_proof.ML file | annotate | diff | comparison | revisions
src/HOL/Integ/presburger.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/cooper_dec.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/cooper_proof.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/presburger.ML file | annotate | diff | comparison | revisions 
--- 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
+
+
--- 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;
+
--- 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;
--- 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
+
+
--- 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;
+
--- 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;
isabelle