src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 39112 611e41ef07c3
parent 39038 dfea12cc5f5a
child 39114 240e2b41a041
equal deleted inserted replaced
39111:2e9bdc6fbedf 39112:611e41ef07c3
   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 () (*###*)
   801   in
   802   in
   802     if exists_type type_has_top_sort (prop_of st0) then
   803     if exists_type type_has_top_sort (prop_of st0) then
   803       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
   804       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
   804     else
   805     else
   805       Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
   806       Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
   806                   (maps neg_clausify)
   807                   (maps neg_clausify)
   807                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   808                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   808                   ctxt i st0
   809                   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")) (*###*)
   809   end
   813   end
   810 
   814 
   811 val metis_tac = generic_metis_tac HO
   815 val metis_tac = generic_metis_tac HO
   812 val metisF_tac = generic_metis_tac FO
   816 val metisF_tac = generic_metis_tac FO
   813 val metisFT_tac = generic_metis_tac FT
   817 val metisFT_tac = generic_metis_tac FT