File ‹unfolding.ML›
signature UNFOLDING =
sig
val get_unfold_thms_by_name: theory -> string -> thm list
val get_unfold_thms: theory -> term -> thm list
val unfold: theory -> conv
val unfold_cmd: string -> Proof.state -> Proof.state
end;
signature UNFOLDING_KEYWORD =
sig
val unfold : string * Position.T
end
functor Unfolding(
structure Auto2_Outer: AUTO2_OUTER;
structure Basic_UtilLogic: BASIC_UTIL_LOGIC;
structure Unfolding_Keyword: UNFOLDING_KEYWORD;
): UNFOLDING =
struct
fun get_unfold_thms_by_name thy nm =
let
val simp_nm = nm ^ ".simps"
val def_nm = nm ^ "_def"
in
Global_Theory.get_thms thy simp_nm
handle ERROR _ => Global_Theory.get_thms thy def_nm
handle ERROR _ => raise Fail "get_unfold_thms"
end
fun get_unfold_thms thy t =
get_unfold_thms_by_name thy (Util.get_head_name t)
fun unfold thy ct =
let
val ths = get_unfold_thms thy (Thm.term_of ct)
in
Conv.first_conv (map Basic_UtilLogic.rewr_obj_eq ths) ct
end
fun unfold_cmd s state =
let
val {context = ctxt, ...} = Proof.goal state
val thy = Proof_Context.theory_of ctxt
val (_, (As, _)) = ctxt |> Auto2_State.get_subgoal
|> Util.strip_meta_horn
val cAs = map (Thm.cterm_of ctxt) As
val t = Syntax.read_term ctxt s
val eq_th = t |> Thm.cterm_of ctxt |> unfold thy
|> Basic_UtilLogic.to_obj_eq
|> fold Thm.implies_intr (rev cAs)
val _ = writeln ("Obtained " ^ (eq_th |> Thm.concl_of
|> Syntax.string_of_term ctxt))
val after_qed = Auto2_Outer.have_after_qed ctxt eq_th
in
state |> Proof.map_contexts (Auto2_State.map_head_th after_qed)
end
val _ =
Outer_Syntax.command Unfolding_Keyword.unfold "unfold a term"
(Parse.term >>
(fn s =>
Toplevel.proof (fn state => unfold_cmd s state)))
end