File ‹UNITY_tactics.ML›
fun Always_Int_tac ctxt =
dresolve_tac ctxt @{thms Always_Int_I} THEN'
assume_tac ctxt THEN'
eresolve_tac ctxt @{thms Always_thin}
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
fun constrains_tac ctxt i =
SELECT_GOAL
(EVERY
[REPEAT (Always_Int_tac ctxt 1),
REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1
ORELSE
resolve_tac ctxt [@{thm StableI}, @{thm stableI},
@{thm constrains_imp_Constrains}] 1),
simp_tac (put_simpset HOL_ss ctxt
addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
resolve_tac ctxt @{thms constrainsI} 1,
full_simp_tac ctxt 1,
REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])),
ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_full_simp_tac ctxt)]) i;
fun ensures_tac ctxt sact =
SELECT_GOAL
(EVERY
[REPEAT (Always_Int_tac ctxt 1),
eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
ORELSE
REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
Rule_Insts.res_inst_tac ctxt
[((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
ORELSE Rule_Insts.res_inst_tac ctxt
[((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
constrains_tac ctxt 1,
ALLGOALS (clarify_tac ctxt),
ALLGOALS (asm_lr_simp_tac ctxt)]);
fun make_o_equivs ctxt th =
[th,
th RS @{thm o_equiv_assoc} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_assoc}]),
th RS @{thm o_equiv_apply} |> simplify (put_simpset HOL_ss ctxt addsimps [@{thm o_def}, @{thm sub_def}])];