Theory Bisimilarity

Up to index of Isabelle/HOL/PI

theory Bisimilarity = Congruence + WkTrans
files [Bisimilarity.ML]:
Bisimilarity = Congruence + WkTrans +

consts
  sim :: "(('a::inf_class) procs * 'a procs) set"
  bisim :: "(('a::inf_class) procs * 'a procs) set"

syntax
 "@sim" :: "[('a::inf_class) procs, 'a procs] => bool"
              (infixl ".<" 60)
 "@bisim" :: "[('a::inf_class) procs, 'a procs] => bool"
              (infixl ".=" 60)

translations
  "P .< Q" == "(P, Q) : sim"
  "P .= Q" == "(P, Q) : bisim"

coinductive "bisim"
  intrs
    intr   "[| ALL a b P'. P -a<b>-> P' --> (EX Q' P'' Q''. Q =a<b>=> Q' & \
             \     P' .> P'' & Q' .> Q'' & P'' .= Q'') ; \
             \ ALL a fP'. P -a<>-> fP' --> (EX fQ'. Q =a<>=> fQ' & \
             \     (ALL c. fresha c fP' & fresha c fQ' --> \
             \             (EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q''))) ; \
             \ ALL a fP'. P -a[]-> fP' --> (EX fQ'. Q =a[]=> fQ' & \
             \     (ALL c. EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q'')) ;\
             \ ALL P'. P -tau-> P' --> (EX Q' P'' Q''. Q =eps=> Q' & \
             \     P' .> P'' & Q' .> Q'' & P'' .= Q'') ; \
             \ ALL a b Q'. Q -a<b>-> Q' --> (EX P' P'' Q''. P =a<b>=> P' & \
             \     P' .> P'' & Q' .> Q'' & P'' .= Q'') ; \
             \ ALL a fQ'. Q -a<>-> fQ' --> (EX fP'. P =a<>=> fP' & \
             \     (ALL c. fresha c fP' & fresha c fQ' --> \
             \             (EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q''))) ;\
             \ ALL a fQ'. Q -a[]-> fQ' --> (EX fP'. P =a[]=> fP' & \
             \     (ALL c. EX P'' Q''. fP' c .> P'' & fQ' c .> Q'' & P'' .= Q'')) ; \
             \ ALL Q'. Q -tau-> Q' --> (EX P' P'' Q''. P =eps=> P' & \
             \     P' .> P'' & Q' .> Q'' & P'' .= Q'') |] ==> P .= Q"

end

theorem bisimI:

  [| (P, Q) : X;
     !!P Q a b P'.
        [| (P, Q) : X; P -a<b>-> P' |]
        ==> EX Q' P'' Q''.
               Q =a<b>=> Q' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim;
     !!P Q a fP'.
        [| (P, Q) : X; P -a<>-> fP' |]
        ==> EX fQ'.
               Q =a<>=> fQ' &
               (ALL c. fresha c fP' & fresha c fQ' -->
                       (EX P'' Q''.
                           fP' c .> P'' &
                           fQ' c .> Q'' & (P'', Q'') : X Un bisim));
     !!P Q a fP'.
        [| (P, Q) : X; P -a[]-> fP' |]
        ==> EX fQ'.
               Q =a[]=> fQ' &
               (ALL c. EX P'' Q''.
                          fP' c .> P'' & fQ' c .> Q'' & (P'', Q'') : X Un bisim);
     !!P Q P'.
        [| (P, Q) : X; P -tau-> P' |]
        ==> EX Q' P'' Q''.
               Q =eps=> Q' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim;
     !!P Q a b Q'.
        [| (P, Q) : X; Q -a<b>-> Q' |]
        ==> EX P' P'' Q''.
               P =a<b>=> P' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim;
     !!P Q a fQ'.
        [| (P, Q) : X; Q -a<>-> fQ' |]
        ==> EX fP'.
               P =a<>=> fP' &
               (ALL c. fresha c fP' & fresha c fQ' -->
                       (EX P'' Q''.
                           fP' c .> P'' &
                           fQ' c .> Q'' & (P'', Q'') : X Un bisim));
     !!P Q a fQ'.
        [| (P, Q) : X; Q -a[]-> fQ' |]
        ==> EX fP'.
               P =a[]=> fP' &
               (ALL c. EX P'' Q''.
                          fP' c .> P'' & fQ' c .> Q'' & (P'', Q'') : X Un bisim);
     !!P Q Q'.
        [| (P, Q) : X; Q -tau-> Q' |]
        ==> EX P' P'' Q''.
               P =eps=> P' & P' .> P'' & Q' .> Q'' & (P'', Q'') : X Un bisim |]
  ==> P .= Q

theorem plain_bisimI:

  [| (P, Q) : X;
     !!P Q a b P'.
        [| (P, Q) : X; P -a<b>-> P' |]
        ==> EX Q' P'' Q''. Q =a<b>=> Q' & (P', Q') : X Un bisim;
     !!P Q a fP'.
        [| (P, Q) : X; P -a<>-> fP' |]
        ==> EX fQ'.
               Q =a<>=> fQ' &
               (ALL c. fresha c fP' & fresha c fQ' -->
                       (fP' c, fQ' c) : X Un bisim);
     !!P Q a fP'.
        [| (P, Q) : X; P -a[]-> fP' |]
        ==> EX fQ'. Q =a[]=> fQ' & (ALL c. (fP' c, fQ' c) : X Un bisim);
     !!P Q P'.
        [| (P, Q) : X; P -tau-> P' |]
        ==> EX Q' P'' Q''. Q =eps=> Q' & (P', Q') : X Un bisim;
     !!P Q a b Q'.
        [| (P, Q) : X; Q -a<b>-> Q' |]
        ==> EX P' P'' Q''. P =a<b>=> P' & (P', Q') : X Un bisim;
     !!P Q a fQ'.
        [| (P, Q) : X; Q -a<>-> fQ' |]
        ==> EX fP'.
               P =a<>=> fP' &
               (ALL c. fresha c fP' & fresha c fQ' -->
                       (fP' c, fQ' c) : X Un bisim);
     !!P Q a fQ'.
        [| (P, Q) : X; Q -a[]-> fQ' |]
        ==> EX fP'. P =a[]=> fP' & (ALL c. (fP' c, fQ' c) : X Un bisim);
     !!P Q Q'.
        [| (P, Q) : X; Q -tau-> Q' |]
        ==> EX P' P'' Q''. P =eps=> P' & (P', Q') : X Un bisim |]
  ==> P .= Q

theorem RstrIdD1:

  (P, Q) : RstrId ==> P = Q

theorem RstrIdI:

  rstr P ==> (P, P) : RstrId

theorem bisim_refl:

  rstr P ==> P .= P