doc-src/IsarImplementation/Thy/logic.thy
changeset 20480 4e0522d38968
parent 20477 e623b0e30541
child 20491 98ba42f19995
--- 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