# HG changeset patch # User wenzelm # Date 1210242558 -7200 # Node ID df50bc1249d72e3b0f20f8a17e035127b4fda5a5 # Parent d3d750ada6045dbc33fae59944d1bac006a890d5 converted HOL specific elements; diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/IsaMakefile --- a/doc-src/IsarRef/IsaMakefile Thu May 08 12:27:19 2008 +0200 +++ b/doc-src/IsarRef/IsaMakefile Thu May 08 12:29:18 2008 +0200 @@ -22,8 +22,8 @@ HOL-IsarRef: $(LOG)/HOL-IsarRef.gz $(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \ - Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/Quick_Reference.thy \ - Thy/ML_Tactic.thy + Thy/syntax.thy Thy/pure.thy Thy/Generic.thy Thy/HOL_Specific.thy \ + Thy/Quick_Reference.thy Thy/ML_Tactic.thy @$(USEDIR) -s IsarRef HOL Thy diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Thu May 08 12:27:19 2008 +0200 +++ b/doc-src/IsarRef/Makefile Thu May 08 12:29:18 2008 +0200 @@ -18,7 +18,7 @@ Thy/document/ML_Tactic.tex Thy/document/Quick_Reference.tex \ Thy/document/ZF_Specific.tex Thy/document/intro.tex \ Thy/document/pure.tex Thy/document/syntax.tex \ - logics.tex ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \ + ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \ ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib dvi: $(NAME).dvi diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 08 12:27:19 2008 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Thu May 08 12:29:18 2008 +0200 @@ -1,7 +1,1146 @@ (* $Id$ *) theory HOL_Specific -imports HOL +imports Main begin +chapter {* HOL specific elements \label{ch:logics} *} + +section {* Primitive types \label{sec:hol-typedef} *} + +text {* + \begin{matharray}{rcl} + @{command_def (HOL) "typedecl"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "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 [@{command (HOL) "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) + t"}] is similar to the original @{command "typedecl"} of + Isabelle/Pure (see \secref{sec:types-pure}), but also declares type + arity @{text "t :: (type, \, type) type"}, making @{text t} an + actual HOL type constructor. %FIXME check, update + + \item [@{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) + t = A"}] sets up a goal stating non-emptiness of the set @{text 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 @{text A} and the new type @{text t}. + + Technically, @{command (HOL) "typedef"} defines both a type @{text + 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 @{text Rep_t}, its inverse @{text Abs_t} (this may be + changed via an explicit @{keyword (HOL) "morphisms"} declaration). + + Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text + Abs_t_inverse} provide the most basic characterization as a + corresponding injection/surjection pair (in both directions). Rules + @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly + more convenient view on the injectivity part, suitable for automated + proof tools (e.g.\ in @{method simp} or @{method iff} declarations). + Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and @{text + Abs_t_cases}/@{text Abs_t_induct} provide alternative views on + surjectivity; these are already declared as set or type rules for + the generic @{method cases} and @{method induct} methods. + + An alternative name may be specified in parentheses; the default is + to use @{text t} as indicated before. The ``@{text "(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 @{command + (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL) + "datatype"} (see \secref{sec:hol-datatype}). +*} + + +section {* Adhoc tuples *} + +text {* + \begin{matharray}{rcl} + @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + 'split\_format' (((name *) + 'and') | ('(' 'complete' ')')) + ; + \end{rail} + + \begin{descr} + + \item [@{method (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m + \ \ \ q\<^sub>1 \ q\<^sub>n"}] puts expressions of + low-level tuple types into canonical form as specified by the + arguments given; the @{text i}-th collection of arguments refers to + occurrences in premise @{text i} of the rule. The ``@{text + "(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} +*} + + +section {* Records \label{sec:hol-record} *} + +text {* + 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. +*} + + +subsection {* Basic concepts *} + +text {* + 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 & @{text "\x = a, y = b\"} & @{text "\x :: A, y :: B\"} \\ + schematic & @{text "\x = a, y = b, \ = m\"} & + @{text "\x :: A, y :: B, \ :: M\"} \\ + \end{tabular} + \end{center} + + \noindent The ASCII representation of @{text "\x = a\"} is @{text + "(| x = a |)"}. + + A fixed record @{text "\x = a, y = b\"} has field @{text x} of value + @{text a} and field @{text y} of value @{text b}. The corresponding + type is @{text "\x :: A, y :: B\"}, assuming that @{text "a :: A"} + and @{text "b :: B"}. + + A record scheme like @{text "\x = a, y = b, \ = m\"} contains fields + @{text x} and @{text y} as before, but also possibly further fields + as indicated by the ``@{text "\"}'' notation (which is actually part + of the syntax). The improper field ``@{text "\"}'' 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 @{text "\x = a, y = b, z = + c, \ = m'"}, where @{text m'} refers to a different more part. + Fixed records are special instances of record schemes, where + ``@{text "\"}'' is properly terminated by the @{text "() :: unit"} + element. In fact, @{text "\x = a, y = b\"} is just an abbreviation + for @{text "\x = a, y = b, \ = ()\"}. + + \medskip Two key observations make extensible records in a simply + typed language like HOL work out: + + \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. +*} + + +subsection {* Record specifications *} + +text {* + \begin{matharray}{rcl} + @{command_def (HOL) "record"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'record' typespec '=' (type '+')? (constdecl +) + ; + \end{rail} + + \begin{descr} + + \item [@{command (HOL) "record"}~@{text "(\\<^sub>1, \, \\<^sub>m) t + = \ + c\<^sub>1 :: \\<^sub>1 \ c\<^sub>n :: \\<^sub>n"}] defines + extensible record type @{text "(\\<^sub>1, \, \\<^sub>m) t"}, + derived from the optional parent record @{text "\"} by adding new + field components @{text "c\<^sub>i :: \\<^sub>i"} etc. + + The type variables of @{text "\"} and @{text "\\<^sub>i"} need to be + covered by the (distinct) parameters @{text "\\<^sub>1, \, + \\<^sub>m"}. Type constructor @{text t} has to be new, while @{text + \} needs to specify an instance of an existing record type. At + least one new field @{text "c\<^sub>i"} 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 @{text \} is optional; if omitted + @{text 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, @{text "(\\<^sub>1, \, \\<^sub>m) t"} is made a + type abbreviation for the fixed record type @{text "\c\<^sub>1 :: + \\<^sub>1, \, c\<^sub>n :: \\<^sub>n\"}, likewise is @{text + "(\\<^sub>1, \, \\<^sub>m, \) t_scheme"} made an abbreviation for + @{text "\c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: + \\"}. + + \end{descr} +*} + + +subsection {* Record operations *} + +text {* + Any record definition of the form presented above produces certain + standard operations. Selectors and updates are provided for any + field, including the improper one ``@{text more}''. There are also + cumulative record constructor functions. To simplify the + presentation below, we assume for now that @{text "(\\<^sub>1, \, + \\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 :: + \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. + + \medskip \textbf{Selectors} and \textbf{updates} are available for + any field (including ``@{text more}''): + + \begin{matharray}{lll} + @{text "c\<^sub>i"} & @{text "::"} & @{text "\c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\ \ \\<^sub>i"} \\ + @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ \c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\ \ \c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\"} \\ + \end{matharray} + + There is special syntax for application of updates: @{text "r\x := + a\"} abbreviates term @{text "x_update a r"}. Further notation for + repeated updates is also available: @{text "r\x := a\\y := b\\z := + c\"} may be written @{text "r\x := a, y := b, z := 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 @{text "\x + := a, y := b, z := 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} + @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n\"} \\ + \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 @{text "(\\<^sub>1, \, \\<^sub>m) t"} has ancestor + fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, + the above record operations will get the following types: + + \begin{matharray}{lll} + @{text "c\<^sub>i"} & @{text "::"} & @{text "\b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\ \ \\<^sub>i"} \\ + @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ + \b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\ \ + \b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\"} \\ + @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>k \ \\<^sub>1 \ \ \\<^sub>n \ + \b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"} \\ + \end{matharray} + \noindent + + \medskip Some further operations address the extension aspect of a + derived record scheme specifically: @{text "t.fields"} produces a + record fragment consisting of exactly the new fields introduced here + (the result may serve as a more part elsewhere); @{text "t.extend"} + takes a fixed record and adds a given more part; @{text + "t.truncate"} restricts a record scheme to a fixed record. + + \begin{matharray}{lll} + @{text "t.fields"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"} \\ + @{text "t.extend"} & @{text "::"} & @{text "\b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n\ \ + \ \ \b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\"} \\ + @{text "t.truncate"} & @{text "::"} & @{text "\b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: \\ \ \b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k, c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n\"} \\ + \end{matharray} + + \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide + for root records. +*} + + +subsection {* Derived rules and proof tools *} + +text {* + 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 + @{text 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 @{method simp} method without further arguments. These rules + are available as @{text "t.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 @{prop "(x, y) = (x', + y') \ x = x' \ y = y'"} are declared to the Simplifier and Classical + Reasoner as @{attribute iff} rules. These rules are available as + @{text "t.iffs"}. + + \item The introduction rule for record equality analogous to @{text + "x r = x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, + and as the basic rule context as ``@{attribute intro}@{text "?"}''. + The rule is called @{text "t.equality"}. + + \item Representations of arbitrary record expressions as canonical + constructor terms are provided both in @{method cases} and @{method + induct} format (cf.\ the generic proof methods of the same name, + \secref{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 ``@{text "(cases + r)"}'' to a certain proof problem. + + \item The derived record operations @{text "t.make"}, @{text + "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not} + treated automatically, but usually need to be expanded by hand, + using the collective fact @{text "t.defs"}. + + \end{enumerate} +*} + + +section {* Datatypes \label{sec:hol-datatype} *} + +text {* + \begin{matharray}{rcl} + @{command_def (HOL) "datatype"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "rep_datatype"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'datatype' (dtspec + 'and') + ; + 'rep\_datatype' (name *) dtrules + ; + + dtspec: parname? typespec infix? '=' (cons + '|') + ; + cons: name (type *) mixfix? + ; + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs + \end{rail} + + \begin{descr} + + \item [@{command (HOL) "datatype"}] defines inductive datatypes in + HOL. + + \item [@{command (HOL) "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 \secref{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 @{method (HOL) case_tac} and @{method (HOL) + induct_tac} available, see \secref{sec:hol-induct-tac}; these admit + to refer directly to the internal structure of subgoals (including + internally bound parameters). +*} + + +section {* Recursive functions \label{sec:recursion} *} + +text {* + \begin{matharray}{rcl} + @{command_def (HOL) "primrec"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def (HOL) "fun"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def (HOL) "function"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + @{command_def (HOL) "termination"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \end{matharray} + + \railalias{funopts}{function\_opts} %FIXME ?? + + \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 [@{command (HOL) "primrec"}] defines primitive recursive + functions over datatypes, see also \cite{isabelle-HOL}. + + \item [@{command (HOL) "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 @{text "f.psimps"}) and induction rule + (named @{text "f.pinduct"}) are guarded by a generated domain + predicate @{text "f_dom"}. The @{command (HOL) "termination"} + command can then be used to establish that the function is total. + + \item [@{command (HOL) "fun"}] is a shorthand notation for + ``@{command (HOL) "function"}~@{text "(sequential)"}, followed by + automated proof attempts regarding pattern matching and termination. + See \cite{isabelle-function} for further details. + + \item [@{command (HOL) "termination"}~@{text f}] commences a + termination proof for the previously defined function @{text f}. If + this is omitted, the command refers to the most recent function + definition. After the proof is closed, the recursive equations and + the induction principle is established. + + \end{descr} + + %FIXME check + + Recursive definitions introduced by both the @{command (HOL) + "primrec"} and the @{command (HOL) "function"} command accommodate + reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text + "c.induct"} (where @{text 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 @{command (HOL) + "primrec"} are that of the datatypes involved, while those of + @{command (HOL) "function"} are numbered (starting from 1). + + The equations provided by these packages may be referred later as + theorem list @{text "f.simps"}, where @{text f} is the (collective) + name of the functions defined. Individual equations may be named + explicitly as well. + + The @{command (HOL) "function"} command accepts the following + options. + + \begin{descr} + + \item [@{text 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 [@{text "\ name"}] gives the target for the definition. + %FIXME ?!? + + \item [@{text 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 [@{text tailrec}] generates the unconstrained recursive + equations even without a termination proof, provided that the + function is tail-recursive. This currently only works + + \item [@{text "default d"}] allows to specify a default value for a + (partial) function, which will ensure that @{text "f x = d x"} + whenever @{text "x \ f_dom"}. + + \end{descr} +*} + + +subsection {* Proof methods related to recursive definitions *} + +text {* + \begin{matharray}{rcl} + @{method_def (HOL) pat_completeness} & : & \isarmeth \\ + @{method_def (HOL) relation} & : & \isarmeth \\ + @{method_def (HOL) lexicographic_order} & : & \isarmeth \\ + \end{matharray} + + \begin{rail} + 'relation' term + ; + 'lexicographic\_order' (clasimpmod *) + ; + \end{rail} + + \begin{descr} + + \item [@{method (HOL) pat_completeness}] is a specialized method to + solve goals regarding the completeness of pattern matching, as + required by the @{command (HOL) "function"} package (cf.\ + \cite{isabelle-function}). + + \item [@{method (HOL) relation}~@{text R}] introduces a termination + proof using the relation @{text R}. The resulting proof state will + contain goals expressing that @{text R} is wellfounded, and that the + arguments of recursive calls decrease with respect to @{text R}. + Usually, this method is used as the initial proof step of manual + termination proofs. + + \item [@{method (HOL) "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 @{method auto} method, + which it uses internally to prove local descents. The same context + modifiers as for @{method auto} are accepted, see + \secref{sec:clasimp}. + + In case of failure, extensive information is printed, which can help + to analyse the situation (cf.\ \cite{isabelle-function}). + + \end{descr} +*} + + +subsection {* Old-style recursive function definitions (TFL) *} + +text {* + The old TFL commands @{command (HOL) "recdef"} and @{command (HOL) + "recdef_tc"} for defining recursive are mostly obsolete; @{command + (HOL) "function"} or @{command (HOL) "fun"} should be used instead. + + \begin{matharray}{rcl} + @{command_def (HOL) "recdef"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & \isartrans{theory}{proof(prove)} \\ + \end{matharray} + + \begin{rail} + 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? + ; + recdeftc thmdecl? tc + ; + hints: '(' 'hints' (recdefmod *) ')' + ; + recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod + ; + tc: nameref ('(' nat ')')? + ; + \end{rail} + + \begin{descr} + + \item [@{command (HOL) "recdef"}] defines general well-founded + recursive functions (using the TFL package), see also + \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells + TFL to recover from failed proof attempts, returning unfinished + results. The @{text recdef_simp}, @{text recdef_cong}, and @{text + recdef_wf} hints refer to auxiliary rules to be used in the internal + automated proof process of TFL. Additional @{syntax clasimpmod} + declarations (cf.\ \secref{sec:clasimp}) may be given to tune the + context of the Simplifier (cf.\ \secref{sec:simplifier}) and + Classical reasoner (cf.\ \secref{sec:classical}). + + \item [@{command (HOL) "recdef_tc"}~@{text "c (i)"}] recommences the + proof for leftover termination condition number @{text i} (default + 1) as generated by a @{command (HOL) "recdef"} definition of + constant @{text c}. + + Note that in most cases, @{command (HOL) "recdef"} is able to finish + its internal proofs without manual intervention. + + \end{descr} + + \medskip Hints for @{command (HOL) "recdef"} may be also declared + globally, using the following attributes. + + \begin{matharray}{rcl} + @{attribute_def (HOL) recdef_simp} & : & \isaratt \\ + @{attribute_def (HOL) recdef_cong} & : & \isaratt \\ + @{attribute_def (HOL) recdef_wf} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') + ; + \end{rail} +*} + + +section {* Definition by specification \label{sec:hol-specification} *} + +text {* + \begin{matharray}{rcl} + @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\ + @{command_def (HOL) "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 [@{command (HOL) "specification"}~@{text "decls \"}] sets up a + goal stating the existence of terms with the properties specified to + hold for the constants given in @{text 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 [@{command (HOL) "ax_specification"}~@{text "decls \"}] sets + up a goal stating the existence of terms with the properties + specified to hold for the constants given in @{text decls}. After + finishing the proof, the theory will be augmented with axioms + expressing the properties given in the first place. + + \item [@{text decl}] declares a constant to be defined by the + specification given. The definition for the constant @{text c} is + bound to the name @{text c_def} unless a theorem name is given in + the declaration. Overloaded constants should be declared as such. + + \end{descr} + + Whether to use @{command (HOL) "specification"} or @{command (HOL) + "ax_specification"} is to some extent a matter of style. @{command + (HOL) "specification"} introduces no new axioms, and so by + construction cannot introduce inconsistencies, whereas @{command + (HOL) "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 @{command (HOL) "specification"}, one can prove + that the two constants are, in fact, equal. If this might be a + problem, one should use @{command (HOL) "ax_specification"}. +*} + + +section {* Inductive and coinductive definitions \label{sec:hol-inductive} *} + +text {* + An \textbf{inductive definition} specifies the least predicate (or + set) @{text R} closed under given rules: applying a rule to elements + of @{text R} yields a result within @{text R}. For example, a + structural operational semantics is an inductive definition of an + evaluation relation. + + Dually, a \textbf{coinductive definition} specifies the greatest + predicate~/ set @{text R} that is consistent with given rules: every + element of @{text R} can be seen as arising by applying a rule to + elements of @{text R}. An important example is using bisimulation + relations to formalise equivalence of processes and infinite data + structures. + + \medskip The HOL package is related to the ZF one, which is + 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 that of ZF thanks to implicit type-checking in HOL. + 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. + + \begin{matharray}{rcl} + @{command_def (HOL) "inductive"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def (HOL) "inductive_set"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def (HOL) "coinductive"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def (HOL) "coinductive_set"} & : & \isarkeep{local{\dsh}theory} \\ + @{attribute_def (HOL) 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 [@{command (HOL) "inductive"} and @{command (HOL) + "coinductive"}] define (co)inductive predicates from the + introduction rules given in the @{keyword "where"} part. The + optional @{keyword "for"} part contains a list of parameters of the + (co)inductive predicates that remain fixed throughout the + definition. The optional @{keyword "monos"} section contains + \emph{monotonicity theorems}, which are required for each operator + applied to a recursive set in the introduction rules. There + \emph{must} be a theorem of the form @{text "A \ B \ M A \ M B"}, + for each premise @{text "M R\<^sub>i t"} in an introduction rule! + + \item [@{command (HOL) "inductive_set"} and @{command (HOL) + "coinductive_set"}] are wrappers for to the previous commands, + allowing the definition of (co)inductive sets. + + \item [@{attribute (HOL) mono}] declares monotonicity rules. These + rule are involved in the automated monotonicity proof of @{command + (HOL) "inductive"}. + + \end{descr} +*} + + +subsection {* Derived rules *} + +text {* + Each (co)inductive definition @{text R} adds definitions to the + theory and also proves some theorems: + + \begin{description} + + \item [@{text R.intros}] is the list of introduction rules as proven + theorems, for the recursive predicates (or sets). The rules are + also available individually, using the names given them in the + theory file; + + \item [@{text R.cases}] is the case analysis (or elimination) rule; + + \item [@{text R.induct} or @{text R.coinduct}] is the (co)induction + rule. + + \end{description} + + When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are + defined simultaneously, the list of introduction rules is called + @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the case analysis rules are + called @{text "R\<^sub>1.cases, \, R\<^sub>n.cases"}, and the list + of mutual induction rules is called @{text + "R\<^sub>1_\_R\<^sub>n.inducts"}. +*} + + +subsection {* Monotonicity theorems *} + +text {* + Each theory contains a default set of theorems that are used in + monotonicity proofs. New rules can be added to this set via the + @{attribute (HOL) mono} attribute. The HOL theory @{text Inductive} + shows how this is done. In general, the following monotonicity + theorems may be added: + + \begin{itemize} + + \item Theorems of the form @{text "A \ B \ M A \ M B"}, for proving + monotonicity of inductive definitions whose introduction rules have + premises involving terms such as @{text "M R\<^sub>i t"}. + + \item Monotonicity theorems for logical operators, which are of the + general form @{text "(\ \ \) \ \ (\ \ \) \ \ \ \"}. For example, in + the case of the operator @{text "\"}, the corresponding theorem is + \[ + \infer{@{text "P\<^sub>1 \ P\<^sub>2 \ Q\<^sub>1 \ Q\<^sub>2"}}{@{text "P\<^sub>1 \ Q\<^sub>1"} & @{text "P\<^sub>2 \ Q\<^sub>2"}} + \] + + \item De Morgan style equations for reasoning about the ``polarity'' + of expressions, e.g. + \[ + @{prop "\ \ P \ P"} \qquad\qquad + @{prop "\ (P \ Q) \ \ P \ \ Q"} + \] + + \item Equations for reducing complex operators to more primitive + ones whose monotonicity can easily be proved, e.g. + \[ + @{prop "(P \ Q) \ \ P \ Q"} \qquad\qquad + @{prop "Ball A P \ \x. x \ A \ P x"} + \] + + \end{itemize} + + %FIXME: Example of an inductive definition +*} + + +section {* Arithmetic proof support *} + +text {* + \begin{matharray}{rcl} + @{method_def (HOL) arith} & : & \isarmeth \\ + @{method_def (HOL) arith_split} & : & \isaratt \\ + \end{matharray} + + The @{method (HOL) arith} method decides linear arithmetic problems + (on types @{text nat}, @{text int}, @{text real}). Any current + facts are inserted into the goal before running the procedure. + + The @{method (HOL) 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. +*} + + +section {* Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac} *} + +text {* + The following important tactical tools of Isabelle/HOL have been + ported to Isar. These should be never used in proper proof texts! + + \begin{matharray}{rcl} + @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\ + @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\ + @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\ + @{command_def (HOL) "inductive_cases"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'case\_tac' goalspec? term rule? + ; + 'induct\_tac' goalspec? (insts * 'and') rule? + ; + 'ind\_cases' (prop +) ('for' (name +)) ? + ; + 'inductive\_cases' (thmdecl? (prop +) + 'and') + ; + + rule: ('rule' ':' thmref) + ; + \end{rail} + + \begin{descr} + + \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}] + admit to reason about inductive datatypes only (unless an + alternative rule is given explicitly). Furthermore, @{method (HOL) + case_tac} does a classical case split on booleans; @{method (HOL) + 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 @{method induct} and @{method cases} proof + methods (see \secref{sec:cases-induct}). + + \item [@{method (HOL) ind_cases} and @{command (HOL) + "inductive_cases"}] provide an interface to the internal + \texttt{mk_cases} operation. Rules are simplified in an + unrestricted forward manner. + + While @{method (HOL) ind_cases} is a proof method to apply the + result immediately as elimination rules, @{command (HOL) + "inductive_cases"} provides case split theorems at the theory level + for later use. The @{keyword "for"} argument of the @{method (HOL) + ind_cases} method allows to specify a list of variables that should + be generalized before applying the resulting rule. + + \end{descr} +*} + + +section {* Executable code *} + +text {* + 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). + + \begin{matharray}{rcl} + @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def (HOL) "code_module"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_library"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "consts_code"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "types_code"} & : & \isartrans{theory}{theory} \\ + @{attribute_def (HOL) code} & : & \isaratt \\ + \end{matharray} + + \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 [@{command (HOL) "value"}~@{text t}] evaluates and prints a + term using the code generator. + + \end{descr} + + \medskip 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. + + \begin{matharray}{rcl} + @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{command_def (HOL) "code_datatype"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_const"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_type"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_class"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_instance"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_monad"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "code_exception"} & : & \isartrans{theory}{theory} \\ + @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ + @{attribute_def (HOL) code} & : & \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 + ; + + 'code' ('func' | 'inline') ( 'del' )? + ; + \end{rail} + + \begin{descr} + + \item [@{command (HOL) "export_code"}] is the canonical interface + for generating and serializing code: for a given list of constants, + code is generated for the specified target languages. 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 executable contants within a certain theory by giving @{text + "name.*"}, or referring to \emph{all} executable constants currently + available by giving @{text "*"}. + + By default, for each involved theory one corresponding name space + module is generated. Alternativly, a module name may be specified + after the @{keyword "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 ``@{text "-"}'' 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 ``@{text + "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim + "deriving (Read, Show)"}'' clause to each appropriate datatype + declaration. + + \item [@{command (HOL) "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 [@{command (HOL) "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 [@{command (HOL) "code_datatype"}] specifies a constructor set + for a logical type. + + \item [@{command (HOL) "code_const"}] associates a list of constants + with target-specific serializations; omitting a serialization + deletes an existing serialization. + + \item [@{command (HOL) "code_type"}] associates a list of type + constructors with target-specific serializations; omitting a + serialization deletes an existing serialization. + + \item [@{command (HOL) "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. This applies only to \emph{Haskell}. + + \item [@{command (HOL) "code_instance"}] declares a list of type + constructor / class instance relations as ``already present'' for a + given target. Omitting a ``@{text "-"}'' deletes an existing + ``already present'' declaration. This applies only to + \emph{Haskell}. + + \item [@{command (HOL) "code_monad"}] provides an auxiliary + mechanism to generate monadic code. + + \item [@{command (HOL) "code_reserved"}] declares a list of names as + reserved for a given target, preventing it to be shadowed by any + generated code. + + \item [@{command (HOL) "code_include"}] adds arbitrary named content + (``include'') to generated code. A as last argument ``@{text "-"}'' + will remove an already added ``include''. + + \item [@{command (HOL) "code_modulename"}] declares aliasings from + one module name onto another. + + \item [@{command (HOL) "code_exception"}] declares constants which + are not required to have a definition by a defining equations; these + are mapped on exceptions instead. + + \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or + with option ``@{text "del:"}'' deselects) a defining equation for + code generation. Usually packages introducing defining equations + provide a resonable default setup for selection. + + \item [@{attribute (HOL) code}@{text inline}] declares (or with + option ``@{text "del:"}'' removes) inlining theorems which are + applied as rewrite rules to any defining equation during + preprocessing. + + \item [@{command (HOL) "print_codesetup"}] gives an overview on + selected defining equations, code generator datatypes and + preprocessor setup. + + \end{descr} +*} + end + diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 08 12:27:19 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu May 08 12:29:18 2008 +0200 @@ -11,18 +11,1153 @@ \isatagtheory \isacommand{theory}\isamarkupfalse% \ HOL{\isacharunderscore}Specific\isanewline -\isakeyword{imports}\ HOL\isanewline -\isakeyword{begin}\isanewline -\isanewline +\isakeyword{imports}\ Main\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{HOL specific elements \label{ch:logics}% +} +\isamarkuptrue% +% +\isamarkupsection{Primitive types \label{sec:hol-typedef}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{command}{typedecl}\mbox{\isa{\isacommand{typedecl}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{typedef}\mbox{\isa{\isacommand{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 [\mbox{\isa{\isacommand{typedecl}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] is similar to the original \mbox{\isa{\isacommand{typedecl}}} of + Isabelle/Pure (see \secref{sec:types-pure}), but also declares type + arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an + actual HOL type constructor. %FIXME check, update + + \item [\mbox{\isa{\isacommand{typedef}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}] sets up a goal stating non-emptiness of the set \isa{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 \isa{A} and the new type \isa{t}. + + Technically, \mbox{\isa{\isacommand{typedef}}} defines both a type \isa{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 \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be + changed via an explicit \mbox{\isa{\isakeyword{morphisms}}} declaration). + + Theorems \isa{Rep{\isacharunderscore}t}, \isa{Rep{\isacharunderscore}t{\isacharunderscore}inverse}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inverse} provide the most basic characterization as a + corresponding injection/surjection pair (in both directions). Rules + \isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly + more convenient view on the injectivity part, suitable for automated + proof tools (e.g.\ in \mbox{\isa{simp}} or \mbox{\isa{iff}} declarations). + Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views on + surjectivity; these are already declared as set or type rules for + the generic \mbox{\isa{cases}} and \mbox{\isa{induct}} methods. + + An alternative name may be specified in parentheses; the default is + to use \isa{t} as indicated before. The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}'' + 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 \mbox{\isa{\isacommand{record}}} (see \secref{sec:hol-record}) or \mbox{\isa{\isacommand{datatype}}} (see \secref{sec:hol-datatype}).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Adhoc tuples% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \mbox{\isa{split{\isacharunderscore}format}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + 'split\_format' (((name *) + 'and') | ('(' 'complete' ')')) + ; + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{split{\isacharunderscore}format}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}}] puts expressions of + low-level tuple types into canonical form as specified by the + arguments given; the \isa{i}-th collection of arguments refers to + occurrences in premise \isa{i} of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' 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}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Records \label{sec:hol-record}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Basic concepts% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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 & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}} \\ + schematic & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} & + \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ M{\isasymrparr}{\isachardoublequote}} \\ + \end{tabular} + \end{center} + + \noindent The ASCII representation of \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} is \isa{{\isachardoublequote}{\isacharparenleft}{\isacharbar}\ x\ {\isacharequal}\ a\ {\isacharbar}{\isacharparenright}{\isachardoublequote}}. + + A fixed record \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} has field \isa{x} of value + \isa{a} and field \isa{y} of value \isa{b}. The corresponding + type is \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}}, assuming that \isa{{\isachardoublequote}a\ {\isacharcolon}{\isacharcolon}\ A{\isachardoublequote}} + and \isa{{\isachardoublequote}b\ {\isacharcolon}{\isacharcolon}\ B{\isachardoublequote}}. + + A record scheme like \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} contains fields + \isa{x} and \isa{y} as before, but also possibly further fields + as indicated by the ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' notation (which is actually part + of the syntax). The improper field ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' 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 \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part. + Fixed records are special instances of record schemes, where + ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}} + element. In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation + for \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}{\isachardoublequote}}. + + \medskip Two key observations make extensible records in a simply + typed language like HOL work out: + + \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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Record specifications% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{command}{record}\mbox{\isa{\isacommand{record}}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'record' typespec '=' (type '+')? (constdecl +) + ; + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{\isacommand{record}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}\ {\isacharplus}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}] defines + extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}}, + derived from the optional parent record \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} by adding new + field components \isa{{\isachardoublequote}c\isactrlsub i\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} etc. + + The type variables of \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i{\isachardoublequote}} need to be + covered by the (distinct) parameters \isa{{\isachardoublequote}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isachardoublequote}}. Type constructor \isa{t} has to be new, while \isa{{\isasymtau}} needs to specify an instance of an existing record type. At + least one new field \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} 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 \isa{{\isasymtau}} is optional; if omitted + \isa{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, \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is made a + type abbreviation for the fixed record type \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}}, likewise is \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharcomma}\ {\isasymzeta}{\isacharparenright}\ t{\isacharunderscore}scheme{\isachardoublequote}} made an abbreviation for + \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}}. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Record operations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Any record definition of the form presented above produces certain + standard operations. Selectors and updates are provided for any + field, including the improper one ``\isa{more}''. There are also + cumulative record constructor functions. To simplify the + presentation below, we assume for now that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is a root record with fields \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}. + + \medskip \textbf{Selectors} and \textbf{updates} are available for + any field (including ``\isa{more}''): + + \begin{matharray}{lll} + \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\ + \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\ + \end{matharray} + + There is special syntax for application of updates: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} abbreviates term \isa{{\isachardoublequote}x{\isacharunderscore}update\ a\ r{\isachardoublequote}}. Further notation for + repeated updates is also available: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}y\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}{\isasymlparr}z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}} may be written \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}. 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 \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}, 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} + \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\ + \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 \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} has ancestor + fields \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isachardoublequote}}, + the above record operations will get the following types: + + \begin{matharray}{lll} + \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\ + \isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\ + \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\ + \end{matharray} + \noindent + + \medskip Some further operations address the extension aspect of a + derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a + record fragment consisting of exactly the new fields introduced here + (the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} + takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record. + + \begin{matharray}{lll} + \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} \\ + \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\ + \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isacharcomma}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}} \\ + \end{matharray} + + \noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide + for root records.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Derived rules and proof tools% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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 + \isa{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 \mbox{\isa{simp}} method without further arguments. These rules + are available as \isa{{\isachardoublequote}t{\isachardot}simps{\isachardoublequote}}, 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 \isa{{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}\ {\isasymequiv}\ x\ {\isacharequal}\ x{\isacharprime}\ {\isasymand}\ y\ {\isacharequal}\ y{\isacharprime}{\isachardoublequote}} are declared to the Simplifier and Classical + Reasoner as \mbox{\isa{iff}} rules. These rules are available as + \isa{{\isachardoublequote}t{\isachardot}iffs{\isachardoublequote}}. + + \item The introduction rule for record equality analogous to \isa{{\isachardoublequote}x\ r\ {\isacharequal}\ x\ r{\isacharprime}\ {\isasymLongrightarrow}\ y\ r\ {\isacharequal}\ y\ r{\isacharprime}\ {\isasymdots}\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ r{\isacharprime}{\isachardoublequote}} is declared to the Simplifier, + and as the basic rule context as ``\mbox{\isa{intro}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''. + The rule is called \isa{{\isachardoublequote}t{\isachardot}equality{\isachardoublequote}}. + + \item Representations of arbitrary record expressions as canonical + constructor terms are provided both in \mbox{\isa{cases}} and \mbox{\isa{induct}} format (cf.\ the generic proof methods of the same name, + \secref{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 ``\isa{{\isachardoublequote}{\isacharparenleft}cases\ r{\isacharparenright}{\isachardoublequote}}'' to a certain proof problem. + + \item The derived record operations \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} are \emph{not} + treated automatically, but usually need to be expanded by hand, + using the collective fact \isa{{\isachardoublequote}t{\isachardot}defs{\isachardoublequote}}. + + \end{enumerate}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Datatypes \label{sec:hol-datatype}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{rep-datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'datatype' (dtspec + 'and') + ; + 'rep\_datatype' (name *) dtrules + ; + + dtspec: parname? typespec infix? '=' (cons + '|') + ; + cons: name (type *) mixfix? + ; + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{\isacommand{datatype}}}] defines inductive datatypes in + HOL. + + \item [\mbox{\isa{\isacommand{rep{\isacharunderscore}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 \secref{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 \mbox{\isa{case{\isacharunderscore}tac}} and \mbox{\isa{induct{\isacharunderscore}tac}} available, see \secref{sec:hol-induct-tac}; these admit + to refer directly to the internal structure of subgoals (including + internally bound parameters).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Recursive functions \label{sec:recursion}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{command}{primrec}\mbox{\isa{\isacommand{primrec}}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{HOL}{command}{fun}\mbox{\isa{\isacommand{fun}}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{HOL}{command}{function}\mbox{\isa{\isacommand{function}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \indexdef{HOL}{command}{termination}\mbox{\isa{\isacommand{termination}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \end{matharray} + + \railalias{funopts}{function\_opts} %FIXME ?? + + \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 [\mbox{\isa{\isacommand{primrec}}}] defines primitive recursive + functions over datatypes, see also \cite{isabelle-HOL}. + + \item [\mbox{\isa{\isacommand{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 \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule + (named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain + predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \mbox{\isa{\isacommand{termination}}} + command can then be used to establish that the function is total. + + \item [\mbox{\isa{\isacommand{fun}}}] is a shorthand notation for + ``\mbox{\isa{\isacommand{function}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by + automated proof attempts regarding pattern matching and termination. + See \cite{isabelle-function} for further details. + + \item [\mbox{\isa{\isacommand{termination}}}~\isa{f}] commences a + termination proof for the previously defined function \isa{f}. If + this is omitted, the command refers to the most recent function + definition. After the proof is closed, the recursive equations and + the induction principle is established. + + \end{descr} + + %FIXME check + + Recursive definitions introduced by both the \mbox{\isa{\isacommand{primrec}}} and the \mbox{\isa{\isacommand{function}}} command accommodate + reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{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 \mbox{\isa{\isacommand{primrec}}} are that of the datatypes involved, while those of + \mbox{\isa{\isacommand{function}}} are numbered (starting from 1). + + The equations provided by these packages may be referred later as + theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective) + name of the functions defined. Individual equations may be named + explicitly as well. + + The \mbox{\isa{\isacommand{function}}} command accepts the following + options. + + \begin{descr} + + \item [\isa{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 [\isa{{\isachardoublequote}{\isasymIN}\ name{\isachardoublequote}}] gives the target for the definition. + %FIXME ?!? + + \item [\isa{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 [\isa{tailrec}] generates the unconstrained recursive + equations even without a termination proof, provided that the + function is tail-recursive. This currently only works + + \item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a + (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}} + whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Proof methods related to recursive definitions% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{method}{pat-completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\ + \indexdef{HOL}{method}{relation}\mbox{\isa{relation}} & : & \isarmeth \\ + \indexdef{HOL}{method}{lexicographic-order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\ + \end{matharray} + + \begin{rail} + 'relation' term + ; + 'lexicographic\_order' (clasimpmod *) + ; + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{pat{\isacharunderscore}completeness}}] is a specialized method to + solve goals regarding the completeness of pattern matching, as + required by the \mbox{\isa{\isacommand{function}}} package (cf.\ + \cite{isabelle-function}). + + \item [\mbox{\isa{relation}}~\isa{R}] introduces a termination + proof using the relation \isa{R}. The resulting proof state will + contain goals expressing that \isa{R} is wellfounded, and that the + arguments of recursive calls decrease with respect to \isa{R}. + Usually, this method is used as the initial proof step of manual + termination proofs. + + \item [\mbox{\isa{lexicographic{\isacharunderscore}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 \mbox{\isa{auto}} method, + which it uses internally to prove local descents. The same context + modifiers as for \mbox{\isa{auto}} are accepted, see + \secref{sec:clasimp}. + + In case of failure, extensive information is printed, which can help + to analyse the situation (cf.\ \cite{isabelle-function}). + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Old-style recursive function definitions (TFL)% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The old TFL commands \mbox{\isa{\isacommand{recdef}}} and \mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}} for defining recursive are mostly obsolete; \mbox{\isa{\isacommand{function}}} or \mbox{\isa{\isacommand{fun}}} should be used instead. + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{recdef-tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\ + \end{matharray} + + \begin{rail} + 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? + ; + recdeftc thmdecl? tc + ; + hints: '(' 'hints' (recdefmod *) ')' + ; + recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod + ; + tc: nameref ('(' nat ')')? + ; + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{\isacommand{recdef}}}] defines general well-founded + recursive functions (using the TFL package), see also + \cite{isabelle-HOL}. The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells + TFL to recover from failed proof attempts, returning unfinished + results. The \isa{recdef{\isacharunderscore}simp}, \isa{recdef{\isacharunderscore}cong}, and \isa{recdef{\isacharunderscore}wf} hints refer to auxiliary rules to be used in the internal + automated proof process of TFL. Additional \mbox{\isa{clasimpmod}} + declarations (cf.\ \secref{sec:clasimp}) may be given to tune the + context of the Simplifier (cf.\ \secref{sec:simplifier}) and + Classical reasoner (cf.\ \secref{sec:classical}). + + \item [\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the + proof for leftover termination condition number \isa{i} (default + 1) as generated by a \mbox{\isa{\isacommand{recdef}}} definition of + constant \isa{c}. + + Note that in most cases, \mbox{\isa{\isacommand{recdef}}} is able to finish + its internal proofs without manual intervention. + + \end{descr} + + \medskip Hints for \mbox{\isa{\isacommand{recdef}}} may be also declared + globally, using the following attributes. + + \begin{matharray}{rcl} + \indexdef{HOL}{attribute}{recdef-simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\ + \indexdef{HOL}{attribute}{recdef-cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\ + \indexdef{HOL}{attribute}{recdef-wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') + ; + \end{rail}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Definition by specification \label{sec:hol-specification}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\ + \indexdef{HOL}{command}{ax-specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\ + \end{matharray} + + \begin{rail} + ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) + ; + decl: ((name ':')? term '(' 'overloaded' ')'?) + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{\isacommand{specification}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a + goal stating the existence of terms with the properties specified to + hold for the constants given in \isa{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 [\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets + up a goal stating the existence of terms with the properties + specified to hold for the constants given in \isa{decls}. After + finishing the proof, the theory will be augmented with axioms + expressing the properties given in the first place. + + \item [\isa{decl}] declares a constant to be defined by the + specification given. The definition for the constant \isa{c} is + bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in + the declaration. Overloaded constants should be declared as such. + + \end{descr} + + Whether to use \mbox{\isa{\isacommand{specification}}} or \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} is to some extent a matter of style. \mbox{\isa{\isacommand{specification}}} introduces no new axioms, and so by + construction cannot introduce inconsistencies, whereas \mbox{\isa{\isacommand{ax{\isacharunderscore}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 \mbox{\isa{\isacommand{specification}}}, one can prove + that the two constants are, in fact, equal. If this might be a + problem, one should use \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +An \textbf{inductive definition} specifies the least predicate (or + set) \isa{R} closed under given rules: applying a rule to elements + of \isa{R} yields a result within \isa{R}. For example, a + structural operational semantics is an inductive definition of an + evaluation relation. + + Dually, a \textbf{coinductive definition} specifies the greatest + predicate~/ set \isa{R} that is consistent with given rules: every + element of \isa{R} can be seen as arising by applying a rule to + elements of \isa{R}. An important example is using bisimulation + relations to formalise equivalence of processes and infinite data + structures. + + \medskip The HOL package is related to the ZF one, which is + 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 that of ZF thanks to implicit type-checking in HOL. + 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. + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{HOL}{command}{inductive-set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{HOL}{command}{coinductive-set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{HOL}{attribute}{mono}\mbox{\isa{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 [\mbox{\isa{\isacommand{inductive}}} and \mbox{\isa{\isacommand{coinductive}}}] define (co)inductive predicates from the + introduction rules given in the \mbox{\isa{\isakeyword{where}}} part. The + optional \mbox{\isa{\isakeyword{for}}} part contains a list of parameters of the + (co)inductive predicates that remain fixed throughout the + definition. The optional \mbox{\isa{\isakeyword{monos}}} section contains + \emph{monotonicity theorems}, which are required for each operator + applied to a recursive set in the introduction rules. There + \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, + for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule! + + \item [\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} and \mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}] are wrappers for to the previous commands, + allowing the definition of (co)inductive sets. + + \item [\mbox{\isa{mono}}] declares monotonicity rules. These + rule are involved in the automated monotonicity proof of \mbox{\isa{\isacommand{inductive}}}. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Derived rules% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Each (co)inductive definition \isa{R} adds definitions to the + theory and also proves some theorems: + + \begin{description} + + \item [\isa{R{\isachardot}intros}] is the list of introduction rules as proven + theorems, for the recursive predicates (or sets). The rules are + also available individually, using the names given them in the + theory file; + + \item [\isa{R{\isachardot}cases}] is the case analysis (or elimination) rule; + + \item [\isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct}] is the (co)induction + rule. + + \end{description} + + When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are + defined simultaneously, the list of introduction rules is called + \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are + called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list + of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Monotonicity theorems% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Each theory contains a default set of theorems that are used in + monotonicity proofs. New rules can be added to this set via the + \mbox{\isa{mono}} attribute. The HOL theory \isa{Inductive} + shows how this is done. In general, the following monotonicity + theorems may be added: + + \begin{itemize} + + \item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving + monotonicity of inductive definitions whose introduction rules have + premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}. + + \item Monotonicity theorems for logical operators, which are of the + general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}. For example, in + the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is + \[ + \infer{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymor}\ P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}\ {\isasymor}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}} + \] + + \item De Morgan style equations for reasoning about the ``polarity'' + of expressions, e.g. + \[ + \isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad + \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}} + \] + + \item Equations for reducing complex operators to more primitive + ones whose monotonicity can easily be proved, e.g. + \[ + \isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad + \isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}} + \] + + \end{itemize} + + %FIXME: Example of an inductive definition% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Arithmetic proof support% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\ + \indexdef{HOL}{method}{arith-split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\ + \end{matharray} + + The \mbox{\isa{arith}} method decides linear arithmetic problems + (on types \isa{nat}, \isa{int}, \isa{real}). Any current + facts are inserted into the goal before running the procedure. + + The \mbox{\isa{arith{\isacharunderscore}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.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The following important tactical tools of Isabelle/HOL have been + ported to Isar. These should be never used in proper proof texts! + + \begin{matharray}{rcl} + \indexdef{HOL}{method}{case-tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ + \indexdef{HOL}{method}{induct-tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ + \indexdef{HOL}{method}{ind-cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\ + \indexdef{HOL}{command}{inductive-cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'case\_tac' goalspec? term rule? + ; + 'induct\_tac' goalspec? (insts * 'and') rule? + ; + 'ind\_cases' (prop +) ('for' (name +)) ? + ; + 'inductive\_cases' (thmdecl? (prop +) + 'and') + ; + + rule: ('rule' ':' thmref) + ; + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{case{\isacharunderscore}tac}} and \mbox{\isa{induct{\isacharunderscore}tac}}] + admit to reason about inductive datatypes only (unless an + alternative rule is given explicitly). Furthermore, \mbox{\isa{case{\isacharunderscore}tac}} does a classical case split on booleans; \mbox{\isa{induct{\isacharunderscore}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 \mbox{\isa{induct}} and \mbox{\isa{cases}} proof + methods (see \secref{sec:cases-induct}). + + \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}] provide an interface to the internal + \texttt{mk_cases} operation. Rules are simplified in an + unrestricted forward manner. + + While \mbox{\isa{ind{\isacharunderscore}cases}} is a proof method to apply the + result immediately as elimination rules, \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} provides case split theorems at the theory level + for later use. The \mbox{\isa{\isakeyword{for}}} argument of the \mbox{\isa{ind{\isacharunderscore}cases}} method allows to specify a list of variables that should + be generalized before applying the resulting rule. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Executable code% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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). + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{HOL}{command}{code-module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{consts-code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{types-code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\ + \end{matharray} + + \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 [\mbox{\isa{\isacommand{value}}}~\isa{t}] evaluates and prints a + term using the code generator. + + \end{descr} + + \medskip 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. + + \begin{matharray}{rcl} + \indexdef{HOL}{command}{export-code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{HOL}{command}{code-thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{HOL}{command}{code-deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{HOL}{command}{code-datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{code-exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\ + \indexdef{HOL}{command}{print-codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\ + \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \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 + ; + + 'code' ('func' | 'inline') ( 'del' )? + ; + \end{rail} + + \begin{descr} + + \item [\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}] is the canonical interface + for generating and serializing code: for a given list of constants, + code is generated for the specified target languages. 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 executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently + available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}. + + By default, for each involved theory one corresponding name space + module is generated. Alternativly, a module name may be specified + after the \mbox{\isa{\isakeyword{module{\isacharunderscore}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 ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' 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 ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype + declaration. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}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 [\mbox{\isa{\isacommand{code{\isacharunderscore}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 [\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}] specifies a constructor set + for a logical type. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}] associates a list of constants + with target-specific serializations; omitting a serialization + deletes an existing serialization. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}] associates a list of type + constructors with target-specific serializations; omitting a + serialization deletes an existing serialization. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}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. This applies only to \emph{Haskell}. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}] declares a list of type + constructor / class instance relations as ``already present'' for a + given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing + ``already present'' declaration. This applies only to + \emph{Haskell}. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}] provides an auxiliary + mechanism to generate monadic code. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}] declares a list of names as + reserved for a given target, preventing it to be shadowed by any + generated code. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}] adds arbitrary named content + (``include'') to generated code. A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' + will remove an already added ``include''. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}] declares aliasings from + one module name onto another. + + \item [\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}] declares constants which + are not required to have a definition by a defining equations; these + are mapped on exceptions instead. + + \item [\mbox{\isa{code}}~\isa{func}] explicitly selects (or + with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for + code generation. Usually packages introducing defining equations + provide a resonable default setup for selection. + + \item [\mbox{\isa{code}}\isa{inline}] declares (or with + option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are + applied as rewrite rules to any defining equation during + preprocessing. + + \item [\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}] gives an overview on + selected defining equations, code generator datatypes and + preprocessor setup. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory \isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% % \isadelimtheory -\isanewline % \endisadelimtheory +\isanewline +\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/Thy/document/session.tex --- a/doc-src/IsarRef/Thy/document/session.tex Thu May 08 12:27:19 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/session.tex Thu May 08 12:29:18 2008 +0200 @@ -1,4 +1,16 @@ -\input{ZF_Specific.tex} +\input{intro.tex} + +\input{syntax.tex} + +\input{pure.tex} + +\input{Generic.tex} + +\input{HOL_Specific.tex} + +\input{Quick_Reference.tex} + +\input{ML_Tactic.tex} %%% Local Variables: %%% mode: latex diff -r d3d750ada604 -r df50bc1249d7 doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Thu May 08 12:27:19 2008 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Thu May 08 12:29:18 2008 +0200 @@ -85,7 +85,6 @@ \input{Thy/document/HOL_Specific.tex} \input{Thy/document/HOLCF_Specific.tex} \input{Thy/document/ZF_Specific.tex} -\input{logics.tex} \appendix \input{Thy/document/Quick_Reference.tex} 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: