Theory CSP_T_law_step

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T

theory CSP_T_law_step
imports CSP_T_traces
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   June 2005  (modified)   |
            |              September 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_law_step = CSP_T_traces:

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

         1. step laws
         2.
         3. 
         4. 

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

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

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

lemma cspT_STOP_step: "STOP =T ? :{} -> Pf"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done

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

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

lemma cspT_Act_prefix_step: "a -> P =T ? x:{a} -> P"
apply (simp add: cspT_semantics)
apply (simp add: traces_def)
done

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

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

lemma cspT_Ext_choice_step:
  "(? :X -> Pf) [+] (? :Y -> Qf) =T
      ? x:(X Un Y) -> 
                (IF (x : X & x : Y) THEN Pf x |~| Qf x
                 ELSE IF (x : X) THEN Pf x
                 ELSE Qf x)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" in exI)
 apply (simp)

 apply (rule_tac x="a" in exI)
 apply (rule_tac x="s" in exI)
 apply (simp)

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE)
 apply (simp_all)

 apply (case_tac "a : Y")
 apply (simp_all add: in_traces)

 apply (case_tac "a : X")
 apply (simp_all add: in_traces)
done

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

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

lemma cspT_Parallel_step: 
  "(? :Y -> Pf) |[X]| (? :Z -> Qf) =T
      ? 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)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

 (* <> *)
  apply (simp)

 (* [Tick]t *)
  apply (simp add: in_traces)

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

  (* 1 *)
  apply (simp)

  (* 2 *)
  apply (simp add: par_tr_head)
  apply (elim conjE exE)
  apply (case_tac "a : Y")
   apply (simp)
   apply (rule disjI2)
   apply (rule_tac x="<>" in exI)
   apply (rule_tac x="sb" in exI)
   apply (simp)
   (* a ~: Y *)
   apply (simp)
   apply (rule_tac x="<>" in exI)
   apply (rule_tac x="sb" in exI)
   apply (simp)

  (* 3 *)
  apply (simp add: par_tr_head)
  apply (elim conjE exE)
  apply (case_tac "a : Z")
   apply (simp)
   apply (rule disjI1)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="<>" in exI)
   apply (simp)
   (* a ~: Z *)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="<>" in exI)
   apply (simp)

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

   (* 4-1 *)
   apply (simp)
   apply (rule_tac x="sb" in exI)
   apply (rule_tac x="sc" in exI)
   apply (simp)

   (* 4-2 *)
   apply (case_tac "a : Z")
    apply (simp)
    apply (rule disjI1)
    apply (rule_tac x="sb" in exI)
    apply (rule_tac x="<Ev ab> ^^ sc" in exI)
    apply (simp)
    (* a ~: Z *)
    apply (simp)
    apply (rule_tac x="sb" in exI)
    apply (rule_tac x="<Ev ab> ^^ sc" in exI)
    apply (simp)

   (* 4-3 *)
   apply (simp)
   apply (case_tac "a : Y")
    apply (simp)
    apply (rule disjI2)
    apply (rule_tac x="<Ev aa> ^^ sb" in exI)
    apply (rule_tac x="sc" in exI)
    apply (simp)
    (* a ~: Y *)
    apply (simp)
    apply (rule_tac x="<Ev aa> ^^ sb" in exI)
    apply (rule_tac x="sc" in exI)
    apply (simp)

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

 (* <> *)
  apply (simp)

 (* [Tick]t *)
  apply (simp add: in_traces)

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

  (* 1 *)
  apply (simp add: in_traces)
  apply (elim conjE exE)
  apply (rule_tac x="<Ev a> ^^ sa" in exI)
  apply (rule_tac x="<Ev a> ^^ ta" in exI)
  apply (simp add: par_tr_head)

  (* 2 *)
  apply (simp add: in_traces)
  apply (case_tac "a : Z")
   apply (simp add: in_traces)
   apply (erule disjE)

    apply (elim conjE exE)
    apply (rule_tac x="<Ev a> ^^ sa" in exI)
    apply (rule_tac x="ta" in exI)
    apply (simp add: par_tr_head)

    apply (elim conjE exE)
    apply (rule_tac x="sa" in exI)
    apply (rule_tac x="<Ev a> ^^ ta" in exI)
    apply (simp add: par_tr_head)

  (* 3 *)
  apply (simp add: in_traces)
  apply (elim conjE exE)

   apply (rule_tac x="<Ev a> ^^ sa" in exI)
   apply (rule_tac x="ta" in exI)
   apply (simp add: par_tr_head)

   apply (simp add: in_traces)
   apply (case_tac "a : Y")

    apply (simp add: in_traces)
    apply (erule disjE)
     apply (elim conjE exE)
     apply (rule_tac x="<Ev a> ^^ sa" in exI)
     apply (rule_tac x="ta" in exI)
     apply (simp add: par_tr_head)
     (* *)
     apply (elim conjE exE)
     apply (rule_tac x="sa" in exI)
     apply (rule_tac x="<Ev a> ^^ ta" in exI)
     apply (simp add: par_tr_head)

    apply (simp add: in_traces)
    apply (elim conjE exE)
    apply (rule_tac x="sa" in exI)
    apply (rule_tac x="<Ev a> ^^ ta" in exI)
    apply (simp add: par_tr_head)
