Activities per year
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.
|Number of pages||6|
|Publication status||Unpublished - 5 Apr 2018|