src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57154 f0eff6393a32
child 57286 4868ec62f533
permissions -rw-r--r--
simplified counterexample handling
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
smolkas@50263
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50263
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50263
     4
smolkas@50263
     5
Basic data structures for representing and basic methods
smolkas@50263
     6
for dealing with Isar proof texts.
smolkas@50263
     7
*)
smolkas@50263
     8
blanchet@55202
     9
signature SLEDGEHAMMER_ISAR_PROOF =
smolkas@50259
    10
sig
blanchet@55287
    11
  type proof_method = Sledgehammer_Proof_Methods.proof_method
blanchet@55285
    12
wenzelm@51239
    13
  type label = string * int
blanchet@54816
    14
  type facts = label list * string list (* local and global facts *)
smolkas@50268
    15
smolkas@51178
    16
  datatype isar_qualifier = Show | Then
smolkas@50268
    17
smolkas@52454
    18
  datatype isar_proof =
blanchet@54700
    19
    Proof of (string * typ) list * (label * term) list * isar_step list
smolkas@51179
    20
  and isar_step =
smolkas@50268
    21
    Let of term * term |
blanchet@55280
    22
    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
blanchet@55299
    23
      * facts * proof_method list * string
smolkas@52592
    24
smolkas@51179
    25
  val no_label : label
smolkas@50268
    26
smolkas@52592
    27
  val label_ord : label * label -> order
blanchet@51998
    28
  val string_of_label : label -> string
smolkas@52592
    29
blanchet@55260
    30
  val steps_of_isar_proof : isar_proof -> isar_step list
smolkas@51179
    31
blanchet@55223
    32
  val label_of_isar_step : isar_step -> label option
blanchet@55279
    33
  val facts_of_isar_step : isar_step -> facts
blanchet@55279
    34
  val proof_methods_of_isar_step : isar_step -> proof_method list
smolkas@51179
    35
blanchet@54765
    36
  val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
blanchet@55212
    37
  val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
blanchet@55212
    38
  val add_isar_steps : isar_step list -> int -> int
smolkas@52454
    39
blanchet@55212
    40
  structure Canonical_Label_Tab : TABLE
smolkas@52556
    41
smolkas@52556
    42
  val canonical_label_ord : (label * label) -> order
blanchet@55220
    43
blanchet@55299
    44
  val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
blanchet@55220
    45
  val chain_isar_proof : isar_proof -> isar_proof
blanchet@55220
    46
  val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
blanchet@55213
    47
  val relabel_isar_proof_canonically : isar_proof -> isar_proof
blanchet@55282
    48
  val relabel_isar_proof_nicely : isar_proof -> isar_proof
smolkas@52556
    49
blanchet@55299
    50
  val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
blanchet@54504
    51
end;
smolkas@50259
    52
blanchet@55202
    53
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
smolkas@50259
    54
struct
smolkas@50259
    55
blanchet@55211
    56
open ATP_Util
blanchet@55211
    57
open ATP_Proof
blanchet@55211
    58
open ATP_Problem_Generate
blanchet@55211
    59
open ATP_Proof_Reconstruct
blanchet@55211
    60
open Sledgehammer_Util
blanchet@55287
    61
open Sledgehammer_Proof_Methods
blanchet@55211
    62
open Sledgehammer_Isar_Annotate
blanchet@55211
    63
smolkas@50259
    64
type label = string * int
blanchet@54534
    65
type facts = label list * string list (* local and global facts *)
smolkas@50259
    66
smolkas@51178
    67
datatype isar_qualifier = Show | Then
smolkas@50259
    68
smolkas@52454
    69
datatype isar_proof =
blanchet@54700
    70
  Proof of (string * typ) list * (label * term) list * isar_step list
smolkas@51179
    71
and isar_step =
smolkas@50259
    72
  Let of term * term |
blanchet@55280
    73
  Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
blanchet@55299
    74
    * facts * proof_method list * string
smolkas@52592
    75
smolkas@51179
    76
val no_label = ("", ~1)
smolkas@50259
    77
smolkas@52592
    78
val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
smolkas@52556
    79
blanchet@51998
    80
fun string_of_label (s, num) = s ^ string_of_int num
smolkas@50259
    81
blanchet@55260
    82
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
smolkas@51179
    83
blanchet@55299
    84
fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
blanchet@55223
    85
  | label_of_isar_step _ = NONE
smolkas@51178
    86
