Theory CSP_T_op_rep_par (Isabelle2005: October 2005)

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

theory CSP_T_op_rep_par = CSP_T_op_alpha_par:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  Union (B ` A) = (UN x:A. B x)                      *)
(*                  Inter (B ` A) = (INT x:A. B x)                     *)

declare Union_image_eq [simp del]
declare Inter_image_eq [simp del]

(*  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]

(*============================================================*
 |                                                            |
 |            replicated alphabetized parallel                |
 |                                                            |
 *============================================================*)

(*** traces Inductive_parallel ***)

lemma in_traces_Inductive_parallel_lm1: 
  "(P, X) : set PXs ==> X <= Union (snd ` (set PXs))"
by (auto)

(* main *)

lemma in_traces_Inductive_parallel_lm:
  "PXs ~= [] --> (ALL u.
    (u :t traces ([||] PXs)) =
     (sett(u) <= insert Tick (Ev ` (Union (snd ` (set PXs)))) & 
      (ALL P X. (P,X):(set PXs) --> (u rest-tr X) :t traces P)))"
apply (induct_tac PXs)

(* case 0 *)
 apply (simp)

(* case 1 *)
 apply (case_tac "list = []")
 apply (simp)
 apply (intro allI)
 apply (simp add: in_traces_Alpha_parallel in_traces)
 apply (simp add: pair_eq_decompo)
 apply (simp add: rest_tr_empty)
 apply (rule iffI)
 (* => *)
  apply (simp)
 (* <= *)
  apply (simp)

(* step case *)
apply (simp add: in_traces_Alpha_parallel)
apply (intro allI impI)
apply (rule iffI)

(* => *)
 apply (simp)
 apply (intro allI)
 apply (rule conjI)

  apply (intro impI)
  apply (simp add: pair_eq_decompo)

  apply (intro impI)
  apply (elim conjE)
  apply (drule_tac x="P" in spec)
  apply (drule_tac x="X" in spec)
  apply (subgoal_tac "X <= Union (snd ` set list)")
  apply (simp add: rest_tr_of_rest_tr_subset)
  apply (simp add: in_traces_Inductive_parallel_lm1)

(* <= *)
 apply (simp add: rest_tr_sett_subseteq_sett)
 apply (intro allI impI)
 apply (elim conjE)
 apply (drule_tac x="P" in spec)
 apply (drule_tac x="X" in spec)
 apply (subgoal_tac "X <= Union (snd ` set list)")
 apply (simp add: rest_tr_of_rest_tr_subset)
 apply (simp add: in_traces_Inductive_parallel_lm1)
done

(*** remove ALL ***)

lemma in_traces_Inductive_parallel:
  "PXs ~= [] 
   ==> (u :t traces ([||] PXs)) =
       (sett(u) <= insert Tick (Ev ` (Union (snd ` (set PXs)))) & 
        (ALL P X. (P,X):(set PXs) --> (u rest-tr X) :t traces P))"
by (simp add: in_traces_Inductive_parallel_lm)

(*** Semantics for replicated alphabetized parallel on T ***)

lemma traces_Inductive_parallel:
  "PXs ~= []
   ==> traces ([||] PXs) =
       {u. sett(u) <= insert Tick (Ev ` (Union (snd ` (set PXs)))) & 
        (ALL P X. (P,X):(set PXs) --> (u rest-tr X) :t traces P)}t"
apply (simp add: in_traces_Inductive_parallel[THEN sym])
done

(************************************
 |              traces              |
 ************************************)

lemma sett_in_traces_Inductive_parallel:
  "[| PXs ~= [] ; t :t traces ([||] PXs) |] 
   ==> sett t <= insert Tick (Ev ` Union (snd ` set PXs))"
by (simp add: in_traces_Inductive_parallel)

(*---------------------------------------------------------*
 |        another expression of Inductive_parallel_eval          |
 *---------------------------------------------------------*)

