equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Typedef}% |
3 \def\isabellecontext{Typedef}% |
4 % |
4 % |
5 \isamarkupsection{Introducing new types} |
5 \isamarkupsection{Introducing new types% |
|
6 } |
6 % |
7 % |
7 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
8 \label{sec:adv-typedef} |
9 \label{sec:adv-typedef} |
9 By now we have seen a number of ways for introducing new types, for example |
10 By now we have seen a number of ways for introducing new types, for example |
10 type synonyms, recursive datatypes and records. For most applications, this |
11 type synonyms, recursive datatypes and records. For most applications, this |
16 Types in HOL must be non-empty; otherwise the quantifier rules would be |
17 Types in HOL must be non-empty; otherwise the quantifier rules would be |
17 unsound, because $\exists x. x=x$ is a theorem. |
18 unsound, because $\exists x. x=x$ is a theorem. |
18 \end{warn}% |
19 \end{warn}% |
19 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
20 % |
21 % |
21 \isamarkupsubsection{Declaring new types} |
22 \isamarkupsubsection{Declaring new types% |
|
23 } |
22 % |
24 % |
23 \begin{isamarkuptext}% |
25 \begin{isamarkuptext}% |
24 \label{sec:typedecl} |
26 \label{sec:typedecl} |
25 The most trivial way of introducing a new type is by a \bfindex{type |
27 The most trivial way of introducing a new type is by a \bfindex{type |
26 declaration}:% |
28 declaration}:% |
53 axioms, in which case you will be able to prove everything but it will mean |
55 axioms, in which case you will be able to prove everything but it will mean |
54 nothing. In the above case it also turns out that the axiomatic approach is |
56 nothing. In the above case it also turns out that the axiomatic approach is |
55 unnecessary: a one-element type called \isa{unit} is already defined in HOL.% |
57 unnecessary: a one-element type called \isa{unit} is already defined in HOL.% |
56 \end{isamarkuptext}% |
58 \end{isamarkuptext}% |
57 % |
59 % |
58 \isamarkupsubsection{Defining new types} |
60 \isamarkupsubsection{Defining new types% |
|
61 } |
59 % |
62 % |
60 \begin{isamarkuptext}% |
63 \begin{isamarkuptext}% |
61 \label{sec:typedef} |
64 \label{sec:typedef} |
62 Now we come to the most general method of safely introducing a new type, the |
65 Now we come to the most general method of safely introducing a new type, the |
63 \bfindex{type definition}. All other methods, for example |
66 \bfindex{type definition}. All other methods, for example |