Formalising Generalised Substitutions

Abstract. We use the theorem prover Isabelle to formalise and machinecheck results of the theory of generalised substitutions given by Dunne and used in the B method. We describe the model of computation implicit in this theory and show how this is based on a compound monad, and we contrast this model of computation and monad with those implicit in Dunne’s theory of abstract commands. Subject to a qualification concerning frames, we prove, using the Isabelle/HOL theorem prover, that Dunne’s results about generalised substitutions follow from the model of computation which we describe.

• Type: Conference
• Year: 2007
• Where: TPHOL
• Authors: Jeremy E. Dawson
• Keywords: Artificial Intelligence, Computation Implicit, Theorem Prover, Theorem Prover Isabelle, TPHOL 2007