10788
|
1 |
(*<*)theory "types" = Main:(*>*)
|
|
2 |
types number = nat
|
9933
|
3 |
gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
|
|
4 |
('a,'b)alist = "('a \<times> 'b)list";
|
8745
|
5 |
|
11428
|
6 |
text{*\noindent
|
8745
|
7 |
Internally all synonyms are fully expanded. As a consequence Isabelle's
|
|
8 |
output never contains synonyms. Their main purpose is to improve the
|
8771
|
9 |
readability of theories. Synonyms can be used just like any other
|
11456
|
10 |
type. Here, we declare two constants of type \isa{gate}:
|
8745
|
11 |
*}
|
|
12 |
|
|
13 |
consts nand :: gate
|
10788
|
14 |
xor :: gate;
|
8745
|
15 |
|
10885
|
16 |
subsection{*Constant Definitions*}
|
8745
|
17 |
|
11428
|
18 |
text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
|
11456
|
19 |
The constants @{term"nand"} and @{term"xor"} above are non-recursive and can
|
|
20 |
be defined directly:
|
8745
|
21 |
*}
|
|
22 |
|
9933
|
23 |
defs nand_def: "nand A B \<equiv> \<not>(A \<and> B)"
|
10788
|
24 |
xor_def: "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B";
|
8745
|
25 |
|
|
26 |
text{*\noindent%
|
11456
|
27 |
Here \commdx{defs} is a keyword and
|
10788
|
28 |
@{thm[source]nand_def} and @{thm[source]xor_def} are user-supplied names.
|
8745
|
29 |
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
|
9541
|
30 |
that must be used in constant definitions.
|
11457
|
31 |
Pattern-matching is not allowed: each definition must be of
|
|
32 |
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
|
|
33 |
Section~\ref{sec:Simp-with-Defs} explains how definitions are used
|
|
34 |
in proofs.
|
|
35 |
|
11456
|
36 |
A \commdx{constdefs} command combines the effects of \isacommand{consts} and
|
|
37 |
\isacommand{defs}. For instance, we can introduce @{term"nand"} and @{term"xor"} by a
|
|
38 |
single command:
|
8745
|
39 |
*}
|
|
40 |
|
|
41 |
constdefs nor :: gate
|
9933
|
42 |
"nor A B \<equiv> \<not>(A \<or> B)"
|
10788
|
43 |
xor2 :: gate
|
|
44 |
"xor2 A B \<equiv> (A \<or> B) \<and> (\<not>A \<or> \<not>B)";
|
8745
|
45 |
|
11428
|
46 |
text{*\noindent
|
|
47 |
The default name of each definition is $f$@{text"_def"}, where
|
10788
|
48 |
$f$ is the name of the defined constant.*}
|
|
49 |
(*<*)end(*>*)
|