src/HOL/Tools/Metis/metis_tactics.ML

more preparations towards hijacking Metis

(*  Title:      HOL/Tools/Metis/metis_tactics.ML
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   Cambridge University 2007

HOL setup for the Metis prover.
*)

signature METIS_TACTICS =
sig
  val metisN : string
  val metisFT_N : string
  val trace : bool Config.T
  val verbose : bool Config.T
  val new_skolemizer : bool Config.T
  val old_metis_tac : Proof.context -> thm list -> int -> tactic
  val old_metisF_tac : Proof.context -> thm list -> int -> tactic
  val old_metisH_tac : Proof.context -> thm list -> int -> tactic
  val old_metisFT_tac : Proof.context -> thm list -> int -> tactic
  val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic
  val new_metisFT_tac : Proof.context -> thm list -> int -> tactic
  val setup : theory -> theory
end

structure Metis_Tactics : METIS_TACTICS =
struct

open ATP_Translate
open Metis_Translate
open Metis_Reconstruct

val full_typesN = "full_types"
val default_unsound_type_sys = "poly_args"
val default_sound_type_sys = "poly_preds_query"

fun method_call_for_mode HO = (@{binding metis}, "")
  | method_call_for_mode FO = (@{binding metisF}, "")
  | method_call_for_mode FT = (@{binding metisFT}, "")
  | method_call_for_mode (Type_Sys type_sys) =
    if type_sys = default_sound_type_sys then
      (@{binding new_metisFT}, "")
    else
      (@{binding new_metis},
       if type_sys = default_unsound_type_sys then "" else type_sys)

val metisN = Binding.qualified_name_of @{binding metis}
val metisFT_N = Binding.qualified_name_of @{binding metisFT}

val new_skolemizer =
  Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)

(* Designed to work also with monomorphic instances of polymorphic theorems. *)
fun have_common_thm ths1 ths2 =
  exists (member (untyped_aconv o pairself prop_of) ths1)
         (map Meson.make_meta_clause ths2)

(*Determining which axiom clauses are actually used*)
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
  | used_axioms _ _ = NONE

(* Lightweight predicate type information comes in two flavors, "t = t'" and
   "t => t'", where "t" and "t'" are the same term modulo type tags.
   In Isabelle, type tags are stripped away, so we are left with "t = t" or
   "t => t". Type tag idempotence is also handled this way. *)
fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
  let val thy = Proof_Context.theory_of ctxt in
    case hol_clause_from_metis ctxt sym_tab old_skolems mth of
      Const (@{const_name HOL.eq}, _) $ _ $ t =>
      t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
    | Const (@{const_name disj}, _) $ t1 $ t2 =>
      (if can HOLogic.dest_not t1 then t2 else t1)
      |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
    | _ => raise Fail "unexpected tags sym clause"
  end
  |> Meson.make_meta_clause

val clause_params =
  {ordering = Metis_KnuthBendixOrder.default,
   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
   orderTerms = true}
