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