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'

theorem AlphaD:

  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'