diff -r c4cd36411983 -r 9700a87f1cc2 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Tue Feb 02 11:47:49 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Tue Feb 02 12:37:57 2010 +0100
@@ -24,7 +24,9 @@
   schematic polymorphism, which is strictly speaking outside the
   logic.\footnote{This is the deeper logical reason, why the theory
   context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}
-  of the core calculus.}
+  of the core calculus: type constructors, term constants, and facts
+  (proof constants) may involve arbitrary type schemes, but the type
+  of a locally fixed term parameter is also fixed!}
 *}
 
 
@@ -41,18 +43,17 @@
   internally.  The resulting relation is an ordering: reflexive,
   transitive, and antisymmetric.
 
-  A \emph{sort} is a list of type classes written as @{text "s =
-  {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 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.
+  A \emph{sort} is a list of type classes written as @{text "s = {c\<^isub>1,
+  \<dots>, c\<^isub>m}"}, it 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 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.  Thus @{text "{}"} represents the ``full sort'', not the
+  empty one!  The intersection of all (finitely many) classes declared
+  in the current theory is the least element wrt.\ the sort ordering.
 
   \medskip A \emph{fixed type variable} is a pair of a basic name
   (starting with a @{text "'"} character) and a sort constraint, e.g.\
@@ -62,10 +63,10 @@
   printed as @{text "?\<alpha>\<^isub>s"}.
 
   Note that \emph{all} syntactic components contribute to the identity
-  of type variables, including the 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.
+  of type variables: basic name, index, and sort constraint.  The core
+  logic handles type variables with the same name but different sorts
+  as different, although the type-inference layer (which is outside
+  the core) rejects anything like that.
 
   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
   on types declared in the theory.  Type constructor application is
@@ -77,8 +78,8 @@
   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
   \<beta>)fun"}.
   
-  A \emph{type} is defined inductively over type variables and type
-  constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
+  The logical category \emph{type} is defined inductively over type
+  variables and type constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}.
 
   A \emph{type abbreviation} is a syntactic definition @{text
@@ -193,15 +194,13 @@
   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   or \cite{paulson-ml2}), with the types being determined by the
   corresponding binders.  In contrast, free variables and constants
-  are have an explicit name and type in each occurrence.
+  have an explicit name and type in each occurrence.
 
   \medskip A \emph{bound variable} is a natural number @{text "b"},
   which accounts for the number of intermediate binders between the
   variable occurrence in the body and its binding position.  For
