src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Tue Jun 22 14:28:22 2010 +0200 (2010-06-22)
changeset 37498 b426cbdb5a23
parent 37479 f6b1ee5b420b
child 37509 f39464d971c4
permissions -rw-r--r--
removed Sledgehammer's support for the DFG syntax;
this removes 350 buggy lines from Sledgehammer. SPASS 3.5 and above support the TPTP syntax.
     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 _ [] = 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, _) =>
   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 ts = map (hol_term_from_fol mode ctxt) fol_tms
   352       val _ = trace_msg (fn () => "  calling type inference:")
   353       val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
   354       val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
   355       val _ = app (fn t => trace_msg
   356                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   357                               "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   358                   ts'
   359   in  ts'  end;
   360 
   361 fun mk_not (Const (@{const_name Not}, _) $ b) = b
   362   | mk_not b = HOLogic.mk_not b;
   363 
   364 val metis_eq = Metis.Term.Fn ("=", []);
   365 
   366 (* ------------------------------------------------------------------------- *)
   367 (* FOL step Inference Rules                                                  *)
   368 (* ------------------------------------------------------------------------- *)
   369 
   370 (*for debugging only*)
   371 fun print_thpair (fth,th) =
   372   (trace_msg (fn () => "=============================================");
   373    trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
   374    trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   375 
   376 fun lookth thpairs (fth : Metis.Thm.thm) =
   377   the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   378   handle Option =>
   379          raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   380 
   381 fun is_TrueI th = Thm.eq_thm(TrueI,th);
   382 
   383 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   384 
   385 fun inst_excluded_middle thy i_atm =
   386   let val th = EXCLUDED_MIDDLE
   387       val [vx] = Term.add_vars (prop_of th) []
   388       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   389   in  cterm_instantiate substs th  end;
   390 
   391 (* INFERENCE RULE: AXIOM *)
   392 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
   393     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   394 
   395 (* INFERENCE RULE: ASSUME *)
   396 fun assume_inf ctxt mode skolem_somes atm =
   397   inst_excluded_middle
   398     (ProofContext.theory_of ctxt)
   399     (singleton (hol_terms_from_fol ctxt mode skolem_somes) (Metis.Term.Fn atm))
   400 
   401 (* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
   402    them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
   403    that new TVars are distinct and that types can be inferred from terms.*)
   404 fun inst_inf ctxt mode skolem_somes thpairs fsubst th =
   405   let val thy = ProofContext.theory_of ctxt
   406       val i_th   = lookth thpairs th
   407       val i_th_vars = Term.add_vars (prop_of i_th) []
   408       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   409       fun subst_translation (x,y) =
   410             let val v = find_var x
   411                 (* We call "reveal_skolem_somes" and "infer_types" below. *)
   412                 val t = hol_term_from_fol mode ctxt y
   413             in  SOME (cterm_of thy (Var v), t)  end
   414             handle Option =>
   415                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
   416                                        " in " ^ Display.string_of_thm ctxt i_th);
   417                  NONE)
   418       fun remove_typeinst (a, t) =
   419             case strip_prefix schematic_var_prefix a of
   420                 SOME b => SOME (b, t)
   421               | NONE   => case strip_prefix tvar_prefix a of
   422                 SOME _ => NONE          (*type instantiations are forbidden!*)
   423               | NONE   => SOME (a,t)    (*internal Metis var?*)
   424       val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   425       val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
   426       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   427       val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
   428                        |> infer_types ctxt
   429       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   430       val substs' = ListPair.zip (vars, map ctm_of tms)
   431       val _ = trace_msg (fn () =>
   432         cat_lines ("subst_translations:" ::
   433           (substs' |> map (fn (x, y) =>
   434             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   435             Syntax.string_of_term ctxt (term_of y)))));
   436   in cterm_instantiate substs' i_th end
   437   handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
   438        | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
   439                              "\n(Perhaps you want to try \"metisFT\" if you \
   440                              \haven't done so already.)")
   441 
   442 (* INFERENCE RULE: RESOLVE *)
   443 
   444 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
   445   of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
   446   could then fail. See comment on mk_var.*)
   447 fun resolve_inc_tyvars(tha,i,thb) =
   448   let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   449       val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
   450   in
   451       case distinct Thm.eq_thm ths of
   452         [th] => th
   453       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
   454   end;
   455 
   456 fun resolve_inf ctxt mode skolem_somes thpairs atm th1 th2 =
   457   let
   458     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   459     val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   460     val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   461   in
   462     if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
   463     else if is_TrueI i_th2 then i_th1
   464     else
   465       let
   466         val i_atm = singleton (hol_terms_from_fol ctxt mode skolem_somes)
   467                               (Metis.Term.Fn atm)
   468         val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   469         val prems_th1 = prems_of i_th1
   470         val prems_th2 = prems_of i_th2
   471         val index_th1 = get_index (mk_not i_atm) prems_th1
   472               handle Empty => raise Fail "Failed to find literal in th1"
   473         val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   474         val index_th2 = get_index i_atm prems_th2
   475               handle Empty => raise Fail "Failed to find literal in th2"
   476         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   477     in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   478   end;
   479 
   480 (* INFERENCE RULE: REFL *)
   481 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   482 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   483 
   484 fun refl_inf ctxt mode skolem_somes t =
   485   let val thy = ProofContext.theory_of ctxt
   486       val i_t = singleton (hol_terms_from_fol ctxt mode skolem_somes) t
   487       val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   488       val c_t = cterm_incr_types thy refl_idx i_t
   489   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   490 
   491 fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
   492   | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   493   | get_ty_arg_size _ _ = 0;
   494 
   495 (* INFERENCE RULE: EQUALITY *)
   496 fun equality_inf ctxt mode skolem_somes (pos, atm) fp fr =
   497   let val thy = ProofContext.theory_of ctxt
   498       val m_tm = Metis.Term.Fn atm
   499       val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolem_somes [m_tm, fr]
   500       val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   501       fun replace_item_list lx 0 (_::ls) = lx::ls
   502         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   503       fun path_finder_FO tm [] = (tm, Term.Bound 0)
   504         | path_finder_FO tm (p::ps) =
   505             let val (tm1,args) = strip_comb tm
   506                 val adjustment = get_ty_arg_size thy tm1
   507                 val p' = if adjustment > p then p else p-adjustment
   508                 val tm_p = List.nth(args,p')
   509                   handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
   510                     Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
   511                 val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   512                                       "  " ^ Syntax.string_of_term ctxt tm_p)
   513                 val (r,t) = path_finder_FO tm_p ps
   514             in
   515                 (r, list_comb (tm1, replace_item_list t p' args))
   516             end
   517       fun path_finder_HO tm [] = (tm, Term.Bound 0)
   518         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   519         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   520         | path_finder_HO tm ps =
   521           raise Fail ("equality_inf, path_finder_HO: path = " ^
   522                       space_implode " " (map Int.toString ps) ^
   523                       " isa-term: " ^  Syntax.string_of_term ctxt tm)
   524       fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
   525         | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
   526             path_finder_FT tm ps t1
   527         | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
   528             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   529         | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
   530             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   531         | path_finder_FT tm ps t =
   532           raise Fail ("equality_inf, path_finder_FT: path = " ^
   533                       space_implode " " (map Int.toString ps) ^
   534                       " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   535                       " fol-term: " ^ Metis.Term.toString t)
   536       fun path_finder FO tm ps _ = path_finder_FO tm ps
   537         | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
   538              (*equality: not curried, as other predicates are*)
   539              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   540              else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   541         | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
   542              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   543         | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
   544                             (Metis.Term.Fn ("=", [t1,t2])) =
   545              (*equality: not curried, as other predicates are*)
   546              if p=0 then path_finder_FT tm (0::1::ps)
   547                           (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
   548                           (*select first operand*)
   549              else path_finder_FT tm (p::ps)
   550                    (Metis.Term.Fn (".", [metis_eq,t2]))
   551                    (*1 selects second operand*)
   552         | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   553              (*if not equality, ignore head to skip the hBOOL predicate*)
   554         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   555       fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
   556             let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   557             in (tm, nt $ tm_rslt) end
   558         | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   559       val (tm_subst, body) = path_finder_lit i_atm fp
   560       val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
   561       val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   562       val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   563       val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   564       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   565       val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   566       val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   567       val eq_terms = map (pairself (cterm_of thy))
   568         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   569   in  cterm_instantiate eq_terms subst'  end;
   570 
   571 val factor = Seq.hd o distinct_subgoals_tac;
   572 
   573 fun step ctxt mode skolem_somes thpairs p =
   574   case p of
   575     (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
   576   | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolem_somes f_atm
   577   | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
   578     factor (inst_inf ctxt mode skolem_somes thpairs f_subst f_th1)
   579   | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
   580     factor (resolve_inf ctxt mode skolem_somes thpairs f_atm f_th1 f_th2)
   581   | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolem_somes f_tm
   582   | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
   583     equality_inf ctxt mode skolem_somes f_lit f_p f_r
   584 
   585 fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
   586 
   587 (* FIXME: use "fold" instead *)
   588 fun translate _ _ _ thpairs [] = thpairs
   589   | translate ctxt mode skolem_somes thpairs ((fol_th, inf) :: infpairs) =
   590       let val _ = trace_msg (fn () => "=============================================")
   591           val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
   592           val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
   593           val th = Meson.flexflex_first_order (step ctxt mode skolem_somes
   594                                                     thpairs (fol_th, inf))
   595           val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   596           val _ = trace_msg (fn () => "=============================================")
   597           val n_metis_lits =
   598             length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   599       in
   600           if nprems_of th = n_metis_lits then ()
   601           else error "Metis: proof reconstruction has gone wrong";
   602           translate ctxt mode skolem_somes ((fol_th, th) :: thpairs) infpairs
   603       end;
   604 
   605 (*Determining which axiom clauses are actually used*)
   606 fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
   607   | used_axioms _ _ = NONE;
   608 
   609 (* ------------------------------------------------------------------------- *)
   610 (* Translation of HO Clauses                                                 *)
   611 (* ------------------------------------------------------------------------- *)
   612 
   613 fun cnf_helper_theorem thy raw th =
   614   if raw then th else the_single (cnf_axiom thy th)
   615 
   616 fun type_ext thy tms =
   617   let val subs = tfree_classes_of_terms tms
   618       val supers = tvar_classes_of_terms tms
   619       and tycons = type_consts_of_terms thy tms
   620       val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   621       val classrel_clauses = make_classrel_clauses thy subs supers'
   622   in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
   623   end;
   624 
   625 (* ------------------------------------------------------------------------- *)
   626 (* Logic maps manage the interface between HOL and first-order logic.        *)
   627 (* ------------------------------------------------------------------------- *)
   628 
   629 type logic_map =
   630   {axioms: (Metis.Thm.thm * thm) list,
   631    tfrees: type_literal list,
   632    skolem_somes: (string * term) list}
   633 
   634 fun const_in_metis c (pred, tm_list) =
   635   let
   636     fun in_mterm (Metis.Term.Var _) = false
   637       | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
   638       | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   639   in  c = pred orelse exists in_mterm tm_list  end;
   640 
   641 (*Extract TFree constraints from context to include as conjecture clauses*)
   642 fun init_tfrees ctxt =
   643   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
   644     Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
   645     |> type_literals_for_types
   646   end;
   647 
   648 (*transform isabelle type / arity clause to metis clause *)
   649 fun add_type_thm [] lmap = lmap
   650   | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolem_somes} =
   651       add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
   652                         skolem_somes = skolem_somes}
   653 
   654 (*Insert non-logical axioms corresponding to all accumulated TFrees*)
   655 fun add_tfrees {axioms, tfrees, skolem_somes} : logic_map =
   656      {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
   657                axioms,
   658       tfrees = tfrees, skolem_somes = skolem_somes}
   659 
   660 fun string_of_mode FO = "FO"
   661   | string_of_mode HO = "HO"
   662   | string_of_mode FT = "FT"
   663 
   664 val helpers =
   665   [("c_COMBI", (false, @{thms COMBI_def})),
   666    ("c_COMBK", (false, @{thms COMBK_def})),
   667    ("c_COMBB", (false, @{thms COMBB_def})),
   668    ("c_COMBC", (false, @{thms COMBC_def})),
   669    ("c_COMBS", (false, @{thms COMBS_def})),
   670    ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
   671    ("c_True", (true, @{thms True_or_False})),
   672    ("c_False", (true, @{thms True_or_False})),
   673    ("c_If", (true, @{thms if_True if_False True_or_False}))]
   674 
   675 (* Function to generate metis clauses, including comb and type clauses *)
   676 fun build_map mode0 ctxt cls ths =
   677   let val thy = ProofContext.theory_of ctxt
   678       (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   679       fun set_mode FO = FO
   680         | set_mode HO =
   681           if forall (is_quasi_fol_term thy o prop_of) (cls @ ths) then FO
   682           else HO
   683         | set_mode FT = FT
   684       val mode = set_mode mode0
   685       (*transform isabelle clause to metis clause *)
   686       fun add_thm is_conjecture ith {axioms, tfrees, skolem_somes} : logic_map =
   687         let
   688           val (mth, tfree_lits, skolem_somes) =
   689             hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolem_somes
   690                            ith
   691         in
   692            {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
   693             tfrees = union (op =) tfree_lits tfrees,
   694             skolem_somes = skolem_somes}
   695         end;
   696       val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolem_somes = []}
   697                  |> fold (add_thm true) cls
   698                  |> add_tfrees
   699                  |> fold (add_thm false) ths
   700       val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
   701       fun is_used c =
   702         exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
   703       val lmap =
   704         if mode = FO then
   705           lmap
   706         else
   707           let
   708             val helper_ths =
   709               helpers |> filter (is_used o fst)
   710                       |> maps (fn (_, (raw, thms)) =>
   711                                   if mode = FT orelse not raw then
   712                                     map (cnf_helper_theorem @{theory} raw) thms
   713                                   else
   714                                     [])
   715           in lmap |> fold (add_thm false) helper_ths end
   716   in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
   717 
   718 fun refute cls =
   719     Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
   720 
   721 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
   722 
   723 fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
   724 
   725 exception METIS of string;
   726 
   727 (* Main function to start metis proof and reconstruction *)
   728 fun FOL_SOLVE mode ctxt cls ths0 =
   729   let val thy = ProofContext.theory_of ctxt
   730       val th_cls_pairs =
   731         map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
   732       val ths = maps #2 th_cls_pairs
   733       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   734       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
   735       val _ = trace_msg (fn () => "THEOREM CLAUSES")
   736       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
   737       val (mode, {axioms, tfrees, skolem_somes}) = build_map mode ctxt cls ths
   738       val _ = if null tfrees then ()
   739               else (trace_msg (fn () => "TFREE CLAUSES");
   740                     app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
   741       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
   742       val thms = map #1 axioms
   743       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
   744       val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
   745       val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
   746   in
   747       case filter (is_false o prop_of) cls of
   748           false_th::_ => [false_th RS @{thm FalseE}]
   749         | [] =>
   750       case refute thms of
   751           Metis.Resolution.Contradiction mth =>
   752             let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
   753                           Metis.Thm.toString mth)
   754                 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
   755                              (*add constraints arising from converting goal to clause form*)
   756                 val proof = Metis.Proof.proof mth
   757                 val result = translate ctxt' mode skolem_somes axioms proof
   758                 and used = map_filter (used_axioms axioms) proof
   759                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
   760                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
   761                 val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
   762                   if common_thm used cls then NONE else SOME name)
   763             in
   764                 if not (null cls) andalso not (common_thm used cls) then
   765                   warning "Metis: The assumptions are inconsistent."
   766                 else
   767                   ();
   768                 if not (null unused) then
   769                   warning ("Metis: Unused theorems: " ^ commas_quote unused
   770                            ^ ".")
   771                 else
   772                   ();
   773                 case result of
   774                     (_,ith)::_ =>
   775                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
   776                          [ith])
   777                   | _ => (trace_msg (fn () => "Metis: No result");
   778                           [])
   779             end
   780         | Metis.Resolution.Satisfiable _ =>
   781             (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
   782              [])
   783   end;
   784 
   785 fun metis_general_tac mode ctxt ths i st0 =
   786   let val _ = trace_msg (fn () =>
   787         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   788   in
   789     if exists_type type_has_topsort (prop_of st0)
   790     then raise METIS "Metis: Proof state contains the universal sort {}"
   791     else
   792       (Meson.MESON (maps neg_clausify)
   793         (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
   794           THEN Meson_Tactic.expand_defs_tac st0) st0
   795   end
   796   handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
   797 
   798 val metis_tac = metis_general_tac HO;
   799 val metisF_tac = metis_general_tac FO;
   800 val metisFT_tac = metis_general_tac FT;
   801 
   802 fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
   803   SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
   804 
   805 val setup =
   806   type_lits_setup #>
   807   method @{binding metis} HO "METIS for FOL and HOL problems" #>
   808   method @{binding metisF} FO "METIS for FOL problems" #>
   809   method @{binding metisFT} FT "METIS with fully-typed translation" #>
   810   Method.setup @{binding finish_clausify}
   811     (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
   812     "cleanup after conversion to clauses";
   813 
   814 end;