author chaieb Sat Jun 12 13:50:55 2004 +0200 (2004-06-12) 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 | revisions src/HOL/Integ/cooper_proof.ML file | annotate | diff | revisions src/HOL/Integ/presburger.ML file | annotate | diff | revisions src/HOL/Tools/Presburger/cooper_dec.ML file | annotate | diff | revisions src/HOL/Tools/Presburger/cooper_proof.ML file | annotate | diff | revisions src/HOL/Tools/Presburger/presburger.ML file | annotate | diff | revisions
1.1 --- a/src/HOL/Integ/cooper_dec.ML	Thu Jun 10 20:17:07 2004 +0200
1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Sat Jun 12 13:50:55 2004 +0200
1.3 @@ -6,7 +6,8 @@
1.4  File containing the implementation of Cooper Algorithm
1.5  decision procedure (intensively inspired from J.Harrison)
1.6  *)
1.7 -
1.8 +
1.9 +
1.10  signature COOPER_DEC =
1.11  sig
1.12    exception COOPER
1.13 @@ -41,6 +42,7 @@
1.14    val plusinf : term -> term -> term
1.15    val onatoms : (term -> term) -> term -> term
1.16    val evalc : term -> term
1.17 +  val integer_qelim : Term.term -> Term.term
1.18  end;
1.20  structure  CooperDec : COOPER_DEC =
1.21 @@ -60,7 +62,6 @@
1.23  (* ------------------------------------------------------------------------- *)
1.25 -
1.26  (*Function is_arith_rel returns true if and only if the term is an atomar presburger
1.27  formula *)
1.28  fun is_arith_rel tm = case tm of
1.29 @@ -560,10 +561,11 @@
1.30    | Const ("op -->",_) \$ p \$ q => simpl1 (HOLogic.mk_imp(simpl p ,simpl q ))
1.31    | Const("op =", Type ("fun",[Type ("bool", []),_]))\$ p \$ q => simpl1
1.32    (HOLogic.mk_eq(simpl p ,simpl q ))
1.33 -  | Const ("All",Ta) \$ Abs(Vn,VT,p) => simpl1(Const("All",Ta) \$
1.34 +(*  | Const ("All",Ta) \$ Abs(Vn,VT,p) => simpl1(Const("All",Ta) \$
1.35    Abs(Vn,VT,simpl p ))
1.36    | Const ("Ex",Ta)  \$ Abs(Vn,VT,p) => simpl1(Const("Ex",Ta)  \$
1.37    Abs(Vn,VT,simpl p ))
1.38 +*)
1.39    | _ => fm;
1.41  (* ------------------------------------------------------------------------- *)
1.42 @@ -655,7 +657,8 @@
1.43      val (xn,p1) = variant_abs (x0,T,p0)
1.44      val x = Free (xn,T)
1.45      val vars = (xn::vars1)
1.46 -    val p = unitycoeff x  (posineq (simpl p1))
1.47 +(*     val p = unitycoeff x  (posineq (simpl p1)) *)
1.48 +    val p = unitycoeff x  p1
1.49      val ast = aset x p
1.50      val bst = bset x p
1.51      val js = 1 upto divlcm x p
1.52 @@ -708,7 +711,26 @@
1.54  (* ------------------------------------------------------------------------- *)
1.55  (* Lift procedure given literal modifier, formula normalizer & basic quelim. *)
1.56 -(* ------------------------------------------------------------------------- *)
1.57 +(* ------------------------------------------------------------------------- *)
1.58 +(*
1.59 +fun lift_qelim afn nfn qfn isat =
1.60 +let
1.61 +fun qelift vars fm = if (isat fm) then afn vars fm
1.62 +else
1.63 +case fm of
1.64 +  Const ("Not",_) \$ p => HOLogic.Not \$ (qelift vars p)
1.65 +  | Const ("op &",_) \$ p \$q => HOLogic.conj \$ (qelift vars p) \$ (qelift vars q)
1.66 +  | Const ("op |",_) \$ p \$ q => HOLogic.disj \$ (qelift vars p) \$ (qelift vars q)
1.67 +  | Const ("op -->",_) \$ p \$ q => HOLogic.imp \$ (qelift vars p) \$ (qelift vars q)
1.68 +  | Const ("op =",Type ("fun",[Type ("bool", []),_])) \$ p \$ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q))
1.69 +  | Const ("All",QT) \$ Abs(x,T,p) => HOLogic.Not \$(qelift vars (Const ("Ex",QT) \$ Abs(x,T,(HOLogic.Not \$ p))))
1.70 +  | (e as Const ("Ex",_)) \$ Abs (x,T,p)  =>  qfn vars (e\$Abs (x,T,(nfn(qelift (x::vars) p))))
1.71 +  | _ => fm
1.72 +
1.73 +in (fn fm => qelift (fv fm) fm)
1.74 +end;
1.75 +*)
1.76 +
1.78  fun lift_qelim afn nfn qfn isat =
1.79   let   fun qelim x vars p =
1.80 @@ -736,7 +758,7 @@
1.82    in (fn fm => simpl(qelift (fv fm) fm))
1.83    end;
1.84 -
1.85 +
1.87  (* ------------------------------------------------------------------------- *)
1.88  (* Cleverer (proposisional) NNF with conditional and literal modification.   *)
1.89 @@ -771,11 +793,17 @@
1.90      | (Const ("Not",_) \$ (Const ("op -->",_) \$ p \$q)) => HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not \$ q))
1.91      | (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))
1.92      | _ => lfn fm
1.93 -  in cnnfh o simpl
1.94 -  end;
1.95 +in cnnfh
1.96 + end;
1.98  (*End- function the quantifierelimination an decion procedure of presburger formulas.*)
1.99 +
1.100 +(*
1.101  val integer_qelim = simpl o evalc o (lift_qelim linform (simpl o (cnnf posineq o evalc)) cooper is_arith_rel) ;
1.102 +*)
1.103 +val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ;
1.106  end;
1.108 \ No newline at end of file
2.1 --- a/src/HOL/Integ/cooper_proof.ML	Thu Jun 10 20:17:07 2004 +0200
2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Sat Jun 12 13:50:55 2004 +0200
2.3 @@ -7,6 +7,7 @@
2.4  generation for Cooper Algorithm
2.5  *)
2.7 +
2.8  signature COOPER_PROOF =
2.9  sig
2.10    val qe_Not : thm
2.11 @@ -957,3 +958,4 @@
2.12    end;
2.14  end;
2.15 +
3.1 --- a/src/HOL/Integ/presburger.ML	Thu Jun 10 20:17:07 2004 +0200
3.2 +++ b/src/HOL/Integ/presburger.ML	Sat Jun 12 13:50:55 2004 +0200
3.3 @@ -267,10 +267,18 @@
3.4      (* The result of the quantifier elimination *)
3.5      val (th, tac) = case (prop_of pre_thm) of
3.6          Const ("==>", _) \$ (Const ("Trueprop", _) \$ t1) \$ _ =>
3.7 +    let val pth =
3.8 +          (* If quick_and_dirty then run without proof generation as oracle*)
3.9 +             if !quick_and_dirty
3.10 +             then assume (cterm_of sg
3.11 +	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
3.12 +	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
3.13 +    in
3.14            (trace_msg ("calling procedure with term:\n" ^
3.15               Sign.string_of_term sg t1);
3.16 -           ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
3.17 +           ((pth RS iffD2) RS pre_thm,
3.18              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
3.19 +    end
3.20        | _ => (pre_thm, assm_tac i)
3.21    in (rtac (((mp_step nh) o (spec_step np)) th) i
3.22        THEN tac) st
3.23 @@ -300,4 +308,4 @@
3.25  end;
3.27 -val presburger_tac = Presburger.presburger_tac true true;
3.28 +val presburger_tac = Presburger.presburger_tac true false;
4.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Thu Jun 10 20:17:07 2004 +0200
4.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Sat Jun 12 13:50:55 2004 +0200
4.3 @@ -6,7 +6,8 @@
4.4  File containing the implementation of Cooper Algorithm
4.5  decision procedure (intensively inspired from J.Harrison)
4.6  *)
4.7 -
4.8 +
4.9 +
4.10  signature COOPER_DEC =
4.11  sig
4.12    exception COOPER
4.13 @@ -41,6 +42,7 @@
4.14    val plusinf : term -> term -> term
4.15    val onatoms : (term -> term) -> term -> term
4.16    val evalc : term -> term
4.17 +  val integer_qelim : Term.term -> Term.term
4.18  end;
4.20  structure  CooperDec : COOPER_DEC =
4.21 @@ -60,7 +62,6 @@
4.23  (* ------------------------------------------------------------------------- *)
4.25 -
4.26  (*Function is_arith_rel returns true if and only if the term is an atomar presburger
4.27  formula *)
4.28  fun is_arith_rel tm = case tm of
4.29 @@ -560,10 +561,11 @@
4.30    | Const ("op -->",_) \$ p \$ q => simpl1 (HOLogic.mk_imp(simpl p ,simpl q ))
4.31    | Const("op =", Type ("fun",[Type ("bool", []),_]))\$ p \$ q => simpl1
4.32    (HOLogic.mk_eq(simpl p ,simpl q ))
4.33 -  | Const ("All",Ta) \$ Abs(Vn,VT,p) => simpl1(Const("All",Ta) \$
4.34 +(*  | Const ("All",Ta) \$ Abs(Vn,VT,p) => simpl1(Const("All",Ta) \$
4.35    Abs(Vn,VT,simpl p ))
4.36    | Const ("Ex",Ta)  \$ Abs(Vn,VT,p) => simpl1(Const("Ex",Ta)  \$
4.37    Abs(Vn,VT,simpl p ))
4.38 +*)
4.39    | _ => fm;
4.41  (* ------------------------------------------------------------------------- *)
4.42 @@ -655,7 +657,8 @@
4.43      val (xn,p1) = variant_abs (x0,T,p0)
4.44      val x = Free (xn,T)
4.45      val vars = (xn::vars1)
4.46 -    val p = unitycoeff x  (posineq (simpl p1))
4.47 +(*     val p = unitycoeff x  (posineq (simpl p1)) *)
4.48 +    val p = unitycoeff x  p1
4.49      val ast = aset x p
4.50      val bst = bset x p
4.51      val js = 1 upto divlcm x p
4.52 @@ -708,7 +711,26 @@
4.54  (* ------------------------------------------------------------------------- *)
4.55  (* Lift procedure given literal modifier, formula normalizer & basic quelim. *)
4.56 -(* ------------------------------------------------------------------------- *)
4.57 +(* ------------------------------------------------------------------------- *)
4.58 +(*
4.59 +fun lift_qelim afn nfn qfn isat =
4.60 +let
4.61 +fun qelift vars fm = if (isat fm) then afn vars fm
4.62 +else
4.63 +case fm of
4.64 +  Const ("Not",_) \$ p => HOLogic.Not \$ (qelift vars p)
4.65 +  | Const ("op &",_) \$ p \$q => HOLogic.conj \$ (qelift vars p) \$ (qelift vars q)
4.66 +  | Const ("op |",_) \$ p \$ q => HOLogic.disj \$ (qelift vars p) \$ (qelift vars q)
4.67 +  | Const ("op -->",_) \$ p \$ q => HOLogic.imp \$ (qelift vars p) \$ (qelift vars q)
4.68 +  | Const ("op =",Type ("fun",[Type ("bool", []),_])) \$ p \$ q => HOLogic.mk_eq ((qelift vars p),(qelift vars q))
4.69 +  | Const ("All",QT) \$ Abs(x,T,p) => HOLogic.Not \$(qelift vars (Const ("Ex",QT) \$ Abs(x,T,(HOLogic.Not \$ p))))
4.70 +  | (e as Const ("Ex",_)) \$ Abs (x,T,p)  =>  qfn vars (e\$Abs (x,T,(nfn(qelift (x::vars) p))))
4.71 +  | _ => fm
4.72 +
4.73 +in (fn fm => qelift (fv fm) fm)
4.74 +end;
4.75 +*)
4.76 +
4.78  fun lift_qelim afn nfn qfn isat =
4.79   let   fun qelim x vars p =
4.80 @@ -736,7 +758,7 @@
4.82    in (fn fm => simpl(qelift (fv fm) fm))
4.83    end;
4.84 -
4.85 +
4.87  (* ------------------------------------------------------------------------- *)
4.88  (* Cleverer (proposisional) NNF with conditional and literal modification.   *)
4.89 @@ -771,11 +793,17 @@
4.90      | (Const ("Not",_) \$ (Const ("op -->",_) \$ p \$q)) => HOLogic.mk_conj(cnnfh p,cnnfh(HOLogic.Not \$ q))
4.91      | (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))
4.92      | _ => lfn fm
4.93 -  in cnnfh o simpl
4.94 -  end;
4.95 +in cnnfh
4.96 + end;
4.98  (*End- function the quantifierelimination an decion procedure of presburger formulas.*)
4.99 +
4.100 +(*
4.101  val integer_qelim = simpl o evalc o (lift_qelim linform (simpl o (cnnf posineq o evalc)) cooper is_arith_rel) ;
4.102 +*)
4.103 +val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ;
4.106  end;
4.108 \ No newline at end of file
5.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Thu Jun 10 20:17:07 2004 +0200
5.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Sat Jun 12 13:50:55 2004 +0200
5.3 @@ -7,6 +7,7 @@
5.4  generation for Cooper Algorithm
5.5  *)
5.7 +
5.8  signature COOPER_PROOF =
5.9  sig
5.10    val qe_Not : thm
5.11 @@ -957,3 +958,4 @@
5.12    end;
5.14  end;
5.15 +
6.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Thu Jun 10 20:17:07 2004 +0200
6.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Sat Jun 12 13:50:55 2004 +0200
6.3 @@ -267,10 +267,18 @@
6.4      (* The result of the quantifier elimination *)
6.5      val (th, tac) = case (prop_of pre_thm) of
6.6          Const ("==>", _) \$ (Const ("Trueprop", _) \$ t1) \$ _ =>
6.7 +    let val pth =
6.8 +          (* If quick_and_dirty then run without proof generation as oracle*)
6.9 +             if !quick_and_dirty
6.10 +             then assume (cterm_of sg
6.11 +	       (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
6.12 +	     else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
6.13 +    in
6.14            (trace_msg ("calling procedure with term:\n" ^
6.15               Sign.string_of_term sg t1);
6.16 -           ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm,
6.17 +           ((pth RS iffD2) RS pre_thm,
6.18              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
6.19 +    end
6.20        | _ => (pre_thm, assm_tac i)
6.21    in (rtac (((mp_step nh) o (spec_step np)) th) i
6.22        THEN tac) st
6.23 @@ -300,4 +308,4 @@
6.25  end;
6.27 -val presburger_tac = Presburger.presburger_tac true true;
6.28 +val presburger_tac = Presburger.presburger_tac true false;