val active_params =
  {clause = clause_params,
   prefactor = #prefactor Metis_Active.default,
   postfactor = #postfactor Metis_Active.default}
val waiting_params =
  {symbolsWeight = 1.0,
   variablesWeight = 0.0,
   literalsWeight = 0.0,
   models = []}
val resolution_params = {active = active_params, waiting = waiting_params}

(* Main function to start Metis proof and reconstruction *)
fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
  let val thy = Proof_Context.theory_of ctxt
      val new_skolemizer =
        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
      val th_cls_pairs =
        map2 (fn j => fn th =>
                (Thm.get_name_hint th,
                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
             (0 upto length ths0 - 1) ths0
      val ths = maps (snd o snd) th_cls_pairs
      val dischargers = map (fst o snd) th_cls_pairs
      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
      val (mode, sym_tab, {axioms, old_skolems, ...}) =
        prepare_metis_problem ctxt mode cls ths
      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
          reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
        | get_isa_thm _ (Isa_Raw ith) = ith
      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
      val thms = axioms |> map fst
      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
      val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
  in
      case filter (fn t => prop_of t aconv @{prop False}) cls of
          false_th :: _ => [false_th RS @{thm FalseE}]
        | [] =>
      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
           |> Metis_Resolution.loop of
          Metis_Resolution.Contradiction mth =>
            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
                          Metis_Thm.toString mth)
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
                             (*add constraints arising from converting goal to clause form*)
                val proof = Metis_Proof.proof mth
                val result =
                  fold (replay_one_inference ctxt' mode old_skolems sym_tab)
                       proof axioms
                val used = map_filter (used_axioms axioms) proof
                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
                val names = th_cls_pairs |> map fst
                val used_names =
                  th_cls_pairs
                  |> map_filter (fn (name, (_, cls)) =>
                                    if have_common_thm used cls then SOME name
                                    else NONE)
                val unused_names = names |> subtract (op =) used_names
            in
                if not (null cls) andalso not (have_common_thm used cls) then
                  verbose_warning ctxt "The assumptions are inconsistent"
                else
                  ();
                if not (null unused_names) then
                  "Unused theorems: " ^ commas_quote unused_names
                  |> verbose_warning ctxt
                else
                  ();
                case result of
                    (_,ith)::_ =>
                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
                         [discharge_skolem_premises ctxt dischargers ith])
                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
            end
        | Metis_Resolution.Satisfiable _ =>
            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
             if null fallback_modes then
               ()
             else
               raise METIS ("FOL_SOLVE",
                            "No first-order proof with the lemmas supplied");
             [])
  end
  handle METIS (loc, msg) =>
         case fallback_modes of
           [] => error ("Failed to replay Metis proof in Isabelle." ^
                        (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
                         else ""))
         | mode :: _ =>
           let val (binding, arg) = method_call_for_mode mode in
             (verbose_warning ctxt
                  ("Falling back on " ^
                   quote (Binding.qualified_name_of binding ^
                          (arg |> arg <> "" ? enclose " (" ")")) ^ "...");
              FOL_SOLVE fallback_modes ctxt cls ths0)
            end

val neg_clausify =
  single
  #> Meson.make_clauses_unsorted
  #> map Meson_Clausify.introduce_combinators_in_theorem
  #> Meson.finish_cnf

fun preskolem_tac ctxt st0 =
  (if exists (Meson.has_too_many_clauses ctxt)
             (Logic.prems_of_goal (prop_of st0) 1) then
     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
     THEN cnf.cnfx_rewrite_tac ctxt 1
   else
     all_tac) st0

val type_has_top_sort =
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)

fun generic_metis_tac modes ctxt ths i st0 =
  let
    val _ = trace_msg ctxt (fn () =>
        "Metis called with theorems\n" ^
        cat_lines (map (Display.string_of_thm ctxt) ths))
    fun tac clause = resolve_tac (FOL_SOLVE modes ctxt clause ths) 1
  in
    if exists_type type_has_top_sort (prop_of st0) then
      (verbose_warning ctxt "Proof state contains the universal sort {}";
       Seq.empty)
    else
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0
  end

val old_metis_modes = [HO, FT]
val old_metisF_modes = [FO, FT]
val old_metisH_modes = [HO]
val old_metisFT_modes = [FT]
val new_metis_default_modes =
  map Type_Sys [default_unsound_type_sys, default_sound_type_sys]
val new_metisFT_modes = [Type_Sys default_sound_type_sys]

val old_metis_tac = generic_metis_tac old_metis_modes
val old_metisF_tac = generic_metis_tac old_metisF_modes
val old_metisH_tac = generic_metis_tac old_metisH_modes
val old_metisFT_tac = generic_metis_tac old_metisFT_modes
fun new_metis_tac [] = generic_metis_tac new_metis_default_modes
  | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss)
val new_metisFT_tac = generic_metis_tac new_metisFT_modes

(* Whenever "X" has schematic type variables, we treat "using X by metis" as
   "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
   We don't do it for nonschematic facts "X" because this breaks a few proofs
   (in the rare and subtle case where a proof relied on extensionality not being
   applied) and brings few benefits. *)
val has_tvar =
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of

fun method modes (type_sys, ths) ctxt facts =
  let
    val (schem_facts, nonschem_facts) = List.partition has_tvar facts
    val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes
  in
    HEADGOAL (Method.insert_tac nonschem_facts THEN'
              CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths))
  end

fun setup_method (modes as mode :: _) =
  (if modes = new_metis_default_modes then
     (Args.parens Parse.short_ident
      >> (fn s => if s = full_typesN then default_sound_type_sys else s))
     |> Scan.option |> Scan.lift
   else
     Scan.succeed NONE)
  -- Attrib.thms >> (METHOD oo method modes)
  |> Method.setup (fst (method_call_for_mode mode))

val setup =
  [(old_metis_modes, "Metis for FOL and HOL problems"),
   (old_metisF_modes, "Metis for FOL problems (legacy)"),
   (old_metisFT_modes,
    "Metis for FOL/HOL problems with fully-typed translation"),
   (new_metis_default_modes, "Metis for FOL and HOL problems (experimental)"),
   (new_metisFT_modes,
    "Metis for FOL/HOL problems with fully-typed translation (experimental)")]
  |> fold (uncurry setup_method)

end;