1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Mar 13 14:44:47 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Mar 13 15:12:17 2010 +0100
     1.3 @@ -22,19 +22,16 @@
     1.4  }
     1.5  \isamarkuptrue%
     1.6  %
     1.7 -\isamarkupsection{Primitive types \label{sec:hol-typedef}%
     1.8 +\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
     1.9  }
    1.10  \isamarkuptrue%
    1.11  %
    1.12  \begin{isamarkuptext}%
    1.13  \begin{matharray}{rcl}
    1.14 -    \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    1.15 -    \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
    1.16 +    \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
    1.17    \end{matharray}
    1.18  
    1.19    \begin{rail}
    1.20 -    'typedecl' typespec mixfix?
    1.21 -    ;
    1.22      'typedef' altname? abstype '=' repset
    1.23      ;
    1.24  
    1.25 @@ -48,21 +45,25 @@
    1.26  
    1.27    \begin{description}
    1.28    
    1.29 -  \item \hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} is similar
    1.30 -  to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see
    1.31 -  \secref{sec:types-pure}), but also declares type arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an actual HOL type
    1.32 -  constructor.  %FIXME check, update
    1.33 +  \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}}
    1.34 +  axiomatizes a Gordon/HOL-style type definition in the background
    1.35 +  theory of the current context, depending on a non-emptiness result
    1.36 +  of the set \isa{A} (which needs to be proven interactively).
    1.37 +
    1.38 +  The raw type may not depend on parameters or assumptions of the
    1.39 +  context --- this is logically impossible in Isabelle/HOL --- but the
    1.40 +  non-emptiness property can be local, potentially resulting in
    1.41 +  multiple interpretations in target contexts.  Thus the established
    1.42 +  bijection between the representing set \isa{A} and the new type
    1.43 +  \isa{t} may semantically depend on local assumptions.
    1.44    
    1.45 -  \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}} sets up
    1.46 -  a goal stating non-emptiness of the set \isa{A}.  After finishing
    1.47 -  the proof, the theory will be augmented by a Gordon/HOL-style type
    1.48 -  definition, which establishes a bijection between the representing
    1.49 -  set \isa{A} and the new type \isa{t}.
    1.50 -  
    1.51 -  Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base
    1.52 -  name may be given in parentheses).  The injection from type to set
    1.53 -  is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be
    1.54 -  changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration).
    1.55 +  By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
    1.56 +  and a set (term constant) of the same name, unless an alternative
    1.57 +  base name is given in parentheses, or the ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
    1.58 +  declaration is used to suppress a separate constant definition
    1.59 +  altogether.  The injection from type to set is called \isa{Rep{\isacharunderscore}t},
    1.60 +  its inverse \isa{Abs{\isacharunderscore}t} --- this may be changed via an explicit
    1.61 +  \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
    1.62    
    1.63    Theorems \isa{Rep{\isacharunderscore}t}, \isa{Rep{\isacharunderscore}t{\isacharunderscore}inverse}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inverse} provide the most basic characterization as a
    1.64    corresponding injection/surjection pair (in both directions).  Rules
    1.65 @@ -74,17 +75,11 @@
    1.66    on surjectivity; these are already declared as set or type rules for
    1.67    the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
    1.68    
    1.69 -  An alternative name may be specified in parentheses; the default is
    1.70 -  to use \isa{t} as indicated before.  The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
    1.71 -  declaration suppresses a separate constant definition for the
    1.72 -  representing set.
    1.73 +  An alternative name for the set definition (and other derived
    1.74 +  entities) may be specified in parentheses; the default is to use
    1.75 +  \isa{t} as indicated before.
    1.76  
    1.77 -  \end{description}
    1.78 -
    1.79 -  Note that raw type declarations are rarely used in practice; the
    1.80 -  main application is with experimental (or even axiomatic!) theory
    1.81 -  fragments.  Instead of primitive HOL type definitions, user-level
    1.82 -  theories usually refer to higher-level packages such as \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}} (see \secref{sec:hol-record}) or \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} (see \secref{sec:hol-datatype}).%
    1.83 +  \end{description}%
    1.84  \end{isamarkuptext}%
    1.85  \isamarkuptrue%
    1.86  %
    1.87 @@ -920,7 +915,7 @@
    1.88  \end{isamarkuptext}%
    1.89  \isamarkuptrue%
    1.90  %
    1.91 -\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
    1.92 +\isamarkupsection{Invoking automated reasoning tools --- The Sledgehammer%
    1.93  }
    1.94  \isamarkuptrue%
    1.95  %