blanchet@55299
    87
fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
blanchet@55281
    88
  | subproofs_of_isar_step _ = []
smolkas@52454
    89
blanchet@55299
    90
fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
blanchet@55279
    91
  | facts_of_isar_step _ = ([], [])
blanchet@55279
    92
blanchet@55299
    93
fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
blanchet@55279
    94
  | proof_methods_of_isar_step _ = []
smolkas@51179
    95
blanchet@55212
    96
fun fold_isar_step f step =
blanchet@55281
    97
  fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step
blanchet@55212
    98
and fold_isar_steps f = fold (fold_isar_step f)
smolkas@52454
    99
blanchet@54765
   100
fun map_isar_steps f =
smolkas@52592
   101
  let
blanchet@55212
   102
    fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
blanchet@55212
   103
    and map_step (step as Let _) = f step
blanchet@55299
   104
      | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
blanchet@55299
   105
        f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
blanchet@55212
   106
  in map_proof end
smolkas@52592
   107
blanchet@55212
   108
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
smolkas@52556
   109
blanchet@55211
   110
(* canonical proof labels: 1, 2, 3, ... in post traversal order *)
smolkas@52557
   111
fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
smolkas@52556
   112
blanchet@55212
   113
structure Canonical_Label_Tab = Table(
smolkas@52556
   114
  type key = label
smolkas@52556
   115
  val ord = canonical_label_ord)
smolkas@52556
   116
blanchet@55299
   117
fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
blanchet@55299
   118
    Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
blanchet@55299
   119
  | comment_isar_step _ step = step
blanchet@55299
   120
fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
blanchet@55299
   121
blanchet@55220
   122
fun chain_qs_lfs NONE lfs = ([], lfs)
blanchet@55220
   123
  | chain_qs_lfs (SOME l0) lfs =
blanchet@55220
   124
    if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
fleury@57154
   125
