1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Jul 02 12:12:26 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Jul 02 13:06:07 2014 +0200
     1.3 @@ -1087,7 +1087,7 @@
     1.4    \begin{description}
     1.5  
     1.6    \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} produces an
     1.7 -  axiomatization (\secref{sec:basic-spec}) for a type definition in the
     1.8 +  axiomatization (\secref{sec:axiomatizations}) for a type definition in the
     1.9    background theory of the current context, depending on a non-emptiness
    1.10    result of the set @{text A} that needs to be proven here. The set @{text
    1.11    A} may contain type variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the
    1.12 @@ -1132,16 +1132,6 @@
    1.13    respectively.
    1.14  
    1.15    \end{description}
    1.16 -
    1.17 -  \begin{warn}
    1.18 -  If you introduce a new type axiomatically, i.e.\ via @{command_ref
    1.19 -  typedecl} and @{command_ref axiomatization}, the minimum requirement
    1.20 -  is that it has a non-empty model, to avoid immediate collapse of the
    1.21 -  HOL logic.  Moreover, one needs to demonstrate that the
    1.22 -  interpretation of such free-form axiomatizations can coexist with
    1.23 -  that of the regular @{command_def typedef} scheme, and any extension
    1.24 -  that other people might have introduced elsewhere.
    1.25 -  \end{warn}
    1.26  *}
    1.27  
    1.28  subsubsection {* Examples *}

     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Wed Jul 02 12:12:26 2014 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Jul 02 13:06:07 2014 +0200
     2.3 @@ -257,11 +257,10 @@
     2.4    including trace by metis
     2.5  
     2.6  
     2.7 -section {* Basic specification elements \label{sec:basic-spec} *}
     2.8 +section {* Term definitions \label{sec:term-definitions} *}
     2.9  
    2.10  text {*
    2.11    \begin{matharray}{rcll}
    2.12 -    @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    2.13      @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    2.14      @{attribute_def "defn"} & : & @{text attribute} \\
    2.15      @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
    2.16 @@ -269,14 +268,12 @@
    2.17      @{command_def "print_abbrevs"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
    2.18    \end{matharray}
    2.19  
    2.20 -  These specification mechanisms provide a slightly more abstract view
    2.21 -  than the underlying primitives of @{command "consts"}, @{command
    2.22 -  "defs"} (see \secref{sec:consts}), and raw axioms.  In particular,
    2.23 -  type-inference covers the whole specification as usual.
    2.24 +  Term definitions may either happen within the logic (as equational axioms
    2.25 +  of a certain form, see also see \secref{sec:consts}), or outside of it as
    2.26 +  rewrite system on abstract syntax. The second form is called
    2.27 +  ``abbreviation''.
    2.28  
    2.29    @{rail \<open>
    2.30 -    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
    2.31 -    ;
    2.32      @@{command definition} @{syntax target}? \<newline>
    2.33        (decl @'where')? @{syntax thmdecl}? @{syntax prop}
    2.34      ;
    2.35 @@ -284,32 +281,11 @@
    2.36        (decl @'where')? @{syntax prop}
    2.37      ;
    2.38  
    2.39 -    @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
    2.40 -      @{syntax mixfix}? | @{syntax vars}) + @'and')
    2.41 -    ;
    2.42 -    specs: (@{syntax thmdecl}? @{syntax props} + @'and')
    2.43 -    ;
    2.44      decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
    2.45    \<close>}
    2.46  
    2.47    \begin{description}
    2.48    
    2.49 -  \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
    2.50 -  introduces several constants simultaneously and states axiomatic
    2.51 -  properties for these.  The constants are marked as being specified
    2.52 -  once and for all, which prevents additional specifications being
    2.53 -  issued later on.
    2.54 -  
    2.55 -  Axiomatic specifications are required when declaring a new logical system
    2.56 -  within Isabelle/Pure, but in an application environment like
    2.57 -  Isabelle/HOL the user normally stays within definitional mechanisms
    2.58 -  provided by the logic and its libraries.
    2.59 -
    2.60 -  Axiomatization is restricted to a global theory context. Despite the
    2.61 -  possibility to mark some constants as specified by a particular
    2.62 -  axiomatization, the dependency tracking may be insufficient and disrupt
    2.63 -  the well-formedness of an otherwise definitional theory.
    2.64 -
    2.65    \item @{command "definition"}~@{text "c \<WHERE> eq"} produces an
    2.66    internal definition @{text "c \<equiv> t"} according to the specification
    2.67    given as @{text eq}, which is then turned into a proven fact.  The
    2.68 @@ -351,6 +327,48 @@
    2.69  *}
    2.70  
    2.71  
    2.72 +section {* Axiomatizations \label{sec:axiomatizations} *}
    2.73 +
    2.74 +text {*
    2.75 +  \begin{matharray}{rcll}
    2.76 +    @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    2.77 +  \end{matharray}
    2.78 +
    2.79 +  @{rail \<open>
    2.80 +    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
    2.81 +    ;
    2.82 +
    2.83 +    @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
    2.84 +      @{syntax mixfix}? | @{syntax vars}) + @'and')
    2.85 +    ;
    2.86 +    specs: (@{syntax thmdecl}? @{syntax props} + @'and')
    2.87 +  \<close>}
    2.88 +
    2.89 +  \begin{description}
    2.90 +
    2.91 +  \item @{command "axiomatization"}~@{text "c\<^sub>1 \<dots> c\<^sub>m \<WHERE> \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
    2.92 +  introduces several constants simultaneously and states axiomatic
    2.93 +  properties for these. The constants are marked as being specified once and
    2.94 +  for all, which prevents additional specifications for the same constants
    2.95 +  later on, but it is always possible do emit axiomatizations without
    2.96 +  referring to particular constants. Note that lack of precise dependency
    2.97 +  tracking of axiomatizations may disrupt the well-formedness of an
    2.98 +  otherwise definitional theory.
    2.99 +
   2.100 +  Axiomatization is restricted to a global theory context: support for local
   2.101 +  theory targets \secref{sec:target} would introduce an extra dimension of
   2.102 +  uncertainty what the written specifications really are, and make it
   2.103 +  infeasible to argue why they are correct.
   2.104 +
   2.105 +  Axiomatic specifications are required when declaring a new logical system
   2.106 +  within Isabelle/Pure, but in an application environment like Isabelle/HOL
   2.107 +  the user normally stays within definitional mechanisms provided by the
   2.108 +  logic and its libraries.
   2.109 +
   2.110 +  \end{description}
   2.111 +*}
   2.112 +
   2.113 +
   2.114  section {* Generic declarations *}
   2.115  
   2.116  text {*
   2.117 @@ -563,7 +581,7 @@
   2.118    Both @{element "assumes"} and @{element "defines"} elements
   2.119    contribute to the locale specification.  When defining an operation
   2.120    derived from the parameters, @{command "definition"}
   2.121 -  (\secref{sec:basic-spec}) is usually more appropriate.
   2.122 +  (\secref{sec:term-definitions}) is usually more appropriate.
   2.123    
   2.124    Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
   2.125    in the syntax of @{element "assumes"} and @{element "defines"} above
   2.126 @@ -1161,7 +1179,7 @@
   2.127  *}
   2.128  
   2.129  
   2.130 -subsection {* Types and type abbreviations \label{sec:types-pure} *}
   2.131 +subsection {* Types \label{sec:types-pure} *}
   2.132  
   2.133  text {*
   2.134    \begin{matharray}{rcll}
   2.135 @@ -1177,11 +1195,10 @@
   2.136  
   2.137    \begin{description}
   2.138  
   2.139 -  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}
   2.140 -  introduces a \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the
   2.141 -  existing type @{text "\<tau>"}.  Unlike actual type definitions, as are
   2.142 -  available in Isabelle/HOL for example, type synonyms are merely
   2.143 -  syntactic abbreviations without any logical significance.
   2.144 +  \item @{command "type_synonym"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"} introduces a
   2.145 +  \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} for the existing type @{text
   2.146 +  "\<tau>"}. Unlike the semantic type definitions in Isabelle/HOL, type synonyms
   2.147 +  are merely syntactic abbreviations without any logical significance.
   2.148    Internally, type synonyms are fully expanded.
   2.149    
   2.150    \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
   2.151 @@ -1190,6 +1207,18 @@
   2.152    the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
   2.153  
   2.154    \end{description}
   2.155 +
   2.156 +  \begin{warn}
   2.157 +  If you introduce a new type axiomatically, i.e.\ via @{command_ref
   2.158 +  typedecl} and @{command_ref axiomatization}
   2.159 +  (\secref{sec:axiomatizations}), the minimum requirement is that it has a
   2.160 +  non-empty model, to avoid immediate collapse of the logical environment.
   2.161 +  Moreover, one needs to demonstrate that the interpretation of such
   2.162 +  free-form axiomatizations can coexist with other axiomatization schemes
   2.163 +  for types, notably @{command_def typedef} in Isabelle/HOL
   2.164 +  (\secref{sec:hol-typedef}), or any other extension that people might have
   2.165 +  introduced elsewhere.
   2.166 +  \end{warn}
   2.167  *}
   2.168  
   2.169