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