# Theory IMP

theory IMP imports Main begin
section ‹The language IMP›
text‹\label{sec:IMP}In this section we define a simple imperative programming
language. Syntax and operational semantics are as in \<^cite>‹"Winskel93"›,
except that we enrich the language with a single unnamed,
parameterless procedure. Both, this section and the following one
merely set the basis for the development described in the later
sections and largely follow the approach to formalize program logics
advocated by Kleymann, Nipkow, and others - see for example
\<^cite>‹"KleymannPhD" and "Nipkow-CSL02" and "Nipkow-AFP-AHL"›.›
subsection‹Syntax›
text‹We start from unspecified categories of program variables and
values.›
typedecl Var
typedecl Val
text‹Arithmetic expressions are inductively built up from variables,
values, and binary operators which are modeled as meta-logical
functions over values. Similarly, boolean expressions are built up
from arithmetic expressions using binary boolean operators which are
modeled as functions of the ambient logic HOL.›