Theory CSP_T_semantics

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               December 2004               |
            |                   July 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_T_semantics = CSP_syntax + Domain_T_cms
                       + Trace_par + Trace_hide + Trace_ren + Trace_seq:

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

         1. semantic clause
         2. 
         3. 
         4. 

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

(*********************************************************
                    semantic clause
 *********************************************************)

consts
  traces  :: "'a proc => 'a domT"

primrec
  "traces(STOP)        = {<>}t"
  "traces(SKIP)        = {<>, <Tick>}t"
  "traces(DIV)         = {<>}t"
  "traces(a -> P)      = {t. t = <> | (EX s. t = <Ev a> ^^ s & s :t traces(P)) }t"

  "traces(? :X -> Pf)  = {t. t = <> | 
                            (EX a s. t = <Ev a> ^^ s & s :t traces(Pf a) & a : X) }t"

  "traces(P [+] Q)     = traces(P) UnT traces(Q)"
  "traces(P |~| Q)     = traces(P) UnT traces(Q)"
  "traces(!! :C .. Pf) = {t. t = <> | (EX c:C. t :t traces(Pf c)) }t"
  "traces(IF b THEN P ELSE Q) = (if b then traces(P) else traces(Q))"
  "traces(P |[X]| Q)   = {u. EX s t. u : s |[X]|tr t & s :t traces(P) & t :t traces(Q) }t"
  "traces(P -- X)      = {t. EX s. t = s --tr X & s :t traces(P) }t"
  "traces(P [[r]])     = {t. EX s. s [[r]]* t & s :t traces(P) }t"
  "traces(P ;; Q)      = {u. (EX s. u = rmTick s & s :t traces(P) ) |
                             (EX s t. u = s ^^ t & s ^^ <Tick> :t traces(P) &
                                      t :t traces(Q) & noTick s) }t"
  "traces(P |. n)      = traces(P) .|. n"

declare traces.simps [simp del]

lemma traces_Rep_int_choice_fun: 
  "inj f ==> traces(!!<f> :X .. Pf) = {t. t = <> | (EX a:X. t :t traces(Pf a)) }t"
apply (simp add: Rep_int_choice_fun_def)
apply (simp add: traces.simps)
done

lemma traces_Rep_int_choice_com: 
  "traces(! :X .. Pf) = {t. t = <> | (EX a:X. t :t traces(Pf a)) }t"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: traces_Rep_int_choice_fun)
apply (subgoal_tac 
  "ALL t. (EX a. (EX aa. a = {aa} & aa : X) & t :t traces (Pf (contents a)))
   = (EX a:X. t :t traces (Pf a))")
apply (simp)
apply (rule allI)
apply (rule)
apply (force)
apply (force)
done

lemmas traces_def = traces.simps
                    traces_Rep_int_choice_fun
                    traces_Rep_int_choice_com

lemma traces_Int_choice_Ext_choice: "traces(P |~| Q) = traces(P [+] Q)"
by (simp add: traces_def)

(*************************************************************
                   set of length of traces+
  lengthset is related to Depth restriction operator (P |. n) 
 *************************************************************)

consts
  lengthset   :: "'a proc => nat set"

defs
  lengthset_def:
    "lengthset P == {n. EX t. t :t traces P & 
                    (n = lengtht t | n = Suc (lengtht t) & noTick t)}"

(*********************************************************
                     semantics
 *********************************************************)

consts
  semT    :: "'a proc => 'a domT"      ("[[_]]T")

defs
  semT_def : "[[P]]T == traces(P)"

syntax (output)
  "_semT"  :: "'a proc => 'a domT"      ("[[_]]T")

syntax (xsymbols)
  "_semT"  :: "'a proc => 'a domT"      ("[|_|]T")

translations
  "[|P|]T" == "[[P]]T"

(*********************************************************
              relations over processes
 *********************************************************)

consts
  refT :: "'a proc => 'a proc => bool"
                                           ("(0_ /<=T /_)" [50,50] 50)
  eqT  :: "'a proc => 'a proc => bool"
                                           ("(0_ /=T /_)" [50,50] 50)
  refT_prod :: "('p => 'a proc) => ('p => 'a proc) => bool"
                                           ("(0_ /<=T' /_)" [50,50] 50)
  eqT_prod  :: "('p => 'a proc) => ('p => 'a proc) => bool"
                                           ("(0_ /=T' /_)" [50,50] 50)

defs
  refT_def : "P1 <=T P2 == [[P2]]T <= [[P1]]T"
  eqT_def  : "P1  =T P2 == [[P1]]T  = [[P2]]T"
  refT_prod_def : "f <=T' g == (ALL p. (f p) <=T (g p))"
  eqT_prod_def  : "f  =T' g == (ALL p. (f p)  =T (g p))"

(*------------------------------------*
 |              X-Symbols             |
 *------------------------------------*)

syntax (output)
  "_refTX"      :: "'a proc => 'a proc => bool"
                   ("(0_ /<=T /_)" [50,50] 50)
  "_refT_prodX" :: "('p => 'a proc) => ('p => 'a proc) => bool"
                   ("(0_ /<=T' /_)" [50,50] 50)

