src/HOL/Tools/Metis/metis_reconstruct.ML
author wenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 60781 2da59cdf531c
parent 60642 48dd1cefb4ae
child 60794 f21f70d24844
permissions -rw-r--r--
updated to infer_instantiate;
tuned;
     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 ctxt idx =
    92   Thm.cterm_of ctxt o map_types (Logic.incr_tvar idx)
    93 
    94 (* INFERENCE RULE: AXIOM *)
    95 
    96 (* This causes variables to have an index of 1 by default. See also
    97    "term_of_atp" in "ATP_Proof_Reconstruct". *)
    98 val axiom_inference = Thm.incr_indexes 1 oo lookth
    99 
   100 (* INFERENCE RULE: ASSUME *)
   101 
   102 val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
   103 
   104 fun inst_excluded_middle ctxt i_atom =
   105   let
   106     val th = EXCLUDED_MIDDLE
   107     val [vx] = Term.add_vars (Thm.prop_of th) []
   108     val substs = [(Thm.cterm_of ctxt (Var vx), Thm.cterm_of ctxt i_atom)]
   109   in
   110     cterm_instantiate substs th
   111   end
   112 
   113 fun assume_inference ctxt type_enc concealed sym_tab atom =
   114   inst_excluded_middle ctxt
   115     (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
   116 
   117 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
   118    to reconstruct them admits new possibilities of errors, e.g. concerning
   119    sorts. Instead we try to arrange that new TVars are distinct and that types
   120    can be inferred from terms. *)
   121 
   122 fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
   123   let
   124     val i_th = lookth th_pairs th
   125     val i_th_vars = Term.add_vars (Thm.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 (Thm.cterm_of ctxt (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 ctxt (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 (Thm.term_of x) ^ " |-> " ^
   164           Syntax.string_of_term ctxt (Thm.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 ctxt inc th =
   175   let
   176     val tvs = Term.add_tvars (Thm.full_prop_of th) []
   177     fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s)))
   178   in
   179     Thm.instantiate (map inc_tvar tvs, []) th
   180   end
   181 
   182 (* Like RSN, but we rename apart only the type variables. Vars here typically
   183    have an index of 1, and the use of RSN would increase this typically to 3.
   184    Instantiations of those Vars could then fail. *)
   185 fun resolve_inc_tyvars ctxt tha i thb =
   186   let
   187     val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
   188     fun res (tha, thb) =
   189       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
   190             (false, tha, Thm.nprems_of tha) i thb
   191            |> Seq.list_of |> distinct Thm.eq_thm of
   192         [th] => th
   193       | _ =>
   194         let
   195           val thaa'bb' as [(tha', _), (thb', _)] =
   196             map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb]
   197         in
   198           if forall Thm.eq_thm_prop thaa'bb' then
   199             raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb])
   200           else
   201             res (tha', thb')
   202         end)
   203   in
   204     res (tha, thb)
   205     handle TERM z =>
   206       let
   207         val ps = []
   208           |> fold (Term.add_vars o Thm.prop_of) [tha, thb]
   209           |> AList.group (op =)
   210           |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
   211           |> rpair (Envir.empty ~1)
   212           |-> fold (Pattern.unify (Context.Proof ctxt))
   213           |> Envir.type_env |> Vartab.dest
   214           |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T))
   215       in
   216         (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
   217            "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
   218            first argument). We then perform unification of the types of variables by hand and try
   219            again. We could do this the first time around but this error occurs seldom and we don't
   220            want to break existing proofs in subtle ways or slow them down. *)
   221         if null ps then raise TERM z
   222         else res (apply2 (Drule.instantiate_normalize (ps, [])) (tha, thb))
   223       end
   224   end
   225 
   226 fun s_not (@{const Not} $ t) = t
   227   | s_not t = HOLogic.mk_not t
   228 fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
   229   | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
   230   | simp_not_not t = t
   231 
   232 val normalize_literal = simp_not_not o Envir.eta_contract
   233 
   234 (* Find the relative location of an untyped term within a list of terms as a
   235    1-based index. Returns 0 in case of failure. *)
   236 fun index_of_literal lit haystack =
   237   let
   238     fun match_lit normalize =
   239       HOLogic.dest_Trueprop #> normalize
   240       #> curry Term.aconv_untyped (lit |> normalize)
   241   in
   242     (case find_index (match_lit I) haystack of
   243        ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
   244      | j => j) + 1
   245   end
   246 
   247 (* Permute a rule's premises to move the i-th premise to the last position. *)
   248 fun make_last i th =
   249   let val n = Thm.nprems_of th in
   250     if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th
   251     else raise THM ("select_literal", i, [th])
   252   end
   253 
   254 (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
   255    to create double negations. The "select" wrapper is a trick to ensure that
   256    "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
   257    don't use this trick in general because it makes the proof object uglier than
   258    necessary. FIXME. *)
   259 fun negate_head ctxt th =
   260   if exists (fn t => t aconv @{prop "~ False"}) (Thm.prems_of th) then
   261     (th RS @{thm select_FalseI})
   262     |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select}
   263   else
   264     th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
   265 
   266 (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   267 fun select_literal ctxt = negate_head ctxt oo make_last
   268 
   269 fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
   270   let
   271     val (i_th1, i_th2) = apply2 (lookth th_pairs) (th1, th2)
   272     val _ = trace_msg ctxt (fn () =>
   273         "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
   274         \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   275   in
   276     (* Trivial cases where one operand is type info *)
   277     if Thm.eq_thm (TrueI, i_th1) then
   278       i_th2
   279     else if Thm.eq_thm (TrueI, i_th2) then
   280       i_th1
   281     else
   282       let
   283         val i_atom =
   284           singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
   285         val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atom)
   286       in
   287         (case index_of_literal (s_not i_atom) (Thm.prems_of i_th1) of
   288           0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1)
   289         | j1 =>
   290           (trace_msg ctxt (fn () => "  index th1: " ^ string_of_int j1);
   291            (case index_of_literal i_atom (Thm.prems_of i_th2) of
   292              0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2)
   293            | j2 =>
   294              (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
   295               resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2
   296               handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s)))))
   297       end
   298   end
   299 
   300 (* INFERENCE RULE: REFL *)
   301 
   302 val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
   303 
   304 val refl_x = Thm.cterm_of @{context} (Var (hd (Term.add_vars (Thm.prop_of REFL_THM) [])));
   305 val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   306 
   307 fun refl_inference ctxt type_enc concealed sym_tab t =
   308   let
   309     val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
   310     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   311     val c_t = cterm_incr_types ctxt refl_idx i_t
   312   in cterm_instantiate [(refl_x, c_t)] REFL_THM end
   313 
   314 (* INFERENCE RULE: EQUALITY *)
   315 
   316 val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   317 val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   318 
   319 fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
   320   let val thy = Proof_Context.theory_of ctxt
   321       val m_tm = Metis_Term.Fn atom
   322       val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
   323       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   324       fun replace_item_list lx 0 (_::ls) = lx::ls
   325         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   326       fun path_finder_fail tm ps t =
   327         raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
   328                   "path = " ^ space_implode " " (map string_of_int ps) ^
   329                   " isa-term: " ^ Syntax.string_of_term ctxt tm ^
   330                   (case t of
   331                     SOME t => " fol-term: " ^ Metis_Term.toString t
   332                   | NONE => ""))
   333       fun path_finder tm [] _ = (tm, Bound 0)
   334         | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
   335           let
   336             val s = s |> Metis_Name.toString
   337                       |> perhaps (try (unprefix_and_unascii const_prefix
   338                                        #> the #> unmangled_const_name #> hd))
   339           in
   340             if s = metis_predicator orelse s = predicator_name orelse
   341                s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
   342                orelse s = type_tag_name then
   343               path_finder tm ps (nth ts p)
   344             else if s = metis_app_op orelse s = app_op_name then
   345               let
   346                 val (tm1, tm2) = dest_comb tm
   347                 val p' = p - (length ts - 2)
   348               in
   349                 if p' = 0 then path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
   350                 else path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
   351               end
   352             else
   353               let
   354                 val (tm1, args) = strip_comb tm
   355                 val adjustment = length ts - length args
   356                 val p' = if adjustment > p then p else p - adjustment
   357                 val tm_p = nth args p'
   358                   handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
   359                 val _ = trace_msg ctxt (fn () =>
   360                     "path_finder: " ^ string_of_int p ^ "  " ^
   361                     Syntax.string_of_term ctxt tm_p)
   362                 val (r, t) = path_finder tm_p ps (nth ts p)
   363               in (r, list_comb (tm1, replace_item_list t p' args)) end
   364           end
   365         | path_finder tm ps t = path_finder_fail tm ps (SOME t)
   366       val (tm_subst, body) = path_finder i_atom fp m_tm
   367       val tm_abs = Abs ("x", type_of tm_subst, body)
   368       val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   369       val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   370       val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   371       val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
   372       val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   373       val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   374       val eq_terms =
   375         map (apply2 (Thm.cterm_of ctxt))
   376           (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
   377   in
   378     cterm_instantiate eq_terms subst'
   379   end
   380 
   381 val factor = Seq.hd o distinct_subgoals_tac
   382 
   383 fun one_step ctxt type_enc concealed sym_tab th_pairs p =
   384   (case p of
   385     (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
   386   | (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom
   387   | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   388     inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor
   389   | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
   390     resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor
   391   | (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm
   392   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   393     equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
   394 
   395 fun flexflex_first_order ctxt th =
   396   (case Thm.tpairs_of th of
   397     [] => th
   398   | pairs =>
   399       let
   400         val thy = Proof_Context.theory_of ctxt
   401         val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
   402   
   403         fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T)
   404         fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t)
   405   
   406         val instsT = Vartab.fold (cons o mkT) tyenv []
   407         val insts = Vartab.fold (cons o mk) tenv []
   408       in
   409         Thm.instantiate (instsT, insts) th
   410       end
   411       handle THM _ => th)
   412 
   413 fun is_metis_literal_genuine (_, (s, _)) =
   414   not (String.isPrefix class_prefix (Metis_Name.toString s))
   415 fun is_isabelle_literal_genuine t =
   416   (case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true)
   417 
   418 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   419 
   420 (* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
   421    disjuncts are impossible. In the Isabelle proof, in spite of efforts to
   422    eliminate them, duplicates sometimes appear with slightly different (but
   423    unifiable) types. *)
   424 fun resynchronize ctxt fol_th th =
   425   let
   426     val num_metis_lits =
   427       count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
   428     val num_isabelle_lits = count is_isabelle_literal_genuine (Thm.prems_of th)
   429   in
   430     if num_metis_lits >= num_isabelle_lits then
   431       th
   432     else
   433       let
   434         val (prems0, concl) = th |> Thm.prop_of |> Logic.strip_horn
   435         val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
   436         val goal = Logic.list_implies (prems, concl)
   437         val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
   438         val tac =
   439           cut_tac th 1 THEN
   440           rewrite_goals_tac ctxt' meta_not_not THEN
   441           ALLGOALS (assume_tac ctxt')
   442       in
   443         if length prems = length prems0 then
   444           raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
   445         else
   446           Goal.prove ctxt' [] [] goal (K tac)
   447           |> resynchronize ctxt' fol_th
   448       end
   449   end
   450 
   451 fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
   452                          th_pairs =
   453   if not (null th_pairs) andalso Thm.prop_of (snd (hd th_pairs)) aconv @{prop False} then
   454     (* Isabelle sometimes identifies literals (premises) that are distinct in
   455        Metis (e.g., because of type variables). We give the Isabelle proof the
   456        benefice of the doubt. *)
   457     th_pairs
   458   else
   459     let
   460       val _ = trace_msg ctxt (fn () => "=============================================")
   461       val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   462       val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   463       val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
   464         |> flexflex_first_order ctxt
   465         |> resynchronize ctxt fol_th
   466       val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   467       val _ = trace_msg ctxt (fn () => "=============================================")
   468     in
   469       (fol_th, th) :: th_pairs
   470     end
   471 
   472 (* It is normally sufficient to apply "assume_tac" to unify the conclusion with
   473    one of the premises. Unfortunately, this sometimes yields "Variable
   474    has two distinct types" errors. To avoid this, we instantiate the
   475    variables before applying "assume_tac". Typical constraints are of the form
   476      ?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,
   477    where the nonvariables are goal parameters. *)
   478 fun unify_first_prem_with_concl ctxt i th =
   479   let
   480     val goal = Logic.get_goal (Thm.prop_of th) i |> Envir.beta_eta_contract
   481     val prem = goal |> Logic.strip_assums_hyp |> hd
   482     val concl = goal |> Logic.strip_assums_concl
   483 
   484     fun pair_untyped_aconv (t1, t2) (u1, u2) =
   485       Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
   486 
   487     fun add_terms tp inst =
   488       if exists (pair_untyped_aconv tp) inst then inst
   489       else tp :: map (apsnd (subst_atomic [tp])) inst
   490 
   491     fun is_flex t =
   492       (case strip_comb t of
   493         (Var _, args) => forall is_Bound args
   494       | _ => false)
   495 
   496     fun unify_flex flex rigid =
   497       (case strip_comb flex of
   498         (Var (z as (_, T)), args) =>
   499         add_terms (Var z,
   500           fold_rev absdummy (take (length args) (binder_types T)) rigid)
   501       | _ => I)
   502 
   503     fun unify_potential_flex comb atom =
   504       if is_flex comb then unify_flex comb atom
   505       else if is_Var atom then add_terms (atom, comb)
   506       else I
   507 
   508     fun unify_terms (t, u) =
   509       (case (t, u) of
   510         (t1 $ t2, u1 $ u2) =>
   511         if is_flex t then unify_flex t u
   512         else if is_flex u then unify_flex u t
   513         else fold unify_terms [(t1, u1), (t2, u2)]
   514       | (_ $ _, _) => unify_potential_flex t u
   515       | (_, _ $ _) => unify_potential_flex u t
   516       | (Var _, _) => add_terms (t, u)
   517       | (_, Var _) => add_terms (u, t)
   518       | _ => I)
   519 
   520     val t_inst =
   521       [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt)))
   522          |> the_default [] (* FIXME *)
   523   in
   524     cterm_instantiate t_inst th
   525   end
   526 
   527 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
   528 
   529 fun copy_prems_tac ctxt [] ns i =
   530     if forall (curry (op =) 1) ns then all_tac else copy_prems_tac ctxt (rev ns) [] i
   531   | copy_prems_tac ctxt (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ctxt ms (1 :: ns) i
   532   | copy_prems_tac ctxt (m :: ms) ns i =
   533     eresolve_tac ctxt [copy_prem] i THEN copy_prems_tac ctxt ms (m div 2 :: (m + 1) div 2 :: ns) i
   534 
   535 (* Metis generates variables of the form _nnn. *)
   536 val is_metis_fresh_variable = String.isPrefix "_"
   537 
   538 fun instantiate_forall_tac ctxt t i st =
   539   let
   540     val params = Logic.strip_params (Logic.get_goal (Thm.prop_of st) i) |> rev
   541 
   542     fun repair (t as (Var ((s, _), _))) =
   543         (case find_index (fn (s', _) => s' = s) params of
   544           ~1 => t
   545         | j => Bound j)
   546       | repair (t $ u) =
   547         (case (repair t, repair u) of
   548           (t as Bound j, u as Bound k) =>
   549           (* This is a trick to repair the discrepancy between the fully skolemized term that MESON
   550              gives us (where existentials were pulled out) and the reality. *)
   551           if k > j then t else t $ u
   552         | (t, u) => t $ u)
   553       | repair t = t
   554 
   555     val t' = t |> repair |> fold (absdummy o snd) params
   556 
   557     fun do_instantiate th =
   558       (case Term.add_vars (Thm.prop_of th) []
   559             |> filter_out ((Meson_Clausify.is_zapped_var_name orf is_metis_fresh_variable) o fst
   560               o fst) of
   561         [] => th
   562       | [var as (_, T)] =>
   563         let
   564           val var_binder_Ts = T |> binder_types |> take (length params) |> rev
   565           val var_body_T = T |> funpow (length params) range_type
   566           val tyenv =
   567             Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
   568                                              var_body_T :: var_binder_Ts)
   569           val env =
   570             Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
   571               tenv = Vartab.empty, tyenv = tyenv}
   572           val ty_inst =
   573             Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T)))
   574               tyenv []
   575           val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')]
   576         in
   577           Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th
   578         end
   579       | _ => raise Fail "expected a single non-zapped, non-Metis Var")
   580   in
   581     (DETERM (eresolve_tac ctxt @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
   582   end
   583 
   584 fun fix_exists_tac ctxt t = eresolve_tac ctxt [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
   585 
   586 fun release_quantifier_tac ctxt (skolem, t) =
   587   (if skolem then fix_exists_tac ctxt else instantiate_forall_tac ctxt) t
   588 
   589 fun release_clusters_tac _ _ _ [] = K all_tac
   590   | release_clusters_tac ctxt 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 ctxt) 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 ctxt 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)) (apply2 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 (apply2 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 Thm.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 apply2 (Meson_Clausify.cluster_of_zapped_var_name
   652                                       o fst o fst))
   653                  |> map (fn (xi, (T, t)) => apply2 (Envir.subst_term_types tyenv) (Var (xi, T), t))
   654           val tysubst = tyenv |> Vartab.dest
   655         in (tysubst, tsubst) end
   656 
   657       fun subst_info_of_prem subgoal_no prem =
   658         (case prem of
   659           _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
   660           let val ax_no = HOLogic.dest_nat num in
   661             (ax_no, (subgoal_no,
   662                      match_term (nth axioms ax_no |> the |> snd, t)))
   663           end
   664         | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
   665 
   666       fun cluster_of_var_name skolem s =
   667         (case try Meson_Clausify.cluster_of_zapped_var_name s of
   668           NONE => NONE
   669         | SOME ((ax_no, (cluster_no, _)), skolem') =>
   670           if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE)
   671 
   672       fun clusters_in_term skolem t =
   673         Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
   674 
   675       fun deps_of_term_subst (var, t) =
   676         (case clusters_in_term false var of
   677           [] => NONE
   678         | [(ax_no, cluster_no)] =>
   679           SOME ((ax_no, cluster_no),
   680             clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
   681         | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]))
   682 
   683       val prems = Logic.strip_imp_prems (Thm.prop_of prems_imp_false)
   684       val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
   685                          |> sort (int_ord o apply2 fst)
   686       val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
   687       val clusters = maps (op ::) depss
   688       val ordered_clusters =
   689         Int_Pair_Graph.empty
   690         |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
   691         |> fold Int_Pair_Graph.add_deps_acyclic depss
   692         |> Int_Pair_Graph.topological_order
   693         handle Int_Pair_Graph.CYCLES _ =>
   694                error "Cannot replay Metis proof in Isabelle without \"Hilbert_Choice\""
   695       val ax_counts =
   696         Int_Tysubst_Table.empty
   697         |> fold (fn (ax_no, (_, (tysubst, _))) =>
   698                     Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
   699                                                   (Integer.add 1)) substs
   700         |> Int_Tysubst_Table.dest
   701       val needed_axiom_props =
   702         0 upto length axioms - 1 ~~ axioms
   703         |> map_filter (fn (_, NONE) => NONE
   704                         | (ax_no, SOME (_, t)) =>
   705                           if exists (fn ((ax_no', _), n) =>
   706                                         ax_no' = ax_no andalso n > 0)
   707                                     ax_counts then
   708                             SOME t
   709                           else
   710                             NONE)
   711       val outer_param_names =
   712         [] |> fold Term.add_var_names needed_axiom_props
   713            |> filter (Meson_Clausify.is_zapped_var_name o fst)
   714            |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
   715            |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
   716                          cluster_no = 0 andalso skolem)
   717            |> sort shuffle_ord |> map (fst o snd)
   718 
   719 (* for debugging only:
   720       fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
   721         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
   722         "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
   723         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
   724                      o apply2 (Syntax.string_of_term ctxt)) tsubst) ^ "}"
   725       val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters)
   726       val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
   727       val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
   728       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
   729                        cat_lines (map string_of_subst_info substs))
   730 *)
   731       val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
   732 
   733       fun cut_and_ex_tac axiom =
   734         cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac ctxt' @{thms exE}) 1)
   735       fun rotation_of_subgoal i =
   736         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
   737     in
   738       Goal.prove ctxt' [] [] @{prop False}
   739         (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts)
   740               THEN rename_tac outer_param_names 1
   741               THEN copy_prems_tac ctxt' (map snd ax_counts) [] 1)
   742             THEN release_clusters_tac ctxt' ax_counts substs ordered_clusters 1
   743             THEN match_tac ctxt' [prems_imp_false] 1
   744             THEN ALLGOALS (fn i => resolve_tac ctxt' @{thms Meson.skolem_COMBK_I} i
   745               THEN rotate_tac (rotation_of_subgoal i) i
   746               THEN PRIMITIVE (unify_first_prem_with_concl ctxt' i)
   747               THEN assume_tac ctxt' i
   748               THEN flexflex_tac ctxt')))
   749       handle ERROR msg =>
   750         cat_error msg
   751           "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"
   752     end
   753 
   754 end;