1192 fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS |
1192 fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS |
1193 in |
1193 in |
1194 (* FIXME: Replace tryfind by get_first !! *) |
1194 (* FIXME: Replace tryfind by get_first !! *) |
1195 fun real_nonlinear_prover proof_method ctxt = |
1195 fun real_nonlinear_prover proof_method ctxt = |
1196 let |
1196 let |
1197 val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt |
1197 val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
1198 (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
1198 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
1199 simple_cterm_ord |
1199 simple_cterm_ord |
1200 val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, |
1200 val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, |
1201 real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) |
1201 real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) |
1202 fun mainf cert_choice translator (eqs,les,lts) = |
1202 fun mainf cert_choice translator (eqs,les,lts) = |
1203 let |
1203 let |
1307 end |
1307 end |
1308 in |
1308 in |
1309 |
1309 |
1310 fun real_nonlinear_subst_prover prover ctxt = |
1310 fun real_nonlinear_subst_prover prover ctxt = |
1311 let |
1311 let |
1312 val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt |
1312 val {add,mul,neg,pow,sub,main} = Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
1313 (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
1313 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
1314 simple_cterm_ord |
1314 simple_cterm_ord |
1315 |
1315 |
1316 val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, |
1316 val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv, |
1317 real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) |
1317 real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main) |
1318 |
1318 |