--- a/doc-src/HOL/HOL.tex Sat May 21 11:31:59 2011 +0200
+++ b/doc-src/HOL/HOL.tex Wed May 25 22:12:46 2011 +0200
@@ -147,9 +147,9 @@
term} if $\sigma$ and~$\tau$ do, allowing quantification over
functions.
-HOL allows new types to be declared as subsets of existing types;
-see~{\S}\ref{sec:HOL:Types}. ML-like datatypes can also be declared; see
-~{\S}\ref{sec:HOL:datatype}.
+HOL allows new types to be declared as subsets of existing types,
+either using the primitive \texttt{typedef} or the more convenient
+\texttt{datatype} (see~{\S}\ref{sec:HOL:datatype}).
Several syntactic type classes --- \cldx{plus}, \cldx{minus},
\cldx{times} and
@@ -1597,95 +1597,13 @@
\index{list@{\textit{list}} type|)}
-\subsection{Introducing new types} \label{sec:typedef}
-
-The HOL-methodology dictates that all extensions to a theory should be
-\textbf{definitional}. The type definition mechanism that meets this
-criterion is \ttindex{typedef}. Note that \emph{type synonyms}, which are
-inherited from Pure and described elsewhere, are just syntactic abbreviations
-that have no logical meaning.
-
-\begin{warn}
- Types in HOL must be non-empty; otherwise the quantifier rules would be
- unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.
-\end{warn}
-A \bfindex{type definition} identifies the new type with a subset of
-an existing type. More precisely, the new type is defined by
-exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
-theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
-and the new type denotes this subset. New functions are defined that
-establish an isomorphism between the new type and the subset. If
-type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
-then the type definition creates a type constructor
-$(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
-
-The syntax for type definitions is given in the Isabelle/Isar
-reference manual.
-
-If all context conditions are met (no duplicate type variables in
-`typevarlist', no extra type variables in `set', and no free term variables
-in `set'), the following components are added to the theory:
-\begin{itemize}
-\item a type $ty :: (term,\dots,term)term$
-\item constants
-\begin{eqnarray*}
-T &::& \tau\;set \\
-Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
-Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
-\end{eqnarray*}
-\item a definition and three axioms
-\[
-\begin{array}{ll}
-T{\tt_def} & T \equiv A \\
-{\tt Rep_}T & Rep_T\,x \in T \\
-{\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
-{\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y
-\end{array}
-\]
-stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
-and its inverse $Abs_T$.
-\end{itemize}
-Below are two simple examples of HOL type definitions. Non-emptiness is
-proved automatically here.
-\begin{ttbox}
-typedef unit = "{\ttlbrace}True{\ttrbrace}"
-
-typedef (prod)
- ('a, 'b) "*" (infixr 20)
- = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
-\end{ttbox}
-
-Type definitions permit the introduction of abstract data types in a safe
-way, namely by providing models based on already existing types. Given some
-abstract axiomatic description $P$ of a type, this involves two steps:
-\begin{enumerate}
-\item Find an appropriate type $\tau$ and subset $A$ which has the desired
- properties $P$, and make a type definition based on this representation.
-\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
-\end{enumerate}
-You can now forget about the representation and work solely in terms of the
-abstract properties $P$.
-
-\begin{warn}
-If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
-declaring the type and its operations and by stating the desired axioms, you
-should make sure the type has a non-empty model. You must also have a clause
-\par
-\begin{ttbox}
-arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
-\end{ttbox}
-in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the
-class of all HOL types.
-\end{warn}
-
-
\section{Datatype definitions}
\label{sec:HOL:datatype}
\index{*datatype|(}
Inductive datatypes, similar to those of \ML, frequently appear in
applications of Isabelle/HOL. In principle, such types could be defined by
-hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too
+hand via \texttt{typedef}, but this would be far too
tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\
\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an
appropriate \texttt{typedef} based on a least fixed-point construction, and
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sat May 21 11:31:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed May 25 22:12:46 2011 +0200
@@ -6,62 +6,154 @@
section {* Typedef axiomatization \label{sec:hol-typedef} *}
-text {*
+text {* A Gordon/HOL-style type definition is a certain axiom scheme
+ that identifies a new type with a subset of an existing type. More
+ precisely, the new type is defined by exhibiting an existing type
+ @{text \<tau>}, a set @{text "A :: \<tau> set"}, and a theorem that proves
+ @{prop "\<exists>x. x \<in> A"}. Thus @{text A} is a non-empty subset of @{text
+ \<tau>}, and the new type denotes this subset. New functions are
+ postulated that establish an isomorphism between the new type and
+ the subset. In general, the type @{text \<tau>} may involve type
+ variables @{text "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} which means that the type definition
+ produces a type constructor @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} depending on
+ those type arguments.
+
+ The axiomatization can be considered a ``definition'' in the sense
+ of the particular set-theoretic interpretation of HOL
+ \cite{pitts93}, where the universe of types is required to be
+ downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
+ new types introduced by @{command "typedef"} stay within the range
+ of HOL models by construction. Note that @{command_ref
+ type_synonym} from Isabelle/Pure merely introduces syntactic
+ abbreviations, without any logical significance.
+
\begin{matharray}{rcl}
@{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
\end{matharray}
@{rail "
- @@{command (HOL) typedef} altname? abstype '=' repset
+ @@{command (HOL) typedef} alt_name? abs_type '=' rep_set
;
- altname: '(' (@{syntax name} | @'open' | @'open' @{syntax name}) ')'
+ alt_name: '(' (@{syntax name} | @'open' | @'open' @{syntax name}) ')'
;
- abstype: @{syntax typespec_sorts} @{syntax mixfix}?
+ abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
;
- repset: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
+ rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
"}
\begin{description}
\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).
+ axiomatizes 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 "\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n"} as specified on the LHS,
+ but no term variables.
- 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.
+ Even though a local theory specification, the newly introduced type
+ constructor cannot depend on parameters or assumptions of the
+ context: this is structurally impossible in HOL. In contrast, the
+ non-emptiness proof may use local assumptions in unusual situations,
+ which could result in different interpretations in target contexts:
+ the meaning of the bijection between the representing set @{text A}
+ and the new type @{text t} may then change in different application
+ contexts.
- 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
+ By default, @{command (HOL) "typedef"} defines both a type
+ constructor @{text t} for the new type, and a term constant @{text
+ t} for the representing set within the old type. Use the ``@{text
+ "(open)"}'' option 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.
+ its inverse @{text Abs_t}, unless explicit @{keyword (HOL)
+ "morphisms"} specification provides alternative names.
+
+ The core axiomatization uses the locale predicate @{const
+ type_definition} as defined in Isabelle/HOL. Various basic
+ consequences of that are instantiated accordingly, re-using the
+ locale facts with names derived from the new type constructor. Thus
+ the generic @{thm type_definition.Rep} is turned into the specific
+ @{text "Rep_t"}, for example.
- Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
- Abs_t_inverse} provide the most basic characterization as a
- corresponding injection/surjection pair (in both directions). Rules
- @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
- more convenient view on the injectivity part, suitable for automated
- proof tools (e.g.\ in @{attribute simp} or @{attribute iff}
- declarations). Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and
- @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
- on surjectivity; these are already declared as set or type rules for
- the generic @{method cases} and @{method induct} methods.
+ Theorems @{thm type_definition.Rep}, @{thm
+ type_definition.Rep_inverse}, and @{thm type_definition.Abs_inverse}
+ provide the most basic characterization as a corresponding
+ injection/surjection pair (in both directions). The derived rules
+ @{thm type_definition.Rep_inject} and @{thm
+ type_definition.Abs_inject} provide a more convenient version of
+ injectivity, suitable for automated proof tools (e.g.\ in
+ declarations involving @{attribute simp} or @{attribute iff}).
+ Furthermore, the rules @{thm type_definition.Rep_cases}~/ @{thm
+ type_definition.Rep_induct}, and @{thm type_definition.Abs_cases}~/
+ @{thm type_definition.Abs_induct} provide alternative views on
+ surjectivity. These rules are already declared as set or type rules
+ for the generic @{method cases} and @{method induct} methods,
+ respectively.
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.
+ @{text t} directly.
\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 (e.g.\ in HOLCF
+ \cite{MuellerNvOS99}).
+ \end{warn}
*}
+subsubsection {* Examples *}
+
+text {* Type definitions permit the introduction of abstract data
+ types in a safe way, namely by providing models based on already
+ existing types. Given some abstract axiomatic description @{text P}
+ of a type, this involves two steps:
+
+ \begin{enumerate}
+
+ \item Find an appropriate type @{text \<tau>} and subset @{text A} which
+ has the desired properties @{text P}, and make a type definition
+ based on this representation.
+
+ \item Prove that @{text P} holds for @{text \<tau>} by lifting @{text P}
+ from the representation.
+
+ \end{enumerate}
+
+ You can later forget about the representation and work solely in
+ terms of the abstract properties @{text P}.
+
+ \medskip The following trivial example pulls a three-element type
+ into existence within the formal logical environment of HOL. *}
+
+typedef three = "{(True, True), (True, False), (False, True)}"
+ by blast
+
+definition "One = Abs_three (True, True)"
+definition "Two = Abs_three (True, False)"
+definition "Three = Abs_three (False, True)"
+
+lemma three_distinct: "One \<noteq> Two" "One \<noteq> Three" "Two \<noteq> Three"
+ by (simp_all add: One_def Two_def Three_def Abs_three_inject three_def)
+
+lemma three_cases:
+ fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
+ by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject three_def)
+
+text {* Note that such trivial constructions are better done with
+ derived specification mechanisms such as @{command datatype}: *}
+
+datatype three' = One' | Two' | Three'
+
+text {* This avoids re-doing basic definitions and proofs from the
+ primitive @{command typedef} above. *}
+
section {* Adhoc tuples *}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat May 21 11:31:59 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed May 25 22:12:46 2011 +0200
@@ -27,7 +27,26 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\begin{matharray}{rcl}
+A Gordon/HOL-style type definition is a certain axiom scheme
+ that identifies a new type with a subset of an existing type. More
+ precisely, the new type is defined by exhibiting an existing type
+ \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, a set \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ set{\isaliteral{22}{\isachardoublequote}}}, and a theorem that proves
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequote}}}. Thus \isa{A} is a non-empty subset of \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}, and the new type denotes this subset. New functions are
+ postulated that establish an isomorphism between the new type and
+ the subset. In general, the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} may involve type
+ variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} which means that the type definition
+ produces a type constructor \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} depending on
+ those type arguments.
+
+ The axiomatization can be considered a ``definition'' in the sense
+ of the particular set-theoretic interpretation of HOL
+ \cite{pitts93}, where the universe of types is required to be
+ downwards-closed wrt.\ arbitrary non-empty subsets. Thus genuinely
+ new types introduced by \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} stay within the range
+ of HOL models by construction. Note that \indexref{}{command}{type\_synonym}\hyperlink{command.type-synonym}{\mbox{\isa{\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}}}} from Isabelle/Pure merely introduces syntactic
+ abbreviations, without any logical significance.
+
+ \begin{matharray}{rcl}
\indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
\end{matharray}
@@ -36,13 +55,13 @@
\rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@nont{\isa{altname}}[]
+\rail@nont{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}[]
\rail@endbar
-\rail@nont{\isa{abstype}}[]
+\rail@nont{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}[]
\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nont{\isa{repset}}[]
+\rail@nont{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}[]
\rail@end
-\rail@begin{3}{\isa{altname}}
+\rail@begin{3}{\isa{alt{\isaliteral{5F}{\isacharunderscore}}name}}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@bar
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
@@ -54,14 +73,14 @@
\rail@endbar
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@end
-\rail@begin{2}{\isa{abstype}}
+\rail@begin{2}{\isa{abs{\isaliteral{5F}{\isacharunderscore}}type}}
\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
\rail@endbar
\rail@end
-\rail@begin{2}{\isa{repset}}
+\rail@begin{2}{\isa{rep{\isaliteral{5F}{\isacharunderscore}}set}}
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@bar
\rail@nextbar{1}
@@ -76,40 +95,161 @@
\begin{description}
\item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\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).
+ axiomatizes a type definition in the background theory of the
+ current context, depending on a non-emptiness result of the set
+ \isa{A} that needs to be proven here. The set \isa{A} may
+ contain type variables \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} as specified on the LHS,
+ but no term variables.
- 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.
+ Even though a local theory specification, the newly introduced type
+ constructor cannot depend on parameters or assumptions of the
+ context: this is structurally impossible in HOL. In contrast, the
+ non-emptiness proof may use local assumptions in unusual situations,
+ which could result in different interpretations in target contexts:
+ the meaning of the bijection between the representing set \isa{A}
+ and the new type \isa{t} may then change in different application
+ contexts.
- 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{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''
- declaration is used to suppress a separate constant definition
+ By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type
+ constructor \isa{t} for the new type, and a term constant \isa{t} for the representing set within the old type. Use the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option to suppress a separate constant definition
altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
- its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t} --- this may be changed via an explicit
- \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
+ its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t}, unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
+
+ The core axiomatization uses the locale predicate \isa{type{\isaliteral{5F}{\isacharunderscore}}definition} as defined in Isabelle/HOL. Various basic
+ consequences of that are instantiated accordingly, re-using the
+ locale facts with names derived from the new type constructor. Thus
+ the generic \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep} is turned into the specific
+ \isa{{\isaliteral{22}{\isachardoublequote}}Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{22}{\isachardoublequote}}}, for example.
- Theorems \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t}, \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse} provide the most basic characterization as a
- corresponding injection/surjection pair (in both directions). Rules
- \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} provide a slightly
- more convenient view on the injectivity part, suitable for automated
- proof tools (e.g.\ in \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}
- declarations). Rules \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct}, and
- \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views
- 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.
+ Theorems \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep}, \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inverse}
+ provide the most basic characterization as a corresponding
+ injection/surjection pair (in both directions). The derived rules
+ \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}inject} provide a more convenient version of
+ injectivity, suitable for automated proof tools (e.g.\ in
+ declarations involving \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}).
+ Furthermore, the rules \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}cases}~/ \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Rep{\isaliteral{5F}{\isacharunderscore}}induct}, and \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}cases}~/
+ \isa{type{\isaliteral{5F}{\isacharunderscore}}definition{\isaliteral{2E}{\isachardot}}Abs{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views on
+ surjectivity. These rules 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,
+ respectively.
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.
+ \isa{t} directly.
+
+ \end{description}
+
+ \begin{warn}
+ If you introduce a new type axiomatically, i.e.\ via \indexref{}{command}{typedecl}\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} and \indexref{}{command}{axiomatization}\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{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 \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}} scheme, and any extension
+ that other people might have introduced elsewhere (e.g.\ in HOLCF
+ \cite{MuellerNvOS99}).
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Examples%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Type definitions permit the introduction of abstract data
+ types in a safe way, namely by providing models based on already
+ existing types. Given some abstract axiomatic description \isa{P}
+ of a type, this involves two steps:
+
+ \begin{enumerate}
+
+ \item Find an appropriate type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} and subset \isa{A} which
+ has the desired properties \isa{P}, and make a type definition
+ based on this representation.
+
+ \item Prove that \isa{P} holds for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} by lifting \isa{P}
+ from the representation.
+
+ \end{enumerate}
+
+ You can later forget about the representation and work solely in
+ terms of the abstract properties \isa{P}.
- \end{description}%
+ \medskip The following trivial example pulls a three-element type
+ into existence within the formal logical environment of HOL.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{typedef}\isamarkupfalse%
+\ three\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}True{\isaliteral{2C}{\isacharcomma}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}Three\ {\isaliteral{3D}{\isacharequal}}\ Abs{\isaliteral{5F}{\isacharunderscore}}three\ {\isaliteral{28}{\isacharparenleft}}False{\isaliteral{2C}{\isacharcomma}}\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ three{\isaliteral{5F}{\isacharunderscore}}distinct{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}One\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}Two\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ three{\isaliteral{5F}{\isacharunderscore}}cases{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \isakeyword{fixes}\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ three\ \isakeyword{obtains}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Two{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Three{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}auto\ simp{\isaliteral{3A}{\isacharcolon}}\ One{\isaliteral{5F}{\isacharunderscore}}def\ Two{\isaliteral{5F}{\isacharunderscore}}def\ Three{\isaliteral{5F}{\isacharunderscore}}def\ Abs{\isaliteral{5F}{\isacharunderscore}}three{\isaliteral{5F}{\isacharunderscore}}inject\ three{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Note that such trivial constructions are better done with
+ derived specification mechanisms such as \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ three{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ One{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Two{\isaliteral{27}{\isacharprime}}\ {\isaliteral{7C}{\isacharbar}}\ Three{\isaliteral{27}{\isacharprime}}%
+\begin{isamarkuptext}%
+This avoids re-doing basic definitions and proofs from the
+ primitive \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} above.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/manual.bib Sat May 21 11:31:59 2011 +0200
+++ b/doc-src/manual.bib Wed May 25 22:12:46 2011 +0200
@@ -532,8 +532,7 @@
@Book{mgordon-hol,
editor = {M. J. C. Gordon and T. F. Melham},
- title = {Introduction to {HOL}: A Theorem Proving Environment for
- Higher Order Logic},
+ title = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
publisher = CUP,
year = 1993}
@@ -1310,6 +1309,15 @@
year = 1986,
note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
+@InCollection{pitts93,
+ author = {A. Pitts},
+ title = {The {HOL} Logic},
+ editor = {M. J. C. Gordon and T. F. Melham},
+ booktitle = {Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic},
+ pages = {191--232},
+ publisher = CUP,
+ year = 1993}
+
@Article{pitts94,
author = {Andrew M. Pitts},
title = {A Co-induction Principle for Recursively Defined Domains},