--- a/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 05 22:05:41 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Tue Sep 05 22:05:49 2006 +0200
@@ -23,30 +23,159 @@
}
\isamarkuptrue%
%
+\begin{isamarkuptext}%
+The logical foundations of Isabelle/Isar are that of the Pure logic,
+ which has been introduced as a natural-deduction framework in
+ \cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract framework of Pure Type Systems (PTS)
+ \cite{Barendregt-Geuvers:2001}, although there are some key
+ differences in the practical treatment of simple types.
+
+ Following type-theoretic parlance, the Pure logic consists of three
+ levels of \isa{{\isasymlambda}}-calculus with corresponding arrows: \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and
+ \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs).
+
+ Pure derivations are relative to a logical theory, which declares
+ type constructors, term constants, and axioms. Term constants and
+ axioms support schematic polymorphism.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Types \label{sec:types}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\glossary{Type class}{FIXME}
+The language of types is an uninterpreted order-sorted first-order
+ algebra; types are qualified by ordered type classes.
- \glossary{Type arity}{FIXME}
+ \medskip A \emph{type class} is an abstract syntactic entity
+ declared in the theory context. The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic
+ generating relation; the transitive closure maintained internally.
- \glossary{Sort}{FIXME}
+ A \emph{sort} is a list of type classes written as \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic
+ intersection. Notationally, the curly braces are omitted for
+ singleton intersections, i.e.\ any class \isa{c} may be read as
+ a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering on type classes is extended to
+ sorts in the canonical fashion: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the
+ universal sort, which is the largest element wrt.\ the sort order.
+ The intersections of all (i.e.\ finitely many) classes declared in
+ the current theory are the minimal elements wrt.\ sort order.
- FIXME classes and sorts
+ \medskip A \emph{fixed type variable} is pair of a basic name
+ (starting with \isa{{\isacharprime}} character) and a sort constraint. For
+ example, \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}. A \emph{schematic type variable} is a pair of an
+ indexname and a sort constraint. For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.
+
+ Note that \emph{all} syntactic components contribute to the identity
+ of a type variables, including the literal sort constraint. The
+ core logic handles type variables with the same name but different
+ sorts as different, even though the outer layers of the system make
+ it hard to produce anything like this.
+ A \emph{type constructor} is an \isa{k}-ary type operator
+ declared in the theory.
+
+ A \emph{type} is defined inductively over type variables and type
+ constructors: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}. Type constructor application is usually written
+ postfix. For \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\
+ \isa{prop} instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the
+ parentheses are omitted, e.g.\ \isa{{\isasymtau}\ list} instead of \isa{{\isacharparenleft}{\isasymtau}{\isacharparenright}\ list}. Further notation is provided for specific
+ constructors, notably right-associative infix \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub {\isadigit{2}}} instead of \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymtau}\isactrlisub {\isadigit{2}}{\isacharparenright}fun}
+ constructor.
- \glossary{Type}{FIXME}
+ A \emph{type abbreviation} is a syntactic abbreviation of an
+ arbitrary type expression of the theory. Type abbreviations looks
+ like type constructors at the surface, but are expanded before the
+ core logic encounters them.
- \glossary{Type constructor}{FIXME}
+ A \emph{type arity} declares the image behavior of a type
+ constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub n{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is
+ of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of
+ sort \isa{s\isactrlisub i}. The sort algebra is always maintained as
+ \emph{coregular}, which means that type arities are consistent with
+ the subclass relation: for each type constructor \isa{c} and
+ classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts.
- \glossary{Type variable}{FIXME}
-
- FIXME simple types%
+ The key property of the order-sorted algebra of types is that sort
+ constraints may be always fulfilled in a most general fashion: for
+ each type constructor \isa{c} and sort \isa{s} there is a
+ most general vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such that \isa{{\isacharparenleft}{\isasymtau}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}} for arbitrary \isa{{\isasymtau}\isactrlisub i} of
+ sort \isa{s\isactrlisub i}. This means the unification problem on
+ the algebra of types has most general solutions (modulo renaming and
+ equivalence of sorts). As a consequence, type-inference is able to
+ produce primary types.%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexmltype{class}\verb|type class| \\
+ \indexmltype{sort}\verb|type sort| \\
+ \indexmltype{typ}\verb|type typ| \\
+ \indexmltype{arity}\verb|type arity| \\
+ \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
+ \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
+ \indexml{Sign.add-types}\verb|Sign.add_types: (bstring * int * mixfix) list -> theory -> theory| \\
+ \indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
+\verb| (bstring * string list * typ * mixfix) list -> theory -> theory| \\
+ \indexml{Sign.primitive-class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
+ \indexml{Sign.primitive-classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
+ \indexml{Sign.primitive-arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|class| represents type classes; this is an alias for
+ \verb|string|.
+
+ \item \verb|sort| represents sorts; this is an alias for
+ \verb|class list|.
+
+ \item \verb|arity| represents type arities; this is an alias for
+ triples of the form \isa{{\isacharparenleft}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.
+
+ \item \verb|typ| represents types; this is a datatype with
+ constructors \verb|TFree|, \verb|TVar|, \verb|Type|.
+
+ \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}}
+ tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.
+
+ \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether a type
+ expression of of a given sort.
+
+ \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new
+ type constructors \isa{c} with \isa{k} arguments, and
+ optional mixfix syntax.
+
+ \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
+ defines type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c} (with optional
+ mixfix syntax) as \isa{{\isasymtau}}.
+
+ \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with
+ class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}.
+
+ \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}.
+
+ \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares
+ arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsection{Terms \label{sec:terms}%
}
\isamarkuptrue%
@@ -54,7 +183,14 @@
\begin{isamarkuptext}%
\glossary{Term}{FIXME}
- FIXME de-Bruijn representation of lambda terms%
+ FIXME de-Bruijn representation of lambda terms
+
+ Term syntax provides explicit abstraction \isa{{\isasymlambda}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ b{\isacharparenleft}x{\isacharparenright}}
+ and application \isa{t\ u}, while types are usually implicit
+ thanks to type-inference.
+
+ Terms of type \isa{prop} are called
+ propositions. Logical statements are composed via \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{A\ {\isasymLongrightarrow}\ B}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -81,7 +217,20 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME
+Primitive reasoning operates on judgments of the form \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, with standard introduction and elimination rules for \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} that refer to fixed parameters \isa{x} and
+ hypotheses \isa{A} from the context \isa{{\isasymGamma}}. The
+ corresponding proof terms are left implicit in the classic
+ ``LCF-approach'', although they could be exploited separately
+ \cite{Berghofer-Nipkow:2000}.
+
+ The framework also provides definitional equality \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop}, with \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion rules. The internal
+ conjunction \isa{{\isacharampersand}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} enables the view of
+ assumptions and conclusions emerging uniformly as simultaneous
+ statements.
+
+
+
+ FIXME
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
\isa{prop}. Internally, there is nothing special about
@@ -155,24 +304,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Raw theories%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
-theory context, but slightly more flexible since it may be used at
-different type-instances, due to \seeglossary{schematic
-polymorphism.}}
-
-\glossary{Axiom}{FIXME}
-
-\glossary{Primitive definition}{FIXME}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Sep 05 22:05:41 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Sep 05 22:05:49 2006 +0200
@@ -692,7 +692,7 @@
\begin{itemize}
- \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}}.
+ \item \isa{{\isacharquery}x} if \isa{x} does not end with a digit and \isa{i\ {\isacharequal}\ {\isadigit{0}}},
\item \isa{{\isacharquery}xi} if \isa{x} does not end with a digit,
@@ -750,32 +750,26 @@
name components. The packed representation a dot as separator, for
example in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called
\emph{base} name, the remaining prefix \emph{qualifier} (which may
- be empty).
+ be empty). The basic idea of qualified names is to encode a
+ hierarchically structured name spaces by recording the access path
+ as part of the name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood
+ as a local entity \isa{c} within a local structure \isa{b}
+ of the enclosing structure \isa{A}. Typically, name space
+ hierarchies consist of 1--3 levels, but this need not be always so.
The empty name is commonly used as an indication of unnamed
entities, if this makes any sense. The operations on qualified
names are smart enough to pass through such improper names
unchanged.
- The basic idea of qualified names is to encode a hierarchically
- structured name spaces by recording the access path as part of the
- name. For example, \isa{A{\isachardot}b{\isachardot}c} may be understood as a local
- entity \isa{c} within a local structure \isa{b} of the
- enclosing structure \isa{A}. Typically, name space hierarchies
- consist of 1--3 levels, but this need not be always so.
-
\medskip A \isa{naming} policy tells how to turn a name
specification into a fully qualified internal name (by the \isa{full} operation), and how to fully qualified names may be accessed
- externally.
-
- For example, the default naming prefixes an implicit path from the
- context: \isa{x} is becomes \isa{path{\isachardot}x} internally; the
- standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further
- partial \isa{path} specifications.
-
+ externally. For example, the default naming prefixes an implicit
+ path from the context: \isa{x} is becomes \isa{path{\isachardot}x}
+ internally; the standard accesses include \isa{x}, \isa{path{\isachardot}x}, and further partial \isa{path} specifications.
Normally, the naming is implicit in the theory or proof context.
- There are separate versions of the corresponding operations for these
- context types.
+ There are separate versions of the corresponding operations for
+ these context types.
\medskip A \isa{name\ space} manages a collection of fully
internalized names, together with a mapping between external names
@@ -787,19 +781,18 @@
of formal entity, such as logical constant, type, type class,
theorem etc. It is usually clear from the occurrence in concrete
syntax (or from the scope) which kind of entity a name refers to.
-
For example, the very same name \isa{c} may be used uniformly
for a constant, type, type class, which are from separate syntactic
- categories. There is a common convention to name theorems
- systematically, according to the name of the main logical entity
- being involved, such as \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for
- theorems related to constant \isa{c}.
+ categories.
- This technique of mapping names from one space into another requires
- some care in order to avoid conflicts. In particular, theorem names
- derived from type or class names are better suffixed in addition to
- the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c} and class
- \isa{c}, respectively.%
+ There are common schemes to name theorems systematically, according
+ to the name of the main logical entity being involved, such as
+ \isa{c{\isachardot}intro} and \isa{c{\isachardot}elim} for theorems related to
+ constant \isa{c}. This technique of mapping names from one
+ space into another requires some care in order to avoid conflicts.
+ In particular, theorem names derived from type or class names are
+ better suffixed in addition to the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to
+ type \isa{c} and class \isa{c}, respectively.%
\end{isamarkuptext}%
\isamarkuptrue%
%