373 end; |
373 end; |
374 |
374 |
375 local |
375 local |
376 val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) |
376 val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) |
377 fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) |
377 fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) |
378 fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u)); |
|
379 (* FIXME: Lookup in the context every time!!! Fix this !!!*) |
378 (* FIXME: Lookup in the context every time!!! Fix this !!!*) |
380 fun splitequation ctxt th acc = |
379 fun splitequation ctxt th acc = |
381 let |
380 let |
382 val real_poly_neg_conv = #neg |
381 val real_poly_neg_conv = #neg |
383 (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
382 (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
384 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) |
383 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) Thm.term_ord) |
385 val (th1,th2) = conj_pair(rawrule th) |
384 val (th1,th2) = conj_pair(rawrule th) |
386 in th1::fconv_rule (arg_conv (arg_conv (real_poly_neg_conv ctxt))) th2::acc |
385 in th1::fconv_rule (arg_conv (arg_conv (real_poly_neg_conv ctxt))) th2::acc |
387 end |
386 end |
388 in fun real_vector_prover ctxt _ translator (eqs,ges,gts) = |
387 in fun real_vector_prover ctxt _ translator (eqs,ges,gts) = |
389 (real_vector_ineq_prover ctxt translator |
388 (real_vector_ineq_prover ctxt translator |