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