Theory CSP_law_step1

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

theory CSP_law_step1 = CSP_proc:

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

declare not_None_eq [simp del]

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

         1. step laws
         2.
         3. 
         4. 

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

consts
  Ext_choice_step  :: 
      "'a set => 'a set => ('a => ('n,'a) proc) 
                        => ('a => ('n,'a) proc) => ('n,'a) proc"

  Parallel_step ::
      "'a set => 'a set => 'a set
          => ('a => ('n,'a) proc) => ('a => ('n,'a) proc)
          => ('n,'a) proc"

  Hiding_step ::
      "'a set => 'a set => ('a => ('n,'a) proc) => ('n,'a) proc"

defs
  Ext_choice_step_def :
   "Ext_choice_step X Y Pf Qf ==
      ? x:(X Un Y) -> 
                (IF (x : X & x : Y) THEN Pf x |~| Qf x
                 ELSE IF (x : X) THEN Pf x
                 ELSE Qf x)"
defs
  Parallel_step_def :
   "Parallel_step X Y Z Pf Qf ==
      ? x:((X Int Y Int Z) Un (Y - X) Un (Z - X))
         -> IF (x : X) THEN (Pf x |[X]| Qf x)
               ELSE IF (x : Y & x : Z) THEN ((Pf x |[X]| ? x:Z -> Qf x)
                                     |~| (? x:Y -> Pf x |[X]| Qf x))
               ELSE IF (x : Y) THEN (Pf x |[X]| ? x:Z -> Qf x)
               ELSE (? x:Y -> Pf x |[X]| Qf x)"
defs
  Hiding_step_def :
   "Hiding_step X Y Pf ==
      IF (Y Int X = {}) THEN (? x:Y -> (Pf x -- X))
                         ELSE ((? x:(Y-X) -> (Pf x -- X)) 
                               [> (! x:(Y Int X) .. (Pf x -- X)))"

(*********************************************************
                    stop expansion
 *********************************************************)

lemma domSF_STOP_step: "[[STOP]]SF ev = [[? x:{} -> DIV]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: evalT_def)
apply (simp add: evalF_def)
done

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

lemma csp_STOP_step: "LET:fp df IN STOP =F LET:fp df IN ? x:{} -> DIV"
apply (induct fp)
by (simp_all add: eqF_def domSF_STOP_step)

(*********************************************************
                    Act_prefix expansion
 *********************************************************)

lemma domSF_Act_prefix_step: "[[a -> P]]SF ev = [[? x:{a} -> P]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: evalT_def)
apply (simp add: evalF_def)
done

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

lemma csp_Act_prefix_step: 
 "LET:fp df IN a -> P =F LET:fp df IN ? x:{a} -> P"
apply (induct fp)
by (simp_all add: eqF_def domSF_Act_prefix_step)

(*********************************************************
                    Ext choice expansion
 *********************************************************)

(*** domT ***)

lemma domT_Ext_choice_step:
  "[[? :X -> Pf [+] ? :Y -> Qf]]T ev =
   [[Ext_choice_step X Y Pf Qf]]T ev"
apply (simp add: Ext_choice_step_def)
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (simp add: Ext_choice_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
 apply (simp_all)

 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" in exI)
 apply (simp add: Conditional_mem Int_choice_mem)

 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" in exI)
 apply (simp add: Conditional_mem Int_choice_mem)

(* <= *)
 apply (rule)
 apply (simp add: Ext_choice_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
 apply (simp_all add: Conditional_mem)

 apply (case_tac "a : Y")
 apply (simp_all add: Conditional_mem Int_choice_mem)
 apply (fast)
 apply (fast)

 apply (case_tac "a : X")
 apply (simp_all add: Conditional_mem Int_choice_mem)
 apply (fast)
 apply (fast)
done

(*** domF ***)

lemma domF_Ext_choice_step:
  "[[? :X -> Pf [+] ? :Y -> Qf]]F ev =
   [[Ext_choice_step X Y Pf Qf]]F ev"
apply (simp add: Ext_choice_step_def)
apply (rule eq_iffI)

(* => *)

 (* 1 *)
 apply (rule)
 apply (simp add: Ext_choice_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
 apply (simp_all)
 apply (simp add: memF_IntF)
 apply (simp add: Ext_pre_choice_mem)
 apply (fast)

 (* 2 *)
 apply (simp add: memF_UnF)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI)
 apply (simp add: Conditional_mem Int_choice_mem)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sa" in exI)
 apply (simp add: Conditional_mem Int_choice_mem)

 (* 3 *)
 apply (simp add: memT_UnT)
 apply (simp add: Ext_pre_choice_mem)

(* <= *)

 (* 1 *)
 apply (rule)
 apply (simp add: Ext_choice_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)
 apply (simp add: memF_IntF)
 apply (simp add: Ext_pre_choice_mem)
 apply (fast)

 (* 2 *)
 apply (simp add: memF_UnF)
 apply (simp add: Ext_pre_choice_mem)
 apply (case_tac "a : Y")
 apply (simp add: Conditional_mem Int_choice_mem)
 apply (fast)
 apply (simp add: Conditional_mem Int_choice_mem)
 apply (fast)

 apply (case_tac "a : X")
 apply (simp add: Conditional_mem Int_choice_mem)
 apply (simp add: memF_UnF Ext_pre_choice_mem)
 apply (fast)

 apply (simp add: Conditional_mem Int_choice_mem)
 apply (simp add: memF_UnF Ext_pre_choice_mem)
 apply (fast)
done

(*** domSF ***)

lemma domSF_Ext_choice_step:
  "[[? :X -> Pf [+] ? :Y -> Qf]]SF ev =
   [[Ext_choice_step X Y Pf Qf]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Ext_choice_step)
apply (simp add: domF_Ext_choice_step)
done

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

lemma csp_Ext_choice_step:
  "LET:fp df IN (? :X -> Pf) [+] (? :Y -> Qf) =F
   LET:fp df IN Ext_choice_step X Y Pf Qf"
apply (induct fp)
by (simp_all add: eqF_def domSF_Ext_choice_step)

(*********************************************************
                    Parallel expansion
 *********************************************************)

(*** domT ***)

lemma domT_Parallel_step: 
  "[[(? :Y -> Pf) |[X]| (? :Z -> Qf)]]T ev =
   [[Parallel_step X Y Z Pf Qf]]T ev"
apply (simp add: Parallel_step_def)
apply (rule eq_iffI)

(* => *)
 apply (rule)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="t" in spec)
 apply (simp add: not_None_T)
 apply (elim disjE conjE exE)

 (* []t *)
  apply (simp)

 (* [Tick]t *)
 apply (simp add: Parallel_mem Ext_pre_choice_mem)

 (* [Ev .]t *)
 apply (simp add: Parallel_mem)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)

  (* 1 *)
  apply (simp)

  (* 2 *)
  apply (simp add: par_tr_head)
  apply (elim conjE exE)
  apply (simp add: not_None_T)
  apply (rule_tac x="aa" in exI)
  apply (rule_tac x="s" in exI)
  apply (simp)

  apply (simp add: Conditional_mem)
  apply (case_tac "aa : Y")
   apply (simp add: Int_choice_mem)
   apply (simp add: Parallel_mem)
   apply (rule disjI2)
   apply (rule_tac x="[]t" in exI)
   apply (rule_tac x="sb" in exI)
   apply (simp)
   (* aa ~: Y *)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="[]t" in exI)
   apply (rule_tac x="sb" in exI)
   apply (simp)

  (* 3 *)
  apply (simp add: par_tr_head)
  apply (elim conjE exE)
  apply (simp add: not_None_T)
  apply (rule_tac x="aa" in exI)
  apply (rule_tac x="s" in exI)
  apply (simp)

  apply (simp add: Conditional_mem)
  apply (case_tac "aa : Z")
   apply (simp add: Int_choice_mem)
   apply (simp add: Parallel_mem)
   apply (rule disjI1)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[]t" in exI)
   apply (simp)
   (* aa ~: Y *)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[]t" in exI)
   apply (simp)

  (* 4 *)
  apply (simp add: par_tr_head)
  apply (elim disjE conjE exE)

   (* 4-1 *)
   apply (simp add: not_None_T)
   apply (rule_tac x="ab" in exI)
   apply (rule_tac x="s" in exI)
   apply (simp)

   apply (simp add: Conditional_mem)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="sc" in exI)
   apply (simp)

   (* 4-2 *)
   apply (simp add: not_None_T)
   apply (rule_tac x="aa" in exI)
   apply (rule_tac x="s" in exI)
   apply (simp)

   apply (simp add: Conditional_mem)
   apply (case_tac "aa : Z")
    apply (simp add: Int_choice_mem)
    apply (simp add: Parallel_mem)
    apply (rule disjI1)
    apply (rule_tac x="sb" in exI)
    apply (rule_tac x="[Ev ab]t @t sc" in exI)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)
    (* aa ~: Z *)
    apply (simp add: Parallel_mem)
    apply (rule_tac x="sb" in exI)
    apply (rule_tac x="[Ev ab]t @t sc" in exI)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)

   (* 4-3 *)
   apply (simp add: not_None_T)
   apply (rule_tac x="ab" in exI)
   apply (rule_tac x="s" in exI)
   apply (simp)

   apply (simp add: Conditional_mem)
   apply (case_tac "ab : Y")
    apply (simp add: Int_choice_mem)
    apply (simp add: Parallel_mem)
    apply (rule disjI2)
    apply (rule_tac x="[Ev aa]t @t sb" in exI)
    apply (rule_tac x="sc" in exI)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)
    (* ab ~: Y *)
    apply (simp add: Parallel_mem)
    apply (rule_tac x="[Ev aa]t @t sb" in exI)
    apply (rule_tac x="sc" in exI)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)

