src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
author blanchet
Thu Apr 29 01:17:14 2010 +0200 (2010-04-29)
changeset 36555 8ff45c2076da
parent 36551 cc42df660808
child 36556 81dc2c20f052
permissions -rw-r--r--
expand combinators in Isar proofs constructed by Sledgehammer;
this requires shuffling around a couple of functions previously defined in Refute
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
     2     Author:     Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Transfer of proofs from external provers.
     6 *)
     7 
     8 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     9 sig
    10   type minimize_command = string list -> string
    11   type name_pool = Sledgehammer_FOL_Clause.name_pool
    12 
    13   val chained_hint: string
    14   val invert_const: string -> string
    15   val invert_type_const: string -> string
    16   val num_typargs: theory -> string -> int
    17   val make_tvar: string -> typ
    18   val strip_prefix: string -> string -> string option
    19   val metis_line: int -> int -> string list -> string
    20   val metis_proof_text:
    21     minimize_command * string * string vector * thm * int
    22     -> string * string list
    23   val isar_proof_text:
    24     name_pool option * bool * int * Proof.context * int list list
    25     -> minimize_command * string * string vector * thm * int
    26     -> string * string list
    27   val proof_text:
    28     bool -> name_pool option * bool * int * Proof.context * int list list
    29     -> minimize_command * string * string vector * thm * int
    30     -> string * string list
    31 end;
    32 
    33 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    34 struct
    35 
    36 open Sledgehammer_Util
    37 open Sledgehammer_FOL_Clause
    38 open Sledgehammer_Fact_Preprocessor
    39 
    40 type minimize_command = string list -> string
    41 
    42 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    43 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    44 
    45 (* Hack: Could return false positives (e.g., a user happens to declare a
    46    constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
    47 val is_skolem_const_name =
    48   Long_Name.base_name
    49   #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
    50 
    51 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
    52 val index_in_shape = find_index o exists o curry (op =)
    53 
    54 fun ugly_name NONE s = s
    55   | ugly_name (SOME the_pool) s =
    56     case Symtab.lookup (snd the_pool) s of
    57       SOME s' => s'
    58     | NONE => s
    59 
    60 fun smart_lambda v t =
    61   Abs (case v of
    62          Const (s, _) =>
    63          List.last (space_explode skolem_infix (Long_Name.base_name s))
    64        | Var ((s, _), _) => s
    65        | Free (s, _) => s
    66        | _ => "", fastype_of v, abstract_over (v, t))
    67 fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
    68 
    69 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
    70   Definition of 'a * 'b * 'c |
    71   Inference of 'a * 'd * 'e list
    72 
    73 (**** PARSING OF TSTP FORMAT ****)
    74 
    75 fun strip_spaces_in_list [] = ""
    76   | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
    77   | strip_spaces_in_list [c1, c2] =
    78     strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
    79   | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
    80     if Char.isSpace c1 then
    81       strip_spaces_in_list (c2 :: c3 :: cs)
    82     else if Char.isSpace c2 then
    83       if Char.isSpace c3 then
    84         strip_spaces_in_list (c1 :: c3 :: cs)
    85       else
    86         str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    87         strip_spaces_in_list (c3 :: cs)
    88     else
    89       str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    90 val strip_spaces = strip_spaces_in_list o String.explode
    91 
    92 (* Syntax trees, either term list or formulae *)
    93 datatype node = IntLeaf of int | StrNode of string * node list
    94 
    95 fun str_leaf s = StrNode (s, [])
    96 
    97 fun scons (x, y) = StrNode ("cons", [x, y])
    98 val slist_of = List.foldl scons (str_leaf "nil")
    99 
   100 (*Strings enclosed in single quotes, e.g. filenames*)
   101 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
   102 
   103 (*Integer constants, typically proof line numbers*)
   104 val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
   105 
   106 val parse_dollar_name =
   107   Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
   108 
   109 (* needed for SPASS's output format *)
   110 fun repair_name _ "$true" = "c_True"
   111   | repair_name _ "$false" = "c_False"
   112   | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
   113   | repair_name _ "equal" = "c_equal" (* probably not needed *)
   114   | repair_name pool s = ugly_name pool s
   115 (* Generalized first-order terms, which include file names, numbers, etc. *)
   116 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
   117    forever at compile time. *)
   118 fun parse_term pool x =
   119      (parse_quoted >> str_leaf
   120    || parse_integer >> IntLeaf
   121    || (parse_dollar_name >> repair_name pool)
   122       -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
   123    || $$ "(" |-- parse_term pool --| $$ ")"
   124    || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
   125 and parse_terms pool x =
   126   (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
   127 
   128 fun negate_node u = StrNode ("c_Not", [u])
   129 fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
   130 
   131 (* Apply equal or not-equal to a term. *)
   132 fun repair_predicate_term (u, NONE) = u
   133   | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
   134   | repair_predicate_term (u1, SOME (SOME _, u2)) =
   135     negate_node (equate_nodes u1 u2)
   136 fun parse_predicate_term pool =
   137   parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
   138                                   -- parse_term pool)
   139   >> repair_predicate_term
   140 fun parse_literal pool x =
   141   ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
   142 fun parse_literals pool =
   143   parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
   144 fun parse_parenthesized_literals pool =
   145   $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
   146 fun parse_clause pool =
   147   parse_parenthesized_literals pool
   148     ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
   149   >> List.concat
   150 
   151 fun ints_of_node (IntLeaf n) = cons n
   152   | ints_of_node (StrNode (_, us)) = fold ints_of_node us
   153 val parse_tstp_annotations =
   154   Scan.optional ($$ "," |-- parse_term NONE
   155                    --| Scan.option ($$ "," |-- parse_terms NONE)
   156                  >> (fn source => ints_of_node source [])) []
   157 
   158 fun parse_definition pool =
   159   $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
   160   -- parse_clause pool --| $$ ")"
   161 
   162 (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
   163    The <num> could be an identifier, but we assume integers. *)
   164 fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
   165 fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
   166 fun parse_tstp_line pool =
   167      ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
   168        --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
   169        --| parse_tstp_annotations --| $$ ")" --| $$ "."
   170       >> finish_tstp_definition_line)
   171   || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
   172        --| Symbol.scan_id --| $$ "," -- parse_clause pool
   173        -- parse_tstp_annotations --| $$ ")" --| $$ "."
   174       >> finish_tstp_inference_line)
   175 
   176 (**** PARSING OF SPASS OUTPUT ****)
   177 
   178 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
   179    is not clear anyway. *)
   180 val parse_dot_name = parse_integer --| $$ "." --| parse_integer
   181 
   182 val parse_spass_annotations =
   183   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
   184                                          --| Scan.option ($$ ","))) []
   185 
   186 (* It is not clear why some literals are followed by sequences of stars. We
   187    ignore them. *)
   188 fun parse_starred_predicate_term pool =
   189   parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
   190 
   191 fun parse_horn_clause pool =
   192   Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
   193   -- Scan.repeat (parse_starred_predicate_term pool)
   194   >> (fn ([], []) => [str_leaf "c_False"]
   195        | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
   196 
   197 (* Syntax: <num>[0:<inference><annotations>] ||
   198            <cnf_formulas> -> <cnf_formulas>. *)
   199 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
   200 fun parse_spass_line pool =
   201   parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   202   -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
   203   -- parse_horn_clause pool --| $$ "."
   204   >> finish_spass_line
   205 
   206 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
   207 fun parse_lines pool = Scan.repeat1 (parse_line pool)
   208 fun parse_proof pool =
   209   fst o Scan.finite Symbol.stopper
   210             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
   211                             (parse_lines pool)))
   212   o explode o strip_spaces
   213 
   214 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   215 
   216 exception NODE of node
   217 
   218 (*If string s has the prefix s1, return the result of deleting it.*)
   219 fun strip_prefix s1 s =
   220   if String.isPrefix s1 s
   221   then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
   222   else NONE;
   223 
   224 (*Invert the table of translations between Isabelle and ATPs*)
   225 val type_const_trans_table_inv =
   226       Symtab.make (map swap (Symtab.dest type_const_trans_table));
   227 
   228 fun invert_type_const c =
   229     case Symtab.lookup type_const_trans_table_inv c of
   230         SOME c' => c'
   231       | NONE => c;
   232 
   233 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS);
   234 fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS)
   235 fun make_var (b,T) = Var((b,0),T);
   236 
   237 (*Type variables are given the basic sort, HOL.type. Some will later be constrained
   238   by information from type literals, or by type inference.*)
   239 fun type_of_node (u as IntLeaf _) = raise NODE u
   240   | type_of_node (u as StrNode (a, us)) =
   241     let val Ts = map type_of_node us in
   242       case strip_prefix tconst_prefix a of
   243         SOME b => Type (invert_type_const b, Ts)
   244       | NONE =>
   245         if not (null us) then
   246           raise NODE u  (*only tconsts have type arguments*)
   247         else case strip_prefix tfree_prefix a of
   248           SOME b => TFree ("'" ^ b, HOLogic.typeS)
   249         | NONE =>
   250           case strip_prefix tvar_prefix a of
   251             SOME b => make_tvar b
   252           | NONE => make_tparam a  (* Variable from the ATP, say "X1" *)
   253     end
   254 
   255 (*Invert the table of translations between Isabelle and ATPs*)
   256 val const_trans_table_inv =
   257   Symtab.update ("fequal", @{const_name "op ="})
   258                 (Symtab.make (map swap (Symtab.dest const_trans_table)))
   259 
   260 fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
   261 
   262 (*The number of type arguments of a constant, zero if it's monomorphic*)
   263 fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s));
   264 
   265 (*Generates a constant, given its type arguments*)
   266 fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts));
   267 
   268 fun fix_atp_variable_name s =
   269   let
   270     fun subscript_name s n = s ^ nat_subscript n
   271     val s = String.map Char.toLower s
   272   in
   273     case space_explode "_" s of
   274       [_] => (case take_suffix Char.isDigit (String.explode s) of
   275                 (cs1 as _ :: _, cs2 as _ :: _) =>
   276                 subscript_name (String.implode cs1)
   277                                (the (Int.fromString (String.implode cs2)))
   278               | (_, _) => s)
   279     | [s1, s2] => (case Int.fromString s2 of
   280                      SOME n => subscript_name s1 n
   281                    | NONE => s)
   282     | _ => s
   283   end
   284 
   285 (*First-order translation. No types are known for variables. HOLogic.typeT should allow
   286   them to be inferred.*)
   287 fun term_of_node args thy u =
   288   case u of
   289     IntLeaf _ => raise NODE u
   290   | StrNode ("hBOOL", [u]) => term_of_node [] thy u  (* ignore hBOOL *)
   291   | StrNode ("hAPP", [u1, u2]) => term_of_node (u2 :: args) thy u1
   292   | StrNode (a, us) =>
   293     case strip_prefix const_prefix a of
   294       SOME "equal" =>
   295       list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
   296                  map (term_of_node [] thy) us)
   297     | SOME b =>
   298       let
   299         val c = invert_const b
   300         val nterms = length us - num_typargs thy c
   301         val ts = map (term_of_node [] thy) (take nterms us @ args)
   302         (*Extra args from hAPP come AFTER any arguments given directly to the
   303           constant.*)
   304         val Ts = map type_of_node (drop nterms us)
   305       in list_comb(const_of thy (c, Ts), ts) end
   306     | NONE => (*a variable, not a constant*)
   307       let
   308         val opr =
   309           (* a Free variable is typically a Skolem function *)
   310           case strip_prefix fixed_var_prefix a of
   311             SOME b => Free (b, HOLogic.typeT)
   312           | NONE =>
   313             case strip_prefix schematic_var_prefix a of
   314               SOME b => make_var (b, HOLogic.typeT)
   315             | NONE =>
   316               (* Variable from the ATP, say "X1" *)
   317               make_var (fix_atp_variable_name a, HOLogic.typeT)
   318       in list_comb (opr, map (term_of_node [] thy) (us @ args)) end
   319 
   320 (* Type class literal applied to a type. Returns triple of polarity, class,
   321    type. *)
   322 fun constraint_of_node pos (StrNode ("c_Not", [u])) =
   323     constraint_of_node (not pos) u
   324   | constraint_of_node pos u = case u of
   325         IntLeaf _ => raise NODE u
   326       | StrNode (a, us) =>
   327             (case (strip_prefix class_prefix a, map type_of_node us) of
   328                  (SOME b, [T]) => (pos, b, T)
   329                | _ => raise NODE u)
   330 
   331 (** Accumulate type constraints in a clause: negative type literals **)
   332 
   333 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   334 
   335 fun add_constraint ((false, cl, TFree(a,_)), vt) = add_var ((a,~1),cl) vt
   336   | add_constraint ((false, cl, TVar(ix,_)), vt) = add_var (ix,cl) vt
   337   | add_constraint (_, vt) = vt;
   338 
   339 fun is_positive_literal (@{const Not} $ _) = false
   340   | is_positive_literal t = true
   341 
   342 fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
   343     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
   344   | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
   345     Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
   346   | negate_term thy (@{const "op -->"} $ t1 $ t2) =
   347     @{const "op &"} $ t1 $ negate_term thy t2
   348   | negate_term thy (@{const "op &"} $ t1 $ t2) =
   349     @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
   350   | negate_term thy (@{const "op |"} $ t1 $ t2) =
   351     @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
   352   | negate_term _ (@{const Not} $ t) = t
   353   | negate_term _ t = @{const Not} $ t
   354 
   355 fun clause_for_literals _ [] = HOLogic.false_const
   356   | clause_for_literals _ [lit] = lit
   357   | clause_for_literals thy lits =
   358     case List.partition is_positive_literal lits of
   359       (pos_lits as _ :: _, neg_lits as _ :: _) =>
   360       @{const "op -->"}
   361           $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
   362           $ foldr1 HOLogic.mk_disj pos_lits
   363     | _ => foldr1 HOLogic.mk_disj lits
   364 
   365 (* Final treatment of the list of "real" literals from a clause.
   366    No "real" literals means only type information. *)
   367 fun finish_clause _ [] = HOLogic.true_const
   368   | finish_clause thy lits =
   369     lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
   370          |> clause_for_literals thy
   371 
   372 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   373 fun lits_of_nodes thy (vt, lits) [] = (vt, finish_clause thy lits)
   374   | lits_of_nodes thy (vt, lits) (u :: us) =
   375     lits_of_nodes thy (add_constraint (constraint_of_node true u, vt), lits) us
   376     handle NODE _ => lits_of_nodes thy (vt, term_of_node [] thy u :: lits) us
   377 
   378 (*Update TVars/TFrees with detected sort constraints.*)
   379 fun repair_sorts vt =
   380   let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
   381         | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
   382         | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
   383       fun tmsubst (Const (a, T)) = Const (a, tysubst T)
   384         | tmsubst (Free (a, T)) = Free (a, tysubst T)
   385         | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
   386         | tmsubst (t as Bound _) = t
   387         | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
   388         | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
   389   in not (Vartab.is_empty vt) ? tmsubst end
   390 
   391 fun unskolemize_term t =
   392   fold forall_of (Term.add_consts t []
   393                  |> filter (is_skolem_const_name o fst) |> map Const) t
   394 
   395 val combinator_table =
   396   [(@{const_name COMBI}, @{thm COMBI_def_raw}),
   397    (@{const_name COMBK}, @{thm COMBK_def_raw}),
   398    (@{const_name COMBB}, @{thm COMBB_def_raw}),
   399    (@{const_name COMBC}, @{thm COMBC_def_raw}),
   400    (@{const_name COMBS}, @{thm COMBS_def_raw})]
   401 
   402 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   403   | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   404   | uncombine_term (t as Const (x as (s, _))) =
   405     (case AList.lookup (op =) combinator_table s of
   406        SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   407      | NONE => t)
   408   | uncombine_term t = t
   409 
   410 (* Interpret a list of syntax trees as a clause, given by "real" literals and
   411    sort constraints. "vt" holds the initial sort constraints, from the
   412    conjecture clauses. *)
   413 fun clause_of_nodes ctxt vt us =
   414   let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
   415     t |> repair_sorts vt
   416   end
   417 fun check_clause ctxt =
   418   TypeInfer.constrain HOLogic.boolT
   419   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   420 
   421 (** Global sort constraints on TFrees (from tfree_tcs) are positive unit
   422     clauses. **)
   423 
   424 fun add_tfree_constraint (true, cl, TFree (a, _)) = add_var ((a, ~1), cl)
   425   | add_tfree_constraint _ = I
   426 fun tfree_constraints_of_clauses vt [] = vt
   427   | tfree_constraints_of_clauses vt ([lit] :: uss) =
   428     (tfree_constraints_of_clauses (add_tfree_constraint
   429                                           (constraint_of_node true lit) vt) uss
   430      handle NODE _ => (* Not a positive type constraint? Ignore the literal. *)
   431      tfree_constraints_of_clauses vt uss)
   432   | tfree_constraints_of_clauses vt (_ :: uss) =
   433     tfree_constraints_of_clauses vt uss
   434 
   435 
   436 (**** Translation of TSTP files to Isar Proofs ****)
   437 
   438 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   439   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   440 
   441 fun clauses_in_lines (Definition (_, u, us)) = u :: us
   442   | clauses_in_lines (Inference (_, us, _)) = us
   443 
   444 fun decode_line vt (Definition (num, u, us)) ctxt =
   445     let
   446       val t1 = clause_of_nodes ctxt vt [u]
   447       val vars = snd (strip_comb t1)
   448       val frees = map unvarify_term vars
   449       val unvarify_args = subst_atomic (vars ~~ frees)
   450       val t2 = clause_of_nodes ctxt vt us
   451       val (t1, t2) =
   452         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   453         |> unvarify_args |> uncombine_term |> check_clause ctxt
   454         |> HOLogic.dest_eq
   455     in
   456       (Definition (num, t1, t2),
   457        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   458     end
   459   | decode_line vt (Inference (num, us, deps)) ctxt =
   460     let
   461       val t = us |> clause_of_nodes ctxt vt
   462                  |> unskolemize_term |> uncombine_term |> check_clause ctxt
   463     in
   464       (Inference (num, t, deps),
   465        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   466     end
   467 fun decode_lines ctxt lines =
   468   let
   469     val vt = tfree_constraints_of_clauses Vartab.empty
   470                                           (map clauses_in_lines lines)
   471   in #1 (fold_map (decode_line vt) lines ctxt) end
   472 
   473 fun aint_inference _ (Definition _) = true
   474   | aint_inference t (Inference (_, t', _)) = not (t aconv t')
   475 
   476 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   477    clsarity). *)
   478 val is_only_type_information = curry (op aconv) HOLogic.true_const
   479 
   480 fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
   481 fun replace_deps_in_line _ (line as Definition _) = line
   482   | replace_deps_in_line p (Inference (num, t, deps)) =
   483     Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
   484 
   485 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   486   only in type information.*)
   487 fun add_line _ _ (line as Definition _) lines = line :: lines
   488   | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
   489     (* No dependencies: axiom, conjecture clause, or internal axioms
   490        (Vampire). *)
   491     if is_axiom_clause_number thm_names num then
   492       (* Axioms are not proof lines. *)
   493       if is_only_type_information t then
   494         map (replace_deps_in_line (num, [])) lines
   495       (* Is there a repetition? If so, replace later line by earlier one. *)
   496       else case take_prefix (aint_inference t) lines of
   497         (_, []) => lines (*no repetition of proof line*)
   498       | (pre, Inference (num', _, _) :: post) =>
   499         pre @ map (replace_deps_in_line (num', [num])) post
   500     else if index_in_shape num conjecture_shape >= 0 then
   501       Inference (num, t, []) :: lines
   502     else
   503       lines
   504   | add_line _ _ (Inference (num, t, deps)) lines =
   505     (* Type information will be deleted later; skip repetition test. *)
   506     if is_only_type_information t then
   507       Inference (num, t, deps) :: lines
   508     (* Is there a repetition? If so, replace later line by earlier one. *)
   509     else case take_prefix (aint_inference t) lines of
   510       (* FIXME: Doesn't this code risk conflating proofs involving different
   511          types?? *)
   512        (_, []) => Inference (num, t, deps) :: lines
   513      | (pre, Inference (num', t', _) :: post) =>
   514        Inference (num, t', deps) ::
   515        pre @ map (replace_deps_in_line (num', [num])) post
   516 
   517 (* Recursively delete empty lines (type information) from the proof. *)
   518 fun add_nontrivial_line (Inference (num, t, [])) lines =
   519     if is_only_type_information t then delete_dep num lines
   520     else Inference (num, t, []) :: lines
   521   | add_nontrivial_line line lines = line :: lines
   522 and delete_dep num lines =
   523   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
   524 
   525 (* FIXME: this seems not to have worked and is obsolete anyway *)
   526 fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
   527   | is_bad_free _ = false
   528 
   529 fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
   530   | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
   531     (j, Inference (num, t, []) :: lines)  (* conjecture clauses must be kept *)
   532   | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
   533     (j + 1,
   534      if is_only_type_information t orelse
   535         not (null (Term.add_tvars t [])) orelse
   536         exists_subterm is_bad_free t orelse
   537         (length deps < 2 orelse j mod shrink_factor <> 0) then
   538        map (replace_deps_in_line (num, deps)) lines  (* delete line *)
   539      else
   540        Inference (num, t, deps) :: lines)
   541 
   542 (** EXTRACTING LEMMAS **)
   543 
   544 (* A list consisting of the first number in each line is returned.
   545    TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
   546    number (108) is extracted.
   547    SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
   548    extracted. *)
   549 fun extract_clause_numbers_in_atp_proof atp_proof =
   550   let
   551     val tokens_of = String.tokens (not o is_ident_char)
   552     fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
   553       | extract_num ("cnf" :: num :: "negated_conjecture" :: _) =
   554         Int.fromString num
   555       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
   556       | extract_num _ = NONE
   557   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
   558   
   559 (* Used to label theorems chained into the Sledgehammer call (or rather
   560    goal?) *)
   561 val chained_hint = "sledgehammer_chained"
   562 
   563 fun apply_command _ 1 = "by "
   564   | apply_command 1 _ = "apply "
   565   | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
   566 fun metis_command i n [] =
   567     apply_command i n ^ "metis"
   568   | metis_command i n xs =
   569     apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")"
   570 fun metis_line i n xs =
   571   "Try this command: " ^
   572   Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
   573 fun minimize_line _ [] = ""
   574   | minimize_line minimize_command facts =
   575     case minimize_command facts of
   576       "" => ""
   577     | command =>
   578       "To minimize the number of lemmas, try this command: " ^
   579       Markup.markup Markup.sendback command ^ ".\n"
   580 
   581 fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
   582   let
   583     val lemmas =
   584       atp_proof |> extract_clause_numbers_in_atp_proof
   585                 |> filter (is_axiom_clause_number thm_names)
   586                 |> map (fn i => Vector.sub (thm_names, i - 1))
   587                 |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint)
   588                 |> sort_distinct string_ord
   589     val n = Logic.count_prems (prop_of goal)
   590   in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
   591 
   592 (** Isar proof construction and manipulation **)
   593 
   594 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   595   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   596 
   597 type label = string * int
   598 type facts = label list * string list
   599 
   600 datatype qualifier = Show | Then | Moreover | Ultimately
   601 
   602 datatype step =
   603   Fix of (string * typ) list |
   604   Let of term * term |
   605   Assume of label * term |
   606   Have of qualifier list * label * term * byline
   607 and byline =
   608   Facts of facts |
   609   CaseSplit of step list list * facts
   610 
   611 val raw_prefix = "X"
   612 val assum_prefix = "A"
   613 val fact_prefix = "F"
   614 
   615 fun add_fact_from_dep thm_names num =
   616   if is_axiom_clause_number thm_names num then
   617     apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
   618   else
   619     apfst (insert (op =) (raw_prefix, num))
   620 
   621 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
   622 
   623 fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
   624   | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
   625   | step_for_line thm_names j (Inference (num, t, deps)) =
   626     Have (if j = 1 then [Show] else [], (raw_prefix, num),
   627           forall_vars t,
   628           Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
   629 
   630 fun proof_from_atp_proof pool ctxt shrink_factor atp_proof conjecture_shape
   631                          thm_names frees =
   632   let
   633     val lines =
   634       atp_proof ^ "$" (* the $ sign is a dummy token *)
   635       |> parse_proof pool
   636       |> decode_lines ctxt
   637       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
   638       |> rpair [] |-> fold_rev add_nontrivial_line
   639       |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
   640       |> snd
   641   in
   642     (if null frees then [] else [Fix frees]) @
   643     map2 (step_for_line thm_names) (length lines downto 1) lines
   644   end
   645 
   646 val indent_size = 2
   647 val no_label = ("", ~1)
   648 
   649 fun no_show qs = not (member (op =) qs Show)
   650 
   651 (* When redirecting proofs, we keep information about the labels seen so far in
   652    the "backpatches" data structure. The first component indicates which facts
   653    should be associated with forthcoming proof steps. The second component is a
   654    pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
   655    "drop_ls" are those that should be dropped in a case split. *)
   656 type backpatches = (label * facts) list * (label list * label list)
   657 
   658 fun using_of_step (Have (_, _, _, by)) =
   659     (case by of
   660        Facts (ls, _) => ls
   661      | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls)
   662   | using_of_step _ = []
   663 and using_of proof = fold (union (op =) o using_of_step) proof []
   664 
   665 fun new_labels_of_step (Fix _) = []
   666   | new_labels_of_step (Let _) = []
   667   | new_labels_of_step (Assume (l, _)) = [l]
   668   | new_labels_of_step (Have (_, l, _, _)) = [l]
   669 val new_labels_of = maps new_labels_of_step
   670 
   671 val join_proofs =
   672   let
   673     fun aux _ [] = NONE
   674       | aux proof_tail (proofs as (proof1 :: _)) =
   675         if exists null proofs then
   676           NONE
   677         else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   678           aux (hd proof1 :: proof_tail) (map tl proofs)
   679         else case hd proof1 of
   680           Have ([], l, t, by) =>
   681           if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   682                       | _ => false) (tl proofs) andalso
   683              not (exists (member (op =) (maps new_labels_of proofs))
   684                          (using_of proof_tail)) then
   685             SOME (l, t, map rev proofs, proof_tail)
   686           else
   687             NONE
   688         | _ => NONE
   689   in aux [] o map rev end
   690 
   691 fun case_split_qualifiers proofs =
   692   case length proofs of
   693     0 => []
   694   | 1 => [Then]
   695   | _ => [Ultimately]
   696 
   697 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
   698   let
   699     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
   700     fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
   701     fun first_pass ([], contra) = ([], contra)
   702       | first_pass ((step as Fix _) :: proof, contra) =
   703         first_pass (proof, contra) |>> cons step
   704       | first_pass ((step as Let _) :: proof, contra) =
   705         first_pass (proof, contra) |>> cons step
   706       | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
   707         if member (op =) concl_ls l then
   708           first_pass (proof, contra ||> cons step)
   709         else
   710           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
   711       | first_pass ((step as Have (qs, l, t, Facts (ls, ss))) :: proof,
   712                     contra) =
   713         if exists (member (op =) (fst contra)) ls then
   714           first_pass (proof, contra |>> cons l ||> cons step)
   715         else
   716           first_pass (proof, contra) |>> cons step
   717       | first_pass _ = raise Fail "malformed proof"
   718     val (proof_top, (contra_ls, contra_proof)) =
   719       first_pass (proof, (concl_ls, []))
   720     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   721     fun backpatch_labels patches ls =
   722       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   723     fun second_pass end_qs ([], assums, patches) =
   724         ([Have (end_qs, no_label,
   725                 if length assums < length concl_ls then
   726                   clause_for_literals thy (map (negate_term thy o fst) assums)
   727                 else
   728                   concl_t,
   729                 Facts (backpatch_labels patches (map snd assums)))], patches)
   730       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   731         second_pass end_qs (proof, (t, l) :: assums, patches)
   732       | second_pass end_qs (Have (qs, l, t, Facts (ls, ss)) :: proof, assums,
   733                             patches) =
   734         if member (op =) (snd (snd patches)) l andalso
   735            not (AList.defined (op =) (fst patches) l) then
   736           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   737         else
   738           (case List.partition (member (op =) contra_ls) ls of
   739              ([contra_l], co_ls) =>
   740              if no_show qs then
   741                second_pass end_qs
   742                            (proof, assums,
   743                             patches |>> cons (contra_l, (l :: co_ls, ss)))
   744                |>> cons (if member (op =) (fst (snd patches)) l then
   745                            Assume (l, negate_term thy t)
   746                          else
   747                            Have (qs, l, negate_term thy t,
   748                                  Facts (backpatch_label patches l)))
   749              else
   750                second_pass end_qs (proof, assums,
   751                                    patches |>> cons (contra_l, (co_ls, ss)))
   752            | (contra_ls as _ :: _, co_ls) =>
   753              let
   754                val proofs =
   755                  map_filter
   756                      (fn l =>
   757                          if member (op =) concl_ls l then
   758                            NONE
   759                          else
   760                            let
   761                              val drop_ls = filter (curry (op <>) l) contra_ls
   762                            in
   763                              second_pass []
   764                                  (proof, assums,
   765                                   patches ||> apfst (insert (op =) l)
   766                                           ||> apsnd (union (op =) drop_ls))
   767                              |> fst |> SOME
   768                            end) contra_ls
   769                val facts = (co_ls, [])
   770              in
   771                (case join_proofs proofs of
   772                   SOME (l, t, proofs, proof_tail) =>
   773                   Have (case_split_qualifiers proofs @
   774                         (if null proof_tail then end_qs else []), l, t,
   775                         CaseSplit (proofs, facts)) :: proof_tail
   776                 | NONE =>
   777                   [Have (case_split_qualifiers proofs @ end_qs, no_label,
   778                          concl_t, CaseSplit (proofs, facts))],
   779                 patches)
   780              end
   781            | _ => raise Fail "malformed proof")
   782        | second_pass _ _ = raise Fail "malformed proof"
   783     val proof_bottom =
   784       second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   785   in proof_top @ proof_bottom end
   786 
   787 val kill_duplicate_assumptions_in_proof =
   788   let
   789     fun relabel_facts subst =
   790       apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   791     fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   792         (case AList.lookup (op aconv) assums t of
   793            SOME l' => (proof, (l', l) :: subst, assums)
   794          | NONE => (step :: proof, subst, (t, l) :: assums))
   795       | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   796         (Have (qs, l, t,
   797                case by of
   798                  Facts facts => Facts (relabel_facts subst facts)
   799                | CaseSplit (proofs, facts) =>
   800                  CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   801          proof, subst, assums)
   802       | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   803     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   804   in do_proof end
   805 
   806 val then_chain_proof =
   807   let
   808     fun aux _ [] = []
   809       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   810       | aux l' (Have (qs, l, t, by) :: proof) =
   811         (case by of
   812            Facts (ls, ss) =>
   813            Have (if member (op =) ls l' then
   814                    (Then :: qs, l, t,
   815                     Facts (filter_out (curry (op =) l') ls, ss))
   816                  else
   817                    (qs, l, t, Facts (ls, ss)))
   818          | CaseSplit (proofs, facts) =>
   819            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   820         aux l proof
   821       | aux _ (step :: proof) = step :: aux no_label proof
   822   in aux no_label end
   823 
   824 fun kill_useless_labels_in_proof proof =
   825   let
   826     val used_ls = using_of proof
   827     fun do_label l = if member (op =) used_ls l then l else no_label
   828     fun kill (Assume (l, t)) = Assume (do_label l, t)
   829       | kill (Have (qs, l, t, by)) =
   830         Have (qs, do_label l, t,
   831               case by of
   832                 CaseSplit (proofs, facts) =>
   833                 CaseSplit (map (map kill) proofs, facts)
   834               | _ => by)
   835       | kill step = step
   836   in map kill proof end
   837 
   838 fun prefix_for_depth n = replicate_string (n + 1)
   839 
   840 val relabel_proof =
   841   let
   842     fun aux _ _ _ [] = []
   843       | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   844         if l = no_label then
   845           Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   846         else
   847           let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   848             Assume (l', t) ::
   849             aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   850           end
   851       | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   852         let
   853           val (l', subst, next_fact) =
   854             if l = no_label then
   855               (l, subst, next_fact)
   856             else
   857               let
   858                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
   859               in (l', (l, l') :: subst, next_fact + 1) end
   860           val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
   861           val by =
   862             case by of
   863               Facts facts => Facts (relabel_facts facts)
   864             | CaseSplit (proofs, facts) =>
   865               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   866                          relabel_facts facts)
   867         in
   868           Have (qs, l', t, by) ::
   869           aux subst depth (next_assum, next_fact) proof
   870         end
   871       | aux subst depth nextp (step :: proof) =
   872         step :: aux subst depth nextp proof
   873   in aux [] 0 (1, 1) end
   874 
   875 fun string_for_proof ctxt i n =
   876   let
   877     fun fix_print_mode f =
   878       PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   879                       (print_mode_value ())) f
   880     fun do_indent ind = replicate_string (ind * indent_size) " "
   881     fun do_free (s, T) =
   882       maybe_quote s ^ " :: " ^
   883       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   884     fun do_raw_label (s, num) = s ^ string_of_int num
   885     fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
   886     fun do_have qs =
   887       (if member (op =) qs Moreover then "moreover " else "") ^
   888       (if member (op =) qs Ultimately then "ultimately " else "") ^
   889       (if member (op =) qs Then then
   890          if member (op =) qs Show then "thus" else "hence"
   891        else
   892          if member (op =) qs Show then "show" else "have")
   893     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   894     fun do_using [] = ""
   895       | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
   896     fun do_by_facts [] = "by metis"
   897       | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
   898     fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
   899     and do_step ind (Fix xs) =
   900         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   901       | do_step ind (Let (t1, t2)) =
   902         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   903       | do_step ind (Assume (l, t)) =
   904         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   905       | do_step ind (Have (qs, l, t, Facts facts)) =
   906         do_indent ind ^ do_have qs ^ " " ^
   907         do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   908       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   909         space_implode (do_indent ind ^ "moreover\n")
   910                       (map (do_block ind) proofs) ^
   911         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   912         do_facts facts ^ "\n"
   913     and do_steps prefix suffix ind steps =
   914       let val s = implode (map (do_step ind) steps) in
   915         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   916         String.extract (s, ind * indent_size,
   917                         SOME (size s - ind * indent_size - 1)) ^
   918         suffix ^ "\n"
   919       end
   920     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   921     (* One-step proofs are pointless; better use the Metis one-liner. *)
   922     and do_proof [_] = ""
   923       | do_proof proof =
   924         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   925         do_indent 0 ^ "proof -\n" ^
   926         do_steps "" "" 1 proof ^
   927         do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   928   in do_proof end
   929 
   930 fun isar_proof_text (pool, debug, shrink_factor, ctxt, conjecture_shape)
   931                     (minimize_command, atp_proof, thm_names, goal, i) =
   932   let
   933     val thy = ProofContext.theory_of ctxt
   934     val (frees, hyp_ts, concl_t) = strip_subgoal goal i
   935     val n = Logic.count_prems (prop_of goal)
   936     val (one_line_proof, lemma_names) =
   937       metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
   938     fun isar_proof_for () =
   939       case proof_from_atp_proof pool ctxt shrink_factor atp_proof
   940                                 conjecture_shape thm_names frees
   941            |> redirect_proof thy conjecture_shape hyp_ts concl_t
   942            |> kill_duplicate_assumptions_in_proof
   943            |> then_chain_proof
   944            |> kill_useless_labels_in_proof
   945            |> relabel_proof
   946            |> string_for_proof ctxt i n of
   947         "" => ""
   948       | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   949     val isar_proof =
   950       if debug then
   951         isar_proof_for ()
   952       else
   953         try isar_proof_for ()
   954         |> the_default "Warning: The Isar proof construction failed.\n"
   955   in (one_line_proof ^ isar_proof, lemma_names) end
   956 
   957 fun proof_text isar_proof isar_params =
   958   if isar_proof then isar_proof_text isar_params else metis_proof_text
   959 
   960 end;