Monad normalisation: 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.
Keywords for this software
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2020)