src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Tue Jun 22 23:54:02 2010 +0200 (2010-06-22)
changeset 37509 f39464d971c4
parent 37498 b426cbdb5a23
child 37516 c81c86bfc18a
permissions -rw-r--r--
factor out TPTP format output into file of its own, to facilitate further changes
     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 open Sledgehammer_TPTP_Format
    28 
    29 val trace = Unsynchronized.ref false;
    30 fun trace_msg msg = if !trace then tracing (msg ()) else ();
    31 
    32 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
    33 
    34 datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
    35 
    36 (* ------------------------------------------------------------------------- *)
    37 (* Useful Theorems                                                           *)
    38 (* ------------------------------------------------------------------------- *)
    39 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
    40 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    41 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
    42 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
    43 
    44 (* ------------------------------------------------------------------------- *)
    45 (* Useful Functions                                                          *)
    46 (* ------------------------------------------------------------------------- *)
    47 
    48 (* Match untyped terms. *)
    49 fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
    50   | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
    51   | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
    52     (a = b) (* The index is ignored, for some reason. *)
    53   | untyped_aconv (Bound i) (Bound j) = (i = j)
    54   | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
    55   | untyped_aconv (t1 $ t2) (u1 $ u2) =
    56     untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    57   | untyped_aconv _ _ = false
    58 
    59 (* Finding the relative location of an untyped term within a list of terms *)
    60 fun get_index lit =
    61   let val lit = Envir.eta_contract lit
    62       fun get _ [] = raise Empty
    63         | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    64                           then n  else get (n+1) xs
    65   in get 1 end;
    66 
    67 (* ------------------------------------------------------------------------- *)
    68 (* HOL to FOL  (Isabelle to Metis)                                           *)
    69 (* ------------------------------------------------------------------------- *)
    70 
    71 fun fn_isa_to_met "equal" = "="
    72   | fn_isa_to_met x       = x;
    73 
    74 fun metis_lit b c args = (b, (c, args));
    75 
    76 fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
    77   | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
    78   | hol_type_to_fol (TyConstr ((s, _), tps)) =
    79     Metis.Term.Fn (s, map hol_type_to_fol tps);
    80 
    81 (*These two functions insert type literals before the real literals. That is the
    82   opposite order from TPTP linkup, but maybe OK.*)
    83 
    84 fun hol_term_to_fol_FO tm =
    85   case strip_combterm_comb tm of
    86       (CombConst ((c, _), _, tys), tms) =>
    87         let val tyargs = map hol_type_to_fol tys
    88             val args   = map hol_term_to_fol_FO tms
    89         in Metis.Term.Fn (c, tyargs @ args) end
    90     | (CombVar ((v, _), _), []) => Metis.Term.Var v
    91     | _ => raise Fail "hol_term_to_fol_FO";
    92 
    93 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    94   | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    95       Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    96   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    97        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    98 
    99 (*The fully-typed translation, to avoid type errors*)
   100 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
   101 
   102 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
   103   | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
   104       wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   105   | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
   106        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   107                   type_of_combterm tm);
   108 
   109 fun hol_literal_to_fol FO (Literal (pol, tm)) =
   110       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
   111           val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   112           val lits = map hol_term_to_fol_FO tms
   113       in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   114   | hol_literal_to_fol HO (Literal (pol, tm)) =
   115      (case strip_combterm_comb tm of
   116           (CombConst(("equal", _), _, _), tms) =>
   117             metis_lit pol "=" (map hol_term_to_fol_HO tms)
   118         | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   119   | hol_literal_to_fol FT (Literal (pol, tm)) =
   120      (case strip_combterm_comb tm of
   121           (CombConst(("equal", _), _, _), tms) =>
   122             metis_lit pol "=" (map hol_term_to_fol_FT tms)
   123         | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   124 
   125 fun literals_of_hol_term thy mode t =
   126       let val (lits, types_sorts) = literals_of_term thy t
   127       in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   128 
   129 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   130 fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
   131     metis_lit pos s [Metis.Term.Var s']
   132   | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
   133     metis_lit pos s [Metis.Term.Fn (s',[])]
   134 
   135 fun default_sort _ (TVar _) = false
   136   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   137 
   138 fun metis_of_tfree tf =
   139   Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
   140 
   141 fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
   142   let
   143     val thy = ProofContext.theory_of ctxt
   144     val (skolem_somes, (mlits, types_sorts)) =
   145      th |> prop_of |> conceal_skolem_somes j skolem_somes
   146         ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   147   in
   148       if is_conjecture then
   149           (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
   150            type_literals_for_types types_sorts, skolem_somes)
   151       else
   152         let val tylits = filter_out (default_sort ctxt) types_sorts
   153                          |> type_literals_for_types
   154             val mtylits = if Config.get ctxt type_lits
   155                           then map (metis_of_type_literals false) tylits else []
   156         in
   157           (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
   158            skolem_somes)
   159         end
   160   end;
   161 
   162 (* ARITY CLAUSE *)
   163 
   164 fun m_arity_cls (TConsLit (c,t,args)) =
   165       metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   166   | m_arity_cls (TVarLit (c,str))     =
   167       metis_lit false (make_type_class c) [Metis.Term.Var str];
   168 
   169 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   170 fun arity_cls (ArityClause {conclLit, premLits, ...}) =
   171   (TrueI,
   172    Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   173 
   174 (* CLASSREL CLAUSE *)
   175 
   176 fun m_classrel_cls subclass superclass =
   177   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   178 
   179 fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
   180   (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   181 
   182 (* ------------------------------------------------------------------------- *)
   183 (* FOL to HOL  (Metis to Isabelle)                                           *)
   184 (* ------------------------------------------------------------------------- *)
   185 
   186 datatype term_or_type = Term of Term.term | Type of Term.typ;
   187 
   188 fun terms_of [] = []
   189   | terms_of (Term t :: tts) = t :: terms_of tts
   190   | terms_of (Type _ :: tts) = terms_of tts;
   191 
   192 fun types_of [] = []
   193   | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
   194       if String.isPrefix "_" a then
   195           (*Variable generated by Metis, which might have been a type variable.*)
   196           TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   197       else types_of tts
   198   | types_of (Term _ :: tts) = types_of tts
   199   | types_of (Type T :: tts) = T :: types_of tts;
   200 
   201 fun apply_list rator nargs rands =
   202   let val trands = terms_of rands
   203   in  if length trands = nargs then Term (list_comb(rator, trands))
   204       else raise Fail
   205         ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   206           " expected " ^ Int.toString nargs ^
   207           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   208   end;
   209 
   210 fun infer_types ctxt =
   211   Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
   212 
   213 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   214   with variable constraints in the goal...at least, type inference often fails otherwise.
   215   SEE ALSO axiom_inf below.*)
   216 fun mk_var (w,T) = Term.Var((w,1), T);
   217 
   218 (*include the default sort, if available*)
   219 fun mk_tfree ctxt w =
   220   let val ww = "'" ^ w
   221   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   222 
   223 (*Remove the "apply" operator from an HO term*)
   224 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   225   | strip_happ args x = (x, args);
   226 
   227 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
   228 
   229 fun fol_type_to_isa _ (Metis.Term.Var v) =
   230      (case strip_prefix tvar_prefix v of
   231           SOME w => make_tvar w
   232         | NONE   => make_tvar v)
   233   | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   234      (case strip_prefix tconst_prefix x of
   235           SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   236         | NONE    =>
   237       case strip_prefix tfree_prefix x of
   238           SOME tf => mk_tfree ctxt tf
   239         | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
   240 
   241 fun reveal_skolem_somes skolem_somes =
   242   map_aterms (fn t as Const (s, _) =>
   243                  if String.isPrefix skolem_theory_name s then
   244                    AList.lookup (op =) skolem_somes s
   245                    |> the |> map_types Type_Infer.paramify_vars
   246                  else
   247                    t
   248                | t => t)
   249 
   250 (*Maps metis terms to isabelle terms*)
   251 fun hol_term_from_fol_PT ctxt fol_tm =
   252   let val thy = ProofContext.theory_of ctxt
   253       val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
   254                                   Metis.Term.toString fol_tm)
   255       fun tm_to_tt (Metis.Term.Var v) =
   256              (case strip_prefix tvar_prefix v of
   257                   SOME w => Type (make_tvar w)
   258                 | NONE =>
   259               case strip_prefix schematic_var_prefix v of
   260                   SOME w => Term (mk_var (w, HOLogic.typeT))
   261                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   262                     (*Var from Metis with a name like _nnn; possibly a type variable*)
   263         | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   264         | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   265             let val (rator,rands) = strip_happ [] t
   266             in  case rator of
   267                     Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   268                   | _ => case tm_to_tt rator of
   269                              Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   270                            | _ => raise Fail "tm_to_tt: HO application"
   271             end
   272         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   273       and applic_to_tt ("=",ts) =
   274             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   275         | applic_to_tt (a,ts) =
   276             case strip_prefix const_prefix a of
   277                 SOME b =>
   278                   let val c = invert_const b
   279                       val ntypes = num_type_args thy c
   280                       val nterms = length ts - ntypes
   281                       val tts = map tm_to_tt ts
   282                       val tys = types_of (List.take(tts,ntypes))
   283                   in if length tys = ntypes then
   284                          apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   285                      else
   286                        raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
   287                                    " but gets " ^ Int.toString (length tys) ^
   288                                    " type arguments\n" ^
   289                                    cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   290                                    " the terms are \n" ^
   291                                    cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   292                      end
   293               | NONE => (*Not a constant. Is it a type constructor?*)
   294             case strip_prefix tconst_prefix a of
   295                 SOME b =>
   296                   Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
   297               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   298             case strip_prefix tfree_prefix a of
   299                 SOME b => Type (mk_tfree ctxt b)
   300               | NONE => (*a fixed variable? They are Skolem functions.*)
   301             case strip_prefix fixed_var_prefix a of
   302                 SOME b =>
   303                   let val opr = Term.Free(b, HOLogic.typeT)
   304                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
   305               | NONE => raise Fail ("unexpected metis function: " ^ a)
   306   in
   307     case tm_to_tt fol_tm of
   308       Term t => t
   309     | _ => raise Fail "fol_tm_to_tt: Term expected"
   310   end
   311 
   312 (*Maps fully-typed metis terms to isabelle terms*)
   313 fun hol_term_from_fol_FT ctxt fol_tm =
   314   let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
   315                                   Metis.Term.toString fol_tm)
   316       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   317              (case strip_prefix schematic_var_prefix v of
   318                   SOME w =>  mk_var(w, dummyT)
   319                 | NONE   => mk_var(v, dummyT))
   320         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   321             Const ("op =", HOLogic.typeT)
   322         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   323            (case strip_prefix const_prefix x of
   324                 SOME c => Const (invert_const c, dummyT)
   325               | NONE => (*Not a constant. Is it a fixed variable??*)
   326             case strip_prefix fixed_var_prefix x of
   327                 SOME v => Free (v, fol_type_to_isa ctxt ty)
   328               | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
   329         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   330             cvt tm1 $ cvt tm2
   331         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   332             cvt tm1 $ cvt tm2
   333         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   334         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   335             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
   336         | cvt (t as Metis.Term.Fn (x, [])) =
   337            (case strip_prefix const_prefix x of
   338                 SOME c => Const (invert_const c, dummyT)
   339               | NONE => (*Not a constant. Is it a fixed variable??*)
   340             case strip_prefix fixed_var_prefix x of
   341                 SOME v => Free (v, dummyT)
   342               | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
   343                   hol_term_from_fol_PT ctxt t))
   344         | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
   345             hol_term_from_fol_PT ctxt t)
   346   in fol_tm |> cvt end
   347 
   348 fun hol_term_from_fol FT = hol_term_from_fol_FT
   349   | hol_term_from_fol _ = hol_term_from_fol_PT
   350 
   351 fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
   352   let 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 = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
   698                  |> fold (add_thm true) cls
   699                  |> add_tfrees
   700                  |> fold (add_thm false) ths
   701       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   702       fun is_used c =
   703         exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   704       val lmap =
   705         if mode = FO then
   706           lmap
   707         else
   708           let
   709             val helper_ths =
   710               helpers |> filter (is_used o fst)
   711                       |> maps (fn (_, (raw, thms)) =>
   712                                   if mode = FT orelse not raw then
   713                                     map (cnf_helper_theorem @{theory} raw) thms
   714                                   else
   715                                     [])
   716           in lmap |> fold (add_thm false) helper_ths end
   717   in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
   718 
   719 fun refute cls =
   720     Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
   721 
   722 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   723 
   724 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
   725 
   726 exception METIS of string;
   727 
   728 (* Main function to start metis proof and reconstruction *)
   729 fun FOL_SOLVE mode ctxt cls ths0 =
   730   let val thy = ProofContext.theory_of ctxt
   731       val th_cls_pairs =
   732         map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
   733       val ths = maps #2 th_cls_pairs
   734       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   735       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   736       val _ = trace_msg (fn () => "THEOREM CLAUSES")
   737       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   738       val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
   739       val _ = if null tfrees then ()
   740               else (trace_msg (fn () => "TFREE CLAUSES");
   741                     app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
   742       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   743       val thms = map #1 axioms
   744       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   745       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   746       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   747   in
   748       case filter (is_false o prop_of) cls of
   749           false_th::_ => [false_th RS @{thm FalseE}]
   750         | [] =>
   751       case refute thms of
   752           Metis.Resolution.Contradiction mth =>
   753             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   754                           Metis.Thm.toString mth)
   755                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   756                              (*add constraints arising from converting goal to clause form*)
   757                 val proof = Metis.Proof.proof mth
   758                 val result = translate ctxt' mode skolem_somes axioms proof
   759                 and used = map_filter (used_axioms axioms) proof
   760                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   761                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   762                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
   763                   if common_thm used cls then NONE else SOME name)
   764             in
   765                 if not (null cls) andalso not (common_thm used cls) then
   766                   warning "Metis: The assumptions are inconsistent."
   767                 else
   768                   ();
   769                 if not (null unused) then
   770                   warning ("Metis: Unused theorems: " ^ commas_quote unused
   771                            ^ ".")
   772                 else
   773                   ();
   774                 case result of
   775                     (_,ith)::_ =>
   776                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   777                          [ith])
   778                   | _ => (trace_msg (fn () => "Metis: No result");
   779                           [])
   780             end
   781         | Metis.Resolution.Satisfiable _ =>
   782             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   783              [])
   784   end;
   785 
   786 fun metis_general_tac mode ctxt ths i st0 =
   787   let val _ = trace_msg (fn () =>
   788         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   789   in
   790     if exists_type type_has_topsort (prop_of st0)
   791     then raise METIS "Metis: Proof state contains the universal sort {}"
   792     else
   793       (Meson.MESON (maps neg_clausify)
   794         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   795           THEN Meson_Tactic.expand_defs_tac st0) st0
   796   end
   797   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   798 
   799 val metis_tac = metis_general_tac HO;
   800 val metisF_tac = metis_general_tac FO;
   801 val metisFT_tac = metis_general_tac FT;
   802 
   803 fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   804   SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
   805 
   806 val setup =
   807   type_lits_setup #>
   808   method @{binding metis} HO "METIS for FOL and HOL problems" #>
   809   method @{binding metisF} FO "METIS for FOL problems" #>
   810   method @{binding metisFT} FT "METIS with fully-typed translation" #>
   811   Method.setup @{binding finish_clausify}
   812     (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
   813     "cleanup after conversion to clauses";
   814 
   815 end;