src/HOL/Tools/Sledgehammer/metis_reconstruct.ML

move functions closer to where they're used

(*  Title:      HOL/Tools/Sledgehammer/metis_reconstruct.ML
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   Cambridge University 2007

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 untyped_aconv : term -> term -> bool
  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 = SomeTerm of term | SomeType of typ

fun terms_of [] = []
  | terms_of (SomeTerm t :: tts) = t :: terms_of tts
  | terms_of (SomeType _ :: tts) = terms_of tts;

fun types_of [] = []
  | types_of (SomeTerm (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 (SomeTerm _ :: tts) = types_of tts
  | types_of (SomeType T :: tts) = T :: types_of tts;

fun apply_list rator nargs rands =
  let val trands = terms_of rands
  in  if length trands = nargs then SomeTerm (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) = 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 => 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 => SomeType (make_tvar w)
                | NONE =>
              case strip_prefix_and_unascii schematic_var_prefix v of
                  SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
                | NONE   => SomeTerm (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
                             SomeTerm t => SomeTerm (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) =
            SomeTerm (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))
                    val t = if String.isPrefix new_skolem_prefix c then
                              Var (new_skolem_var_from_const c, tl tys ---> hd tys)
                            else
                              Const (c, dummyT)
                  in if length tys = ntypes then
                         apply_list t 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 =>
                SomeType (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 => SomeType (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 = 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
      SomeTerm t => t
    | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
  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 old_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_old_skolem_terms old_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 old_skolems atm =
  inst_excluded_middle
      (ProofContext.theory_of ctxt)
      (singleton (hol_terms_from_fol ctxt mode old_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 old_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_old_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.Option =>
               (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
                                    " in " ^ Display.string_of_thm ctxt i_th);
                NONE)
             | TYPE _ =>
               (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ 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_old_skolem_terms old_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

(* Permute a rule's premises to move the i-th premise to the last position. *)
fun make_last i th =
  let val n = nprems_of th
  in  if 1 <= i andalso i <= n
      then Thm.permute_prems (i-1) 1 th
      else raise THM("select_literal", i, [th])
  end;

(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   double-negations. *)
val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]

(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last

fun resolve_inf ctxt mode old_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 old_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 (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 old_skolems t =
  let val thy = ProofContext.theory_of ctxt
      val i_t = singleton (hol_terms_from_fol ctxt mode old_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 old_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 old_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, 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, 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 ("Cannot replay Metis proof in Isabelle:\n" ^
                      "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, 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 ("Cannot replay Metis proof in Isabelle:\n" ^
                      "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 = 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 old_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 old_skolems f_atm
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
    factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
  | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
    factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
    equality_inf ctxt mode old_skolems f_lit f_p f_r

fun flexflex_first_order th =
  case Thm.tpairs_of th of
      [] => th
    | pairs =>
        let val thy = theory_of_thm th
            val (_, tenv) =
              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
        in  th'  end
        handle THM _ => th;

fun replay_one_inference ctxt mode old_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 = step ctxt mode old_skolems thpairs (fol_th, inf)
             |> flexflex_first_order
    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
    val _ = trace_msg (fn () => "=============================================")
  in (fol_th, th) :: thpairs end

end;