src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
author blanchet
Tue, 16 Oct 2012 20:31:08 +0200
changeset 49883 a6ebdaf8e267
child 49913 2e7d0655b176
permissions -rw-r--r--
added missing file
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49883
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     4
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     5
*)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     6
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     7
signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     8
sig
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
     9
  type isar_params = ATP_Proof_Reconstruct.isar_params
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    10
  type one_line_params = ATP_Proof_Reconstruct.one_line_params
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    11
  val isar_proof_text :
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    12
    Proof.context -> bool -> isar_params -> 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    13
      one_line_params -> string
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    14
  val proof_text :
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    15
    Proof.context -> bool -> isar_params -> 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    16
      int -> one_line_params -> string
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    17
end;
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    18
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    19
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    20
struct
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    21
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    22
open ATP_Util
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    23
open ATP_Proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    24
open ATP_Problem_Generate
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    25
open ATP_Proof_Reconstruct
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    26
open String_Redirect
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    27
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    28
(** Type annotations **)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    29
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    30
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    31
  | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    32
  | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    33
  | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    34
  | post_traverse_term_type' f env (Abs (x, T1, b)) s =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    35
    let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    36
      val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    37
    in f (Abs (x, T1, b')) (T1 --> T2) s' end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    38
  | post_traverse_term_type' f env (u $ v) s =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    39
    let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    40
      val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    41
      val ((v', s''), _) = post_traverse_term_type' f env v s'
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    42
    in f (u' $ v') T s'' end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    43
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    44
fun post_traverse_term_type f s t =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    45
  post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    46
fun post_fold_term_type f s t =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    47
  post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    48
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    49
(* Data structures, orders *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    50
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    51
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    52
structure Var_Set_Tab = Table(
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    53
  type key = indexname list
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    54
  val ord = list_ord Term_Ord.fast_indexname_ord)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    55
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    56
(* (1) Generalize Types *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    57
fun generalize_types ctxt t =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    58
  t |> map_types (fn _ => dummyT)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    59
    |> Syntax.check_term
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    60
         (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    61
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    62
(* (2) Typing-spot Table *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    63
local
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    64
fun key_of_atype (TVar (idxn, _)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    65
    Ord_List.insert Term_Ord.fast_indexname_ord idxn
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    66
  | key_of_atype _ = I
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    67
fun key_of_type T = fold_atyps key_of_atype T []
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    68
fun update_tab t T (tab, pos) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    69
  (case key_of_type T of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    70
     [] => tab
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    71
   | key =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    72
     let val cost = (size_of_typ T, (size_of_term t, pos)) in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    73
       case Var_Set_Tab.lookup tab key of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    74
         NONE => Var_Set_Tab.update_new (key, cost) tab
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    75
       | SOME old_cost =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    76
         (case cost_ord (cost, old_cost) of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    77
            LESS => Var_Set_Tab.update (key, cost) tab
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    78
          | _ => tab)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    79
     end,
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    80
   pos + 1)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    81
in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    82
val typing_spot_table =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    83
  post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    84
end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    85
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    86
(* (3) Reverse-Greedy *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    87
fun reverse_greedy typing_spot_tab =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    88
  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    89
    fun update_count z =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    90
      fold (fn tvar => fn tab =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    91
        let val c = Vartab.lookup tab tvar |> the_default 0 in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    92
          Vartab.update (tvar, c + z) tab
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    93
        end)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    94
    fun superfluous tcount =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    95
      forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    96
    fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    97
      if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    98
      else (spot :: spots, tcount)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
    99
    val (typing_spots, tvar_count_tab) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   100
      Var_Set_Tab.fold
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   101
        (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   102
        typing_spot_tab ([], Vartab.empty)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   103
      |>> sort_distinct (rev_order o cost_ord o pairself snd)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   104
  in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   105
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   106
(* (4) Introduce Annotations *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   107
fun introduce_annotations thy spots t t' =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   108
  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   109
    val get_types = post_fold_term_type (K cons) []
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   110
    fun match_types tp =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   111
      fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   112
    fun unica' b x [] = if b then [x] else []
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   113
      | unica' b x (y :: ys) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   114
        if x = y then unica' false x ys
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   115
        else unica' true y ys |> b ? cons x
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   116
    fun unica ord xs =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   117
      case sort ord xs of x :: ys => unica' true x ys | [] => []
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   118
    val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   119
    fun erase_unica_tfrees env =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   120
      let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   121
        val unica =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   122
          Vartab.fold (add_all_tfree_namesT o snd o snd) env []
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   123
          |> unica fast_string_ord
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   124
        val erase_unica = map_atyps
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   125
          (fn T as TFree (s, _) =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   126
              if Ord_List.member fast_string_ord unica s then dummyT else T
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   127
            | T => T)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   128
      in Vartab.map (K (apsnd erase_unica)) env end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   129
    val env = match_types (t', t) |> erase_unica_tfrees
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   130
    fun get_annot env (TFree _) = (false, (env, dummyT))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   131
      | get_annot env (T as TVar (v, S)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   132
        let val T' = Envir.subst_type env T in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   133
          if T' = dummyT then (false, (env, dummyT))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   134
          else (true, (Vartab.update (v, (S, dummyT)) env, T'))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   135
        end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   136
      | get_annot env (Type (S, Ts)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   137
        (case fold_rev (fn T => fn (b, (env, Ts)) =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   138
                  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   139
                    val (b', (env', T)) = get_annot env T
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   140
                  in (b orelse b', (env', T :: Ts)) end)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   141
                Ts (false, (env, [])) of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   142
           (true, (env', Ts)) => (true, (env', Type (S, Ts)))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   143
         | (false, (env', _)) => (false, (env', dummyT)))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   144
    fun post1 _ T (env, cp, ps as p :: ps', annots) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   145
        if p <> cp then
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   146
          (env, cp + 1, ps, annots)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   147
        else
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   148
          let val (_, (env', T')) = get_annot env T in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   149
            (env', cp + 1, ps', (p, T') :: annots)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   150
          end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   151
      | post1 _ _ accum = accum
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   152
    val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   153
    fun post2 t _ (cp, annots as (p, T) :: annots') =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   154
        if p <> cp then (t, (cp + 1, annots))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   155
        else (Type.constraint T t, (cp + 1, annots'))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   156
      | post2 t _ x = (t, x)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   157
  in post_traverse_term_type post2 (0, rev annots) t |> fst end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   158
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   159
(* (5) Annotate *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   160
fun annotate_types ctxt t =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   161
  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   162
    val thy = Proof_Context.theory_of ctxt
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   163
    val t' = generalize_types ctxt t
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   164
    val typing_spots =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   165
      t' |> typing_spot_table
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   166
         |> reverse_greedy
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   167
         |> sort int_ord
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   168
  in introduce_annotations thy typing_spots t t' end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   169
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   170
fun string_for_proof ctxt type_enc lam_trans i n =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   171
  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   172
    fun fix_print_mode f x =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   173
      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   174
                               (print_mode_value ())) f x
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   175
    fun do_indent ind = replicate_string (ind * indent_size) " "
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   176
    fun do_free (s, T) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   177
      maybe_quote s ^ " :: " ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   178
      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   179
    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   180
    fun do_have qs =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   181
      (if member (op =) qs Moreover then "moreover " else "") ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   182
      (if member (op =) qs Ultimately then "ultimately " else "") ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   183
      (if member (op =) qs Then then
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   184
         if member (op =) qs Show then "thus" else "hence"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   185
       else
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   186
         if member (op =) qs Show then "show" else "have")
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   187
    val do_term =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   188
      maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   189
      o annotate_types ctxt
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   190
    val reconstr = Metis (type_enc, lam_trans)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   191
    fun do_facts (ls, ss) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   192
      reconstructor_command reconstr 1 1 [] 0
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   193
          (ls |> sort_distinct (prod_ord string_ord int_ord),
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   194
           ss |> sort_distinct string_ord)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   195
    and do_step ind (Fix xs) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   196
        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   197
      | do_step ind (Let (t1, t2)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   198
        do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   199
      | do_step ind (Assume (l, t)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   200
        do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   201
      | do_step ind (Prove (qs, l, t, By_Metis facts)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   202
        do_indent ind ^ do_have qs ^ " " ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   203
        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   204
      | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   205
        implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   206
                     proofs) ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   207
        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   208
        do_facts facts ^ "\n"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   209
    and do_steps prefix suffix ind steps =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   210
      let val s = implode (map (do_step ind) steps) in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   211
        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   212
        String.extract (s, ind * indent_size,
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   213
                        SOME (size s - ind * indent_size - 1)) ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   214
        suffix ^ "\n"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   215
      end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   216
    and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   217
    (* One-step proofs are pointless; better use the Metis one-liner
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   218
       directly. *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   219
    and do_proof [Prove (_, _, _, By_Metis _)] = ""
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   220
      | do_proof proof =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   221
        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   222
        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   223
        (if n <> 1 then "next" else "qed")
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   224
  in do_proof end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   225
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   226
fun min_local ctxt type_enc lam_trans proof =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   227
  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   228
    (* Merging spots, greedy algorithm *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   229
    fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   230
      | cost _ = ~1
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   231
    fun can_merge (Prove (_, lbl, _, By_Metis _))  (Prove (_, _, _, By_Metis _)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   232
      (lbl = no_label)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   233
      | can_merge _ _ = false
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   234
    val merge_spots = 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   235
      fold_index 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   236
        (fn (i, s2) => fn (s1, pile) => (s2, pile |> can_merge s1 s2 ? cons (i, cost s1)))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   237
        (tl proof) (hd proof, [])
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   238
    |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   239
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   240
    (* Enrich context with facts *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   241
    val thy = Proof_Context.theory_of ctxt
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   242
    fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   243
    fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   244
      if lbl = no_label then ctxt 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   245
      else Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) ctxt
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   246
      | enrich_ctxt' _ ctxt = ctxt
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   247
    val rich_ctxt = fold enrich_ctxt' proof ctxt
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   248
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   249
    (* Timing *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   250
    fun take_time tac arg =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   251
      let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   252
        val t_start = Timing.start ()
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   253
      in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   254
        (tac arg ; Timing.result t_start |> #cpu)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   255
      end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   256
    fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   257
      let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   258
        fun thmify (Prove (_, _, t, _)) = sorry t
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   259
        val facts = fact_names |>> map string_for_label
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   260
                               |> op@
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   261
                               |> map (Proof_Context.get_thm rich_ctxt)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   262
                               |> (if member op= qs Then 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   263
                                   then cons (the s0 |> thmify)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   264
                                   else I)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   265
        val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   266
        fun tac {context = ctxt, prems = _} =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   267
          Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   268
      in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   269
        take_time (fn () => goal tac)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   270
      end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   271
  
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   272
    (* Merging *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   273
    fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1))) 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   274
              (Prove (qs2, lbl , t, By_Metis (ls2, ss2))) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   275
      let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   276
        val qs = (inter op= qs1 qs2) (* FIXME: Is this correct? *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   277
          |> member op= (union op= qs1 qs2) Ultimately ? cons Ultimately
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   278
          |> member op= qs2 Show ? cons Show
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   279
      in Prove (qs, lbl, t, By_Metis (ls1@ls2, ss1@ss2)) end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   280
    fun try_merge proof i =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   281
      let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   282
        val (front, s0, s1, s2, tail) = 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   283
          case (proof, i) of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   284
            ((s1::s2::proof), 0) => ([], NONE, s1, s2, proof)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   285
          | _ => let val (front, s0::s1::s2::tail) = chop (i-1) proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   286
                 in (front, SOME s0, s1, s2, tail) end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   287
        val s12 = merge s1 s2
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   288
        val t1 = try_metis s1 s0 ()
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   289
        val t2 = try_metis s2 (SOME s1) ()
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   290
        val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   291
      in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   292
        (TimeLimit.timeLimit tlimit (try_metis s12 s0) ();
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   293
          SOME (front @ (case s0 of NONE => s12::tail | SOME s => s::s12::tail)))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   294
        handle _ => NONE
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   295
      end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   296
    fun merge_steps proof [] = proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   297
      | merge_steps proof (i::is) = 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   298
        case try_merge proof i of 
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   299
          NONE => merge_steps proof is
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   300
        | SOME proof' => merge_steps proof' (map (fn j => if j>i then j-1 else j) is)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   301
  in merge_steps proof merge_spots end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   302
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   303
fun isar_proof_text ctxt isar_proof_requested
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   304
        (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   305
        (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   306
  let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   307
    val isar_shrink_factor =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   308
      (if isar_proof_requested then 1 else 2) * isar_shrink_factor
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   309
    val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   310
    val frees = fold Term.add_frees (concl_t :: hyp_ts) []
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   311
    val one_line_proof = one_line_proof_text 0 one_line_params
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   312
    val type_enc =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   313
      if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   314
      else partial_typesN
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   315
    val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   316
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   317
    fun isar_proof_of () =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   318
      let
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   319
        val atp_proof =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   320
          atp_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   321
          |> clean_up_atp_proof_dependencies
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   322
          |> nasty_atp_proof pool
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   323
          |> map_term_names_in_atp_proof repair_name
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   324
          |> decode_lines ctxt sym_tab
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   325
          |> rpair [] |-> fold_rev (add_line fact_names)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   326
          |> repair_waldmeister_endgame
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   327
          |> rpair [] |-> fold_rev add_nontrivial_line
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   328
          |> rpair (0, [])
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   329
          |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   330
          |> snd
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   331
        val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   332
        val conjs =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   333
          atp_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   334
          |> map_filter (fn Inference_Step (name as (_, ss), _, _, []) =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   335
                            if member (op =) ss conj_name then SOME name else NONE
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   336
                          | _ => NONE)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   337
        fun dep_of_step (Definition_Step _) = NONE
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   338
          | dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   339
        val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   340
        val axioms = axioms_of_ref_graph ref_graph conjs
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   341
        val tainted = tainted_atoms_of_ref_graph ref_graph conjs
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   342
        val props =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   343
          Symtab.empty
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   344
          |> fold (fn Definition_Step _ => I (* FIXME *)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   345
                    | Inference_Step ((s, _), t, _, _) =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   346
                      Symtab.update_new (s,
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   347
                          t |> fold forall_of (map Var (Term.add_vars t []))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   348
                            |> member (op = o apsnd fst) tainted s ? s_not))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   349
                  atp_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   350
        fun prop_of_clause c =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   351
          fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   352
               @{term False}
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   353
        fun label_of_clause [name] = raw_label_for_name name
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   354
          | label_of_clause c = (space_implode "___" (map fst c), 0)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   355
        fun maybe_show outer c =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   356
          (outer andalso length c = 1 andalso subset (op =) (c, conjs))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   357
          ? cons Show
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   358
        fun do_have outer qs (gamma, c) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   359
          Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   360
                 By_Metis (fold (add_fact_from_dependency fact_names
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   361
                                 o the_single) gamma ([], [])))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   362
        fun do_inf outer (Have z) = do_have outer [] z
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   363
          | do_inf outer (Hence z) = do_have outer [Then] z
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   364
          | do_inf outer (Cases cases) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   365
            let val c = succedent_of_cases cases in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   366
              Prove (maybe_show outer c [Ultimately], label_of_clause c,
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   367
                     prop_of_clause c,
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   368
                     Case_Split (map (do_case false) cases, ([], [])))
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   369
            end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   370
        and do_case outer (c, infs) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   371
          Assume (label_of_clause c, prop_of_clause c) ::
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   372
          map (do_inf outer) infs
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   373
        val isar_proof =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   374
          (if null params then [] else [Fix params]) @
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   375
           (ref_graph
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   376
           |> redirect_graph axioms tainted
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   377
           |> chain_direct_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   378
           |> map (do_inf true)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   379
           |> kill_duplicate_assumptions_in_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   380
           |> kill_useless_labels_in_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   381
           |> relabel_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   382
           |> min_local ctxt type_enc lam_trans)
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   383
          |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   384
      in
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   385
        case isar_proof of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   386
          "" =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   387
          if isar_proof_requested then
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   388
            "\nNo structured proof available (proof too short)."
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   389
          else
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   390
            ""
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   391
        | _ =>
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   392
          "\n\n" ^ (if isar_proof_requested then "Structured proof"
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   393
                    else "Perhaps this will work") ^
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   394
          ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   395
      end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   396
    val isar_proof =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   397
      if debug then
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   398
        isar_proof_of ()
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   399
      else case try isar_proof_of () of
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   400
        SOME s => s
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   401
      | NONE => if isar_proof_requested then
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   402
                  "\nWarning: The Isar proof construction failed."
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   403
                else
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   404
                  ""
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   405
  in one_line_proof ^ isar_proof end
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   406
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   407
fun proof_text ctxt isar_proof isar_params num_chained
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   408
               (one_line_params as (preplay, _, _, _, _, _)) =
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   409
  (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   410
     isar_proof_text ctxt isar_proof isar_params
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   411
   else
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   412
     one_line_proof_text num_chained) one_line_params
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   413
a6ebdaf8e267 added missing file
blanchet
parents:
diff changeset
   414
end;