src/HOL/Tools/Metis/metis_reconstruct.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 58963 26bf09b95dda
permissions -rw-r--r--
proper context for match_tac etc.;
     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 type_enc = ATP_Problem_Generate.type_enc
    13 
    14   exception METIS_RECONSTRUCT of string * string
    15 
    16   val hol_clause_of_metis : Proof.context -> type_enc -> int Symtab.table ->
    17     (string * term) list * (string * term) list -> Metis_Thm.thm -> term
    18   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    19   val replay_one_inference : Proof.context -> type_enc ->
    20     (string * term) list * (string * term) list -> int Symtab.table ->
    21     Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list ->
    22     (Metis_Thm.thm * thm) list
    23   val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm
    24 end;
    25 
    26 structure Metis_Reconstruct : METIS_RECONSTRUCT =
    27 struct
    28 
    29 open ATP_Problem
    30 open ATP_Problem_Generate
    31 open ATP_Proof_Reconstruct
    32 open Metis_Generate
    33 
    34 exception METIS_RECONSTRUCT of string * string
    35 
    36 val meta_not_not = @{thms not_not[THEN eq_reflection]}
    37 
    38 fun atp_name_of_metis type_enc s =
    39   (case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
    40     SOME ((s, _), (_, swap)) => (s, swap)
    41   | _ => (s, false))
    42 
    43 fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
    44     let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
    45       ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
    46     end
    47   | atp_term_of_metis _ (Metis_Term.Var s) =
    48     ATerm ((Metis_Name.toString s, []), [])
    49 
    50 fun hol_term_of_metis ctxt type_enc sym_tab =
    51   atp_term_of_metis type_enc #> term_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab NONE
    52 
    53 fun atp_literal_of_metis type_enc (pos, atom) =
    54   atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
    55        |> AAtom |> not pos ? mk_anot
    56 
    57 fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
    58   | atp_clause_of_metis type_enc lits =
    59     lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
    60 
    61 fun polish_hol_terms ctxt (lifted, old_skolems) =
    62   map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
    63   #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    64 
    65 fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
    66   Metis_Thm.clause
    67   #> Metis_LiteralSet.toList
    68   #> atp_clause_of_metis type_enc
    69   #> prop_of_atp ctxt ATP_Problem.CNF type_enc false sym_tab
    70   #> singleton (polish_hol_terms ctxt concealed)
    71 
    72 fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
    73   let
    74     val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
    75     val _ = trace_msg ctxt (fn () => "  calling type inference:")
    76     val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts
    77     val ts' = ts |> polish_hol_terms ctxt concealed
    78     val _ = app (fn t => trace_msg ctxt
    79                   (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    80                             " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts'
    81   in ts' end
    82 
    83 (* ------------------------------------------------------------------------- *)
    84 (* FOL step Inference Rules                                                  *)
    85 (* ------------------------------------------------------------------------- *)
    86 
    87 fun lookth th_pairs fth =
    88   the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
    89   handle Option.Option => raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
    90 
    91 fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx))
    92 
    93 (* INFERENCE RULE: AXIOM *)
    94 
    95 (* This causes variables to have an index of 1 by default. See also
    96    "term_of_atp" in "ATP_Proof_Reconstruct". *)
    97 val axiom_inference = Thm.incr_indexes 1 oo lookth
    98 
    99 (* INFERENCE RULE: ASSUME *)
   100 
   101 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
   102 
   103 fun inst_excluded_middle thy i_atom =
   104   let
   105     val th = EXCLUDED_MIDDLE
   106     val [vx] = Term.add_vars (prop_of th) []
   107     val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
   108   in
   109     cterm_instantiate substs th
   110   end
   111 
   112 fun assume_inference ctxt type_enc concealed sym_tab atom =
   113   inst_excluded_middle (Proof_Context.theory_of ctxt)
   114     (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
   115 
   116 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
   117    to reconstruct them admits new possibilities of errors, e.g. concerning
   118    sorts. Instead we try to arrange that new TVars are distinct and that types
   119    can be inferred from terms. *)
   120 
   121 fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
   122   let
   123     val thy = Proof_Context.theory_of ctxt
   124     val i_th = lookth th_pairs th
   125     val i_th_vars = Term.add_vars (prop_of i_th) []
   126 
   127     fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   128     fun subst_translation (x,y) =
   129       let
   130         val v = find_var x
   131         (* We call "polish_hol_terms" below. *)
   132         val t = hol_term_of_metis ctxt type_enc sym_tab y
   133       in
   134         SOME (cterm_of thy (Var v), t)
   135       end
   136       handle Option.Option =>
   137              (trace_msg ctxt (fn () =>
   138                 "\"find_var\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
   139               NONE)
   140            | TYPE _ =>
   141              (trace_msg ctxt (fn () =>
   142                 "\"hol_term_of_metis\" failed for " ^ x ^ " in " ^ Display.string_of_thm ctxt i_th);
   143               NONE)
   144     fun remove_typeinst (a, t) =
   145       let val a = Metis_Name.toString a in
   146         (case unprefix_and_unascii schematic_var_prefix a of
   147           SOME b => SOME (b, t)
   148         | NONE =>
   149           (case unprefix_and_unascii tvar_prefix a of
   150             SOME _ => NONE (* type instantiations are forbidden *)
   151           | NONE => SOME (a, t) (* internal Metis var? *)))
   152       end
   153     val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   154     val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   155     val (vars, tms) =
   156       ListPair.unzip (map_filter subst_translation substs)
   157       ||> polish_hol_terms ctxt concealed
   158     val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   159     val substs' = ListPair.zip (vars, map ctm_of tms)
   160     val _ = trace_msg ctxt (fn () =>
   161       cat_lines ("subst_translations:" ::
   162         (substs' |> map (fn (x, y) =>
   163           Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   164           Syntax.string_of_term ctxt (term_of y)))))
   165   in
   166     cterm_instantiate substs' i_th
   167   end
   168   handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg)
   169        | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg)
   170 
   171 (* INFERENCE RULE: RESOLVE *)
   172 
   173 (*Increment the indexes of only the type variables*)
   174 fun incr_type_indexes inc th =
   175   let
   176     val tvs = Term.add_tvars (Thm.full_prop_of th) []
   177     val thy = Thm.theory_of_thm th
   178     fun inc_tvar ((a, i), s) = pairself (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
   179   in
   180     Thm.instantiate (map inc_tvar tvs, []) th
   181   end
   182 
   183 (* Like RSN, but we rename apart only the type variables. Vars here typically
   184    have an index of 1, and the use of RSN would increase this typically to 3.
   185    Instantiations of those Vars could then fail. *)
   186 fun resolve_inc_tyvars ctxt tha i thb =
   187   let
   188     val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
   189     fun res (tha, thb) =
   190       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
   191             (false, tha, nprems_of tha) i thb
   192            |> Seq.list_of |> distinct Thm.eq_thm of
   193         [th] => th
   194       | _ =>
   195         let
   196           val thaa'bb' as [(tha', _), (thb', _)] =
   197             map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb]
   198         in
   199           if forall Thm.eq_thm_prop thaa'bb' then
   200             raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb])
   201           else
   202             res (tha', thb')
   203         end)
   204   in
   205     res (tha, thb)
   206     handle TERM z =>
   207       let
   208         val thy = Proof_Context.theory_of ctxt
   209         val ps = []
   210           |> fold (Term.add_vars o prop_of) [tha, thb]
   211           |> AList.group (op =)
   212           |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
   213           |> rpair (Envir.empty ~1)
   214           |-> fold (Pattern.unify (Context.Proof ctxt))
   215           |> Envir.type_env |> Vartab.dest
   216           |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T))
   217       in
   218         (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
   219            "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
   220            first argument). We then perform unification of the types of variables by hand and try
   221            again. We could do this the first time around but this error occurs seldom and we don't
   222            want to break existing proofs in subtle ways or slow them down. *)
   223         if null ps then raise TERM z
   224         else res (pairself (Drule.instantiate_normalize (ps, [])) (tha, thb))
   225       end
   226   end
   227 
   228 fun s_not (@{const Not} $ t) = t
   229   | s_not t = HOLogic.mk_not t
   230 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
   231   | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   232   | simp_not_not t = t
   233 
   234 val normalize_literal = simp_not_not o Envir.eta_contract
   235 
   236 (* Find the relative location of an untyped term within a list of terms as a
   237    1-based index. Returns 0 in case of failure. *)
   238 fun index_of_literal lit haystack =
   239   let
   240     fun match_lit normalize =
   241       HOLogic.dest_Trueprop #> normalize
   242       #> curry Term.aconv_untyped (lit |> normalize)
   243   in
   244     (case find_index (match_lit I) haystack of
   245        ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
   246      | j => j) + 1
   247   end
   248 
   249 (* Permute a rule's premises to move the i-th premise to the last position. *)
   250 fun make_last i th =
   251   let val n = nprems_of th in
   252     if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th
   253     else raise THM ("select_literal", i, [th])
   254   end
   255 
   256 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
   257    to create double negations. The "select" wrapper is a trick to ensure that
   258    "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
   259    don't use this trick in general because it makes the proof object uglier than
   260    necessary. FIXME. *)
   261 fun negate_head ctxt th =
   262   if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
   263     (th RS @{thm select_FalseI})
   264     |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select}
   265   else
   266     th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
   267 
   268 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   269 fun select_literal ctxt = negate_head ctxt oo make_last
   270 
   271 fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
   272   let
   273     val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
   274     val _ = trace_msg ctxt (fn () =>
   275         "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
   276         \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   277   in
   278     (* Trivial cases where one operand is type info *)
   279     if Thm.eq_thm (TrueI, i_th1) then
   280       i_th2
   281     else if Thm.eq_thm (TrueI, i_th2) then
   282       i_th1
   283     else
   284       let
   285         val i_atom =
   286           singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
   287         val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atom)
   288       in
   289         (case index_of_literal (s_not i_atom) (prems_of i_th1) of
   290           0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1)
   291         | j1 =>
   292           (trace_msg ctxt (fn () => "  index th1: " ^ string_of_int j1);
   293            (case index_of_literal i_atom (prems_of i_th2) of
   294              0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2)
   295            | j2 =>
   296              (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
   297               resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2
   298               handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s)))))
   299       end
   300   end
   301 
   302 (* INFERENCE RULE: REFL *)
   303 
   304 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
   305 
   306 val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   307 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   308 
   309 fun refl_inference ctxt type_enc concealed sym_tab t =
   310   let
   311     val thy = Proof_Context.theory_of ctxt
   312     val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
   313     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   314     val c_t = cterm_incr_types thy refl_idx i_t
   315   in cterm_instantiate [(refl_x, c_t)] REFL_THM end
   316 
   317 (* INFERENCE RULE: EQUALITY *)
   318 
   319 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   320 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   321 
   322 fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
   323   let val thy = Proof_Context.theory_of ctxt
   324       val m_tm = Metis_Term.Fn atom
   325       val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
   326       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   327       fun replace_item_list lx 0 (_::ls) = lx::ls
   328         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   329       fun path_finder_fail tm ps t =
   330         raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
   331                   "path = " ^ space_implode " " (map string_of_int ps) ^
   332                   " isa-term: " ^ Syntax.string_of_term ctxt tm ^
   333                   (case t of
   334                     SOME t => " fol-term: " ^ Metis_Term.toString t
   335                   | NONE => ""))
   336       fun path_finder tm [] _ = (tm, Bound 0)
   337         | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
   338           let
   339             val s = s |> Metis_Name.toString
   340                       |> perhaps (try (unprefix_and_unascii const_prefix
   341                                        #> the #> unmangled_const_name #> hd))
   342           in
   343             if s = metis_predicator orelse s = predicator_name orelse
   344                s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
   345                orelse s = type_tag_name then
   346               path_finder tm ps (nth ts p)
   347             else if s = metis_app_op orelse s = app_op_name then
   348               let
   349                 val (tm1, tm2) = dest_comb tm
   350                 val p' = p - (length ts - 2)
   351               in
   352                 if p' = 0 then path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
   353                 else path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
   354               end
   355             else
   356               let
   357                 val (tm1, args) = strip_comb tm
   358                 val adjustment = length ts - length args
   359                 val p' = if adjustment > p then p else p - adjustment
   360                 val tm_p = nth args p'
   361                   handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
   362                 val _ = trace_msg ctxt (fn () =>
   363                     "path_finder: " ^ string_of_int p ^ "  " ^
   364                     Syntax.string_of_term ctxt tm_p)
   365                 val (r, t) = path_finder tm_p ps (nth ts p)
   366               in (r, list_comb (tm1, replace_item_list t p' args)) end
   367           end
   368         | path_finder tm ps t = path_finder_fail tm ps (SOME t)
   369       val (tm_subst, body) = path_finder i_atom fp m_tm
   370       val tm_abs = Abs ("x", type_of tm_subst, body)
   371       val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   372       val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   373       val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   374       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
   375       val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   376       val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   377       val eq_terms = map (pairself (cterm_of thy))
   378         (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   379   in
   380     cterm_instantiate eq_terms subst'
   381   end
   382 
   383 val factor = Seq.hd o distinct_subgoals_tac
   384 
   385 fun one_step ctxt type_enc concealed sym_tab th_pairs p =
   386   (case p of
   387     (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
   388   | (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom
   389   | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   390     inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor
   391   | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
   392     resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor
   393   | (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm
   394   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   395     equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
   396 
   397 fun flexflex_first_order th =
   398   (case Thm.tpairs_of th of
   399     [] => th
   400   | pairs =>
   401     let
   402       val thy = theory_of_thm th
   403       val cert = cterm_of thy
   404       val certT = ctyp_of thy
   405       val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   406 
   407       fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
   408       fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
   409 
   410       val instsT = Vartab.fold (cons o mkT) tyenv []
   411       val insts = Vartab.fold (cons o mk) tenv []
   412     in
   413       Thm.instantiate (instsT, insts) th
   414     end
   415     handle THM _ => th)
   416 
   417 fun is_metis_literal_genuine (_, (s, _)) =
   418   not (String.isPrefix class_prefix (Metis_Name.toString s))
   419 fun is_isabelle_literal_genuine t =
   420   (case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true)
   421 
   422 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   423 
   424 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
   425    disjuncts are impossible. In the Isabelle proof, in spite of efforts to
   426    eliminate them, duplicates sometimes appear with slightly different (but
   427    unifiable) types. *)
   428 fun resynchronize ctxt fol_th th =
   429   let
   430     val num_metis_lits =
   431       count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
   432     val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
   433   in
   434     if num_metis_lits >= num_isabelle_lits then
   435       th
   436     else
   437       let
   438         val (prems0, concl) = th |> prop_of |> Logic.strip_horn
   439         val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
   440         val goal = Logic.list_implies (prems, concl)
   441         val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
   442         val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS assume_tac
   443       in
   444         if length prems = length prems0 then
   445           raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
   446         else
   447           Goal.prove ctxt' [] [] goal (K tac)
   448           |> resynchronize ctxt' fol_th
   449       end
   450   end
   451 
   452 fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
   453                          th_pairs =
   454   if not (null th_pairs) andalso prop_of (snd (hd th_pairs)) aconv @{prop False} then
   455     (* Isabelle sometimes identifies literals (premises) that are distinct in
   456        Metis (e.g., because of type variables). We give the Isabelle proof the
   457        benefice of the doubt. *)
   458     th_pairs
   459   else
   460     let
   461       val _ = trace_msg ctxt (fn () => "=============================================")
   462       val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   463       val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   464       val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
   465         |> flexflex_first_order
   466         |> resynchronize ctxt fol_th
   467       val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   468       val _ = trace_msg ctxt (fn () => "=============================================")
   469     in
   470       (fol_th, th) :: th_pairs
   471     end
   472 
   473 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
   474    one of the premises. Unfortunately, this sometimes yields "Variable
   475    has two distinct types" errors. To avoid this, we instantiate the
   476    variables before applying "assume_tac". Typical constraints are of the form
   477      ?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,
   478    where the nonvariables are goal parameters. *)
   479 fun unify_first_prem_with_concl thy i th =
   480   let
   481     val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
   482     val prem = goal |> Logic.strip_assums_hyp |> hd
   483     val concl = goal |> Logic.strip_assums_concl
   484 
   485     fun pair_untyped_aconv (t1, t2) (u1, u2) =
   486       Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
   487 
   488     fun add_terms tp inst =
   489       if exists (pair_untyped_aconv tp) inst then inst
   490       else tp :: map (apsnd (subst_atomic [tp])) inst
   491 
   492     fun is_flex t =
   493       (case strip_comb t of
   494         (Var _, args) => forall is_Bound args
   495       | _ => false)
   496 
   497     fun unify_flex flex rigid =
   498       (case strip_comb flex of
   499         (Var (z as (_, T)), args) =>
   500         add_terms (Var z,
   501           fold_rev absdummy (take (length args) (binder_types T)) rigid)
   502       | _ => I)
   503 
   504     fun unify_potential_flex comb atom =
   505       if is_flex comb then unify_flex comb atom
   506       else if is_Var atom then add_terms (atom, comb)
   507       else I
   508 
   509     fun unify_terms (t, u) =
   510       (case (t, u) of
   511         (t1 $ t2, u1 $ u2) =>
   512         if is_flex t then unify_flex t u
   513         else if is_flex u then unify_flex u t
   514         else fold unify_terms [(t1, u1), (t2, u2)]
   515       | (_ $ _, _) => unify_potential_flex t u
   516       | (_, _ $ _) => unify_potential_flex u t
   517       | (Var _, _) => add_terms (t, u)
   518       | (_, Var _) => add_terms (u, t)
   519       | _ => I)
   520 
   521     val t_inst =
   522       [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
   523          |> the_default [] (* FIXME *)
   524   in
   525     cterm_instantiate t_inst th
   526   end
   527 
   528 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
   529 
   530 fun copy_prems_tac [] ns i =
   531     if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
   532   | copy_prems_tac (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
   533   | copy_prems_tac (m :: ms) ns i =
   534     eresolve_tac [copy_prem] i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
   535 
   536 (* Metis generates variables of the form _nnn. *)
   537 val is_metis_fresh_variable = String.isPrefix "_"
   538 
   539 fun instantiate_forall_tac thy t i st =
   540   let
   541     val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
   542 
   543     fun repair (t as (Var ((s, _), _))) =
   544         (case find_index (fn (s', _) => s' = s) params of
   545           ~1 => t
   546         | j => Bound j)
   547       | repair (t $ u) =
   548         (case (repair t, repair u) of
   549           (t as Bound j, u as Bound k) =>
   550           (* This is a trick to repair the discrepancy between the fully skolemized term that MESON
   551              gives us (where existentials were pulled out) and the reality. *)
   552           if k > j then t else t $ u
   553         | (t, u) => t $ u)
   554       | repair t = t
   555 
   556     val t' = t |> repair |> fold (absdummy o snd) params
   557 
   558     fun do_instantiate th =
   559       (case Term.add_vars (prop_of th) []
   560             |> filter_out ((Meson_Clausify.is_zapped_var_name orf is_metis_fresh_variable) o fst
   561               o fst) of
   562         [] => th
   563       | [var as (_, T)] =>
   564         let
   565           val var_binder_Ts = T |> binder_types |> take (length params) |> rev
   566           val var_body_T = T |> funpow (length params) range_type
   567           val tyenv =
   568             Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
   569                                              var_body_T :: var_binder_Ts)
   570           val env =
   571             Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
   572               tenv = Vartab.empty, tyenv = tyenv}
   573           val ty_inst =
   574             Vartab.fold (fn (x, (S, T)) => cons (pairself (ctyp_of thy) (TVar (x, S), T))) tyenv []
   575           val t_inst = [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
   576         in
   577           Drule.instantiate_normalize (ty_inst, t_inst) th
   578         end
   579       | _ => raise Fail "expected a single non-zapped, non-Metis Var")
   580   in
   581     (DETERM (eresolve_tac @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
   582   end
   583 
   584 fun fix_exists_tac t = eresolve_tac [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
   585 
   586 fun release_quantifier_tac thy (skolem, t) =
   587   (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
   588 
   589 fun release_clusters_tac _ _ _ [] = K all_tac
   590   | release_clusters_tac thy ax_counts substs ((ax_no, cluster_no) :: clusters) =
   591     let
   592       val cluster_of_var = Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
   593       fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
   594       val cluster_substs =
   595         substs
   596         |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
   597                           if ax_no' = ax_no then
   598                             tsubst |> map (apfst cluster_of_var)
   599                                    |> filter (in_right_cluster o fst)
   600                                    |> map (apfst snd)
   601                                    |> SOME
   602                           else
   603                             NONE)
   604       fun do_cluster_subst cluster_subst =
   605         map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
   606       val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
   607     in
   608       rotate_tac first_prem
   609       THEN' (EVERY' (maps do_cluster_subst cluster_substs))
   610       THEN' rotate_tac (~ first_prem - length cluster_substs)
   611       THEN' release_clusters_tac thy ax_counts substs clusters
   612     end
   613 
   614 fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
   615   (ax_no, (cluster_no, (skolem, index_no)))
   616 fun cluster_ord p =
   617   prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (pairself cluster_key p)
   618 
   619 val tysubst_ord =
   620   list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
   621 
   622 structure Int_Tysubst_Table =
   623   Table(type key = int * (indexname * (sort * typ)) list
   624         val ord = prod_ord int_ord tysubst_ord)
   625 
   626 structure Int_Pair_Graph =
   627   Graph(type key = int * int val ord = prod_ord int_ord int_ord)
   628 
   629 fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
   630 fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
   631 
   632 (* Attempts to derive the theorem "False" from a theorem of the form
   633    "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
   634    specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
   635    must be eliminated first. *)
   636 fun discharge_skolem_premises ctxt axioms prems_imp_false =
   637   if prop_of prems_imp_false aconv @{prop False} then
   638     prems_imp_false
   639   else
   640     let
   641       val thy = Proof_Context.theory_of ctxt
   642 
   643       fun match_term p =
   644         let
   645           val (tyenv, tenv) =
   646             Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
   647           val tsubst =
   648             tenv |> Vartab.dest
   649                  |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
   650                  |> sort (cluster_ord
   651                           o pairself (Meson_Clausify.cluster_of_zapped_var_name
   652                                       o fst o fst))
   653                  |> map (Meson.term_pair_of
   654                          #> pairself (Envir.subst_term_types tyenv))
   655           val tysubst = tyenv |> Vartab.dest
   656         in (tysubst, tsubst) end
   657 
   658       fun subst_info_of_prem subgoal_no prem =
   659         (case prem of
   660           _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
   661           let val ax_no = HOLogic.dest_nat num in
   662             (ax_no, (subgoal_no,
   663                      match_term (nth axioms ax_no |> the |> snd, t)))
   664           end
   665         | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
   666 
   667       fun cluster_of_var_name skolem s =
   668         (case try Meson_Clausify.cluster_of_zapped_var_name s of
   669           NONE => NONE
   670         | SOME ((ax_no, (cluster_no, _)), skolem') =>
   671           if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE)
   672 
   673       fun clusters_in_term skolem t =
   674         Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
   675 
   676       fun deps_of_term_subst (var, t) =
   677         (case clusters_in_term false var of
   678           [] => NONE
   679         | [(ax_no, cluster_no)] =>
   680           SOME ((ax_no, cluster_no),
   681             clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
   682         | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]))
   683 
   684       val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
   685       val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
   686                          |> sort (int_ord o pairself fst)
   687       val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
   688       val clusters = maps (op ::) depss
   689       val ordered_clusters =
   690         Int_Pair_Graph.empty
   691         |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
   692         |> fold Int_Pair_Graph.add_deps_acyclic depss
   693         |> Int_Pair_Graph.topological_order
   694         handle Int_Pair_Graph.CYCLES _ =>
   695                error "Cannot replay Metis proof in Isabelle without \"Hilbert_Choice\""
   696       val ax_counts =
   697         Int_Tysubst_Table.empty
   698         |> fold (fn (ax_no, (_, (tysubst, _))) =>
   699                     Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
   700                                                   (Integer.add 1)) substs
   701         |> Int_Tysubst_Table.dest
   702       val needed_axiom_props =
   703         0 upto length axioms - 1 ~~ axioms
   704         |> map_filter (fn (_, NONE) => NONE
   705                         | (ax_no, SOME (_, t)) =>
   706                           if exists (fn ((ax_no', _), n) =>
   707                                         ax_no' = ax_no andalso n > 0)
   708                                     ax_counts then
   709                             SOME t
   710                           else
   711                             NONE)
   712       val outer_param_names =
   713         [] |> fold Term.add_var_names needed_axiom_props
   714            |> filter (Meson_Clausify.is_zapped_var_name o fst)
   715            |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
   716            |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
   717                          cluster_no = 0 andalso skolem)
   718            |> sort shuffle_ord |> map (fst o snd)
   719 
   720 (* for debugging only:
   721       fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
   722         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
   723         "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
   724         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
   725                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
   726       val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters)
   727       val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
   728       val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
   729       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
   730                        cat_lines (map string_of_subst_info substs))
   731 *)
   732 
   733       fun cut_and_ex_tac axiom =
   734         cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac @{thms exE}) 1)
   735       fun rotation_of_subgoal i =
   736         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
   737 
   738       val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
   739     in
   740       Goal.prove ctxt' [] [] @{prop False}
   741         (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts)
   742               THEN rename_tac outer_param_names 1
   743               THEN copy_prems_tac (map snd ax_counts) [] 1)
   744             THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
   745             THEN match_tac ctxt' [prems_imp_false] 1
   746             THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
   747               THEN rotate_tac (rotation_of_subgoal i) i
   748               THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   749               THEN assume_tac i
   750               THEN flexflex_tac ctxt')))
   751       handle ERROR msg =>
   752         cat_error msg
   753           "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"
   754     end
   755 
   756 end;