Theory CSP_semantics

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

theory CSP_semantics = CSP_syntax + Domain_SF_prod
                     + Trace_par + Trace_hide + Trace_ren + Trace_seq:

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

         1. semantic clause
         2. 
         3. 
         4. 

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

consts
  evalT  :: "('n,'a) proc => ('n,'a) domSF_prod => 'a domT"  ("[[_]]T")
  evalF  :: "('n,'a) proc => ('n,'a) domSF_prod => 'a domF"  ("[[_]]F")
  evalSF :: "('n,'a) proc => ('n,'a) domSF_prod => 'a domSF" ("[[_]]SF")

primrec
  "[[STOP]]T       = (%ev. {[]t}t)"

  "[[SKIP]]T       = (%ev. {[]t, [Tick]t}t)"

  "[[DIV]]T        = (%ev. {[]t}t)"

  "[[a -> P]]T     = (%ev. {t. t = []t | 
                              (EX s. t = [Ev a]t @t s & s :t [[P]]T ev) }t)"

  "[[? :X -> Pf]]T = (%ev. {t. t = []t | 
                              (EX a s. t = [Ev a]t @t s & 
                                       s :t [[Pf a]]T ev & a : X) }t)"

  "[[P [+] Q]]T    = (%ev. [[P]]T ev UnT [[Q]]T ev)"

  "[[P |~| Q]]T    = (%ev. [[P]]T ev UnT [[Q]]T ev)"

  "[[! :X .. Pf]]T = (%ev. {t. t = []t | (EX a. t :t [[Pf a]]T ev & a : X) }t)"

  "[[IF b THEN P ELSE Q]]T = (%ev. (if b then ([[P]]T ev) else ([[Q]]T ev)))"

  "[[P |[X]| Q]]T  = (%ev. {u. EX s t. u : s |[X]|tr t & 
                               s :t [[P]]T ev & t :t [[Q]]T ev }t)"

  "[[P -- X]]T     = (%ev. {t. EX s. t = s --tr X & s :t [[P]]T ev }t)"

  "[[P [[r]]]]T    = (%ev. {t. EX s. s [[r]]tr t & s :t [[P]]T ev }t)"

  "[[P ;; Q]]T     = (%ev. {u. (EX s. u = rmtick s & s :t [[P]]T ev) |
                               (EX s t. u = s @t t & 
                                        s @t [Tick]t :t [[P]]T ev & t :t [[Q]]T ev) }t)"

  "[[<C>]]T        = (%ev. fstSF (ev C))"

