748 |
748 |
749 (* Interface to HOL. *) |
749 (* Interface to HOL. *) |
750 local |
750 local |
751 open Conv |
751 open Conv |
752 val concl = Thm.dest_arg o Thm.cprop_of |
752 val concl = Thm.dest_arg o Thm.cprop_of |
753 fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u)) |
|
754 in |
753 in |
755 (* FIXME: Replace tryfind by get_first !! *) |
754 (* FIXME: Replace tryfind by get_first !! *) |
756 fun real_nonlinear_prover proof_method ctxt = |
755 fun real_nonlinear_prover proof_method ctxt = |
757 let |
756 let |
758 val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} = |
757 val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} = |
759 Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
758 Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
760 (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>)) |
759 (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>)) |
761 simple_cterm_ord |
760 Thm.term_ord |
762 fun mainf cert_choice translator (eqs, les, lts) = |
761 fun mainf cert_choice translator (eqs, les, lts) = |
763 let |
762 let |
764 val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs |
763 val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs |
765 val le0 = map (poly_of_term o Thm.dest_arg o concl) les |
764 val le0 = map (poly_of_term o Thm.dest_arg o concl) les |
766 val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts |
765 val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts |
849 |
848 |
850 (* A wrapper that tries to substitute away variables first. *) |
849 (* A wrapper that tries to substitute away variables first. *) |
851 |
850 |
852 local |
851 local |
853 open Conv |
852 open Conv |
854 fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u)) |
|
855 val concl = Thm.dest_arg o Thm.cprop_of |
853 val concl = Thm.dest_arg o Thm.cprop_of |
856 val shuffle1 = |
854 val shuffle1 = |
857 fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" |
855 fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" |
858 by (atomize (full)) (simp add: field_simps)}) |
856 by (atomize (full)) (simp add: field_simps)}) |
859 val shuffle2 = |
857 val shuffle2 = |
892 fun real_nonlinear_subst_prover prover ctxt = |
890 fun real_nonlinear_subst_prover prover ctxt = |
893 let |
891 let |
894 val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} = |
892 val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} = |
895 Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
893 Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
896 (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>)) |
894 (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>)) |
897 simple_cterm_ord |
895 Thm.term_ord |
898 |
896 |
899 fun make_substitution th = |
897 fun make_substitution th = |
900 let |
898 let |
901 val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th)) |
899 val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th)) |
902 val th1 = |
900 val th1 = |