learn from low-level, inside-class facts
authorblanchet
Fri Jan 04 21:56:19 2013 +0100 (2013-01-04 ago)
changeset 5073473612ad116e6
parent 50733 7ce87037fbeb
child 50735 6b232d76cbc9
learn from low-level, inside-class facts
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 04 21:56:19 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 04 21:56:19 2013 +0100
     1.3 @@ -330,12 +330,22 @@
     1.4  fun if_thm_before th th' =
     1.5    if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
     1.6  
     1.7 +(* Hack: Conflate the facts about a class as seen from the outside with the
     1.8 +   corresponding low-level facts, so that MaSh can learn from the low-level
     1.9 +   proofs. *)
    1.10 +fun un_class_ify s =
    1.11 +  case first_field "_class" s of
    1.12 +    SOME (pref, suf) => [s, pref ^ suf]
    1.13 +  | NONE => [s]
    1.14 +
    1.15  fun build_all_names name_of facts =
    1.16    let
    1.17      fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
    1.18      fun add_alias canon alias =
    1.19 -      Symtab.update (name_of alias, name_of (if_thm_before canon alias))
    1.20 -    fun add_aliases (_, aliases as canon :: _) = fold (add_alias canon) aliases
    1.21 +      fold (fn s => Symtab.update (s, name_of (if_thm_before canon alias)))
    1.22 +           (un_class_ify (Thm.get_name_hint canon))
    1.23 +    fun add_aliases (_, aliases as canon :: _) =
    1.24 +      fold (add_alias canon) aliases
    1.25      val tab = fold_rev cons_thm facts Termtab.empty
    1.26    in Termtab.fold add_aliases tab Symtab.empty end
    1.27  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 04 21:56:19 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 04 21:56:19 2013 +0100
     2.3 @@ -86,32 +86,36 @@
     2.4  (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
     2.5     fixes that seem to be missing over there; or maybe the two code portions are
     2.6     not doing the same? *)
     2.7 -fun fold_body_thms thm_name f =
     2.8 +fun fold_body_thms thm_name name_map =
     2.9    let
    2.10 +    val thm_name' = name_map thm_name
    2.11      fun app n (PBody {thms, ...}) =
    2.12        thms |> fold (fn (_, (name, _, body)) => fn accum =>
    2.13            let
    2.14 -            (* The second disjunct caters for the uncommon case where the proved
    2.15 -               theorem occurs in its own proof (e.g.,
    2.16 -               "Transitive_Closure.trancl_into_trancl"). *)
    2.17 -            val no_name = (name = "" orelse (n = 1 andalso name = thm_name))
    2.18 +            val name' = name_map name
    2.19 +            val collect = union (op =) o the_list
    2.20 +            (* The "name = thm_name" case caters for the uncommon case where the
    2.21 +               proved theorem occurs in its own proof (e.g.,
    2.22 +               "Transitive_Closure.trancl_into_trancl"). The "name' = thm_name'"
    2.23 +               case is to unfold low-level class facts ("Xxx.yyy.zzz") in the
    2.24 +               proof of high-level class facts ("XXX.yyy_class.zzz"). *)
    2.25 +            val no_name =
    2.26 +              (name = "" orelse
    2.27 +               (n = 1 andalso (name = thm_name orelse name' = thm_name')))
    2.28              val accum =
    2.29 -              accum |> (if n = 1 andalso not no_name then f name else I)
    2.30 +              accum |> (if n = 1 andalso not no_name then collect name' else I)
    2.31              val n = n + (if no_name then 0 else 1)
    2.32            in accum |> (if n <= 1 then app n (Future.join body) else I) end)
    2.33    in fold (app 0) end
    2.34  
    2.35  fun thms_in_proof all_names th =
    2.36    let
    2.37 -    val collect =
    2.38 +    val name_map =
    2.39        case all_names of
    2.40 -        SOME names =>
    2.41 -        (fn s => case Symtab.lookup names s of
    2.42 -                   SOME s' => insert (op =) s'
    2.43 -                 | NONE => I)
    2.44 -      | NONE => insert (op =)
    2.45 +        SOME names => Symtab.lookup names
    2.46 +      | NONE => SOME
    2.47      val names =
    2.48 -      [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
    2.49 +      [] |> fold_body_thms (Thm.get_name_hint th) name_map [Thm.proof_body_of th]
    2.50    in names end
    2.51  
    2.52  fun thms_of_name ctxt name =