Theory CSP_F_semantics

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

theory CSP_F_semantics
imports CSP_T_semantics Domain_F_cms
begin

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

         1. semantic clause
         2. 
         3. 
         4. 

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

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

consts
  failures :: "('p,'a) proc =>  ('p => 'a domF) => 'a setF"

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

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

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

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

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

  "failures(P |~| Q) = (%M. failures(P) M UnF failures(Q) M)"

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

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

  "failures(P |[X]| Q)  = (%M. {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) M & (t,Z) :f failures(Q) M) }f)"

  "failures(P -- X)  = (%M. {f. 
      EX s Y. f = (s --tr X, Y) & (s,(Ev`X) Un Y) :f failures(P) M}f)"

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

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

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

  "failures($p)     = (%M. sndF (M p))"

declare failures.simps [simp del]

(*** for dealing with both !nat and !set ***)

lemma failures_inv_inj[simp]:
   "inj g ==> (EX c. (EX n. c = g n & n : N) & f :f failures (Pf (inv g c)) x)
            = (EX z:N. f :f failures (Pf z) x)"
by (auto)

lemma Rep_int_choice_failures_nat:
  "failures(!nat :N .. Pf) = (%M. {f. EX n:N. f :f failures(Pf n) M}f)"
apply (simp add: Rep_int_choice_ss_def)
apply (simp add: failures.simps)
done

lemma Rep_int_choice_failures_set:
  "failures(!set :Xs .. Pf) = (%M. {f. EX X:Xs. f :f failures(Pf X) M}f)"
apply (simp add: Rep_int_choice_ss_def)
apply (simp add: failures.simps)
done

lemma Rep_int_choice_failures_com_lm:
   "(EX z. (EX a. z = {a} & a : X) & f :f failures (Pf (contents z)) M)
  = (EX a:X. f :f failures (Pf a) M)"
apply (auto)
apply (rule_tac x="{a}" in exI)
apply (auto)
done

lemma Rep_int_choice_failures_com: 
  "failures(! :X .. Pf) = (%M. {f. EX a:X. f :f failures(Pf a) M}f)"
apply (simp add: Rep_int_choice_com_def)
apply (simp add: Rep_int_choice_failures_set)
apply (simp add: Rep_int_choice_failures_com_lm)
done

lemma Rep_int_choice_failures_f: 
  "inj g ==> failures(!<g> :X .. Pf) = 
             (%M. {f. EX a:X. f :f failures(Pf a) M}f)"
apply (simp add: Rep_int_choice_f_def)
apply (simp add: Rep_int_choice_failures_com)
done

lemmas Rep_int_choice_failures =
       Rep_int_choice_failures_nat
       Rep_int_choice_failures_set
       Rep_int_choice_failures_com
       Rep_int_choice_failures_f

lemmas failures_def = failures.simps Rep_int_choice_failures

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

consts
  semFf   :: "('p,'a) proc => ('p => 'a domF) => 'a domF" ("[[_]]Ff")
  semFfun :: "('p => ('p,'a) proc) => ('p => 'a domF) => ('p => 'a domF)" 
                                                         ("[[_]]Ffun")

defs
  semFf_def  : "[[P]]Ff == (%M. (traces(P) (fstF o M) ,, failures(P) M))"
  semFfun_def: "[[Pf]]Ffun == (%M. %p. [[Pf p]]Ff M)"

(*
notation (xsymbols) semFf   ("[|_|]Ff")
notation (xsymbols) semFfun ("[|_|]Ffun")
*)

(*** relation ***)

lemma semFf_semFfun:
  "(%p. [[Pf p]]Ff M) = [[Pf]]Ffun M"
by (simp add: semFfun_def semFf_def)

(*------------------------------------------------------------------*
        M such that [[p]]Ff M = [[PNfun(p)]]Ff M
   such M is the fixed point of the function [[PNfun(p)]]Ffun
 *------------------------------------------------------------------*)

consts
  semFfix  :: "('p => ('p,'a) proc) => ('p => 'a domF)"      ("[[_]]Ffix")

defs
  semFfix_def : 
   "[[Pf]]Ffix == (if (FPmode = CMSmode) then (UFP ([[Pf]]Ffun))
                                         else (LFP ([[Pf]]Ffun)))"

(*
notation (xsymbols) semFfix ("[|_|]Ffix")
*)

consts
 MF :: "('p => 'a domF)"

defs
 MF_def : "MF == [[PNfun]]Ffix"

(*** semantics ***)

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

defs
  semF_def : "[[P]]F == [[P]]Ff MF"
(*
notation (xsymbols) semF ("[|_|]F")
*)

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

consts
  refF :: "('p,'a) proc => ('p => 'a domF) => 
           ('q => 'a domF) => ('q,'a) proc => bool"
                               ("(0_ /<=F[_,_] /_)" [51,0,0,50] 50)

  eqF :: "('p,'a) proc => ('p => 'a domF) => 
           ('q => 'a domF) => ('q,'a) proc => bool"
                               ("(0_ /=F[_,_] /_)"[51,0,0,50] 50)

defs
  refF_def : "P1 <=F[M1,M2] P2 == [[P2]]Ff M2 <= [[P1]]Ff M1"
  eqF_def  : "P1  =F[M1,M2] P2 == [[P1]]Ff M1  = [[P2]]Ff M2"

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

(*
notation (xsymbols) refF ("(0_ /\<sqsubseteq>F[_,_] /_)" [51,100,100,50] 50)
*)

(*********************************************************
        relations over processes (fixed point)
 *********************************************************)

abbreviation
 refFfix :: "('p,'a) proc => ('q,'a) proc => bool" ("(0_ /<=F /_)" [51,50] 50)
 where "P1 <=F P2 == P1 <=F[MF,MF] P2"

abbreviation
 eqFfix :: "('p,'a) proc => ('q,'a) proc => bool"  ("(0_ /=F /_)" [51,50] 50)
 where "P1  =F P2 == P1  =F[MF,MF] P2"

(* =F and <=F *)

lemma refF_semF: "(P1 <=F P2) = ([[P2]]F <= [[P1]]F)"
apply (simp add: refF_def)
apply (simp add: semF_def)
done

lemma eqF_semF: "(P1 =F P2) = ([[P1]]F = [[P2]]F)"
apply (simp add: eqF_def)
apply (simp add: semF_def)
done

(*------------------------------------*
 |              X-Symbols             |
 *------------------------------------*)
(*
notation (xsymbols) refFfix ("(0_ /\<sqsubseteq>F /_)" [51,50] 50)
*)

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

(*** eq and ref ***)

lemma cspF_eq_ref_iff:
 "(P1 =F[M1,M2] P2) = (P1 <=F[M1,M2] P2 & P2 <=F[M2,M1] P1)"
by (auto simp add: refF_def eqF_def)

lemma cspF_eq_ref:
  "P1 =F[M1,M2] P2 ==> P1 <=F[M1,M2] P2"
by (simp add: cspF_eq_ref_iff)

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

(*** reflexivity ***)

lemma cspF_reflex_eq_P[simp]: "P =F[M,M] P"
by (simp add: eqF_def)

lemma cspF_reflex_eq_STOP[simp]: "STOP =F[M1,M2] STOP"   
by (simp add: eqF_def semFf_def traces_def failures_def)

lemma cspF_reflex_eq_SKIP[simp]: "SKIP =F[M1,M2] SKIP"   
by (simp add: eqF_def semFf_def traces_def failures_def)

lemma cspF_reflex_eq_DIV[simp]: "DIV =F[M1,M2] DIV"   
by (simp add: eqF_def semFf_def traces_def failures_def)

lemmas cspF_reflex_eq = cspF_reflex_eq_P
                        cspF_reflex_eq_STOP
                        cspF_reflex_eq_SKIP
                        cspF_reflex_eq_DIV

lemma cspF_reflex_ref_P[simp]: "P <=F[M,M] P"
by (simp add: refF_def)

lemma cspF_reflex_ref_STOP[simp]: "STOP <=F[M1,M2] STOP"   
by (simp add: refF_def semFf_def traces_def failures_def)

lemma cspF_reflex_ref_SKIP[simp]: "SKIP <=F[M1,M2] SKIP"   
by (simp add: refF_def semFf_def traces_def failures_def)

lemma cspF_reflex_ref_DIV[simp]: "DIV <=F[M1,M2] DIV"   
by (simp add: refF_def semFf_def traces_def failures_def)

lemmas cspF_reflex_ref = cspF_reflex_ref_P
                         cspF_reflex_ref_STOP
                         cspF_reflex_ref_SKIP
                         cspF_reflex_ref_DIV

lemmas cspF_reflex = cspF_reflex_eq cspF_reflex_ref

(*** symmetry ***)

lemma cspF_sym: "P1 =F[M1,M2] P2 ==> P2 =F[M2,M1] P1"
by (simp add: eqF_def)

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

(*** transitivity ***)

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

lemma cspF_trans_left_ref: 
  "[| P1 <=F[M1,M2] P2 ; P2 <=F[M2,M3] P3 |] ==> P1 <=F[M1,M3] 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[M2,M3] P3 ; P1 =F[M1,M2] P2 |] ==> P1 =F[M1,M3] P3"
by (simp add: eqF_def)

lemma cspF_trans_right_ref: 
  "[| P2 <=F[M2,M3] P3 ;  P1 <=F[M1,M2] P2 |] ==> P1 <=F[M1,M3] 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_MF:
  "[| P1 =F P2 ; P2 =F P3 |] ==> P1 =F P3"
by (simp add: eqF_def)

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

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

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

lemmas cspF_rw_left = 
   cspF_rw_left_eq_MF cspF_rw_left_ref_MF
   cspF_rw_left_eq cspF_rw_left_ref

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

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

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

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

lemmas cspF_rw_right =
   cspF_rw_right_eq_MF cspF_rw_right_ref_MF
   cspF_rw_right_eq cspF_rw_right_ref

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

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

lemma cspF_tr_left_ref:
   "[| P1 <=F[M1,M1] P2 ; P2 <=F[M1,M3] P3 |] ==> P1 <=F[M1,M3] 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[M3,M3] P3 ; P1 =F[M1,M3] P2 |] ==> P1 =F[M1,M3] P3"
by (simp add: eqF_def)

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

lemmas cspF_tr_right = cspF_tr_right_eq cspF_tr_right_ref

(*-----------------------------------------*
 |                   noPN                  |
 *-----------------------------------------*)

lemma failures_noPN_Constant_lm:
  "noPN P --> (EX F. failures P = (%M. F))"
apply (induct_tac P)
apply (simp add: failures_def, force)
apply (simp add: failures_def, force)
apply (simp add: failures_def, force)
apply (simp add: failures_def, force)

(* Ext_pre_choice *)
 apply (intro impI)
 apply (simp)
 apply (subgoal_tac "ALL x. EX F. failures (fun2 x) = (%M. F)")
 apply (simp add: choice_ALL_EX)
 apply (erule exE)
 apply (simp add: failures_def)
 apply (force)
 apply (simp)

(* Ext_choice *)
 apply (intro impI)
 apply (simp)
 apply (elim exE)
 apply (simp add: failures_def)
 apply (subgoal_tac "ALL P. noPN P --> (EX T. traces P = (%M. T))")
 apply (frule_tac x="proc1" in spec)
 apply (drule_tac x="proc2" in spec)
 apply (simp)
 apply (elim exE)
 apply (simp)
 apply (force)
 apply (simp add: traces_noPN_Constant)

apply (simp add: failures_def, force)

(* Rep_int_choice_nat *)
 apply (intro impI)
 apply (simp)
 apply (subgoal_tac "ALL x. EX F. failures (fun x) = (%M. F)")
 apply (simp add: choice_ALL_EX)
 apply (erule exE)
 apply (simp add: failures_def)
 apply (force)
 apply (simp)

(* IF *)
 apply (simp add: failures_def)
 apply (case_tac "bool")
 apply (simp)
 apply (simp)

apply (simp add: failures_def, force)
apply (simp add: failures_def, force)
apply (simp add: failures_def, force)

(* Seq_comp *)
 apply (intro impI)
 apply (simp)
 apply (elim exE)
 apply (simp add: failures_def)
 apply (subgoal_tac "ALL P. noPN P --> (EX T. traces P = (%M. T))")
 apply (drule_tac x="proc1" in spec)
 apply (simp)
 apply (elim exE)
 apply (simp)
 apply (force)
 apply (simp add: traces_noPN_Constant)

apply (simp add: failures_def, force)
apply (simp add: failures_def)
done

lemma failures_noPN_Constant:
  "noPN P ==> (EX F. failures P = (%M. F))"
apply (simp add: failures_noPN_Constant_lm)
done

end