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