lemma in_traces_Inductive_parallel_nth:
  "PXs ~= [] 
   ==> (u :t traces ([||] PXs)) =
       (sett(u) <= insert Tick (Ev ` (Union (snd ` (set PXs)))) & 
        (ALL i. i < length PXs --> (u rest-tr (snd (PXs!i))) :t traces (fst (PXs!i))))"
apply (simp add: in_traces_Inductive_parallel)
apply (simp add: set_nth)
apply (simp add: pair_eq_decompo)
by (auto)

(*============================================================*
 |                                                            |
 |              indexed alphabetized parallel                 |
 |                                                            |
 *============================================================*)

(*** index_style ***)

lemma to_index_style_T:
   "(ALL P X. (P,X):(PXf ` I) --> (u rest-tr X) :t traces P)
  = (ALL i:I. u rest-tr (snd (PXf i)) :t traces (fst (PXf i)))"
apply (auto)
apply (simp add: pair_eq_decompo)
done

(*** in_traces_Rep_parallel (pre) ***)

lemma in_traces_Rep_parallel_pre:
  "[| I ~= {} ; finite I |]
   ==> (u :t traces ([||]:I PXf)) =
       (sett(u) <= insert Tick (Ev ` (Union (snd ` PXf ` I))) & 
        (ALL P X. (P,X):PXf ` I --> (u rest-tr X) :t traces P))"
apply (simp add: Rep_parallel_def)
apply (subgoal_tac "EX Is. Is isListOf I")
apply (elim conjE exE)
apply (subgoal_tac "(map PXf (SOME Is. Is isListOf I)) ~= []")
apply (simp add: in_traces in_traces_Inductive_parallel)
apply (rule someI2)
 apply (simp)
 apply (simp add: isListOf_set_eq)

apply (rule someI2)
 apply (simp)
 apply (simp add: isListOf_nonemptyset)

apply (simp add: isListOf_EX)
done

(*** in_traces_Rep_parallel ***)

lemma in_traces_Rep_parallel:
  "[| I ~= {} ; finite I |]
   ==> (u :t traces ([||]:I PXf)) =
       (sett(u) <= insert Tick (Ev ` (Union (snd ` PXf ` I))) & 
        (ALL i:I. (u rest-tr (snd (PXf i))) :t traces (fst (PXf i))))"
apply (simp add: in_traces_Rep_parallel_pre)
apply (simp add: to_index_style_T)
done

lemmas in_traces_par = in_traces_Alpha_parallel
                       in_traces_Inductive_parallel
                       in_traces_Rep_parallel

(*** Semantics for indexed alphabetized parallel on T ***)

lemma traces_Rep_parallel:
  "[| I ~= {} ; finite I |]
   ==> traces ([||]:I PXf) =
             {u. (sett(u) <= insert Tick (Ev ` (Union (snd ` PXf ` I))) & 
              (ALL i:I. (u rest-tr (snd (PXf i))) :t traces (fst (PXf i))))}t"
apply (simp add: in_traces_Rep_parallel[THEN sym])
done

(************************************
 |              traces              |
 ************************************)

lemma sett_in_traces_Rep_parallel:
  "[| I ~= {} ; finite I ; t :t traces ([||]:I PXf) |] 
   ==> sett t <= insert Tick (Ev ` Union (snd ` PXf ` I))"
by (simp add: in_traces_Rep_parallel)

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

declare disj_not1   [simp]
declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end

lemma in_traces_Inductive_parallel_lm1:

  (P, X) ∈ set PXs ==> X ⊆ Union (snd ` set PXs)

lemma in_traces_Inductive_parallel_lm:

  PXs ≠ [] -->
  (∀u. (u :t traces ([||] PXs)) =
       (sett u ⊆ insert Tick (Ev ` Union (snd ` set PXs)) ∧
        (∀P X. (P, X) ∈ set PXs --> u rest-tr X :t traces P)))

