src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
author wenzelm
Tue Jun 06 13:13:25 2017 +0200 (2017-06-06)
changeset 66020 a31760eee09d
parent 61756 21c2b1f691d1
child 67399 eab6ce8368fa
permissions -rw-r--r--
discontinued obsolete print mode;
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Basic data structures for representing and basic methods
     6 for dealing with Isar proof texts.
     7 *)
     8 
     9 signature SLEDGEHAMMER_ISAR_PROOF =
    10 sig
    11   type proof_method = Sledgehammer_Proof_Methods.proof_method
    12 
    13   type label = string * int
    14   type facts = label list * string list (* local and global facts *)
    15 
    16   datatype isar_qualifier = Show | Then
    17 
    18   datatype isar_proof =
    19     Proof of (string * typ) list * (label * term) list * isar_step list
    20   and isar_step =
    21     Let of term * term |
    22     Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
    23       * facts * proof_method list * string
    24 
    25   val no_label : label
    26 
    27   val label_ord : label * label -> order
    28   val string_of_label : label -> string
    29   val sort_facts : facts -> facts
    30 
    31   val steps_of_isar_proof : isar_proof -> isar_step list
    32   val label_of_isar_step : isar_step -> label option
    33   val facts_of_isar_step : isar_step -> facts
    34   val proof_methods_of_isar_step : isar_step -> proof_method list
    35 
    36   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
    37   val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
    38   val add_isar_steps : isar_step list -> int -> int
    39 
    40   structure Canonical_Label_Tab : TABLE
    41 
    42   val canonical_label_ord : (label * label) -> order
    43 
    44   val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
    45   val chain_isar_proof : isar_proof -> isar_proof
    46   val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
    47   val relabel_isar_proof_canonically : isar_proof -> isar_proof
    48   val relabel_isar_proof_nicely : isar_proof -> isar_proof
    49   val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof
    50 
    51   val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
    52 end;
    53 
    54 structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    55 struct
    56 
    57 open ATP_Util
    58 open ATP_Proof
    59 open ATP_Problem_Generate
    60 open ATP_Proof_Reconstruct
    61 open Sledgehammer_Util
    62 open Sledgehammer_Proof_Methods
    63 open Sledgehammer_Isar_Annotate
    64 
    65 type label = string * int
    66 type facts = label list * string list (* local and global facts *)
    67 
    68 datatype isar_qualifier = Show | Then
    69 
    70 datatype isar_proof =
    71   Proof of (string * typ) list * (label * term) list * isar_step list
    72 and isar_step =
    73   Let of term * term |
    74   Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
    75     * facts * proof_method list * string
    76 
    77 val no_label = ("", ~1)
    78 
    79 (* cf. "label_ord" below *)
    80 val assume_prefix = "a"
    81 val have_prefix = "f"
    82 
    83 fun label_ord ((s1, i1), (s2, i2)) =
    84   (case int_ord (apply2 String.size (s1, s2)) of
    85     EQUAL =>
    86     (case string_ord (s1, s2) of
    87       EQUAL => int_ord (i1, i2)
    88     | ord => ord (* "assume" before "have" *))
    89   | ord => ord)
    90 
    91 fun string_of_label (s, num) = s ^ string_of_int num
    92 
    93 (* Put the nearest local label first, since it's the most likely to be replaced by a "hence".
    94    (Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *)
    95 fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs)
    96 
    97 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
    98 
    99 fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
   100   | label_of_isar_step _ = NONE
   101 
   102 fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
   103   | subproofs_of_isar_step _ = []
   104 
   105 fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
   106   | facts_of_isar_step _ = ([], [])
   107 
   108 fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
   109   | proof_methods_of_isar_step _ = []
   110 
   111 fun fold_isar_step f step =
   112   fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step
   113 and fold_isar_steps f = fold (fold_isar_step f)
   114 
   115 fun map_isar_steps f =
   116   let
   117     fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
   118     and map_step (step as Let _) = f step
   119       | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
   120         f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
   121   in map_proof end
   122 
   123 val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
   124 
   125 (* canonical proof labels: 1, 2, 3, ... in post traversal order *)
   126 fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
   127 
   128 structure Canonical_Label_Tab = Table(
   129   type key = label
   130   val ord = canonical_label_ord)
   131 
   132 fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
   133     Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
   134   | comment_isar_step _ step = step
   135 fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
   136 
   137 fun chain_qs_lfs NONE lfs = ([], lfs)
   138   | chain_qs_lfs (SOME l0) lfs =
   139     if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs)
   140 
   141 fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
   142     let val (qs', lfs) = chain_qs_lfs lbl lfs in
   143       Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
   144     end
   145   | chain_isar_step _ step = step
   146 and chain_isar_steps _ [] = []
   147   | chain_isar_steps prev (i :: is) =
   148     chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
   149 and chain_isar_proof (Proof (fix, assms, steps)) =
   150   Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
   151 
   152 fun kill_useless_labels_in_isar_proof proof =
   153   let
   154     val used_ls =
   155       fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
   156 
   157     fun kill_label l = if member (op =) used_ls l then l else no_label
   158 
   159     fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
   160         Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
   161       | kill_step step = step
   162     and kill_proof (Proof (fix, assms, steps)) =
   163       Proof (fix, map (apfst kill_label) assms, map kill_step steps)
   164   in
   165     kill_proof proof
   166   end
   167 
   168 fun relabel_isar_proof_canonically proof =
   169   let
   170     fun next_label l (next, subst) =
   171       let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
   172 
   173     fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
   174           (accum as (_, subst)) =
   175         let
   176           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
   177           val ((subs', l'), accum') = accum
   178             |> fold_map relabel_proof subs
   179             ||>> next_label l
   180         in
   181           (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
   182         end
   183       | relabel_step step accum = (step, accum)
   184     and relabel_proof (Proof (fix, assms, steps)) =
   185       fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms
   186       ##>> fold_map relabel_step steps
   187       #>> (fn (assms, steps) => Proof (fix, assms, steps))
   188   in
   189     fst (relabel_proof proof (0, []))
   190   end
   191 
   192 val relabel_isar_proof_nicely =
   193   let
   194     fun next_label depth prefix l (accum as (next, subst)) =
   195       if l = no_label then
   196         (l, accum)
   197       else
   198         let val l' = (replicate_string (depth + 1) prefix, next) in
   199           (l', (next + 1, (l, l') :: subst))
   200         end
   201 
   202     fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
   203           (accum as (_, subst)) =
   204         let
   205           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
   206           val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
   207           val subs' = map (relabel_proof subst' (depth + 1)) subs
   208         in
   209           (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
   210         end
   211       | relabel_step _ step accum = (step, accum)
   212     and relabel_proof subst depth (Proof (fix, assms, steps)) =
   213       (1, subst)
   214       |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms
   215       ||>> fold_map (relabel_step depth) steps
   216       |> (fn ((assms, steps), _) => Proof (fix, assms, steps))
   217   in
   218     relabel_proof [] 0
   219   end
   220 
   221 fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s
   222 
   223 fun rationalize_obtains_in_isar_proofs ctxt =
   224   let
   225     fun rename_obtains xs (subst, ctxt) =
   226       let
   227         val Ts = map snd xs
   228         val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts
   229         val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
   230         val ys = map2 pair new_names Ts
   231       in
   232         (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
   233       end
   234 
   235     fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt =
   236         let
   237           val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt
   238           val t' = subst_atomic subst' t
   239           val subs' = map (rationalize_proof false subst_ctxt') subs
   240         in
   241           (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt')
   242         end
   243     and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) =
   244       let
   245         val (fix', subst_ctxt' as (subst', _)) =
   246           if outer then
   247             (* last call: eliminate any remaining skolem names (from SMT proofs) *)
   248             (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt))
   249           else
   250             rename_obtains fix subst_ctxt
   251       in
   252         Proof (fix', map (apsnd (subst_atomic subst')) assms,
   253           fst (fold_map rationalize_step steps subst_ctxt'))
   254       end
   255   in
   256     rationalize_proof true ([], ctxt)
   257   end
   258 
   259 val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT)
   260 
   261 fun is_thesis ctxt t =
   262   (case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of
   263     SOME (_, t') => HOLogic.mk_Trueprop t' aconv t
   264   | NONE => false)
   265 
   266 val indent_size = 2
   267 
   268 fun string_of_isar_proof ctxt0 i n proof =
   269   let
   270     val keywords = Thy_Header.get_keywords' ctxt0
   271 
   272     (* Make sure only type constraints inserted by the type annotation code are printed. *)
   273     val ctxt = ctxt0
   274       |> Config.put show_markup false
   275       |> Config.put Printer.show_type_emphasis false
   276       |> Config.put show_types false
   277       |> Config.put show_sorts false
   278       |> Config.put show_consts false
   279 
   280     fun add_str s' = apfst (suffix s')
   281 
   282     fun of_indent ind = replicate_string (ind * indent_size) " "
   283     fun of_moreover ind = of_indent ind ^ "moreover\n"
   284     fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
   285 
   286     fun of_obtain qs nr =
   287       (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
   288        else if nr = 1 orelse member (op =) qs Then then "then "
   289        else "") ^ "obtain"
   290 
   291     fun of_show_have qs = if member (op =) qs Show then "show" else "have"
   292     fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have"
   293 
   294     fun of_have qs nr =
   295       if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
   296       else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
   297       else of_show_have qs
   298 
   299     fun add_term term (s, ctxt) =
   300       (s ^ (term
   301             |> singleton (Syntax.uncheck_terms ctxt)
   302             |> annotate_types_in_term ctxt
   303             |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
   304             |> simplify_spaces
   305             |> maybe_quote keywords),
   306        ctxt |> perhaps (try (Variable.auto_fixes term)))
   307 
   308     fun using_facts [] [] = ""
   309       | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
   310 
   311     (* Local facts are always passed via "using", which affects "meson" and "metis". This is
   312        arguably stylistically superior, because it emphasises the structure of the proof. It is also
   313        more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "then"
   314        is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
   315     fun of_method ls ss meth =
   316       let val direct = is_proof_method_direct meth in
   317         using_facts ls (if direct then [] else ss) ^
   318         "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
   319       end
   320 
   321     fun of_free (s, T) =
   322       maybe_quote keywords s ^ " :: " ^
   323       maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
   324 
   325     fun add_frees xs (s, ctxt) =
   326       (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
   327 
   328     fun add_fix _ [] = I
   329       | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
   330 
   331     fun add_assm ind (l, t) =
   332       add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n"
   333 
   334     fun of_subproof ind ctxt proof =
   335       let
   336         val ind = ind + 1
   337         val s = of_proof ind ctxt proof
   338         val prefix = "{ "
   339         val suffix = " }"
   340       in
   341         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   342         String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
   343         suffix ^ "\n"
   344       end
   345     and of_subproofs _ _ _ [] = ""
   346       | of_subproofs ind ctxt qs subs =
   347         (if member (op =) qs Then then of_moreover ind else "") ^
   348         space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
   349     and add_step_pre ind qs subs (s, ctxt) =
   350       (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
   351     and add_step ind (Let (t1, t2)) =
   352         add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2
   353         #> add_str "\n"
   354       | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
   355         add_step_pre ind qs subs
   356         #> (case xs of
   357             [] => add_str (of_have qs (length subs) ^ " ")
   358           | _ =>
   359             add_str (of_obtain qs (length subs) ^ " ")
   360             #> add_frees xs
   361             #> add_str (" where\n" ^ of_indent (ind + 1)))
   362         #> add_str (of_label l)
   363         #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var thesis_var) else t)
   364         #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
   365           (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
   366     and add_steps ind = fold (add_step ind)
   367     and of_proof ind ctxt (Proof (xs, assms, steps)) =
   368       ("", ctxt)
   369       |> add_fix ind xs
   370       |> fold (add_assm ind) assms
   371       |> add_steps ind steps
   372       |> fst
   373   in
   374     (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   375     of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   376     of_indent 0 ^ (if n = 1 then "qed" else "next")
   377   end
   378 
   379 end;