Theory CSP_F_op_alpha_par (Isabelle2008: June 2008)

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |                  April 2005               |
            |                   June 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |               November 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_F_op_alpha_par
imports CSP_F_domain CSP_T_op_alpha_par
begin

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite (notick | t = <>)                  *)
(*                                                                     *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*********************************************************
             Alphabetized Parallel eval
 *********************************************************)

lemma in_failures_Parallel_SKIP_lm1: 
  "[| Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X) ; 
     (Tick ~: Z | Z <= Evset) |]
   ==> Z - Y <= Ev ` X"
by (auto simp add: Evset_def)

lemma in_failures_Parallel_SKIP_lm2: 
  "Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X)  
   ==> Z - insert Tick Y <= Ev ` X"
by (auto)

(* Para SKIP *)

lemma in_failures_Parallel_SKIP:
  "(f :f failures(P |[X]| SKIP) M) = 
   (EX u Y Z. f = (u, Y Un Z) & (u, Y) :f failures(P) M & 
              sett(u) Int (Ev ` X) = {} & Z <= Ev ` X)"
apply (simp add: in_failures)
apply (rule iffI)

(* => *)
 apply (elim conjE exE)
 apply (erule disjE)

 (* t = <> *)
  apply (simp add: par_tr_nil)
  apply (elim conjE, simp)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z - Y" in exI)
  apply (simp add: in_failures_Parallel_SKIP_lm1)

 (* t = <Tick> *)
  apply (simp add: par_tr_Tick)
  apply (elim conjE, simp)
  apply (case_tac "Tick ~: Z")

   apply (rule_tac x="Y" in exI)
   apply (rule_tac x="Z - Y" in exI)
   apply (simp add: in_failures_Parallel_SKIP_lm1)

   (* Tick : Z *)
   apply (rule_tac x="insert Tick Y" in exI)
   apply (rule_tac x="(Z - insert Tick Y)" in exI)
   apply (rule conjI, force)
   apply (simp add: Tick_in_sett)
   apply (erule exE)
   apply (rule conjI)
   apply (simp)
   apply (rule proc_T2_T3)
   apply (simp)
   apply (simp)
   apply (simp add: in_failures_Parallel_SKIP_lm2)

(* <= *)
 apply (elim conjE exE)
 apply (case_tac "Tick ~: sett u")

 (* t = <> *)
  apply (rule_tac x="u" in exI)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z Un (Y - {Tick})" in exI)
  apply (simp)
  apply (rule conjI)
  apply (fast)
  apply (rule conjI)
  apply (fast)
  apply (rule_tac x="u" in exI)
  apply (rule_tac x="<>" in exI)
  apply (simp add: par_tr_nil)
  apply (simp add: Evset_def)
  apply (force)

 (* t = <Tick> *)
  apply (rule_tac x="u" in exI)
  apply (rule_tac x="Y" in exI)
  apply (rule_tac x="Z Un Y" in exI)
  apply (simp)
  apply (rule conjI)
  apply (fast)
  apply (rule conjI)
  apply (fast)
  apply (rule_tac x="u" in exI)
  apply (rule_tac x="<Tick>" in exI)
  apply (simp add: par_tr_Tick)
done

(*** complement ***)

lemma in_failures_Parallel_SKIP_comp:
  "(f :f failures(P |[- X]| SKIP) M) =
   (EX u Y Z. f = (u, Y Un Z) & (u, Y) :f failures(P) M & 
              sett(u) <= insert Tick (Ev ` X) & Z Int insert Tick (Ev ` X) = {})"
apply (simp add: in_failures_Parallel_SKIP)
apply (auto)
apply (rule_tac x="Y" in exI)
apply (rule_tac x="Z" in exI)
apply (simp)
apply (rule conjI)
 apply (rule subsetI)
 apply (case_tac "x : Ev ` (- X)")
 apply (fast)
 apply (simp add: notin_Ev_set)
 apply (erule disjE, simp)
 apply (force)
apply (force)

apply (rule_tac x="Y" in exI)
apply (rule_tac x="Z" in exI)
apply (auto)
apply (case_tac "x = Tick", simp)
apply (simp add: not_Tick_to_Ev)
apply (auto)
done

(*** Alpha_parallel_evalF ***)

lemma in_failures_Alpha_parallel_lm1:
  "[| Tick ~: Za ; Za Int Ev ` X1 = {}; 
      Tick ~: Zb ; Zb Int Ev ` X2 = {};
      Ya Un Za - insert Tick (Ev ` (X1 Int X2)) =
      Yb Un Zb - insert Tick (Ev ` (X1 Int X2)) |]
       ==>
       (Ya Un Za Un (Yb Un Zb)) Int insert Tick (Ev ` (X1 Un X2)) =
         (Ya Int insert Tick (Ev ` X1)) Un
         (Yb Int insert Tick (Ev ` X2))"
