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