diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML @@ -1,414 +1,398 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) signature SLEDGEHAMMER_COMMANDS = sig type params = Sledgehammer_Prover.params val provers : string Unsynchronized.ref val default_params : theory -> (string * string) list -> params val parse_params: (string * string) list parser end; structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = struct open ATP_Util open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_SMT open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer val runN = "run" val supported_proversN = "supported_provers" val refresh_tptpN = "refresh_tptp" (** Sledgehammer commands **) fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) (*** parameters ***) val provers = Unsynchronized.ref "" type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("spy", "false"), ("abduce", "0"), ("falsify", "false"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), ("uncurried_aliases", "smart"), ("learn", "true"), ("fact_filter", "smart"), ("induction_rules", "smart"), ("max_facts", "smart"), ("fact_thresholds", "0.45 0.85"), ("max_mono_iters", "smart"), ("max_new_mono_instances", "smart"), ("max_proofs", "4"), ("isar_proofs", "smart"), ("compress", "smart"), ("try0", "true"), ("smt_proofs", "true"), ("minimize", "true"), ("slices", string_of_int (12 * Multithreading.max_threads ())), ("preplay_timeout", "1")] val alias_params = [("prover", ("provers", [])), (* undocumented *) ("dont_abduce", ("abduce", ["0"])), ("dont_preplay", ("preplay_timeout", ["0"])), ("dont_compress", ("compress", ["1"])), ("dont_slice", ("slices", ["1"])), ("isar_proof", ("isar_proofs", [])) (* legacy *)] val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), ("dont_falsify", "falsify"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), ("no_isar_proofs", "isar_proofs"), ("dont_minimize", "minimize"), ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse AList.defined (op =) alias_params s orelse AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s orelse s = "expect" fun is_prover_list ctxt s = (case space_explode " " s of ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false) fun unalias_raw_param (name, value) = (case AList.lookup (op =) alias_params name of SOME (name', []) => (name', value) | SOME (param' as (name', _)) => if value <> ["false"] then param' else error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', (case value of ["false"] => ["true"] | ["true"] => ["false"] | [] => ["false"] | _ => value)) | NONE => (name, value))) val any_type_enc = type_enc_of_string Strict "erased" (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" can be omitted. For the last four, this is a secret feature. *) fun normalize_raw_param ctxt = unalias_raw_param #> (fn (name, value) => if is_known_raw_param name then (name, value) else if null value then if is_prover_list ctxt name then ("provers", [name]) else if can (type_enc_of_string Strict) name then ("type_enc", [name]) else if can (trans_lams_of_string ctxt any_type_enc) name then ("lam_trans", [name]) else if member (op =) fact_filters name then ("fact_filter", [name]) else if is_some (Int.fromString name) then ("max_facts", [name]) else error ("Unknown parameter: " ^ quote name) else error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) val implode_param = strip_spaces_except_between_idents o space_implode " " (* FIXME: use "Generic_Data" *) structure Data = Theory_Data ( type T = raw_param list val empty = default_default_params |> map (apsnd single) fun merge data : T = AList.merge (op =) (K true) data ) (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value ctxt = \ \see also \<^system_option>\sledgehammer_provers\\ filter (is_prover_installed ctxt) (smts ctxt @ local_atps) |> implode_param fun set_default_raw_param param thy = let val ctxt = Proof_Context.init_global thy in thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) end fun default_raw_params thy = let val ctxt = Proof_Context.init_global thy in Data.get thy |> fold (AList.default (op =)) [("provers", [(case !provers of "" => default_provers_param_value ctxt | s => s)]), ("timeout", let val timeout = Options.default_int \<^system_option>\sledgehammer_timeout\ in [if timeout <= 0 then "none" else string_of_int timeout] end)] end fun extract_params mode default_params override_params = let val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s | NONE => default_value) val lookup_bool = the o general_lookup_bool false (SOME false) fun lookup_time name = (case lookup name of SOME s => parse_time name s | NONE => Time.zeroTime) fun lookup_int name = (case lookup name of NONE => 0 | SOME s => (case Int.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) | SOME s => (case s |> space_explode " " |> map Real.fromString of [SOME r1, SOME r2] => (r1, r2) | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ \values (e.g., \"0.6 0.95\")"))) fun lookup_option lookup' name = (case lookup name of SOME "smart" => NONE | _ => SOME (lookup' name)) val debug = mode <> Auto_Try andalso lookup_bool "debug" val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val abduce = if mode = Auto_Try then SOME 0 else lookup_option lookup_int "abduce" val falsify = if mode = Auto_Try then SOME false else lookup_option lookup_bool "falsify" val type_enc = if mode = Auto_Try then NONE else (case lookup_string "type_enc" of "smart" => NONE | s => (type_enc_of_string Strict s; SOME s)) val strict = mode = Auto_Try orelse lookup_bool "strict" val lam_trans = lookup_option lookup_string "lam_trans" val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" val learn = lookup_bool "learn" val fact_filter = lookup_option lookup_string "fact_filter" |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) val induction_rules = lookup_option (the o induction_rules_of_string o lookup_string) "induction_rules" val max_facts = lookup_option lookup_int "max_facts" val fact_thresholds = lookup_real_pair "fact_thresholds" val max_mono_iters = lookup_option lookup_int "max_mono_iters" val max_new_mono_instances = lookup_option lookup_int "max_new_mono_instances" val max_proofs = lookup_int "max_proofs" val isar_proofs = lookup_option lookup_bool "isar_proofs" val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") val try0 = lookup_bool "try0" val smt_proofs = lookup_bool "smt_proofs" val minimize = mode <> Auto_Try andalso lookup_bool "minimize" val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices") val timeout = lookup_time "timeout" val preplay_timeout = lookup_time "preplay_timeout" val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, abduce = abduce, falsify = falsify, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end fun get_params mode = extract_params mode o default_raw_params fun default_params thy = get_params Normal thy o map (apsnd single) val silence_state = Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) (* Sledgehammer the given subgoal *) val default_learn_prover_timeout = 2.0 fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = let - (* We generally want chained facts to be picked up by the relevance filter, because it can then - give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, - verbose output, machine learning). However, if the fact is available by no other means (not - even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice - but to insert it into the state as an additional hypothesis. *) - val {facts = chained0, ...} = Proof.goal state0 - val (inserts, keep_chained) = - if null chained0 orelse #only fact_override then - (chained0, []) - else - let val ctxt0 = Proof.context_of state0 in - List.partition (is_useful_unnamed_local_fact ctxt0) chained0 - end - val state = state0 - |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) - |> silence_state - + val state = silence_state state0 val thy = Proof.theory_of state val ctxt = Proof.context_of state val override_params = override_params |> map (normalize_raw_param ctxt) in if subcommand = runN then let val i = the_default 1 opt_i in ignore (run_sledgehammer (get_params Normal thy override_params) Normal writeln_result i fact_override state) end else if subcommand = supported_proversN then supported_provers ctxt else if subcommand = unlearnN then mash_unlearn ctxt else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse subcommand = relearn_isarN orelse subcommand = relearn_proverN then (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); mash_learn ctxt - (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) + (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params". *) (get_params Normal thy ([("timeout", [string_of_real default_learn_prover_timeout]), ("slice", ["false"])] @ override_params @ [("preplay_timeout", ["0"])])) fact_override (#facts (Proof.goal state)) (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) val parse_query_bang = \<^keyword>\?\ || \<^keyword>\!\ || \<^keyword>\!!\ val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (\<^keyword>\=\ |-- parse_value) [] val parse_raw_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_params = parse_raw_params >> map (apsnd implode_param) val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) val parse_fact_override_chunk = (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) || (Args.add |-- Args.colon |-- Scan.succeed [] >> add_fact_override) || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (Args.del |-- Args.colon |-- Scan.succeed [] >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer\ "search for first-order proof using automatic theorem provers" (Scan.optional Parse.name runN -- parse_raw_params -- parse_fact_override -- Scan.option Parse.nat >> (fn (((subcommand, params), fact_override), opt_i) => Toplevel.keep_proof (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) val _ = Outer_Syntax.command \<^command_keyword>\sledgehammer_params\ "set and display the default parameters for Sledgehammer" (parse_raw_params >> (fn params => Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Sledgehammer:\n" ^ (case rev (default_raw_params thy) of [] => "none" | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) val _ = Try.tool_setup {name = sledgehammerN, weight = 40, auto_option = \<^system_option>\auto_sledgehammer\, body = fn auto => fn state => let val thy = Proof.theory_of state val mode = if auto then Auto_Try else Try val i = 1 in run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) |> apsnd (map_prod short_string_of_sledgehammer_outcome single) end} val _ = Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, writeln_result, ...} => (case try Toplevel.proof_of st of SOME state => let val [provers_arg, isar_proofs_arg, try0_arg] = args val override_params = ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), ("try0", [try0_arg]), ("debug", ["false"]), ("verbose", ["false"]), ("overlord", ["false"])]); in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end | NONE => error "Unknown proof context")) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML @@ -1,574 +1,573 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact.ML Author: Jia Meng, Cambridge University Computer Laboratory and NICTA Author: Jasmin Blanchette, TU Muenchen Sledgehammer fact handling. *) 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 is_useful_unnamed_local_fact : Proof.context -> thm -> bool 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 (* gracefully handle huge background theories *) 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) (* TODO: get rid of *) 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 (* FIXME: use structured name *) 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 (* Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as these are definitions arising from packages. *) 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 (* FIXME: put other record thms here, or declare as "no_atp" *) 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) (* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *) 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 (* FIXME: Ad hoc list *) 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 (* FIXME: make more reliable *) 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 (* This is a terrible hack. Free variables are sometimes coded as "M__" when they are displayed as "M" and we want to avoid clashes with these. But sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all prefixes of all free variables. In the worse case scenario, where the fact won't be resolved correctly, the user can fix it manually, e.g., by giving a name to the offending fact. *) 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 (* TODO: rewrite to use nets and/or to reuse existing data structures *) 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, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs val intros = map #1 (Item_Net.content safeIs @ Item_Net.content unsafeIs) (* Add once it is used: val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs |> map Classical.classical_rule *) 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 (* Add once it is used: |> fold (add Elim) elims *) |> 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' (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level facts, so that MaSh can learn from the low-level proofs. *) 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 = Facts.props local_facts |> map #1 |> 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 (* ignore theory name *) 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 (* Names like "xxx" are preferred to "xxx.yyy", which are preferred to "xxx(666)" and the like. "Preferred" means "put to the front of the list". *) ([], ([], [])) |> 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;