Enlarge the trace monad rule set for RG logic

[corlewis]

This generally follows the structure and naming conventions of the existing rule set for Hoare logic, in Trace_VCG.thy and Trace_More_VCG.thy (and the very similar ruleset and files in the nondet directory).

I took the opportunity to make some changes as I went along. In particular:

• validIE_R and validIE_L are abbreviations instead of definitions.
• some lemmas were relocated to better follow the structure of the file and to improve reuse.
• some lemmas were renamed in an attempt to be more consistent.

It would be good to propagate the last two back to the Hoare versions, to keep things consistent and allow us to update the rest of the proofs now. The first one might not be worth it however, as it would require too many other changes to work.

Lemmas for lifting over combinators in the guarantee have been left out for now as it is unclear if they would be useful. They shouldn't be too hard to add if we come across a use case.

[lsf37]

Happy with that.

[lsf37]

It would be good to propagate the last two back to the Hoare versions, to keep things consistent and allow us to update the rest of the proofs now.

We probably should do that, at least if the lemma rename is not too intrusive and it doesn't take too long. It's easiest to do when the cache is still hot, but priority would be the refinement rules.

The first one might not be worth it however, as it would require too many other changes to work.

Agreed.