265 (trivial ct)) |
265 (trivial ct)) |
266 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
266 fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i) |
267 (* The result of the quantifier elimination *) |
267 (* The result of the quantifier elimination *) |
268 val (th, tac) = case (prop_of pre_thm) of |
268 val (th, tac) = case (prop_of pre_thm) of |
269 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
269 Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ => |
|
270 let val pth = |
|
271 (* If quick_and_dirty then run without proof generation as oracle*) |
|
272 if !quick_and_dirty |
|
273 then assume (cterm_of sg |
|
274 (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) |
|
275 else tmproof_of_int_qelim sg (Pattern.eta_long [] t1) |
|
276 in |
270 (trace_msg ("calling procedure with term:\n" ^ |
277 (trace_msg ("calling procedure with term:\n" ^ |
271 Sign.string_of_term sg t1); |
278 Sign.string_of_term sg t1); |
272 ((tmproof_of_int_qelim sg (Pattern.eta_long [] t1) RS iffD2) RS pre_thm, |
279 ((pth RS iffD2) RS pre_thm, |
273 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
280 assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))) |
|
281 end |
274 | _ => (pre_thm, assm_tac i) |
282 | _ => (pre_thm, assm_tac i) |
275 in (rtac (((mp_step nh) o (spec_step np)) th) i |
283 in (rtac (((mp_step nh) o (spec_step np)) th) i |
276 THEN tac) st |
284 THEN tac) st |
277 end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st); |
285 end handle Subscript => no_tac st | CooperDec.COOPER => no_tac st); |
278 |
286 |