src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
author blanchet
Fri Oct 22 13:54:51 2010 +0200 (2010-10-22)
changeset 40067 0783415ed7f0
parent 40064 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML@db8413d82c3b
child 40068 ed2869dd9bfa
permissions -rw-r--r--
renamed files
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_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 Proof reconstruction for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_RECONSTRUCT =
    10 sig
    11   type locality = Sledgehammer_Filter.locality
    12   type minimize_command = string list -> string
    13   type metis_params =
    14     string * bool * minimize_command * string * (string * locality) list vector
    15     * thm * int
    16   type isar_params =
    17     string Symtab.table * bool * int * Proof.context * int list list
    18   type text_result = string * (string * locality) list
    19 
    20   val repair_conjecture_shape_and_axiom_names :
    21     string -> int list list -> (string * locality) list vector
    22     -> int list list * (string * locality) list vector
    23   val apply_on_subgoal : int -> int -> string
    24   val command_call : string -> string list -> string
    25   val try_command_line : string -> string -> string
    26   val minimize_line : ('a list -> string) -> 'a list -> string
    27   val metis_proof_text : metis_params -> text_result
    28   val isar_proof_text : isar_params -> metis_params -> text_result
    29   val proof_text : bool -> isar_params -> metis_params -> text_result
    30 end;
    31 
    32 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    33 struct
    34 
    35 open ATP_Problem
    36 open ATP_Proof
    37 open Metis_Translate
    38 open Sledgehammer_Util
    39 open Sledgehammer_Filter
    40 open Sledgehammer_Translate
    41 
    42 type minimize_command = string list -> string
    43 type metis_params =
    44   string * bool * minimize_command * string * (string * locality) list vector
    45   * thm * int
    46 type isar_params =
    47   string Symtab.table * bool * int * Proof.context * int list list
    48 type text_result = string * (string * locality) list
    49 
    50 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    51 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    52 
    53 fun find_first_in_list_vector vec key =
    54   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    55                  | (_, value) => value) NONE vec
    56 
    57 
    58 (** SPASS's Flotter hack **)
    59 
    60 (* This is a hack required for keeping track of axioms after they have been
    61    clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
    62    part of this hack. *)
    63 
    64 val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
    65 
    66 fun extract_clause_sequence output =
    67   let
    68     val tokens_of = String.tokens (not o Char.isAlphaNum)
    69     fun extract_num ("clause" :: (ss as _ :: _)) =
    70     Int.fromString (List.last ss)
    71       | extract_num _ = NONE
    72   in output |> split_lines |> map_filter (extract_num o tokens_of) end
    73 
    74 val parse_clause_formula_pair =
    75   $$ "(" |-- scan_integer --| $$ ","
    76   -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
    77   --| Scan.option ($$ ",")
    78 val parse_clause_formula_relation =
    79   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
    80   |-- Scan.repeat parse_clause_formula_pair
    81 val extract_clause_formula_relation =
    82   Substring.full #> Substring.position set_ClauseFormulaRelationN
    83   #> snd #> Substring.position "." #> fst #> Substring.string
    84   #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
    85   #> fst
    86 
    87 fun repair_conjecture_shape_and_axiom_names output conjecture_shape
    88                                             axiom_names =
    89   if String.isSubstring set_ClauseFormulaRelationN output then
    90     let
    91       val j0 = hd (hd conjecture_shape)
    92       val seq = extract_clause_sequence output
    93       val name_map = extract_clause_formula_relation output
    94       fun renumber_conjecture j =
    95         conjecture_prefix ^ string_of_int (j - j0)
    96         |> AList.find (fn (s, ss) => member (op =) ss s) name_map
    97         |> map (fn s => find_index (curry (op =) s) seq + 1)
    98       fun names_for_number j =
    99         j |> AList.lookup (op =) name_map |> these
   100           |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
   101           |> map (fn name =>
   102                      (name, name |> find_first_in_list_vector axiom_names
   103                                  |> the)
   104                      handle Option.Option =>
   105                             error ("No such fact: " ^ quote name ^ "."))
   106     in
   107       (conjecture_shape |> map (maps renumber_conjecture),
   108        seq |> map names_for_number |> Vector.fromList)
   109     end
   110   else
   111     (conjecture_shape, axiom_names)
   112 
   113 
   114 (** Soft-core proof reconstruction: Metis one-liner **)
   115 
   116 fun string_for_label (s, num) = s ^ string_of_int num
   117 
   118 fun apply_on_subgoal _ 1 = "by "
   119   | apply_on_subgoal 1 _ = "apply "
   120   | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
   121 fun command_call name [] = name
   122   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   123 fun try_command_line banner command =
   124   banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   125 fun using_labels [] = ""
   126   | using_labels ls =
   127     "using " ^ space_implode " " (map string_for_label ls) ^ " "
   128 fun metis_name full_types = if full_types then "metisFT" else "metis"
   129 fun metis_call full_types ss = command_call (metis_name full_types) ss
   130 fun metis_command full_types i n (ls, ss) =
   131   using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
   132 fun metis_line banner full_types i n ss =
   133   try_command_line banner (metis_command full_types i n ([], ss))
   134 fun minimize_line _ [] = ""
   135   | minimize_line minimize_command ss =
   136     case minimize_command ss of
   137       "" => ""
   138     | command =>
   139       "\nTo minimize the number of lemmas, try this: " ^
   140       Markup.markup Markup.sendback command ^ "."
   141 
   142 fun resolve_axiom axiom_names ((_, SOME s)) =
   143     (case strip_prefix_and_unascii axiom_prefix s of
   144        SOME s' => (case find_first_in_list_vector axiom_names s' of
   145                      SOME x => [(s', x)]
   146                    | NONE => [])
   147      | NONE => [])
   148   | resolve_axiom axiom_names (num, NONE) =
   149     case Int.fromString num of
   150       SOME j =>
   151       if j > 0 andalso j <= Vector.length axiom_names then
   152         Vector.sub (axiom_names, j - 1)
   153       else
   154         []
   155     | NONE => []
   156 
   157 fun add_fact axiom_names (Inference (name, _, [])) =
   158     append (resolve_axiom axiom_names name)
   159   | add_fact _ _ = I
   160 
   161 fun used_facts_in_tstplike_proof axiom_names =
   162   atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
   163 
   164 fun used_facts axiom_names =
   165   used_facts_in_tstplike_proof axiom_names
   166   #> List.partition (curry (op =) Chained o snd)
   167   #> pairself (sort_distinct (string_ord o pairself fst))
   168 
   169 fun metis_proof_text (banner, full_types, minimize_command,
   170                       tstplike_proof, axiom_names, goal, i) =
   171   let
   172     val (chained_lemmas, other_lemmas) =
   173       used_facts axiom_names tstplike_proof
   174     val n = Logic.count_prems (prop_of goal)
   175   in
   176     (metis_line banner full_types i n (map fst other_lemmas) ^
   177      minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
   178      other_lemmas @ chained_lemmas)
   179   end
   180 
   181 
   182 (** Hard-core proof reconstruction: structured Isar proofs **)
   183 
   184 (* Simple simplifications to ensure that sort annotations don't leave a trail of
   185    spurious "True"s. *)
   186 fun s_not @{const False} = @{const True}
   187   | s_not @{const True} = @{const False}
   188   | s_not (@{const Not} $ t) = t
   189   | s_not t = @{const Not} $ t
   190 fun s_conj (@{const True}, t2) = t2
   191   | s_conj (t1, @{const True}) = t1
   192   | s_conj p = HOLogic.mk_conj p
   193 fun s_disj (@{const False}, t2) = t2
   194   | s_disj (t1, @{const False}) = t1
   195   | s_disj p = HOLogic.mk_disj p
   196 fun s_imp (@{const True}, t2) = t2
   197   | s_imp (t1, @{const False}) = s_not t1
   198   | s_imp p = HOLogic.mk_imp p
   199 fun s_iff (@{const True}, t2) = t2
   200   | s_iff (t1, @{const True}) = t1
   201   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
   202 
   203 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   204 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
   205 
   206 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   207     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
   208   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   209     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
   210   | negate_term (@{const HOL.implies} $ t1 $ t2) =
   211     @{const HOL.conj} $ t1 $ negate_term t2
   212   | negate_term (@{const HOL.conj} $ t1 $ t2) =
   213     @{const HOL.disj} $ negate_term t1 $ negate_term t2
   214   | negate_term (@{const HOL.disj} $ t1 $ t2) =
   215     @{const HOL.conj} $ negate_term t1 $ negate_term t2
   216   | negate_term (@{const Not} $ t) = t
   217   | negate_term t = @{const Not} $ t
   218 
   219 val indent_size = 2
   220 val no_label = ("", ~1)
   221 
   222 val raw_prefix = "X"
   223 val assum_prefix = "A"
   224 val fact_prefix = "F"
   225 
   226 fun resolve_conjecture conjecture_shape (num, s_opt) =
   227   let
   228     val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   229               SOME s => Int.fromString s |> the_default ~1
   230             | NONE => case Int.fromString num of
   231                         SOME j => find_index (exists (curry (op =) j))
   232                                              conjecture_shape
   233                       | NONE => ~1
   234   in if k >= 0 then [k] else [] end
   235 
   236 fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
   237 fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   238 
   239 fun raw_label_for_name conjecture_shape name =
   240   case resolve_conjecture conjecture_shape name of
   241     [j] => (conjecture_prefix, j)
   242   | _ => case Int.fromString (fst name) of
   243            SOME j => (raw_prefix, j)
   244          | NONE => (raw_prefix ^ fst name, 0)
   245 
   246 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   247 
   248 exception FO_TERM of string fo_term list
   249 exception FORMULA of (string, string fo_term) formula list
   250 exception SAME of unit
   251 
   252 (* Type variables are given the basic sort "HOL.type". Some will later be
   253    constrained by information from type literals, or by type inference. *)
   254 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   255   let val Ts = map (type_from_fo_term tfrees) us in
   256     case strip_prefix_and_unascii type_const_prefix a of
   257       SOME b => Type (invert_const b, Ts)
   258     | NONE =>
   259       if not (null us) then
   260         raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   261       else case strip_prefix_and_unascii tfree_prefix a of
   262         SOME b =>
   263         let val s = "'" ^ b in
   264           TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   265         end
   266       | NONE =>
   267         case strip_prefix_and_unascii tvar_prefix a of
   268           SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   269         | NONE =>
   270           (* Variable from the ATP, say "X1" *)
   271           Type_Infer.param 0 (a, HOLogic.typeS)
   272   end
   273 
   274 (* Type class literal applied to a type. Returns triple of polarity, class,
   275    type. *)
   276 fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
   277   case (strip_prefix_and_unascii class_prefix a,
   278         map (type_from_fo_term tfrees) us) of
   279     (SOME b, [T]) => (pos, b, T)
   280   | _ => raise FO_TERM [u]
   281 
   282 (** Accumulate type constraints in a formula: negative type literals **)
   283 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   284 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   285   | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   286   | add_type_constraint _ = I
   287 
   288 fun repair_atp_variable_name f s =
   289   let
   290     fun subscript_name s n = s ^ nat_subscript n
   291     val s = String.map f s
   292   in
   293     case space_explode "_" s of
   294       [_] => (case take_suffix Char.isDigit (String.explode s) of
   295                 (cs1 as _ :: _, cs2 as _ :: _) =>
   296                 subscript_name (String.implode cs1)
   297                                (the (Int.fromString (String.implode cs2)))
   298               | (_, _) => s)
   299     | [s1, s2] => (case Int.fromString s2 of
   300                      SOME n => subscript_name s1 n
   301                    | NONE => s)
   302     | _ => s
   303   end
   304 
   305 (* First-order translation. No types are known for variables. "HOLogic.typeT"
   306    should allow them to be inferred. *)
   307 fun raw_term_from_pred thy full_types tfrees =
   308   let
   309     fun aux opt_T extra_us u =
   310       case u of
   311         ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   312       | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   313       | ATerm (a, us) =>
   314         if a = type_wrapper_name then
   315           case us of
   316             [typ_u, term_u] =>
   317             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   318           | _ => raise FO_TERM us
   319         else case strip_prefix_and_unascii const_prefix a of
   320           SOME "equal" =>
   321           let val ts = map (aux NONE []) us in
   322             if length ts = 2 andalso hd ts aconv List.last ts then
   323               (* Vampire is keen on producing these. *)
   324               @{const True}
   325             else
   326               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
   327           end
   328         | SOME b =>
   329           let
   330             val c = invert_const b
   331             val num_type_args = num_type_args thy c
   332             val (type_us, term_us) =
   333               chop (if full_types then 0 else num_type_args) us
   334             (* Extra args from "hAPP" come after any arguments given directly to
   335                the constant. *)
   336             val term_ts = map (aux NONE []) term_us
   337             val extra_ts = map (aux NONE []) extra_us
   338             val t =
   339               Const (c, if full_types then
   340                           case opt_T of
   341                             SOME T => map fastype_of term_ts ---> T
   342                           | NONE =>
   343                             if num_type_args = 0 then
   344                               Sign.const_instance thy (c, [])
   345                             else
   346                               raise Fail ("no type information for " ^ quote c)
   347                         else
   348                           Sign.const_instance thy (c,
   349                               map (type_from_fo_term tfrees) type_us))
   350           in list_comb (t, term_ts @ extra_ts) end
   351         | NONE => (* a free or schematic variable *)
   352           let
   353             val ts = map (aux NONE []) (us @ extra_us)
   354             val T = map fastype_of ts ---> HOLogic.typeT
   355             val t =
   356               case strip_prefix_and_unascii fixed_var_prefix a of
   357                 SOME b => Free (b, T)
   358               | NONE =>
   359                 case strip_prefix_and_unascii schematic_var_prefix a of
   360                   SOME b => Var ((b, 0), T)
   361                 | NONE =>
   362                   if is_atp_variable a then
   363                     Var ((repair_atp_variable_name Char.toLower a, 0), T)
   364                   else
   365                     (* Skolem constants? *)
   366                     Var ((repair_atp_variable_name Char.toUpper a, 0), T)
   367           in list_comb (t, ts) end
   368   in aux (SOME HOLogic.boolT) [] end
   369 
   370 fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
   371   if String.isPrefix class_prefix s then
   372     add_type_constraint (type_constraint_from_term pos tfrees u)
   373     #> pair @{const True}
   374   else
   375     pair (raw_term_from_pred thy full_types tfrees u)
   376 
   377 val combinator_table =
   378   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
   379    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
   380    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
   381    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
   382    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
   383 
   384 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   385   | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   386   | uncombine_term (t as Const (x as (s, _))) =
   387     (case AList.lookup (op =) combinator_table s of
   388        SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   389      | NONE => t)
   390   | uncombine_term t = t
   391 
   392 (* Update schematic type variables with detected sort constraints. It's not
   393    totally clear when this code is necessary. *)
   394 fun repair_tvar_sorts (t, tvar_tab) =
   395   let
   396     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   397       | do_type (TVar (xi, s)) =
   398         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   399       | do_type (TFree z) = TFree z
   400     fun do_term (Const (a, T)) = Const (a, do_type T)
   401       | do_term (Free (a, T)) = Free (a, do_type T)
   402       | do_term (Var (xi, T)) = Var (xi, do_type T)
   403       | do_term (t as Bound _) = t
   404       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   405       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   406   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   407 
   408 fun quantify_over_var quant_of var_s t =
   409   let
   410     val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
   411                   |> map Var
   412   in fold_rev quant_of vars t end
   413 
   414 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
   415    appear in the formula. *)
   416 fun prop_from_formula thy full_types tfrees phi =
   417   let
   418     fun do_formula pos phi =
   419       case phi of
   420         AQuant (_, [], phi) => do_formula pos phi
   421       | AQuant (q, x :: xs, phi') =>
   422         do_formula pos (AQuant (q, xs, phi'))
   423         #>> quantify_over_var (case q of
   424                                  AForall => forall_of
   425                                | AExists => exists_of)
   426                               (repair_atp_variable_name Char.toLower x)
   427       | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
   428       | AConn (c, [phi1, phi2]) =>
   429         do_formula (pos |> c = AImplies ? not) phi1
   430         ##>> do_formula pos phi2
   431         #>> (case c of
   432                AAnd => s_conj
   433              | AOr => s_disj
   434              | AImplies => s_imp
   435              | AIf => s_imp o swap
   436              | AIff => s_iff
   437              | ANotIff => s_not o s_iff)
   438       | AAtom tm => term_from_pred thy full_types tfrees pos tm
   439       | _ => raise FORMULA [phi]
   440   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   441 
   442 fun check_formula ctxt =
   443   Type.constraint HOLogic.boolT
   444   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   445 
   446 
   447 (**** Translation of TSTP files to Isar Proofs ****)
   448 
   449 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   450   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   451 
   452 fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
   453     let
   454       val thy = ProofContext.theory_of ctxt
   455       val t1 = prop_from_formula thy full_types tfrees phi1
   456       val vars = snd (strip_comb t1)
   457       val frees = map unvarify_term vars
   458       val unvarify_args = subst_atomic (vars ~~ frees)
   459       val t2 = prop_from_formula thy full_types tfrees phi2
   460       val (t1, t2) =
   461         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   462         |> unvarify_args |> uncombine_term |> check_formula ctxt
   463         |> HOLogic.dest_eq
   464     in
   465       (Definition (name, t1, t2),
   466        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   467     end
   468   | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
   469     let
   470       val thy = ProofContext.theory_of ctxt
   471       val t = u |> prop_from_formula thy full_types tfrees
   472                 |> uncombine_term |> check_formula ctxt
   473     in
   474       (Inference (name, t, deps),
   475        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   476     end
   477 fun decode_lines ctxt full_types tfrees lines =
   478   fst (fold_map (decode_line full_types tfrees) lines ctxt)
   479 
   480 fun is_same_inference _ (Definition _) = false
   481   | is_same_inference t (Inference (_, t', _)) = t aconv t'
   482 
   483 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   484    clsarity). *)
   485 val is_only_type_information = curry (op aconv) HOLogic.true_const
   486 
   487 fun replace_one_dependency (old, new) dep =
   488   if is_same_step (dep, old) then new else [dep]
   489 fun replace_dependencies_in_line _ (line as Definition _) = line
   490   | replace_dependencies_in_line p (Inference (name, t, deps)) =
   491     Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   492 
   493 (* Discard axioms; consolidate adjacent lines that prove the same formula, since
   494    they differ only in type information.*)
   495 fun add_line _ _ (line as Definition _) lines = line :: lines
   496   | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
   497     (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
   498        definitions. *)
   499     if is_axiom axiom_names name then
   500       (* Axioms are not proof lines. *)
   501       if is_only_type_information t then
   502         map (replace_dependencies_in_line (name, [])) lines
   503       (* Is there a repetition? If so, replace later line by earlier one. *)
   504       else case take_prefix (not o is_same_inference t) lines of
   505         (_, []) => lines (* no repetition of proof line *)
   506       | (pre, Inference (name', _, _) :: post) =>
   507         pre @ map (replace_dependencies_in_line (name', [name])) post
   508     else if is_conjecture conjecture_shape name then
   509       Inference (name, negate_term t, []) :: lines
   510     else
   511       map (replace_dependencies_in_line (name, [])) lines
   512   | add_line _ _ (Inference (name, t, deps)) lines =
   513     (* Type information will be deleted later; skip repetition test. *)
   514     if is_only_type_information t then
   515       Inference (name, t, deps) :: lines
   516     (* Is there a repetition? If so, replace later line by earlier one. *)
   517     else case take_prefix (not o is_same_inference t) lines of
   518       (* FIXME: Doesn't this code risk conflating proofs involving different
   519          types? *)
   520        (_, []) => Inference (name, t, deps) :: lines
   521      | (pre, Inference (name', t', _) :: post) =>
   522        Inference (name, t', deps) ::
   523        pre @ map (replace_dependencies_in_line (name', [name])) post
   524 
   525 (* Recursively delete empty lines (type information) from the proof. *)
   526 fun add_nontrivial_line (Inference (name, t, [])) lines =
   527     if is_only_type_information t then delete_dependency name lines
   528     else Inference (name, t, []) :: lines
   529   | add_nontrivial_line line lines = line :: lines
   530 and delete_dependency name lines =
   531   fold_rev add_nontrivial_line
   532            (map (replace_dependencies_in_line (name, [])) lines) []
   533 
   534 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   535    offending lines often does the trick. *)
   536 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   537   | is_bad_free _ _ = false
   538 
   539 fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
   540     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   541   | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
   542                      (Inference (name, t, deps)) (j, lines) =
   543     (j + 1,
   544      if is_axiom axiom_names name orelse
   545         is_conjecture conjecture_shape name orelse
   546         (* the last line must be kept *)
   547         j = 0 orelse
   548         (not (is_only_type_information t) andalso
   549          null (Term.add_tvars t []) andalso
   550          not (exists_subterm (is_bad_free frees) t) andalso
   551          length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
   552          (* kill next to last line, which usually results in a trivial step *)
   553          j <> 1) then
   554        Inference (name, t, deps) :: lines  (* keep line *)
   555      else
   556        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   557 
   558 (** Isar proof construction and manipulation **)
   559 
   560 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   561   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   562 
   563 type label = string * int
   564 type facts = label list * string list
   565 
   566 datatype isar_qualifier = Show | Then | Moreover | Ultimately
   567 
   568 datatype isar_step =
   569   Fix of (string * typ) list |
   570   Let of term * term |
   571   Assume of label * term |
   572   Have of isar_qualifier list * label * term * byline
   573 and byline =
   574   ByMetis of facts |
   575   CaseSplit of isar_step list list * facts
   576 
   577 fun smart_case_split [] facts = ByMetis facts
   578   | smart_case_split proofs facts = CaseSplit (proofs, facts)
   579 
   580 fun add_fact_from_dependency conjecture_shape axiom_names name =
   581   if is_axiom axiom_names name then
   582     apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
   583   else
   584     apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   585 
   586 fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   587   | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   588     Assume (raw_label_for_name conjecture_shape name, t)
   589   | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
   590     Have (if j = 1 then [Show] else [],
   591           raw_label_for_name conjecture_shape name,
   592           fold_rev forall_of (map Var (Term.add_vars t [])) t,
   593           ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   594                         deps ([], [])))
   595 
   596 fun repair_name "$true" = "c_True"
   597   | repair_name "$false" = "c_False"
   598   | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
   599   | repair_name "equal" = "c_equal" (* needed by SPASS? *)
   600   | repair_name s =
   601     if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   602       "c_equal" (* seen in Vampire proofs *)
   603     else
   604       s
   605 
   606 fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   607         tstplike_proof conjecture_shape axiom_names params frees =
   608   let
   609     val lines =
   610       tstplike_proof
   611       |> atp_proof_from_tstplike_string
   612       |> nasty_atp_proof pool
   613       |> map_term_names_in_atp_proof repair_name
   614       |> decode_lines ctxt full_types tfrees
   615       |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   616       |> rpair [] |-> fold_rev add_nontrivial_line
   617       |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   618                                              conjecture_shape axiom_names frees)
   619       |> snd
   620   in
   621     (if null params then [] else [Fix params]) @
   622     map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
   623          lines
   624   end
   625 
   626 (* When redirecting proofs, we keep information about the labels seen so far in
   627    the "backpatches" data structure. The first component indicates which facts
   628    should be associated with forthcoming proof steps. The second component is a
   629    pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   630    become assumptions and "drop_ls" are the labels that should be dropped in a
   631    case split. *)
   632 type backpatches = (label * facts) list * (label list * label list)
   633 
   634 fun used_labels_of_step (Have (_, _, _, by)) =
   635     (case by of
   636        ByMetis (ls, _) => ls
   637      | CaseSplit (proofs, (ls, _)) =>
   638        fold (union (op =) o used_labels_of) proofs ls)
   639   | used_labels_of_step _ = []
   640 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   641 
   642 fun new_labels_of_step (Fix _) = []
   643   | new_labels_of_step (Let _) = []
   644   | new_labels_of_step (Assume (l, _)) = [l]
   645   | new_labels_of_step (Have (_, l, _, _)) = [l]
   646 val new_labels_of = maps new_labels_of_step
   647 
   648 val join_proofs =
   649   let
   650     fun aux _ [] = NONE
   651       | aux proof_tail (proofs as (proof1 :: _)) =
   652         if exists null proofs then
   653           NONE
   654         else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   655           aux (hd proof1 :: proof_tail) (map tl proofs)
   656         else case hd proof1 of
   657           Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   658           if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   659                       | _ => false) (tl proofs) andalso
   660              not (exists (member (op =) (maps new_labels_of proofs))
   661                          (used_labels_of proof_tail)) then
   662             SOME (l, t, map rev proofs, proof_tail)
   663           else
   664             NONE
   665         | _ => NONE
   666   in aux [] o map rev end
   667 
   668 fun case_split_qualifiers proofs =
   669   case length proofs of
   670     0 => []
   671   | 1 => [Then]
   672   | _ => [Ultimately]
   673 
   674 fun redirect_proof hyp_ts concl_t proof =
   675   let
   676     (* The first pass outputs those steps that are independent of the negated
   677        conjecture. The second pass flips the proof by contradiction to obtain a
   678        direct proof, introducing case splits when an inference depends on
   679        several facts that depend on the negated conjecture. *)
   680      val concl_l = (conjecture_prefix, length hyp_ts)
   681      fun first_pass ([], contra) = ([], contra)
   682        | first_pass ((step as Fix _) :: proof, contra) =
   683          first_pass (proof, contra) |>> cons step
   684        | first_pass ((step as Let _) :: proof, contra) =
   685          first_pass (proof, contra) |>> cons step
   686        | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
   687          if l = concl_l then first_pass (proof, contra ||> cons step)
   688          else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
   689        | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   690          let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   691            if exists (member (op =) (fst contra)) ls then
   692              first_pass (proof, contra |>> cons l ||> cons step)
   693            else
   694              first_pass (proof, contra) |>> cons step
   695          end
   696        | first_pass _ = raise Fail "malformed proof"
   697     val (proof_top, (contra_ls, contra_proof)) =
   698       first_pass (proof, ([concl_l], []))
   699     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   700     fun backpatch_labels patches ls =
   701       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   702     fun second_pass end_qs ([], assums, patches) =
   703         ([Have (end_qs, no_label, concl_t,
   704                 ByMetis (backpatch_labels patches (map snd assums)))], patches)
   705       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   706         second_pass end_qs (proof, (t, l) :: assums, patches)
   707       | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   708                             patches) =
   709         (if member (op =) (snd (snd patches)) l andalso
   710             not (member (op =) (fst (snd patches)) l) andalso
   711             not (AList.defined (op =) (fst patches) l) then
   712            second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   713          else case List.partition (member (op =) contra_ls) ls of
   714            ([contra_l], co_ls) =>
   715            if member (op =) qs Show then
   716              second_pass end_qs (proof, assums,
   717                                  patches |>> cons (contra_l, (co_ls, ss)))
   718            else
   719              second_pass end_qs
   720                          (proof, assums,
   721                           patches |>> cons (contra_l, (l :: co_ls, ss)))
   722              |>> cons (if member (op =) (fst (snd patches)) l then
   723                          Assume (l, negate_term t)
   724                        else
   725                          Have (qs, l, negate_term t,
   726                                ByMetis (backpatch_label patches l)))
   727          | (contra_ls as _ :: _, co_ls) =>
   728            let
   729              val proofs =
   730                map_filter
   731                    (fn l =>
   732                        if l = concl_l then
   733                          NONE
   734                        else
   735                          let
   736                            val drop_ls = filter (curry (op <>) l) contra_ls
   737                          in
   738                            second_pass []
   739                                (proof, assums,
   740                                 patches ||> apfst (insert (op =) l)
   741                                         ||> apsnd (union (op =) drop_ls))
   742                            |> fst |> SOME
   743                          end) contra_ls
   744              val (assumes, facts) =
   745                if member (op =) (fst (snd patches)) l then
   746                  ([Assume (l, negate_term t)], (l :: co_ls, ss))
   747                else
   748                  ([], (co_ls, ss))
   749            in
   750              (case join_proofs proofs of
   751                 SOME (l, t, proofs, proof_tail) =>
   752                 Have (case_split_qualifiers proofs @
   753                       (if null proof_tail then end_qs else []), l, t,
   754                       smart_case_split proofs facts) :: proof_tail
   755               | NONE =>
   756                 [Have (case_split_qualifiers proofs @ end_qs, no_label,
   757                        concl_t, smart_case_split proofs facts)],
   758               patches)
   759              |>> append assumes
   760            end
   761          | _ => raise Fail "malformed proof")
   762        | second_pass _ _ = raise Fail "malformed proof"
   763     val proof_bottom =
   764       second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   765   in proof_top @ proof_bottom end
   766 
   767 (* FIXME: Still needed? Probably not. *)
   768 val kill_duplicate_assumptions_in_proof =
   769   let
   770     fun relabel_facts subst =
   771       apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   772     fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   773         (case AList.lookup (op aconv) assums t of
   774            SOME l' => (proof, (l, l') :: subst, assums)
   775          | NONE => (step :: proof, subst, (t, l) :: assums))
   776       | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   777         (Have (qs, l, t,
   778                case by of
   779                  ByMetis facts => ByMetis (relabel_facts subst facts)
   780                | CaseSplit (proofs, facts) =>
   781                  CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   782          proof, subst, assums)
   783       | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   784     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   785   in do_proof end
   786 
   787 val then_chain_proof =
   788   let
   789     fun aux _ [] = []
   790       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   791       | aux l' (Have (qs, l, t, by) :: proof) =
   792         (case by of
   793            ByMetis (ls, ss) =>
   794            Have (if member (op =) ls l' then
   795                    (Then :: qs, l, t,
   796                     ByMetis (filter_out (curry (op =) l') ls, ss))
   797                  else
   798                    (qs, l, t, ByMetis (ls, ss)))
   799          | CaseSplit (proofs, facts) =>
   800            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   801         aux l proof
   802       | aux _ (step :: proof) = step :: aux no_label proof
   803   in aux no_label end
   804 
   805 fun kill_useless_labels_in_proof proof =
   806   let
   807     val used_ls = used_labels_of proof
   808     fun do_label l = if member (op =) used_ls l then l else no_label
   809     fun do_step (Assume (l, t)) = Assume (do_label l, t)
   810       | do_step (Have (qs, l, t, by)) =
   811         Have (qs, do_label l, t,
   812               case by of
   813                 CaseSplit (proofs, facts) =>
   814                 CaseSplit (map (map do_step) proofs, facts)
   815               | _ => by)
   816       | do_step step = step
   817   in map do_step proof end
   818 
   819 fun prefix_for_depth n = replicate_string (n + 1)
   820 
   821 val relabel_proof =
   822   let
   823     fun aux _ _ _ [] = []
   824       | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   825         if l = no_label then
   826           Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   827         else
   828           let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   829             Assume (l', t) ::
   830             aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   831           end
   832       | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   833         let
   834           val (l', subst, next_fact) =
   835             if l = no_label then
   836               (l, subst, next_fact)
   837             else
   838               let
   839                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
   840               in (l', (l, l') :: subst, next_fact + 1) end
   841           val relabel_facts =
   842             apfst (maps (the_list o AList.lookup (op =) subst))
   843           val by =
   844             case by of
   845               ByMetis facts => ByMetis (relabel_facts facts)
   846             | CaseSplit (proofs, facts) =>
   847               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   848                          relabel_facts facts)
   849         in
   850           Have (qs, l', t, by) ::
   851           aux subst depth (next_assum, next_fact) proof
   852         end
   853       | aux subst depth nextp (step :: proof) =
   854         step :: aux subst depth nextp proof
   855   in aux [] 0 (1, 1) end
   856 
   857 fun string_for_proof ctxt0 full_types i n =
   858   let
   859     val ctxt = ctxt0
   860       |> Config.put show_free_types false
   861       |> Config.put show_types true
   862     fun fix_print_mode f x =
   863       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   864                                (print_mode_value ())) f x
   865     fun do_indent ind = replicate_string (ind * indent_size) " "
   866     fun do_free (s, T) =
   867       maybe_quote s ^ " :: " ^
   868       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   869     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   870     fun do_have qs =
   871       (if member (op =) qs Moreover then "moreover " else "") ^
   872       (if member (op =) qs Ultimately then "ultimately " else "") ^
   873       (if member (op =) qs Then then
   874          if member (op =) qs Show then "thus" else "hence"
   875        else
   876          if member (op =) qs Show then "show" else "have")
   877     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   878     fun do_facts (ls, ss) =
   879       metis_command full_types 1 1
   880                     (ls |> sort_distinct (prod_ord string_ord int_ord),
   881                      ss |> sort_distinct string_ord)
   882     and do_step ind (Fix xs) =
   883         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   884       | do_step ind (Let (t1, t2)) =
   885         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   886       | do_step ind (Assume (l, t)) =
   887         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   888       | do_step ind (Have (qs, l, t, ByMetis facts)) =
   889         do_indent ind ^ do_have qs ^ " " ^
   890         do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   891       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   892         space_implode (do_indent ind ^ "moreover\n")
   893                       (map (do_block ind) proofs) ^
   894         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   895         do_facts facts ^ "\n"
   896     and do_steps prefix suffix ind steps =
   897       let val s = implode (map (do_step ind) steps) in
   898         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   899         String.extract (s, ind * indent_size,
   900                         SOME (size s - ind * indent_size - 1)) ^
   901         suffix ^ "\n"
   902       end
   903     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   904     (* One-step proofs are pointless; better use the Metis one-liner
   905        directly. *)
   906     and do_proof [Have (_, _, _, ByMetis _)] = ""
   907       | do_proof proof =
   908         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   909         do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   910         (if n <> 1 then "next" else "qed")
   911   in do_proof end
   912 
   913 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   914                     (other_params as (_, full_types, _, tstplike_proof,
   915                                       axiom_names, goal, i)) =
   916   let
   917     val (params, hyp_ts, concl_t) = strip_subgoal goal i
   918     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   919     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   920     val n = Logic.count_prems (prop_of goal)
   921     val (one_line_proof, lemma_names) = metis_proof_text other_params
   922     fun isar_proof_for () =
   923       case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   924                isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   925                params frees
   926            |> redirect_proof hyp_ts concl_t
   927            |> kill_duplicate_assumptions_in_proof
   928            |> then_chain_proof
   929            |> kill_useless_labels_in_proof
   930            |> relabel_proof
   931            |> string_for_proof ctxt full_types i n of
   932         "" => "\nNo structured proof available."
   933       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   934     val isar_proof =
   935       if debug then
   936         isar_proof_for ()
   937       else
   938         try isar_proof_for ()
   939         |> the_default "\nWarning: The Isar proof construction failed."
   940   in (one_line_proof ^ isar_proof, lemma_names) end
   941 
   942 fun proof_text isar_proof isar_params other_params =
   943   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   944       other_params
   945 
   946 end;