[pi] variable substitution of pi-calculus agents (and residuals)

[binghe]

Hi,

Finally the variable substitution of pi-calculus agents (and transition residuals) is done. The following two theorems fully character the behavior of variable substitution (string -> string):

[pi_sub_thm]
⊢ (∀u E. [E/u] Nil = Nil) ∧ (∀u E t. [E/u] (Tau t) = Tau ([E/u] t)) ∧
  (∀v u E e t.
     v ≠ u ∧ v ≠ E ⇒ [E/u] (Input e v t) = Input ([E/u] e) v ([E/u] t)) ∧
  (∀u E a b t. [E/u] (Output a b t) = Output ([E/u] a) ([E/u] b) ([E/u] t)) ∧
  (∀u E a b t. [E/u] (Match a b t) = Match ([E/u] a) ([E/u] b) ([E/u] t)) ∧
  (∀u E a b t. [E/u] (Mismatch a b t) = Mismatch ([E/u] a) ([E/u] b) ([E/u] t)) ∧
  (∀u E t t'. [E/u] (t' + t) = [E/u] t' + [E/u] t) ∧
  (∀u E t t'. [E/u] (t' || t) = [E/u] t' || [E/u] t) ∧
  (∀v u E t. v ≠ u ∧ v ≠ E ⇒ [E/u] (Res v t) = Res v ([E/u] t)) ∧
  ∀u E x y t.
    tpm [(x,y)] ([E/u] t) = [swapstr x y E/swapstr x y u] (tpm [(x,y)] t)

[residual_sub_thm]
⊢ (∀u E t. [E/u] (TauR t) = TauR ([E/u] t)) ∧
  (∀v u E e t.
     v ≠ u ∧ v ≠ E ⇒ [E/u] (InputS e v t) = InputS ([E/u] e) v ([E/u] t)) ∧
  (∀v u E e t.
     v ≠ u ∧ v ≠ E ⇒
     [E/u] (BoundOutput e v t) = BoundOutput ([E/u] e) v ([E/u] t)) ∧
  (∀u E a b t.
     [E/u] (FreeOutput a b t) = FreeOutput ([E/u] a) ([E/u] b) ([E/u] t)) ∧
  ∀u E x y t.
    rpm [(x,y)] ([E/u] t) = [swapstr x y E/swapstr x y u] (rpm [(x,y)] t)

As uaual, the API function prove_alpha_fcbhyp (in nomdatatype) has been generalised: one of its argument (ppm) was a term, now is a list of terms (ppms):

  val prove_alpha_fcbhyp : {ppms :term list, alphas: thm list, rwts: thm list} -> thm -> thm

All existing function calls of it are modified to fit the new type of this function.

--Chun

[mn200]

Very nice! Thanks.