Monadic_Rewrite overhaul

[Xaphiosis]

This is the final significant PR for the Monadic_Rewrite overhaul funded by the seL4 Foundation. There is one item outstanding: re-indenting Fastpath_Equiv and Fastpath_C but I don't want the noise of that in this PR, and I want to hack together a little indenter improvement to fix up mis-indented comments / subgoal afterwards, for which there's no time right now.

Generally:

• we now have useful tactics to work with most simple cases of monadic rewriting, plus other quality-of-life such as wp_pre understanding monadic_rewrite_guard_imp
• the rules have names that make more sense and are at least consistent with each other
• a number of rules were redundant or had assumptions that were too strong
• monadic_rewrite proofs have generally gotten shorter, but the extreme specificity of walking over the code structure makes automation prohibitive in a fair few cases, more than I initially estimated

The hope is the availability of this tech will improve willingness to use it for the simple cases which used to be a huge pain previously.

The overhaul includes work that was merged as previous PRs:

• #487
• #516
• #517
• #518
• #521

Unhappinesses that were not solved (and I don't know how to solve at a fundamental level):

• fragility of name bindings inside a monad: these are just lambdas and follow eta-contraction and other random rules
  • for symbolic execution at the head, we have done well to preserve the names in the monad even in adverse circumstances (see no_name_eta for example)
  • unfortunately rules that "step through", like monadic_rewrite_bind_tail can only make use of the name capturing trick (which is deep in Isabelle and used for stuff like allE preserving names) on the first subgoal, with later subgoals getting rv or x or whatever is the name in the rule
  • this means that targeted tactics like monadic_rewrite_l will damage all names until the point where the supplied rule matches
  • there might be a way to hack past this in the future, but it will always be a hack, because we do not have an actual name binding, just a lambda in a shallow embedding, so we'd have to dive in and try extract it, then apply a rename that sticks to other goals... yuck. Try capture the name in some kind of deeper embedding? no idea how that can work; etc.

[Xaphiosis]

@mbrcknl this might be of limited interest to you, and you might have other interesting ideas for the future, but I know you're very busy :)

@michaelmcinerney : you wanted to learn a bit more about tactical stuff works, and a bunch of these renames will bite on the next merge with MCS, so you should be aware in order to yell at me then

[lsf37]

For some reason the GitHub tests didn't trigger apart from the DCO. I'm very confused by this -- shouldn't be possible and the tests seem to be working fine on the previous PRs (from forks as well as internal branches). Was there anything special in the UI when you opened this PR?

[Xaphiosis]

All PR issues should now be addressed. I rebased, and did a re-indent pass on Fastpath_Equiv. Because of the rebase I'll wait for tests to succeed (am running them in parallel on a faster machine). For a better indentation script, I have to wait until the newer Isabelle and the Scala 3 stuff clears.