Theory CSP_Processes

section ‹CSP processes›

theory CSP_Processes
imports Reactive_Processes
begin

text ‹A CSP process is a UTP reactive process that satisfies two additional
healthiness conditions called $CSP1$ and $CSP2$. A reactive process that satisfies 
$CSP1$ and $CSP2$ is said to be CSP healthy.›

subsection ‹Definitions›

text ‹We introduce here the definitions of the CSP healthiness conditions.›

definition CSP1::"((,) alphabet_rp) Healthiness_condition"
where "CSP1 (P)    P  (λ(A, A'). ¬ok A  tr A  tr A')"

definition J_csp
where "J_csp    λ(A, A'). (ok A  ok A')  tr A = tr A'  wait A = wait A' 
                                                      ref A = ref A'  more A = more A'"

definition CSP2::"((,) alphabet_rp) Healthiness_condition"
where "CSP2 (P)    P ;; J_csp"

definition is_CSP_process::"(,) relation_rp  bool" where
"is_CSP_process P  P is CSP1 healthy  P is CSP2 healthy  P is R healthy"

lemmas csp_defs = CSP1_def J_csp_def CSP2_def is_CSP_process_def

lemma is_CSP_processE1 [elim?]:
  assumes "is_CSP_process P"
  obtains "P is CSP1 healthy" "P is CSP2 healthy" "P is R healthy"
  using assms unfolding is_CSP_process_def by simp

