Download Isabelle Tutorial and User's Manual

104
Chapter 5. Defining Logics
The name of a rule can be an arbitrary string; the rule itself has to conform to the
syntax associated with the theory.
The following functions construct elements of the abstract type theory of theories in an incremental way:
pure thy: theory
enrich theory:
theory -> string -> sorts * ops * syntax -> rules -> theory
extend theory: theory -> string -> sorts * ops -> rules -> theory
merge theories: theory * theory -> theory
The abstract type syntax and the hierarchical definition of syntaxes is described in
Section 5.4.
pure_thy contains just the types, constants, and syntax of the meta-logic. Note
that there are no rules since meta-logical inferences are carried out by ml functions
as in lcf.
enrich theory thy s (sorts,ops,syn) axs
returns a new theory which enriches thy with the ground types in sorts, the
constants in ops, and the rules axs. The concrete syntax of the new theory is given by syn. Note that concrete syntaxes are also built up incrementally, but with a different set of functions described in Section 5.4. The
rules in axs are interpreted under the new signature. All Frees are replaced
by Vars, so that axioms can be written without question marks. The name
s of the new theory is there merely for reasons of documentation. Example:
enrich_theory pure_thy "int" (isorts,iops,syn) irls, where isorts, iops
and irls are as in Example 5.1 above and syn defines some appropriate syntax.
extend theory thy s (sorts,ops) axs
is equivalent to
enrich theory thy s (sorts,ops,syn) axs
where syn is the concrete syntax of theory thy. This is a simplified way of enriching
theories in case no new concrete syntax information has to be added. In essence,
this means that the signature extension involves only identifiers.
merge_theories(th1,th2) merges the two theories th1 and th2. The resulting
theory contains the union of all types, constants and axioms of the constituent
theories.
Isabelle does not support overloading, i.e. a theory cannot contain two constants
with the same name but different types. Trying to create such a theory by enriching
or merging raises an exception. Constants with the same name and the same type
are identified when theories are enriched or merged.
Axioms can be extracted from theories with the function
get axiom: theory -> string -> thm