Title: Monad normalisation Authors: Joshua Schneider, Manuel Eberl and Andreas Lochbihler Submission date: 2017-05-05 Abstract: The usual monad laws can directly be used as rewrite rules for Isabelle’s simplifier to normalise monadic HOL terms and decide equivalences. In a commutative monad, however, the commutativity law is a higher-order permutative rewrite rule that makes the simplifier loop. This AFP entry implements a simproc that normalises monadic expressions in commutative monads using ordered rewriting. The simproc can also permute computations across control operators like if and case. BibTeX: @article{Monad_Normalisation-AFP, author = {Joshua Schneider and Manuel Eberl and Andreas Lochbihler}, title = {Monad normalisation}, journal = {Archive of Formal Proofs}, month = may, year = 2017, note = {\url{https://isa-afp.org/entries/Monad_Normalisation.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: CryptHOL, Randomised_BSTs, Skip_Lists