--- a/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 07 15:16:51 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 07 20:12:08 2006 +0200
@@ -11,7 +11,8 @@
\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.
+ differences in the specific treatment of simple types in
+ Isabelle/Pure.
Following type-theoretic parlance, the Pure logic consists of three
levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
@@ -20,8 +21,11 @@
@{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.
+ type constructors, term constants, and axioms. Theory declarations
+ support schematic polymorphism, which is strictly speaking outside
+ the logic.\footnote{Incidently, this is the main logical reason, why
+ the theory context @{text "\<Theta>"} is separate from the context @{text
+ "\<Gamma>"} of the core calculus.}
*}
@@ -34,46 +38,48 @@
\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.
+ generating relation; the transitive closure is maintained
+ internally. The resulting relation is an ordering: reflexive,
+ transitive, and antisymmetric.
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.
+ sorts according to the meaning of intersections: @{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 (finitely
+ many) classes declared in the current theory are the minimal
+ elements wrt.\ the sort order.
- \medskip A \emph{fixed type variable} is pair of a basic name
+ \medskip A \emph{fixed type variable} is a 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"}.
+ s)"} which is usually printed as @{text "?\<alpha>\<^isub>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.
+ of type variables, including the literal sort constraint. The core
+ logic handles type variables with the same name but different sorts
+ as different, although some outer layers of the system make it hard
+ to produce anything like this.
- A \emph{type constructor} is an @{text "k"}-ary type operator
- declared in the theory.
+ A \emph{type constructor} is a @{text "k"}-ary operator on types
+ declared in the theory. 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 "\<alpha> list"} instead of
+ @{text "(\<alpha>)list"}. Further notation is provided for specific
+ constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"}
+ instead of @{text "(\<alpha>, \<beta>)fun"} constructor.
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.
+ constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
+ (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
A \emph{type abbreviation} is a syntactic abbreviation of an
arbitrary type expression of the theory. Type abbreviations looks
@@ -82,26 +88,30 @@
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
+ s\<^isub>k)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 ::
+ sort @{text "s\<^isub>i"}. Arity declarations are implicitly
+ completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
+ (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
+
+ \medskip 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.
- The key property of the order-sorted algebra of types is that sort
+ The key property of a coregular order-sorted algebra 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.
+ s\<^isub>k)"} such that a type scheme @{text
+ "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
+ of sort @{text "s"}. Consequently, the unification problem on the
+ algebra of types has most general solutions (modulo renaming and
+ equivalence of sorts). Moreover, the usual type-inference algorithm
+ will produce primary types as expected \cite{nipkow-prehofer}.
*}
text %mlref {*
@@ -139,19 +149,19 @@
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.
+ is 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
+ type constructors @{text "c"} with @{text "k"} arguments and
optional mixfix syntax.
\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>"}.
+ defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
+ optional mixfix syntax.
\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"}.
+ class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
\item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
@@ -170,6 +180,13 @@
text {*
\glossary{Term}{FIXME}
+ The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
+ with de-Bruijn indices for bound variables, and named free
+ variables, and constants. Terms with loose bound variables are
+ usually considered malformed. The types of variables and constants
+ is stored explicitly at each occurrence in the term (which is a
+ known performance issue).
+
FIXME de-Bruijn representation of lambda terms
Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
@@ -193,13 +210,6 @@
*}
-section {* Proof terms *}
-
-text {*
- FIXME
-*}
-
-
section {* Theorems \label{sec:thms} *}
text {*
@@ -258,17 +268,54 @@
*}
-subsection {* Primitive inferences *}
+
+section {* Proof terms *}
-text FIXME
+text {*
+ FIXME !?
+*}
-subsection {* Higher-order resolution *}
+section {* Rules \label{sec:rules} *}
text {*
FIXME
+ A \emph{rule} is any Pure theorem in HHF normal form; there is a
+ separate calculus for rule composition, which is modeled after
+ Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
+ rules to be nested arbitrarily, similar to \cite{extensions91}.
+
+ Normally, all theorems accessible to the user are proper rules.
+ Low-level inferences are occasional required internally, but the
+ result should be always presented in canonical form. The higher
+ interfaces of Isabelle/Isar will always produce proper rules. It is
+ important to maintain this invariant in add-on applications!
+
+ There are two main principles of rule composition: @{text
+ "resolution"} (i.e.\ backchaining of rules) and @{text
+ "by-assumption"} (i.e.\ closing a branch); both principles are
+ combined in the variants of @{text "elim-resosultion"} and @{text
+ "dest-resolution"}. Raw @{text "composition"} is occasionally
+ useful as well, also it is strictly speaking outside of the proper
+ rule calculus.
+
+ Rules are treated modulo general higher-order unification, which is
+ unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
+ on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo
+ the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
+
+ This means that any operations within the rule calculus may be
+ subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common
+ practice not to contract or expand unnecessarily. Some mechanisms
+ prefer an one form, others the opposite, so there is a potential
+ danger to produce some oscillation!
+
+ Only few operations really work \emph{modulo} HHF conversion, but
+ expect a normal form: quantifiers @{text "\<And>"} before implications
+ @{text "\<Longrightarrow>"} at each level of nesting.
+
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
@@ -282,9 +329,4 @@
*}
-subsection {* Equational reasoning *}
-
-text FIXME
-
-
end