Updated CCS example

[binghe]

Hi,

This PR contains some updates to the CCS example, after the underlying datatype was converted to nominal types, shared with the lambda example. (These updates, however, are big not enough for new publications on the CCS example.)

In the formalization of multivariate unique solution of equations, the previous home-craft simultaneous substitution (called fromList) has been replaced with the ssub (in form of fromPairs) inherited from the lambda examples. This name change has caused many modifications in MultivariateScript.sml while the actual proof changes are minor.

In addition, the concept of multivariate context has slightly changed, with a parameter changed from list to set (as the order is irrelevant):

context_def
⊢ ∀Xs E. context Xs E ⇔ ∀X. X ∈ Xs ⇒ CONTEXT (λt. CCS_Subst E t X)

On the other hand, the univariate version of strong unique solution of equations has the following "extended" version:

STRONG_UNIQUE_SOLUTION_EXT
⊢ ∀C1 C2 P Q. WG C1 ∧ WG C2 ∧ (∀t. C1 t ∼ C2 t) ∧ P ∼ C1 P ∧ Q ∼ C2 Q ⇒ P ∼ Q

which easily leads to the original version:

STRONG_UNIQUE_SOLUTION
⊢ ∀E P Q. WG E ∧ P ∼ E P ∧ Q ∼ E Q ⇒ P ∼ Q

The above "extended" version may have some other applications (in the future).

P.S. These work has been pending in my personal branch for several months.

--Chun

[mn200]

It's nice to see this continue to develop!