src/HOL/Tools/Metis/metis_reconstruct.ML
author blanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42344 4a58173ffb99
parent 42342 6babd86a54a4
child 42348 187354e22c7d
permissions -rw-r--r--
"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now
     1 (*  Title:      HOL/Tools/Metis/metis_reconstruct.ML
     2     Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     3     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     4     Author:     Jasmin Blanchette, TU Muenchen
     5     Copyright   Cambridge University 2007
     6 
     7 Proof reconstruction for Metis.
     8 *)
     9 
    10 signature METIS_RECONSTRUCT =
    11 sig
    12   type mode = Metis_Translate.mode
    13 
    14   val trace : bool Config.T
    15   val trace_msg : Proof.context -> (unit -> string) -> unit
    16   val verbose : bool Config.T
    17   val verbose_warning : Proof.context -> string -> unit
    18   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    19   val untyped_aconv : term -> term -> bool
    20   val replay_one_inference :
    21     Proof.context -> mode -> (string * term) list
    22     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    23     -> (Metis_Thm.thm * thm) list
    24   val discharge_skolem_premises :
    25     Proof.context -> (thm * term) option list -> thm -> thm
    26   val setup : theory -> theory
    27 end;
    28 
    29 structure Metis_Reconstruct : METIS_RECONSTRUCT =
    30 struct
    31 
    32 open Metis_Translate
    33 
    34 val (trace, trace_setup) = Attrib.config_bool "metis_trace" (K false)
    35 val (verbose, verbose_setup) = Attrib.config_bool "metis_verbose" (K true)
    36 
    37 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    38 fun verbose_warning ctxt msg =
    39   if Config.get ctxt verbose then warning msg else ()
    40 
    41 datatype term_or_type = SomeTerm of term | SomeType of typ
    42 
    43 fun terms_of [] = []
    44   | terms_of (SomeTerm t :: tts) = t :: terms_of tts
    45   | terms_of (SomeType _ :: tts) = terms_of tts;
    46 
    47 fun types_of [] = []
    48   | types_of (SomeTerm (Var ((a,idx), _)) :: tts) =
    49       if String.isPrefix metis_generated_var_prefix a then
    50           (*Variable generated by Metis, which might have been a type variable.*)
    51           TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
    52       else types_of tts
    53   | types_of (SomeTerm _ :: tts) = types_of tts
    54   | types_of (SomeType T :: tts) = T :: types_of tts;
    55 
    56 fun apply_list rator nargs rands =
    57   let val trands = terms_of rands
    58   in  if length trands = nargs then SomeTerm (list_comb(rator, trands))
    59       else raise Fail
    60         ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
    61           " expected " ^ string_of_int nargs ^
    62           " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
    63   end;
    64 
    65 fun infer_types ctxt =
    66   Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
    67 
    68 (*We use 1 rather than 0 because variable references in clauses may otherwise conflict
    69   with variable constraints in the goal...at least, type inference often fails otherwise.
    70   SEE ALSO axiom_inf below.*)
    71 fun mk_var (w, T) = Var ((w, 1), T)
    72 
    73 (*include the default sort, if available*)
    74 fun mk_tfree ctxt w =
    75   let val ww = "'" ^ w
    76   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
    77 
    78 (*Remove the "apply" operator from an HO term*)
    79 fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
    80   | strip_happ args x = (x, args);
    81 
    82 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
    83 
    84 fun hol_type_from_metis_term _ (Metis_Term.Var v) =
    85      (case strip_prefix_and_unascii tvar_prefix v of
    86           SOME w => make_tvar w
    87         | NONE   => make_tvar v)
    88   | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
    89      (case strip_prefix_and_unascii type_const_prefix x of
    90           SOME tc => Type (invert_const tc,
    91                            map (hol_type_from_metis_term ctxt) tys)
    92         | NONE    =>
    93       case strip_prefix_and_unascii tfree_prefix x of
    94           SOME tf => mk_tfree ctxt tf
    95         | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
    96 
    97 (*Maps metis terms to isabelle terms*)
    98 fun hol_term_from_metis_PT ctxt fol_tm =
    99   let val thy = ProofContext.theory_of ctxt
   100       val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
   101                                        Metis_Term.toString fol_tm)
   102       fun tm_to_tt (Metis_Term.Var v) =
   103              (case strip_prefix_and_unascii tvar_prefix v of
   104                   SOME w => SomeType (make_tvar w)
   105                 | NONE =>
   106               case strip_prefix_and_unascii schematic_var_prefix v of
   107                   SOME w => SomeTerm (mk_var (w, HOLogic.typeT))
   108                 | NONE   => SomeTerm (mk_var (v, HOLogic.typeT)))
   109                     (*Var from Metis with a name like _nnn; possibly a type variable*)
   110         | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
   111         | tm_to_tt (t as Metis_Term.Fn (".",_)) =
   112             let val (rator,rands) = strip_happ [] t
   113             in  case rator of
   114                     Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
   115                   | _ => case tm_to_tt rator of
   116                              SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
   117                            | _ => raise Fail "tm_to_tt: HO application"
   118             end
   119         | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
   120       and applic_to_tt ("=",ts) =
   121             SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
   122         | applic_to_tt (a,ts) =
   123             case strip_prefix_and_unascii const_prefix a of
   124                 SOME b =>
   125                   let
   126                     val c = invert_const b
   127                     val ntypes = num_type_args thy c
   128                     val nterms = length ts - ntypes
   129                     val tts = map tm_to_tt ts
   130                     val tys = types_of (List.take(tts,ntypes))
   131                     val t =
   132                       if String.isPrefix new_skolem_const_prefix c then
   133                         Var ((new_skolem_var_name_from_const c, 1),
   134                              Type_Infer.paramify_vars (tl tys ---> hd tys))
   135                       else
   136                         Const (c, dummyT)
   137                   in if length tys = ntypes then
   138                          apply_list t nterms (List.drop(tts,ntypes))
   139                      else
   140                        raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^
   141                                    " but gets " ^ string_of_int (length tys) ^
   142                                    " type arguments\n" ^
   143                                    cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
   144                                    " the terms are \n" ^
   145                                    cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
   146                      end
   147               | NONE => (*Not a constant. Is it a type constructor?*)
   148             case strip_prefix_and_unascii type_const_prefix a of
   149                 SOME b =>
   150                 SomeType (Type (invert_const b, types_of (map tm_to_tt ts)))
   151               | NONE => (*Maybe a TFree. Should then check that ts=[].*)
   152             case strip_prefix_and_unascii tfree_prefix a of
   153                 SOME b => SomeType (mk_tfree ctxt b)
   154               | NONE => (*a fixed variable? They are Skolem functions.*)
   155             case strip_prefix_and_unascii fixed_var_prefix a of
   156                 SOME b =>
   157                   let val opr = Free (b, HOLogic.typeT)
   158                   in  apply_list opr (length ts) (map tm_to_tt ts)  end
   159               | NONE => raise Fail ("unexpected metis function: " ^ a)
   160   in
   161     case tm_to_tt fol_tm of
   162       SomeTerm t => t
   163     | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], [])
   164   end
   165 
   166 (*Maps fully-typed metis terms to isabelle terms*)
   167 fun hol_term_from_metis_FT ctxt fol_tm =
   168   let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
   169                                        Metis_Term.toString fol_tm)
   170       fun do_const c =
   171         let val c = c |> invert_const in
   172           if String.isPrefix new_skolem_const_prefix c then
   173             Var ((new_skolem_var_name_from_const c, 1), dummyT)
   174           else
   175             Const (c, dummyT)
   176         end
   177       fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
   178              (case strip_prefix_and_unascii schematic_var_prefix v of
   179                   SOME w =>  mk_var(w, dummyT)
   180                 | NONE   => mk_var(v, dummyT))
   181         | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
   182             Const (@{const_name HOL.eq}, HOLogic.typeT)
   183         | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
   184            (case strip_prefix_and_unascii const_prefix x of
   185                 SOME c => do_const c
   186               | NONE => (*Not a constant. Is it a fixed variable??*)
   187             case strip_prefix_and_unascii fixed_var_prefix x of
   188                 SOME v => Free (v, hol_type_from_metis_term ctxt ty)
   189               | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
   190         | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
   191             cvt tm1 $ cvt tm2
   192         | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
   193             cvt tm1 $ cvt tm2
   194         | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
   195         | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
   196             list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
   197         | cvt (t as Metis_Term.Fn (x, [])) =
   198            (case strip_prefix_and_unascii const_prefix x of
   199                 SOME c => do_const c
   200               | NONE => (*Not a constant. Is it a fixed variable??*)
   201             case strip_prefix_and_unascii fixed_var_prefix x of
   202                 SOME v => Free (v, dummyT)
   203               | NONE => (trace_msg ctxt (fn () =>
   204                                       "hol_term_from_metis_FT bad const: " ^ x);
   205                          hol_term_from_metis_PT ctxt t))
   206         | cvt t = (trace_msg ctxt (fn () =>
   207                    "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
   208                    hol_term_from_metis_PT ctxt t)
   209   in fol_tm |> cvt end
   210 
   211 fun hol_term_from_metis FT = hol_term_from_metis_FT
   212   | hol_term_from_metis _ = hol_term_from_metis_PT
   213 
   214 fun hol_terms_from_metis ctxt mode old_skolems fol_tms =
   215   let val ts = map (hol_term_from_metis mode ctxt) fol_tms
   216       val _ = trace_msg ctxt (fn () => "  calling type inference:")
   217       val _ = app (fn t => trace_msg ctxt
   218                                      (fn () => Syntax.string_of_term ctxt t)) ts
   219       val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
   220                    |> infer_types ctxt
   221       val _ = app (fn t => trace_msg ctxt
   222                     (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
   223                               "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
   224                   ts'
   225   in  ts'  end;
   226 
   227 (* ------------------------------------------------------------------------- *)
   228 (* FOL step Inference Rules                                                  *)
   229 (* ------------------------------------------------------------------------- *)
   230 
   231 (*for debugging only*)
   232 (*
   233 fun print_thpair ctxt (fth,th) =
   234   (trace_msg ctxt (fn () => "=============================================");
   235    trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
   236    trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   237 *)
   238 
   239 fun lookth thpairs (fth : Metis_Thm.thm) =
   240   the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
   241   handle Option.Option =>
   242          raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
   243 
   244 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
   245 
   246 (* INFERENCE RULE: AXIOM *)
   247 
   248 fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
   249     (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
   250 
   251 (* INFERENCE RULE: ASSUME *)
   252 
   253 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
   254 
   255 fun inst_excluded_middle thy i_atm =
   256   let val th = EXCLUDED_MIDDLE
   257       val [vx] = Term.add_vars (prop_of th) []
   258       val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
   259   in  cterm_instantiate substs th  end;
   260 
   261 fun assume_inf ctxt mode skolem_params atm =
   262   inst_excluded_middle
   263       (ProofContext.theory_of ctxt)
   264       (singleton (hol_terms_from_metis ctxt mode skolem_params)
   265                  (Metis_Term.Fn atm))
   266 
   267 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
   268    to reconstruct them admits new possibilities of errors, e.g. concerning
   269    sorts. Instead we try to arrange that new TVars are distinct and that types
   270    can be inferred from terms. *)
   271 
   272 fun inst_inf ctxt mode old_skolems thpairs fsubst th =
   273   let val thy = ProofContext.theory_of ctxt
   274       val i_th = lookth thpairs th
   275       val i_th_vars = Term.add_vars (prop_of i_th) []
   276       fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   277       fun subst_translation (x,y) =
   278         let val v = find_var x
   279             (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
   280             val t = hol_term_from_metis mode ctxt y
   281         in  SOME (cterm_of thy (Var v), t)  end
   282         handle Option.Option =>
   283                (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
   284                                          " in " ^ Display.string_of_thm ctxt i_th);
   285                 NONE)
   286              | TYPE _ =>
   287                (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   288                                          " in " ^ Display.string_of_thm ctxt i_th);
   289                 NONE)
   290       fun remove_typeinst (a, t) =
   291             case strip_prefix_and_unascii schematic_var_prefix a of
   292                 SOME b => SOME (b, t)
   293               | NONE => case strip_prefix_and_unascii tvar_prefix a of
   294                 SOME _ => NONE          (*type instantiations are forbidden!*)
   295               | NONE => SOME (a,t)    (*internal Metis var?*)
   296       val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   297       val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   298       val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   299       val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
   300                        |> infer_types ctxt
   301       val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   302       val substs' = ListPair.zip (vars, map ctm_of tms)
   303       val _ = trace_msg ctxt (fn () =>
   304         cat_lines ("subst_translations:" ::
   305           (substs' |> map (fn (x, y) =>
   306             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   307             Syntax.string_of_term ctxt (term_of y)))));
   308   in cterm_instantiate substs' i_th end
   309   handle THM (msg, _, _) =>
   310          error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
   311 
   312 (* INFERENCE RULE: RESOLVE *)
   313 
   314 (* Like RSN, but we rename apart only the type variables. Vars here typically
   315    have an index of 1, and the use of RSN would increase this typically to 3.
   316    Instantiations of those Vars could then fail. See comment on "mk_var". *)
   317 fun resolve_inc_tyvars thy tha i thb =
   318   let
   319     val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
   320     fun aux tha thb =
   321       case Thm.bicompose false (false, tha, nprems_of tha) i thb
   322            |> Seq.list_of |> distinct Thm.eq_thm of
   323         [th] => th
   324       | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
   325                         [tha, thb])
   326   in
   327     aux tha thb
   328     handle TERM z =>
   329            (* The unifier, which is invoked from "Thm.bicompose", will sometimes
   330               refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
   331               "TERM" exception (with "add_ffpair" as first argument). We then
   332               perform unification of the types of variables by hand and try
   333               again. We could do this the first time around but this error
   334               occurs seldom and we don't want to break existing proofs in subtle
   335               ways or slow them down needlessly. *)
   336            case [] |> fold (Term.add_vars o prop_of) [tha, thb]
   337                    |> AList.group (op =)
   338                    |> maps (fn ((s, _), T :: Ts) =>
   339                                map (fn T' => (Free (s, T), Free (s, T'))) Ts)
   340                    |> rpair (Envir.empty ~1)
   341                    |-> fold (Pattern.unify thy)
   342                    |> Envir.type_env |> Vartab.dest
   343                    |> map (fn (x, (S, T)) =>
   344                               pairself (ctyp_of thy) (TVar (x, S), T)) of
   345              [] => raise TERM z
   346            | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
   347   end
   348 
   349 fun s_not (@{const Not} $ t) = t
   350   | s_not t = HOLogic.mk_not t
   351 fun simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   352   | simp_not_not t = t
   353 
   354 (* Match untyped terms. *)
   355 fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
   356   | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
   357   | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
   358     (a = b) (* The index is ignored, for some reason. *)
   359   | untyped_aconv (Bound i) (Bound j) = (i = j)
   360   | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
   361   | untyped_aconv (t1 $ t2) (u1 $ u2) =
   362     untyped_aconv t1 u1 andalso untyped_aconv t2 u2
   363   | untyped_aconv _ _ = false
   364 
   365 (* Finding the relative location of an untyped term within a list of terms *)
   366 fun index_of_literal lit haystack =
   367   let
   368     val normalize = simp_not_not o Envir.eta_contract
   369     val match_lit =
   370       HOLogic.dest_Trueprop #> normalize #> untyped_aconv (lit |> normalize)
   371   in case find_index match_lit haystack of ~1 => raise Empty | n => n + 1 end
   372 
   373 (* Permute a rule's premises to move the i-th premise to the last position. *)
   374 fun make_last i th =
   375   let val n = nprems_of th
   376   in  if 1 <= i andalso i <= n
   377       then Thm.permute_prems (i-1) 1 th
   378       else raise THM("select_literal", i, [th])
   379   end;
   380 
   381 val neg_neg_imp = @{lemma "~ ~ Q ==> Q" by blast}
   382 
   383 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
   384    double-negations. *)
   385 fun negate_head thy =
   386   rewrite_rule @{thms atomize_not}
   387   #> perhaps (try (fn th => resolve_inc_tyvars thy th 1 neg_neg_imp))
   388 
   389 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   390 fun select_literal thy = negate_head thy oo make_last
   391 
   392 fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
   393   let
   394     val thy = ProofContext.theory_of ctxt
   395     val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   396     val _ = trace_msg ctxt (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   397     val _ = trace_msg ctxt (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   398   in
   399     (* Trivial cases where one operand is type info *)
   400     if Thm.eq_thm (TrueI, i_th1) then
   401       i_th2
   402     else if Thm.eq_thm (TrueI, i_th2) then
   403       i_th1
   404     else
   405       let
   406         val i_atm =
   407           singleton (hol_terms_from_metis ctxt mode skolem_params)
   408                     (Metis_Term.Fn atm)
   409         val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   410         val prems_th1 = prems_of i_th1
   411         val prems_th2 = prems_of i_th2
   412         val index_th1 =
   413           index_of_literal (s_not i_atm) prems_th1
   414           handle Empty => raise Fail "Failed to find literal in th1"
   415         val _ = trace_msg ctxt (fn () => "  index_th1: " ^ string_of_int index_th1)
   416         val index_th2 =
   417           index_of_literal i_atm prems_th2
   418           handle Empty => raise Fail "Failed to find literal in th2"
   419         val _ = trace_msg ctxt (fn () => "  index_th2: " ^ string_of_int index_th2)
   420     in
   421       resolve_inc_tyvars thy (select_literal thy index_th1 i_th1) index_th2
   422                          i_th2
   423     end
   424   end;
   425 
   426 (* INFERENCE RULE: REFL *)
   427 
   428 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
   429 
   430 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   431 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   432 
   433 fun refl_inf ctxt mode skolem_params t =
   434   let val thy = ProofContext.theory_of ctxt
   435       val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
   436       val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   437       val c_t = cterm_incr_types thy refl_idx i_t
   438   in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   439 
   440 (* INFERENCE RULE: EQUALITY *)
   441 
   442 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   443 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   444 
   445 val metis_eq = Metis_Term.Fn ("=", []);
   446 
   447 fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
   448   | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   449   | get_ty_arg_size _ _ = 0;
   450 
   451 fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
   452   let val thy = ProofContext.theory_of ctxt
   453       val m_tm = Metis_Term.Fn atm
   454       val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
   455       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   456       fun replace_item_list lx 0 (_::ls) = lx::ls
   457         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   458       fun path_finder_FO tm [] = (tm, Bound 0)
   459         | path_finder_FO tm (p::ps) =
   460             let val (tm1,args) = strip_comb tm
   461                 val adjustment = get_ty_arg_size thy tm1
   462                 val p' = if adjustment > p then p else p-adjustment
   463                 val tm_p = List.nth(args,p')
   464                   handle Subscript =>
   465                          error ("Cannot replay Metis proof in Isabelle:\n" ^
   466                                 "equality_inf: " ^ string_of_int p ^ " adj " ^
   467                                 string_of_int adjustment ^ " term " ^
   468                                 Syntax.string_of_term ctxt tm)
   469                 val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^
   470                                       "  " ^ Syntax.string_of_term ctxt tm_p)
   471                 val (r,t) = path_finder_FO tm_p ps
   472             in
   473                 (r, list_comb (tm1, replace_item_list t p' args))
   474             end
   475       fun path_finder_HO tm [] = (tm, Bound 0)
   476         | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
   477         | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
   478         | path_finder_HO tm ps =
   479           raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
   480                       "equality_inf, path_finder_HO: path = " ^
   481                       space_implode " " (map string_of_int ps) ^
   482                       " isa-term: " ^  Syntax.string_of_term ctxt tm)
   483       fun path_finder_FT tm [] _ = (tm, Bound 0)
   484         | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
   485             path_finder_FT tm ps t1
   486         | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
   487             (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
   488         | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
   489             (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
   490         | path_finder_FT tm ps t =
   491           raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
   492                       "equality_inf, path_finder_FT: path = " ^
   493                       space_implode " " (map string_of_int ps) ^
   494                       " isa-term: " ^  Syntax.string_of_term ctxt tm ^
   495                       " fol-term: " ^ Metis_Term.toString t)
   496       fun path_finder FO tm ps _ = path_finder_FO tm ps
   497         | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
   498              (*equality: not curried, as other predicates are*)
   499              if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
   500              else path_finder_HO tm (p::ps)        (*1 selects second operand*)
   501         | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
   502              path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
   503         | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
   504                             (Metis_Term.Fn ("=", [t1,t2])) =
   505              (*equality: not curried, as other predicates are*)
   506              if p=0 then path_finder_FT tm (0::1::ps)
   507                           (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
   508                           (*select first operand*)
   509              else path_finder_FT tm (p::ps)
   510                    (Metis_Term.Fn (".", [metis_eq,t2]))
   511                    (*1 selects second operand*)
   512         | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
   513              (*if not equality, ignore head to skip the hBOOL predicate*)
   514         | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
   515       fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
   516             let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
   517             in (tm, nt $ tm_rslt) end
   518         | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   519       val (tm_subst, body) = path_finder_lit i_atm fp
   520       val tm_abs = Abs ("x", type_of tm_subst, body)
   521       val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   522       val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   523       val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   524       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   525       val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   526       val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   527       val eq_terms = map (pairself (cterm_of thy))
   528         (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   529   in  cterm_instantiate eq_terms subst'  end;
   530 
   531 val factor = Seq.hd o distinct_subgoals_tac;
   532 
   533 fun step ctxt mode skolem_params thpairs p =
   534   case p of
   535     (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
   536   | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
   537   | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   538     factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
   539   | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
   540     factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
   541   | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
   542   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   543     equality_inf ctxt mode skolem_params f_lit f_p f_r
   544 
   545 fun flexflex_first_order th =
   546   case Thm.tpairs_of th of
   547       [] => th
   548     | pairs =>
   549         let val thy = theory_of_thm th
   550             val (_, tenv) =
   551               fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   552             val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
   553             val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
   554         in  th'  end
   555         handle THM _ => th;
   556 
   557 fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
   558 fun is_isabelle_literal_genuine t =
   559   case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
   560 
   561 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   562 
   563 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
   564    disjuncts are impossible. In the Isabelle proof, in spite of efforts to
   565    eliminate them, duplicates sometimes appear with slightly different (but
   566    unifiable) types. *)
   567 fun resynchronize ctxt fol_th th =
   568   let
   569     val num_metis_lits =
   570       count is_metis_literal_genuine
   571             (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
   572     val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
   573   in
   574     if num_metis_lits >= num_isabelle_lits then
   575       th
   576     else
   577       let
   578         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
   579         val prems = prems0 |> distinct (uncurry untyped_aconv)
   580         val goal = Logic.list_implies (prems, concl)
   581       in
   582         if length prems = length prems0 then
   583           error "Cannot replay Metis proof in Isabelle: Out of sync."
   584         else
   585           Goal.prove ctxt [] [] goal (K (cut_rules_tac [th] 1
   586                                          THEN ALLGOALS assume_tac))
   587           |> resynchronize ctxt fol_th
   588       end
   589   end
   590 
   591 fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
   592   if not (null thpairs) andalso prop_of (snd (hd thpairs)) aconv @{prop False} then
   593     (* Isabelle sometimes identifies literals (premises) that are distinct in
   594        Metis (e.g., because of type variables). We give the Isabelle proof the
   595        benefice of the doubt. *)
   596     thpairs
   597   else
   598     let
   599       val _ = trace_msg ctxt
   600                   (fn () => "=============================================")
   601       val _ = trace_msg ctxt
   602                   (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   603       val _ = trace_msg ctxt
   604                   (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   605       val th = step ctxt mode skolem_params thpairs (fol_th, inf)
   606                |> flexflex_first_order
   607                |> resynchronize ctxt fol_th
   608       val _ = trace_msg ctxt
   609                   (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   610       val _ = trace_msg ctxt
   611                   (fn () => "=============================================")
   612     in (fol_th, th) :: thpairs end
   613 
   614 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
   615    one of the premises. Unfortunately, this sometimes yields "Variable
   616    ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
   617    variables before applying "assume_tac". Typical constraints are of the form
   618      ?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,
   619    where the nonvariables are goal parameters. *)
   620 fun unify_first_prem_with_concl thy i th =
   621   let
   622     val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
   623     val prem = goal |> Logic.strip_assums_hyp |> hd
   624     val concl = goal |> Logic.strip_assums_concl
   625     fun pair_untyped_aconv (t1, t2) (u1, u2) =
   626       untyped_aconv t1 u1 andalso untyped_aconv t2 u2
   627     fun add_terms tp inst =
   628       if exists (pair_untyped_aconv tp) inst then inst
   629       else tp :: map (apsnd (subst_atomic [tp])) inst
   630     fun is_flex t =
   631       case strip_comb t of
   632         (Var _, args) => forall is_Bound args
   633       | _ => false
   634     fun unify_flex flex rigid =
   635       case strip_comb flex of
   636         (Var (z as (_, T)), args) =>
   637         add_terms (Var z,
   638           fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
   639       | _ => I
   640     fun unify_potential_flex comb atom =
   641       if is_flex comb then unify_flex comb atom
   642       else if is_Var atom then add_terms (atom, comb)
   643       else I
   644     fun unify_terms (t, u) =
   645       case (t, u) of
   646         (t1 $ t2, u1 $ u2) =>
   647         if is_flex t then unify_flex t u
   648         else if is_flex u then unify_flex u t
   649         else fold unify_terms [(t1, u1), (t2, u2)]
   650       | (_ $ _, _) => unify_potential_flex t u
   651       | (_, _ $ _) => unify_potential_flex u t
   652       | (Var _, _) => add_terms (t, u)
   653       | (_, Var _) => add_terms (u, t)
   654       | _ => I
   655     val t_inst =
   656       [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
   657          |> the_default [] (* FIXME *)
   658   in th |> cterm_instantiate t_inst end
   659 
   660 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
   661 
   662 fun copy_prems_tac [] ns i =
   663     if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
   664   | copy_prems_tac (1 :: ms) ns i =
   665     rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
   666   | copy_prems_tac (m :: ms) ns i =
   667     etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
   668 
   669 (* Metis generates variables of the form _nnn. *)
   670 val is_metis_fresh_variable = String.isPrefix "_"
   671 
   672 fun instantiate_forall_tac thy t i st =
   673   let
   674     val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
   675     fun repair (t as (Var ((s, _), _))) =
   676         (case find_index (fn (s', _) => s' = s) params of
   677            ~1 => t
   678          | j => Bound j)
   679       | repair (t $ u) =
   680         (case (repair t, repair u) of
   681            (t as Bound j, u as Bound k) =>
   682            (* This is a rather subtle trick to repair the discrepancy between
   683               the fully skolemized term that MESON gives us (where existentials
   684               were pulled out) and the reality. *)
   685            if k > j then t else t $ u
   686          | (t, u) => t $ u)
   687       | repair t = t
   688     val t' = t |> repair |> fold (curry absdummy) (map snd params)
   689     fun do_instantiate th =
   690       case Term.add_vars (prop_of th) []
   691            |> filter_out ((Meson_Clausify.is_zapped_var_name orf
   692                            is_metis_fresh_variable) o fst o fst) of
   693         [] => th
   694       | [var as (_, T)] =>
   695         let
   696           val var_binder_Ts = T |> binder_types |> take (length params) |> rev
   697           val var_body_T = T |> funpow (length params) range_type
   698           val tyenv =
   699             Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
   700                                              var_body_T :: var_binder_Ts)
   701           val env =
   702             Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
   703                          tenv = Vartab.empty, tyenv = tyenv}
   704           val ty_inst =
   705             Vartab.fold (fn (x, (S, T)) =>
   706                             cons (pairself (ctyp_of thy) (TVar (x, S), T)))
   707                         tyenv []
   708           val t_inst =
   709             [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
   710         in th |> instantiate (ty_inst, t_inst) end
   711       | _ => raise Fail "expected a single non-zapped, non-Metis Var"
   712   in
   713     (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
   714      THEN PRIMITIVE do_instantiate) st
   715   end
   716 
   717 fun fix_exists_tac t =
   718   etac @{thm exE}
   719   THEN' rename_tac [t |> dest_Var |> fst |> fst]
   720 
   721 fun release_quantifier_tac thy (skolem, t) =
   722   (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
   723 
   724 fun release_clusters_tac _ _ _ [] = K all_tac
   725   | release_clusters_tac thy ax_counts substs
   726                          ((ax_no, cluster_no) :: clusters) =
   727     let
   728       val cluster_of_var =
   729         Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
   730       fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
   731       val cluster_substs =
   732         substs
   733         |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
   734                           if ax_no' = ax_no then
   735                             tsubst |> map (apfst cluster_of_var)
   736                                    |> filter (in_right_cluster o fst)
   737                                    |> map (apfst snd)
   738                                    |> SOME
   739                           else
   740                             NONE)
   741       fun do_cluster_subst cluster_subst =
   742         map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
   743       val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
   744     in
   745       rotate_tac first_prem
   746       THEN' (EVERY' (maps do_cluster_subst cluster_substs))
   747       THEN' rotate_tac (~ first_prem - length cluster_substs)
   748       THEN' release_clusters_tac thy ax_counts substs clusters
   749     end
   750 
   751 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
   752   (ax_no, (cluster_no, (skolem, index_no)))
   753 fun cluster_ord p =
   754   prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
   755            (pairself cluster_key p)
   756 
   757 val tysubst_ord =
   758   list_ord (prod_ord Term_Ord.fast_indexname_ord
   759                      (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
   760 
   761 structure Int_Tysubst_Table =
   762   Table(type key = int * (indexname * (sort * typ)) list
   763         val ord = prod_ord int_ord tysubst_ord)
   764 
   765 structure Int_Pair_Graph =
   766   Graph(type key = int * int val ord = prod_ord int_ord int_ord)
   767 
   768 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
   769 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
   770 
   771 (* Attempts to derive the theorem "False" from a theorem of the form
   772    "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
   773    specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
   774    must be eliminated first. *)
   775 fun discharge_skolem_premises ctxt axioms prems_imp_false =
   776   if prop_of prems_imp_false aconv @{prop False} then
   777     prems_imp_false
   778   else
   779     let
   780       val thy = ProofContext.theory_of ctxt
   781       fun match_term p =
   782         let
   783           val (tyenv, tenv) =
   784             Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
   785           val tsubst =
   786             tenv |> Vartab.dest
   787                  |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
   788                  |> sort (cluster_ord
   789                           o pairself (Meson_Clausify.cluster_of_zapped_var_name
   790                                       o fst o fst))
   791                  |> map (Meson.term_pair_of
   792                          #> pairself (Envir.subst_term_types tyenv))
   793           val tysubst = tyenv |> Vartab.dest
   794         in (tysubst, tsubst) end
   795       fun subst_info_for_prem subgoal_no prem =
   796         case prem of
   797           _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
   798           let val ax_no = HOLogic.dest_nat num in
   799             (ax_no, (subgoal_no,
   800                      match_term (nth axioms ax_no |> the |> snd, t)))
   801           end
   802         | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
   803                            [prem])
   804       fun cluster_of_var_name skolem s =
   805         case try Meson_Clausify.cluster_of_zapped_var_name s of
   806           NONE => NONE
   807         | SOME ((ax_no, (cluster_no, _)), skolem') =>
   808           if skolem' = skolem andalso cluster_no > 0 then
   809             SOME (ax_no, cluster_no)
   810           else
   811             NONE
   812       fun clusters_in_term skolem t =
   813         Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
   814       fun deps_for_term_subst (var, t) =
   815         case clusters_in_term false var of
   816           [] => NONE
   817         | [(ax_no, cluster_no)] =>
   818           SOME ((ax_no, cluster_no),
   819                 clusters_in_term true t
   820                 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
   821         | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
   822       val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
   823       val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
   824                          |> sort (int_ord o pairself fst)
   825       val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
   826       val clusters = maps (op ::) depss
   827       val ordered_clusters =
   828         Int_Pair_Graph.empty
   829         |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
   830         |> fold Int_Pair_Graph.add_deps_acyclic depss
   831         |> Int_Pair_Graph.topological_order
   832         handle Int_Pair_Graph.CYCLES _ =>
   833                error "Cannot replay Metis proof in Isabelle without \
   834                      \\"Hilbert_Choice\"."
   835       val ax_counts =
   836         Int_Tysubst_Table.empty
   837         |> fold (fn (ax_no, (_, (tysubst, _))) =>
   838                     Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
   839                                                   (Integer.add 1)) substs
   840         |> Int_Tysubst_Table.dest
   841       val needed_axiom_props =
   842         0 upto length axioms - 1 ~~ axioms
   843         |> map_filter (fn (_, NONE) => NONE
   844                         | (ax_no, SOME (_, t)) =>
   845                           if exists (fn ((ax_no', _), n) =>
   846                                         ax_no' = ax_no andalso n > 0)
   847                                     ax_counts then
   848                             SOME t
   849                           else
   850                             NONE)
   851       val outer_param_names =
   852         [] |> fold Term.add_var_names needed_axiom_props
   853            |> filter (Meson_Clausify.is_zapped_var_name o fst)
   854            |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
   855            |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
   856                          cluster_no = 0 andalso skolem)
   857            |> sort shuffle_ord |> map (fst o snd)
   858 (* for debugging only:
   859       fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
   860         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
   861         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
   862         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
   863                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
   864       val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
   865       val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
   866       val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
   867       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
   868                        cat_lines (map string_for_subst_info substs))
   869 *)
   870       fun cut_and_ex_tac axiom =
   871         cut_rules_tac [axiom] 1
   872         THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
   873       fun rotation_for_subgoal i =
   874         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
   875     in
   876       Goal.prove ctxt [] [] @{prop False}
   877           (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
   878                                   o fst) ax_counts)
   879                       THEN rename_tac outer_param_names 1
   880                       THEN copy_prems_tac (map snd ax_counts) [] 1)
   881               THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
   882               THEN match_tac [prems_imp_false] 1
   883               THEN ALLGOALS (fn i =>
   884                        rtac @{thm Meson.skolem_COMBK_I} i
   885                        THEN rotate_tac (rotation_for_subgoal i) i
   886                        THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   887                        THEN assume_tac i
   888                        THEN flexflex_tac)))
   889       handle ERROR _ =>
   890              error ("Cannot replay Metis proof in Isabelle:\n\
   891                     \Error when discharging Skolem assumptions.")
   892     end
   893 
   894 val setup = trace_setup #> verbose_setup
   895 
   896 end;