(* <= *)
 apply (rule)+
 apply (drule_tac x="t" in spec)
 apply (simp add: not_None_T)
 apply (elim disjE conjE exE)

 (* []t *)
  apply (simp)

 (* [Tick]t *)
 apply (simp add: Parallel_mem Ext_pre_choice_mem)

 (* [Ev .]t *)
 apply (simp add: Ext_pre_choice_mem)
 apply (elim disjE conjE exE)

  (* 1 *)
  apply (simp add: Conditional_mem)
  apply (simp add: Parallel_mem)
  apply (elim conjE exE)
  apply (rule_tac x="[Ev aa]t @t sb" in exI)
  apply (rule_tac x="[Ev aa]t @t ta" in exI)
  apply (simp add: par_tr_head)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)

  (* 2 *)
  apply (simp add: not_None_T)
  apply (simp add: Conditional_mem)
  apply (case_tac "aa : Z")
   apply (simp add: Int_choice_mem)
   apply (erule disjE)
    apply (simp add: Parallel_mem)
    apply (elim conjE exE)
    apply (rule_tac x="[Ev aa]t @t sb" in exI)
    apply (rule_tac x="ta" in exI)
    apply (simp add: par_tr_head)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)
    (* *)
    apply (simp add: Parallel_mem)
    apply (elim conjE exE)
    apply (rule_tac x="sb" in exI)
    apply (rule_tac x="[Ev aa]t @t ta" in exI)
    apply (simp add: par_tr_head)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)

   (* aa ~: Z" *)
   apply (simp add: Conditional_mem)
   apply (simp add: Parallel_mem)
   apply (elim conjE exE)
   apply (rule_tac x="[Ev aa]t @t sb" in exI)
   apply (rule_tac x="ta" in exI)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)

  (* 3 *)
  apply (simp add: not_None_T)
  apply (simp add: Conditional_mem)
  apply (case_tac "aa : Y")
   apply (simp add: Int_choice_mem)
   apply (erule disjE)
    apply (simp add: Parallel_mem)
    apply (elim conjE exE)
    apply (rule_tac x="[Ev aa]t @t sb" in exI)
    apply (rule_tac x="ta" in exI)
    apply (simp add: par_tr_head)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)
    (* *)
    apply (simp add: Parallel_mem)
    apply (elim conjE exE)
    apply (rule_tac x="sb" in exI)
    apply (rule_tac x="[Ev aa]t @t ta" in exI)
    apply (simp add: par_tr_head)
    apply (simp add: Ext_pre_choice_mem)
    apply (fast)

   (* aa ~: Y" *)
   apply (simp add: Conditional_mem)
   apply (simp add: Parallel_mem)
   apply (elim conjE exE)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[Ev aa]t @t ta" in exI)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
done

(*** domF ***)

(* set 1 *)

lemma domF_Parallel_step_set1:
  "[| Ya - insert Tick (Ev ` X) = Za - insert Tick (Ev ` X) ;
       Ev ` Y Int Ya = {}; Ev ` Z Int Za = {} |]
   ==> Ev ` (X Int Y Int Z) Int (Ya Un Za) = {}"
by (auto)

(* set 2 *)

lemma domF_Parallel_step_set2:
  "[| Ya - insert Tick (Ev ` X) = Za - insert Tick (Ev ` X) ;
       Ev ` Y Int Ya = {}; Ev ` Z Int Za = {} |]
   ==> Ev ` (Y - X) Int (Ya Un Za) = {}"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: inj_image_diff_dist inj_Ev)
 apply (simp add: in_Ev_set)
 apply (elim conjE exE)

 apply (erule disjE)
  apply (fast)
    (* *)
  apply (simp)
   apply (case_tac "Ev a : Ya")
   apply (fast)
   apply (rotate_tac 1)
   apply (erule equalityE)
   apply (rotate_tac -1)
   apply (erule subsetE)
   apply (drule_tac x="Ev a" in bspec, fast)
   apply (simp)
  apply (fast)
done

(* set 3 *)

lemma domF_Parallel_step_set3:
  "[| Ya - insert Tick (Ev ` X) = Za - insert Tick (Ev ` X) ;
       Ev ` Y Int Ya = {}; Ev ` Z Int Za = {} |]
   ==> Ev ` (Z - X) Int (Ya Un Za) = {}"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: inj_image_diff_dist inj_Ev)
 apply (simp add: in_Ev_set)
 apply (elim conjE exE)
 apply (erule disjE)
  apply (simp)
   apply (case_tac "Ev a : Za")
   apply (fast)
   apply (rotate_tac 1)
   apply (erule equalityE)
   apply (erule subsetE)
   apply (drule_tac x="Ev a" in bspec, fast)
   apply (simp)
  apply (fast)
    (* *)
  apply (simp)
done

(* set 4 *)

lemma domF_Parallel_step_set4:
  "Ev ` (X Int Y Int Z Un (Y - X) Un (Z - X)) Int Xa = {} 
   ==> Xa =
       Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Y) Un
      (Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Z))"
