11 We now start with the theory of ordering relations, which we shall phrase |
24 We now start with the theory of ordering relations, which we shall phrase |
12 in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} |
25 in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} |
13 to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we |
26 to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we |
14 introduce the class \isa{ordrel}:% |
27 introduce the class \isa{ordrel}:% |
15 \end{isamarkuptext}% |
28 \end{isamarkuptext}% |
16 \isamarkuptrue% |
29 \isamarkupfalse% |
17 \isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkupfalse% |
30 \isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkuptrue% |
18 % |
31 % |
19 \begin{isamarkuptext}% |
32 \begin{isamarkuptext}% |
20 \noindent |
33 \noindent |
21 This introduces a new class \isa{ordrel} and makes it a subclass of |
34 This introduces a new class \isa{ordrel} and makes it a subclass of |
22 the predefined class \isa{type}, which |
35 the predefined class \isa{type}, which |
23 is the class of all HOL types. |
36 is the class of all HOL types. |
24 This is a degenerate form of axiomatic type class without any axioms. |
37 This is a degenerate form of axiomatic type class without any axioms. |
25 Its sole purpose is to restrict the use of overloaded constants to meaningful |
38 Its sole purpose is to restrict the use of overloaded constants to meaningful |
26 instances:% |
39 instances:% |
27 \end{isamarkuptext}% |
40 \end{isamarkuptext}% |
28 \isamarkuptrue% |
41 \isamarkupfalse% |
29 \isacommand{consts}\ less\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isachardoublequote}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline |
42 \isacommand{consts}\ less\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isachardoublequote}\ \ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline |
30 \ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% |
43 \ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isamarkuptrue% |
31 % |
44 % |
32 \begin{isamarkuptext}% |
45 \begin{isamarkuptext}% |
33 \noindent |
46 \noindent |
34 Note that only one occurrence of a type variable in a type needs to be |
47 Note that only one occurrence of a type variable in a type needs to be |
35 constrained with a class; the constraint is propagated to the other |
48 constrained with a class; the constraint is propagated to the other |
37 |
50 |
38 So far there are no types of class \isa{ordrel}. To breathe life |
51 So far there are no types of class \isa{ordrel}. To breathe life |
39 into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of |
52 into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of |
40 \isa{ordrel}:% |
53 \isa{ordrel}:% |
41 \end{isamarkuptext}% |
54 \end{isamarkuptext}% |
|
55 \isamarkupfalse% |
|
56 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel% |
|
57 \isadelimproof |
|
58 % |
|
59 \endisadelimproof |
|
60 % |
|
61 \isatagproof |
42 \isamarkuptrue% |
62 \isamarkuptrue% |
43 \isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ ordrel\isamarkupfalse% |
|
44 % |
63 % |
45 \begin{isamarkuptxt}% |
64 \begin{isamarkuptxt}% |
46 \noindent |
65 \noindent |
47 Command \isacommand{instance} actually starts a proof, namely that |
66 Command \isacommand{instance} actually starts a proof, namely that |
48 \isa{bool} satisfies all axioms of \isa{ordrel}. |
67 \isa{bool} satisfies all axioms of \isa{ordrel}. |
49 There are none, but we still need to finish that proof, which we do |
68 There are none, but we still need to finish that proof, which we do |
50 by invoking the \methdx{intro_classes} method:% |
69 by invoking the \methdx{intro_classes} method:% |
51 \end{isamarkuptxt}% |
70 \end{isamarkuptxt}% |
|
71 \isamarkupfalse% |
|
72 \isacommand{by}\ intro{\isacharunderscore}classes% |
|
73 \endisatagproof |
|
74 {\isafoldproof}% |
|
75 % |
|
76 \isadelimproof |
|
77 % |
|
78 \endisadelimproof |
52 \isamarkuptrue% |
79 \isamarkuptrue% |
53 \isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse% |
|
54 % |
80 % |
55 \begin{isamarkuptext}% |
81 \begin{isamarkuptext}% |
56 \noindent |
82 \noindent |
57 More interesting \isacommand{instance} proofs will arise below |
83 More interesting \isacommand{instance} proofs will arise below |
58 in the context of proper axiomatic type classes. |
84 in the context of proper axiomatic type classes. |
59 |
85 |
60 Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say |
86 Although terms like \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} are now legal, we still need to say |
61 what the relation symbols actually mean at type \isa{bool}:% |
87 what the relation symbols actually mean at type \isa{bool}:% |
62 \end{isamarkuptext}% |
88 \end{isamarkuptext}% |
63 \isamarkuptrue% |
89 \isamarkupfalse% |
64 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
90 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline |
65 le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline |
91 le{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ \ {\isachardoublequote}P\ {\isacharless}{\isacharless}{\isacharequal}\ Q\ {\isasymequiv}\ P\ {\isasymlongrightarrow}\ Q{\isachardoublequote}\isanewline |
66 less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}\isamarkupfalse% |
92 less{\isacharunderscore}bool{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}P\ {\isacharless}{\isacharless}\ Q\ {\isasymequiv}\ {\isasymnot}P\ {\isasymand}\ Q{\isachardoublequote}\isamarkuptrue% |
67 % |
93 % |
68 \begin{isamarkuptext}% |
94 \begin{isamarkuptext}% |
69 \noindent |
95 \noindent |
70 Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:% |
96 Now \isa{False\ {\isacharless}{\isacharless}{\isacharequal}\ P} is provable:% |
71 \end{isamarkuptext}% |
97 \end{isamarkuptext}% |
|
98 \isamarkupfalse% |
|
99 \isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline |
|
100 % |
|
101 \isadelimproof |
|
102 % |
|
103 \endisadelimproof |
|
104 % |
|
105 \isatagproof |
|
106 \isamarkupfalse% |
|
107 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}% |
|
108 \endisatagproof |
|
109 {\isafoldproof}% |
|
110 % |
|
111 \isadelimproof |
|
112 % |
|
113 \endisadelimproof |
72 \isamarkuptrue% |
114 \isamarkuptrue% |
73 \isacommand{lemma}\ {\isachardoublequote}False\ {\isacharless}{\isacharless}{\isacharequal}\ P{\isachardoublequote}\isanewline |
|
74 \isamarkupfalse% |
|
75 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharunderscore}bool{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% |
|
76 % |
115 % |
77 \begin{isamarkuptext}% |
116 \begin{isamarkuptext}% |
78 \noindent |
117 \noindent |
79 At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. |
118 At this point, \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} is not even well-typed. |
80 To make it well-typed, |
119 To make it well-typed, |
81 we need to make lists a type of class \isa{ordrel}:% |
120 we need to make lists a type of class \isa{ordrel}:% |
82 \end{isamarkuptext}% |
121 \end{isamarkuptext}% |
83 \isamarkuptrue% |
122 % |
84 \isamarkupfalse% |
123 \isadelimtheory |
|
124 % |
|
125 \endisadelimtheory |
|
126 % |
|
127 \isatagtheory |
|
128 % |
|
129 \endisatagtheory |
|
130 {\isafoldtheory}% |
|
131 % |
|
132 \isadelimtheory |
|
133 % |
|
134 \endisadelimtheory |
85 \end{isabellebody}% |
135 \end{isabellebody}% |
86 %%% Local Variables: |
136 %%% Local Variables: |
87 %%% mode: latex |
137 %%% mode: latex |
88 %%% TeX-master: "root" |
138 %%% TeX-master: "root" |
89 %%% End: |
139 %%% End: |