--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 04 21:56:19 2013 +0100
@@ -330,12 +330,22 @@
fun if_thm_before th th' =
if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
+(* Hack: Conflate the facts about a class as seen from the outside with the
+ corresponding low-level facts, so that MaSh can learn from the low-level
+ proofs. *)
+fun un_class_ify s =
+ case first_field "_class" s of
+ SOME (pref, suf) => [s, pref ^ suf]
+ | NONE => [s]
+
fun build_all_names name_of facts =
let
fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
fun add_alias canon alias =
- Symtab.update (name_of alias, name_of (if_thm_before canon alias))
- fun add_aliases (_, aliases as canon :: _) = fold (add_alias canon) aliases
+ fold (fn s => Symtab.update (s, name_of (if_thm_before canon alias)))
+ (un_class_ify (Thm.get_name_hint canon))
+ fun add_aliases (_, aliases as canon :: _) =
+ fold (add_alias canon) aliases
val tab = fold_rev cons_thm facts Termtab.empty
in Termtab.fold add_aliases tab Symtab.empty end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 04 21:56:19 2013 +0100
@@ -86,32 +86,36 @@
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
fixes that seem to be missing over there; or maybe the two code portions are
not doing the same? *)
-fun fold_body_thms thm_name f =
+fun fold_body_thms thm_name name_map =
let
+ val thm_name' = name_map thm_name
fun app n (PBody {thms, ...}) =
thms |> fold (fn (_, (name, _, body)) => fn accum =>
let
- (* The second disjunct caters for the uncommon case where the proved
- theorem occurs in its own proof (e.g.,
- "Transitive_Closure.trancl_into_trancl"). *)
- val no_name = (name = "" orelse (n = 1 andalso name = thm_name))
+ val name' = name_map name
+ val collect = union (op =) o the_list
+ (* The "name = thm_name" case caters for the uncommon case where the
+ proved theorem occurs in its own proof (e.g.,
+ "Transitive_Closure.trancl_into_trancl"). The "name' = thm_name'"
+ case is to unfold low-level class facts ("Xxx.yyy.zzz") in the
+ proof of high-level class facts ("XXX.yyy_class.zzz"). *)
+ val no_name =
+ (name = "" orelse
+ (n = 1 andalso (name = thm_name orelse name' = thm_name')))
val accum =
- accum |> (if n = 1 andalso not no_name then f name else I)
+ accum |> (if n = 1 andalso not no_name then collect name' else I)
val n = n + (if no_name then 0 else 1)
in accum |> (if n <= 1 then app n (Future.join body) else I) end)
in fold (app 0) end
fun thms_in_proof all_names th =
let
- val collect =
+ val name_map =
case all_names of
- SOME names =>
- (fn s => case Symtab.lookup names s of
- SOME s' => insert (op =) s'
- | NONE => I)
- | NONE => insert (op =)
+ SOME names => Symtab.lookup names
+ | NONE => SOME
val names =
- [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
+ [] |> fold_body_thms (Thm.get_name_hint th) name_map [Thm.proof_body_of th]
in names end
fun thms_of_name ctxt name =