File ‹assn_matcher.ML›
type assn_matcher = Proof.context -> term * cterm -> id_inst -> id_inst_th list
signature ASSN_MATCHER =
sig
val add_assn_matcher: assn_matcher -> theory -> theory
val assn_match_term:
Proof.context -> term * cterm -> id_inst -> id_inst_th list
val assn_match_all:
Proof.context -> term * cterm -> id_inst -> id_inst_th list
val assn_match_strict:
Proof.context -> term * cterm -> id_inst -> id_inst_th list
val triv_assn_matcher: assn_matcher
val emp_assn_matcher: assn_matcher
val true_assn_matcher: assn_matcher
val add_entail_matcher: thm -> theory -> theory
val assn_match_single:
Proof.context -> term * cterm -> id_inst -> id_inst_th list
val add_assn_matcher_proofsteps: theory -> theory
end
structure MatchData = Theory_Data
(
type T = (assn_matcher * serial) list
val empty = []
val merge = Library.merge (eq_snd op =)
)
functor AssnMatcher(SepUtil: SEP_UTIL): ASSN_MATCHER =
struct
open SepUtil
structure ACUtil = Auto2_HOL_Extra_Setup.ACUtil
fun add_assn_matcher matcher = MatchData.map (cons (matcher, serial ()))
fun assn_match_term ctxt (pat, ct) (id, inst) =
let
val _ = assert (not (Term.is_Var pat))
"assn_match_term: pat should not be Var."
val thy = Proof_Context.theory_of ctxt
fun apply_matcher matcher = matcher ctxt (pat, ct) (id, inst)
fun process_res ((id, inst'), th) =
let
val _ = assert (is_entail (prop_of' th)) "assn_match_term"
val (_, rhs) = th |> prop_of' |> dest_entail
val exp_rhs = Util.subst_term_norm inst' pat
in
if rhs aconv exp_rhs then
((id, inst'), th |> apply_to_entail_r mult_emp_right)
else if UtilArith.is_times rhs andalso
dest_arg1 rhs aconv exp_rhs then
((id, inst'), th)
else if UtilArith.is_times rhs andalso
dest_arg rhs aconv exp_rhs then
((id, inst'),
th |> apply_to_entail_r (ACUtil.comm_cv assn_ac_info))
else
raise Fail "assn_match_term"
end
in
(maps (apply_matcher o #1) (MatchData.get thy))
|> map process_res
end
fun assn_match_all ctxt (pat, ct) (id, inst) =
if UtilArith.is_times pat then
let
val (A, B) = Util.dest_binop_args pat
val insts = assn_match_all ctxt (A, ct) (id, inst)
fun process_inst ((id', inst'), th) =
let
val ct' = th |> cprop_of' |> cdest_entail |> snd |> Thm.dest_arg
val B' = Util.subst_term_norm inst' B
val insts' = assn_match_all ctxt (B', ct') (id', inst')
fun process_inst' ((id'', inst''), th') =
let
val res = ([th, th'] MRS entails_trans2_th)
|> apply_to_entail_r (
ACUtil.assoc_sym_cv assn_ac_info)
in
((id'', inst''), res)
end
in
map process_inst' insts'
end
in
maps process_inst insts
end
else
assn_match_term ctxt (pat, ct) (id, inst)
fun assn_match_strict ctxt (pat, ct) (id, inst) =
let
val inst = assn_match_all ctxt (pat, ct) (id, inst)
fun process_inst ((id', inst'), th) =
let
val rhs = th |> prop_of' |> dest_entail |> snd
val _ = assert (UtilArith.is_times rhs andalso
dest_arg1 rhs aconv Util.subst_term_norm inst' pat)
"assn_match_strict"
in
if dest_arg rhs aconv emp then
[((id', inst'), th |> apply_to_entail_r reduce_emp_right)]
else []
end
in
maps process_inst inst
end
fun triv_assn_matcher ctxt (pat, ct) (id, inst) =
if pat aconv emp then []
else let
val cts = ACUtil.cdest_ac assn_ac_info ct
fun match_i i =
let
val ct' = nth cts i
val insts = Auto2_Setup.Matcher.rewrite_match ctxt (pat, ct') (id, inst)
fun process_inst ((id', inst'), eq_th) =
let
val th = entail_triv_th ctxt (Thm.term_of ct)
val cv = Conv.every_conv [
ACUtil.move_outmost assn_ac_info (Thm.term_of ct'),
ACUtil.ac_last_conv
assn_ac_info (Conv.rewr_conv (meta_sym eq_th))]
in
((id', inst'), th |> apply_to_entail_r cv)
end
in
map process_inst insts
end
in
maps match_i (0 upto (length cts - 1))
end
fun emp_assn_matcher ctxt (pat, ct) (id, inst) =
if not (pat aconv emp) then []
else [((id, inst), ct |> Thm.term_of |> entail_triv_th ctxt
|> apply_to_entail_r mult_emp_left)]
fun true_assn_matcher ctxt (pat, ct) (id, inst) =
if not (pat aconv assn_true) then []
else [((id, inst), ct |> Thm.term_of |> entail_true_th ctxt
|> apply_to_entail_r mult_emp_left)]
fun entail_matcher' entail_th ctxt r ct id =
let
val pat_r = entail_th |> prop_of' |> dest_entail |> snd |> dest_arg
val inst_r = Auto2_Setup.Matcher.rewrite_match ctxt (pat_r, Thm.cterm_of ctxt r) (id, fo_init)
fun process_inst_r ((id', inst'), eq_th) =
let
val entail_th' = Util.subst_thm ctxt inst' entail_th
val pat = entail_th' |> prop_of' |> dest_arg1
val matches = assn_match_all ctxt (pat, ct) (id', fo_init)
fun process_match ((id'', _), th) =
let
val cv = eq_th |> Conv.rewr_conv |> Util.argn_conv 1
|> ACUtil.ac_last_conv assn_ac_info
val th' = th |> apply_to_entail_r (ACUtil.comm_cv assn_ac_info)
in
(id'', ([th', entail_th'] MRS entails_trans2_th)
|> apply_to_entail_r cv)
end
in
map process_match matches
end
in
maps process_inst_r inst_r
end
fun entail_matcher entail_th ctxt (pat, ct) (id, inst) =
let
val (f, args) = Term.strip_comb pat
val pat_f = entail_th |> prop_of' |> dest_entail |> snd |> Term.head_of
in
if not (Term.aconv_untyped (f, pat_f)) orelse
Util.has_vars (nth args 1) then []
else let
val (pat_xs, r) = the_pair args
val matches = entail_matcher' entail_th ctxt r ct id
fun process_res (id', th) =
let
val xs = th |> cprop_of' |> Thm.dest_arg
|> ACUtil.cdest_ac assn_ac_info
|> List.last |> Drule.strip_comb |> snd |> hd
val insts = Auto2_Setup.Matcher.rewrite_match ctxt (pat_xs, xs) (id', inst)
fun process_inst ((id'', inst'), eq_th) =
let
val cv = eq_th |> meta_sym |> Conv.rewr_conv
|> Conv.arg1_conv
|> ACUtil.ac_last_conv assn_ac_info
in
((id'', inst'), th |> apply_to_entail_r cv)
end
in
map process_inst insts
end
in
maps process_res matches
end
end
fun add_entail_matcher th =
let
val (pat_f, pat_args) = th |> prop_of' |> dest_entail |> snd
|> Term.strip_comb
val _ = assert (length pat_args = 2 andalso Term.is_Const pat_f)
"add_entail_matcher: th must be in form A ==> f ?xs pat_r."
in
add_assn_matcher (entail_matcher th)
end
fun assn_match_single ctxt (pat, ct) (id, inst) =
let
val cts = ACUtil.cdest_ac assn_ac_info ct
fun match_i i =
let
val ct' = nth cts i
val t' = Thm.term_of ct'
val insts = Auto2_Setup.Matcher.rewrite_match ctxt (pat, ct') (id, inst)
fun process_inst ((id', inst'), eq_th) =
let
val eq_th' =
if length cts = 1 then
eq_th |> meta_sym
|> apply_to_rhs mult_emp_right
else
Conv.every_conv [
ACUtil.move_outmost assn_ac_info t',
Conv.arg_conv (Conv.rewr_conv (meta_sym eq_th)),
ACUtil.comm_cv assn_ac_info] ct
in
((id', inst'), eq_th')
end
in
map process_inst insts
end
in
maps match_i (0 upto (length cts - 1))
end
val add_assn_matcher_proofsteps =
fold add_assn_matcher [
triv_assn_matcher, emp_assn_matcher, true_assn_matcher
]
end