done

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

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

lemma cspT_Hiding_step: 
  "(? :Y -> Pf) -- X =T
      IF (Y Int X = {}) THEN (? x:Y -> (Pf x -- X))
                         ELSE ((? x:(Y-X) -> (Pf x -- X)) 
                               [> (! x:(Y Int X) .. (Pf x -- X)))"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

 apply (case_tac "Y Int X = {}")
  apply (simp)
  apply (case_tac "a : X", fast)
  apply (simp)
  apply (rule_tac x="sa" in exI)
  apply (simp)

  (* Y Int X ~= {} *)
  apply (simp)
  apply (case_tac "a : X")
   apply (simp)
   apply (fast)
  (* a ~: X *)
   apply (simp)
   apply (fast)

 (* <= *)
 apply (rule)
 apply (case_tac "Y Int X = {}")
  apply (simp add: in_traces)
  apply (erule disjE, simp)
   apply (rule_tac x="<>" in exI)
   apply (simp)

  apply (elim conjE exE)
  apply (case_tac "a : X", fast)
   apply (rule_tac x="<Ev a> ^^ sa" in exI)
   apply (simp)

 (* Y Int X = {} *)
  apply (simp add: in_traces)
  apply (erule disjE, simp)
   apply (rule_tac x="<>" in exI)
   apply (simp)

  apply (erule disjE)
  (* a~:X *)
   apply (elim conjE exE)
   apply (rule_tac x="<Ev a> ^^ sa" in exI)
   apply (simp)
  (* a:X *)
   apply (erule disjE, simp)
    apply (rule_tac x="<>" in exI)
    apply (simp)

   apply (elim conjE exE bexE)
   apply (rule_tac x="<Ev a> ^^ s" in exI)
   apply (simp)
done

(*********************************************************
                    Renaming expansion
 *********************************************************)

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

lemma cspT_Renaming_step:
  "(? :X -> Pf) [[r]] =T 
    ? y:(r `` X) -> (! x:{x. x:X & (x,y):r} .. (Pf x)[[r]])"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

(* => *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE)
  (* 1 *)
  apply (simp)

  (* 2 *)
  apply (rule disjI2)
  apply (simp add: ren_tr_decompo)
  apply (elim conjE exE)
  apply (rule_tac x="b" in exI)
  apply (rule_tac x="ta" in exI)
  apply (simp)
  apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE, simp)
 apply (elim disjE conjE exE)
  apply (simp add: Image_iff)
  apply (erule bexE)
  apply (rule_tac x="<Ev x>" in exI)
  apply (simp)
 (* *)
  apply (rule_tac x="<Ev aa> ^^ sa" in exI)
  apply (simp)
done

(*********************************************************
            Sequential composition expansion
 *********************************************************)

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

lemma cspT_Seq_compo_step: 
  "(? :X -> Pf) ;; Q =T ? x:X -> (Pf x ;; Q)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

  (* 1 *)
 apply (fast)

  (* 2 *)
 apply (insert trace_last_nil_or_unnil)
 apply (drule_tac x="sa" in spec)
 apply (erule disjE, simp)
 apply (elim conjE exE, simp)
 apply (simp add: appt_assoc_sym)
 apply (rule_tac x="a" in exI)
 apply (rule_tac x="sb ^^ ta" in exI)
 apply (simp add: appt_assoc)
 apply (fast)

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (erule disjE, simp)
 apply (rule disjI1)
 apply (rule_tac x="<>" in exI)
 apply (simp)
 apply (elim disjE conjE exE)

 (* 1 *)
  apply (rule disjI1)
  apply (rule_tac x="<Ev a> ^^ sa" in exI, simp)

 (* 2 *)
  apply (rule disjI2)
  apply (rule_tac x="<Ev a> ^^ sa" in exI)
  apply (rule_tac x="ta" in exI)
  apply (simp add: appt_assoc)
done

(*********************************************************
                    Depth_rest expansion
 *********************************************************)

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

lemma cspT_Depth_rest_step:
  "(? :X -> Pf) |. (Suc n) =T ? x:X -> (Pf x |. n)"
apply (simp add: cspT_semantics)
apply (rule order_antisym)

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

(* <= *)
 apply (rule)
 apply (simp add: in_traces)
 apply (elim disjE conjE exE)
 apply (simp_all)
done

