
diff -r 02bfd6d622ca -r 6faccf7d0f25 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Thu Mar 07 19:07:56 2002 +0100
+++ b/doc-src/IsarRef/logics.tex	Thu Mar 07 22:52:07 2002 +0100
@@ -18,11 +18,13 @@
 The very starting point for any Isabelle object-logic is a ``truth judgment''
 that links object-level statements to the meta-logic (with its minimal
 language of $prop$ that covers universal quantification $\Forall$ and
-implication $\Imp$).  Common object-logics are sufficiently expressive to
-\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
-language.  This is useful in certain situations where a rule needs to be
-viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
-\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
+implication $\Imp$).
+
+Common object-logics are sufficiently expressive to internalize rule
+statements over $\Forall$ and $\Imp$ within their own language.  This is
+useful in certain situations where a rule needs to be viewed as an atomic
+statement from the meta-level perspective, e.g.\ $\All x x \in A \Imp P(x)$
+versus $\forall x \in A. P(x)$.
 
 From the following language elements, only the $atomize$ method and
 $rule_format$ attribute are occasionally required by end-users, the rest is
@@ -31,34 +33,36 @@
 realistic examples.
 
 Generic tools may refer to the information provided by object-logic
-declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
-Reasoner \S\ref{sec:classical}).
+declarations internally.
+
+\railalias{ruleformat}{rule\_format}
+\railterm{ruleformat}
 
 \begin{rail}
   'judgment' constdecl
   ;
-  atomize ('(' 'full' ')')?
+  'atomize' ('(' 'full' ')')?
   ;
   ruleformat ('(' 'noasm' ')')?
   ;
 \end{rail}
 
 \begin{descr}
-
-\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
+  
+\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the
   truth judgment of the current object-logic.  Its type $\sigma$ should
   specify a coercion of the category of object-level propositions to $prop$ of
-  the Pure meta-logic; the mixfix annotation $syn$ would typically just link
+  the Pure meta-logic; the mixfix annotation $(mx)$ would typically just link
   the object language (internally of syntactic category $logic$) with that of
   $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
   theory development.
-
+  
 \item [$atomize$] (as a method) rewrites any non-atomic premises of a
   sub-goal, using the meta-level equations declared via $atomize$ (as an
   attribute) beforehand.  As a result, heavily nested goals become amenable to
   fundamental operations such as resolution (cf.\ the $rule$ method) and
   proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
-  here means to turn the subgoal into an object-statement (if possible),
+  here means to turn the whole subgoal into an object-statement (if possible),
   including the outermost parameters and assumptions as well.
 
   A typical collection of $atomize$ rules for a particular object-logic would
@@ -106,7 +110,7 @@
   
 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
   $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
-  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
+  also declares type arity $t :: (type, \dots, type) type$, making $t$ an
   actual HOL type constructor.
   
 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
@@ -120,21 +124,22 @@
   $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
   declaration).
   
-  Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic
-  characterization as a corresponding injection/surjection pair (in both
+  Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most
+  basic characterization as a corresponding injection/surjection pair (in both
   directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
-  more comfortable view on the injectivity part, suitable for automated proof
-  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules $Rep_t_cases$,
-  $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views
-  on surjectivity; these are already declared as type or set rules for the
-  generic $cases$ and $induct$ methods.
+  more convenient view on the injectivity part, suitable for automated proof
+  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules
+  $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide
+  alternative views on surjectivity; these are already declared as set or type
+  rules for the generic $cases$ and $induct$ methods.
 \end{descr}
 
-Raw type declarations are rarely used in practice; the main application is
-with experimental (or even axiomatic!) theory fragments.  Instead of primitive
-HOL type definitions, user-level theories usually refer to higher-level
-packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
-$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
+Note that raw type declarations are rarely used in practice; the main
+application is with experimental (or even axiomatic!) theory fragments.
+Instead of primitive HOL type definitions, user-level theories usually refer
+to higher-level packages such as $\isarkeyword{record}$ (see
+\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see
+\S\ref{sec:hol-datatype}).
 
 
 \subsection{Adhoc tuples}
@@ -153,13 +158,12 @@
 \end{rail}
 
 \begin{descr}
-
+  
 \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
   tuple types into canonical form as specified by the arguments given; $\vec
-  p@i$ refers to occurrences in premise $i$ of the rule.  The
-  $split_format~(complete)$ form causes \emph{all} arguments in function
-  applications to be represented canonically according to their tuple type
-  structure.
+  p@i$ refers to occurrences in premise $i$ of the rule.  The $(complete)$
+  option causes \emph{all} arguments in function applications to be
+  represented canonically according to their tuple type structure.
 
   Note that these operations tend to invent funny names for new local
   parameters to be introduced.
@@ -169,8 +173,8 @@
 
 \subsection{Records}\label{sec:hol-record}
 
-In principle, records merely generalize the concept of tuples where components
-may be addressed by labels instead of just position.  The logical
+In principle, records merely generalize the concept of tuples, where
+components may be addressed by labels instead of just position.  The logical
 infrastructure of records in Isabelle/HOL is slightly more advanced, though,
 supporting truly extensible record schemes.  This admits operations that are
 polymorphic with respect to record extension, yielding ``object-oriented''
@@ -203,8 +207,8 @@
 ``$\more$'' notation (which is actually part of the syntax).  The improper
 field ``$\more$'' of a record scheme is called the \emph{more part}.
 Logically it is just a free variable, which is occasionally referred to as
-\emph{row variable} in the literature.  The more part of a record scheme may
-be instantiated by zero or more further components.  For example, the above
+``row variable'' in the literature.  The more part of a record scheme may be
+instantiated by zero or more further components.  For example, the previous
 scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =
   m'}$, where $m'$ refers to a different more part.  Fixed records are special
 instances of record schemes, where ``$\more$'' is properly terminated by the
@@ -295,11 +299,11 @@
 reverse than in the actual term.  Since repeated updates are just function
 applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
   b\fs z \asn c}$, as far as logical equality is concerned.  Thus
-commutativity of updates can be proven within the logic for any two fields,
-but not as a general theorem: fields are not first-class values.
+commutativity of independent updates can be proven within the logic for any
+two fields, but not as a general theorem.
 
 \medskip The \textbf{make} operation provides a cumulative record constructor
-functions:
+function:
 \begin{matharray}{lll}
   t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
 \end{matharray}
@@ -336,25 +340,26 @@
     \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
 \end{matharray}
 
-\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
+\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.
 
 
 \subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms}
 
 The record package proves several results internally, declaring these facts to
 appropriate proof tools.  This enables users to reason about record structures