-  example, the de-Bruijn term @{text
-  "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would
-  correspond to @{text
-  "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named
+  example, the de-Bruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would
+  correspond to @{text "\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y"} in a named
   representation.  Note that a bound variable may be represented by
   different de-Bruijn indices at different occurrences, depending on
   the nesting of abstractions.
@@ -213,27 +212,27 @@
   without any loose variables.
 
   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
-  @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}.  A
+  @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"} here.  A
   \emph{schematic variable} is a pair of an indexname and a type,
-  e.g.\ @{text "((x, 0), \<tau>)"} which is usually printed as @{text
+  e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text
   "?x\<^isub>\<tau>"}.
 
   \medskip A \emph{constant} is a pair of a basic name and a type,
-  e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text
-  "c\<^isub>\<tau>"}.  Constants are declared in the context as polymorphic
-  families @{text "c :: \<sigma>"}, meaning that all substitution instances
-  @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
+  e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^isub>\<tau>"}
+  here.  Constants are declared in the context as polymorphic families
+  @{text "c :: \<sigma>"}, meaning that all substitution instances @{text
+  "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.
 
-  The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"}
-  wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of
-  the matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>,
-  ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in canonical order @{text
-  "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  Within a given theory context,
-  there is a one-to-one correspondence between any constant @{text
-  "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1, \<dots>,
-  \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus
-  :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow>
-  nat\<^esub>"} corresponds to @{text "plus(nat)"}.
+  The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"} wrt.\
+  the declaration @{text "c :: \<sigma>"} is defined as the codomain of the
+  matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>, ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in
+  canonical order @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}, corresponding to the
+  left-to-right occurrences of the @{text "\<alpha>\<^isub>i"} in @{text "\<sigma>"}.
+  Within a given theory context, there is a one-to-one correspondence
+  between any constant @{text "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1,
+  \<dots>, \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus :: \<alpha>
+  \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} corresponds to
+  @{text "plus(nat)"}.
 
   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   for type variables in @{text "\<sigma>"}.  These are observed by
@@ -242,14 +241,13 @@
   polymorphic constants that the user-level type-checker would reject
   due to violation of type class restrictions.
 
-  \medskip An \emph{atomic} term is either a variable or constant.  A
-  \emph{term} is defined inductively over atomic terms, with
-  abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> |
-  ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.
-  Parsing and printing takes care of converting between an external
-  representation with named bound variables.  Subsequently, we shall
-  use the latter notation instead of internal de-Bruijn
-  representation.
+  \medskip An \emph{atomic} term is either a variable or constant.
+  The logical category \emph{term} is defined inductively over atomic
+  terms, with abstraction and application as follows: @{text "t = b |
+  x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes care of
+  converting between an external representation with named bound
+  variables.  Subsequently, we shall use the latter notation instead
+  of internal de-Bruijn representation.
 
   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a
   term according to the structure of atomic terms, abstractions, and
@@ -271,18 +269,17 @@
 
   The identity of atomic terms consists both of the name and the type
   component.  This means that different variables @{text
-  "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text
-  "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type
-  instantiation.  Some outer layers of the system make it hard to
-  produce variables of the same name, but different types.  In
-  contrast, mixed instances of polymorphic constants occur frequently.
+  "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after
+  type instantiation.  Type-inference rejects variables of the same
+  name, but different types.  In contrast, mixed instances of
+  polymorphic constants occur routinely.
 
   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   is the set of type variables occurring in @{text "t"}, but not in
-  @{text "\<sigma>"}.  This means that the term implicitly depends on type
-  arguments that are not accounted in the result type, i.e.\ there are
-  different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text
-  "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
+  its type @{text "\<sigma>"}.  This means that the term implicitly depends
+  on type arguments that are not accounted in the result type, i.e.\
+  there are different type instances @{text "t\<vartheta> :: \<sigma>"} and
+  @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly
   pathological situation notoriously demands additional care.
 
   \medskip A \emph{term abbreviation} is a syntactic definition @{text
@@ -431,14 +428,14 @@
   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   \]
   \[
-  \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
+  \infer[@{text "(\<And>\<dash>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}
   \qquad
-  \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
+  \infer[@{text "(\<And>\<dash>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}
   \]
   \[
-  \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
+  \infer[@{text "(\<Longrightarrow>\<dash>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   \qquad
-  \infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
+  \infer[@{text "(\<Longrightarrow>\<dash>elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
   \]
   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   \end{center}
@@ -467,21 +464,21 @@
   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\
   \cite{Berghofer-Nipkow:2000:TPHOL}).
 
-  Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need
-  not be recorded in the hypotheses, because the simple syntactic
-  types of Pure are always inhabitable.  ``Assumptions'' @{text "x ::
-  \<tau>"} for type-membership are only present as long as some @{text
-  "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key
-  difference to ``@{text "\<lambda>HOL"}'' in the PTS framework
-  \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are
-  treated uniformly for propositions and types.}
+  Observe that locally fixed parameters (as in @{text
+  "\<And>\<dash>intro"}) need not be recorded in the hypotheses, because
+  the simple syntactic types of Pure are always inhabitable.
+  ``Assumptions'' @{text "x :: \<tau>"} for type-membership are only
+  present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement
+  body.\footnote{This is the key difference to ``@{text "\<lambda>HOL"}'' in
+  the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
+  @{text "x : A"} are treated uniformly for propositions and types.}
 
   \medskip The axiomatization of a theory is implicitly closed by
   forming all instances of type and term variables: @{text "\<turnstile>
   A\<vartheta>"} holds for any substitution instance of an axiom
   @{text "\<turnstile> A"}.  By pushing substitutions through derivations
   inductively, we also get admissible @{text "generalize"} and @{text
-  "instance"} rules as shown in \figref{fig:subst-rules}.
+  "instantiate"} rules as shown in \figref{fig:subst-rules}.
 
   \begin{figure}[htb]
   \begin{center}
@@ -588,11 +585,11 @@
   Every @{ML thm} value contains a sliding back-reference to the
   enclosing theory, cf.\ \secref{sec:context-theory}.
 
-  \item @{ML proofs} determines the detail of proof recording within
+  \item @{ML proofs} specifies the detail of proof recording within
   @{ML_type thm} values: @{ML 0} records only the names of oracles,
   @{ML 1} records oracle names and propositions, @{ML 2} additionally
   records full proof terms.  Officially named theorems that contribute
-  to a result are always recorded.
+  to a result are recorded in any case.
 
   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
@@ -644,8 +641,8 @@
   \begin{figure}[htb]
   \begin{center}
   \begin{tabular}{ll}
-  @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
-  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
+  @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&&&"}) \\
+  @{text "\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\
   @{text "#A \<equiv> A"} \\[1ex]
   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
@@ -657,13 +654,15 @@
   \end{center}
   \end{figure}
 
-  Derived conjunction rules include introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &
-  B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.
-  Conjunction allows to treat simultaneous assumptions and conclusions
-  uniformly.  For example, multiple claims are intermediately
-  represented as explicit conjunction, but this is refined into
-  separate sub-goals before the user continues the proof; the final
-  result is projected into a list of theorems (cf.\
+  The introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &&& B"}, and eliminations
+  (projections) @{text "A &&& B \<Longrightarrow> A"} and @{text "A &&& B \<Longrightarrow> B"} are
+  available as derived rules.  Conjunction allows to treat
+  simultaneous assumptions and conclusions uniformly, e.g.\ consider
+  @{text "A \<Longrightarrow> B \<Longrightarrow> C &&& D"}.  In particular, the goal mechanism
+  represents multiple claims as explicit conjunction internally, but
+  this is refined (via backwards introduction) into separate sub-goals
+  before the user commences the proof; the final result is projected
+  into a list of theorems using eliminations (cf.\
   \secref{sec:tactical-goals}).
 
   The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex
@@ -681,7 +680,7 @@
   language of types into that of terms.  There is specific notation
   @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
  itself\<^esub>"}.
-  Although being devoid of any particular meaning, the @{text
+  Although being devoid of any particular meaning, the term @{text
   "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term
   language.  In particular, @{text "TYPE(\<alpha>)"} may be used as formal
   argument in primitive definitions, in order to circumvent hidden
@@ -703,11 +702,11 @@
 
   \begin{description}
 
-  \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text
+  \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text
   "A"} and @{text "B"}.
 
   \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}
-  from @{text "A & B"}.
+  from @{text "A &&& B"}.
 
   \item @{ML Drule.mk_term} derives @{text "TERM t"}.
 
@@ -784,7 +783,8 @@
   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded
   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this
-  already marks the limit of rule complexity seen in practice.
+  already marks the limit of rule complexity that is usually seen in
+  practice.
 
   \medskip Regular user-level inferences in Isabelle/Pure always
   maintain the following canonical form of results:
@@ -890,11 +890,10 @@
 
   \begin{description}
 
-  \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text
-  "rule\<^sub>1"} with @{text "rule\<^sub>2"} according to the
-  @{inference resolution} principle explained above.  Note that the
-  corresponding attribute in the Isar language is called @{attribute
-  THEN}.
+  \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text "rule\<^sub>1"} with @{text
+  "rule\<^sub>2"} according to the @{inference resolution} principle
+  explained above.  Note that the corresponding rule attribute in the
+  Isar language is called @{attribute THEN}.
 
   \item @{text "rule OF rules"} resolves a list of rules with the
   first rule, addressing its premises @{text "1, \<dots>, length rules"}