Theory Procs

Up to index of Isabelle/HOL/PI

theory Procs = Names + ExtMain
files [Procs.ML]:
(* Title:    Procs.thy
   Author:   Christine Roeckl

Introducing the syntax of monadic pi-calculus processes in terms of
a datatype definition. Primitively recursive functions to compute
the free and fresh names of a process, as well as its depth of binders,
are defined.
*)

Procs = Names + ExtMain +

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)"
           | Res     "'a => ('a procs)"       (binder ".#" 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)


syntax
  "_In"    :: "['a, 'a, ('a procs)] => ('a procs)"
               ("_[_]._" [120, 0, 110] 110)

translations
  "a[x].P" => "procs.In a (%x. P)"


(* free names *)
consts
  fn   :: (('a::inf_class) procs) => 'a set
  fna  :: (('a::inf_class) => ('a procs)) => 'a set
  fnaa :: (('a::inf_class) => 'a => ('a procs)) => 'a set

primrec
  fn0 "fn (.0) = {}"
  fn1 "fn (.t.P) = fn P"
  fn2 "fn (a<b>.P) = {a,b} Un fn P"
  fn3 "fn (In a fP) = {a} Un {a. ALL b. a: fn (fP b)}"
  fn4 "fn (Res fP) = {a. ALL b. a: fn (fP b)}"
  fn5 "fn (P .+ Q) = fn P Un fn Q"
  fn6 "fn (P .| Q) = fn P Un fn Q"
  fn7 "fn (.[a.=b]P) = {a,b} Un fn P"
  fn8 "fn (.[a.~=b]P) = {a,b} Un fn P"
  fn9 "fn (.!P) = (fn P)"

defs
  fna_def  "fna fP == {a. ALL b. a: fn (fP b)}"
  fnaa_def "fnaa ffP == {a. ALL b. a: fna (ffP b)}"


(* fresh names *)
constdefs
  fresh :: ('a::inf_class) => ('a procs) => bool
 "fresh a P == a ~: fn P"

  fresha :: ('a::inf_class) => ('a => ('a procs)) => bool
 "fresha a fP == a ~: fna fP"

  freshaa :: ('a::inf_class) => ('a => 'a => ('a procs)) => bool
 "freshaa a ffP == a ~: fnaa ffP"


(* depth of binders *)
consts
  dob  :: "('a::inf_class) procs => 'a => nat"
  doba :: "(('a::inf_class) => ('a procs)) => 'a => nat"

primrec
  dob0 "dob (.0) c = 0"
  dob1 "dob (.t.P) c = dob P c"
  dob2 "dob (a<b>.P) c = dob P c"
  dob3 "dob (In a fP) c = Suc (dob (fP c) c)"
  dob4 "dob (Res fP) c = Suc (dob (fP c) c)"
  dob5 "dob (P .+ Q) c = max (dob P c) (dob Q c)"
  dob6 "dob (P .| Q) c = max (dob P c) (dob Q c)"
  dob7 "dob (.[a.=b]P) c = dob P c"
  dob8 "dob (.[a.~=b]P) c = dob P c"
  dob9 "dob (.!P) c = dob P c"

defs
  doba_def "doba fP c == dob (fP c) c"

end

theorem fnaa_sym:

  fnaa (%x y. ffP y x) = fnaa ffP

theorem not_fna1:

  a ~: fna (%x. .t.fP x) ==> a ~: fna fP

theorem not_fna2a:

  a ~: fna (%x. fa x<fb x>.fP x) ==> a ~: fnna fa

theorem not_fna2b:

  a ~: fna (%x. fa x<fb x>.fP x) ==> a ~: fnna fb

theorem not_fna2c:

  a ~: fna (%x. fa x<fb x>.fP x) ==> a ~: fna fP

theorem not_fna3a:

  a ~: fna (%x. In (fa x) (%y. ffP y x)) ==> a ~: fnna fa

theorem not_fna3b:

  a ~: fna (%x. In (fa x) (%y. ffP y x)) ==> a ~: fnaa ffP

theorem not_fna4:

  a ~: fna (%x. .#y. ffP y x) ==> a ~: fnaa ffP

theorem not_fna5a:

  a ~: fna (%x. procs.Plus (fP x) (fQ x)) ==> a ~: fna fP

theorem not_fna5b:

  a ~: fna (%x. procs.Plus (fP x) (fQ x)) ==> a ~: fna fQ

theorem not_fna6a:

  a ~: fna (%x. fP x .| fQ x) ==> a ~: fna fP

theorem not_fna6b:

  a ~: fna (%x. fP x .| fQ x) ==> a ~: fna fQ

theorem not_fna7a:

  a ~: fna (%x. .[fa x.=fb x]fP x) ==> a ~: fnna fa

theorem not_fna7b:

  a ~: fna (%x. .[fa x.=fb x]fP x) ==> a ~: fnna fb

theorem not_fna7c:

  a ~: fna (%x. .[fa x.=fb x]fP x) ==> a ~: fna fP

theorem not_fna8a:

  a ~: fna (%x. .[fa x.~=fb x]fP x) ==> a ~: fnna fa

theorem not_fna8b:

  a ~: fna (%x. .[fa x.~=fb x]fP x) ==> a ~: fnna fb

theorem not_fna8c:

  a ~: fna (%x. .[fa x.~=fb x]fP x) ==> a ~: fna fP

theorem not_fna9:

  a ~: fna (%x. .!fP x) ==> a ~: fna fP

theorem fna_subset1:

  fna (%x. .t.fP x) <= A ==> fna fP <= A

theorem fna_subset2:

  fna (%x. fa x<fb x>.fP x) <= A ==> fnna fa <= A & fnna fb <= A & fna fP <= A

theorem fna_subset3:

  fna (%x. In (fa x) (%y. ffP y x)) <= A ==> fnna fa <= A & fnaa ffP <= A

theorem fna_subset4:

  fna (%x. .#y. ffP y x) <= A ==> fnaa ffP <= A

theorem fna_subset5:

  fna (%x. procs.Plus (fP x) (fQ x)) <= A ==> fna fP <= A & fna fQ <= A

theorem fna_subset6:

  fna (%x. fP x .| fQ x) <= A ==> fna fP <= A & fna fQ <= A

theorem fna_subset7:

  fna (%x. .[fa x.=fb x]fP x) <= A ==> fnna fa <= A & fnna fb <= A & fna fP <= A

theorem fna_subset8:

  fna (%x. .[fa x.~=fb x]fP x) <= A ==> fnna fa <= A & fnna fb <= A & fna fP <= A

theorem fna_subset9:

  fna (%x. .!fP x) <= A ==> fna fP <= A

theorem fna_Inter:

  fna fP = Inter {A. EX a. A = fn (fP a)}

theorem fnaa_Inter:

  fnaa ffP = Inter {A. EX a b. A = fn (ffP a b)}

theorem lemma:

  EX A:AA. finite A ==> finite (Inter AA)

theorem finite_fn:

  finite (fn P)

theorem finite_fna:

  finite (fna fP)

theorem finite_fnaa:

  finite (fnaa ffP)

theorem not_fn_fna:

  a ~: fn (fP b) ==> a ~: fna fP

theorem fresh_mono:

  fresh a (fP b) ==> fresha a fP

theorem fresha_mono:

  fresha a (ffP b) ==> freshaa a ffP

theorem doba_leq1:

  doba (%x. .t.fP x) c <= n ==> doba fP c <= n

theorem doba_leq2:

  doba (%x. fa x<fb x>.fP x) c <= n ==> doba fP c <= n

theorem doba_leq3:

  doba (%x. In (fa x) (%y. ffP y x)) c <= n ==> Suc (doba (ffP c) c) <= n

theorem doba_leq4:

  doba (%x. .#y. ffP y x) c <= n ==> Suc (doba (ffP c) c) <= n

theorem doba_leq5:

  doba (%x. procs.Plus (fP x) (fQ x)) c <= n ==> doba fP c <= n & doba fQ c <= n

theorem doba_leq6:

  doba (%x. fP x .| fQ x) c <= n ==> doba fP c <= n & doba fQ c <= n

theorem doba_leq7:

  doba (%x. .[fa x.=fb x]fP x) c <= n ==> doba fP c <= n

theorem doba_leq8:

  doba (%x. .[fa x.~=fb x]fP x) c <= n ==> doba fP c <= n

theorem doba_leq9:

  doba (%x. .!fP x) c <= n ==> doba fP c <= n

theorem fn3':

  fn (In a fP) = {a} Un fna fP

theorem fn4':

  fn (Res fP) = fna fP