fun chain_isar_step lbl (x as Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
blanchet@55220
   126
    let val (qs', lfs) = chain_qs_lfs lbl lfs in
blanchet@55299
   127
      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
blanchet@55220
   128
    end
blanchet@55220
   129
  | chain_isar_step _ step = step
blanchet@55220
   130
and chain_isar_steps _ [] = []
blanchet@55220
   131
  | chain_isar_steps (prev as SOME _) (i :: is) =
blanchet@55223
   132
    chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
blanchet@55223
   133
  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
blanchet@55220
   134
and chain_isar_proof (Proof (fix, assms, steps)) =
blanchet@55220
   135
  Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
blanchet@55220
   136
blanchet@55220
   137
fun kill_useless_labels_in_isar_proof proof =
blanchet@55220
   138
  let
blanchet@55220
   139
    val used_ls =
blanchet@55279
   140
      fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
blanchet@55220
   141
blanchet@55220
   142
    fun kill_label l = if member (op =) used_ls l then l else no_label
blanchet@55220
   143
blanchet@55299
   144
    fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
blanchet@55299
   145
        Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
blanchet@55220
   146
      | kill_step step = step
blanchet@55220
   147
    and kill_proof (Proof (fix, assms, steps)) =
blanchet@55220
   148
      Proof (fix, map (apfst kill_label) assms, map kill_step steps)
blanchet@55220
   149
  in
blanchet@55220
   150
    kill_proof proof
blanchet@55220
   151
  end
blanchet@55220
   152
blanchet@55213
   153
fun relabel_isar_proof_canonically proof =
smolkas@52556
   154
  let
smolkas@52556
   155
    fun next_label l (next, subst) =
blanchet@54534
   156
      let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
smolkas@52556
   157
blanchet@55299
   158
    fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
blanchet@55299
   159
          (accum as (_, subst)) =
blanchet@54534
   160
        let
blanchet@55281
   161
          val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
blanchet@55281
   162
          val ((subs', l'), accum') = accum
blanchet@55281
   163
            |> fold_map relabel_proof subs
blanchet@55281
   164
            ||>> next_label l
blanchet@54534
   165
        in
blanchet@55299
   166
          (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
blanchet@54534
   167
        end
blanchet@55281
   168
      | relabel_step step accum = (step, accum)
blanchet@55281
   169
    and relabel_proof (Proof (fix, assms, steps)) =
blanchet@55281
   170
      fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms
blanchet@55281
   171
      ##>> fold_map relabel_step steps
blanchet@55281
   172
      #>> (fn (assms, steps) => Proof (fix, assms, steps))
smolkas@52556
   173
  in
blanchet@55279
   174
    fst (relabel_proof proof (0, []))
smolkas@52556
   175
  end
smolkas@52556
   176
blanchet@55220
   177
val assume_prefix = "a"
blanchet@55220
   178
val have_prefix = "f"
blanchet@55220
   179
blanchet@55282
   180
val relabel_isar_proof_nicely =
blanchet@55220
   181
  let
blanchet@55281
   182
    fun next_label depth prefix l (accum as (next, subst)) =
blanchet@55220
   183
      if l = no_label then
blanchet@55281
   184
        (l, accum)
blanchet@55220
   185
      else
blanchet@55220
   186
        let val l' = (replicate_string (depth + 1) prefix, next) in
blanchet@55281
   187
          (l', (next + 1, (l, l') :: subst))
blanchet@55220
   188
        end
blanchet@55220
   189
blanchet@55299
   190
    fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
blanchet@55299
   191
          (accum as (_, subst)) =
blanchet@55220
   192
        let
blanchet@55281
   193
          val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
blanchet@55309
   194
          val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
blanchet@55281
   195
          val subs' = map (relabel_proof subst' (depth + 1)) subs
blanchet@55220
   196
        in
blanchet@55299
   197
          (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
blanchet@55220
   198
        end
blanchet@55281
   199
      | relabel_step _ step accum = (step, accum)
blanchet@55220
   200
    and relabel_proof subst depth (Proof (fix, assms, steps)) =
blanchet@55281
   201
      (1, subst)
blanchet@55281
   202
      |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms
blanchet@55281
   203
      ||>> fold_map (relabel_step depth) steps
blanchet@55281
   204
      |> (fn ((assms, steps), _) => Proof (fix, assms, steps))
blanchet@55220
   205
  in
blanchet@55220
   206
    relabel_proof [] 0
blanchet@55220
   207
  end
blanchet@55220
   208
blanchet@55211
   209
val indent_size = 2
blanchet@55211
   210
blanchet@56985
   211
fun string_of_isar_proof ctxt0 i n proof =
blanchet@55211
   212
  let
blanchet@55211
   213
    (* Make sure only type constraints inserted by the type annotation code are printed. *)
blanchet@56985
   214
    val ctxt = ctxt0
blanchet@56985
   215
      |> Config.put show_markup false
blanchet@56985
   216
      |> Config.put Printer.show_type_emphasis false
blanchet@56985
   217
      |> Config.put show_types false
blanchet@56985
   218
      |> Config.put show_sorts false
blanchet@56985
   219
      |> Config.put show_consts false
blanchet@55211
   220
blanchet@55211
   221
    val register_fixes = map Free #> fold Variable.auto_fixes
blanchet@55211
   222
blanchet@55216
   223
    fun add_str s' = apfst (suffix s')
blanchet@55211
   224
blanchet@55211
   225
    fun of_indent ind = replicate_string (ind * indent_size) " "
blanchet@55211
   226
    fun of_moreover ind = of_indent ind ^ "moreover\n"
blanchet@55211
   227
    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
blanchet@55211
   228
blanchet@55211
   229
    fun of_obtain qs nr =
blanchet@55211
   230
      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
blanchet@55211
   231
       else if nr = 1 orelse member (op =) qs Then then "then "
blanchet@55211
   232
       else "") ^ "obtain"
blanchet@55211
   233
blanchet@55211
   234
    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
blanchet@55211
   235
    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
blanchet@55211
   236
blanchet@55211
   237
    fun of_have qs nr =
blanchet@55211
   238
      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
blanchet@55211
   239
      else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
blanchet@55211
   240
      else of_show_have qs
blanchet@55211
   241
blanchet@55211
   242
    fun add_term term (s, ctxt) =
blanchet@55211
   243
      (s ^ (term
blanchet@55211
   244
            |> singleton (Syntax.uncheck_terms ctxt)
blanchet@55213
   245
            |> annotate_types_in_term ctxt
blanchet@55211
   246
            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
blanchet@55211
   247
            |> simplify_spaces
blanchet@55211
   248
            |> maybe_quote),
blanchet@55211
   249
       ctxt |> Variable.auto_fixes term)
blanchet@55211
   250
blanchet@56983
   251
    fun using_facts [] [] = ""
blanchet@56983
   252
      | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
blanchet@55257
   253
