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 Jun 12 13:50:55 2004 +0200 (2004-06-12)
changeset 14920a7525235e20f
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
src/HOL/Integ/cooper_proof.ML
src/HOL/Integ/presburger.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/cooper_proof.ML
src/HOL/Tools/Presburger/presburger.ML
     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.19  
    1.20  structure  CooperDec : COOPER_DEC =
    1.21 @@ -60,7 +62,6 @@
    1.22   
    1.23  (* ------------------------------------------------------------------------- *) 
    1.24   
    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.40   
    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.53   
    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.77     
    1.78  fun lift_qelim afn nfn qfn isat = 
    1.79   let   fun qelim x vars p = 
    1.80 @@ -736,7 +758,7 @@
    1.81   
    1.82    in (fn fm => simpl(qelift (fv fm) fm)) 
    1.83    end; 
    1.84 - 
    1.85 +
    1.86   
    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.97   
    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.104 +
   1.105  
   1.106  end;
   1.107 - 
   1.108 \ No newline at end of file
   1.109 +
   1.110 +
     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.6  
     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.13  
    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.24  
    3.25  end;
    3.26  
    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.19  
    4.20  structure  CooperDec : COOPER_DEC =
    4.21 @@ -60,7 +62,6 @@
    4.22   
    4.23  (* ------------------------------------------------------------------------- *) 
    4.24   
    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.40   
    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.53   
    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.77     
    4.78  fun lift_qelim afn nfn qfn isat = 
    4.79   let   fun qelim x vars p = 
    4.80 @@ -736,7 +758,7 @@
    4.81   
    4.82    in (fn fm => simpl(qelift (fv fm) fm)) 
    4.83    end; 
    4.84 - 
    4.85 +
    4.86   
    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.97   
    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.104 +
   4.105  
   4.106  end;
   4.107 - 
   4.108 \ No newline at end of file
   4.109 +
   4.110 +
     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.6  
     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.13  
    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.24  
    6.25  end;
    6.26  
    6.27 -val presburger_tac = Presburger.presburger_tac true true;
    6.28 +val presburger_tac = Presburger.presburger_tac true false;