Reasoning with inductively defined relations in the HOL theorem prover
Juanito Camilleri, Tom Melham · 2021
Abstract: Inductively defined relations are among the basic mathematical tools of computer science. Examples include evaluation and computation relations in structural operational semantics, labelled transition relations in process algebra semantics, inductively-defined typing judgements, and proof systems in general. This paper describes a set of HOL theorem-proving tools for reasoning about such inductively defined relations. We also describe a suite of worked examples using these tools. First printed: August 1992