Theory CSP_F_law_rep_par (Isabelle2005: October 2005)

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

theory CSP_F_law_rep_par
imports CSP_F_law_alpha_par CSP_F_op_rep_par CSP_T_law_rep_par
begin

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

(*****************************************************************

         1. associativity of [||]:I
         2. commutativity of [||]:I
         3. 
         4. 

 *****************************************************************)

(*****************************************************
   replace an index set with another equal index set
 *****************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Rep_parallel_index_eq_lm1:
   "[| inj_on f I1 ; ALL i:I1. PXf2 (f i) = PXf1 i |] ==>
    Union {Yf i Int insert Tick (Ev ` snd (PXf1 i)) |i. i : I1} =
    Union {Yf (inv_on I1 f i) Int insert Tick (Ev ` snd (PXf2 i)) |i. i : f ` I1}"
apply (rule) 

 (* => *)
 apply (rule, simp)
 apply (elim conjE exE)
 apply (rule_tac x="(Yf i) Int insert Tick (Ev ` snd (PXf2 (f i)))" in exI)
 apply (simp)
 apply (rule_tac x="f i" in exI)
 apply (simp add: inv_f_f_on)

 (* <= *)
 apply (rule, simp)
 apply (simp add: image_iff)
 apply (elim conjE exE bexE)
 apply (rule_tac x=
   "(Yf xb) Int insert Tick (Ev ` snd (PXf1 xb))" in exI)
 apply (simp)
 apply (simp add: inv_f_f_on)
 apply (rule_tac x="xb" in exI)
 apply (simp)
done

lemma cspF_Rep_parallel_index_eq_lm2:
   "ALL i:I1. PXf2 (f i) = PXf1 i ==>
    Union {Yf i Int insert Tick (Ev ` snd (PXf2 i)) |i. i : f ` I1} =
    Union {Yf (f i) Int insert Tick (Ev ` snd (PXf1 i)) |i. i : I1}"
apply (rule) 

 (* => *)
 apply (rule, simp)
 apply (simp add: image_iff)
 apply (elim conjE exE bexE)
 apply (simp)
 apply (rule_tac x="xa" in exI)
 apply (simp)
 apply (rule_tac x="xb" in exI)
 apply (simp)

 (* <= *)
 apply (rule, simp)
 apply (elim conjE exE)
 apply (rule_tac x="xa" in exI)
 apply (simp)
 apply (rule_tac x="f i" in exI)
 apply (simp)
done

(* main *)

lemma cspF_Rep_parallel_index_eq:
   "[| finite I1 ;
       EX f. I2 = f ` I1 & inj_on f I1 &
             (ALL i:I1. PXf2 (f i) = PXf1 i) |]
     ==> [||]:I1 PXf1 =F[M,M] [||]:I2 PXf2"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_parallel_index_eq)
apply (case_tac "I1 = {}", simp)
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (elim conjE exE)
 apply (simp add: in_failures_Rep_parallel)
 apply (subgoal_tac "Union (snd ` PXf2 ` f ` I1) = Union (snd ` PXf1 ` I1)")
 apply (simp)
 apply (elim conjE exE)
 apply (rule_tac x="(%i. Yf (inv_on I1 f i))" in exI)
 apply (simp add: inv_f_f_on)
 apply (simp add: cspF_Rep_parallel_index_eq_lm1)
 apply (simp add: Union_index_fun)

 (* => *)
 apply (rule)
 apply (elim conjE exE)
 apply (simp add: in_failures_Rep_parallel)
 apply (subgoal_tac "Union (snd ` PXf2 ` f ` I1) = Union (snd ` PXf1 ` I1)")
 apply (simp)
 apply (elim conjE exE)
 apply (rule_tac x="(%i. Yf (f i))" in exI)
 apply (simp)
 apply (simp add: cspF_Rep_parallel_index_eq_lm2)
 apply (simp add: Union_index_fun)
done

(*********************************************************
                [||]:I PXf ==> [||] PXs
 *********************************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Index_to_Inductive_parallel:
  "[| finite I ; Is isListOf I |] ==>
   [||]:I PXf =F[M,M] [||] (map PXf Is)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Index_to_Inductive_parallel)
apply (case_tac "I = {}", simp)

apply (case_tac "map PXf Is = []")
apply (simp)
apply (rule order_antisym)

 (* <= *)
 apply (rule)
 apply (simp add: in_failures_Rep_parallel)
 apply (simp add: in_failures_Inductive_parallel_nth)
 apply (simp add: isListOf_set_eq)
 apply (elim conjE exE)
  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)
 apply (simp add: in_failures_Rep_parallel)
 apply (simp add: in_failures_Inductive_parallel_nth)
 apply (simp add: isListOf_set_eq)
 apply (elim conjE exE)
 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 (erule isListOf_index_to_nthE)
  apply (drule_tac x="i" in bspec, simp)
  apply (elim conjE exE, simp)

  apply (drule_tac x="n" in spec, simp)
  apply (rotate_tac 4)
  apply (drule sym)
  apply (simp add: isListOf_THE_nth)
done

(************************************
 |       [||]:I PXf and SKIP        |
 ************************************)

lemma cspF_SKIP_Rep_parallel_right_lm1:
  "I ~= {} ==>
   insert Tick (Union {Yf i Int insert Tick (Ev ` snd (PXf i)) |i. i : I})
   = Union {insert Tick (Yf i Int Ev ` snd (PXf i)) |i. i : I}"
by (auto)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_SKIP_Rep_parallel_right:
  "finite I ==>
   (([||]:I PXf) |[Union (snd `  PXf ` I), {}]| SKIP) =F[M,M]
   ([||]:I PXf)"
apply (case_tac "I={}")
apply (simp add: cspF_SKIP_Alpha_parallel)

apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_SKIP_Rep_parallel_right)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_failures_Alpha_parallel)
 apply (simp add: in_failures_Rep_parallel)
 apply (elim conjE exE)

  apply (case_tac "Tick ~: Z")
  apply (simp)
  apply (rule_tac x="Yf" in exI)
  apply (rule conjI)
  apply (subgoal_tac "Z Int {Tick} = {}")
  apply (simp (no_asm_simp))
  apply (simp)

  apply (intro ballI)
  apply (drule_tac x="i" in bspec, simp)
  apply (subgoal_tac " snd (PXf i) <= Union (snd ` PXf ` I)")
  apply (simp add: rest_tr_of_rest_tr_subset)
  apply (force)

  apply (simp add: in_failures)
  apply (erule disjE)
  apply (simp add: Evset_def)
  apply (force)

  apply (rule_tac x="(%i. insert Tick (Yf i))" in exI)
  apply (simp)
  apply (subgoal_tac "Z Int {Tick} = {Tick}", simp)
  apply (simp add: cspF_SKIP_Rep_parallel_right_lm1)

  apply (intro ballI)
  apply (drule_tac x="i" in bspec, simp)
  apply (subgoal_tac " snd (PXf i) <= Union (snd ` PXf ` I)")
  apply (simp add: rest_tr_of_rest_tr_subset)

  apply (simp add: rest_tr_Tick_sett)
  apply (elim conjE exE)
  apply (simp)
  apply (rule proc_T2_T3)
  apply (simp)
  apply (simp)
  apply (force)
  apply (force)

(* <= *)
 apply (rule)
 apply (simp add: in_failures_Alpha_parallel)
 apply (rule_tac x="X" in exI)
 apply (rule_tac x="{}" in exI)
 apply (simp)

 apply (simp add: in_failures)
 apply (simp add: rest_tr_empty)
 apply (simp add: in_failures_Rep_parallel)
 apply (elim conjE exE)
 apply (rule_tac x="Yf" in exI)
 apply (simp)
 apply (intro ballI)
 apply (drule_tac x="i" in bspec, simp)

 apply (subgoal_tac " snd (PXf i) <= Union (snd ` PXf ` I)")
 apply (simp add: rest_tr_of_rest_tr_subset)
 apply (force)
done

(************************************
 |        SKIP and [||]:I PXf       |
 ************************************)

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_SKIP_Rep_parallel_left:
  "finite I ==>
   (SKIP |[{}, Union (snd ` PXf ` I)]| ([||]:I PXf)) =F[M,M]
   ([||]:I PXf)"
apply (subgoal_tac 
    "(SKIP |[{}, Union (snd ` PXf ` I)]| ([||]:I PXf)) =F[M,M]
     (([||]:I PXf) |[Union (snd ` PXf ` I), {}]| SKIP)")
apply (rule cspF_trans)
apply (simp)
apply (simp add: cspF_SKIP_Rep_parallel_right)
apply (simp add: cspF_Alpha_parallel_commut)
done

(*** left and right ***)

lemmas cspF_SKIP_Rep_parallel = cspF_SKIP_Rep_parallel_left
                                  cspF_SKIP_Rep_parallel_right

(************************************
 |          associativity           |
 ************************************)

lemma cspF_Rep_parallel_ass_lm1:
   "Union {Yf i Int insert Tick (Ev ` snd (PXf i)) |i. i : I} Int
           insert Tick (Ev ` Union (snd ` PXf ` I))
    = Union {Yf i Int insert Tick (Ev ` snd (PXf i)) |i. i : I}"
by (auto)

lemma cspF_Rep_parallel_ass_lm2:
   "I1 Int I2 = {} ==>
    Union {Yf1 i Int insert Tick (Ev ` snd (PXf i)) |i. i : I1} Un
    Union {Yf2 i Int insert Tick (Ev ` snd (PXf i)) |i. i : I2} =
    Union {(if i : I1 then Yf1 i else Yf2 i) Int insert Tick (Ev ` snd (PXf i)) |i.
           i : I1 | i : I2}"
apply (rule)

 apply (rule)
 apply (simp)
 apply (elim disjE conjE exE)

  apply (rule_tac x="Yf1 i Int insert Tick (Ev ` snd (PXf i))" in exI, simp)
  apply (rule_tac x="i" in exI, simp)
  apply (rule_tac x="Yf2 i Int insert Tick (Ev ` snd (PXf i))" in exI, simp)
  apply (rule_tac x="i" in exI, simp)
  apply (force)

 apply (rule)
 apply (simp)
 apply (elim disjE conjE exE)

  apply (rule disjI1)
  apply (rule_tac x="Yf1 i Int insert Tick (Ev ` snd (PXf i))" in exI, simp)
  apply (rule_tac x="i" in exI, simp)
  apply (rule disjI2)
  apply (case_tac "i ~: I1")
  apply (rule_tac x="Yf2 i Int insert Tick (Ev ` snd (PXf i))" in exI, simp)
  apply (rule_tac x="i" in exI, simp)
  apply (force)
done

(*------------------*
 |      csp law     |
 *------------------*)

lemma cspF_Rep_parallel_assoc:
 "[| I1 Int I2 = {} ; finite I1 ; finite I2 |] ==>
  [||]:(I1 Un I2) PXf =F[M,M]
  [||]:I1 PXf |[Union (snd ` PXf ` I1), Union (snd ` PXf ` I2)]| [||]:I2 PXf"

apply (case_tac "I1 = {}")
apply (case_tac "I2 = {}")
apply (rule cspF_sym)
apply (simp add: cspF_SKIP_Alpha_parallel)
apply (rule cspF_sym)
apply (simp add: cspF_SKIP_Rep_parallel)

apply (case_tac "I2 = {}")
apply (rule cspF_sym)
apply (simp add: cspF_SKIP_Rep_parallel)

apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_parallel_assoc)
apply (rule order_antisym)

 (* => *)
 apply (rule)
 apply (simp add: in_failures_Alpha_parallel)
 apply (simp add: in_failures_Rep_parallel)
 apply (elim conjE exE)

 apply (rule_tac x="Union {Yf i Int insert Tick (Ev ` snd (PXf i)) |i. i : I1}" in exI)
 apply (rule_tac x="Union {Yf i Int insert Tick (Ev ` snd (PXf i)) |i. i : I2}" in exI)
 apply (simp add: Union_snd_Un)
 apply (rule conjI)
  apply (simp add: cspF_Rep_parallel_ass_lm1)
  apply (blast)

 apply (rule conjI)

  (* I1 *)
  apply (rule_tac x="Yf" in exI)
  apply (simp add: cspF_Rep_parallel_ass_lm1)

  apply (intro ballI)
  apply (drule_tac x="i" in bspec, simp)
  apply (subgoal_tac "snd (PXf i) <= Union (snd ` PXf ` I1)")
  apply (simp add: rest_tr_of_rest_tr_subset)
  apply (force)

  (* I2 *)
  apply (rule_tac x="Yf" in exI)
  apply (simp add: cspF_Rep_parallel_ass_lm1)

  apply (intro ballI)
  apply (drule_tac x="i" in bspec, simp)
  apply (subgoal_tac "snd (PXf i) <= Union (snd ` PXf ` I2)")
  apply (simp add: rest_tr_of_rest_tr_subset)
  apply (force)

 (* <= *)
 apply (rule)
 apply (simp add: in_failures_Alpha_parallel)
 apply (simp add: in_failures_Rep_parallel)
 apply (elim exE conjE)
 apply (simp add: Union_snd_Un)
 apply (rename_tac s X Y Z Yf1 Yf2)

 apply (rule_tac x="(%i. if i:I1 then Yf1 i else Yf2 i)" in exI)
       (* the necessity of the condition "I1 Int I2 = {}" *)
 apply (simp add: cspF_Rep_parallel_ass_lm2)

 apply (intro ballI)
 apply (simp)
 apply (erule disjE)

  apply (drule_tac x="i" in bspec, simp, simp)
  apply (subgoal_tac "snd (PXf i) <= Union (snd ` PXf ` I1)")
  apply (simp add: rest_tr_of_rest_tr_subset)
  apply (force)

  apply (drule_tac x="i" in bspec, simp)
  apply (case_tac "i ~: I1")
  apply (subgoal_tac "snd (PXf i) <= Union (snd ` PXf ` I2)")
  apply (simp add: rest_tr_of_rest_tr_subset)
  apply (force)
  apply (blast)
done

(************************************
 |             induct               |
 ************************************)

(*------------------*
 |     csp law      |
 |   (derivable)    |
 *------------------*)

lemma cspF_Rep_parallel_induct:
 "[| finite I ; i ~: I |] ==>
  [||]:(insert i I) PXf =F[M,M]
  fst (PXf i) |[snd (PXf i), Union (snd ` PXf ` I)]| [||]:I PXf"
apply (insert cspF_Rep_parallel_assoc[of "{i}" I PXf M])
apply (simp add: Rep_parallel_one)
apply (rule cspF_rw_left)
apply (simp)

apply (insert cspF_Alpha_parallel_assoc
  [of "fst (PXf i)" "snd (PXf i)" "{}" "SKIP" "Union (snd ` PXf ` I)" "[||]:I PXf" M])
apply (rule cspF_trans)
apply (simp)

apply (rule cspF_decompo_Alpha_parallel)
apply (simp_all)

apply (simp add: cspF_SKIP_Rep_parallel)
done

(****************** to add them again ******************)

declare Union_image_eq [simp]
declare Inter_image_eq [simp]

end

lemma cspF_Rep_parallel_index_eq_lm1:

  [| inj_on f I1.0; ∀i∈I1.0. PXf2.0 (f i) = PXf1.0 i |]
  ==> Union {Yf i ∩ insert Tick (Ev ` snd (PXf1.0 i)) |i. i ∈ I1.0} =
      Union
       {Yf (inv_on I1.0 f i) ∩ insert Tick (Ev ` snd (PXf2.0 i)) |i. i ∈ f ` I1.0}

lemma cspF_Rep_parallel_index_eq_lm2:

  ∀i∈I1.0. PXf2.0 (f i) = PXf1.0 i
  ==> Union {Yf i ∩ insert Tick (Ev ` snd (PXf2.0 i)) |i. i ∈ f ` I1.0} =
      Union {Yf (f i) ∩ insert Tick (Ev ` snd (PXf1.0 i)) |i. i ∈ I1.0}

