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 backquote_thm : Proof.context -> thm -> string |
26 val backquote_thm : Proof.context -> thm -> string |
27 val is_blacklisted_or_something : Proof.context -> bool -> string -> bool |
27 val is_blacklisted_or_something : Proof.context -> bool -> string -> bool |
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
28 val clasimpset_rule_table_of : Proof.context -> status Termtab.table |
29 val build_all_names : |
29 val build_name_tables : |
30 (thm -> string) -> ('a * thm) list -> string Symtab.table |
30 (thm -> string) -> ('a * thm) list |
|
31 -> string Symtab.table * string Symtab.table |
31 val maybe_instantiate_inducts : |
32 val maybe_instantiate_inducts : |
32 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
33 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list |
33 -> (((unit -> string) * 'a) * thm) list |
34 -> (((unit -> string) * 'a) * thm) list |
34 val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list |
35 val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list |
35 val all_facts : |
36 val all_facts : |
336 fun un_class_ify s = |
337 fun un_class_ify s = |
337 case first_field "_class" s of |
338 case first_field "_class" s of |
338 SOME (pref, suf) => [s, pref ^ suf] |
339 SOME (pref, suf) => [s, pref ^ suf] |
339 | NONE => [s] |
340 | NONE => [s] |
340 |
341 |
341 fun build_all_names name_of facts = |
342 fun build_name_tables name_of facts = |
342 let |
343 let |
343 fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th) |
344 fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th) |
344 fun add_alias canon alias = |
345 fun add_plain canon alias = |
345 fold (fn s => Symtab.update (s, name_of (if_thm_before canon alias))) |
346 Symtab.update (Thm.get_name_hint canon, |
346 (un_class_ify (Thm.get_name_hint canon)) |
347 name_of (if_thm_before canon alias)) |
347 fun add_aliases (_, aliases as canon :: _) = |
348 fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases |
348 fold (add_alias canon) aliases |
349 fun add_inclass (name, target) = |
349 val tab = fold_rev cons_thm facts Termtab.empty |
350 fold (fn s => Symtab.update (s, target)) (un_class_ify name) |
350 in Termtab.fold add_aliases tab Symtab.empty end |
351 val prop_tab = fold_rev cons_thm facts Termtab.empty |
|
352 val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty |
|
353 val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty |
|
354 in (plain_name_tab, inclass_name_tab) end |
351 |
355 |
352 fun uniquify facts = |
356 fun uniquify facts = |
353 Termtab.fold (cons o snd) |
357 Termtab.fold (cons o snd) |
354 (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts |
358 (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts |
355 Termtab.empty) [] |
359 Termtab.empty) [] |