Theory Parallel (Isabelle2004: April 2004)

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               December 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Parallel = CSP_semantics:

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

declare disj_not1 [simp del]

(*  The following simplification is sometimes unexpected.              *)
(*                                                                     *)
(*             not_None_eq: (x ~= None) = (EX y. x = Some y)           *)

declare not_None_eq [simp del]

(*********************************************************
                        DomT
 *********************************************************)

(*** Parallel_domT ***)

lemma Parallel_domT : 
  "{u. EX s t. u : s |[X]|tr t & s :t [[P]]T ev & t :t [[Q]]T ev} : domT"
apply (simp add: domT_def HC_T1_def)
apply (rule conjI)
apply (rule_tac x="[]t" in exI, simp)

(* prefix closed *)
apply (simp add: prefix_closed_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (erule par_tr_prefixE, simp)
apply (rule_tac x="s'" in exI)
apply (rule_tac x="t'" in exI)
apply (simp)

apply (rule conjI)
by (rule memT_prefix_closed, simp_all)+

(*** Parallel_memT ***)

lemma Parallel_memT:
  "(u :t [[P |[X]| Q]]T ev) = 
   (EX s t. u : s |[X]|tr t & s :t [[P]]T ev & t :t [[Q]]T ev)"
apply (simp add: evalT_def)
by (simp add: memT_def Abs_domT_inverse Parallel_domT[simplified memT_def])

(*********************************************************
                         DomF
 *********************************************************)

(*** Parallel_domF ***)

lemma Parallel_domF : 
  "{f. EX u Y Z. f = (u, Y Un Z) & Y-((Ev`X) Un {Tick})= Z-((Ev`X) Un {Tick}) &
      (EX s t. u : s |[X]|tr t & (s,Y) :f [[P]]F ev & (t,Z) :f [[Q]]F ev)}: domF"
