# HG changeset patch # User blanchet # Date 1342035799 -7200 # Node ID 6cdcfbddc077137684fc8123f5978fd65bf9500d # Parent 1065c307fafe15d33dc3f97afa9e7dd0c8eb5c59 moved most of MaSh exporter code to Sledgehammer diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200 @@ -14,9 +14,9 @@ "Tools/Sledgehammer/sledgehammer_fact.ML" "Tools/Sledgehammer/sledgehammer_filter_iter.ML" "Tools/Sledgehammer/sledgehammer_provers.ML" + "Tools/Sledgehammer/sledgehammer_minimize.ML" "Tools/Sledgehammer/sledgehammer_filter_mash.ML" "Tools/Sledgehammer/sledgehammer_filter.ML" - "Tools/Sledgehammer/sledgehammer_minimize.ML" "Tools/Sledgehammer/sledgehammer_run.ML" "Tools/Sledgehammer/sledgehammer_isar.ML" begin diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200 @@ -14,17 +14,19 @@ lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] ML {* +open Sledgehammer_Filter_MaSh open MaSh_Export *} ML {* val do_it = false (* switch to "true" to generate the files *); -val thy = @{theory Nat} +val thy = @{theory Nat}; +val params = Sledgehammer_Isar.default_params @{context} [] *} ML {* if do_it then - generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies" + generate_accessibility thy false "/tmp/mash_accessibility" else () *} @@ -38,13 +40,6 @@ ML {* if do_it then - generate_accessibility thy false "/tmp/mash_accessibility" -else - () -*} - -ML {* -if do_it then generate_isa_dependencies thy false "/tmp/mash_isa_dependencies" else () @@ -52,7 +47,7 @@ ML {* if do_it then - generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies" + generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" else () *} @@ -66,7 +61,7 @@ ML {* if do_it then - generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions" + generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions" else () *} diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/TPTP/MaSh_Import.thy --- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200 @@ -16,13 +16,14 @@ *} ML {* -val do_it = true (* switch to "true" to generate the files *); -val thy = @{theory List} +val do_it = false (* switch to "true" to generate the files *); +val thy = @{theory List}; +val params = Sledgehammer_Isar.default_params @{context} [] *} ML {* if do_it then - import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list" + import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" else () *} diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200 @@ -8,11 +8,7 @@ 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 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; @@ -27,45 +23,6 @@ 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 - not doing the same? *) -fun fold_body_thms thm_name f = - let - fun app n (PBody {thms, ...}) = - thms |> fold (fn (_, (name, prop, body)) => fn x => - let - val body' = Future.join body - val n' = - n + (if name = "" orelse - (* uncommon case where the proved theorem occurs twice - (e.g., "Transitive_Closure.trancl_into_trancl") *) - (n = 1 andalso name = thm_name) then - 0 - else - 1) - val x' = x |> n' <= 1 ? app n' body' - in (x' |> n = 1 ? f (name, prop, body')) end) - in fold (app 0) end - -fun theorems_mentioned_in_proof_term all_names th = - let - val is_name_ok = - case all_names of - SOME names => member (op =) names - | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) - 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] - in names end - -fun all_facts_of_theory thy = - let val ctxt = Proof_Context.init_global thy in - Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] [] - (Sledgehammer_Fact.clasimpset_rule_table_of ctxt) - |> rev (* try to restore the original order of facts, for MaSh *) - end - fun inference_term [] = NONE | inference_term ss = ATerm (("inference", []), @@ -153,7 +110,7 @@ val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" - val facts = all_facts_of_theory thy + val facts = Sledgehammer_Fact.all_facts_of thy val atp_problem = facts |> map (fn ((_, loc), th) => @@ -170,7 +127,7 @@ val infers = facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), - th |> theorems_mentioned_in_proof_term (SOME all_names) + th |> Sledgehammer_Util.thms_in_proof (SOME all_names) |> map fact_name_of)) val all_atp_problem_names = atp_problem |> maps (map ident_of_problem_line o snd) diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200 @@ -7,348 +7,23 @@ signature MASH_EXPORT = sig - type stature = ATP_Problem_Generate.stature - type prover_result = Sledgehammer_Provers.prover_result + type params = Sledgehammer_Provers.params - 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 : theory -> thm -> thm - val meng_paulson_facts : - Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list - -> ((string * stature) * thm) list - val run_sledgehammer : - Proof.context -> ((string * stature) * thm) list -> thm -> prover_result - val generate_accessibility : theory -> bool -> string -> unit - val generate_features : theory -> bool -> string -> unit - val generate_isa_dependencies : theory -> bool -> string -> unit - val generate_atp_dependencies : - Proof.context -> theory -> bool -> string -> unit val generate_commands : theory -> string -> unit - val generate_meng_paulson_suggestions : - Proof.context -> theory -> int -> string -> unit + val generate_iter_suggestions : + Proof.context -> params -> theory -> int -> string -> unit end; structure MaSh_Export : MASH_EXPORT = struct -open ATP_Util -open ATP_Problem_Generate -open ATP_Theory_Export - -type prover_result = Sledgehammer_Provers.prover_result - -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 - 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)) = union (op =) (map class_name_of S) - | do_add_type (TVar (_, S)) = union (op =) (map class_name_of 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 - -fun dependencies_of all_facts = - theorems_mentioned_in_proof_term (SOME all_facts) - #> map fact_name_of - #> sort string_ord - -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 - -fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init - -fun meng_paulson_facts ctxt max_relevant goal = - let - val {provers, relevance_thresholds, ...} = - Sledgehammer_Isar.default_params ctxt [] - val prover_name = hd provers - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 - 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 run_sledgehammer ctxt facts goal = - let - val params as {provers, ...} = Sledgehammer_Isar.default_params ctxt [] - val problem = - {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, - facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} - val prover = - Sledgehammer_Minimize.get_minimizing_prover ctxt - Sledgehammer_Provers.Normal (hd provers) - in prover params (K (K (K ""))) problem end - -fun generate_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_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_isa_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_atp_dependencies ctxt thy include_thy file_name = - let - val {max_relevant, ...} = Sledgehammer_Isar.default_params ctxt [] - 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) - val ths = facts |> map snd - val all_names = ths |> map Thm.get_name_hint - fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep - fun add_isa_dep facts dep accum = - if exists (is_dep dep) accum then - accum - else case find_first (is_dep dep) facts of - SOME ((name, status), th) => accum @ [((name (), status), th)] - | NONE => accum (* shouldn't happen *) - fun fix_name ((_, stature), th) = - ((th |> Thm.get_name_hint |> fact_name_of, stature), th) - fun do_thm th = - let - val name = Thm.get_name_hint th - val goal = goal_of_thm thy th - val deps = - case dependencies_of all_names th of - [] => [] - | isa_dep as [_] => isa_dep (* can hardly beat that *) - | isa_deps => - let - val facts = - facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) - val facts = - facts |> meng_paulson_facts ctxt (the max_relevant) goal - |> fold (add_isa_dep facts) isa_deps - |> map fix_name - in - case run_sledgehammer ctxt facts goal of - {outcome = NONE, used_facts, ...} => - used_facts |> map fst |> sort string_ord - | _ => isa_deps - end - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" - in File.append path s end - in List.app do_thm ths end +open Sledgehammer_Filter_MaSh fun generate_commands thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" - val facts = non_tautological_facts_of thy + val facts = all_non_tautological_facts_of thy val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) @@ -358,7 +33,7 @@ let val name = Thm.get_name_hint th val feats = features_of thy (status, th) - val deps = dependencies_of all_names th + val deps = isabelle_dependencies_of all_names th val kind = Thm.legacy_get_kind th val name = fact_name_of name val core = @@ -371,11 +46,11 @@ val parents = parent_thms thy_ths thy in fold do_fact new_facts parents; () end -fun generate_meng_paulson_suggestions ctxt thy max_relevant file_name = +fun generate_iter_suggestions ctxt params thy max_relevant file_name = let val path = file_name |> Path.explode val _ = File.write path "" - val facts = non_tautological_facts_of thy + val facts = all_non_tautological_facts_of thy val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) @@ -388,7 +63,7 @@ if kind <> "" then let val suggs = - old_facts |> meng_paulson_facts ctxt max_relevant goal + old_facts |> iter_facts ctxt params max_relevant goal |> map (fact_name_of o fst o fst) |> sort string_ord val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/TPTP/mash_import.ML --- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200 @@ -8,13 +8,16 @@ signature MASH_IMPORT = sig + type params = Sledgehammer_Provers.params + val import_and_evaluate_mash_suggestions : - Proof.context -> theory -> string -> unit + Proof.context -> params -> theory -> string -> unit end; structure MaSh_Import : MASH_IMPORT = struct +open Sledgehammer_Filter_MaSh open MaSh_Export val unescape_meta = @@ -30,26 +33,26 @@ val of_fact_name = unescape_meta -val depN = "Dependencies" -val mengN = "Meng & Paulson" +val isaN = "Isabelle" +val iterN = "Iterative" val mashN = "MaSh" -val meng_mashN = "M&P+MaSh" +val iter_mashN = "Iter+MaSh" val max_relevant_slack = 2 -fun import_and_evaluate_mash_suggestions ctxt thy file_name = +fun import_and_evaluate_mash_suggestions ctxt params thy file_name = let val {provers, max_relevant, 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 facts = all_non_tautological_facts_of thy val all_names = facts |> map (Thm.get_name_hint o snd) - val meng_ok = Unsynchronized.ref 0 + val iter_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 - val meng_mash_ok = Unsynchronized.ref 0 - val dep_ok = Unsynchronized.ref 0 + val iter_mash_ok = Unsynchronized.ref 0 + val isa_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 = @@ -57,7 +60,7 @@ #> take (max_relevant_slack * the max_relevant) #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t #> map (apfst (apfst (fn name => name ()))) - fun meng_mash_facts fs1 fs2 = + fun iter_mash_facts fs1 fs2 = let val fact_eq = (op =) o pairself fst fun score_in f fs = @@ -92,10 +95,10 @@ |> tag_list 1 |> map index_string |> space_implode " ")) - fun run_sh ok heading facts goal = + fun prove ok heading facts goal = let val facts = facts |> take (the max_relevant) - val res as {outcome, ...} = run_sledgehammer ctxt facts goal + val res as {outcome, ...} = run_prover ctxt params facts goal val _ = if is_none outcome then ok := !ok + 1 else () in str_of_res heading facts res end fun solve_goal j name suggs = @@ -105,23 +108,23 @@ 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 isa_deps = isabelle_dependencies_of all_names th val goal = goal_of_thm thy th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 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 (max_relevant_slack * the max_relevant) goal - facts + val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps + val iter_facts = + iter_facts ctxt params (max_relevant_slack * the max_relevant) goal + 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 + val iter_mash_facts = iter_mash_facts iter_facts mash_facts + val iter_s = prove iter_ok iterN iter_facts goal + val mash_s = prove mash_ok mashN mash_facts goal + val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal + val isa_s = prove isa_ok isaN isa_facts goal in - ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s, - dep_s] + ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s, + isa_s] |> cat_lines |> tracing end val explode_suggs = space_explode " " #> filter_out (curry (op =) "") @@ -145,10 +148,10 @@ tracing ("Options: " ^ commas options); List.app do_line (tag_list 1 lines); ["Successes (of " ^ string_of_int n ^ " goals)", - total_of mengN meng_ok n, + total_of iterN iter_ok n, total_of mashN mash_ok n, - total_of meng_mashN meng_mash_ok n, - total_of depN dep_ok n] + total_of iter_mashN iter_mash_ok n, + total_of isaN isa_ok n] |> cat_lines |> tracing end diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200 @@ -252,10 +252,6 @@ Other characters go to _nnn where nnn is the decimal ASCII code.*) val upper_a_minus_space = Char.ord #"A" - Char.ord #" " -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 ascii_of_char c = if Char.isAlphaNum c then String.str c diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200 @@ -9,6 +9,7 @@ val timestamp : unit -> string val hash_string : string -> int val hash_term : term -> int + val stringN_of_int : int -> int -> string val strip_spaces : bool -> (char -> bool) -> string -> string val strip_spaces_except_between_idents : string -> string val nat_subscript : int -> string @@ -65,6 +66,10 @@ fun hash_string s = Word.toInt (hashw_string (s, 0w0)) val hash_term = Word.toInt o hashw_term +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 strip_spaces skip_comments is_evil = let fun strip_c_style_comment [] accum = accum diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200 @@ -21,15 +21,16 @@ val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list - val all_facts : - Proof.context -> bool -> 'a Symtab.table -> bool -> thm list - -> thm list -> status Termtab.table - -> (((unit -> string) * stature) * thm) list val clasimpset_rule_table_of : Proof.context -> status Termtab.table 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 all_facts : + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list + -> thm list -> status Termtab.table + -> (((unit -> string) * stature) * thm) list + val all_facts_of : theory -> (((unit -> string) * stature) * thm) list val nearly_all_facts : Proof.context -> bool -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * stature) * thm) list @@ -240,77 +241,6 @@ (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst -fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table = - 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 = local_facts |> Facts.dest_static [] - val assms = Assumption.all_assms_of ctxt - fun is_good_unnamed_local th = - not (Thm.has_name_hint th) andalso - forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals - val unnamed_locals = - union Thm.eq_thm_prop (Facts.props local_facts) chained_ths - |> filter is_good_unnamed_local |> 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) => - if not exporter andalso name0 <> "" andalso - forall (not o member Thm.eq_thm_prop add_ths) ths andalso - (Facts.is_concealed facts name0 orelse - (not (Config.get ctxt ignore_no_atp) andalso - is_package_def name0) orelse - exists (fn s => String.isSuffix s name0) - (multi_base_blacklist ctxt ho_atp)) then - I - else - let - val multi = length ths > 1 - val backquote_thm = - backquote o hackish_string_for_term ctxt o close_form o prop_of - 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 - pair 1 - #> fold (fn th => fn (j, (multis, unis)) => - (j + 1, - if not (member Thm.eq_thm_prop add_ths th) andalso - is_theorem_bad_for_atps ho_atp exporter th then - (multis, unis) - else - let - val new = - (((fn () => - if name0 = "" then - th |> backquote_thm - else - [Facts.extern ctxt facts name0, - Name_Space.extern ctxt full_space name0, - name0] - |> find_first check_thms - |> (fn SOME name => - make_name reserved multi j name - | NONE => "")), - stature_of_thm global assms chained_ths - css_table name0 th), th) - in - if multi then (new :: multis, unis) - else (multis, new :: unis) - end)) ths - #> snd - end) - in - (* The single-name theorems go after the multiple-name ones, so that single - names are preferred when both are available. *) - ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) - |> add_facts true Facts.fold_static global_facts global_facts - |> op @ - end - fun clasimpset_rule_table_of ctxt = let val thy = Proof_Context.theory_of ctxt @@ -416,6 +346,84 @@ fun maybe_filter_no_atps ctxt = not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd) +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table = + 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 = local_facts |> Facts.dest_static [] + val assms = Assumption.all_assms_of ctxt + fun is_good_unnamed_local th = + not (Thm.has_name_hint th) andalso + forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals + val unnamed_locals = + union Thm.eq_thm_prop (Facts.props local_facts) chained_ths + |> filter is_good_unnamed_local |> 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) => + if not exporter andalso name0 <> "" andalso + forall (not o member Thm.eq_thm_prop add_ths) ths andalso + (Facts.is_concealed facts name0 orelse + (not (Config.get ctxt ignore_no_atp) andalso + is_package_def name0) orelse + exists (fn s => String.isSuffix s name0) + (multi_base_blacklist ctxt ho_atp)) then + I + else + let + val multi = length ths > 1 + val backquote_thm = + backquote o hackish_string_for_term ctxt o close_form o prop_of + 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 + pair 1 + #> fold (fn th => fn (j, (multis, unis)) => + (j + 1, + if not (member Thm.eq_thm_prop add_ths th) andalso + is_theorem_bad_for_atps ho_atp exporter th then + (multis, unis) + else + let + val new = + (((fn () => + if name0 = "" then + th |> backquote_thm + else + [Facts.extern ctxt facts name0, + Name_Space.extern ctxt full_space name0, + name0] + |> find_first check_thms + |> (fn SOME name => + make_name reserved multi j name + | NONE => "")), + stature_of_thm global assms chained_ths + css_table name0 th), th) + in + if multi then (new :: multis, unis) + else (multis, new :: unis) + end)) ths + #> snd + end) + in + (* The single-name theorems go after the multiple-name ones, so that single + names are preferred when both are available. *) + ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals) + |> add_facts true Facts.fold_static global_facts global_facts + |> op @ + end + +fun all_facts_of thy = + let val ctxt = Proof_Context.init_global thy in + all_facts ctxt false Symtab.empty true [] [] + (clasimpset_rule_table_of ctxt) + |> rev (* try to restore the original order of facts, for MaSh *) + end + fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) chained_ths hyp_ts concl_t = if only andalso null add then diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200 @@ -6,6 +6,35 @@ signature SLEDGEHAMMER_FILTER_MASH = sig + type status = ATP_Problem_Generate.status + type stature = ATP_Problem_Generate.stature + type params = Sledgehammer_Provers.params + type prover_result = Sledgehammer_Provers.prover_result + + val fact_name_of : string -> string + val all_non_tautological_facts_of : + theory -> (((unit -> string) * stature) * thm) list + val theory_ord : theory * theory -> order + val thm_ord : thm * thm -> order + val thms_by_thy : ('a * thm) list -> (string * thm list) list + val has_thy : theory -> thm -> bool + val parent_thms : (string * thm list) list -> theory -> string list + val features_of : theory -> status * thm -> string list + val isabelle_dependencies_of : string list -> thm -> string list + val goal_of_thm : theory -> thm -> thm + val iter_facts : + Proof.context -> params -> int -> thm + -> (((unit -> string) * stature) * thm) list + -> ((string * stature) * thm) list + val run_prover : + Proof.context -> params -> ((string * stature) * thm) list -> thm + -> prover_result + val generate_accessibility : theory -> bool -> string -> unit + val generate_features : theory -> bool -> string -> unit + val generate_isa_dependencies : theory -> bool -> string -> unit + val generate_atp_dependencies : + Proof.context -> params -> theory -> bool -> string -> unit + val reset : unit -> unit val can_suggest : unit -> bool val can_learn_thy : theory -> bool @@ -16,6 +45,16 @@ structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH = struct +open ATP_Util +open ATP_Problem_Generate +open Sledgehammer_Util +open Sledgehammer_Fact +open Sledgehammer_Filter_Iter +open Sledgehammer_Provers + + +(*** Low-level communication with MaSh ***) + fun mash_reset () = tracing "MaSh RESET" @@ -30,6 +69,311 @@ tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ space_implode " " feats) + +(*** Isabelle helpers ***) + +val fact_name_of = prefix fact_prefix o ascii_of + +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 + 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)) = union (op =) (map class_name_of S) + | do_add_type (TVar (_, S)) = union (op =) (map class_name_of 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 all_non_tautological_facts_of thy = + all_facts_of 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 + +fun isabelle_dependencies_of all_facts = + thms_in_proof (SOME all_facts) + #> map fact_name_of #> sort string_ord + +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 + +fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init + +fun iter_facts ctxt ({provers, relevance_thresholds, ...} : params) max_relevant + goal = + let + val prover_name = hd provers + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 + 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 + iterative_relevant_facts ctxt relevance_thresholds max_relevant + is_built_in_const relevance_fudge + relevance_override [] hyp_ts concl_t + end + +fun run_prover ctxt (params as {provers, ...}) facts goal = + let + val problem = + {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, + facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} + val prover = + Sledgehammer_Minimize.get_minimizing_prover ctxt + Sledgehammer_Provers.Normal (hd provers) + in prover params (K (K (K ""))) problem end + +fun generate_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 = + all_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_features thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = + all_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_isa_dependencies thy include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val ths = + all_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 = isabelle_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_atp_dependencies ctxt (params as {max_relevant, ...}) thy + include_thy file_name = + let + val path = file_name |> Path.explode + val _ = File.write path "" + val facts = + all_non_tautological_facts_of thy + |> not include_thy ? filter_out (has_thy thy o snd) + val ths = facts |> map snd + val all_names = ths |> map Thm.get_name_hint + fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep + fun add_isa_dep facts dep accum = + if exists (is_dep dep) accum then + accum + else case find_first (is_dep dep) facts of + SOME ((name, status), th) => accum @ [((name (), status), th)] + | NONE => accum (* shouldn't happen *) + fun fix_name ((_, stature), th) = + ((th |> Thm.get_name_hint |> fact_name_of, stature), th) + fun do_thm th = + let + val name = Thm.get_name_hint th + val goal = goal_of_thm thy th + val deps = + case isabelle_dependencies_of all_names th of + [] => [] + | isa_dep as [_] => isa_dep (* can hardly beat that *) + | isa_deps => + let + val facts = + facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) + val facts = + facts |> iter_facts ctxt params (the max_relevant) goal + |> fold (add_isa_dep facts) isa_deps + |> map fix_name + in + case run_prover ctxt params facts goal of + {outcome = NONE, used_facts, ...} => + used_facts |> map fst |> sort string_ord + | _ => isa_deps + end + val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" + in File.append path s end + in List.app do_thm ths end + + +(*** High-level communication with MaSh ***) + fun reset () = () diff -r 1065c307fafe -r 6cdcfbddc077 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200 @@ -14,6 +14,7 @@ val subgoal_count : Proof.state -> int val normalize_chained_theorems : thm list -> thm list val reserved_isar_keyword_table : unit -> unit Symtab.table + val thms_in_proof : string list option -> thm -> string list end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = @@ -60,4 +61,36 @@ Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make +(* 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 + not doing the same? *) +fun fold_body_thms thm_name f = + let + fun app n (PBody {thms, ...}) = + thms |> fold (fn (_, (name, prop, body)) => fn x => + let + val body' = Future.join body + val n' = + n + (if name = "" orelse + (* uncommon case where the proved theorem occurs twice + (e.g., "Transitive_Closure.trancl_into_trancl") *) + (n = 1 andalso name = thm_name) then + 0 + else + 1) + val x' = x |> n' <= 1 ? app n' body' + in (x' |> n = 1 ? f (name, prop, body')) end) + in fold (app 0) end + +fun thms_in_proof all_names th = + let + val is_name_ok = + case all_names of + SOME names => member (op =) names + | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s)) + 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] + in names end + end;