Split up large induction proofs #1245
Description
Some induction proofs get really large. In those cases, it is possible to deal with every case in a separate lemma, combining them again in the end. A recent example can be found here.
It is probably a good idea to identify large induction proofs and split them up using, ideally, the same SML functions, so we can put them into preamble or even upstream them to HOL (perhaps with syntactic sugar?) in the long term.
(Current) advantages:
- It will probably become easier to locate and navigate to specific points (in particular failures) in large induction proofs.
- Temporary workaround for the cache being slow. #1222 clears the cache for arithmetic operations, which, to my understanding, leads to some speedups. Splitting up large induction proofs could benefit twice from this by having shorter proofs and clearing of the cache between them