lemma cspF_Rep_parallel_index_eq:

  [| finite I1.0;
     ∃f. I2.0 = f ` I1.0 ∧ inj_on f I1.0 ∧ (∀i∈I1.0. PXf2.0 (f i) = PXf1.0 i) |]
  ==> [||]:I1.0 PXf1.0 =F[M,M] [||]:I2.0 PXf2.0

lemma cspF_Index_to_Inductive_parallel:

  [| finite I; Is isListOf I |] ==> [||]:I PXf =F[M,M] [||] map PXf Is

lemma cspF_SKIP_Rep_parallel_right_lm1:

  I ≠ {}
  ==> insert Tick (Union {Yf i ∩ insert Tick (Ev ` snd (PXf i)) |i. i ∈ I}) =
      Union {insert Tick (Yf i ∩ Ev ` snd (PXf i)) |i. i ∈ I}

lemma cspF_SKIP_Rep_parallel_right:

  finite I ==> [||]:I PXf |[Union (snd ` PXf ` I),{}]| SKIP =F[M,M] [||]:I PXf

lemma cspF_SKIP_Rep_parallel_left:

  finite I ==> SKIP |[{},Union (snd ` PXf ` I)]| [||]:I PXf =F[M,M] [||]:I PXf

lemmas cspF_SKIP_Rep_parallel:

  finite I ==> SKIP |[{},Union (snd ` PXf ` I)]| [||]:I PXf =F[M,M] [||]:I PXf

  finite I ==> [||]:I PXf |[Union (snd ` PXf ` I),{}]| SKIP =F[M,M] [||]:I PXf

lemmas cspF_SKIP_Rep_parallel:

  finite I ==> SKIP |[{},Union (snd ` PXf ` I)]| [||]:I PXf =F[M,M] [||]:I PXf

  finite I ==> [||]:I PXf |[Union (snd ` PXf ` I),{}]| SKIP =F[M,M] [||]:I PXf

lemma cspF_Rep_parallel_ass_lm1:

  Union {Yf i ∩ insert Tick (Ev ` snd (PXf i)) |i. i ∈ I} ∩
  insert Tick (Ev ` Union (snd ` PXf ` I)) =
  Union {Yf i ∩ insert Tick (Ev ` snd (PXf i)) |i. i ∈ I}

lemma cspF_Rep_parallel_ass_lm2:

  I1.0 ∩ I2.0 = {}
  ==> Union {Yf1.0 i ∩ insert Tick (Ev ` snd (PXf i)) |i. i ∈ I1.0} ∪
      Union {Yf2.0 i ∩ insert Tick (Ev ` snd (PXf i)) |i. i ∈ I2.0} =
      Union
       {(if i ∈ I1.0 then Yf1.0 i else Yf2.0 i) ∩ insert Tick (Ev ` snd (PXf i)) |
        i. i ∈ I1.0 ∨ i ∈ I2.0}

lemma cspF_Rep_parallel_assoc:

  [| I1.0 ∩ I2.0 = {}; finite I1.0; finite I2.0 |]
  ==> [||]:(I1.0 ∪ I2.0) PXf =F[M,M] 
      [||]:I1.0 PXf |[Union (snd ` PXf ` I1.0),Union (snd ` PXf ` I2.0)]|
       [||]:I2.0 PXf

lemma cspF_Rep_parallel_induct:

  [| finite I; i ∉ I |]
  ==> [||]:insert i I PXf =F[M,M] 
      fst (PXf i) |[snd (PXf i),Union (snd ` PXf ` I)]| [||]:I PXf