796 fun generic_metis_tac mode ctxt ths i st0 = |
796 fun generic_metis_tac mode ctxt ths i st0 = |
797 let |
797 let |
798 val thy = ProofContext.theory_of ctxt |
798 val thy = ProofContext.theory_of ctxt |
799 val _ = trace_msg (fn () => |
799 val _ = trace_msg (fn () => |
800 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
800 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
801 val timer = Timer.startRealTimer () (*###*) |
|
802 in |
801 in |
803 if exists_type type_has_top_sort (prop_of st0) then |
802 if exists_type type_has_top_sort (prop_of st0) then |
804 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
803 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
805 else |
804 else |
806 Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *) |
805 Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *) |
807 (maps neg_clausify) |
806 (maps neg_clausify) |
808 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
807 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
809 ctxt i st0 |
808 ctxt i st0 |
810 |> tap (fn _ => priority (" METIS " ^ |
|
811 cat_lines (map (Display.string_of_thm ctxt) ths) ^ |
|
812 string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ " ms")) (*###*) |
|
813 end |
809 end |
814 |
810 |
815 val metis_tac = generic_metis_tac HO |
811 val metis_tac = generic_metis_tac HO |
816 val metisF_tac = generic_metis_tac FO |
812 val metisF_tac = generic_metis_tac FO |
817 val metisFT_tac = generic_metis_tac FT |
813 val metisFT_tac = generic_metis_tac FT |