Theory CSP_F_op_rep_par

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

theory CSP_F_op_rep_par = CSP_F_op_alpha_par + CSP_T_op_rep_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                |
 |                                                            |
 *============================================================*)

(*** Inductive_parallel ***)

lemma in_failures_Inductive_parallel_lm1: 
       "Y Int insert Tick (Ev ` snd a) Un
        Union {Y Int insert Tick (Ev ` X) |X Y. EX P. ((P, X), Y) : set PXYs} =
          Union {Ya Int insert Tick (Ev ` X) |X Ya.
                 EX P. P = fst a & X = snd a & Ya = Y | ((P, X), Ya) : set PXYs}"
by (auto)

lemma in_failures_Inductive_parallel_lm2: 
  "((P, X), Y) : set s ==> X <= Union (snd ` fst ` set s)"
apply (auto)
apply (rule_tac x="((P, X), Y)" in bexI)
by (simp_all)

lemma in_failures_Inductive_parallel_lm3:
   "Union {Y Int insert Tick (Ev ` X) |X Y. EX P. ((P, X), Y) : set zs} <=
    insert Tick (Ev ` Union (snd ` fst ` set zs))"
apply (rule)
apply (simp)
apply (elim conjE exE)
apply (simp)
apply (elim conjE disjE)
apply (simp)
apply (rule disjI2)
apply (auto)
apply (simp add: image_iff)
apply (rule_tac x="((P, X), Y)" in bexI)
apply (auto)
done

lemma in_failures_Inductive_parallel_lm4:
   "Union {Y Int insert Tick (Ev ` X) |X Y. EX P. ((P, X), Y) : set zs} Int
    insert Tick (Ev ` Union (snd ` fst ` set zs))
    = Union {Y Int insert Tick (Ev ` X) |X Y. EX P. ((P, X), Y) : set zs}"
apply (rule Int_subset_eq)
apply (simp add: in_failures_Inductive_parallel_lm3)
done

(* main *)

