wenzelm@26840: theory HOL_Specific wenzelm@26849: imports Main wenzelm@26840: begin wenzelm@26840: wenzelm@26852: chapter {* Isabelle/HOL \label{ch:hol} *} wenzelm@26849: wenzelm@26849: section {* Primitive types \label{sec:hol-typedef} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "typedecl"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "typedef"} & : & @{text "theory \ proof(prove)"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'typedecl' typespec infix? wenzelm@26849: ; wenzelm@26849: 'typedef' altname? abstype '=' repset wenzelm@26849: ; wenzelm@26849: wenzelm@26849: altname: '(' (name | 'open' | 'open' name) ')' wenzelm@26849: ; wenzelm@26849: abstype: typespec infix? wenzelm@26849: ; wenzelm@26849: repset: term ('morphisms' name name)? wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} is similar wenzelm@28760: to the original @{command "typedecl"} of Isabelle/Pure (see wenzelm@28760: \secref{sec:types-pure}), but also declares type arity @{text "t :: wenzelm@28760: (type, \, type) type"}, making @{text t} an actual HOL type wenzelm@28760: constructor. %FIXME check, update wenzelm@26849: wenzelm@28760: \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} sets up wenzelm@28760: a goal stating non-emptiness of the set @{text A}. After finishing wenzelm@28760: the proof, the theory will be augmented by a Gordon/HOL-style type wenzelm@28760: definition, which establishes a bijection between the representing wenzelm@28760: set @{text A} and the new type @{text t}. wenzelm@26849: wenzelm@26849: Technically, @{command (HOL) "typedef"} defines both a type @{text wenzelm@26849: t} and a set (term constant) of the same name (an alternative base wenzelm@26849: name may be given in parentheses). The injection from type to set wenzelm@26849: is called @{text Rep_t}, its inverse @{text Abs_t} (this may be wenzelm@26849: changed via an explicit @{keyword (HOL) "morphisms"} declaration). wenzelm@26849: wenzelm@26849: Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text wenzelm@26849: Abs_t_inverse} provide the most basic characterization as a wenzelm@26849: corresponding injection/surjection pair (in both directions). Rules wenzelm@26849: @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly wenzelm@26849: more convenient view on the injectivity part, suitable for automated wenzelm@26894: proof tools (e.g.\ in @{attribute simp} or @{attribute iff} wenzelm@26894: declarations). Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and wenzelm@26894: @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views wenzelm@26894: on surjectivity; these are already declared as set or type rules for wenzelm@26849: the generic @{method cases} and @{method induct} methods. wenzelm@26849: wenzelm@26849: An alternative name may be specified in parentheses; the default is wenzelm@26849: to use @{text t} as indicated before. The ``@{text "(open)"}'' wenzelm@26849: declaration suppresses a separate constant definition for the wenzelm@26849: representing set. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: wenzelm@26849: Note that raw type declarations are rarely used in practice; the wenzelm@26849: main application is with experimental (or even axiomatic!) theory wenzelm@26849: fragments. Instead of primitive HOL type definitions, user-level wenzelm@26849: theories usually refer to higher-level packages such as @{command wenzelm@26849: (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL) wenzelm@26849: "datatype"} (see \secref{sec:hol-datatype}). wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Adhoc tuples *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} haftmann@31912: 'split\_format' ((( name * ) + 'and') | ('(' 'complete' ')')) wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m \ \ wenzelm@28760: \ q\<^sub>1 \ q\<^sub>n"} puts expressions of low-level tuple types into wenzelm@28760: canonical form as specified by the arguments given; the @{text i}-th wenzelm@28760: collection of arguments refers to occurrences in premise @{text i} wenzelm@28760: of the rule. The ``@{text "(complete)"}'' option causes \emph{all} wenzelm@28760: arguments in function applications to be represented canonically wenzelm@28760: according to their tuple type structure. wenzelm@26849: wenzelm@26849: Note that these operations tend to invent funny names for new local wenzelm@26849: parameters to be introduced. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Records \label{sec:hol-record} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: In principle, records merely generalize the concept of tuples, where wenzelm@26849: components may be addressed by labels instead of just position. The wenzelm@26849: logical infrastructure of records in Isabelle/HOL is slightly more wenzelm@26849: advanced, though, supporting truly extensible record schemes. This wenzelm@26849: admits operations that are polymorphic with respect to record wenzelm@26849: extension, yielding ``object-oriented'' effects like (single) wenzelm@26849: inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more wenzelm@26849: details on object-oriented verification and record subtyping in HOL. wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Basic concepts *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records wenzelm@26849: at the level of terms and types. The notation is as follows: wenzelm@26849: wenzelm@26849: \begin{center} wenzelm@26849: \begin{tabular}{l|l|l} wenzelm@26849: & record terms & record types \\ \hline wenzelm@26849: fixed & @{text "\x = a, y = b\"} & @{text "\x :: A, y :: B\"} \\ wenzelm@26849: schematic & @{text "\x = a, y = b, \ = m\"} & wenzelm@26849: @{text "\x :: A, y :: B, \ :: M\"} \\ wenzelm@26849: \end{tabular} wenzelm@26849: \end{center} wenzelm@26849: wenzelm@26849: \noindent The ASCII representation of @{text "\x = a\"} is @{text wenzelm@26849: "(| x = a |)"}. wenzelm@26849: wenzelm@26849: A fixed record @{text "\x = a, y = b\"} has field @{text x} of value wenzelm@26849: @{text a} and field @{text y} of value @{text b}. The corresponding wenzelm@26849: type is @{text "\x :: A, y :: B\"}, assuming that @{text "a :: A"} wenzelm@26849: and @{text "b :: B"}. wenzelm@26849: wenzelm@26849: A record scheme like @{text "\x = a, y = b, \ = m\"} contains fields wenzelm@26849: @{text x} and @{text y} as before, but also possibly further fields wenzelm@26849: as indicated by the ``@{text "\"}'' notation (which is actually part wenzelm@26849: of the syntax). The improper field ``@{text "\"}'' of a record wenzelm@26849: scheme is called the \emph{more part}. Logically it is just a free wenzelm@26849: variable, which is occasionally referred to as ``row variable'' in wenzelm@26849: the literature. The more part of a record scheme may be wenzelm@26849: instantiated by zero or more further components. For example, the wenzelm@26849: previous scheme may get instantiated to @{text "\x = a, y = b, z = wenzelm@26852: c, \ = m'\"}, where @{text m'} refers to a different more part. wenzelm@26849: Fixed records are special instances of record schemes, where wenzelm@26849: ``@{text "\"}'' is properly terminated by the @{text "() :: unit"} wenzelm@26849: element. In fact, @{text "\x = a, y = b\"} is just an abbreviation wenzelm@26849: for @{text "\x = a, y = b, \ = ()\"}. wenzelm@26849: wenzelm@26849: \medskip Two key observations make extensible records in a simply wenzelm@26849: typed language like HOL work out: wenzelm@26849: wenzelm@26849: \begin{enumerate} wenzelm@26849: wenzelm@26849: \item the more part is internalized, as a free term or type wenzelm@26849: variable, wenzelm@26849: wenzelm@26852: \item field names are externalized, they cannot be accessed within wenzelm@26852: the logic as first-class values. wenzelm@26849: wenzelm@26849: \end{enumerate} wenzelm@26849: wenzelm@26849: \medskip In Isabelle/HOL record types have to be defined explicitly, wenzelm@26849: fixing their field names and types, and their (optional) parent wenzelm@26849: record. Afterwards, records may be formed using above syntax, while wenzelm@26849: obeying the canonical order of fields as given by their declaration. wenzelm@26849: The record package provides several standard operations like wenzelm@26849: selectors and updates. The common setup for various generic proof wenzelm@26849: tools enable succinct reasoning patterns. See also the Isabelle/HOL wenzelm@26849: tutorial \cite{isabelle-hol-book} for further instructions on using wenzelm@26849: records in practice. wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Record specifications *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "record"} & : & @{text "theory \ theory"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'record' typespec '=' (type '+')? (constdecl +) wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "record"}~@{text "(\\<^sub>1, \, \\<^sub>m) t = \ + c\<^sub>1 :: \\<^sub>1 wenzelm@28760: \ c\<^sub>n :: \\<^sub>n"} defines extensible record type @{text "(\\<^sub>1, \, \\<^sub>m) t"}, wenzelm@26849: derived from the optional parent record @{text "\"} by adding new wenzelm@26849: field components @{text "c\<^sub>i :: \\<^sub>i"} etc. wenzelm@26849: wenzelm@26849: The type variables of @{text "\"} and @{text "\\<^sub>i"} need to be wenzelm@26849: covered by the (distinct) parameters @{text "\\<^sub>1, \, wenzelm@26849: \\<^sub>m"}. Type constructor @{text t} has to be new, while @{text wenzelm@26849: \} needs to specify an instance of an existing record type. At wenzelm@26849: least one new field @{text "c\<^sub>i"} has to be specified. wenzelm@26849: Basically, field names need to belong to a unique record. This is wenzelm@26849: not a real restriction in practice, since fields are qualified by wenzelm@26849: the record name internally. wenzelm@26849: wenzelm@26849: The parent record specification @{text \} is optional; if omitted wenzelm@26849: @{text t} becomes a root record. The hierarchy of all records wenzelm@26849: declared within a theory context forms a forest structure, i.e.\ a wenzelm@26849: set of trees starting with a root record each. There is no way to wenzelm@26849: merge multiple parent records! wenzelm@26849: wenzelm@26849: For convenience, @{text "(\\<^sub>1, \, \\<^sub>m) t"} is made a wenzelm@26849: type abbreviation for the fixed record type @{text "\c\<^sub>1 :: wenzelm@26849: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n\"}, likewise is @{text wenzelm@26849: "(\\<^sub>1, \, \\<^sub>m, \) t_scheme"} made an abbreviation for wenzelm@26849: @{text "\c\<^sub>1 :: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n, \ :: wenzelm@26849: \\"}. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Record operations *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: Any record definition of the form presented above produces certain wenzelm@26849: standard operations. Selectors and updates are provided for any wenzelm@26849: field, including the improper one ``@{text more}''. There are also wenzelm@26849: cumulative record constructor functions. To simplify the wenzelm@26849: presentation below, we assume for now that @{text "(\\<^sub>1, \, wenzelm@26849: \\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 :: wenzelm@26849: \\<^sub>1, \, c\<^sub>n :: \\<^sub>n"}. wenzelm@26849: wenzelm@26849: \medskip \textbf{Selectors} and \textbf{updates} are available for wenzelm@26849: any field (including ``@{text more}''): wenzelm@26849: wenzelm@26849: \begin{matharray}{lll} wenzelm@26852: @{text "c\<^sub>i"} & @{text "::"} & @{text "\\<^vec>c :: \<^vec>\, \ :: \\ \ \\<^sub>i"} \\ wenzelm@26852: @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ \\<^vec>c :: \<^vec>\, \ :: \\ \ \\<^vec>c :: \<^vec>\, \ :: \\"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: There is special syntax for application of updates: @{text "r\x := wenzelm@26849: a\"} abbreviates term @{text "x_update a r"}. Further notation for wenzelm@26849: repeated updates is also available: @{text "r\x := a\\y := b\\z := wenzelm@26849: c\"} may be written @{text "r\x := a, y := b, z := c\"}. Note that wenzelm@26849: because of postfix notation the order of fields shown here is wenzelm@26849: reverse than in the actual term. Since repeated updates are just wenzelm@26849: function applications, fields may be freely permuted in @{text "\x wenzelm@26849: := a, y := b, z := c\"}, as far as logical equality is concerned. wenzelm@26849: Thus commutativity of independent updates can be proven within the wenzelm@26849: logic for any two fields, but not as a general theorem. wenzelm@26849: wenzelm@26849: \medskip The \textbf{make} operation provides a cumulative record wenzelm@26849: constructor function: wenzelm@26849: wenzelm@26849: \begin{matharray}{lll} wenzelm@26852: @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \\<^vec>c :: \<^vec>\\"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \medskip We now reconsider the case of non-root records, which are wenzelm@26849: derived of some parent. In general, the latter may depend on wenzelm@26849: another parent as well, resulting in a list of \emph{ancestor wenzelm@26849: records}. Appending the lists of fields of all ancestors results in wenzelm@26849: a certain field prefix. The record package automatically takes care wenzelm@26849: of this by lifting operations over this context of ancestor fields. wenzelm@26849: Assuming that @{text "(\\<^sub>1, \, \\<^sub>m) t"} has ancestor wenzelm@26849: fields @{text "b\<^sub>1 :: \\<^sub>1, \, b\<^sub>k :: \\<^sub>k"}, wenzelm@26849: the above record operations will get the following types: wenzelm@26849: wenzelm@26852: \medskip wenzelm@26852: \begin{tabular}{lll} wenzelm@26852: @{text "c\<^sub>i"} & @{text "::"} & @{text "\\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\ \ \\<^sub>i"} \\ wenzelm@26849: @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\\<^sub>i \ wenzelm@26852: \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\ \ wenzelm@26852: \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\"} \\ wenzelm@26852: @{text "t.make"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>k \ \\<^sub>1 \ \ \\<^sub>n \ wenzelm@26852: \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\\"} \\ wenzelm@26852: \end{tabular} wenzelm@26852: \medskip wenzelm@26849: wenzelm@26852: \noindent Some further operations address the extension aspect of a wenzelm@26849: derived record scheme specifically: @{text "t.fields"} produces a wenzelm@26849: record fragment consisting of exactly the new fields introduced here wenzelm@26849: (the result may serve as a more part elsewhere); @{text "t.extend"} wenzelm@26849: takes a fixed record and adds a given more part; @{text wenzelm@26849: "t.truncate"} restricts a record scheme to a fixed record. wenzelm@26849: wenzelm@26852: \medskip wenzelm@26852: \begin{tabular}{lll} wenzelm@26852: @{text "t.fields"} & @{text "::"} & @{text "\\<^sub>1 \ \ \\<^sub>n \ \\<^vec>c :: \<^vec>\\"} \\ wenzelm@26852: @{text "t.extend"} & @{text "::"} & @{text "\\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\\ \ wenzelm@26852: \ \ \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\"} \\ wenzelm@26852: @{text "t.truncate"} & @{text "::"} & @{text "\\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\, \ :: \\ \ \\<^vec>b :: \<^vec>\, \<^vec>c :: \<^vec>\\"} \\ wenzelm@26852: \end{tabular} wenzelm@26852: \medskip wenzelm@26849: wenzelm@26849: \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide wenzelm@26849: for root records. wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Derived rules and proof tools *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: The record package proves several results internally, declaring wenzelm@26849: these facts to appropriate proof tools. This enables users to wenzelm@26849: reason about record structures quite conveniently. Assume that wenzelm@26849: @{text t} is a record type as specified above. wenzelm@26849: wenzelm@26849: \begin{enumerate} wenzelm@26849: wenzelm@26849: \item Standard conversions for selectors or updates applied to wenzelm@26849: record constructor terms are made part of the default Simplifier wenzelm@26849: context; thus proofs by reduction of basic operations merely require wenzelm@26849: the @{method simp} method without further arguments. These rules wenzelm@26849: are available as @{text "t.simps"}, too. wenzelm@26849: wenzelm@26849: \item Selectors applied to updated records are automatically reduced wenzelm@26849: by an internal simplification procedure, which is also part of the wenzelm@26849: standard Simplifier setup. wenzelm@26849: wenzelm@26849: \item Inject equations of a form analogous to @{prop "(x, y) = (x', wenzelm@26849: y') \ x = x' \ y = y'"} are declared to the Simplifier and Classical wenzelm@26849: Reasoner as @{attribute iff} rules. These rules are available as wenzelm@26849: @{text "t.iffs"}. wenzelm@26849: wenzelm@26849: \item The introduction rule for record equality analogous to @{text wenzelm@26849: "x r = x r' \ y r = y r' \ \ r = r'"} is declared to the Simplifier, wenzelm@26849: and as the basic rule context as ``@{attribute intro}@{text "?"}''. wenzelm@26849: The rule is called @{text "t.equality"}. wenzelm@26849: wenzelm@26849: \item Representations of arbitrary record expressions as canonical wenzelm@26849: constructor terms are provided both in @{method cases} and @{method wenzelm@26849: induct} format (cf.\ the generic proof methods of the same name, wenzelm@26849: \secref{sec:cases-induct}). Several variations are available, for wenzelm@26849: fixed records, record schemes, more parts etc. wenzelm@26849: wenzelm@26849: The generic proof methods are sufficiently smart to pick the most wenzelm@26849: sensible rule according to the type of the indicated record wenzelm@26849: expression: users just need to apply something like ``@{text "(cases wenzelm@26849: r)"}'' to a certain proof problem. wenzelm@26849: wenzelm@26849: \item The derived record operations @{text "t.make"}, @{text wenzelm@26849: "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not} wenzelm@26849: treated automatically, but usually need to be expanded by hand, wenzelm@26849: using the collective fact @{text "t.defs"}. wenzelm@26849: wenzelm@26849: \end{enumerate} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Datatypes \label{sec:hol-datatype} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "datatype"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "rep_datatype"} & : & @{text "theory \ proof(prove)"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'datatype' (dtspec + 'and') wenzelm@26849: ; haftmann@27452: 'rep\_datatype' ('(' (name +) ')')? (term +) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: dtspec: parname? typespec infix? '=' (cons + '|') wenzelm@26849: ; haftmann@31912: cons: name ( type * ) mixfix? wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "datatype"} defines inductive datatypes in wenzelm@26849: HOL. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "rep_datatype"} represents existing types as wenzelm@26849: inductive ones, generating the standard infrastructure of derived wenzelm@26849: concepts (primitive recursion etc.). wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: wenzelm@26849: The induction and exhaustion theorems generated provide case names wenzelm@26849: according to the constructors involved, while parameters are named wenzelm@26849: after the types (see also \secref{sec:cases-induct}). wenzelm@26849: wenzelm@26849: See \cite{isabelle-HOL} for more details on datatypes, but beware of wenzelm@26849: the old-style theory syntax being used there! Apart from proper wenzelm@26849: proof methods for case-analysis and induction, there are also wenzelm@26849: emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL) wenzelm@26849: induct_tac} available, see \secref{sec:hol-induct-tac}; these admit wenzelm@26849: to refer directly to the internal structure of subgoals (including wenzelm@26849: internally bound parameters). wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Recursive functions \label{sec:recursion} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "primrec"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def (HOL) "fun"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def (HOL) "function"} & : & @{text "local_theory \ proof(prove)"} \\ wenzelm@28761: @{command_def (HOL) "termination"} & : & @{text "local_theory \ proof(prove)"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'primrec' target? fixes 'where' equations wenzelm@26849: ; wenzelm@26849: equations: (thmdecl? prop + '|') wenzelm@26849: ; wenzelm@26985: ('fun' | 'function') target? functionopts? fixes 'where' clauses wenzelm@26849: ; wenzelm@26849: clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|') wenzelm@26849: ; wenzelm@26985: functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')' wenzelm@26849: ; wenzelm@26849: 'termination' ( term )? wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "primrec"} defines primitive recursive wenzelm@26849: functions over datatypes, see also \cite{isabelle-HOL}. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "function"} defines functions by general wenzelm@26849: wellfounded recursion. A detailed description with examples can be wenzelm@26849: found in \cite{isabelle-function}. The function is specified by a wenzelm@26849: set of (possibly conditional) recursive equations with arbitrary wenzelm@26849: pattern matching. The command generates proof obligations for the wenzelm@26849: completeness and the compatibility of patterns. wenzelm@26849: wenzelm@26849: The defined function is considered partial, and the resulting wenzelm@26849: simplification rules (named @{text "f.psimps"}) and induction rule wenzelm@26849: (named @{text "f.pinduct"}) are guarded by a generated domain wenzelm@26849: predicate @{text "f_dom"}. The @{command (HOL) "termination"} wenzelm@26849: command can then be used to establish that the function is total. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "fun"} is a shorthand notation for ``@{command wenzelm@28760: (HOL) "function"}~@{text "(sequential)"}, followed by automated wenzelm@28760: proof attempts regarding pattern matching and termination. See wenzelm@28760: \cite{isabelle-function} for further details. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "termination"}~@{text f} commences a wenzelm@26849: termination proof for the previously defined function @{text f}. If wenzelm@26849: this is omitted, the command refers to the most recent function wenzelm@26849: definition. After the proof is closed, the recursive equations and wenzelm@26849: the induction principle is established. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: wenzelm@26849: %FIXME check wenzelm@26849: haftmann@27452: Recursive definitions introduced by the @{command (HOL) "function"} haftmann@27452: command accommodate wenzelm@26849: reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text wenzelm@26849: "c.induct"} (where @{text c} is the name of the function definition) wenzelm@26849: refers to a specific induction rule, with parameters named according haftmann@27452: to the user-specified equations. haftmann@27452: For the @{command (HOL) "primrec"} the induction principle coincides haftmann@27452: with structural recursion on the datatype the recursion is carried haftmann@27452: out. haftmann@27452: Case names of @{command (HOL) wenzelm@26849: "primrec"} are that of the datatypes involved, while those of wenzelm@26849: @{command (HOL) "function"} are numbered (starting from 1). wenzelm@26849: wenzelm@26849: The equations provided by these packages may be referred later as wenzelm@26849: theorem list @{text "f.simps"}, where @{text f} is the (collective) wenzelm@26849: name of the functions defined. Individual equations may be named wenzelm@26849: explicitly as well. wenzelm@26849: wenzelm@26849: The @{command (HOL) "function"} command accepts the following wenzelm@26849: options. wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{text sequential} enables a preprocessor which disambiguates wenzelm@28760: overlapping patterns by making them mutually disjoint. Earlier wenzelm@28760: equations take precedence over later ones. This allows to give the wenzelm@28760: specification in a format very similar to functional programming. wenzelm@28760: Note that the resulting simplification and induction rules wenzelm@28760: correspond to the transformed specification, not the one given wenzelm@26849: originally. This usually means that each equation given by the user wenzelm@26849: may result in several theroems. Also note that this automatic wenzelm@26849: transformation only works for ML-style datatype patterns. wenzelm@26849: wenzelm@28760: \item @{text domintros} enables the automated generation of wenzelm@26849: introduction rules for the domain predicate. While mostly not wenzelm@26849: needed, they can be helpful in some proofs about partial functions. wenzelm@26849: wenzelm@28760: \item @{text tailrec} generates the unconstrained recursive wenzelm@26849: equations even without a termination proof, provided that the wenzelm@26849: function is tail-recursive. This currently only works wenzelm@26849: wenzelm@28760: \item @{text "default d"} allows to specify a default value for a wenzelm@26849: (partial) function, which will ensure that @{text "f x = d x"} wenzelm@26849: whenever @{text "x \ f_dom"}. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Proof methods related to recursive definitions *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{method_def (HOL) pat_completeness} & : & @{text method} \\ wenzelm@28761: @{method_def (HOL) relation} & : & @{text method} \\ wenzelm@28761: @{method_def (HOL) lexicographic_order} & : & @{text method} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'relation' term wenzelm@26849: ; haftmann@31912: 'lexicographic\_order' ( clasimpmod * ) wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{method (HOL) pat_completeness} is a specialized method to wenzelm@26849: solve goals regarding the completeness of pattern matching, as wenzelm@26849: required by the @{command (HOL) "function"} package (cf.\ wenzelm@26849: \cite{isabelle-function}). wenzelm@26849: wenzelm@28760: \item @{method (HOL) relation}~@{text R} introduces a termination wenzelm@26849: proof using the relation @{text R}. The resulting proof state will wenzelm@26849: contain goals expressing that @{text R} is wellfounded, and that the wenzelm@26849: arguments of recursive calls decrease with respect to @{text R}. wenzelm@26849: Usually, this method is used as the initial proof step of manual wenzelm@26849: termination proofs. wenzelm@26849: wenzelm@28760: \item @{method (HOL) "lexicographic_order"} attempts a fully wenzelm@26849: automated termination proof by searching for a lexicographic wenzelm@26849: combination of size measures on the arguments of the function. The wenzelm@26849: method accepts the same arguments as the @{method auto} method, wenzelm@26849: which it uses internally to prove local descents. The same context wenzelm@26849: modifiers as for @{method auto} are accepted, see wenzelm@26849: \secref{sec:clasimp}. wenzelm@26849: wenzelm@26849: In case of failure, extensive information is printed, which can help wenzelm@26849: to analyse the situation (cf.\ \cite{isabelle-function}). wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Old-style recursive function definitions (TFL) *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: The old TFL commands @{command (HOL) "recdef"} and @{command (HOL) wenzelm@26849: "recdef_tc"} for defining recursive are mostly obsolete; @{command wenzelm@26849: (HOL) "function"} or @{command (HOL) "fun"} should be used instead. wenzelm@26849: wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "recdef"} & : & @{text "theory \ theory)"} \\ wenzelm@28761: @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \ proof(prove)"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints? wenzelm@26849: ; wenzelm@26849: recdeftc thmdecl? tc wenzelm@26849: ; haftmann@31912: hints: '(' 'hints' ( recdefmod * ) ')' wenzelm@26849: ; wenzelm@26849: recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod wenzelm@26849: ; wenzelm@26849: tc: nameref ('(' nat ')')? wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "recdef"} defines general well-founded wenzelm@26849: recursive functions (using the TFL package), see also wenzelm@26849: \cite{isabelle-HOL}. The ``@{text "(permissive)"}'' option tells wenzelm@26849: TFL to recover from failed proof attempts, returning unfinished wenzelm@26849: results. The @{text recdef_simp}, @{text recdef_cong}, and @{text wenzelm@26849: recdef_wf} hints refer to auxiliary rules to be used in the internal wenzelm@26849: automated proof process of TFL. Additional @{syntax clasimpmod} wenzelm@26849: declarations (cf.\ \secref{sec:clasimp}) may be given to tune the wenzelm@26849: context of the Simplifier (cf.\ \secref{sec:simplifier}) and wenzelm@26849: Classical reasoner (cf.\ \secref{sec:classical}). wenzelm@26849: wenzelm@28760: \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the wenzelm@26849: proof for leftover termination condition number @{text i} (default wenzelm@26849: 1) as generated by a @{command (HOL) "recdef"} definition of wenzelm@26849: constant @{text c}. wenzelm@26849: wenzelm@26849: Note that in most cases, @{command (HOL) "recdef"} is able to finish wenzelm@26849: its internal proofs without manual intervention. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: wenzelm@26849: \medskip Hints for @{command (HOL) "recdef"} may be also declared wenzelm@26849: globally, using the following attributes. wenzelm@26849: wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\ wenzelm@28761: @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\ wenzelm@28761: @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Inductive and coinductive definitions \label{sec:hol-inductive} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: An \textbf{inductive definition} specifies the least predicate (or wenzelm@26849: set) @{text R} closed under given rules: applying a rule to elements wenzelm@26849: of @{text R} yields a result within @{text R}. For example, a wenzelm@26849: structural operational semantics is an inductive definition of an wenzelm@26849: evaluation relation. wenzelm@26849: wenzelm@26849: Dually, a \textbf{coinductive definition} specifies the greatest wenzelm@26849: predicate~/ set @{text R} that is consistent with given rules: every wenzelm@26849: element of @{text R} can be seen as arising by applying a rule to wenzelm@26849: elements of @{text R}. An important example is using bisimulation wenzelm@26849: relations to formalise equivalence of processes and infinite data wenzelm@26849: structures. wenzelm@26849: wenzelm@26849: \medskip The HOL package is related to the ZF one, which is wenzelm@26849: described in a separate paper,\footnote{It appeared in CADE wenzelm@26849: \cite{paulson-CADE}; a longer version is distributed with Isabelle.} wenzelm@26849: which you should refer to in case of difficulties. The package is wenzelm@26849: simpler than that of ZF thanks to implicit type-checking in HOL. wenzelm@26849: The types of the (co)inductive predicates (or sets) determine the wenzelm@26849: domain of the fixedpoint definition, and the package does not have wenzelm@26849: to use inference rules for type-checking. wenzelm@26849: wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "inductive"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def (HOL) "coinductive"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@28761: @{attribute_def (HOL) mono} & : & @{text attribute} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\ wenzelm@26849: ('where' clauses)? ('monos' thmrefs)? wenzelm@26849: ; wenzelm@26849: clauses: (thmdecl? prop + '|') wenzelm@26849: ; wenzelm@26849: 'mono' (() | 'add' | 'del') wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "inductive"} and @{command (HOL) wenzelm@28760: "coinductive"} define (co)inductive predicates from the wenzelm@26849: introduction rules given in the @{keyword "where"} part. The wenzelm@26849: optional @{keyword "for"} part contains a list of parameters of the wenzelm@26849: (co)inductive predicates that remain fixed throughout the wenzelm@26849: definition. The optional @{keyword "monos"} section contains wenzelm@26849: \emph{monotonicity theorems}, which are required for each operator wenzelm@26849: applied to a recursive set in the introduction rules. There wenzelm@26849: \emph{must} be a theorem of the form @{text "A \ B \ M A \ M B"}, wenzelm@26849: for each premise @{text "M R\<^sub>i t"} in an introduction rule! wenzelm@26849: wenzelm@28760: \item @{command (HOL) "inductive_set"} and @{command (HOL) wenzelm@28760: "coinductive_set"} are wrappers for to the previous commands, wenzelm@26849: allowing the definition of (co)inductive sets. wenzelm@26849: wenzelm@28760: \item @{attribute (HOL) mono} declares monotonicity rules. These wenzelm@26849: rule are involved in the automated monotonicity proof of @{command wenzelm@26849: (HOL) "inductive"}. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Derived rules *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: Each (co)inductive definition @{text R} adds definitions to the wenzelm@26849: theory and also proves some theorems: wenzelm@26849: wenzelm@26849: \begin{description} wenzelm@26849: wenzelm@28760: \item @{text R.intros} is the list of introduction rules as proven wenzelm@26849: theorems, for the recursive predicates (or sets). The rules are wenzelm@26849: also available individually, using the names given them in the wenzelm@26849: theory file; wenzelm@26849: wenzelm@28760: \item @{text R.cases} is the case analysis (or elimination) rule; wenzelm@26849: wenzelm@28760: \item @{text R.induct} or @{text R.coinduct} is the (co)induction wenzelm@26849: rule. wenzelm@26849: wenzelm@26849: \end{description} wenzelm@26849: wenzelm@26849: When several predicates @{text "R\<^sub>1, \, R\<^sub>n"} are wenzelm@26849: defined simultaneously, the list of introduction rules is called wenzelm@26849: @{text "R\<^sub>1_\_R\<^sub>n.intros"}, the case analysis rules are wenzelm@26849: called @{text "R\<^sub>1.cases, \, R\<^sub>n.cases"}, and the list wenzelm@26849: of mutual induction rules is called @{text wenzelm@26849: "R\<^sub>1_\_R\<^sub>n.inducts"}. wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: subsection {* Monotonicity theorems *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: Each theory contains a default set of theorems that are used in wenzelm@26849: monotonicity proofs. New rules can be added to this set via the wenzelm@26849: @{attribute (HOL) mono} attribute. The HOL theory @{text Inductive} wenzelm@26849: shows how this is done. In general, the following monotonicity wenzelm@26849: theorems may be added: wenzelm@26849: wenzelm@26849: \begin{itemize} wenzelm@26849: wenzelm@26849: \item Theorems of the form @{text "A \ B \ M A \ M B"}, for proving wenzelm@26849: monotonicity of inductive definitions whose introduction rules have wenzelm@26849: premises involving terms such as @{text "M R\<^sub>i t"}. wenzelm@26849: wenzelm@26849: \item Monotonicity theorems for logical operators, which are of the wenzelm@26849: general form @{text "(\ \ \) \ \ (\ \ \) \ \ \ \"}. For example, in wenzelm@26849: the case of the operator @{text "\"}, the corresponding theorem is wenzelm@26849: \[ wenzelm@26849: \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"}} wenzelm@26849: \] wenzelm@26849: wenzelm@26849: \item De Morgan style equations for reasoning about the ``polarity'' wenzelm@26849: of expressions, e.g. wenzelm@26849: \[ wenzelm@26849: @{prop "\ \ P \ P"} \qquad\qquad wenzelm@26849: @{prop "\ (P \ Q) \ \ P \ \ Q"} wenzelm@26849: \] wenzelm@26849: wenzelm@26849: \item Equations for reducing complex operators to more primitive wenzelm@26849: ones whose monotonicity can easily be proved, e.g. wenzelm@26849: \[ wenzelm@26849: @{prop "(P \ Q) \ \ P \ Q"} \qquad\qquad wenzelm@26849: @{prop "Ball A P \ \x. x \ A \ P x"} wenzelm@26849: \] wenzelm@26849: wenzelm@26849: \end{itemize} wenzelm@26849: wenzelm@26849: %FIXME: Example of an inductive definition wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Arithmetic proof support *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{method_def (HOL) arith} & : & @{text method} \\ nipkow@30863: @{attribute_def (HOL) arith} & : & @{text attribute} \\ wenzelm@28761: @{attribute_def (HOL) arith_split} & : & @{text attribute} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: The @{method (HOL) arith} method decides linear arithmetic problems wenzelm@26849: (on types @{text nat}, @{text int}, @{text real}). Any current wenzelm@26849: facts are inserted into the goal before running the procedure. wenzelm@26849: nipkow@30863: The @{attribute (HOL) arith} attribute declares facts that are nipkow@30863: always supplied to the arithmetic provers implicitly. wenzelm@26849: nipkow@30863: The @{attribute (HOL) arith_split} attribute declares case split wenzelm@30865: rules to be expanded before @{method (HOL) arith} is invoked. nipkow@30863: nipkow@30863: Note that a simpler (but faster) arithmetic prover is nipkow@30863: already invoked by the Simplifier. wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@30169: section {* Intuitionistic proof search *} wenzelm@30169: wenzelm@30169: text {* wenzelm@30169: \begin{matharray}{rcl} wenzelm@30171: @{method_def (HOL) iprover} & : & @{text method} \\ wenzelm@30169: \end{matharray} wenzelm@30169: wenzelm@30169: \begin{rail} haftmann@31912: 'iprover' ('!' ?) ( rulemod * ) wenzelm@30169: ; wenzelm@30169: \end{rail} wenzelm@30169: wenzelm@30171: The @{method (HOL) iprover} method performs intuitionistic proof wenzelm@30171: search, depending on specifically declared rules from the context, wenzelm@30171: or given as explicit arguments. Chained facts are inserted into the wenzelm@30171: goal before commencing proof search; ``@{method (HOL) iprover}@{text wenzelm@30171: "!"}'' means to include the current @{fact prems} as well. wenzelm@30169: wenzelm@30169: Rules need to be classified as @{attribute (Pure) intro}, wenzelm@30169: @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the wenzelm@30169: ``@{text "!"}'' indicator refers to ``safe'' rules, which may be wenzelm@30169: applied aggressively (without considering back-tracking later). wenzelm@30169: Rules declared with ``@{text "?"}'' are ignored in proof search (the wenzelm@30169: single-step @{method rule} method still observes these). An wenzelm@30169: explicit weight annotation may be given as well; otherwise the wenzelm@30169: number of rule premises will be taken into account here. wenzelm@30169: *} wenzelm@30169: wenzelm@30169: wenzelm@30171: section {* Coherent Logic *} wenzelm@30171: wenzelm@30171: text {* wenzelm@30171: \begin{matharray}{rcl} wenzelm@30171: @{method_def (HOL) "coherent"} & : & @{text method} \\ wenzelm@30171: \end{matharray} wenzelm@30171: wenzelm@30171: \begin{rail} wenzelm@30171: 'coherent' thmrefs? wenzelm@30171: ; wenzelm@30171: \end{rail} wenzelm@30171: wenzelm@30171: The @{method (HOL) coherent} method solves problems of wenzelm@30171: \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers wenzelm@30171: applications in confluence theory, lattice theory and projective wenzelm@30171: geometry. See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some wenzelm@30171: examples. wenzelm@30171: *} wenzelm@30171: wenzelm@30171: haftmann@31912: section {* Checking and refuting propositions *} haftmann@31912: haftmann@31912: text {* haftmann@31912: Identifying incorrect propositions usually involves evaluation of haftmann@31912: particular assignments and systematic counter example search. This haftmann@31912: is supported by the following commands. haftmann@31912: haftmann@31912: \begin{matharray}{rcl} haftmann@31912: @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@31912: @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ haftmann@31912: @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \ theory"} haftmann@31912: \end{matharray} haftmann@31912: haftmann@31912: \begin{rail} haftmann@31912: 'value' ( ( '[' name ']' ) ? ) modes? term haftmann@31912: ; haftmann@31912: haftmann@31912: 'quickcheck' ( ( '[' args ']' ) ? ) nat? haftmann@31912: ; haftmann@31912: haftmann@31912: 'quickcheck_params' ( ( '[' args ']' ) ? ) haftmann@31912: ; haftmann@31912: haftmann@31912: modes: '(' (name + ) ')' haftmann@31912: ; haftmann@31912: haftmann@31912: args: ( name '=' value + ',' ) haftmann@31912: ; haftmann@31912: \end{rail} haftmann@31912: haftmann@31912: \begin{description} haftmann@31912: haftmann@31912: \item @{command (HOL) "value"}~@{text t} evaluates and prints a haftmann@31912: term; optionally @{text modes} can be specified, which are haftmann@31912: appended to the current print mode (see also \cite{isabelle-ref}). haftmann@31912: Internally, the evaluation is performed by registered evaluators, haftmann@31912: which are invoked sequentially until a result is returned. haftmann@31912: Alternatively a specific evaluator can be selected using square haftmann@31912: brackets; available evaluators include @{text nbe} for haftmann@31912: \emph{normalization by evaluation} and \emph{code} for code haftmann@31912: generation in SML. haftmann@31912: haftmann@31912: \item @{command (HOL) "quickcheck"} tests the current goal for haftmann@31912: counter examples using a series of arbitrary assignments for its haftmann@31912: free variables; by default the first subgoal is tested, an other haftmann@31912: can be selected explicitly using an optional goal index. haftmann@31912: A number of configuration options are supported for haftmann@31912: @{command (HOL) "quickcheck"}, notably: haftmann@31912: haftmann@31912: \begin{description} haftmann@31912: haftmann@31912: \item[size] specifies the maximum size of the search space for haftmann@31912: assignment values. haftmann@31912: haftmann@31912: \item[iterations] sets how many sets of assignments are haftmann@31912: generated for each particular size. haftmann@31912: haftmann@31912: \end{description} haftmann@31912: haftmann@31912: These option can be given within square brackets. haftmann@31912: haftmann@31912: \item @{command (HOL) "quickcheck_params"} changes quickcheck haftmann@31912: configuration options persitently. haftmann@31912: haftmann@31912: \end{description} haftmann@31912: *} haftmann@31912: haftmann@31912: wenzelm@28603: section {* Invoking automated reasoning tools -- The Sledgehammer *} wenzelm@28603: wenzelm@28603: text {* wenzelm@28603: Isabelle/HOL includes a generic \emph{ATP manager} that allows wenzelm@28603: external automated reasoning tools to crunch a pending goal. wenzelm@28603: Supported provers include E\footnote{\url{http://www.eprover.org}}, wenzelm@28603: SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire. wenzelm@28603: There is also a wrapper to invoke provers remotely via the wenzelm@28603: SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}} wenzelm@28603: web service. wenzelm@28603: wenzelm@28603: The problem passed to external provers consists of the goal together wenzelm@28603: with a smart selection of lemmas from the current theory context. wenzelm@28603: The result of a successful proof search is some source text that wenzelm@28603: usually reconstructs the proof within Isabelle, without requiring wenzelm@28603: external provers again. The Metis wenzelm@28603: prover\footnote{\url{http://www.gilith.com/software/metis/}} that is wenzelm@28603: integrated into Isabelle/HOL is being used here. wenzelm@28603: wenzelm@28603: In this mode of operation, heavy means of automated reasoning are wenzelm@28603: used as a strong relevance filter, while the main proof checking wenzelm@28603: works via explicit inferences going through the Isabelle kernel. wenzelm@28603: Moreover, rechecking Isabelle proof texts with already specified wenzelm@28603: auxiliary facts is much faster than performing fully automated wenzelm@28603: search over and over again. wenzelm@28603: wenzelm@28603: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "sledgehammer"}@{text "\<^sup>*"} & : & @{text "proof \"} \\ wenzelm@28761: @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ wenzelm@28761: @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \"} \\ wenzelm@28761: @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \"} \\ wenzelm@29112: @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \"} \\ wenzelm@28761: @{method_def (HOL) metis} & : & @{text method} \\ wenzelm@28603: \end{matharray} wenzelm@28603: wenzelm@28603: \begin{rail} haftmann@31912: 'sledgehammer' ( nameref * ) wenzelm@28603: ; wenzelm@29112: 'atp\_messages' ('(' nat ')')? wenzelm@29114: ; wenzelm@28603: wenzelm@28603: 'metis' thmrefs wenzelm@28603: ; wenzelm@28603: \end{rail} wenzelm@28603: wenzelm@28760: \begin{description} wenzelm@28603: wenzelm@28760: \item @{command (HOL) sledgehammer}~@{text "prover\<^sub>1 \ prover\<^sub>n"} wenzelm@28760: invokes the specified automated theorem provers on the first wenzelm@28760: subgoal. Provers are run in parallel, the first successful result wenzelm@28760: is displayed, and the other attempts are terminated. wenzelm@28603: wenzelm@28603: Provers are defined in the theory context, see also @{command (HOL) wenzelm@28603: print_atps}. If no provers are given as arguments to @{command wenzelm@28603: (HOL) sledgehammer}, the system refers to the default defined as wenzelm@28603: ``ATP provers'' preference by the user interface. wenzelm@28603: wenzelm@28603: There are additional preferences for timeout (default: 60 seconds), wenzelm@28603: and the maximum number of independent prover processes (default: 5); wenzelm@28603: excessive provers are automatically terminated. wenzelm@28603: wenzelm@28760: \item @{command (HOL) print_atps} prints the list of automated wenzelm@28603: theorem provers available to the @{command (HOL) sledgehammer} wenzelm@28603: command. wenzelm@28603: wenzelm@28760: \item @{command (HOL) atp_info} prints information about presently wenzelm@28603: running provers, including elapsed runtime, and the remaining time wenzelm@28603: until timeout. wenzelm@28603: wenzelm@28760: \item @{command (HOL) atp_kill} terminates all presently running wenzelm@28603: provers. wenzelm@28603: wenzelm@29112: \item @{command (HOL) atp_messages} displays recent messages issued wenzelm@29112: by automated theorem provers. This allows to examine results that wenzelm@29112: might have got lost due to the asynchronous nature of default wenzelm@29112: @{command (HOL) sledgehammer} output. An optional message limit may wenzelm@29112: be specified (default 5). wenzelm@29112: wenzelm@28760: \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover wenzelm@28760: with the given facts. Metis is an automated proof tool of medium wenzelm@28760: strength, but is fully integrated into Isabelle/HOL, with explicit wenzelm@28760: inferences going through the kernel. Thus its results are wenzelm@28603: guaranteed to be ``correct by construction''. wenzelm@28603: wenzelm@28603: Note that all facts used with Metis need to be specified as explicit wenzelm@28603: arguments. There are no rule declarations as for other Isabelle wenzelm@28603: provers, like @{method blast} or @{method fast}. wenzelm@28603: wenzelm@28760: \end{description} wenzelm@28603: *} wenzelm@28603: wenzelm@28603: wenzelm@28752: section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@27123: The following tools of Isabelle/HOL support cases analysis and wenzelm@27123: induction in unstructured tactic scripts; see also wenzelm@27123: \secref{sec:cases-induct} for proper Isar versions of similar ideas. wenzelm@26849: wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\ wenzelm@28761: @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\ wenzelm@28761: @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\ wenzelm@28761: @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \ local_theory"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'case\_tac' goalspec? term rule? wenzelm@26849: ; wenzelm@26849: 'induct\_tac' goalspec? (insts * 'and') rule? wenzelm@26849: ; wenzelm@26849: 'ind\_cases' (prop +) ('for' (name +)) ? wenzelm@26849: ; wenzelm@26849: 'inductive\_cases' (thmdecl? (prop +) + 'and') wenzelm@26849: ; wenzelm@26849: wenzelm@26849: rule: ('rule' ':' thmref) wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit wenzelm@28760: to reason about inductive types. Rules are selected according to wenzelm@28760: the declarations by the @{attribute cases} and @{attribute induct} wenzelm@28760: attributes, cf.\ \secref{sec:cases-induct}. The @{command (HOL) wenzelm@28760: datatype} package already takes care of this. wenzelm@27123: wenzelm@27123: These unstructured tactics feature both goal addressing and dynamic wenzelm@26849: instantiation. Note that named rule cases are \emph{not} provided wenzelm@27123: as would be by the proper @{method cases} and @{method induct} proof wenzelm@27123: methods (see \secref{sec:cases-induct}). Unlike the @{method wenzelm@27123: induct} method, @{method induct_tac} does not handle structured rule wenzelm@27123: statements, only the compact object-logic conclusion of the subgoal wenzelm@27123: being addressed. wenzelm@26849: wenzelm@28760: \item @{method (HOL) ind_cases} and @{command (HOL) wenzelm@28760: "inductive_cases"} provide an interface to the internal @{ML_text wenzelm@26860: mk_cases} operation. Rules are simplified in an unrestricted wenzelm@26860: forward manner. wenzelm@26849: wenzelm@26849: While @{method (HOL) ind_cases} is a proof method to apply the wenzelm@26849: result immediately as elimination rules, @{command (HOL) wenzelm@26849: "inductive_cases"} provides case split theorems at the theory level wenzelm@26849: for later use. The @{keyword "for"} argument of the @{method (HOL) wenzelm@26849: ind_cases} method allows to specify a list of variables that should wenzelm@26849: be generalized before applying the resulting rule. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@26849: wenzelm@26849: section {* Executable code *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: Isabelle/Pure provides two generic frameworks to support code wenzelm@26849: generation from executable specifications. Isabelle/HOL wenzelm@26849: instantiates these mechanisms in a way that is amenable to end-user wenzelm@26849: applications. wenzelm@26849: wenzelm@26849: One framework generates code from both functional and relational wenzelm@26849: programs to SML. See \cite{isabelle-HOL} for further information wenzelm@26849: (this actually covers the new-style theory format as well). wenzelm@26849: wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "code_module"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_library"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "consts_code"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "types_code"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{attribute_def (HOL) code} & : & @{text attribute} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: ( 'code\_module' | 'code\_library' ) modespec ? name ? \\ wenzelm@26849: ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ wenzelm@26849: 'contains' ( ( name '=' term ) + | term + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: modespec: '(' ( name * ) ')' wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'consts\_code' (codespec +) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: codespec: const template attachment ? wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'types\_code' (tycodespec +) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: tycodespec: name template attachment ? wenzelm@26849: ; wenzelm@26849: wenzelm@26849: const: term wenzelm@26849: ; wenzelm@26849: wenzelm@26849: template: '(' string ')' wenzelm@26849: ; wenzelm@26849: wenzelm@26849: attachment: 'attach' modespec ? verblbrace text verbrbrace wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code' (name)? wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@26849: \medskip The other framework generates code from functional programs wenzelm@26849: (including overloading using type classes) to SML \cite{SML}, OCaml wenzelm@26849: \cite{OCaml} and Haskell \cite{haskell-revised-report}. wenzelm@26849: Conceptually, code generation is split up in three steps: wenzelm@26849: \emph{selection} of code theorems, \emph{translation} into an wenzelm@26849: abstract executable view and \emph{serialization} to a specific wenzelm@26849: \emph{target language}. See \cite{isabelle-codegen} for an wenzelm@26849: introduction on how to use it. wenzelm@26849: wenzelm@26849: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \"} \\ wenzelm@28761: @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ wenzelm@28761: @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ wenzelm@28761: @{command_def (HOL) "code_datatype"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ wenzelm@28761: @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@31254: @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \"} \\ wenzelm@28761: @{attribute_def (HOL) code} & : & @{text attribute} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'export\_code' ( constexpr + ) ? \\ wenzelm@26849: ( ( 'in' target ( 'module\_name' string ) ? \\ wenzelm@26849: ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_thms' ( constexpr + ) ? wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_deps' ( constexpr + ) ? wenzelm@26849: ; wenzelm@26849: wenzelm@26849: const: term wenzelm@26849: ; wenzelm@26849: wenzelm@26849: constexpr: ( const | 'name.*' | '*' ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: typeconstructor: nameref wenzelm@26849: ; wenzelm@26849: wenzelm@26849: class: nameref wenzelm@26849: ; wenzelm@26849: wenzelm@26849: target: 'OCaml' | 'SML' | 'Haskell' wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_datatype' const + wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_const' (const + 'and') \\ wenzelm@26849: ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_type' (typeconstructor + 'and') \\ wenzelm@26849: ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_class' (class + 'and') \\ haftmann@28687: ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_instance' (( typeconstructor '::' class ) + 'and') \\ wenzelm@26849: ( ( '(' target ( '-' ? + 'and' ) ')' ) + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_monad' const const target wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_reserved' target ( string + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_include' target ( string ( string | '-') ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: 'code\_modulename' target ( ( string string ) + ) wenzelm@26849: ; wenzelm@26849: haftmann@27452: 'code\_abort' ( const + ) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string wenzelm@26849: ; wenzelm@26849: haftmann@31998: 'code' ( 'del' ) ? haftmann@31998: ; haftmann@31998: haftmann@31998: 'code_unfold' ( 'del' ) ? haftmann@31998: ; haftmann@31998: haftmann@31998: 'code_post' ( 'del' ) ? wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@28760: \item @{command (HOL) "export_code"} is the canonical interface for wenzelm@28760: generating and serializing code: for a given list of constants, code wenzelm@28760: is generated for the specified target languages. Abstract code is wenzelm@28760: cached incrementally. If no constant is given, the currently cached wenzelm@28760: code is serialized. If no serialization instruction is given, only wenzelm@28760: abstract code is cached. wenzelm@26849: wenzelm@26849: Constants may be specified by giving them literally, referring to wenzelm@26849: all executable contants within a certain theory by giving @{text wenzelm@26849: "name.*"}, or referring to \emph{all} executable constants currently wenzelm@26849: available by giving @{text "*"}. wenzelm@26849: wenzelm@26849: By default, for each involved theory one corresponding name space wenzelm@26849: module is generated. Alternativly, a module name may be specified wenzelm@26849: after the @{keyword "module_name"} keyword; then \emph{all} code is wenzelm@26849: placed in this module. wenzelm@26849: wenzelm@26849: For \emph{SML} and \emph{OCaml}, the file specification refers to a wenzelm@26849: single file; for \emph{Haskell}, it refers to a whole directory, wenzelm@26849: where code is generated in multiple files reflecting the module wenzelm@26849: hierarchy. The file specification ``@{text "-"}'' denotes standard wenzelm@26849: output. For \emph{SML}, omitting the file specification compiles wenzelm@26849: code internally in the context of the current ML session. wenzelm@26849: wenzelm@26849: Serializers take an optional list of arguments in parentheses. For wenzelm@26849: \emph{Haskell} a module name prefix may be given using the ``@{text wenzelm@26849: "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim wenzelm@26849: "deriving (Read, Show)"}'' clause to each appropriate datatype wenzelm@26849: declaration. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_thms"} prints a list of theorems wenzelm@26849: representing the corresponding program containing all given wenzelm@26849: constants; if no constants are given, the currently cached code wenzelm@26849: theorems are printed. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_deps"} visualizes dependencies of wenzelm@26849: theorems representing the corresponding program containing all given wenzelm@26849: constants; if no constants are given, the currently cached code wenzelm@26849: theorems are visualized. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_datatype"} specifies a constructor set wenzelm@26849: for a logical type. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_const"} associates a list of constants wenzelm@26849: with target-specific serializations; omitting a serialization wenzelm@26849: deletes an existing serialization. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_type"} associates a list of type wenzelm@26849: constructors with target-specific serializations; omitting a wenzelm@26849: serialization deletes an existing serialization. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_class"} associates a list of classes wenzelm@28760: with target-specific class names; omitting a serialization deletes wenzelm@28760: an existing serialization. This applies only to \emph{Haskell}. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_instance"} declares a list of type wenzelm@26849: constructor / class instance relations as ``already present'' for a wenzelm@26849: given target. Omitting a ``@{text "-"}'' deletes an existing wenzelm@26849: ``already present'' declaration. This applies only to wenzelm@26849: \emph{Haskell}. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_monad"} provides an auxiliary mechanism wenzelm@28760: to generate monadic code for Haskell. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_reserved"} declares a list of names as wenzelm@26849: reserved for a given target, preventing it to be shadowed by any wenzelm@26849: generated code. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_include"} adds arbitrary named content haftmann@27706: (``include'') to generated code. A ``@{text "-"}'' as last argument wenzelm@26849: will remove an already added ``include''. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_modulename"} declares aliasings from one wenzelm@28760: module name onto another. wenzelm@26849: wenzelm@28760: \item @{command (HOL) "code_abort"} declares constants which are not haftmann@29560: required to have a definition by means of code equations; if wenzelm@28760: needed these are implemented by program abort instead. wenzelm@26849: wenzelm@28760: \item @{attribute (HOL) code} explicitly selects (or with option haftmann@29560: ``@{text "del"}'' deselects) a code equation for code haftmann@29560: generation. Usually packages introducing code equations provide wenzelm@28760: a reasonable default setup for selection. wenzelm@26849: haftmann@31998: \item @{attribute (HOL) code_inline} declares (or with haftmann@28562: option ``@{text "del"}'' removes) inlining theorems which are haftmann@29560: applied as rewrite rules to any code equation during wenzelm@26849: preprocessing. wenzelm@26849: haftmann@31998: \item @{attribute (HOL) code_post} declares (or with haftmann@31998: option ``@{text "del"}'' removes) theorems which are haftmann@31998: applied as rewrite rules to any result of an evaluation. haftmann@31998: wenzelm@28760: \item @{command (HOL) "print_codesetup"} gives an overview on haftmann@31254: selected code equations and code generator datatypes. haftmann@31254: haftmann@31254: \item @{command (HOL) "print_codeproc"} prints the setup haftmann@31254: of the code generator preprocessor. wenzelm@26849: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: wenzelm@27045: wenzelm@27045: section {* Definition by specification \label{sec:hol-specification} *} wenzelm@27045: wenzelm@27045: text {* wenzelm@27045: \begin{matharray}{rcl} wenzelm@28761: @{command_def (HOL) "specification"} & : & @{text "theory \ proof(prove)"} \\ wenzelm@28761: @{command_def (HOL) "ax_specification"} & : & @{text "theory \ proof(prove)"} \\ wenzelm@27045: \end{matharray} wenzelm@27045: wenzelm@27045: \begin{rail} wenzelm@27045: ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) wenzelm@27045: ; wenzelm@27045: decl: ((name ':')? term '(' 'overloaded' ')'?) wenzelm@27045: \end{rail} wenzelm@27045: wenzelm@28760: \begin{description} wenzelm@27045: wenzelm@28760: \item @{command (HOL) "specification"}~@{text "decls \"} sets up a wenzelm@27045: goal stating the existence of terms with the properties specified to wenzelm@27045: hold for the constants given in @{text decls}. After finishing the wenzelm@27045: proof, the theory will be augmented with definitions for the given wenzelm@27045: constants, as well as with theorems stating the properties for these wenzelm@27045: constants. wenzelm@27045: wenzelm@28760: \item @{command (HOL) "ax_specification"}~@{text "decls \"} sets up wenzelm@28760: a goal stating the existence of terms with the properties specified wenzelm@28760: to hold for the constants given in @{text decls}. After finishing wenzelm@28760: the proof, the theory will be augmented with axioms expressing the wenzelm@28760: properties given in the first place. wenzelm@27045: wenzelm@28760: \item @{text decl} declares a constant to be defined by the wenzelm@27045: specification given. The definition for the constant @{text c} is wenzelm@27045: bound to the name @{text c_def} unless a theorem name is given in wenzelm@27045: the declaration. Overloaded constants should be declared as such. wenzelm@27045: wenzelm@28760: \end{description} wenzelm@27045: wenzelm@27045: Whether to use @{command (HOL) "specification"} or @{command (HOL) wenzelm@27045: "ax_specification"} is to some extent a matter of style. @{command wenzelm@27045: (HOL) "specification"} introduces no new axioms, and so by wenzelm@27045: construction cannot introduce inconsistencies, whereas @{command wenzelm@27045: (HOL) "ax_specification"} does introduce axioms, but only after the wenzelm@27045: user has explicitly proven it to be safe. A practical issue must be wenzelm@27045: considered, though: After introducing two constants with the same wenzelm@27045: properties using @{command (HOL) "specification"}, one can prove wenzelm@27045: that the two constants are, in fact, equal. If this might be a wenzelm@27045: problem, one should use @{command (HOL) "ax_specification"}. wenzelm@27045: *} wenzelm@27045: wenzelm@26840: end