src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Mon Jun 21 12:31:41 2010 +0200 (2010-06-21 ago)
changeset 37479 f6b1ee5b420b
parent 37417 0714ece49081
child 37498 b426cbdb5a23
permissions -rw-r--r--
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
     1 (*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
     2     Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
     3     Copyright   Cambridge University 2007
     4 
     5 HOL setup for the Metis prover.
     6 *)
     7 
     8 signature METIS_TACTICS =
     9 sig
    10   val trace: bool Unsynchronized.ref
    11   val type_lits: bool Config.T
    12   val metis_tac: Proof.context -> thm list -> int -> tactic
    13   val metisF_tac: Proof.context -> thm list -> int -> tactic
    14   val metisFT_tac: Proof.context -> thm list -> int -> tactic
    15   val setup: theory -> theory
    16 end
    17 
    18 structure Metis_Tactics : METIS_TACTICS =
    19 struct
    20 
    21 open Sledgehammer_Util
    22 open Sledgehammer_FOL_Clause
    23 open Sledgehammer_Fact_Preprocessor
    24 open Sledgehammer_HOL_Clause
    25 open Sledgehammer_Proof_Reconstruct
    26 open Sledgehammer_Fact_Filter
    27 
    28 val trace = Unsynchronized.ref false;
    29 fun trace_msg msg = if !trace then tracing (msg ()) else ();
    30 
    31 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
    32 
    33 datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
    34 
    35 (* ------------------------------------------------------------------------- *)
    36 (* Useful Theorems                                                           *)
    37 (* ------------------------------------------------------------------------- *)
    38 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
    39 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    40 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
    41 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
    42 
    43 (* ------------------------------------------------------------------------- *)
    44 (* Useful Functions                                                          *)
    45 (* ------------------------------------------------------------------------- *)
    46 
    47 (* Match untyped terms. *)
    48 fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
    49   | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
    50   | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
    51     (a = b) (* The index is ignored, for some reason. *)
    52   | untyped_aconv (Bound i) (Bound j) = (i = j)
    53   | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
    54   | untyped_aconv (t1 $ t2) (u1 $ u2) =
    55     untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    56   | untyped_aconv _ _ = false
    57 
    58 (* Finding the relative location of an untyped term within a list of terms *)
    59 fun get_index lit =
    60   let val lit = Envir.eta_contract lit
    61       fun get n [] = raise Empty
    62         | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    63                           then n  else get (n+1) xs
    64   in get 1 end;
    65 
    66 (* ------------------------------------------------------------------------- *)
    67 (* HOL to FOL  (Isabelle to Metis)                                           *)
    68 (* ------------------------------------------------------------------------- *)
    69 
    70 fun fn_isa_to_met "equal" = "="
    71   | fn_isa_to_met x       = x;
    72 
    73 fun metis_lit b c args = (b, (c, args));
    74 
    75 fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
    76   | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
    77   | hol_type_to_fol (TyConstr ((s, _), tps)) =
    78     Metis.Term.Fn (s, map hol_type_to_fol tps);
    79 
    80 (*These two functions insert type literals before the real literals. That is the
    81   opposite order from TPTP linkup, but maybe OK.*)
    82 
    83 fun hol_term_to_fol_FO tm =
    84   case strip_combterm_comb tm of
    85       (CombConst ((c, _), _, tys), tms) =>
    86         let val tyargs = map hol_type_to_fol tys
    87             val args   = map hol_term_to_fol_FO tms
    88         in Metis.Term.Fn (c, tyargs @ args) end
    89     | (CombVar ((v, _), _), []) => Metis.Term.Var v
    90     | _ => raise Fail "hol_term_to_fol_FO";
    91 
    92 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    93   | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    94       Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    95   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    96        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    97 
    98 (*The fully-typed translation, to avoid type errors*)
    99 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
   100 
   101 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
   102   | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
   103       wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   104   | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
   105        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   106                   type_of_combterm tm);
   107 
   108 fun hol_literal_to_fol FO (Literal (pol, tm)) =
   109       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
   110           val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   111           val lits = map hol_term_to_fol_FO tms
   112       in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   113   | hol_literal_to_fol HO (Literal (pol, tm)) =
   114      (case strip_combterm_comb tm of
   115           (CombConst(("equal", _), _, _), tms) =>
   116             metis_lit pol "=" (map hol_term_to_fol_HO tms)
   117         | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   118   | hol_literal_to_fol FT (Literal (pol, tm)) =
   119      (case strip_combterm_comb tm of
   120           (CombConst(("equal", _), _, _), tms) =>
   121             metis_lit pol "=" (map hol_term_to_fol_FT tms)
   122         | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   123 
   124 fun literals_of_hol_term thy mode t =
   125       let val (lits, types_sorts) = literals_of_term thy t
   126       in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   127 
   128 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   129 fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
   130     metis_lit pos s [Metis.Term.Var s']
   131   | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
   132     metis_lit pos s [Metis.Term.Fn (s',[])]
   133 
   134 fun default_sort _ (TVar _) = false
   135   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   136 
   137 fun metis_of_tfree tf =
   138   Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
   139 
   140 fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
   141   let
   142     val thy = ProofContext.theory_of ctxt
   143     val (skolem_somes, (mlits, types_sorts)) =
   144      th |> prop_of |> conceal_skolem_somes j skolem_somes
   145         ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   146   in
   147       if is_conjecture then
   148           (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
   149            type_literals_for_types types_sorts, skolem_somes)
   150       else
   151         let val tylits = filter_out (default_sort ctxt) types_sorts
   152                          |> type_literals_for_types
   153             val mtylits = if Config.get ctxt type_lits
   154                           then map (metis_of_type_literals false) tylits else []
   155         in
   156           (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
   157            skolem_somes)
   158         end
   159   end;
   160 
   161 (* ARITY CLAUSE *)
   162 
   163 fun m_arity_cls (TConsLit (c,t,args)) =
   164       metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   165   | m_arity_cls (TVarLit (c,str))     =
   166       metis_lit false (make_type_class c) [Metis.Term.Var str];
   167 
   168 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   169 fun arity_cls (ArityClause {conclLit, premLits, ...}) =
   170   (TrueI,
   171    Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   172 
   173 (* CLASSREL CLAUSE *)
   174 
   175 fun m_classrel_cls subclass superclass =
   176   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   177 
   178 fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
   179   (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   180 
   181 (* ------------------------------------------------------------------------- *)
   182 (* FOL to HOL  (Metis to Isabelle)                                           *)
   183 (* ------------------------------------------------------------------------- *)
   184 
   185 datatype term_or_type = Term of Term.term | Type of Term.typ;
   186 
   187 fun terms_of [] = []
   188   | terms_of (Term t :: tts) = t :: terms_of tts
   189   | terms_of (Type _ :: tts) = terms_of tts;
   190 
   191 fun types_of [] = []
   192   | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
   193       if String.isPrefix "_" a then
   194           (*Variable generated by Metis, which might have been a type variable.*)
   195           TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   196       else types_of tts
   197   | types_of (Term _ :: tts) = types_of tts
   198   | types_of (Type T :: tts) = T :: types_of tts;
   199 
   200 fun apply_list rator nargs rands =
   201   let val trands = terms_of rands
   202   in  if length trands = nargs then Term (list_comb(rator, trands))
   203       else raise Fail
   204         ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   205           " expected " ^ Int.toString nargs ^
   206           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   207   end;
   208 
   209 fun infer_types ctxt =
   210   Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
   211 
   212 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   213   with variable constraints in the goal...at least, type inference often fails otherwise.
   214   SEE ALSO axiom_inf below.*)
   215 fun mk_var (w,T) = Term.Var((w,1), T);
   216 
   217 (*include the default sort, if available*)
   218 fun mk_tfree ctxt w =
   219   let val ww = "'" ^ w
   220   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   221 
   222 (*Remove the "apply" operator from an HO term*)
   223 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   224   | strip_happ args x = (x, args);
   225 
   226 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
   227 
   228 fun fol_type_to_isa _ (Metis.Term.Var v) =
   229      (case strip_prefix tvar_prefix v of
   230           SOME w => make_tvar w
   231         | NONE   => make_tvar v)
   232   | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   233      (case strip_prefix tconst_prefix x of
   234           SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   235         | NONE    =>
   236       case strip_prefix tfree_prefix x of
   237           SOME tf => mk_tfree ctxt tf
   238         | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
   239 
   240 fun reveal_skolem_somes skolem_somes =
   241   map_aterms (fn t as Const (s, T) =>
   242                  if String.isPrefix skolem_theory_name s then
   243                    AList.lookup (op =) skolem_somes s
   244                    |> the |> map_types Type_Infer.paramify_vars
   245                  else
   246                    t
   247                | t => t)
   248 
   249 (*Maps metis terms to isabelle terms*)
   250 fun hol_term_from_fol_PT ctxt fol_tm =
   251   let val thy = ProofContext.theory_of ctxt
   252       val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
   253                                   Metis.Term.toString fol_tm)
   254       fun tm_to_tt (Metis.Term.Var v) =
   255              (case strip_prefix tvar_prefix v of
   256                   SOME w => Type (make_tvar w)
   257                 | NONE =>
   258               case strip_prefix schematic_var_prefix v of
   259                   SOME w => Term (mk_var (w, HOLogic.typeT))
   260                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   261                     (*Var from Metis with a name like _nnn; possibly a type variable*)
   262         | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   263         | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   264             let val (rator,rands) = strip_happ [] t
   265             in  case rator of
   266                     Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   267                   | _ => case tm_to_tt rator of
   268                              Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   269                            | _ => raise Fail "tm_to_tt: HO application"
   270             end
   271         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   272       and applic_to_tt ("=",ts) =
   273             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   274         | applic_to_tt (a,ts) =
   275             case strip_prefix const_prefix a of
   276                 SOME b =>
   277                   let val c = invert_const b
   278                       val ntypes = num_type_args thy c
   279                       val nterms = length ts - ntypes
   280                       val tts = map tm_to_tt ts
   281                       val tys = types_of (List.take(tts,ntypes))
   282                   in if length tys = ntypes then
   283                          apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   284                      else
   285                        raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
   286                                    " but gets " ^ Int.toString (length tys) ^
   287                                    " type arguments\n" ^
   288                                    cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   289                                    " the terms are \n" ^
   290                                    cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   291                      end
   292               | NONE => (*Not a constant. Is it a type constructor?*)
   293             case strip_prefix tconst_prefix a of
   294                 SOME b =>
   295                   Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
   296               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   297             case strip_prefix tfree_prefix a of
   298                 SOME b => Type (mk_tfree ctxt b)
   299               | NONE => (*a fixed variable? They are Skolem functions.*)
   300             case strip_prefix fixed_var_prefix a of
   301                 SOME b =>
   302                   let val opr = Term.Free(b, HOLogic.typeT)
   303                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
   304               | NONE => raise Fail ("unexpected metis function: " ^ a)
   305   in
   306     case tm_to_tt fol_tm of
   307       Term t => t
   308     | _ => raise Fail "fol_tm_to_tt: Term expected"
   309   end
   310 
   311 (*Maps fully-typed metis terms to isabelle terms*)
   312 fun hol_term_from_fol_FT ctxt fol_tm =
   313   let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
   314                                   Metis.Term.toString fol_tm)
   315       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   316              (case strip_prefix schematic_var_prefix v of
   317                   SOME w =>  mk_var(w, dummyT)
   318                 | NONE   => mk_var(v, dummyT))
   319         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   320             Const ("op =", HOLogic.typeT)
   321         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   322            (case strip_prefix const_prefix x of
   323                 SOME c => Const (invert_const c, dummyT)
   324               | NONE => (*Not a constant. Is it a fixed variable??*)
   325             case strip_prefix fixed_var_prefix x of
   326                 SOME v => Free (v, fol_type_to_isa ctxt ty)
   327               | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
   328         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   329             cvt tm1 $ cvt tm2
   330         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   331             cvt tm1 $ cvt tm2
   332         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   333         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   334             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
   335         | cvt (t as Metis.Term.Fn (x, [])) =
   336            (case strip_prefix const_prefix x of
   337                 SOME c => Const (invert_const c, dummyT)
   338               | NONE => (*Not a constant. Is it a fixed variable??*)
   339             case strip_prefix fixed_var_prefix x of
   340                 SOME v => Free (v, dummyT)
   341               | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
   342                   hol_term_from_fol_PT ctxt t))
   343         | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
   344             hol_term_from_fol_PT ctxt t)
   345   in fol_tm |> cvt end
   346 
   347 fun hol_term_from_fol FT = hol_term_from_fol_FT
   348   | hol_term_from_fol _ = hol_term_from_fol_PT
   349 
   350 fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
   351   let val thy = ProofContext.theory_of ctxt
   352       val ts = map (hol_term_from_fol mode ctxt) fol_tms
   353       val _ = trace_msg (fn () => "  calling type inference:")
   354       val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   355       val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
   356       val _ = app (fn t => trace_msg
   357                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   358                               "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   359                   ts'
   360   in  ts'  end;
   361 
   362 fun mk_not (Const (@{const_name Not}, _) $ b) = b
   363   | mk_not b = HOLogic.mk_not b;
   364 
   365 val metis_eq = Metis.Term.Fn ("=", []);
   366 
   367 (* ------------------------------------------------------------------------- *)
   368 (* FOL step Inference Rules                                                  *)
   369 (* ------------------------------------------------------------------------- *)
   370 
   371 (*for debugging only*)
   372 fun print_thpair (fth,th) =
   373   (trace_msg (fn () => "=============================================");
   374    trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
   375    trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   376 
   377 fun lookth thpairs (fth : Metis.Thm.thm) =
   378   the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   379   handle Option =>
   380          raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   381 
   382 fun is_TrueI th = Thm.eq_thm(TrueI,th);
   383 
   384 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   385 
   386 fun inst_excluded_middle thy i_atm =
   387   let val th = EXCLUDED_MIDDLE
   388       val [vx] = Term.add_vars (prop_of th) []
   389       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   390   in  cterm_instantiate substs th  end;
   391 
   392 (* INFERENCE RULE: AXIOM *)
   393 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
   394     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   395 
   396 (* INFERENCE RULE: ASSUME *)
   397 fun assume_inf ctxt mode skolem_somes atm =
   398   inst_excluded_middle
   399     (ProofContext.theory_of ctxt)
   400     (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
   401 
   402 (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   403    them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   404    that new TVars are distinct and that types can be inferred from terms.*)
   405 fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
   406   let val thy = ProofContext.theory_of ctxt
   407       val i_th   = lookth thpairs th
   408       val i_th_vars = Term.add_vars (prop_of i_th) []
   409       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   410       fun subst_translation (x,y) =
   411             let val v = find_var x
   412                 (* We call "reveal_skolem_somes" and "infer_types" below. *)
   413                 val t = hol_term_from_fol mode ctxt y
   414             in  SOME (cterm_of thy (Var v), t)  end
   415             handle Option =>
   416                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   417                                        " in " ^ Display.string_of_thm ctxt i_th);
   418                  NONE)
   419       fun remove_typeinst (a, t) =
   420             case strip_prefix schematic_var_prefix a of
   421                 SOME b => SOME (b, t)
   422               | NONE   => case strip_prefix tvar_prefix a of
   423                 SOME _ => NONE          (*type instantiations are forbidden!*)
   424               | NONE   => SOME (a,t)    (*internal Metis var?*)
   425       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   426       val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   427       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   428       val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
   429                        |> infer_types ctxt
   430       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   431       val substs' = ListPair.zip (vars, map ctm_of tms)
   432       val _ = trace_msg (fn () =>
   433         cat_lines ("subst_translations:" ::
   434           (substs' |> map (fn (x, y) =>
   435             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   436             Syntax.string_of_term ctxt (term_of y)))));
   437   in cterm_instantiate substs' i_th end
   438   handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
   439        | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
   440                              "\n(Perhaps you want to try \"metisFT\" if you \
   441                              \haven't done so already.)")
   442 
   443 (* INFERENCE RULE: RESOLVE *)
   444 
   445 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   446   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   447   could then fail. See comment on mk_var.*)
   448 fun resolve_inc_tyvars(tha,i,thb) =
   449   let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   450       val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   451   in
   452       case distinct Thm.eq_thm ths of
   453         [th] => th
   454       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   455   end;
   456 
   457 fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
   458   let
   459     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   460     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   461     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   462   in
   463     if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   464     else if is_TrueI i_th2 then i_th1
   465     else
   466       let
   467         val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
   468                               (Metis.Term.Fn atm)
   469         val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   470         val prems_th1 = prems_of i_th1
   471         val prems_th2 = prems_of i_th2
   472         val index_th1 = get_index (mk_not i_atm) prems_th1
   473               handle Empty => raise Fail "Failed to find literal in th1"
   474         val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   475         val index_th2 = get_index i_atm prems_th2
   476               handle Empty => raise Fail "Failed to find literal in th2"
   477         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   478     in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   479   end;
   480 
   481 (* INFERENCE RULE: REFL *)
   482 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   483 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   484 
   485 fun refl_inf ctxt mode skolem_somes t =
   486   let val thy = ProofContext.theory_of ctxt
   487       val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
   488       val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   489       val c_t = cterm_incr_types thy refl_idx i_t
   490   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   491 
   492 fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
   493   | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   494   | get_ty_arg_size _ _ = 0;
   495 
   496 (* INFERENCE RULE: EQUALITY *)
   497 fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
   498   let val thy = ProofContext.theory_of ctxt
   499       val m_tm = Metis.Term.Fn atm
   500       val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr]
   501       val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   502       fun replace_item_list lx 0 (_::ls) = lx::ls
   503         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   504       fun path_finder_FO tm [] = (tm, Term.Bound 0)
   505         | path_finder_FO tm (p::ps) =
   506             let val (tm1,args) = strip_comb tm
   507                 val adjustment = get_ty_arg_size thy tm1
   508                 val p' = if adjustment > p then p else p-adjustment
   509                 val tm_p = List.nth(args,p')
   510                   handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   511                     Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   512                 val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   513                                       "  " ^ Syntax.string_of_term ctxt tm_p)
   514                 val (r,t) = path_finder_FO tm_p ps
   515             in
   516                 (r, list_comb (tm1, replace_item_list t p' args))
   517             end
   518       fun path_finder_HO tm [] = (tm, Term.Bound 0)
   519         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   520         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   521         | path_finder_HO tm ps =
   522           raise Fail ("equality_inf, path_finder_HO: path = " ^
   523                       space_implode " " (map Int.toString ps) ^
   524                       " isa-term: " ^  Syntax.string_of_term ctxt tm)
   525       fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   526         | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
   527             path_finder_FT tm ps t1
   528         | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
   529             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   530         | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
   531             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   532         | path_finder_FT tm ps t =
   533           raise Fail ("equality_inf, path_finder_FT: path = " ^
   534                       space_implode " " (map Int.toString ps) ^
   535                       " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   536                       " fol-term: " ^ Metis.Term.toString t)
   537       fun path_finder FO tm ps _ = path_finder_FO tm ps
   538         | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
   539              (*equality: not curried, as other predicates are*)
   540              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   541              else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   542         | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
   543              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   544         | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
   545                             (Metis.Term.Fn ("=", [t1,t2])) =
   546              (*equality: not curried, as other predicates are*)
   547              if p=0 then path_finder_FT tm (0::1::ps)
   548                           (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
   549                           (*select first operand*)
   550              else path_finder_FT tm (p::ps)
   551                    (Metis.Term.Fn (".", [metis_eq,t2]))
   552                    (*1 selects second operand*)
   553         | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   554              (*if not equality, ignore head to skip the hBOOL predicate*)
   555         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   556       fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
   557             let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   558             in (tm, nt $ tm_rslt) end
   559         | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   560       val (tm_subst, body) = path_finder_lit i_atm fp
   561       val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   562       val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   563       val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   564       val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   565       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   566       val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   567       val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   568       val eq_terms = map (pairself (cterm_of thy))
   569         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   570   in  cterm_instantiate eq_terms subst'  end;
   571 
   572 val factor = Seq.hd o distinct_subgoals_tac;
   573 
   574 fun step ctxt mode skolem_somes thpairs p =
   575   case p of
   576     (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
   577   | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm
   578   | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
   579     factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
   580   | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
   581     factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
   582   | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
   583   | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
   584     equality_inf ctxt mode skolem_somes f_lit f_p f_r
   585 
   586 fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
   587 
   588 (* FIXME: use "fold" instead *)
   589 fun translate _ _ _ thpairs [] = thpairs
   590   | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
   591       let val _ = trace_msg (fn () => "=============================================")
   592           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   593           val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   594           val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
   595                                                     thpairs (fol_th, inf))
   596           val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   597           val _ = trace_msg (fn () => "=============================================")
   598           val n_metis_lits =
   599             length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   600       in
   601           if nprems_of th = n_metis_lits then ()
   602           else error "Metis: proof reconstruction has gone wrong";
   603           translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
   604       end;
   605 
   606 (*Determining which axiom clauses are actually used*)
   607 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
   608   | used_axioms _ _ = NONE;
   609 
   610 (* ------------------------------------------------------------------------- *)
   611 (* Translation of HO Clauses                                                 *)
   612 (* ------------------------------------------------------------------------- *)
   613 
   614 fun cnf_helper_theorem thy raw th =
   615   if raw then th else the_single (cnf_axiom thy th)
   616 
   617 fun type_ext thy tms =
   618   let val subs = tfree_classes_of_terms tms
   619       val supers = tvar_classes_of_terms tms
   620       and tycons = type_consts_of_terms thy tms
   621       val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   622       val classrel_clauses = make_classrel_clauses thy subs supers'
   623   in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   624   end;
   625 
   626 (* ------------------------------------------------------------------------- *)
   627 (* Logic maps manage the interface between HOL and first-order logic.        *)
   628 (* ------------------------------------------------------------------------- *)
   629 
   630 type logic_map =
   631   {axioms: (Metis.Thm.thm * thm) list,
   632    tfrees: type_literal list,
   633    skolem_somes: (string * term) list}
   634 
   635 fun const_in_metis c (pred, tm_list) =
   636   let
   637     fun in_mterm (Metis.Term.Var _) = false
   638       | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
   639       | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   640   in  c = pred orelse exists in_mterm tm_list  end;
   641 
   642 (*Extract TFree constraints from context to include as conjecture clauses*)
   643 fun init_tfrees ctxt =
   644   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
   645     Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
   646     |> type_literals_for_types
   647   end;
   648 
   649 (*transform isabelle type / arity clause to metis clause *)
   650 fun add_type_thm [] lmap = lmap
   651   | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
   652       add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
   653                         skolem_somes = skolem_somes}
   654 
   655 (*Insert non-logical axioms corresponding to all accumulated TFrees*)
   656 fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
   657      {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
   658                axioms,
   659       tfrees = tfrees, skolem_somes = skolem_somes}
   660 
   661 fun string_of_mode FO = "FO"
   662   | string_of_mode HO = "HO"
   663   | string_of_mode FT = "FT"
   664 
   665 val helpers =
   666   [("c_COMBI", (false, @{thms COMBI_def})),
   667    ("c_COMBK", (false, @{thms COMBK_def})),
   668    ("c_COMBB", (false, @{thms COMBB_def})),
   669    ("c_COMBC", (false, @{thms COMBC_def})),
   670    ("c_COMBS", (false, @{thms COMBS_def})),
   671    ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
   672    ("c_True", (true, @{thms True_or_False})),
   673    ("c_False", (true, @{thms True_or_False})),
   674    ("c_If", (true, @{thms if_True if_False True_or_False}))]
   675 
   676 (* Function to generate metis clauses, including comb and type clauses *)
   677 fun build_map mode0 ctxt cls ths =
   678   let val thy = ProofContext.theory_of ctxt
   679       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   680       fun set_mode FO = FO
   681         | set_mode HO =
   682           if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
   683           else HO
   684         | set_mode FT = FT
   685       val mode = set_mode mode0
   686       (*transform isabelle clause to metis clause *)
   687       fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
   688         let
   689           val (mth, tfree_lits, skolem_somes) =
   690             hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
   691                            ith
   692         in
   693            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   694             tfrees = union (op =) tfree_lits tfrees,
   695             skolem_somes = skolem_somes}
   696         end;
   697       val lmap as {skolem_somes, ...} =
   698         {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
   699         |> fold (add_thm true) cls
   700         |> add_tfrees
   701         |> fold (add_thm false) ths
   702       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   703       fun is_used c =
   704         exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   705       val lmap =
   706         if mode = FO then
   707           lmap
   708         else
   709           let
   710             val helper_ths =
   711               helpers |> filter (is_used o fst)
   712                       |> maps (fn (_, (raw, thms)) =>
   713                                   if mode = FT orelse not raw then
   714                                     map (cnf_helper_theorem @{theory} raw) thms
   715                                   else
   716                                     [])
   717           in lmap |> fold (add_thm false) helper_ths end
   718   in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
   719 
   720 fun refute cls =
   721     Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
   722 
   723 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   724 
   725 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
   726 
   727 exception METIS of string;
   728 
   729 (* Main function to start metis proof and reconstruction *)
   730 fun FOL_SOLVE mode ctxt cls ths0 =
   731   let val thy = ProofContext.theory_of ctxt
   732       val th_cls_pairs =
   733         map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
   734       val ths = maps #2 th_cls_pairs
   735       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   736       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   737       val _ = trace_msg (fn () => "THEOREM CLAUSES")
   738       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   739       val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
   740       val _ = if null tfrees then ()
   741               else (trace_msg (fn () => "TFREE CLAUSES");
   742                     app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
   743       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   744       val thms = map #1 axioms
   745       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   746       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   747       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   748   in
   749       case filter (is_false o prop_of) cls of
   750           false_th::_ => [false_th RS @{thm FalseE}]
   751         | [] =>
   752       case refute thms of
   753           Metis.Resolution.Contradiction mth =>
   754             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   755                           Metis.Thm.toString mth)
   756                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   757                              (*add constraints arising from converting goal to clause form*)
   758                 val proof = Metis.Proof.proof mth
   759                 val result = translate ctxt' mode skolem_somes axioms proof
   760                 and used = map_filter (used_axioms axioms) proof
   761                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   762                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   763                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
   764                   if common_thm used cls then NONE else SOME name)
   765             in
   766                 if not (null cls) andalso not (common_thm used cls) then
   767                   warning "Metis: The assumptions are inconsistent."
   768                 else
   769                   ();
   770                 if not (null unused) then
   771                   warning ("Metis: Unused theorems: " ^ commas_quote unused
   772                            ^ ".")
   773                 else
   774                   ();
   775                 case result of
   776                     (_,ith)::_ =>
   777                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   778                          [ith])
   779                   | _ => (trace_msg (fn () => "Metis: No result");
   780                           [])
   781             end
   782         | Metis.Resolution.Satisfiable _ =>
   783             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   784              [])
   785   end;
   786 
   787 fun metis_general_tac mode ctxt ths i st0 =
   788   let val _ = trace_msg (fn () =>
   789         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   790   in
   791     if exists_type type_has_topsort (prop_of st0)
   792     then raise METIS "Metis: Proof state contains the universal sort {}"
   793     else
   794       (Meson.MESON (maps neg_clausify)
   795         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   796           THEN Meson_Tactic.expand_defs_tac st0) st0
   797   end
   798   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   799 
   800 val metis_tac = metis_general_tac HO;
   801 val metisF_tac = metis_general_tac FO;
   802 val metisFT_tac = metis_general_tac FT;
   803 
   804 fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   805   SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
   806 
   807 val setup =
   808   type_lits_setup #>
   809   method @{binding metis} HO "METIS for FOL and HOL problems" #>
   810   method @{binding metisF} FO "METIS for FOL problems" #>
   811   method @{binding metisFT} FT "METIS with fully-typed translation" #>
   812   Method.setup @{binding finish_clausify}
   813     (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
   814     "cleanup after conversion to clauses";
   815 
   816 end;