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