Theory CSP_F_semantics

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

theory CSP_F_semantics = CSP_T_semantics + Domain_F_cms:

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

         1. semantic clause
         2. 
         3. 
         4. 

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

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

consts
  failures :: "'a proc => 'a setF"

primrec
  "failures(STOP)       = {f. EX X. f = (<>, X) }f"

  "failures(SKIP)       = {f. (EX X. f = (<>, X) & X <= Evset) |
                              (EX X. f = (<Tick>, X)) }f"
  "failures(DIV)        = {}f"

  "failures(a -> P)     = {f. (EX X.   f = (<>,X) & Ev a ~: X) |
                              (EX s X. f = (<Ev a> ^^ s, X) & (s,X) :f failures(P) ) }f"

  "failures(? :X -> Pf) = {f. (EX Y.     f = (<>,Y) & Ev`X Int Y = {}) |
                              (EX a s Y. f = (<Ev a> ^^ s, Y) & 
                                   (s,Y) :f failures(Pf a) & a : X) }f"

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

  "failures(P |~| Q)    = failures(P) UnF failures(Q)"

  "failures(!! :C .. Pf) = {f. EX c:C. f :f failures(Pf c)}f"

  "failures(IF b THEN P ELSE Q) = (if b then failures(P) else failures(Q))"

  "failures(P |[X]| Q)  = {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 failures(P) & 
                                                        (t,Z) :f failures(Q)) }f"
  "failures(P -- X)     = {f. EX s Y. f = (s --tr X, Y) & 
                                      (s,(Ev`X) Un Y) :f failures(P) }f"

  "failures(P [[r]])    = {f. EX s t X. f = (t,X) & s [[r]]* t & 
                                        (s, [[r]]inv X) :f failures(P) }f"

  "failures(P ;; Q)     = {f. (EX t X. f = (t,X) & (t, X Un {Tick}) :f failures(P) &
                                  noTick t) |
                              (EX s t X. f = (s ^^ t,X) & s ^^ <Tick> :t traces(P) & 
                                  (t, X) :f failures(Q) & noTick s) }f"

  "failures(P |. n)     = failures(P) .|. n"

declare failures.simps [simp del]

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

lemma failures_Rep_int_choice_com: 
  "failures(! :X .. Pf) = {f. EX a:X. f :f failures(Pf a)}f"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: failures_Rep_int_choice_fun)
apply (subgoal_tac 
  "ALL f. (EX a. (EX aa. a = {aa} & aa : X) & f :f failures (Pf (contents a)))
   = (EX a:X. f :f failures (Pf a))")
apply (simp (no_asm_simp))
apply (rule allI)
apply (rule)
apply (force)
apply (force)
done

lemmas failures_def = failures.simps
                      failures_Rep_int_choice_fun
                      failures_Rep_int_choice_com

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

consts
  semF    :: "'a proc => 'a domF"      ("[[_]]F")

defs
  semF_def : "[[P]]F == (traces(P) ,, failures(P))"

syntax (output)
  "_semF"  :: "'a proc => 'a domF"      ("[[_]]F")

syntax (xsymbols)
  "_semF"  :: "'a proc => 'a domF"      ("[|_|]F")

translations
  "[|P|]F" == "[[P]]F"

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

consts
  refF :: "'a proc => 'a proc => bool"
                                           ("(0_ /<=F /_)" [50,50] 50)
  eqF  :: "'a proc => 'a proc => bool"
                                           ("(0_ /=F /_)" [50,50] 50)
  refF_prod :: "('p => 'a proc) => ('p => 'a proc) => bool"
                                           ("(0_ /<=F' /_)" [50,50] 50)
  eqF_prod  :: "('p => 'a proc) => ('p => 'a proc) => bool"
                                           ("(0_ /=F' /_)" [50,50] 50)

defs
  refF_def : "P1 <=F P2 == [[P2]]F <= [[P1]]F"
  eqF_def  : "P1  =F P2 == [[P1]]F  = [[P2]]F"
  refF_prod_def : "f <=F' g == (ALL p. (f p) <=F (g p))"
  eqF_prod_def  : "f  =F' g == (ALL p. (f p)  =F (g p))"

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

syntax (output)
  "_refFX"      :: "'a proc => 'a proc => bool"
                   ("(0_ /<=F /_)" [50,50] 50)
  "_refF_prodX" :: "('p => 'a proc) => ('p => 'a proc) => bool"
                   ("(0_ /<=F' /_)" [50,50] 50)

syntax (xsymbols)
  "_refFX"    :: "'a proc => 'a proc => bool"
                   ("(0_ /\<sqsubseteq>F /_)" [50,50] 50)
  "_refF_prodX" :: "('p => 'a proc) => ('p => 'a proc) => bool"
                   ("(0_ /\<sqsubseteq>F' /_)" [50,50] 50)

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


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

(*** eq and ref ***)

lemma cspF_eq_ref_iff:
  "(P1 =F P2) = (P1 <=F P2 & P2 <=F P1)"
by (auto simp add: refF_def eqF_def)

lemma cspF_eq_ref:
  "P1 =F P2 ==> P1 <=F P2"
by (simp add: cspF_eq_ref_iff)

lemma cspF_ref_eq:
  "[| P1 <=F P2 ; P2 <=F P1 |] ==> P1 =F P2"
by (simp add: cspF_eq_ref_iff)

(*** reflexivity ***)

lemma cspF_reflex_eq[simp]: "P =F P"
by (simp add: eqF_def)

lemma cspF_reflex_ref[simp]: "P <=F P"
by (simp add: refF_def)

lemmas cspF_reflex = cspF_reflex_eq cspF_reflex_ref

(*** symmetry ***)

lemma cspF_sym: "P1 =F P2 ==> P2 =F P1"
by (simp add: eqF_def)

lemma cspF_symE:
  "[| P1 =F P2 ; P2 =F P1 ==> Z |] ==> Z"
by (simp add: eqF_def)

(*** transitivity ***)

lemma cspF_trans_left_eq: "[| P1 =F P2 ; P2 =F P3 |] ==> P1 =F P3"
by (simp add: eqF_def)

lemma cspF_trans_left_ref: "[| P1 <=F P2 ; P2 <=F P3 |] ==> P1 <=F P3"
by (simp add: refF_def)

lemmas cspF_trans_left = cspF_trans_left_eq cspF_trans_left_ref
lemmas cspF_trans = cspF_trans_left

lemma cspF_trans_right_eq: "[| P2 =F P3 ; P1 =F P2 |] ==> P1 =F P3"
by (simp add: eqF_def)

lemma cspF_trans_right_ref: "[| P2 <=F P3 ;  P1 <=F P2 |] ==> P1 <=F P3"
by (simp add: refF_def)

lemmas cspF_trans_rught = cspF_trans_right_eq cspF_trans_right_ref

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

lemma cspF_rw_left_eq:
  "[| P1 =F P2 ; P2 =F P3 |] ==> P1 =F P3"
by (simp add: eqF_def)

lemma cspF_rw_left_ref:
  "[| P1 =F P2 ; P2 <=F P3 |] ==> P1 <=F P3"
by (simp add: refF_def eqF_def)

lemmas cspF_rw_left = cspF_rw_left_eq cspF_rw_left_ref

lemma cspF_rw_right_eq:
  "[| P3 =F P2 ; P1 =F P2 |] ==> P1 =F P3"
by (simp add: eqF_def)

lemma cspF_rw_right_ref:
  "[| P3 =F P2 ; P1 <=F P2 |] ==> P1 <=F P3"
by (simp add: refF_def eqF_def)

lemmas cspF_rw_right = cspF_rw_right_eq cspF_rw_right_ref

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

lemma cspF_tr_left_eq: "[| P1 =F P2 ; P2 =F P3 |] ==> P1 =F P3"
by (simp add: eqF_def)

lemma cspF_tr_left_ref: "[| P1 <=F P2 ; P2 <=F P3 |] ==> P1 <=F P3"
by (simp add: refF_def eqF_def)

lemmas cspF_tr_left = cspF_tr_left_eq cspF_tr_left_ref

lemma cspF_tr_right_eq: "[| P2 =F P3 ; P1 =F P2 |] ==> P1 =F P3"
by (simp add: eqF_def)

lemma cspF_tr_right_ref: "[| P2 <=F P3 ; P1 <=F P2 |] ==> P1 <=F P3"
by (simp add: refF_def eqF_def)

lemmas cspF_tr_right = cspF_tr_right_eq cspF_tr_right_ref

end