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