Theory Procs

Up to index of Isabelle/HOL/Pi2

theory Procs = Names
files [Procs.ML]:
Procs = Names +

datatype
  'a procs = Null                             (".0" 115)
           | Tau     "('a::inf_class) procs"  (".t.(_)" [111] 110)
           | Out     'a 'a ('a procs)         ("_<_>._" [120, 0, 110] 110)
           | In      'a 'a ('a procs)         ("_[_]._" [120, 0, 110] 110)
           | Res     'a ('a procs)            (".#_ _"  [180, 101] 100)
           | Plus    ('a procs) ('a procs)    (infixl ".+" 85)
           | Par     ('a procs) ('a procs)    (infixl ".|" 90)
           | Mt      'a 'a ('a procs)         (".[_.=_]_" [100, 100, 96] 95)
           | Mmt     'a 'a ('a procs)         (".[_.~=_]_" [100, 100, 96] 95)
           | Repl    ('a procs)               (".!_" [100] 100)

consts
  fn :: "('a::inf_class) procs => 'a set"
  bn :: "('a::inf_class) procs => 'a set"
  n  :: "('a::inf_class) procs => 'a set"

primrec
  "fn (.0) = {}"
  "fn (.t.P) = fn P"
  "fn (a<b>.P) = {a,b} Un fn P"
  "fn (a[b].P) = insert a ((fn P) - {b})"
  "fn (.#b P) = fn P - {b}"
  "fn (P .+ Q) = fn P Un fn Q"
  "fn (P .| Q) = fn P Un fn Q"
  "fn (.[a.=b]P) = {a,b} Un fn P"
  "fn (.[a.~=b]P) = {a,b} Un fn P"
  "fn (.!P) = (fn P)"

primrec
  "bn (.0) = {}"
  "bn (.t.P) = bn P"
  "bn (a<b>.P) = bn P"
  "bn (a[b].P) = insert b (bn P)"
  "bn (.#b P) = insert b (bn P)"
  "bn (P .+ Q) = bn P Un bn Q"
  "bn (P .| Q) = bn P Un bn Q"
  "bn (.[a.=b]P) = bn P"
  "bn (.[a.~=b]P) = bn P"
  "bn (.!P) = (bn P)"

defs
  n_def "n P == fn P Un bn P"

end

theorem fn_finite:

  finite (fn P)

theorem bn_finite:

  finite (bn P)

theorem n_finite:

  finite (n P)

theorem n_Null:

  n (.0) = {}

theorem n_Tau:

  n (.t.P) = n P

theorem n_Out:

  n (a<b>.P) = {a, b} Un n P

theorem n_In:

  n (a[b].P) = {a, b} Un n P

theorem n_Res:

  n (.#b P) = insert b (n P)

theorem n_Plus:

  n (procs.Plus P Q) = n P Un n Q

theorem n_Par:

  n (P .| Q) = n P Un n Q

theorem n_Mt:

  n (.[a.=b]P) = {a, b} Un n P

theorem n_Mmt:

  n (.[a.~=b]P) = {a, b} Un n P

theorem n_Repl:

  n (.!P) = n P