Theory Iteration
section ‹Iteration›
theory Iteration imports Well_Sorted_Terms
begin
text‹In this section, we introduce first-order models (models, for short).
These are structures having operators that
match those for terms (including variable-injection, binding operations, freshness,
swapping and substitution) and satisfy some clauses,
and show that terms form initial models. This gives iteration principles.
As a matter of notation: the prefix
``g" will stand for ``generalized" -- elements of models are referred to as ``generalized terms".
The actual full prefix will be ``ig" (where ``i" stands for ``iteration"), symbolizing the fact that
the models from this section support iteration, and not general recursion.
The latter is dealt with by the models introduced in the next section, for which we
use the simple prefix ``g".
›
subsection ‹Models›
text‹We have two basic kinds of models:
\\- fresh-swap (FSw) models, featuring operations corresponding to
the concrete syntactic constructs (``Var", ``Op", ``Abs"),
henceforth referred to simply as {\em the constructs}, and to fresh and swap;
\\- fresh-swap-subst (FSb) models, featuring substitution instead of swapping.
We also consider two combinations of the above, FSwSb-models and FSbSw-models.
To keep things structurally
simple, we use one single Isabelle for all the 4 kinds models,
allowing the most generous signature.
Since terms are the main actors of our theory, models being considered only
for the sake of recursive definitions, we call the items inhabiting these models
``generalized" terms, abstractions and inputs, and correspondingly
the operations; hence the prefix ``g" from the names of the type parameters and
operators.
(However,
we refer to the generalized items using the same notations as for
``concrete items": X, A, etc.)
%
Indeed, a model can be regarded as implementing
a generalization/axiomatization of the term structure, where now the objects are
not terms, but do have term-like properties.
›
subsubsection ‹Raw models›