Pure [isa-0017]

December 2, 2025
Liam O'Connor

Isabelle's logical framework consists of terms ( $t$ ), types ( $\tau$ ) and formulae ( $\varphi$ ). Each term $t$ must have a type $\tau$ , written $t :: \tau$ .

In the below code, we define a new type called bool, and we declare that terms of type bool can be used as judgments in our formulae. The details of the judgment command are not important for now.

typedecl bool judgment Trueprop :: "bool ⇒ prop" (‹(_)› 5)

Formulae in Isabelle are hereditary Harrop formulae, defined as:

\begin {array}{lclll} \varphi & ::= & \bigwedge x.\ \varphi & & \textit {(meta-forall)} \\ & \mid & \varphi \implies \varphi & & \textit {(meta-implication)}\\ & \mid & t & \text {where}\ t\ \text {:: \texttt {bool}} & \textit {(judgments)} \end {array}

In Isabelle's syntax, formulae, terms, and types are typically surrounded by quote marks "" or cartouches ‹› — the two are equivalent.