[lambda, CCS] "fromPairs" ported from CCS to lambda example

[binghe]

Hi,

Previously in some proofs of the lambda examples (e.g. in solvableTheory), sometimes there's the need of simultaneous substitution (ssub) given by a pair of key list and value list: FEMPTY |++ ZIP (Xs,Ps). The properties such "explicit" finite maps can be more specific (also more useful in certain contexts) than those existing theorems for "blackbox" finite maps (in termTheory).

In the CCS example, the theory of simultaneous substitution given by a pair of key list and value list (previously named fromList but to avoid conflicts I have renamed it to fromPairs), is more developed for the proofs of multivariate "unique solution of equations" theorem, etc. After the changes of CCS term definitions in #1176, now all the related theorems can be ported to the lambda example with almost identical proofs, increasing the size of supporting theorems for ssub of lambda terms in the future. (In theory, if needed, these theorems can be easily ported for any user code of the generic_termsTheory).

The basic definition is the following:

[fromPairs_def] (termTheory)
⊢ ∀Xs Ps. fromPairs Xs Ps = FEMPTY |++ ZIP (Xs,Ps)

And the most notable theorems about fromPairs are the following two, one converts simultaneous substitution to iterated substitution based on FOLDR, the other deals with nested simultaneous substitution:

[fromPairs_FOLDR]
⊢ ∀Xs Ps E.
    ALL_DISTINCT Xs ∧ LENGTH Ps = LENGTH Xs ∧
    EVERY (λp. DISJOINT (set Xs) (FV p)) Ps ⇒
    fromPairs Xs Ps ' E = FOLDR (λ(x,y) e. [y/x] e) E (ZIP (Xs,Ps))

[fromPairs_nested]
⊢ ∀Xs Ps Es E.
    ALL_DISTINCT Xs ∧ LENGTH Ps = LENGTH Xs ∧ LENGTH Es = LENGTH Xs ⇒
    fromPairs Xs Ps ' (fromPairs Xs Es ' E) =
    fromPairs Xs (MAP ($' (fromPairs Xs Ps)) Es) ' E

I may revise (and shorten) some existing proofs of the lambda example, to actually use these new devices, in the future.

[binghe]

Hi, I'm going to use alistTheory instead of this fromPairs. This will avoid one definition. Close this PR for now.