# HG changeset patch # User wenzelm # Date 1404299167 -7200 # Node ID 7806a74c54ac165237abd86f41c4176433803c89 # Parent 2131b6633529dba36c88918163d879b4df1bac0d misc tuning and clarification; diff -r 2131b6633529 -r 7806a74c54ac src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Jul 02 12:12:26 2014 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Wed Jul 02 13:06:07 2014 +0200 @@ -1087,7 +1087,7 @@ \begin{description} \item @{command (HOL) "typedef"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = A"} produces an - axiomatization (\secref{sec:basic-spec}) for a type definition in the + axiomatization (\secref{sec:axiomatizations}) for a type definition in the background theory of the current context, depending on a non-emptiness result of the set @{text A} that needs to be proven here. The set @{text A} may contain type variables @{text "\\<^sub>1, \, \\<^sub>n"} as specified on the @@ -1132,16 +1132,6 @@ respectively. \end{description} - - \begin{warn} - If you introduce a new type axiomatically, i.e.\ via @{command_ref - typedecl} and @{command_ref axiomatization}, the minimum requirement - is that it has a non-empty model, to avoid immediate collapse of the - HOL logic. Moreover, one needs to demonstrate that the - interpretation of such free-form axiomatizations can coexist with - that of the regular @{command_def typedef} scheme, and any extension - that other people might have introduced elsewhere. - \end{warn} *} subsubsection {* Examples *} diff -r 2131b6633529 -r 7806a74c54ac src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Wed Jul 02 12:12:26 2014 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Wed Jul 02 13:06:07 2014 +0200 @@ -257,11 +257,10 @@ including trace by metis -section {* Basic specification elements \label{sec:basic-spec} *} +section {* Term definitions \label{sec:term-definitions} *} text {* \begin{matharray}{rcll} - @{command_def "axiomatization"} & : & @{text "theory \ theory"} & (axiomatic!) \\ @{command_def "definition"} & : & @{text "local_theory \ local_theory"} \\ @{attribute_def "defn"} & : & @{text attribute} \\ @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ @@ -269,14 +268,12 @@ @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \ "} \\ \end{matharray} - These specification mechanisms provide a slightly more abstract view - than the underlying primitives of @{command "consts"}, @{command - "defs"} (see \secref{sec:consts}), and raw axioms. In particular, - type-inference covers the whole specification as usual. + Term definitions may either happen within the logic (as equational axioms + of a certain form, see also see \secref{sec:consts}), or outside of it as + rewrite system on abstract syntax. The second form is called + ``abbreviation''. @{rail \ - @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)? - ; @@{command definition} @{syntax target}? \ (decl @'where')? @{syntax thmdecl}? @{syntax prop} ; @@ -284,32 +281,11 @@ (decl @'where')? @{syntax prop} ; - @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})? - @{syntax mixfix}? | @{syntax vars}) + @'and') - ; - specs: (@{syntax thmdecl}? @{syntax props} + @'and') - ; decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? \} \begin{description} - \item @{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m \ \\<^sub>1 \ \\<^sub>n"} - introduces several constants simultaneously and states axiomatic - properties for these. The constants are marked as being specified - once and for all, which prevents additional specifications being - issued later on. - - Axiomatic specifications are required when declaring a new logical system - within Isabelle/Pure, but in an application environment like - Isabelle/HOL the user normally stays within definitional mechanisms - provided by the logic and its libraries. - - Axiomatization is restricted to a global theory context. Despite the - possibility to mark some constants as specified by a particular - axiomatization, the dependency tracking may be insufficient and disrupt - the well-formedness of an otherwise definitional theory. - \item @{command "definition"}~@{text "c \ eq"} produces an internal definition @{text "c \ t"} according to the specification given as @{text eq}, which is then turned into a proven fact. The @@ -351,6 +327,48 @@ *} +section {* Axiomatizations \label{sec:axiomatizations} *} + +text {* + \begin{matharray}{rcll} + @{command_def "axiomatization"} & : & @{text "theory \ theory"} & (axiomatic!) \\ + \end{matharray} + + @{rail \ + @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)? + ; + + @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})? + @{syntax mixfix}? | @{syntax vars}) + @'and') + ; + specs: (@{syntax thmdecl}? @{syntax props} + @'and') + \} + + \begin{description} + + \item @{command "axiomatization"}~@{text "c\<^sub>1 \ c\<^sub>m \ \\<^sub>1 \ \\<^sub>n"} + introduces several constants simultaneously and states axiomatic + properties for these. The constants are marked as being specified once and + for all, which prevents additional specifications for the same constants + later on, but it is always possible do emit axiomatizations without + referring to particular constants. Note that lack of precise dependency + tracking of axiomatizations may disrupt the well-formedness of an + otherwise definitional theory. + + Axiomatization is restricted to a global theory context: support for local + theory targets \secref{sec:target} would introduce an extra dimension of + uncertainty what the written specifications really are, and make it + infeasible to argue why they are correct. + + Axiomatic specifications are required when declaring a new logical system + within Isabelle/Pure, but in an application environment like Isabelle/HOL + the user normally stays within definitional mechanisms provided by the + logic and its libraries. + + \end{description} +*} + + section {* Generic declarations *} text {* @@ -563,7 +581,7 @@ Both @{element "assumes"} and @{element "defines"} elements contribute to the locale specification. When defining an operation derived from the parameters, @{command "definition"} - (\secref{sec:basic-spec}) is usually more appropriate. + (\secref{sec:term-definitions}) is usually more appropriate. Note that ``@{text "(\ p\<^sub>1 \ p\<^sub>n)"}'' patterns given in the syntax of @{element "assumes"} and @{element "defines"} above @@ -1161,7 +1179,7 @@ *} -subsection {* Types and type abbreviations \label{sec:types-pure} *} +subsection {* Types \label{sec:types-pure} *} text {* \begin{matharray}{rcll} @@ -1177,11 +1195,10 @@ \begin{description} - \item @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} - introduces a \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the - existing type @{text "\"}. Unlike actual type definitions, as are - available in Isabelle/HOL for example, type synonyms are merely - syntactic abbreviations without any logical significance. + \item @{command "type_synonym"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"} introduces a + \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} for the existing type @{text + "\"}. Unlike the semantic type definitions in Isabelle/HOL, type synonyms + are merely syntactic abbreviations without any logical significance. Internally, type synonyms are fully expanded. \item @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"} declares a new @@ -1190,6 +1207,18 @@ the axiomatic type-class instance @{text "t :: (s, \, s)s"}. \end{description} + + \begin{warn} + If you introduce a new type axiomatically, i.e.\ via @{command_ref + typedecl} and @{command_ref axiomatization} + (\secref{sec:axiomatizations}), the minimum requirement is that it has a + non-empty model, to avoid immediate collapse of the logical environment. + Moreover, one needs to demonstrate that the interpretation of such + free-form axiomatizations can coexist with other axiomatization schemes + for types, notably @{command_def typedef} in Isabelle/HOL + (\secref{sec:hol-typedef}), or any other extension that people might have + introduced elsewhere. + \end{warn} *}