1 (*<*) |
1 (*<*) |
2 theory "types" = Main:; |
2 theory "types" = Main:; |
3 (*>*)types number = nat |
3 (*>*)types number = nat |
4 gate = "bool \\<Rightarrow> bool \\<Rightarrow> bool" |
4 gate = "bool \<Rightarrow> bool \<Rightarrow> bool" |
5 ('a,'b)alist = "('a * 'b)list"; |
5 ('a,'b)alist = "('a \<times> 'b)list"; |
6 |
6 |
7 text{*\noindent\indexbold{*types}% |
7 text{*\noindent\indexbold{*types}% |
8 Internally all synonyms are fully expanded. As a consequence Isabelle's |
8 Internally all synonyms are fully expanded. As a consequence Isabelle's |
9 output never contains synonyms. Their main purpose is to improve the |
9 output never contains synonyms. Their main purpose is to improve the |
10 readability of theories. Synonyms can be used just like any other |
10 readability of theories. Synonyms can be used just like any other |
21 |
21 |
22 The above constants @{term"nand"} and @{term"exor"} are non-recursive and can |
22 The above constants @{term"nand"} and @{term"exor"} are non-recursive and can |
23 therefore be defined directly by |
23 therefore be defined directly by |
24 *} |
24 *} |
25 |
25 |
26 defs nand_def: "nand A B \\<equiv> \\<not>(A \\<and> B)" |
26 defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)" |
27 exor_def: "exor A B \\<equiv> A \\<and> \\<not>B \\<or> \\<not>A \\<and> B"; |
27 exor_def: "exor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"; |
28 |
28 |
29 text{*\noindent% |
29 text{*\noindent% |
30 where \isacommand{defs}\indexbold{*defs} is a keyword and |
30 where \isacommand{defs}\indexbold{*defs} is a keyword and |
31 @{thm[source]nand_def} and @{thm[source]exor_def} are user-supplied names. |
31 @{thm[source]nand_def} and @{thm[source]exor_def} are user-supplied names. |
32 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality |
32 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality |
33 that must be used in constant definitions. |
33 that must be used in constant definitions. |
34 Declarations and definitions can also be merged |
34 Declarations and definitions can also be merged |
35 *} |
35 *} |
36 |
36 |
37 constdefs nor :: gate |
37 constdefs nor :: gate |
38 "nor A B \\<equiv> \\<not>(A \\<or> B)" |
38 "nor A B \<equiv> \<not>(A \<or> B)" |
39 exor2 :: gate |
39 exor2 :: gate |
40 "exor2 A B \\<equiv> (A \\<or> B) \\<and> (\\<not>A \\<or> \\<not>B)"; |
40 "exor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)"; |
41 |
41 |
42 text{*\noindent\indexbold{*constdefs}% |
42 text{*\noindent\indexbold{*constdefs}% |
43 in which case the default name of each definition is $f$@{text"_def"}, where |
43 in which case the default name of each definition is $f$@{text"_def"}, where |
44 $f$ is the name of the defined constant.*}(*<*) |
44 $f$ is the name of the defined constant.*}(*<*) |
45 end |
45 end |