doc-src/TutorialI/document/types.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/types.tex	Thu Jul 26 17:16:02 2012 +0200
@@ -0,0 +1,75 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{types}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+\ number\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+\ gate\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ alist\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent
+Internally all synonyms are fully expanded.  As a consequence Isabelle's
+output never contains synonyms.  Their main purpose is to improve the
+readability of theories.  Synonyms can be used just like any other
+type.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Constant Definitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\label{sec:ConstDefinitions}\indexbold{definitions}%
+Nonrecursive definitions can be made with the \commdx{definition}
+command, for example \isa{nand} and \isa{xor} gates
+(based on type \isa{gate} above):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{definition}\isamarkupfalse%
+\ nand\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ gate\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}nand\ A\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ xor\ \ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ gate\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}xor\ \ A\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent%
+The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
+that must be used in constant definitions.
+Pattern-matching is not allowed: each definition must be of
+the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
+Section~\ref{sec:Simp-with-Defs} explains how definitions are used
+in proofs. The default name of each definition is $f$\isa{{\isaliteral{5F}{\isacharunderscore}}def}, where
+$f$ is the name of the defined constant.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: