utp_rdes_tactics.thy

section \<open> Reactive design tactics \<close>

theory utp_rdes_tactics
  imports utp_rdes_triples
begin

text \<open> Theorems for normalisation \<close>

lemmas rdes_rel_norms = 
  prod.case_eq_if
(*  conj_assoc
  disj_assoc *)
  pred_ba.distrib(3,4)
  seqr_or_distl
  seqr_or_distr
  seq_SUP_distl
  seq_SUP_distr

text \<open> The following tactic can be used to simply and evaluate reactive predicates. \<close>

method rpred_simp = (expr_simp add: rpred usubst closure unrest)

text \<open> Tactic to expand out healthy reactive design predicates into the syntactic triple form. \<close>
  
method rdes_expand uses cls = (insert cls, (erule RD_elim)+)    

text \<open> Tactic to simplify the definition of a reactive design \<close>
  
method rdes_simp uses cls cong simps =
  ((rdes_expand cls: cls)?(* , (simp add: closure)? *), (simp add: rdes_def rdes_rel_norms rdes rpred cls closure alpha frame usubst unrest wp simps del: SEXP_apply cong: cong))

text \<open> Tactic to split a refinement conjecture into three POs \<close>

method rdes_refine_split uses cls cong simps =
  (rdes_simp cls: cls cong: cong simps: simps; rule_tac rdes_tri_refine_intro' srdes_tri_refine_intro')

text \<open> Tactics to split an equality conjecture into three POs \<close>

method rdes_eq_split uses cls cong simps =
  (rdes_simp cls: cls cong: cong simps: simps; (rule_tac rdes_tri_eq_intro srdes_tri_eq_intro))
         
method rdes_eq_split' uses cls cong simps =
  (rdes_simp cls: cls cong: cong simps: simps; (rule_tac rdes_tri_eq_intro' srdes_tri_eq_intro'))

text \<open> Tactic to prove a refinement \<close>
  
method rdes_refine uses cls cong simps =
  (rdes_refine_split cls: cls cong: cong simps: simps; (insert cls; pred_auto))

text \<open> Tactics to prove an equality \<close>

method rdes_eq uses cls cong simps =
  (rdes_eq_split cls: cls cong: cong simps: simps; pred_auto)

method rdes_eq' uses cls cong simps =
  (rdes_eq_split' cls: cls cong: cong simps: simps; pred_auto)

text \<open> Via antisymmetry \<close>

method rdes_eq_anti uses cls cong simps =
  (rdes_simp cls: cls cong: cong simps: simps; (rule_tac antisym; (rule_tac rdes_tri_refine_intro srdes_tri_refine_intro; pred_auto)))

text \<open> Tactic to calculate pre/peri/postconditions from reactive designs \<close>

method rdes_calc = (simp add: rdes rpred closure alpha usubst unrest wp prod.case_eq_if)

text \<open> The following tactic attempts to prove a reactive design refinement by calculation of
  the pre-, peri-, and postconditions and then showing three implications between them using
  rel-blast. \<close>

method rdspl_refine =
  (rule_tac SRD_refine_intro; (simp add: closure rdes unrest usubst ; (pred_auto, blast)?))

text \<open> The following tactic combines antisymmetry with the previous tactic to prove an equality. \<close>

method rdspl_eq =
  (rule_tac antisym, rdes_refine, rdes_refine)  

end