# HG changeset patch # User wenzelm # Date 1121362099 -7200 # Node ID 416e860889310d17384e115a94b06b72dbc4e371 # Parent 45a3dc4688bc1b85cebfa7af328afde818bb9bfe improved oracle setup; replace itlist by fold_rev; replace end_itlist by Utils.end_itlist; diff -r 45a3dc4688bc -r 416e86088931 src/HOL/Integ/cooper_dec.ML --- a/src/HOL/Integ/cooper_dec.ML Thu Jul 14 19:28:18 2005 +0200 +++ b/src/HOL/Integ/cooper_dec.ML Thu Jul 14 19:28:19 2005 +0200 @@ -10,7 +10,6 @@ signature COOPER_DEC = sig exception COOPER - exception COOPER_ORACLE of term val is_arith_rel : term -> bool val mk_numeral : IntInf.int -> term val dest_numeral : term -> IntInf.int @@ -45,7 +44,7 @@ val evalc : term -> term val cooper_w : string list -> term -> (term option * term) val integer_qelim : Term.term -> Term.term - val mk_presburger_oracle : (Sign.sg * exn) -> term + val presburger_oracle : theory -> term -> term end; structure CooperDec : COOPER_DEC = @@ -56,9 +55,6 @@ (* ========================================================================= *) exception COOPER; -(* Exception for the oracle *) -exception COOPER_ORACLE of term; - (* ------------------------------------------------------------------------- *) (* Lift operations up to numerals. *) @@ -523,12 +519,6 @@ (* Hence overall quantifier elimination. *) (* ------------------------------------------------------------------------- *) -(*Applyes a function iteratively on the list*) - -fun end_itlist f [] = error "end_itlist" - |end_itlist f [x] = x - |end_itlist f (h::t) = f h (end_itlist f t); - (*list_disj[conj] makes a disj[conj] of a given list. used with conjucts or disjuncts it liearises iterated conj[disj]unctions. *) @@ -536,12 +526,12 @@ fun disj_help p q = HOLogic.disj $ p $ q ; fun list_disj l = - if l = [] then HOLogic.false_const else end_itlist disj_help l; + if l = [] then HOLogic.false_const else Utils.end_itlist disj_help l; fun conj_help p q = HOLogic.conj $ p $ q ; fun list_conj l = - if l = [] then HOLogic.true_const else end_itlist conj_help l; + if l = [] then HOLogic.true_const else Utils.end_itlist conj_help l; (*Simplification of Formulas *) @@ -826,14 +816,6 @@ | _ => error "cooper: not an existential formula"; -(*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a -list With End condition b. ict calculates f(e1,f(f(e2,f(e3,...(...f(en,b))..))))) - assuming l = [e1,e2,...,en]*) - -fun itlist f l b = case l of - [] => b - | (h::t) => f h (itlist f t b); - (* ------------------------------------------------------------------------- *) (* Free variables in terms and formulas. *) (* ------------------------------------------------------------------------- *) @@ -890,7 +872,7 @@ (if ycjs = [] then p else let val q = (qfn vars ((HOLogic.exists_const HOLogic.intT ) $ Abs(x,HOLogic.intT,(list_conj ycjs)))) in - (itlist conj_help ncjs q) + (fold_rev conj_help ncjs q) end) end @@ -956,9 +938,8 @@ val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; -fun mk_presburger_oracle (sg,COOPER_ORACLE t) = +fun presburger_oracle thy t = if (!quick_and_dirty) then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t)) - else raise COOPER_ORACLE t - |mk_presburger_oracle (sg,_) = error "Oops"; + else error "Presburger oracle: not in quick_and_dirty mode" end; diff -r 45a3dc4688bc -r 416e86088931 src/HOL/Tools/Presburger/cooper_dec.ML --- a/src/HOL/Tools/Presburger/cooper_dec.ML Thu Jul 14 19:28:18 2005 +0200 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML Thu Jul 14 19:28:19 2005 +0200 @@ -10,7 +10,6 @@ signature COOPER_DEC = sig exception COOPER - exception COOPER_ORACLE of term val is_arith_rel : term -> bool val mk_numeral : IntInf.int -> term val dest_numeral : term -> IntInf.int @@ -45,7 +44,7 @@ val evalc : term -> term val cooper_w : string list -> term -> (term option * term) val integer_qelim : Term.term -> Term.term - val mk_presburger_oracle : (Sign.sg * exn) -> term + val presburger_oracle : theory -> term -> term end; structure CooperDec : COOPER_DEC = @@ -56,9 +55,6 @@ (* ========================================================================= *) exception COOPER; -(* Exception for the oracle *) -exception COOPER_ORACLE of term; - (* ------------------------------------------------------------------------- *) (* Lift operations up to numerals. *) @@ -523,12 +519,6 @@ (* Hence overall quantifier elimination. *) (* ------------------------------------------------------------------------- *) -(*Applyes a function iteratively on the list*) - -fun end_itlist f [] = error "end_itlist" - |end_itlist f [x] = x - |end_itlist f (h::t) = f h (end_itlist f t); - (*list_disj[conj] makes a disj[conj] of a given list. used with conjucts or disjuncts it liearises iterated conj[disj]unctions. *) @@ -536,12 +526,12 @@ fun disj_help p q = HOLogic.disj $ p $ q ; fun list_disj l = - if l = [] then HOLogic.false_const else end_itlist disj_help l; + if l = [] then HOLogic.false_const else Utils.end_itlist disj_help l; fun conj_help p q = HOLogic.conj $ p $ q ; fun list_conj l = - if l = [] then HOLogic.true_const else end_itlist conj_help l; + if l = [] then HOLogic.true_const else Utils.end_itlist conj_help l; (*Simplification of Formulas *) @@ -826,14 +816,6 @@ | _ => error "cooper: not an existential formula"; -(*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a -list With End condition b. ict calculates f(e1,f(f(e2,f(e3,...(...f(en,b))..))))) - assuming l = [e1,e2,...,en]*) - -fun itlist f l b = case l of - [] => b - | (h::t) => f h (itlist f t b); - (* ------------------------------------------------------------------------- *) (* Free variables in terms and formulas. *) (* ------------------------------------------------------------------------- *) @@ -890,7 +872,7 @@ (if ycjs = [] then p else let val q = (qfn vars ((HOLogic.exists_const HOLogic.intT ) $ Abs(x,HOLogic.intT,(list_conj ycjs)))) in - (itlist conj_help ncjs q) + (fold_rev conj_help ncjs q) end) end @@ -956,9 +938,8 @@ val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; -fun mk_presburger_oracle (sg,COOPER_ORACLE t) = +fun presburger_oracle thy t = if (!quick_and_dirty) then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t)) - else raise COOPER_ORACLE t - |mk_presburger_oracle (sg,_) = error "Oops"; + else error "Presburger oracle: not in quick_and_dirty mode" end;