-quite comfortably.  Assume that $t$ is a record type as specified above.
+quite conveniently.  Assume that $t$ is a record type as specified above.
 
 \begin{enumerate}
-
+  
 \item Standard conversions for selectors or updates applied to record
   constructor terms are made part of the default Simplifier context; thus
   proofs by reduction of basic operations merely require the $simp$ method
-  without further arguments.  These rules are available as $t{\dtt}simps$.
-
+  without further arguments.  These rules are available as $t{\dtt}simps$,
+  too.
+  
 \item Selectors applied to updated records are automatically reduced by an
-  internal simplification procedure, which is also part of the default
-  Simplifier context.
+  internal simplification procedure, which is also part of the standard
+  Simplifier setup.
 
 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
   \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
@@ -368,10 +373,10 @@
   terms are provided both in $cases$ and $induct$ format (cf.\ the generic
   proof methods of the same name, \S\ref{sec:cases-induct}).  Several
   variations are available, for fixed records, record schemes, more parts etc.
-
+  
   The generic proof methods are sufficiently smart to pick the most sensible
   rule according to the type of the indicated record expression: users just
-  need to apply something like ``$(cases r)$'' to a certain proof problem.
+  need to apply something like ``$(cases~r)$'' to a certain proof problem.
 
 \item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
   $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
@@ -471,7 +476,7 @@
   
 \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   functions (using the TFL package), see also \cite{isabelle-HOL}.  The
-  $(permissive)$ option tells TFL to recover from failed proof attempts,
+  ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
   returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
   $recdef_wf$ hints refer to auxiliary rules to be used in the internal
   automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
@@ -496,8 +501,8 @@
 $\isarkeyword{recdef}$ are numbered (starting from $1$).
 
 The equations provided by these packages may be referred later as theorem list
-$f\mathord.simps$, where $f$ is the (collective) name of the functions
-defined.  Individual equations may be named explicitly as well; note that for
+$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
+Individual equations may be named explicitly as well; note that for
 $\isarkeyword{recdef}$ each specification given by the user may result in
 several theorems.
 
@@ -631,10 +636,10 @@
   both goal addressing and dynamic instantiation.  Note that named rule cases
   are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
   methods (see \S\ref{sec:cases-induct}).
-
+  
 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
-  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
-  forward manner.
+  to the internal \texttt{mk_cases} operation.  Rules are simplified in an
+  unrestricted forward manner.
 
   While $ind_cases$ is a proof method to apply the result immediately as
   elimination rules, $\isarkeyword{inductive_cases}$ provides case split
@@ -648,7 +653,7 @@
 from executable specifications, both functional and relational programs.
 Isabelle/HOL instantiates these mechanisms in a way that is amenable to
 end-user applications.  See \cite{isabelle-HOL} for further information (this
-actually covers the new-style theory format).
+actually covers the new-style theory format as well).
 
 \indexisarcmd{generate-code}\indexisarcmd{consts-code}\indexisarcmd{types-code}
 \indexisaratt{code}
@@ -727,10 +732,10 @@
   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
 \end{rail}
 
-Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
-\S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor
+Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
+\S\ref{sec:hol-datatype}).  Mutual recursion is supported, but no nesting nor
 arbitrary branching.  Domain constructors may be strict (default) or lazy, the
-latter admits to introduce infinitary objects in the typical LCF manner (e.g.\
+latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 
 lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
 domains.
 
@@ -742,7 +747,7 @@
 The ZF logic is essentially untyped, so the concept of ``type checking'' is
 performed as logical reasoning about set-membership statements.  A special
 method assists users in this task; a version of this is already declared as a
-``solver'' in the default Simplifier context.
+``solver'' in the standard Simplifier setup.
 
 \indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
 
@@ -779,7 +784,7 @@
 
 In ZF everything is a set.  The generic inductive package also provides a
 specific view for ``datatype'' specifications.  Coinductive definitions are
-available as well.
+available in both cases, too.
 
 \indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
 \indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}




