# Theory Alpha

Up to index of Isabelle/HOL/Pi2

theory Alpha = Subst
files [Alpha.ML]:
```Alpha = Subst +

(*** Alpha-equivalence ***)
consts
Al    :: "('a procs * ('a::inf_class) set * 'a procs) set"
Alpha :: "(('a::inf_class) procs * 'a procs) set"

syntax
"@Al"    :: "['a procs, 'a set, 'a procs] => bool"
("_ =a[_] _" [70, 0, 71] 70)
"@Alpha" :: "['a procs, 'a procs] => bool"
("_ =a _" [70, 71] 70)

translations
"P =a[S] P'" == "(P, S, P') : Al"
"P =a P'" == "(P, P') : Alpha"

inductive "Al"
intrs
Null  ".0 =a[S] .0"
Tau   "P =a[S] P' ==> .t.P =a[S] .t.P'"
Out   "P =a[S] P' ==> a<b>.P =a[S] a<b>.P'"
In    "ALL x. x ~: S --> p{x<->b}P =a[insert x S] p{x<->b'}P' \
\ ==> a[b].P =a[S] a[b'].P'"
Res   "ALL x. x ~: S --> p{x<->b}P =a[insert x S] p{x<->b'}P' \
\ ==> .#b P =a[S] .#b' P'"
Plus  "[| P =a[S] P' ; Q =a[S] Q' |] ==> P .+ Q =a[S] P' .+ Q'"
Par   "[| P =a[S] P' ; Q =a[S] Q' |] ==> P .| Q =a[S] P' .| Q'"
Mt    "P =a[S] P' ==> .[a.=b]P =a[S] .[a.=b]P'"
Mmt   "P =a[S] P' ==> .[a.~=b]P =a[S] .[a.~=b]P'"
Repl  "P =a[S] P' ==> .!P =a[S] .!P'"

defs
Alpha_def  "Alpha == {(P, P') . EX S. finite S & P =a[S] P'}"

(*** Alpha-conversion ***)
consts
conv :: "[('a::inf_class), 'a, 'a procs] => 'a procs"
("c{_<-_}_" [0,0,114] 115)

primrec
"c{x<-y}.0 = .0"
"c{x<-y}(.t.P) = .t.c{x<-y}P"
"c{x<-y}(a<b>.P) = a<b>.c{x<-y}P"
"c{x<-y}(a[b].P) = (if b=y then a[n{x<->y}b].p{x<->y}P \
\ else a[b].c{x<-y}P)"
"c{x<-y}(.#b P) = (if b=y then .#n{x<->y}b p{x<->y}P \
\ else .#b c{x<-y}P)"
"c{x<-y}(P .+ Q) = c{x<-y}P .+ c{x<-y}Q"
"c{x<-y}(P .| Q) = c{x<-y}P .| c{x<-y}Q"
"c{x<-y}(.[a.=b]P) = .[a.=b]c{x<-y}P"
"c{x<-y}(.[a.~=b]P) = .[a.~=b]c{x<-y}P"
"c{x<-y}(.!P) = .!c{x<-y}P"

end
```

theorem Al_un1:

`  P =a[S] P' ==> P =a[S Un T] P'`

theorem Al_un2:

`  P =a[T] P' ==> P =a[S Un T] P'`

theorem Al_insert:

`  P =a[S] P' ==> P =a[insert x S] P'`

theorem lemma:

`  T <= S ==> T Un S = S`

theorem Al_subset:

`  [| P =a[T] P'; T <= S |] ==> P =a[S] P'`

theorem Al_refl_subst:

`  p{xs}P =a[S] p{xs}P`

theorem Al_refl:

`  P =a[S] P`

theorem Al_sym:

`  P =a[S] P' ==> P' =a[S] P`

theorem lemma:

`  P =a[S] P' ==> ALL P''. P' =a[S] P'' --> P =a[S] P''`

theorem Al_trans:

`  [| P =a[S] P'; P' =a[S] P'' |] ==> P =a[S] P''`

theorem Al_pren_sym:

`  p{y<->z}P =a[S] p{y<->z}P' ==> p{z<->y}P =a[S] p{z<->y}P'`

theorem lemma:

