This is a work-in-progress port of the Isabelle/HOL address translation
simplification proof for Arm v8-A. At present there is much of
the background machinery for the proof. It should build with the snapshot of
the Arm model in commit ad30a51 of the sail-arm repository.
See the Isabelle proof's README file for details of what can be
found in the files. There are also some results about bitvectors in Mword.v
that might move to the main library later.
Brian Campbell, 22nd June 2020.