# 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`