(*********************************************************)

lemmas cspT_step = cspT_STOP_step       cspT_Act_prefix_step 
                   cspT_Ext_choice_step cspT_Parallel_step
                   cspT_Hiding_step     cspT_Renaming_step
                   cspT_Seq_compo_step  cspT_Depth_rest_step

lemmas cspT_light_step = cspT_STOP_step  cspT_Act_prefix_step 

end

lemma cspT_STOP_step: 

  STOP =T ? :{} -> Pf

lemma cspT_Act_prefix_step: 

  a -> P =T ? x:{a} -> P

lemma cspT_Ext_choice_step: 

  ? :X -> Pf [+] ? :Y -> Qf =T 
  ? x:(X ∪ Y) 
   -> IF (x ∈ X ∧ x ∈ Y) THEN Pf x |~| Qf x ELSE IF (x ∈ X) THEN Pf x ELSE Qf x

lemma cspT_Parallel_step: 

  ? :Y -> Pf |[X]| ? :Z -> Qf =T 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf ELSE ? :Y -> Pf |[X]| Qf x

lemma cspT_Hiding_step: 

  (? :Y -> Pf) -- X =T 
  IF (Y ∩ X = {}) THEN ? x:Y -> Pf x -- X 
  ELSE ? x:(Y - X) -> Pf x -- X [> (! x:(Y ∩ X) .. Pf x -- X)

lemma cspT_Renaming_step: 

  (? :X -> Pf) [[r]] =T ? y:(r `` X) -> (! x:{x : X. (x, y) ∈ r} .. Pf x [[r]])

lemma cspT_Seq_compo_step: 

  ? :X -> Pf ;; Q =T ? x:X -> (Pf x ;; Q)

lemma cspT_Depth_rest_step: 

  (? :X -> Pf) |. Suc n =T ? x:X -> Pf x |. n

lemmas cspT_step: 

  STOP =T ? :{} -> Pf
  a -> P =T ? x:{a} -> P
  ? :X -> Pf [+] ? :Y -> Qf =T 
  ? x:(X ∪ Y) 
   -> IF (x ∈ X ∧ x ∈ Y) THEN Pf x |~| Qf x ELSE IF (x ∈ X) THEN Pf x ELSE Qf x
  ? :Y -> Pf |[X]| ? :Z -> Qf =T 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf ELSE ? :Y -> Pf |[X]| Qf x
  (? :Y -> Pf) -- X =T 
  IF (Y ∩ X = {}) THEN ? x:Y -> Pf x -- X 
  ELSE ? x:(Y - X) -> Pf x -- X [> (! x:(Y ∩ X) .. Pf x -- X)
  (? :X -> Pf) [[r]] =T ? y:(r `` X) -> (! x:{x : X. (x, y) ∈ r} .. Pf x [[r]])
  ? :X -> Pf ;; Q =T ? x:X -> (Pf x ;; Q)
  (? :X -> Pf) |. Suc n =T ? x:X -> Pf x |. n

lemmas cspT_step: 

  STOP =T ? :{} -> Pf
  a -> P =T ? x:{a} -> P
  ? :X -> Pf [+] ? :Y -> Qf =T 
  ? x:(X ∪ Y) 
   -> IF (x ∈ X ∧ x ∈ Y) THEN Pf x |~| Qf x ELSE IF (x ∈ X) THEN Pf x ELSE Qf x
  ? :Y -> Pf |[X]| ? :Z -> Qf =T 
  ? x:(X ∩ Y ∩ Z ∪ (Y - X) ∪ (Z - X)) 
   -> IF (x ∈ X) THEN Pf x |[X]| Qf x 
      ELSE IF (x ∈ Y ∧ x ∈ Z) 
           THEN Pf x |[X]| ? :Z -> Qf |~| ? :Y -> Pf |[X]| Qf x 
           ELSE IF (x ∈ Y) THEN Pf x |[X]| ? :Z -> Qf ELSE ? :Y -> Pf |[X]| Qf x
  (? :Y -> Pf) -- X =T 
  IF (Y ∩ X = {}) THEN ? x:Y -> Pf x -- X 
  ELSE ? x:(Y - X) -> Pf x -- X [> (! x:(Y ∩ X) .. Pf x -- X)
  (? :X -> Pf) [[r]] =T ? y:(r `` X) -> (! x:{x : X. (x, y) ∈ r} .. Pf x [[r]])
  ? :X -> Pf ;; Q =T ? x:X -> (Pf x ;; Q)
  (? :X -> Pf) |. Suc n =T ? x:X -> Pf x |. n

lemmas cspT_light_step: 

  STOP =T ? :{} -> Pf
  a -> P =T ? x:{a} -> P

lemmas cspT_light_step: 

  STOP =T ? :{} -> Pf
  a -> P =T ? x:{a} -> P