diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/logics.tex --- a/doc-src/IsarRef/logics.tex Thu May 08 12:27:19 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1055 +0,0 @@ - -\chapter{Object-logic specific elements}\label{ch:logics} - -\section{HOL} - -\subsection{Primitive types}\label{sec:hol-typedef} - -\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} -\begin{matharray}{rcl} - \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ - \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ -\end{matharray} - -\begin{rail} - 'typedecl' typespec infix? - ; - 'typedef' altname? abstype '=' repset - ; - - altname: '(' (name | 'open' | 'open' name) ')' - ; - abstype: typespec infix? - ; - repset: term ('morphisms' name name)? - ; -\end{rail} - -\begin{descr} - -\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 :: (type, \dots, type) type$, making $t$ an - actual HOL type constructor. - -\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating - non-emptiness of the set $A$. After finishing the proof, the theory will be - augmented by a Gordon/HOL-style type definition, which establishes a - bijection between the representing set $A$ and the new type $t$. - - Technically, $\isarkeyword{typedef}$ defines both a type $t$ and a set (term - constant) of the same name (an alternative base name may be given in - parentheses). The injection from type to set is called $Rep_t$, its inverse - $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$ - declaration). - - 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 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. - - An alternative name may be specified in parentheses; the default is to use - $t$ as indicated before. The $open$ declaration suppresses a separate - constant definition for the representing set. -\end{descr} - -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} - -\indexisarattof{HOL}{split-format} -\begin{matharray}{rcl} - split_format^* & : & \isaratt \\ -\end{matharray} - -\railalias{splitformat}{split\_format} -\railterm{splitformat} - -\begin{rail} - splitformat (((name *) + 'and') | ('(' 'complete' ')')) - ; -\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 ``$(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. - -\end{descr} - - -\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 -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'' -effects like (single) inheritance. See also \cite{NaraschewskiW-TPHOLs98} for -more details on object-oriented verification and record subtyping in HOL. - - -\subsubsection{Basic concepts} - -Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records at the -level of terms and types. The notation is as follows: - -\begin{center} -\begin{tabular}{l|l|l} - & record terms & record types \\ \hline - fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\ - schematic & $\record{x = a\fs y = b\fs \more = m}$ & - $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\ -\end{tabular} -\end{center} - -\noindent The ASCII representation of $\record{x = a}$ is \texttt{(| x = a |)}. - -A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field -$y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$, -assuming that $a \ty A$ and $b \ty B$. - -A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields -$x$ and $y$ as before, but also possibly further fields as indicated by the -``$\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 -``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 -$() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an -abbreviation for $\record{x = a\fs y = b\fs \more = ()}$. - -\medskip - -Two key observations make extensible records in a simply typed language like -HOL feasible: -\begin{enumerate} -\item the more part is internalized, as a free term or type variable, -\item field names are externalized, they cannot be accessed within the logic - as first-class values. -\end{enumerate} - -\medskip - -In Isabelle/HOL record types have to be defined explicitly, fixing their field -names and types, and their (optional) parent record. Afterwards, records may -be formed using above syntax, while obeying the canonical order of fields as -given by their declaration. The record package provides several standard -operations like selectors and updates. The common setup for various generic -proof tools enable succinct reasoning patterns. See also the Isabelle/HOL -tutorial \cite{isabelle-hol-book} for further instructions on using records in -practice. - - -\subsubsection{Record specifications} - -\indexisarcmdof{HOL}{record} -\begin{matharray}{rcl} - \isarcmd{record} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\begin{rail} - 'record' typespec '=' (type '+')? (constdecl +) - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] - defines extensible record type $(\vec\alpha)t$, derived from the optional - parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. - - The type variables of $\tau$ and $\vec\sigma$ need to be covered by the - (distinct) parameters $\vec\alpha$. Type constructor $t$ has to be new, - while $\tau$ needs to specify an instance of an existing record type. At - least one new field $\vec c$ has to be specified. Basically, field names - need to belong to a unique record. This is not a real restriction in - practice, since fields are qualified by the record name internally. - - The parent record specification $\tau$ is optional; if omitted $t$ becomes a - root record. The hierarchy of all records declared within a theory context - forms a forest structure, i.e.\ a set of trees starting with a root record - each. There is no way to merge multiple parent records! - - For convenience, $(\vec\alpha) \, t$ is made a type abbreviation for the - fixed record type $\record{\vec c \ty \vec\sigma}$, likewise is - $(\vec\alpha, \zeta) \, t_scheme$ made an abbreviation for $\record{\vec c - \ty \vec\sigma\fs \more \ty \zeta}$. - -\end{descr} - -\subsubsection{Record operations} - -Any record definition of the form presented above produces certain standard -operations. Selectors and updates are provided for any field, including the -improper one ``$more$''. There are also cumulative record constructor -functions. To simplify the presentation below, we assume for now that -$(\vec\alpha) \, t$ is a root record with fields $\vec c \ty \vec\sigma$. - -\medskip \textbf{Selectors} and \textbf{updates} are available for any field -(including ``$more$''): -\begin{matharray}{lll} - c@i & \ty & \record{\vec c \ty \vec \sigma, \more \ty \zeta} \To \sigma@i \\ - c@i_update & \ty & \sigma@i \To \record{\vec c \ty \vec\sigma, \more \ty \zeta} \To - \record{\vec c \ty \vec\sigma, \more \ty \zeta} -\end{matharray} - -There is special syntax for application of updates: $r \, \record{x \asn a}$ -abbreviates term $x_update \, a \, r$. Further notation for repeated updates -is also available: $r \, \record{x \asn a} \, \record{y \asn b} \, \record{z - \asn c}$ may be written $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. -Note that because of postfix notation the order of fields shown here is -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 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 -function: -\begin{matharray}{lll} - t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ -\end{matharray} - -\medskip We now reconsider the case of non-root records, which are derived of -some parent. In general, the latter may depend on another parent as well, -resulting in a list of \emph{ancestor records}. Appending the lists of fields -of all ancestors results in a certain field prefix. The record package -automatically takes care of this by lifting operations over this context of -ancestor fields. Assuming that $(\vec\alpha) \, t$ has ancestor fields $\vec -b \ty \vec\rho$, the above record operations will get the following types: -\begin{matharray}{lll} - c@i & \ty & \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty - \zeta} \To \sigma@i \\ - c@i_update & \ty & \sigma@i \To - \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To - \record{\vec b \ty \vec\rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ - t{\dtt}make & \ty & \vec\rho \To \vec\sigma \To - \record{\vec b \ty \vec\rho, \vec c \ty \vec \sigma} \\ -\end{matharray} -\noindent - -\medskip Some further operations address the extension aspect of a derived -record scheme specifically: $fields$ produces a record fragment consisting of -exactly the new fields introduced here (the result may serve as a more part -elsewhere); $extend$ takes a fixed record and adds a given more part; -$truncate$ restricts a record scheme to a fixed record. - -\begin{matharray}{lll} - t{\dtt}fields & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ - t{\dtt}extend & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \To - \zeta \To \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \\ - t{\dtt}truncate & \ty & \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma, \more \ty \zeta} \To - \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\ -\end{matharray} - -\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records. - - -\subsubsection{Derived rules and proof tools} - -The record package proves several results internally, declaring these facts to -appropriate proof tools. This enables users to reason about record structures -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$, - too. - -\item Selectors applied to updated records are automatically reduced by an - 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$ - rules. These rules are available as $t{\dtt}iffs$. - -\item The introduction rule for record equality analogous to $x~r = x~r' \Imp - y~r = y~r' \Imp \dots \Imp r = r'$ is declared to the Simplifier, and as the - basic rule context as ``$intro?$''. The rule is called $t{\dtt}equality$. - -\item Representations of arbitrary record expressions as canonical constructor - 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. - -\item The derived record operations $t{\dtt}make$, $t{\dtt}fields$, - $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but - usually need to be expanded by hand, using the collective fact - $t{\dtt}defs$. - -\end{enumerate} - - -\subsection{Datatypes}\label{sec:hol-datatype} - -\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} -\begin{matharray}{rcl} - \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ - \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{repdatatype}{rep\_datatype} -\railterm{repdatatype} - -\begin{rail} - 'datatype' (dtspec + 'and') - ; - repdatatype (name *) dtrules - ; - - dtspec: parname? typespec infix? '=' (cons + '|') - ; - cons: name (type *) mixfix? - ; - dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs -\end{rail} - -\begin{descr} -\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. -\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive - ones, generating the standard infrastructure of derived concepts (primitive - recursion etc.). -\end{descr} - -The induction and exhaustion theorems generated provide case names according -to the constructors involved, while parameters are named after the types (see -also \S\ref{sec:cases-induct}). - -See \cite{isabelle-HOL} for more details on datatypes, but beware of the -old-style theory syntax being used there! Apart from proper proof methods for -case-analysis and induction, there are also emulations of ML tactics -\texttt{case_tac} and \texttt{induct_tac} available, see -\S\ref{sec:hol-induct-tac}; these admit to refer directly to the internal -structure of subgoals (including internally bound parameters). - - -\subsection{Recursive functions}\label{sec:recursion} - -\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{fun}\indexisarcmdof{HOL}{function}\indexisarcmdof{HOL}{termination} - -\begin{matharray}{rcl} - \isarcmd{primrec} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{fun} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{function} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ - \isarcmd{termination} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ -\end{matharray} - -\railalias{funopts}{function\_opts} - -\begin{rail} - 'primrec' target? fixes 'where' equations - ; - equations: (thmdecl? prop + '|') - ; - ('fun' | 'function') (funopts)? fixes 'where' clauses - ; - clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|') - ; - funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' | - 'default' term) + ',') ')' - ; - 'termination' ( term )? -\end{rail} - -\begin{descr} - -\item [$\isarkeyword{primrec}$] defines primitive recursive functions over - datatypes, see also \cite{isabelle-HOL}. - -\item [$\isarkeyword{function}$] defines functions by general - wellfounded recursion. A detailed description with examples can be - found in \cite{isabelle-function}. The function is specified by a - set of (possibly conditional) recursive equations with arbitrary - pattern matching. The command generates proof obligations for the - completeness and the compatibility of patterns. - - The defined function is considered partial, and the resulting - simplification rules (named $f.psimps$) and induction rule (named - $f.pinduct$) are guarded by a generated domain predicate $f_dom$. - The $\isarkeyword{termination}$ command can then be used to establish - that the function is total. - -\item [$\isarkeyword{fun}$] is a shorthand notation for - $\isarkeyword{function}~(\textit{sequential})$, followed by automated - proof attemts regarding pattern matching and termination. For - details, see \cite{isabelle-function}. - -\item [$\isarkeyword{termination}$~f] commences a termination proof - for the previously defined function $f$. If no name is given, it - refers to the most recent function definition. After the proof is - closed, the recursive equations and the induction principle is established. -\end{descr} - -Recursive definitions introduced by both the $\isarkeyword{primrec}$ -and the $\isarkeyword{function}$ command accommodate reasoning by -induction (cf.\ \S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ -(where $c$ is the name of the function definition) refers to a -specific induction rule, with parameters named according to the -user-specified equations. Case names of $\isarkeyword{primrec}$ are -that of the datatypes involved, while those of -$\isarkeyword{function}$ are numbered (starting from $1$). - -The equations provided by these packages may be referred later as theorem list -$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined. -Individual equations may be named explicitly as well. - -The $\isarkeyword{function}$ command accepts the following options: - -\begin{descr} -\item [\emph{sequential}] enables a preprocessor which disambiguates - overlapping patterns by making them mutually disjoint. Earlier - equations take precedence over later ones. This allows to give the - specification in a format very similar to functional programming. - Note that the resulting simplification and induction rules - correspond to the transformed specification, not the one given - originally. This usually means that each equation given by the user - may result in several theroems. - Also note that this automatic transformation only works - for ML-style datatype patterns. - - -\item [\emph{in name}] gives the target for the definition. - -\item [\emph{domintros}] enables the automated generation of - introduction rules for the domain predicate. While mostly not - needed, they can be helpful in some proofs about partial functions. - -\item [\emph{tailrec}] generates the unconstrained recursive equations - even without a termination proof, provided that the function is - tail-recursive. This currently only works - -\item [\emph{default d}] allows to specify a default value for a - (partial) function, which will ensure that $f(x)=d(x)$ whenever $x - \notin \textit{f\_dom}$. This feature is experimental. -\end{descr} - -\subsubsection{Proof methods related to recursive definitions} - -\indexisarmethof{HOL}{pat-completeness} -\indexisarmethof{HOL}{relation} -\indexisarmethof{HOL}{lexicographic-order} - -\begin{matharray}{rcl} - pat\_completeness & : & \isarmeth \\ - relation & : & \isarmeth \\ - lexicographic\_order & : & \isarmeth \\ -\end{matharray} - -\begin{rail} - 'pat\_completeness' - ; - 'relation' term - ; - 'lexicographic\_order' clasimpmod -\end{rail} - -\begin{descr} -\item [\emph{pat\_completeness}] Specialized method to solve goals - regarding the completeness of pattern matching, as required by the - $\isarkeyword{function}$ package (cf.~\cite{isabelle-function}). - -\item [\emph{relation R}] Introduces a termination proof using the - relation $R$. The resulting proof state will contain goals - expressing that $R$ is wellfounded, and that the arguments - of recursive calls decrease with respect to $R$. Usually, this - method is used as the initial proof step of manual termination - proofs. - -\item [\emph{lexicographic\_order}] Attempts a fully automated - termination proof by searching for a lexicographic combination of - size measures on the arguments of the function. The method - accepts the same arguments as the \emph{auto} method, which it uses - internally to prove local descents. Hence, modifiers like - \emph{simp}, \emph{intro} etc.\ can be used to add ``hints'' for the - automated proofs. In case of failure, extensive information is - printed, which can help to analyse the failure (cf.~\cite{isabelle-function}). -\end{descr} - -\subsubsection{Legacy recursion package} -\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} - -The use of the legacy $\isarkeyword{recdef}$ command is now deprecated -in favour of $\isarkeyword{function}$ and $\isarkeyword{fun}$. - -\begin{matharray}{rcl} - \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ - \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ -\end{matharray} - -\railalias{recdefsimp}{recdef\_simp} -\railterm{recdefsimp} - -\railalias{recdefcong}{recdef\_cong} -\railterm{recdefcong} - -\railalias{recdefwf}{recdef\_wf} -\railterm{recdefwf} - -\railalias{recdeftc}{recdef\_tc} -\railterm{recdeftc} - -\begin{rail} - 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? - ; - recdeftc thmdecl? tc - ; - hints: '(' 'hints' (recdefmod *) ')' - ; - recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod - ; - tc: nameref ('(' nat ')')? - ; -\end{rail} - -\begin{descr} - -\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, - 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.\ - \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier - (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ - \S\ref{sec:classical}). - -\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover - termination condition number $i$ (default $1$) as generated by a - $\isarkeyword{recdef}$ definition of constant $c$. - - Note that in most cases, $\isarkeyword{recdef}$ is able to finish its - internal proofs without manual intervention. - -\end{descr} - -\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using -the following attributes. - -\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} -\begin{matharray}{rcl} - recdef_simp & : & \isaratt \\ - recdef_cong & : & \isaratt \\ - recdef_wf & : & \isaratt \\ -\end{matharray} - -\railalias{recdefsimp}{recdef\_simp} -\railterm{recdefsimp} - -\railalias{recdefcong}{recdef\_cong} -\railterm{recdefcong} - -\railalias{recdefwf}{recdef\_wf} -\railterm{recdefwf} - -\begin{rail} - (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') - ; -\end{rail} - -\subsection{Definition by specification}\label{sec:hol-specification} - -\indexisarcmdof{HOL}{specification} -\begin{matharray}{rcl} - \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\ - \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\ -\end{matharray} - -\begin{rail} -('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) -; -decl: ((name ':')? term '(' 'overloaded' ')'?) -\end{rail} - -\begin{descr} -\item [$\isarkeyword{specification}~decls~\phi$] sets up a goal stating - the existence of terms with the properties specified to hold for the - constants given in $\mathit{decls}$. After finishing the proof, the - theory will be augmented with definitions for the given constants, - as well as with theorems stating the properties for these constants. -\item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating - the existence of terms with the properties specified to hold for the - constants given in $\mathit{decls}$. After finishing the proof, the - theory will be augmented with axioms expressing the properties given - in the first place. -\item[$decl$] declares a constant to be defined by the specification - given. The definition for the constant $c$ is bound to the name - $c$\_def unless a theorem name is given in the declaration. - Overloaded constants should be declared as such. -\end{descr} - -Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$ -is to some extent a matter of style. $\isarkeyword{specification}$ introduces no new axioms, -and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$ -does introduce axioms, but only after the user has explicitly proven it to be -safe. A practical issue must be considered, though: After introducing two constants -with the same properties using $\isarkeyword{specification}$, one can prove -that the two constants are, in fact, equal. If this might be a problem, -one should use $\isarkeyword{ax_specification}$. - -\subsection{Inductive and coinductive definitions}\label{sec:hol-inductive} - -An {\bf inductive definition} specifies the least predicate (or set) $R$ closed under given -rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For -example, a structural operational semantics is an inductive definition of an -evaluation relation. Dually, a {\bf coinductive definition} specifies the -greatest predicate (or set) $R$ consistent with given rules. (Every element of~$R$ can be -seen as arising by applying a rule to elements of~$R$.) An important example -is using bisimulation relations to formalise equivalence of processes and -infinite data structures. - -This package is related to the ZF one, described in a separate -paper,% -\footnote{It appeared in CADE~\cite{paulson-CADE}; a longer version is - distributed with Isabelle.} % -which you should refer to in case of difficulties. The package is simpler -than ZF's thanks to HOL's extra-logical automatic type-checking. The types of -the (co)inductive predicates (or sets) determine the domain of the fixedpoint definition, and -the package does not have to use inference rules for type-checking. - -\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{inductive-set}\indexisarcmdof{HOL}{coinductive}\indexisarcmdof{HOL}{coinductive-set}\indexisarattof{HOL}{mono} -\begin{matharray}{rcl} - \isarcmd{inductive} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{inductive_set} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{coinductive} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{coinductive_set} & : & \isarkeep{local{\dsh}theory} \\ - mono & : & \isaratt \\ -\end{matharray} - -\begin{rail} - ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ - ('where' clauses)? ('monos' thmrefs)? - ; - clauses: (thmdecl? prop + '|') - ; - 'mono' (() | 'add' | 'del') - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define - (co)inductive predicates from the introduction rules given in the \texttt{where} section. - The optional \texttt{for} section contains a list of parameters of the (co)inductive - predicates that remain fixed throughout the definition. - The optional \texttt{monos} section contains \textit{monotonicity theorems}, - which are required for each operator applied to a recursive set in the introduction rules. - There {\bf must} be a theorem of the form $A \leq B \Imp M~A \leq M~B$, for each - premise $M~R@i~t$ in an introduction rule! -\item [$\isarkeyword{inductive_set}$ and $\isarkeyword{coinductive_set}$] are wrappers - for to the previous commands, allowing the definition of (co)inductive sets. -\item [$mono$] declares monotonicity rules. These rule are involved in the - automated monotonicity proof of $\isarkeyword{inductive}$. -\end{descr} - -\subsubsection{Derived rules} - -Each (co)inductive definition $R$ adds definitions to the theory and also -proves some theorems: -\begin{description} -\item[$R{\dtt}intros$] is the list of introduction rules, now proved as theorems, for -the recursive predicates (or sets). The rules are also available individually, -using the names given them in the theory file. -\item[$R{\dtt}cases$] is the case analysis (or elimination) rule. -\item[$R{\dtt}(co)induct$] is the (co)induction rule. -\end{description} -When several predicates $R@1$, $\ldots$, $R@n$ are defined simultaneously, -the list of introduction rules is called $R@1_\ldots_R@n{\dtt}intros$, the -case analysis rules are called $R@1{\dtt}cases$, $\ldots$, $R@n{\dtt}cases$, and -the list of mutual induction rules is called $R@1_\ldots_R@n{\dtt}inducts$. - -\subsubsection{Monotonicity theorems} - -Each theory contains a default set of theorems that are used in monotonicity -proofs. New rules can be added to this set via the $mono$ attribute. -Theory \texttt{Inductive} shows how this is done. In general, the following -monotonicity theorems may be added: -\begin{itemize} -\item Theorems of the form $A \leq B \Imp M~A \leq M~B$, for proving - monotonicity of inductive definitions whose introduction rules have premises - involving terms such as $M~R@i~t$. -\item Monotonicity theorems for logical operators, which are of the general form - $\List{\cdots \to \cdots;~\ldots;~\cdots \to \cdots} \Imp - \cdots \to \cdots$. - For example, in the case of the operator $\lor$, the corresponding theorem is - \[ - \infer{P@1 \lor P@2 \to Q@1 \lor Q@2} - {P@1 \to Q@1 & P@2 \to Q@2} - \] -\item De Morgan style equations for reasoning about the ``polarity'' of expressions, e.g. - \[ - (\lnot \lnot P) ~=~ P \qquad\qquad - (\lnot (P \land Q)) ~=~ (\lnot P \lor \lnot Q) - \] -\item Equations for reducing complex operators to more primitive ones whose - monotonicity can easily be proved, e.g. - \[ - (P \to Q) ~=~ (\lnot P \lor Q) \qquad\qquad - \mathtt{Ball}~A~P ~\equiv~ \forall x.~x \in A \to P~x - \] -\end{itemize} - -%FIXME: Example of an inductive definition - - -\subsection{Arithmetic proof support} - -\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split} -\begin{matharray}{rcl} - arith & : & \isarmeth \\ - arith_split & : & \isaratt \\ -\end{matharray} - -\begin{rail} - 'arith' '!'? - ; -\end{rail} - -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, -$real$). Any current facts are inserted into the goal before running the -procedure. The ``!''~argument causes the full context of assumptions to be -included. The $arith_split$ attribute declares case split rules to be -expanded before the arithmetic procedure is invoked. - -Note that a simpler (but faster) version of arithmetic reasoning is already -performed by the Simplifier. - - -\subsection{Cases and induction: emulating tactic scripts}\label{sec:hol-induct-tac} - -The following important tactical tools of Isabelle/HOL have been ported to -Isar. These should be never used in proper proof texts! - -\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} -\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} -\begin{matharray}{rcl} - case_tac^* & : & \isarmeth \\ - induct_tac^* & : & \isarmeth \\ - ind_cases^* & : & \isarmeth \\ - \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{casetac}{case\_tac} -\railterm{casetac} - -\railalias{inducttac}{induct\_tac} -\railterm{inducttac} - -\railalias{indcases}{ind\_cases} -\railterm{indcases} - -\railalias{inductivecases}{inductive\_cases} -\railterm{inductivecases} - -\begin{rail} - casetac goalspec? term rule? - ; - inducttac goalspec? (insts * 'and') rule? - ; - indcases (prop +) ('for' (name +)) ? - ; - inductivecases (thmdecl? (prop +) + 'and') - ; - - rule: ('rule' ':' thmref) - ; -\end{rail} - -\begin{descr} -\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes - only (unless an alternative rule is given explicitly). Furthermore, - $case_tac$ does a classical case split on booleans; $induct_tac$ allows only - variables to be given as instantiation. These tactic emulations feature - 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 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 - theorems at the theory level for later use. - The \texttt{for} option of the $ind_cases$ method allows to specify a list - of variables that should be generalized before applying the resulting rule. -\end{descr} - - -\subsection{Executable code} - -Isabelle/Pure provides two generic frameworks to support code -generation from executable specifications. Isabelle/HOL -instantiates these mechanisms in a -way that is amenable to end-user applications. - -One framework generates code from both functional and -relational programs to SML. See -\cite{isabelle-HOL} for further information (this actually covers the -new-style theory format as well). - -\indexisarcmd{value}\indexisarcmd{code-module}\indexisarcmd{code-library} -\indexisarcmd{consts-code}\indexisarcmd{types-code} -\indexisaratt{code} - -\begin{matharray}{rcl} - \isarcmd{value}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{code_module} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_library} & : & \isartrans{theory}{theory} \\ - \isarcmd{consts_code} & : & \isartrans{theory}{theory} \\ - \isarcmd{types_code} & : & \isartrans{theory}{theory} \\ - code & : & \isaratt \\ -\end{matharray} - -\railalias{verblbrace}{\texttt{\ttlbrace*}} -\railalias{verbrbrace}{\texttt{*\ttrbrace}} -\railterm{verblbrace} -\railterm{verbrbrace} - -\begin{rail} -'value' term; - -( 'code\_module' | 'code\_library' ) modespec ? name ? \\ - ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ - 'contains' ( ( name '=' term ) + | term + ); - -modespec : '(' ( name * ) ')'; - -'consts\_code' (codespec +); - -codespec : const template attachment ?; - -'types\_code' (tycodespec +); - -tycodespec : name template attachment ?; - -const: term; - -template: '(' string ')'; - -attachment: 'attach' modespec ? verblbrace text verbrbrace; - -'code' (name)?; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{value}~t$] reads, evaluates and prints a term - using the code generator. -\end{descr} - -The other framework generates code from functional programs -(including overloading using type classes) to SML \cite{SML}, -OCaml \cite{OCaml} and Haskell \cite{haskell-revised-report}. -Conceptually, code generation is split up in three steps: \emph{selection} -of code theorems, \emph{translation} into an abstract executable view -and \emph{serialization} to a specific \emph{target language}. -See \cite{isabelle-codegen} for an introduction on how to use it. - -\indexisarcmd{export-code} -\indexisarcmd{code-thms} -\indexisarcmd{code-deps} -\indexisarcmd{code-datatype} -\indexisarcmd{code-const} -\indexisarcmd{code-type} -\indexisarcmd{code-class} -\indexisarcmd{code-instance} -\indexisarcmd{code-monad} -\indexisarcmd{code-reserved} -\indexisarcmd{code-include} -\indexisarcmd{code-modulename} -\indexisarcmd{code-exception} -\indexisarcmd{print-codesetup} -\indexisaratt{code func} -\indexisaratt{code inline} - -\begin{matharray}{rcl} - \isarcmd{export_code}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{code_thms}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{code_deps}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{code_datatype} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_const} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_type} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_class} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_instance} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_monad} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_reserved} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_include} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_modulename} & : & \isartrans{theory}{theory} \\ - \isarcmd{code_exception} & : & \isartrans{theory}{theory} \\ - \isarcmd{print_codesetup}^* & : & \isarkeep{theory~|~proof} \\ - code\ func & : & \isaratt \\ - code\ inline & : & \isaratt \\ -\end{matharray} - -\begin{rail} -'export\_code' ( constexpr + ) ? \\ - ( ( 'in' target ( 'module\_name' string ) ? \\ - ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?; - -'code\_thms' ( constexpr + ) ?; - -'code\_deps' ( constexpr + ) ?; - -const : term; - -constexpr : ( const | 'name.*' | '*' ); - -typeconstructor : nameref; - -class : nameref; - -target : 'OCaml' | 'SML' | 'Haskell'; - -'code\_datatype' const +; - -'code\_const' (const + 'and') \\ - ( ( '(' target ( syntax ? + 'and' ) ')' ) + ); - -'code\_type' (typeconstructor + 'and') \\ - ( ( '(' target ( syntax ? + 'and' ) ')' ) + ); - -'code\_class' (class + 'and') \\ - ( ( '(' target \\ - ( ( string ('where' \\ - ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + ); - -'code\_instance' (( typeconstructor '::' class ) + 'and') \\ - ( ( '(' target ( '-' ? + 'and' ) ')' ) + ); - -'code\_monad' const const target; - -'code\_reserved' target ( string + ); - -'code\_include' target ( string ( string | '-') ); - -'code\_modulename' target ( ( string string ) + ); - -'code\_exception' ( const + ); - -syntax : string | ( 'infix' | 'infixl' | 'infixr' ) nat string; - -'print\_codesetup'; - -'code\ func' ( 'del' ) ?; - -'code\ inline' ( 'del' ) ?; -\end{rail} - -\begin{descr} - -\item [$\isarcmd{export_code}$] is the canonical interface for generating and - serializing code: for a given list of constants, code is generated for the specified - target language(s). Abstract code is cached incrementally. If no constant is given, - the currently cached code is serialized. If no serialization instruction - is given, only abstract code is cached. - - Constants may be specified by giving them literally, referring - to all exeuctable contants within a certain theory named ``name'' - by giving (``name.*''), or referring to \emph{all} executable - constants currently available (``*''). - - By default, for each involved theory one corresponding name space module - is generated. Alternativly, a module name may be specified after the - (``module_name'') keyword; then \emph{all} code is placed in this module. - - For \emph{SML} and \emph{OCaml}, the file specification refers to - a single file; for \emph{Haskell}, it refers to a whole directory, - where code is generated in multiple files reflecting the module hierarchy. - The file specification ``-'' denotes standard output. For \emph{SML}, - omitting the file specification compiles code internally - in the context of the current ML session. - - Serializers take an optional list of arguments in parentheses. - For \emph{Haskell} a module name prefix may be given using the ``root:'' - argument; ``string\_classes'' adds a ``deriving (Read, Show)'' clause - to each appropriate datatype declaration. - -\item [$\isarcmd{code_thms}$] prints a list of theorems representing the - corresponding program containing all given constants; if no constants are - given, the currently cached code theorems are printed. - -\item [$\isarcmd{code_deps}$] visualizes dependencies of theorems representing the - corresponding program containing all given constants; if no constants are - given, the currently cached code theorems are visualized. - -\item [$\isarcmd{code_datatype}$] specifies a constructor set for a logical type. - -\item [$\isarcmd{code_const}$] associates a list of constants - with target-specific serializations; omitting a serialization - deletes an existing serialization. - -\item [$\isarcmd{code_type}$] associates a list of type constructors - with target-specific serializations; omitting a serialization - deletes an existing serialization. - -\item [$\isarcmd{code_class}$] associates a list of classes - with target-specific class names; in addition, constants associated - with this class may be given target-specific names used for instance - declarations; omitting a serialization - deletes an existing serialization. Applies only to \emph{Haskell}. - -\item [$\isarcmd{code_instance}$] declares a list of type constructor / class - instance relations as ``already present'' for a given target. - Omitting a ``-'' deletes an existing ``already present'' declaration. - Applies only to \emph{Haskell}. - -\item [$\isarcmd{code_monad}$] provides an auxiliary mechanism - to generate monadic code. - -\item [$\isarcmd{code_reserved}$] declares a list of names - as reserved for a given target, preventing it to be shadowed - by any generated code. - -\item [$\isarcmd{code_include}$] adds arbitrary named content (''include``) - to generated code. A as last argument ``-'' will remove an already added ''include``. - -\item [$\isarcmd{code_modulename}$] declares aliasings from one module name - onto another. - -\item [$\isarcmd{code_exception}$] declares constants which are not required - to have a definition by a defining equations; these are mapped on exceptions - instead. - -\item [$code\ func$] selects (or with option ''del``, deselects) explicitly - a defining equation for code generation. Usually packages introducing - defining equations provide a resonable default setup for selection. - -\item [$code\ inline$] declares (or with option ''del``, removes) - inlining theorems which are applied as rewrite rules to any defining equation - during preprocessing. - -\item [$\isarcmd{print_codesetup}$] gives an overview on selected - defining equations, code generator datatypes and preprocessor setup. - -\end{descr} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "isar-ref" -%%% End: