# HG changeset patch # User blanchet # Date 1282319546 -7200 # Node ID 760a2d5cc671bc931725e48a691a7e80602a1cad # Parent 5536897d04c24fbf81bc20fb448f62ca0bb3d0dd make sure minimizer facts go through "transform_elim_theorems" diff -r 5536897d04c2 -r 760a2d5cc671 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 17:04:15 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 20 17:52:26 2010 +0200 @@ -43,7 +43,7 @@ val name = Facts.string_of_ref xref |> forall (member Thm.eq_thm chained_ths) ths ? prefix chained_prefix - in (name, ths) end + in (name, ths |> map Clausifier.transform_elim_theorem) end (***************************************************************) @@ -433,78 +433,6 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun is_theorem_bad_for_atps thm = - let val t = prop_of thm in - is_formula_too_complex t orelse exists_type type_has_top_sort t orelse - exists_sledgehammer_const t orelse is_strange_thm thm - end - -fun all_name_thms_pairs ctxt add_thms chained_ths = - let - val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); - val local_facts = ProofContext.facts_of ctxt; - val full_space = - Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); - - fun valid_facts facts = - (facts, []) |-> Facts.fold_static (fn (name, ths0) => - if (Facts.is_concealed facts name orelse - (respect_no_atp andalso is_package_def name) orelse - member (op =) multi_base_blacklist (Long_Name.base_name name) orelse - String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso - forall (not o member Thm.eq_thm add_thms) ths0 then - I - else - let - fun check_thms a = - (case try (ProofContext.get_thms ctxt) a of - NONE => false - | SOME ths1 => Thm.eq_thms (ths0, ths1)) - val name1 = Facts.extern facts name; - val name2 = Name_Space.extern full_space name; - val ths = filter (fn th => not (is_theorem_bad_for_atps th) orelse - member Thm.eq_thm add_thms th) ths0 - in - case find_first check_thms [name1, name2, name] of - NONE => I - | SOME name' => - cons (name' |> forall (member Thm.eq_thm chained_ths) ths - ? prefix chained_prefix, ths) - end) - in valid_facts global_facts @ valid_facts local_facts end; - -fun multi_name a th (n, pairs) = - (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); - -fun add_names (_, []) pairs = pairs - | add_names (a, [th]) pairs = (a, th) :: pairs - | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) - -fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; - -(* The single-name theorems go after the multiple-name ones, so that single - names are preferred when both are available. *) -fun name_thm_pairs ctxt respect_no_atp name_thms_pairs = - let - val (mults, singles) = List.partition is_multi name_thms_pairs - val ps = [] |> fold add_names singles |> fold add_names mults - in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; - -fun is_named ("", th) = - (warning ("No name for theorem " ^ - Display.string_of_thm_without_context th); false) - | is_named _ = true -fun checked_name_thm_pairs respect_no_atp ctxt = - name_thm_pairs ctxt respect_no_atp - #> tap (fn ps => trace_msg - (fn () => ("Considering " ^ Int.toString (length ps) ^ - " theorems"))) - #> filter is_named - -(***************************************************************) -(* ATP invocation methods setup *) -(***************************************************************) - (**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) @@ -547,7 +475,6 @@ | _ => false in do_formula true end - fun has_bound_or_var_of_type tycons = exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s | Abs (_, Type (s, _), _) => member (op =) tycons s @@ -567,6 +494,81 @@ not full_types andalso (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t) +fun is_theorem_bad_for_atps full_types thm = + let val t = prop_of thm in + is_formula_too_complex t orelse exists_type type_has_top_sort t orelse + is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse + is_strange_thm thm + end + +fun all_name_thms_pairs ctxt full_types add_thms chained_ths = + let + val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); + val local_facts = ProofContext.facts_of ctxt; + val full_space = + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); + + fun valid_facts facts = + (facts, []) |-> Facts.fold_static (fn (name, ths0) => + if (Facts.is_concealed facts name orelse + (respect_no_atp andalso is_package_def name) orelse + member (op =) multi_base_blacklist (Long_Name.base_name name) orelse + String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso + forall (not o member Thm.eq_thm add_thms) ths0 then + I + else + let + fun check_thms a = + (case try (ProofContext.get_thms ctxt) a of + NONE => false + | SOME ths1 => Thm.eq_thms (ths0, ths1)) + val name1 = Facts.extern facts name; + val name2 = Name_Space.extern full_space name; + val ths = + ths0 |> map Clausifier.transform_elim_theorem + |> filter ((not o is_theorem_bad_for_atps full_types) orf + member Thm.eq_thm add_thms) + in + case find_first check_thms [name1, name2, name] of + NONE => I + | SOME name' => + cons (name' |> forall (member Thm.eq_thm chained_ths) ths + ? prefix chained_prefix, ths) + end) + in valid_facts global_facts @ valid_facts local_facts end; + +fun multi_name a th (n, pairs) = + (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs); + +fun add_names (_, []) pairs = pairs + | add_names (a, [th]) pairs = (a, th) :: pairs + | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs)) + +fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; + +(* The single-name theorems go after the multiple-name ones, so that single + names are preferred when both are available. *) +fun name_thm_pairs ctxt respect_no_atp name_thms_pairs = + let + val (mults, singles) = List.partition is_multi name_thms_pairs + val ps = [] |> fold add_names singles |> fold add_names mults + in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end; + +fun is_named ("", th) = + (warning ("No name for theorem " ^ + Display.string_of_thm_without_context th); false) + | is_named _ = true +fun checked_name_thm_pairs respect_no_atp ctxt = + name_thm_pairs ctxt respect_no_atp + #> tap (fn ps => trace_msg + (fn () => ("Considering " ^ Int.toString (length ps) ^ + " theorems"))) + #> filter is_named + +(***************************************************************) +(* ATP invocation methods setup *) +(***************************************************************) + fun relevant_facts full_types relevance_threshold relevance_convergence defs_relevant max_new theory_relevant (relevance_override as {add, del, only}) @@ -576,11 +578,8 @@ val axioms = checked_name_thm_pairs (respect_no_atp andalso not only) ctxt (if only then map (name_thms_pair_from_ref ctxt chained_ths) add - else all_name_thms_pairs ctxt add_thms chained_ths) + else all_name_thms_pairs ctxt full_types add_thms chained_ths) |> make_unique - |> map (apsnd Clausifier.transform_elim_theorem) - |> filter (fn (_, th) => member Thm.eq_thm add_thms th orelse - not (is_dangerous_term full_types (prop_of th))) in relevance_filter ctxt relevance_threshold relevance_convergence defs_relevant max_new theory_relevant relevance_override