```  P =a[S] P'
==> ALL Q Q' xs xs'.
P = p{xs}Q &
P' = p{xs'}Q' &
y ~: insert z (Subst.dom xs Un Subst.dom xs' Un n Q Un n Q') -->
p{y<->z}P =a[{y, z} Un S] p{y<->z}P'```

theorem Al_pren_cong1:

`  [| P =a[S] P'; y ~: n P Un n P' |] ==> p{y<->z}P =a[{y, z} Un S] p{y<->z}P'`

theorem lemma:

`  {x, y} Un A = {y, x} Un A`

theorem Al_pren_cong2:

`  [| P =a[S] P'; z ~: n P Un n P' |] ==> p{y<->z}P =a[{y, z} Un S] p{y<->z}P'`

theorem Al_pren_choose:

```  [| p{x<->b}P =a[S] p{x<->b'}P'; {x, y} Int (n P Un n P') = {} |]
==> p{y<->b}P =a[{y, x} Un S] p{y<->b'}P'```

theorem AlphaI:

`  [| finite S; P =a[S] P' |] ==> P =a P'`

`  P =a P' ==> EX S. finite S & P =a[S] P'`

theorem Alpha_refl:

`  P =a P`

theorem Alpha_sym:

`  P =a P' ==> P' =a P`

theorem Alpha_trans:

`  [| P =a P'; P' =a P'' |] ==> P =a P''`

theorem Alpha_pren_cong1:

`  [| P =a P'; y ~: n P Un n P' |] ==> p{y<->z}P =a p{y<->z}P'`

theorem Alpha_pren_cong2:

`  [| P =a P'; z ~: n P Un n P' |] ==> p{y<->z}P =a p{y<->z}P'`

theorem Alpha_pren_choose:

```  [| p{x<->b}P =a p{x<->b'}P'; {x, y} Int (n P Un n P') = {} |]
==> p{y<->b}P =a p{y<->b'}P'```

theorem Alpha_Null:

`  .0 =a .0`

theorem Alpha_Tau:

`  P =a P' ==> .t.P =a .t.P'`

theorem Alpha_Out:

`  P =a P' ==> a<b>.P =a a<b>.P'`

theorem lemma:

```  [| finite S; ALL x. x ~: S --> p{x<->b}P =a[insert x S] p{x<->b'}P' |]
==> a[b].P =a a[b'].P'```

theorem Alpha_In:

`  [| p{x<->b}P =a p{x<->b'}P'; x ~: n P Un n P' |] ==> a[b].P =a a[b'].P'`

theorem Alpha_In_eq:

`  P =a P' ==> a[b].P =a a[b].P'`

theorem lemma:

```  [| finite S; ALL x. x ~: S --> p{x<->b}P =a[insert x S] p{x<->b'}P' |]
==> .#b P =a .#b' P'```

theorem Alpha_Res:

`  [| p{x<->b}P =a p{x<->b'}P'; x ~: n P Un n P' |] ==> .#b P =a .#b' P'`

theorem Alpha_Res_eq:

`  P =a P' ==> .#b P =a .#b P'`

theorem Alpha_Plus:

`  [| P =a P'; Q =a Q' |] ==> procs.Plus P Q =a procs.Plus P' Q'`

theorem Alpha_Par:

`  [| P =a P'; Q =a Q' |] ==> P .| Q =a P' .| Q'`

theorem Alpha_Mt:

`  P =a P' ==> .[a.=b]P =a .[a.=b]P'`

theorem Alpha_Mmt:

`  P =a P' ==> .[a.~=b]P =a .[a.~=b]P'`

theorem Alpha_Repl:

`  P =a P' ==> .!P =a .!P'`

theorem Alpha_In_conv:

`  x ~: n P ==> a[x].p{x<->b}P =a a[b].P`

theorem Alpha_Res_conv:

`  x ~: n P ==> .#x p{x<->b}P =a .#b P`

theorem lemma:

`  x ~: n P --> b ~: bn (c{x<-b}P)`

theorem Conv_del:

`  x ~: n P ==> b ~: bn (c{x<-b}P)`

theorem lemma:

`  x ~: n P --> c{x<-b}P =a P`

theorem Conv_eq:

`  x ~: n P ==> c{x<-b}P =a P`

theorem Alpha_conv:

`  EX P'. P =a P' & b ~: bn P'`