--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200
@@ -14,6 +14,7 @@
val subgoal_count : Proof.state -> int
val normalize_chained_theorems : thm list -> thm list
val reserved_isar_keyword_table : unit -> unit Symtab.table
+ val thms_in_proof : string list option -> thm -> string list
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -60,4 +61,36 @@
Keyword.dest () |-> union (op =)
|> map (rpair ()) |> Symtab.make
+(* 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 =
+ let
+ fun app n (PBody {thms, ...}) =
+ thms |> fold (fn (_, (name, prop, body)) => fn x =>
+ let
+ val body' = Future.join body
+ val n' =
+ n + (if name = "" orelse
+ (* uncommon case where the proved theorem occurs twice
+ (e.g., "Transitive_Closure.trancl_into_trancl") *)
+ (n = 1 andalso name = thm_name) then
+ 0
+ else
+ 1)
+ val x' = x |> n' <= 1 ? app n' body'
+ in (x' |> n = 1 ? f (name, prop, body')) end)
+ in fold (app 0) end
+
+fun thms_in_proof all_names th =
+ let
+ val is_name_ok =
+ case all_names of
+ SOME names => member (op =) names
+ | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
+ fun collect (s, _, _) = is_name_ok s ? insert (op =) s
+ val names =
+ [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
+ in names end
+
end;