File ‹CS_UM.ML›
signature CS_UM =
sig
val match_inst_rec :
(thm -> term) ->
(thm -> bool) ->
Proof.context ->
thm ->
term ->
Envir.env list ->
thm list
val match_inst_list :
(thm -> term) ->
(thm -> bool) ->
Proof.context ->
thm ->
term ->
Envir.env list ->
thm list
val match_inst :
(
(thm -> term) ->
(thm -> bool) ->
Proof.context ->
thm ->
term ->
Envir.env list ->
thm list
) ->
(thm -> term) ->
(thm -> bool) ->
Proof.context ->
thm ->
term ->
thm list
end;
structure CS_UM: CS_UM =
struct
local
fun prep_trm ctxt (x, (T, t)) = ((x, T), Thm.cterm_of ctxt t);
fun prep_ty ctxt (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty);
fun um_inst ctxt thm env =
let
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
val inst =
(
TVars.make (map (prep_ty ctxt) tyenv),
Vars.make (map (prep_trm ctxt) tenv)
)
in
thm
|> Drule.instantiate_normalize inst
|> Drule.eta_contraction_rule
end;
fun um_inst_rec _ _ _ _ _ _ [] = []
| um_inst_rec cond pat_fun is_trivial ctxt thm trm (env::envs) =
let val thm' = um_inst ctxt thm env
in
if cond pat_fun is_trivial thm' trm
then single thm'
else um_inst_rec cond pat_fun is_trivial ctxt thm trm envs
end;
fun um_inst_list cond pat_fun is_trivial ctxt thm trm envs =
let
fun um_inst_rec_single env =
let val thm' = um_inst ctxt thm env
in
if cond pat_fun is_trivial thm' trm
then single thm'
else []
end
val thms = envs |> map um_inst_rec_single |> flat
in thms end;
fun match_cond pat_fun is_trivial thm' trm =
(pat_fun thm') aconv trm andalso not (is_trivial thm');
in
val match_inst_rec = um_inst_rec match_cond;
val match_inst_list = um_inst_list match_cond;
fun match_inst match_inst_impl pat_fun is_trivial ctxt thm trm =
let
val envs = Unify.matchers (Context.Proof ctxt) [(pat_fun thm, trm)]
|> Seq.list_of
in match_inst_impl pat_fun is_trivial ctxt thm trm envs end;
end;
end;