File ‹list_ac.ML›
signature LIST_AC =
sig
datatype heads = LIST_APPEND | LIST_CONS | LIST_NIL | LIST_OTHER
val append_const: typ -> term
val case_head: typ -> term -> heads
val is_list_head: typ -> term -> bool
val get_list_ty: term -> typ option
val rewrite_on_eqs: typ -> thm list -> cterm -> thm
val dest_list_full: Proof.context -> typ -> cterm -> cterm list
val simp_list_expr:
Proof.context -> typ -> box_id * cterm -> (box_id * thm) list
val get_list_head_equiv:
Proof.context -> typ -> box_id * cterm -> (box_id * thm) list
val list_expand_once:
Proof.context -> typ -> box_id * cterm -> (box_id * thm) list
val list_expand:
Proof.context -> typ -> box_id * cterm -> (box_id * thm) list
val normalize_list_assoc: typ -> conv
val normalize_list: typ -> conv
val list_expand_equiv: proofstep
val list_expand_unit: proofstep
val add_list_proofsteps: theory -> theory
end;
structure List_AC : LIST_AC =
struct
datatype heads = LIST_APPEND | LIST_CONS | LIST_NIL | LIST_OTHER
fun append_const T =
let val lT = HOLogic.listT T
in Const (@{const_name append}, lT --> lT --> lT) end
fun case_head T t =
if Util.is_head (append_const T) t then LIST_APPEND
else if Util.is_head (HOLogic.cons_const T) t andalso
not (dest_arg t aconv HOLogic.nil_const T) then LIST_CONS
else if t aconv HOLogic.nil_const T then LIST_NIL
else LIST_OTHER
fun is_list_head T t =
case case_head T t of
LIST_APPEND => true
| LIST_CONS => true
| _ => false
fun get_list_ty t =
case fastype_of t of
Type ("List.list", [T]) => SOME T
| _ => NONE
fun rewrite_on_eqs T eqs ct =
case case_head T (Thm.term_of ct) of
LIST_APPEND => Conv.binop_conv (rewrite_on_eqs T eqs) ct
| LIST_CONS => Conv.binop_conv (rewrite_on_eqs T eqs) ct
| LIST_NIL => Conv.all_conv ct
| _ =>
(case find_first (fn eq => (Thm.term_of ct) aconv (Util.lhs_of eq)) eqs of
NONE => Conv.all_conv ct
| SOME eq_th => eq_th)
fun dest_list_full ctxt T ct =
case case_head T (Thm.term_of ct) of
LIST_APPEND => dest_list_full ctxt T (Thm.dest_arg1 ct) @
dest_list_full ctxt T (Thm.dest_arg ct)
| LIST_CONS => Thm.cterm_of ctxt (
HOLogic.mk_list T [dest_arg1 (Thm.term_of ct)]) ::
dest_list_full ctxt T (Thm.dest_arg ct)
| LIST_NIL => []
| _ => [ct]
fun dest_subs ctxt T ct =
case case_head T (Thm.term_of ct) of
LIST_APPEND => dest_subs ctxt T (Thm.dest_arg1 ct) @
dest_subs ctxt T (Thm.dest_arg ct)
| LIST_CONS => Thm.dest_arg1 ct ::
dest_subs ctxt T (Thm.dest_arg ct)
| LIST_NIL => []
| _ => [ct]
fun simp_list_expr ctxt T (id, cu) =
let
val cus = dest_subs ctxt T cu
in
if null cus then [(id, Thm.reflexive cu)] else
cus |> map (Auto2_Setup.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 T eqs cu))
end
fun get_list_head_equiv ctxt T (id, cu) =
let
fun process_head_equiv (id', eq_th) =
let
val infos = simp_list_expr ctxt T (id', Thm.rhs_of eq_th)
in
map (BoxID.merge_eq_infos ctxt (id', eq_th)) infos
end
in
cu |> Auto2_Setup.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 list_expand_once ctxt T (id, ct) =
let
val cus = dest_subs ctxt T ct
fun get_equiv cu = get_list_head_equiv ctxt T (id, cu)
fun process_info (id', eq) =
(id', rewrite_on_eqs T [eq] ct)
in
map process_info (maps get_equiv cus)
end
fun list_expand ctxt T (id, ct) =
let
val max_ac = Config.get ctxt Auto2_HOL_Extra_Setup.AC_ProofSteps.max_ac
fun list_equiv_eq_better (id, th) (id', th') =
let
val seq1 = dest_list_full ctxt T (Thm.rhs_of th)
val seq2 = dest_list_full ctxt T (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_list_equiv_eq_better infos info' =
exists (fn info => list_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 =
(list_expand_once ctxt T (id', Thm.rhs_of eq_th))
|> Util.max_partial list_equiv_eq_better
|> map (BoxID.merge_eq_infos ctxt (id', eq_th))
|> filter_out (has_list_equiv_eq_better (old' @ rest))
in
helper (old', rest @ rhs_expand)
end
val start = simp_list_expr ctxt T (id, ct)
in
helper ([], start)
end
fun normalize_list_assoc T ct =
case case_head T (Thm.term_of ct) of
LIST_APPEND =>
(case case_head T (dest_arg1 (Thm.term_of ct)) of
LIST_APPEND =>
Conv.every_conv [rewr_obj_eq @{thm List.append_assoc},
Conv.arg_conv (normalize_list_assoc T)] ct
| _ => Conv.all_conv ct)
| _ => Conv.all_conv ct
fun normalize_list T ct =
case case_head T (Thm.term_of ct) of
LIST_APPEND =>
Conv.every_conv [
Conv.binop_conv (normalize_list T),
Conv.try_conv (rewr_obj_eq @{thm List.append.append_Nil}),
Conv.try_conv (rewr_obj_eq @{thm List.append_Nil2}),
normalize_list_assoc T] ct
| LIST_CONS =>
Conv.every_conv [rewr_obj_eq @{thm cons_to_append},
normalize_list T] ct
| _ => Conv.all_conv ct
fun list_expand_equiv_fn ctxt item1 item2 =
let
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)
val T = the (get_list_ty t1)
in
if Term_Ord.term_ord (t2, t1) = LESS then []
else if Auto2_Setup.RewriteTable.is_equiv id ctxt (ct1, ct2) then []
else if not (is_list_head T t1) orelse not (is_list_head T t2) then []
else let
val expand1 = list_expand ctxt T (id, ct1)
val expand2 = list_expand ctxt T (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_list_full ctxt T ct1
val ts2 = dest_list_full ctxt T ct2
in
if eq_list (op aconv o apply2 Thm.term_of) (ts1, ts2) then
let
val eq_th1' = normalize_list T ct1
val eq_th2' = normalize_list T 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', 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) => Auto2_Setup.Update.thm_update_sc 1 (id, th))
end
end
val list_expand_equiv =
{name = "list_expand_equiv",
args = [TypedMatch (TY_TERM, @{term_pat "?A::?'a list"}),
TypedMatch (TY_TERM, @{term_pat "?B::?'a list"})],
func = TwoStep list_expand_equiv_fn}
fun list_expand_unit_fn ctxt item =
let
val {id, tname, ...} = item
val ct = the_single tname
val t = Thm.term_of ct
val T = the (get_list_ty t)
in
if not (is_list_head T t) then []
else let
val expand = list_expand ctxt T (id, ct)
fun process_expand (id', eq_th) =
let
val ct = Thm.rhs_of eq_th
val ts = dest_list_full ctxt T ct
in
if length ts <= 1 then
let
val eq' = normalize_list T ct
val eq = Util.transitive_list [eq_th, eq']
in
[(id', to_obj_eq eq)]
end
else []
end
in
(maps process_expand expand)
|> filter (BoxID.has_incr_id o fst)
|> map (fn (id, th) => Auto2_Setup.Update.thm_update_sc 1 (id, th))
end
end
val list_expand_unit =
{name = "list_expand_unit",
args = [TypedMatch (TY_TERM, @{term_pat "?A::?'a list"})],
func = OneStep list_expand_unit_fn}
val add_list_proofsteps =
fold add_prfstep [
list_expand_equiv, list_expand_unit
]
end
val _ = Theory.setup List_AC.add_list_proofsteps