Theory CSP_xsymbols

Up to index of Isabelle/HOL/HOL-Complex/CSP

theory CSP_xsymbols
imports CSP_syntax Trace RS
begin

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2008         |
            |                   June 2008  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory CSP_xsymbols
imports Infra_type CSP_syntax Trace RS
begin

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

(*------------------------------------*
 |                                    |
 |             Infra_type             |
 |                                    |
 *------------------------------------*)

notation (xsymbols) sum_cup_mix ("_ ∪s _" [65,66] 65)
notation (xsymbols) sum_cap_mix ("_ ∩s _" [70,71] 70)

notation (xsymbols) nilt ("⟨⟩")
notation (xsymbols) appt (infixr "\<frown>" 65)

syntax (output)
  "_traceX"     :: "args => 'a trace"                       ("<(_)>")

syntax (xsymbols)
  "_traceX"     :: "args => 'a trace"       ("⟨(_)⟩" [900] 1000)

translations
  "⟨s⟩"  == "<s>"

(*------------------------------------*
 |                                    |
 |                Trace               |
 |                                    |
 *------------------------------------*)

notation (xsymbols) Tick ("\<surd>")

(*------------------------------------*
 |                                    |
 |                  RS                |
 |                                    |
 *------------------------------------*)

notation (xsymbols) restriction ("_ \<down> _" [84,900] 84)

(*------------------------------------*
 |                                    |
 |             CSP_syntax             |
 |                                    |
 *------------------------------------*)

syntax (output)
  "_PrefixX"         :: "'a => ('p,'a) proc => ('p,'a) proc"
                                   ("(1_ /-> _)" [150,80] 80)
  "_Ext_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"  
                                   ("(1? _:_ /-> _)" [900,900,80] 80)
  "_Ext_choiceX"     :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
                                   ("(1_ /[+] _)" [72,73] 72)
  "_Int_choiceX"     :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
                                   ("(1_ /|~| _)" [64,65] 64)
  "_Int_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"  
                                   ("(1! _:_ /-> _)" [900,900,80] 80)

syntax (xsymbols)
  "_PrefixX"         :: "'a => ('p,'a) proc => ('p,'a) proc"
                          ("(1_ /-> _)" [150,80] 80)
  "_Ext_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"  
                          ("(1? _:_ /-> _)" [900,900,80] 80)
  "_Ext_choiceX"     :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
                          ("(1_ /\<box> _)" [72,73] 72)
  "_Int_choiceX"     :: "('p,'a) proc => ('p,'a) proc => ('p,'a) proc"
                          ("(1_ /\<sqinter> _)" [64,65] 64)

  "_Int_pre_choiceX" :: "pttrn => 'a set => ('p,'a) proc => ('p,'a) proc"  
                          ("(1! _:_ /-> _)" [900,900,80] 80)

translations
  "a -> P"     == "a -> P"
  "? x:X -> P" == "? x:X -> P"
  "P \<box> Q"            == "P [+] Q"
  "P \<sqinter> Q"        == "P |~| Q"
  "! x:X -> P" == "! x:X -> P"

syntax (output)
  "_Nondet_send_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                                  ('p,'a) proc => ('p,'a) proc"
                                  ("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
  "_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
                               ("(1_ !? _ /-> _)" [900,900,80] 80)

  "_Send_prefixX"     :: "('x => 'a) => 'x => ('p,'a) proc => ('p,'a) proc" 
                          ("(1_ ! _ /-> _)" [900,1000,80] 80)

  "_Rec_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                          ('p,'a) proc => ('p,'a) proc"
                          ("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
  "_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
                          ('p,'a) proc => ('p,'a) proc"
                          ("(1_ ? _ /-> _)" [900,900,80] 80)

syntax (xsymbols)
  "_Nondet_send_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                                  ('p,'a) proc => ('p,'a) proc"
                               ("(1_ !? _:_ /-> _)" [900,900,1000,80] 80)
  "_Nondet_send_prefix_UNIVX" :: "('x => 'a) => pttrn => ('p,'a) proc => ('p,'a) proc"
                               ("(1_ !? _ /-> _)" [900,900,80] 80)

  "_Send_prefixX"     :: "('x => 'a) => 'x => ('p,'a) proc => ('p,'a) proc" 
                          ("(1_ ! _ /-> _)" [900,1000,80] 80)

  "_Rec_prefixX"      :: "('x => 'a) => pttrn => 'x set => 
                          ('p,'a) proc => ('p,'a) proc"
                          ("(1_ ? _:_ /-> _)" [900,900,1000,80] 80)
  "_Rec_prefix_UNIVX" :: "('x => 'a) => pttrn =>
                          ('p,'a) proc => ('p,'a) proc"
                          ("(1_ ? _ /-> _)" [900,900,80] 80)

translations
  "a !? x:X -> P" == "a !? x:X -> P"
  "a !? x -> P"   == "a !? x:UNIV -> P"

  "a ! x -> P"    == "a ! x -> P"
  "a ? x:X -> P"  == "a ? x:X -> P"
  "a ? x -> P"    == "a ? x:UNIV -> P"

syntax (output)
  "_TimeoutX"   :: "('p,'a) proc => ('p,'a) proc 
                 => ('p,'a) proc"  ("(1_ /[> _)" [73,74] 73)
  "_TimeoutdefX" :: "('p,'a) proc => ('p,'a) proc 
                 => ('p,'a) proc"  ("(1_ /[>def _)" [73,74] 73)
  "_HidingX"    :: "('p,'a) proc => 'a set => ('p,'a) proc"  
                                        ("(1_ /-- _)" [84,85] 84)
  "_RenamingX"  :: "('p,'a) proc => ('a * 'a) set => ('p,'a) proc"  
                                        ("(1_ /[[_]])" [84,0] 84)
  "_Depth_rest" :: "('p,'a) proc => ('p,'a) proc 
                 => ('p,'a) proc"   ("(1_ /|. _)" [84,900] 84)

syntax (xsymbols)
  "_TimeoutX"   :: "('p,'a) proc => ('p,'a) proc 
                 => ('p,'a) proc"  ("(1_ /\<rhd> _)" [73,74] 73)
  "_TimeoutdefX":: "('p,'a) proc => ('p,'a) proc 
                 => ('p,'a) proc"  ("(1_ /\<unrhd> _)" [73,74] 73)
  "_HidingX"    :: "('p,'a) proc => 'a set => ('p,'a) proc"  
                                   ("(1_ /\<midarrow> _)" [84,85] 84)
  "_RenamingX"  :: "('p,'a) proc => ('a * 'a) set => ('p,'a) proc"  
                                        ("(1_ /[|_|])" [84,0] 84)
  "_Depth_rest" :: "('p,'a) proc => ('p,'a) proc 
                 => ('p,'a) proc"   ("(1_ /⌊ _)" [84,900] 84)

translations
  "P \<rhd> Q"            == "(P |~| STOP) [+] Q"
  "P \<unrhd> Q"          == "P [>def Q"
  "P \<midarrow> X"       == "P -- X"
  "P [|r|]" == "P [[r]]"
  "P ⌊ n"            == "P |. n"

end