Formalise DEFLATE and add implementation to examples

[Deflate](https://en.wikipedia.org/wiki/DEFLATE) is a lossless data compression file format that [zip](https://en.wikipedia.org/wiki/ZIP_(file_format)) and [gzip](https://en.wikipedia.org/wiki/Gzip) are based on.

The [deflate algorithm](https://tools.ietf.org/html/rfc1951) would be a nice formalisation and verification exercise in HOL. The result of the formalisation effort could be used to construct a verified gzip-like executable using CakeML.

The same compression and decompression algorithm might come in handy inside the CakeML compiler, once the compiler stores bulky constant data structures as read-only data. Such bulky constants could, for example, be the AST for the basis library or the bignum library.

This project is likely to fit the scope of an internship or MSc thesis.