lemma is_CSP_processE2 [elim?]:
  assumes "is_CSP_process P"
  obtains "CSP1 P = P" "CSP2 P = P" "R P = P"
  using assms unfolding is_CSP_process_def by (simp add: Healthy_def')


subsection ‹Proofs›

text ‹Theorems and lemmas relative to CSP processes are introduced here.›

lemma CSP1_CSP2_commute: "CSP1 o CSP2 = CSP2 o CSP1"
by (auto simp: csp_defs fun_eq_iff)

lemma CSP2_is_H2: "H2 = CSP2"
apply (clarsimp simp add: csp_defs design_defs rp_defs fun_eq_iff)
apply (rule iffI)
apply (erule_tac [!] comp_elim)
apply (rule_tac [!] b=ba in comp_intro)
apply (auto elim!: alpha_d_more_eqE intro!: alpha_d_more_eqI)
done

lemma H2_CSP1_commute: "H2 o CSP1 = CSP1 o H2" 
apply (subst CSP2_is_H2[simplified Healthy_def])+
apply (rule CSP1_CSP2_commute[symmetric])
done

lemma H2_CSP1_commute2: "H2 (CSP1 P) = CSP1 (H2 P)" 
by (simp add: H2_CSP1_commute[simplified Fun.comp_def fun_eq_iff, rule_format] fun_eq_iff)

lemma CSP1_R_commute:
  "CSP1 (R P) = R (CSP1 P)"
by (auto simp: csp_defs rp_defs fun_eq_iff prefix_def split: cond_splits)

lemma CSP2_R_commute:
  "CSP2 (R P) = R (CSP2 P)"
apply (subst CSP2_is_H2[symmetric])+
apply (rule R_H2_commute2[symmetric])
done

lemma CSP1_idem: "CSP1 = CSP1 o CSP1"
by (auto simp: csp_defs fun_eq_iff)

lemma CSP2_idem: "CSP2 = CSP2 o CSP2"
by (auto simp: csp_defs fun_eq_iff)

lemma CSP_is_CSP1:
  assumes A: "is_CSP_process P"
  shows "P is CSP1 healthy"
using A by (auto simp: is_CSP_process_def design_defs)

lemma CSP_is_CSP2:
  assumes A: "is_CSP_process P"
  shows "P is CSP2 healthy"
using A by (simp add: design_defs prefix_def is_CSP_process_def)

lemma CSP_is_R:
  assumes A: "is_CSP_process P"
  shows "P is R healthy"
using A by (simp add: design_defs prefix_def is_CSP_process_def)

lemma t_or_f_a: "P(a, b)  ((P(a, bok := True))  (P(a, bok := False)))"
apply (case_tac "ok b", auto)
apply (rule_tac t="bok := True" and s="b" in ssubst, simp_all)
by (subgoal_tac "b = bok := False", simp_all)

lemma CSP2_ok_a: 
"(CSP2 P)(a, bok:=True)  (P(a, bok:=True)  P(a, bok:=False))"
apply (clarsimp simp: csp_defs design_defs rp_defs split: cond_splits elim: prefixE)
apply (case_tac "ok ba")
apply (rule_tac t="bok := True" and s="ba" in ssubst, simp_all)
apply (drule_tac b="bok := False" and a="ba" in back_subst)
apply (auto intro: alpha_rp.equality)
done

lemma CSP2_ok_b: 
"(P(a, bok:=True)  P(a, bok:=False))  (CSP2 P)(a, bok:=True)"
by (auto simp: csp_defs design_defs rp_defs)

lemma CSP2_ok: 
"(CSP2 P)(a, bok:=True) = (P(a, bok:=True)  P(a, bok:=False))"
apply (rule iffI)
apply (simp add: CSP2_ok_a)
by (simp add: CSP2_ok_b)

lemma CSP2_notok_a: "(CSP2 P)(a, bok:=False)  P(a, bok:=False)"
apply (clarsimp simp: csp_defs design_defs rp_defs)
apply (case_tac "ok ba")
apply (rule_tac t="bok := True" and s="ba" in ssubst, simp_all)
apply (drule_tac b="bok := False" and a="ba" in back_subst)
apply (auto intro: alpha_rp.equality)
done

lemma CSP2_notok_b: "P(a, bok:=False)  (CSP2 P)(a, bok:=False)"
by (auto simp: csp_defs design_defs rp_defs)

lemma CSP2_notok: "(CSP2 P)(a, bok:=False) = P(a, bok:=False)"
apply (rule iffI)
apply (simp add: CSP2_notok_a)
by (simp add: CSP2_notok_b)

lemma CSP2_t_f: 
  assumes A:"(CSP2 (R (r  p)))(a, b)"
  and B: "((CSP2 (R (r  p)))(a, bok:=False))  
          ((CSP2 (R (r  p)))(a, bok:=True))  Q"
  shows "Q"
apply (rule B)
apply (rule disjI2)
apply (insert A)
apply (auto simp add: csp_defs design_defs rp_defs)
done

lemma disj_CSP1:
  assumes "P is CSP1 healthy"
    and "Q is CSP1 healthy"
  shows "(P  Q) is CSP1 healthy"
using assms by (auto simp: csp_defs design_defs rp_defs fun_eq_iff)

lemma disj_CSP2:
  "P is CSP2 healthy ==> Q is CSP2 healthy ==> (P  Q) is CSP2 healthy"
  by (simp add: CSP2_is_H2[symmetric] Healthy_def' design_defs comp_ndet_l_distr)

lemma disj_CSP:
  assumes A: "is_CSP_process P"
  assumes B: "is_CSP_process Q"
  shows "is_CSP_process (P  Q)"
apply (simp add: is_CSP_process_def Healthy_def)
apply (subst disj_CSP2[simplified Healthy_def, symmetric])
apply (rule A[THEN CSP_is_CSP2, simplified Healthy_def])
apply (rule B[THEN CSP_is_CSP2, simplified Healthy_def], simp)
apply (subst disj_CSP1[simplified Healthy_def, symmetric])
apply (rule A[THEN CSP_is_CSP1, simplified Healthy_def])
apply (rule B[THEN CSP_is_CSP1, simplified Healthy_def], simp)
apply (subst R_disj[simplified Healthy_def])
apply (rule A[THEN CSP_is_R, simplified Healthy_def])
apply (rule B[THEN CSP_is_R, simplified Healthy_def], simp)
done

lemma seq_CSP1:
  assumes A: "P is CSP1 healthy"
  assumes B: "Q is CSP1 healthy"
  shows "(P ;; Q) is CSP1 healthy"
using A B by (auto simp: csp_defs design_defs rp_defs fun_eq_iff)

lemma seq_CSP2:
  assumes A: "Q is CSP2 healthy"
  shows "(P ;; Q) is CSP2 healthy"
using A
by (auto simp: CSP2_is_H2[symmetric] H2_J[symmetric])

lemma seq_R:
  assumes "P is R healthy"
  and "Q is R healthy"
  shows "(P ;; Q) is R healthy"
proof -
  have "R P = P" and "R Q = Q"
    using assms by (simp_all only: Healthy_def)
  moreover
  have "(R P ;; R Q) is R healthy"
    apply (auto simp add: design_defs rp_defs prefix_def fun_eq_iff split: cond_splits)
           apply (rule_tac b=a in comp_intro, auto split: cond_splits)
       apply (rule_tac x="zs" in exI, auto split: cond_splits)
      apply (rule_tac b="batr := tr a @ tr ba" in comp_intro, auto split: cond_splits)+
    done
  ultimately show ?thesis by simp
qed


lemma seq_CSP:
  assumes A: "P is CSP1 healthy"
  and B: "P is R healthy"
  and C: "is_CSP_process Q"
  shows "is_CSP_process (P ;; Q)"
apply (auto simp add: is_CSP_process_def)
apply (subst seq_CSP1[simplified Healthy_def])
apply (rule A[simplified Healthy_def])
apply (rule CSP_is_CSP1[OF C, simplified Healthy_def])
apply (simp add: Healthy_def, subst CSP1_idem, auto)
apply (subst seq_CSP2[simplified Healthy_def])
apply (rule CSP_is_CSP2[OF C, simplified Healthy_def])
apply (simp add: Healthy_def, subst CSP2_idem, auto)
apply (subst seq_R[simplified Healthy_def])
apply (rule B[simplified Healthy_def])
apply (rule CSP_is_R[OF C, simplified Healthy_def])
apply (simp add: Healthy_def, subst R_idem2, auto)
done

lemma rd_ind_wait: "(R(¬(P ff)  (P tf)))
                        = (R((¬(λ (A, A'). P (A, A'ok := False))) 
                                   (λ (A, A'). P (A, A'ok := True))))"
apply (auto simp: design_defs rp_defs fun_eq_iff split: cond_splits)
apply (subgoal_tac "atr := [], wait := False = atr := []", auto)
apply (subgoal_tac "atr := [], wait := False = atr := []", auto)
apply (subgoal_tac "atr := [], wait := False = atr := []", auto)
apply (subgoal_tac "atr := [], wait := False = atr := []", auto)
apply (subgoal_tac "atr := [], wait := False = atr := []", auto)
apply (rule_tac t="atr := [], wait := False" and s="atr := []" in subst, simp_all)
done

lemma rd_H1: "(R((¬(λ (A, A'). P (A, A'ok := False))) 
                               (λ (A, A'). P (A, A'ok := True)))) = 
                      (R ((¬ H1 (λ (A, A'). P (A, A'ok := False))) 
                               H1 (λ (A, A'). P (A, A'ok := True))))"
