File ‹thm_util.ML›
signature THM_UTIL =
sig
include HAS_LOGGER
val pretty_THM : Proof.context -> string * int * thm list -> Pretty.T
val abstract_rule : Proof.context -> string -> cterm -> thm -> thm option
val protect : thm -> thm
end
structure Thm_Util : THM_UTIL =
struct
val logger = Logger.setup_new_logger Logger.root "Thm_Util"
fun pretty_THM ctxt (msg, subgoal, thms) = Pretty.block [
Pretty.str msg,
Pretty.fbrk,
Pretty.str "Subgoal number ",
Pretty.str (string_of_int subgoal),
Pretty.fbrk,
Pretty.str "Theorems ",
Pretty.list "[" "]" (map (Thm.pretty_thm ctxt) thms)
]
fun abstract_rule ctxt n ct thm = SOME (Thm.abstract_rule n ct thm)
handle THM data => (@{log Logger.DEBUG} ctxt (fn _ => pretty_THM ctxt data |> Pretty.string_of);
NONE)
fun protect thm = Thm.instantiate' [] [SOME (Thm.cprop_of thm)] Drule.protectI
|> Thm.elim_implies thm
end