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