# HG changeset patch # User bulwahn # Date 1342007979 -7200 # Node ID b88c3e0b752e9f89c9b3e71c6ddb5c62358aed74 # Parent b149de01d669532ec7826f24d285b227aa1bf037# Parent 713e32be9845fbf08da164f8dcd325341de9246b merged diff -r b149de01d669 -r b88c3e0b752e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 11 13:59:39 2012 +0200 @@ -1147,8 +1147,10 @@ $(LOG)/HOL-TPTP.gz: $(OUT)/HOL \ TPTP/ATP_Problem_Import.thy \ TPTP/ATP_Theory_Export.thy \ + TPTP/MaSh_Export.thy \ + TPTP/MaSh_Import.thy \ + TPTP/ROOT.ML \ TPTP/THF_Arith.thy \ - TPTP/ROOT.ML \ TPTP/TPTP_Parser.thy \ TPTP/TPTP_Parser/ml_yacc_lib.ML \ TPTP/TPTP_Parser/tptp_interpret.ML \ @@ -1159,6 +1161,8 @@ TPTP/TPTP_Parser_Test.thy \ TPTP/atp_problem_import.ML \ TPTP/atp_theory_export.ML \ + TPTP/mash_export.ML \ + TPTP/mash_import.ML \ TPTP/sledgehammer_tactics.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/ATP_Theory_Export.thy --- a/src/HOL/TPTP/ATP_Theory_Export.thy Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/TPTP/ATP_Theory_Export.thy Wed Jul 11 13:59:39 2012 +0200 @@ -16,52 +16,14 @@ ML {* val do_it = false; (* switch to "true" to generate the files *) -val thy = @{theory Complex_Main}; +val thy = @{theory}; val ctxt = @{context} *} - -(* MaSh *) - -ML {* -if do_it then - "/tmp/mash_sample_problem.out" - |> generate_mash_problem_file_for_theory thy -else - () -*} - ML {* if do_it then - "/tmp/mash_accessibility.out" - |> generate_mash_accessibility_file_for_theory thy false -else - () -*} - -ML {* -if do_it then - "/tmp/mash_features.out" - |> generate_mash_feature_file_for_theory thy false -else - () -*} - -ML {* -if do_it then - "/tmp/mash_dependencies.out" - |> generate_mash_dependency_file_for_theory thy false -else - () -*} - - -(* TPTP/DFG *) - -ML {* -if do_it then "/tmp/infs_poly_guards_query_query.tptp" - |> generate_tptp_inference_file_for_theory ctxt thy FOF + |> generate_atp_inference_file_for_theory ctxt thy FOF "poly_guards_query_query" else () @@ -70,7 +32,7 @@ ML {* if do_it then "/tmp/infs_poly_tags_query_query.tptp" - |> generate_tptp_inference_file_for_theory ctxt thy FOF + |> generate_atp_inference_file_for_theory ctxt thy FOF "poly_tags_query_query" else () @@ -79,7 +41,7 @@ ML {* if do_it then "/tmp/axs_tc_native.dfg" - |> generate_tptp_inference_file_for_theory ctxt thy (DFG Polymorphic) + |> generate_atp_inference_file_for_theory ctxt thy (DFG Polymorphic) "tc_native" else () diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/MaSh_Export.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 13:59:39 2012 +0200 @@ -0,0 +1,48 @@ +(* Title: HOL/TPTP/MaSh_Export.thy + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* MaSh Exporter *} + +theory MaSh_Export +imports ATP_Theory_Export +uses "mash_export.ML" +begin + +sledgehammer_params [provers = e, max_relevant = 500] + +ML {* +open MaSh_Export +*} + +ML {* +val do_it = false (* switch to "true" to generate the files *); +val thy = @{theory List} +*} + +ML {* +if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions" +else () +*} + +ML {* +if do_it then generate_mash_commands thy "/tmp/mash_commands" +else () +*} + +ML {* +if do_it then generate_mash_features thy false "/tmp/mash_features" +else () +*} + +ML {* +if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility" +else () +*} + +ML {* +if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies" +else () +*} + +end diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/MaSh_Import.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 13:59:39 2012 +0200 @@ -0,0 +1,32 @@ +(* Title: HOL/TPTP/MaSh_Import.thy + Author: Jasmin Blanchette, TU Muenchen +*) + +header {* MaSh Importer *} + +theory MaSh_Import +imports MaSh_Export +uses "mash_import.ML" +begin + +sledgehammer_params + [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, + lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] + +declare [[sledgehammer_instantiate_inducts]] + +ML {* +open MaSh_Import +*} + +ML {* +val do_it = false (* switch to "true" to generate the files *); +val thy = @{theory Nat} +*} + +ML {* +if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions" +else () +*} + +end diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/ROOT.ML --- a/src/HOL/TPTP/ROOT.ML Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/TPTP/ROOT.ML Wed Jul 11 13:59:39 2012 +0200 @@ -8,6 +8,7 @@ use_thys [ "ATP_Theory_Export", + "MaSh_Import", "TPTP_Interpret", "THF_Arith" ]; diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 13:59:39 2012 +0200 @@ -2,68 +2,30 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2011 -Export Isabelle theories as MaSh (Machine-learning for Sledgehammer) or as -first-order TPTP inferences. +Export Isabelle theories as first-order TPTP inferences. *) signature ATP_THEORY_EXPORT = sig type atp_format = ATP_Problem.atp_format + type stature = Sledgehammer_Filter.stature val theorems_mentioned_in_proof_term : string list option -> thm -> string list - val generate_mash_accessibility_file_for_theory : - theory -> bool -> string -> unit - val generate_mash_feature_file_for_theory : theory -> bool -> string -> unit - val generate_mash_dependency_file_for_theory : - theory -> bool -> string -> unit - val generate_mash_problem_file_for_theory : theory -> string -> unit - val generate_tptp_inference_file_for_theory : + val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list + val generate_atp_inference_file_for_theory : Proof.context -> theory -> atp_format -> string -> string -> unit end; -structure ATP_Theory_Export (* ### : ATP_THEORY_EXPORT *) = +structure ATP_Theory_Export : ATP_THEORY_EXPORT = struct open ATP_Problem open ATP_Proof open ATP_Problem_Generate open ATP_Systems -open ATP_Util -fun stringN_of_int 0 _ = "" - | stringN_of_int k n = - stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) - -fun escape_meta_char c = - if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse - c = #")" then - String.str c - else if c = #"'" then - "~" - else - (* fixed width, in case more digits follow *) - "\\" ^ stringN_of_int 3 (Char.ord c) -val escape_meta = String.translate escape_meta_char - -val fact_name_of = escape_meta -val thy_name_of = escape_meta -val const_name_of = prefix const_prefix o escape_meta -val type_name_of = prefix type_const_prefix o escape_meta -val class_name_of = prefix class_prefix o escape_meta - -val thy_name_of_thm = theory_of_thm #> Context.theory_name - -fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) - -fun facts_of thy = - let val ctxt = Proof_Context.init_global thy in - Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] - (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) - |> filter (curry (op =) @{typ bool} o fastype_of - o Object_Logic.atomize_term thy o prop_of o snd) - |> rev - end +val fact_name_of = prefix fact_prefix o ascii_of (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to be missing over there; or maybe the two code portions are @@ -95,215 +57,15 @@ fun collect (s, _, _) = is_name_ok s ? insert (op =) s val names = [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] - |> map fact_name_of in names end -fun raw_interesting_const_names thy = +fun all_facts_of_theory thy = let val ctxt = Proof_Context.init_global thy in - Sledgehammer_Filter.const_names_in_fact thy - (Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) + Sledgehammer_Filter.all_facts ctxt false Symtab.empty true [] [] + (Sledgehammer_Filter.clasimpset_rule_table_of ctxt) + |> rev (* try to restore the original order of facts, for MaSh *) end -fun interesting_const_names thy = - raw_interesting_const_names thy - #> map const_name_of - #> sort_distinct string_ord - -fun interesting_type_and_class_names t = - let - val bad = [@{type_name prop}, @{type_name bool}, @{type_name fun}] - val add_classes = - subtract (op =) @{sort type} #> map class_name_of #> union (op =) - fun maybe_add_type (Type (s, Ts)) = - (not (member (op =) bad s) ? insert (op =) (type_name_of s)) - #> fold maybe_add_type Ts - | maybe_add_type (TFree (_, S)) = add_classes S - | maybe_add_type (TVar (_, S)) = add_classes S - in [] |> fold_types maybe_add_type t end - -fun theory_ord p = - if Theory.eq_thy p then EQUAL - else if Theory.subthy p then LESS - else if Theory.subthy (swap p) then GREATER - else EQUAL - -val thm_ord = theory_ord o pairself theory_of_thm - -fun parent_thms thy_ths thy = - Theory.parents_of thy - |> map (thy_name_of o Context.theory_name) - |> map_filter (AList.lookup (op =) thy_ths) - |> map List.last - |> map (fact_name_of o Thm.get_name_hint) - -val thms_by_thy = - map (snd #> `thy_name_of_thm) - #> AList.group (op =) - #> sort (int_ord - o pairself (length o Theory.ancestors_of o theory_of_thm o hd o snd)) - #> map (apsnd (sort thm_ord)) - -fun generate_mash_accessibility_file_for_theory thy include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - fun do_thm th prevs = - let - val s = th ^ ": " ^ space_implode " " prevs ^ "\n" - val _ = File.append path s - in [th] end - val thy_ths = - facts_of thy - |> not include_thy ? filter_out (has_thy thy o snd) - |> thms_by_thy - fun do_thy ths = - let - val thy = theory_of_thm (hd ths) - val parents = parent_thms thy_ths thy - val ths = ths |> map (fact_name_of o Thm.get_name_hint) - val _ = fold do_thm ths parents - in () end - val _ = List.app (do_thy o snd) thy_ths - in () end - -fun has_bool @{typ bool} = true - | has_bool (Type (_, Ts)) = exists has_bool Ts - | has_bool _ = false - -fun has_fun (Type (@{type_name fun}, _)) = true - | has_fun (Type (_, Ts)) = exists has_fun Ts - | has_fun _ = false - -val is_conn = member (op =) - [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, - @{const_name HOL.implies}, @{const_name Not}, - @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, - @{const_name HOL.eq}] - -val has_bool_arg_const = - exists_Const (fn (c, T) => - not (is_conn c) andalso exists has_bool (binder_types T)) - -fun higher_inst_const thy (c, T) = - case binder_types T of - [] => false - | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts - -val binders = [@{const_name All}, @{const_name Ex}] - -fun is_fo_term thy t = - let - val t = - t |> Envir.beta_eta_contract - |> transform_elim_prop - |> Object_Logic.atomize_term thy - in - Term.is_first_order binders t andalso - not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T - | _ => false) t orelse - has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) - end - -val is_skolem = String.isSubstring Sledgehammer_Filter.pseudo_skolem_prefix -val is_abs = String.isSubstring Sledgehammer_Filter.pseudo_abs_name - -(* TODO: Add types, subterms *) -fun features_of thy (status, th) = - let val prop = Thm.prop_of th in - interesting_const_names thy prop @ - interesting_type_and_class_names prop - |> (fn feats => - case List.partition is_skolem feats of - ([], feats) => feats - | (_, feats) => "skolem" :: feats) - |> (fn feats => - case List.partition is_abs feats of - ([], feats) => feats - | (_, feats) => "abs" :: feats) - |> not (is_fo_term thy prop) ? cons "ho" - |> (case status of - General => I - | Induction => cons "induction" - | Intro => cons "intro" - | Inductive => cons "inductive" - | Elim => cons "elim" - | Simp => cons "simp" - | Def => cons "def") - end - -fun generate_mash_feature_file_for_theory thy include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val facts = facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) - fun do_fact ((_, (_, status)), th) = - let - val name = Thm.get_name_hint th - val feats = features_of thy (status, th) - val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" - in File.append path s end - val _ = List.app do_fact facts - in () end - -val dependencies_of = theorems_mentioned_in_proof_term o SOME - -val known_tautologies = - [@{thm All_def}, @{thm Ex_def}, @{thm Ex1_def}, @{thm Ball_def}, - @{thm Bex_def}, @{thm If_def}] - -fun is_likely_tautology thy th = - (member Thm.eq_thm_prop known_tautologies th orelse - th |> prop_of |> raw_interesting_const_names thy - |> forall (is_skolem orf is_abs)) andalso - not (Thm.eq_thm_prop (@{thm ext}, th)) - -fun generate_mash_dependency_file_for_theory thy include_thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val ths = - facts_of thy |> not include_thy ? filter_out (has_thy thy o snd) - |> map snd - val all_names = - ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint - fun do_thm th = - let - val name = Thm.get_name_hint th - val deps = dependencies_of all_names th - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" - in File.append path s end - val _ = List.app do_thm ths - in () end - -fun generate_mash_problem_file_for_theory thy file_name = - let - val path = file_name |> Path.explode - val _ = File.write path "" - val facts = facts_of thy - val (new_facts, old_facts) = - facts |> List.partition (has_thy thy o snd) - |>> sort (thm_ord o pairself snd) - val ths = facts |> map snd - val all_names = - ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint - fun do_fact ((_, (_, status)), th) prevs = - let - val name = Thm.get_name_hint th - val feats = features_of thy (status, th) - val deps = dependencies_of all_names th - val th = fact_name_of name - val s = - th ^ ": " ^ - space_implode " " prevs ^ "; " ^ - space_implode " " feats ^ "; " ^ - space_implode " " deps ^ "\n" - val _ = File.append path s - in [th] end - val thy_ths = old_facts |> thms_by_thy - val parents = parent_thms thy_ths thy - val _ = fold do_fact new_facts parents - in () end - fun inference_term [] = NONE | inference_term ss = ATerm (("inference", []), @@ -384,14 +146,14 @@ handle TYPE _ => @{prop True} end -fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name = +fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = let val type_enc = type_enc |> type_enc_from_string Strict |> adjust_type_enc format val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = facts_of thy + val facts = all_facts_of_theory thy val atp_problem = facts |> map (fn ((_, loc), th) => @@ -404,12 +166,12 @@ atp_problem |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) val ths = facts |> map snd - val all_names = - ths |> filter_out (is_likely_tautology thy) |> map Thm.get_name_hint + val all_names = ths |> map Thm.get_name_hint val infers = facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), - theorems_mentioned_in_proof_term (SOME all_names) th)) + th |> theorems_mentioned_in_proof_term (SOME all_names) + |> map fact_name_of)) val all_atp_problem_names = atp_problem |> maps (map ident_of_problem_line o snd) val infers = diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/mash_export.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 13:59:39 2012 +0200 @@ -0,0 +1,341 @@ +(* Title: HOL/TPTP/mash_export.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer). +*) + +signature MASH_EXPORT = +sig + type stature = ATP_Problem_Generate.stature + + val non_tautological_facts_of : + theory -> (((unit -> string) * stature) * thm) list + val theory_ord : theory * theory -> order + val thm_ord : thm * thm -> order + val dependencies_of : string list -> thm -> string list + val goal_of_thm : thm -> thm + val meng_paulson_facts : + Proof.context -> string -> int -> real * real -> thm -> int + -> (((unit -> string) * stature) * thm) list + -> ((string * stature) * thm) list + val generate_mash_accessibility : theory -> bool -> string -> unit + val generate_mash_features : theory -> bool -> string -> unit + val generate_mash_dependencies : theory -> bool -> string -> unit + val generate_mash_commands : theory -> string -> unit + val generate_meng_paulson_suggestions : + Proof.context -> theory -> string -> unit +end; + +structure MaSh_Export : MASH_EXPORT = +struct + +open ATP_Problem_Generate +open ATP_Util + +fun stringN_of_int 0 _ = "" + | stringN_of_int k n = + stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) + +fun escape_meta_char c = + if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse + c = #")" orelse c = #"," then + String.str c + else + (* fixed width, in case more digits follow *) + "\\" ^ stringN_of_int 3 (Char.ord c) + +val escape_meta = String.translate escape_meta_char + +val thy_prefix = "y_" + +val fact_name_of = escape_meta +val thy_name_of = prefix thy_prefix o escape_meta +val const_name_of = prefix const_prefix o escape_meta +val type_name_of = prefix type_const_prefix o escape_meta +val class_name_of = prefix class_prefix o escape_meta + +val thy_name_of_thm = theory_of_thm #> Context.theory_name + +local + +fun has_bool @{typ bool} = true + | has_bool (Type (_, Ts)) = exists has_bool Ts + | has_bool _ = false + +fun has_fun (Type (@{type_name fun}, _)) = true + | has_fun (Type (_, Ts)) = exists has_fun Ts + | has_fun _ = false + +val is_conn = member (op =) + [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj}, + @{const_name HOL.implies}, @{const_name Not}, + @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex}, + @{const_name HOL.eq}] + +val has_bool_arg_const = + exists_Const (fn (c, T) => + not (is_conn c) andalso exists has_bool (binder_types T)) + +fun higher_inst_const thy (c, T) = + case binder_types T of + [] => false + | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts + +val binders = [@{const_name All}, @{const_name Ex}] + +in + +fun is_fo_term thy t = + let + val t = + t |> Envir.beta_eta_contract + |> transform_elim_prop + |> Object_Logic.atomize_term thy + in + Term.is_first_order binders t andalso + not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T + | _ => false) t orelse + has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t) + end + +end + +fun interesting_terms_types_and_classes term_max_depth type_max_depth t = + let + val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] + val bad_consts = atp_widely_irrelevant_consts + val add_classes = + subtract (op =) @{sort type} #> map class_name_of #> union (op =) + fun do_add_type (Type (s, Ts)) = + (not (member (op =) bad_types s) ? insert (op =) (type_name_of s)) + #> fold do_add_type Ts + | do_add_type (TFree (_, S)) = add_classes S + | do_add_type (TVar (_, S)) = add_classes S + fun add_type T = type_max_depth >= 0 ? do_add_type T + fun mk_app s args = + if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" + else s + fun patternify ~1 _ = "" + | patternify depth t = + case strip_comb t of + (Const (s, _), args) => + mk_app (const_name_of s) (map (patternify (depth - 1)) args) + | _ => "" + fun add_term_patterns ~1 _ = I + | add_term_patterns depth t = + insert (op =) (patternify depth t) + #> add_term_patterns (depth - 1) t + val add_term = add_term_patterns term_max_depth + fun add_patterns t = + let val (head, args) = strip_comb t in + (case head of + Const (s, T) => + not (member (op =) bad_consts s) ? (add_term t #> add_type T) + | Free (_, T) => add_type T + | Var (_, T) => add_type T + | Abs (_, T, body) => add_type T #> add_patterns body + | _ => I) + #> fold add_patterns args + end + in [] |> add_patterns t |> sort string_ord end + +fun is_likely_tautology th = + null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso + not (Thm.eq_thm_prop (@{thm ext}, th)) + +fun is_too_meta thy th = + fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool} + +fun non_tautological_facts_of thy = + all_facts_of_theory thy + |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd) + +fun theory_ord p = + if Theory.eq_thy p then EQUAL + else if Theory.subthy p then LESS + else if Theory.subthy (swap p) then GREATER + else EQUAL + +val thm_ord = theory_ord o pairself theory_of_thm + +fun thms_by_thy ths = + ths |> map (snd #> `thy_name_of_thm) + |> AList.group (op =) + |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm + o hd o snd)) + |> map (apsnd (sort thm_ord)) + +fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) + +fun parent_thms thy_ths thy = + Theory.parents_of thy + |> map Context.theory_name + |> map_filter (AList.lookup (op =) thy_ths) + |> map List.last + |> map (fact_name_of o Thm.get_name_hint) + +fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) + +val max_depth = 1 + +(* TODO: Generate type classes for types? *) +fun features_of thy (status, th) = + let val t = Thm.prop_of th in + thy_name_of (thy_name_of_thm th) :: + interesting_terms_types_and_classes max_depth max_depth t + |> not (has_no_lambdas t) ? cons "lambdas" + |> exists_Const is_exists t ? cons "skolems" + |> not (is_fo_term thy t) ? cons "ho" + |> (case status of + General => I + | Induction => cons "induction" + | Intro => cons "intro" + | Inductive => cons "inductive" + | Elim => cons "elim" + | Simp => cons "simp" + | Def => cons "def") + end + +val dependencies_of = + map fact_name_of oo theorems_mentioned_in_proof_term o SOME + +val freezeT = Type.legacy_freeze_type + +fun freeze (t $ u) = freeze t $ freeze u + | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t) + | freeze (Var ((s, _), T)) = Free (s, freezeT T) + | freeze (Const (s, T)) = Const (s, freezeT T) + | freeze (Free (s, T)) = Free (s, freezeT T) + | freeze t = t + +val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init + +fun meng_paulson_facts ctxt prover_name max_relevant relevance_thresholds + goal i = + let + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i + val is_built_in_const = + Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name + val relevance_fudge = + Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name + val relevance_override = {add = [], del = [], only = false} + in + Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + max_relevant is_built_in_const relevance_fudge relevance_override [] + hyp_ts concl_t + end + +fun generate_mash_accessibility thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + fun do_thm th prevs = + let + val s = th ^ ": " ^ space_implode " " prevs ^ "\n" + val _ = File.append path s + in [th] end + val thy_ths = + non_tautological_facts_of thy + |> not include_thy ? filter_out (has_thy thy o snd) + |> thms_by_thy + fun do_thy ths = + let + val thy = theory_of_thm (hd ths) + val parents = parent_thms thy_ths thy + val ths = ths |> map (fact_name_of o Thm.get_name_hint) + in fold do_thm ths parents; () end + in List.app (do_thy o snd) thy_ths end + +fun generate_mash_features thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = + non_tautological_facts_of thy + |> not include_thy ? filter_out (has_thy thy o snd) + fun do_fact ((_, (_, status)), th) = + let + val name = Thm.get_name_hint th + val feats = features_of thy (status, th) + val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" + in File.append path s end + in List.app do_fact facts end + +fun generate_mash_dependencies thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val ths = + non_tautological_facts_of thy + |> not include_thy ? filter_out (has_thy thy o snd) + |> map snd + val all_names = ths |> map Thm.get_name_hint + fun do_thm th = + let + val name = Thm.get_name_hint th + val deps = dependencies_of all_names th + val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" + in File.append path s end + in List.app do_thm ths end + +fun generate_mash_commands thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = non_tautological_facts_of thy + val (new_facts, old_facts) = + facts |> List.partition (has_thy thy o snd) + |>> sort (thm_ord o pairself snd) + val ths = facts |> map snd + val all_names = ths |> map Thm.get_name_hint + fun do_fact ((_, (_, status)), th) prevs = + let + val name = Thm.get_name_hint th + val feats = features_of thy (status, th) + val deps = dependencies_of all_names th + val kind = Thm.legacy_get_kind th + val name = fact_name_of name + val core = + name ^ ": " ^ space_implode " " prevs ^ "; " ^ space_implode " " feats + val query = if kind <> "" then "? " ^ core ^ "\n" else "" + val update = "! " ^ core ^ "; " ^ space_implode " " deps ^ "\n" + val _ = File.append path (query ^ update) + in [name] end + val thy_ths = old_facts |> thms_by_thy + val parents = parent_thms thy_ths thy + in fold do_fact new_facts parents; () end + +fun generate_meng_paulson_suggestions ctxt thy file_name = + let + val {provers, max_relevant, relevance_thresholds, ...} = + Sledgehammer_Isar.default_params ctxt [] + val prover_name = hd provers + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = non_tautological_facts_of thy + val (new_facts, old_facts) = + facts |> List.partition (has_thy thy o snd) + |>> sort (thm_ord o pairself snd) + val i = 1 + fun do_fact (fact as (_, th)) old_facts = + let + val name = Thm.get_name_hint th + val goal = goal_of_thm th + val kind = Thm.legacy_get_kind th + val _ = + if kind <> "" then + let + val suggs = + old_facts + |> meng_paulson_facts ctxt prover_name (the max_relevant) + relevance_thresholds goal i + |> map (fact_name_of o Thm.get_name_hint o snd) + val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" + in File.append path s end + else + () + in fact :: old_facts end + in fold do_fact new_facts old_facts; () end + +end; diff -r b149de01d669 -r b88c3e0b752e src/HOL/TPTP/mash_import.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 13:59:39 2012 +0200 @@ -0,0 +1,163 @@ +(* Title: HOL/TPTP/mash_import.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Import proof suggestions from MaSh (Machine-learning for Sledgehammer) and +evaluate them. +*) + +signature MASH_IMPORT = +sig + val import_and_evaluate_mash_suggestions : + Proof.context -> theory -> string -> unit +end; + +structure MaSh_Import : MASH_IMPORT = +struct + +open MaSh_Export + +val unescape_meta = + let + fun un accum [] = String.implode (rev accum) + | un accum (#"\\" :: d1 :: d2 :: d3 :: cs) = + (case Int.fromString (String.implode [d1, d2, d3]) of + SOME n => un (Char.chr n :: accum) cs + | NONE => "" (* error *)) + | un _ (#"\\" :: _) = "" (* error *) + | un accum (c :: cs) = un (c :: accum) cs + in un [] o String.explode end + +val of_fact_name = unescape_meta + +val depN = "Dependencies" +val mengN = "Meng & Paulson" +val mashN = "MaSh" +val meng_mashN = "M&P+MaSh" + +val max_relevant_slack = 2 + +fun import_and_evaluate_mash_suggestions ctxt thy file_name = + let + val params as {provers, max_relevant, relevance_thresholds, + slice, type_enc, lam_trans, timeout, ...} = + Sledgehammer_Isar.default_params ctxt [] + val prover_name = hd provers + val path = file_name |> Path.explode + val lines = path |> File.read_lines + val facts = non_tautological_facts_of thy + val all_names = facts |> map (Thm.get_name_hint o snd) + val i = 1 + val meng_ok = Unsynchronized.ref 0 + val mash_ok = Unsynchronized.ref 0 + val meng_mash_ok = Unsynchronized.ref 0 + val dep_ok = Unsynchronized.ref 0 + fun find_sugg facts sugg = + find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts + fun sugg_facts hyp_ts concl_t facts = + map_filter (find_sugg facts o of_fact_name) + #> take (max_relevant_slack * the max_relevant) + #> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t + #> map (apfst (apfst (fn name => name ()))) + fun meng_mash_facts fs1 fs2 = + let + val fact_eq = (op =) o pairself fst + fun score_in f fs = + case find_index (curry fact_eq f) fs of + ~1 => length fs + | j => j + fun score_of f = score_in f fs1 + score_in f fs2 + in + union fact_eq fs1 fs2 + |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd + |> take (the max_relevant) + end + fun with_index facts s = + (find_index (fn ((s', _), _) => s = s') facts + 1, s) + fun index_string (j, s) = s ^ "@" ^ string_of_int j + fun str_of_res label facts {outcome, run_time, used_facts, ...} = + " " ^ label ^ ": " ^ + (if is_none outcome then + "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^ + (used_facts |> map (with_index facts o fst) + |> sort (int_ord o pairself fst) + |> map index_string + |> space_implode " ") ^ + (if length facts < the max_relevant then + " (of " ^ string_of_int (length facts) ^ ")" + else + "") + else + "Failure: " ^ + (facts |> map (fst o fst) + |> tag_list 1 + |> map index_string + |> space_implode " ")) + fun run_sh ok heading facts goal = + let + val problem = + {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1, + facts = facts |> take (the max_relevant) + |> map Sledgehammer_Provers.Untranslated_Fact} + val prover = + Sledgehammer_Run.get_minimizing_prover ctxt + Sledgehammer_Provers.Normal prover_name + val res as {outcome, ...} = prover params (K (K (K ""))) problem + val _ = if is_none outcome then ok := !ok + 1 else () + in str_of_res heading facts res end + fun solve_goal j name suggs = + let + val name = of_fact_name name + val th = + case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of + SOME (_, th) => th + | NONE => error ("No fact called \"" ^ name ^ "\"") + val deps = dependencies_of all_names th + val goal = goal_of_thm th + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i + val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val deps_facts = sugg_facts hyp_ts concl_t facts deps + val meng_facts = + meng_paulson_facts ctxt prover_name + (max_relevant_slack * the max_relevant) relevance_thresholds goal + i facts + val mash_facts = sugg_facts hyp_ts concl_t facts suggs + val meng_mash_facts = meng_mash_facts meng_facts mash_facts + val meng_s = run_sh meng_ok mengN meng_facts goal + val mash_s = run_sh mash_ok mashN mash_facts goal + val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal + val dep_s = run_sh dep_ok depN deps_facts goal + in + ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s, + dep_s] + |> cat_lines |> tracing + end + val explode_suggs = space_explode " " #> filter_out (curry (op =) "") + fun do_line (j, line) = + case space_explode ":" line of + [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs) + | _ => () + fun total_of heading ok n = + " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ + Real.fmt (StringCvt.FIX (SOME 1)) + (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)" + val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts + val params = + [prover_name, string_of_int (the max_relevant) ^ " facts", + "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc, + the_default "smart" lam_trans, ATP_Util.string_from_time timeout, + "instantiate_inducts" |> not inst_inducts ? prefix "dont_"] + val n = length lines + in + tracing " * * *"; + tracing ("Options: " ^ commas params); + List.app do_line (tag_list 1 lines); + ["Successes (of " ^ string_of_int n ^ " goals)", + total_of mengN meng_ok n, + total_of mashN mash_ok n, + total_of meng_mashN meng_mash_ok n, + total_of depN dep_ok n] + |> cat_lines |> tracing + end + +end; diff -r b149de01d669 -r b88c3e0b752e src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 13:59:39 2012 +0200 @@ -86,6 +86,7 @@ val unproxify_const : string -> string val new_skolem_var_name_from_const : string -> string val atp_irrelevant_consts : string list + val atp_widely_irrelevant_consts : string list val atp_schematic_consts_of : term -> typ list Symtab.table val is_type_enc_higher_order : type_enc -> bool val is_type_enc_polymorphic : type_enc -> bool @@ -93,6 +94,7 @@ val is_type_enc_sound : type_enc -> bool val type_enc_from_string : strictness -> string -> type_enc val adjust_type_enc : atp_format -> type_enc -> type_enc + val has_no_lambdas : term -> bool val mk_aconns : connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula val unmangled_const : string -> string * (string, 'b) ho_term list @@ -399,7 +401,7 @@ @{const_name conj}, @{const_name disj}, @{const_name implies}, @{const_name HOL.eq}, @{const_name If}, @{const_name Let}] -val atp_monomorph_bad_consts = +val atp_widely_irrelevant_consts = atp_irrelevant_consts @ (* These are ignored anyway by the relevance filter (unless they appear in higher-order places) but not by the monomorphizer. *) @@ -411,7 +413,7 @@ Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x val add_schematic_consts_of = Term.fold_aterms (fn Const (x as (s, _)) => - not (member (op =) atp_monomorph_bad_consts s) + not (member (op =) atp_widely_irrelevant_consts s) ? add_schematic_const x | _ => I) fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty @@ -701,22 +703,22 @@ (if is_type_enc_sound type_enc then Tags else Guards) stuff | adjust_type_enc _ type_enc = type_enc -fun is_fol_term t = +fun has_no_lambdas t = case t of - @{const Not} $ t1 => is_fol_term t1 - | Const (@{const_name All}, _) $ Abs (_, _, t') => is_fol_term t' - | Const (@{const_name All}, _) $ t1 => is_fol_term t1 - | Const (@{const_name Ex}, _) $ Abs (_, _, t') => is_fol_term t' - | Const (@{const_name Ex}, _) $ t1 => is_fol_term t1 - | @{const HOL.conj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2 - | @{const HOL.disj} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2 - | @{const HOL.implies} $ t1 $ t2 => is_fol_term t1 andalso is_fol_term t2 + @{const Not} $ t1 => has_no_lambdas t1 + | Const (@{const_name All}, _) $ Abs (_, _, t') => has_no_lambdas t' + | Const (@{const_name All}, _) $ t1 => has_no_lambdas t1 + | Const (@{const_name Ex}, _) $ Abs (_, _, t') => has_no_lambdas t' + | Const (@{const_name Ex}, _) $ t1 => has_no_lambdas t1 + | @{const HOL.conj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2 + | @{const HOL.disj} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2 + | @{const HOL.implies} $ t1 $ t2 => has_no_lambdas t1 andalso has_no_lambdas t2 | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => - is_fol_term t1 andalso is_fol_term t2 + has_no_lambdas t1 andalso has_no_lambdas t2 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t) fun simple_translate_lambdas do_lambdas ctxt t = - if is_fol_term t then + if has_no_lambdas t then t else let @@ -2494,8 +2496,7 @@ let val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts - val decl_lines = - fold_rev (append o lines_for_sym_decls ctxt mono type_enc) syms [] + val decl_lines = maps (lines_for_sym_decls ctxt mono type_enc) syms in mono_lines @ decl_lines end fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) diff -r b149de01d669 -r b88c3e0b752e src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 11 13:59:39 2012 +0200 @@ -213,7 +213,8 @@ (* E *) -fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER) +fun is_recent_e_version () = (string_ord (getenv "E_VERSION", "1.3") <> LESS) +fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.6") <> LESS) val tstp_proof_delims = [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"), @@ -289,23 +290,35 @@ else "") end +fun e_shell_level_argument full_proof = + if is_new_e_version () then + " --pcl-shell-level=" ^ (if full_proof then "0" else "2") + else + "" + fun effective_e_selection_heuristic ctxt = - if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN + if is_recent_e_version () then Config.get ctxt e_selection_heuristic + else e_autoN -fun e_kbo () = if is_new_e_version () then "KBO6" else "KBO" +fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO" val e_config : atp_config = {exec = (["E_HOME"], "eproof"), required_vars = [], arguments = - fn ctxt => fn _ => fn heuristic => fn timeout => + fn ctxt => fn full_proof => fn heuristic => fn timeout => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => "--tstp-in --tstp-out --output-level=5 --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^ - "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), - proof_delims = tstp_proof_delims, + "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ + e_shell_level_argument full_proof, + proof_delims = + (* work-around for bug in "epclextract" version 1.6 *) + ("# SZS status Theorem\n# SZS output start Saturation.", + "# SZS output end Saturation.") :: + tstp_proof_delims, known_failures = [(TimedOut, "Failure: Resource limit exceeded (time)"), (TimedOut, "time limit exceeded")] @ diff -r b149de01d669 -r b88c3e0b752e src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 13:59:39 2012 +0200 @@ -131,7 +131,7 @@ fun type_instance thy T T' = Sign.typ_instance thy (T, T') fun type_generalization thy T T' = Sign.typ_instance thy (T', T) fun type_intersect thy T T' = - can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T')) + can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T')) (Vartab.empty, 0) val type_equiv = Sign.typ_equiv @@ -192,6 +192,7 @@ | (k1, k2) => if k1 >= max orelse k2 >= max then max else Int.min (max, Integer.pow k2 k1)) + | Type (@{type_name set}, [T']) => aux slack avoid (T' --> @{typ bool}) | @{typ prop} => 2 | @{typ bool} => 2 (* optimization *) | @{typ nat} => 0 (* optimization *) diff -r b149de01d669 -r b88c3e0b752e src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 13:54:37 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 13:59:39 2012 +0200 @@ -53,6 +53,10 @@ Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list -> status Termtab.table -> (((unit -> string) * stature) * thm) list + val maybe_instantiate_inducts : + Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list + -> (((unit -> string) * 'a) * thm) list + val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list val nearly_all_facts : Proof.context -> bool -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * stature) * thm) list @@ -446,8 +450,15 @@ | _ => do_term false t in do_formula pos end -(*Inserts a dummy "constant" referring to the theory name, so that relevance - takes the given theory into account.*) +fun pconsts_in_fact thy is_built_in_const t = + Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) + (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true + (SOME true) t) [] + +val const_names_in_fact = map fst ooo pconsts_in_fact + +(* Inserts a dummy "constant" referring to the theory name, so that relevance + takes the given theory into account. *) fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...} : relevance_fudge) thy_name t = if exists (curry (op <) 0.0) [theory_const_rel_weight, @@ -459,6 +470,13 @@ fun theory_const_prop_of fudge th = theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th) +fun pair_consts_fact thy is_built_in_const fudge fact = + case fact |> snd |> theory_const_prop_of fudge + |> pconsts_in_fact thy is_built_in_const of + [] => NONE + | consts => SOME ((fact, consts), NONE) + + (**** Constant / Type Frequencies ****) (* A two-dimensional symbol table counts frequencies of constants. It's keyed @@ -597,19 +615,6 @@ val res = rel_weight / (rel_weight + irrel_weight) in if Real.isFinite res then res else 0.0 end -fun pconsts_in_fact thy is_built_in_const t = - Symtab.fold (fn (s, pss) => fold (cons o pair s) pss) - (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true - (SOME true) t) [] - -fun pair_consts_fact thy is_built_in_const fudge fact = - case fact |> snd |> theory_const_prop_of fudge - |> pconsts_in_fact thy is_built_in_const of - [] => NONE - | consts => SOME ((fact, consts), NONE) - -val const_names_in_fact = map fst ooo pconsts_in_fact - type annotated_thm = (((unit -> string) * stature) * thm) * (string * ptype) list @@ -958,19 +963,29 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) +fun maybe_instantiate_inducts ctxt hyp_ts concl_t = + if Config.get ctxt instantiate_inducts then + let + val thy = Proof_Context.theory_of ctxt + val ind_stmt = + (hyp_ts |> filter_out (null o external_frees), concl_t) + |> Logic.list_implies |> Object_Logic.atomize_term thy + val ind_stmt_xs = external_frees ind_stmt + in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end + else + I + +fun maybe_filter_no_atps ctxt = + not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) + fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) chained_ths hyp_ts concl_t = if only andalso null add then [] else let - val thy = Proof_Context.theory_of ctxt val reserved = reserved_isar_keyword_table () val add_ths = Attrib.eval_thms ctxt add - val ind_stmt = - (hyp_ts |> filter_out (null o external_frees), concl_t) - |> Logic.list_implies |> Object_Logic.atomize_term thy - val ind_stmt_xs = external_frees ind_stmt val css_table = clasimpset_rule_table_of ctxt in (if only then @@ -978,10 +993,8 @@ o fact_from_ref ctxt reserved chained_ths css_table) add else all_facts ctxt ho_atp reserved false add_ths chained_ths css_table) - |> Config.get ctxt instantiate_inducts - ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) - |> (not (Config.get ctxt ignore_no_atp) andalso not only) - ? filter_out (No_ATPs.member ctxt o snd) + |> maybe_instantiate_inducts ctxt hyp_ts concl_t + |> not only ? maybe_filter_no_atps ctxt |> uniquify end