blanchet@55257
   254
    fun is_direct_method (Metis_Method _) = true
blanchet@55257
   255
      | is_direct_method Meson_Method = true
blanchet@56081
   256
      | is_direct_method SMT2_Method = true
blanchet@56983
   257
      | is_direct_method Simp_Method = true
blanchet@55257
   258
      | is_direct_method _ = false
blanchet@55211
   259
blanchet@55211
   260
    (* Local facts are always passed via "using", which affects "meson" and "metis". This is
blanchet@55211
   261
       arguably stylistically superior, because it emphasises the structure of the proof. It is also
blanchet@55211
   262
       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
blanchet@55211
   263
       and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
blanchet@55257
   264
    fun of_method ls ss meth =
blanchet@55281
   265
      let val direct = is_direct_method meth in
blanchet@55281
   266
        using_facts ls (if direct then [] else ss) ^
blanchet@56985
   267
        "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
blanchet@55281
   268
      end
blanchet@55211
   269
blanchet@55211
   270
    fun of_free (s, T) =
blanchet@55211
   271
      maybe_quote s ^ " :: " ^
blanchet@55211
   272
      maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
blanchet@55211
   273
blanchet@55211
   274
    fun add_frees xs (s, ctxt) =
blanchet@55211
   275
      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
blanchet@55211
   276
blanchet@55211
   277
    fun add_fix _ [] = I
blanchet@55281
   278
      | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
blanchet@55211
   279
blanchet@55211
   280
    fun add_assm ind (l, t) =
blanchet@55281
   281
      add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n"
blanchet@55211
   282
blanchet@55211
   283
    fun of_subproof ind ctxt proof =
blanchet@55211
   284
      let
blanchet@55211
   285
        val ind = ind + 1
blanchet@55211
   286
        val s = of_proof ind ctxt proof
blanchet@55211
   287
        val prefix = "{ "
blanchet@55211
   288
        val suffix = " }"
blanchet@55211
   289
      in
blanchet@55211
   290
        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
blanchet@55211
   291
        String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
blanchet@55211
   292
        suffix ^ "\n"
blanchet@55211
   293
      end
blanchet@55211
   294
    and of_subproofs _ _ _ [] = ""
blanchet@55281
   295
      | of_subproofs ind ctxt qs subs =
blanchet@55211
   296
        (if member (op =) qs Then then of_moreover ind else "") ^
blanchet@55281
   297
        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
blanchet@55281
   298
    and add_step_pre ind qs subs (s, ctxt) =
blanchet@55281
   299
      (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
blanchet@55211
   300
    and add_step ind (Let (t1, t2)) =
blanchet@55216
   301
        add_str (of_indent ind ^ "let ")
blanchet@55281
   302
        #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
blanchet@55309
   303
      | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
blanchet@55281
   304
        add_step_pre ind qs subs
blanchet@55211
   305
        #> (case xs of
blanchet@55281
   306
             [] => add_str (of_have qs (length subs) ^ " ")
blanchet@55281
   307
           | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
blanchet@55217
   308
        #> add_str (of_label l)
blanchet@55217
   309
        #> add_term t
blanchet@55217
   310
        #> add_str (" " ^
blanchet@55218
   311
             of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
blanchet@55299
   312
             (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
blanchet@55211
   313
    and add_steps ind = fold (add_step ind)
blanchet@55211
   314
    and of_proof ind ctxt (Proof (xs, assms, steps)) =
blanchet@55281
   315
      ("", ctxt)
blanchet@55281
   316
      |> add_fix ind xs
blanchet@55281
   317
      |> fold (add_assm ind) assms
blanchet@55281
   318
      |> add_steps ind steps
blanchet@55281
   319
      |> fst
blanchet@55211
   320
  in
blanchet@55211
   321
    (* One-step Metis proofs are pointless; better use the one-liner directly. *)
blanchet@55211
   322
    (case proof of
blanchet@55211
   323
      Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
blanchet@55299
   324
    | Proof ([], [], [Prove (_, [], _, _, [], _, Metis_Method _ :: _, _)]) => ""
blanchet@55211
   325
    | _ =>
blanchet@55211
   326
      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
blanchet@55211
   327
      of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
blanchet@55211
   328
      of_indent 0 ^ (if n <> 1 then "next" else "qed"))
blanchet@55211
   329
  end
blanchet@55211
   330
blanchet@54504
   331
end;