by (auto)

lemma in_failures_Alpha_parallel_lm2:
  "X Int insert Tick (Ev ` (X1 Un X2)) <= Y Un Z
   ==> X = X Int Ev ` (X1 - X2) Un X Int Y Int insert Tick (Ev ` (X1 Int X2)) Un
               (X - insert Tick (Ev ` X1)) Un
               (X Int Ev ` (X2 - X1) Un X Int Z Int insert Tick (Ev ` (X1 Int X2)) Un
                (X - insert Tick (Ev ` X2)))"
by (auto)

lemma in_failures_Alpha_parallel_lm3:
  "X Int Ev ` (X1 - X2) Un X Int Y Int insert Tick (Ev ` (X1 Int X2)) Un
           (X - insert Tick (Ev ` X1)) -
           insert Tick (Ev ` (X1 Int X2)) =
           X Int Ev ` (X2 - X1) Un X Int Z Int insert Tick (Ev ` (X1 Int X2)) Un
           (X - insert Tick (Ev ` X2)) -
           insert Tick (Ev ` (X1 Int X2))"
by (auto)

(* F *)

lemma in_failures_Alpha_parallel:
  "(f :f failures(P |[X1,X2]| Q) M) =
   (EX u X.
     f = (u, X) &
     (EX Y Z.
         X Int insert Tick (Ev ` (X1 Un X2)) =
         Y Int insert Tick (Ev ` X1) Un Z Int insert Tick (Ev ` X2) &
         (u rest-tr X1, Y) :f failures(P) M &
         (u rest-tr X2, Z) :f failures(Q) M & 
          sett u <= insert Tick (Ev ` (X1 Un X2))))"
apply (simp add: Alpha_parallel_def)
apply (simp add: in_failures_Parallel[of _ _ "X1 Int X2"])
apply (simp add: in_failures_Parallel_SKIP_comp)
apply (rule iffI)

(* => *)
 apply (elim conjE exE)
 apply (simp add: par_tr_rest_tr)
 apply (rule_tac x="Ya" in exI, simp)
 apply (rule_tac x="Yb" in exI, simp)
 apply (simp add: in_failures_Alpha_parallel_lm1)

(* <= *)
 apply (elim conjE exE)
 apply (simp)
 apply (rule_tac x=
   "(X Int (Ev ` (X1 - X2))) Un 
    (X Int Y Int insert Tick (Ev ` (X1 Int X2))) Un
    (X - insert Tick (Ev ` X1))" in exI)
 apply (rule_tac x=
   "(X Int (Ev ` (X2 - X1))) Un 
    (X Int Z Int insert Tick (Ev ` (X1 Int X2))) Un
    (X - insert Tick (Ev ` X2))" in exI)

(* X = Y' Un Z' *)
  apply (rule conjI)
  apply (rule in_failures_Alpha_parallel_lm2)
  apply (fast)

(* Parallel condition *)
  apply (rule conjI)
  apply (simp add: in_failures_Alpha_parallel_lm3)

(* failures *)
  apply (rule_tac x="u rest-tr X1" in exI)
  apply (rule_tac x="u rest-tr X2" in exI)
  apply (simp add: par_tr_rest_tr_if)

  apply (rule conjI)
   apply (rule_tac x=
     "(X Int (Ev ` (X1 - X2))) Un 
      (X Int Y Int insert Tick (Ev ` (X1 Int X2)))" in exI)
   apply (rule_tac x= "(X - insert Tick (Ev ` X1))" in exI)
   apply (simp)
   apply (rule conjI)
   apply (rule memF_F2)
   apply (simp)
   apply (force)
   apply (force)

   apply (rule_tac x=
     "(X Int (Ev ` (X2 - X1))) Un 
      (X Int Z Int insert Tick (Ev ` (X1 Int X2)))" in exI)
   apply (rule_tac x= "(X - insert Tick (Ev ` X2))" in exI)
   apply (simp)
   apply (rule conjI)
   apply (rule memF_F2)
   apply (simp)
   apply (force)
   apply (force)
done

(*** Semantics for alphabetized parallel on F ***)

lemma failures_Alpha_parallel:
  "failures(P |[X1,X2]| Q) = (%M.
   {f. (EX u X. f = (u, X) &
     (EX Y Z.
         X Int insert Tick (Ev ` (X1 Un X2)) =
         Y Int insert Tick (Ev ` X1) Un Z Int insert Tick (Ev ` X2) &
         (u rest-tr X1, Y) :f failures(P) M &
         (u rest-tr X2, Z) :f failures(Q) M &
          sett u <= insert Tick (Ev ` (X1 Un X2))))}f)"
apply (simp only: in_failures_Alpha_parallel[THEN sym])
apply (simp)
done

(****************** to add it again ******************)

declare disj_not1   [simp]

end

lemma in_failures_Parallel_SKIP_lm1:

  [| Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X); Tick ∉ Z ∨ Z ⊆ Evset |]
  ==> Z - Y ⊆ Ev ` X

lemma in_failures_Parallel_SKIP_lm2:

  Y - insert Tick (Ev ` X) = Z - insert Tick (Ev ` X)
  ==> Z - insert Tick Y ⊆ Ev ` X

lemma in_failures_Parallel_SKIP:

  (f :f failures (P |[X]| SKIP) M) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧ (u, Y) :f failures P M ∧ sett u ∩ Ev ` X = {} ∧ Z ⊆ Ev ` X)

lemma in_failures_Parallel_SKIP_comp:

  (f :f failures (P |[- X]| SKIP) M) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧
      (u, Y) :f failures P M ∧
      sett u ⊆ insert Tick (Ev ` X) ∧ Z ∩ insert Tick (Ev ` X) = {})

lemma in_failures_Alpha_parallel_lm1:

  [| Tick ∉ Za; Za ∩ Ev ` X1.0 = {}; Tick ∉ Zb; Zb ∩ Ev ` X2.0 = {};
     Ya ∪ Za - insert Tick (Ev ` (X1.0 ∩ X2.0)) =
     Yb ∪ Zb - insert Tick (Ev ` (X1.0 ∩ X2.0)) |]
  ==> (Ya ∪ Za ∪ (Yb ∪ Zb)) ∩ insert Tick (Ev ` (X1.0 ∪ X2.0)) =
      Ya ∩ insert Tick (Ev ` X1.0) ∪ Yb ∩ insert Tick (Ev ` X2.0)

lemma in_failures_Alpha_parallel_lm2:

  X ∩ insert Tick (Ev ` (X1.0 ∪ X2.0)) ⊆ Y ∪ Z
  ==> X = X ∩ Ev ` (X1.0 - X2.0) ∪ X ∩ Y ∩ insert Tick (Ev ` (X1.0 ∩ X2.0)) ∪
          (X - insert Tick (Ev ` X1.0)) ∪
          (X ∩ Ev ` (X2.0 - X1.0) ∪ X ∩ Z ∩ insert Tick (Ev ` (X1.0 ∩ X2.0)) ∪
           (X - insert Tick (Ev ` X2.0)))

