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