Abstract
Fixed-point constructions are fundamental to defining recursive and co-recursive functions.
However, a general axiom $Y f = f (Y f)$ leads to inconsistency, and definitions
must therefore be based on theories guaranteeing existence under suitable conditions.
In Isabelle/HOL, these constructions are typically based on sets, well-founded orders
or domain-theoretic models such as for example HOLCF.
In this submission we introduce a formalization of restriction spaces i.e. spaces
equipped with a so-called restriction, denoted by $\downarrow$,
satifying three properties:
\begin{align*}
& x \downarrow 0 = y \downarrow 0\\
& x \downarrow n \downarrow m = x \downarrow \mathrm{min} \ n \ m\\
& x \not = y \Longrightarrow \exists n. \ x \downarrow n \not = y \downarrow n
\end{align*}
They turn out to be cartesian closed and admit natural notions of constructiveness and
completeness, enabling the definition of a fixed-point operator under verifiable side-conditions.
This is achieved in our entry, from topological definitions to induction principles.
Additionally, we configure the simplifier so that it can automatically solve both
constructiveness and admissibility subgoals, as long as users write higher-order rules
for their operators.
Since our implementation relies on axiomatic type classes, the resulting library
is a fully abstract, flexible and reusable framework.