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@35744: section {* Typedef axiomatization \label{sec:hol-typedef} *} wenzelm@26849: wenzelm@26849: text {* wenzelm@26849: \begin{matharray}{rcl} wenzelm@35744: @{command_def (HOL) "typedef"} & : & @{text "local_theory \ proof(prove)"} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'typedef' altname? abstype '=' repset wenzelm@26849: ; wenzelm@26849: wenzelm@26849: altname: '(' (name | 'open' | 'open' name) ')' wenzelm@26849: ; wenzelm@35841: abstype: typespecsorts mixfix? wenzelm@26849: ; wenzelm@26849: repset: term ('morphisms' name name)? wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: wenzelm@35744: \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} wenzelm@35744: axiomatizes a Gordon/HOL-style type definition in the background wenzelm@35744: theory of the current context, depending on a non-emptiness result wenzelm@35744: of the set @{text A} (which needs to be proven interactively). wenzelm@35744: wenzelm@35744: The raw type may not depend on parameters or assumptions of the wenzelm@35744: context --- this is logically impossible in Isabelle/HOL --- but the wenzelm@35744: non-emptiness property can be local, potentially resulting in wenzelm@35744: multiple interpretations in target contexts. Thus the established wenzelm@35744: bijection between the representing set @{text A} and the new type wenzelm@35744: @{text t} may semantically depend on local assumptions. wenzelm@26849: wenzelm@35744: By default, @{command (HOL) "typedef"} defines both a type @{text t} wenzelm@35744: and a set (term constant) of the same name, unless an alternative wenzelm@35744: base name is given in parentheses, or the ``@{text "(open)"}'' wenzelm@35744: declaration is used to suppress a separate constant definition wenzelm@35744: altogether. The injection from type to set is called @{text Rep_t}, wenzelm@35744: its inverse @{text Abs_t} --- this may be changed via an explicit wenzelm@35744: @{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@35744: An alternative name for the set definition (and other derived wenzelm@35744: entities) may be specified in parentheses; the default is to use wenzelm@35744: @{text t} as indicated before. wenzelm@26849: wenzelm@28760: \end{description} 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} krauss@40388: 'split_format' '(' 'complete' ')' wenzelm@26849: ; wenzelm@26849: \end{rail} wenzelm@26849: wenzelm@28760: \begin{description} wenzelm@26849: krauss@40388: \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes wenzelm@28760: arguments in function applications to be represented canonically wenzelm@28760: according to their tuple type structure. wenzelm@26849: krauss@40388: Note that this operation tends to invent funny names for new local krauss@40388: parameters 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@36158: 'record' typespecsorts '=' (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: ; wenzelm@40255: 'rep_datatype' ('(' (name +) ')')? (term +) wenzelm@26849: ; wenzelm@26849: wenzelm@35351: dtspec: parname? typespec mixfix? '=' (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: ; krauss@40170: ('fun' | 'function') target? functionopts? fixes \\ 'where' equations wenzelm@26849: ; krauss@40170: equations: (thmdecl? prop + '|') 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: 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 krauss@33857: to the user-specified equations. Cases are numbered (starting from 1). krauss@33857: krauss@33857: For @{command (HOL) "primrec"}, the induction principle coincides haftmann@27452: with structural recursion on the datatype the recursion is carried haftmann@27452: out. 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 hoelzl@36139: may result in several theorems. 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} \\ krauss@33858: @{method_def (HOL) size_change} & : & @{text method} \\ wenzelm@26849: \end{matharray} wenzelm@26849: wenzelm@26849: \begin{rail} wenzelm@26849: 'relation' term wenzelm@26849: ; wenzelm@40255: 'lexicographic_order' ( clasimpmod * ) wenzelm@26849: ; wenzelm@40255: 'size_change' ( orders ( clasimpmod * ) ) krauss@33858: ; krauss@33858: orders: ( 'max' | 'min' | 'ms' ) * 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: krauss@33858: \item @{method (HOL) "size_change"} also works on termination goals, krauss@33858: using a variation of the size-change principle, together with a krauss@33858: graph decomposition technique (see \cite{krauss_phd} for details). krauss@33858: Three kinds of orders are used internally: @{text max}, @{text min}, krauss@33858: and @{text ms} (multiset), which is only available when the theory krauss@33858: @{text Multiset} is loaded. When no order kinds are given, they are krauss@33858: tried in order. The search for a termination proof uses SAT solving krauss@33858: internally. krauss@33858: krauss@33858: For local descent proofs, the same context modifiers as for @{method krauss@33858: auto} are accepted, see \secref{sec:clasimp}. krauss@33858: wenzelm@28760: \end{description} wenzelm@26849: *} wenzelm@26849: krauss@40171: subsection {* Functions with explicit partiality *} krauss@40171: krauss@40171: text {* krauss@40171: \begin{matharray}{rcl} krauss@40171: @{command_def (HOL) "partial_function"} & : & @{text "local_theory \ local_theory"} \\ krauss@40171: @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\ krauss@40171: \end{matharray} krauss@40171: krauss@40171: \begin{rail} krauss@40171: 'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop krauss@40171: \end{rail} krauss@40171: krauss@40171: \begin{description} krauss@40171: krauss@40171: \item @{command (HOL) "partial_function"} defines recursive krauss@40171: functions based on fixpoints in complete partial orders. No krauss@40171: termination proof is required from the user or constructed krauss@40171: internally. Instead, the possibility of non-termination is modelled krauss@40171: explicitly in the result type, which contains an explicit bottom krauss@40171: element. krauss@40171: krauss@40171: Pattern matching and mutual recursion are currently not supported. krauss@40171: Thus, the specification consists of a single function described by a krauss@40171: single recursive equation. krauss@40171: krauss@40171: There are no fixed syntactic restrictions on the body of the krauss@40171: function, but the induced functional must be provably monotonic krauss@40171: wrt.\ the underlying order. The monotonicitity proof is performed krauss@40171: internally, and the definition is rejected when it fails. The proof krauss@40171: can be influenced by declaring hints using the krauss@40171: @{attribute (HOL) partial_function_mono} attribute. krauss@40171: krauss@40171: The mandatory @{text mode} argument specifies the mode of operation krauss@40171: of the command, which directly corresponds to a complete partial krauss@40171: order on the result type. By default, the following modes are krauss@40171: defined: krauss@40171: krauss@40171: \begin{description} krauss@40171: \item @{text option} defines functions that map into the @{type krauss@40171: option} type. Here, the value @{term None} is used to model a krauss@40171: non-terminating computation. Monotonicity requires that if @{term krauss@40171: None} is returned by a recursive call, then the overall result krauss@40171: must also be @{term None}. This is best achieved through the use of krauss@40171: the monadic operator @{const "Option.bind"}. krauss@40171: krauss@40171: \item @{text tailrec} defines functions with an arbitrary result krauss@40171: type and uses the slightly degenerated partial order where @{term krauss@40171: "undefined"} is the bottom element. Now, monotonicity requires that krauss@40171: if @{term undefined} is returned by a recursive call, then the krauss@40171: overall result must also be @{term undefined}. In practice, this is krauss@40171: only satisfied when each recursive call is a tail call, whose result krauss@40171: is directly returned. Thus, this mode of operation allows the krauss@40171: definition of arbitrary tail-recursive functions. krauss@40171: \end{description} krauss@40171: krauss@40171: Experienced users may define new modes by instantiating the locale krauss@40171: @{const "partial_function_definitions"} appropriately. krauss@40171: krauss@40171: \item @{attribute (HOL) partial_function_mono} declares rules for krauss@40171: use in the internal monononicity proofs of partial function krauss@40171: definitions. krauss@40171: krauss@40171: \end{description} krauss@40171: krauss@40171: *} 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@40255: 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@40255: ('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@40255: ('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} wenzelm@35613: '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@35613: goal before commencing proof search. wenzelm@35613: 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@37444: brackets; typical evaluators use the current set of code equations haftmann@37444: to normalize and include @{text simp} for fully symbolic evaluation haftmann@37444: using the simplifier, @{text nbe} for \emph{normalization by evaluation} haftmann@37444: and \emph{code} for code 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: wenzelm@40254: \item[@{text size}] specifies the maximum size of the search space wenzelm@40254: for assignment values. haftmann@31912: wenzelm@40254: \item[@{text iterations}] sets how many sets of assignments are wenzelm@40254: generated for each particular size. haftmann@31912: wenzelm@40254: \item[@{text no_assms}] specifies whether assumptions in wenzelm@40254: structured proofs should be ignored. blanchet@35331: wenzelm@40254: \item[@{text timeout}] sets the time limit in seconds. bulwahn@40245: wenzelm@40254: \item[@{text default_type}] sets the type(s) generally used to wenzelm@40254: instantiate type variables. bulwahn@40245: wenzelm@40254: \item[@{text report}] if set quickcheck reports how many tests wenzelm@40254: fulfilled the preconditions. bulwahn@40245: wenzelm@40254: \item[@{text quiet}] if not set quickcheck informs about the wenzelm@40254: current size for assignment values. bulwahn@40245: wenzelm@40254: \item[@{text expect}] can be used to check if the user's wenzelm@40254: expectation was met (@{text no_expectation}, @{text wenzelm@40254: no_counterexample}, or @{text counterexample}). bulwahn@40245: 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@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@40255: 'case_tac' goalspec? term rule? wenzelm@26849: ; wenzelm@40255: 'induct_tac' goalspec? (insts * 'and') rule? wenzelm@26849: ; wenzelm@40255: 'ind_cases' (prop +) ('for' (name +)) ? wenzelm@26849: ; wenzelm@40255: '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: haftmann@37422: \medskip One framework generates code from functional programs haftmann@37422: (including overloading using type classes) to SML \cite{SML}, OCaml haftmann@38814: \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala haftmann@38814: \cite{scala-overview-tech-report}. haftmann@37422: Conceptually, code generation is split up in three steps: haftmann@37422: \emph{selection} of code theorems, \emph{translation} into an haftmann@37422: abstract executable view and \emph{serialization} to a specific haftmann@37422: \emph{target language}. Inductive specifications can be executed haftmann@37422: using the predicate compiler which operates within HOL. haftmann@37422: See \cite{isabelle-codegen} for an introduction. haftmann@37422: haftmann@37422: \begin{matharray}{rcl} haftmann@37422: @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@37422: @{attribute_def (HOL) code} & : & @{text attribute} \\ haftmann@37422: @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_datatype"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@37422: @{attribute_def (HOL) code_inline} & : & @{text attribute} \\ haftmann@37422: @{attribute_def (HOL) code_post} & : & @{text attribute} \\ haftmann@37422: @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@37422: @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@37422: @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ haftmann@37422: @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ haftmann@37422: @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ haftmann@39608: @{command_def (HOL) "code_reflect"} & : & @{text "theory \ theory"} haftmann@37422: \end{matharray} haftmann@37422: haftmann@37422: \begin{rail} wenzelm@40255: 'export_code' ( constexpr + ) \\ wenzelm@40255: ( ( 'in' target ( 'module_name' string ) ? \\ haftmann@37820: ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ? haftmann@37422: ; haftmann@37422: haftmann@37422: const: term haftmann@37422: ; haftmann@37422: haftmann@37422: constexpr: ( const | 'name.*' | '*' ) haftmann@37422: ; haftmann@37422: haftmann@37422: typeconstructor: nameref haftmann@37422: ; haftmann@37422: haftmann@37422: class: nameref haftmann@37422: ; haftmann@37422: haftmann@38814: target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' haftmann@37422: ; haftmann@37422: haftmann@38462: 'code' ( 'del' | 'abstype' | 'abstract' ) ? haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_abort' ( const + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_datatype' ( const + ) haftmann@37422: ; haftmann@37422: haftmann@37422: 'code_inline' ( 'del' ) ? haftmann@37422: ; haftmann@37422: haftmann@37422: 'code_post' ( 'del' ) ? haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_thms' ( constexpr + ) ? haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_deps' ( constexpr + ) ? haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_const' (const + 'and') \\ haftmann@37422: ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_type' (typeconstructor + 'and') \\ haftmann@37422: ( ( '(' target ( syntax ? + 'and' ) ')' ) + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_class' (class + 'and') \\ haftmann@37422: ( ( '(' target \\ ( string ? + 'and' ) ')' ) + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_instance' (( typeconstructor '::' class ) + 'and') \\ haftmann@37422: ( ( '(' target ( '-' ? + 'and' ) ')' ) + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_reserved' target ( string + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_monad' const const target haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_include' target ( string ( string | '-') ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_modulename' target ( ( string string ) + ) haftmann@37422: ; haftmann@37422: wenzelm@40255: 'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\ haftmann@39608: ( 'functions' ( string + ) ) ? ( 'file' string ) ? haftmann@39608: ; haftmann@39608: haftmann@37422: syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string haftmann@37422: ; haftmann@37422: haftmann@37422: \end{rail} haftmann@37422: haftmann@37422: \begin{description} haftmann@37422: haftmann@37422: \item @{command (HOL) "export_code"} generates code for a given list haftmann@39608: of constants in the specified target language(s). If no haftmann@39608: serialization instruction is given, only abstract code is generated haftmann@39608: internally. haftmann@37422: haftmann@37422: Constants may be specified by giving them literally, referring to haftmann@37422: all executable contants within a certain theory by giving @{text haftmann@37422: "name.*"}, or referring to \emph{all} executable constants currently haftmann@37422: available by giving @{text "*"}. haftmann@37422: haftmann@37422: By default, for each involved theory one corresponding name space haftmann@37422: module is generated. Alternativly, a module name may be specified haftmann@37422: after the @{keyword "module_name"} keyword; then \emph{all} code is haftmann@37422: placed in this module. haftmann@37422: haftmann@39608: For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification haftmann@39608: refers to a single file; for \emph{Haskell}, it refers to a whole haftmann@39608: directory, where code is generated in multiple files reflecting the haftmann@39608: module hierarchy. Omitting the file specification denotes standard haftmann@37749: output. haftmann@37422: haftmann@37422: Serializers take an optional list of arguments in parentheses. For haftmann@37422: \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits haftmann@37422: explicit module signatures. haftmann@37422: haftmann@39608: For \emph{Haskell} a module name prefix may be given using the haftmann@39608: ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a haftmann@39608: ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate haftmann@39608: datatype declaration. haftmann@37422: haftmann@37422: \item @{attribute (HOL) code} explicitly selects (or with option haftmann@38462: ``@{text "del"}'' deselects) a code equation for code generation. haftmann@38462: Usually packages introducing code equations provide a reasonable haftmann@38462: default setup for selection. Variants @{text "code abstype"} and haftmann@38462: @{text "code abstract"} declare abstract datatype certificates or haftmann@38462: code equations on abstract datatype representations respectively. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_abort"} declares constants which are not haftmann@39608: required to have a definition by means of code equations; if needed haftmann@39608: these are implemented by program abort instead. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_datatype"} specifies a constructor set haftmann@37422: for a logical type. haftmann@37422: haftmann@37422: \item @{command (HOL) "print_codesetup"} gives an overview on haftmann@37422: selected code equations and code generator datatypes. haftmann@37422: haftmann@39608: \item @{attribute (HOL) code_inline} declares (or with option haftmann@39608: ``@{text "del"}'' removes) inlining theorems which are applied as haftmann@39608: rewrite rules to any code equation during preprocessing. haftmann@37422: haftmann@39608: \item @{attribute (HOL) code_post} declares (or with option ``@{text haftmann@39608: "del"}'' removes) theorems which are applied as rewrite rules to any haftmann@39608: result of an evaluation. haftmann@37422: haftmann@39608: \item @{command (HOL) "print_codeproc"} prints the setup of the code haftmann@39608: generator preprocessor. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_thms"} prints a list of theorems haftmann@37422: representing the corresponding program containing all given haftmann@37422: constants after preprocessing. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_deps"} visualizes dependencies of haftmann@37422: theorems representing the corresponding program containing all given haftmann@37422: constants after preprocessing. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_const"} associates a list of constants haftmann@37422: with target-specific serializations; omitting a serialization haftmann@37422: deletes an existing serialization. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_type"} associates a list of type haftmann@37422: constructors with target-specific serializations; omitting a haftmann@37422: serialization deletes an existing serialization. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_class"} associates a list of classes haftmann@37422: with target-specific class names; omitting a serialization deletes haftmann@37422: an existing serialization. This applies only to \emph{Haskell}. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_instance"} declares a list of type haftmann@37422: constructor / class instance relations as ``already present'' for a haftmann@37422: given target. Omitting a ``@{text "-"}'' deletes an existing haftmann@37422: ``already present'' declaration. This applies only to haftmann@37422: \emph{Haskell}. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_reserved"} declares a list of names as haftmann@37422: reserved for a given target, preventing it to be shadowed by any haftmann@37422: generated code. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_monad"} provides an auxiliary mechanism haftmann@37422: to generate monadic code for Haskell. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_include"} adds arbitrary named content haftmann@37422: (``include'') to generated code. A ``@{text "-"}'' as last argument haftmann@37422: will remove an already added ``include''. haftmann@37422: haftmann@37422: \item @{command (HOL) "code_modulename"} declares aliasings from one haftmann@37422: module name onto another. haftmann@37422: haftmann@39608: \item @{command (HOL) "code_reflect"} without a ``@{text "file"}'' haftmann@39608: argument compiles code into the system runtime environment and haftmann@39608: modifies the code generator setup that future invocations of system haftmann@39608: runtime code generation referring to one of the ``@{text haftmann@39608: "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled haftmann@39608: entities. With a ``@{text "file"}'' argument, the corresponding code haftmann@39608: is generated into that specified file without modifying the code haftmann@39608: generator setup. haftmann@39608: haftmann@37422: \end{description} haftmann@37422: haftmann@39608: The other framework generates code from both functional and haftmann@39608: relational programs to SML. See \cite{isabelle-HOL} for further haftmann@39608: information (this actually covers the new-style theory format as haftmann@39608: 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@40255: ( '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@40255: 'consts_code' (codespec +) wenzelm@26849: ; wenzelm@26849: wenzelm@26849: codespec: const template attachment ? wenzelm@26849: ; wenzelm@26849: wenzelm@40255: '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: *} 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@40255: ('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