apply (simp add: domF_def HC_F2_def)
apply (intro allI impI)
apply (elim conjE exE, simp)
apply (rename_tac u Y Z Y1 Y2 s t)
apply (rule_tac x="Z Int (Y1 - (Y2 - insert Tick (Ev ` X))) Un
                   Z Int (Y2 - insert Tick (Ev ` X))" in exI)
apply (rule_tac x="Z Int (Y2 - (Y2 - insert Tick (Ev ` X))) Un
                   Z Int (Y2 - insert Tick (Ev ` X))" in exI)

(* (s,Y), Z <= Y, Y = Y1 Un Y2, Z = Z1 Un Z2 *)

apply (rule conjI, force)
apply (rule conjI, force)

apply (rule_tac x="s" in exI)
apply (rule_tac x="t" in exI)
apply (simp)
apply (rule conjI)
apply (rule memF_F2, simp, force)+
done

lemma Parallel_memF:
  "(f :f [[P |[X]| Q]]F ev) = 
   (EX u Y Z. f = (u, Y Un Z) & Y-((Ev`X) Un {Tick})= Z-((Ev`X) Un {Tick}) &
      (EX s t. u : s |[X]|tr t & (s,Y) :f [[P]]F ev & (t,Z) :f [[Q]]F ev))"
apply (simp only: evalF_def)
apply (simp only: memF_def Abs_domF_inverse Parallel_domF[simplified memF_def])
by (simp)

lemmas Parallel_mem = Parallel_memT Parallel_memF

(*********************************************************
                         domSF
 *********************************************************)

(*** T2 ***)

lemma Parallel_T2 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T2 ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev)"
apply (simp add: HC_T2_def Parallel_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
apply (simp)
apply (simp add: domSF_def HC_T2_def)
apply (elim conjE)
apply (drule_tac x="sa" in spec)
apply (drule_tac x="t" in spec)

apply (drule mp, rule_tac x="Y" in exI, simp)
apply (drule mp, rule_tac x="Z" in exI, simp)
by (simp)

(*** F3 ***)

lemma Parallel_F3_lm1: "X1 Un (X2 Un X3) - X = (X1 - X) Un (X2 - X) Un (X3 - X)"
by (auto)

lemma Parallel_F3_lm2: "[| X1 = X2 ; Y1 = Y2 |] ==> X1 Un Y1 = X2 Un Y2"
by (auto)

lemma Parallel_F3 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_F3 ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev)"
apply (simp add: HC_F3_def Parallel_mem)
apply (intro allI impI)
apply (elim conjE exE)
apply (rename_tac u X12 Y X1 X2 s t)

(* (u, X12) :f [[P |[X]| Q]]F ev *)
(* (s, X1)  :f [[P]]F ev         *)
(* (t, X2)  :f [[Q]]F ev         *)
(*  X12 = X1 Un X2               *)

apply (rule_tac x=
        "X1 Un
         ({a. a : Y & (a = Tick | a : Ev ` X) & s @t [a]t ~:t [[P]]T ev} Un
          {a. a : Y & a ~= Tick & a ~: Ev ` X})" in exI)       (* Z1 *)
apply (rule_tac x=
        "X2 Un
         ({a. a : Y & (a = Tick | a : Ev ` X) & t @t [a]t ~:t [[Q]]T ev} Un
          {a. a : Y & a ~= Tick & a ~: Ev ` X})" in exI)       (* Z2 *)

apply (subgoal_tac "notick s & notick t", simp)
apply (rule conjI)

(* show X12 Un Y = X1 Un Z1 Un Z2 *)
apply (rule equalityI)

 (* <= *)
 apply (rule subsetI, simp)
 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (simp)

 apply (drule_tac x="x" in spec, simp)
 apply (drule_tac x="s @t [x]t" in spec)
 apply (drule_tac x="t @t [x]t" in spec)

  (* no sync *)
  apply (case_tac "x ~= Tick & x ~: Ev ` X", simp)
  (* sync *)
  apply (simp add: par_tr_last)
  apply (erule disjE, simp)

  apply (rotate_tac -1)
  apply (erule disjE, simp)
  apply (simp)

 (* => *)
 apply (force)

apply (rule conjI)

 (* show X1 Un ... = X2 Un ... *)
 apply (simp add: Parallel_F3_lm1)
 apply (rule Parallel_F3_lm2)
 apply (rule Parallel_F3_lm2)
 apply (simp)
 apply (force)
 apply (simp)

 (* condition 2 *)
 apply (rule_tac x="s" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp)

 apply (simp add: domSF_def HC_F3_def)
 apply (elim conjE)
 apply (drule_tac x="s" in spec)
 apply (drule_tac x="t" in spec)
 apply (drule_tac x="X1" in spec)
 apply (drule_tac x="X2" in spec)
 apply (drule_tac x="{a. a : Y & (a = Tick | a : Ev ` X) & s @t [a]t ~:t [[P]]T ev} Un
                     {a. a : Y & a ~= Tick & a ~: Ev ` X}" in spec)
 apply (drule_tac x="{a. a : Y & (a = Tick | a : Ev ` X) & t @t [a]t ~:t [[Q]]T ev} Un
                     {a. a : Y & a ~= Tick & a ~: Ev ` X}" in spec)
 apply (simp)

 (* left *)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (drule_tac x="s @t [a]t" in spec)
  apply (drule_tac x="t" in spec)
  apply (erule disjE)
  apply (simp add: par_tr_last)
  apply (erule disjE, simp)

  apply (simp add: HC_T2_def)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="t" in spec)
  apply (force)

 (* right *)
 apply (drule mp)
  apply (intro allI impI)
  apply (drule_tac x="a" in spec, simp)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="t @t [a]t" in spec)
  apply (erule disjE)
  apply (simp add: par_tr_last)

  apply (erule disjE)
  apply (simp add: HC_T2_def)
  apply (drule_tac x="s" in spec)
  apply (drule_tac x="t" in spec)
  apply (force)
  apply (simp)
 apply (simp)

(* notick s & notick t *)
apply (rule conjI)
apply (rule par_tr_notick_left, simp_all)
apply (rule par_tr_notick_right, simp_all)
done

(* T3_F4 *)

lemma Parallel_T3_F4 :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> HC_T3_F4 ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev)"
apply (simp add: HC_T3_F4_def Parallel_mem)
apply (intro allI impI)
apply (simp add: par_tr_last)
apply (elim conjE exE)
apply (rule conjI)

 (* F4 *)
 apply (rule_tac x="Evset" in exI)
 apply (rule_tac x="Evset" in exI)
 apply (simp)
 apply (rule_tac x="s'" in exI)
 apply (rule_tac x="t'" in exI)
 apply (simp add: domSF_def HC_F4_def)

 (* T3 *)
 apply (rule allI)
 apply (rule_tac x="Xa" in exI)
 apply (rule_tac x="Xa" in exI)
 apply (simp)
 apply (rule_tac x="sa" in exI)
 apply (rule_tac x="t" in exI)
 apply (simp add: domSF_def HC_T3_def)
done

(*** Parallel_domSF ***)

lemma Parallel_domSF :
  "[| ([[P]]T ev, [[P]]F ev) : domSF ; ([[Q]]T ev, [[Q]]F ev) : domSF |]
     ==> ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev) : domSF"
apply (simp (no_asm) add: domSF_iff)
apply (simp add: Parallel_T2)
apply (simp add: Parallel_F3)
apply (simp add: Parallel_T3_F4)
done

(*********************************************************
                      mono
 *********************************************************)

(*** T ***)

lemma Parallel_evalT_mono:
  "[| [[P1]]T ev1 <= [[P2]]T ev2 ; [[Q1]]T ev1 <= [[Q2]]T ev2 |]
   ==> [[P1 |[X]| Q1]]T ev1 <= [[P2 |[X]| Q2]]T ev2"
apply (simp add: subsetT_iff)
apply (intro allI impI)
apply (simp add: Parallel_memT)
apply (elim conjE exE)
apply (rule_tac x="s" in exI)
apply (rule_tac x="ta" in exI)
by (simp_all)

(*** F ***)

lemma Parallel_evalF_mono:
  "[| [[P1]]F ev1 <= [[P2]]F ev2 ; [[Q1]]F ev1 <= [[Q2]]F ev2 |]
   ==> [[P1 |[X]| Q1]]F ev1 <= [[P2 |[X]| Q2]]F ev2"
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (simp add: Parallel_memF)
apply (elim conjE exE)
apply (rule_tac x="Y" in exI)
apply (rule_tac x="Z" in exI)
apply (simp)
apply (rule_tac x="sa" in exI)
apply (rule_tac x="t" in exI)
by (simp_all)

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

declare disj_not1   [simp] 
declare not_None_eq [simp]

end

lemma Parallel_domT:

  {u. ∃s t. u ∈ s |[X]|tr t ∧ s :t [[P]]T ev ∧ t :t [[Q]]T ev} ∈ domT

lemma Parallel_memT:

  (u :t [[P |[X]| Q]]T ev) =
  (∃s t. u ∈ s |[X]|tr t ∧ s :t [[P]]T ev ∧ t :t [[Q]]T ev)

lemma Parallel_domF:

  {(u, Y ∪ Z) |u Y Z.
   Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧
   (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f [[P]]F ev ∧ (t, Z) :f [[Q]]F ev)}
  ∈ domF

lemma Parallel_memF:

  (f :f [[P |[X]| Q]]F ev) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧
      Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧
      (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f [[P]]F ev ∧ (t, Z) :f [[Q]]F ev))

lemmas Parallel_mem:

  (u :t [[P |[X]| Q]]T ev) =
  (∃s t. u ∈ s |[X]|tr t ∧ s :t [[P]]T ev ∧ t :t [[Q]]T ev)

  (f :f [[P |[X]| Q]]F ev) =
  (∃u Y Z.
      f = (u, Y ∪ Z) ∧
      Y - (Ev ` X ∪ {Tick}) = Z - (Ev ` X ∪ {Tick}) ∧
      (∃s t. u ∈ s |[X]|tr t ∧ (s, Y) :f [[P]]F ev ∧ (t, Z) :f [[Q]]F ev))

lemma Parallel_T2:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_T2 ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev)

lemma Parallel_F3_lm1:

  X1 ∪ (X2 ∪ X3) - X = X1 - X ∪ (X2 - X) ∪ (X3 - X)

lemma Parallel_F3_lm2:

  [| X1 = X2; Y1 = Y2 |] ==> X1 ∪ Y1 = X2 ∪ Y2

lemma Parallel_F3:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_F3 ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev)

lemma Parallel_T3_F4:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> HC_T3_F4 ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev)

lemma Parallel_domSF:

  [| ([[P]]T ev, [[P]]F ev) ∈ domSF; ([[Q]]T ev, [[Q]]F ev) ∈ domSF |]
  ==> ([[P |[X]| Q]]T ev, [[P |[X]| Q]]F ev) ∈ domSF

lemma Parallel_evalT_mono:

  [| [[P1]]T ev1 ≤ [[P2]]T ev2; [[Q1]]T ev1 ≤ [[Q2]]T ev2 |]
  ==> [[P1 |[X]| Q1]]T ev1 ≤ [[P2 |[X]| Q2]]T ev2

lemma Parallel_evalF_mono:

  [| [[P1]]F ev1 ≤ [[P2]]F ev2; [[Q1]]F ev1 ≤ [[Q2]]F ev2 |]
  ==> [[P1 |[X]| Q1]]F ev1 ≤ [[P2 |[X]| Q2]]F ev2