File ‹ac_steps.ML›
signature AC_PROOFSTEPS =
sig
val max_ac: int Config.T
val simp_ac_expr: Proof.context -> ac_info -> box_id * cterm -> (box_id * thm) list
val get_ac_head_equiv:
Proof.context -> ac_info -> box_id * cterm -> (box_id * thm) list
val ac_expand_once:
Proof.context -> ac_info -> box_id * cterm -> (box_id * thm) list
val ac_expand:
Proof.context -> ac_info -> box_id * cterm -> (box_id * thm) list
val ac_expand_equiv: proofstep
val ac_expand_unit: proofstep
val add_ac_proofsteps: theory -> theory
end;
functor AC_ProofSteps(
structure ACUtil: ACUTIL;
structure Basic_UtilLogic: BASIC_UTIL_LOGIC;
structure ProofStepData: PROOFSTEP_DATA;
structure RewriteTable: REWRITE_TABLE;
structure Update: UPDATE;
): AC_PROOFSTEPS =
struct
val max_ac = Attrib.setup_config_int @{binding "max_ac"} (K 20)
fun rewrite_on_eqs ac_info eqs ct =
let
val t = Thm.term_of ct
in
if ACUtil.head_agrees ac_info t then
Conv.binop_conv (rewrite_on_eqs ac_info eqs) ct
else
case find_first (fn eq => t aconv (Util.lhs_of eq)) eqs of
NONE => Conv.all_conv ct
| SOME eq_th => eq_th
end
fun dest_ac_full ac_info ct =
if ACUtil.head_agrees ac_info (Thm.term_of ct) then
let
val (a1, a2) = Util.dest_binop_cargs ct
val sort_opt = if ACUtil.has_comm_th ac_info then
sort (Term_Ord.term_ord o apply2 Thm.term_of) else I
in
sort_opt (dest_ac_full ac_info a1 @ dest_ac_full ac_info a2)
end
else if ACUtil.eq_unit ac_info (Thm.term_of ct) then []
else [ct]
fun simp_ac_expr ctxt ac_info (id, cu) =
let
val cus = dest_ac_full ac_info cu
in
if null cus then [(id, Thm.reflexive cu)] else
cus |> map (RewriteTable.simplify_info ctxt)
|> BoxID.get_all_merges_info ctxt
|> BoxID.merge_box_with_info ctxt id
|> map (fn (id', eqs) => (id', rewrite_on_eqs ac_info eqs cu))
end
fun get_ac_head_equiv ctxt ac_info (id, cu) =
let
fun process_head_equiv (id', eq_th) =
let
val infos = simp_ac_expr ctxt ac_info (id', Thm.rhs_of eq_th)
in
map (BoxID.merge_eq_infos ctxt (id', eq_th)) infos
end
in
cu |> RewriteTable.get_head_equiv ctxt
|> BoxID.merge_box_with_info ctxt id
|> maps process_head_equiv
|> filter_out (Thm.is_reflexive o snd)
end
fun ac_expand_once ctxt ac_info (id, ct) =
let
val cus = dest_ac_full ac_info ct
fun get_equiv cu = get_ac_head_equiv ctxt ac_info (id, cu)
fun process_info (id', eq) =
(id', rewrite_on_eqs ac_info [eq] ct)
in
map process_info (maps get_equiv cus)
end
fun ac_expand ctxt ac_info (id, ct) =
let
val max_ac = Config.get ctxt max_ac
fun ac_equiv_eq_better (id, th) (id', th') =
let
val seq1 = dest_ac_full ac_info (Thm.rhs_of th)
val seq2 = dest_ac_full ac_info (Thm.rhs_of th')
in
Util.is_subseq (op aconv o apply2 Thm.term_of) (seq1, seq2) andalso
BoxID.is_eq_ancestor ctxt id id'
end
fun has_ac_equiv_eq_better infos info' =
exists (fn info => ac_equiv_eq_better info info') infos
fun helper (old, new) =
case new of
[] => old
| (id', eq_th) :: rest =>
if length old + length new > max_ac then
old @ take (max_ac - length old) new
else let
val old' = ((id', eq_th) :: old)
val rhs_expand =
(ac_expand_once ctxt ac_info (id', Thm.rhs_of eq_th))
|> Util.max_partial ac_equiv_eq_better
|> map (BoxID.merge_eq_infos ctxt (id', eq_th))
|> filter_out (has_ac_equiv_eq_better (old' @ rest))
in
helper (old', rest @ rhs_expand)
end
val start = simp_ac_expr ctxt ac_info (id, ct)
in
helper ([], start)
end
fun ac_expand_equiv_fn ctxt item1 item2 =
let
val thy = Proof_Context.theory_of ctxt
val {id = id1, tname = tname1, ...} = item1
val {id = id2, tname = tname2, ...} = item2
val (ct1, ct2) = (the_single tname1, the_single tname2)
val (t1, t2) = (Thm.term_of ct1, Thm.term_of ct2)
val id = BoxID.merge_boxes ctxt (id1, id2)
in
case ACUtil.get_head_ac_info thy t1 of
NONE => []
| SOME ac_info =>
if not (ACUtil.head_agrees ac_info t2) then []
else if Term_Ord.term_ord (t2, t1) = LESS then []
else if RewriteTable.is_equiv id ctxt (ct1, ct2) then []
else let
val expand1 = ac_expand ctxt ac_info (id, ct1)
val expand2 = ac_expand ctxt ac_info (id, ct2)
fun get_equiv ((id1, eq_th1), (id2, eq_th2)) =
let
val ct1 = Thm.rhs_of eq_th1
val ct2 = Thm.rhs_of eq_th2
val ts1 = dest_ac_full ac_info ct1
val ts2 = dest_ac_full ac_info ct2
in
if eq_list (op aconv o apply2 Thm.term_of) (ts1, ts2) then
let
val eq_th1' = ACUtil.normalize_all_ac ac_info ct1
val eq_th2' = ACUtil.normalize_all_ac ac_info ct2
val id' = BoxID.merge_boxes ctxt (id1, id2)
val eq = Util.transitive_list [
eq_th1, eq_th1', meta_sym eq_th2', meta_sym eq_th2]
in
[(id', Basic_UtilLogic.to_obj_eq eq)]
end
else []
end
in
(maps get_equiv (Util.all_pairs (expand1, expand2)))
|> filter (BoxID.has_incr_id o fst)
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
|> map (fn (id, th) => Update.thm_update_sc 1 (id, th))
end
end
val ac_expand_equiv =
{name = "ac_expand_equiv",
args = [TypedUniv TY_TERM, TypedUniv TY_TERM],
func = TwoStep ac_expand_equiv_fn}
fun ac_expand_unit_fn ctxt item =
let
val thy = Proof_Context.theory_of ctxt
val {id, tname, ...} = item
val ct = the_single tname
val t = Thm.term_of ct
in
case ACUtil.get_head_ac_info thy t of
NONE => []
| SOME ac_info =>
let
val expand = ac_expand ctxt ac_info (id, ct)
fun process_expand (id', eq_th) =
let
val ct = Thm.rhs_of eq_th
val ts = dest_ac_full ac_info ct
in
if length ts <= 1 then
let
val eq' = ACUtil.normalize_all_ac ac_info ct
val eq = Util.transitive_list [eq_th, eq']
in
[(id', Basic_UtilLogic.to_obj_eq eq)]
end
else []
end
in
(maps process_expand expand)
|> filter (BoxID.has_incr_id o fst)
|> map (fn (id, th) => Update.thm_update_sc 1 (id, th))
end
end
val ac_expand_unit =
{name = "ac_expand_unit",
args = [TypedUniv TY_TERM],
func = OneStep ac_expand_unit_fn}
val add_ac_proofsteps =
fold ProofStepData.add_prfstep [
ac_expand_equiv, ac_expand_unit
]
end