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