--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 13 14:44:47 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Mar 13 15:12:17 2010 +0100
@@ -4,17 +4,14 @@
chapter {* Isabelle/HOL \label{ch:hol} *}
-section {* Primitive types \label{sec:hol-typedef} *}
+section {* Typedef axiomatization \label{sec:hol-typedef} *}
text {*
\begin{matharray}{rcl}
- @{command_def (HOL) "typedecl"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "typedef"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
\end{matharray}
\begin{rail}
- 'typedecl' typespec mixfix?
- ;
'typedef' altname? abstype '=' repset
;
@@ -28,23 +25,25 @@
\begin{description}
- \item @{command (HOL) "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} is similar
- to the original @{command "typedecl"} of Isabelle/Pure (see
- \secref{sec:types-pure}), but also declares type arity @{text "t ::
- (type, \<dots>, type) type"}, making @{text t} an actual HOL type
- constructor. %FIXME check, update
+ \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
+ axiomatizes a Gordon/HOL-style type definition in the background
+ theory of the current context, depending on a non-emptiness result
+ of the set @{text A} (which needs to be proven interactively).
+
+ The raw type may not depend on parameters or assumptions of the
+ context --- this is logically impossible in Isabelle/HOL --- but the
+ non-emptiness property can be local, potentially resulting in
+ multiple interpretations in target contexts. Thus the established
+ bijection between the representing set @{text A} and the new type
+ @{text t} may semantically depend on local assumptions.
- \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"} sets up
- a goal stating non-emptiness of the set @{text A}. After finishing
- the proof, the theory will be augmented by a Gordon/HOL-style type
- definition, which establishes a bijection between the representing
- set @{text A} and the new type @{text t}.
-
- Technically, @{command (HOL) "typedef"} defines both a type @{text
- t} and a set (term constant) of the same name (an alternative base
- name may be given in parentheses). The injection from type to set
- is called @{text Rep_t}, its inverse @{text Abs_t} (this may be
- changed via an explicit @{keyword (HOL) "morphisms"} declaration).
+ By default, @{command (HOL) "typedef"} defines both a type @{text t}
+ and a set (term constant) of the same name, unless an alternative
+ base name is given in parentheses, or the ``@{text "(open)"}''
+ declaration is used to suppress a separate constant definition
+ altogether. The injection from type to set is called @{text Rep_t},
+ its inverse @{text Abs_t} --- this may be changed via an explicit
+ @{keyword (HOL) "morphisms"} declaration.
Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
Abs_t_inverse} provide the most basic characterization as a
@@ -57,19 +56,11 @@
on surjectivity; these are already declared as set or type rules for
the generic @{method cases} and @{method induct} methods.
- An alternative name may be specified in parentheses; the default is
- to use @{text t} as indicated before. The ``@{text "(open)"}''
- declaration suppresses a separate constant definition for the
- representing set.
+ An alternative name for the set definition (and other derived
+ entities) may be specified in parentheses; the default is to use
+ @{text t} as indicated before.
\end{description}
-
- Note that raw type declarations are rarely used in practice; the
- main application is with experimental (or even axiomatic!) theory
- fragments. Instead of primitive HOL type definitions, user-level
- theories usually refer to higher-level packages such as @{command
- (HOL) "record"} (see \secref{sec:hol-record}) or @{command (HOL)
- "datatype"} (see \secref{sec:hol-datatype}).
*}
@@ -906,7 +897,7 @@
*}
-section {* Invoking automated reasoning tools -- The Sledgehammer *}
+section {* Invoking automated reasoning tools --- The Sledgehammer *}
text {*
Isabelle/HOL includes a generic \emph{ATP manager} that allows
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 13 14:44:47 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Mar 13 15:12:17 2010 +0100
@@ -22,19 +22,16 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Primitive types \label{sec:hol-typedef}%
+\isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
- \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}} \\
+ \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}} \\
\end{matharray}
\begin{rail}
- 'typedecl' typespec mixfix?
- ;
'typedef' altname? abstype '=' repset
;
@@ -48,21 +45,25 @@
\begin{description}
- \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
- to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see
- \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
- constructor. %FIXME check, update
+ \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}}
+ axiomatizes a Gordon/HOL-style type definition in the background
+ theory of the current context, depending on a non-emptiness result
+ of the set \isa{A} (which needs to be proven interactively).
+
+ The raw type may not depend on parameters or assumptions of the
+ context --- this is logically impossible in Isabelle/HOL --- but the
+ non-emptiness property can be local, potentially resulting in
+ multiple interpretations in target contexts. Thus the established
+ bijection between the representing set \isa{A} and the new type
+ \isa{t} may semantically depend on local assumptions.
- \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
- a goal stating non-emptiness of the set \isa{A}. After finishing
- the proof, the theory will be augmented by a Gordon/HOL-style type
- definition, which establishes a bijection between the representing
- set \isa{A} and the new type \isa{t}.
-
- 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
- name may be given in parentheses). The injection from type to set
- is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be
- changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration).
+ By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
+ and a set (term constant) of the same name, unless an alternative
+ base name is given in parentheses, or the ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
+ declaration is used to suppress a separate constant definition
+ altogether. The injection from type to set is called \isa{Rep{\isacharunderscore}t},
+ its inverse \isa{Abs{\isacharunderscore}t} --- this may be changed via an explicit
+ \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
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
corresponding injection/surjection pair (in both directions). Rules
@@ -74,17 +75,11 @@
on surjectivity; these are already declared as set or type rules for
the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
- An alternative name may be specified in parentheses; the default is
- to use \isa{t} as indicated before. The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
- declaration suppresses a separate constant definition for the
- representing set.
+ An alternative name for the set definition (and other derived
+ entities) may be specified in parentheses; the default is to use
+ \isa{t} as indicated before.
- \end{description}
-
- Note that raw type declarations are rarely used in practice; the
- main application is with experimental (or even axiomatic!) theory
- fragments. Instead of primitive HOL type definitions, user-level
- 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}).%
+ \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -920,7 +915,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
+\isamarkupsection{Invoking automated reasoning tools --- The Sledgehammer%
}
\isamarkuptrue%
%