syntax (xsymbols)
  "_refTX"      :: "'a proc => 'a proc => bool"
                   ("(0_ /\<sqsubseteq>T /_)" [50,50] 50)
  "_refT_prodX" :: "('p => 'a proc) => ('p => 'a proc) => bool"
                   ("(0_ /\<sqsubseteq>T' /_)" [50,50] 50)

translations
  "P \<sqsubseteq>T Q" == "P <=T Q"
  "f \<sqsubseteq>T' g" == "f <=T' g"

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

(*** semantics ***)

lemma cspT_eqT_semantics:
  "(P =T Q) = (traces P = traces Q)"
by (simp add: eqT_def semT_def)

lemma cspT_refT_semantics:
  "(P <=T Q) = (traces Q <= traces P)"
by (simp add: refT_def semT_def)

lemma cspT_eqT_prod_semantics:
  "(f =T' g) = 
   (ALL p. traces (f p) = traces(g p))"
apply (simp add: eqT_prod_def)
apply (simp add: cspT_eqT_semantics)
done

lemma cspT_refT_prod_semantics:
  "(f <=T' g) = 
   (ALL p. traces (g p) <= traces(f p))"
apply (simp add: refT_prod_def)
apply (simp add: cspT_refT_semantics)
done

lemmas cspT_semantics = cspT_eqT_semantics  cspT_refT_semantics
                        cspT_eqT_prod_semantics cspT_refT_prod_semantics

(*** eq and ref ***)

lemma cspT_eq_ref_iff:
  "(P1 =T P2) = (P1 <=T P2 & P2 <=T P1)"
by (auto simp add: refT_def eqT_def intro:order_antisym)

lemma cspT_eq_ref:
  "P1 =T P2 ==> P1 <=T P2"
by (simp add: cspT_eq_ref_iff)

lemma cspT_ref_eq:
  "[| P1 <=T P2 ; P2 <=T P1 |] ==> P1 =T P2"
by (simp add: cspT_eq_ref_iff)

(*** reflexivity ***)

lemma cspT_reflex_eq[simp]: "P =T P"
by (simp add: eqT_def)

lemma cspT_reflex_ref[simp]: "P <=T P"
by (simp add: refT_def)

lemmas cspT_reflex = cspT_reflex_eq cspT_reflex_ref

(*** symmetry ***)

lemma cspT_sym: "P1 =T P2 ==> P2 =T P1"
by (simp add: eqT_def)

lemma cspT_symE:
  "[| P1 =T P2 ; P2 =T P1 ==> Z |] ==> Z"
by (simp add: eqT_def)

(*** transitivity ***)

lemma cspT_trans_left_eq: "[| P1 =T P2 ; P2 =T P3 |] ==> P1 =T P3"
by (simp add: eqT_def)

lemma cspT_trans_left_ref: "[| P1 <=T P2 ; P2 <=T P3 |] ==> P1 <=T P3"
by (simp add: refT_def)

lemmas cspT_trans_left = cspT_trans_left_eq cspT_trans_left_ref
lemmas cspT_trans = cspT_trans_left

lemma cspT_trans_right_eq: "[| P2 =T P3 ; P1 =T P2 |] ==> P1 =T P3"
by (simp add: eqT_def)

lemma cspT_trans_right_ref: "[| P2 <=T P3 ;  P1 <=T P2 |] ==> P1 <=T P3"
by (simp add: refT_def)

lemmas cspT_trans_rught = cspT_trans_right_eq cspT_trans_right_ref

(*** rewrite (eq) ***)

lemma cspT_rw_left_eq:
  "[| P1 =T P2 ; P2 =T P3 |] ==> P1 =T P3"
by (simp add: eqT_def)

lemma cspT_rw_left_ref:
  "[| P1 =T P2 ; P2 <=T P3 |] ==> P1 <=T P3"
by (simp add: refT_def eqT_def)

lemmas cspT_rw_left = cspT_rw_left_eq cspT_rw_left_ref

lemma cspT_rw_right_eq:
  "[| P3 =T P2 ; P1 =T P2 |] ==> P1 =T P3"
by (simp add: eqT_def)

lemma cspT_rw_right_ref:
  "[| P3 =T P2 ; P1 <=T P2 |] ==> P1 <=T P3"
by (simp add: refT_def eqT_def)

lemmas cspT_rw_right = cspT_rw_right_eq cspT_rw_right_ref

(*** rewrite (ref) ***)

lemma cspT_tr_left_eq: "[| P1 =T P2 ; P2 =T P3 |] ==> P1 =T P3"
by (simp add: eqT_def)

lemma cspT_tr_left_ref: "[| P1 <=T P2 ; P2 <=T P3 |] ==> P1 <=T P3"
by (simp add: refT_def eqT_def)

lemmas cspT_tr_left = cspT_tr_left_eq cspT_tr_left_ref

lemma cspT_tr_right_eq: "[| P2 =T P3 ; P1 =T P2 |] ==> P1 =T P3"
by (simp add: eqT_def)

lemma cspT_tr_right_ref: "[| P2 <=T P3 ; P1 <=T P2 |] ==> P1 <=T P3"
by (simp add: refT_def eqT_def)

lemmas cspT_tr_right = cspT_tr_right_eq cspT_tr_right_ref

end