1.1 --- a/src/HOL/IsaMakefile	Fri Sep 02 14:43:20 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 02 14:43:20 2011 +0200
     1.3 @@ -234,7 +234,7 @@
     1.4    Tools/Meson/meson_clausify.ML \
     1.5    Tools/Meson/meson_tactic.ML \
     1.6    Tools/Metis/metis_reconstruct.ML \
     1.7 -  Tools/Metis/metis_tactics.ML \
     1.8 +  Tools/Metis/metis_tactic.ML \
     1.9    Tools/Metis/metis_translate.ML \
    1.10    Tools/abel_cancel.ML \
    1.11    Tools/arith_data.ML \

     2.1 --- a/src/HOL/Metis.thy	Fri Sep 02 14:43:20 2011 +0200
     2.2 +++ b/src/HOL/Metis.thy	Fri Sep 02 14:43:20 2011 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  uses "~~/src/Tools/Metis/metis.ML"
     2.5       ("Tools/Metis/metis_translate.ML")
     2.6       ("Tools/Metis/metis_reconstruct.ML")
     2.7 -     ("Tools/Metis/metis_tactics.ML")
     2.8 +     ("Tools/Metis/metis_tactic.ML")
     2.9       ("Tools/try_methods.ML")
    2.10  begin
    2.11  
    2.12 @@ -36,9 +36,9 @@
    2.13  
    2.14  use "Tools/Metis/metis_translate.ML"
    2.15  use "Tools/Metis/metis_reconstruct.ML"
    2.16 -use "Tools/Metis/metis_tactics.ML"
    2.17 +use "Tools/Metis/metis_tactic.ML"
    2.18  
    2.19 -setup {* Metis_Tactics.setup *}
    2.20 +setup {* Metis_Tactic.setup *}
    2.21  
    2.22  hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
    2.23  hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def

     3.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Sep 02 14:43:20 2011 +0200
     3.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Sep 02 14:43:20 2011 +0200
     3.3 @@ -70,7 +70,7 @@
     3.4        | tac (type_enc :: type_encs) st =
     3.5          st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
     3.6             |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
     3.7 -               THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1
     3.8 +               THEN Metis_Tactic.metis_tac [type_enc] ctxt ths 1
     3.9                 THEN COND (has_fewer_prems 2) all_tac no_tac
    3.10                 THEN tac type_encs)
    3.11    in tac end

     4.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 02 14:43:20 2011 +0200
     4.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Fri Sep 02 14:43:20 2011 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  
     4.5      val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
     4.6  
     4.7 -    fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts)
     4.8 +    fun metis ctxt = Metis_Tactic.metis_tac [] ctxt (thms @ facts)
     4.9    in
    4.10      (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    4.11      |> prefix (metis_tag id)

     5.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 02 14:43:20 2011 +0200
     5.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 02 14:43:20 2011 +0200
     5.3 @@ -577,15 +577,15 @@
     5.4            sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple"
     5.5            ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?"
     5.6            ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform"
     5.7 -          ORELSE' Metis_Tactics.metis_tac [] ctxt thms
     5.8 +          ORELSE' Metis_Tactic.metis_tac [] ctxt thms
     5.9          else if !reconstructor = "smt" then
    5.10            SMT_Solver.smt_tac ctxt thms
    5.11          else if full orelse !reconstructor = "metis (full_types)" then
    5.12 -          Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms
    5.13 +          Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms
    5.14          else if !reconstructor = "metis (no_types)" then
    5.15 -          Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms
    5.16 +          Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms
    5.17          else if !reconstructor = "metis" then
    5.18 -          Metis_Tactics.metis_tac [] ctxt thms
    5.19 +          Metis_Tactic.metis_tac [] ctxt thms
    5.20          else
    5.21            K all_tac
    5.22        end

     6.1 --- a/src/HOL/TPTP/CASC_Setup.thy	Fri Sep 02 14:43:20 2011 +0200
     6.2 +++ b/src/HOL/TPTP/CASC_Setup.thy	Fri Sep 02 14:43:20 2011 +0200
     6.3 @@ -131,7 +131,7 @@
     6.4                            Sledgehammer_Filter.no_relevance_override))
     6.5     ORELSE
     6.6     SOLVE_TIMEOUT (max_secs div 10) "metis"
     6.7 -       (ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
     6.8 +       (ALLGOALS (Metis_Tactic.metis_tac [] ctxt []))
     6.9     ORELSE
    6.10     SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
    6.11     ORELSE

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Sep 02 14:43:20 2011 +0200
     7.3 @@ -0,0 +1,268 @@
     7.4 +(*  Title:      HOL/Tools/Metis/metis_tactic.ML
     7.5 +    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     7.6 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     7.7 +    Author:     Jasmin Blanchette, TU Muenchen
     7.8 +    Copyright   Cambridge University 2007
     7.9 +
    7.10 +HOL setup for the Metis prover.
    7.11 +*)
    7.12 +
    7.13 +signature METIS_TACTIC =
    7.14 +sig
    7.15 +  val metisN : string
    7.16 +  val full_typesN : string
    7.17 +  val partial_typesN : string
    7.18 +  val no_typesN : string
    7.19 +  val really_full_type_enc : string
    7.20 +  val full_type_enc : string
    7.21 +  val partial_type_enc : string
    7.22 +  val no_type_enc : string
    7.23 +  val full_type_syss : string list
    7.24 +  val partial_type_syss : string list
    7.25 +  val trace : bool Config.T
    7.26 +  val verbose : bool Config.T
    7.27 +  val new_skolemizer : bool Config.T
    7.28 +  val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
    7.29 +  val setup : theory -> theory
    7.30 +end
    7.31 +
    7.32 +structure Metis_Tactic : METIS_TACTIC =
    7.33 +struct
    7.34 +
    7.35 +open ATP_Translate
    7.36 +open Metis_Translate
    7.37 +open Metis_Reconstruct
    7.38 +
    7.39 +val metisN = "metis"
    7.40 +
    7.41 +val full_typesN = "full_types"
    7.42 +val partial_typesN = "partial_types"
    7.43 +val no_typesN = "no_types"
    7.44 +
    7.45 +val really_full_type_enc = "mono_tags_uniform"
    7.46 +val full_type_enc = "poly_guards_uniform_query"
    7.47 +val partial_type_enc = "poly_args"
    7.48 +val no_type_enc = "erased"
    7.49 +
    7.50 +val full_type_syss = [full_type_enc, really_full_type_enc]
    7.51 +val partial_type_syss = partial_type_enc :: full_type_syss
    7.52 +
    7.53 +val type_enc_aliases =
    7.54 +  [(full_typesN, full_type_syss),
    7.55 +   (partial_typesN, partial_type_syss),
    7.56 +   (no_typesN, [no_type_enc])]
    7.57 +
    7.58 +fun method_call_for_type_enc type_syss =
    7.59 +  metisN ^ " (" ^
    7.60 +  (case AList.find (op =) type_enc_aliases type_syss of
    7.61 +     [alias] => alias
    7.62 +   | _ => hd type_syss) ^ ")"
    7.63 +
    7.64 +val new_skolemizer =
    7.65 +  Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    7.66 +
    7.67 +(* Designed to work also with monomorphic instances of polymorphic theorems. *)
    7.68 +fun have_common_thm ths1 ths2 =
    7.69 +  exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    7.70 +         (map Meson.make_meta_clause ths2)
    7.71 +
    7.72 +(*Determining which axiom clauses are actually used*)
    7.73 +fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    7.74 +  | used_axioms _ _ = NONE
    7.75 +
    7.76 +(* Lightweight predicate type information comes in two flavors, "t = t'" and
    7.77 +   "t => t'", where "t" and "t'" are the same term modulo type tags.
    7.78 +   In Isabelle, type tags are stripped away, so we are left with "t = t" or
    7.79 +   "t => t". Type tag idempotence is also handled this way. *)
    7.80 +fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
    7.81 +  let val thy = Proof_Context.theory_of ctxt in
    7.82 +    case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
    7.83 +      Const (@{const_name HOL.eq}, _) $ _ $ t =>
    7.84 +      let
    7.85 +        val ct = cterm_of thy t
    7.86 +        val cT = ctyp_of_term ct
    7.87 +      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    7.88 +    | Const (@{const_name disj}, _) $ t1 $ t2 =>
    7.89 +      (if can HOLogic.dest_not t1 then t2 else t1)
    7.90 +      |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
    7.91 +    | _ => raise Fail "unexpected tags sym clause"
    7.92 +  end
    7.93 +  |> Meson.make_meta_clause
    7.94 +
    7.95 +val clause_params =
    7.96 +  {ordering = Metis_KnuthBendixOrder.default,
    7.97 +   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    7.98 +   orderTerms = true}
    7.99 +val active_params =
   7.100 +  {clause = clause_params,
   7.101 +   prefactor = #prefactor Metis_Active.default,
   7.102 +   postfactor = #postfactor Metis_Active.default}
   7.103 +val waiting_params =
   7.104 +  {symbolsWeight = 1.0,
   7.105 +   variablesWeight = 0.0,
   7.106 +   literalsWeight = 0.0,
   7.107 +   models = []}
   7.108 +val resolution_params = {active = active_params, waiting = waiting_params}
   7.109 +
   7.110 +(* Main function to start Metis proof and reconstruction *)
   7.111 +fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
   7.112 +  let val thy = Proof_Context.theory_of ctxt
   7.113 +      val new_skolemizer =
   7.114 +        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
   7.115 +      val th_cls_pairs =
   7.116 +        map2 (fn j => fn th =>
   7.117 +                (Thm.get_name_hint th,
   7.118 +                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
   7.119 +             (0 upto length ths0 - 1) ths0
   7.120 +      val ths = maps (snd o snd) th_cls_pairs
   7.121 +      val dischargers = map (fst o snd) th_cls_pairs
   7.122 +      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   7.123 +      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   7.124 +      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
   7.125 +      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
   7.126 +      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   7.127 +      val type_enc = type_enc_from_string Sound type_enc
   7.128 +      val (sym_tab, axioms, old_skolems) =
   7.129 +        prepare_metis_problem ctxt type_enc cls ths
   7.130 +      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   7.131 +          reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
   7.132 +        | get_isa_thm _ (Isa_Raw ith) = ith
   7.133 +      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
   7.134 +      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
   7.135 +      val thms = axioms |> map fst
   7.136 +      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
   7.137 +      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
   7.138 +  in
   7.139 +      case filter (fn t => prop_of t aconv @{prop False}) cls of
   7.140 +          false_th :: _ => [false_th RS @{thm FalseE}]
   7.141 +        | [] =>
   7.142 +      case Metis_Resolution.new resolution_params
   7.143 +                                {axioms = thms, conjecture = []}
   7.144 +           |> Metis_Resolution.loop of
   7.145 +          Metis_Resolution.Contradiction mth =>
   7.146 +            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
   7.147 +                          Metis_Thm.toString mth)
   7.148 +                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   7.149 +                             (*add constraints arising from converting goal to clause form*)
   7.150 +                val proof = Metis_Proof.proof mth
   7.151 +                val result =
   7.152 +                  axioms
   7.153 +                  |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
   7.154 +                val used = map_filter (used_axioms axioms) proof
   7.155 +                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
   7.156 +                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
   7.157 +                val names = th_cls_pairs |> map fst
   7.158 +                val used_names =
   7.159 +                  th_cls_pairs
   7.160 +                  |> map_filter (fn (name, (_, cls)) =>
   7.161 +                                    if have_common_thm used cls then SOME name
   7.162 +                                    else NONE)
   7.163 +                val unused_names = names |> subtract (op =) used_names
   7.164 +            in
   7.165 +                if not (null cls) andalso not (have_common_thm used cls) then
   7.166 +                  verbose_warning ctxt "The assumptions are inconsistent"
   7.167 +                else
   7.168 +                  ();
   7.169 +                if not (null unused_names) then
   7.170 +                  "Unused theorems: " ^ commas_quote unused_names
   7.171 +                  |> verbose_warning ctxt
   7.172 +                else
   7.173 +                  ();
   7.174 +                case result of
   7.175 +                    (_,ith)::_ =>
   7.176 +                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   7.177 +                         [discharge_skolem_premises ctxt dischargers ith])
   7.178 +                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
   7.179 +            end
   7.180 +        | Metis_Resolution.Satisfiable _ =>
   7.181 +            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
   7.182 +             if null fallback_type_syss then
   7.183 +               ()
   7.184 +             else
   7.185 +               raise METIS ("FOL_SOLVE",
   7.186 +                            "No first-order proof with the lemmas supplied");
   7.187 +             [])
   7.188 +  end
   7.189 +  handle METIS (loc, msg) =>
   7.190 +         case fallback_type_syss of
   7.191 +           [] => error ("Failed to replay Metis proof in Isabelle." ^
   7.192 +                        (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
   7.193 +                         else ""))
   7.194 +         | _ =>
   7.195 +           (verbose_warning ctxt
   7.196 +                ("Falling back on " ^
   7.197 +                 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
   7.198 +            FOL_SOLVE fallback_type_syss ctxt cls ths0)
   7.199 +
   7.200 +fun neg_clausify ctxt =
   7.201 +  single
   7.202 +  #> Meson.make_clauses_unsorted ctxt
   7.203 +  #> map Meson_Clausify.introduce_combinators_in_theorem
   7.204 +  #> Meson.finish_cnf
   7.205 +
   7.206 +fun preskolem_tac ctxt st0 =
   7.207 +  (if exists (Meson.has_too_many_clauses ctxt)
   7.208 +             (Logic.prems_of_goal (prop_of st0) 1) then
   7.209 +     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
   7.210 +     THEN cnf.cnfx_rewrite_tac ctxt 1
   7.211 +   else
   7.212 +     all_tac) st0
   7.213 +
   7.214 +val type_has_top_sort =
   7.215 +  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   7.216 +
   7.217 +fun generic_metis_tac type_syss ctxt ths i st0 =
   7.218 +  let
   7.219 +    val _ = trace_msg ctxt (fn () =>
   7.220 +        "Metis called with theorems\n" ^
   7.221 +        cat_lines (map (Display.string_of_thm ctxt) ths))
   7.222 +    fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
   7.223 +  in
   7.224 +    if exists_type type_has_top_sort (prop_of st0) then
   7.225 +      verbose_warning ctxt "Proof state contains the universal sort {}"
   7.226 +    else
   7.227 +      ();
   7.228 +    Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
   7.229 +  end
   7.230 +
   7.231 +fun metis_tac [] = generic_metis_tac partial_type_syss
   7.232 +  | metis_tac type_syss = generic_metis_tac type_syss
   7.233 +
   7.234 +(* Whenever "X" has schematic type variables, we treat "using X by metis" as
   7.235 +   "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
   7.236 +   We don't do it for nonschematic facts "X" because this breaks a few proofs
   7.237 +   (in the rare and subtle case where a proof relied on extensionality not being
   7.238 +   applied) and brings few benefits. *)
   7.239 +val has_tvar =
   7.240 +  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   7.241 +
   7.242 +fun method default_type_syss (override_type_syss, ths) ctxt facts =
   7.243 +  let
   7.244 +    val _ =
   7.245 +      if default_type_syss = full_type_syss then
   7.246 +        legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
   7.247 +      else
   7.248 +        ()
   7.249 +    val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   7.250 +    val type_syss = override_type_syss |> the_default default_type_syss
   7.251 +  in
   7.252 +    HEADGOAL (Method.insert_tac nonschem_facts THEN'
   7.253 +              CHANGED_PROP
   7.254 +              o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   7.255 +  end
   7.256 +
   7.257 +fun setup_method (binding, type_syss) =
   7.258 +  ((Args.parens (Scan.repeat Parse.short_ident)
   7.259 +    >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
   7.260 +    |> Scan.option |> Scan.lift)
   7.261 +  -- Attrib.thms >> (METHOD oo method type_syss)
   7.262 +  |> Method.setup binding
   7.263 +
   7.264 +val setup =
   7.265 +  [((@{binding metis}, partial_type_syss),
   7.266 +    "Metis for FOL and HOL problems"),
   7.267 +   ((@{binding metisFT}, full_type_syss),
   7.268 +    "Metis for FOL/HOL problems with fully-typed translation")]
   7.269 +  |> fold (uncurry setup_method)
   7.270 +
   7.271 +end;

     8.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Fri Sep 02 14:43:20 2011 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,268 +0,0 @@
     8.4 -(*  Title:      HOL/Tools/Metis/metis_tactics.ML
     8.5 -    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     8.6 -    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     8.7 -    Author:     Jasmin Blanchette, TU Muenchen
     8.8 -    Copyright   Cambridge University 2007
     8.9 -
    8.10 -HOL setup for the Metis prover.
    8.11 -*)
    8.12 -
    8.13 -signature METIS_TACTICS =
    8.14 -sig
    8.15 -  val metisN : string
    8.16 -  val full_typesN : string
    8.17 -  val partial_typesN : string
    8.18 -  val no_typesN : string
    8.19 -  val really_full_type_enc : string
    8.20 -  val full_type_enc : string
    8.21 -  val partial_type_enc : string
    8.22 -  val no_type_enc : string
    8.23 -  val full_type_syss : string list
    8.24 -  val partial_type_syss : string list
    8.25 -  val trace : bool Config.T
    8.26 -  val verbose : bool Config.T
    8.27 -  val new_skolemizer : bool Config.T
    8.28 -  val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
    8.29 -  val setup : theory -> theory
    8.30 -end
    8.31 -
    8.32 -structure Metis_Tactics : METIS_TACTICS =
    8.33 -struct
    8.34 -
    8.35 -open ATP_Translate
    8.36 -open Metis_Translate
    8.37 -open Metis_Reconstruct
    8.38 -
    8.39 -val metisN = "metis"
    8.40 -
    8.41 -val full_typesN = "full_types"
    8.42 -val partial_typesN = "partial_types"
    8.43 -val no_typesN = "no_types"
    8.44 -
    8.45 -val really_full_type_enc = "mono_tags_uniform"
    8.46 -val full_type_enc = "poly_guards_uniform_query"
    8.47 -val partial_type_enc = "poly_args"
    8.48 -val no_type_enc = "erased"
    8.49 -
    8.50 -val full_type_syss = [full_type_enc, really_full_type_enc]
    8.51 -val partial_type_syss = partial_type_enc :: full_type_syss
    8.52 -
    8.53 -val type_enc_aliases =
    8.54 -  [(full_typesN, full_type_syss),
    8.55 -   (partial_typesN, partial_type_syss),
    8.56 -   (no_typesN, [no_type_enc])]
    8.57 -
    8.58 -fun method_call_for_type_enc type_syss =
    8.59 -  metisN ^ " (" ^
    8.60 -  (case AList.find (op =) type_enc_aliases type_syss of
    8.61 -     [alias] => alias
    8.62 -   | _ => hd type_syss) ^ ")"
    8.63 -
    8.64 -val new_skolemizer =
    8.65 -  Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    8.66 -
    8.67 -(* Designed to work also with monomorphic instances of polymorphic theorems. *)
    8.68 -fun have_common_thm ths1 ths2 =
    8.69 -  exists (member (Term.aconv_untyped o pairself prop_of) ths1)
    8.70 -         (map Meson.make_meta_clause ths2)
    8.71 -
    8.72 -(*Determining which axiom clauses are actually used*)
    8.73 -fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
    8.74 -  | used_axioms _ _ = NONE
    8.75 -
    8.76 -(* Lightweight predicate type information comes in two flavors, "t = t'" and
    8.77 -   "t => t'", where "t" and "t'" are the same term modulo type tags.
    8.78 -   In Isabelle, type tags are stripped away, so we are left with "t = t" or
    8.79 -   "t => t". Type tag idempotence is also handled this way. *)
    8.80 -fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
    8.81 -  let val thy = Proof_Context.theory_of ctxt in
    8.82 -    case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
    8.83 -      Const (@{const_name HOL.eq}, _) $ _ $ t =>
    8.84 -      let
    8.85 -        val ct = cterm_of thy t
    8.86 -        val cT = ctyp_of_term ct
    8.87 -      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    8.88 -    | Const (@{const_name disj}, _) $ t1 $ t2 =>
    8.89 -      (if can HOLogic.dest_not t1 then t2 else t1)
    8.90 -      |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
    8.91 -    | _ => raise Fail "unexpected tags sym clause"
    8.92 -  end
    8.93 -  |> Meson.make_meta_clause
    8.94 -
    8.95 -val clause_params =
    8.96 -  {ordering = Metis_KnuthBendixOrder.default,
    8.97 -   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    8.98 -   orderTerms = true}
    8.99 -val active_params =
   8.100 -  {clause = clause_params,
   8.101 -   prefactor = #prefactor Metis_Active.default,
   8.102 -   postfactor = #postfactor Metis_Active.default}
   8.103 -val waiting_params =
   8.104 -  {symbolsWeight = 1.0,
   8.105 -   variablesWeight = 0.0,
   8.106 -   literalsWeight = 0.0,
   8.107 -   models = []}
   8.108 -val resolution_params = {active = active_params, waiting = waiting_params}
   8.109 -
   8.110 -(* Main function to start Metis proof and reconstruction *)
   8.111 -fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
   8.112 -  let val thy = Proof_Context.theory_of ctxt
   8.113 -      val new_skolemizer =
   8.114 -        Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
   8.115 -      val th_cls_pairs =
   8.116 -        map2 (fn j => fn th =>
   8.117 -                (Thm.get_name_hint th,
   8.118 -                 Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
   8.119 -             (0 upto length ths0 - 1) ths0
   8.120 -      val ths = maps (snd o snd) th_cls_pairs
   8.121 -      val dischargers = map (fst o snd) th_cls_pairs
   8.122 -      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   8.123 -      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   8.124 -      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
   8.125 -      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
   8.126 -      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   8.127 -      val type_enc = type_enc_from_string Sound type_enc
   8.128 -      val (sym_tab, axioms, old_skolems) =
   8.129 -        prepare_metis_problem ctxt type_enc cls ths
   8.130 -      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   8.131 -          reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
   8.132 -        | get_isa_thm _ (Isa_Raw ith) = ith
   8.133 -      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
   8.134 -      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
   8.135 -      val thms = axioms |> map fst
   8.136 -      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
   8.137 -      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
   8.138 -  in
   8.139 -      case filter (fn t => prop_of t aconv @{prop False}) cls of
   8.140 -          false_th :: _ => [false_th RS @{thm FalseE}]
   8.141 -        | [] =>
   8.142 -      case Metis_Resolution.new resolution_params
   8.143 -                                {axioms = thms, conjecture = []}
   8.144 -           |> Metis_Resolution.loop of
   8.145 -          Metis_Resolution.Contradiction mth =>
   8.146 -            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
   8.147 -                          Metis_Thm.toString mth)
   8.148 -                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   8.149 -                             (*add constraints arising from converting goal to clause form*)
   8.150 -                val proof = Metis_Proof.proof mth
   8.151 -                val result =
   8.152 -                  axioms
   8.153 -                  |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
   8.154 -                val used = map_filter (used_axioms axioms) proof
   8.155 -                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
   8.156 -                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
   8.157 -                val names = th_cls_pairs |> map fst
   8.158 -                val used_names =
   8.159 -                  th_cls_pairs
   8.160 -                  |> map_filter (fn (name, (_, cls)) =>
   8.161 -                                    if have_common_thm used cls then SOME name
   8.162 -                                    else NONE)
   8.163 -                val unused_names = names |> subtract (op =) used_names
   8.164 -            in
   8.165 -                if not (null cls) andalso not (have_common_thm used cls) then
   8.166 -                  verbose_warning ctxt "The assumptions are inconsistent"
   8.167 -                else
   8.168 -                  ();
   8.169 -                if not (null unused_names) then
   8.170 -                  "Unused theorems: " ^ commas_quote unused_names
   8.171 -                  |> verbose_warning ctxt
   8.172 -                else
   8.173 -                  ();
   8.174 -                case result of
   8.175 -                    (_,ith)::_ =>
   8.176 -                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   8.177 -                         [discharge_skolem_premises ctxt dischargers ith])
   8.178 -                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
   8.179 -            end
   8.180 -        | Metis_Resolution.Satisfiable _ =>
   8.181 -            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
   8.182 -             if null fallback_type_syss then
   8.183 -               ()
   8.184 -             else
   8.185 -               raise METIS ("FOL_SOLVE",
   8.186 -                            "No first-order proof with the lemmas supplied");
   8.187 -             [])
   8.188 -  end
   8.189 -  handle METIS (loc, msg) =>
   8.190 -         case fallback_type_syss of
   8.191 -           [] => error ("Failed to replay Metis proof in Isabelle." ^
   8.192 -                        (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
   8.193 -                         else ""))
   8.194 -         | _ =>
   8.195 -           (verbose_warning ctxt
   8.196 -                ("Falling back on " ^
   8.197 -                 quote (method_call_for_type_enc fallback_type_syss) ^ "...");
   8.198 -            FOL_SOLVE fallback_type_syss ctxt cls ths0)
   8.199 -
   8.200 -fun neg_clausify ctxt =
   8.201 -  single
   8.202 -  #> Meson.make_clauses_unsorted ctxt
   8.203 -  #> map Meson_Clausify.introduce_combinators_in_theorem
   8.204 -  #> Meson.finish_cnf
   8.205 -
   8.206 -fun preskolem_tac ctxt st0 =
   8.207 -  (if exists (Meson.has_too_many_clauses ctxt)
   8.208 -             (Logic.prems_of_goal (prop_of st0) 1) then
   8.209 -     Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1
   8.210 -     THEN cnf.cnfx_rewrite_tac ctxt 1
   8.211 -   else
   8.212 -     all_tac) st0
   8.213 -
   8.214 -val type_has_top_sort =
   8.215 -  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   8.216 -
   8.217 -fun generic_metis_tac type_syss ctxt ths i st0 =
   8.218 -  let
   8.219 -    val _ = trace_msg ctxt (fn () =>
   8.220 -        "Metis called with theorems\n" ^
   8.221 -        cat_lines (map (Display.string_of_thm ctxt) ths))
   8.222 -    fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
   8.223 -  in
   8.224 -    if exists_type type_has_top_sort (prop_of st0) then
   8.225 -      verbose_warning ctxt "Proof state contains the universal sort {}"
   8.226 -    else
   8.227 -      ();
   8.228 -    Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
   8.229 -  end
   8.230 -
   8.231 -fun metis_tac [] = generic_metis_tac partial_type_syss
   8.232 -  | metis_tac type_syss = generic_metis_tac type_syss
   8.233 -
   8.234 -(* Whenever "X" has schematic type variables, we treat "using X by metis" as
   8.235 -   "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
   8.236 -   We don't do it for nonschematic facts "X" because this breaks a few proofs
   8.237 -   (in the rare and subtle case where a proof relied on extensionality not being
   8.238 -   applied) and brings few benefits. *)
   8.239 -val has_tvar =
   8.240 -  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
   8.241 -
   8.242 -fun method default_type_syss (override_type_syss, ths) ctxt facts =
   8.243 -  let
   8.244 -    val _ =
   8.245 -      if default_type_syss = full_type_syss then
   8.246 -        legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
   8.247 -      else
   8.248 -        ()
   8.249 -    val (schem_facts, nonschem_facts) = List.partition has_tvar facts
   8.250 -    val type_syss = override_type_syss |> the_default default_type_syss
   8.251 -  in
   8.252 -    HEADGOAL (Method.insert_tac nonschem_facts THEN'
   8.253 -              CHANGED_PROP
   8.254 -              o generic_metis_tac type_syss ctxt (schem_facts @ ths))
   8.255 -  end
   8.256 -
   8.257 -fun setup_method (binding, type_syss) =
   8.258 -  ((Args.parens (Scan.repeat Parse.short_ident)
   8.259 -    >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
   8.260 -    |> Scan.option |> Scan.lift)
   8.261 -  -- Attrib.thms >> (METHOD oo method type_syss)
   8.262 -  |> Method.setup binding
   8.263 -
   8.264 -val setup =
   8.265 -  [((@{binding metis}, partial_type_syss),
   8.266 -    "Metis for FOL and HOL problems"),
   8.267 -   ((@{binding metisFT}, full_type_syss),
   8.268 -    "Metis for FOL/HOL problems with fully-typed translation")]
   8.269 -  |> fold (uncurry setup_method)
   8.270 -
   8.271 -end;

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 02 14:43:20 2011 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Sep 02 14:43:20 2011 +0200
     9.3 @@ -299,7 +299,7 @@
     9.4  
     9.5  (* Sledgehammer the given subgoal *)
     9.6  
     9.7 -val default_minimize_prover = Metis_Tactics.metisN
     9.8 +val default_minimize_prover = Metis_Tactic.metisN
     9.9  
    9.10  val is_raw_param_relevant_for_minimize =
    9.11    member (op =) params_for_minimize o fst o unalias_raw_param

    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 02 14:43:20 2011 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 02 14:43:20 2011 +0200
    10.3 @@ -128,9 +128,9 @@
    10.4     "Async_Manager". *)
    10.5  val das_tool = "Sledgehammer"
    10.6  
    10.7 -val metisN = Metis_Tactics.metisN
    10.8 -val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN
    10.9 -val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN
   10.10 +val metisN = Metis_Tactic.metisN
   10.11 +val metis_full_typesN = metisN ^ "_" ^ Metis_Tactic.full_typesN
   10.12 +val metis_no_typesN = metisN ^ "_" ^ Metis_Tactic.no_typesN
   10.13  
   10.14  val metis_prover_infos =
   10.15    [(metisN, Metis),
   10.16 @@ -413,15 +413,15 @@
   10.17    in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
   10.18  
   10.19  fun tac_for_reconstructor Metis =
   10.20 -    Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc]
   10.21 +    Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc]
   10.22    | tac_for_reconstructor Metis_Full_Types =
   10.23 -    Metis_Tactics.metis_tac Metis_Tactics.full_type_syss
   10.24 +    Metis_Tactic.metis_tac Metis_Tactic.full_type_syss
   10.25    | tac_for_reconstructor Metis_No_Types =
   10.26 -    Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc]
   10.27 +    Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
   10.28    | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
   10.29  
   10.30  fun timed_reconstructor reconstructor debug timeout ths =
   10.31 -  (Config.put Metis_Tactics.verbose debug
   10.32 +  (Config.put Metis_Tactic.verbose debug
   10.33     #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))
   10.34    |> timed_apply timeout
   10.35  

    11.1 --- a/src/HOL/Tools/try_methods.ML	Fri Sep 02 14:43:20 2011 +0200
    11.2 +++ b/src/HOL/Tools/try_methods.ML	Fri Sep 02 14:43:20 2011 +0200
    11.3 @@ -113,7 +113,7 @@
    11.4  
    11.5  fun do_try_methods mode timeout_opt quad st =
    11.6    let
    11.7 -    val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false #>
    11.8 +    val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #>
    11.9        Config.put Lin_Arith.verbose false)
   11.10    in
   11.11      if mode = Normal then

    12.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Fri Sep 02 14:43:20 2011 +0200
    12.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri Sep 02 14:43:20 2011 +0200
    12.3 @@ -71,7 +71,7 @@
    12.4  fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
    12.5    case run_atp override_params relevance_override i i ctxt th of
    12.6      SOME facts =>
    12.7 -    Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    12.8 +    Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    12.9    | NONE => Seq.empty
   12.10  
   12.11  fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =