# HG changeset patch # User wenzelm # Date 1306354366 -7200 # Node ID dfd4ef8e73f668f607c1a27fad34022f778477a6 # Parent 7438ee56b89a43a05ad3427fac3589df3d6d4b65 updated and re-unified HOL typedef, with some live examples; diff -r 7438ee56b89a -r dfd4ef8e73f6 doc-src/HOL/HOL.tex --- 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 diff -r 7438ee56b89a -r dfd4ef8e73f6 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \}, a set @{text "A :: \ set"}, and a theorem that proves + @{prop "\x. x \ A"}. Thus @{text A} is a non-empty subset of @{text + \}, 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 \} may involve type + variables @{text "\\<^sub>1, \, \\<^sub>n"} which means that the type definition + produces a type constructor @{text "(\\<^sub>1, \, \\<^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 \ 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 "(\\<^sub>1, \, \\<^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 "\\<^sub>1, \, \\<^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 \} 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 \} 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 \ Two" "One \ Three" "Two \ 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 *} diff -r 7438ee56b89a -r dfd4ef8e73f6 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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% % diff -r 7438ee56b89a -r dfd4ef8e73f6 doc-src/manual.bib --- 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},