Arch split Corres.thy and Bits_R.thy

[Xaphiosis]

Once again, please review commit-by-commit. I will want to ultimately squash the refine and crefine updates together, and also squash the hierarchy update into the Bits_R arch-split (smaller chunks make review easier).

For Corres.thy, there's nothing interesting, I picked the one that had the most stuff in it (ARM) and removed the rest.

For Bits_R, there were some adventures needed:

• projectKOs has a generic and arch-specific part; since RISCV64 and AARCH64 expect both to be [simp], and the other arches expect neither to be [simp], there was no good way to reconcile. After discussion, projectKOs exports both arch and generic lemmas into the global context, and is now [simp] on all architectures
• isCap_simps shows up a lot, but it had to be arch-split into gen_ and arch_ ; there are some places where I had to use the arch version in a "generic" proof, which will have to be untangled further down the arch-split line

Addresses https://github.com/seL4/l4v/issues/687 but will need a projectKOs warning cleanup pass on arches beside RISCV64 and AARCH64.

Removes 1658 lines of proof.