lemma in_failures_Inductive_parallel_lm:
 "PXs ~= [] --> (ALL f.
   (f :f failures([||] PXs)) =
         (EX u. (sett(u) <= insert Tick (Ev ` Union (snd ` set PXs)) & 
          (EX Z. f = (u, Z) &
          (EX PXYs. map fst PXYs = PXs &
          (Z Int insert Tick (Ev ` Union (snd ` set PXs))
           = Union {(Y Int insert Tick (Ev ` X))|X Y. EX P. ((P,X),Y) : set PXYs} &
          (ALL P X Y. ((P,X),Y) : set PXYs --> ((u rest-tr X), Y) :f failures(P))))))))"
apply (induct_tac PXs)

(* case 0 *)
 apply (simp)

(* case 1 *)
 apply (case_tac "list = []")
 apply (simp)
 apply (intro allI)
 apply (simp add: in_failures_Alpha_parallel)
 apply (simp add: in_failures)
 apply (rule iffI)
 (* => *)
  apply (elim conjE exE)
  apply (simp)
  apply (erule disjE)

   apply (rule_tac x="[(a,Y)]" in exI)
   apply (rule conjI)
    apply (rule_tac x="fst a" in exI)
    apply (rule_tac x="snd a" in exI)
    apply (simp)
    apply (rule conjI)
    apply (simp add: Evset_def pair_eq_decompo)
    apply (fast)
    apply (intro allI impI)
    apply (simp add: pair_eq_decompo)

   apply (case_tac "Tick ~: Z")
    apply (rule_tac x="[(a,Y)]" in exI)
    apply (simp add: Evset_def pair_eq_decompo)
    apply (fast)
   (* Tick : Z *)
    apply (rule_tac x="[(a,insert Tick Y)]" in exI)
    apply (simp)
    apply (rule conjI)
    apply (fast)
    apply (simp add: rest_tr_Tick_sett)
    apply (elim conjE exE)
    apply (simp add: pair_eq_decompo)
    apply (rule conjI)
    apply (fast)
    apply (rule proc_T2_T3, simp)
    apply (simp)

 (* <= *)
  apply (elim conjE exE)
  apply (simp)
  apply (subgoal_tac "aa rest-tr {} = <> | aa rest-tr {} = <Tick>")
  apply (erule disjE)

   (* <> *)
   apply (rule_tac x="bb" in exI)
   apply (rule_tac x="{}" in exI)
   apply (simp add: pair_eq_decompo)

   (* <Tick> *)
   apply (rule_tac x="bb" in exI)
   apply (rule_tac x="{}" in exI)
   apply (simp add: pair_eq_decompo)

   apply (simp add: rest_tr_empty)

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

(* => *)
 apply (elim conjE exE, simp)
 apply (rule_tac x="(a,Y) # PXYs" in exI)
 apply (simp add: pair_eq_decompo)
 apply (simp add: in_failures_Inductive_parallel_lm1)

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

 apply (rotate_tac -4)
 apply (drule sym)
 apply (simp add: in_failures_Inductive_parallel_lm2)

(* <= *)
 apply (simp)
 apply (elim conjE exE)

 apply (rule_tac x="bb" in exI)
 apply (rule_tac x=
    "Union {Y Int insert Tick (Ev ` X) |X Y. EX P. ((P, X), Y) : set zs}" in exI)
 apply (simp)
 apply (rule conjI)
 apply (simp add: pair_eq_decompo)
 apply (rotate_tac -1)
 apply (drule sym)
 apply (simp)
 apply (simp add: in_failures_Inductive_parallel_lm4)
 apply (simp add: in_failures_Inductive_parallel_lm1)

 apply (rule_tac x="zs" in exI)
 apply (rotate_tac -1)
 apply (drule sym)
 apply (simp add: in_failures_Inductive_parallel_lm4)

 apply (intro allI impI)
 apply (subgoal_tac "X <= Union (snd ` set list)")
 apply (simp add: rest_tr_of_rest_tr_subset)
 apply (simp add: in_failures_Inductive_parallel_lm2)
done

(*** remove ALL ***)

lemma in_failures_Inductive_parallel:
 "PXs ~= [] ==> 
   (f :f failures([||] PXs)) =
         (EX u. (sett(u) <= insert Tick (Ev ` Union (snd ` set PXs)) & 
          (EX Z. f = (u, Z) &
          (EX PXYs. map fst PXYs = PXs &
          (Z Int insert Tick (Ev ` Union (snd ` set PXs))
           = Union {(Y Int insert Tick (Ev ` X))|X Y. EX P. ((P,X),Y) : set PXYs} &
          (ALL P X Y. ((P,X),Y) : set PXYs --> ((u rest-tr X), Y) :f failures(P)))))))"
by (simp add: in_failures_Inductive_parallel_lm)

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

lemma failures_Inductive_parallel:
  "PXs ~= []
   ==> failures([||] PXs) =
      {f. (EX u. (sett(u) <= insert Tick (Ev ` Union (snd ` set PXs)) & 
          (EX Z. f = (u, Z) &
          (EX PXYs. map fst PXYs = PXs &
          (Z Int insert Tick (Ev ` Union (snd ` set PXs))
           = Union {(Y Int insert Tick (Ev ` X))|X Y. EX P. ((P,X),Y) : set PXYs} &
          (ALL P X Y. ((P,X),Y) : set PXYs --> ((u rest-tr X), Y) :f failures(P)))))))}f"
apply (simp add: in_failures_Inductive_parallel[THEN sym])
done

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

lemma sett_in_failures_Inductive_parallel:
  "[| PXs ~= [] ; (t,X) :f failures([||] PXs) |] 
   ==> sett t <= insert Tick (Ev ` Union (snd ` set PXs))"
by (simp add: in_failures_Inductive_parallel)

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

lemma in_failures_Inductive_parallel_nth:
 "PXs ~= [] ==> 
   (f :f failures([||] PXs)) =
         (EX u. (sett(u) <= insert Tick (Ev ` Union (snd ` set PXs)) & 
          (EX Z. f = (u, Z) &
          (EX Ys. length PXs = length Ys &
          (Z Int insert Tick (Ev ` Union (snd ` set PXs))
           = Union {((Ys!i) Int insert Tick (Ev ` (snd (PXs!i))))|i. i < length PXs} &
          (ALL i. i < length PXs --> ((u rest-tr (snd (PXs!i))), Ys!i) :f 
            failures(fst (PXs!i))))))))"
apply (simp add: in_failures_Inductive_parallel)
apply (simp add: set_nth)
apply (rule iffI)

(* => *)
 apply (elim conjE exE)
 apply (simp)
 apply (rule_tac x="map snd PXYs" in exI)
 apply (simp)
 apply (rotate_tac 3)
 apply (drule sym)
 apply (simp)
 apply (rule conjI)
 apply (simp add: pair_eq_decompo)

 apply (rule equalityI)
 (* <= *)
  apply (rule)
  apply (simp)
  apply (elim conjE exE)
  apply (simp)
  apply (elim conjE disjE)
   apply (simp)
   apply (rule_tac x="map snd PXYs ! i Int
                      insert Tick (Ev ` snd (map fst PXYs ! i))" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

   apply (rule_tac x="map snd PXYs ! i Int
                      insert Tick (Ev ` snd (map fst PXYs ! i))" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

 (* => *)
  apply (rule)
  apply (simp)
  apply (elim conjE exE)
  apply (simp)
  apply (elim conjE disjE)
   apply (simp)
   apply (rule_tac x=
     "(snd (PXYs ! i)) Int insert Tick (Ev ` snd (fst (PXYs ! i)))" in exI)
   apply (simp)
   apply (rule_tac x="snd (fst (PXYs ! i))" in exI)
   apply (rule_tac x="snd (PXYs ! i)" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

   apply (rule_tac x=
     "(snd (PXYs ! i)) Int insert Tick (Ev ` snd (fst (PXYs ! i)))" in exI)
   apply (simp)
   apply (rule_tac x="snd (fst (PXYs ! i))" in exI)
   apply (rule_tac x="snd (PXYs ! i)" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

  apply (intro allI impI)
  apply (drule_tac x="fst (fst (PXYs ! i))" in spec)
  apply (drule_tac x="snd (fst (PXYs ! i))" in spec)
  apply (drule_tac x="snd (PXYs ! i)" in spec)
  apply (simp)
  apply (fast)

 (* => *)
 apply (elim conjE exE)
 apply (simp)
 apply (rule_tac x="zip PXs Ys" in exI)
 apply (simp add: map_fst_zip_eq)

 apply (rule conjI)
 apply (simp add: pair_eq_decompo)

 apply (rule equalityI)
 (* <= *)
  apply (rule)
  apply (simp)
  apply (elim conjE exE)
  apply (simp)
  apply (elim conjE disjE)
   apply (simp)
   apply (rule_tac x="Ys ! i Int insert Tick (Ev ` snd (PXs ! i))" in exI)
   apply (simp)
   apply (rule_tac x="snd (PXs ! i)" in exI)
   apply (rule_tac x="Ys ! i" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

   apply (rule_tac x="Ys ! i Int insert Tick (Ev ` snd (PXs ! i))" in exI)
   apply (simp)
   apply (rule_tac x="snd (PXs ! i)" in exI)
   apply (rule_tac x="Ys ! i" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

 (* => *)
  apply (rule)
  apply (simp)
  apply (elim conjE exE)
  apply (simp)
  apply (elim conjE disjE)
   apply (simp)
   apply (rule_tac x="Ys ! i Int insert Tick (Ev ` snd (PXs ! i))" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

   apply (rule_tac x="Ys ! i Int insert Tick (Ev ` snd (PXs ! i))" in exI)
   apply (simp)
   apply (rule_tac x="i" in exI)
   apply (simp)

  apply (intro allI impI)
  apply (elim conjE exE)
  apply (drule_tac x="i" in spec)
  apply (simp add: pair_eq_decompo)
done

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

(*** failures Inductive_parallel ***)

lemma in_failures_Rep_parallel_lm1:
  "[| Is isListOf I ; length Ys = length Is |] ==>
    Union {Ys ! i Int insert Tick (Ev ` snd (map PXf Is ! i)) |i. i < length Ys} =
    Union {Ys ! (THE n. Is ! n = i & n < length Is) Int
           insert Tick (Ev ` snd (PXf i)) | i. i : I}"
apply (rule)

 (* <= *)
 apply (rule)
 apply (simp)
 apply (elim conjE exE)
 apply (rule_tac x=
   "Ys ! (THE n. Is ! n = (Is ! i) & n < length Is) Int
    insert Tick (Ev ` snd (PXf (Is ! i)))" in exI)
 apply (simp add: isListOf_THE_nth)
 apply (rule_tac x="(Is ! i)" in exI)
 apply (simp add: isListOf_THE_nth)
 apply (simp add: isListOf_nth_in_index)

 (* => *)
 apply (rule)
 apply (simp)
 apply (elim conjE exE)
 apply (simp)
 apply (erule isListOf_index_to_nthE)
 apply (drule_tac x="i" in bspec, simp)
 apply (elim conjE exE, simp)
 apply (simp add: isListOf_THE_nth)
 apply (rule_tac x=
   "Ys ! n Int insert Tick (Ev ` snd (PXf (Is ! n)))" in exI)
 apply (simp)
 apply (rule_tac x="n" in exI)
 apply (simp)
done

lemma in_failures_Rep_parallel_lm2:
  "Is isListOf I ==>
   Union {Yf i Int insert Tick (Ev ` snd (PXf i)) |i. i : I} =
   Union {map Yf Is ! i Int insert Tick (Ev ` snd (map PXf Is ! i)) |i. i < length Is}"
apply (rule)

 (* <= *)
 apply (rule)
 apply (simp)
 apply (elim conjE exE)
 apply (erule isListOf_index_to_nthE)
 apply (drule_tac x="i" in bspec, simp)
 apply (elim conjE exE, simp)
 apply (rule_tac x=
   "map Yf Is ! n Int insert Tick (Ev ` snd (map PXf Is ! n))" in exI)
 apply (simp)
 apply (rule_tac x="n" in exI)
 apply (simp)

 (* => *)
 apply (rule)
 apply (simp)
 apply (elim conjE exE)
 apply (rule_tac x= "Yf (Is!i) Int insert Tick (Ev ` snd (PXf (Is!i)))" in exI)
 apply (simp)
 apply (rule_tac x="(Is!i)" in exI)
 apply (simp add: isListOf_nth_in_index)
done

lemma in_failures_Rep_parallel:
  "[| I ~= {} ; finite I |]
   ==> (f :f failures ([||]:I PXf)) =
         (EX u. (sett(u) <= insert Tick (Ev ` Union (snd ` PXf ` I)) & 
          (EX Z. f = (u, Z) &
          (EX Yf. 
          (Z Int insert Tick (Ev ` Union (snd ` PXf ` I))
           = Union {((Yf i) Int insert Tick (Ev ` (snd (PXf i))))|i. i : I} &
          (ALL i:I. ((u rest-tr (snd (PXf i))), Yf i) :f failures(fst (PXf i))))))))"
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_failures_Inductive_parallel_nth)
apply (rule someI2)
 apply (simp)
 apply (rule iffI)

  (* => *)
  apply (elim conjE exE)
  apply (rename_tac Is' Is u Z Ys)
  apply (rule_tac x="u" in exI)
  apply (simp add: isListOf_set_eq)
  apply (rule_tac x= "(%i. (Ys!(THE n. (Is!n) = i & n<length Is)))" in exI)
  apply (rule conjI)
  apply (simp add: in_failures_Rep_parallel_lm1)
  apply (rule ballI)

  apply (rotate_tac 4)
  apply (erule isListOf_index_to_nthE)
  apply (drule_tac x="i" in bspec, simp)
  apply (elim conjE exE, simp)

  apply (rotate_tac 2)
  apply (drule sym)
  apply (simp add: isListOf_THE_nth)

  (* <= *)
  apply (elim conjE exE)
  apply (rename_tac Is' Is u Z Yf)
  apply (rule_tac x="u" in exI)
  apply (simp add: isListOf_set_eq)
  apply (rule_tac x= "map Yf Is" in exI)
  apply (simp)
  apply (rule conjI)
  apply (rule in_failures_Rep_parallel_lm2, simp)
  apply (intro allI impI)
  apply (drule_tac x="Is ! i" in bspec)
  apply (simp add: isListOf_nth_in_index)
  apply (simp)

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

apply (simp add: isListOf_EX)
done

lemmas in_failures_par = in_failures_Alpha_parallel
                         in_failures_Inductive_parallel
                         in_failures_Rep_parallel

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

lemma failures_Rep_parallel:
  "[| I ~= {} ; finite I |]
   ==> failures ([||]:I PXf) =
      {f. (EX u. (sett(u) <= insert Tick (Ev ` Union (snd ` PXf ` I)) & 
          (EX Z. f = (u, Z) &
          (EX Yf. 
          (Z Int insert Tick (Ev ` Union (snd ` PXf ` I))
           = Union {((Yf i) Int insert Tick (Ev ` (snd (PXf i))))|i. i : I} &
          (ALL i:I. ((u rest-tr (snd (PXf i))), Yf i) :f failures(fst (PXf i))))))))}f"
apply (simp add: in_failures_Rep_parallel[THEN sym])
done

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

lemma sett_in_failures_Rep_parallel:
  "[| I ~= {} ; finite I ; (t,X) :f failures([||]:I PXf) |] 
   ==> sett t <= insert Tick (Ev ` Union (snd ` PXf ` I))"
by (simp add: in_failures_Rep_parallel)

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

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

end