equal
deleted
inserted
replaced
25 |
25 |
26 (*-----------------------------------------------------------------*) |
26 (*-----------------------------------------------------------------*) |
27 (*cooper_pp: provefunction for the one-exstance quantifier elimination*) |
27 (*cooper_pp: provefunction for the one-exstance quantifier elimination*) |
28 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*) |
28 (* Here still only one problem : The proof for the arithmetical transformations done on the dvd atomic formulae*) |
29 (*-----------------------------------------------------------------*) |
29 (*-----------------------------------------------------------------*) |
|
30 |
|
31 |
|
32 (* Invoking the oracle *) |
|
33 |
|
34 fun pres_oracle sg t = |
|
35 invoke_oracle (the_context()) "presburger_oracle" |
|
36 (sg, CooperDec.COOPER_ORACLE t) ; |
30 |
37 |
31 val presburger_ss = simpset_of (theory "Presburger"); |
38 val presburger_ss = simpset_of (theory "Presburger"); |
32 |
39 |
33 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |
40 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = |
34 let val (xn1,p1) = variant_abs (xn,xT,p) |
41 let val (xn1,p1) = variant_abs (xn,xT,p) |
268 val (th, tac) = case (prop_of pre_thm) of |
275 val (th, tac) = case (prop_of pre_thm) of |
269 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
276 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
270 let val pth = |
277 let val pth = |
271 (* If quick_and_dirty then run without proof generation as oracle*) |
278 (* If quick_and_dirty then run without proof generation as oracle*) |
272 if !quick_and_dirty |
279 if !quick_and_dirty |
273 then assume (cterm_of sg |
280 then pres_oracle sg (Pattern.eta_long [] t1) |
|
281 (* |
|
282 assume (cterm_of sg |
274 (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) |
283 (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) |
|
284 *) |
275 else tmproof_of_int_qelim sg (Pattern.eta_long [] t1) |
285 else tmproof_of_int_qelim sg (Pattern.eta_long [] t1) |
276 in |
286 in |
277 (trace_msg ("calling procedure with term:\n" ^ |
287 (trace_msg ("calling procedure with term:\n" ^ |
278 Sign.string_of_term sg t1); |
288 Sign.string_of_term sg t1); |
279 ((pth RS iffD2) RS pre_thm, |
289 ((pth RS iffD2) RS pre_thm, |