--- a/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 05 22:05:15 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Tue Sep 05 22:05:41 2006 +0200
@@ -5,34 +5,180 @@
chapter {* Primitive logic \label{ch:logic} *}
+text {*
+ 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 ``@{text
+ "\<lambda>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 @{text "\<lambda>"}-calculus with corresponding arrows: @{text
+ "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
+ "\<And>"} for universal quantification (proofs depending on terms), and
+ @{text "\<Longrightarrow>"} 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.
+*}
+
+
section {* Types \label{sec:types} *}
text {*
- \glossary{Type class}{FIXME}
+ The language of types is an uninterpreted order-sorted first-order
+ algebra; types are qualified by ordered type classes.
+
+ \medskip A \emph{type class} is an abstract syntactic entity
+ declared in the theory context. The \emph{subclass relation} @{text
+ "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
+ generating relation; the transitive closure maintained internally.
- \glossary{Type arity}{FIXME}
+ A \emph{sort} is a list of type classes written as @{text
+ "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
+ intersection. Notationally, the curly braces are omitted for
+ singleton intersections, i.e.\ any class @{text "c"} may be read as
+ a sort @{text "{c}"}. The ordering on type classes is extended to
+ sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
+ {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
+ d\<^isub>j"}. The empty intersection @{text "{}"} 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.
+
+ \medskip A \emph{fixed type variable} is pair of a basic name
+ (starting with @{text "'"} character) and a sort constraint. For
+ example, @{text "('a, s)"} which is usually printed as @{text
+ "\<alpha>\<^isub>s"}. A \emph{schematic type variable} is a pair of an
+ indexname and a sort constraint. For example, @{text "(('a, 0),
+ s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
- \glossary{Sort}{FIXME}
+ 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.
- FIXME classes and sorts
+ A \emph{type constructor} is an @{text "k"}-ary type operator
+ declared in the theory.
+
+ A \emph{type} is defined inductively over type variables and type
+ constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
+ \<tau>\<^sub>k)c"}. Type constructor application is usually written
+ postfix. For @{text "k = 0"} the argument tuple is omitted, e.g.\
+ @{text "prop"} instead of @{text "()prop"}. For @{text "k = 1"} the
+ parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
+ "(\<tau>) list"}. Further notation is provided for specific
+ constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
+ \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
+ constructor.
+ 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.
+
+ A \emph{type arity} declares the image behavior of a type
+ constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
+ s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
+ of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
+ sort @{text "s\<^isub>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 @{text "c"} and
+ classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
+ (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
+ :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
+ \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
- \glossary{Type}{FIXME}
+ 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 @{text "c"} and sort @{text "s"} there is a
+ most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
+ s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
+ \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
+ sort @{text "s\<^isub>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.
+*}
- \glossary{Type constructor}{FIXME}
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type class} \\
+ @{index_ML_type sort} \\
+ @{index_ML_type typ} \\
+ @{index_ML_type arity} \\
+ @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
+ @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
+ @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.add_tyabbrs_i: "
+ (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
+ @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
+ @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type class} represents type classes; this is an alias for
+ @{ML_type string}.
+
+ \item @{ML_type sort} represents sorts; this is an alias for
+ @{ML_type "class list"}.
- \glossary{Type variable}{FIXME}
+ \item @{ML_type arity} represents type arities; this is an alias for
+ triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
+ (\<^vec>s)s"} described above.
+
+ \item @{ML_type typ} represents types; this is a datatype with
+ constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
+
+ \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
+ tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
+
+ \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
+ expression of of a given sort.
+
+ \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
+ type constructors @{text "c"} with @{text "k"} arguments, and
+ optional mixfix syntax.
- FIXME simple types
+ \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
+ defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional
+ mixfix syntax) as @{text "\<tau>"}.
+
+ \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
+ c\<^isub>n])"} declares new class @{text "c"} derived together with
+ class relations @{text "c \<subseteq> c\<^isub>i"}.
+
+ \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
+ c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
+ c\<^isub>2"}.
+
+ \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
+ arity @{text "c :: (\<^vec>s)s"}.
+
+ \end{description}
*}
+
section {* Terms \label{sec:terms} *}
text {*
\glossary{Term}{FIXME}
FIXME de-Bruijn representation of lambda terms
+
+ Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
+ and application @{text "t u"}, while types are usually implicit
+ thanks to type-inference.
+
+ Terms of type @{text "prop"} are called
+ propositions. Logical statements are composed via @{text "\<And>x ::
+ \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
*}
@@ -58,6 +204,22 @@
text {*
+ Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
+ \<phi>"}, with standard introduction and elimination rules for @{text
+ "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
+ hypotheses @{text "A"} from the context @{text "\<Gamma>"}. 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 @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
+ \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules. The internal
+ conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
+ assumptions and conclusions emerging uniformly as simultaneous
+ statements.
+
+
+
FIXME
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
@@ -100,6 +262,7 @@
text FIXME
+
subsection {* Higher-order resolution *}
text {*
@@ -124,21 +287,4 @@
text FIXME
-section {* Raw theories *}
-
-text {*
-
-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