removed obsolete HOL 'typedecl';
authorwenzelm
Sat Mar 13 15:12:17 2010 +0100 (2010-03-13)
changeset 3574493603d7b8ee9
parent 35743 c506c029a082
child 35745 1416f568b2b6
removed obsolete HOL 'typedecl';
local theory version of HOL 'typedef';
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 13 14:44:47 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Mar 13 15:12:17 2010 +0100
     1.3 @@ -4,17 +4,14 @@
     1.4  
     1.5  chapter {* Isabelle/HOL \label{ch:hol} *}
     1.6  
     1.7 -section {* Primitive types \label{sec:hol-typedef} *}
     1.8 +section {* Typedef axiomatization \label{sec:hol-typedef} *}
     1.9  
    1.10  text {*
    1.11    \begin{matharray}{rcl}
    1.12 -    @{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
    1.13 -    @{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
    1.14 +    @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    1.15    \end{matharray}
    1.16  
    1.17    \begin{rail}
    1.18 -    'typedecl' typespec mixfix?
    1.19 -    ;
    1.20      'typedef' altname? abstype '=' repset
    1.21      ;
    1.22  
    1.23 @@ -28,23 +25,25 @@
    1.24  
    1.25    \begin{description}
    1.26    
    1.27 -  \item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar
    1.28 -  to the original @{command "typedecl"} of Isabelle/Pure (see
    1.29 -  \secref{sec:types-pure}), but also declares type arity @{text "t ::
    1.30 -  (type, \<dots>, type) type"}, making @{text t} an actual HOL type
    1.31 -  constructor.  %FIXME check, update
    1.32 +  \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
    1.33 +  axiomatizes a Gordon/HOL-style type definition in the background
    1.34 +  theory of the current context, depending on a non-emptiness result
    1.35 +  of the set @{text A} (which needs to be proven interactively).
    1.36 +
    1.37 +  The raw type may not depend on parameters or assumptions of the
    1.38 +  context --- this is logically impossible in Isabelle/HOL --- but the
    1.39 +  non-emptiness property can be local, potentially resulting in
    1.40 +  multiple interpretations in target contexts.  Thus the established
    1.41 +  bijection between the representing set @{text A} and the new type
    1.42 +  @{text t} may semantically depend on local assumptions.
    1.43    
    1.44 -  \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up
    1.45 -  a goal stating non-emptiness of the set @{text A}.  After finishing
    1.46 -  the proof, the theory will be augmented by a Gordon/HOL-style type
    1.47 -  definition, which establishes a bijection between the representing
    1.48 -  set @{text A} and the new type @{text t}.
    1.49 -  
    1.50 -  Technically, @{command (HOL) "typedef"} defines both a type @{text
    1.51 -  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 @{text Rep_t}, its inverse @{text Abs_t} (this may be
    1.54 -  changed via an explicit @{keyword (HOL) "morphisms"} declaration).
    1.55 +  By default, @{command (HOL) "typedef"} defines both a type @{text 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 ``@{text "(open)"}''
    1.58 +  declaration is used to suppress a separate constant definition
    1.59 +  altogether.  The injection from type to set is called @{text Rep_t},
    1.60 +  its inverse @{text Abs_t} --- this may be changed via an explicit
    1.61 +  @{keyword (HOL) "morphisms"} declaration.
    1.62    
    1.63    Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
    1.64    Abs_t_inverse} provide the most basic characterization as a
    1.65 @@ -57,19 +56,11 @@
    1.66    on surjectivity; these are already declared as set or type rules for
    1.67    the generic @{method cases} and @{method induct} methods.
    1.68    
    1.69 -  An alternative name may be specified in parentheses; the default is
    1.70 -  to use @{text t} as indicated before.  The ``@{text "(open)"}''
    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 +  @{text 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 @{command
    1.83 -  (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)
    1.84 -  "datatype"} (see \secref{sec:hol-datatype}).
    1.85  *}
    1.86  
    1.87  
    1.88 @@ -906,7 +897,7 @@
    1.89  *}
    1.90  
    1.91  
    1.92 -section {* Invoking automated reasoning tools -- The Sledgehammer *}
    1.93 +section {* Invoking automated reasoning tools --- The Sledgehammer *}
    1.94  
    1.95  text {*
    1.96    Isabelle/HOL includes a generic \emph{ATP manager} that allows
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Mar 13 14:44:47 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Mar 13 15:12:17 2010 +0100
     2.3 @@ -22,19 +22,16 @@
     2.4  }
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{Primitive types \label{sec:hol-typedef}%
     2.8 +\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
    2.12  \begin{isamarkuptext}%
    2.13  \begin{matharray}{rcl}
    2.14 -    \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    2.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}} \\
    2.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}} \\
    2.17    \end{matharray}
    2.18  
    2.19    \begin{rail}
    2.20 -    'typedecl' typespec mixfix?
    2.21 -    ;
    2.22      'typedef' altname? abstype '=' repset
    2.23      ;
    2.24  
    2.25 @@ -48,21 +45,25 @@
    2.26  
    2.27    \begin{description}
    2.28    
    2.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
    2.30 -  to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see
    2.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
    2.32 -  constructor.  %FIXME check, update
    2.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}}
    2.34 +  axiomatizes a Gordon/HOL-style type definition in the background
    2.35 +  theory of the current context, depending on a non-emptiness result
    2.36 +  of the set \isa{A} (which needs to be proven interactively).
    2.37 +
    2.38 +  The raw type may not depend on parameters or assumptions of the
    2.39 +  context --- this is logically impossible in Isabelle/HOL --- but the
    2.40 +  non-emptiness property can be local, potentially resulting in
    2.41 +  multiple interpretations in target contexts.  Thus the established
    2.42 +  bijection between the representing set \isa{A} and the new type
    2.43 +  \isa{t} may semantically depend on local assumptions.
    2.44    
    2.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
    2.46 -  a goal stating non-emptiness of the set \isa{A}.  After finishing
    2.47 -  the proof, the theory will be augmented by a Gordon/HOL-style type
    2.48 -  definition, which establishes a bijection between the representing
    2.49 -  set \isa{A} and the new type \isa{t}.
    2.50 -  
    2.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
    2.52 -  name may be given in parentheses).  The injection from type to set
    2.53 -  is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be
    2.54 -  changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration).
    2.55 +  By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
    2.56 +  and a set (term constant) of the same name, unless an alternative
    2.57 +  base name is given in parentheses, or the ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
    2.58 +  declaration is used to suppress a separate constant definition
    2.59 +  altogether.  The injection from type to set is called \isa{Rep{\isacharunderscore}t},
    2.60 +  its inverse \isa{Abs{\isacharunderscore}t} --- this may be changed via an explicit
    2.61 +  \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
    2.62    
    2.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
    2.64    corresponding injection/surjection pair (in both directions).  Rules
    2.65 @@ -74,17 +75,11 @@
    2.66    on surjectivity; these are already declared as set or type rules for
    2.67    the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
    2.68    
    2.69 -  An alternative name may be specified in parentheses; the default is
    2.70 -  to use \isa{t} as indicated before.  The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
    2.71 -  declaration suppresses a separate constant definition for the
    2.72 -  representing set.
    2.73 +  An alternative name for the set definition (and other derived
    2.74 +  entities) may be specified in parentheses; the default is to use
    2.75 +  \isa{t} as indicated before.
    2.76  
    2.77 -  \end{description}
    2.78 -
    2.79 -  Note that raw type declarations are rarely used in practice; the
    2.80 -  main application is with experimental (or even axiomatic!) theory
    2.81 -  fragments.  Instead of primitive HOL type definitions, user-level
    2.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}).%
    2.83 +  \end{description}%
    2.84  \end{isamarkuptext}%
    2.85  \isamarkuptrue%
    2.86  %
    2.87 @@ -920,7 +915,7 @@
    2.88  \end{isamarkuptext}%
    2.89  \isamarkuptrue%
    2.90  %
    2.91 -\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
    2.92 +\isamarkupsection{Invoking automated reasoning tools --- The Sledgehammer%
    2.93  }
    2.94  \isamarkuptrue%
    2.95  %