File ‹~~/src/Provers/typedsimp.ML›
signature TSIMP_DATA =
sig
val refl: thm
val sym: thm
val trans: thm
val refl_red: thm
val trans_red: thm
val red_if_equal: thm
val default_rls: thm list
val routine_tac: Proof.context -> thm list -> int -> tactic
end;
signature TSIMP =
sig
val asm_res_tac: Proof.context -> thm list -> int -> tactic
val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic
val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic
val norm_tac: Proof.context -> (thm list * thm list) -> tactic
val process_rules: thm list -> thm list * thm list
val rewrite_res_tac: Proof.context -> int -> tactic
val split_eqn: thm
val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic
val subconv_res_tac: Proof.context -> thm list -> int -> tactic
end;
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =
struct
local open TSimp_data
in
val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym);
val red_trans = Drule.zero_var_indexes (trans RS red_if_equal);
fun simp_rule rl = rl RS trans;
fun resimp_rule rl = rl RS red_trans;
fun subconv_rule rl = rl RS trans_red;
fun add_rule rl (simp_rls, other_rls) =
(simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
handle THM _ => (simp_rls, rl :: other_rls);
fun process_rules rls = fold_rev add_rule rls ([], []);
fun process_rewrites rls =
case process_rules rls of
(simp_rls,[]) => simp_rls
| (_,others) => raise THM
("process_rewrites: Ill-formed rewrite", 0, others);
val simp_rls = process_rewrites default_rls;
val simp_net = Tactic.build_net simp_rls;
fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net;
fun subconv_res_tac ctxt congr_rls =
filt_resolve_from_net_tac ctxt 2 (Tactic.build_net (map subconv_rule congr_rls))
ORELSE' filt_resolve_from_net_tac ctxt 1 (Tactic.build_net [refl, refl_red]);
fun asm_res_tac ctxt asms =
let val (xsimp_rls, xother_rls) = process_rules asms
in routine_tac ctxt xother_rls ORELSE'
filt_resolve_from_net_tac ctxt 2 (Tactic.build_net xsimp_rls)
end;
fun step_tac ctxt (congr_rls, asms) =
asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE'
subconv_res_tac ctxt congr_rls;
fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE'
(resolve_tac ctxt [trans, red_trans] THEN' prove_cond_tac) ORELSE'
subconv_res_tac ctxt congr_rls;
fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg) THEN
TRYALL (resolve_tac ctxt [red_if_equal]);
fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg) THEN
TRYALL (resolve_tac ctxt [red_if_equal]);
end;
end;