backport Lib enhancements from `rt` branch

[lsf37]

The MCS proofs for AInvs and Refine produced a number of enhancements and additional lemmas in the Lib session.

We should backport these to master to reduce merge effort later and to make use of them in new proofs.

[lsf37]

Ideally we'd do this by cherry-picking the relevant commits similar to #468. This only works if proof adjustments are minimal.

The list of files with relevant differences currently is:

• lib/BCorres_UL.thy
• lib/Corres_UL.thy
• lib/EmptyFailLib.thy
• lib/ExtraCorres.thy
• lib/HaskellLemmaBucket.thy
• lib/HaskellLib_H.thy
• lib/LemmaBucket.thy
• lib/Lib.thy
• lib/ListLibLemmas.thy
• lib/List_Lib.thy
• lib/Monad_WP/NonDetMonad.thy
• lib/Monad_WP/NonDetMonadVCG.thy
• lib/Monad_WP/OptionMonadWP.thy
• lib/Monad_WP/WhileLoopRules.thy
• lib/MonadicRewrite.thy
• lib/NonDetMonadLemmaBucket.thy
• lib/Word_Lib/Word_Lemmas.thy
• lib/Word_Lib/Word_Lemmas_Internal.thy

The following are new in rt and not used in master, so probably should be left for now:

• lib/Heap_List.thy
• lib/Log.thy