|
nipkow@9722
|
1 |
%
|
|
nipkow@9722
|
2 |
\begin{isabellebody}%
|
|
wenzelm@9924
|
3 |
\def\isabellecontext{types}%
|
|
wenzelm@9673
|
4 |
\isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline
|
|
wenzelm@9673
|
5 |
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
|
|
nipkow@9933
|
6 |
\ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}%
|
|
nipkow@8749
|
7 |
\begin{isamarkuptext}%
|
|
nipkow@8749
|
8 |
\noindent\indexbold{*types}%
|
|
nipkow@8749
|
9 |
Internally all synonyms are fully expanded. As a consequence Isabelle's
|
|
nipkow@8749
|
10 |
output never contains synonyms. Their main purpose is to improve the
|
|
nipkow@8771
|
11 |
readability of theories. Synonyms can be used just like any other
|
|
nipkow@8749
|
12 |
type:%
|
|
nipkow@8749
|
13 |
\end{isamarkuptext}%
|
|
wenzelm@9673
|
14 |
\isacommand{consts}\ nand\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
|
|
wenzelm@9673
|
15 |
\ \ \ \ \ \ \ exor\ {\isacharcolon}{\isacharcolon}\ gate%
|
|
nipkow@8749
|
16 |
\begin{isamarkuptext}%
|
|
nipkow@8749
|
17 |
\subsection{Constant definitions}
|
|
nipkow@8749
|
18 |
\label{sec:ConstDefinitions}
|
|
nipkow@8749
|
19 |
\indexbold{definition}
|
|
nipkow@8749
|
20 |
|
|
nipkow@8749
|
21 |
The above constants \isa{nand} and \isa{exor} are non-recursive and can
|
|
nipkow@8749
|
22 |
therefore be defined directly by%
|
|
nipkow@8749
|
23 |
\end{isamarkuptext}%
|
|
wenzelm@9673
|
24 |
\isacommand{defs}\ nand{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
|
|
wenzelm@9673
|
25 |
\ \ \ \ \ exor{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{\isachardoublequote}%
|
|
nipkow@8749
|
26 |
\begin{isamarkuptext}%
|
|
nipkow@8749
|
27 |
\noindent%
|
|
nipkow@9792
|
28 |
where \isacommand{defs}\indexbold{*defs} is a keyword and
|
|
nipkow@9792
|
29 |
\isa{nand{\isacharunderscore}def} and \isa{exor{\isacharunderscore}def} are user-supplied names.
|
|
nipkow@8749
|
30 |
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
|
|
nipkow@9541
|
31 |
that must be used in constant definitions.
|
|
nipkow@8749
|
32 |
Declarations and definitions can also be merged%
|
|
nipkow@8749
|
33 |
\end{isamarkuptext}%
|
|
wenzelm@9673
|
34 |
\isacommand{constdefs}\ nor\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
|
|
wenzelm@9673
|
35 |
\ \ \ \ \ \ \ \ \ {\isachardoublequote}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isanewline
|
|
nipkow@10187
|
36 |
\ \ \ \ \ \ \ \ \ \ exor{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ gate\isanewline
|
|
nipkow@10187
|
37 |
\ \ \ \ \ \ \ \ \ {\isachardoublequote}exor{\isadigit{2}}\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymnot}A\ {\isasymor}\ {\isasymnot}B{\isacharparenright}{\isachardoublequote}%
|
|
nipkow@8749
|
38 |
\begin{isamarkuptext}%
|
|
nipkow@8749
|
39 |
\noindent\indexbold{*constdefs}%
|
|
nipkow@9792
|
40 |
in which case the default name of each definition is $f$\isa{{\isacharunderscore}def}, where
|
|
nipkow@8749
|
41 |
$f$ is the name of the defined constant.%
|
|
nipkow@8749
|
42 |
\end{isamarkuptext}%
|
|
nipkow@9722
|
43 |
\end{isabellebody}%
|
|
wenzelm@9145
|
44 |
%%% Local Variables:
|
|
wenzelm@9145
|
45 |
%%% mode: latex
|
|
wenzelm@9145
|
46 |
%%% TeX-master: "root"
|
|
wenzelm@9145
|
47 |
%%% End:
|