by (auto)

(* set 5 *)

lemma domF_Parallel_step_set5:
  "Ev ` (X Int Y Int Z Un (Y - X) Un (Z - X)) Int Xa = {} 
   ==> Ev ` Y Int
      (Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Y)) = {} &
       Ev ` Z Int
      (Xa - insert Tick (Ev ` X) Un (Xa Int insert Tick (Ev ` X) - Ev ` Z)) = {}"
by (auto)

(* => *)

lemma domF_Parallel_step_sub: 
  "[[(? :Y -> Pf) |[X]| (? :Z -> Qf)]]F ev <=
   [[Parallel_step X Y Z Pf Qf]]F ev"
apply (rule)+
apply (simp add: Parallel_step_def)
apply (simp add: Parallel_mem Ext_pre_choice_mem)
apply (elim disjE conjE exE)

 (* (nil,nil) *)
 apply (simp add: image_Un Int_Un_distrib2)
 apply (simp add: domF_Parallel_step_set1
                  domF_Parallel_step_set2
                  domF_Parallel_step_set3)

 (* (nil,Ev) *)
 apply (simp)
 apply (insert trace_nil_or_Tick_or_Ev)
 apply (drule_tac x="s" in spec)
 apply (simp add: par_tr_not_None)

 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: par_tr_head)
 apply (elim conjE exE, simp)
 apply (simp add: not_None)
 
 apply (rule_tac x="aa" in exI)
 apply (rule_tac x="sc" in exI)
 apply (simp add: Conditional_mem)

 apply (case_tac "aa : Y")
  apply (simp add: Int_choice_mem)
  apply (rule disjI2)
  apply (simp add: Parallel_mem)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="[]t" in exI)
  apply (rule_tac x="sb" in exI)
  apply (simp add: Ext_pre_choice_mem)
  (* "aa ~: Y" *)
  apply (simp add: Parallel_mem)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="[]t" in exI)
  apply (rule_tac x="sb" in exI)
  apply (simp add: Ext_pre_choice_mem)

 (* (Ev,nil) *)
 apply (simp)
 apply (drule_tac x="s" in spec)
 apply (simp add: par_tr_not_None)

 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: par_tr_head)
 apply (elim conjE exE, simp)
 apply (simp add: not_None)
 
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sc" in exI)
 apply (simp add: Conditional_mem)

 apply (case_tac "a : Z")
  apply (simp add: Int_choice_mem)
  apply (rule disjI1)
  apply (simp add: Parallel_mem)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="[]t" in exI)
  apply (simp add: Ext_pre_choice_mem)
  (* "a ~: Z" *)
  apply (simp add: Parallel_mem)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="[]t" in exI)
  apply (simp add: Ext_pre_choice_mem)

 (* (Ev,Ev) *)
 apply (simp)
 apply (drule_tac x="s" in spec)
 apply (simp add: par_tr_not_None)

 apply (erule disjE, simp)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: par_tr_head)
 apply (elim disjE conjE exE, simp)

  (* sync *)
  apply (simp add: not_None)
  apply (rule_tac x="aa" in exI)
  apply (rule_tac x="sd" in exI)
  apply (simp add: Conditional_mem)
  apply (simp add: Parallel_mem)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="sc" in exI)
  apply (simp)

  (* left *)
  apply (simp add: not_None)
  apply (rule_tac x="a" in exI)
  apply (rule_tac x="sd" in exI)
  apply (simp add: Conditional_mem)

  apply (case_tac "a : Z")
   apply (simp add: Int_choice_mem)
   apply (rule disjI1)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[Ev aa]t @t sc" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
   (* "a ~: Z" *)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[Ev aa]t @t sc" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)

  (* right *)
  apply (simp add: not_None)
  apply (rule_tac x="aa" in exI)
  apply (rule_tac x="sd" in exI)
  apply (simp add: Conditional_mem)

  apply (case_tac "aa : Y")
   apply (simp add: Int_choice_mem)
   apply (rule disjI2)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="[Ev a]t @t sb" in exI)
   apply (rule_tac x="sc" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
   (* "aa ~: Y" *)
   apply (simp add: Parallel_mem)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="[Ev a]t @t sb" in exI)
   apply (rule_tac x="sc" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
done

(* => *)

lemma domF_Parallel_step_sup: 
  "[[Parallel_step X Y Z Pf Qf]]F ev <= 
   [[(? :Y -> Pf) |[X]| (? :Z -> Qf)]]F ev"
apply (rule)
apply (simp add: Parallel_step_def)
apply (simp add: Ext_pre_choice_mem)
apply (elim disjE conjE exE)

 (* nil *)
 apply (simp add: Parallel_mem)
 apply (rule_tac x="(Xa - insert Tick (Ev ` X)) Un
                   ((Xa Int insert Tick (Ev ` X)) - Ev ` Y)" in exI)
 apply (rule_tac x="(Xa - insert Tick (Ev ` X)) Un
                   ((Xa Int insert Tick (Ev ` X)) - Ev ` Z)" in exI)
 apply (simp add: domF_Parallel_step_set4)
 apply (rule conjI, force)
 apply (simp add: Ext_pre_choice_mem)
 apply (simp add: domF_Parallel_step_set5)

 (* sync *)
 apply (simp add: Conditional_mem)
 apply (simp add: Parallel_mem)
 apply (elim conjE exE, simp)
 apply (rule_tac x="Ya" in exI)
 apply (rule_tac x="Za" in exI)
 apply (simp)
 apply (rule_tac x="[Ev a]t @t sb" in exI)
 apply (rule_tac x="[Ev a]t @t t" in exI)
 apply (simp add: par_tr_head)
 apply (simp add: Ext_pre_choice_mem)
 apply (fast)

 (* left *)
 apply (simp add: Conditional_mem)
 apply (case_tac "a : Z")
  apply (simp add: Int_choice_mem)
  apply (erule disjE)
   apply (simp add: Parallel_mem)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="[Ev a]t @t sb" in exI)
   apply (rule_tac x="t" in exI)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
   (* *)
   apply (simp add: Parallel_mem)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[Ev a]t @t t" in exI)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
  (* "a ~: Z" *)
  apply (simp add: Conditional_mem)
  apply (simp add: Parallel_mem)
  apply (elim conjE exE, simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="[Ev a]t @t sb" in exI)
  apply (rule_tac x="t" in exI)
  apply (simp add: par_tr_head)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)

 (* right *)
 apply (simp add: Conditional_mem)
 apply (case_tac "a : Y")
  apply (simp add: Int_choice_mem)
  apply (erule disjE)
   apply (simp add: Parallel_mem)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="[Ev a]t @t sb" in exI)
   apply (rule_tac x="t" in exI)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
   (* *)
   apply (simp add: Parallel_mem)
   apply (elim conjE exE, simp)
   apply (rule_tac x="Ya" in exI)
   apply (rule_tac x="Za" in exI)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="[Ev a]t @t t" in exI)
   apply (simp add: par_tr_head)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
  (* "a ~: Y" *)
  apply (simp add: Conditional_mem)
  apply (simp add: Parallel_mem)
  apply (elim conjE exE, simp)
  apply (rule_tac x="Ya" in exI)
  apply (rule_tac x="Za" in exI)
  apply (simp)
  apply (rule_tac x="sb" in exI)
  apply (rule_tac x="[Ev a]t @t t" in exI)
  apply (simp add: par_tr_head)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
done

(* domF *)

lemma domF_Parallel_step: 
  "[[(? :Y -> Pf) |[X]| (? :Z -> Qf)]]F ev =
   [[Parallel_step X Y Z Pf Qf]]F ev"
apply (rule eq_iffI)
apply (simp add: domF_Parallel_step_sub)
apply (simp add: domF_Parallel_step_sup)
done

(*** domSF ***)

lemma domSF_Parallel_step:
  "[[(? :Y -> Pf) |[X]| (? :Z -> Qf)]]SF ev =
   [[Parallel_step X Y Z Pf Qf]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Parallel_step)
apply (simp add: domF_Parallel_step)
done

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

lemma csp_Parallel_step: 
  "LET:fp df IN (? :Y -> Pf) |[X]| (? :Z -> Qf) =F
   LET:fp df IN Parallel_step X Y Z Pf Qf"
apply (induct fp)
by (simp_all add: eqF_def domSF_Parallel_step)

(*********************************************************
                      Hide expansion
 *********************************************************)

(*** domT ***)

lemma domT_Hiding_step: 
  "[[(? :Y -> Pf) -- X]]T ev =
   [[Hiding_step X Y Pf]]T ev"
apply (simp add: Hiding_step_def)
apply (rule eq_iffI)

 (* => *)
 apply (rule)
 apply (simp add: Hiding_mem)
 apply (elim conjE exE)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE, simp)
 apply (elim conjE exE)

 apply (case_tac "Y Int X = {}")
  apply (simp)
  apply (case_tac "a : X", fast)
  apply (simp add: Conditional_mem)
  apply (simp add: Ext_pre_choice_mem)
  apply (rule_tac x="a" in exI)
  apply (rule_tac x="sa --tr X" in exI)
  apply (simp add: Hiding_mem)
  apply (fast)
  (* Y Int X ~= {} *)
  apply (simp add: Conditional_mem)
  apply (simp add: Timeout_mem)
  apply (case_tac "a : X")
   apply (rule disjI2)
   apply (simp add: Rep_int_choice_mem)
   apply (rule disjI2)
   apply (rule_tac x="a" in exI)
   apply (simp add: Hiding_mem)
   apply (fast)
  (* a ~: X *)
   apply (rule disjI1)
   apply (simp add: Ext_pre_choice_mem)
   apply (rule_tac x="a" in exI)
   apply (rule_tac x="sa --tr X" in exI)
   apply (simp add: Hiding_mem)
   apply (fast)

 (* <= *)
 apply (rule)
 apply (case_tac "Y Int X = {}")
  apply (simp add: Conditional_mem)
  apply (simp add: Ext_pre_choice_mem)
  apply (erule disjE, simp)
  apply (elim conjE exE)
  apply (simp add: Hiding_mem)
  apply (elim conjE exE)
  apply (simp add: Ext_pre_choice_mem)
  apply (case_tac "a : X", fast)
  apply (rule_tac x="[Ev a]t @t sa" in exI)
  apply (simp)
  apply (fast)
 (* Y Int X = {} *)
  apply (simp add: Conditional_mem)
  apply (simp add: Timeout_mem)
  apply (erule disjE)
  (* a~:X *)
   apply (simp add: Ext_pre_choice_mem)
   apply (erule disjE, simp)
   apply (simp add: Hiding_mem)
   apply (elim conjE exE)
   apply (rule_tac x="[Ev a]t @t sa" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
  (* a:X *)
   apply (simp add: Rep_int_choice_mem)
   apply (erule disjE, simp)
   apply (simp add: Hiding_mem)
   apply (elim conjE exE)
   apply (rule_tac x="[Ev a]t @t s" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
done

(*** domF ***)

lemma domF_Hiding_step: 
  "[[(? :Y -> Pf) -- X]]F ev =
   [[Hiding_step X Y Pf]]F ev"
apply (simp add: Hiding_step_def)
apply (rule eq_iffI)

 (* => *)
 apply (rule)
 apply (simp add: Hiding_mem)
 apply (elim conjE exE)
 apply (simp add: Ext_pre_choice_mem)
 apply (erule disjE)
  (* not hidden *)
  apply (simp)
  apply (case_tac "Y Int X ~= {}", fast)
  apply (simp add: Conditional_mem)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
  (* hidden *)
  apply (elim conjE exE)
  apply (case_tac "a : X")
  apply (case_tac "Y Int X = {}", fast)
   apply (simp add: Conditional_mem)
   apply (simp add: Timeout_mem)
   apply (rule disjI1)
   apply (simp add: Rep_int_choice_mem)
   apply (simp add: Hiding_mem)
   apply (fast)
  (* a ~: X *)
   apply (case_tac "Y Int X = {}")
    apply (simp add: Conditional_mem)
    apply (simp add: Ext_pre_choice_mem)
    apply (simp add: Hiding_mem)
    apply (fast)
   (* Y Int X ~= {} *)
    apply (simp add: Conditional_mem)
    apply (simp add: Timeout_mem)
    apply (rule disjI2)
    apply (simp add: Ext_pre_choice_mem)
    apply (simp add: Hiding_mem)
    apply (fast)

 (* <= *)
 apply (rule)
 apply (simp add: Conditional_mem)
 apply (case_tac "Y Int X = {}")
  apply (simp add: Ext_pre_choice_mem)
  apply (erule disjE)
   apply (simp add: Hiding_mem)
   apply (rule_tac x="[]t" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
  (* *)
   apply (simp add: Hiding_mem)
   apply (elim conjE exE)
   apply (case_tac "a : X", fast)
   apply (rule_tac x="[Ev a]t @t sb" in exI)
   apply (simp add: Ext_pre_choice_mem)
   apply (fast)
 (* Y Int X ~= {} *)
 apply (simp add: Timeout_mem)
 apply (elim disjE)
  (* 1 *)
  apply (simp add: Rep_int_choice_mem)
  apply (simp add: Hiding_mem)
  apply (elim conjE exE)
  apply (rule_tac x="[Ev a]t @t sa" in exI)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
  (* 2 *)
  apply (simp add: Ext_pre_choice_mem)
  apply (elim conjE, simp)
  apply (simp add: Hiding_mem)
  apply (elim conjE exE)
  apply (rule_tac x="[Ev a]t @t sb" in exI)
  apply (simp add: Ext_pre_choice_mem)
  apply (fast)
  (* 3 *)
  apply (simp add: Ext_pre_choice_mem)
done

(*** domSF ***)

lemma domSF_Hiding_step: 
  "[[(? :Y -> Pf) -- X]]SF ev =
   [[Hiding_step X Y Pf]]SF ev"
apply (simp add: proc_eqSF_decompo)
apply (simp add: domT_Hiding_step)
apply (simp add: domF_Hiding_step)
done

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

lemma csp_Hiding_step: 
  "LET:fp df IN (? :Y -> Pf) -- X =F
   LET:fp df IN Hiding_step X Y Pf"
apply (induct fp)
by (simp_all add: eqF_def domSF_Hiding_step)

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

declare not_None_eq    [simp]

end