equal
deleted
inserted
replaced
42 val plusinf : term -> term -> term |
42 val plusinf : term -> term -> term |
43 val onatoms : (term -> term) -> term -> term |
43 val onatoms : (term -> term) -> term -> term |
44 val evalc : term -> term |
44 val evalc : term -> term |
45 val cooper_w : string list -> term -> (term option * term) |
45 val cooper_w : string list -> term -> (term option * term) |
46 val integer_qelim : Term.term -> Term.term |
46 val integer_qelim : Term.term -> Term.term |
47 val presburger_oracle : theory -> term -> term |
|
48 end; |
47 end; |
49 |
48 |
50 structure CooperDec : COOPER_DEC = |
49 structure CooperDec : COOPER_DEC = |
51 struct |
50 struct |
52 |
51 |
936 *) |
935 *) |
937 |
936 |
938 |
937 |
939 val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; |
938 val integer_qelim = simpl o evalc o (lift_qelim linform (cnnf posineq o evalc) cooper is_arith_rel) ; |
940 |
939 |
941 fun presburger_oracle thy t = |
|
942 if (!quick_and_dirty) |
|
943 then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t)) |
|
944 else error "Presburger oracle: not in quick_and_dirty mode" |
|
945 end; |
940 end; |