17914
|
1 |
(*<*)theory "types" imports Main begin(*>*)
|
42765
|
2 |
type_synonym number = nat
|
|
3 |
type_synonym gate = "bool \<Rightarrow> bool \<Rightarrow> bool"
|
|
4 |
type_synonym ('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
|
27015
|
10 |
type.
|
8745
|
11 |
*}
|
|
12 |
|
10885
|
13 |
subsection{*Constant Definitions*}
|
8745
|
14 |
|
11428
|
15 |
text{*\label{sec:ConstDefinitions}\indexbold{definitions}%
|
27015
|
16 |
Nonrecursive definitions can be made with the \commdx{definition}
|
|
17 |
command, for example @{text nand} and @{text xor} gates
|
|
18 |
(based on type @{typ gate} above):
|
8745
|
19 |
*}
|
|
20 |
|
27015
|
21 |
definition nand :: gate where "nand A B \<equiv> \<not>(A \<and> B)"
|
|
22 |
definition xor :: gate where "xor A B \<equiv> A \<and> \<not>B \<or> \<not>A \<and> B"
|
8745
|
23 |
|
|
24 |
text{*\noindent%
|
|
25 |
The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
|
9541
|
26 |
that must be used in constant definitions.
|
11457
|
27 |
Pattern-matching is not allowed: each definition must be of
|
|
28 |
the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
|
|
29 |
Section~\ref{sec:Simp-with-Defs} explains how definitions are used
|
27015
|
30 |
in proofs. The default name of each definition is $f$@{text"_def"}, where
|
10788
|
31 |
$f$ is the name of the defined constant.*}
|
|
32 |
(*<*)end(*>*)
|