1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 23:30:18 2011 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Jun 10 12:01:15 2011 +0200
1.3 @@ -39,19 +39,23 @@
1.4 val new_monomorphizer : bool Config.T
1.5 val ignore_no_atp : bool Config.T
1.6 val instantiate_inducts : bool Config.T
1.7 + val const_names_in_fact :
1.8 + theory -> (string * typ -> term list -> bool * term list) -> term
1.9 + -> string list
1.10 val fact_from_ref :
1.11 Proof.context -> unit Symtab.table -> thm list
1.12 -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
1.13 val all_facts :
1.14 - Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list
1.15 - -> thm list -> (((unit -> string) * locality) * thm) list
1.16 - val const_names_in_fact :
1.17 - theory -> (string * typ -> term list -> bool * term list) -> term
1.18 - -> string list
1.19 + Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
1.20 + -> (((unit -> string) * locality) * thm) list
1.21 + val nearly_all_facts :
1.22 + Proof.context -> relevance_override -> thm list -> term list -> term
1.23 + -> (((unit -> string) * locality) * thm) list
1.24 val relevant_facts :
1.25 - Proof.context -> real * real -> int -> (term -> bool)
1.26 + Proof.context -> real * real -> int
1.27 -> (string * typ -> term list -> bool * term list) -> relevance_fudge
1.28 -> relevance_override -> thm list -> term list -> term
1.29 + -> (((unit -> string) * locality) * thm) list
1.30 -> ((string * locality) * thm) list
1.31 end;
1.32
1.33 @@ -778,12 +782,11 @@
1.34 (**** Predicates to detect unwanted facts (prolific or likely to cause
1.35 unsoundness) ****)
1.36
1.37 -fun is_theorem_bad_for_atps is_appropriate_prop thm =
1.38 +fun is_theorem_bad_for_atps thm =
1.39 let val t = prop_of thm in
1.40 - not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
1.41 - exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
1.42 - exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
1.43 - is_that_fact thm
1.44 + is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
1.45 + exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
1.46 + is_metastrange_theorem thm orelse is_that_fact thm
1.47 end
1.48
1.49 fun meta_equify (@{const Trueprop}
1.50 @@ -810,7 +813,7 @@
1.51 |> add Simp normalize_simp_prop snd simps
1.52 end
1.53
1.54 -fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
1.55 +fun all_facts ctxt reserved really_all add_ths chained_ths =
1.56 let
1.57 val thy = Proof_Context.theory_of ctxt
1.58 val global_facts = Global_Theory.facts_of thy
1.59 @@ -860,7 +863,7 @@
1.60 #> fold (fn th => fn (j, (multis, unis)) =>
1.61 (j + 1,
1.62 if not (member Thm.eq_thm_prop add_ths th) andalso
1.63 - is_theorem_bad_for_atps is_appropriate_prop th then
1.64 + is_theorem_bad_for_atps th then
1.65 (multis, unis)
1.66 else
1.67 let
1.68 @@ -894,30 +897,36 @@
1.69 fun external_frees t =
1.70 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
1.71
1.72 +fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths
1.73 + hyp_ts concl_t =
1.74 + let
1.75 + val thy = Proof_Context.theory_of ctxt
1.76 + val reserved = reserved_isar_keyword_table ()
1.77 + val add_ths = Attrib.eval_thms ctxt add
1.78 + val ind_stmt =
1.79 + Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
1.80 + |> Object_Logic.atomize_term thy
1.81 + val ind_stmt_xs = external_frees ind_stmt
1.82 + in
1.83 + (if only then
1.84 + maps (map (fn ((name, loc), th) => ((K name, loc), th))
1.85 + o fact_from_ref ctxt reserved chained_ths) add
1.86 + else
1.87 + all_facts ctxt reserved false add_ths chained_ths)
1.88 + |> Config.get ctxt instantiate_inducts
1.89 + ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
1.90 + |> (not (Config.get ctxt ignore_no_atp) andalso not only)
1.91 + ? filter_out (No_ATPs.member ctxt o snd)
1.92 + |> uniquify
1.93 + end
1.94 +
1.95 fun relevant_facts ctxt (threshold0, threshold1) max_relevant
1.96 - is_appropriate_prop is_built_in_const fudge
1.97 - (override as {add, only, ...}) chained_ths hyp_ts concl_t =
1.98 + is_built_in_const fudge (override as {only, ...}) chained_ths
1.99 + hyp_ts concl_t facts =
1.100 let
1.101 val thy = Proof_Context.theory_of ctxt
1.102 val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.103 1.0 / Real.fromInt (max_relevant + 1))
1.104 - val add_ths = Attrib.eval_thms ctxt add
1.105 - val reserved = reserved_isar_keyword_table ()
1.106 - val ind_stmt =
1.107 - Logic.list_implies (hyp_ts |> filter_out (null o external_frees), concl_t)
1.108 - |> Object_Logic.atomize_term thy
1.109 - val ind_stmt_xs = external_frees ind_stmt
1.110 - val facts =
1.111 - (if only then
1.112 - maps (map (fn ((name, loc), th) => ((K name, loc), th))
1.113 - o fact_from_ref ctxt reserved chained_ths) add
1.114 - else
1.115 - all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
1.116 - |> Config.get ctxt instantiate_inducts
1.117 - ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
1.118 - |> (not (Config.get ctxt ignore_no_atp) andalso not only)
1.119 - ? filter_out (No_ATPs.member ctxt o snd)
1.120 - |> uniquify
1.121 in
1.122 trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
1.123 " facts");