src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
author blanchet
Thu Dec 13 23:47:01 2012 +0100 (2012-12-13 ago)
changeset 50523 0799339fea0f
parent 50512 c283bc0a8f1a
child 50586 e31ee2076db1
permissions -rw-r--r--
get rid of some junk facts in the MaSh evaluation driver
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Sledgehammer fact handling.
     6 *)
     7 
     8 signature SLEDGEHAMMER_FACT =
     9 sig
    10   type status = ATP_Problem_Generate.status
    11   type stature = ATP_Problem_Generate.stature
    12 
    13   type fact = ((unit -> string) * stature) * thm
    14 
    15   type fact_override =
    16     {add : (Facts.ref * Attrib.src list) list,
    17      del : (Facts.ref * Attrib.src list) list,
    18      only : bool}
    19 
    20   val ignore_no_atp : bool Config.T
    21   val instantiate_inducts : bool Config.T
    22   val no_fact_override : fact_override
    23   val fact_from_ref :
    24     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    25     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
    26   val backquote_thm : Proof.context -> thm -> string
    27   val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
    28   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
    29   val build_all_names :
    30     (thm -> string) -> ('a * thm) list -> string Symtab.table
    31   val maybe_instantiate_inducts :
    32     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    33     -> (((unit -> string) * 'a) * thm) list
    34   val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    35   val all_facts :
    36     Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    37     -> status Termtab.table -> fact list
    38   val nearly_all_facts :
    39     Proof.context -> bool -> fact_override -> unit Symtab.table
    40     -> status Termtab.table -> thm list -> term list -> term -> fact list
    41 end;
    42 
    43 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
    44 struct
    45 
    46 open ATP_Util
    47 open ATP_Problem_Generate
    48 open Metis_Tactic
    49 open Sledgehammer_Util
    50 
    51 type fact = ((unit -> string) * stature) * thm
    52 
    53 type fact_override =
    54   {add : (Facts.ref * Attrib.src list) list,
    55    del : (Facts.ref * Attrib.src list) list,
    56    only : bool}
    57 
    58 (* experimental features *)
    59 val ignore_no_atp =
    60   Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    61 val instantiate_inducts =
    62   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    63 
    64 val no_fact_override = {add = [], del = [], only = false}
    65 
    66 fun needs_quoting reserved s =
    67   Symtab.defined reserved s orelse
    68   exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
    69 
    70 fun make_name reserved multi j name =
    71   (name |> needs_quoting reserved name ? quote) ^
    72   (if multi then "(" ^ string_of_int j ^ ")" else "")
    73 
    74 fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
    75   | explode_interval max (Facts.From i) = i upto i + max - 1
    76   | explode_interval _ (Facts.Single i) = [i]
    77 
    78 val backquote =
    79   raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
    80 
    81 (* unfolding these can yield really huge terms *)
    82 val risky_defs = @{thms Bit0_def Bit1_def}
    83 
    84 fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
    85 fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
    86   | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
    87   | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
    88   | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
    89   | is_rec_def _ = false
    90 
    91 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
    92 fun is_chained chained = member Thm.eq_thm_prop chained
    93 
    94 fun scope_of_thm global assms chained th =
    95   if is_chained chained th then Chained
    96   else if global then Global
    97   else if is_assum assms th then Assum
    98   else Local
    99 
   100 val may_be_induction =
   101   exists_subterm (fn Var (_, Type (@{type_name fun}, [_, T])) =>
   102                      body_type T = @{typ bool}
   103                    | _ => false)
   104 
   105 fun status_of_thm css name th =
   106   (* FIXME: use structured name *)
   107   if (String.isSubstring ".induct" name orelse
   108       String.isSubstring ".inducts" name) andalso
   109      may_be_induction (prop_of th) then
   110     Induction
   111   else case Termtab.lookup css (prop_of th) of
   112     SOME status => status
   113   | NONE => General
   114 
   115 fun stature_of_thm global assms chained css name th =
   116   (scope_of_thm global assms chained th, status_of_thm css name th)
   117 
   118 fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
   119   let
   120     val ths = Attrib.eval_thms ctxt [xthm]
   121     val bracket =
   122       map (enclose "[" "]" o Pretty.str_of o Args.pretty_src ctxt) args
   123       |> implode
   124     fun nth_name j =
   125       case xref of
   126         Facts.Fact s => backquote s ^ bracket
   127       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
   128       | Facts.Named ((name, _), NONE) =>
   129         make_name reserved (length ths > 1) (j + 1) name ^ bracket
   130       | Facts.Named ((name, _), SOME intervals) =>
   131         make_name reserved true
   132                  (nth (maps (explode_interval (length ths)) intervals) j) name ^
   133         bracket
   134     fun add_nth th (j, rest) =
   135       let val name = nth_name j in
   136         (j + 1, ((name, stature_of_thm false [] chained css name th), th)
   137                 :: rest)
   138       end
   139   in (0, []) |> fold add_nth ths |> snd end
   140 
   141 (* Reject theorems with names like "List.filter.filter_list_def" or
   142   "Accessible_Part.acc.defs", as these are definitions arising from packages. *)
   143 fun is_package_def a =
   144   let val names = Long_Name.explode a in
   145     (length names > 2 andalso not (hd names = "local") andalso
   146      String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
   147   end
   148 
   149 (* FIXME: put other record thms here, or declare as "no_atp" *)
   150 fun multi_base_blacklist ctxt ho_atp =
   151   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
   152    "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
   153    "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
   154    "nibble.distinct"]
   155   |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
   156         append ["induct", "inducts"]
   157   |> map (prefix Long_Name.separator)
   158 
   159 val max_lambda_nesting = 5 (*only applies if not ho_atp*)
   160 
   161 fun term_has_too_many_lambdas max (t1 $ t2) =
   162     exists (term_has_too_many_lambdas max) [t1, t2]
   163   | term_has_too_many_lambdas max (Abs (_, _, t)) =
   164     max = 0 orelse term_has_too_many_lambdas (max - 1) t
   165   | term_has_too_many_lambdas _ _ = false
   166 
   167 (* Don't count nested lambdas at the level of formulas, since they are
   168    quantifiers. *)
   169 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
   170     formula_has_too_many_lambdas (T :: Ts) t
   171   | formula_has_too_many_lambdas Ts t =
   172     if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then
   173       exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
   174     else
   175       term_has_too_many_lambdas max_lambda_nesting t
   176 
   177 (* The maximum apply depth of any "metis" call in "Metis_Examples" (on
   178    2007-10-31) was 11. *)
   179 val max_apply_depth = 18
   180 
   181 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   182   | apply_depth (Abs (_, _, t)) = apply_depth t
   183   | apply_depth _ = 0
   184 
   185 fun is_too_complex ho_atp t =
   186   apply_depth t > max_apply_depth orelse
   187   (not ho_atp andalso formula_has_too_many_lambdas [] t)
   188 
   189 (* FIXME: Ad hoc list *)
   190 val technical_prefixes =
   191   ["ATP", "Code_Evaluation", "DSequence", "Enum", "Lazy_Sequence", "Meson",
   192    "Metis", "Nitpick", "New_DSequence", "New_Random_Sequence", "Quickcheck",
   193    "Quickcheck_Exhaustive", "Quickcheck_Narrowing", "Random_Sequence",
   194    "Sledgehammer", "SMT"]
   195   |> map (suffix Long_Name.separator)
   196 
   197 fun has_technical_prefix s =
   198   exists (fn pref => String.isPrefix pref s) technical_prefixes
   199 val exists_technical_const = exists_Const (has_technical_prefix o fst)
   200 
   201 (* FIXME: make more reliable *)
   202 val exists_low_level_class_const =
   203   exists_Const (fn (s, _) =>
   204      s = @{const_name equal_class.equal} orelse
   205      String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
   206 
   207 fun is_that_fact th =
   208   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
   209   andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
   210                            | _ => false) (prop_of th)
   211 
   212 fun is_likely_tautology_too_meta_or_too_technical th =
   213   let
   214     fun is_interesting_subterm (Const (s, _)) =
   215         not (member (op =) atp_widely_irrelevant_consts s)
   216       | is_interesting_subterm (Free _) = true
   217       | is_interesting_subterm _ = false
   218     fun is_boring_bool t =
   219       not (exists_subterm is_interesting_subterm t) orelse
   220       exists_type (exists_subtype (curry (op =) @{typ prop})) t
   221     fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
   222       | is_boring_prop Ts (@{const "==>"} $ t $ u) =
   223         is_boring_prop Ts t andalso is_boring_prop Ts u
   224       | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
   225         is_boring_prop (T :: Ts) t
   226       | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
   227         is_boring_prop Ts (t $ eta_expand Ts u 1)
   228       | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
   229         is_boring_bool t andalso is_boring_bool u
   230       | is_boring_prop _ _ = true
   231     val t = prop_of th
   232   in
   233     (is_boring_prop [] (prop_of th) andalso
   234      not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
   235     exists_type type_has_top_sort t orelse exists_technical_const t orelse
   236     exists_low_level_class_const t orelse is_that_fact th
   237   end
   238 
   239 fun is_blacklisted_or_something ctxt ho_atp name =
   240   (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
   241   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
   242 
   243 fun hackish_string_for_term ctxt =
   244   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   245 
   246 (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   247    they are displayed as "M" and we want to avoid clashes with these. But
   248    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
   249    prefixes of all free variables. In the worse case scenario, where the fact
   250    won't be resolved correctly, the user can fix it manually, e.g., by giving a
   251    name to the offending fact. *)
   252 fun all_prefixes_of s =
   253   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
   254 
   255 fun close_form t =
   256   (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
   257   |> fold (fn ((s, i), T) => fn (t', taken) =>
   258               let val s' = singleton (Name.variant_list taken) s in
   259                 ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
   260                   else Logic.all_const) T
   261                  $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
   262                  s' :: taken)
   263               end)
   264           (Term.add_vars t [] |> sort_wrt (fst o fst))
   265   |> fst
   266 
   267 fun backquote_term ctxt t =
   268   t |> close_form
   269     |> hackish_string_for_term ctxt
   270     |> backquote
   271 
   272 fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
   273 
   274 fun clasimpset_rule_table_of ctxt =
   275   let
   276     val thy = Proof_Context.theory_of ctxt
   277     val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
   278     fun add stature normalizers get_th =
   279       fold (fn rule =>
   280                let
   281                  val th = rule |> get_th
   282                  val t =
   283                    th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
   284                in
   285                  fold (fn normalize => Termtab.update (normalize t, stature))
   286                       (I :: normalizers)
   287                end)
   288     val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
   289       ctxt |> claset_of |> Classical.rep_cs
   290     val intros = Item_Net.content safeIs @ Item_Net.content hazIs
   291 (* Add once it is used:
   292     val elims =
   293       Item_Net.content safeEs @ Item_Net.content hazEs
   294       |> map Classical.classical_rule
   295 *)
   296     val simps = ctxt |> simpset_of |> dest_ss |> #simps
   297     val specs = ctxt |> Spec_Rules.get
   298     val (rec_defs, nonrec_defs) =
   299       specs |> filter (curry (op =) Spec_Rules.Equational o fst)
   300             |> maps (snd o snd)
   301             |> filter_out (member Thm.eq_thm_prop risky_defs)
   302             |> List.partition (is_rec_def o prop_of)
   303     val spec_intros =
   304       specs |> filter (member (op =) [Spec_Rules.Inductive,
   305                                       Spec_Rules.Co_Inductive] o fst)
   306             |> maps (snd o snd)
   307   in
   308     Termtab.empty |> add Simp [atomize] snd simps
   309                   |> add Rec_Def [] I rec_defs
   310                   |> add Non_Rec_Def [] I nonrec_defs
   311 (* Add once it is used:
   312                   |> add Elim [] I elims
   313 *)
   314                   |> add Intro [] I intros
   315                   |> add Inductive [] I spec_intros
   316   end
   317 
   318 fun normalize_eq (t as @{const Trueprop}
   319         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
   320     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   321     else HOLogic.mk_Trueprop (t0 $ t2 $ t1)
   322   | normalize_eq (t as @{const Trueprop} $ (@{const Not}
   323         $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
   324     if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t
   325     else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
   326   | normalize_eq t = t
   327 
   328 val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
   329 
   330 fun if_thm_before th th' =
   331   if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
   332 
   333 fun build_all_names name_of facts =
   334   Termtab.fold
   335       (fn (_, aliases as main :: _) =>
   336           fold (fn alias =>
   337                    Symtab.update (name_of alias,
   338                                   name_of (if_thm_before main alias))) aliases)
   339       (fold_rev (fn (_, thm) =>
   340                     Termtab.cons_list (normalize_eq_etc (prop_of thm), thm))
   341             facts Termtab.empty)
   342       Symtab.empty
   343 
   344 fun uniquify facts =
   345   Termtab.fold (cons o snd)
   346       (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
   347             Termtab.empty) []
   348 
   349 fun struct_induct_rule_on th =
   350   case Logic.strip_horn (prop_of th) of
   351     (prems, @{const Trueprop}
   352             $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
   353     if not (is_TVar ind_T) andalso length prems > 1 andalso
   354        exists (exists_subterm (curry (op aconv) p)) prems andalso
   355        not (exists (exists_subterm (curry (op aconv) a)) prems) then
   356       SOME (p_name, ind_T)
   357     else
   358       NONE
   359   | _ => NONE
   360 
   361 fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
   362   let
   363     fun varify_noninducts (t as Free (s, T)) =
   364         if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
   365       | varify_noninducts t = t
   366     val p_inst =
   367       concl_prop |> map_aterms varify_noninducts |> close_form
   368                  |> lambda (Free ind_x)
   369                  |> hackish_string_for_term ctxt
   370   in
   371     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   372       stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
   373   end
   374 
   375 fun type_match thy (T1, T2) =
   376   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   377   handle Type.TYPE_MATCH => false
   378 
   379 fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
   380   case struct_induct_rule_on th of
   381     SOME (p_name, ind_T) =>
   382     let val thy = Proof_Context.theory_of ctxt in
   383       stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
   384               |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
   385     end
   386   | NONE => [ax]
   387 
   388 fun external_frees t =
   389   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
   390 
   391 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   392   if Config.get ctxt instantiate_inducts then
   393     let
   394       val thy = Proof_Context.theory_of ctxt
   395       val ind_stmt =
   396         (hyp_ts |> filter_out (null o external_frees), concl_t)
   397         |> Logic.list_implies |> Object_Logic.atomize_term thy
   398       val ind_stmt_xs = external_frees ind_stmt
   399     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   400   else
   401     I
   402 
   403 fun maybe_filter_no_atps ctxt =
   404   not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
   405 
   406 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   407   let
   408     val thy = Proof_Context.theory_of ctxt
   409     val global_facts = Global_Theory.facts_of thy
   410     val local_facts = Proof_Context.facts_of ctxt
   411     val named_locals = local_facts |> Facts.dest_static []
   412     val assms = Assumption.all_assms_of ctxt
   413     fun is_good_unnamed_local th =
   414       not (Thm.has_name_hint th) andalso
   415       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
   416     val unnamed_locals =
   417       union Thm.eq_thm_prop (Facts.props local_facts) chained
   418       |> filter is_good_unnamed_local |> map (pair "" o single)
   419     val full_space =
   420       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
   421     fun add_facts global foldx facts =
   422       foldx (fn (name0, ths) =>
   423         if name0 <> "" andalso
   424            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   425            (Facts.is_concealed facts name0 orelse
   426             not (can (Proof_Context.get_thms ctxt) name0) orelse
   427             (not generous andalso
   428              is_blacklisted_or_something ctxt ho_atp name0)) then
   429           I
   430         else
   431           let
   432             val n = length ths
   433             val multi = n > 1
   434             fun check_thms a =
   435               case try (Proof_Context.get_thms ctxt) a of
   436                 NONE => false
   437               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
   438           in
   439             pair n
   440             #> fold_rev (fn th => fn (j, (multis, unis)) =>
   441                    (j - 1,
   442                     if not (member Thm.eq_thm_prop add_ths th) andalso
   443                        (is_likely_tautology_too_meta_or_too_technical th orelse
   444                         (not generous andalso
   445                          is_too_complex ho_atp (prop_of th))) then
   446                       (multis, unis)
   447                     else
   448                       let
   449                         val new =
   450                           (((fn () =>
   451                                 if name0 = "" then
   452                                   backquote_thm ctxt th
   453                                 else
   454                                   [Facts.extern ctxt facts name0,
   455                                    Name_Space.extern ctxt full_space name0]
   456                                   |> find_first check_thms
   457                                   |> the_default name0
   458                                   |> make_name reserved multi j),
   459                              stature_of_thm global assms chained css name0 th),
   460                            th)
   461                       in
   462                         if multi then (new :: multis, unis)
   463                         else (multis, new :: unis)
   464                       end)) ths
   465             #> snd
   466           end)
   467   in
   468     (* The single-name theorems go after the multiple-name ones, so that single
   469        names are preferred when both are available. *)
   470     ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
   471              |> add_facts true Facts.fold_static global_facts global_facts
   472              |> op @
   473   end
   474 
   475 fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts
   476                      concl_t =
   477   if only andalso null add then
   478     []
   479   else
   480     let
   481       val chained =
   482         chained
   483         |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
   484     in
   485       (if only then
   486          maps (map (fn ((name, stature), th) => ((K name, stature), th))
   487                o fact_from_ref ctxt reserved chained css) add
   488        else
   489          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   490            all_facts ctxt false ho_atp reserved add chained css
   491            |> filter_out (member Thm.eq_thm_prop del o snd)
   492            |> maybe_filter_no_atps ctxt
   493            |> uniquify
   494          end)
   495       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
   496     end
   497 
   498 end;