Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Monad normalisation

Email Gateway (Aug 22 2022 at 15:28):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Monad normalisation
by Joshua Schneider, Manuel Eberl, and Andreas Lochbihler

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.

Enjoy 2/5

Last updated: Nov 21 2024 at 12:39 UTC