Theory Subst

Up to index of Isabelle/HOL/Pi2

theory Subst = Procs
files [Subst.ML]:

Subst = Procs +

(*** Renaming on names ***)
constdefs
  nren :: "[('a::inf_class), 'a, 'a] => 'a" ("n{_<->_}_" [0,0,199] 200)
 "n{x<->y}a == if a=x then y else if a=y then x else a"


(*** Renaming on processes ***)
consts
  pren :: "[('a::inf_class), 'a, 'a procs] => 'a procs"
           ("p{_<->_}_" [0,0,114] 115)

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


(*** Substitution ***)
consts
  nsubst :: "[(('a::inf_class) * 'a) list, 'a] => 'a"
             ("n{_}_" [0,199] 200)
  psubst :: "[(('a::inf_class) * 'a) list, 'a procs] => 'a procs"
             ("p{_}_" [0,114] 115)

primrec
  "n{[]}a = a"
  "n{x#xs}a = n{xs}n{(fst x)<->(snd x)}a"

primrec
  "p{[]}P = P"
  "p{x#xs}P = p{xs}p{(fst x)<->(snd x)}P"

constdefs
  dom :: "(('a::inf_class) * 'a) list => 'a set"
 "dom xs == set (map fst xs) Un set (map snd xs)"

end

theorem nren_id:

  n{x<->x}a = a

theorem pren_id:

  p{x<->x}P = P

theorem nren_sym:

  n{x<->y}a = n{y<->x}a

theorem pren_sym:

  p{x<->y}P = p{y<->x}P

theorem nren_trans:

  a ~: {y, z} ==> n{y<->z}n{z<->x}a = n{y<->x}a

theorem lemma:

  {y, z} Int n P = {} --> p{y<->z}p{z<->x}P = p{y<->x}P

theorem pren_trans:

  [| y ~: n P; z ~: n P |] ==> p{y<->z}p{z<->x}P = p{y<->x}P

theorem nren_vain:

  a ~: {x, y} ==> n{x<->y}a = a

theorem lemma:

  x ~: n P & y ~: n P --> p{y<->x}P = P

theorem pren_vain:

  [| x ~: n P; y ~: n P |] ==> p{y<->x}P = P

theorem nren_swap:

  n{n{x<->y}x'<->n{x<->y}y'}n{x<->y}a = n{x<->y}n{x'<->y'}a

theorem nren_swap_alt:

  n{x'<->y'}n{n{x'<->y'}x<->n{x'<->y'}y}a = n{x<->y}n{x'<->y'}a

theorem pren_swap:

  p{n{x<->y}x'<->n{x<->y}y'}p{x<->y}P = p{x<->y}p{x'<->y'}P

theorem pren_swap_alt:

  p{x'<->y'}p{n{x'<->y'}x<->n{x'<->y'}y}P = p{x<->y}p{x'<->y'}P

theorem pren_swap1:

  x' ~: {x, y} ==> p{x'<->n{x<->y}y'}p{x<->y}P = p{x<->y}p{x'<->y'}P

theorem pren_swap2:

  y' ~: {x, y} ==> p{n{x<->y}x'<->y'}p{x<->y}P = p{x<->y}p{x'<->y'}P

theorem lemma:

  x ~: n P -->
  (if b : n P then n (p{x<->b}P) = insert x (n P) - {b} else n (p{x<->b}P) = n P)

theorem n_pren:

  x ~: n P
  ==> if b : n P then n (p{x<->b}P) = insert x (n P) - {b}
      else n (p{x<->b}P) = n P

theorem n_pren1:

  [| x ~: n P; b ~: n P |] ==> n (p{x<->b}P) = n P

theorem n_pren2:

  [| x ~: n P; b : n P |] ==> n (p{x<->b}P) = insert x (n P) - {b}

theorem pren_del:

  x ~: n P ==> b ~: n (p{x<->b}P)

theorem lemma:

  x : n P & b : n P --> n (p{x<->b}P) = n P

theorem n_pren3:

  [| x : n P; b : n P |] ==> n (p{x<->b}P) = n P

theorem dom_empty:

  Subst.dom [] = {}

