773 end; |
773 end; |
774 |
774 |
775 val type_has_top_sort = |
775 val type_has_top_sort = |
776 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
776 exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
777 |
777 |
|
778 val neg_clausify = |
|
779 single |
|
780 #> Meson.make_clauses_unsorted |
|
781 #> map Clausifier.introduce_combinators_in_theorem |
|
782 #> Meson.finish_cnf |
|
783 |
778 fun generic_metis_tac mode ctxt ths i st0 = |
784 fun generic_metis_tac mode ctxt ths i st0 = |
779 let |
785 let |
780 val _ = trace_msg (fn () => |
786 val _ = trace_msg (fn () => |
781 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
787 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
782 in |
788 in |
783 if exists_type type_has_top_sort (prop_of st0) then |
789 if exists_type type_has_top_sort (prop_of st0) then |
784 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
790 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
785 else |
791 else |
786 Meson.MESON (maps Clausifier.neg_clausify) |
792 Meson.MESON (maps neg_clausify) |
787 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
793 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
788 ctxt i st0 |
794 ctxt i st0 |
789 handle ERROR msg => raise METIS ("generic_metis_tac", msg) |
795 handle ERROR msg => raise METIS ("generic_metis_tac", msg) |
790 end |
796 end |
791 handle METIS (loc, msg) => |
797 handle METIS (loc, msg) => |