File ‹Transform_Tactic.ML›
signature TRANSFORM_TACTIC =
sig
val my_print_tac: string -> tactic
val totality_resolve_tac: thm -> thm -> thm -> Proof.context -> tactic
val totality_replay_tac: Function.info -> Function.info -> Proof.context -> tactic
val solve_relator_tac: Proof.context -> int -> tactic
val transfer_raw_tac: Proof.context -> int -> tactic
val step_tac: Proof.context -> Transform_Data.cmd_info -> int -> tactic
val prepare_case_tac: Proof.context -> Transform_Data.cmd_info -> int -> tactic
val prepare_consistentDP_tac: Proof.context -> Transform_Data.cmd_info -> int -> tactic
val solve_consistentDP_tac: Proof.context -> Transform_Data.cmd_info -> int -> tactic
val prepare_combinator_tac: Proof.context -> Transform_Data.cmd_info -> int -> tactic
val dp_unfold_defs_tac: Proof.context -> Transform_Data.cmd_info -> int -> tactic
end
structure Transform_Tactic : TRANSFORM_TACTIC =
struct
fun my_print_tac msg st = (tracing msg; all_tac st)
fun totality_resolve_tac totality0 def0 def1 ctxt =
let
val totality0_unfolded = totality0 |> Local_Defs.unfold ctxt [def0]
val totality1 = totality0_unfolded |> Local_Defs.fold ctxt [def1]
in
if Thm.full_prop_of totality0_unfolded aconv Thm.full_prop_of totality1
then
let
val msg = Pretty.string_of (Pretty.block [
Pretty.str "Failed to transform totality from", Pretty.brk 1,
Pretty.quote (Syntax.pretty_term ctxt (Thm.full_prop_of def0)), Pretty.brk 1,
Pretty.str "to", Pretty.brk 1,
Pretty.quote (Syntax.pretty_term ctxt (Thm.full_prop_of def1)), Pretty.brk 1])
in no_tac end
else HEADGOAL (resolve_tac ctxt [totality1])
end
fun totality_blast_tac totality0 def0 def1 ctxt =
HEADGOAL (
(resolve_tac ctxt [totality0 RS @{thm rev_iffD1}])
THEN' (resolve_tac ctxt [@{thm arg_cong[where f=HOL.All]}])
THEN' SELECT_GOAL (unfold_tac ctxt (map (Local_Defs.abs_def_rule ctxt) [def0, def1]))
THEN' (resolve_tac ctxt [@{thm arg_cong[where f=Wellfounded.accp]}])
THEN' (Blast.depth_tac ctxt 2)
)
fun totality_replay_tac old_info new_info ctxt =
let
val totality0 = Transform_Misc.totality_of old_info
val def0 = Transform_Misc.rel_of old_info ctxt
val def1 = Transform_Misc.rel_of new_info ctxt
fun my_print_tac msg st = (tracing msg; all_tac st)
in
no_tac
ORELSE (totality_resolve_tac totality0 def0 def1 ctxt
THEN my_print_tac "termination by replaying")
ORELSE (totality_blast_tac totality0 def0 def1 ctxt
THEN my_print_tac "termination by blast")
end
fun dp_intro_tac ctxt (cmd_info: Transform_Data.cmd_info) =
let
val scope_name = Binding.name_of (#scope cmd_info)
val consistentDP_rule = Transform_Misc.locale_thms ctxt scope_name "consistentDP_intro"
in
resolve_tac ctxt consistentDP_rule
end
fun expand_relator_tac ctxt =
SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt))
fun solve_relator_tac ctxt =
SOLVED' (Transfer.eq_tac ctxt)
fun split_params_tac ctxt =
clarify_tac ctxt
fun dp_induct_tac ctxt (cmd_info: Transform_Data.cmd_info) =
let
val dpT' = cmd_info |> #dp_info |> the |> #new_head'
val dpT'_info = Function.get_info ctxt dpT'
val induct_rule = dpT'_info |> #inducts |> the
in
resolve_tac ctxt induct_rule
end
fun dp_unfold_def_tac ctxt (cmd_info: Transform_Data.cmd_info) sel =
cmd_info |> #dp_info |> the |> sel
|> map (Local_Defs.meta_rewrite_rule ctxt)
|> Conv.rewrs_conv
|> Conv.try_conv
|> Conv.binop_conv
|> HOLogic.Trueprop_conv
|> Conv.concl_conv ~1
|> (fn cv => Conv.params_conv ~1 (K cv) ctxt)
|> CONVERSION
fun dp_match_rule_tac ctxt (cmd_info: Transform_Data.cmd_info) =
let
val scope_name = Binding.name_of (#scope cmd_info)
val dp_match_rules = Transform_Misc.locale_thms ctxt scope_name "dp_match_rule"
in
resolve_tac ctxt dp_match_rules
end
fun checkmem_tac ctxt (cmd_info: Transform_Data.cmd_info) =
let
val scope_name = Binding.name_of (#scope cmd_info)
val dp_match_rules = Transform_Misc.locale_thms ctxt scope_name "crel_vs_checkmem_tupled"
in
resolve_tac ctxt dp_match_rules
THEN' SOLVED' (clarify_tac ctxt)
THEN' Transfer.eq_tac ctxt
end
fun solve_IH_tac ctxt =
Method.assm_tac ctxt
fun transfer_raw_tac ctxt =
resolve_tac ctxt (Transfer.get_transfer_raw ctxt)
fun step_tac ctxt (cmd_info: Transform_Data.cmd_info) =
solve_IH_tac ctxt
ORELSE' solve_relator_tac ctxt
ORELSE' dp_match_rule_tac ctxt cmd_info
ORELSE' transfer_raw_tac ctxt
fun prepare_case_tac ctxt (cmd_info: Transform_Data.cmd_info) =
dp_unfold_def_tac ctxt cmd_info #new_def'
THEN' checkmem_tac ctxt cmd_info
THEN' dp_unfold_def_tac ctxt cmd_info #old_defs
fun solve_case_tac ctxt (cmd_info: Transform_Data.cmd_info) =
prepare_case_tac ctxt cmd_info
THEN' REPEAT_ALL_NEW (step_tac ctxt cmd_info)
fun prepare_consistentDP_tac ctxt (cmd_info: Transform_Data.cmd_info) =
dp_intro_tac ctxt cmd_info
THEN' expand_relator_tac ctxt
THEN' split_params_tac ctxt
THEN' dp_induct_tac ctxt cmd_info
fun solve_consistentDP_tac ctxt (cmd_info: Transform_Data.cmd_info) =
prepare_consistentDP_tac ctxt cmd_info
THEN_ALL_NEW SOLVED' (solve_case_tac ctxt cmd_info)
fun prepare_combinator_tac ctxt (cmd_info: Transform_Data.cmd_info) =
EqSubst.eqsubst_tac ctxt [0] @{thms Rel_def[symmetric]}
THEN' dp_unfold_def_tac ctxt cmd_info (single o #new_defT)
THEN' REPEAT_ALL_NEW (resolve_tac ctxt (@{thm Rel_abs} :: Transform_Misc.locale_thms ctxt "local" "crel_vs_return_ext"))
THEN' (SELECT_GOAL (unfold_tac ctxt @{thms Rel_def}))
fun dp_unfold_defs_tac ctxt (cmd_info: Transform_Data.cmd_info) =
dp_unfold_def_tac ctxt cmd_info #new_def'
THEN' dp_unfold_def_tac ctxt cmd_info #old_defs
end