theorem dom_cons:

  Subst.dom (x # xs) = insert (fst x) (insert (snd x) (Subst.dom xs))

theorem dom_app:

  Subst.dom (xs @ ys) = Subst.dom xs Un Subst.dom ys

theorem dom_finite:

  finite (Subst.dom xs)

theorem psubst_app:

  p{xs @ ys}P = p{ys}p{xs}P

theorem psubst_Null:

  p{xs}.0 = .0

theorem psubst_Tau:

  p{xs}(.t.P) = .t.p{xs}P

theorem psubst_Out:

  p{xs}(a<b>.P) = n{xs}a<n{xs}b>.p{xs}P

theorem psubst_In:

  p{xs}(a[b].P) = n{xs}a[n{xs}b].p{xs}P

theorem psubst_Res:

  p{xs}(.#b P) = .#n{xs}b p{xs}P

theorem psubst_Plus:

  p{xs}procs.Plus P Q = procs.Plus (p{xs}P) (p{xs}Q)

theorem psubst_Par:

  p{xs}(P .| Q) = p{xs}P .| p{xs}Q

theorem psubst_Mt:

  p{xs}(.[a.=b]P) = .[n{xs}a.=n{xs}b]p{xs}P

theorem psubst_Mmt:

  p{xs}(.[a.~=b]P) = .[n{xs}a.~=n{xs}b]p{xs}P

theorem psubst_Repl:

  p{xs}(.!P) = .!p{xs}P

theorem nren_ineq:

  [| b ~: {x, y}; b ~= a |] ==> b ~= n{x<->y}a

theorem lemma:

  b ~: Subst.dom xs & b ~= a --> b ~= n{xs}a

theorem pren_ineq:

  [| b ~: Subst.dom xs; b ~= a |] ==> b ~= n{xs}a

theorem lemma:

  .0 = p{xs}Q --> Q = .0

theorem psubst_cases_Null:

  .0 = p{xs}Q ==> Q = .0

theorem lemma:

  .t.P = p{xs}Q --> (EX R. Q = .t.R & P = p{xs}R)

theorem psubst_cases_Tau:

  .t.P = p{xs}Q ==> EX R. Q = .t.R & P = p{xs}R

theorem lemma:

  a<b>.P = p{xs}Q -->
  (EX c d R. Q = c<d>.R & a = n{xs}c & b = n{xs}d & P = p{xs}R)

theorem psubst_cases_Out:

  a<b>.P = p{xs}Q ==> EX c d R. Q = c<d>.R & a = n{xs}c & b = n{xs}d & P = p{xs}R

theorem lemma:

  a[b].P = p{xs}Q -->
  (EX c d R. Q = c[d].R & a = n{xs}c & b = n{xs}d & P = p{xs}R)

theorem psubst_cases_In:

  a[b].P = p{xs}Q ==> EX c d R. Q = c[d].R & a = n{xs}c & b = n{xs}d & P = p{xs}R

theorem lemma:

  .#b P = p{xs}Q --> (EX d R. Q = .#d R & b = n{xs}d & P = p{xs}R)

theorem psubst_cases_Res:

  .#b P = p{xs}Q ==> EX d R. Q = .#d R & b = n{xs}d & P = p{xs}R

theorem lemma:

  procs.Plus P P' = p{xs}Q -->
  (EX R S. Q = procs.Plus R S & P = p{xs}R & P' = p{xs}S)

theorem psubst_cases_Plus:

  procs.Plus P P' = p{xs}Q
  ==> EX R S. Q = procs.Plus R S & P = p{xs}R & P' = p{xs}S

theorem lemma:

  P .| P' = p{xs}Q --> (EX R S. Q = R .| S & P = p{xs}R & P' = p{xs}S)

theorem psubst_cases_Par:

  P .| P' = p{xs}Q ==> EX R S. Q = R .| S & P = p{xs}R & P' = p{xs}S

theorem lemma:

  .[a.=b]P = p{xs}Q -->
  (EX c d R. Q = .[c.=d]R & a = n{xs}c & b = n{xs}d & P = p{xs}R)

theorem psubst_cases_Mt:

  .[a.=b]P = p{xs}Q
  ==> EX c d R. Q = .[c.=d]R & a = n{xs}c & b = n{xs}d & P = p{xs}R

theorem lemma:

  .[a.~=b]P = p{xs}Q -->
  (EX c d R. Q = .[c.~=d]R & a = n{xs}c & b = n{xs}d & P = p{xs}R)

theorem psubst_cases_Mmt:

  .[a.~=b]P = p{xs}Q
  ==> EX c d R. Q = .[c.~=d]R & a = n{xs}c & b = n{xs}d & P = p{xs}R

theorem lemma:

  .!P = p{xs}Q --> (EX R. Q = .!R & P = p{xs}R)

theorem psubst_cases_Repl:

  .!P = p{xs}Q ==> EX R. Q = .!R & P = p{xs}R