primrec
  "[[STOP]]F       = (%ev. {f. EX X. f = ([]t, X) }f)"

  "[[SKIP]]F       = (%ev. {f. (EX X. f = ([]t, X) & X <= Evset) |
                               (EX X. f = ([Tick]t, X)) }f)"

  "[[DIV]]F        = (%ev. {}f)"

  "[[a -> P]]F     = (%ev. {f. (EX X.   f = ([]t,X) & Ev a ~: X) |
                               (EX s X. f = ([Ev a]t @t s, X) & (s,X) :f [[P]]F ev) }f)"

  "[[? :X -> Pf]]F = (%ev. {f. (EX Y.     f = ([]t,Y) & Ev`X Int Y = {}) |
                               (EX a s Y. f = ([Ev a]t @t s, Y) & 
                                          (s,Y) :f [[Pf a]]F ev & a : X) }f)"

  "[[P [+] Q]]F    = (%ev. {f. (EX   X. f = ([]t,X) & f :f [[P]]F ev IntF [[Q]]F ev) |
                               (EX s X. f = (s,X)   & f :f [[P]]F ev UnF  [[Q]]F ev & 
                                        s ~= []t) |
                               (EX   X. f = ([]t,X) & [Tick]t :t [[P]]T ev UnT [[Q]]T ev &
                                        X <= Evset) }f)"

  "[[P |~| Q]]F    = (%ev. [[P]]F ev UnF [[Q]]F ev)"

  "[[! :X .. Pf]]F = (%ev. {f. EX a. f :f [[Pf a]]F ev & a : X }f )"

  "[[IF b THEN P ELSE Q]]F = (%ev. (if b then ([[P]]F ev) else ([[Q]]F ev)))"

  "[[P |[X]| Q]]F  = (%ev. {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) }f )"

  "[[P -- X]]F     = (%ev. {f. EX s Y. f = (s --tr X, Y) & 
                               (s,(Ev`X) Un Y) :f [[P]]F ev }f)"

  "[[P [[r]]]]F    = (%ev. {f. EX s t X. f = (t,X) & s [[r]]tr t & 
                               (s, [[r]]inv X) :f [[P]]F ev }f)"

  "[[P ;; Q]]F     = (%ev. {f. (EX t X.   f = (t,X) & (t, X Un {Tick}) :f [[P]]F ev &
                                          notick t) |
                               (EX s t X. f = (s @t t,X) & s @t [Tick]t :t [[P]]T ev & 
                                          (t, X) :f [[Q]]F ev) }f)"

  "[[<C>]]F        = (%ev. sndSF (ev C))"

declare evalT.simps [simp del]
declare evalF.simps [simp del]

lemmas evalT_def = evalT.simps
lemmas evalF_def = evalF.simps

defs
  evalSF_def : "[[P]]SF == (%ev. ([[P]]T ev ,, [[P]]F ev))"

(*********************************************************
             process definition & recursion
 *********************************************************)

consts
  evalDF :: 
    "('n => ('m,'a) proc) => ('m,'a) domSF_prod 
                          => ('n,'a) domSF_prod"        ("[[_]]DF")
defs
  evalDF_def :  "[[df]]DF == (%ev. (%C. [[df C]]SF ev))"

consts
  evalRC ::
    "('n,'a) procRC => 'a domSF"                   ("[[_]]RC")

recdef evalRC "measure (%x. 0)"
  "[[LET:Ufp df IN P]]RC = [[P]]SF (UFP [[df]]DF)"
  "[[LET:Lfp df IN P]]RC = [[P]]SF (LFP [[df]]DF)"

(*** proj_fun ***)

lemma proj_fun_evalDF: "proj_fun C o [[df]]DF = [[df C]]SF"
apply (simp add: proj_fun_def)
apply (simp add: evalDF_def)
apply (simp add: expand_fun_eq)
done

lemma evalSF_evalDF:
   "[[df C]]SF ev = ([[df]]DF ev) C"
apply (simp add: evalDF_def)
done

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

consts
  refF :: "('n,'a) procRC => ('m,'a) procRC => bool"
                                           ("(0_ /<=F /_)" [50,50] 50)
  eqF  :: "('n,'a) procRC => ('m,'a) procRC => bool"
                                           ("(0_ /=F /_)" [50,50] 50)

defs
  refF_def : "R1 <=F R2 == [[R2]]RC <= [[R1]]RC"
  eqF_def  : "R1  =F R2 == [[R1]]RC  = [[R2]]RC"

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

syntax (output)
  "_refRCX"    :: "('n,'a) procRC => ('m,'a) procRC => bool"
                   ("(0_ /<=F /_)" [50,50] 50)

syntax (xsymbols)
  "_refRCX"    :: "('n,'a) procRC => ('m,'a) procRC => bool"
                   ("(0_ /\<sqsubseteq>F /_)" [50,50] 50)

translations
  "R1 \<sqsubseteq>F R2"            == "R1 <=F R2"

(*** lemmas ***)

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

(*** eq and ref ***)

lemma csp_eq_ref_iff:
  "(R1 =F R2) = (R1 <=F R2 & R2 <=F R1)"
by (auto simp add: refF_def eqF_def)

lemma csp_eq_ref:
  "R1 =F R2 ==> R1 <=F R2"
by (simp add: csp_eq_ref_iff)

lemma csp_ref_eq:
  "[| R1 <=F R2 ; R2 <=F R1 |] ==> R1 =F R2"
by (simp add: csp_eq_ref_iff)

(*** reflexivity ***)

lemma csp_reflex_eq[simp]: "R =F R"
by (simp add: eqF_def)

lemma csp_reflex_ref[simp]: "R <=F R"
by (simp add: refF_def)

lemmas csp_reflex = csp_reflex_eq csp_reflex_ref

(*** symmetry ***)

lemma csp_sym: "R1 =F R2 ==> R2 =F R1"
by (simp add: eqF_def)

lemma csp_symE:
  "[| R1 =F R2 ; R2 =F R1 ==> Z |] ==> Z"
by (simp add: eqF_def)

(*** transitivity ***)

lemma csp_trans_left_eq: "[| R1 =F R2 ; R2 =F R3 |] ==> R1 =F R3"
by (simp add: eqF_def)

lemma csp_trans_left_ref: "[| R1 <=F R2 ; R2 <=F R3 |] ==> R1 <=F R3"
by (simp add: refF_def)

lemmas csp_trans_left = csp_trans_left_eq csp_trans_left_ref
lemmas csp_trans = csp_trans_left

lemma csp_trans_right_eq: "[| R2 =F R3 ; R1 =F R2 |] ==> R1 =F R3"
by (simp add: eqF_def)

lemma csp_trans_right_ref: "[| R2 <=F R3 ;  R1 <=F R2 |] ==> R1 <=F R3"
by (simp add: refF_def)

lemmas csp_trans_rught = csp_trans_right_eq csp_trans_right_ref

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

lemma csp_rw_left_eq:
  "[| R1 =F R2 ; R2 =F R3 |] ==> R1 =F R3"
by (simp add: eqF_def)

lemma csp_rw_left_ref:
  "[| R1 =F R2 ; R2 <=F R3 |] ==> R1 <=F R3"
by (simp add: refF_def eqF_def)

lemmas csp_rw_left = csp_rw_left_eq csp_rw_left_ref

lemma csp_rw_right_eq:
  "[| R3 =F R2 ; R1 =F R2 |] ==> R1 =F R3"
by (simp add: eqF_def)

lemma csp_rw_right_ref:
  "[| R3 =F R2 ; R1 <=F R2 |] ==> R1 <=F R3"
by (simp add: refF_def eqF_def)

lemmas csp_rw_right = csp_rw_right_eq csp_rw_right_ref

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

lemma csp_tr_left_eq: "[| R1 =F R2 ; R2 =F R3 |] ==> R1 =F R3"
by (simp add: eqF_def)

lemma csp_tr_left_ref: "[| R1 <=F R2 ; R2 <=F R3 |] ==> R1 <=F R3"
by (simp add: refF_def eqF_def)

lemmas csp_tr_left = csp_tr_left_eq csp_tr_left_ref

lemma csp_tr_right_eq: "[| R2 =F R3 ; R1 =F R2 |] ==> R1 =F R3"
by (simp add: eqF_def)

lemma csp_tr_right_ref: "[| R2 <=F R3 ; R1 <=F R2 |] ==> R1 <=F R3"
by (simp add: refF_def eqF_def)

lemmas csp_tr_right = csp_tr_right_eq csp_tr_right_ref

end