feat(CCS): Milner's Vending Machine

[fmontesi]

This PR formalises Milner's classical Vending Machine example for CCS and adds general utilities to LTS, bisimulation, and CCS that have been very useful in developing the example.

One of the reasons to develop this is to test the new AI instructions in #763. Albeit all code is manually written, interacting with the AI to see where it got stuck has been very informative for finding missing utilities.

Depends on #763.

[rudywasfound]

The example showing the machine can do a coin action only proves that one transition exists. It does not state that this is the only transition possible at that state, or that the whole deterministic machine is deterministic everywhere. Would it be worth adding an explicit lemma or instance saying the deterministic machine actually satisfies Deterministic (or is deterministic at every reachable state), so the claim in the file's description is backed by a named result and not just used implicitly inside the bigger proof?

[fmontesi]

I have that result hidden in this proof:

https://github.com/leanprover/cslib/pull/764/changes#diff-ed8d7e4654d2484fa0d479ebbc2db48e43fe4b146df49f01b62a968623186365R79

But I agree in general, and yes, a proof that the deterministic vending machine is indeed deterministic (as in LTS.Deterministic) would be welcome.

I'm introducing this specific example also because it's a minimal example to explore infrastructure to make reasoning about this kind of things easier. I think there's much space for improvement in reasoning about unique transitions, traces, etc.

[rudywasfound]

makes sense.