116 val {relevance_thresholds, max_relevant, slicing, ...} = |
116 val {relevance_thresholds, max_relevant, slicing, ...} = |
117 Sledgehammer_Isar.default_params ctxt args |
117 Sledgehammer_Isar.default_params ctxt args |
118 val default_max_relevant = |
118 val default_max_relevant = |
119 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing |
119 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing |
120 prover |
120 prover |
121 val is_good_prop = |
121 val is_appropriate_prop = |
122 Sledgehammer_Provers.is_good_prop_for_prover ctxt default_prover |
122 Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt |
|
123 default_prover |
123 val is_built_in_const = |
124 val is_built_in_const = |
124 Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover |
125 Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover |
125 val relevance_fudge = |
126 val relevance_fudge = |
126 extract_relevance_fudge args |
127 extract_relevance_fudge args |
127 (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) |
128 (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover) |
128 val relevance_override = {add = [], del = [], only = false} |
129 val relevance_override = {add = [], del = [], only = false} |
129 val subgoal = 1 |
130 val subgoal = 1 |
130 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
131 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal |
131 val facts = |
132 val facts = |
132 Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
133 Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
133 (the_default default_max_relevant max_relevant) is_good_prop |
134 (the_default default_max_relevant max_relevant) |
134 is_built_in_const relevance_fudge relevance_override facts hyp_ts |
135 is_appropriate_prop is_built_in_const relevance_fudge |
135 concl_t |
136 relevance_override facts hyp_ts concl_t |
136 |> map (fst o fst) |
137 |> map (fst o fst) |
137 val (found_facts, lost_facts) = |
138 val (found_facts, lost_facts) = |
138 flat proofs |> sort_distinct string_ord |
139 flat proofs |> sort_distinct string_ord |
139 |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
140 |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
140 |> List.partition (curry (op <=) 0 o fst) |
141 |> List.partition (curry (op <=) 0 o fst) |