Kleene Algebra in Unifying Theories of Programming
Simon Foster · White Rose Research Online (University of Leeds, The University of Sheffield, University of York) · 2018
This development links Isabelle/UTP to the mechanised Kleene Algebra (KA) hiearchy for Isabelle/HOL. We substantiate the required KA laws, and provides a large body of additional theorems for alphabetised relations which are provided by the KA library. Additionally, we show how such theorems can be lifted to a subclass of UTP theories, provided certain conditions hold.