lemma in_traces_Inductive_parallel:

  PXs ≠ []
  ==> (u :t traces ([||] PXs)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` set PXs)) ∧
       (∀P X. (P, X) ∈ set PXs --> u rest-tr X :t traces P))

lemma traces_Inductive_parallel:

  PXs ≠ []
  ==> traces ([||] PXs) =
      {u. sett u ⊆ insert Tick (Ev ` Union (snd ` set PXs)) ∧
          (∀P X. (P, X) ∈ set PXs --> u rest-tr X :t traces P)}t

lemma sett_in_traces_Inductive_parallel:

  [| PXs ≠ []; t :t traces ([||] PXs) |]
  ==> sett t ⊆ insert Tick (Ev ` Union (snd ` set PXs))

lemma in_traces_Inductive_parallel_nth:

  PXs ≠ []
  ==> (u :t traces ([||] PXs)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` set PXs)) ∧
       (∀i<length PXs. u rest-tr snd (PXs ! i) :t traces (fst (PXs ! i))))

lemma to_index_style_T:

  (∀P X. (P, X) ∈ PXf ` I --> u rest-tr X :t traces P) =
  (∀i∈I. u rest-tr snd (PXf i) :t traces (fst (PXf i)))

lemma in_traces_Rep_parallel_pre:

  [| I ≠ {}; finite I |]
  ==> (u :t traces ([||]:I PXf)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` PXf ` I)) ∧
       (∀P X. (P, X) ∈ PXf ` I --> u rest-tr X :t traces P))

lemma in_traces_Rep_parallel:

  [| I ≠ {}; finite I |]
  ==> (u :t traces ([||]:I PXf)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` PXf ` I)) ∧
       (∀i∈I. u rest-tr snd (PXf i) :t traces (fst (PXf i))))

lemmas in_traces_par:

  (u :t traces (P |[X1.0,X2.0]| Q)) =
  (u rest-tr X1.0 :t traces P ∧
   u rest-tr X2.0 :t traces Q ∧ sett u ⊆ insert Tick (Ev ` (X1.0 ∪ X2.0)))

  PXs ≠ []
  ==> (u :t traces ([||] PXs)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` set PXs)) ∧
       (∀P X. (P, X) ∈ set PXs --> u rest-tr X :t traces P))

  [| I ≠ {}; finite I |]
  ==> (u :t traces ([||]:I PXf)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` PXf ` I)) ∧
       (∀i∈I. u rest-tr snd (PXf i) :t traces (fst (PXf i))))

lemmas in_traces_par:

  (u :t traces (P |[X1.0,X2.0]| Q)) =
  (u rest-tr X1.0 :t traces P ∧
   u rest-tr X2.0 :t traces Q ∧ sett u ⊆ insert Tick (Ev ` (X1.0 ∪ X2.0)))

  PXs ≠ []
  ==> (u :t traces ([||] PXs)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` set PXs)) ∧
       (∀P X. (P, X) ∈ set PXs --> u rest-tr X :t traces P))

  [| I ≠ {}; finite I |]
  ==> (u :t traces ([||]:I PXf)) =
      (sett u ⊆ insert Tick (Ev ` Union (snd ` PXf ` I)) ∧
       (∀i∈I. u rest-tr snd (PXf i) :t traces (fst (PXf i))))

lemma traces_Rep_parallel:

  [| I ≠ {}; finite I |]
  ==> traces ([||]:I PXf) =
      {u. sett u ⊆ insert Tick (Ev ` Union (snd ` PXf ` I)) ∧
          (∀i∈I. u rest-tr snd (PXf i) :t traces (fst (PXf i)))}t

lemma sett_in_traces_Rep_parallel:

  [| I ≠ {}; finite I; t :t traces ([||]:I PXf) |]
  ==> sett t ⊆ insert Tick (Ev ` Union (snd ` PXf ` I))