by (auto simp: design_defs rp_defs fun_eq_iff split: cond_splits)

lemma rd_H1_H2: "(R((¬ H1 (λ (A, A'). P (A, A'ok := False))) 
                                   H1 (λ (A, A'). P (A, A'ok := True)))) = 
                        (R((¬(H1 o H2) (λ (A, A'). P (A, A'ok := False))) 
                                   (H1 o H2) (λ (A, A'). P (A, A'ok := True))))"
apply (auto simp: design_defs rp_defs prefix_def fun_eq_iff split: cond_splits elim: alpha_d_more_eqE)
apply (subgoal_tac "btr := zs, ok := False = baok := False", auto intro: alpha_d.equality)
apply (subgoal_tac "btr := zs, ok := False = baok := False", auto intro: alpha_d.equality)
apply (subgoal_tac "btr := zs, ok := False = baok := False", auto intro: alpha_d.equality)
apply (subgoal_tac "btr := zs, ok := True = baok := True", auto intro: alpha_d.equality)
apply (subgoal_tac "btr := zs, ok := True = baok := True", auto intro: alpha_d.equality)
done

lemma rd_H1_H2_R_H1_H2:
   "(R ((¬ (H1 o H2) (λ (A, A'). P (A, A'ok := False))) 
             (H1 o H2) (λ (A, A'). P (A, A'ok := True)))) = 
    (R o H1 o H2) P"
apply (auto simp: design_defs rp_defs fun_eq_iff split: cond_splits)
apply (erule notE) back back
apply (rule_tac b="ba" in comp_intro, auto)
apply (rule_tac t="baok := False" and s=ba in subst, auto intro: alpha_d.equality)
apply (erule notE) back back
apply (rule_tac b="ba" in comp_intro, auto)
apply (rule_tac t="baok := False" and s=ba in subst, auto intro: alpha_d.equality)
apply (case_tac "ok ba")
apply (rule_tac b="ba" in comp_intro, auto)
apply (rule_tac t="baok := True" and s=ba in subst, auto)
apply (erule notE) back
apply (rule_tac b="ba" in comp_intro, auto)
apply (rule_tac t="baok := False" and s=ba in subst, auto intro: alpha_d.equality)
done

lemma CSP1_is_R1_H1:
  assumes "P is R1 healthy"
  shows "CSP1 P = R1 (H1 P)"
using assms
by (auto simp: csp_defs design_defs rp_defs fun_eq_iff split: cond_splits)

lemma CSP1_is_R1_H1_2: "CSP1 (R1 P) = R1 (H1 P)"
by (auto simp: csp_defs design_defs rp_defs fun_eq_iff split: cond_splits)

lemma CSP1_R1_commute: "CSP1 o R1 = R1 o CSP1"
by (auto simp: csp_defs design_defs rp_defs fun_eq_iff split: cond_splits)

lemma CSP1_R1_commute2: "CSP1 (R1 P) = R1 (CSP1 P)"
by (auto simp: csp_defs design_defs rp_defs fun_eq_iff split: cond_splits)

