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}