# HG changeset patch
# User blanchet
# Date 1357332979 -3600
# Node ID 73612ad116e6408f564187a09aa75fc48fe874e1
# Parent  7ce87037fbeba049222ba30637c55b2b14a73704
learn from low-level, inside-class facts

diff -r 7ce87037fbeb -r 73612ad116e6 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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
 
diff -r 7ce87037fbeb -r 73612ad116e6 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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 =