src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Wed Jun 23 14:36:23 2010 +0200 (2010-06-23)
changeset 37516 c81c86bfc18a
parent 37509 f39464d971c4
child 37538 97ab019d5ac8
permissions -rw-r--r--
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
     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 exception METIS of string * string
    30 
    31 val trace = Unsynchronized.ref false;
    32 fun trace_msg msg = if !trace then tracing (msg ()) else ();
    33 
    34 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
    35 
    36 datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
    37 
    38 (* ------------------------------------------------------------------------- *)
    39 (* Useful Theorems                                                           *)
    40 (* ------------------------------------------------------------------------- *)
    41 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
    42 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
    43 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
    44 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
    45 
    46 (* ------------------------------------------------------------------------- *)
    47 (* Useful Functions                                                          *)
    48 (* ------------------------------------------------------------------------- *)
    49 
    50 (* Match untyped terms. *)
    51 fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
    52   | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
    53   | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
    54     (a = b) (* The index is ignored, for some reason. *)
    55   | untyped_aconv (Bound i) (Bound j) = (i = j)
    56   | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
    57   | untyped_aconv (t1 $ t2) (u1 $ u2) =
    58     untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    59   | untyped_aconv _ _ = false
    60 
    61 (* Finding the relative location of an untyped term within a list of terms *)
    62 fun get_index lit =
    63   let val lit = Envir.eta_contract lit
    64       fun get _ [] = raise Empty
    65         | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
    66                           then n  else get (n+1) xs
    67   in get 1 end;
    68 
    69 (* ------------------------------------------------------------------------- *)
    70 (* HOL to FOL  (Isabelle to Metis)                                           *)
    71 (* ------------------------------------------------------------------------- *)
    72 
    73 fun fn_isa_to_met "equal" = "="
    74   | fn_isa_to_met x       = x;
    75 
    76 fun metis_lit b c args = (b, (c, args));
    77 
    78 fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
    79   | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
    80   | hol_type_to_fol (TyConstr ((s, _), tps)) =
    81     Metis.Term.Fn (s, map hol_type_to_fol tps);
    82 
    83 (*These two functions insert type literals before the real literals. That is the
    84   opposite order from TPTP linkup, but maybe OK.*)
    85 
    86 fun hol_term_to_fol_FO tm =
    87   case strip_combterm_comb tm of
    88       (CombConst ((c, _), _, tys), tms) =>
    89         let val tyargs = map hol_type_to_fol tys
    90             val args   = map hol_term_to_fol_FO tms
    91         in Metis.Term.Fn (c, tyargs @ args) end
    92     | (CombVar ((v, _), _), []) => Metis.Term.Var v
    93     | _ => raise Fail "hol_term_to_fol_FO";
    94 
    95 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    96   | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    97       Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    98   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    99        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
   100 
   101 (*The fully-typed translation, to avoid type errors*)
   102 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
   103 
   104 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
   105   | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
   106       wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
   107   | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
   108        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   109                   type_of_combterm tm);
   110 
   111 fun hol_literal_to_fol FO (Literal (pol, tm)) =
   112       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
   113           val tylits = if p = "equal" then [] else map hol_type_to_fol tys
   114           val lits = map hol_term_to_fol_FO tms
   115       in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
   116   | hol_literal_to_fol HO (Literal (pol, tm)) =
   117      (case strip_combterm_comb tm of
   118           (CombConst(("equal", _), _, _), tms) =>
   119             metis_lit pol "=" (map hol_term_to_fol_HO tms)
   120         | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   121   | hol_literal_to_fol FT (Literal (pol, tm)) =
   122      (case strip_combterm_comb tm of
   123           (CombConst(("equal", _), _, _), tms) =>
   124             metis_lit pol "=" (map hol_term_to_fol_FT tms)
   125         | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   126 
   127 fun literals_of_hol_term thy mode t =
   128       let val (lits, types_sorts) = literals_of_term thy t
   129       in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   130 
   131 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   132 fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
   133     metis_lit pos s [Metis.Term.Var s']
   134   | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
   135     metis_lit pos s [Metis.Term.Fn (s',[])]
   136 
   137 fun default_sort _ (TVar _) = false
   138   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   139 
   140 fun metis_of_tfree tf =
   141   Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
   142 
   143 fun hol_thm_to_fol is_conjecture ctxt mode j skolem_somes th =
   144   let
   145     val thy = ProofContext.theory_of ctxt
   146     val (skolem_somes, (mlits, types_sorts)) =
   147      th |> prop_of |> conceal_skolem_somes j skolem_somes
   148         ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   149   in
   150       if is_conjecture then
   151           (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
   152            type_literals_for_types types_sorts, skolem_somes)
   153       else
   154         let val tylits = filter_out (default_sort ctxt) types_sorts
   155                          |> type_literals_for_types
   156             val mtylits = if Config.get ctxt type_lits
   157                           then map (metis_of_type_literals false) tylits else []
   158         in
   159           (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
   160            skolem_somes)
   161         end
   162   end;
   163 
   164 (* ARITY CLAUSE *)
   165 
   166 fun m_arity_cls (TConsLit (c,t,args)) =
   167       metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
   168   | m_arity_cls (TVarLit (c,str))     =
   169       metis_lit false (make_type_class c) [Metis.Term.Var str];
   170 
   171 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   172 fun arity_cls (ArityClause {conclLit, premLits, ...}) =
   173   (TrueI,
   174    Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   175 
   176 (* CLASSREL CLAUSE *)
   177 
   178 fun m_classrel_cls subclass superclass =
   179   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
   180 
   181 fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
   182   (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
   183 
   184 (* ------------------------------------------------------------------------- *)
   185 (* FOL to HOL  (Metis to Isabelle)                                           *)
   186 (* ------------------------------------------------------------------------- *)
   187 
   188 datatype term_or_type = Term of Term.term | Type of Term.typ;
   189 
   190 fun terms_of [] = []
   191   | terms_of (Term t :: tts) = t :: terms_of tts
   192   | terms_of (Type _ :: tts) = terms_of tts;
   193 
   194 fun types_of [] = []
   195   | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
   196       if String.isPrefix "_" a then
   197           (*Variable generated by Metis, which might have been a type variable.*)
   198           TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
   199       else types_of tts
   200   | types_of (Term _ :: tts) = types_of tts
   201   | types_of (Type T :: tts) = T :: types_of tts;
   202 
   203 fun apply_list rator nargs rands =
   204   let val trands = terms_of rands
   205   in  if length trands = nargs then Term (list_comb(rator, trands))
   206       else raise Fail
   207         ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
   208           " expected " ^ Int.toString nargs ^
   209           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
   210   end;
   211 
   212 fun infer_types ctxt =
   213   Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
   214 
   215 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
   216   with variable constraints in the goal...at least, type inference often fails otherwise.
   217   SEE ALSO axiom_inf below.*)
   218 fun mk_var (w,T) = Term.Var((w,1), T);
   219 
   220 (*include the default sort, if available*)
   221 fun mk_tfree ctxt w =
   222   let val ww = "'" ^ w
   223   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   224 
   225 (*Remove the "apply" operator from an HO term*)
   226 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   227   | strip_happ args x = (x, args);
   228 
   229 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
   230 
   231 fun fol_type_to_isa _ (Metis.Term.Var v) =
   232      (case strip_prefix tvar_prefix v of
   233           SOME w => make_tvar w
   234         | NONE   => make_tvar v)
   235   | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
   236      (case strip_prefix tconst_prefix x of
   237           SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
   238         | NONE    =>
   239       case strip_prefix tfree_prefix x of
   240           SOME tf => mk_tfree ctxt tf
   241         | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
   242 
   243 fun reveal_skolem_somes skolem_somes =
   244   map_aterms (fn t as Const (s, _) =>
   245                  if String.isPrefix skolem_theory_name s then
   246                    AList.lookup (op =) skolem_somes s
   247                    |> the |> map_types Type_Infer.paramify_vars
   248                  else
   249                    t
   250                | t => t)
   251 
   252 (*Maps metis terms to isabelle terms*)
   253 fun hol_term_from_fol_PT ctxt fol_tm =
   254   let val thy = ProofContext.theory_of ctxt
   255       val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
   256                                   Metis.Term.toString fol_tm)
   257       fun tm_to_tt (Metis.Term.Var v) =
   258              (case strip_prefix tvar_prefix v of
   259                   SOME w => Type (make_tvar w)
   260                 | NONE =>
   261               case strip_prefix schematic_var_prefix v of
   262                   SOME w => Term (mk_var (w, HOLogic.typeT))
   263                 | NONE   => Term (mk_var (v, HOLogic.typeT)) )
   264                     (*Var from Metis with a name like _nnn; possibly a type variable*)
   265         | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   266         | tm_to_tt (t as Metis.Term.Fn (".",_)) =
   267             let val (rator,rands) = strip_happ [] t
   268             in  case rator of
   269                     Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   270                   | _ => case tm_to_tt rator of
   271                              Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
   272                            | _ => raise Fail "tm_to_tt: HO application"
   273             end
   274         | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
   275       and applic_to_tt ("=",ts) =
   276             Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   277         | applic_to_tt (a,ts) =
   278             case strip_prefix const_prefix a of
   279                 SOME b =>
   280                   let val c = invert_const b
   281                       val ntypes = num_type_args thy c
   282                       val nterms = length ts - ntypes
   283                       val tts = map tm_to_tt ts
   284                       val tys = types_of (List.take(tts,ntypes))
   285                   in if length tys = ntypes then
   286                          apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
   287                      else
   288                        raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
   289                                    " but gets " ^ Int.toString (length tys) ^
   290                                    " type arguments\n" ^
   291                                    cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   292                                    " the terms are \n" ^
   293                                    cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   294                      end
   295               | NONE => (*Not a constant. Is it a type constructor?*)
   296             case strip_prefix tconst_prefix a of
   297                 SOME b =>
   298                   Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
   299               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   300             case strip_prefix tfree_prefix a of
   301                 SOME b => Type (mk_tfree ctxt b)
   302               | NONE => (*a fixed variable? They are Skolem functions.*)
   303             case strip_prefix fixed_var_prefix a of
   304                 SOME b =>
   305                   let val opr = Term.Free(b, HOLogic.typeT)
   306                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
   307               | NONE => raise Fail ("unexpected metis function: " ^ a)
   308   in
   309     case tm_to_tt fol_tm of
   310       Term t => t
   311     | _ => raise Fail "fol_tm_to_tt: Term expected"
   312   end
   313 
   314 (*Maps fully-typed metis terms to isabelle terms*)
   315 fun hol_term_from_fol_FT ctxt fol_tm =
   316   let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
   317                                   Metis.Term.toString fol_tm)
   318       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
   319              (case strip_prefix schematic_var_prefix v of
   320                   SOME w =>  mk_var(w, dummyT)
   321                 | NONE   => mk_var(v, dummyT))
   322         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
   323             Const ("op =", HOLogic.typeT)
   324         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
   325            (case strip_prefix const_prefix x of
   326                 SOME c => Const (invert_const c, dummyT)
   327               | NONE => (*Not a constant. Is it a fixed variable??*)
   328             case strip_prefix fixed_var_prefix x of
   329                 SOME v => Free (v, fol_type_to_isa ctxt ty)
   330               | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
   331         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
   332             cvt tm1 $ cvt tm2
   333         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   334             cvt tm1 $ cvt tm2
   335         | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   336         | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
   337             list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
   338         | cvt (t as Metis.Term.Fn (x, [])) =
   339            (case strip_prefix const_prefix x of
   340                 SOME c => Const (invert_const c, dummyT)
   341               | NONE => (*Not a constant. Is it a fixed variable??*)
   342             case strip_prefix fixed_var_prefix x of
   343                 SOME v => Free (v, dummyT)
   344               | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
   345                   hol_term_from_fol_PT ctxt t))
   346         | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
   347             hol_term_from_fol_PT ctxt t)
   348   in fol_tm |> cvt end
   349 
   350 fun hol_term_from_fol FT = hol_term_from_fol_FT
   351   | hol_term_from_fol _ = hol_term_from_fol_PT
   352 
   353 fun hol_terms_from_fol ctxt mode skolem_somes fol_tms =
   354   let val ts = map (hol_term_from_fol mode ctxt) fol_tms
   355       val _ = trace_msg (fn () => "  calling type inference:")
   356       val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   357       val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
   358       val _ = app (fn t => trace_msg
   359                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   360                               "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   361                   ts'
   362   in  ts'  end;
   363 
   364 fun mk_not (Const (@{const_name Not}, _) $ b) = b
   365   | mk_not b = HOLogic.mk_not b;
   366 
   367 val metis_eq = Metis.Term.Fn ("=", []);
   368 
   369 (* ------------------------------------------------------------------------- *)
   370 (* FOL step Inference Rules                                                  *)
   371 (* ------------------------------------------------------------------------- *)
   372 
   373 (*for debugging only*)
   374 fun print_thpair (fth,th) =
   375   (trace_msg (fn () => "=============================================");
   376    trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
   377    trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   378 
   379 fun lookth thpairs (fth : Metis.Thm.thm) =
   380   the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   381   handle Option =>
   382          raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   383 
   384 fun is_TrueI th = Thm.eq_thm(TrueI,th);
   385 
   386 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   387 
   388 fun inst_excluded_middle thy i_atm =
   389   let val th = EXCLUDED_MIDDLE
   390       val [vx] = Term.add_vars (prop_of th) []
   391       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   392   in  cterm_instantiate substs th  end;
   393 
   394 (* INFERENCE RULE: AXIOM *)
   395 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
   396     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   397 
   398 (* INFERENCE RULE: ASSUME *)
   399 fun assume_inf ctxt mode skolem_somes atm =
   400   inst_excluded_middle
   401     (ProofContext.theory_of ctxt)
   402     (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
   403 
   404 (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   405    them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   406    that new TVars are distinct and that types can be inferred from terms.*)
   407 fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
   408   let val thy = ProofContext.theory_of ctxt
   409       val i_th   = lookth thpairs th
   410       val i_th_vars = Term.add_vars (prop_of i_th) []
   411       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   412       fun subst_translation (x,y) =
   413             let val v = find_var x
   414                 (* We call "reveal_skolem_somes" and "infer_types" below. *)
   415                 val t = hol_term_from_fol mode ctxt y
   416             in  SOME (cterm_of thy (Var v), t)  end
   417             handle Option =>
   418                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   419                                        " in " ^ Display.string_of_thm ctxt i_th);
   420                  NONE)
   421       fun remove_typeinst (a, t) =
   422             case strip_prefix schematic_var_prefix a of
   423                 SOME b => SOME (b, t)
   424               | NONE   => case strip_prefix tvar_prefix a of
   425                 SOME _ => NONE          (*type instantiations are forbidden!*)
   426               | NONE   => SOME (a,t)    (*internal Metis var?*)
   427       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   428       val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   429       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   430       val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
   431                        |> infer_types ctxt
   432       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   433       val substs' = ListPair.zip (vars, map ctm_of tms)
   434       val _ = trace_msg (fn () =>
   435         cat_lines ("subst_translations:" ::
   436           (substs' |> map (fn (x, y) =>
   437             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   438             Syntax.string_of_term ctxt (term_of y)))));
   439   in cterm_instantiate substs' i_th end
   440   handle THM (msg, _, _) => raise METIS ("inst_inf", msg)
   441        | ERROR msg => raise METIS ("inst_inf", msg)
   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 => raise METIS ("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 raise METIS ("translate", "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 (* Main function to start Metis proof and reconstruction *)
   727 fun FOL_SOLVE mode ctxt cls ths0 =
   728   let val thy = ProofContext.theory_of ctxt
   729       val th_cls_pairs =
   730         map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
   731       val ths = maps #2 th_cls_pairs
   732       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   733       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   734       val _ = trace_msg (fn () => "THEOREM CLAUSES")
   735       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   736       val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
   737       val _ = if null tfrees then ()
   738               else (trace_msg (fn () => "TFREE CLAUSES");
   739                     app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
   740       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   741       val thms = map #1 axioms
   742       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   743       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   744       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   745   in
   746       case filter (is_false o prop_of) cls of
   747           false_th::_ => [false_th RS @{thm FalseE}]
   748         | [] =>
   749       case refute thms of
   750           Metis.Resolution.Contradiction mth =>
   751             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   752                           Metis.Thm.toString mth)
   753                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   754                              (*add constraints arising from converting goal to clause form*)
   755                 val proof = Metis.Proof.proof mth
   756                 val result = translate ctxt' mode skolem_somes axioms proof
   757                 and used = map_filter (used_axioms axioms) proof
   758                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   759                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   760                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
   761                   if common_thm used cls then NONE else SOME name)
   762             in
   763                 if not (null cls) andalso not (common_thm used cls) then
   764                   warning "Metis: The assumptions are inconsistent."
   765                 else
   766                   ();
   767                 if not (null unused) then
   768                   warning ("Metis: Unused theorems: " ^ commas_quote unused
   769                            ^ ".")
   770                 else
   771                   ();
   772                 case result of
   773                     (_,ith)::_ =>
   774                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   775                          [ith])
   776                   | _ => (trace_msg (fn () => "Metis: No result");
   777                           raise METIS ("FOL_SOLVE", ""))
   778             end
   779         | Metis.Resolution.Satisfiable _ =>
   780             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   781              raise METIS ("FOL_SOLVE", ""))
   782   end;
   783 
   784 fun generic_metis_tac mode ctxt ths i st0 =
   785   let val _ = trace_msg (fn () =>
   786         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   787   in
   788     if exists_type type_has_topsort (prop_of st0) then
   789       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
   790     else
   791       (Meson.MESON (maps neg_clausify)
   792                    (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
   793                    ctxt i
   794        THEN Meson_Tactic.expand_defs_tac st0) st0
   795      handle ERROR msg => raise METIS ("generic_metis_tac", msg)
   796   end
   797   handle METIS (loc, msg) =>
   798          if mode = HO then
   799            (warning ("Metis: Falling back on \"metisFT\".");
   800             generic_metis_tac FT ctxt ths i st0)
   801          else if msg = "" then
   802            Seq.empty
   803          else
   804            raise error ("Metis (" ^ loc ^ "): " ^ msg)
   805 
   806 val metis_tac = generic_metis_tac HO
   807 val metisF_tac = generic_metis_tac FO
   808 val metisFT_tac = generic_metis_tac FT
   809 
   810 fun method name mode =
   811   Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   812     SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths)))
   813 
   814 val setup =
   815   type_lits_setup
   816   #> method @{binding metis} HO "Metis for FOL/HOL problems"
   817   #> method @{binding metisF} FO "Metis for FOL problems"
   818   #> method @{binding metisFT} FT
   819             "Metis for FOL/HOL problems with fully-typed translation"
   820 
   821 end;