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, b⦇ok := True⦈)) ∨ (P(a, b⦇ok := False⦈)))"
apply (case_tac "ok b", auto)
apply (rule_tac t="b⦇ok := True⦈" and s="b" in ssubst, simp_all)
by (subgoal_tac "b = b⦇ok := False⦈", simp_all)

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

lemma CSP2_ok_b: 
"(P(a, b⦇ok:=True⦈) ∨ P(a, b⦇ok:=False⦈)) ⟹ (CSP2 P)(a, b⦇ok:=True⦈)"
by (auto simp: csp_defs design_defs rp_defs)

lemma CSP2_ok: 
"(CSP2 P)(a, b⦇ok:=True⦈) = (P(a, b⦇ok:=True⦈) ∨ P(a, b⦇ok:=False⦈))"
apply (rule iffI)
apply (simp add: CSP2_ok_a)
by (simp add: CSP2_ok_b)

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

lemma CSP2_notok_b: "P(a, b⦇ok:=False⦈) ⟹ (CSP2 P)(a, b⦇ok:=False⦈)"
by (auto simp: csp_defs design_defs rp_defs)

lemma CSP2_notok: "(CSP2 P)(a, b⦇ok:=False⦈) = P(a, b⦇ok:=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, b⦇ok:=False⦈)) ∨ 
          ((CSP2 (R (r ⊢ p)))(a, b⦇ok:=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="ba⦇tr := 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 ⇧f⇩f) ⊢ (P ⇧t⇩f)))
                        = (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 "a⦇tr := [], wait := False⦈ = a⦇tr := []⦈", auto)
apply (subgoal_tac "a⦇tr := [], wait := False⦈ = a⦇tr := []⦈", auto)
apply (subgoal_tac "a⦇tr := [], wait := False⦈ = a⦇tr := []⦈", auto)
apply (subgoal_tac "a⦇tr := [], wait := False⦈ = a⦇tr := []⦈", auto)
apply (subgoal_tac "a⦇tr := [], wait := False⦈ = a⦇tr := []⦈", auto)
apply (rule_tac t="a⦇tr := [], wait := False⦈" and s="a⦇tr := []⦈" 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 "b⦇tr := zs, ok := False⦈ = ba⦇ok := False⦈", auto intro: alpha_d.equality)
apply (subgoal_tac "b⦇tr := zs, ok := False⦈ = ba⦇ok := False⦈", auto intro: alpha_d.equality)
apply (subgoal_tac "b⦇tr := zs, ok := False⦈ = ba⦇ok := False⦈", auto intro: alpha_d.equality)
apply (subgoal_tac "b⦇tr := zs, ok := True⦈ = ba⦇ok := True⦈", auto intro: alpha_d.equality)
apply (subgoal_tac "b⦇tr := zs, ok := True⦈ = ba⦇ok := 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="ba⦇ok := 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="ba⦇ok := 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="ba⦇ok := True⦈" and s=ba in subst, auto)
apply (erule notE) back
apply (rule_tac b="ba" in comp_intro, auto)
apply (rule_tac t="ba⦇ok := 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, b⦇ok := True⦈) ⟶ r (a, b⦇ok := 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, b⦇ok := True⦈) ⟶ r (a, b⦇ok := 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 ⇧f⇩f) ⊢ (P ⇧t⇩f)))"
  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