lemma in_failures_Alpha_parallel_lm3:

  X ∩ Ev ` (X1.0 - X2.0) ∪ X ∩ Y ∩ insert Tick (Ev ` (X1.0 ∩ X2.0)) ∪
  (X - insert Tick (Ev ` X1.0)) -
  insert Tick (Ev ` (X1.0 ∩ X2.0)) =
  X ∩ Ev ` (X2.0 - X1.0) ∪ X ∩ Z ∩ insert Tick (Ev ` (X1.0 ∩ X2.0)) ∪
  (X - insert Tick (Ev ` X2.0)) -
  insert Tick (Ev ` (X1.0 ∩ X2.0))

lemma in_failures_Alpha_parallel:

  (f :f failures (P |[X1.0,X2.0]| Q) M) =
  (∃u X. f = (u, X) ∧
         (∃Y Z. X ∩ insert Tick (Ev ` (X1.0 ∪ X2.0)) =
                Y ∩ insert Tick (Ev ` X1.0) ∪ Z ∩ insert Tick (Ev ` X2.0) ∧
                (u rest-tr X1.0, Y) :f failures P M ∧
                (u rest-tr X2.0, Z) :f failures Q M ∧
                sett u ⊆ insert Tick (Ev ` (X1.0 ∪ X2.0))))

lemma failures_Alpha_parallel:

  failures (P |[X1.0,X2.0]| Q) =
  (λM. Abs_setF
        {(u, X) |u X.
         ∃Y Z. X ∩ insert Tick (Ev ` (X1.0 ∪ X2.0)) =
               Y ∩ insert Tick (Ev ` X1.0) ∪ Z ∩ insert Tick (Ev ` X2.0) ∧
               (u rest-tr X1.0, Y) :f failures P M ∧
               (u rest-tr X2.0, Z) :f failures Q M ∧
               sett u ⊆ insert Tick (Ev ` (X1.0 ∪ X2.0))})