1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Overloading{\isadigit{0}}}% |
3 \def\isabellecontext{Overloading{\isadigit{0}}}% |
4 \isamarkupfalse% |
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 \isamarkuptrue% |
5 % |
18 % |
6 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
7 We start with a concept that is required for type classes but already |
20 We start with a concept that is required for type classes but already |
8 useful on its own: \emph{overloading}. Isabelle allows overloading: a |
21 useful on its own: \emph{overloading}. Isabelle allows overloading: a |
9 constant may have multiple definitions at non-overlapping types.% |
22 constant may have multiple definitions at non-overlapping types.% |
16 % |
29 % |
17 \begin{isamarkuptext}% |
30 \begin{isamarkuptext}% |
18 If we want to introduce the notion of an \emph{inverse} for arbitrary types we |
31 If we want to introduce the notion of an \emph{inverse} for arbitrary types we |
19 give it a polymorphic type% |
32 give it a polymorphic type% |
20 \end{isamarkuptext}% |
33 \end{isamarkuptext}% |
21 \isamarkuptrue% |
34 \isamarkupfalse% |
22 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isamarkupfalse% |
35 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isamarkuptrue% |
23 % |
36 % |
24 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
25 \noindent |
38 \noindent |
26 and provide different definitions at different instances:% |
39 and provide different definitions at different instances:% |
27 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
28 \isamarkuptrue% |
41 \isamarkupfalse% |
29 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
42 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
30 inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline |
43 inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline |
31 inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline |
44 inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline |
32 inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
45 inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
33 % |
46 % |
34 \begin{isamarkuptext}% |
47 \begin{isamarkuptext}% |
35 \noindent |
48 \noindent |
36 Isabelle will not complain because the three definitions do not overlap: no |
49 Isabelle will not complain because the three definitions do not overlap: no |
37 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a |
50 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a |
46 However, there is nothing to prevent the user from forming terms such as |
59 However, there is nothing to prevent the user from forming terms such as |
47 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about |
60 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about |
48 unspecified constants does not endanger soundness, but it is pointless. |
61 unspecified constants does not endanger soundness, but it is pointless. |
49 To prevent such terms from even being formed requires the use of type classes.% |
62 To prevent such terms from even being formed requires the use of type classes.% |
50 \end{isamarkuptext}% |
63 \end{isamarkuptext}% |
51 \isamarkuptrue% |
64 % |
52 \isamarkupfalse% |
65 \isadelimtheory |
|
66 % |
|
67 \endisadelimtheory |
|
68 % |
|
69 \isatagtheory |
|
70 % |
|
71 \endisatagtheory |
|
72 {\isafoldtheory}% |
|
73 % |
|
74 \isadelimtheory |
|
75 % |
|
76 \endisadelimtheory |
53 \end{isabellebody}% |
77 \end{isabellebody}% |
54 %%% Local Variables: |
78 %%% Local Variables: |
55 %%% mode: latex |
79 %%% mode: latex |
56 %%% TeX-master: "root" |
80 %%% TeX-master: "root" |
57 %%% End: |
81 %%% End: |