author chaieb 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;```