Monad Normalisation

Joshua Schneider, Manuel Eberl 🌐 and Andreas Lochbihler 🌐

May 5, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Monad_Normalisation