File ‹logic_steps.ML›
signature LOGIC_PROOFSTEPS =
sig
val shadow_prop_item: proofstep
val shadow_term_item: proofstep
val exists_elim_prfstep: proofstep
val add_logic_proofsteps: theory -> theory
val mk_all_disj: term list * term list -> term
val strip_all_disj: term -> term list * term list
val norm_all_disj: Proof.context -> conv
val replace_disj_vars:
Proof.context -> term list * term list -> term list * term list
val disj_prop_match:
Proof.context -> id_inst ->
term * (term list * term list) * ((indexname * typ) list * cterm list) ->
id_inst_th list
val norm_conj: conv
val TY_DISJ: string
val disj_to_ritems: bool -> term -> thm -> raw_item list
val disj_to_update: bool -> term -> box_id * int option * thm -> raw_update
val dest_tname_of_disj: cterm list -> term * cterm list
val is_match_prem_only: box_item -> bool
val analyze_disj_th: Proof.context -> thm -> term * thm
val disj_rewr_terms: term list -> term list
val output_disj_fn: item_output
val disj_prop_matcher: item_matcher
val reduce_disj_True: conv
val match_update_prfstep: proofstep
val match_one_sch_prfstep: proofstep
val disj_match_iff_prfstep: proofstep
val disj_create_case_prfstep: proofstep
val disj_shadow_prfstep: proofstep
val add_disj_proofsteps: theory -> theory
val split_not_imp_th: thm -> thm list
val split_conj_gen_th: Proof.context -> thm -> thm list
val eq_normalizer: Normalizer_Type.normalizer
val property_normalizer: Normalizer_Type.normalizer
val disj_normalizer: Normalizer_Type.normalizer
val logic_thm_update: Proof.context -> box_id * thm -> raw_update
val add_disj_normalizers: theory -> theory
end;
functor Logic_ProofSteps(
structure BoxItem: BOXITEM;
structure ItemIO: ITEM_IO;
structure Matcher: MATCHER;
structure Normalizer: NORMALIZER;
structure Property: PROPERTY;
structure ProofStepData: PROOFSTEP_DATA;
structure RewriteTable: REWRITE_TABLE;
structure UtilBase: UTIL_BASE;
structure UtilLogic: UTIL_LOGIC;
structure Update: UPDATE;
): LOGIC_PROOFSTEPS =
struct
fun boolVar s = Var ((s, 0), UtilBase.boolT)
fun shadow_item_fn ctxt item1 item2 =
if #sc item1 = 0 andalso #sc item2 = 0 then []
else let
val id = BoxItem.merged_id ctxt [item1, item2]
val _ = assert (forall (BoxItem.match_ty_strs [TY_TERM, TY_PROP])
[item1, item2])
"shadow_item_fn"
val (tname1, tname2) =
(the_single (#tname item1), the_single (#tname item2))
handle List.Empty => raise Fail "shadow_item_fn"
val (t1, t2) = (Thm.term_of tname1, Thm.term_of tname2)
val (lhs, rhs) =
if fastype_of t1 = UtilBase.boolT andalso UtilLogic.is_neg t1 andalso
fastype_of t2 = UtilBase.boolT andalso UtilLogic.is_neg t2 then
(UtilLogic.get_cneg tname1, UtilLogic.get_cneg tname2)
else
(tname1, tname2)
val equiv_ids =
(RewriteTable.subequiv_info ctxt id (lhs, rhs))
|> map fst |> filter BoxID.has_incr_id
|> Util.max_partial (BoxID.is_eq_ancestor ctxt)
val item_to_shadow =
if #uid item1 > #uid item2 then item1 else item2
fun process_id id' =
ShadowItem {id = id', item = item_to_shadow}
in
map process_id equiv_ids
end
val shadow_prop_item =
{name = "shadow_prop",
args = [TypedUniv TY_PROP, TypedUniv TY_PROP],
func = TwoStep shadow_item_fn}
val shadow_term_item =
{name = "shadow_term",
args = [TypedUniv TY_TERM, TypedUniv TY_TERM],
func = TwoStep shadow_item_fn}
fun eq_abs_fn ctxt item1 item2 =
let
val {id = id1, tname = tname1, ...} = item1
val {id = id2, tname = tname2, ...} = item2
val id = BoxID.merge_boxes ctxt (id1, id2)
val (ct1, ct2) = apply2 the_single (tname1, tname2)
val (t1, t2) = apply2 Thm.term_of (ct1, ct2)
in
if not (Util.is_abs t1) orelse not (Util.is_abs t2) then []
else if RewriteTable.is_equiv id ctxt (ct1, ct2) then []
else if Term_Ord.term_ord (t2, t1) = LESS then []
else let
fun process_equiv (id', eq_th) =
let
val (lhs, rhs) = (Util.lhs_of eq_th, Util.rhs_of eq_th)
in
AddItems {id = id', sc = SOME 1,
raw_items = [Fact (TY_EQ, [lhs, rhs], eq_th)]}
end
in
(Matcher.rewrite_match ctxt (t1, ct2) (id, fo_init))
|> map (fn ((id, _), eq_th) => (id, eq_th))
|> filter (BoxID.has_incr_id o fst)
|> Util.max_partial (BoxID.id_is_eq_ancestor ctxt)
|> map process_equiv
end
end
val eq_abs_prfstep =
{name = "eq_abs",
args = [TypedUniv TY_TERM, TypedUniv TY_TERM],
func = TwoStep eq_abs_fn}
fun exists_elim_fn ctxt {id, prop, ...} =
if not (BoxID.has_incr_id id) then [] else
let
val t = UtilLogic.prop_of' prop
in
if UtilLogic.is_ex t orelse UtilLogic.is_bex t orelse
(UtilLogic.is_neg t andalso UtilLogic.is_obj_all (UtilLogic.dest_not t)) orelse
(UtilLogic.is_neg t andalso UtilLogic.is_ball (UtilLogic.dest_not t)) then
let
val (ritems, th') =
prop |> UtilLogic.apply_to_thm' (UtilLogic.normalize_exists ctxt)
|> Update.apply_exists_ritems ctxt
in
[AddItems {id = id, sc = NONE,
raw_items = ritems @ [Update.thm_to_ritem th']}]
end
else []
end
val exists_elim_prfstep =
{name = "exists_elim",
args = [TypedUniv TY_PROP],
func = OneStep exists_elim_fn}
val add_logic_proofsteps =
fold ProofStepData.add_prfstep [
shadow_prop_item, shadow_term_item, exists_elim_prfstep, eq_abs_prfstep
]
fun mk_all_disj (vars, terms) =
case vars of
[] => UtilLogic.list_disj terms
| var :: vars' => UtilLogic.mk_obj_all var (mk_all_disj (vars', terms))
fun strip_disj t =
if UtilLogic.is_disj t then
maps strip_disj [dest_arg1 t, dest_arg t]
else if UtilLogic.is_imp t then
maps strip_disj [UtilLogic.get_neg (dest_arg1 t), dest_arg t]
else if UtilLogic.is_neg t then
let
val t' = UtilLogic.dest_not t
in
if UtilLogic.is_neg t' then strip_disj (UtilLogic.dest_not t')
else if UtilLogic.is_conj t' then
maps strip_disj [UtilLogic.get_neg (dest_arg1 t'), UtilLogic.get_neg (dest_arg t')]
else [t]
end
else [t]
fun strip_all_disj t =
if UtilLogic.is_obj_all t then
case t of
_ $ (u as Abs _) =>
let
val (v, body) = Term.dest_abs_global u
val var = Free v
val (vars, disjs) = strip_all_disj body
in
if exists (Util.occurs_free var) disjs then (var :: vars, disjs)
else (vars, disjs)
end
| f $ arg => strip_all_disj (f $ UtilLogic.force_abs_form arg)
| _ => raise Fail "strip_all_disj"
else if UtilLogic.is_ball t then
case t of
_ $ S $ (u as Abs _) =>
let
val (v, body) = Term.dest_abs_global u
val var = Free v
val mem = UtilLogic.mk_mem (var, S)
val (vars, disjs) = strip_all_disj body
in
(var :: vars, UtilLogic.get_neg mem :: disjs)
end
| f $ S $ arg => strip_all_disj (f $ S $ UtilLogic.force_abs_form arg)
| _ => raise Fail "strip_all_disj"
else if UtilLogic.is_neg t andalso UtilLogic.is_ex (UtilLogic.dest_not t) then
case UtilLogic.dest_not t of
_ $ (u as Abs _) =>
let
val (v, body) = Term.dest_abs_global u
val var = Free v
val (vars, disjs) = strip_all_disj (UtilLogic.get_neg body)
in
if exists (Util.occurs_free var) disjs then (var :: vars, disjs)
else (vars, disjs)
end
| f $ arg => strip_all_disj (UtilLogic.get_neg (f $ UtilLogic.force_abs_form arg))
| _ => raise Fail "strip_all_disj"
else if UtilLogic.is_neg t andalso UtilLogic.is_bex (UtilLogic.dest_not t) then
case UtilLogic.dest_not t of
_ $ S $ (u as Abs _) =>
let
val (v, body) = Term.dest_abs_global u
val var = Free v
val mem = UtilLogic.mk_mem (var, S)
val (vars, disjs) = strip_all_disj (UtilLogic.get_neg body)
in
(var :: vars, UtilLogic.get_neg mem :: disjs)
end
| f $ S $ arg => strip_all_disj (UtilLogic.get_neg (f $ S $ UtilLogic.force_abs_form arg))
| _ => raise Fail "strip_all_disj"
else if UtilLogic.is_disj t then
let
val (v1, ts1) = strip_all_disj (dest_arg1 t)
val (v2, ts2) = strip_all_disj (dest_arg t)
in
(v1 @ v2, ts1 @ ts2)
end
else if UtilLogic.is_imp t then
let
val (v1, ts1) = strip_all_disj (UtilLogic.get_neg (dest_arg1 t))
val (v2, ts2) = strip_all_disj (dest_arg t)
in
(v1 @ v2, ts1 @ ts2)
end
else if UtilLogic.is_neg t then
let
val t' = UtilLogic.dest_not t
in
if UtilLogic.is_neg t' then strip_all_disj (UtilLogic.dest_not t')
else if UtilLogic.is_conj t' then
let
val (v1, ts1) = strip_all_disj (UtilLogic.get_neg (dest_arg1 t'))
val (v2, ts2) = strip_all_disj (UtilLogic.get_neg (dest_arg t'))
in
(v1 @ v2, ts1 @ ts2)
end
else ([], [t])
end
else ([], [t])
fun norm_disj_clauses ct =
let
val (arg1, _) = Util.dest_binop_args (Thm.term_of ct)
in
if UtilLogic.is_disj arg1 then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.disj_assoc_th,
Conv.arg_conv norm_disj_clauses] ct
else
Conv.all_conv ct
end
fun norm_disj ct =
let
val t = Thm.term_of ct
val _ = assert (fastype_of t = UtilBase.boolT) "norm_disj: wrong type"
in
if UtilLogic.is_disj t then
Conv.every_conv [Conv.binop_conv norm_disj, norm_disj_clauses] ct
else if UtilLogic.is_imp t then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.imp_conv_disj_th, norm_disj] ct
else if UtilLogic.is_neg t andalso UtilLogic.is_neg (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.nn_cancel_th, norm_disj] ct
else if UtilLogic.is_neg t andalso UtilLogic.is_conj (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.de_Morgan_conj_th, norm_disj] ct
else
Conv.all_conv ct
end
fun norm_all_disj ctxt ct =
let
val t = Thm.term_of ct
in
if UtilLogic.is_obj_all t then
if not (Util.is_subterm (Bound 0) (dest_arg t)) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.all_trivial_th,
norm_all_disj ctxt] ct
else
Conv.every_conv [Conv.binder_conv (norm_all_disj o snd) ctxt] ct
else if UtilLogic.is_ball t then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.Ball_def_th, norm_all_disj ctxt] ct
else if UtilLogic.is_neg t andalso UtilLogic.is_ex (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.not_ex_th, norm_all_disj ctxt] ct
else if UtilLogic.is_neg t andalso UtilLogic.is_bex (UtilLogic.dest_not t) then
Conv.every_conv [
Conv.arg_conv (UtilLogic.rewr_obj_eq UtilBase.Bex_def_th), norm_all_disj ctxt] ct
else if UtilLogic.is_disj t then
let
val eq1 = Conv.binop_conv (norm_all_disj ctxt) ct
val rhs = Util.rhs_of eq1
in
if UtilLogic.is_obj_all (dest_arg1 rhs) then
Conv.every_conv [Conv.rewr_conv eq1,
UtilLogic.rewr_obj_eq UtilBase.disj_commute_th,
UtilLogic.rewr_obj_eq UtilBase.swap_all_disj_th,
norm_all_disj ctxt] ct
else if UtilLogic.is_obj_all (dest_arg rhs) then
Conv.every_conv [Conv.rewr_conv eq1,
UtilLogic.rewr_obj_eq UtilBase.swap_all_disj_th,
norm_all_disj ctxt] ct
else
Conv.every_conv [Conv.rewr_conv eq1, norm_disj_clauses] ct
end
else if UtilLogic.is_imp t then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.imp_conv_disj_th, norm_all_disj ctxt] ct
else if UtilLogic.is_neg t andalso UtilLogic.is_neg (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.nn_cancel_th, norm_all_disj ctxt] ct
else if UtilLogic.is_neg t andalso UtilLogic.is_conj (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.de_Morgan_conj_th, norm_all_disj ctxt] ct
else
Conv.all_conv ct
end
fun mk_disj_eq eq_ths =
case eq_ths of
[] => raise Fail "mk_disj_eq"
| [eq] => eq
| eq :: eqs' => Drule.binop_cong_rule UtilBase.cDisj eq (mk_disj_eq eqs')
fun sort_disj_clause_aux ct =
if not (UtilLogic.is_disj (Thm.term_of ct)) then Conv.all_conv ct else
let
val (arg1, arg2) = Util.dest_binop_args (Thm.term_of ct)
in
if UtilLogic.is_disj arg2 then
if Term_Ord.term_ord (dest_arg1 arg2, arg1) = LESS then
Conv.every_conv [UtilLogic.rewr_obj_eq (UtilLogic.obj_sym UtilBase.disj_assoc_th),
Conv.arg1_conv (UtilLogic.rewr_obj_eq UtilBase.disj_commute_th),
UtilLogic.rewr_obj_eq UtilBase.disj_assoc_th,
Conv.arg_conv sort_disj_clause_aux] ct
else
Conv.all_conv ct
else
if Term_Ord.term_ord (arg2, arg1) = LESS then
UtilLogic.rewr_obj_eq (UtilLogic.obj_sym UtilBase.disj_commute_th) ct
else
Conv.all_conv ct
end
fun sort_disj_clause ct =
if not (UtilLogic.is_disj (Thm.term_of ct)) then Conv.all_conv ct
else Conv.every_conv [Conv.arg_conv sort_disj_clause,
sort_disj_clause_aux] ct
fun forall_body_conv cv ctxt ct =
if UtilLogic.is_obj_all (Thm.term_of ct) then
Conv.binder_conv (fn (_, ctxt) => forall_body_conv cv ctxt) ctxt ct
else
cv ct
fun norm_all_disj_sorted ctxt ct =
Conv.every_conv [norm_all_disj ctxt,
forall_body_conv sort_disj_clause ctxt] ct
fun abstract_eq ctxt var eq =
let
val (x, T) = Term.dest_Free var
val all_const = Const (UtilBase.All_name, (T --> UtilBase.boolT) --> UtilBase.boolT)
in
Drule.arg_cong_rule (Thm.cterm_of ctxt all_const)
(Thm.abstract_rule x (Thm.cterm_of ctxt var) eq)
end
fun replace_disj_vars ctxt (vars, disjs) =
let
val vars' = vars |> map Term.dest_Free
|> Variable.variant_frees ctxt []
|> map Free
val subst = vars ~~ vars'
in
(vars', map (subst_atomic subst) disjs)
end
fun disj_prop_match ctxt (id, (tyinst, inst)) (t, (var_t, ts), (var_u, cus)) =
let
val thy = Proof_Context.theory_of ctxt
val us = map Thm.term_of cus
in
if length var_t <> length var_u orelse length ts <> length us then [] else
let
val tys_t = map fastype_of var_t
val tys_u = map snd var_u
val tyinst' = fold (Sign.typ_match thy) (tys_t ~~ tys_u) tyinst
val var_t' = map (Envir.subst_term_types tyinst') var_t
val ts' = ts |> map (Envir.subst_term_types tyinst')
val var_ct' = map (Thm.cterm_of ctxt) var_t'
val cus' = cus |> map (Thm.instantiate_cterm (TVars.empty, Vars.make (var_u ~~ var_ct')))
val insts = Matcher.rewrite_match_subset
ctxt var_t' (ts', cus') (id, (tyinst', inst))
fun process_inst ((id', instsp'), ths) =
let
val eq_th = ths |> mk_disj_eq
|> fold (abstract_eq ctxt) (rev var_t')
|> apply_to_lhs (norm_all_disj_sorted ctxt)
|> apply_to_rhs (norm_all_disj_sorted ctxt)
val t' = Util.subst_term_norm instsp' t
val norm1 = norm_all_disj_sorted ctxt (Thm.cterm_of ctxt t')
val cu = Thm.cterm_of ctxt (mk_all_disj (var_t', map Thm.term_of cus'))
val norm2 = norm_all_disj_sorted ctxt cu
val eq_th' = Util.transitive_list [norm1, eq_th, meta_sym norm2]
in
((id', instsp'), eq_th')
end
in
map process_inst insts
end
handle Type.TYPE_MATCH => []
end
fun norm_conj_de_Morgan ct =
let
val t = Thm.term_of ct
in
if UtilLogic.is_neg t andalso UtilLogic.is_disj (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.de_Morgan_disj_th,
Conv.arg_conv norm_conj_de_Morgan] ct
else
Conv.all_conv ct
end
fun norm_conj_not_imp ct =
let
val t = Thm.term_of ct
in
if UtilLogic.is_neg t andalso UtilLogic.is_imp (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.not_imp_th,
Conv.arg_conv norm_conj_not_imp] ct
else
Conv.all_conv ct
end
fun norm_nn_cancel ct =
let
val t = Thm.term_of ct
in
if UtilLogic.is_neg t andalso UtilLogic.is_neg (UtilLogic.dest_not t) then
Conv.every_conv [UtilLogic.rewr_obj_eq UtilBase.nn_cancel_th,
norm_nn_cancel] ct
else
Conv.all_conv ct
end
fun norm_conj ct =
let
val t = Thm.term_of ct
val _ = assert (fastype_of t = UtilBase.boolT) "norm_conj: wrong type"
in
if UtilLogic.is_neg t andalso UtilLogic.is_neg (UtilLogic.dest_not t) then
norm_nn_cancel ct
else if UtilLogic.is_neg t andalso UtilLogic.is_imp (UtilLogic.dest_not t) then
norm_conj_not_imp ct
else if UtilLogic.is_neg t andalso UtilLogic.is_disj (UtilLogic.dest_not t) then
norm_conj_de_Morgan ct
else
Conv.all_conv ct
end
val TY_DISJ = "DISJ"
fun disj_to_ritems prem_only disj_head th =
let
val subs = strip_disj (UtilLogic.prop_of' th)
in
if length subs = 1 then
if Util.has_vars (Thm.prop_of th) then
let
fun th_to_ritem th =
Fact (TY_DISJ,
UtilLogic.term_of_bool prem_only :: UtilLogic.disj :: strip_disj (UtilLogic.prop_of' th),
th)
in
map th_to_ritem (th |> UtilLogic.apply_to_thm' norm_conj
|> UtilLogic.split_conj_th)
end
else
[Fact (TY_PROP, [UtilLogic.prop_of' th], th)]
else let
val tname = UtilLogic.term_of_bool prem_only :: disj_head :: subs
in
[Fact (TY_DISJ, tname, th)]
end
end
fun disj_to_update prem_only disj_head (id, sc, th) =
if Thm.prop_of th aconv UtilLogic.pFalse then
ResolveBox {id = id, th = th}
else
AddItems {id = id, sc = sc,
raw_items = disj_to_ritems prem_only disj_head th}
fun get_disj_head t =
if UtilLogic.is_disj t then UtilLogic.disj
else if UtilLogic.is_imp t then get_disj_head (dest_arg t)
else if UtilLogic.is_neg t andalso UtilLogic.is_neg (UtilLogic.dest_not t) then
get_disj_head (UtilLogic.dest_not (UtilLogic.dest_not t))
else if UtilLogic.is_neg t andalso UtilLogic.is_conj (UtilLogic.dest_not t) then UtilLogic.conj
else if UtilLogic.is_obj_all t orelse UtilLogic.is_ball t then
case dest_arg t of
u as Abs _ => get_disj_head (snd (Term.dest_abs_global u))
| _ => UtilLogic.imp
else if UtilLogic.is_neg t andalso UtilLogic.is_ex (UtilLogic.dest_not t) then UtilLogic.conj
else if UtilLogic.is_neg t andalso UtilLogic.is_bex (UtilLogic.dest_not t) then UtilLogic.conj
else UtilLogic.imp
fun analyze_disj_th ctxt th =
let
val head = get_disj_head (UtilLogic.prop_of' th)
val th' = th |> UtilLogic.apply_to_thm' (norm_all_disj ctxt)
|> Util.apply_to_thm (UtilLogic.to_meta_conv ctxt)
|> Util.forall_elim_sch
in
(head, th')
end
fun dest_tname_of_disj tname =
case tname of
_ :: disj_head :: rest => (Thm.term_of disj_head, rest)
| _ => raise Fail "dest_tname_of_disj: too few terms in tname."
fun is_match_prem_only {tname, ...} =
UtilLogic.bool_of_term (Thm.term_of (hd tname))
fun is_active_head disj_head = (not (disj_head aconv UtilLogic.imp))
fun disj_rewr_terms ts =
if UtilLogic.bool_of_term (hd ts) then [] else drop 2 ts
fun output_disj_fn ctxt (ts, _) =
let
val (match_prem, disj_head, subs) = (hd ts, hd (tl ts), tl (tl ts))
val prefix = if UtilLogic.bool_of_term match_prem then "(match_prem) " else ""
in
if disj_head aconv UtilLogic.disj then
prefix ^ ((foldr1 UtilLogic.mk_disj subs) |> Syntax.string_of_term ctxt)
else if disj_head aconv UtilLogic.conj then
prefix ^ ((foldr1 UtilLogic.mk_conj (map UtilLogic.get_neg subs))
|> UtilLogic.get_neg |> Syntax.string_of_term ctxt)
else if disj_head aconv UtilLogic.imp then
prefix ^ ((foldr1 UtilLogic.mk_imp (subs |> split_last |> apfst (map UtilLogic.get_neg)
|> apsnd single |> (op @)))
|> Syntax.string_of_term ctxt)
else
raise Fail "output_disj_fn: unexpected disj_head."
end
val disj_prop_matcher =
let
fun pre_match pat {tname, ...} ctxt =
let
val (var_t, ts) = (strip_all_disj pat) |> replace_disj_vars ctxt
val (_, cus) = dest_tname_of_disj tname
val us = map Thm.term_of cus
val var_u = fold Term.add_vars us []
in
length ts = length us andalso length var_t = length var_u
end
fun match pat item ctxt (id, instsp) =
let
val {tname, prop = th, ...} = item
val (_, cus) = dest_tname_of_disj tname
val us = map Thm.term_of cus
val var_u = fold Term.add_vars us []
val (var_t, ts) = (strip_all_disj pat) |> replace_disj_vars ctxt
fun process_perm perm =
map (pair (map Var perm))
(disj_prop_match ctxt (id, instsp) (pat, (var_t, ts), (perm, cus)))
fun process_inst (var_u, ((id', instsp'), eq_th)) =
let
val eq_th' = UtilLogic.make_trueprop_eq (meta_sym eq_th)
val forall_th =
th |> fold Thm.forall_intr (rev (map (Thm.cterm_of ctxt) var_u))
|> Util.apply_to_thm (UtilLogic.to_obj_conv ctxt)
in
((id', instsp'), Thm.equal_elim eq_th' forall_th)
end
in
if length var_t <> length var_u orelse length ts <> length us then []
else var_u |> Util.all_permutes |> maps process_perm
|> map process_inst
end
in
{pre_match = pre_match, match = match}
end
fun ac_disj_conv cv ct =
if UtilLogic.is_disj (Thm.term_of ct) then
Conv.every_conv [Conv.arg1_conv cv,
Conv.arg_conv (ac_disj_conv cv)] ct
else cv ct
fun reduce_disj_True ct =
if UtilLogic.is_disj (Thm.term_of ct) then
((UtilLogic.rewr_obj_eq UtilBase.disj_True1_th)
else_conv ((Conv.arg_conv reduce_disj_True)
then_conv (UtilLogic.rewr_obj_eq UtilBase.disj_True2_th))) ct
else
Conv.all_conv ct
fun match_prop ctxt (id, item2) pat =
let
val disj_pats = strip_disj pat
fun process_inst ((id, inst), th) =
let
val to_eqT_cv = (th RS UtilBase.eq_True_th) |> UtilLogic.rewr_obj_eq |> Conv.try_conv
val pat_eqT =
pat |> Thm.cterm_of ctxt |> norm_disj
|> Util.subst_thm ctxt inst
|> apply_to_rhs (ac_disj_conv to_eqT_cv)
|> apply_to_rhs reduce_disj_True
|> UtilLogic.to_obj_eq
val patT = pat_eqT RS UtilBase.eq_True_inv_th
in
((id, inst), patT)
end
val insts1 =
(ItemIO.match_arg ctxt (PropMatch pat) item2 (id, fo_init))
|> filter (BoxID.has_incr_id o fst o fst)
val insts2 =
if length disj_pats > 1 then
map process_inst (maps (match_prop ctxt (id, item2)) disj_pats)
else []
in
insts1 @ insts2
end
fun disj_cancel_cv ctxt th ct =
if UtilLogic.is_disj (Thm.term_of ct) then
Conv.every_conv [Conv.arg_conv (disj_cancel_cv ctxt th),
Conv.try_conv (UtilLogic.rewr_obj_eq (th RS UtilBase.or_cancel1_th)),
Conv.try_conv (UtilLogic.rewr_obj_eq (th RS UtilBase.or_cancel2_th))] ct
else
Conv.all_conv ct
fun disj_cancel_prop ctxt th prop =
let
val th' = if UtilLogic.is_neg (UtilLogic.prop_of' th) then th
else th RS UtilBase.nn_create_th
val prop' = prop |> UtilLogic.apply_to_thm' (disj_cancel_cv ctxt th')
val P = th' |> UtilLogic.prop_of' |> UtilLogic.dest_not
in
if UtilLogic.prop_of' prop' aconv P then
[th', prop'] MRS UtilBase.contra_triv_th
else prop'
end
fun match_update_fn ctxt item1 item2 =
if is_match_prem_only item1 andalso
Util.has_vars (Thm.prop_of (#prop item1)) then [] else
let
val {id, prop, tname, ...} = item1
val thy = Proof_Context.theory_of ctxt
val (disj_head, csubs) = dest_tname_of_disj tname
val subs = map Thm.term_of csubs
fun count_var t = length (Term.add_vars t [])
val max_nvar = fold (curry Int.max) (map count_var subs) 0
fun is_priority_term t =
if UtilLogic.is_neg t then
exists (UtilLogic.is_ex orf UtilLogic.is_bex) (UtilLogic.strip_conj (UtilLogic.dest_not t))
else
exists (UtilLogic.is_obj_all orf UtilLogic.is_ball) (strip_disj t)
val has_priority_term = exists is_priority_term (map UtilLogic.get_neg subs)
val (NO_MATCH, SLOW_MATCH, YES_MATCH) = (0, 1, 2)
fun test_do_match t =
let
val nvar = count_var t
val neg_t = UtilLogic.get_neg t
in
if not (Util.is_pattern t) then NO_MATCH
else if length subs > 1 andalso
Property.is_property_prem thy neg_t then NO_MATCH
else if has_priority_term andalso
not (is_priority_term neg_t) then SLOW_MATCH
else if UtilLogic.is_mem neg_t andalso Term.is_Var (dest_arg1 neg_t) andalso
null (Term.add_frees (dest_arg neg_t) []) then SLOW_MATCH
else if nvar = 0 orelse nvar = max_nvar then YES_MATCH
else NO_MATCH
end
fun get_matches i =
let
val t = nth subs i
val do_match = test_do_match t
fun process_inst ((id', inst), th) =
let
val prop' = prop |> Util.subst_thm_thy thy inst
|> disj_cancel_prop ctxt th
val sc = if do_match = SLOW_MATCH then 200 else 10
in
disj_to_update false disj_head (id', SOME sc, prop') ::
(if count_var t > 0 then []
else [ShadowItem {id = id', item = item1}])
end
in
if do_match = NO_MATCH then []
else t |> UtilLogic.get_neg |> match_prop ctxt (id, item2)
|> maps process_inst
end
fun get_matches_no_var () =
let
fun process_inst (id', ths) =
let
val prop' = prop |> fold (disj_cancel_prop ctxt) ths
in
disj_to_update false disj_head (id', SOME 1, prop') ::
(if is_match_prem_only item1 then []
else [ShadowItem {id = id', item = item1}])
end
fun get_match_at_id id' insts =
insts |> filter (fn ((id, _), _) =>
BoxID.is_eq_ancestor ctxt id id')
|> map snd |> take 1
fun get_matches_at_id all_insts id' =
(id', maps (get_match_at_id id') all_insts)
fun merge_matches all_insts =
let
val ids = distinct (op =) (maps (map (fst o fst)) all_insts)
in
map (get_matches_at_id all_insts) ids
end
val _ = assert (length subs >= 2)
val ts = [hd subs, List.last subs]
in
ts |> map UtilLogic.get_neg |> map (match_prop ctxt (id, item2))
|> merge_matches
|> maps process_inst
end
in
if max_nvar = 0 then
get_matches_no_var ()
else
maps get_matches (0 upto (length subs - 1))
end
val match_update_prfstep =
{name = "disj_match_update",
args = [TypedUniv TY_DISJ, PropMatch (boolVar "A")],
func = TwoStep match_update_fn}
fun match_one_sch_fn ctxt item1 item2 =
if is_match_prem_only item1 then [] else
let
val {id, tname, prop = th1, ...} = item1
val thy = Proof_Context.theory_of ctxt
val subs = (dest_tname_of_disj tname) |> snd |> map Thm.term_of
in
if length subs > 1 then [] else
let
val t = the_single subs
val args = Util.dest_args t
fun count_var t = length (Term.add_vars t [])
val nvar = count_var t
fun get_matches i =
if count_var (nth args i) < nvar then [] else
let
val arg = nth args i
val targ = TypedMatch (TY_TERM, arg)
val insts = (ItemIO.match_arg ctxt targ item2 (id, fo_init))
|> filter (BoxID.has_incr_id o fst o fst)
fun inst_to_updt ((id', inst), _) =
let
val th1' = Util.subst_thm_thy thy inst th1
val prop' = UtilLogic.prop_of' th1'
in
if UtilBase.is_eq_term prop' andalso
RewriteTable.is_equiv_t id' ctxt (UtilBase.dest_eq prop')
then [] else [Update.thm_update (id', th1')]
end
in
maps inst_to_updt insts
end
in
maps get_matches (0 upto (length args - 1))
end
end
val match_one_sch_prfstep =
{name = "disj_match_one_sch",
args = [TypedUniv TY_DISJ, TypedUniv TY_TERM],
func = TwoStep match_one_sch_fn}
fun disj_match_iff_fn ctxt {id, tname, prop, ...} =
if not (BoxID.has_incr_id id) then [] else
let
val (_, csubs) = dest_tname_of_disj tname
val subs = map Thm.term_of csubs
in
if length subs > 1 then []
else if not (UtilBase.is_eq_term (the_single subs) andalso
fastype_of (dest_arg (the_single subs)) = UtilBase.boolT) then []
else let
val cv = (UtilLogic.to_obj_conv ctxt) then_conv (UtilLogic.Trueprop_conv norm_disj)
val forward = prop |> UtilLogic.equiv_forward_th |> Util.apply_to_thm cv
val backward = prop |> UtilLogic.equiv_backward_th |> Util.apply_to_thm cv
in
[disj_to_update false UtilLogic.imp (id, NONE, forward),
disj_to_update false UtilLogic.imp (id, NONE, backward)]
end
end
val disj_match_iff_prfstep =
{name = "disj_match_iff",
args = [TypedUniv TY_DISJ],
func = OneStep disj_match_iff_fn}
fun disj_create_case_fn _ {id, tname, ...} =
if not (BoxID.has_incr_id id) then [] else
if exists Util.has_vars (map Thm.term_of tname) then [] else
let
val (disj_head, csubs) = dest_tname_of_disj tname
in
if not (is_active_head disj_head) then []
else if length csubs = 1 then []
else let
val subs = map Thm.term_of csubs
in
[AddBoxes {id = id,
sc = NONE, init_assum = UtilLogic.mk_Trueprop (hd subs)}]
end
end
val disj_create_case_prfstep =
{name = "disj_create_case",
args = [TypedUniv TY_DISJ],
func = OneStep disj_create_case_fn}
fun disj_shadow_fn ctxt (item1 as {tname = tname1, ...})
(item2 as {tname = tname2, ...}) =
let
val id = BoxItem.merged_id ctxt [item1, item2]
val (disj_head1, subs1) = dest_tname_of_disj tname1
val (disj_head2, subs2) = dest_tname_of_disj tname2
in
if not (BoxID.has_incr_id id) then [] else
if not (is_active_head disj_head1) andalso
is_active_head disj_head2 then []
else if is_match_prem_only item1 andalso
not (is_match_prem_only item2) then []
else if subset (op aconvc) (subs1, subs2) then
[ShadowItem {id = id, item = item2}]
else []
end
val disj_shadow_prfstep =
{name = "disj_shadow",
args = [TypedUniv TY_DISJ, TypedUniv TY_DISJ],
func = TwoStep disj_shadow_fn}
val add_disj_proofsteps =
fold ItemIO.add_item_type [
(TY_DISJ, SOME disj_rewr_terms, SOME output_disj_fn, NONE)
] #> fold ItemIO.add_prop_matcher [
(TY_DISJ, disj_prop_matcher)
] #> fold ProofStepData.add_prfstep [
match_update_prfstep, match_one_sch_prfstep, disj_match_iff_prfstep,
disj_create_case_prfstep, disj_shadow_prfstep
]
fun split_not_imp_th th =
th |> UtilLogic.apply_to_thm' norm_conj_not_imp
|> UtilLogic.split_conj_th
fun split_conj_gen_th _ th =
th |> UtilLogic.apply_to_thm' norm_conj
|> UtilLogic.split_conj_th
fun eq_normalizer _ ritem =
case ritem of
Handler _ => [ritem]
| Fact (ty_str, _, th) =>
if ty_str <> TY_PROP then [ritem]
else if UtilBase.is_eq_term (UtilLogic.prop_of' th) then
let
val (lhs, rhs) = UtilBase.dest_eq (UtilLogic.prop_of' th)
in
if fastype_of lhs = UtilBase.boolT then
map Update.thm_to_ritem
(UtilLogic.split_conj_th (th RS UtilBase.iffD_th))
else
[Fact (TY_EQ, [lhs, rhs], th)]
end
else [ritem]
fun property_normalizer _ ritem =
case ritem of
Handler _ => [ritem]
| Fact (ty_str, _, th) =>
if ty_str <> TY_PROP then [ritem]
else if Property.is_property (UtilLogic.prop_of' th) then
[Fact (TY_PROPERTY, [UtilLogic.prop_of' th], th)]
else [ritem]
fun disj_normalizer ctxt ritem =
case ritem of
Handler _ => [ritem]
| Fact (ty_str, _, th) =>
if ty_str <> TY_PROP then [ritem]
else let
val t = UtilLogic.prop_of' th
in
if UtilLogic.is_neg t andalso UtilLogic.is_conj (UtilLogic.dest_not t) orelse
UtilLogic.is_disj t orelse UtilLogic.is_imp t orelse
UtilLogic.is_obj_all t orelse UtilLogic.is_ball t orelse
UtilLogic.is_neg t andalso UtilLogic.is_ex (UtilLogic.dest_not t) orelse
UtilLogic.is_neg t andalso UtilLogic.is_bex (UtilLogic.dest_not t)
then
let
val (disj_head, disj_th) = analyze_disj_th ctxt th
val prem_only = Auto2_State.lookup_prem_only ctxt t
val disj_th = if prem_only then disj_th
else snd (Normalizer.meta_use_vardefs disj_th)
in
disj_to_ritems prem_only disj_head disj_th
end
else [ritem]
end
fun logic_thm_update ctxt (id, th) =
let
val t = UtilLogic.prop_of' th
in
if UtilLogic.is_obj_all t orelse UtilLogic.is_ball t orelse
UtilLogic.is_neg t andalso UtilLogic.is_ex (UtilLogic.dest_not t) orelse
UtilLogic.is_neg t andalso UtilLogic.is_bex (UtilLogic.dest_not t) orelse
UtilLogic.is_disj t orelse UtilLogic.is_imp t orelse
UtilLogic.is_neg t andalso UtilLogic.is_conj (UtilLogic.dest_not t)
then
let
val (disj_head, disj_th) = analyze_disj_th ctxt th
val raw_items = disj_to_ritems true disj_head disj_th
in
AddItems {id = id, sc = NONE, raw_items = raw_items}
end
else
Update.thm_update (id, th)
end
val add_disj_normalizers =
Normalizer.add_th_normalizer (
"split_conj_gen", split_conj_gen_th
) #> fold Normalizer.add_normalizer [
("eq", eq_normalizer),
("property", property_normalizer),
("disj", disj_normalizer)
]
end