File ‹Tools/Sledgehammer/sledgehammer_fact.ML›
signature SLEDGEHAMMER_FACT =
sig
type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
type lazy_fact = ((unit -> string) * stature) * thm
type fact = (string * stature) * thm
type fact_override =
{add : (Facts.ref * Token.src list) list,
del : (Facts.ref * Token.src list) list,
only : bool}
val sledgehammer_goal_as_fact : string
val no_fact_override : fact_override
val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
Facts.ref * Token.src list -> ((string * stature) * thm) list
val cartouche_thm : Proof.context -> thm -> string
val is_blacklisted_or_something : string -> bool
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val build_name_tables : (thm -> string) -> ('a * thm) list ->
string Symtab.table * string Symtab.table
val fact_distinct : (term * term -> bool) -> ('a * thm) list -> ('a * thm) list
val instantiate_inducts : Proof.context -> term list -> term ->
(((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
val fact_of_lazy_fact : lazy_fact -> fact
val all_facts : Proof.context -> bool -> Keyword.keywords -> thm list -> thm list ->
status Termtab.table -> lazy_fact list
val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
status Termtab.table -> thm list -> term list -> term -> lazy_fact list
val nearly_all_facts_of_context : Proof.context -> bool -> fact_override -> thm list ->
term list -> term -> lazy_fact list
val drop_duplicate_facts : lazy_fact list -> lazy_fact list
end;
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
struct
open ATP_Util
open ATP_Problem_Generate
open Sledgehammer_Util
type lazy_fact = ((unit -> string) * stature) * thm
type fact = (string * stature) * thm
type fact_override =
{add : (Facts.ref * Token.src list) list,
del : (Facts.ref * Token.src list) list,
only : bool}
val local_thisN = Long_Name.localN ^ Long_Name.separator ^ Auto_Bind.thisN
val max_facts_for_duplicates = 50000
val max_facts_for_complex_check = 25000
val max_simps_for_clasimpset = 10000
val sledgehammer_goal_as_fact = "Sledgehammer.goal_as_fact"
val no_fact_override = {add = [], del = [], only = false}
fun needs_quoting keywords s =
Keyword.is_literal keywords s orelse
exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
fun make_name keywords multi j name =
(name |> needs_quoting keywords name ? quote) ^
(if multi then "(" ^ string_of_int j ^ ")" else "")
fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
| explode_interval max (Facts.From i) = i upto i + max - 1
| explode_interval _ (Facts.Single i) = [i]
fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
fun is_rec_def \<^Const_>‹Trueprop for t› = is_rec_def t
| is_rec_def \<^Const_>‹Pure.imp for _ t2› = is_rec_def t2
| is_rec_def \<^Const_>‹Pure.eq _ for t1 t2› = is_rec_eq t1 t2
| is_rec_def \<^Const_>‹HOL.eq _ for t1 t2› = is_rec_eq t1 t2
| is_rec_def _ = false
fun is_assum assms th = exists (fn ct => Thm.prop_of th aconv Thm.term_of ct) assms
fun is_chained chained = member Thm.eq_thm_prop chained
fun scope_of_thm global assms chained th =
if is_chained chained th then Chained
else if global then Global
else if is_assum assms th then Assum
else Local
val may_be_induction =
exists_subterm (fn Var (_, Type (\<^type_name>‹fun›, [_, T])) => body_type T = \<^typ>‹bool›
| _ => false)
fun normalize_vars t =
let
fun normT (Type (s, Ts)) = fold_map normT Ts #>> curry Type s
| normT (TVar (z as (_, S))) =
(fn ((knownT, nT), accum) =>
(case find_index (equal z) knownT of
~1 => (TVar ((Name.uu, nT), S), ((z :: knownT, nT + 1), accum))
| j => (TVar ((Name.uu, nT - j - 1), S), ((knownT, nT), accum))))
| normT (T as TFree _) = pair T
fun norm (t $ u) = norm t ##>> norm u #>> op $
| norm (Const (s, T)) = normT T #>> curry Const s
| norm (Var (z as (_, T))) = normT T
#> (fn (T, (accumT, (known, n))) =>
(case find_index (equal z) known of
~1 => (Var ((Name.uu, n), T), (accumT, (z :: known, n + 1)))
| j => (Var ((Name.uu, n - j - 1), T), (accumT, (known, n)))))
| norm (Abs (_, T, t)) = norm t ##>> normT T #>> (fn (t, T) => Abs (Name.uu, T, t))
| norm (Bound j) = pair (Bound j)
| norm (Free (s, T)) = normT T #>> curry Free s
in fst (norm t (([], 0), ([], 0))) end
fun status_of_thm css name th =
if Termtab.is_empty css then
General
else
let val t = Thm.prop_of th in
if String.isSubstring ".induct" name andalso may_be_induction t then
Induction
else
let val t = normalize_vars t in
(case Termtab.lookup css t of
SOME status => status
| NONE =>
let val concl = Logic.strip_imp_concl t in
(case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl of
SOME lrhss =>
let
val prems = Logic.strip_imp_prems t
val t' = Logic.list_implies (prems, Logic.mk_equals lrhss)
in
Termtab.lookup css t' |> the_default General
end
| NONE => General)
end)
end
end
fun stature_of_thm global assms chained css name th =
(scope_of_thm global assms chained th, status_of_thm css name th)
fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args)
fun nth_name j =
(case xref of
Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
| Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>
make_name keywords true
(nth (maps (explode_interval (length ths)) intervals) j) name ^ bracket)
fun add_nth th (j, rest) =
let val name = nth_name j in
(j + 1, ((name, stature_of_thm false [] chained css name th), th) :: rest)
end
in
(0, []) |> fold add_nth ths |> snd
end
fun is_package_def s =
exists (fn suf => String.isSuffix suf s)
["_case_def", "_rec_def", "_size_def", "_size_overloaded_def"]
andalso
let val ss = Long_Name.explode s in
length ss > 2 andalso not (hd ss = "local")
end
val multi_base_blacklist =
["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps",
"eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps",
"nibble.distinct"]
|> map (prefix Long_Name.separator)
val max_apply_depth = 18
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
| apply_depth (Abs (_, _, t)) = apply_depth t
| apply_depth _ = 0
fun is_too_complex t = apply_depth t > max_apply_depth
val technical_prefixes =
["ATP", "Code_Evaluation", "Datatype", "Enum", "Lazy_Sequence", "Limited_Sequence", "Meson",
"Metis", "Nitpick", "Quickcheck_Random", "Quickcheck_Exhaustive", "Quickcheck_Narrowing",
"Random_Sequence", "Sledgehammer", "SMT"]
|> map (suffix Long_Name.separator)
fun is_technical_const s = exists (fn pref => String.isPrefix pref s) technical_prefixes
val sep_class_sep = Long_Name.separator ^ "class" ^ Long_Name.separator
fun is_low_level_class_const s =
s = \<^const_name>‹equal_class.equal› orelse String.isSubstring sep_class_sep s
val sep_that = Long_Name.separator ^ Auto_Bind.thatN
val skolem_thesis = Name.skolem Auto_Bind.thesisN
fun is_that_fact th =
exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th)
andalso String.isSuffix sep_that (Thm.get_name_hint th)
datatype interest = Deal_Breaker | Interesting | Boring
fun combine_interests Deal_Breaker _ = Deal_Breaker
| combine_interests _ Deal_Breaker = Deal_Breaker
| combine_interests Interesting _ = Interesting
| combine_interests _ Interesting = Interesting
| combine_interests Boring Boring = Boring
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
fun is_likely_tautology_too_meta_or_too_technical th =
let
fun is_interesting_subterm (Const (s, _)) =
not (member (op =) atp_widely_irrelevant_consts s)
| is_interesting_subterm (Free _) = true
| is_interesting_subterm _ = false
fun interest_of_bool t =
if exists_Const ((is_technical_const o fst) orf (is_low_level_class_const o fst) orf
type_has_top_sort o snd) t then
Deal_Breaker
else if exists_type (exists_subtype (curry (op =) \<^typ>‹prop›)) t orelse
not (exists_subterm is_interesting_subterm t) then
Boring
else
Interesting
fun interest_of_prop _ \<^Const_>‹Trueprop for t› = interest_of_bool t
| interest_of_prop Ts \<^Const_>‹Pure.imp for t u› =
combine_interests (interest_of_prop Ts t) (interest_of_prop Ts u)
| interest_of_prop Ts (Const (\<^const_name>‹Pure.all›, _) $ Abs (_, T, t)) =
if type_has_top_sort T then Deal_Breaker else interest_of_prop (T :: Ts) t
| interest_of_prop Ts ((t as Const (\<^const_name>‹Pure.all›, _)) $ u) =
interest_of_prop Ts (t $ eta_expand Ts u 1)
| interest_of_prop _ (Const (\<^const_name>‹Pure.eq›, _) $ t $ u) =
combine_interests (interest_of_bool t) (interest_of_bool u)
| interest_of_prop _ _ = Deal_Breaker
val t = Thm.prop_of th
in
(interest_of_prop [] t <> Interesting andalso not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
is_that_fact th
end
val is_blacklisted_or_something =
let val blist = multi_base_blacklist in
fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist
end
fun all_prefixes_of s = map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
fun close_form t =
(t, [] |> Term.add_free_names t |> maps all_prefixes_of)
|> fold (fn ((s, i), T) => fn (t', taken) =>
let val s' = singleton (Name.variant_list taken) s in
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
else Logic.all_const) T
$ Abs (s', T, abstract_over (Var ((s, i), T), t')),
s' :: taken)
end)
(Term.add_vars t [] |> sort_by (fst o fst))
|> fst
fun cartouche_term ctxt = close_form #> hackish_string_of_term ctxt #> cartouche
fun cartouche_thm ctxt = cartouche_term ctxt o Thm.prop_of
fun clasimpset_rule_table_of ctxt =
let val simps = ctxt |> simpset_of |> dest_ss |> #simps in
if length simps >= max_simps_for_clasimpset then
Termtab.empty
else
let
fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature)
val {safeIs, unsafeIs, ...} =
ctxt |> claset_of |> Classical.rep_cs
val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs)
val specs = Spec_Rules.get ctxt
val (rec_defs, nonrec_defs) = specs
|> filter (Spec_Rules.is_equational o #rough_classification)
|> maps #rules
|> List.partition (is_rec_def o Thm.prop_of)
val spec_intros = specs
|> filter (Spec_Rules.is_relational o #rough_classification)
|> maps #rules
in
Termtab.empty
|> fold (add Simp o snd) simps
|> fold (add Rec_Def) rec_defs
|> fold (add Non_Rec_Def) nonrec_defs
|> fold (add Intro) intros
|> fold (add Inductive) spec_intros
end
end
fun normalize_eq (\<^Const_>‹Trueprop› $ (t as (t0 as Const (\<^const_name>‹HOL.eq›, _)) $ t1 $ t2)) =
if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1
| normalize_eq (\<^Const_>‹Trueprop› $ (t as \<^Const_>‹Not›
$ ((t0 as Const (\<^const_name>‹HOL.eq›, _)) $ t1 $ t2))) =
if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1)
| normalize_eq (Const (\<^const_name>‹Pure.eq›, Type (_, [T, _])) $ t1 $ t2) =
(if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then (t1, t2) else (t2, t1))
|> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
| normalize_eq t = t
fun if_thm_before th th' =
if Context.subthy_id (apply2 Thm.theory_id (th, th')) then th else th'
fun un_class_ify s =
(case first_field "_class" s of
SOME (pref, suf) => [s, pref ^ suf]
| NONE => [s])
fun build_name_tables name_of facts =
let
fun cons_thm (_, th) = Termtab.cons_list (normalize_vars (normalize_eq (Thm.prop_of th)), th)
fun add_plain canon alias =
Symtab.update (Thm.get_name_hint alias, name_of (if_thm_before canon alias))
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
fun add_inclass (name, target) = fold (fn s => Symtab.update (s, target)) (un_class_ify name)
val prop_tab = fold cons_thm facts Termtab.empty
val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
in
(plain_name_tab, inclass_name_tab)
end
fun fact_distinct eq facts =
fold (fn (i, fact as (_, th)) =>
Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd))
(normalize_eq (Thm.prop_of th), (i, fact)))
(tag_list 0 facts) Net.empty
|> Net.entries
|> sort (int_ord o apply2 fst)
|> map snd
fun struct_induct_rule_on th =
(case Logic.strip_horn (Thm.prop_of th) of
(prems, \<^Const_>‹Trueprop› $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
if not (is_TVar ind_T) andalso length prems > 1 andalso
exists (exists_subterm (curry (op aconv) p)) prems andalso
not (exists (exists_subterm (curry (op aconv) a)) prems) then
SOME (p_name, ind_T)
else
NONE
| _ => NONE)
val instantiate_induct_timeout = seconds 0.01
fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
let
fun varify_noninducts (t as Free (s, T)) =
if (s, T) = ind_x then t else Var ((s, 0), T)
| varify_noninducts t = t
val p_inst = concl_prop
|> map_aterms varify_noninducts
|> close_form
|> lambda (Free ind_x)
|> hackish_string_of_term ctxt
in
((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature),
th |> Rule_Insts.read_instantiate ctxt [(((p_name, 0), Position.none), p_inst)] [])
end
fun type_match thy (T1, T2) =
(Sign.typ_match thy (T2, T1) Vartab.empty; true)
handle Type.TYPE_MATCH => false
fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
(case struct_induct_rule_on th of
SOME (p_name, ind_T) =>
let val thy = Proof_Context.theory_of ctxt in
stmt_xs
|> filter (fn (_, T) => type_match thy (T, ind_T))
|> map_filter (try (Timeout.apply instantiate_induct_timeout
(instantiate_induct_rule ctxt stmt p_name ax)))
end
| NONE => [ax])
fun external_frees t =
[] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
fun instantiate_inducts ctxt hyp_ts concl_t =
let
val ind_stmt =
(hyp_ts |> filter_out (null o external_frees), concl_t)
|> Logic.list_implies |> Object_Logic.atomize_term ctxt
val ind_stmt_xs = external_frees ind_stmt
in
maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
end
fun fact_of_lazy_fact ((name, stature), th) = ((name (), stature), th)
fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
fun is_useful_unnamed_local_fact ctxt =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
val local_facts = Proof_Context.facts_of ctxt
val named_locals = Facts.dest_static true [global_facts] local_facts
|> maps (map (normalize_eq o Thm.prop_of) o snd)
in
fn th =>
not (Thm.has_name_hint th) andalso
not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th)))
end
fun all_facts ctxt generous keywords add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
val transfer = Global_Theory.transfer_theories thy
val global_facts = Global_Theory.facts_of thy
val is_too_complex =
if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false
else is_too_complex
val local_facts = Proof_Context.facts_of ctxt
val assms = Assumption.all_assms_of ctxt
val named_locals = Facts.dest_static true [global_facts] local_facts
val unnamed_locals =
chained @ map #1 (Facts.props local_facts)
|> filter (is_useful_unnamed_local_fact ctxt)
|> map (pair "" o single)
val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
fun add_facts global foldx facts =
foldx (fn (name0, ths) => fn accum =>
if name0 <> "" andalso
(Long_Name.is_hidden (Facts.intern facts name0) orelse
((Facts.is_concealed facts name0 orelse
(not generous andalso is_blacklisted_or_something name0)) andalso
forall (not o member Thm.eq_thm_prop add_ths) ths)) then
accum
else
let
val n = length ths
val collection = n > 1
val dotted_name = Long_Name.count name0 > 2
fun check_thms a =
(case try (Proof_Context.get_thms ctxt) a of
NONE => false
| SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
in
snd (fold_rev (fn th0 => fn (j, accum) =>
let val th = transfer th0 in
(j - 1,
if not (member Thm.eq_thm_prop add_ths th) andalso
(is_likely_tautology_too_meta_or_too_technical th orelse
is_too_complex (Thm.prop_of th)) then
accum
else
let
fun get_name () =
if name0 = "" orelse name0 = local_thisN then
cartouche_thm ctxt th
else
let val short_name = Facts.extern ctxt facts name0 in
if check_thms short_name then
short_name
else
let val long_name = Name_Space.extern ctxt full_space name0 in
if check_thms long_name then
long_name
else
name0
end
end
|> make_name keywords collection j
val stature = stature_of_thm global assms chained css name0 th
val new = ((get_name, stature), th)
in
(if collection then apsnd o apsnd
else if dotted_name then apsnd o apfst
else apfst) (cons new) accum
end)
end) ths (n, accum))
end)
in
([], ([], []))
|> add_facts false fold local_facts (unnamed_locals @ named_locals)
|> add_facts true Facts.fold_static global_facts global_facts
||> op @ |> op @
end
fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t =
if only andalso null add then
[]
else
let
val chained = chained |> maps (fn th => insert Thm.eq_thm_prop (zero_var_indexes th) [th])
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
o fact_of_ref ctxt keywords chained css) add
else
let
val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del)
val facts =
all_facts ctxt false keywords add chained css
|> filter_out ((member Thm.eq_thm_prop del orf
(Named_Theorems.member ctxt \<^named_theorems>‹no_atp› andf
not o member Thm.eq_thm_prop add)) o snd)
in
facts
end)
|> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
end
fun nearly_all_facts_of_context ctxt inst_inducts fact_override =
let
val keywords = Thy_Header.get_keywords' ctxt
val css = clasimpset_rule_table_of ctxt
in
nearly_all_facts ctxt inst_inducts fact_override keywords css
end
fun drop_duplicate_facts facts =
let val num_facts = length facts in
facts |> num_facts <= max_facts_for_duplicates ? fact_distinct (op aconv)
end
end;