src/HOL/Tools/ATP/atp_proof_reconstruct.ML
author wenzelm
Sat Mar 22 18:19:57 2014 +0100 (2014-03-22)
changeset 56254 a2dd9200854d
parent 56104 fd6e132ee4fb
child 56854 ddd3af5a683d
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOL/Tools/ATP/atp_proof_reconstruct.ML
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Claire Quigley, Cambridge University Computer Laboratory
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Basic proof reconstruction from ATP proofs.
     7 *)
     8 
     9 signature ATP_PROOF_RECONSTRUCT =
    10 sig
    11   type 'a atp_type = 'a ATP_Problem.atp_type
    12   type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
    13   type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
    14   type stature = ATP_Problem_Generate.stature
    15   type atp_step_name = ATP_Proof.atp_step_name
    16   type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
    17   type 'a atp_proof = 'a ATP_Proof.atp_proof
    18 
    19   val metisN : string
    20   val full_typesN : string
    21   val partial_typesN : string
    22   val no_typesN : string
    23   val really_full_type_enc : string
    24   val full_type_enc : string
    25   val partial_type_enc : string
    26   val no_type_enc : string
    27   val full_type_encs : string list
    28   val partial_type_encs : string list
    29   val default_metis_lam_trans : string
    30 
    31   val forall_of : term -> term -> term
    32   val exists_of : term -> term -> term
    33   val type_enc_aliases : (string * string list) list
    34   val unalias_type_enc : string -> string list
    35   val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
    36     (string, string atp_type) atp_term -> term
    37   val prop_of_atp : Proof.context -> bool -> int Symtab.table ->
    38     (string, string, (string, string atp_type) atp_term, string) atp_formula -> term
    39 
    40   val used_facts_in_atp_proof :
    41     Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
    42   val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector ->
    43     'a atp_proof -> string list option
    44   val atp_proof_prefers_lifting : string atp_proof -> bool
    45   val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
    46   val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
    47     ('a, 'b) atp_step
    48   val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list ->
    49     int Symtab.table -> string atp_proof -> (term, string) atp_step list
    50   val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list
    51   val factify_atp_proof : (string * 'a) list vector -> term list -> term ->
    52     (term, string) atp_step list -> (term, string) atp_step list
    53 end;
    54 
    55 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
    56 struct
    57 
    58 open ATP_Util
    59 open ATP_Problem
    60 open ATP_Proof
    61 open ATP_Problem_Generate
    62 
    63 val metisN = "metis"
    64 
    65 val full_typesN = "full_types"
    66 val partial_typesN = "partial_types"
    67 val no_typesN = "no_types"
    68 
    69 val really_full_type_enc = "mono_tags"
    70 val full_type_enc = "poly_guards_query"
    71 val partial_type_enc = "poly_args"
    72 val no_type_enc = "erased"
    73 
    74 val full_type_encs = [full_type_enc, really_full_type_enc]
    75 val partial_type_encs = partial_type_enc :: full_type_encs
    76 
    77 val type_enc_aliases =
    78   [(full_typesN, full_type_encs),
    79    (partial_typesN, partial_type_encs),
    80    (no_typesN, [no_type_enc])]
    81 
    82 fun unalias_type_enc s =
    83   AList.lookup (op =) type_enc_aliases s |> the_default [s]
    84 
    85 val default_metis_lam_trans = combsN
    86 
    87 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
    88   | term_name' _ = ""
    89 
    90 fun lambda' v = Term.lambda_name (term_name' v, v)
    91 
    92 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t
    93 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t
    94 
    95 fun make_tfree ctxt w =
    96   let val ww = "'" ^ w in
    97     TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
    98   end
    99 
   100 exception ATP_CLASS of string list
   101 exception ATP_TYPE of string atp_type list
   102 exception ATP_TERM of (string, string atp_type) atp_term list
   103 exception ATP_FORMULA of
   104   (string, string, (string, string atp_type) atp_term, string) atp_formula list
   105 exception SAME of unit
   106 
   107 fun class_of_atp_class cls =
   108   (case unprefix_and_unascii class_prefix cls of
   109     SOME s => s
   110   | NONE => raise ATP_CLASS [cls])
   111 
   112 (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information
   113    from type literals, or by type inference. *)
   114 fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) =
   115   let val Ts = map (typ_of_atp_type ctxt) tys in
   116     (case unprefix_and_unascii type_const_prefix a of
   117       SOME b => Type (invert_const b, Ts)
   118     | NONE =>
   119       if not (null tys) then
   120         raise ATP_TYPE [ty] (* only "tconst"s have type arguments *)
   121       else
   122         (case unprefix_and_unascii tfree_prefix a of
   123           SOME b => make_tfree ctxt b
   124         | NONE =>
   125           (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
   126              Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
   127              forces us to use a type parameter in all cases. *)
   128           Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
   129             (if null clss then @{sort type} else map class_of_atp_class clss))))
   130   end
   131 
   132 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
   133 
   134 fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term
   135 
   136 (* Type class literal applied to a type. Returns triple of polarity, class, type. *)
   137 fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) =
   138   (case (unprefix_and_unascii class_prefix a, map (typ_of_atp_term ctxt) us) of
   139     (SOME b, [T]) => (b, T)
   140   | _ => raise ATP_TERM [u])
   141 
   142 (* Accumulate type constraints in a formula: negative type literals. *)
   143 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   144 fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   145   | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
   146   | add_type_constraint _ _ = I
   147 
   148 fun repair_var_name_raw s =
   149   let
   150     fun subscript_name s n = s ^ nat_subscript n
   151     val s = s |> String.map Char.toLower
   152   in
   153     (case space_explode "_" s of
   154       [_] =>
   155       (case take_suffix Char.isDigit (String.explode s) of
   156         (cs1 as _ :: _, cs2 as _ :: _) =>
   157         subscript_name (String.implode cs1) (the (Int.fromString (String.implode cs2)))
   158       | (_, _) => s)
   159     | [s1, s2] => (case Int.fromString s2 of SOME n => subscript_name s1 n | NONE => s)
   160     | _ => s)
   161   end
   162 
   163 fun repair_var_name textual s =
   164   (case unprefix_and_unascii schematic_var_prefix s of
   165     SOME s => s
   166   | NONE => s |> textual ? repair_var_name_raw)
   167 
   168 (* The number of type arguments of a constant, zero if it's monomorphic. For (instances of) Skolem
   169    pseudoconstants, this information is encoded in the constant name. *)
   170 fun robust_const_num_type_args thy s =
   171   if String.isPrefix skolem_const_prefix s then
   172     s |> Long_Name.explode |> List.last |> Int.fromString |> the
   173   else if String.isPrefix lam_lifted_prefix s then
   174     if String.isPrefix lam_lifted_poly_prefix s then 2 else 0
   175   else
   176     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
   177 
   178 fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
   179 
   180 (* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
   181 fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
   182   | loose_aconv (t, t') = t aconv t'
   183 
   184 val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
   185 val vampire_skolem_prefix = "sK"
   186 
   187 (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
   188    should allow them to be inferred. *)
   189 fun term_of_atp ctxt textual sym_tab =
   190   let
   191     val thy = Proof_Context.theory_of ctxt
   192     (* For Metis, we use 1 rather than 0 because variable references in clauses may otherwise
   193        conflict with variable constraints in the goal. At least, type inference often fails
   194        otherwise. See also "axiom_inference" in "Metis_Reconstruct". *)
   195     val var_index = if textual then 0 else 1
   196     fun do_term extra_ts opt_T u =
   197       (case u of
   198         ATerm ((s, tys), us) =>
   199         if s = ""
   200           then error "Isar proof reconstruction failed because the ATP proof \
   201                      \contains unparsable material."
   202         else if String.isPrefix native_type_prefix s then
   203           @{const True} (* ignore TPTP type information *)
   204         else if s = tptp_equal then
   205           let val ts = map (do_term [] NONE) us in
   206             if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
   207               @{const True}
   208             else
   209               list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
   210           end
   211         else
   212           (case unprefix_and_unascii const_prefix s of
   213             SOME s' =>
   214             let val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const in
   215               if s' = type_tag_name then
   216                 (case mangled_us @ us of
   217                   [typ_u, term_u] => do_term extra_ts (SOME (typ_of_atp_term ctxt typ_u)) term_u
   218                 | _ => raise ATP_TERM us)
   219               else if s' = predicator_name then
   220                 do_term [] (SOME @{typ bool}) (hd us)
   221               else if s' = app_op_name then
   222                 let val extra_t = do_term [] NONE (List.last us) in
   223                   do_term (extra_t :: extra_ts)
   224                           (case opt_T of
   225                              SOME T => SOME (slack_fastype_of extra_t --> T)
   226                            | NONE => NONE)
   227                           (nth us (length us - 2))
   228                 end
   229               else if s' = type_guard_name then
   230                 @{const True} (* ignore type predicates *)
   231               else
   232                 let
   233                   val new_skolem = String.isPrefix new_skolem_const_prefix s''
   234                   val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
   235                   val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
   236                   val term_ts = map (do_term [] NONE) term_us
   237 
   238                   val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us
   239                   val T =
   240                     (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then
   241                        if new_skolem then
   242                          SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
   243                        else if textual then
   244                          try (Sign.const_instance thy) (s', Ts)
   245                        else
   246                          NONE
   247                      else
   248                        NONE)
   249                     |> (fn SOME T => T
   250                          | NONE =>
   251                            map slack_fastype_of term_ts --->
   252                             the_default (Type_Infer.anyT @{sort type}) opt_T)
   253                   val t =
   254                     if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
   255                     else Const (unproxify_const s', T)
   256                 in list_comb (t, term_ts @ extra_ts) end
   257             end
   258           | NONE => (* a free or schematic variable *)
   259             let
   260               (* This assumes that distinct names are mapped to distinct names by
   261                  "Variable.variant_frees". This does not hold in general but should hold for
   262                  ATP-generated Skolem function names, since these end with a digit and
   263                  "variant_frees" appends letters. *)
   264               fun fresh_up s =
   265                 [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst
   266               val term_ts =
   267                 map (do_term [] NONE) us
   268                 (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse
   269                    order, which is incompatible with the new Metis skolemizer. *)
   270                 |> exists (fn pre => String.isPrefix pre s)
   271                   [spass_skolem_prefix, vampire_skolem_prefix] ? rev
   272               val ts = term_ts @ extra_ts
   273               val T =
   274                 (case opt_T of
   275                   SOME T => map slack_fastype_of term_ts ---> T
   276                 | NONE =>
   277                   map slack_fastype_of ts --->
   278                   (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT @{sort type}))
   279               val t =
   280                 (case unprefix_and_unascii fixed_var_prefix s of
   281                   SOME s => Free (s, T)
   282                 | NONE =>
   283                   if textual andalso not (is_tptp_variable s) then
   284                     Free (s |> textual ? (repair_var_name_raw #> fresh_up), T)
   285                   else
   286                     Var ((repair_var_name textual s, var_index), T))
   287             in list_comb (t, ts) end))
   288   in do_term [] end
   289 
   290 fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
   291   if String.isPrefix class_prefix s then
   292     add_type_constraint pos (type_constraint_of_term ctxt u)
   293     #> pair @{const True}
   294   else
   295     pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)
   296 
   297 (* Update schematic type variables with detected sort constraints. It's not
   298    totally clear whether this code is necessary. *)
   299 fun repair_tvar_sorts (t, tvar_tab) =
   300   let
   301     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   302       | do_type (TVar (xi, s)) =
   303         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   304       | do_type (TFree z) = TFree z
   305     fun do_term (Const (a, T)) = Const (a, do_type T)
   306       | do_term (Free (a, T)) = Free (a, do_type T)
   307       | do_term (Var (xi, T)) = Var (xi, do_type T)
   308       | do_term (t as Bound _) = t
   309       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   310       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   311   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   312 
   313 fun quantify_over_var quant_of var_s t =
   314   let
   315     val vars = filter (fn ((s, _), _) => s = var_s) (Term.add_vars t [])
   316     val normTs = vars |> AList.group (op =) |> map (apsnd hd)
   317     fun norm_var_types (Var (x, T)) =
   318         Var (x, (case AList.lookup (op =) normTs x of NONE => T | SOME T' => T'))
   319       | norm_var_types t = t
   320   in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
   321 
   322 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the
   323    formula. *)
   324 fun prop_of_atp ctxt textual sym_tab phi =
   325   let
   326     fun do_formula pos phi =
   327       (case phi of
   328         AQuant (_, [], phi) => do_formula pos phi
   329       | AQuant (q, (s, _) :: xs, phi') =>
   330         do_formula pos (AQuant (q, xs, phi'))
   331         (* FIXME: TFF *)
   332         #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of)
   333           (repair_var_name textual s)
   334       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   335       | AConn (c, [phi1, phi2]) =>
   336         do_formula (pos |> c = AImplies ? not) phi1
   337         ##>> do_formula pos phi2
   338         #>> (case c of
   339               AAnd => s_conj
   340             | AOr => s_disj
   341             | AImplies => s_imp
   342             | AIff => s_iff
   343             | ANot => raise Fail "impossible connective")
   344       | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
   345       | _ => raise ATP_FORMULA [phi])
   346   in
   347     repair_tvar_sorts (do_formula true phi Vartab.empty)
   348   end
   349 
   350 fun find_first_in_list_vector vec key =
   351   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
   352                  | (_, value) => value) NONE vec
   353 
   354 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
   355 
   356 fun resolve_one_named_fact fact_names s =
   357   (case try (unprefix fact_prefix) s of
   358     SOME s' =>
   359     let val s' = s' |> unprefix_fact_number |> unascii_of in
   360       s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
   361     end
   362   | NONE => NONE)
   363 
   364 fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
   365 
   366 fun resolve_one_named_conjecture s =
   367   (case try (unprefix conjecture_prefix) s of
   368     SOME s' => Int.fromString s'
   369   | NONE => NONE)
   370 
   371 val resolve_conjecture = map_filter resolve_one_named_conjecture
   372 
   373 fun is_axiom_used_in_proof pred =
   374   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
   375 
   376 fun add_non_rec_defs fact_names accum =
   377   Vector.foldl (fn (facts, facts') =>
   378       union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts')
   379     accum fact_names
   380 
   381 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
   382 val leo2_unfold_def_rule = "unfold_def"
   383 
   384 fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
   385   (if rule = leo2_extcnf_equal_neg_rule then
   386      insert (op =) (short_thm_name ctxt ext, (Global, General))
   387    else if rule = leo2_unfold_def_rule then
   388      (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP
   389         proof. Remove the next line once this is fixed. *)
   390      add_non_rec_defs fact_names
   391    else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then
   392      (fn [] =>
   393          (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we
   394             assume the worst and include them all here. *)
   395          [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs fact_names
   396        | facts => facts)
   397    else
   398      I)
   399   #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
   400 
   401 fun used_facts_in_atp_proof ctxt fact_names atp_proof =
   402   if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
   403   else fold (add_fact ctxt fact_names) atp_proof []
   404 
   405 fun used_facts_in_unsound_atp_proof _ _ [] = NONE
   406   | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
   407     let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
   408       if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
   409          not (is_axiom_used_in_proof (not o null o resolve_conjecture o single) atp_proof) then
   410         SOME (map fst used_facts)
   411       else
   412         NONE
   413     end
   414 
   415 val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
   416 
   417 (* overapproximation (good enough) *)
   418 fun is_lam_lifted s =
   419   String.isPrefix fact_prefix s andalso
   420   String.isSubstring ascii_of_lam_fact_prefix s
   421 
   422 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
   423 
   424 fun atp_proof_prefers_lifting atp_proof =
   425   (is_axiom_used_in_proof is_combinator_def atp_proof,
   426    is_axiom_used_in_proof is_lam_lifted atp_proof) = (false, true)
   427 
   428 val is_typed_helper_name =
   429   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
   430 
   431 fun is_typed_helper_used_in_atp_proof atp_proof =
   432   is_axiom_used_in_proof is_typed_helper_name atp_proof
   433 
   434 fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep]
   435 fun replace_dependencies_in_line old_new (name, role, t, rule, deps) =
   436   (name, role, t, rule, fold (union (op =) o replace_one_dependency old_new) deps [])
   437 
   438 fun repair_name "$true" = "c_True"
   439   | repair_name "$false" = "c_False"
   440   | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
   441   | repair_name s =
   442     if is_tptp_equal s orelse
   443        (* seen in Vampire proofs *)
   444        (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
   445       tptp_equal
   446     else
   447       s
   448 
   449 fun infer_formula_types ctxt =
   450   Type.constraint HOLogic.boolT
   451   #> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
   452 
   453 val combinator_table =
   454   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
   455    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
   456    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
   457    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
   458    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
   459 
   460 fun uncombine_term thy =
   461   let
   462     fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
   463       | aux (Abs (s, T, t')) = Abs (s, T, aux t')
   464       | aux (t as Const (x as (s, _))) =
   465         (case AList.lookup (op =) combinator_table s of
   466           SOME thm => thm |> prop_of |> specialize_type thy x |> Logic.dest_equals |> snd
   467         | NONE => t)
   468       | aux t = t
   469   in aux end
   470 
   471 fun unlift_term lifted =
   472   map_aterms (fn t as Const (s, _) =>
   473                  if String.isPrefix lam_lifted_prefix s then
   474                    (* FIXME: do something about the types *)
   475                    (case AList.lookup (op =) lifted s of
   476                      SOME t => unlift_term lifted t
   477                    | NONE => t)
   478                  else
   479                    t
   480                | t => t)
   481 
   482 fun termify_line ctxt lifted sym_tab (name, role, u, rule, deps) =
   483   let
   484     val thy = Proof_Context.theory_of ctxt
   485     val t = u
   486       |> prop_of_atp ctxt true sym_tab
   487       |> uncombine_term thy
   488       |> unlift_term lifted
   489       |> infer_formula_types ctxt
   490       |> HOLogic.mk_Trueprop
   491   in
   492     (name, role, t, rule, deps)
   493   end
   494 
   495 val waldmeister_conjecture_num = "1.0.0.0"
   496 
   497 fun repair_waldmeister_endgame proof =
   498   let
   499     fun repair_tail (name, _, t, rule, deps) = (name, Negated_Conjecture, s_not t, rule, deps)
   500     fun repair_body [] = []
   501       | repair_body ((line as ((num, _), _, _, _, _)) :: lines) =
   502         if num = waldmeister_conjecture_num then map repair_tail (line :: lines)
   503         else line :: repair_body lines
   504   in
   505     repair_body proof
   506   end
   507 
   508 fun termify_atp_proof ctxt pool lifted sym_tab =
   509   clean_up_atp_proof_dependencies
   510   #> nasty_atp_proof pool
   511   #> map_term_names_in_atp_proof repair_name
   512   #> map (termify_line ctxt lifted sym_tab)
   513   #> repair_waldmeister_endgame
   514 
   515 fun take_distinct_vars seen ((t as Var _) :: ts) =
   516     if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
   517   | take_distinct_vars seen _ = rev seen
   518 
   519 fun unskolemize_term skos t =
   520   let
   521     val is_sko = member (op =) skos
   522 
   523     fun find_args args (t $ u) = find_args (u :: args) t #> find_args [] u
   524       | find_args _ (Abs (_, _, t)) = find_args [] t
   525       | find_args args (Free (s, _)) =
   526         if is_sko s then
   527           let val new = take_distinct_vars [] args in
   528             (fn [] => new | old => if length new < length old then new else old)
   529           end
   530         else
   531           I
   532       | find_args _ _ = I
   533 
   534     val alls = find_args [] t []
   535     val num_alls = length alls
   536 
   537     fun fix_skos args (t $ u) = fix_skos (fix_skos [] u :: args) t
   538       | fix_skos args (t as Free (s, T)) =
   539         if is_sko s then list_comb (Free (s, funpow num_alls body_type T), drop num_alls args)
   540         else list_comb (t, args)
   541       | fix_skos [] (Abs (s, T, t)) = Abs (s, T, fix_skos [] t)
   542       | fix_skos [] t = t
   543       | fix_skos args t = list_comb (fix_skos [] t, args)
   544 
   545     val t' = fix_skos [] t
   546 
   547     fun add_sko (t as Free (s, _)) = is_sko s ? insert (op aconv) t
   548       | add_sko _ = I
   549 
   550     val exs = Term.fold_aterms add_sko t' []
   551   in
   552     t'
   553     |> HOLogic.dest_Trueprop
   554     |> fold exists_of exs |> Term.map_abs_vars (K Name.uu)
   555     |> fold_rev forall_of alls
   556     |> HOLogic.mk_Trueprop
   557   end
   558 
   559 fun introduce_spass_skolem [] = []
   560   | introduce_spass_skolem (proof as (_, _, _, rule1, _) :: _) =
   561     if rule1 = spass_input_rule then
   562       let
   563         fun add_sko (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s
   564           | add_sko _ = I
   565 
   566         (* union-find would be faster *)
   567         fun add_cycle [] = I
   568           | add_cycle ss =
   569             fold (fn s => Graph.default_node (s, ())) ss
   570             #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss])
   571 
   572         val (input_steps, other_steps) = List.partition (null o #5) proof
   573 
   574         val skoss = map (fn (_, _, t, _, _) => Term.fold_aterms add_sko t []) input_steps
   575         val skoss_input_steps = filter_out (null o fst) (skoss ~~ input_steps)
   576         val groups = Graph.strong_conn (fold add_cycle skoss Graph.empty)
   577 
   578         fun step_name_of_group skos = (implode skos, [])
   579         fun in_group group = member (op =) group o hd
   580         fun group_of sko = the (find_first (fn group => in_group group sko) groups)
   581 
   582         fun new_steps (skoss_steps : (string list * (term, 'a) atp_step) list) group =
   583           let
   584             val name = step_name_of_group group
   585             val name0 = name |>> prefix "0"
   586             val t =
   587               skoss_steps
   588               |> map (snd #> #3 #> HOLogic.dest_Trueprop)
   589               |> Library.foldr1 s_conj
   590               |> HOLogic.mk_Trueprop
   591             val skos = fold (union (op =) o fst) skoss_steps []
   592             val deps = map (snd #> #1) skoss_steps
   593           in
   594             [(name0, Unknown, unskolemize_term skos t, spass_pre_skolemize_rule, deps),
   595              (name, Unknown, t, spass_skolemize_rule, [name0])]
   596           end
   597 
   598         val sko_steps =
   599           maps (fn group => new_steps (filter (in_group group o fst) skoss_input_steps) group)
   600             groups
   601 
   602         val old_news =
   603           map (fn (skos, (name, _, _, _, _)) => (name, [step_name_of_group (group_of skos)]))
   604             skoss_input_steps
   605         val repair_deps = fold replace_dependencies_in_line old_news
   606       in
   607         input_steps @ sko_steps @ map repair_deps other_steps
   608       end
   609   else
   610     proof
   611 
   612 fun factify_atp_proof fact_names hyp_ts concl_t atp_proof =
   613   let
   614     fun factify_step ((num, ss), _, t, rule, deps) =
   615       let
   616         val (ss', role', t') =
   617           (case resolve_conjecture ss of
   618             [j] =>
   619             if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
   620           | _ =>
   621             (case resolve_fact fact_names ss of
   622               [] => (ss, Plain, t)
   623             | facts => (map fst facts, Axiom, t)))
   624       in
   625         ((num, ss'), role', t', rule, deps)
   626       end
   627 
   628     val atp_proof = map factify_step atp_proof
   629     val names = map #1 atp_proof
   630 
   631     fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num))
   632     fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps)
   633   in
   634     map repair_deps atp_proof
   635   end
   636 
   637 end;