src/HOL/Tools/Sledgehammer/metis_reconstruct.ML

 Proof reconstruction for Metis.
 *)
 
 signature METIS_RECONSTRUCT =
 sig
+  type mode = Metis_Translate.mode
+
+  val trace: bool Unsynchronized.ref
+  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
+  val replay_one_inference :
+    Proof.context -> mode -> (string * term) list
+    -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
+    -> (Metis_Thm.thm * thm) list
 end;
 
 structure Metis_Reconstruct : METIS_RECONSTRUCT =
 struct
 
+open Metis_Translate
+
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if !trace then tracing (msg ()) else ()
+
+datatype term_or_type = Term of Term.term | Type of Term.typ;
+
+fun terms_of [] = []
+  | terms_of (Term t :: tts) = t :: terms_of tts
+  | terms_of (Type _ :: tts) = terms_of tts;
+
+fun types_of [] = []
+  | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
+      if String.isPrefix "_" a then
+          (*Variable generated by Metis, which might have been a type variable.*)
+          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
+      else types_of tts
+  | types_of (Term _ :: tts) = types_of tts
+  | types_of (Type T :: tts) = T :: types_of tts;
+
+fun apply_list rator nargs rands =
+  let val trands = terms_of rands
+  in  if length trands = nargs then Term (list_comb(rator, trands))
+      else raise Fail
+        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
+          " expected " ^ Int.toString nargs ^
+          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
+  end;
+
+fun infer_types ctxt =
+  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
+
+(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
+  with variable constraints in the goal...at least, type inference often fails otherwise.
+  SEE ALSO axiom_inf below.*)
+fun mk_var (w,T) = Term.Var((w,1), T);
+
+(*include the default sort, if available*)
+fun mk_tfree ctxt w =
+  let val ww = "'" ^ w
+  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
+
+(*Remove the "apply" operator from an HO term*)
+fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
+  | strip_happ args x = (x, args);
+
+fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
+
+fun smart_invert_const "fequal" = @{const_name HOL.eq}
+  | smart_invert_const s = invert_const s
+
+fun hol_type_from_metis_term _ (Metis_Term.Var v) =
+     (case strip_prefix_and_unascii tvar_prefix v of
+          SOME w => make_tvar w
+        | NONE   => make_tvar v)
+  | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
+     (case strip_prefix_and_unascii type_const_prefix x of
+          SOME tc => Term.Type (smart_invert_const tc,
+                                map (hol_type_from_metis_term ctxt) tys)
+        | NONE    =>
+      case strip_prefix_and_unascii tfree_prefix x of
+          SOME tf => mk_tfree ctxt tf
+        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
+
+(*Maps metis terms to isabelle terms*)
+fun hol_term_from_metis_PT ctxt fol_tm =
+  let val thy = ProofContext.theory_of ctxt
+      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
+                                  Metis_Term.toString fol_tm)
+      fun tm_to_tt (Metis_Term.Var v) =
+             (case strip_prefix_and_unascii tvar_prefix v of
+                  SOME w => Type (make_tvar w)
+                | NONE =>
+              case strip_prefix_and_unascii schematic_var_prefix v of
+                  SOME w => Term (mk_var (w, HOLogic.typeT))
+                | NONE   => Term (mk_var (v, HOLogic.typeT)) )
+                    (*Var from Metis with a name like _nnn; possibly a type variable*)
+        | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
+        | tm_to_tt (t as Metis_Term.Fn (".",_)) =
+            let val (rator,rands) = strip_happ [] t
+            in  case rator of
+                    Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
+                  | _ => case tm_to_tt rator of
+                             Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
+                           | _ => raise Fail "tm_to_tt: HO application"
+            end
+        | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
+      and applic_to_tt ("=",ts) =
+            Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+        | applic_to_tt (a,ts) =
+            case strip_prefix_and_unascii const_prefix a of
+                SOME b =>
+                  let val c = smart_invert_const b
+                      val ntypes = num_type_args thy c
+                      val nterms = length ts - ntypes
+                      val tts = map tm_to_tt ts
+                      val tys = types_of (List.take(tts,ntypes))
+                  in if length tys = ntypes then
+                         apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
+                     else
+                       raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
+                                   " but gets " ^ Int.toString (length tys) ^
+                                   " type arguments\n" ^
+                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
+                                   " the terms are \n" ^
+                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
+                     end
+              | NONE => (*Not a constant. Is it a type constructor?*)
+            case strip_prefix_and_unascii type_const_prefix a of
+                SOME b =>
+                  Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
+              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
+            case strip_prefix_and_unascii tfree_prefix a of
+                SOME b => Type (mk_tfree ctxt b)
+              | NONE => (*a fixed variable? They are Skolem functions.*)
+            case strip_prefix_and_unascii fixed_var_prefix a of
+                SOME b =>
+                  let val opr = Term.Free(b, HOLogic.typeT)
+                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
+              | NONE => raise Fail ("unexpected metis function: " ^ a)
+  in
+    case tm_to_tt fol_tm of
+      Term t => t
+    | _ => raise Fail "fol_tm_to_tt: Term expected"
+  end
+
+(*Maps fully-typed metis terms to isabelle terms*)
+fun hol_term_from_metis_FT ctxt fol_tm =
+  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
+                                  Metis_Term.toString fol_tm)
+      fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
+             (case strip_prefix_and_unascii schematic_var_prefix v of
+                  SOME w =>  mk_var(w, dummyT)
+                | NONE   => mk_var(v, dummyT))
+        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
+            Const (@{const_name HOL.eq}, HOLogic.typeT)
+        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
+           (case strip_prefix_and_unascii const_prefix x of
+                SOME c => Const (smart_invert_const c, dummyT)
+              | NONE => (*Not a constant. Is it a fixed variable??*)
+            case strip_prefix_and_unascii fixed_var_prefix x of
+                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
+              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
+        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
+            cvt tm1 $ cvt tm2
+        | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
+            cvt tm1 $ cvt tm2
+        | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
+        | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
+            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
+        | cvt (t as Metis_Term.Fn (x, [])) =
+           (case strip_prefix_and_unascii const_prefix x of
+                SOME c => Const (smart_invert_const c, dummyT)
+              | NONE => (*Not a constant. Is it a fixed variable??*)
+            case strip_prefix_and_unascii fixed_var_prefix x of
+                SOME v => Free (v, dummyT)
+              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
+                  hol_term_from_metis_PT ctxt t))
+        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
+            hol_term_from_metis_PT ctxt t)
+  in fol_tm |> cvt end
+
+fun hol_term_from_metis FT = hol_term_from_metis_FT
+  | hol_term_from_metis _ = hol_term_from_metis_PT
+
+fun hol_terms_from_fol ctxt mode skolems fol_tms =
+  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
+      val _ = trace_msg (fn () => "  calling type inference:")
+      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
+      val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
+      val _ = app (fn t => trace_msg
+                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
+                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
+                  ts'
+  in  ts'  end;
+
+(* ------------------------------------------------------------------------- *)
+(* FOL step Inference Rules                                                  *)
+(* ------------------------------------------------------------------------- *)
+
+(*for debugging only*)
+(*
+fun print_thpair (fth,th) =
+  (trace_msg (fn () => "=============================================");
+   trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
+   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
+*)
+
+fun lookth thpairs (fth : Metis_Thm.thm) =
+  the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
+  handle Option.Option =>
+         raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
+
+fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
+
+(* INFERENCE RULE: AXIOM *)
+
+fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
+    (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
+
+(* INFERENCE RULE: ASSUME *)
+
+val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
+
+fun inst_excluded_middle thy i_atm =
+  let val th = EXCLUDED_MIDDLE
+      val [vx] = Term.add_vars (prop_of th) []
+      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
+  in  cterm_instantiate substs th  end;
+
+fun assume_inf ctxt mode skolems atm =
+  inst_excluded_middle
+      (ProofContext.theory_of ctxt)
+      (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
+
+(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying
+   to reconstruct them admits new possibilities of errors, e.g. concerning
+   sorts. Instead we try to arrange that new TVars are distinct and that types
+   can be inferred from terms.*)
+
+fun inst_inf ctxt mode skolems thpairs fsubst th =
+  let val thy = ProofContext.theory_of ctxt
+      val i_th   = lookth thpairs th
+      val i_th_vars = Term.add_vars (prop_of i_th) []
+      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
+      fun subst_translation (x,y) =
+            let val v = find_var x
+                (* We call "reveal_skolem_terms" and "infer_types" below. *)
+                val t = hol_term_from_metis mode ctxt y
+            in  SOME (cterm_of thy (Var v), t)  end
+            handle Option =>
+                (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^
+                                       " in " ^ Display.string_of_thm ctxt i_th);
+                 NONE)
+      fun remove_typeinst (a, t) =
+            case strip_prefix_and_unascii schematic_var_prefix a of
+                SOME b => SOME (b, t)
+              | NONE => case strip_prefix_and_unascii tvar_prefix a of
+                SOME _ => NONE          (*type instantiations are forbidden!*)
+              | NONE => SOME (a,t)    (*internal Metis var?*)
+      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
+      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
+      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
+      val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
+      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
+      val substs' = ListPair.zip (vars, map ctm_of tms)
+      val _ = trace_msg (fn () =>
+        cat_lines ("subst_translations:" ::
+          (substs' |> map (fn (x, y) =>
+            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
+            Syntax.string_of_term ctxt (term_of y)))));
+  in cterm_instantiate substs' i_th end
+  handle THM (msg, _, _) =>
+         error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
+
+(* INFERENCE RULE: RESOLVE *)
+
+(* Like RSN, but we rename apart only the type variables. Vars here typically
+   have an index of 1, and the use of RSN would increase this typically to 3.
+   Instantiations of those Vars could then fail. See comment on "mk_var". *)
+fun resolve_inc_tyvars thy tha i thb =
+  let
+    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
+    fun aux tha thb =
+      case Thm.bicompose false (false, tha, nprems_of tha) i thb
+           |> Seq.list_of |> distinct Thm.eq_thm of
+        [th] => th
+      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
+                        [tha, thb])
+  in
+    aux tha thb
+    handle TERM z =>
+           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
+              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
+              "TERM" exception (with "add_ffpair" as first argument). We then
+              perform unification of the types of variables by hand and try
+              again. We could do this the first time around but this error
+              occurs seldom and we don't want to break existing proofs in subtle
+              ways or slow them down needlessly. *)
+           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
+                   |> AList.group (op =)
+                   |> maps (fn ((s, _), T :: Ts) =>
+                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
+                   |> rpair (Envir.empty ~1)
+                   |-> fold (Pattern.unify thy)
+                   |> Envir.type_env |> Vartab.dest
+                   |> map (fn (x, (S, T)) =>
+                              pairself (ctyp_of thy) (TVar (x, S), T)) of
+             [] => raise TERM z
+           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
+  end
+
+fun mk_not (Const (@{const_name Not}, _) $ b) = b
+  | mk_not b = HOLogic.mk_not b
+
+(* Match untyped terms. *)
+fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
+  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
+  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
+    (a = b) (* The index is ignored, for some reason. *)
+  | untyped_aconv (Bound i) (Bound j) = (i = j)
+  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
+  | untyped_aconv (t1 $ t2) (u1 $ u2) =
+    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+  | untyped_aconv _ _ = false
+
+(* Finding the relative location of an untyped term within a list of terms *)
+fun literal_index lit =
+  let
+    val lit = Envir.eta_contract lit
+    fun get _ [] = raise Empty
+      | get n (x :: xs) =
+        if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then
+          n
+        else
+          get (n+1) xs
+  in get 1 end
+
+fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
+    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
+    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
+  in
+    (* Trivial cases where one operand is type info *)
+    if Thm.eq_thm (TrueI, i_th1) then
+      i_th2
+    else if Thm.eq_thm (TrueI, i_th2) then
+      i_th1
+    else
+      let
+        val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
+                              (Metis_Term.Fn atm)
+        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
+        val prems_th1 = prems_of i_th1
+        val prems_th2 = prems_of i_th2
+        val index_th1 = literal_index (mk_not i_atm) prems_th1
+              handle Empty => raise Fail "Failed to find literal in th1"
+        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
+        val index_th2 = literal_index i_atm prems_th2
+              handle Empty => raise Fail "Failed to find literal in th2"
+        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
+    in
+      resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
+                         i_th2
+    end
+  end;
+
+(* INFERENCE RULE: REFL *)
+
+val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
+
+val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
+val refl_idx = 1 + Thm.maxidx_of REFL_THM;
+
+fun refl_inf ctxt mode skolems t =
+  let val thy = ProofContext.theory_of ctxt
+      val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
+      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
+      val c_t = cterm_incr_types thy refl_idx i_t
+  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
+
+(* INFERENCE RULE: EQUALITY *)
+
+val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
+val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
+
+val metis_eq = Metis_Term.Fn ("=", []);
+
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
+  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
+  | get_ty_arg_size _ _ = 0;
+
+fun equality_inf ctxt mode skolems (pos, atm) fp fr =
+  let val thy = ProofContext.theory_of ctxt
+      val m_tm = Metis_Term.Fn atm
+      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
+      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
+      fun replace_item_list lx 0 (_::ls) = lx::ls
+        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
+      fun path_finder_FO tm [] = (tm, Term.Bound 0)
+        | path_finder_FO tm (p::ps) =
+            let val (tm1,args) = strip_comb tm
+                val adjustment = get_ty_arg_size thy tm1
+                val p' = if adjustment > p then p else p-adjustment
+                val tm_p = List.nth(args,p')
+                  handle Subscript =>
+                         error ("Cannot replay Metis proof in Isabelle:\n" ^
+                                "equality_inf: " ^ Int.toString p ^ " adj " ^
+                                Int.toString adjustment ^ " term " ^
+                                Syntax.string_of_term ctxt tm)
+                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
+                                      "  " ^ Syntax.string_of_term ctxt tm_p)
+                val (r,t) = path_finder_FO tm_p ps
+            in
+                (r, list_comb (tm1, replace_item_list t p' args))
+            end
+      fun path_finder_HO tm [] = (tm, Term.Bound 0)
+        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
+        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
+        | path_finder_HO tm ps =
+          raise Fail ("equality_inf, path_finder_HO: path = " ^
+                      space_implode " " (map Int.toString ps) ^
+                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
+      fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
+        | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
+            path_finder_FT tm ps t1
+        | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
+            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
+        | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
+            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
+        | path_finder_FT tm ps t =
+          raise Fail ("equality_inf, path_finder_FT: path = " ^
+                      space_implode " " (map Int.toString ps) ^
+                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
+                      " fol-term: " ^ Metis_Term.toString t)
+      fun path_finder FO tm ps _ = path_finder_FO tm ps
+        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
+             (*equality: not curried, as other predicates are*)
+             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
+             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
+        | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
+             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
+        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
+                            (Metis_Term.Fn ("=", [t1,t2])) =
+             (*equality: not curried, as other predicates are*)
+             if p=0 then path_finder_FT tm (0::1::ps)
+                          (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
+                          (*select first operand*)
+             else path_finder_FT tm (p::ps)
+                   (Metis_Term.Fn (".", [metis_eq,t2]))
+                   (*1 selects second operand*)
+        | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
+             (*if not equality, ignore head to skip the hBOOL predicate*)
+        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
+      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
+            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
+            in (tm, nt $ tm_rslt) end
+        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
+      val (tm_subst, body) = path_finder_lit i_atm fp
+      val tm_abs = Term.Abs ("x", type_of tm_subst, body)
+      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
+      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
+      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
+      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
+      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
+      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
+      val eq_terms = map (pairself (cterm_of thy))
+        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
+  in  cterm_instantiate eq_terms subst'  end;
+
+val factor = Seq.hd o distinct_subgoals_tac;
+
+fun step ctxt mode skolems thpairs p =
+  case p of
+    (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
+  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
+  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
+    factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
+  | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
+    factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
+  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
+  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
+    equality_inf ctxt mode skolems f_lit f_p f_r
+
+fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c)
+
+fun replay_one_inference ctxt mode skolems (fol_th, inf) thpairs =
+  let
+    val _ = trace_msg (fn () => "=============================================")
+    val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
+    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
+    val th = Meson.flexflex_first_order (step ctxt mode skolems
+                                              thpairs (fol_th, inf))
+    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
+    val _ = trace_msg (fn () => "=============================================")
+    val n_metis_lits =
+      length (filter is_real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
+    val _ = if nprems_of th = n_metis_lits then ()
+            else error "Cannot replay Metis proof in Isabelle."
+  in (fol_th, th) :: thpairs end
+
 end;