5 |
5 |
6 text{*\noindent |
6 text{*\noindent |
7 Internally all synonyms are fully expanded. As a consequence Isabelle's |
7 Internally all synonyms are fully expanded. As a consequence Isabelle's |
8 output never contains synonyms. Their main purpose is to improve the |
8 output never contains synonyms. Their main purpose is to improve the |
9 readability of theories. Synonyms can be used just like any other |
9 readability of theories. Synonyms can be used just like any other |
10 type: |
10 type. Here, we declare two constants of type \isa{gate}: |
11 *} |
11 *} |
12 |
12 |
13 consts nand :: gate |
13 consts nand :: gate |
14 xor :: gate; |
14 xor :: gate; |
15 |
15 |
16 subsection{*Constant Definitions*} |
16 subsection{*Constant Definitions*} |
17 |
17 |
18 text{*\label{sec:ConstDefinitions}\indexbold{definitions}% |
18 text{*\label{sec:ConstDefinitions}\indexbold{definitions}% |
19 The above constants @{term"nand"} and @{term"xor"} are non-recursive and can |
19 The constants @{term"nand"} and @{term"xor"} above are non-recursive and can |
20 therefore be defined directly by |
20 be defined directly: |
21 *} |
21 *} |
22 |
22 |
23 defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)" |
23 defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)" |
24 xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"; |
24 xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"; |
25 |
25 |
26 text{*\noindent% |
26 text{*\noindent% |
27 where \commdx{defs} is a keyword and |
27 Here \commdx{defs} is a keyword and |
28 @{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names. |
28 @{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names. |
29 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality |
29 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality |
30 that must be used in constant definitions. |
30 that must be used in constant definitions. |
31 Declarations and definitions can also be merged in a \commdx{constdefs} |
31 A \commdx{constdefs} command combines the effects of \isacommand{consts} and |
32 command: |
32 \isacommand{defs}. For instance, we can introduce @{term"nand"} and @{term"xor"} by a |
|
33 single command: |
33 *} |
34 *} |
34 |
35 |
35 constdefs nor :: gate |
36 constdefs nor :: gate |
36 "nor A B \<equiv> \<not>(A \<or> B)" |
37 "nor A B \<equiv> \<not>(A \<or> B)" |
37 xor2 :: gate |
38 xor2 :: gate |