9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{types}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
17175
|
17 |
\isacommand{types}\isamarkupfalse%
|
40406
|
18 |
\ number\ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
|
|
19 |
\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
20 |
\ \ \ \ \ \ {\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}}%
|
8749
|
21 |
\begin{isamarkuptext}%
|
11428
|
22 |
\noindent
|
8749
|
23 |
Internally all synonyms are fully expanded. As a consequence Isabelle's
|
|
24 |
output never contains synonyms. Their main purpose is to improve the
|
8771
|
25 |
readability of theories. Synonyms can be used just like any other
|
27015
|
26 |
type.%
|
8749
|
27 |
\end{isamarkuptext}%
|
17175
|
28 |
\isamarkuptrue%
|
27015
|
29 |
%
|
10878
|
30 |
\isamarkupsubsection{Constant Definitions%
|
10788
|
31 |
}
|
11866
|
32 |
\isamarkuptrue%
|
10788
|
33 |
%
|
8749
|
34 |
\begin{isamarkuptext}%
|
11428
|
35 |
\label{sec:ConstDefinitions}\indexbold{definitions}%
|
27015
|
36 |
Nonrecursive definitions can be made with the \commdx{definition}
|
|
37 |
command, for example \isa{nand} and \isa{xor} gates
|
|
38 |
(based on type \isa{gate} above):%
|
8749
|
39 |
\end{isamarkuptext}%
|
17175
|
40 |
\isamarkuptrue%
|
27015
|
41 |
\isacommand{definition}\isamarkupfalse%
|
40406
|
42 |
\ 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
|
27015
|
43 |
\isacommand{definition}\isamarkupfalse%
|
40406
|
44 |
\ 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}}%
|
8749
|
45 |
\begin{isamarkuptext}%
|
|
46 |
\noindent%
|
|
47 |
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
|
9541
|
48 |
that must be used in constant definitions.
|
11457
|
49 |
Pattern-matching is not allowed: each definition must be of
|
|
50 |
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
|
|
51 |
Section~\ref{sec:Simp-with-Defs} explains how definitions are used
|
40406
|
52 |
in proofs. The default name of each definition is $f$\isa{{\isaliteral{5F}{\isacharunderscore}}def}, where
|
8749
|
53 |
$f$ is the name of the defined constant.%
|
|
54 |
\end{isamarkuptext}%
|
17175
|
55 |
\isamarkuptrue%
|
17056
|
56 |
%
|
|
57 |
\isadelimtheory
|
|
58 |
%
|
|
59 |
\endisadelimtheory
|
|
60 |
%
|
|
61 |
\isatagtheory
|
|
62 |
%
|
|
63 |
\endisatagtheory
|
|
64 |
{\isafoldtheory}%
|
|
65 |
%
|
|
66 |
\isadelimtheory
|
|
67 |
%
|
|
68 |
\endisadelimtheory
|
9722
|
69 |
\end{isabellebody}%
|
9145
|
70 |
%%% Local Variables:
|
|
71 |
%%% mode: latex
|
|
72 |
%%% TeX-master: "root"
|
|
73 |
%%% End:
|