(*  Title:      HOL/Tools/Metis/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

   exception METIS of string * string

   val trace : bool Config.T

   val trace_msg : Proof.context -> (unit -> string) -> unit

   val verbose : bool Config.T

   val verbose_warning : Proof.context -> string -> unit

   val hol_clause_from_metis :

     Proof.context -> int Symtab.table -> Metis_Thm.thm -> term

   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 -> int Symtab.table

     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list

     -> (Metis_Thm.thm * thm) list

   val discharge_skolem_premises :

     Proof.context -> (thm * term) option list -> thm -> thm

 end;

 structure Metis_Reconstruct : METIS_RECONSTRUCT =

 struct

 open ATP_Problem

 open ATP_Translate

 open ATP_Reconstruct

 open Metis_Translate

 exception METIS of string * string

 val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)

 val verbose = Attrib.setup_config_bool @{binding metis_verbose} (K true)

 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()

 fun verbose_warning ctxt msg =

   if Config.get ctxt verbose then warning ("Metis: " ^ 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) =

     types_of tts

     |> (if String.isPrefix metis_generated_var_prefix a then

           (* Variable generated by Metis, which might have been a type

              variable. *)

           cons (TVar (("'" ^ a, idx), HOLogic.typeS))

         else

           I)

   | 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 " ^ string_of_int nargs ^

           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))

   end;

 fun infer_types ctxt =

   Syntax.check_terms (Proof_Context.set_mode Proof_Context.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 make_var (w, T) = Var ((w, 1), T)

 (*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 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 (invert_const tc,

                            map (hol_type_from_metis_term ctxt) tys)

         | NONE    =>

       case strip_prefix_and_unascii tfree_prefix x of

           SOME tf => make_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 = Proof_Context.theory_of ctxt

       val _ = trace_msg ctxt (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 (make_var (w, HOLogic.typeT))

                 | NONE   => SomeTerm (make_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 = b |> invert_const |> unproxify_const

                     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_const_prefix c then

                         Var ((new_skolem_var_name_from_const c, 1),

                              Type_Infer.paramify_vars (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 " ^ string_of_int ntypes ^

                                    " but gets " ^ string_of_int (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 (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 (make_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 ctxt (fn () => "hol_term_from_metis_FT: " ^

                                        Metis_Term.toString fol_tm)

       fun do_const c =

         let val c = c |> invert_const |> unproxify_const in

           if String.isPrefix new_skolem_const_prefix c then

             Var ((new_skolem_var_name_from_const c, 1), dummyT)

           else

             Const (c, dummyT)

         end

       fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) =

              (case strip_prefix_and_unascii schematic_var_prefix v of

                   SOME w =>  make_var (w, dummyT)

                 | NONE   => make_var (v, dummyT))

         | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) =

             Const (@{const_name HOL.eq}, HOLogic.typeT)

         | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) =

            (case strip_prefix_and_unascii const_prefix x of

                 SOME c => do_const c

               | 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 (":", [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 => do_const c

               | 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 ctxt (fn () =>

                                       "hol_term_from_metis_FT bad const: " ^ x);

                          hol_term_from_metis_PT ctxt t))

         | cvt t = (trace_msg ctxt (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 atp_name_from_metis s =

   case find_first (fn (_, (s', _)) => s' = s) metis_name_table of

     SOME ((s, _), (_, swap)) => (s, swap)

   | _ => (s, false)

 fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =

     let val (s, swap) = atp_name_from_metis s in

       ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)

     end

   | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])

 fun hol_term_from_metis_MX ctxt sym_tab =

   atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE

 fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt

   | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt

   | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt

   | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab

 fun atp_literal_from_metis (pos, atom) =

   atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot

 fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))

   | atp_clause_from_metis lits =

     lits |> map atp_literal_from_metis |> mk_aconns AOr

 fun hol_clause_from_metis ctxt sym_tab =

   Metis_Thm.clause

   #> Metis_LiteralSet.toList

   #> atp_clause_from_metis

   #> prop_from_atp ctxt false sym_tab

 fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =

   let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms

       val _ = trace_msg ctxt (fn () => "  calling type inference:")

       val _ = app (fn t => trace_msg ctxt

                                      (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 ctxt

                     (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 ctxt (fth,th) =

   (trace_msg ctxt (fn () => "=============================================");

    trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);

    trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));

 *)

 fun lookth th_pairs fth =

   the (AList.lookup (uncurry Metis_Thm.equal) th_pairs 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 *)

 (* This causes variables to have an index of 1 by default. See also "make_var"

    above. *)

 fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)

 (* 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 sym_tab atm =

   inst_excluded_middle

       (Proof_Context.theory_of ctxt)

       (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)

                  (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 sym_tab th_pairs fsubst th =

   let val thy = Proof_Context.theory_of ctxt

       val i_th = lookth th_pairs 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 ctxt mode sym_tab y

         in  SOME (cterm_of thy (Var v), t)  end

         handle Option.Option =>

                (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^

                                          " in " ^ Display.string_of_thm ctxt i_th);

                 NONE)

              | TYPE _ =>

                (trace_msg ctxt (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 ctxt (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 ctxt (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, _, _) => raise METIS ("inst_inf", msg)

        | ERROR msg => raise METIS ("inst_inf", 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 "make_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 s_not (@{const Not} $ t) = t

   | s_not t = HOLogic.mk_not t

 fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)

   | simp_not_not t = t

 (* 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)

   | 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 index_of_literal lit haystack =

   let

     val normalize = simp_not_not o Envir.eta_contract

     val match_lit =

       HOLogic.dest_Trueprop #> normalize

       #> curry untyped_aconv (lit |> normalize)

   in case find_index match_lit haystack of ~1 => raise Empty | n => n + 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 avoiding

    to create double negations. The "select" wrapper is a trick to ensure that

    "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We

    don't use this trick in general because it makes the proof object uglier than

    necessary. FIXME. *)

 fun negate_head th =

   if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then

     (th RS @{thm select_FalseI})

     |> fold (rewrite_rule o single)

             @{thms not_atomize_select atomize_not_select}

   else

     th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}

 (* 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 sym_tab th_pairs atm th1 th2 =

   let

     val thy = Proof_Context.theory_of ctxt

     val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)

     val _ = trace_msg ctxt (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)

     val _ = trace_msg ctxt (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_metis ctxt mode old_skolems sym_tab)

                     (Metis_Term.Fn atm)

         val _ = trace_msg ctxt (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 =

           index_of_literal (s_not i_atm) prems_th1

           handle Empty => raise Fail "Failed to find literal in th1"

         val _ = trace_msg ctxt (fn () => "  index_th1: " ^ string_of_int index_th1)

         val index_th2 =

           index_of_literal i_atm prems_th2

           handle Empty => raise Fail "Failed to find literal in th2"

         val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)

     in

       resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2

       handle TERM (s, _) => raise METIS ("resolve_inf", s)

     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 sym_tab t =

   let

     val thy = Proof_Context.theory_of ctxt

     val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t

     val _ = trace_msg ctxt (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 ("=", []);

 (* Equality has no type arguments *)

 fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0

   | get_ty_arg_size thy (Const (s, _)) =

     (num_type_args thy s handle TYPE _ => 0)

   | get_ty_arg_size _ _ = 0

 fun equality_inf ctxt mode old_skolems sym_tab (pos, atm) fp fr =

   let val thy = Proof_Context.theory_of ctxt

       val m_tm = Metis_Term.Fn atm

       val [i_atm, i_tm] =

         hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr]

       val _ = trace_msg ctxt (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_fail mode tm ps t =

         raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^

                     "equality_inf, path_finder_" ^ string_of_mode mode ^

                     ": path = " ^ space_implode " " (map string_of_int ps) ^

                     " isa-term: " ^ Syntax.string_of_term ctxt tm ^

                     (case t of

                        SOME t => " fol-term: " ^ Metis_Term.toString t

                      | NONE => ""))

       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 = nth args p'

                   handle Subscript =>

                          raise METIS ("equality_inf",

                                       string_of_int p ^ " adj " ^

                                       string_of_int adjustment ^ " term " ^

                                       Syntax.string_of_term ctxt tm)

                 val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int 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 = path_finder_fail HO tm ps NONE

       fun path_finder_FT tm [] _ = (tm, Bound 0)

         | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [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 = path_finder_fail FT tm ps (SOME t)

       fun path_finder_MX tm [] _ = (tm, Bound 0)

         | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =

           let val s = s |> unmangled_const_name in

             if s = metis_predicator orelse s = prefixed_predicator_name orelse

                s = metis_type_tag orelse s = prefixed_type_tag_name then

               path_finder_MX tm ps (nth ts p)

             else if s = metis_app_op orelse s = prefixed_app_op_name then

               let

                 val (tm1, tm2) = dest_comb tm

                 val p' = p - (length ts - 2)

               in

                 if p' = 0 then

                   path_finder_MX tm1 ps (nth ts p) ||> (fn y => y $ tm2)

                 else

                   path_finder_MX tm2 ps (nth ts p) ||> (fn y => tm1 $ y)

               end

             else

               let

                 val (tm1, args) = strip_comb tm

                 val adjustment = length ts - length args

                 val p' = if adjustment > p then p else p - adjustment

                 val tm_p = nth args p'

                   handle Subscript =>

                          path_finder_fail MX tm (p :: ps) (SOME t)

                 val _ = trace_msg ctxt (fn () =>

                     "path_finder: " ^ string_of_int p ^ "  " ^

                     Syntax.string_of_term ctxt tm_p)

                 val (r, t) = path_finder_MX tm_p ps (nth ts p)

               in (r, list_comb (tm1, replace_item_list t p' args)) end

           end

         | path_finder_MX tm ps t = path_finder_fail MX tm ps (SOME 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_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2]))

                           (*select first operand*)

              else path_finder_FT tm (p::ps)

                    (Metis_Term.Fn (metis_app_op, [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!*)

         | path_finder MX tm ps t = path_finder_MX tm ps t

       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 ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)

       val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)

       val _ = trace_msg ctxt (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 ctxt (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 one_step ctxt mode old_skolems sym_tab th_pairs p =

   case p of

     (fol_th, Metis_Proof.Axiom _) => axiom_inf th_pairs fol_th |> factor

   | (_, Metis_Proof.Assume f_atm) =>

     assume_inf ctxt mode old_skolems sym_tab f_atm

   | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>

     inst_inf ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 |> factor

   | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>

     resolve_inf ctxt mode old_skolems sym_tab th_pairs f_atm f_th1 f_th2

     |> factor

   | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems sym_tab f_tm

   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>

     equality_inf ctxt mode old_skolems sym_tab 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 is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)

 fun is_isabelle_literal_genuine t =

   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true

 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0

 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate

    disjuncts are impossible. In the Isabelle proof, in spite of efforts to

    eliminate them, duplicates sometimes appear with slightly different (but

    unifiable) types. *)

 fun resynchronize ctxt fol_th th =

   let

     val num_metis_lits =

       count is_metis_literal_genuine

             (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))

     val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)

   in

     if num_metis_lits >= num_isabelle_lits then

       th

     else

       let

         val (prems0, concl) = th |> prop_of |> Logic.strip_horn

         val prems = prems0 |> distinct untyped_aconv

         val goal = Logic.list_implies (prems, concl)

       in

         if length prems = length prems0 then

           raise METIS ("resynchronize", "Out of sync")

         else

           Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1

                                          THEN ALLGOALS assume_tac))

           |> resynchronize ctxt fol_th

       end

   end

 fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs =

   if not (null th_pairs) andalso

      prop_of (snd (hd th_pairs)) aconv @{prop False} then

     (* Isabelle sometimes identifies literals (premises) that are distinct in

        Metis (e.g., because of type variables). We give the Isabelle proof the

        benefice of the doubt. *)

     th_pairs

   else

     let

       val _ = trace_msg ctxt

                   (fn () => "=============================================")

       val _ = trace_msg ctxt

                   (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)

       val _ = trace_msg ctxt

                   (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)

       val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf)

                |> flexflex_first_order

                |> resynchronize ctxt fol_th

       val _ = trace_msg ctxt

                   (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)

       val _ = trace_msg ctxt

                   (fn () => "=============================================")

     in (fol_th, th) :: th_pairs end

 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with

    one of the premises. Unfortunately, this sometimes yields "Variable

    ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the

    variables before applying "assume_tac". Typical constraints are of the form

      ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,

    where the nonvariables are goal parameters. *)

 fun unify_first_prem_with_concl thy i th =

   let

     val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract

     val prem = goal |> Logic.strip_assums_hyp |> hd

     val concl = goal |> Logic.strip_assums_concl

     fun pair_untyped_aconv (t1, t2) (u1, u2) =

       untyped_aconv (t1, u1) andalso untyped_aconv (t2, u2)

     fun add_terms tp inst =

       if exists (pair_untyped_aconv tp) inst then inst

       else tp :: map (apsnd (subst_atomic [tp])) inst

     fun is_flex t =

       case strip_comb t of

         (Var _, args) => forall is_Bound args

       | _ => false

     fun unify_flex flex rigid =

       case strip_comb flex of

         (Var (z as (_, T)), args) =>

         add_terms (Var z,

           fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)

       | _ => I

     fun unify_potential_flex comb atom =

       if is_flex comb then unify_flex comb atom

       else if is_Var atom then add_terms (atom, comb)

       else I

     fun unify_terms (t, u) =

       case (t, u) of

         (t1 $ t2, u1 $ u2) =>

         if is_flex t then unify_flex t u

         else if is_flex u then unify_flex u t

         else fold unify_terms [(t1, u1), (t2, u2)]

       | (_ $ _, _) => unify_potential_flex t u

       | (_, _ $ _) => unify_potential_flex u t

       | (Var _, _) => add_terms (t, u)

       | (_, Var _) => add_terms (u, t)

       | _ => I

     val t_inst =

       [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))

          |> the_default [] (* FIXME *)

   in th |> cterm_instantiate t_inst end

 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}

 fun copy_prems_tac [] ns i =

     if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i

   | copy_prems_tac (1 :: ms) ns i =

     rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i

   | copy_prems_tac (m :: ms) ns i =

     etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i

 (* Metis generates variables of the form _nnn. *)

 val is_metis_fresh_variable = String.isPrefix "_"

 fun instantiate_forall_tac thy t i st =

   let

     val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev

     fun repair (t as (Var ((s, _), _))) =

         (case find_index (fn (s', _) => s' = s) params of

            ~1 => t

          | j => Bound j)

       | repair (t $ u) =

         (case (repair t, repair u) of

            (t as Bound j, u as Bound k) =>

            (* This is a rather subtle trick to repair the discrepancy between

               the fully skolemized term that MESON gives us (where existentials

               were pulled out) and the reality. *)

            if k > j then t else t $ u

          | (t, u) => t $ u)

       | repair t = t

     val t' = t |> repair |> fold (curry absdummy) (map snd params)

     fun do_instantiate th =

       case Term.add_vars (prop_of th) []

            |> filter_out ((Meson_Clausify.is_zapped_var_name orf

                            is_metis_fresh_variable) o fst o fst) of

         [] => th

       | [var as (_, T)] =>

         let

           val var_binder_Ts = T |> binder_types |> take (length params) |> rev

           val var_body_T = T |> funpow (length params) range_type

           val tyenv =

             Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,

                                              var_body_T :: var_binder_Ts)

           val env =

             Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,

                          tenv = Vartab.empty, tyenv = tyenv}

           val ty_inst =

             Vartab.fold (fn (x, (S, T)) =>

                             cons (pairself (ctyp_of thy) (TVar (x, S), T)))

                         tyenv []

           val t_inst =

             [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]

         in th |> instantiate (ty_inst, t_inst) end

       | _ => raise Fail "expected a single non-zapped, non-Metis Var"

   in

     (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)

      THEN PRIMITIVE do_instantiate) st

   end

 fun fix_exists_tac t =

   etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]

 fun release_quantifier_tac thy (skolem, t) =

   (if skolem then fix_exists_tac else instantiate_forall_tac thy) t

 fun release_clusters_tac _ _ _ [] = K all_tac

   | release_clusters_tac thy ax_counts substs

                          ((ax_no, cluster_no) :: clusters) =

     let

       val cluster_of_var =

         Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var

       fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no

       val cluster_substs =

         substs

         |> map_filter (fn (ax_no', (_, (_, tsubst))) =>

                           if ax_no' = ax_no then

                             tsubst |> map (apfst cluster_of_var)

                                    |> filter (in_right_cluster o fst)

                                    |> map (apfst snd)

                                    |> SOME

                           else

                             NONE)

       fun do_cluster_subst cluster_subst =

         map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]

       val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs

     in

       rotate_tac first_prem

       THEN' (EVERY' (maps do_cluster_subst cluster_substs))

       THEN' rotate_tac (~ first_prem - length cluster_substs)

       THEN' release_clusters_tac thy ax_counts substs clusters

     end

 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =

   (ax_no, (cluster_no, (skolem, index_no)))

 fun cluster_ord p =

   prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))

            (pairself cluster_key p)

 val tysubst_ord =

   list_ord (prod_ord Term_Ord.fast_indexname_ord

                      (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))

 structure Int_Tysubst_Table =

   Table(type key = int * (indexname * (sort * typ)) list

         val ord = prod_ord int_ord tysubst_ord)

 structure Int_Pair_Graph =

   Graph(type key = int * int val ord = prod_ord int_ord int_ord)

 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)

 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)

 (* Attempts to derive the theorem "False" from a theorem of the form

    "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the

    specified axioms. The axioms have leading "All" and "Ex" quantifiers, which

    must be eliminated first. *)

 fun discharge_skolem_premises ctxt axioms prems_imp_false =

   if prop_of prems_imp_false aconv @{prop False} then

     prems_imp_false

   else

     let

       val thy = Proof_Context.theory_of ctxt

       fun match_term p =

         let

           val (tyenv, tenv) =

             Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)

           val tsubst =

             tenv |> Vartab.dest

                  |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)

                  |> sort (cluster_ord

                           o pairself (Meson_Clausify.cluster_of_zapped_var_name

                                       o fst o fst))

                  |> map (Meson.term_pair_of

                          #> pairself (Envir.subst_term_types tyenv))

           val tysubst = tyenv |> Vartab.dest

         in (tysubst, tsubst) end

       fun subst_info_for_prem subgoal_no prem =

         case prem of

           _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>

           let val ax_no = HOLogic.dest_nat num in

             (ax_no, (subgoal_no,

                      match_term (nth axioms ax_no |> the |> snd, t)))

           end

         | _ => raise TERM ("discharge_skolem_premises: Malformed premise",

                            [prem])

       fun cluster_of_var_name skolem s =

         case try Meson_Clausify.cluster_of_zapped_var_name s of

           NONE => NONE

         | SOME ((ax_no, (cluster_no, _)), skolem') =>

           if skolem' = skolem andalso cluster_no > 0 then

             SOME (ax_no, cluster_no)

           else

             NONE

       fun clusters_in_term skolem t =

         Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)

       fun deps_for_term_subst (var, t) =

         case clusters_in_term false var of

           [] => NONE

         | [(ax_no, cluster_no)] =>

           SOME ((ax_no, cluster_no),

                 clusters_in_term true t

                 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))

         | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])

       val prems = Logic.strip_imp_prems (prop_of prems_imp_false)

       val substs = prems |> map2 subst_info_for_prem (1 upto length prems)

                          |> sort (int_ord o pairself fst)

       val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs

       val clusters = maps (op ::) depss

       val ordered_clusters =

         Int_Pair_Graph.empty

         |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)

         |> fold Int_Pair_Graph.add_deps_acyclic depss

         |> Int_Pair_Graph.topological_order

         handle Int_Pair_Graph.CYCLES _ =>

                error "Cannot replay Metis proof in Isabelle without \

                      \\"Hilbert_Choice\"."

       val ax_counts =

         Int_Tysubst_Table.empty

         |> fold (fn (ax_no, (_, (tysubst, _))) =>

                     Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)

                                                   (Integer.add 1)) substs

         |> Int_Tysubst_Table.dest

       val needed_axiom_props =

         0 upto length axioms - 1 ~~ axioms

         |> map_filter (fn (_, NONE) => NONE

                         | (ax_no, SOME (_, t)) =>

                           if exists (fn ((ax_no', _), n) =>

                                         ax_no' = ax_no andalso n > 0)

                                     ax_counts then

                             SOME t

                           else

                             NONE)

       val outer_param_names =

         [] |> fold Term.add_var_names needed_axiom_props

            |> filter (Meson_Clausify.is_zapped_var_name o fst)

            |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))

            |> filter (fn (((_, (cluster_no, _)), skolem), _) =>

                          cluster_no = 0 andalso skolem)

            |> sort shuffle_ord |> map (fst o snd)

 (* for debugging only:

       fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =

         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^

         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^

         commas (map ((fn (s, t) => s ^ " |-> " ^ t)

                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"

       val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)

       val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)

       val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)

       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^

                        cat_lines (map string_for_subst_info substs))

 *)

       fun cut_and_ex_tac axiom =

         cut_rules_tac [axiom] 1

         THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)

       fun rotation_for_subgoal i =

         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs

     in

       Goal.prove ctxt [] [] @{prop False}

           (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst

                                   o fst) ax_counts)

                       THEN rename_tac outer_param_names 1

                       THEN copy_prems_tac (map snd ax_counts) [] 1)

               THEN release_clusters_tac thy ax_counts substs ordered_clusters 1

               THEN match_tac [prems_imp_false] 1

               THEN ALLGOALS (fn i =>

                        rtac @{thm Meson.skolem_COMBK_I} i

                        THEN rotate_tac (rotation_for_subgoal i) i

                        THEN PRIMITIVE (unify_first_prem_with_concl thy i)

                        THEN assume_tac i

                        THEN flexflex_tac)))

       handle ERROR _ =>

              error ("Cannot replay Metis proof in Isabelle:\n\

                     \Error when discharging Skolem assumptions.")

     end

 end;