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