Derive PMATCH thms for relevant parts of compiler definition

Certain case expressions are huge within HOL. For such case expressions, the translator produces huge CakeML output, which in turn is highly likely to cause problems for the compiler bootstrapping.

One way to make the translator produce better output is to introduce `PMATCH`-reformulations of the exploding case expressions and use the reformulations in the translator. This can make the CakeML output much smaller and hence easier for the bootstrapping process to digest.

The task for this issue is to look through the compiler definitions for suspicious looking case expressions, e.g. deeply nested matches and wildcards:

```
foo x =
case x of
| SOME [x; SOME (NONE, [t1; t2; t3])] => SOME (x,t2)
| _ => NONE
```

For each such:
- a `PMATCH` reformulation needs to be proved and stored with a predictable name, e.g. `foo_pmatch`
- the translator's look up mechanism in the bootstrap should be changed so that it first looks for theorems ending in `_pmatch` before it looks for the usual `_def` theorems