lemma CSP1_is_R1_H1_b: 
"(P = (R  R1  H1  H2) P) = (P = (R  CSP1  H2) P)"
apply (simp add: fun_eq_iff)
apply (subst H1_H2_commute2)
apply (subst R1_H2_commute2)
apply (subst CSP1_is_R1_H1_2[symmetric])
apply (subst H2_CSP1_commute2)
apply (subst R1_H2_commute2[symmetric])
apply (subst CSP1_R1_commute2)
apply (subst R_abs_R1[simplified Fun.comp_def fun_eq_iff])
apply (auto)
done

lemma CSP1_join: 
  assumes A: "x is CSP1 healthy"
  and B: "y is CSP1 healthy"
  shows "(x  y) is CSP1 healthy"
  using A B
  by (simp add: Healthy_def CSP1_def fun_eq_iff utp_defs)

lemma CSP2_join:
  assumes A: "x is CSP2 healthy"
  and B: "y is CSP2 healthy"
  shows "(x  y) is CSP2 healthy"
  using A B
  apply (simp add: design_defs csp_defs fun_eq_iff)
  apply (rule allI)
  apply (rule allI)
  apply (erule_tac x="a" in allE)
  apply (erule_tac x="a" in allE)
  apply (erule_tac x="b" in allE)+
  by (auto)

lemma CSP1_meet:
  assumes A: "x is CSP1 healthy"
  and B: "y is CSP1 healthy"
  shows "(x  y) is CSP1 healthy"
  using A B
  apply (simp add: Healthy_def CSP1_def fun_eq_iff utp_defs)
  apply (rule allI)
  apply (rule allI)
  apply (erule_tac x="a" in allE)
  apply (erule_tac x="a" in allE)
  apply (erule_tac x="b" in allE)+
  by (auto)

lemma CSP2_meet:
  assumes A: "x is CSP2 healthy"
  and B: "y is CSP2 healthy"
  shows "(x  y) is CSP2 healthy"
  using A B
  apply (simp add: Healthy_def CSP2_def fun_eq_iff)
  apply (rule allI)+
  apply (erule_tac x="a" in allE)
  apply (erule_tac x="a" in allE)
  apply (erule_tac x="b" in allE)+
  apply (auto)
  apply (rule_tac b="ca" in comp_intro)
  apply (auto simp: J_csp_def)
done

lemma CSP_join: 
  assumes A: "is_CSP_process x"
  and B: "is_CSP_process y"
  shows "is_CSP_process (x  y)"
  using A B
by (simp add: is_CSP_process_def CSP1_join CSP2_join R_join)

lemma CSP_meet:
  assumes A: "is_CSP_process x"
  and B: "is_CSP_process y"
  shows "is_CSP_process (x  y)"
  using A B
by (simp add: is_CSP_process_def CSP1_meet CSP2_meet R_meet)

subsection ‹CSP processes and reactive designs›

text ‹In this section, we prove the relation between CSP processes and reactive designs.›

lemma rd_is_CSP1: "(R (r  p)) is CSP1 healthy"
by (auto simp: csp_defs design_defs rp_defs fun_eq_iff split: cond_splits elim: prefixE)

lemma rd_is_CSP2:
  assumes A: " a b. r (a, bok := True)  r (a, bok := False)"
  shows "(R (r  p)) is CSP2 healthy"
apply (subst CSP2_is_H2[symmetric]) 
apply (simp add: Healthy_def)
apply (subst R_H2_commute2[symmetric])
apply (subst design_H2[simplified Healthy_def], auto simp: A)
done

lemma rd_is_CSP:
  assumes A: " a b. r (a, bok := True)  r (a, bok := False)"
  shows "is_CSP_process (R (r  p))"
apply (simp add: is_CSP_process_def Healthy_def fun_eq_iff)
apply (subst R_idem2)
apply (subst rd_is_CSP2[simplified Healthy_def, symmetric], rule A)
apply (subst rd_is_CSP1[simplified Healthy_def, symmetric], simp)
done

lemma CSP_is_rd:
  assumes A: "is_CSP_process P"
  shows "P = (R (¬(P ff)  (P tf)))"
  apply (subst rd_ind_wait)
  apply (subst rd_H1)
  apply (subst rd_H1_H2)
  apply (subst rd_H1_H2_R_H1_H2)
  apply (subst R_abs_R1[symmetric])
  apply (subst CSP1_is_R1_H1_b)
  apply (subst CSP2_is_H2)
  apply (simp)
  apply (subst CSP_is_CSP2[OF A, simplified Healthy_def, symmetric])
  apply (subst CSP_is_CSP1[OF A, simplified Healthy_def, symmetric])
  apply (subst CSP_is_R[OF A, simplified Healthy_def, symmetric], simp)
done


end