21 val instantiate_inducts : bool Config.T |
21 val instantiate_inducts : bool Config.T |
22 val no_fact_override : fact_override |
22 val no_fact_override : fact_override |
23 val fact_from_ref : |
23 val fact_from_ref : |
24 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table |
24 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table |
25 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list |
25 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list |
26 val is_likely_tautology_or_too_meta : thm -> bool |
|
27 val backquote_thm : thm -> string |
26 val backquote_thm : thm -> string |
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
27 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
29 val maybe_instantiate_inducts : |
28 val maybe_instantiate_inducts : |
30 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
29 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
31 -> (((unit -> string) * 'a) * thm) list |
30 -> (((unit -> string) * 'a) * thm) list |
48 type fact_override = |
47 type fact_override = |
49 {add : (Facts.ref * Attrib.src list) list, |
48 {add : (Facts.ref * Attrib.src list) list, |
50 del : (Facts.ref * Attrib.src list) list, |
49 del : (Facts.ref * Attrib.src list) list, |
51 only : bool} |
50 only : bool} |
52 |
51 |
53 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator |
52 val sledgehammer_prefixes = |
|
53 ["ATP", "Meson", "Metis", "Sledgehammer"] |> map (suffix Long_Name.separator) |
54 |
54 |
55 (* experimental features *) |
55 (* experimental features *) |
56 val ignore_no_atp = |
56 val ignore_no_atp = |
57 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) |
57 Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false) |
58 val instantiate_inducts = |
58 val instantiate_inducts = |
180 |
180 |
181 fun is_formula_too_complex ho_atp t = |
181 fun is_formula_too_complex ho_atp t = |
182 apply_depth t > max_apply_depth orelse |
182 apply_depth t > max_apply_depth orelse |
183 (not ho_atp andalso formula_has_too_many_lambdas [] t) |
183 (not ho_atp andalso formula_has_too_many_lambdas [] t) |
184 |
184 |
185 (* FIXME: Extend to "Meson" and "Metis" *) |
|
186 val exists_sledgehammer_const = |
185 val exists_sledgehammer_const = |
187 exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) |
186 exists_Const (fn (s, _) => |
|
187 exists (fn pref => String.isPrefix pref s) sledgehammer_prefixes) |
188 |
188 |
189 (* FIXME: make more reliable *) |
189 (* FIXME: make more reliable *) |
190 val exists_low_level_class_const = |
190 val exists_low_level_class_const = |
191 exists_Const (fn (s, _) => |
191 exists_Const (fn (s, _) => |
192 s = @{const_name equal_class.equal} orelse |
192 s = @{const_name equal_class.equal} orelse |
193 String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) |
193 String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s) |
194 |
194 |
195 fun is_metastrange_theorem th = |
|
196 case head_of (concl_of th) of |
|
197 Const (s, _) => (s <> @{const_name Trueprop} andalso |
|
198 s <> @{const_name "=="}) |
|
199 | _ => false |
|
200 |
|
201 fun is_that_fact th = |
195 fun is_that_fact th = |
202 String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) |
196 String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th) |
203 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN |
197 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN |
204 | _ => false) (prop_of th) |
198 | _ => false) (prop_of th) |
205 |
|
206 fun is_theorem_bad_for_atps ho_atp thm = |
|
207 is_metastrange_theorem thm orelse |
|
208 let val t = prop_of thm in |
|
209 is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse |
|
210 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
|
211 is_that_fact thm |
|
212 end |
|
213 |
199 |
214 fun is_likely_tautology_or_too_meta th = |
200 fun is_likely_tautology_or_too_meta th = |
215 let |
201 let |
216 val is_boring_const = member (op =) atp_widely_irrelevant_consts |
202 val is_boring_const = member (op =) atp_widely_irrelevant_consts |
217 fun is_boring_bool t = |
203 fun is_boring_bool t = |
225 | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = |
211 | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) = |
226 is_boring_bool t andalso is_boring_bool u |
212 is_boring_bool t andalso is_boring_bool u |
227 | is_boring_prop _ = true |
213 | is_boring_prop _ = true |
228 in |
214 in |
229 is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) |
215 is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th)) |
|
216 end |
|
217 |
|
218 fun is_theorem_bad_for_atps ho_atp th = |
|
219 is_likely_tautology_or_too_meta th orelse |
|
220 let val t = prop_of th in |
|
221 is_formula_too_complex ho_atp t orelse |
|
222 exists_type type_has_top_sort t orelse |
|
223 exists_sledgehammer_const t orelse exists_low_level_class_const t orelse |
|
224 is_that_fact th |
230 end |
225 end |
231 |
226 |
232 fun hackish_string_for_term thy t = |
227 fun hackish_string_for_term thy t = |
233 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
228 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) |
234 (print_mode_value ())) (Syntax.string_of_term_global thy) t |
229 (print_mode_value ())) (Syntax.string_of_term_global thy) t |
297 specs |> filter (member (op =) [Spec_Rules.Inductive, |
292 specs |> filter (member (op =) [Spec_Rules.Inductive, |
298 Spec_Rules.Co_Inductive] o fst) |
293 Spec_Rules.Co_Inductive] o fst) |
299 |> maps (snd o snd) |
294 |> maps (snd o snd) |
300 in |
295 in |
301 Termtab.empty |> add Simp [atomize] snd simps |
296 Termtab.empty |> add Simp [atomize] snd simps |
302 |> add Simp [] I rec_defs |
297 |> add Rec_Def [] I rec_defs |
303 |> add Def [] I nonrec_defs |
298 |> add Non_Rec_Def [] I nonrec_defs |
304 (* Add once it is used: |
299 (* Add once it is used: |
305 |> add Elim [] I elims |
300 |> add Elim [] I elims |
306 *) |
301 *) |
307 |> add Intro [] I intros |
302 |> add Intro [] I intros |
308 |> add Inductive [] I spec_intros |
303 |> add Inductive [] I spec_intros |
456 maps (map (fn ((name, stature), th) => ((K name, stature), th)) |
451 maps (map (fn ((name, stature), th) => ((K name, stature), th)) |
457 o fact_from_ref ctxt reserved chained css) add |
452 o fact_from_ref ctxt reserved chained css) add |
458 else |
453 else |
459 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in |
454 let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in |
460 all_facts ctxt ho_atp reserved add chained css |
455 all_facts ctxt ho_atp reserved add chained css |
461 |> filter_out (is_likely_tautology_or_too_meta o snd) |
|
462 |> filter_out (member Thm.eq_thm_prop del o snd) |
456 |> filter_out (member Thm.eq_thm_prop del o snd) |
463 |> maybe_filter_no_atps ctxt |
457 |> maybe_filter_no_atps ctxt |
464 |> uniquify |
458 |> uniquify |
465 end) |
459 end) |
466 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
460 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |