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