doc-src/IsarRef/logics.tex
changeset 13041 6faccf7d0f25
parent 13039 cfcc1f6f21df
child 13042 d8a345d9e067
     1.1 --- a/doc-src/IsarRef/logics.tex	Thu Mar 07 19:04:00 2002 +0100
     1.2 +++ b/doc-src/IsarRef/logics.tex	Thu Mar 07 22:52:07 2002 +0100
     1.3 @@ -18,11 +18,13 @@
     1.4  The very starting point for any Isabelle object-logic is a ``truth judgment''
     1.5  that links object-level statements to the meta-logic (with its minimal
     1.6  language of $prop$ that covers universal quantification $\Forall$ and
     1.7 -implication $\Imp$).  Common object-logics are sufficiently expressive to
     1.8 -\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own
     1.9 -language.  This is useful in certain situations where a rule needs to be
    1.10 -viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x
    1.11 -\in A \Imp P(x)$ versus $\forall x \in A. P(x)$).
    1.12 +implication $\Imp$).
    1.13 +
    1.14 +Common object-logics are sufficiently expressive to internalize rule
    1.15 +statements over $\Forall$ and $\Imp$ within their own language.  This is
    1.16 +useful in certain situations where a rule needs to be viewed as an atomic
    1.17 +statement from the meta-level perspective, e.g.\ $\All x x \in A \Imp P(x)$
    1.18 +versus $\forall x \in A. P(x)$.
    1.19  
    1.20  From the following language elements, only the $atomize$ method and
    1.21  $rule_format$ attribute are occasionally required by end-users, the rest is
    1.22 @@ -31,34 +33,36 @@
    1.23  realistic examples.
    1.24  
    1.25  Generic tools may refer to the information provided by object-logic
    1.26 -declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical
    1.27 -Reasoner \S\ref{sec:classical}).
    1.28 +declarations internally.
    1.29 +
    1.30 +\railalias{ruleformat}{rule\_format}
    1.31 +\railterm{ruleformat}
    1.32  
    1.33  \begin{rail}
    1.34    'judgment' constdecl
    1.35    ;
    1.36 -  atomize ('(' 'full' ')')?
    1.37 +  'atomize' ('(' 'full' ')')?
    1.38    ;
    1.39    ruleformat ('(' 'noasm' ')')?
    1.40    ;
    1.41  \end{rail}
    1.42  
    1.43  \begin{descr}
    1.44 -
    1.45 -\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the
    1.46 +  
    1.47 +\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the
    1.48    truth judgment of the current object-logic.  Its type $\sigma$ should
    1.49    specify a coercion of the category of object-level propositions to $prop$ of
    1.50 -  the Pure meta-logic; the mixfix annotation $syn$ would typically just link
    1.51 +  the Pure meta-logic; the mixfix annotation $(mx)$ would typically just link
    1.52    the object language (internally of syntactic category $logic$) with that of
    1.53    $prop$.  Only one $\isarkeyword{judgment}$ declaration may be given in any
    1.54    theory development.
    1.55 -
    1.56 +  
    1.57  \item [$atomize$] (as a method) rewrites any non-atomic premises of a
    1.58    sub-goal, using the meta-level equations declared via $atomize$ (as an
    1.59    attribute) beforehand.  As a result, heavily nested goals become amenable to
    1.60    fundamental operations such as resolution (cf.\ the $rule$ method) and
    1.61    proof-by-assumption (cf.\ $assumption$).  Giving the ``$(full)$'' option
    1.62 -  here means to turn the subgoal into an object-statement (if possible),
    1.63 +  here means to turn the whole subgoal into an object-statement (if possible),
    1.64    including the outermost parameters and assumptions as well.
    1.65  
    1.66    A typical collection of $atomize$ rules for a particular object-logic would
    1.67 @@ -106,7 +110,7 @@
    1.68    
    1.69  \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original
    1.70    $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but
    1.71 -  also declares type arity $t :: (term, \dots, term) term$, making $t$ an
    1.72 +  also declares type arity $t :: (type, \dots, type) type$, making $t$ an
    1.73    actual HOL type constructor.
    1.74    
    1.75  \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating
    1.76 @@ -120,21 +124,22 @@
    1.77    $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$
    1.78    declaration).
    1.79    
    1.80 -  Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic
    1.81 -  characterization as a corresponding injection/surjection pair (in both
    1.82 +  Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most
    1.83 +  basic characterization as a corresponding injection/surjection pair (in both
    1.84    directions).  Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly
    1.85 -  more comfortable view on the injectivity part, suitable for automated proof
    1.86 -  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules $Rep_t_cases$,
    1.87 -  $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views
    1.88 -  on surjectivity; these are already declared as type or set rules for the
    1.89 -  generic $cases$ and $induct$ methods.
    1.90 +  more convenient view on the injectivity part, suitable for automated proof
    1.91 +  tools (e.g.\ in $simp$ or $iff$ declarations).  Rules
    1.92 +  $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide
    1.93 +  alternative views on surjectivity; these are already declared as set or type
    1.94 +  rules for the generic $cases$ and $induct$ methods.
    1.95  \end{descr}
    1.96  
    1.97 -Raw type declarations are rarely used in practice; the main application is
    1.98 -with experimental (or even axiomatic!) theory fragments.  Instead of primitive
    1.99 -HOL type definitions, user-level theories usually refer to higher-level
   1.100 -packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or
   1.101 -$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}).
   1.102 +Note that raw type declarations are rarely used in practice; the main
   1.103 +application is with experimental (or even axiomatic!) theory fragments.
   1.104 +Instead of primitive HOL type definitions, user-level theories usually refer
   1.105 +to higher-level packages such as $\isarkeyword{record}$ (see
   1.106 +\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see
   1.107 +\S\ref{sec:hol-datatype}).
   1.108  
   1.109  
   1.110  \subsection{Adhoc tuples}
   1.111 @@ -153,13 +158,12 @@
   1.112  \end{rail}
   1.113  
   1.114  \begin{descr}
   1.115 -
   1.116 +  
   1.117  \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level
   1.118    tuple types into canonical form as specified by the arguments given; $\vec
   1.119 -  p@i$ refers to occurrences in premise $i$ of the rule.  The
   1.120 -  $split_format~(complete)$ form causes \emph{all} arguments in function
   1.121 -  applications to be represented canonically according to their tuple type
   1.122 -  structure.
   1.123 +  p@i$ refers to occurrences in premise $i$ of the rule.  The $(complete)$
   1.124 +  option causes \emph{all} arguments in function applications to be
   1.125 +  represented canonically according to their tuple type structure.
   1.126  
   1.127    Note that these operations tend to invent funny names for new local
   1.128    parameters to be introduced.
   1.129 @@ -169,8 +173,8 @@
   1.130  
   1.131  \subsection{Records}\label{sec:hol-record}
   1.132  
   1.133 -In principle, records merely generalize the concept of tuples where components
   1.134 -may be addressed by labels instead of just position.  The logical
   1.135 +In principle, records merely generalize the concept of tuples, where
   1.136 +components may be addressed by labels instead of just position.  The logical
   1.137  infrastructure of records in Isabelle/HOL is slightly more advanced, though,
   1.138  supporting truly extensible record schemes.  This admits operations that are
   1.139  polymorphic with respect to record extension, yielding ``object-oriented''
   1.140 @@ -203,8 +207,8 @@
   1.141  ``$\more$'' notation (which is actually part of the syntax).  The improper
   1.142  field ``$\more$'' of a record scheme is called the \emph{more part}.
   1.143  Logically it is just a free variable, which is occasionally referred to as
   1.144 -\emph{row variable} in the literature.  The more part of a record scheme may
   1.145 -be instantiated by zero or more further components.  For example, the above
   1.146 +``row variable'' in the literature.  The more part of a record scheme may be
   1.147 +instantiated by zero or more further components.  For example, the previous
   1.148  scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more =
   1.149    m'}$, where $m'$ refers to a different more part.  Fixed records are special
   1.150  instances of record schemes, where ``$\more$'' is properly terminated by the
   1.151 @@ -295,11 +299,11 @@
   1.152  reverse than in the actual term.  Since repeated updates are just function
   1.153  applications, fields may be freely permuted in $\record{x \asn a\fs y \asn
   1.154    b\fs z \asn c}$, as far as logical equality is concerned.  Thus
   1.155 -commutativity of updates can be proven within the logic for any two fields,
   1.156 -but not as a general theorem: fields are not first-class values.
   1.157 +commutativity of independent updates can be proven within the logic for any
   1.158 +two fields, but not as a general theorem.
   1.159  
   1.160  \medskip The \textbf{make} operation provides a cumulative record constructor
   1.161 -functions:
   1.162 +function:
   1.163  \begin{matharray}{lll}
   1.164    t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\
   1.165  \end{matharray}
   1.166 @@ -336,25 +340,26 @@
   1.167      \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\
   1.168  \end{matharray}
   1.169  
   1.170 -\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records.
   1.171 +\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records.
   1.172  
   1.173  
   1.174  \subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms}
   1.175  
   1.176  The record package proves several results internally, declaring these facts to
   1.177  appropriate proof tools.  This enables users to reason about record structures
   1.178 -quite comfortably.  Assume that $t$ is a record type as specified above.
   1.179 +quite conveniently.  Assume that $t$ is a record type as specified above.
   1.180  
   1.181  \begin{enumerate}
   1.182 -
   1.183 +  
   1.184  \item Standard conversions for selectors or updates applied to record
   1.185    constructor terms are made part of the default Simplifier context; thus
   1.186    proofs by reduction of basic operations merely require the $simp$ method
   1.187 -  without further arguments.  These rules are available as $t{\dtt}simps$.
   1.188 -
   1.189 +  without further arguments.  These rules are available as $t{\dtt}simps$,
   1.190 +  too.
   1.191 +  
   1.192  \item Selectors applied to updated records are automatically reduced by an
   1.193 -  internal simplification procedure, which is also part of the default
   1.194 -  Simplifier context.
   1.195 +  internal simplification procedure, which is also part of the standard
   1.196 +  Simplifier setup.
   1.197  
   1.198  \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'
   1.199    \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$
   1.200 @@ -368,10 +373,10 @@
   1.201    terms are provided both in $cases$ and $induct$ format (cf.\ the generic
   1.202    proof methods of the same name, \S\ref{sec:cases-induct}).  Several
   1.203    variations are available, for fixed records, record schemes, more parts etc.
   1.204 -
   1.205 +  
   1.206    The generic proof methods are sufficiently smart to pick the most sensible
   1.207    rule according to the type of the indicated record expression: users just
   1.208 -  need to apply something like ``$(cases r)$'' to a certain proof problem.
   1.209 +  need to apply something like ``$(cases~r)$'' to a certain proof problem.
   1.210  
   1.211  \item The derived record operations $t{\dtt}make$, $t{\dtt}fields$,
   1.212    $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but
   1.213 @@ -471,7 +476,7 @@
   1.214    
   1.215  \item [$\isarkeyword{recdef}$] defines general well-founded recursive
   1.216    functions (using the TFL package), see also \cite{isabelle-HOL}.  The
   1.217 -  $(permissive)$ option tells TFL to recover from failed proof attempts,
   1.218 +  ``$(permissive)$'' option tells TFL to recover from failed proof attempts,
   1.219    returning unfinished results.  The $recdef_simp$, $recdef_cong$, and
   1.220    $recdef_wf$ hints refer to auxiliary rules to be used in the internal
   1.221    automated proof process of TFL.  Additional $clasimpmod$ declarations (cf.\ 
   1.222 @@ -496,8 +501,8 @@
   1.223  $\isarkeyword{recdef}$ are numbered (starting from $1$).
   1.224  
   1.225  The equations provided by these packages may be referred later as theorem list
   1.226 -$f\mathord.simps$, where $f$ is the (collective) name of the functions
   1.227 -defined.  Individual equations may be named explicitly as well; note that for
   1.228 +$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined.
   1.229 +Individual equations may be named explicitly as well; note that for
   1.230  $\isarkeyword{recdef}$ each specification given by the user may result in
   1.231  several theorems.
   1.232  
   1.233 @@ -631,10 +636,10 @@
   1.234    both goal addressing and dynamic instantiation.  Note that named rule cases
   1.235    are \emph{not} provided as would be by the proper $induct$ and $cases$ proof
   1.236    methods (see \S\ref{sec:cases-induct}).
   1.237 -
   1.238 +  
   1.239  \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface
   1.240 -  to the \texttt{mk_cases} operation.  Rules are simplified in an unrestricted
   1.241 -  forward manner.
   1.242 +  to the internal \texttt{mk_cases} operation.  Rules are simplified in an
   1.243 +  unrestricted forward manner.
   1.244  
   1.245    While $ind_cases$ is a proof method to apply the result immediately as
   1.246    elimination rules, $\isarkeyword{inductive_cases}$ provides case split
   1.247 @@ -648,7 +653,7 @@
   1.248  from executable specifications, both functional and relational programs.
   1.249  Isabelle/HOL instantiates these mechanisms in a way that is amenable to
   1.250  end-user applications.  See \cite{isabelle-HOL} for further information (this
   1.251 -actually covers the new-style theory format).
   1.252 +actually covers the new-style theory format as well).
   1.253  
   1.254  \indexisarcmd{generate-code}\indexisarcmd{consts-code}\indexisarcmd{types-code}
   1.255  \indexisaratt{code}
   1.256 @@ -727,10 +732,10 @@
   1.257    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
   1.258  \end{rail}
   1.259  
   1.260 -Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\
   1.261 -\S\ref{sec:hol-datatype}).  Mutual recursive is supported, but no nesting nor
   1.262 +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 
   1.263 +\S\ref{sec:hol-datatype}).  Mutual recursion is supported, but no nesting nor
   1.264  arbitrary branching.  Domain constructors may be strict (default) or lazy, the
   1.265 -latter admits to introduce infinitary objects in the typical LCF manner (e.g.\
   1.266 +latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 
   1.267  lazy lists).  See also \cite{MuellerNvOS99} for a general discussion of HOLCF
   1.268  domains.
   1.269  
   1.270 @@ -742,7 +747,7 @@
   1.271  The ZF logic is essentially untyped, so the concept of ``type checking'' is
   1.272  performed as logical reasoning about set-membership statements.  A special
   1.273  method assists users in this task; a version of this is already declared as a
   1.274 -``solver'' in the default Simplifier context.
   1.275 +``solver'' in the standard Simplifier setup.
   1.276  
   1.277  \indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC}
   1.278  
   1.279 @@ -779,7 +784,7 @@
   1.280  
   1.281  In ZF everything is a set.  The generic inductive package also provides a
   1.282  specific view for ``datatype'' specifications.  Coinductive definitions are
   1.283 -available as well.
   1.284 +available in both cases, too.
   1.285  
   1.286  \indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive}
   1.287  \indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}